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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b311ccfb6ffaa46d31b710028f8257d80dca7f46	Apalache	And	InstanceNamed	True	Passed	Model Under Test Equivalent Model
4b8946aafaa516d92a37c960241913fb979f8c88	Apalache	And	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a73b85d6046af86f899d1e82b583ac889941efc8	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceNamed	True	Passed	Model Under Test Equivalent Model
733690ff800b973935b8535e3fd072206525484c	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceNamed	False	Passed	Model Under Test Equivalent Model
bceae87d312230daa757d9fc08700f029104aa00	Apalache	Imply	InstanceNamed	True	Passed	Model Under Test Equivalent Model
694363262f38af54ed8a30d59866ec86f48f6d35	Apalache	Imply	InstanceNamed	False	Passed	Model Under Test Equivalent Model
19a08da53d1e909a65a031f9de55662d85abe9e9	Apalache	Not	InstanceNamed	True	Passed	Model Under Test Equivalent Model
951442cdf08367ffa67b344743289167d2bc28bb	Apalache	Not	InstanceNamed	False	Passed	Model Under Test Equivalent Model
535ada481246c7084dc6cd45ef5201872387069f	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceNamed	True	Passed	Model Under Test Equivalent Model
b9237548e1562bbda52dda2c0e502acb38675d45	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceNamed	False	Passed	Model Under Test Equivalent Model
6008902672b113f7e1875c180e1f70b6b096bec2	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5aa48973282d1612dfda572b7d6fa64800616817	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceNamed	False	Passed	Model Under Test Equivalent Model
1af85443a83fb30974777a94a834e8b22115516e	Apalache	AndProp	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3a0c6aa97c18d2fd3138391e749762e698d2ba39	Apalache	AndProp	InstanceNamed	False	Passed	Model Under Test Equivalent Model
c9f7a08f65c8ed0bd66ad782512db27d2a304784	Apalache	Boxed	InstanceNamed	True	Passed	Model Under Test Equivalent Model
ad0325f35e2ae8974d6a3df27d767d1d18c1c272	Apalache	Boxed	InstanceNamed	False	Passed	Model Under Test Equivalent Model
045bcbc1a51d43f32d22057af5f415687f534d8d	Apalache	Eq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0eecb1ba94a8a9ca4f34c834f1bd5de3508f5cbe	Apalache	Eq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5b4abb480f416acd725ef7729a0759f02574bf93	Apalache	Ne	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5c70992d3932e4fb3e4d213f042eae8e56087185	Apalache	Ne	InstanceNamed	False	Passed	Model Under Test Equivalent Model
905c8ec97dae649f5945a47a71a650f8f82d927f	Apalache	Let	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d469016fbaf54f7e41491cc6abe78659ce67a74f	Apalache	Let	InstanceNamed	False	Passed	Model Under Test Equivalent Model
3818e79663731b4d047adcd76a29503b723fb1ca	Apalache	Set0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8ed54246892be586ce44380cebd716e798566337	Apalache	Set0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
ed13bf3b98129a5b6dfb8e051b39e954a05d433d	Apalache	Set1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
cbb17cea71082d11512911b9318f4b05bce205c7	Apalache	Set1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b4167ab7958052458e3cecfe1b4c674e2848cf67	Apalache	Set2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8e0173ecec5cea72457085a8e4130352c62a8f9c	Apalache	Set2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
e984717dd6562df1d1b66d65cea8384b34b1dfb7	Apalache	Fun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6ac2cc4597aaf61a53dfdc703f6c34481875ab49	Apalache	Fun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5e8c75f7b6a18bda2dbc9b43666d6eb7183bed40	Apalache	In	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d414c56332bc41a9b08ec10e5baae9df29b241d3	Apalache	In	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d3d285bc1c6794efd5866fe8068801f28c36e2f9	Apalache	NotIn	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2ab0a0fce9a619d4cd1238e1aa691a5bf9edcd4e	Apalache	NotIn	InstanceNamed	False	Passed	Model Under Test Equivalent Model
341a1df8ba3e4f85539ac6e5fd8f8864327d69db	Apalache	Exists	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f419e4eedfb0709cd1bcf40aab83afc29997e82d	Apalache	Exists	InstanceNamed	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
a62ac97ee55d5e124514dd1d695392283e0ca6b6	Apalache	Choose	InstanceNamed	True	Passed	Model Under Test Equivalent Model
4bf5112759d437fdd0ae735765ccbab7ecf887da	Apalache	Choose	InstanceNamed	False	Passed	Model Under Test Equivalent Model
7f19ce0407ece47c913aa6e38df7e3c675b88413	Apalache	Record	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7109cc989490a6c99be48e1856240ab3e7bb2323	Apalache	Record	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a72d3d754bb87c4dbbeb784b64d40ae49ba33bc9	Apalache	Tuple	InstanceNamed	True	Passed	Model Under Test Equivalent Model
33c90f086c248201ec6e8ff7f029e2b2cd3d6713	Apalache	Tuple	InstanceNamed	False	Passed	Model Under Test Equivalent Model
9d80a06d7ed8e27ad8c23100fbd1a14668f74490	Apalache	FunApp	InstanceNamed	True	Passed	Model Under Test Equivalent Model
23b1fd438ceb1d5063908e20f3380ff6a4ee6c87	Apalache	FunApp	InstanceNamed	False	Passed	Model Under Test Equivalent Model
930ff86231c5a48cd5097361ce482072625ffea4	Apalache	Except0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6022cfa4c415cb61f86f14c746e2d2bfab311360	Apalache	Except0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
8ac4341e9bd07a36f2cda098f30e7fb56c88c96b	Apalache	Except1Fun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
92281c5dac73ab436037d69adbf39454f4221291	Apalache	Except1Fun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
8e7d4beadc574ba2478a716e0d3869e8c4340b90	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceNamed	True	Passed	Model Under Test Equivalent Model
a183b10e4a0aa063d78877879e469709c3fab789	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceNamed	False	Passed	Model Under Test Equivalent Model
6b49eda84b4f808368941e770fb4da801bc92628	Apalache	Except1Rec	InstanceNamed	True	Passed	Model Under Test Equivalent Model
24d6c3cf38e17e99a23a8a13e82a158496abcb99	Apalache	Except1Rec	InstanceNamed	False	Passed	Model Under Test Equivalent Model
dfc57043c719d2f4f9cd8b003cf1fe4a5cbc69f0	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceNamed	True	Passed	Model Under Test Equivalent Model
ef09d7539b4275f121a2f5a0d147d91f13fc8562	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceNamed	False	Passed	Model Under Test Equivalent Model
bebf1bf838348d79bc78a63184728e72ef0a1816	Apalache	Except2Fun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0fa43a4109539a13289dfe2b0e10632a9ff579ff	Apalache	Except2Fun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
196da80f0cb086ad653a7f9267439c65e44979ea	Apalache	Except2FunTuple	InstanceNamed	True	Passed	Model Under Test Equivalent Model
759f6d8644138180deb345974f5e0347821e95d3	Apalache	Except2FunTuple	InstanceNamed	False	Passed	Model Under Test Equivalent Model
94aca8a8ebbe6e4f5e62925ecd54a1ece898610b	Apalache	Prime	InstanceNamed	True	Passed	Model Under Test Equivalent Model
677a6de6f94b22556892a560728120e20fc886e8	Apalache	Prime	InstanceNamed	False	Passed	Model Under Test Equivalent Model
9fe0abdb1754a03d28592698c9142788995c7196	Apalache	NumUnaryMinus	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0163c8d493e026435ee0b797a3cc15c26dd7e962	Apalache	NumUnaryMinus	InstanceNamed	False	Passed	Model Under Test Equivalent Model
3975c0558e03c8e7526c6439d00a2c956cffe88c	Apalache	NumPlus	InstanceNamed	True	Passed	Model Under Test Equivalent Model
90d28f8ad1b74432d69a72a29cc9af1f2e5dc784	Apalache	NumPlus	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a8295fa2f2e9f2e7e9530b6671aaa360ed401c0e	Apalache	NumMinus	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7ecb39287ecf66ede52d41dc57df126696ae80b2	Apalache	NumMinus	InstanceNamed	False	Passed	Model Under Test Equivalent Model
500372df39f94a5a4fd3d8673cb9160026394f5a	Apalache	NumMul	InstanceNamed	True	Passed	Model Under Test Equivalent Model
ebba66f411d4d92f546e72727955624145e75076	Apalache	NumMul	InstanceNamed	False	Passed	Model Under Test Equivalent Model
6a6747b17a3256ca92bf9b37155a4fe7bdf6f971	Apalache	NumDiv	InstanceNamed	True	Passed	Model Under Test Equivalent Model
270620726fdd3242b1833f7473120809429c17dc	Apalache	NumDiv	InstanceNamed	False	Passed	Model Under Test Equivalent Model
3df6f6c646d20fd2b50a4238740966ecb1e1b907	Apalache	NumMod	InstanceNamed	True	Passed	Model Under Test Equivalent Model
823f3438f35f51191fb0101fc9aa62ca67ffc3c3	Apalache	NumMod	InstanceNamed	False	Passed	Model Under Test Equivalent Model
dd8eab80f3a8f5c2c97ffd4b938417a2502e68e3	Apalache	NumPow	InstanceNamed	True	Passed	Model Under Test Equivalent Model
161d28011fba98bb7192537d8aa8aa96701cfab5	Apalache	NumPow	InstanceNamed	False	Passed	Model Under Test Equivalent Model
50eed444f4aa42066dec443ab0083a0e68a71470	Apalache	NumGt	InstanceNamed	True	Passed	Model Under Test Equivalent Model
9f2991b72dec051cbed43fd9e3ab720afb63aafc	Apalache	NumGt	InstanceNamed	False	Passed	Model Under Test Equivalent Model
61d15decd55946a01f9fdff430e1d7c6f925c21d	Apalache	NumGe	InstanceNamed	True	Passed	Model Under Test Equivalent Model
21494c15245103a1e9f5994410f209129f49740a	Apalache	NumGe	InstanceNamed	False	Passed	Model Under Test Equivalent Model
1a58ae3e38993543e891133b1582924c646c3aee	Apalache	NumLt	InstanceNamed	True	Passed	Model Under Test Equivalent Model
830d8c68b6f575c32895f059bb39f573466f56e5	Apalache	NumLt	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5846f72222c879455e7b42f66ab1f153ce1fe52e	Apalache	NumLe	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2cb0fa9985a79a506369020bd8f7421c4cce531d	Apalache	NumLe	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d2b94ba4f8ffe944ed2f8055532dcdbf605ec78c	Apalache	DefFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3b5aa6cee5b4d1351205fc9d9eebc488699a3f2d	Apalache	DefFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b6255bf5cb67a185cb5927db74a9e6cf8e716abe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2144308ad9cd6bc6c866df4066a23023acb7074d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fd6ba117c53593a2f48994e236025025236b8d05	Apalache	DefFunRecursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
9be42d095475a237850f1b847e74f9860ca08616	Apalache	DefFunRecursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f076b455248395d563c0a555d02c38559a4d9a81	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f62a998da5003190cfdc34c27dbee8b288f031e6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
52d5f9d160b442a6edfaaeae990a5a8785838ee7	Apalache	Def0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
eef612f775a1d8938d946bdc64bf436b82a67505	Apalache	Def0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
4b3902e1a3dcdb5ad63b943868b948be06884cbb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f85a1347ebcec96752041af2debef02a8ad277cc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
0fb0cc8878929fc173372715c38cc5baac417d23	Apalache	Def1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
43e0addc28bbc00b6c25bd716c2d086dcfe1741b	Apalache	Def1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fc967a58fe53f8448268e05bdd3a309d288722f5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
bc281a8f330907a5450cb08c8126ec4788896a88	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
ef7bc06d187fda5be568d1a665d9424c45047aae	Apalache	Def2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6121df629a4c820f1b699ae1c3cc1f0e269023aa	Apalache	Def2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a347a2f83b43dc9a2806eda4a8a477b60c1b517e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
20d776da3e641b535b40b7fb2cf319bfe0ed5402	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
0eb0c759e0d6434f60249209fe4174d5384a8ea3	Apalache	Def1Recursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5a71a0b801616d1d9b488c3e536843cdbedd9c6c	Apalache	Def1Recursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f383334fcdc7761f454062c44fe5d92512a24dae	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
79650477c5bc90e01f7f08363220061ea691e850	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
28ae19035281e3f0500cb9d0edb8c5f68757aacf	Apalache	Extends	InstanceNamed	True	Passed	Model Under Test Equivalent Model
53ac7fd6e0b6a66c8f0ad10d728dabb6a92503aa	Apalache	Extends	InstanceNamed	False	Passed	Model Under Test Equivalent Model
7301f0c608b58ec663c4fcff2801007a49219572	Apalache	ExtendsInDifferentFolder	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8cd05c9afbb37ef380d2f0b5dc08135671e8dfdf	Apalache	ExtendsInDifferentFolder	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fd9fcc93f00d35913474be50828524028f693094	Apalache	Variable	InstanceNamed	True	Passed	Model Under Test Equivalent Model
de9a0415398e0d37d2791ad887a3f89f68d54199	Apalache	Variable	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fc2f84db3b451ef77c914014325d46636ab0eaf7	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceNamed	True	Passed	Model Under Test Equivalent Model
db46dda62e8e55a8c28d2c02b6691c568d4ea7e9	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceNamed	False	Passed	Model Under Test Equivalent Model
99a0e5e807e7416e7979f9b15e76c01e2beef15c	Apalache	Constant	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7ab73cfff59faf78f57c95ab29c2603fae1cde00	Apalache	Constant	InstanceNamed	False	Passed	Model Under Test Equivalent Model
543c932130753c0e552dfabb2e8f5370a37449b9	Apalache	ConstantRank1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d2c051f568a4f4e6f63b6a48e73227ce60660dd3	Apalache	ConstantRank1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f5255dec7834d85ce7f1acc03c4adbede190c1ed	Apalache	Instance	InstanceNamed	True	Passed	Model Under Test Equivalent Model
833a99785a2b7b814eea7800bbe7c8d9c55faec0	Apalache	Instance	InstanceNamed	False	Passed	Model Under Test Equivalent Model
160f48114161c3c5ddd74f7e961c92884a9b3c56	Apalache	InstanceWith	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5d4b18495672aae1bf6300b7291d871520161c48	Apalache	InstanceWith	InstanceNamed	False	Passed	Model Under Test Equivalent Model
383c9f2a26b7b2dc87ceb72ca100a6f5599d268e	Apalache	InstanceNamed	InstanceNamed	True	Passed	Model Under Test Equivalent Model
40e9d9d4528ffc5202fcef24c548586a5ff8e072	Apalache	InstanceNamed	InstanceNamed	False	Passed	Model Under Test Equivalent Model
63b20de38025a31eab2124e5663984998a7c6358	Apalache	InstanceNamedWith	InstanceNamed	True	Passed	Model Under Test Equivalent Model
afde42bb15983bda87ce6e60849b16c7acdef95f	Apalache	InstanceNamedWith	InstanceNamed	False	Passed	Model Under Test Equivalent Model
eacfac5e311a9f8e33f93b612bcabb0c273a795b	Apalache	InstanceInFolder	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0f137a71aff7f08177e068ff6c322e122b75f2a6	Apalache	InstanceInFolder	InstanceNamed	False	Passed	Model Under Test Equivalent Model
26e681bcee94481dad0d1ec1b35c324052a2bbad	Apalache	InstanceWithInFolder	InstanceNamed	True	Passed	Model Under Test Equivalent Model
02087af64eaecaddff5a8404349e9a14554a2f73	Apalache	InstanceWithInFolder	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b8ed01acf5f472e57891c008492af418e37f1e6e	Apalache	InstanceNamedInFolder	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7645587fb22781920878b115896f3e98d833cdbe	Apalache	InstanceNamedInFolder	InstanceNamed	False	Passed	Model Under Test Equivalent Model
810936f8572b2faa8de5181b712a9067db0d7010	Apalache	InstanceNamedWithInFolder	InstanceNamed	True	Passed	Model Under Test Equivalent Model
a3e8559714171f0267ebeb2b6fb3e22988d1165f	Apalache	InstanceNamedWithInFolder	InstanceNamed	False	Passed	Model Under Test Equivalent Model
39db4c32e8bf4636ceecf218d0bd32cf45aab532	Apalache	Enabled	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2fe236d90b91aebeca5dc3ddea84714f818e40c6	Apalache	Enabled	InstanceNamed	False	Passed	Model Under Test Equivalent Model
672ee0f7a8d9f929c6714eb320b97516a4158e3a	Apalache	Assume	InstanceNamed	True	Passed	Model Under Test Equivalent Model
b5011c455f53e2bfe8cdbbe74cf1f90dcbfb2b18	Apalache	Assume	InstanceNamed	False	Passed	Model Under Test Equivalent Model
557ec024649c17587a53601a1810de6dddcb7979	Apalache	AssumeNamed	InstanceNamed	True	Passed	Model Under Test Equivalent Model
9435b263f2712709acf94da13edccc8c402f37f3	Apalache	AssumeNamed	InstanceNamed	False	Passed	Model Under Test Equivalent Model
926e194aa44ad22596584e18706deec1b246a656	Apalache	Lambda	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8a76fe061c38794313224e2f1cb91e0ca6b61ab2	Apalache	Lambda	InstanceNamed	False	Passed	Model Under Test Equivalent Model
ba4b9bd98ac67640d9ab23a653b661ccba7801ee	Apalache	Cross2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d9f245b61785fda80e081a0b8c70f12abfe88c55	Apalache	Cross2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
67ba8275b4b4f54117d32ce04d345a88d82cca0c	Apalache	Cross3	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3a0c95c7735567d922c08d0ba5394b1ed66ecac6	Apalache	Cross3	InstanceNamed	False	Passed	Model Under Test Equivalent Model
cda87b04869d1bf5e4b5181c24b03c44c9eed29f	TLC with reduction strategy: Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	FunSet	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7b4d9ad6e21e57004c9e31dc5e76faac45c1323e	TLC with reduction strategy: Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	FunSet	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d340eae142f5e6d2ade91989e0432c82848eec48	TLC with reduction strategy: Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	RecordSet	InstanceNamed	True	Passed	Model Under Test Equivalent Model
fae2a04c9589f5f2c91817e2e1f2784c5c9109f5	TLC with reduction strategy: Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	RecordSet	InstanceNamed	False	Passed	Model Under Test Equivalent Model
41f9576c42f9096dc2d055a0a9b3fa68e011aca2	Apalache	SetDiff	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0620af8569893f43c9afc45063974e4bac1598ce	Apalache	SetDiff	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d3e5d197d6e4336b87d6289c0fa7f10ec520a2b7	Apalache	SetUnion	InstanceNamed	True	Passed	Model Under Test Equivalent Model
dac7810c9f602ad4e5e0d913a6f22ac8b0b14d21	Apalache	SetUnion	InstanceNamed	False	Passed	Model Under Test Equivalent Model
4dd373fef54e4bb75b28c4502346a472e4e88ee9	Apalache	SetIntersect	InstanceNamed	True	Passed	Model Under Test Equivalent Model
fd4eecc6958a4ce879636d2554c459ac043fe6f3	Apalache	SetIntersect	InstanceNamed	False	Passed	Model Under Test Equivalent Model
783a277d313b0b85d187cca5e914f55032d80979	Apalache	SubsetEq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e10de991293579fd23702f938cc298eadc4dbf4f	Apalache	SubsetEq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b5f2807f98617ef708f1685152d4b4128b506fcc	Apalache	IfCond	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8403bbbc17fd17ef25f1ac3ca8a6c63c55c2c077	Apalache	IfCond	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d7dba212ca0e03c86defafde4c6e27092357cabb	Apalache	IfThen	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f3bee8200384bc47b6b98e0a359497bb20a8d08b	Apalache	IfThen	InstanceNamed	False	Passed	Model Under Test Equivalent Model
bc13b77c25a48ba9c7ef158d3af666bb0018fda8	Apalache	IfElse	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e24590389b658a1d56d20201eb0daa1c00d738c7	Apalache	IfElse	InstanceNamed	False	Passed	Model Under Test Equivalent Model
ab945c58e4ef7741cb270bc45c48c72edb6d6a05	Apalache	Subset	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0add343e39d80bf7078cd6bff55b7c415c33f9da	Apalache	Subset	InstanceNamed	False	Passed	Model Under Test Equivalent Model
8b0d5c9398139be6ae0c2dba4f9582239944578d	Apalache	Domain	InstanceNamed	True	Passed	Model Under Test Equivalent Model
542167f2d367254777bde288f3d50b186765eae9	Apalache	Domain	InstanceNamed	False	Passed	Model Under Test Equivalent Model
981facb2408cbf5780fd429c19803790b6354300	Apalache	Union	InstanceNamed	True	Passed	Model Under Test Equivalent Model
93a413624bf26c465482344187be5374d6425fb1	Apalache	Union	InstanceNamed	False	Passed	Model Under Test Equivalent Model
56eac6979e6510bcde3778c663e0ddb2810982f8	Apalache	Unchanged	InstanceNamed	True	Passed	Model Under Test Equivalent Model
a259b384905924afd2f73c1834564834197f6c6d	Apalache	Unchanged	InstanceNamed	False	Passed	Model Under Test Equivalent Model
0a35b085baae594b6c12df483d9265a37332ce38	Apalache	Equivalence	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e90fa0eedec883a379ed34193f8920adc1d59114	Apalache	Equivalence	InstanceNamed	False	Passed	Model Under Test Equivalent Model
942476e525a72b29cb3945e1bb7ed7b77c89289b	Apalache	SeqLen	InstanceNamed	True	Passed	Model Under Test Equivalent Model
bf8825cddac27ab7f59a93c17b1cf8d3faea0f4d	Apalache	SeqLen	InstanceNamed	False	Passed	Model Under Test Equivalent Model
979bbbd30fd8d75b38cef9fac362f12a0e01bcd0	Apalache	SeqConcat	InstanceNamed	True	Passed	Model Under Test Equivalent Model
272cfeb5a31f032146da649decca9940932088c8	Apalache	SeqConcat	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fe7e6cb82e2b242f2eee8d58ada3978633309f08	Apalache	SeqSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
aeb62e5e766d8ee10dd639cc1c37eb8a3e3d4dbe	Apalache	SeqSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f5a75fc010af859b2c352aa3d1afeb9caf138244	Apalache	SeqSelectSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f5cac1aa06c927d3937b4508855e9d111f0a5627	Apalache	SeqSelectSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
7c703b7e4da9f24b88adda48e5e35bbfbdaaea00	Apalache	SeqSubSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
1465ca8b0c3fe0625e03a8e5e7cfde60fb5bbf77	Apalache	SeqSubSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fe685207446205241cceec302c962160a260ae39	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	InstanceNamed	True	Passed	Model Under Test Equivalent Model
52c955f89139d18306434e137422cdc85f030ce1	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	InstanceNamed	False	Passed	Model Under Test Equivalent Model
78e0fd9afa5c262f197890259e6d6f5bb0e6487a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
79aecbf9bb6229b9757b1e454604c8760d41c869	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
e94f643adb58ac4d62b8d4f04e54a4ef8c16a676	TLC with reduction strategy: Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	TlcExtendFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
84af4fbe6c38f0b66cd38bf5e5544f73e23b0f79	TLC with reduction strategy: Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	TlcExtendFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
87e7a7a6ad7899d2f943351ae1a2abf528c6adec	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
ef7a7d29a165882be973afe34ff4d65d140f78b1	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b716b0a3c8be04127ed741b9a50ba14fff28515c	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
c28af3c79ff1d5015e6c4e816bfc0c57e6c02c63	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f4318cb94735aa37a6f32af582812fe4ab540a95	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceNamed	True	Passed	Model Under Test Equivalent Model
78c1e69f67fef1a4a450ada95f6aa77259e559bc	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceNamed	False	Passed	Model Under Test Equivalent Model
2ee41d1039b0fb9e48f29cb41aa26cbd13a4a57e	Apalache	BagBagToSet	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2dd07b7f977008d4bdbaa94dca94906ee3042216	Apalache	BagBagToSet	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d856d962b0aeaeeb635e0bf9d832e65ce26a622f	Apalache	BagSetToBag	InstanceNamed	True	Passed	Model Under Test Equivalent Model
375ac9a209a754bf516506463322cce8294233c5	Apalache	BagSetToBag	InstanceNamed	False	Passed	Model Under Test Equivalent Model
dd56b09b9e257dade229ac2326c2b4e87fa50037	Apalache	BagBagIn	InstanceNamed	True	Passed	Model Under Test Equivalent Model
b133b1a17474599ea85d511b519df2fdbf336ba9	Apalache	BagBagIn	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d0296455c611eeb61d9b5a130958711e500e572c	Apalache	BagAddBag	InstanceNamed	True	Passed	Model Under Test Equivalent Model
dea09b622d65afcb188ebe977d79bec0b3c228bc	Apalache	BagAddBag	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b95d276d828a6440048c0185d191d14b04b523d6	Apalache	BagBagSub	InstanceNamed	True	Passed	Model Under Test Equivalent Model
a03ebdc7eccbc584e0569da9982b6fd49e8a27dc	Apalache	BagBagSub	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d14efc8fbe0cbc57bf7d08c87d75d645aecef084	Apalache	BagCopiesIn	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e6a79687ea39095ccd49eba78d7d0dce1134cdf6	Apalache	BagCopiesIn	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a6f401d1c78d374c098824b159e6582dbf9f1073	Apalache	BagSubsetEqBag	InstanceNamed	True	Passed	Model Under Test Equivalent Model
32e37f56f42381b25e96f1631b30352c6eba8ca2	Apalache	BagSubsetEqBag	InstanceNamed	False	Passed	Model Under Test Equivalent Model
2b0684d3a1bd1a68a0760c8d231e26a6cf9eb2c4	Apalache	BagBagUnion	InstanceNamed	True	Passed	Model Under Test Equivalent Model
61a5e0dc773c82b6e113877b16cb0086965b2cbe	Apalache	BagBagUnion	InstanceNamed	False	Passed	Model Under Test Equivalent Model
3fdbf51f3345c69f44e92ba7e293b1849c4dff19	Apalache	BagBagCardinality	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6ea3d78d89a847d1cc13cc7acf52be3ead7eeceb	Apalache	BagBagCardinality	InstanceNamed	False	Passed	Model Under Test Equivalent Model
466f13688cb80fc795e085cee865058c86e08818	Apalache	BagBagOfAll	InstanceNamed	True	Passed	Model Under Test Equivalent Model
52130037efeb5e954d87fbf573ea29134934880d	Apalache	BagBagOfAll	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5c3cb9b4ac612e920dafec21d7019e2ea488e6b0	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceNamed	True	Passed	Model Under Test Equivalent Model
63de49fc99e2563fb9dd3be63a58838e74d7f32e	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceNamed	False	Passed	Model Under Test Equivalent Model
33442b56164be44ffb9b425f5c330316cfd609fe	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	InstanceNamed	True	Passed	Model Under Test Equivalent Model
24d77c3b813232f39bf75a8346419c9c2fb6f238	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b3f27fb19b7c254a2e03cb01d757924b81742cdb	Apalache	FiniteSetsCardinality	InstanceNamed	True	Passed	Model Under Test Equivalent Model
cf8ed92457c0f24360463ffe71b654aa64efcb96	Apalache	FiniteSetsCardinality	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d351edc78f92c502d5981814add8226026bc67f9	Apalache	SeqHead	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e03dbe352254cb31a39f8b9d5125a8014d5e4105	Apalache	SeqHead	InstanceNamed	False	Passed	Model Under Test Equivalent Model
a81d7abff3cc9e02174e949efc33710c7261953c	Apalache	SeqTail	InstanceNamed	True	Passed	Model Under Test Equivalent Model
fcfb3e74a30ab8f31cfeb0c0dd893b820ca4ddc6	Apalache	SeqTail	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fdcc38e5e9d39d044cf53ef1a344f43585efedd2	Apalache	SeqAppend	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0c148643f1acee98fcb618f78e29bae8f38ecf3b	Apalache	SeqAppend	InstanceNamed	False	Passed	Model Under Test Equivalent Model

Index

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