Tests by case feature SeqSubSeq; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
d1e747ec3c7a5c9d6fb06c3ac566da6d57992a74	Apalache	SeqSubSeq	Let	True	Passed	Model Under Test Equivalent Model
766b5df459c36e496a923d08dc7b11ceb603ef40	Apalache	SeqSubSeq	Let	False	Passed	Model Under Test Equivalent Model
234188b033ded1618e0f591b8552a67858bc4d1d	Apalache	SeqSubSeq	Choose	True	Passed	Model Under Test Equivalent Model
b759927d9666a8b5c0a6a1c00be97cd266ec679b	Apalache	SeqSubSeq	Choose	False	Passed	Model Under Test Equivalent Model
1c7a90e7867dae2bafae5d89705a2928b44982ed	Apalache	SeqSubSeq	Tuple	True	Passed	Model Under Test Equivalent Model
512390bfe5fd5686789861005e015a24877fac66	Apalache	SeqSubSeq	Tuple	False	Passed	Model Under Test Equivalent Model
241439717be0ec493be023b444bdb8c4262c80ed	Apalache	SeqSubSeq	TupleEmpty	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
40db46ac9db7ea5895d1f9d252f78ddbeed1317f	Apalache	SeqSubSeq	TupleEmpty	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
1ed5b3da6d2d149d6755d064826b322541a10192	Apalache	SeqSubSeq	FunApp	True	Passed	Model Under Test Equivalent Model
90959f858809186b8b95d65774dc90fe5e8034ef	Apalache	SeqSubSeq	FunApp	False	Passed	Model Under Test Equivalent Model
94feca230080b5db33510cc25ff24c51b9db97d5	Apalache	SeqSubSeq	Prime	True	Passed	Model Under Test Equivalent Model
18ff2e878980780658e2866e3bb32ae6dafbd2c7	Apalache	SeqSubSeq	Prime	False	Passed	Model Under Test Equivalent Model
e482c5a76e7f757e9d4a414b2d9e947d4f9f9d5a	Apalache	SeqSubSeq	NumZero	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
82060af70766c1abbf3b87848db5bee5b514b36c	Apalache	SeqSubSeq	NumZero	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
726325b520e82c006380d04a24dcf17bf1d9834a	Apalache	SeqSubSeq	NumOne	True	Passed	Model Under Test Equivalent Model
373cca992eb0e29812249508b873113a7cec3d2c	Apalache	SeqSubSeq	NumOne	False	Passed	Model Under Test Equivalent Model
77f419d906715a262d36e7d9af1eb2e46acab58c	Apalache	SeqSubSeq	NumMaxInt	True	Passed	Model Under Test Equivalent Model
89020b2a9bb6d995df448e5e034d98a5cae6359b	Apalache	SeqSubSeq	NumMaxInt	False	Passed	Model Under Test Equivalent Model
50780b1b4f662f20b8e04a43041b58e8c99cb876	Apalache	SeqSubSeq	NumUnaryMinus	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
bf75ac824a18bbf6c47d7f496587d59835eca063	Apalache	SeqSubSeq	NumUnaryMinus	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
c004d0c433ac4626002bb8c2fb45db23a34f6546	Apalache	SeqSubSeq	NumPlus	True	Passed	Model Under Test Equivalent Model
3988fbbf3fe45775e0ca396a293deb4c326a951e	Apalache	SeqSubSeq	NumPlus	False	Passed	Model Under Test Equivalent Model
30760c62c4c515dac8cb3b45cf0ece18a2d02e2e	Apalache	SeqSubSeq	NumMinus	True	Passed	Model Under Test Equivalent Model
3352bc8719aede252b6668197d144e9ae8643ec1	Apalache	SeqSubSeq	NumMinus	False	Passed	Model Under Test Equivalent Model
27095c4e108bbc811443a650826876fc40049bcc	Apalache	SeqSubSeq	NumMul	True	Passed	Model Under Test Equivalent Model
0d785598c3fb971cba09cae4effd466ef40d9cb8	Apalache	SeqSubSeq	NumMul	False	Passed	Model Under Test Equivalent Model
4dc4bb2a7a64aa2925dbe0ae5e4faeffa3a68691	Apalache	SeqSubSeq	NumDiv	True	Passed	Model Under Test Equivalent Model
92bd49dbafaa2bb441dcc58dcf2b480dbb38403f	Apalache	SeqSubSeq	NumDiv	False	Passed	Model Under Test Equivalent Model
3ec1b130d755a4171f0ea760edbdb6c70a983152	Apalache	SeqSubSeq	NumMod	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
40bd407efeb40fb2903926bdab5cf529bacfed8a	Apalache	SeqSubSeq	NumMod	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
cb15ca43d2519d7a325ecef9af44eb766f67513e	Apalache	SeqSubSeq	NumPow	True	Passed	Model Under Test Equivalent Model
14f1060904ff679444510b93b9e7b1b537121362	Apalache	SeqSubSeq	NumPow	False	Passed	Model Under Test Equivalent Model
3542e22feddeb747531034083bfbc09b9471a81c	Apalache	SeqSubSeq	Def0	True	Passed	Model Under Test Equivalent Model
905de5c5d9be96733e791dd6d371108725216364	Apalache	SeqSubSeq	Def0	False	Passed	Model Under Test Equivalent Model
d93b1e15b4febeccaaaceb1c58c33899f5e96053	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
7b8bded5feb7525b85f09a92fb8195153ea255fd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
c06e0952c28b9e3fa7658007502819bd0fd29b05	Apalache	SeqSubSeq	Def1	True	Passed	Model Under Test Equivalent Model
5c814dac5eca60d3aa983dd99af96c776706e5d0	Apalache	SeqSubSeq	Def1	False	Passed	Model Under Test Equivalent Model
8fc67867d0120d3fa4fc5a60b062e23675bf3cdf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
59daa828ff800d116a5320d7690b62a915081ac0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
a397cd65a10e1a946ff46d597d99fed54f7e056a	Apalache	SeqSubSeq	Def2	True	Passed	Model Under Test Equivalent Model
78df63a1cd3c18a3ba9028100be58a65990ef9be	Apalache	SeqSubSeq	Def2	False	Passed	Model Under Test Equivalent Model
c30b86d8f9fc9e8996adf1d7beb014a9f680127a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
d5362ef550cacec3dce07db10feada68855e4ccc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
67b73efeafdde041147a92d5b095bf7c2f4f0b68	Apalache	SeqSubSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1b093c337cb30207a1d55d3aa80a5a080f8aeabf	Apalache	SeqSubSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
40d6a9c07b3448c4b7cd9b3e1814f2d449fe20f5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
afed273d15478ddb7c0650ff2e8a5c2f28b49695	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
3cb53ffc8e44fb3e779ebbf234500b755454049b	Apalache	SeqSubSeq	Extends	True	Passed	Model Under Test Equivalent Model
8c3f7bcf7a53442e254b8ee1a7f0a733ad93b28d	Apalache	SeqSubSeq	Extends	False	Passed	Model Under Test Equivalent Model
f7df2e85e8dcbd0cc5733f10d7fda0a36c1ad488	Apalache	SeqSubSeq	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
5e8b88254b69709b07d8adf22e8713125773929c	Apalache	SeqSubSeq	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
29b6e713779e7cc2b21d11c44038e9a085e5f19b	Apalache	SeqSubSeq	Variable	True	Passed	Model Under Test Equivalent Model
2aeb4a55225d71e7e9f206946beb8149750e334d	Apalache	SeqSubSeq	Variable	False	Passed	Model Under Test Equivalent Model
c9f34e957e523e32e31204e9b2c910a24faeb11d	Apalache	SeqSubSeq	Constant	True	Passed	Model Under Test Equivalent Model
ace8d0edac134c6b10b8033578c5560a409efdf0	Apalache	SeqSubSeq	Constant	False	Passed	Model Under Test Equivalent Model
742ea498c1140cb1115f9b0cf39d5c9e94d72759	Apalache	SeqSubSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
37ec52b864e13fe693dd6bb3d01db0a0a9c98ba1	Apalache	SeqSubSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
04ec840541e29cbef2d15303d4f2c6530eebde14	Apalache	SeqSubSeq	Instance	True	Passed	Model Under Test Equivalent Model
88800836821f5fbf37aa9fdf72c15c355da03eaa	Apalache	SeqSubSeq	Instance	False	Passed	Model Under Test Equivalent Model
3576219cc61cbccdfb2486ab3b1c79663b71f905	Apalache	SeqSubSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
349e0d989497c0184457b157a0033d1e08fc5949	Apalache	SeqSubSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
7c703b7e4da9f24b88adda48e5e35bbfbdaaea00	Apalache	SeqSubSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
1465ca8b0c3fe0625e03a8e5e7cfde60fb5bbf77	Apalache	SeqSubSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d445b48016754746555a13000849fd247c49dcfc	Apalache	SeqSubSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
beb660ba3506f4b78ad04e02674a72f1b375b968	Apalache	SeqSubSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d28a4ba8e0feb864e428f113f0eb4f1cb7fb746a	Apalache	SeqSubSeq	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
e730254c3b488e04653784b0bdf46c1972ec9e6d	Apalache	SeqSubSeq	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
c050113ad09d5c03ef19ca624f5664608a8c0535	Apalache	SeqSubSeq	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
3d5999c7c490edf147106557a7072c9c08a41f83	Apalache	SeqSubSeq	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
14eaddbb9883289036064f8a9b3ac0fe654d0fb5	Apalache	SeqSubSeq	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
f7048deb67a78881ace9d2f0f19912f0f8111365	Apalache	SeqSubSeq	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
9baf57751678527fc8209e583dd384442c5b57ca	Apalache	SeqSubSeq	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
f4aa53be0486ad32811fd89144efa17cf07f2060	Apalache	SeqSubSeq	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
f9f4eaafd2815e134fdc5bcc31d1cb4a0e258fe7	Apalache	SeqSubSeq	IfCond	True	Passed	Model Under Test Equivalent Model
36441e3673aceb7636fba3b399e261fbf63a873f	Apalache	SeqSubSeq	IfCond	False	Passed	Model Under Test Equivalent Model
d3c2cfaeeeb2c82150599c240ba89099d3ad029d	Apalache	SeqSubSeq	IfThen	True	Passed	Model Under Test Equivalent Model
ee141f9431588c5e353feb8c292f8a1269c8abbb	Apalache	SeqSubSeq	IfThen	False	Passed	Model Under Test Equivalent Model
04d3b01d339770a79b74fd1653011769d8980e33	Apalache	SeqSubSeq	IfElse	True	Passed	Model Under Test Equivalent Model
3e25695f6f555867be38f6659b512f18c0f56900	Apalache	SeqSubSeq	IfElse	False	Passed	Model Under Test Equivalent Model
598ac9f2427e7fb3e20383fb5ec45968216f431b	Apalache	SeqSubSeq	SeqLen	True	Passed	Model Under Test Equivalent Model
1169139ea84fe6806dfb312ee6a8476e60981b14	Apalache	SeqSubSeq	SeqLen	False	Passed	Model Under Test Equivalent Model
ab5739439a2474d4671140cea8b204def228e8b9	Apalache	SeqSubSeq	SeqConcat	True	Passed	Model Under Test Equivalent Model
ffd9f92596c46f4d30730d73c7f42787f6070ca2	Apalache	SeqSubSeq	SeqConcat	False	Passed	Model Under Test Equivalent Model
ba2101d766b4f51927f83a7b76befa0cea7c0724	Apalache	SeqSubSeq	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
732dd9faad08253be834b828b6fc5ff4f3d59834	Apalache	SeqSubSeq	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
2aaae43ae019cc97313dc5bb7e11517d5876a96d	Apalache	SeqSubSeq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e37b75cee1d86e9444f39b5bdef927b39c326b13	Apalache	SeqSubSeq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
886f69c526ea5e3362b7ea3f78a58a52a25f6dbb	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	SeqSubSeq	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
36b4c5cf69806ea7d8f4eedfd514f1ac8396f4c5	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	SeqSubSeq	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
eeacd5151e46d1952eae028cbd54d5df62783447	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqSubSeq	TlcEval	True	Passed	Model Under Test Equivalent Model
360fedd5ea70e7d1d8d35efd6112171bb7ff9041	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqSubSeq	TlcEval	False	Passed	Model Under Test Equivalent Model
186a484931432d9055cc55ea9908f4b619eb4e68	Apalache	SeqSubSeq	BagCopiesIn	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations	Model Under Test Equivalent Model
1e51fed60a710cf8752f73c807de2510e96a90fe	Apalache	SeqSubSeq	BagCopiesIn	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations	Model Under Test Equivalent Model
7149c3fce30b4e7f1113fa456e68f9f91da8b634	Apalache	SeqSubSeq	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7836a91f9e124b7bea77d0aad9c7cd8eaf8f7da9	Apalache	SeqSubSeq	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
de71f078dc1cf95544350453cd7d3136555f1023	Apalache	SeqSubSeq	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
a81a7371c7aa6131ce2c9a56fe41e323c57e6b99	Apalache	SeqSubSeq	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
05893f40ad00e7a82f92d83e9f07d464ea6a9c95	Apalache	SeqSubSeq	SeqHead	True	Passed	Model Under Test Equivalent Model
62df1eb406f01047e91a3d62c36e810656b324a1	Apalache	SeqSubSeq	SeqHead	False	Passed	Model Under Test Equivalent Model
093b5c2b34aba6e26c00c1c26704f40caadb0ddd	Apalache	SeqSubSeq	SeqTail	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
899e9ddba7041cce422b9427fc6de31ff23e1c06	Apalache	SeqSubSeq	SeqTail	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
3d8d17a8e5919843f8d02a7e909bad2638721163	Apalache	SeqSubSeq	SeqAppend	True	Passed	Model Under Test Equivalent Model
535900323370181632623f7d7439c7cfd914b4f3	Apalache	SeqSubSeq	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

Tests by case feature SeqSubSeq; CLI Option: -workers 1