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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b7d63fc15933d511a231b6f5668c12999d9b5c48	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	InstanceWith	OneLineComment	True	Passed	Model Under Test Equivalent Model
51ec975e7ba23ee0437d322220d2b013a12206d0	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	InstanceWith	OneLineComment	False	Passed	Model Under Test Equivalent Model
886466fe70a45f7dce03fc3a4e04e7d216379780	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	InstanceWith	MultiLineComment	True	Passed	Model Under Test Equivalent Model
69b6ef062e43e33b0c98a344c05ac44c6c32a9ed	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	InstanceWith	MultiLineComment	False	Passed	Model Under Test Equivalent Model
1838a88ab4fac33518655d7a2991d1dc151e4b9f	Apalache	InstanceWith	BoolTrue	True	Passed	Model Under Test Equivalent Model
002781a1856b29a3e501d196da9439f55cb04af4	Apalache	InstanceWith	BoolTrue	False	Passed	Model Under Test Equivalent Model
74ec2655b480b66ef073c48a7950e597d23124bc	Apalache	InstanceWith	BoolFalse	True	Passed	Model Under Test Equivalent Model
bf3c0aa3e4701be2f31f90b41d79dd49b69626da	Apalache	InstanceWith	BoolFalse	False	Passed	Model Under Test Equivalent Model
a7146c2a808828692b81d12d44f1bc4f97cdfaac	Apalache	InstanceWith	BoolSet	True	Passed	Model Under Test Equivalent Model
86e638f87143b703713a228b88a6f5d9b18f56e3	Apalache	InstanceWith	BoolSet	False	Passed	Model Under Test Equivalent Model
cfd95aa67162c5d452e566d2c29aefae12bdd619	Apalache	InstanceWith	And	True	Passed	Model Under Test Equivalent Model
e0892d77dea96e24755bcea349b54fa4afe270ce	Apalache	InstanceWith	And	False	Passed	Model Under Test Equivalent Model
2556edc9db7d4c172e7c38b195afb6108fd76da6	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	InstanceWith	AndMultiLine	True	Passed	Model Under Test Equivalent Model
0dcad25f23138e4d15a87e3f28c946bf694f584d	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	InstanceWith	AndMultiLine	False	Passed	Model Under Test Equivalent Model
901f2dd11e5458e3c37de0637bf22dd66e1a582d	Apalache	InstanceWith	Imply	True	Passed	Model Under Test Equivalent Model
278df3358cf4aa85dc6210778b97ada2a6fe45d8	Apalache	InstanceWith	Imply	False	Passed	Model Under Test Equivalent Model
b02dac24c226ef3234d1dbece6e40a69ef250b48	Apalache	InstanceWith	Not	True	Passed	Model Under Test Equivalent Model
f204c067f5e8c595943d5945e701b6d3de229f52	Apalache	InstanceWith	Not	False	Passed	Model Under Test Equivalent Model
63a0a83cc8e826b0ed800880aa971362236e478e	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	InstanceWith	Or	True	Passed	Model Under Test Equivalent Model
92fcf41af16d055ad4b39abbe4ffeeee78f30a90	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	InstanceWith	Or	False	Passed	Model Under Test Equivalent Model
6566809c82696ec1437b58f9ad1dc3541735ef4c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	InstanceWith	OrMultiLine	True	Passed	Model Under Test Equivalent Model
b70bf5ae1cf8b103fe10579a3b809915d7e3fcb6	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	InstanceWith	OrMultiLine	False	Passed	Model Under Test Equivalent Model
5e1684a9a7cf0d55f68175220db0a6a0b728f460	Apalache	InstanceWith	AndProp	True	Passed	Model Under Test Equivalent Model
424509c766781063d3e95271c9f27da6d75e5ae0	Apalache	InstanceWith	AndProp	False	Passed	Model Under Test Equivalent Model
eaf8bed47c2b7f94cbb557da51843f52f9873764	Apalache	InstanceWith	Boxed	True	Passed	Model Under Test Equivalent Model
5fe91b38b2fe929aed990be9a56277105a895b5d	Apalache	InstanceWith	Boxed	False	Passed	Model Under Test Equivalent Model
99c93c7f71423c7d5b25e8db86b06827b53a99db	Apalache	InstanceWith	Eq	True	Passed	Model Under Test Equivalent Model
78f6bb5fa56a012db5b30685c5876ac8917186bf	Apalache	InstanceWith	Eq	False	Passed	Model Under Test Equivalent Model
276e6e7106d2f5188026c686b2239023f9645a2a	Apalache	InstanceWith	Ne	True	Passed	Model Under Test Equivalent Model
e969c490e01dad77474f04170498ebcb9c8f73ba	Apalache	InstanceWith	Ne	False	Passed	Model Under Test Equivalent Model
137f03d7edf87a4484629b677dccbe7c8de8a4d0	Apalache	InstanceWith	Let	True	Passed	Model Under Test Equivalent Model
ab6ae72640a6054ef6a01160b4ba0a776a3be156	Apalache	InstanceWith	Let	False	Passed	Model Under Test Equivalent Model
5bcd7ff09eebe8e6d404a3907413654af487140e	Apalache	InstanceWith	SetEmpty	True	Passed	Model Under Test Equivalent Model
73431edcacf62694ea0f956258d219cee8faf641	Apalache	InstanceWith	SetEmpty	False	Passed	Model Under Test Equivalent Model
76de8229193da9c3aa9e29eee3712946e1231559	Apalache	InstanceWith	Set0	True	Passed	Model Under Test Equivalent Model
55b77b9b5b3de207688dee48d6d6933eb6c97190	Apalache	InstanceWith	Set0	False	Passed	Model Under Test Equivalent Model
74d389ae15c1c73c1fc75e441d9c0603060f8169	Apalache	InstanceWith	Set1	True	Passed	Model Under Test Equivalent Model
5e4541f4f905b8885777e1be7cf84de2a30baa95	Apalache	InstanceWith	Set1	False	Passed	Model Under Test Equivalent Model
50c4b84fbb5f4df1b222547b87aa8e401c45ebbf	Apalache	InstanceWith	Set2	True	Passed	Model Under Test Equivalent Model
66d2c5d7332524e241f7e572264480d34351d2f3	Apalache	InstanceWith	Set2	False	Passed	Model Under Test Equivalent Model
1d4d2bb1492d3d70dfdf88e1de923aca1b802fab	Apalache	InstanceWith	Fun	True	Passed	Model Under Test Equivalent Model
2876befa54cba3863ce65782ee43489626479527	Apalache	InstanceWith	Fun	False	Passed	Model Under Test Equivalent Model
656c1c18edec5fcb1ab99330ac9e0146933a0b6b	Apalache	InstanceWith	In	True	Passed	Model Under Test Equivalent Model
3f9c84f45229f1ee34bc97e77c5492b2c52f2b32	Apalache	InstanceWith	In	False	Passed	Model Under Test Equivalent Model
a1084e43064c70eab0db484954f09c8fb5d49310	Apalache	InstanceWith	NotIn	True	Passed	Model Under Test Equivalent Model
7cdb3277ca7c0a248b25fa83c3364ad4bb5fc3f2	Apalache	InstanceWith	NotIn	False	Passed	Model Under Test Equivalent Model
b1762bd7ebf25f91a8f34d569cbdabbd42a7d878	Apalache	InstanceWith	Exists	True	Passed	Model Under Test Equivalent Model
a4270fafac8478aaaa4b0abc08db049a5a94220a	Apalache	InstanceWith	Exists	False	Passed	Model Under Test Equivalent Model
dda9f7c416d12a0c7adf86d4ebd932d7b9314eca	Apalache	InstanceWith	Forall	True	Passed	Model Under Test Equivalent Model
d9f4c6e245340c788291651d580f8fe281f30399	Apalache	InstanceWith	Forall	False	Passed	Model Under Test Equivalent Model
2ecc294ef45b5821d222c21d2b1a2368a9772098	Apalache	InstanceWith	Choose	True	Passed	Model Under Test Equivalent Model
4e5ac940e1566e0d0328f83f27b1073b75c9fe3e	Apalache	InstanceWith	Choose	False	Passed	Model Under Test Equivalent Model
2c2b31951445ebddf5db62accc6f6687a468519b	Apalache	InstanceWith	Record	True	Passed	Model Under Test Equivalent Model
7ad3f2ee42607384b02fb10de87d451a230e700b	Apalache	InstanceWith	Record	False	Passed	Model Under Test Equivalent Model
9b5455ddfa773ed55be377cd63398249ffcbda5a	Apalache	InstanceWith	Tuple	True	Passed	Model Under Test Equivalent Model
0411c7dc6927d418ffc3b43bf1bfc7b27707337c	Apalache	InstanceWith	Tuple	False	Passed	Model Under Test Equivalent Model
d54e0190c8bb867239c0c628ebdaf9ec9b8c8bee	Apalache	InstanceWith	TupleEmpty	True	Passed	Model Under Test Equivalent Model
becc20ead3c0be05d0e56aa6820d1ef8e60ee913	Apalache	InstanceWith	TupleEmpty	False	Passed	Model Under Test Equivalent Model
1d0512e93678c1e25d5d23cb7ec850f40c91300e	Apalache	InstanceWith	FunApp	True	Passed	Model Under Test Equivalent Model
ce18e80eb80a2004ba684907b757d6398eb96ac8	Apalache	InstanceWith	FunApp	False	Passed	Model Under Test Equivalent Model
710a4ae21b9704cc24ff1ce8c200eb9388b3e2e4	Apalache	InstanceWith	Prime	True	Passed	Model Under Test Equivalent Model
9f40f6e88e31470d72e066b74ad773949a1d29c6	Apalache	InstanceWith	Prime	False	Passed	Model Under Test Equivalent Model
a2a7d56e592d5bf0f94d23abe224385618a17fd4	Apalache	InstanceWith	NumZero	True	Passed	Model Under Test Equivalent Model
2e064815ff9c11e927c3b01aa99b4c5569cf5825	Apalache	InstanceWith	NumZero	False	Passed	Model Under Test Equivalent Model
c2d5bc49b759d21ecbd8df434900c87c23410fa4	Apalache	InstanceWith	NumOne	True	Passed	Model Under Test Equivalent Model
dbbe2a2ead8574709bcf25514caa18405ad45a2f	Apalache	InstanceWith	NumOne	False	Passed	Model Under Test Equivalent Model
94bc0e70ffe318582a60ce29de4d0321bd4a58a1	Apalache	InstanceWith	NumMaxInt	True	Passed	Model Under Test Equivalent Model
316285f73f38aaf50b46141174f88139eec44a55	Apalache	InstanceWith	NumMaxInt	False	Passed	Model Under Test Equivalent Model
2c0742492b9ffb4d0aeb1d23be68399839118552	Apalache	InstanceWith	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
33b140bda260ba0a695adbcb7350ca581e2ef80b	Apalache	InstanceWith	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
3091b6993af386c5a97bc7aedbddb4ea1d559142	Apalache	InstanceWith	NumPlus	True	Passed	Model Under Test Equivalent Model
3a2135ff951df7837c138107dde7aa29b13d8768	Apalache	InstanceWith	NumPlus	False	Passed	Model Under Test Equivalent Model
2d820ca0d9583aecd0a1acc6982abae5457fc41f	Apalache	InstanceWith	NumMinus	True	Passed	Model Under Test Equivalent Model
ad2af1edb4a8ecc55c67a011c38ed4668fc3ef2e	Apalache	InstanceWith	NumMinus	False	Passed	Model Under Test Equivalent Model
6786f6b9026a571e116866c8856b7550983d53c8	Apalache	InstanceWith	NumMul	True	Passed	Model Under Test Equivalent Model
e47fc4147992bd9c489485ded1dfdf8ce3775290	Apalache	InstanceWith	NumMul	False	Passed	Model Under Test Equivalent Model
9581c81d1251359a52f87573c2235e00b0279ccf	Apalache	InstanceWith	NumDiv	True	Passed	Model Under Test Equivalent Model
85543149acab050bb805f8eff8f1a0fe9adf4052	Apalache	InstanceWith	NumDiv	False	Passed	Model Under Test Equivalent Model
4d8793a24301661e647c26fef6763fec3f7b8e6c	Apalache	InstanceWith	NumMod	True	Passed	Model Under Test Equivalent Model
6e06b514b5c188a6a756ff3c2bc2c16225f8f5f1	Apalache	InstanceWith	NumMod	False	Passed	Model Under Test Equivalent Model
7df8cd7d2b3f294743c39eb87e84fa0da80d8b6a	Apalache	InstanceWith	NumPow	True	Passed	Model Under Test Equivalent Model
eebf20936d1ec9be817b463ae5aabd67984f555e	Apalache	InstanceWith	NumPow	False	Passed	Model Under Test Equivalent Model
9734babf0826c1aa41b6a9916a409ccc72226e77	Apalache	InstanceWith	NumGt	True	Passed	Model Under Test Equivalent Model
e4fd3173721e878d84995139d47ecc0d9dcc060b	Apalache	InstanceWith	NumGt	False	Passed	Model Under Test Equivalent Model
bc3912e1ed2142d29a5811e13f68d5280ed56177	Apalache	InstanceWith	NumGe	True	Passed	Model Under Test Equivalent Model
59fe0d56b97fa3e6e2e1dbed8fbf1de84f7d9a58	Apalache	InstanceWith	NumGe	False	Passed	Model Under Test Equivalent Model
6ecc62cc3804ad5b76b18c0004dde55064548a97	Apalache	InstanceWith	NumLt	True	Passed	Model Under Test Equivalent Model
4a00154f64d1953bfc7615b1a9ddc9b22fbacccc	Apalache	InstanceWith	NumLt	False	Passed	Model Under Test Equivalent Model
f0a0fac12c02e43e0e422ca36ea952893bf0885a	Apalache	InstanceWith	NumLe	True	Passed	Model Under Test Equivalent Model
c9ca23d2d29ee22740bf65845799b5bd3a966446	Apalache	InstanceWith	NumLe	False	Passed	Model Under Test Equivalent Model
fa6dd11b4a89a9f90118a9f9a67398d0e8703a94	Apalache	InstanceWith	DefFun	True	Passed	Model Under Test Equivalent Model
b713c3ccde96a3132609a2869bc87572833e99f2	Apalache	InstanceWith	DefFun	False	Passed	Model Under Test Equivalent Model
f7215298cc1aa9ffe3a5079d3e970c1cb2347c34	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDefFun	True	Passed	Model Under Test Equivalent Model
5e5ea540f45ada95fa786eddf93997d29d49fe6c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDefFun	False	Passed	Model Under Test Equivalent Model
2cb2aaa3fcda0e105a4dc38b51e7046bfab2444c	Apalache	InstanceWith	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
39aa868e04d0c76e8f30c237fd1fc649665c0446	Apalache	InstanceWith	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
579742fcfd5d553762bc3759bd58994c994859f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
2d28c8db17e75e48597717e0f89e350d56a51bd8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
30435098c01b98d42ff6c141add977016bc68645	Apalache	InstanceWith	Def0	True	Passed	Model Under Test Equivalent Model
81b24f92cf39a9dbde1f271bff17fdbdce47f5d3	Apalache	InstanceWith	Def0	False	Passed	Model Under Test Equivalent Model
f217c4e4c6b8cefd3f90c619057c9e9654404ca3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef0	True	Passed	Model Under Test Equivalent Model
a3f59d2d3b4a2954492a79b948c433f63e45593a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef0	False	Passed	Model Under Test Equivalent Model
875c65914585372966d5a722e3b8b1435c39b5e8	Apalache	InstanceWith	Def1	True	Passed	Model Under Test Equivalent Model
7661a55853702736f7d0eba17ce401c2947d8d69	Apalache	InstanceWith	Def1	False	Passed	Model Under Test Equivalent Model
35c42eab027bc245b46c39701f42b9fd97c83798	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1	True	Passed	Model Under Test Equivalent Model
d018bf7a217dc481c0d3e2e3756e8e8f75e14fd4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1	False	Passed	Model Under Test Equivalent Model
33454474641e6faf4c693dd272d82f2b1e5d6be4	Apalache	InstanceWith	Def2	True	Passed	Model Under Test Equivalent Model
78c9aa430d96728ba7e82bd603823ec0499819e9	Apalache	InstanceWith	Def2	False	Passed	Model Under Test Equivalent Model
4d1a91cf1f89ac20fe09519ef5e61064762998a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef2	True	Passed	Model Under Test Equivalent Model
d974fb153dd4d56bfc9386c6c4a325954d2cd2eb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef2	False	Passed	Model Under Test Equivalent Model
56fb9bdd4440a42023a507c4220fe246274786ce	Apalache	InstanceWith	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3e78a8eecac7da2b4bc865baee2356ae388cdec2	Apalache	InstanceWith	Def1Recursive	False	Passed	Model Under Test Equivalent Model
49fcd4fbbe256a5ffb8ab366ac960b88345d60dc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
c37ae3cdb560ec97d29d93a34c22a084a2c31ed7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
ddb7df94261c8f6ba0d232ebdc74fd0e0b7a6481	Apalache	InstanceWith	Extends	True	Passed	Model Under Test Equivalent Model
4b42d3112150b38b845cc51f71c95d000b00ebfc	Apalache	InstanceWith	Extends	False	Passed	Model Under Test Equivalent Model
472cc747a42c1e1ff02d4fedbc8650a4d73183f7	Apalache	InstanceWith	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
5967b5d6d1e91094f8fbf28a2d2ac5b8b761077e	Apalache	InstanceWith	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
a4912964f5e9e26ea2bb5538450d1a46693dc85f	Apalache	InstanceWith	Variable	True	Passed	Model Under Test Equivalent Model
23cb1bc4e226bdba56d0d6725d23ef3e81204f0e	Apalache	InstanceWith	Variable	False	Passed	Model Under Test Equivalent Model
ad9497e2c410cb199bba2ff7b098f5fac9aabddd	Apalache	InstanceWith	Constant	True	Passed	Model Under Test Equivalent Model
c4acb9128211dbe842f2e6fc64354a66980fb183	Apalache	InstanceWith	Constant	False	Passed	Model Under Test Equivalent Model
03914d4f371f10c6a95d4f41db81f38cc6f442fa	Apalache	InstanceWith	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
ec98765cbb44394f469b022e480064f5dbd2241f	Apalache	InstanceWith	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
e6dc50404282317a692d0204a60d0de5f6f03605	Apalache	InstanceWith	ConstantRank1	True	Passed	Model Under Test Equivalent Model
552328426bd9defeb729a13d70b2dd62f93cccca	Apalache	InstanceWith	ConstantRank1	False	Passed	Model Under Test Equivalent Model
bc72b566a0d5363485d7e1448b1d80504eaa6934	Apalache	InstanceWith	Instance	True	Passed	Model Under Test Equivalent Model
cb8f5ac2dfb934c4664afb0698071771f6b28c98	Apalache	InstanceWith	Instance	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
160f48114161c3c5ddd74f7e961c92884a9b3c56	Apalache	InstanceWith	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5d4b18495672aae1bf6300b7291d871520161c48	Apalache	InstanceWith	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5571841034013bdbc44a109c499a7a4683e34373	Apalache	InstanceWith	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
84a0f26986e7a0b6524ac03798f96732f469dc46	Apalache	InstanceWith	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
0b9777aab1ee1d5bdaf5e078812585234575aa03	Apalache	InstanceWith	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
8635cba93eb0e198dff916d517b5c5c32dec8a69	Apalache	InstanceWith	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
3d17ac8f5dced8b699470719136562d8e6b6f074	Apalache	InstanceWith	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
699ab5ff088135aff7746a29a1c14d270e15156e	Apalache	InstanceWith	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
d82139ac59f7ccdd957ab930d0421325f862bec1	Apalache	InstanceWith	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
fd37b7894ebe686fc59e310dbbf64738d401588b	Apalache	InstanceWith	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
52668e094e5e3eb24b0b297b868d2d2ca0369917	Apalache	InstanceWith	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
5732f918a0752af9b9e6a870158b6de7e0acbe8e	Apalache	InstanceWith	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
a45997b3abe437c47ee11973fb3583a6640eba5c	Apalache	InstanceWith	Enabled	True	Passed	Model Under Test Equivalent Model
8d5cb6d5d6a0b4ef4a216c01122b5a9bbbd0e817	Apalache	InstanceWith	Enabled	False	Passed	Model Under Test Equivalent Model
fe8f4649f2f4e2c7e4ea9891e85a8ccfca9b9114	Apalache	InstanceWith	Cross2	True	Passed	Model Under Test Equivalent Model
8715c5a0eba88204c02dd19ceb5f39cf085c1058	Apalache	InstanceWith	Cross2	False	Passed	Model Under Test Equivalent Model
05dc5af69bac28bd3cffcc82d9735eb18e96df91	Apalache	InstanceWith	Cross3	True	Passed	Model Under Test Equivalent Model
453c2dfcfeb314295ac09193c27e886a3efc93f4	Apalache	InstanceWith	Cross3	False	Passed	Model Under Test Equivalent Model
7e34c470906e9efcf539c89578b5f7da9d9dd6ac	TLC with reduction strategy: Plug 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))	InstanceWith	FunSet	True	Passed	Model Under Test Equivalent Model
7fef4463d743276657cfae8b41622ea190685442	TLC with reduction strategy: Plug 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))	InstanceWith	FunSet	False	Passed	Model Under Test Equivalent Model
53a1f8aba27ae88439d89f6358f8cf63cdb53f6f	TLC with reduction strategy: Plug 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)	InstanceWith	RecordSet	True	Passed	Model Under Test Equivalent Model
51383b2fcd8747da6ab217c65cc04c04c1476e4f	TLC with reduction strategy: Plug 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)	InstanceWith	RecordSet	False	Passed	Model Under Test Equivalent Model
e0358d787a154f1cc2100656b8a89030588759bc	Apalache	InstanceWith	SetDiff	True	Passed	Model Under Test Equivalent Model
c750e72aa6a97482e4620390eb097d5638a7ecdf	Apalache	InstanceWith	SetDiff	False	Passed	Model Under Test Equivalent Model
f9bab0e5fda9d0cae586cd344d8fec1128ee8b9c	Apalache	InstanceWith	SetUnion	True	Passed	Model Under Test Equivalent Model
53c71824eeae689aa603cb5ea2c3cc2b8c197148	Apalache	InstanceWith	SetUnion	False	Passed	Model Under Test Equivalent Model
8fc4041c43d5e1c58ca6555972b2962b138cfefd	Apalache	InstanceWith	SetIntersect	True	Passed	Model Under Test Equivalent Model
f12f5a4239e416549c2d80f2b660c7a41946f2c5	Apalache	InstanceWith	SetIntersect	False	Passed	Model Under Test Equivalent Model
62dae35b17c6dea31b0998f1774b803862a8cea6	Apalache	InstanceWith	SubsetEq	True	Passed	Model Under Test Equivalent Model
40edbd152ed883211a7039cd98f510be752b8eda	Apalache	InstanceWith	SubsetEq	False	Passed	Model Under Test Equivalent Model
8691314bc46867fbebd8c435030b9c6fec81fdff	Apalache	InstanceWith	IfCond	True	Passed	Model Under Test Equivalent Model
4019a74af39f519007315b76d1cea75ff275df20	Apalache	InstanceWith	IfCond	False	Passed	Model Under Test Equivalent Model
3061b2336bf585390c6e5062a0fb0a4422c32c95	Apalache	InstanceWith	IfThen	True	Passed	Model Under Test Equivalent Model
9748fdf97de15b6482edad1a7a2aff17a52d2ee2	Apalache	InstanceWith	IfThen	False	Passed	Model Under Test Equivalent Model
717f6f187e666540597f37bf82f88d9d13ffb202	Apalache	InstanceWith	IfElse	True	Passed	Model Under Test Equivalent Model
90dd803d3e2d9038b8eee84ba47d7ce1ccf446d2	Apalache	InstanceWith	IfElse	False	Passed	Model Under Test Equivalent Model
6e5be8e66ed9900c644862531c0d2ebb2d09c5f5	Apalache	InstanceWith	Subset	True	Passed	Model Under Test Equivalent Model
3c981a27e09d155f78ee81acb33ca364cfb1882a	Apalache	InstanceWith	Subset	False	Passed	Model Under Test Equivalent Model
6bc8e36637ae32655f5071293e178e514e356cc7	Apalache	InstanceWith	Domain	True	Passed	Model Under Test Equivalent Model
ebb46259b8c1175c08475f7d278bfd52a6ea4de8	Apalache	InstanceWith	Domain	False	Passed	Model Under Test Equivalent Model
81abc4bb60eaee125c757a0e8de8b8ea6dc4a5db	Apalache	InstanceWith	Union	True	Passed	Model Under Test Equivalent Model
51d201f5d5adecbc2e3a50b199d1abf2558602c9	Apalache	InstanceWith	Union	False	Passed	Model Under Test Equivalent Model
3874b65d9457907fab7dd3351d96a38f773bf22b	Apalache	InstanceWith	Unchanged	True	Passed	Model Under Test Equivalent Model
dff0640cbc54651efc1ad6863d4c4d21ecda9310	Apalache	InstanceWith	Unchanged	False	Passed	Model Under Test Equivalent Model
00e62949e77ab5841c1b768a718bf39eb1702d23	Apalache	InstanceWith	Equivalence	True	Passed	Model Under Test Equivalent Model
76cc17d02600a0228d8fefcf135b7d52a1572573	Apalache	InstanceWith	Equivalence	False	Passed	Model Under Test Equivalent Model
7d6e933a805ddd3494cfd079206def00cada24d0	Apalache	InstanceWith	StringEmpty	True	Passed	Model Under Test Equivalent Model
eb118e39e2474617d37b13d0c141538a79d8461b	Apalache	InstanceWith	StringEmpty	False	Passed	Model Under Test Equivalent Model
c8dc5fc08fbe6bf593fc15a1bd58869ade50602b	Apalache	InstanceWith	String	True	Passed	Model Under Test Equivalent Model
19727abe819db05eb53da30a3c123536eede5b23	Apalache	InstanceWith	String	False	Passed	Model Under Test Equivalent Model
2969a31491962eb044d388ac8da50a9e98658c6b	Apalache	InstanceWith	SeqLen	True	Passed	Model Under Test Equivalent Model
523e73d92a04cb7daf9ef87221e1bce12f2a8e14	Apalache	InstanceWith	SeqLen	False	Passed	Model Under Test Equivalent Model
449113738f692c2ea84105c8e416623b3ae63956	Apalache	InstanceWith	SeqConcat	True	Passed	Model Under Test Equivalent Model
21452302cd90f6f46a1c426a613656bf543e8a8c	Apalache	InstanceWith	SeqConcat	False	Passed	Model Under Test Equivalent Model
2b450a1ce7dc644c8436bab04a676c01e99b01d7	Apalache	InstanceWith	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a9e8ba236f38d71886fe776953a4d6c216a3898e	Apalache	InstanceWith	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
d7826437292f83545f533b6cfacb29cbf41850b2	Apalache	InstanceWith	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
5a5dddd719077a1cb2490162a67a74adf1be97f8	Apalache	InstanceWith	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d7e53433df992091fa263ad615c11cc6f5c56ff3	TLC with reduction strategy: Plug 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	InstanceWith	NumRange	True	Passed	Model Under Test Equivalent Model
dfa6503af767b109bf3bd88fc82aaacc0337cf4b	TLC with reduction strategy: Plug 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	InstanceWith	NumRange	False	Passed	Model Under Test Equivalent Model
c3787d71c1dbc38704960ce73b37b72735425615	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	InstanceWith	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
335fee002529e6dc8afeab31447554f4ea3899f0	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	InstanceWith	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
32d3c65063f7a23926047975e7014c4fd67b506c	TLC with reduction strategy: Plug 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]]	InstanceWith	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
f4c59589bbe23919b32f248ff5f30534417309b3	TLC with reduction strategy: Plug 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]]	InstanceWith	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
d080ebec07b1b34c908386ae5417bc318eb24eaa	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	InstanceWith	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
f4a4569de117e383d08d10b549105c21cdd48fd7	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	InstanceWith	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
d5ad7399471acad7aa0c31c2aea647863df45ca4	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	InstanceWith	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
ddfdaf35f43aaa4d0dcb5a67f593f1ab80e295e0	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	InstanceWith	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
ff1dcb4e356df9d66f72a6fa7028179725184e36	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	InstanceWith	TlcEval	True	Passed	Model Under Test Equivalent Model
05a80dccce2a7a37bdea663dd0ed8c9db943a339	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	InstanceWith	TlcEval	False	Passed	Model Under Test Equivalent Model
ad1add32aa010fb26b044a4c9d56ad8e8e6c6517	Apalache	InstanceWith	BagBagToSet	True	Passed	Model Under Test Equivalent Model
4552cc49558993314d32ec9b138ed43b298dda6b	Apalache	InstanceWith	BagBagToSet	False	Passed	Model Under Test Equivalent Model
1bbdf716070c64221863556aa9954ee1b58d26fb	Apalache	InstanceWith	BagSetToBag	True	Passed	Model Under Test Equivalent Model
e070e619c6e38ed3b4752f21a8db90d083dc9716	Apalache	InstanceWith	BagSetToBag	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
5bb2c91ee1fdb2bacc0a087fa9df76926f31498a	Apalache	InstanceWith	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
824d0bc1dac1b3b51f1a3195cce8f3d1d9601581	Apalache	InstanceWith	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
9fe062ab339a13d3011bc9d52f08ce29df2f2184	Apalache	InstanceWith	BagAddBag	True	Passed	Model Under Test Equivalent Model
fe1a9a76438f27823c4b2c5cfbc3aec196f866ca	Apalache	InstanceWith	BagAddBag	False	Passed	Model Under Test Equivalent Model
6058f214e3144ee6e8be0e2ededaedda26b584a5	Apalache	InstanceWith	BagBagSub	True	Passed	Model Under Test Equivalent Model
f3fabd81bf417b70a29766e903abc96df360a0dd	Apalache	InstanceWith	BagBagSub	False	Passed	Model Under Test Equivalent Model
ef6ad8d28baca88fc26dc6e909b76000a9bed07b	Apalache	InstanceWith	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
dbe3c72ad7875b39b4c35d308baa03f2b3ab2697	Apalache	InstanceWith	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
b962e3f831e838f0a6f48bdc3115ce44484a45d3	Apalache	InstanceWith	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
5390ee408e3322d7937648bb30acd86ecd4a1678	Apalache	InstanceWith	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
78b138cd8cdecabd828fb100798613288eecb193	Apalache	InstanceWith	BagBagUnion	True	Passed	Model Under Test Equivalent Model
b96222a250e2c910219d8558fa7f8bb7890d604c	Apalache	InstanceWith	BagBagUnion	False	Passed	Model Under Test Equivalent Model
7968786e1cb073a01514f71ca82acbbcd3294b15	Apalache	InstanceWith	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
1de3c29a126d6ff8243da163e435493c773387a0	Apalache	InstanceWith	BagBagCardinality	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
f93c84faf95d56891a03b5653d4f2c05dc3a8456	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	InstanceWith	BagSubBag	True	Passed	Model Under Test Equivalent Model
da2a153891e1375cbdaabc0761ba68f0c517f7fe	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	InstanceWith	BagSubBag	False	Passed	Model Under Test Equivalent Model
897f9fe0bcbc60bf12b0a55a0c88a2e4660e1ccb	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	InstanceWith	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
ed5c76336f655da44b14095a33437416581e500f	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	InstanceWith	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
c1733070d6ec3bf1673a7202b7abf3d8ecadb35c	Apalache	InstanceWith	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
91123429d4f70ddc5e5a80e12fc3fac06e71d20c	Apalache	InstanceWith	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
73d57f11175aaac680c562ae961e3de5d7cae988	Apalache	InstanceWith	SeqHead	True	Passed	Model Under Test Equivalent Model
092e3d79080b215c593df1900ca7260124a6d44e	Apalache	InstanceWith	SeqHead	False	Passed	Model Under Test Equivalent Model
8c7ad456321478e36d377b2a201e182fbc67b0f4	Apalache	InstanceWith	SeqTail	True	Passed	Model Under Test Equivalent Model
b0cfee773c8cca6634af8c7e3b03ff2a734d8235	Apalache	InstanceWith	SeqTail	False	Passed	Model Under Test Equivalent Model
76e5711423565978a6895d719dac1806a054a37d	Apalache	InstanceWith	SeqAppend	True	Passed	Model Under Test Equivalent Model
6d92edf5fa09eb71e0de495f9212b1ecae62c8e8	Apalache	InstanceWith	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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