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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
22f58a0b5dcdf96c4fbc3a0af270f70f2009d92d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Enabled	OneLineComment	True	Passed	Model Under Test Equivalent Model
5662fcd924cc95d827aeefb3bd7d9bf45085bc1a	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Enabled	OneLineComment	False	Passed	Model Under Test Equivalent Model
f17c61a23dc66a3b7835d9090ea262e0e7fd8a19	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Enabled	MultiLineComment	True	Passed	Model Under Test Equivalent Model
a0fb4984288cd5bf763f8fe6f5b2e51b847f8200	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Enabled	MultiLineComment	False	Passed	Model Under Test Equivalent Model
f85a8c8b070809cb0f54c081da908852bbb949be	Apalache	Enabled	BoolTrue	True	Passed	Model Under Test Equivalent Model
aca89d8f9ace59a5fd7716214cc8866242eb7135	Apalache	Enabled	BoolTrue	False	Passed	Model Under Test Equivalent Model
5d9425415c79d7fd9b6407f9eb3d100716e6bc2a	Apalache	Enabled	BoolFalse	True	Passed	Model Under Test Equivalent Model
e5d7e351f1d2a4c04a6827d0297b2a90db5011ce	Apalache	Enabled	BoolFalse	False	Passed	Model Under Test Equivalent Model
0e0801a307b1c0a412c0f4c8046aa0eeeb3004de	Apalache	Enabled	And	True	Passed	Model Under Test Equivalent Model
c326c874e88d400492ee29585f7efd473e0ccccd	Apalache	Enabled	And	False	Passed	Model Under Test Equivalent Model
fc40a23a7cfcf3b4b1a4cfd1174c6e78d8b4faec	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Enabled	AndMultiLine	True	Passed	Model Under Test Equivalent Model
7584c8631a4dad88b160ffa72bef7471f80977b5	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Enabled	AndMultiLine	False	Passed	Model Under Test Equivalent Model
a9fe40438fb217276a7bd536330d7fe3f8ead9c1	Apalache	Enabled	Imply	True	Passed	Model Under Test Equivalent Model
c5996b3bf82ef51af8153188648262311bb5caff	Apalache	Enabled	Imply	False	Passed	Model Under Test Equivalent Model
89c236159a0cbea584b1c43cc58659ca793b66d9	Apalache	Enabled	Not	True	Passed	Model Under Test Equivalent Model
37e0a8995dbf39dc7b9d9ebccd61406092d03c0d	Apalache	Enabled	Not	False	Passed	Model Under Test Equivalent Model
a0b767d5f28b5e27b01a71fa5af25e752f61b517	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Enabled	Or	True	Passed	Model Under Test Equivalent Model
6aa95382a31b80f4e46a30c21e567449d53522a3	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Enabled	Or	False	Passed	Model Under Test Equivalent Model
898b38422efe231f327253a96c03687cfc2ed8ce	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Enabled	OrMultiLine	True	Passed	Model Under Test Equivalent Model
20012c629a6d49dca37b1e12a441e0088c1fbe0e	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Enabled	OrMultiLine	False	Passed	Model Under Test Equivalent Model
27f472e093c8a635e3e4390daf7cb786cc269747	Apalache	Enabled	Eq	True	Passed	Model Under Test Equivalent Model
8657dd6d24a934fa4741c759a9aa5ae083abab65	Apalache	Enabled	Eq	False	Passed	Model Under Test Equivalent Model
aa9957d1ec73697dba5e1b700a3dab555e17b44e	Apalache	Enabled	Ne	True	Passed	Model Under Test Equivalent Model
5528e99a55a7e3ebe47560d9d660ff60b7f677ae	Apalache	Enabled	Ne	False	Passed	Model Under Test Equivalent Model
e787fd1072947590c5fa8f048cc526f29ab1d7cc	Apalache	Enabled	Let	True	Passed	Model Under Test Equivalent Model
14a8952437c5e540aa9538e75cb386d372b4bf5e	Apalache	Enabled	Let	False	Passed	Model Under Test Equivalent Model
3a087653ffaf5703b7ce8f0954e0e219f4600430	Apalache	Enabled	In	True	Passed	Model Under Test Equivalent Model
d522fa0077ce34b9baa0845f943182947054c342	Apalache	Enabled	In	False	Passed	Model Under Test Equivalent Model
f5e6368168df6219190193c4943cee118d2f3c59	Apalache	Enabled	NotIn	True	Passed	Model Under Test Equivalent Model
89cb0538b9513bd1a4775748573793bf7fc9c956	Apalache	Enabled	NotIn	False	Passed	Model Under Test Equivalent Model
59b8c1b98c55d31b0b5769fab978d360809101b7	Apalache	Enabled	Exists	True	Passed	Model Under Test Equivalent Model
8d4a467079c9e833198b228ed7d3ea09d19faaaf	Apalache	Enabled	Exists	False	Passed	Model Under Test Equivalent Model
30e6256d472fb78d644c00733928a11201137f88	Apalache	Enabled	Forall	True	Passed	Model Under Test Equivalent Model
443920f3f17364fe46550f08b4946c536439e9a9	Apalache	Enabled	Forall	False	Passed	Model Under Test Equivalent Model
7129c45f0e1c402b785faed75a19f387da4fd660	Apalache	Enabled	Choose	True	Passed	Model Under Test Equivalent Model
d8f340ea2155e72877ffae147cdda69ac7c282df	Apalache	Enabled	Choose	False	Passed	Model Under Test Equivalent Model
d860b9838009d08e00a4f786bf315d75c6729874	Apalache	Enabled	FunApp	True	Passed	Model Under Test Equivalent Model
18297d8e53a5b775d1ec919c7915392d73380937	Apalache	Enabled	FunApp	False	Passed	Model Under Test Equivalent Model
3f3001acd9119182626f3574409308511d49d62e	Apalache	Enabled	Prime	True	Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form	Model Under Test Equivalent Model
c7f97baecf90cb807d26ee99123473a6f8b317f7	Apalache	Enabled	Prime	False	Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form	Model Under Test Equivalent Model
a6f4c5d899312a2fb972977f640c984c1e1c82d9	Apalache	Enabled	NumGt	True	Passed	Model Under Test Equivalent Model
50c6db42ceded617768f7ba3f91247e4eefc5a68	Apalache	Enabled	NumGt	False	Passed	Model Under Test Equivalent Model
71a591cc6dcd2fb77836d8878ad0781d5c08e2d7	Apalache	Enabled	NumGe	True	Passed	Model Under Test Equivalent Model
837bb2f23109050933d190542ad1cfa32adc637f	Apalache	Enabled	NumGe	False	Passed	Model Under Test Equivalent Model
b02fbb6db483297294cde6eb5552b2b87a15760c	Apalache	Enabled	NumLt	True	Passed	Model Under Test Equivalent Model
cf0c894e3321de1b21b4d06f5ce01669192a5b17	Apalache	Enabled	NumLt	False	Passed	Model Under Test Equivalent Model
6db6acb0317880c27e9dd6f2481ed5e725174f32	Apalache	Enabled	NumLe	True	Passed	Model Under Test Equivalent Model
e2ee46e778bb3c6545f5d4914b487bdd81fd7a48	Apalache	Enabled	NumLe	False	Passed	Model Under Test Equivalent Model
4faa93a1b713bbf8ca3c57e30198a179a1414d44	Apalache	Enabled	Def0	True	Passed	Model Under Test Equivalent Model
ce0a2a4607c4a6603813f5c8f81ec54559e81640	Apalache	Enabled	Def0	False	Passed	Model Under Test Equivalent Model
1e81a9752e0daf4a2841354fde3e187796030d9e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef0	True	Passed	Model Under Test Equivalent Model
01ca6d6a9960fbd01ab087d9ca612c9958b3f948	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef0	False	Passed	Model Under Test Equivalent Model
b382cb2a2fed60fbe78e51095c20b381a2adc86c	Apalache	Enabled	Def1	True	Passed	Model Under Test Equivalent Model
9eca1fb3a207d068c9d7abd8a048b30b4c7f87e8	Apalache	Enabled	Def1	False	Passed	Model Under Test Equivalent Model
58081d0c306fc8dddf8ac3a1da0969b150bb58d1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1	True	Passed	Model Under Test Equivalent Model
5c0b89971c0c5103d3df36695808168175d9b1c0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1	False	Passed	Model Under Test Equivalent Model
eeaf65775f20b8101f178629769c22c2e7cc08c7	Apalache	Enabled	Def2	True	Passed	Model Under Test Equivalent Model
61b95e5676fb4955608a018415df0f59c84348b2	Apalache	Enabled	Def2	False	Passed	Model Under Test Equivalent Model
45a577578362575b8272ca7c2386c47fd2cab11b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef2	True	Passed	Model Under Test Equivalent Model
49237d5a2fe8b0b2c9e97d2748ebd30031e3e2f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef2	False	Passed	Model Under Test Equivalent Model
f50e224946e1954faf6cd2f828b5409a660da506	Apalache	Enabled	Def1Recursive	True	Passed	Model Under Test Equivalent Model
8bd0b1e0cf17dccd431453e24980d0ef99b27573	Apalache	Enabled	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f542efb35ce3ca7c37453b64169f3739ebb2bdd6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
c7774663c65d03d4bdb38891d0399b97221b811e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
722353afb4de40023b9e0de8fcdbf91729a41ac9	Apalache	Enabled	Extends	True	Passed	Model Under Test Equivalent Model
1412acc3d1e5935323dc84a7eb7e126e6d6ee2d2	Apalache	Enabled	Extends	False	Passed	Model Under Test Equivalent Model
721ee7e0fa82ccbb59aea133fa50d9519273db4f	Apalache	Enabled	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
d35b8d97489727c7b8438fa34880dcecaa923f64	Apalache	Enabled	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
009de57ca1b4595a55cf98245635fe0f6e80d5ed	Apalache	Enabled	Variable	True	Passed	Model Under Test Equivalent Model
d882ec607eb88804cef4c35e84861a8fdfd27579	Apalache	Enabled	Variable	False	Passed	Model Under Test Equivalent Model
944c987479ada9daec55c916096602dbb81edc02	Apalache	Enabled	Constant	True	Passed	Model Under Test Equivalent Model
d588b3e8929b12474459566f7c45d3450c961447	Apalache	Enabled	Constant	False	Passed	Model Under Test Equivalent Model
8e4b53cfc246696c75b2ced2c983d87c25e140e6	Apalache	Enabled	ConstantRank1	True	Passed	Model Under Test Equivalent Model
acfccac88ea1418444694c7c67b1d7764bf6d756	Apalache	Enabled	ConstantRank1	False	Passed	Model Under Test Equivalent Model
8321f38d089b76e015b0762e12ea4392f48345d7	Apalache	Enabled	Instance	True	Passed	Model Under Test Equivalent Model
4bed2a44e4314e55702acb3707833ba31c4b46b5	Apalache	Enabled	Instance	False	Passed	Model Under Test Equivalent Model
e1c5eff5ce8fbe3c0cc169e200ce0ace8aae6e9a	Apalache	Enabled	InstanceWith	True	Passed	Model Under Test Equivalent Model
784b45213e2cd5163c0a3af2ad76eb86f9e1e479	Apalache	Enabled	InstanceWith	False	Passed	Model Under Test Equivalent Model
39db4c32e8bf4636ceecf218d0bd32cf45aab532	Apalache	Enabled	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2fe236d90b91aebeca5dc3ddea84714f818e40c6	Apalache	Enabled	InstanceNamed	False	Passed	Model Under Test Equivalent Model
18fce6f34fe5a4a5505f7d56b0faabbf32048bea	Apalache	Enabled	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
02d6b13cd73c047f63b6d2a7eb40acd5685ffacd	Apalache	Enabled	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
02837c33988de99a34531811f038bb15e2b03885	Apalache	Enabled	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
596b7bd245b3df0f5be2cf3168c5c280bc996432	Apalache	Enabled	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
86a1fcd98f630ec5d19f7e23cd0e63285efa7b7a	Apalache	Enabled	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
fae4a06b8c61705587dd2b599012209ed64ec9c7	Apalache	Enabled	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
87546aab3da518ce814f20c52f5dc6727ad9a23c	Apalache	Enabled	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
e6af96dcb2bc1a9b3a233cb237d87c049fa179c0	Apalache	Enabled	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
dfe99a51549323cdb072195a019664929f912f2f	Apalache	Enabled	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
b1d3637d385cbf7708dd9fcce22261deaa4ebfcf	Apalache	Enabled	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
db76a35439106173132ff9015e8a313644b5298b	Apalache	Enabled	Enabled	True	Passed	Model Under Test Equivalent Model
fd726140cefaa245a181fc057440dde6b360b687	Apalache	Enabled	Enabled	False	Passed	Model Under Test Equivalent Model
ebdac084d2b75a3cbe114ff589e159127c590580	Apalache	Enabled	SubsetEq	True	Passed	Model Under Test Equivalent Model
0730291349ce5aedbbc410e9d476e32bbc601c00	Apalache	Enabled	SubsetEq	False	Passed	Model Under Test Equivalent Model
de434e270e057b8a743b7e9d44cc3b408542e761	Apalache	Enabled	IfCond	True	Passed	Model Under Test Equivalent Model
9aae582d87f3946dbee1b81102a4a68fcdb7b582	Apalache	Enabled	IfCond	False	Passed	Model Under Test Equivalent Model
00bf49032c9db14dd81bcae5879d0fa369456722	Apalache	Enabled	IfThen	True	Passed	Model Under Test Equivalent Model
5ac2681ada6d1e6ceb9db2d2d3f41c09cc730d28	Apalache	Enabled	IfThen	False	Passed	Model Under Test Equivalent Model
b611a80fea25749a1df34b20f478cef2ee2a5f65	Apalache	Enabled	IfElse	True	Passed	Model Under Test Equivalent Model
6e56f8ba520133813bbc2b60e178408a95f413a0	Apalache	Enabled	IfElse	False	Passed	Model Under Test Equivalent Model
d856805729fc05540be362eff9a4f8038326eea4	Apalache	Enabled	Unchanged	True	Passed	Model Under Test Equivalent Model
de85c596c6cef02259946d412754818c3d692d65	Apalache	Enabled	Unchanged	False	Passed	Model Under Test Equivalent Model
7bd4c9936a24b376682a19a4da638daabbc9af1d	Apalache	Enabled	Equivalence	True	Passed	Model Under Test Equivalent Model
00c946bef0a50fff85da141729495765dd28d733	Apalache	Enabled	Equivalence	False	Passed	Model Under Test Equivalent Model
237042bfe0f0c4db6c194a0cfeb61316df7daf91	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Enabled	TlcEval	True	Passed	Model Under Test Equivalent Model
12cd862cda08e6bcd774047dc9f0eaaaba9eed15	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Enabled	TlcEval	False	Passed	Model Under Test Equivalent Model
e5ae0f3acccb5cd762f362e136fb2efba6314416	Apalache	Enabled	BagBagIn	True	Passed	Model Under Test Equivalent Model
d7979664f5c70bc3a88cafe7a72b786d5598fe8b	Apalache	Enabled	BagBagIn	False	Passed	Model Under Test Equivalent Model
64b8098acc329c87fed23a0f8b0bef671200d47a	Apalache	Enabled	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
5b66a22b372780017fe8a1eb6cf8efe48631ed95	Apalache	Enabled	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
13da141377626b01da382d10349c9c1f20a44131	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)	Enabled	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
c55bab3ecd597e2a6af58c65e60b58054c39cf92	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)	Enabled	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
791e7c9ab7a35abce819905fcc80ce0c047a6782	Apalache	Enabled	SeqHead	True	Passed	Model Under Test Equivalent Model
bd695a2e71bcfb69e23f82eeb3e8641eb39e151a	Apalache	Enabled	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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