Tests by plug feature SeqSelectSeq; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
d2264019d545a58a8e329e8c95cbe31a9bd452c2	Apalache	Eq	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
036395d9a932a162f931801bf3e53fb5dfc92b6e	Apalache	Eq	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
57ddae4faa7688e1a829612639c5683ebf9ade0f	Apalache	Ne	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
e135ae16d86d8cc19139e240b9371027431119ca	Apalache	Ne	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b25a4c8bb58e4e677155665542395ffbc924abfd	Apalache	Let	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
4d59222795212edde98c3b0c160b744dbaba3efa	Apalache	Let	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9c59e90ccae8e4973f8f3f30d3586cae2b1b90df	Apalache	Set0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
1c41ff0260fb3135a5fd9b033cc2015deb351905	Apalache	Set0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9768e298ca19225c19dca27acea3e4fd8b56f62f	Apalache	Set1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
6d54d2fe045a6c9ec7b1aba6872e69a683b801c3	Apalache	Set1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
bd29f794563a4148726da6bb1f7f0f056496f24f	Apalache	Set2	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
340812dcf5e72a8c14bdd3c1cf3a12d104553271	Apalache	Set2	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
354b4f947ba95d064f441642357c905db8d27778	Apalache	Fun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
f99f31602f7284497ecab0a3c67bab1082e6e6af	Apalache	Fun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
e7d72d3d122b51c75d999e9ecc61a144a45927e7	Apalache	In	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
8d69c357ebc1b38631dc7e156176a95858a064ed	Apalache	In	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
f046944f185202ccfdf1b2d0f6e50b743a36c160	Apalache	NotIn	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
8fa20b32538e5b6a1f04e55bb7ff07182b369d55	Apalache	NotIn	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
ca01f5266f1ce3eba37df0ae49afab127a3de75c	Apalache	Record	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
efba664b33757c127b9c6e78f5b69020772907cc	Apalache	Record	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
641eab039c25e6192c002c69d91c082609031cae	Apalache	Tuple	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b61066b4c2c8d54249334c3039e89ae20d47e205	Apalache	Tuple	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
5b1c24f643cd7c8adb5efb999276e12386d5d2fb	Apalache	FunApp	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
dddaca85247635af0faa78b6aade46c8d676271d	Apalache	FunApp	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b442dd12a710bd97d202a80ba096b922714e3c54	Apalache	Except0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
cd006e55d4cb3f2c85f57d649eb9280bfc3fa397	Apalache	Except0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
f59c6b67fbc30bff8a54a5d1c9965a72c3826d6c	Apalache	Except1Fun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
d4ac9749d4ef4008fbba90ad8125e6850dcbb2ef	Apalache	Except1Fun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
daf954018497f939746e3de7004cda4b2b41f755	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
d85159e97b68d4584ca162256dc7564aeccd4175	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
8a81e1fc5b26452ccc72f66e5e06e45ea636bff6	Apalache	Except1Rec	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
d9a284c3fc9468a8a85a94b55c94d49b486c9602	Apalache	Except1Rec	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
f9a10f220a4b09fb9ade82ec671d40dcc611e573	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
7f3bfbf6b82f2dc7bceeaa0a750ac303cdfc8173	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
45d8f4f6067f677409261345f2136349212771a4	Apalache	Except2Fun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
dc922bff4a8e7c091757bcd1b87ec783651deae6	Apalache	Except2Fun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
148dbf857b187bb18dd094bf84ec9498434d81bf	Apalache	Prime	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
abf2bef8af699d2bb28c87439a15e216cea05040	Apalache	Prime	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
4899934771de3887c364bad91f0f48ddf7d3beee	Apalache	DefFun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
04cb2573f37bd8b157d38fd705928a424ad161c0	Apalache	DefFun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
fc0d0ce2d316ee062469dcdd7f60a87f1b3403aa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
cef28e0bfbb4e190e83a65cee5c1ff9491926cef	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
590e96f02a140397a1a1fc973ff2671d02dc2130	Apalache	DefFunRecursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
64fb2b98de0ab6cdedbfbc4e7f5cf8f4d27bda5b	Apalache	DefFunRecursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b60863e8fa523f6bb3019189fc7cf9c5ed7f49e6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
8ffd89fe74c97ea3dc3206c17a0b38a3443d4c58	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
58b9caf356c49c5fefff6328caf701719aaa190e	Apalache	Def0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
e5cc19f3675e539ffe6ebfb86aaf1424d94894c4	Apalache	Def0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
cab37156c097f1780f03fdf3f44ca51390fa61a4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
74850950ad7cfc35cc3c7ba0aef674aa44ea69fd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
6d66a1733a02619b49553b1bea833a08e93c1849	Apalache	Def1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a74cd0e79928c5dc26221929e5fa019d93057f96	Apalache	Def1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9342f474dfe01adf76913fccba186e4a630efcfe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
5fc3a3935d307010ad1f6545533667833b25acb0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
29b72352e353fcd5b7e54f3104afdd61739627f4	Apalache	Def2	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a0274fefb9975a3124c878787412e784a6eece82	Apalache	Def2	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
4477e25a4b5a941edaf34f8a629422058b69265c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
fee4033cdb7f4a8732f6027724b2772459b7b981	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
f167c50ea629db74e9e78749218b223cf2542368	Apalache	Def1Recursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
77400583aac0950cef55082320bbd8153fb317f7	Apalache	Def1Recursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
8f4fa34b514e94975382642bd058b942844c0d28	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
6cb4f4f2b337e7056421b7b686dd959cea54b869	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
61d55e5c3342d3def03cc5597cdbfbb709771efc	Apalache	Extends	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
ab60f89af34fbea7ab6fbab26d5ffa881d96b3b4	Apalache	Extends	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
c0604fc4dd0fe6c39b58534d4c625b3cb7cbfd6e	Apalache	ExtendsInDifferentFolder	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b53ca58f7ee42a74fd321a87dfd9326088d01907	Apalache	ExtendsInDifferentFolder	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9b1d42aa6be75762f1024fdb0b9086c35e247a5b	Apalache	Variable	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
fc83f55d4016f5f6ace639dde98a4fc50fd8ff01	Apalache	Variable	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
dbfa64d0be849f58174473f3273d4be61e5b6e62	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
c9ba567129bdd2e3b73adf8ae50d8a0a8fb1481e	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
2206e5689b7c578f6accf457e58405fa11f42e27	Apalache	Constant	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
f02be9160f4b487b4dbce060ed3cd5866fd2e49a	Apalache	Constant	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
7f313049a1486005fae87ad25dcf6966959b39e0	Apalache	ConstantRank1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
661d4eca6fa1ab10dd56a222892cbb8e99fa35fe	Apalache	ConstantRank1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9d4e871d764c1a17572a1e227a005d33c8040a2b	Apalache	Instance	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
34767839c9846db997f675ad6a299612d2dd9984	Apalache	Instance	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
2b450a1ce7dc644c8436bab04a676c01e99b01d7	Apalache	InstanceWith	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a9e8ba236f38d71886fe776953a4d6c216a3898e	Apalache	InstanceWith	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
64d4b3a1df104447e0b19d9715ce58c26aae0345	Apalache	InstanceNamed	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
08b6f93f4a86267952a74416f95972656bb8ed27	Apalache	InstanceNamed	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
c7f3de89765e2b9d97586e642833aad78097c6c3	Apalache	InstanceNamedWith	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
0fce704c2593cf29714d7c3c179c2357e5df8444	Apalache	InstanceNamedWith	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
d60911eaedb70cc62ff04023826436f900010c69	Apalache	InstanceInFolder	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
28b2c0244f2587a542dd46253bfd279d266847e4	Apalache	InstanceInFolder	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
39d144a8de99713c7a8c8cac3c9b8a3a0177fc8f	Apalache	InstanceWithInFolder	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
c5a8a4378e8dfb51c89618414ad877fcf1d86860	Apalache	InstanceWithInFolder	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
0af4e024b002fea39d620a3f6dc08e8f0b58ee60	Apalache	InstanceNamedInFolder	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
87b8d942fd861720a718a53c9ff3fb6bfe9d95bf	Apalache	InstanceNamedInFolder	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
32164d0e93dc9b01428f174dade7f9492c62e3f1	Apalache	InstanceNamedWithInFolder	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
17de8a2578cbf949d845d6b71310b6881eca0088	Apalache	InstanceNamedWithInFolder	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
bd15ecf3f087dd933cb121156e68458ec9676b56	Apalache	Lambda	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
36ce90cb715e0c4aecb36002c0e6d2a15291534c	Apalache	Lambda	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
11a4fb8816fe4c611a67aa8041fbb1be6294d88f	Apalache	IfThen	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b3ad32c6b644a1f4e0928d641b633c7cd1e658c4	Apalache	IfThen	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
eb370a4e54f4c53cb7ecd0f5c644de3e4e7cd620	Apalache	IfElse	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
0a162de42c5b28d7c01b15ab0aaecaa9737059e0	Apalache	IfElse	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9ff1b4a3b930a634d4d8de9e86c083f431ebb444	Apalache	Unchanged	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b3c9b22c1c48be85af186865cee7ace0aed49930	Apalache	Unchanged	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
a44d9c1c62bc2b30dd71572730e32891c5517769	Apalache	SeqLen	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
fe6960ac5a5d9e752defd281c54f66a235606f39	Apalache	SeqLen	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
c59260440f907275e2ddc9f3439545af383ba222	Apalache	SeqConcat	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
e957fe82076f1a2ec4c576fc8cf6cccd9bc70246	Apalache	SeqConcat	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
5f482122aa155f4736d0a88870229a8acf4ee220	Apalache	SeqSelectSeq	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a3ebbedded9e5fdd8ff926122493e2401b1ed431	Apalache	SeqSelectSeq	SeqSelectSeq	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
4a67e2058979f9b391e17ddd47e90c8a258b13ba	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
3bc637de7714bcc3b4cd030f98c78027d802299a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
40d62eacf502c33771ecb74bb4cd47339b96277e	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
5ed755d6827b28d8937e5cbdcdfa5c5a431cd1bc	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b7e3bac6740131f826ebf9cf735977a5647e6e4e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
2e72033788f05aff3bc909e25f8cfdb4733a571f	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b829c0c562b7461848f3c14e2e6651f4f0c59dbf	Apalache	BagBagIn	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
561b9c41ebf81222f84797ac5dbdcc98b1485aa5	Apalache	BagBagIn	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
7bc86b360c40434cf594fcbf5bbe371175e8642c	Apalache	BagCopiesIn	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
7fe35e46ca6a3441c618cb094071f6069ed4cb9e	Apalache	BagCopiesIn	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
448c6384156cfeb120ee68712030a30fd861d6f0	Apalache	SeqHead	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
88bed97c90c5b355e28a1cc478ed2e1e850d9b29	Apalache	SeqHead	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
395d1c9ecfe3d128db6494c255600a72be21546d	Apalache	SeqTail	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
37c072d0ed2772e18571bb9ea87f0ba943c6acb9	Apalache	SeqTail	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9f6f0b6ad5da2a94debf6dce8c468464169c5f4f	Apalache	SeqAppend	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
26cc42d7ab8cf0c888a451e9898a5751dc4e055a	Apalache	SeqAppend	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model

Index

Tests by plug feature SeqSelectSeq; CLI Option: -workers 1