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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
706da1b468c81f5853ce350634a4fb6425bd9244	Apalache	And	NumLe	True	Passed	Model Under Test Equivalent Model
cc2c8a0ce9c6a9be308921ad328236958351e8b9	Apalache	And	NumLe	False	Passed	Model Under Test Equivalent Model
f075b81eb2db5b476a6b7491f5a98eb0d083650a	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NumLe	True	Passed	Model Under Test Equivalent Model
d072b4b9eca84fa78b81f4811b92354711a9ef55	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NumLe	False	Passed	Model Under Test Equivalent Model
4c9792ad912f869d4064a347a67fd72078e726d5	Apalache	Imply	NumLe	True	Passed	Model Under Test Equivalent Model
4d60859dfb52064c21cf35793c6638070f6b2bcd	Apalache	Imply	NumLe	False	Passed	Model Under Test Equivalent Model
5a90ada9f018d443a31d290d014f93a04bbed9d6	Apalache	Not	NumLe	True	Passed	Model Under Test Equivalent Model
c5f788cce1507cecac84317e0fe0a22899cd4eda	Apalache	Not	NumLe	False	Passed	Model Under Test Equivalent Model
c3577a6f0bb9e94f6648972086b6eaccd608a189	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NumLe	True	Passed	Model Under Test Equivalent Model
4f54472797ec39673049b08dd06366231b4e0fd2	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NumLe	False	Passed	Model Under Test Equivalent Model
4abc2066308d5ff6bfbcde2f1b25faffdb24ba7c	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NumLe	True	Passed	Model Under Test Equivalent Model
6b3a55c0bd61f1fdaff7c0a5b4a697988388565d	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NumLe	False	Passed	Model Under Test Equivalent Model
90d13ec06873d0e8a14d614fb3b07fb6e94cc2c1	Apalache	AndProp	NumLe	True	Passed	Model Under Test Equivalent Model
add309c8a1d3c633abe946483dc0aaa8f87f1810	Apalache	AndProp	NumLe	False	Passed	Model Under Test Equivalent Model
69c9a1a5b1e754da0b68329670bbe717c6a0dd76	Apalache	Boxed	NumLe	True	Passed	Model Under Test Equivalent Model
43f99a58ed2064d27de53673d69150131eb6206c	Apalache	Boxed	NumLe	False	Passed	Model Under Test Equivalent Model
cb91b14ec8590f9d30d1cc929b87408342bf0c6a	Apalache	Eq	NumLe	True	Passed	Model Under Test Equivalent Model
185ff3a6b7a3b4640b62f6a1c59193b9cf580245	Apalache	Eq	NumLe	False	Passed	Model Under Test Equivalent Model
1fa7044fd3adcaf3ee0241b98b196b762522c5a2	Apalache	Ne	NumLe	True	Passed	Model Under Test Equivalent Model
8502029eebcbe44c6a2271557e4440f347d5bd89	Apalache	Ne	NumLe	False	Passed	Model Under Test Equivalent Model
28068509151cfb9839a60b4481adf17667159abb	Apalache	Let	NumLe	True	Passed	Model Under Test Equivalent Model
560173feb1b63c4fd9acccbcd24b1ee185750e21	Apalache	Let	NumLe	False	Passed	Model Under Test Equivalent Model
2e02dcef5539fcd9fdfc433e67c969b61d25932c	Apalache	Set0	NumLe	True	Passed	Model Under Test Equivalent Model
8041755549c8d70b62133f55dbf3f7eacdcf7ce5	Apalache	Set0	NumLe	False	Passed	Model Under Test Equivalent Model
8c5c9cc70d97ffb3698e126bfd89189d55104822	Apalache	Set1	NumLe	True	Passed	Model Under Test Equivalent Model
2dda2d2a781ef247a2a036863fb049385cc56be6	Apalache	Set1	NumLe	False	Passed	Model Under Test Equivalent Model
3ee63be0b2c185b352908f7abe96a716854f1621	Apalache	Set2	NumLe	True	Passed	Model Under Test Equivalent Model
7dc1612d82e36d3f4003fa7944fbaee6bd87658a	Apalache	Set2	NumLe	False	Passed	Model Under Test Equivalent Model
b303edb56a0a3f9533dc7e78e2d9060751c64301	Apalache	Fun	NumLe	True	Passed	Model Under Test Equivalent Model
eb3548b4228af796d278224f2078cc410310dd4b	Apalache	Fun	NumLe	False	Passed	Model Under Test Equivalent Model
9350e7bba357c81f36f5b234311f0c8556bffe32	Apalache	In	NumLe	True	Passed	Model Under Test Equivalent Model
cc3fb509e6ea231e2c59203477610f2f2da7223b	Apalache	In	NumLe	False	Passed	Model Under Test Equivalent Model
2e1235c07463aa20655c9d85ef458827bedbd5e4	Apalache	NotIn	NumLe	True	Passed	Model Under Test Equivalent Model
2add9b8391638a802fed51e7180ddd250ef56c9e	Apalache	NotIn	NumLe	False	Passed	Model Under Test Equivalent Model
e0b7429fb1701c90407f170ac70902cce8aea6fa	Apalache	Exists	NumLe	True	Passed	Model Under Test Equivalent Model
7c9f5def29b95d03454b01ea9a2fc876d75ddccc	Apalache	Exists	NumLe	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
4493f66012b2bb44826f65d0defa60c9ca91e152	Apalache	Choose	NumLe	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
fd1f4c2fa95da9521dd80b2b24cfbce6a63fbc68	Apalache	Choose	NumLe	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
1333615049a34d36af58e1ea9abb9514692fe5ee	Apalache	Record	NumLe	True	Passed	Model Under Test Equivalent Model
5c24a738c8c3b3f30abb66313541724bcdd0cadd	Apalache	Record	NumLe	False	Passed	Model Under Test Equivalent Model
780f01aebab0fb32cefe97491f73ce5efba586ce	Apalache	Tuple	NumLe	True	Passed	Model Under Test Equivalent Model
b7659c7484810d6235b3b75c17a7ad548a652ec9	Apalache	Tuple	NumLe	False	Passed	Model Under Test Equivalent Model
15495a746306d9f212a0a8f5bd02d17c98ef77e6	Apalache	FunApp	NumLe	True	Passed	Model Under Test Equivalent Model
b3d7afbc4a5ce0e5386ee5951b9ed00534fa73d6	Apalache	FunApp	NumLe	False	Passed	Model Under Test Equivalent Model
85668276ecb25837e61fb2c56b0edd513a677ab1	Apalache	Except1Fun	NumLe	True	Passed	Model Under Test Equivalent Model
26405a1ac29cb4de57ef0ee2418f3ae3ea6f0dea	Apalache	Except1Fun	NumLe	False	Passed	Model Under Test Equivalent Model
9363a5d720f2edbe4cd199b06ff2c2bac380646b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumLe	True	Passed	Model Under Test Equivalent Model
ec1e483ceb65d7e12e63c4480954a6004796b141	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumLe	False	Passed	Model Under Test Equivalent Model
295a36a343911a31636b65d7f253284a820bac98	Apalache	Except1Rec	NumLe	True	Passed	Model Under Test Equivalent Model
78f5afdbe72482f43651386f587026ae050565d3	Apalache	Except1Rec	NumLe	False	Passed	Model Under Test Equivalent Model
9f22c2a3fd158640cff3ab516328710ea7c779dc	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumLe	True	Passed	Model Under Test Equivalent Model
c16cbc1e2d10ff850041be6ea7332f661338edee	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumLe	False	Passed	Model Under Test Equivalent Model
fd03cfb226cbc625ef16054534e5ad238e94bc0d	Apalache	Except2Fun	NumLe	True	Passed	Model Under Test Equivalent Model
37c218aabeb73ac6877f2d5c029f6511d65c1245	Apalache	Except2Fun	NumLe	False	Passed	Model Under Test Equivalent Model
cdb271883f3cadf0be2124ed908845646aec7551	Apalache	Prime	NumLe	True	Passed	Model Under Test Equivalent Model
ef921aa525add1761a264a46adee7d2c1d6e04f8	Apalache	Prime	NumLe	False	Passed	Model Under Test Equivalent Model
15ef75fdbc0cd67c9460be186016da1a57e4e0f7	Apalache	DefFun	NumLe	True	Passed	Model Under Test Equivalent Model
904585de29fe5308a2b16c9d4cb8452198526c3d	Apalache	DefFun	NumLe	False	Passed	Model Under Test Equivalent Model
010e34e3f630173288af2baadaf9237bc1ae0d25	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumLe	True	Passed	Model Under Test Equivalent Model
c8b200600dc2d45e0801e5174e68acdb1b385c46	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumLe	False	Passed	Model Under Test Equivalent Model
a11be8158969c88a0625cb2fc9611c3e7ffb2629	Apalache	DefFunRecursive	NumLe	True	Passed	Model Under Test Equivalent Model
34361354adeb5e4e45328143024dbe32bf39abbe	Apalache	DefFunRecursive	NumLe	False	Passed	Model Under Test Equivalent Model
2db862c4cf9018381116fa71ef72da4914123201	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumLe	True	Passed	Model Under Test Equivalent Model
659b20b00a47a642a9ba1633a710f50eec318814	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumLe	False	Passed	Model Under Test Equivalent Model
a62cd4f9a2e7815eb2fb5cc59a5f47ac613f71f7	Apalache	Def0	NumLe	True	Passed	Model Under Test Equivalent Model
ded4d1b802d399af8c412cc8346f1ef87f6600c3	Apalache	Def0	NumLe	False	Passed	Model Under Test Equivalent Model
9c801fa85815155fcee1d4c2c352039f6d0e8cc2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumLe	True	Passed	Model Under Test Equivalent Model
dd6b9decb81c911b8c13bc31a9786b745d196a2a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumLe	False	Passed	Model Under Test Equivalent Model
3824c7952a66252642eb716438e1ecb3fa6a8924	Apalache	Def1	NumLe	True	Passed	Model Under Test Equivalent Model
7d2c249cf23f556e8f01a55c7075a5301baa24e3	Apalache	Def1	NumLe	False	Passed	Model Under Test Equivalent Model
d8bf0181492c45c3a08514e1c9b38d1288cd48fb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumLe	True	Passed	Model Under Test Equivalent Model
1c6cc90f9d6e2fb3a5b3f99d61500bf8402fd825	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumLe	False	Passed	Model Under Test Equivalent Model
7bd152a2ac7e341c0b5fbd5fb23ccccbc90b89f4	Apalache	Def2	NumLe	True	Passed	Model Under Test Equivalent Model
79a0caff2b35314ded504a565e9f3150c6c190a7	Apalache	Def2	NumLe	False	Passed	Model Under Test Equivalent Model
821cd4f79d6b084c30c342d451782a9aac28eab0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumLe	True	Passed	Model Under Test Equivalent Model
a15a3a4329e533f9e53fd1b252c71375e2fb2945	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumLe	False	Passed	Model Under Test Equivalent Model
88ec959f852211bfe5aba600991f0712d97c6a45	Apalache	Def1Recursive	NumLe	True	Passed	Model Under Test Equivalent Model
771b166a4b58557ba60e4b6d2f2d168207ddf5a8	Apalache	Def1Recursive	NumLe	False	Passed	Model Under Test Equivalent Model
026c67d1738c65e1ead1223602ac1aff7d16a1e7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumLe	True	Passed	Model Under Test Equivalent Model
4e024918c4878a7226bd1324301a376700513864	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumLe	False	Passed	Model Under Test Equivalent Model
b67480410d705cd43ece20a4c3130dd57d83017d	Apalache	Extends	NumLe	True	Passed	Model Under Test Equivalent Model
bf4df8f866b89f9e811173550b96bb2c99c31a96	Apalache	Extends	NumLe	False	Passed	Model Under Test Equivalent Model
1257d495c9ebb99ee3fa2c8144d0a3f690839952	Apalache	ExtendsInDifferentFolder	NumLe	True	Passed	Model Under Test Equivalent Model
bb3c6bd22c8a097f45f43a32118d4f747ef70f5a	Apalache	ExtendsInDifferentFolder	NumLe	False	Passed	Model Under Test Equivalent Model
85caebe5763efd1d38fbfab851bfaf5f6825e239	Apalache	Variable	NumLe	True	Passed	Model Under Test Equivalent Model
64aca7520f430d9b5910de80268082b1a5b836ab	Apalache	Variable	NumLe	False	Passed	Model Under Test Equivalent Model
c49a6a08bf7c6b532894f90d39e0f149c71cdbec	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumLe	True	Passed	Model Under Test Equivalent Model
38d1dd04e19f237d0e018826a15b437290e95f4c	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumLe	False	Passed	Model Under Test Equivalent Model
fb22d061423d72886dc6f923409740352ac64fd0	Apalache	Constant	NumLe	True	Passed	Model Under Test Equivalent Model
8599ce19893eaccd155e845f8e7eb520bd956b71	Apalache	Constant	NumLe	False	Passed	Model Under Test Equivalent Model
1058b11458109201b9260ed2d00c95b1e6407634	Apalache	ConstantRank1	NumLe	True	Passed	Model Under Test Equivalent Model
41dc3b2552985a10b0ecc6e828f3d07bd034370e	Apalache	ConstantRank1	NumLe	False	Passed	Model Under Test Equivalent Model
f256ad67cf46ad7d9e8a74f742004981a190e9ef	Apalache	Instance	NumLe	True	Passed	Model Under Test Equivalent Model
b57a4f039fb474fe2610c38b1e507b6e104d3931	Apalache	Instance	NumLe	False	Passed	Model Under Test Equivalent Model
f0a0fac12c02e43e0e422ca36ea952893bf0885a	Apalache	InstanceWith	NumLe	True	Passed	Model Under Test Equivalent Model
c9ca23d2d29ee22740bf65845799b5bd3a966446	Apalache	InstanceWith	NumLe	False	Passed	Model Under Test Equivalent Model
a6125ffabe28db9490db48886d46c2d893a957af	Apalache	InstanceNamed	NumLe	True	Passed	Model Under Test Equivalent Model
ab4318f3021034675d11370eb415c33019b48f5b	Apalache	InstanceNamed	NumLe	False	Passed	Model Under Test Equivalent Model
0b7952bc2bc48063f75097af849da268311f9fac	Apalache	InstanceNamedWith	NumLe	True	Passed	Model Under Test Equivalent Model
688ebbaa118d10f4100c4496b391294da5bf918e	Apalache	InstanceNamedWith	NumLe	False	Passed	Model Under Test Equivalent Model
5d8e0006504fed70c0626965531901bb565980cf	Apalache	InstanceInFolder	NumLe	True	Passed	Model Under Test Equivalent Model
7927af66887d5b641c2a8223e0327851ab28b055	Apalache	InstanceInFolder	NumLe	False	Passed	Model Under Test Equivalent Model
9c05af101b5f9aea390ae5abda74bd570b2a142c	Apalache	InstanceWithInFolder	NumLe	True	Passed	Model Under Test Equivalent Model
1551954543c43d58e6ee5c097434824625a5d55e	Apalache	InstanceWithInFolder	NumLe	False	Passed	Model Under Test Equivalent Model
52f3c1c51a7cc0ad48d7315bd177be0c27254dc1	Apalache	InstanceNamedInFolder	NumLe	True	Passed	Model Under Test Equivalent Model
e3191646da31c7f7ad0a028f17aa48a4dde806d4	Apalache	InstanceNamedInFolder	NumLe	False	Passed	Model Under Test Equivalent Model
a1828a0a4242a3412321fc98e29eb2ca75b2c855	Apalache	InstanceNamedWithInFolder	NumLe	True	Passed	Model Under Test Equivalent Model
cc3c8f15fc0afcae196cbbbb56b85e286f3935b2	Apalache	InstanceNamedWithInFolder	NumLe	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
9907a68d07c8e523e66fb81348af0eb32c1cb759	Apalache	Assume	NumLe	True	Passed	Model Under Test Equivalent Model
261c78ee44da22391af12427bcff7c197a652241	Apalache	Assume	NumLe	False	Passed	Model Under Test Equivalent Model
f1104aa13a5157184e8c7a5eddbb8d7dc7eadb5a	Apalache	AssumeNamed	NumLe	True	Passed	Model Under Test Equivalent Model
20402a8c90d33cb8c40ac0c708ca96dc4d1c59d9	Apalache	AssumeNamed	NumLe	False	Passed	Model Under Test Equivalent Model
95076204d44a1b19800909bcdf610de37bf719a5	Apalache	Lambda	NumLe	True	Passed	Model Under Test Equivalent Model
73a69490d1df50d7dc08068048ee01099a57333a	Apalache	Lambda	NumLe	False	Passed	Model Under Test Equivalent Model
9ad1563a063b18adb1d10828357e86b4451c2115	Apalache	IfCond	NumLe	True	Passed	Model Under Test Equivalent Model
a3dbbaebd852e576a94ba1910d90f791aa6c311a	Apalache	IfCond	NumLe	False	Passed	Model Under Test Equivalent Model
5449ac38427d4ecc9ea8f2aa8cd8ec183b8f9b72	Apalache	IfThen	NumLe	True	Passed	Model Under Test Equivalent Model
c48bc6ebfe7bf2d79616923c2554e22585200bc2	Apalache	IfThen	NumLe	False	Passed	Model Under Test Equivalent Model
73e3261235966e01889662d8454a066d9cdba140	Apalache	IfElse	NumLe	True	Passed	Model Under Test Equivalent Model
33be60c60fd47e4ed12dcb9b0045da3b4d79ad69	Apalache	IfElse	NumLe	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
a2a9f8faa7bbe30090f595fa19488e695b5d3e93	Apalache	Equivalence	NumLe	True	Passed	Model Under Test Equivalent Model
642978eb90264d5d3bd24ad3c220e05fc6d9d510	Apalache	Equivalence	NumLe	False	Passed	Model Under Test Equivalent Model
bacfb217ed6ae88abedfab55adce0bfacb4d33b3	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumLe	True	Passed	Model Under Test Equivalent Model
7e708c474bc9568e207a6d9c9d16168605dc8b33	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumLe	False	Passed	Model Under Test Equivalent Model
5a2ffce9f93084d073e94f0c436d8cdb339dc7e9	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumLe	True	Passed	Model Under Test Equivalent Model
a466e25dca2d6aaf1578eacd143bcf9345cd757e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumLe	False	Passed	Model Under Test Equivalent Model
6001b3c708512e59a48fc8b2345e189943356cbd	Apalache	BagBagIn	NumLe	True	Passed	Model Under Test Equivalent Model
5099f3cf13eebf9ac6cc545567a93ae1b9b55379	Apalache	BagBagIn	NumLe	False	Passed	Model Under Test Equivalent Model
18a68265094bce70008cd091474ce7bfb1091096	Apalache	BagCopiesIn	NumLe	True	Passed	Model Under Test Equivalent Model
b58c9d0389b09a868261e971ecc988b8dd7bbab6	Apalache	BagCopiesIn	NumLe	False	Passed	Model Under Test Equivalent Model
3d2940c488b8a764cd5e4c64e660224550f31c56	Apalache	SeqAppend	NumLe	True	Passed	Model Under Test Equivalent Model
592237afd1347cc02a776fbb3ef674f623ef10c2	Apalache	SeqAppend	NumLe	False	Passed	Model Under Test Equivalent Model

Index

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