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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
075b5284839238612156df4bd45a20700f3e706b	Apalache	And	BagBagIn	True	Passed	Model Under Test Equivalent Model
b259291ace3761bef9957ecb04c6b3286b36757b	Apalache	And	BagBagIn	False	Passed	Model Under Test Equivalent Model
1e277176ea3587c0985bce12f063f8cb50e87d2b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	BagBagIn	True	Passed	Model Under Test Equivalent Model
4ed928469be561f5365e9107d312ac3147b8445d	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	BagBagIn	False	Passed	Model Under Test Equivalent Model
fb7574bd72fea35618dc117779fba5e267e6e7e9	Apalache	Imply	BagBagIn	True	Passed	Model Under Test Equivalent Model
21a0ae69196f3e12df69bff8dc8900de1b183818	Apalache	Imply	BagBagIn	False	Passed	Model Under Test Equivalent Model
b700e6f3d9f1b62a91a4b64682498fa56f4999e6	Apalache	Not	BagBagIn	True	Passed	Model Under Test Equivalent Model
84aaa221832734a338785a2cb8a1f73c4dffdbc8	Apalache	Not	BagBagIn	False	Passed	Model Under Test Equivalent Model
3f696cb7c59ceed987daa7c25680806d5f7171f1	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	BagBagIn	True	Passed	Model Under Test Equivalent Model
3b5f313fc3feb54eb6f219e64d104523aecc5406	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	BagBagIn	False	Passed	Model Under Test Equivalent Model
5ba49e659753a8f00d916352126eb2f003aac550	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	BagBagIn	True	Passed	Model Under Test Equivalent Model
0b5d73c6a064cbab066109e6b317fbc8e21173a8	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	BagBagIn	False	Passed	Model Under Test Equivalent Model
fc0bb98f6e30d8c6accd8bb7d31395016e4af5ac	Apalache	AndProp	BagBagIn	True	Passed	Model Under Test Equivalent Model
49899a521d4b95a86c211e3edd559c88005dafab	Apalache	AndProp	BagBagIn	False	Passed	Model Under Test Equivalent Model
071c3923265ed35ccf799af3174b45e2f93a8d4b	Apalache	Boxed	BagBagIn	True	Passed	Model Under Test Equivalent Model
31ba79d1ace67d5f76f143087dba4a6043382917	Apalache	Boxed	BagBagIn	False	Passed	Model Under Test Equivalent Model
180879fe8d10cfbeaf710c87c0550965644e815b	Apalache	Eq	BagBagIn	True	Passed	Model Under Test Equivalent Model
42f3de3dd8e5b3f85bdd54b3df7bf7b7135861d4	Apalache	Eq	BagBagIn	False	Passed	Model Under Test Equivalent Model
7cbf04e9c81d467a2b3a33b87d13f5e51f4c7427	Apalache	Ne	BagBagIn	True	Passed	Model Under Test Equivalent Model
c8378c0ced14a7ea7e33aeee962b978f7fbaecf7	Apalache	Ne	BagBagIn	False	Passed	Model Under Test Equivalent Model
d492346b4558f2c0d0875e50e4ed13b7bd8e40a9	Apalache	Let	BagBagIn	True	Passed	Model Under Test Equivalent Model
b4147996b5263ed9c22f79372135999f3df647a5	Apalache	Let	BagBagIn	False	Passed	Model Under Test Equivalent Model
33cb8dff1d4f6807b66ce35fb85bf97942d29890	Apalache	Set0	BagBagIn	True	Passed	Model Under Test Equivalent Model
a1e71fffb2480c12df7cfa5b50356f8cb4eafc9c	Apalache	Set0	BagBagIn	False	Passed	Model Under Test Equivalent Model
7c89986ea7ef4405ab73c88617cea7a661be6aad	Apalache	Set1	BagBagIn	True	Passed	Model Under Test Equivalent Model
31e4f813877da5665a0bb32da48a101ad3ae6152	Apalache	Set1	BagBagIn	False	Passed	Model Under Test Equivalent Model
981655d9b5f67db81716ef6cb38ab260ee0f3fcc	Apalache	Set2	BagBagIn	True	Passed	Model Under Test Equivalent Model
57ba2804b8d63f42e3e9ec897e2e393936539363	Apalache	Set2	BagBagIn	False	Passed	Model Under Test Equivalent Model
3035b982aff40234217b26d3db6ac6dc35aa09a4	Apalache	Fun	BagBagIn	True	Passed	Model Under Test Equivalent Model
bc63fdc572fd0cfc7c0683505becea8b53c4cda8	Apalache	Fun	BagBagIn	False	Passed	Model Under Test Equivalent Model
3333965b6c77a346a9c6dfdfa55a87a991e8de98	Apalache	In	BagBagIn	True	Passed	Model Under Test Equivalent Model
b69b2dec7a6ea1a8fe930e19e54d4c33b466bad0	Apalache	In	BagBagIn	False	Passed	Model Under Test Equivalent Model
33e9234283ef7d22d488fcd04b14121732923707	Apalache	NotIn	BagBagIn	True	Passed	Model Under Test Equivalent Model
fdccf38314d8d4f3e51c0d52bf0ace880278f0fa	Apalache	NotIn	BagBagIn	False	Passed	Model Under Test Equivalent Model
52ac2555ada96addccc00de61adc58e84c93f32a	Apalache	Exists	BagBagIn	True	Passed	Model Under Test Equivalent Model
dc308f74c1774fac273865287ccd880e7464d968	Apalache	Exists	BagBagIn	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
65cf83d03843a162e4db3125fda5c3129da22212	Apalache	Choose	BagBagIn	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
8a3d42c2decdc31f60dacb204bb371dd57296414	Apalache	Choose	BagBagIn	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
a4af553dda768e78a818ce3e236eff4769796d79	Apalache	Record	BagBagIn	True	Passed	Model Under Test Equivalent Model
00f0c4ced4d83213ef27f2b60842e87df5c6884d	Apalache	Record	BagBagIn	False	Passed	Model Under Test Equivalent Model
cd5694b4f17bfd4678fcfbbff22b77023e98b5af	Apalache	Tuple	BagBagIn	True	Passed	Model Under Test Equivalent Model
be697d1553a5447cc694dac6324a57a8be6d9e6e	Apalache	Tuple	BagBagIn	False	Passed	Model Under Test Equivalent Model
699ee502e45f1a6e35e05483551294b68b2a223b	Apalache	FunApp	BagBagIn	True	Passed	Model Under Test Equivalent Model
6a95b91aa7431a0f337043289d53e0f345beeecf	Apalache	FunApp	BagBagIn	False	Passed	Model Under Test Equivalent Model
dad37f3fcbf3b2f8a322f638826fd77255dfce7a	Apalache	Except1Fun	BagBagIn	True	Passed	Model Under Test Equivalent Model
cc5825bf95af876fdc7afd78d440849828f0a98b	Apalache	Except1Fun	BagBagIn	False	Passed	Model Under Test Equivalent Model
dd0a19d4f2dd19af1b5a184e10472e8c26b393e0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagIn	True	Passed	Model Under Test Equivalent Model
2ecb1997f5ca1722f7b08266a957ad34c32ce173	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagIn	False	Passed	Model Under Test Equivalent Model
73ffcdab5ec19cd2b685a7d48c7b25f3ae6c0af2	Apalache	Except1Rec	BagBagIn	True	Passed	Model Under Test Equivalent Model
d88ff9e00628837f07e6ffb30577e4a76b5ec4fa	Apalache	Except1Rec	BagBagIn	False	Passed	Model Under Test Equivalent Model
dae30049a3b60238cba55c9ac40fedbc19f4b099	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagIn	True	Passed	Model Under Test Equivalent Model
b2f550b970ae84e1e3e98ad90a965e2eee87d623	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagIn	False	Passed	Model Under Test Equivalent Model
05c42942a5428dc90cf99e7f3e09b44d7dc31efd	Apalache	Except2Fun	BagBagIn	True	Passed	Model Under Test Equivalent Model
71f7e735428c9ea9b5d6dffe09e25aaa9346f9c0	Apalache	Except2Fun	BagBagIn	False	Passed	Model Under Test Equivalent Model
1ba3caa76c8693c0f595a246ffb3202b15e0bd87	Apalache	Prime	BagBagIn	True	Passed	Model Under Test Equivalent Model
19e346b644738f3891bbae4eadb1fbd02e83430f	Apalache	Prime	BagBagIn	False	Passed	Model Under Test Equivalent Model
8e7cd6faf85c6bc869e87de1d26efb53e7b18406	Apalache	DefFun	BagBagIn	True	Passed	Model Under Test Equivalent Model
bd8cb8b8318fa43a451efb58e6150969c736813a	Apalache	DefFun	BagBagIn	False	Passed	Model Under Test Equivalent Model
71eb88cdb6147a592f2a5bc794ea9b9beee3f8fa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagIn	True	Passed	Model Under Test Equivalent Model
9f996c22766a340417a46e2a82e0c61da98e7b82	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagIn	False	Passed	Model Under Test Equivalent Model
89fc4ad72306bc1c1b06d692be5f2f2daff4c332	Apalache	DefFunRecursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
4c06387edd31f678fa9ea99230a05d7de445821a	Apalache	DefFunRecursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
1b0a5b63477d165c3b36c50259259523a36b6d65	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
9577baf162353e005fb70156b3c0eaf2672aafc8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
5aed43d8a80aa18ab737bce42387b0415914a3f1	Apalache	Def0	BagBagIn	True	Passed	Model Under Test Equivalent Model
514dd55e4c1af60643a81894a8eda50cf18655b3	Apalache	Def0	BagBagIn	False	Passed	Model Under Test Equivalent Model
b423f4c424d6d282ff3d9655101bc1cd4319dd4b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagIn	True	Passed	Model Under Test Equivalent Model
81ab5cc8bddad8e7d04e24ea61e40312d30b493f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagIn	False	Passed	Model Under Test Equivalent Model
49a6848e5a881104f938be4950979cac73c5d398	Apalache	Def1	BagBagIn	True	Passed	Model Under Test Equivalent Model
0d17cd6f039e1ce7e0be9941f8aa0730706fa483	Apalache	Def1	BagBagIn	False	Passed	Model Under Test Equivalent Model
a6850ad0af5427b9e5095d382c32a6e819a2839c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagIn	True	Passed	Model Under Test Equivalent Model
79b3dc74e35749c1514f7131587a2dcb6310b0b8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagIn	False	Passed	Model Under Test Equivalent Model
0ce1b0a7f1b43b92550976dd0bbcd437331d081b	Apalache	Def2	BagBagIn	True	Passed	Model Under Test Equivalent Model
154469579c898ec753b801bfba189900a5cef82b	Apalache	Def2	BagBagIn	False	Passed	Model Under Test Equivalent Model
b1494bad60e777a6da920a67e1bf7abaef4a1dc7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagIn	True	Passed	Model Under Test Equivalent Model
88c4e839ed709c9dca985a48a4aa75a584a2483d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagIn	False	Passed	Model Under Test Equivalent Model
a72d0c7c6a98cc6577a3321576bcc855dd0d6ae8	Apalache	Def1Recursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
dd8be872b7f2a8310418419dd0e7b4679cf14f40	Apalache	Def1Recursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
f5e262eef73a045723e217b5598cda039b34d016	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
cfe40a3e5f821ab5ebfb0616b9ac0d80708bdbcb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
adc8441965ad261d3a19da0736c6bf48a5607695	Apalache	Extends	BagBagIn	True	Passed	Model Under Test Equivalent Model
bd10699b3df8ac83fb0349de4adc98fe7d54b532	Apalache	Extends	BagBagIn	False	Passed	Model Under Test Equivalent Model
0d9fc11e5d0d083921ce5623f62b9760bf719ccd	Apalache	ExtendsInDifferentFolder	BagBagIn	True	Passed	Model Under Test Equivalent Model
d82ee577704a6c9ecb8e8c2c790a911949a05e43	Apalache	ExtendsInDifferentFolder	BagBagIn	False	Passed	Model Under Test Equivalent Model
808a627d7767dd92eb010de2691ea339a731e05d	Apalache	Variable	BagBagIn	True	Passed	Model Under Test Equivalent Model
a9626aa5b7aee52309e8128c6a86303025d9a2df	Apalache	Variable	BagBagIn	False	Passed	Model Under Test Equivalent Model
859d58e347803742f85a3731cf78c73d7cb60377	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagIn	True	Passed	Model Under Test Equivalent Model
35c1d7ed7b507df8036e2ef0d46d7b087561d122	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagIn	False	Passed	Model Under Test Equivalent Model
300ca175d0ba0bf32e375dfe8b888ce43ad2e32d	Apalache	Constant	BagBagIn	True	Passed	Model Under Test Equivalent Model
21410d8c4dcc3be0fa7d0cb3833ecafa60052817	Apalache	Constant	BagBagIn	False	Passed	Model Under Test Equivalent Model
9a86b84b5c600b2fbddb1b5683e72c307fb2b738	Apalache	ConstantRank1	BagBagIn	True	Passed	Model Under Test Equivalent Model
79c0ad9dff627718a4e562b865c9397a40a9de27	Apalache	ConstantRank1	BagBagIn	False	Passed	Model Under Test Equivalent Model
b61a588bad8663578362385935015b4db3aa55fc	Apalache	Instance	BagBagIn	True	Passed	Model Under Test Equivalent Model
1cd9b41f454f679343cc07851a990c6b1b19e134	Apalache	Instance	BagBagIn	False	Passed	Model Under Test Equivalent Model
d8652fb870a4527e6d1ccee02404a1da21dfc7b9	Apalache	InstanceWith	BagBagIn	True	Passed	Model Under Test Equivalent Model
17d772ea386ec78f1a0055572376f7a8f8c0ffbc	Apalache	InstanceWith	BagBagIn	False	Passed	Model Under Test Equivalent Model
a89b39bd6c966df38010dbd70161f28db93d9491	Apalache	InstanceNamed	BagBagIn	True	Passed	Model Under Test Equivalent Model
6d0b2fb07c8717c5e5125b42d25b851da909a6d0	Apalache	InstanceNamed	BagBagIn	False	Passed	Model Under Test Equivalent Model
a53716a2b2a953f2bb549964ac1da13a9ad7a038	Apalache	InstanceNamedWith	BagBagIn	True	Passed	Model Under Test Equivalent Model
9e881b3dea17e9106e761fea80305b60f41233c3	Apalache	InstanceNamedWith	BagBagIn	False	Passed	Model Under Test Equivalent Model
ba68835407bb8935746a6507b4625526816abba4	Apalache	InstanceInFolder	BagBagIn	True	Passed	Model Under Test Equivalent Model
75db41974ad46c6d7c1d6a1395da8c4d9aee2cb0	Apalache	InstanceInFolder	BagBagIn	False	Passed	Model Under Test Equivalent Model
633ab4ef135a048c7d08880437ab8f9c68a449ca	Apalache	InstanceWithInFolder	BagBagIn	True	Passed	Model Under Test Equivalent Model
f7084a6206306752e84e82314ba464db6737ed3f	Apalache	InstanceWithInFolder	BagBagIn	False	Passed	Model Under Test Equivalent Model
5a81b5f67d5761d73e86282eb901ea7d6a44db3e	Apalache	InstanceNamedInFolder	BagBagIn	True	Passed	Model Under Test Equivalent Model
02ebd42127c4931f39f17ae45aec10384bb42576	Apalache	InstanceNamedInFolder	BagBagIn	False	Passed	Model Under Test Equivalent Model
268f24e1ddffb119e010ba7ad2ed4dd06870421e	Apalache	InstanceNamedWithInFolder	BagBagIn	True	Passed	Model Under Test Equivalent Model
5ee710c0f8ce705b398cbee97d1e7c69a2fdcaf1	Apalache	InstanceNamedWithInFolder	BagBagIn	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
63e029213e913466172281e8378b44c16fd7519e	Apalache	Assume	BagBagIn	True	Passed	Model Under Test Equivalent Model
72664287f1a7535210d4d448adb65d675b47366b	Apalache	Assume	BagBagIn	False	Passed	Model Under Test Equivalent Model
fcae7d5161b56cfe35d24b064db14d386de66fd9	Apalache	AssumeNamed	BagBagIn	True	Passed	Model Under Test Equivalent Model
7655faab407a2e22f5a516bb57a9d36655230592	Apalache	AssumeNamed	BagBagIn	False	Passed	Model Under Test Equivalent Model
fac7e309a67a799e682f0939b26e5b2a71f8c3b8	Apalache	Lambda	BagBagIn	True	Passed	Model Under Test Equivalent Model
139704ca64b5a0a0376b1a8b4694c7ace507fcf4	Apalache	Lambda	BagBagIn	False	Passed	Model Under Test Equivalent Model
cf14e12a301d77145778c0fd16493c17f7616c3f	Apalache	IfCond	BagBagIn	True	Passed	Model Under Test Equivalent Model
5a729e2610df85f8d98e303ec693709f68d34fce	Apalache	IfCond	BagBagIn	False	Passed	Model Under Test Equivalent Model
ee3257d399fb06f4d99f8229111f18c0d062765f	Apalache	IfThen	BagBagIn	True	Passed	Model Under Test Equivalent Model
0a3da56f75eb942a6058306d8d2c7438f1b8bcfa	Apalache	IfThen	BagBagIn	False	Passed	Model Under Test Equivalent Model
213cd059b697fa5767b568cea7f27024172f54d3	Apalache	IfElse	BagBagIn	True	Passed	Model Under Test Equivalent Model
30210cc5eff49d2d27870596f89ab12f89b0bc81	Apalache	IfElse	BagBagIn	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
5ac5a681b18aa05a52d481741caac4aae83c76d9	Apalache	Equivalence	BagBagIn	True	Passed	Model Under Test Equivalent Model
82f978d3bf598d11c144197e6e82ad3576a182a3	Apalache	Equivalence	BagBagIn	False	Passed	Model Under Test Equivalent Model
21f7ad24e1da031ab354d089f478a8504f51d103	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagIn	True	Passed	Model Under Test Equivalent Model
7c4b5b559d24d3b31b5ec8c4e6be542d5138de46	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagIn	False	Passed	Model Under Test Equivalent Model
4f7847880a7bef8cbf0896aa15a8bafcd15b3242	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagIn	True	Passed	Model Under Test Equivalent Model
8a5d761ea722fb586f85f40ba5d07fa167a5d67b	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagIn	False	Passed	Model Under Test Equivalent Model
a0877d32ed62a039215b9d0cfb645bf394270715	Apalache	BagBagIn	BagBagIn	True	Passed	Model Under Test Equivalent Model
bf0abc06e55b2c726cff843e566a9c2e75c784eb	Apalache	BagBagIn	BagBagIn	False	Passed	Model Under Test Equivalent Model
169a6cab64268ef8b0c42340dcd355f3e43eb092	Apalache	BagCopiesIn	BagBagIn	True	Passed	Model Under Test Equivalent Model
c5972abf9176f0b7d20f076e3a3be7e168b7056e	Apalache	BagCopiesIn	BagBagIn	False	Passed	Model Under Test Equivalent Model
36a84b3ac66079f91c79330109f109e8481d5113	Apalache	SeqAppend	BagBagIn	True	Passed	Model Under Test Equivalent Model
85f3c2d3867a56897c99027ef430e522abaa324e	Apalache	SeqAppend	BagBagIn	False	Passed	Model Under Test Equivalent Model

Index

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