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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
1743f06e6110d7369b91f0967757e5671a2ce412	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Forall	OneLineComment	True	Passed	Model Under Test Equivalent Model
87f078867cf596ea3c4d750c7bb6d8f607efc1e8	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Forall	OneLineComment	False	Passed	Model Under Test Equivalent Model
bf567b9e31f6514a0529b7376ead6786452be002	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Forall	MultiLineComment	True	Passed	Model Under Test Equivalent Model
45372613643db916a879b0383e73ddb5b1bc7dfc	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Forall	MultiLineComment	False	Passed	Model Under Test Equivalent Model
43c46ac34d06bec00db835172fac33d7772e77f5	Apalache	Forall	BoolTrue	True	Passed	Model Under Test Equivalent Model
e3908d7fc1c072c4f00ea15522625f527a90aee9	Apalache	Forall	BoolTrue	False	Passed	Model Under Test Equivalent Model
07338e830629cab6ed32919cd1672e37dd4a6edd	Apalache	Forall	BoolFalse	True	Passed	Model Under Test Equivalent Model
e98a7038eca3f88850f3ad804646ff9616b07dab	Apalache	Forall	BoolFalse	False	Passed	Model Under Test Equivalent Model
9da46ad15f99ba3a7af1ee2065369ae3e8d84a53	Apalache	Forall	And	True	Passed	Model Under Test Equivalent Model
880b7defc6fe642b0a2206180cdf7f3085af8d5e	Apalache	Forall	And	False	Passed	Model Under Test Equivalent Model
0cf1f2a6e1f22944c0fb3796a08b6aabb2109956	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Forall	AndMultiLine	True	Passed	Model Under Test Equivalent Model
b9c73d82c3b949908518a3c82b9160241a487217	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Forall	AndMultiLine	False	Passed	Model Under Test Equivalent Model
49fa40a870e1aefcb0e22b22ad0eef8c4117d8a1	Apalache	Forall	Imply	True	Passed	Model Under Test Equivalent Model
74a0b9dcfb9f710b2fe1412277963d1371ea06fe	Apalache	Forall	Imply	False	Passed	Model Under Test Equivalent Model
79715d99ec5ab4d68cb805fdef68335d9bf1e31d	Apalache	Forall	Not	True	Passed	Model Under Test Equivalent Model
559c1fd79ee55a143503d5ea00d5d90bce05f520	Apalache	Forall	Not	False	Passed	Model Under Test Equivalent Model
1ac187464571e494bc9fd0637f4d88567712c9dc	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Forall	Or	True	Passed	Model Under Test Equivalent Model
2307edd1bdb35fe43aa7123a0ccf7765b70d4067	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Forall	Or	False	Passed	Model Under Test Equivalent Model
deeef08259d6443430e0406840ef22e120d01ec2	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Forall	OrMultiLine	True	Passed	Model Under Test Equivalent Model
fb10555febded4772c700fb3dcf9a67ae971319f	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Forall	OrMultiLine	False	Passed	Model Under Test Equivalent Model
3bed658b78268fea2928d6e3f8e5cf8c3b6659f9	Apalache	Forall	Eq	True	Passed	Model Under Test Equivalent Model
5c76f77e64f00e0001391f52ad0e8c76ca08e27a	Apalache	Forall	Eq	False	Passed	Model Under Test Equivalent Model
659e00c31f8a685696a3a91cfae343810bb6567f	Apalache	Forall	Ne	True	Passed	Model Under Test Equivalent Model
e1918432e1b7fbf31a942c05492d76509e6a3469	Apalache	Forall	Ne	False	Passed	Model Under Test Equivalent Model
a651e1abbc3430395266b5e3a2c4605c6ef5cec3	Apalache	Forall	Let	True	Passed	Model Under Test Equivalent Model
fff3f5ed4e49ab0af8ad436d7121595b49ec7a39	Apalache	Forall	Let	False	Passed	Model Under Test Equivalent Model
7d041623fc348da6204e1afa23c78fbf5d0d497d	Apalache	Forall	In	True	Passed	Model Under Test Equivalent Model
43221f8838b935ecfc8b5e9bcbcdc77c02122350	Apalache	Forall	In	False	Passed	Model Under Test Equivalent Model
4dc7205527ce5820efba6326d5035ec7f1808728	Apalache	Forall	NotIn	True	Passed	Model Under Test Equivalent Model
caabe42270996a302d085b774cff4a7b13422fc0	Apalache	Forall	NotIn	False	Passed	Model Under Test Equivalent Model
205b0f52aa1883b07e738fc22a80cb86a8a1ad1e	Apalache	Forall	Exists	True	Passed	Model Under Test Equivalent Model
1ee477e330d86725d6634c83a0485e9952a87d54	Apalache	Forall	Exists	False	Passed	Model Under Test Equivalent Model
6b79f87d81d02a9c7c4cad00dccf91287a14c3b8	Apalache	Forall	Forall	True	Passed	Model Under Test Equivalent Model
00e63e97ea93b69c1f27ed4a65dd7fbc106c49b9	Apalache	Forall	Forall	False	Passed	Model Under Test Equivalent Model
0ce6d5c91bc9e9b2a21ec3f6f5a2b1296cab11c0	Apalache	Forall	Choose	True	Passed	Model Under Test Equivalent Model
1ced9777940c9e8b4a8d373c5ef8d7cae1b2e927	Apalache	Forall	Choose	False	Passed	Model Under Test Equivalent Model
257ffa40d61b51c75dadcec9d665d1c87f07c858	Apalache	Forall	FunApp	True	Passed	Model Under Test Equivalent Model
67aee127ee35313d309f7d5fc74f9fa8bab6ffef	Apalache	Forall	FunApp	False	Passed	Model Under Test Equivalent Model
f67ce6be250fee94102b71540e92987991fe8e1a	Apalache	Forall	Prime	True	Passed	Model Under Test Equivalent Model
e2bd8f315a52ebe8bd03ab860e99cd18c3234770	Apalache	Forall	Prime	False	Passed	Model Under Test Equivalent Model
640150ce9db0c332124168f441dc1c3389ef81b1	Apalache	Forall	NumGt	True	Passed	Model Under Test Equivalent Model
016d6df55e6c0ccffd7f85141baba36b34fc8fca	Apalache	Forall	NumGt	False	Passed	Model Under Test Equivalent Model
16635fd5adf70953fc9bc753cbb7e6f29eb9d988	Apalache	Forall	NumGe	True	Passed	Model Under Test Equivalent Model
025439bb6e6a4611861400c2b476da791e8b56d2	Apalache	Forall	NumGe	False	Passed	Model Under Test Equivalent Model
d2e99d01d8d847bdee5f549882748bad193c0c4f	Apalache	Forall	NumLt	True	Passed	Model Under Test Equivalent Model
bd55da018eda1a3a5003227028f123b16708297e	Apalache	Forall	NumLt	False	Passed	Model Under Test Equivalent Model
9aae7a325d5892ec8f248ee6372121877418fa9d	Apalache	Forall	NumLe	True	Passed	Model Under Test Equivalent Model
e17f1cccbf65dabb528dd350f2e0a2593eff2da7	Apalache	Forall	NumLe	False	Passed	Model Under Test Equivalent Model
cff1c96a1b8a0e175e2562b343b2f7a8e5d08d11	Apalache	Forall	Def0	True	Passed	Model Under Test Equivalent Model
d286390173fd5ed126c2981c5f66bbab1814d747	Apalache	Forall	Def0	False	Passed	Model Under Test Equivalent Model
66579749c168227a2f8e15642c332dc57e6482da	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef0	True	Passed	Model Under Test Equivalent Model
a060af23843b0bfa40e9fdd6cddc538e03e6e368	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef0	False	Passed	Model Under Test Equivalent Model
3824290ee255daf7443640e770cdae786140faf1	Apalache	Forall	Def1	True	Passed	Model Under Test Equivalent Model
f93c27aedffed6c73e65876eb9ee84e48e4ecfdf	Apalache	Forall	Def1	False	Passed	Model Under Test Equivalent Model
0b524cd314a78b4cd9db72286ba6f25da4395b4e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1	True	Passed	Model Under Test Equivalent Model
02f995efa8406ee88bc8c50f1d03b633838e253d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1	False	Passed	Model Under Test Equivalent Model
cba538ce8e7825c1e188fa668c7e8abe854c727d	Apalache	Forall	Def2	True	Passed	Model Under Test Equivalent Model
98e9ca9a5aeb690ba6cf81eede0cf8f726c2f39a	Apalache	Forall	Def2	False	Passed	Model Under Test Equivalent Model
cca1b0aa9db540d87cb5e8d9a583e8b59bcc5abc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef2	True	Passed	Model Under Test Equivalent Model
0bab078b9815bc3aabe61afafdce619c9473d684	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef2	False	Passed	Model Under Test Equivalent Model
0a5449487f2f5c3801cc869d848d8f40793cf51a	Apalache	Forall	Def1Recursive	True	Passed	Model Under Test Equivalent Model
625fe45051442aa717fb6fd56eb144d34d95f8a6	Apalache	Forall	Def1Recursive	False	Passed	Model Under Test Equivalent Model
d7ad39e268c71546dea6b37493e09d35e1372b5b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
19a8fc8bcef79ce90213fd322315a23205a8ea0f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
9aea2a05ebdcc22fa10790067fe095ef0f2270d9	Apalache	Forall	Extends	True	Passed	Model Under Test Equivalent Model
570daf61db0edd8555598dbbf6c1bbb381e6bae5	Apalache	Forall	Extends	False	Passed	Model Under Test Equivalent Model
894affc054d89eff1d6d4441501946e0bca4ad41	Apalache	Forall	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
aa4a1e85a78ffc427e0f4c2da5968d43648558a9	Apalache	Forall	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
51528949fecc6ecd3443e3ce65b5e36128820d55	Apalache	Forall	Variable	True	Passed	Model Under Test Equivalent Model
16f189f9f84a2ce070cefc6285bfb04d8be688f2	Apalache	Forall	Variable	False	Passed	Model Under Test Equivalent Model
5d9c4138647fd2ee227b5375e5e1797eaa9245a2	Apalache	Forall	Constant	True	Passed	Model Under Test Equivalent Model
13c8235e1cbc456ff68c31592dde588ca5d74dc3	Apalache	Forall	Constant	False	Passed	Model Under Test Equivalent Model
d593590aea3743c81f5e058313906c64694f4c4a	Apalache	Forall	ConstantRank1	True	Passed	Model Under Test Equivalent Model
fdd1e4f9e161e4bc03b49e12366e5f2fd1a4ca63	Apalache	Forall	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2c2fd2de9d6fa9dff20ab4c075a7c7349751a04b	Apalache	Forall	Instance	True	Passed	Model Under Test Equivalent Model
2b3ec5e176324aa9f29fb03e16c92b2491390af8	Apalache	Forall	Instance	False	Passed	Model Under Test Equivalent Model
92ab77684c6f4931d32d65e11442c758467485a6	Apalache	Forall	InstanceWith	True	Passed	Model Under Test Equivalent Model
341f9470b28c67dc22e182f07b69d02a66d8ab40	Apalache	Forall	InstanceWith	False	Passed	Model Under Test Equivalent Model
a34a03e7b5757f74eded1fd6a5fc0c7796eb757e	Apalache	Forall	InstanceNamed	True	Passed	Model Under Test Equivalent Model
accf7d747e657f6794c0345ed9282e4bfd435a18	Apalache	Forall	InstanceNamed	False	Passed	Model Under Test Equivalent Model
efd1e2dea51866d3bc9206387ea3f1b81938f0a5	Apalache	Forall	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
eb520450982ccb1d2220d533a078e362d903352e	Apalache	Forall	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
30811d65ceb2cd4790f6a464e01f01a7aab27569	Apalache	Forall	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
4f41db3f67b589428cb736d891163045dca2a6d1	Apalache	Forall	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
c506f5de1f0033293541b771159d143347e079fa	Apalache	Forall	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
5995266c1bb718f6ffe2ab95183f24b256984ad6	Apalache	Forall	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
6865948a54f9b2fa15434865d6b988f628571792	Apalache	Forall	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
3e34fbee1769a2666794f9900bdb3ec15050a0b0	Apalache	Forall	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
badf219896d0b63396969788e0d18c91fdebdc92	Apalache	Forall	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
427c6a4c233dedd461eaa27556a2fbf958b14a1b	Apalache	Forall	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
086b6bb2399049e0291e2bb8bd27ca860c44b9cf	Apalache	Forall	Enabled	True	Passed	Model Under Test Equivalent Model
daec55cb5e46597dbbe37bd9744a880476bb98f9	Apalache	Forall	Enabled	False	Passed	Model Under Test Equivalent Model
560436d5c99edbc9867f4f3d8929f14c16c1020b	Apalache	Forall	SubsetEq	True	Passed	Model Under Test Equivalent Model
0415c092621a3357e2bf45da854a675c75ec2a3c	Apalache	Forall	SubsetEq	False	Passed	Model Under Test Equivalent Model
e015fb9a0983941de177e9d67016e755c093a515	Apalache	Forall	IfCond	True	Passed	Model Under Test Equivalent Model
3e55afa137ff42dbb03ddf8e1e083e49cfef8403	Apalache	Forall	IfCond	False	Passed	Model Under Test Equivalent Model
eb8a12607233cf9200d18cc0c877b9a32b3781ec	Apalache	Forall	IfThen	True	Passed	Model Under Test Equivalent Model
cd60f8b06c48fa242728966a5ffa1682e11412c4	Apalache	Forall	IfThen	False	Passed	Model Under Test Equivalent Model
a79e2fb60ff165cd7da2dfa598cba3fb620ea6c5	Apalache	Forall	IfElse	True	Passed	Model Under Test Equivalent Model
675369d160d254e1fb8b3c7d3838a797d7e97932	Apalache	Forall	IfElse	False	Passed	Model Under Test Equivalent Model
e6faaaf83d1ef06bef1cf62d355d597bf98d86df	Apalache	Forall	Unchanged	True	Passed	Model Under Test Equivalent Model
0d62bdfea0fc3a0e7c5a14b82ab6d4808a0f420a	Apalache	Forall	Unchanged	False	Passed	Model Under Test Equivalent Model
669946725e7165580e738252068394f5cfa50d73	Apalache	Forall	Equivalence	True	Passed	Model Under Test Equivalent Model
71ee72546d51f743faf0cb805ba352cd00fe0dc4	Apalache	Forall	Equivalence	False	Passed	Model Under Test Equivalent Model
49870bec609dad20c1a7444cf35323dfaeadbc4e	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Forall	TlcEval	True	Passed	Model Under Test Equivalent Model
f2df33bf0c61fd0290456f09b915d8361e701a73	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Forall	TlcEval	False	Passed	Model Under Test Equivalent Model
d311d7448a20b714c83af82c32b75f819742ce32	Apalache	Forall	BagBagIn	True	Passed	Model Under Test Equivalent Model
a8f455e1bb29f43d0f683a8a21cf8a005a576236	Apalache	Forall	BagBagIn	False	Passed	Model Under Test Equivalent Model
1c38127cf9e689bcb673700fefe0050ee155ad51	Apalache	Forall	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
071638dc2df97bada7e5943095d908ae501083e7	Apalache	Forall	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
9c8c3e2444c0314ac93a722402556bb78da35ad9	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)	Forall	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
065b119e804df262437b3d572032e3f06f28e284	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)	Forall	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
9bdae37ee65772dc78391b136f2f274fadf5d68c	Apalache	Forall	SeqHead	True	Passed	Model Under Test Equivalent Model
7a07891739df18ff94d2cf902ccfb6520b2e979d	Apalache	Forall	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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