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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
96b842ecc4a364698078eab6d225365383003597	Apalache	And	Enabled	True	Passed	Model Under Test Equivalent Model
18c091666b4d57070c922490c38012fdb7fe7c24	Apalache	And	Enabled	False	Passed	Model Under Test Equivalent Model
b9ce2a896a273827551099e440f7c5dc7259307d	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Enabled	True	Passed	Model Under Test Equivalent Model
91f37ec336d8e31e8e8b59ec07d0987c77e82609	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Enabled	False	Passed	Model Under Test Equivalent Model
8a0f063fb517a05679feb71b4242b319849599fa	Apalache	Imply	Enabled	True	Passed	Model Under Test Equivalent Model
42dd73b7a301798e773027e286caa59423c4573b	Apalache	Imply	Enabled	False	Passed	Model Under Test Equivalent Model
787a4c9535ca7a7482c0756af13595a06f32fda4	Apalache	Not	Enabled	True	Passed	Model Under Test Equivalent Model
3fea92155647da726e56e6d1a196dfe2bc9a2cd1	Apalache	Not	Enabled	False	Passed	Model Under Test Equivalent Model
ae714a2a3f0f43c002099348b0a5bba49b1a5711	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Enabled	True	Passed	Model Under Test Equivalent Model
304212b5ee732e7835aef1f291f5b2a65124ca46	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Enabled	False	Passed	Model Under Test Equivalent Model
d260ceb756fac9d570ded23056fccc256bb00857	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Enabled	True	Passed	Model Under Test Equivalent Model
fcdfa7677d9742a0e9954eb30c663c1851b7e207	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Enabled	False	Passed	Model Under Test Equivalent Model
580698336ac0a8026381f2b7bc97659b85a2dbaa	Apalache	AndProp	Enabled	True	Passed	Model Under Test Equivalent Model
e0fc93f5e208785dadcc8067e7b3e009f93abe2c	Apalache	AndProp	Enabled	False	Passed	Model Under Test Equivalent Model
d67380be4c97193e5b9424e3f2758cf9757049c7	Apalache	Boxed	Enabled	True	Passed	Model Under Test Equivalent Model
a330ada29638053d6d848105e521c38692ec8e2f	Apalache	Boxed	Enabled	False	Passed	Model Under Test Equivalent Model
642c976e3e9e355ac985d67464226b476983531e	Apalache	Eq	Enabled	True	Passed	Model Under Test Equivalent Model
0d6911e351e1785c9cec483220b8bed8abd16a6e	Apalache	Eq	Enabled	False	Passed	Model Under Test Equivalent Model
1828875686fae94065b7c3eeffa988840a3625ef	Apalache	Ne	Enabled	True	Passed	Model Under Test Equivalent Model
460a22adecdac8bb1a587fdf25b368ea0b541b87	Apalache	Ne	Enabled	False	Passed	Model Under Test Equivalent Model
9b7eecbff91185fc4be51b620f933f7d71a7eff6	Apalache	Let	Enabled	True	Passed	Model Under Test Equivalent Model
b355a2a324ef62377da62023dd4ca4367b9d8396	Apalache	Let	Enabled	False	Passed	Model Under Test Equivalent Model
638709aca5c1f12df5f4e82a18d8e65df4499fe1	Apalache	Set0	Enabled	True	Passed	Model Under Test Equivalent Model
e2ad43367bc91f772aba59834a2da850e3eadcf2	Apalache	Set0	Enabled	False	Passed	Model Under Test Equivalent Model
4b6594b3cb34e2c090ea30b5e76c2988c46a56ca	Apalache	Set1	Enabled	True	Passed	Model Under Test Equivalent Model
6df6863271ce5dcc33815223302dfdef2552482e	Apalache	Set1	Enabled	False	Passed	Model Under Test Equivalent Model
660906175528ff330bd8c72769a9c16cc60280fa	Apalache	Set2	Enabled	True	Passed	Model Under Test Equivalent Model
d2daf911ad42ff9c4c57db9711a22092cdfaae68	Apalache	Set2	Enabled	False	Passed	Model Under Test Equivalent Model
546409d81965c42dc84c7532ec5ced99d0c28ccb	Apalache	Fun	Enabled	True	Passed	Model Under Test Equivalent Model
026d5623e65fbe2b311eb4d0f4d933eb7c6c65f7	Apalache	Fun	Enabled	False	Passed	Model Under Test Equivalent Model
01e84074de3da0825a00585b094bd8beff2665de	Apalache	In	Enabled	True	Passed	Model Under Test Equivalent Model
2433487fab6117dd41c5ea3c47d29c30bbcbb86e	Apalache	In	Enabled	False	Passed	Model Under Test Equivalent Model
71ba630e2981eab53c84b0399209d0a44a125f4b	Apalache	NotIn	Enabled	True	Passed	Model Under Test Equivalent Model
fa2cd0b35463fbd7d6f8753a67c75c0aa685490e	Apalache	NotIn	Enabled	False	Passed	Model Under Test Equivalent Model
820985ec5d4a1b834361483f91072b181db23333	Apalache	Exists	Enabled	True	Passed	Model Under Test Equivalent Model
b080300d3bedd92760638d514969b90e90bd7a55	Apalache	Exists	Enabled	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
bc2627758a45f82e84982eb8e4934dda9f5663db	Apalache	Choose	Enabled	True	Passed	Model Under Test Equivalent Model
47c5c454e49f037aab45f35c718a6b0712ca3438	Apalache	Choose	Enabled	False	Passed	Model Under Test Equivalent Model
b0b4d9a9654f421a0d65ff52d36f3b88d63ef38d	Apalache	Record	Enabled	True	Passed	Model Under Test Equivalent Model
5d4e3253356d53d565e39ee95f554a950017a5be	Apalache	Record	Enabled	False	Passed	Model Under Test Equivalent Model
4b8587d69d6a7a29621a34293377a539bb891a81	Apalache	Tuple	Enabled	True	Passed	Model Under Test Equivalent Model
fb5a421db009cc7daa6b956d87ac8e520d6fa375	Apalache	Tuple	Enabled	False	Passed	Model Under Test Equivalent Model
d96489168c995807f457b4e92ff156e8080009aa	Apalache	FunApp	Enabled	True	Passed	Model Under Test Equivalent Model
92980fef8568cea05e465240de2bfc70dd6b8f71	Apalache	FunApp	Enabled	False	Passed	Model Under Test Equivalent Model
4e07f865d562d1017315de9a97af0463bcbc5568	Apalache	Except1Fun	Enabled	True	Passed	Model Under Test Equivalent Model
81bfb37b4326fa6c3805948c61ee4958b6855c32	Apalache	Except1Fun	Enabled	False	Passed	Model Under Test Equivalent Model
00222391e6890dbcb9f7f71c4e13c021ecc1f8cd	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Enabled	True	Passed	Model Under Test Equivalent Model
61cb78b39b744028741f5ea594098b0cfa919186	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Enabled	False	Passed	Model Under Test Equivalent Model
930513d8c910be2e5fbf8117465c829de69719d0	Apalache	Except1Rec	Enabled	True	Passed	Model Under Test Equivalent Model
68fe3374645a5e3e781b661cd33fa838a0685387	Apalache	Except1Rec	Enabled	False	Passed	Model Under Test Equivalent Model
479af36a3f22d65bc6dad5fb0da7ef04cc3ed3dc	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Enabled	True	Passed	Model Under Test Equivalent Model
bfe0fab9c95642a705d28d9e06624cd24d50ec1b	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Enabled	False	Passed	Model Under Test Equivalent Model
e23eb6f30867b3fc6a7add003019246031209746	Apalache	Except2Fun	Enabled	True	Passed	Model Under Test Equivalent Model
c002810502fadb18c6d940c3b07e81db022158a5	Apalache	Except2Fun	Enabled	False	Passed	Model Under Test Equivalent Model
c3861b249cbb9b62e9e98f1c1d23ad400ae8975f	Apalache	Prime	Enabled	True	Passed	Model Under Test Equivalent Model
ea1e49fc0b3f8cd4e414650c4923d1abd3acf333	Apalache	Prime	Enabled	False	Passed	Model Under Test Equivalent Model
7a459e1f0071bca3d91dc7e5535d2bc6f2259d7d	Apalache	DefFun	Enabled	True	Passed	Model Under Test Equivalent Model
8f262d49d36bd754455ad81c95d0dd465f4395e0	Apalache	DefFun	Enabled	False	Passed	Model Under Test Equivalent Model
c29cd2a94791cd3c87250848caa799972e942780	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Enabled	True	Passed	Model Under Test Equivalent Model
8dc107fa0d1bef56b3aed9e99e9102999935f441	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Enabled	False	Passed	Model Under Test Equivalent Model
678f157e65b8fec62c5c7b6b313c81b59d9f3086	Apalache	DefFunRecursive	Enabled	True	Passed	Model Under Test Equivalent Model
a2d980858fbaa009da5207d7f364eefda25ff7e9	Apalache	DefFunRecursive	Enabled	False	Passed	Model Under Test Equivalent Model
7eaf4de68d372fdf273dd426239399c19bb6436e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Enabled	True	Passed	Model Under Test Equivalent Model
e3f6b119c5af76afc448f6bb40b3d796b84343cc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Enabled	False	Passed	Model Under Test Equivalent Model
24864eac23409dd76ad0b90b8ea007dac3a68d97	Apalache	Def0	Enabled	True	Passed	Model Under Test Equivalent Model
12310c2b399662d98b67b64ae4ea7125570d1a2e	Apalache	Def0	Enabled	False	Passed	Model Under Test Equivalent Model
fbf510b76e52dcd2d8a77bf7e0e30849557a8332	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Enabled	True	Passed	Model Under Test Equivalent Model
b6552e3ebab4fcf93fb3432bd5fcf541595366e6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Enabled	False	Passed	Model Under Test Equivalent Model
cfc4116e031495f37c9242cdfb0f7d8052514641	Apalache	Def1	Enabled	True	Passed	Model Under Test Equivalent Model
dd51ea6886abe6219eff697b3519491a834ad827	Apalache	Def1	Enabled	False	Passed	Model Under Test Equivalent Model
3f33567b2b1126d471db23dd0102b6c569a33d7f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Enabled	True	Passed	Model Under Test Equivalent Model
e18c3913315276259c1ce205c646c66f3a6d4a64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Enabled	False	Passed	Model Under Test Equivalent Model
d14e2a8ed65209964b1c61fed2a8afdf211e8229	Apalache	Def2	Enabled	True	Passed	Model Under Test Equivalent Model
c41d77004b232a189557e72df5e4b0320e12b8ce	Apalache	Def2	Enabled	False	Passed	Model Under Test Equivalent Model
cc5dd1b39eaa85dfa8ddb9e7cd84d46725555d02	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Enabled	True	Passed	Model Under Test Equivalent Model
0c155ce09e28c2d11595e105671a377b9c87ddb7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Enabled	False	Passed	Model Under Test Equivalent Model
5db2f894c17bf8d0d5b86a42938f14b43cc5cb61	Apalache	Def1Recursive	Enabled	True	Passed	Model Under Test Equivalent Model
f3833f6c9fc832ff8facf17f4d13f01626090635	Apalache	Def1Recursive	Enabled	False	Passed	Model Under Test Equivalent Model
9995b806be2568520bafd36719c1fbfa2b62bf8b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Enabled	True	Passed	Model Under Test Equivalent Model
00441b3fbc8e1e574302d5a2df7fe373a61094bd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Enabled	False	Passed	Model Under Test Equivalent Model
baca5dba3dc837c06c7b8db4d43da1acfe5f41e4	Apalache	Extends	Enabled	True	Passed	Model Under Test Equivalent Model
ee9eb0f42bae269968a65ec5e185bcd179158bd0	Apalache	Extends	Enabled	False	Passed	Model Under Test Equivalent Model
7b2025c0f44c125cb04ece0ea790cba752d7c9f8	Apalache	ExtendsInDifferentFolder	Enabled	True	Passed	Model Under Test Equivalent Model
12fab41c42ead1cce4cadcd8b7ae92be6041fd23	Apalache	ExtendsInDifferentFolder	Enabled	False	Passed	Model Under Test Equivalent Model
52fe08036077e989cf1966566d1219a3c4d91c0f	Apalache	Variable	Enabled	True	Passed	Model Under Test Equivalent Model
adcb99211770fe5d91e53b6097965ed1cd0c6816	Apalache	Variable	Enabled	False	Passed	Model Under Test Equivalent Model
e165f5d291a00d6c962e1a4924a20abaf948afe6	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Enabled	True	Passed	Model Under Test Equivalent Model
fb8d67bf5b4b9e2bae1eb271a22c3d40efab721c	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Enabled	False	Passed	Model Under Test Equivalent Model
e2a3765897607f0a868be8e9745fcddaecd99ad8	Apalache	Instance	Enabled	True	Passed	Model Under Test Equivalent Model
e2fe61f11a149ce79d52a24823f3c14637332c70	Apalache	Instance	Enabled	False	Passed	Model Under Test Equivalent Model
a45997b3abe437c47ee11973fb3583a6640eba5c	Apalache	InstanceWith	Enabled	True	Passed	Model Under Test Equivalent Model
8d5cb6d5d6a0b4ef4a216c01122b5a9bbbd0e817	Apalache	InstanceWith	Enabled	False	Passed	Model Under Test Equivalent Model
f2fe0cc6ef3c2734b0bb7e7c18691544044ada23	Apalache	InstanceNamed	Enabled	True	Passed	Model Under Test Equivalent Model
3ead6d499d5742b8cdda653153492ffb8f258bf5	Apalache	InstanceNamed	Enabled	False	Passed	Model Under Test Equivalent Model
bbaf942607d72f9e2b1feadd6a2e27161164f7ad	Apalache	InstanceNamedWith	Enabled	True	Passed	Model Under Test Equivalent Model
ac49b960429ffec15de730b5caab5a8a8b428a6c	Apalache	InstanceNamedWith	Enabled	False	Passed	Model Under Test Equivalent Model
a3e61b816f5b4401ee396b7739cc11f147d4997e	Apalache	InstanceInFolder	Enabled	True	Passed	Model Under Test Equivalent Model
42d3aa0b8391f5fbd0d129a1b3818d93599d1ecc	Apalache	InstanceInFolder	Enabled	False	Passed	Model Under Test Equivalent Model
d1c098750bb8ca0a9367b59ceedb8dfbe66d5fda	Apalache	InstanceWithInFolder	Enabled	True	Passed	Model Under Test Equivalent Model
0b7b1d28a6134156320c2fc149b4f7f8a8b9e927	Apalache	InstanceWithInFolder	Enabled	False	Passed	Model Under Test Equivalent Model
d3833e6697da1a2c456f89ade2b123182b80fd14	Apalache	InstanceNamedInFolder	Enabled	True	Passed	Model Under Test Equivalent Model
e6bd5ad1480d3be3312501e2fa3fce2f0ad22b4c	Apalache	InstanceNamedInFolder	Enabled	False	Passed	Model Under Test Equivalent Model
659c4b75cd31d3fb769b4343914729302ec94c94	Apalache	InstanceNamedWithInFolder	Enabled	True	Passed	Model Under Test Equivalent Model
e962da61340a864fcdf9b2ec3ae620e97fd8e7fb	Apalache	InstanceNamedWithInFolder	Enabled	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
73edbe7175e12de4586e6310055719ae987ce291	Apalache	Lambda	Enabled	True	Passed	Model Under Test Equivalent Model
d55b0c31529dbe4d78f6378a6bb966e5d0750b0b	Apalache	Lambda	Enabled	False	Passed	Model Under Test Equivalent Model
46d7c292d7de076086222e21e41c546daf03debc	Apalache	IfCond	Enabled	True	Passed	Model Under Test Equivalent Model
4e4f428f084ad7455ae0224415ac4de35d2104a8	Apalache	IfCond	Enabled	False	Passed	Model Under Test Equivalent Model
bb1fd94701673b11cb16b70897b9d75b3fd583bb	Apalache	IfThen	Enabled	True	Passed	Model Under Test Equivalent Model
2b4c81b46ee96390ad35eb099060cd43daa26413	Apalache	IfThen	Enabled	False	Passed	Model Under Test Equivalent Model
3bbd9de54dce11bcc9825249006313b6fa74ac82	Apalache	IfElse	Enabled	True	Passed	Model Under Test Equivalent Model
b4e88c4ace7a8d4ea4ba5ae2a70e148a48aa56b3	Apalache	IfElse	Enabled	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
e0b05b6ee0a988f4c5f41f322a8c94d6eb3576ce	Apalache	Equivalence	Enabled	True	Passed	Model Under Test Equivalent Model
e6370594eabd05d81590a263c47ca913e3da4c6d	Apalache	Equivalence	Enabled	False	Passed	Model Under Test Equivalent Model
26d930dc65d4b20ad67cb3746b167448cab15406	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Enabled	True	Passed	Model Under Test Equivalent Model
ea17097df405ddfae96e082f00e1cf3bc41345d8	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Enabled	False	Passed	Model Under Test Equivalent Model
6970b36b6948dc812ce0421aa90e04eeac296090	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Enabled	True	Passed	Model Under Test Equivalent Model
78f0e09e726ccedd0cf0bd3fce796ec1eb5d164a	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Enabled	False	Passed	Model Under Test Equivalent Model
c02ff7f21f5b294f491afa2fd730eda00e576e3a	Apalache	BagBagIn	Enabled	True	Passed	Model Under Test Equivalent Model
db575cbd1d2e9d80260ad3f7438b914308c3e573	Apalache	BagBagIn	Enabled	False	Passed	Model Under Test Equivalent Model
1e5c678abc2ccf994fcb78126d47917be1def97b	Apalache	BagCopiesIn	Enabled	True	Passed	Model Under Test Equivalent Model
22322f9b29aea600301f18fee459d64a2ab151bf	Apalache	BagCopiesIn	Enabled	False	Passed	Model Under Test Equivalent Model
fe5ce7c94ed5fbbf520b4e43f611232feeb04a9c	Apalache	SeqAppend	Enabled	True	Passed	Model Under Test Equivalent Model
12f772a5ca5b4130787e8073d7dd53dbeb7f0559	Apalache	SeqAppend	Enabled	False	Passed	Model Under Test Equivalent Model

Index

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