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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
27ea8cc797a27b9576fff3251ea0047c47aede30	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Unchanged	OneLineComment	True	Passed	Model Under Test Equivalent Model
37517ea222a7547d9498ad9724a80b7985193ec8	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Unchanged	OneLineComment	False	Passed	Model Under Test Equivalent Model
f35a4f52b7cd7e53d644a7d57b0efd61dc00ec4c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Unchanged	MultiLineComment	True	Passed	Model Under Test Equivalent Model
2d988fac5c5b9167de80cbe4dbb9441b1d1af04d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Unchanged	MultiLineComment	False	Passed	Model Under Test Equivalent Model
907c0b0dd3b24047bf843593bc70c0523b3917e6	Apalache	Unchanged	BoolTrue	True	Passed	Model Under Test Equivalent Model
449e553aa186882f43f78c3974620e0889b2cfe2	Apalache	Unchanged	BoolTrue	False	Passed	Model Under Test Equivalent Model
7137701d9d4f237c49e230393f1cf631a97e3acf	Apalache	Unchanged	BoolFalse	True	Passed	Model Under Test Equivalent Model
275975f93f366be21edb0ec793efb487a51cf8d1	Apalache	Unchanged	BoolFalse	False	Passed	Model Under Test Equivalent Model
78ce367b918580626c077764c2ebf057c7011353	Apalache	Unchanged	BoolSet	True	Passed	Model Under Test Equivalent Model
3b2fa7f5b2264d42dbd9d31a7800a5b28943e6af	Apalache	Unchanged	BoolSet	False	Passed	Model Under Test Equivalent Model
e3d147f6643207195e76e489d5165145e20d2675	Apalache	Unchanged	And	True	Passed	Model Under Test Equivalent Model
8060a873668e669c3194bc616182b7d8640ca796	Apalache	Unchanged	And	False	Passed	Model Under Test Equivalent Model
ce77f0585d7f22a3faa9bacbc4f1c24311082775	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Unchanged	AndMultiLine	True	Passed	Model Under Test Equivalent Model
ad3b7ec9cdce87c4d387b4dda7f8867494241836	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Unchanged	AndMultiLine	False	Passed	Model Under Test Equivalent Model
ae5f0c660fd08a74d59b76bd479452e58938378d	Apalache	Unchanged	Imply	True	Passed	Model Under Test Equivalent Model
4c840fd127d3c80f18266dc5a8dda943747578d4	Apalache	Unchanged	Imply	False	Passed	Model Under Test Equivalent Model
f4a5fc7eca8c1027815dc7867e0364e46b827e2c	Apalache	Unchanged	Not	True	Passed	Model Under Test Equivalent Model
320a7eb5a4eee1bbf9f3ae33ba578b5d563630cb	Apalache	Unchanged	Not	False	Passed	Model Under Test Equivalent Model
e33310394c96ca0f2cf25ab9efb233e4e48e9907	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Unchanged	Or	True	Passed	Model Under Test Equivalent Model
4549f67ddb9f740722e147a68525b86aedbe8414	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Unchanged	Or	False	Passed	Model Under Test Equivalent Model
e5f630dde641fb0af090c64db2414e4d3abaf659	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Unchanged	OrMultiLine	True	Passed	Model Under Test Equivalent Model
5c77e7583531794722ce6064b960203fffd1b1b9	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Unchanged	OrMultiLine	False	Passed	Model Under Test Equivalent Model
1640384b0eb710e7c24d50ea30085a17c82b29e7	Apalache	Unchanged	Eq	True	Passed	Model Under Test Equivalent Model
fcdb3bb0b5136b6cd66df14082800aeae2447c4f	Apalache	Unchanged	Eq	False	Passed	Model Under Test Equivalent Model
7f5c36348d5a1d63d43d4ddfefaf3723a21ff36a	Apalache	Unchanged	Ne	True	Passed	Model Under Test Equivalent Model
0f3e43bfee46e311f1839542826c7332c3c60653	Apalache	Unchanged	Ne	False	Passed	Model Under Test Equivalent Model
003334938af7ce3cb5790a15f71e4dfcb968ff40	Apalache	Unchanged	Let	True	Passed	Model Under Test Equivalent Model
507babf81908513f9989538f2522016d589591c3	Apalache	Unchanged	Let	False	Passed	Model Under Test Equivalent Model
9c1dccd591dcadf61b5f110032f7b00daaf2b7dc	Apalache	Unchanged	SetEmpty	True	Passed	Model Under Test Equivalent Model
eb878da153699e74ad48a31e8f654e437d06d538	Apalache	Unchanged	SetEmpty	False	Passed	Model Under Test Equivalent Model
d84b4bed8c9f0c555dcfc34d913adb28a3112bd0	Apalache	Unchanged	Set0	True	Passed	Model Under Test Equivalent Model
cbc4a5be7cd7c7ef205fd62932ac4ca7765f910c	Apalache	Unchanged	Set0	False	Passed	Model Under Test Equivalent Model
f08d94f1a9d33a9d9ea53abc9bd0c593c785bad5	Apalache	Unchanged	Set1	True	Passed	Model Under Test Equivalent Model
39b8b66c66b9cf762dd66539e6e7ae2069741c44	Apalache	Unchanged	Set1	False	Passed	Model Under Test Equivalent Model
760ac35a9218a12b065fdcccb2c3381bb042f40c	Apalache	Unchanged	Set2	True	Passed	Model Under Test Equivalent Model
586160080189793d3323b4814ca5808f22047758	Apalache	Unchanged	Set2	False	Passed	Model Under Test Equivalent Model
88f4c1921665a28d318278e9c0fd395b5f32ef19	Apalache	Unchanged	Fun	True	Passed	Model Under Test Equivalent Model
36393cb1cc83a9a2addedf9e0975305ab0698bf7	Apalache	Unchanged	Fun	False	Passed	Model Under Test Equivalent Model
362d84ef158476d53f6f31fc2ca7ed41436a90fc	Apalache	Unchanged	In	True	Passed	Model Under Test Equivalent Model
d455de00f151cc556105cea8c81303cc547f6d6a	Apalache	Unchanged	In	False	Passed	Model Under Test Equivalent Model
fc860f6e8786856a5efe0dbd5bf6761f6eed538c	Apalache	Unchanged	NotIn	True	Passed	Model Under Test Equivalent Model
074de848c60abb1d4a8475d5a64702e6a54b8aad	Apalache	Unchanged	NotIn	False	Passed	Model Under Test Equivalent Model
a3dc6f4e5c0ce209b268896de09141016a614c27	Apalache	Unchanged	Exists	True	Passed	Model Under Test Equivalent Model
be4dba9edb3d94702ce677095eedf378c7dc0ae3	Apalache	Unchanged	Exists	False	Passed	Model Under Test Equivalent Model
16b703f30baeb30e753aa7bcffa428886a12e292	Apalache	Unchanged	Forall	True	Passed	Model Under Test Equivalent Model
dd53a7c885f258dc26597aabb2bf62a5cbe7d8d5	Apalache	Unchanged	Forall	False	Passed	Model Under Test Equivalent Model
1a2ce90cbfc7090462d85dde389a82fda0bf35ff	Apalache	Unchanged	Choose	True	Passed	Model Under Test Equivalent Model
43fb6293783f18ede51c5c4b5407623d2f421446	Apalache	Unchanged	Choose	False	Passed	Model Under Test Equivalent Model
ddba1b51cc626c14ccb75cb5db28e6280950d72b	Apalache	Unchanged	Record	True	Passed	Model Under Test Equivalent Model
4d28427625d1c6c01aa0368dc3c2de5f1e235af6	Apalache	Unchanged	Record	False	Passed	Model Under Test Equivalent Model
ed596c878767f0613231056bba7d8e0d213d96be	Apalache	Unchanged	Tuple	True	Passed	Model Under Test Equivalent Model
e1839c8263d417e7be8d28a3e3cff0d2267ad1e5	Apalache	Unchanged	Tuple	False	Passed	Model Under Test Equivalent Model
67c5b0e7e0e2c53660b8766c4f85fa7ef4197250	Apalache	Unchanged	TupleEmpty	True	Passed	Model Under Test Equivalent Model
2feba8bd6617b2c53760fef8e4fa118e8fac3ff8	Apalache	Unchanged	TupleEmpty	False	Passed	Model Under Test Equivalent Model
1614c9eb8dd255a743c7b103504fcd7d5bdf71e2	Apalache	Unchanged	FunApp	True	Passed	Model Under Test Equivalent Model
731b346250042a577830d007f2652c3d3e2e8539	Apalache	Unchanged	FunApp	False	Passed	Model Under Test Equivalent Model
d8dbd14e750f63f4c0ef00069bf06116e3e77532	Apalache	Unchanged	NumZero	True	Passed	Model Under Test Equivalent Model
c9ba94cf49ce2fcba0bfb3bcba7132cae3d85655	Apalache	Unchanged	NumZero	False	Passed	Model Under Test Equivalent Model
319d75a4d17cadcfda36fc444e80118471dba43b	Apalache	Unchanged	NumOne	True	Passed	Model Under Test Equivalent Model
661a8ebd0e83fce658ef372ac953b00f3b7c868a	Apalache	Unchanged	NumOne	False	Passed	Model Under Test Equivalent Model
0d474d9e155934031f2ecde9ea0407be01f33288	Apalache	Unchanged	NumMaxInt	True	Passed	Model Under Test Equivalent Model
020e89bc8fe5d90191df87a358b15ccad688fe1f	Apalache	Unchanged	NumMaxInt	False	Passed	Model Under Test Equivalent Model
34f216851bafbfa6fd247fad906724ed69ee961c	Apalache	Unchanged	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
26970a6c1d939aeecfa77c00c588e6cb2a31e89d	Apalache	Unchanged	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
7eb958e5f683c9f7b761ff8af65045156e9e9aa8	Apalache	Unchanged	NumPlus	True	Passed	Model Under Test Equivalent Model
420e7cb8bab02c43bfa7d11efac5db33bae11437	Apalache	Unchanged	NumPlus	False	Passed	Model Under Test Equivalent Model
74ee154898d690b63ecbc92d31d5d7cd4ed144a0	Apalache	Unchanged	NumMinus	True	Passed	Model Under Test Equivalent Model
9a56759a1619c7e1c001d7a8bbb66535583cec78	Apalache	Unchanged	NumMinus	False	Passed	Model Under Test Equivalent Model
f18a93408628b748d37ed43370523f32699651ba	Apalache	Unchanged	NumMul	True	Passed	Model Under Test Equivalent Model
2055e715429ec8643a3a404ac748c0d783fed5f6	Apalache	Unchanged	NumMul	False	Passed	Model Under Test Equivalent Model
876a341b56c873345abf803e2d7a2d22c492070f	Apalache	Unchanged	NumDiv	True	Passed	Model Under Test Equivalent Model
1a83ffdf73a413695a23f66355adc4ee987893e9	Apalache	Unchanged	NumDiv	False	Passed	Model Under Test Equivalent Model
8a2150dc1efd9abb2166f41841f808d54ab4ba8c	Apalache	Unchanged	NumMod	True	Passed	Model Under Test Equivalent Model
3c4359b8aad191ee9579d34685b160e78223b205	Apalache	Unchanged	NumMod	False	Passed	Model Under Test Equivalent Model
7bc1a1c463c10945f36333182488050ab9ee6f0c	Apalache	Unchanged	NumPow	True	Passed	Model Under Test Equivalent Model
c6070ce971a46f471597c71d3b6dbf4802c457d6	Apalache	Unchanged	NumPow	False	Passed	Model Under Test Equivalent Model
3a4b9b9842ff4c5bb2ce29ebac3777d50b7d42d2	Apalache	Unchanged	NumGt	True	Passed	Model Under Test Equivalent Model
f7e9f7b49f5039a4c1e02725f5dc0820abbef066	Apalache	Unchanged	NumGt	False	Passed	Model Under Test Equivalent Model
4e2da392d4f230021a719d3bd09cfe8c3ca814db	Apalache	Unchanged	NumGe	True	Passed	Model Under Test Equivalent Model
1eb4f6ccb1c8c2149c6dab09e55cb59840a532ce	Apalache	Unchanged	NumGe	False	Passed	Model Under Test Equivalent Model
d51b6e8af0eb43caf767f869b585bc87f33239e4	Apalache	Unchanged	NumLt	True	Passed	Model Under Test Equivalent Model
5907748f02e79e4f313d875ec32ba84c19912d8f	Apalache	Unchanged	NumLt	False	Passed	Model Under Test Equivalent Model
4c741d7dd1b9802614e2404d525e4d1b4b96a7a6	Apalache	Unchanged	NumLe	True	Passed	Model Under Test Equivalent Model
9ff4d061f27fb3da95c079c64662abfdbe79e600	Apalache	Unchanged	NumLe	False	Passed	Model Under Test Equivalent Model
fa278160b598e47aa11457b371f951ba782dbb59	Apalache	Unchanged	DefFun	True	Passed	Model Under Test Equivalent Model
d0476ea6622b69055860a7fd7ed49436d4787e64	Apalache	Unchanged	DefFun	False	Passed	Model Under Test Equivalent Model
968792eb9f9b19d9b5d2e54b2a1211525ba28807	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDefFun	True	Passed	Model Under Test Equivalent Model
2ee804910705d1883ea223438c8be7c52efa31c0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDefFun	False	Passed	Model Under Test Equivalent Model
aefc3d3ca8b4a0a9e8dda1473532c702474ada1b	Apalache	Unchanged	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
db2a5a8113f292de8ce39804fa06bdb1374b501b	Apalache	Unchanged	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
622caa38f5d24ffcd59886fb35a90f5343a6a610	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
4dd0365e5bd98b8a12699783197b5bb37da33454	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
0c35a8524613d5b6bfbbef0466557eedb9878afe	Apalache	Unchanged	Def0	True	Passed	Model Under Test Equivalent Model
4b032ca039d38c33c3e0d5e3864e2a0aee8bdc44	Apalache	Unchanged	Def0	False	Passed	Model Under Test Equivalent Model
36fc78817411522e3967925f5371c6bf1e08604c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef0	True	Passed	Model Under Test Equivalent Model
f419f75565a4fffca9749f6c1d9d7e23ba140ec7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef0	False	Passed	Model Under Test Equivalent Model
ffc1e5bebd25c1f77f8cddf5699278727605d6a7	Apalache	Unchanged	Def1	True	Passed	Model Under Test Equivalent Model
cd09d08ad2e47f571da0984b5d1d98fa09cd1a9d	Apalache	Unchanged	Def1	False	Passed	Model Under Test Equivalent Model
6c3a098f026584f6efd43a44bf8a10cd76b26ae5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1	True	Passed	Model Under Test Equivalent Model
e778a12b440b57fe5e928e3a3cfbdad5e248a0cb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1	False	Passed	Model Under Test Equivalent Model
838959dc26a00232bf6e13ebe06325ba71fd7f27	Apalache	Unchanged	Def2	True	Passed	Model Under Test Equivalent Model
e00a2330640d07f707c26438aee9918dc7b50f63	Apalache	Unchanged	Def2	False	Passed	Model Under Test Equivalent Model
675bbbd310c6af76dbeb029c8f05addfaf08e482	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef2	True	Passed	Model Under Test Equivalent Model
f1085eb72b0ec0f2e1d28319a20af4f73f1b9b4b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef2	False	Passed	Model Under Test Equivalent Model
7398422264a9641f23c013f9cc22e5fac8de6560	Apalache	Unchanged	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f154f450f54419423a65fc74f7b60292e5164d36	Apalache	Unchanged	Def1Recursive	False	Passed	Model Under Test Equivalent Model
aab3cae8aadd478ab78153563e9582501ff12bf4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
8c9fda13fd00e63a6367843419e68eebf770c6b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
1f779cceb6b95e6b39a910b5a9b29c6395bbbfea	Apalache	Unchanged	Extends	True	Passed	Model Under Test Equivalent Model
4920126b5eb2d33531f80b789c8c4717d136447c	Apalache	Unchanged	Extends	False	Passed	Model Under Test Equivalent Model
2bdc1c3a5e9fb3a6d39ae171ee02974335336e25	Apalache	Unchanged	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
93c1ad208958c9a446029aaacff502ebb6b5f9b0	Apalache	Unchanged	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
a110750136d046336d0a5077f28cefa7d7a38605	Apalache	Unchanged	Variable	True	Failed: TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op	Model Under Test Equivalent Model
d621f2ef4ad3be8f4e084ccd91d1730804f2a9c8	Apalache	Unchanged	Variable	False	Failed: TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op	Model Under Test Equivalent Model
b9fc716dc414c457bda393f396c72352a64ed398	Apalache	Unchanged	Instance	True	Passed	Model Under Test Equivalent Model
5c166d960f03709d8f54d6d02cc810bfeaf0fe91	Apalache	Unchanged	Instance	False	Passed	Model Under Test Equivalent Model
6b9b5ed99856fce626f22ec4735e8eac9b2704fd	Apalache	Unchanged	InstanceWith	True	Passed	Model Under Test Equivalent Model
079f7772e9e702042eed60fe1896128f3d6b81ad	Apalache	Unchanged	InstanceWith	False	Passed	Model Under Test Equivalent Model
56eac6979e6510bcde3778c663e0ddb2810982f8	Apalache	Unchanged	InstanceNamed	True	Passed	Model Under Test Equivalent Model
a259b384905924afd2f73c1834564834197f6c6d	Apalache	Unchanged	InstanceNamed	False	Passed	Model Under Test Equivalent Model
ab1008325129beea78743bc02d00a58aa0bbd33b	Apalache	Unchanged	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
59f17fc9546dab1303a2265f6d295b1f3456c428	Apalache	Unchanged	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
594ce72e4cbfea4c0fe53b00cc79bfaad1840b87	Apalache	Unchanged	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
10f348700faf3907563dd6dd81cb4c2c93285f4e	Apalache	Unchanged	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
4ce61b79cc6c2c979a4bca8dfec08ee82c4761c7	Apalache	Unchanged	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
c2f3dc394d837e6bb268251f0958e5c75dac0416	Apalache	Unchanged	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
c19dc41d78579d186596b7f8a2b04d2336a217e7	Apalache	Unchanged	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
0480a205b35ca368c2a8608737d616fe3886ecdf	Apalache	Unchanged	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
3dd60b73c76ce3c1956b86530fa9cb9d1912ca44	Apalache	Unchanged	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
dce637e7838bc6c6bfc32df67437264f8acea86a	Apalache	Unchanged	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
aecd62247f2bb92624dbe4a35ea90747cb65c0b1	Apalache	Unchanged	Enabled	True	Passed	Model Under Test Equivalent Model
20b2eb9be8284c3cdab84954defe757af34ad3e5	Apalache	Unchanged	Enabled	False	Passed	Model Under Test Equivalent Model
d48eb14d757d039e3b1ca5b4176cf09fbe38527b	Apalache	Unchanged	Cross2	True	Passed	Model Under Test Equivalent Model
399931044d316b24936b3a983d1b1b32ec68f021	Apalache	Unchanged	Cross2	False	Passed	Model Under Test Equivalent Model
bc2de906152d7cd7940872d23844630952abb37c	Apalache	Unchanged	Cross3	True	Passed	Model Under Test Equivalent Model
b4a824abeb520d664498dd19a6f2f785b853ebfe	Apalache	Unchanged	Cross3	False	Passed	Model Under Test Equivalent Model
e092c52fd9219cdceac4ad8034a6f2ffdf248fcd	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	Unchanged	FunSet	True	Passed	Model Under Test Equivalent Model
66d7e2e33e6c10d8f5df08fcaf43f297fdbc559a	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	Unchanged	FunSet	False	Passed	Model Under Test Equivalent Model
f18a5ef80ad60191732713ce3e234ad57c45e0f0	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	Unchanged	RecordSet	True	Passed	Model Under Test Equivalent Model
587ae28a774fe1698bc4895f62dbf2d196ba9dea	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	Unchanged	RecordSet	False	Passed	Model Under Test Equivalent Model
16db14eb8ad901c74cc83d7d9d4292c30d1ed09b	Apalache	Unchanged	SetDiff	True	Passed	Model Under Test Equivalent Model
417b1d111581830fa3784f7250be697b9b0120e5	Apalache	Unchanged	SetDiff	False	Passed	Model Under Test Equivalent Model
30fddc9f66948bf4b17fe85b952c4891364fdf1b	Apalache	Unchanged	SetUnion	True	Passed	Model Under Test Equivalent Model
2dbe8b675f99dbd294ef85c37da1f035f0b34dd3	Apalache	Unchanged	SetUnion	False	Passed	Model Under Test Equivalent Model
75e25dce835b23a0ab5325d4fbe1c390b670d38f	Apalache	Unchanged	SetIntersect	True	Passed	Model Under Test Equivalent Model
71d5615b68c25df07f4cc98be73c39b1c5dd4663	Apalache	Unchanged	SetIntersect	False	Passed	Model Under Test Equivalent Model
5c22900208f11ded0b3612bbdbbf4133578f81da	Apalache	Unchanged	SubsetEq	True	Passed	Model Under Test Equivalent Model
e64115a60d9efd0732b29639d370d946f3a8893a	Apalache	Unchanged	SubsetEq	False	Passed	Model Under Test Equivalent Model
d18ac0dd74402d75a27478cbe694067d9c0c6131	Apalache	Unchanged	IfCond	True	Passed	Model Under Test Equivalent Model
163314ebd441da67c2e024eda41f7137ade244af	Apalache	Unchanged	IfCond	False	Passed	Model Under Test Equivalent Model
0794f119f42045b612c5e8f4668e850883bea330	Apalache	Unchanged	IfThen	True	Passed	Model Under Test Equivalent Model
bf98381c4247ea4366786bbb013407f4e6f97f64	Apalache	Unchanged	IfThen	False	Passed	Model Under Test Equivalent Model
946d12972bd8ac31711db23e1757673a0bbc46b0	Apalache	Unchanged	IfElse	True	Passed	Model Under Test Equivalent Model
a1fc8a6ca2113ebe6701fad9b5ae3d0ac62da500	Apalache	Unchanged	IfElse	False	Passed	Model Under Test Equivalent Model
700c2575640ae4d7617d37281ea76a06bf4251c3	Apalache	Unchanged	Subset	True	Passed	Model Under Test Equivalent Model
c80bb031fdafd09e1b867929d46b9496387f558f	Apalache	Unchanged	Subset	False	Passed	Model Under Test Equivalent Model
4b48970a3bf447cf9d889b092a9aae95900a4360	Apalache	Unchanged	Domain	True	Passed	Model Under Test Equivalent Model
5f222c49307290dedbc4a4e2778d8d2d7a058a67	Apalache	Unchanged	Domain	False	Passed	Model Under Test Equivalent Model
676c7e4bebed62fe6db3b6d58d7b18675000ec1c	Apalache	Unchanged	Union	True	Passed	Model Under Test Equivalent Model
a1f728dec85c13da31a3b84cfaa7352f390220ff	Apalache	Unchanged	Union	False	Passed	Model Under Test Equivalent Model
69e950190d7be5019960506170fa39f4b016425b	Apalache	Unchanged	Equivalence	True	Passed	Model Under Test Equivalent Model
ab2282ee5e8acaea6bcf347420e51efef564a2dd	Apalache	Unchanged	Equivalence	False	Passed	Model Under Test Equivalent Model
f8a1a3ff88646e25bb94d1ffc52637f407337f41	Apalache	Unchanged	StringEmpty	True	Passed	Model Under Test Equivalent Model
e1c673dbdd7ab0b85946be0ceb368c95401e5dae	Apalache	Unchanged	StringEmpty	False	Passed	Model Under Test Equivalent Model
973c9b479c0b444833ef980ba6e365b47bc0011b	Apalache	Unchanged	String	True	Passed	Model Under Test Equivalent Model
aa534e35baf1457e3d88f2d484a4ca58f85865d9	Apalache	Unchanged	String	False	Passed	Model Under Test Equivalent Model
83dedf2cce82780b2aa9e10853d7a12aa9ac7c83	Apalache	Unchanged	SeqLen	True	Passed	Model Under Test Equivalent Model
3b792ece826a2c385b8aae552dfbe1bfceb164fe	Apalache	Unchanged	SeqLen	False	Passed	Model Under Test Equivalent Model
e824578f8641bece609c142ad631a5283ec26c12	Apalache	Unchanged	SeqConcat	True	Passed	Model Under Test Equivalent Model
582da95962268d365c45cc32cdd81da3d26ab89e	Apalache	Unchanged	SeqConcat	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
b388d862ebade989d278455ea8f9a3d9bd174e94	Apalache	Unchanged	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
8afa93f864ea08d2e4dd71b71989bd5cf6cb98be	Apalache	Unchanged	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
7d080790c06c78851e148a2c0edbc606c2e78177	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	Unchanged	NumRange	True	Passed	Model Under Test Equivalent Model
9cad26a4d5cfc1e9ae86c88eebffa88f6554acb6	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	Unchanged	NumRange	False	Passed	Model Under Test Equivalent Model
b6b6764679be654f3ead094a2201a5eed2a760ed	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Unchanged	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
8124cd779c4edbb79410d424003f95e3513a0511	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Unchanged	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
00d60feebec5a26a2a054d6bdc4fd5bfdf0e9a42	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Unchanged	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
e8e823b105a418a9121aa47c9d1c20c5bbb3f964	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Unchanged	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
5250615f8595ae39c4c80ec5bb9bd41f4728bfb6	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Unchanged	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
792e9973f88d9afeb94e013bcb70b03047c58029	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Unchanged	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
b97ce502da3b27a62ff3c4364a5bf89cd438eb1a	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Unchanged	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
cf9a047b8c29f18917809b7ba028b1ede46362f8	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Unchanged	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
8fbdc2ca01409032e36d1b38f9a14c27eb7a75d3	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Unchanged	TlcEval	True	Passed	Model Under Test Equivalent Model
c27a99a06016bcab67f1d7d202dab5df59209d5e	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Unchanged	TlcEval	False	Passed	Model Under Test Equivalent Model
3b49dc2d739367f860892233979bf45a9f1306f9	Apalache	Unchanged	BagBagToSet	True	Passed	Model Under Test Equivalent Model
070952983d9d3dd2e5878f33d919812c0e575ff9	Apalache	Unchanged	BagBagToSet	False	Passed	Model Under Test Equivalent Model
fcada1a3f4d3fa34e73e41271cfb48e7e029dac9	Apalache	Unchanged	BagSetToBag	True	Passed	Model Under Test Equivalent Model
596f422690f90545bdfb20e682bc3861b7909d0a	Apalache	Unchanged	BagSetToBag	False	Passed	Model Under Test Equivalent Model
49de5024a17f6805499012d2dd4f0aa437fa593b	Apalache	Unchanged	BagBagIn	True	Passed	Model Under Test Equivalent Model
9cbe9b2aace2caf37b49dd63bab526d68772eda2	Apalache	Unchanged	BagBagIn	False	Passed	Model Under Test Equivalent Model
395d274b07e5afe1771278559610b3421eff614d	Apalache	Unchanged	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
ef202553887ff4bd4c58ee22a1d1ffb270de52eb	Apalache	Unchanged	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
0a2302f7e188dce196fde2874bc57052ad1c47b9	Apalache	Unchanged	BagAddBag	True	Passed	Model Under Test Equivalent Model
0449dc412abec44b1e8ab4f15e8cdb89dff32c30	Apalache	Unchanged	BagAddBag	False	Passed	Model Under Test Equivalent Model
aa8724c23d635152d5d312c0bfccfe9124c55238	Apalache	Unchanged	BagBagSub	True	Passed	Model Under Test Equivalent Model
f14839cca164ddd68daa55b0813a283fc9457b50	Apalache	Unchanged	BagBagSub	False	Passed	Model Under Test Equivalent Model
fa24b8eba8669bce889812250925a2ce3622721c	Apalache	Unchanged	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1a189c172d156041819f94c8ce6a002e97ecdfc8	Apalache	Unchanged	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
399fc70f3e43c2fe54ffc8b3ddd099ce4b59c895	Apalache	Unchanged	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
1b86764624ea111c6e35e8b89269ddc0505f67b5	Apalache	Unchanged	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4fbcd1893d012e11b3776e105ac391a20699dfec	Apalache	Unchanged	BagBagUnion	True	Passed	Model Under Test Equivalent Model
cee437dc20c8f874cb9772580f1070672f6b900f	Apalache	Unchanged	BagBagUnion	False	Passed	Model Under Test Equivalent Model
965dc40492d8c5063c701b46463cef5159a9531e	Apalache	Unchanged	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
fcb29ccb383331b23c5ca7e1f39aec4a0400c196	Apalache	Unchanged	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e2e6455b879eb3ac6aa4854cad99014a7ccd8fd6	Apalache	Unchanged	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
4255256bc71876913fec393fff9c65115eeec19b	Apalache	Unchanged	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
92ba00b9a467fb4a25ba73d8c52876ea93e3dd74	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Unchanged	BagSubBag	True	Passed	Model Under Test Equivalent Model
1ecb02748154e0da60e6cd32b8665426ab58e6bf	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Unchanged	BagSubBag	False	Passed	Model Under Test Equivalent Model
d3330548ab08d6b5195a20c8b72507eb07a2d94c	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Unchanged	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
0adda875c19ba0c50d9061c92a3b7308af607de3	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Unchanged	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
f632fdebdd4759745a6c6a5e6492c7cf1bf07990	Apalache	Unchanged	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
2f2724edd3ff661625d818094b9d8188f5cf4d3d	Apalache	Unchanged	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
dc7ebb2bccfa5f51ca711740c38725f3bfa266f0	Apalache	Unchanged	SeqHead	True	Passed	Model Under Test Equivalent Model
86ff6237e717cd65b3a160c26e9f1be943b3e09f	Apalache	Unchanged	SeqHead	False	Passed	Model Under Test Equivalent Model
486ee5c024c31a69b10dce2ea66b542cedce161a	Apalache	Unchanged	SeqTail	True	Passed	Model Under Test Equivalent Model
85c7c78b7a91810a8724e7917f404b45c475aaf7	Apalache	Unchanged	SeqTail	False	Passed	Model Under Test Equivalent Model
cdf855eae24d8a2f7eec91351c69752e0ceb597d	Apalache	Unchanged	SeqAppend	True	Passed	Model Under Test Equivalent Model
dab557c306a94737fd39913c9c0f93672375d9bf	Apalache	Unchanged	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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