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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
033d00f6284e6518992eb6ddab55fe4155839557	Apalache	And	InstanceWith	True	Passed	Model Under Test Equivalent Model
e934f896c2f773869a3ff7dbca67552574510339	Apalache	And	InstanceWith	False	Passed	Model Under Test Equivalent Model
a09721b75b35c97a122e4fbe066def6aef67549b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceWith	True	Passed	Model Under Test Equivalent Model
95a21e3ea82e7b4334298512f651c9e0c4c06901	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceWith	False	Passed	Model Under Test Equivalent Model
dad5964a1579dfd020b6866127f69aaea55da046	Apalache	Imply	InstanceWith	True	Passed	Model Under Test Equivalent Model
d24e02005338c668c25b47fd6dda3f255d2c2ffd	Apalache	Imply	InstanceWith	False	Passed	Model Under Test Equivalent Model
f065634db37a298899a34a512c69a460f9b2ba09	Apalache	Not	InstanceWith	True	Passed	Model Under Test Equivalent Model
9ac066ec91767ad380414f18a3a49fcf8904ce34	Apalache	Not	InstanceWith	False	Passed	Model Under Test Equivalent Model
225b0c1f3ceaa2cfa32dd9da26bdb64073ef4935	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceWith	True	Passed	Model Under Test Equivalent Model
30b89ddcf11c1bfdd1ec7c581e3b18636480d19b	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceWith	False	Passed	Model Under Test Equivalent Model
0510d47da398284ca5de23f93e29a4cf883a2529	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceWith	True	Passed	Model Under Test Equivalent Model
4033235bb507a835142803bbb20a5b92da70f2a6	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceWith	False	Passed	Model Under Test Equivalent Model
6086f9374923815a3b4aa1ccfba57899449959d0	Apalache	AndProp	InstanceWith	True	Passed	Model Under Test Equivalent Model
799c396acdcc598dd574105edab49a47786894e8	Apalache	AndProp	InstanceWith	False	Passed	Model Under Test Equivalent Model
d24733ffcfca18a58edc295918d9617a2a592d39	Apalache	Boxed	InstanceWith	True	Passed	Model Under Test Equivalent Model
8ad6082405eebe737a9a8e0b9fb38281daa1e42b	Apalache	Boxed	InstanceWith	False	Passed	Model Under Test Equivalent Model
fbcee23a86f4e0dec5185c50ddc01c373cc8fb4e	Apalache	Eq	InstanceWith	True	Passed	Model Under Test Equivalent Model
c600bb278be0d7847f001a752badb0c7a8e6254d	Apalache	Eq	InstanceWith	False	Passed	Model Under Test Equivalent Model
c60a34305204ba7ee114f462d339d588d0552ec8	Apalache	Ne	InstanceWith	True	Passed	Model Under Test Equivalent Model
8a8c40cd549eead0042eec7eff79128e20c43e37	Apalache	Ne	InstanceWith	False	Passed	Model Under Test Equivalent Model
6b49036f1700aaf6e07fdd31b49eb3ad3eb84a9f	Apalache	Let	InstanceWith	True	Passed	Model Under Test Equivalent Model
41aff8e558ef0bbd5f694e4564099d233ffaf2ea	Apalache	Let	InstanceWith	False	Passed	Model Under Test Equivalent Model
888c3b50fc397818071fca241331b3fa4671cee6	Apalache	Set0	InstanceWith	True	Passed	Model Under Test Equivalent Model
b5b32006f2869b2685f2e7e68b7903c7a82acedd	Apalache	Set0	InstanceWith	False	Passed	Model Under Test Equivalent Model
b471e3ca2d9e451f876067bf4e365a4f9eee373b	Apalache	Set1	InstanceWith	True	Passed	Model Under Test Equivalent Model
370e21558dbe2748e17140f7ee4fc592c7895969	Apalache	Set1	InstanceWith	False	Passed	Model Under Test Equivalent Model
c42521330c7e0098f09c6b3694c0158c2994fbde	Apalache	Set2	InstanceWith	True	Passed	Model Under Test Equivalent Model
cec6926a13ad09d84cac0c29328ece2cdd66998f	Apalache	Set2	InstanceWith	False	Passed	Model Under Test Equivalent Model
3f59062290c87d21cc7115f44d5fd49e9672cbf8	Apalache	Fun	InstanceWith	True	Passed	Model Under Test Equivalent Model
f377b18f1372c77205e71118ad3331bb3404081e	Apalache	Fun	InstanceWith	False	Passed	Model Under Test Equivalent Model
b8bdbe49101b09e3e8af2a4879c3be83a6084983	Apalache	In	InstanceWith	True	Passed	Model Under Test Equivalent Model
a347d76e0c059157820caa17428e62900066d005	Apalache	In	InstanceWith	False	Passed	Model Under Test Equivalent Model
1ca57a5dc9bd3bf8b0a50380a90c18589ebf2c65	Apalache	NotIn	InstanceWith	True	Passed	Model Under Test Equivalent Model
3689b0ea2d05aee0e9793842ae75c90540f210e1	Apalache	NotIn	InstanceWith	False	Passed	Model Under Test Equivalent Model
44e10088791c0264a72924ccbca6fd6523071dee	Apalache	Exists	InstanceWith	True	Passed	Model Under Test Equivalent Model
2fbcb2229245f20efa43c4c7b9e255687dc3ad6d	Apalache	Exists	InstanceWith	False	Passed	Model Under Test Equivalent Model
92ab77684c6f4931d32d65e11442c758467485a6	Apalache	Forall	InstanceWith	True	Passed	Model Under Test Equivalent Model
341f9470b28c67dc22e182f07b69d02a66d8ab40	Apalache	Forall	InstanceWith	False	Passed	Model Under Test Equivalent Model
4227ec31b7de640770f1eac06cf325f4b01c8714	Apalache	Choose	InstanceWith	True	Passed	Model Under Test Equivalent Model
6fd191d8169769d3ab90d97e6d2919609de0ee6c	Apalache	Choose	InstanceWith	False	Passed	Model Under Test Equivalent Model
f86dab7486ace9da7f84f0ebf733c163b97a21e7	Apalache	Record	InstanceWith	True	Passed	Model Under Test Equivalent Model
2755b9a12cc8342967955f18285caad5d64edb89	Apalache	Record	InstanceWith	False	Passed	Model Under Test Equivalent Model
d0c4099917838a278106d93a4c366a53a3867132	Apalache	Tuple	InstanceWith	True	Passed	Model Under Test Equivalent Model
0c423aa30ce2e8288d3e136455d25d1c352066cf	Apalache	Tuple	InstanceWith	False	Passed	Model Under Test Equivalent Model
18baae4b069e5585a99a6a26c55c7e073c179bc5	Apalache	FunApp	InstanceWith	True	Passed	Model Under Test Equivalent Model
bd2faf68c1ce916fc8f43ca3e9dec5d5ceceb6d7	Apalache	FunApp	InstanceWith	False	Passed	Model Under Test Equivalent Model
b31f45199881f461f9caea78969dd843968ce286	Apalache	Except0	InstanceWith	True	Passed	Model Under Test Equivalent Model
bb717d0e72558439e291bf84f5ad30d1b972b260	Apalache	Except0	InstanceWith	False	Passed	Model Under Test Equivalent Model
70183e98326068c81d96ab24cf13fc35e9d00f9b	Apalache	Except1Fun	InstanceWith	True	Passed	Model Under Test Equivalent Model
1d0ed7218107380e2f98d5b364172c78e62838ca	Apalache	Except1Fun	InstanceWith	False	Passed	Model Under Test Equivalent Model
89d75eaf24bc283dd0a5f1de4656357234449da6	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceWith	True	Passed	Model Under Test Equivalent Model
048915609138cd3195dcb2d73998635c6bd65a47	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceWith	False	Passed	Model Under Test Equivalent Model
7c4fb7a7ec0e700f8d4d1297f414f5dbc82179ce	Apalache	Except1Rec	InstanceWith	True	Passed	Model Under Test Equivalent Model
1be279e008a26dceb104aca5a98ec8e42330a994	Apalache	Except1Rec	InstanceWith	False	Passed	Model Under Test Equivalent Model
e6bf998eacd5605f36b1c3d7708e8096b0dee969	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceWith	True	Passed	Model Under Test Equivalent Model
339b31382eb7267a1aa731c98ca86644cd5ca9ce	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceWith	False	Passed	Model Under Test Equivalent Model
e15cc420344d913b3174398109272ddc03e5efee	Apalache	Except2Fun	InstanceWith	True	Passed	Model Under Test Equivalent Model
09a1109bee874264be530a61f74fb51b086f4a9e	Apalache	Except2Fun	InstanceWith	False	Passed	Model Under Test Equivalent Model
962ac775c02383690c2e226ced92ecde3ce9c5c0	Apalache	Except2FunTuple	InstanceWith	True	Passed	Model Under Test Equivalent Model
5d4f814abbedac95f14471b6088d24a8479b7065	Apalache	Except2FunTuple	InstanceWith	False	Passed	Model Under Test Equivalent Model
79643192b9c608fd2159a72ddd103d15b58b2c31	Apalache	Prime	InstanceWith	True	Passed	Model Under Test Equivalent Model
3ba7e14b6d5f4b97d4a1d4ff5bc9a7e086be8f55	Apalache	Prime	InstanceWith	False	Passed	Model Under Test Equivalent Model
5f59f2fbc77be5572ba99796e10c3024a0782f60	Apalache	NumUnaryMinus	InstanceWith	True	Passed	Model Under Test Equivalent Model
94abf5578a832dd18ccd90b78985e15d3fea05bb	Apalache	NumUnaryMinus	InstanceWith	False	Passed	Model Under Test Equivalent Model
96a8ab28041a12b015c5e3d779712bee7d8157c6	Apalache	NumPlus	InstanceWith	True	Passed	Model Under Test Equivalent Model
b2b3d872ab2568d39204a2100ca63bbfc8088c0a	Apalache	NumPlus	InstanceWith	False	Passed	Model Under Test Equivalent Model
bb9d5042992f1f6de559d405e92a077454918b84	Apalache	NumMinus	InstanceWith	True	Passed	Model Under Test Equivalent Model
0f59f72e945b71b29cc10ab7b700b72eddf2f371	Apalache	NumMinus	InstanceWith	False	Passed	Model Under Test Equivalent Model
dcca0550a7d93f76688a1ecb19e3c4794971b3ee	Apalache	NumMul	InstanceWith	True	Passed	Model Under Test Equivalent Model
67c5da273f4b559828b85914fc5b44647da4d15b	Apalache	NumMul	InstanceWith	False	Passed	Model Under Test Equivalent Model
4d83fa1b3942af2d5e23ef3095057c4e5a7acf40	Apalache	NumDiv	InstanceWith	True	Passed	Model Under Test Equivalent Model
a538cafb697a0c10076eff38bbd111839fdba5be	Apalache	NumDiv	InstanceWith	False	Passed	Model Under Test Equivalent Model
cc376664f18098fdd552a0b5e2eb68eb1e30e950	Apalache	NumMod	InstanceWith	True	Passed	Model Under Test Equivalent Model
cccc0d2d0b8a26699eb9a7c584343ea7f77f2adf	Apalache	NumMod	InstanceWith	False	Passed	Model Under Test Equivalent Model
ad964669add18d44f5d85573c6b1ba9c58658f2c	Apalache	NumPow	InstanceWith	True	Passed	Model Under Test Equivalent Model
a949455af673f2991aac23a9be31a7efc41dfc61	Apalache	NumPow	InstanceWith	False	Passed	Model Under Test Equivalent Model
56c3f8572acc9df418fe4c26d293266f22d79bbe	Apalache	NumGt	InstanceWith	True	Passed	Model Under Test Equivalent Model
5b0628419db75b477d6018f13d7f504231095290	Apalache	NumGt	InstanceWith	False	Passed	Model Under Test Equivalent Model
9a7f4b9ddf907960dcb4d7265c693be76dd98944	Apalache	NumGe	InstanceWith	True	Passed	Model Under Test Equivalent Model
97eff6c273d46da3e7258650c59b9d08e0129947	Apalache	NumGe	InstanceWith	False	Passed	Model Under Test Equivalent Model
b90f779268b145af85c5a242702ceaaa1816aa5d	Apalache	NumLt	InstanceWith	True	Passed	Model Under Test Equivalent Model
60dee6d8c1623c64ca2ed6aec201abf8ddb75ba0	Apalache	NumLt	InstanceWith	False	Passed	Model Under Test Equivalent Model
ebf8703a254fa7847a3d8e19aacf5eda75e10802	Apalache	NumLe	InstanceWith	True	Passed	Model Under Test Equivalent Model
39cd95ed6fc6f9587aa275b15bd0c862b607342e	Apalache	NumLe	InstanceWith	False	Passed	Model Under Test Equivalent Model
3b51606862c1adb794ac714a0d07a0309a96ec80	Apalache	DefFun	InstanceWith	True	Passed	Model Under Test Equivalent Model
371be8f9e9fe50dba74a56e0c5584d1669dcfcd0	Apalache	DefFun	InstanceWith	False	Passed	Model Under Test Equivalent Model
26938c19d4d472ba874277f640425783d95b7944	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceWith	True	Passed	Model Under Test Equivalent Model
3786dc73ececfdd1209c0c60e2aba2df1e46ce71	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceWith	False	Passed	Model Under Test Equivalent Model
46579236289d6f70fe8c8e33eae08b7dda744c54	Apalache	DefFunRecursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
229eb2c3c033f34bc0cf339da6cb6c376fad4924	Apalache	DefFunRecursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
32deb89df0224bd94cb979336bbba8043d577ca9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
39f59b22675cbd7bc1f6b4f9cfa6d6bb2d4f9fb5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
7249c94c7b73bad6e28b54fb37661519ab1187ac	Apalache	Def0	InstanceWith	True	Passed	Model Under Test Equivalent Model
e69371e60e107a0d36689d79939171b23b6da6da	Apalache	Def0	InstanceWith	False	Passed	Model Under Test Equivalent Model
dc6e6ea913d103bfc4586b1e3a5a348ec90dbc54	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceWith	True	Passed	Model Under Test Equivalent Model
01f6b7f8a65dbb277135df5317bcda7d03a48967	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceWith	False	Passed	Model Under Test Equivalent Model
ca1d327bf78b8f58f6a9af79fb779bd0e1d1f6b2	Apalache	Def1	InstanceWith	True	Passed	Model Under Test Equivalent Model
657b9f30aa0022cdf60b7b68201c5aa8a82a80e4	Apalache	Def1	InstanceWith	False	Passed	Model Under Test Equivalent Model
a838827ddd15c59450ab8d5c1e882009752535bd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceWith	True	Passed	Model Under Test Equivalent Model
94693b6b179b12e589fe91a8a27166cfd7a9312a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceWith	False	Passed	Model Under Test Equivalent Model
fcc316fb579142497afbf39ae49d5ea25fe4bfdd	Apalache	Def2	InstanceWith	True	Passed	Model Under Test Equivalent Model
eeb1d274dbd3046343fc5f283c710a850c18d526	Apalache	Def2	InstanceWith	False	Passed	Model Under Test Equivalent Model
b44754dce79e5a78f62f56546178a1fd3eff9c20	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceWith	True	Passed	Model Under Test Equivalent Model
7dab05feecc1bea1b7d8d681f652052a11f18278	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceWith	False	Passed	Model Under Test Equivalent Model
63de6574650c5edce454604cd67e57040960ea33	Apalache	Def1Recursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
563bdbe79e591f6da5737727a778c322ddd9ae18	Apalache	Def1Recursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
330e983de7325be96854b844fc2b500ba49f166f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
fea5b26c2ab4291597b9fad19f083432aad1de19	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
341990fdd50c65810f7b4662a912f757755c0a1f	Apalache	Extends	InstanceWith	True	Passed	Model Under Test Equivalent Model
95c37a7650145fad961d76280d8b52660e53ee2b	Apalache	Extends	InstanceWith	False	Passed	Model Under Test Equivalent Model
92e9722c0e14a8faca5c8f40e164db986bc90002	Apalache	ExtendsInDifferentFolder	InstanceWith	True	Passed	Model Under Test Equivalent Model
96958953ecbd678712ae118c161e09b5c8253f82	Apalache	ExtendsInDifferentFolder	InstanceWith	False	Passed	Model Under Test Equivalent Model
b7a7cf799d688161be3323575fc6fbdc31540388	Apalache	Variable	InstanceWith	True	Passed	Model Under Test Equivalent Model
87d1665d37da92027b21ca67a265a5160e3746e2	Apalache	Variable	InstanceWith	False	Passed	Model Under Test Equivalent Model
f933e73769d61eb856e9428227c7875118255325	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceWith	True	Passed	Model Under Test Equivalent Model
26d5a282e450381a6b1ea78744f1cefb3483f6cb	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceWith	False	Passed	Model Under Test Equivalent Model
b706147ad1f73dbed8c2fccb5e2df391498e69ab	Apalache	Constant	InstanceWith	True	Passed	Model Under Test Equivalent Model
fb6bf2991fd16870dc0e94c8ef5aca6edc08937a	Apalache	Constant	InstanceWith	False	Passed	Model Under Test Equivalent Model
280c7ecc3e33c7a6c76407a0c82f1d47255655c1	Apalache	ConstantRank1	InstanceWith	True	Passed	Model Under Test Equivalent Model
762645772f5978ba91fec08bc222009f946b1855	Apalache	ConstantRank1	InstanceWith	False	Passed	Model Under Test Equivalent Model
2fbd31f97c9dbce7f5278e0e143478ee6523a5d2	Apalache	Instance	InstanceWith	True	Passed	Model Under Test Equivalent Model
6d63d377fa09d4453c0aefe1cffbde99e5820bb1	Apalache	Instance	InstanceWith	False	Passed	Model Under Test Equivalent Model
8eacbc849f3e5b46da24a5d5701215d4b649ba54	Apalache	InstanceWith	InstanceWith	True	Passed	Model Under Test Equivalent Model
fd913075ed17d801a4d973a9b9f16a7f2d056d33	Apalache	InstanceWith	InstanceWith	False	Passed	Model Under Test Equivalent Model
54f47a6f211da55273e7008d894f7ae605ee7b3c	Apalache	InstanceNamed	InstanceWith	True	Passed	Model Under Test Equivalent Model
7ceaccb0e68eff3455b4ab5b30faa6f4ab325126	Apalache	InstanceNamed	InstanceWith	False	Passed	Model Under Test Equivalent Model
6c040dab865f76e0a4c02a08cc0c831bba49d5b7	Apalache	InstanceNamedWith	InstanceWith	True	Passed	Model Under Test Equivalent Model
df16ecaa06a3a60e2546a841a814fa3cd249650f	Apalache	InstanceNamedWith	InstanceWith	False	Passed	Model Under Test Equivalent Model
60ca816ffbb03b73614562d0c6892ff3b9095c7a	Apalache	InstanceInFolder	InstanceWith	True	Passed	Model Under Test Equivalent Model
9db47bb99cb2e55a7152cca2e5e910add1c08f76	Apalache	InstanceInFolder	InstanceWith	False	Passed	Model Under Test Equivalent Model
74d2041055f880b1d9b817a37f5fb1fb50d2523e	Apalache	InstanceWithInFolder	InstanceWith	True	Passed	Model Under Test Equivalent Model
b18898451802897233fecae2b40867ff2b57648a	Apalache	InstanceWithInFolder	InstanceWith	False	Passed	Model Under Test Equivalent Model
780336b4539e1f544d02bd5d9c77257e8d7f56d4	Apalache	InstanceNamedInFolder	InstanceWith	True	Passed	Model Under Test Equivalent Model
1662cfdd1d1dc1a14c28b46836bbc5cd63255f18	Apalache	InstanceNamedInFolder	InstanceWith	False	Passed	Model Under Test Equivalent Model
bca3ba95a974348c7c0f7fefc8a921c43fadbc39	Apalache	InstanceNamedWithInFolder	InstanceWith	True	Passed	Model Under Test Equivalent Model
e26aba6af7531e57884c4a067d4f68da6266ffae	Apalache	InstanceNamedWithInFolder	InstanceWith	False	Passed	Model Under Test Equivalent Model
e1c5eff5ce8fbe3c0cc169e200ce0ace8aae6e9a	Apalache	Enabled	InstanceWith	True	Passed	Model Under Test Equivalent Model
784b45213e2cd5163c0a3af2ad76eb86f9e1e479	Apalache	Enabled	InstanceWith	False	Passed	Model Under Test Equivalent Model
54ead1e53a735a239365d925a0dfda87216d37d4	Apalache	Assume	InstanceWith	True	Passed	Model Under Test Equivalent Model
d181f0620b05c7dba72d3aaa0ebf8a9d03c47dda	Apalache	Assume	InstanceWith	False	Passed	Model Under Test Equivalent Model
139e8b1066eedc38d1b6569090361d034677d383	Apalache	AssumeNamed	InstanceWith	True	Passed	Model Under Test Equivalent Model
203b9fd78804a5eabf4bb2e1077fbbf80cd6bce7	Apalache	AssumeNamed	InstanceWith	False	Passed	Model Under Test Equivalent Model
b0768969d06c4b44bf5cb8297ee1348fe9c3c169	Apalache	Lambda	InstanceWith	True	Passed	Model Under Test Equivalent Model
2861d8281b46e34c223fe37e3f317b4f580fc87f	Apalache	Lambda	InstanceWith	False	Passed	Model Under Test Equivalent Model
e9a68032e446dde38672a2005bd9695e3e1a1c11	Apalache	Cross2	InstanceWith	True	Passed	Model Under Test Equivalent Model
3aff98a7c84af42578a81f12f483db47de542d6f	Apalache	Cross2	InstanceWith	False	Passed	Model Under Test Equivalent Model
3fa90e7a6249ff9fe55d8f525270aea41789bbff	Apalache	Cross3	InstanceWith	True	Passed	Model Under Test Equivalent Model
c3a35c236c121e80e9236ad0e8ea7ff845f04f5f	Apalache	Cross3	InstanceWith	False	Passed	Model Under Test Equivalent Model
f66cf72c26230c85e5f6bc932638f3d97e697797	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	InstanceWith	True	Passed	Model Under Test Equivalent Model
6685bc9a32b50aafb275e53c77b091177715b691	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	InstanceWith	False	Passed	Model Under Test Equivalent Model
25b32638a83ac3a77f6b4ac91eb7d2fc92fec514	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	InstanceWith	True	Passed	Model Under Test Equivalent Model
694ffd3b9d8503a7e197d21bbd3c9e479d1b513e	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	InstanceWith	False	Passed	Model Under Test Equivalent Model
2a54f93ab41141c61b4b4240f30768071468113c	Apalache	SetDiff	InstanceWith	True	Passed	Model Under Test Equivalent Model
d60d85069d2718596d5268e170c3544bebd2c344	Apalache	SetDiff	InstanceWith	False	Passed	Model Under Test Equivalent Model
341d9336376c1735f29c9e671388ba37291b2a63	Apalache	SetUnion	InstanceWith	True	Passed	Model Under Test Equivalent Model
a8633cc2c44c02e5b727d20ef530b9afee40edd3	Apalache	SetUnion	InstanceWith	False	Passed	Model Under Test Equivalent Model
3f1c7e70a0f35cff42ae8c2d927b0a46bbb7b3cc	Apalache	SetIntersect	InstanceWith	True	Passed	Model Under Test Equivalent Model
d3b9b79183372a5822ae032b679a991013a8eee0	Apalache	SetIntersect	InstanceWith	False	Passed	Model Under Test Equivalent Model
59cdb713174c3e082921fe4a55aa9f5c60c5635d	Apalache	SubsetEq	InstanceWith	True	Passed	Model Under Test Equivalent Model
eb6fe61f090fd80f27fbd7724350a6aee1bf2513	Apalache	SubsetEq	InstanceWith	False	Passed	Model Under Test Equivalent Model
aa29eca9a60ce2e3be555fbc325ccf95b066ae8b	Apalache	IfCond	InstanceWith	True	Passed	Model Under Test Equivalent Model
59a2fbfea9703a597fdf8c8966d45069aac41556	Apalache	IfCond	InstanceWith	False	Passed	Model Under Test Equivalent Model
3eb5b782aa76a242b3ff4910264ef492eb114183	Apalache	IfThen	InstanceWith	True	Passed	Model Under Test Equivalent Model
1ae0f65f58d0332c8b6f0726c75b88133736251c	Apalache	IfThen	InstanceWith	False	Passed	Model Under Test Equivalent Model
8e85c5296ec741b98c1ce41947d64f7f9f309e97	Apalache	IfElse	InstanceWith	True	Passed	Model Under Test Equivalent Model
aa09a2dd4e13ff729df0335147907be8be4e47ee	Apalache	IfElse	InstanceWith	False	Passed	Model Under Test Equivalent Model
ea75818ca32a0cb047da2db70d0547dacb7dde20	Apalache	Subset	InstanceWith	True	Passed	Model Under Test Equivalent Model
d6a3483e0bfd52bf52a10c278a010b2ea15558fb	Apalache	Subset	InstanceWith	False	Passed	Model Under Test Equivalent Model
ea794cbf75f587eeeed46e6dade4182224b5ff28	Apalache	Domain	InstanceWith	True	Passed	Model Under Test Equivalent Model
f6b60637fa3359682833944d591a3ac8a5e73d27	Apalache	Domain	InstanceWith	False	Passed	Model Under Test Equivalent Model
9cbe4faf5da1e26b262f264c50d5d326f35c58ff	Apalache	Union	InstanceWith	True	Passed	Model Under Test Equivalent Model
6b58fcffbef71ad9ea14ce911a5e7722c38a1ddf	Apalache	Union	InstanceWith	False	Passed	Model Under Test Equivalent Model
6b9b5ed99856fce626f22ec4735e8eac9b2704fd	Apalache	Unchanged	InstanceWith	True	Passed	Model Under Test Equivalent Model
079f7772e9e702042eed60fe1896128f3d6b81ad	Apalache	Unchanged	InstanceWith	False	Passed	Model Under Test Equivalent Model
03e650dea2b5561dd8f094f50e3e5b2e6da4e409	Apalache	Equivalence	InstanceWith	True	Passed	Model Under Test Equivalent Model
d43d16c00a0551d597c987c36dedcf327854c63e	Apalache	Equivalence	InstanceWith	False	Passed	Model Under Test Equivalent Model
30557f8b764d055c109f3c58828684ee2d08edd9	Apalache	SeqLen	InstanceWith	True	Passed	Model Under Test Equivalent Model
023e69a29cd81f9cf42683c4c065945b6b667908	Apalache	SeqLen	InstanceWith	False	Passed	Model Under Test Equivalent Model
ebec4ece0def000fc589738c69626cbf4be6567a	Apalache	SeqConcat	InstanceWith	True	Passed	Model Under Test Equivalent Model
251cd619c37eaaed07d69d4810421e9966ae34e0	Apalache	SeqConcat	InstanceWith	False	Passed	Model Under Test Equivalent Model
0a50a4aad2f2e5075cd44e1107ca99fff99faed2	Apalache	SeqSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
ef2ab75d2b19e85b35b235cef6d5344831b55319	Apalache	SeqSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
76e769eeb1d21cb92ba4f93c1daade0c10813722	Apalache	SeqSelectSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
4227bc1b1eb9bcb6f5682aee0470b813bd56110c	Apalache	SeqSelectSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
3576219cc61cbccdfb2486ab3b1c79663b71f905	Apalache	SeqSubSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
349e0d989497c0184457b157a0033d1e08fc5949	Apalache	SeqSubSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
8530db1550c9257bb4b84eddec32589ed4f0e5cd	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	InstanceWith	True	Passed	Model Under Test Equivalent Model
32c16a0928057d3447d609638fb18c8b28cdfae5	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	InstanceWith	False	Passed	Model Under Test Equivalent Model
5b7b11a0032d5459be3d1139744bb0d3760a48f7	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceWith	True	Passed	Model Under Test Equivalent Model
85004fada3df35e6f0f2a392a8dbf3a12c01c488	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceWith	False	Passed	Model Under Test Equivalent Model
c6d1350dddba32889a55d2a9b1f02b40bdb6c529	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	InstanceWith	True	Passed	Model Under Test Equivalent Model
587711775fc10f92f565e77e8c793a807eea3151	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	InstanceWith	False	Passed	Model Under Test Equivalent Model
a59aa32ff026654bc12104e12ffd79595d9b1f02	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceWith	True	Passed	Model Under Test Equivalent Model
e07e376722c872272db8b42492cec799b24e6908	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceWith	False	Passed	Model Under Test Equivalent Model
13da1bedd6e90afb645f3898f946589f4565b8d7	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
fdb412b00c0aee45cd96f9eb1900c8c03f26022c	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
5f6e6906b7428b176efa6a90e040e32dc30fe722	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceWith	True	Passed	Model Under Test Equivalent Model
48012815fff2c2032d21c5bd67740a77e3d73cb9	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceWith	False	Passed	Model Under Test Equivalent Model
7d24c1e91996a586fc93315679d9ee4e2c8877fb	Apalache	BagBagToSet	InstanceWith	True	Passed	Model Under Test Equivalent Model
7c86a0cfc20b3c46fc7a4518e29570cdb6d82a01	Apalache	BagBagToSet	InstanceWith	False	Passed	Model Under Test Equivalent Model
99dd97b2402cedc5b26790169bea492a7c0f6f85	Apalache	BagSetToBag	InstanceWith	True	Passed	Model Under Test Equivalent Model
becad0d7fff67180ad2c3ed40b105f328d884635	Apalache	BagSetToBag	InstanceWith	False	Passed	Model Under Test Equivalent Model
add39047cd9b81141de7c24288b06955b46eb06d	Apalache	BagBagIn	InstanceWith	True	Passed	Model Under Test Equivalent Model
ea197e0220be8319d8eb5481c956aa8cf8252334	Apalache	BagBagIn	InstanceWith	False	Passed	Model Under Test Equivalent Model
26cf97104baaf627e0b26ae1eafb294f15884898	Apalache	BagAddBag	InstanceWith	True	Passed	Model Under Test Equivalent Model
8b5f1b4e0e6ee61a1aca3a52251ccefc12d2b936	Apalache	BagAddBag	InstanceWith	False	Passed	Model Under Test Equivalent Model
72369da98ff797f96ffb0bbee2b79bb15dcebda6	Apalache	BagBagSub	InstanceWith	True	Passed	Model Under Test Equivalent Model
cc2e3e9d531e70b394ca9397dde8add48af8a53d	Apalache	BagBagSub	InstanceWith	False	Passed	Model Under Test Equivalent Model
0c97877c70881da257b183c0fc65c96a443f7d39	Apalache	BagCopiesIn	InstanceWith	True	Passed	Model Under Test Equivalent Model
1c64f88d80905802564d11544944177507547f2e	Apalache	BagCopiesIn	InstanceWith	False	Passed	Model Under Test Equivalent Model
015842cb0f4025dd28cc006b2c9d0c44ee6397e3	Apalache	BagSubsetEqBag	InstanceWith	True	Passed	Model Under Test Equivalent Model
77d648f28f25351d944c612625cdd7359ff683a5	Apalache	BagSubsetEqBag	InstanceWith	False	Passed	Model Under Test Equivalent Model
ffcf31c9eb2801366ed1168550818a8dc2b54b2c	Apalache	BagBagUnion	InstanceWith	True	Passed	Model Under Test Equivalent Model
28d90cb3e1d6096fb1b48a3c7b37c6c59030ef61	Apalache	BagBagUnion	InstanceWith	False	Passed	Model Under Test Equivalent Model
a61128c4901f6185d1905a219c508dd63e6521b0	Apalache	BagBagCardinality	InstanceWith	True	Passed	Model Under Test Equivalent Model
d3f19799ff5faec2c4c895ac69ab4c10837f21c9	Apalache	BagBagCardinality	InstanceWith	False	Passed	Model Under Test Equivalent Model
6f92776c1d7ed4e89ad5a2081d7890ef45d6618e	Apalache	BagBagOfAll	InstanceWith	True	Passed	Model Under Test Equivalent Model
d42c48b068dbd5005dfc013e6df2e81f2ec2d366	Apalache	BagBagOfAll	InstanceWith	False	Passed	Model Under Test Equivalent Model
c7ad3a4b7fe8a0503e5795f3a9553d9d07ead091	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceWith	True	Passed	Model Under Test Equivalent Model
7beb547dbe57e43904c1e34a875a1fe84211bbfb	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceWith	False	Passed	Model Under Test Equivalent Model
a223c83ad581eba4044b744b2174ff3f1dba5183	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	InstanceWith	True	Passed	Model Under Test Equivalent Model
e4d87639c22ed326392a391cd8a83567308af02d	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	InstanceWith	False	Passed	Model Under Test Equivalent Model
06060e4a75fed3356bc3f6275cdaddcc271695fd	Apalache	FiniteSetsCardinality	InstanceWith	True	Passed	Model Under Test Equivalent Model
a54e7557d259c513ca44a6d7043afb2bde41fe50	Apalache	FiniteSetsCardinality	InstanceWith	False	Passed	Model Under Test Equivalent Model
feee2fd85054ea9876a78c90b9fe7b508c4b9424	Apalache	SeqHead	InstanceWith	True	Passed	Model Under Test Equivalent Model
501483323f290b605e4652d82fcedf3281011e3f	Apalache	SeqHead	InstanceWith	False	Passed	Model Under Test Equivalent Model
e67cb92b8e0f032a8b791a543e480c8ab38e15fe	Apalache	SeqTail	InstanceWith	True	Passed	Model Under Test Equivalent Model
f778b48a0824e06eaabfded05f911d6c984ab624	Apalache	SeqTail	InstanceWith	False	Passed	Model Under Test Equivalent Model
95eb5df79e0591d0622a7fd1b6510c7de86c0e3a	Apalache	SeqAppend	InstanceWith	True	Passed	Model Under Test Equivalent Model
e88943812422068689b7903d414ad68fbd869653	Apalache	SeqAppend	InstanceWith	False	Passed	Model Under Test Equivalent Model

Index

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