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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
36e4807aae9e3f3e7a45849806f736d7ec23170d	Apalache	Eq	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b5d4a242ee4dd096380d4e8c7b352fac177c221c	Apalache	Eq	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
86e0bc6c861e258e4d4db41e7d0875a29b1d1333	Apalache	Ne	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
809d69e7f172934a7183ded1e8f41af3be23c8ad	Apalache	Ne	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
e2c5a6b07d0944e3bfd39caf281556ecae6e4bd1	Apalache	Let	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
25389eee8747c2dc13ba81df46b8b8a7bde2e6ed	Apalache	Let	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
9d3b65c997260d821e1fdda0d41b14e02b44cceb	Apalache	Set0	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9716e16434df6b47736b72c47f3cd83d3904b4f3	Apalache	Set0	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
ff677f7d77d1122b65c4d8ced6cc68fffb94fc27	Apalache	Set1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
528a52c07e8938d9ec16167fda3fdb02f6d590f6	Apalache	Set1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
d913f005eb8a4c7fd7b1bada28a5c489313e82d0	Apalache	Set2	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
bea2949d053a6f684df68242e6ba2a15433279ba	Apalache	Set2	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
266bcf7bdb3956536c561013069aacb32b3539e3	Apalache	Fun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
54bb0c972e6cabc74a2a1677e0102a1226d1525a	Apalache	Fun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
92bec56fdfe45eecb00497ce47418212d14c8366	Apalache	In	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
7295980d8250442c5f321c1242f1832ca4edb72b	Apalache	In	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
86514bab2042d3c81f559f1aac8693686f202f84	Apalache	NotIn	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
f616adbbea0213f26db396d2e912d371e837eb14	Apalache	NotIn	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
45ab57444a590d5672149cf556e10b00ff01eb79	Apalache	Record	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
524284894d3c2dcae99690e9467b0b4e648909b8	Apalache	Record	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
eb884c0c4dcfdd7ce27f74e8ba43952fdb83941b	Apalache	Tuple	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
150c211b2360f68978cefde954959aa595d71c9b	Apalache	Tuple	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
3068142bba536c7e26b09d4598ae91ccc1484b78	Apalache	FunApp	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b85505941a6ce3a98933ec70e6f4bc4db4f9317c	Apalache	FunApp	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
948388ad5bc6db8350bdf1512a7d9913fc3aab3c	Apalache	Except1Fun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
207f715b3cceb85e62ff816e9c051e48d5e3727d	Apalache	Except1Fun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
4b7430d712ea0e7a53f6e50828141d95cc905e3a	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9b8c4e0462fec307505950beb0acb202da1512c2	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
66192dce7d6aba1746fde3eaef2d8cb1f9f5dbff	Apalache	Except1Rec	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
d085908bd3ce869ebd95dc62fe6350a843c01649	Apalache	Except1Rec	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8db17b737776c2e0dc32e28174e9fd58b0e609a0	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
7ce5a69b9920519ea3f20cf8441a80ff7f76a3d6	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
fbae0449d7abb899da21d70fe7e8e5d23f01868f	Apalache	Except2Fun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
64669de3ef80d2b23daf94f47dcff4e5d9aec83e	Apalache	Except2Fun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8c2862a39a21eabc5e5f1a29c0f12804deb62bb4	Apalache	Prime	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b4f56eac009657c5cbd92f5735dc6d29623a4cab	Apalache	Prime	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
cf1d5cb0d2c11071b9e8f75b272a737aefe4fa97	Apalache	DefFun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
dbc1543d8456e389571c9e24f175305902346133	Apalache	DefFun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
fe3ab3d3d1332302c6c4fc83a491da1123d39c8b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
01dcb3ce04583cc4b4d3a30263528a0a52b9b753	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
7c6943937e154bb16d6039bbc228351bfbacf170	Apalache	DefFunRecursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
2c1048d284f6ae794182cae10a7dc090b81c9770	Apalache	DefFunRecursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
b9856ff0433d8073e624da43499051f277b4b5d9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
c0a150b689e0086c61140fd137c602c488a4e83e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
61eab3a62b3b3765423a31bdb1d5a9b6cb119aff	Apalache	Def0	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
84109080847331241f333a809d45ffbbd2ffdd83	Apalache	Def0	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
17d745f1cfee6b201eb5f22ea637dc241c076887	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3d46ba645c687292090314b07200f2d7903073d4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
6f2d543df1dd1a0ee00569cac8abeda42aa59438	Apalache	Def1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3fb5ccbac9172713d309e4a5957fa5918260d32b	Apalache	Def1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
13b4380d83c842dfb67f8c7879a837ff30bac0bb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
4d2b5d9691b5d61577af85c1605bab8fef509a8c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
1d4a25eb5fdba69d2eb86432472c0a83105a274a	Apalache	Def2	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
11175529657fef33aaccf74f03ba70bec3dbbc9e	Apalache	Def2	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
d3604fb7e322bf6248f930560b2a591264ae6699	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
1c228b9859ee618d50c7343fab96bf0d1882f49a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
07297c33b96d883d4bcebd276a838a875e33c8a2	Apalache	Def1Recursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9f41deb79db5d0cb5a614c71711f73d149e5e72c	Apalache	Def1Recursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
48c1edd28c9bb3d0677875cff3188c81ec47778d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3a8c5f07514191dfefe7b629ef05a31e84f148aa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8fa72b476877aed1137dc37bc0112127c28beaf0	Apalache	Extends	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
0c37cc504d1492bc78df4c8ad2bd6e760a7d3fc9	Apalache	Extends	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
b1ed8a74b191176043878d5ca59e44da5e721ac1	Apalache	ExtendsInDifferentFolder	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
62e8868294c998ae1b79b920a9a0e6e8d5e09e22	Apalache	ExtendsInDifferentFolder	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
70b6e93d75d5da89bb39b44140c6586a83e3db45	Apalache	Variable	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
e62a761b8b707827a665ba6e542afddc6f34b8d2	Apalache	Variable	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
59c9bfec48a900440cce27feb5b3842ad47eb5ef	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
cf1f16ae1e877080595a051812a9c391eb0c3c41	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
6a9768ddb8bd6bd47902075027bddda29d336786	Apalache	Constant	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
a9acdb1ef0bc14f804e06e13897542bc7228f003	Apalache	Constant	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
49eab2d4425daaadcce21b790d02030d2bd37300	Apalache	ConstantRank1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
ef888b4405913a1c678df7115489c37cd836ffc8	Apalache	ConstantRank1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
96e001da500c83b8ffdc99a9656822303548548b	Apalache	Instance	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
8e7f8c565f3efa48c035025e9d146b5f71b62290	Apalache	Instance	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
872dcd035a714a3c7ecd9989935e0ed449410c76	Apalache	InstanceWith	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
6db545d239d6778ab0d14f69f7a5392f35b356a6	Apalache	InstanceWith	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
59b41b82efc639b9b7c095ac6dbe6ba7e4ef5d58	Apalache	InstanceNamed	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9d6caafdbf7597bb88c02adbb204d37fa352d462	Apalache	InstanceNamed	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
88c15c1fb5ed9b02129205adfe02e6a3f8f8c41c	Apalache	InstanceNamedWith	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3fa2710625ae53a22b02c71019ee548179d0d240	Apalache	InstanceNamedWith	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
32daa0cfd7b17f0d3e4e753462ec3ce4980186e6	Apalache	InstanceInFolder	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
2dcaa4c2d8f2272f5b65fb4c2f31713f07c772a9	Apalache	InstanceInFolder	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
c4aedab465bae333e1d59b4c9814bbf158e144bc	Apalache	InstanceWithInFolder	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
051ddfc0bc58beb968e66ee58da0b0f8351ce68e	Apalache	InstanceWithInFolder	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
c66aa2da82e634ebefdad3535bfbd02d8b6f2fa5	Apalache	InstanceNamedInFolder	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
ebf0283273da27e2f52accca17a3635e24cc622a	Apalache	InstanceNamedInFolder	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
c4d23432941d694a97a1a206e94dd4ea11df6581	Apalache	InstanceNamedWithInFolder	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
912e55e2d8383e9039a8519b556976cfa850f3be	Apalache	InstanceNamedWithInFolder	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
a942cb994b060c986d3539229be6624a7369353f	Apalache	Lambda	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
62465e21897a7ed58669acdf4a6652647f1c3d30	Apalache	Lambda	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
f68398bca4f7aaad0508abba4bd41e31ae247677	Apalache	IfThen	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
be6b03b2a973897cb2aabc410668dabe4df1271e	Apalache	IfThen	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
ea46896dcb1d199f86b9cbae4daf3ea70ea2652b	Apalache	IfElse	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
d6d3d917c2a5a1e70a8f4e5e8a3d6dd41758de29	Apalache	IfElse	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
e2e6455b879eb3ac6aa4854cad99014a7ccd8fd6	Apalache	Unchanged	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
4255256bc71876913fec393fff9c65115eeec19b	Apalache	Unchanged	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
ebd1b463210f86033171392511643b2cd57bd8c4	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
f8eaac6a6337456690d89d104b249df5dbad3869	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
2d627408d6d35245b2eb546c35df330181837844	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9b805f95f1ec71b7109e1563e1bc9eecd2e5d8d2	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
0d6bd06effdb6be7544ee6b02ee0c436d511bf08	Apalache	BagBagToSet	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
bc92aad22a3c73beea054805a49880a4784b8ebf	Apalache	BagBagToSet	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
7845a717d2739117fc44fa4b7589efed6cbc0393	Apalache	BagBagIn	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
016e88634fcb7ecae75908fbdf38966806acce88	Apalache	BagBagIn	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
dc1546b074e9163d68a5f47343e4c26aa0adec79	Apalache	BagAddBag	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
87e1866b04bbe65f37fc572a629df48026fce1aa	Apalache	BagAddBag	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
d0fcb363b041eb40fe7c4aeb336567feda19df8d	Apalache	BagBagSub	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
37b79e418178693f651f209a3c715ac8bdb44c16	Apalache	BagBagSub	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8bdf992f15296589e3f0797cc776a2c91c9d3cc7	Apalache	BagCopiesIn	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
82ff8f807bb712164585c3b01e7e645957fde280	Apalache	BagCopiesIn	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
0f6d5dfac52d235cdf113ba251b33f4703b0d82b	Apalache	BagSubsetEqBag	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
e94231aede2ba0cc78f72ed9ac548ef4ad95624d	Apalache	BagSubsetEqBag	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
cd1d51db9a6da989bdbad17900d1f1f04a436ec6	Apalache	BagBagCardinality	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
8aac642f4aba60c23603a570dfa384431c38a3d6	Apalache	BagBagCardinality	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
ce4443007d0bb6cdaa36f7d5b90bd6393b9654c0	Apalache	BagBagOfAll	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3aed5da4a0f3372a6cf67f74c6f6961f3393b2e5	Apalache	BagBagOfAll	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
4ecb7664b8a3f668bde523bdd0ea273b05a6c729	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
c50b784e4573c4ccc95cd64995492f198c1547eb	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
641db3a3483e029d874852ece52ba014ec2cd19e	Apalache	SeqAppend	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
15e987afc59e64e09ded5e1e17f281bcdac3ebb9	Apalache	SeqAppend	BagBagOfAll	False	Passed	Model Under Test Equivalent Model

Index

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