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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
530b41c043c951c79b570512097a812b9fc2c875	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Instance	OneLineComment	True	Passed	Model Under Test Equivalent Model
c4565c3263b67f2c0af00b6a5895ac0eccc32663	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Instance	OneLineComment	False	Passed	Model Under Test Equivalent Model
a6e7b7ef3839acb6d778f8c6f38c05ebdf161bff	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Instance	MultiLineComment	True	Passed	Model Under Test Equivalent Model
16b09fcb3b578ea65d6e302c143a66f7c06296f2	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Instance	MultiLineComment	False	Passed	Model Under Test Equivalent Model
2295337e3de31845468f2741ad64c9c81c91e146	Apalache	Instance	BoolTrue	True	Passed	Model Under Test Equivalent Model
d59f8b30fb983751c628e2e3118bacee5a772d51	Apalache	Instance	BoolTrue	False	Passed	Model Under Test Equivalent Model
48c407c33c7a677b163bf0ef174bdc28bb9ce3d3	Apalache	Instance	BoolFalse	True	Passed	Model Under Test Equivalent Model
a81a54f4d3e2beeccf35eb66dbe2b0bc65f28788	Apalache	Instance	BoolFalse	False	Passed	Model Under Test Equivalent Model
9efe56ce06377f558af1e0500ad92c93c96954be	Apalache	Instance	BoolSet	True	Passed	Model Under Test Equivalent Model
902e95763162bf8dfa6c3112f55883e352371c23	Apalache	Instance	BoolSet	False	Passed	Model Under Test Equivalent Model
9364f95ea8bfee7b6711cd36e08f395465ae2f15	Apalache	Instance	And	True	Passed	Model Under Test Equivalent Model
27ee7659e2015386230a9d05b2a3325e9b11dc51	Apalache	Instance	And	False	Passed	Model Under Test Equivalent Model
8aa6a92ff19c2fca8f1bc9fc7b4b87691f4688a9	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Instance	AndMultiLine	True	Passed	Model Under Test Equivalent Model
bf5e20338f46cfd46ee77a31413fef32b1f25edc	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Instance	AndMultiLine	False	Passed	Model Under Test Equivalent Model
b78919fe92c258d903c1b5dea124fc9e519cf919	Apalache	Instance	Imply	True	Passed	Model Under Test Equivalent Model
822936ee097ee22d777a7ca13b6946bf5b211c1c	Apalache	Instance	Imply	False	Passed	Model Under Test Equivalent Model
95c0ef9a622fc4a90526158599fcbac5e42ddabd	Apalache	Instance	Not	True	Passed	Model Under Test Equivalent Model
7d8a8127df7ce8339ca8648190985cec1314a095	Apalache	Instance	Not	False	Passed	Model Under Test Equivalent Model
d06b570cc13c914145560b53135b68721f68a480	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Instance	Or	True	Passed	Model Under Test Equivalent Model
24fab264efb9a4ee2a4ce0a2c4451c58932b6b50	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Instance	Or	False	Passed	Model Under Test Equivalent Model
ee66ac75d25134b8da1591e933c44aa9a10fde88	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Instance	OrMultiLine	True	Passed	Model Under Test Equivalent Model
16e9cb74777c3da9ab037c7fec82ddf3c6015d26	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Instance	OrMultiLine	False	Passed	Model Under Test Equivalent Model
beb7d55386ff6e9ac9f5952a9a46c671af4df63d	Apalache	Instance	AndProp	True	Passed	Model Under Test Equivalent Model
203eaa47b920ee05a7ed11dbeaf1f6468ac7b97b	Apalache	Instance	AndProp	False	Passed	Model Under Test Equivalent Model
fd627611942b61adefde3cecbcacc97cd9d4d1a7	Apalache	Instance	Boxed	True	Passed	Model Under Test Equivalent Model
1c5fa0b2541edd2c1b3ec001fb3e5331340d4e1b	Apalache	Instance	Boxed	False	Passed	Model Under Test Equivalent Model
bceff5f7140e68afbd43ea0e874a555edc7a10f4	Apalache	Instance	Eq	True	Passed	Model Under Test Equivalent Model
cdda85df6c7e7f3db11c0c46cec6fb37ded0da42	Apalache	Instance	Eq	False	Passed	Model Under Test Equivalent Model
260f9ee108867d0227e81687f77718219678fc7d	Apalache	Instance	Ne	True	Passed	Model Under Test Equivalent Model
7c177032643250d2eaf3429ebcba0d456e74fe76	Apalache	Instance	Ne	False	Passed	Model Under Test Equivalent Model
451436f1b15cd72ed0b3e9289ed9f50d461d6d87	Apalache	Instance	Let	True	Passed	Model Under Test Equivalent Model
c029294473543fddb2bebd271ac89db54f19620f	Apalache	Instance	Let	False	Passed	Model Under Test Equivalent Model
122388c35d3e08453b4905bd970f92b0593014c6	Apalache	Instance	SetEmpty	True	Passed	Model Under Test Equivalent Model
67b2914504a928f43a6db02806e97fa40e036fe1	Apalache	Instance	SetEmpty	False	Passed	Model Under Test Equivalent Model
6a3467296e07e13d29ef9babb265919c2b7fe42f	Apalache	Instance	Set0	True	Passed	Model Under Test Equivalent Model
6ddde844cff30cee7dad1ffbc2f6d42435aaa148	Apalache	Instance	Set0	False	Passed	Model Under Test Equivalent Model
d38bcc86d842c347c92060c9709fb4a2f78e5e00	Apalache	Instance	Set1	True	Passed	Model Under Test Equivalent Model
0dd0d9f4cb949ce4bd44117f1c993a3e313737a7	Apalache	Instance	Set1	False	Passed	Model Under Test Equivalent Model
275eafa860654ab4cf8e44eec2126f3965cd6d0d	Apalache	Instance	Set2	True	Passed	Model Under Test Equivalent Model
c4924d71d3c1073598ee780584896f913bca6b1c	Apalache	Instance	Set2	False	Passed	Model Under Test Equivalent Model
0a0c86ae435fbf0ef6ee95ec5024112a6c45f47d	Apalache	Instance	Fun	True	Passed	Model Under Test Equivalent Model
422a80899440b31f66770973e7b5b8402a006605	Apalache	Instance	Fun	False	Passed	Model Under Test Equivalent Model
d9630b8fbec2e412972b6f77874857725307d242	Apalache	Instance	In	True	Passed	Model Under Test Equivalent Model
c146271feea511d59c106c6a9a1c4902bf7ddf7b	Apalache	Instance	In	False	Passed	Model Under Test Equivalent Model
b58aeb69b496faaf5c1970574660b0f4a433af88	Apalache	Instance	NotIn	True	Passed	Model Under Test Equivalent Model
773cbd220d8e716764bc21e9749990de33412a41	Apalache	Instance	NotIn	False	Passed	Model Under Test Equivalent Model
04f159752747c08d7e0727c822f63a3265c8f01c	Apalache	Instance	Exists	True	Passed	Model Under Test Equivalent Model
0f23a4d3bba8f3003d962c8c376ff4a64cd70d6e	Apalache	Instance	Exists	False	Passed	Model Under Test Equivalent Model
e8384d36c0674b00167132f50ab90907a6ae79bf	Apalache	Instance	Forall	True	Passed	Model Under Test Equivalent Model
88936f0b2ace481b6221b9952a9624c46f1efd20	Apalache	Instance	Forall	False	Passed	Model Under Test Equivalent Model
b3fb9cac7824a23bc52b88ab14a5d4a61c9c8c61	Apalache	Instance	Choose	True	Passed	Model Under Test Equivalent Model
03fe765d9c7eac17dcf7483dc7a42a6701ca63b9	Apalache	Instance	Choose	False	Passed	Model Under Test Equivalent Model
64e6ee7bf6c31016d00f64d7c4b30299541a6e7b	Apalache	Instance	Record	True	Passed	Model Under Test Equivalent Model
ae6cea83d60d19132e4397b8349304c6ce211e22	Apalache	Instance	Record	False	Passed	Model Under Test Equivalent Model
e54e40059bf1949c6e2f86983110199b6ed8c313	Apalache	Instance	Tuple	True	Passed	Model Under Test Equivalent Model
022e2891c8ed0f11d8fccc3e201e3a85be4caa88	Apalache	Instance	Tuple	False	Passed	Model Under Test Equivalent Model
ca955c468330e0ed59e12c7b67b71a05858b1b09	Apalache	Instance	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4e6893f1e1616be8d79a6029b47d06ccd707490a	Apalache	Instance	TupleEmpty	False	Passed	Model Under Test Equivalent Model
eaff91da5e11b5c8de104da3b4880b66d481f226	Apalache	Instance	FunApp	True	Passed	Model Under Test Equivalent Model
ffcde4ecaf0d200e0e6650490ad8b9d7438b04af	Apalache	Instance	FunApp	False	Passed	Model Under Test Equivalent Model
a1d9a610999004e017744cedf1c9988c024d6dc7	Apalache	Instance	Prime	True	Passed	Model Under Test Equivalent Model
9a0b3ce8f6b4e5ef0e1ef3f46d6a2009d74515b1	Apalache	Instance	Prime	False	Passed	Model Under Test Equivalent Model
4d96b3c69db5fa951ebbfc5801713df6f8c84e9b	Apalache	Instance	NumZero	True	Passed	Model Under Test Equivalent Model
58d5eaa9c81eec56e02ae653c6beef5a5dbfa6e0	Apalache	Instance	NumZero	False	Passed	Model Under Test Equivalent Model
48c6c40bbd496d5fd95654e06be112c6635fe526	Apalache	Instance	NumOne	True	Passed	Model Under Test Equivalent Model
32e70e6d0e4a776ff016292ebea803f8281c3da2	Apalache	Instance	NumOne	False	Passed	Model Under Test Equivalent Model
4f84f78e106d4086f6eca9fbdff5161b6e624936	Apalache	Instance	NumMaxInt	True	Passed	Model Under Test Equivalent Model
1aa168883e7ff0db285eb5b0d2db8d7b01ef4a3d	Apalache	Instance	NumMaxInt	False	Passed	Model Under Test Equivalent Model
ffa0cc1d7bc355db957b511ca475d2c29839141d	Apalache	Instance	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e34dd684869a8d539eda62ac9cf6853d08e62d8a	Apalache	Instance	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
031473bb4131678a8bbe8e55780ff57d2732afd5	Apalache	Instance	NumPlus	True	Passed	Model Under Test Equivalent Model
cc1c3832042d70a9ffc1f7f60194d1a358809dd7	Apalache	Instance	NumPlus	False	Passed	Model Under Test Equivalent Model
142d1d45d1abb17c2a813773fbf5d9a7d249bad3	Apalache	Instance	NumMinus	True	Passed	Model Under Test Equivalent Model
f7f136c8c6ed7fca1a7e2ae75e8de7eea65731f8	Apalache	Instance	NumMinus	False	Passed	Model Under Test Equivalent Model
091284e198b1684436a5fbb00386db6ca2dba09a	Apalache	Instance	NumMul	True	Passed	Model Under Test Equivalent Model
f45198d61b6c2cab3a3ffeb3ef629a483158e782	Apalache	Instance	NumMul	False	Passed	Model Under Test Equivalent Model
aeb3645743a394012dcc814c1879a8e54d5d6d82	Apalache	Instance	NumDiv	True	Passed	Model Under Test Equivalent Model
0ad24805fd7ba91757059733517f394b3e62a1c6	Apalache	Instance	NumDiv	False	Passed	Model Under Test Equivalent Model
083c5944592858a7f22ab8790da670070ea8607a	Apalache	Instance	NumMod	True	Passed	Model Under Test Equivalent Model
edb7a251cbe88eb88a9ac0a6c887ec12d59546da	Apalache	Instance	NumMod	False	Passed	Model Under Test Equivalent Model
7f06ae550bddb54400302f126d78e74b5067a86d	Apalache	Instance	NumPow	True	Passed	Model Under Test Equivalent Model
72f10c0623017e4a02e710a48931bf844e5ca148	Apalache	Instance	NumPow	False	Passed	Model Under Test Equivalent Model
61102584fc18f8e867b194a997ee19452fd76781	Apalache	Instance	NumGt	True	Passed	Model Under Test Equivalent Model
f62ca666fc515f37c47a2f40224fb17599ad66ca	Apalache	Instance	NumGt	False	Passed	Model Under Test Equivalent Model
fe34d5af9050ba82ee0eaf0ca59480ba74849771	Apalache	Instance	NumGe	True	Passed	Model Under Test Equivalent Model
f14f1977b8abb4739001d328da60af96baf72704	Apalache	Instance	NumGe	False	Passed	Model Under Test Equivalent Model
a680ea2612742fc6cc0de8f250849126b2289efb	Apalache	Instance	NumLt	True	Passed	Model Under Test Equivalent Model
f646957b4e2df2e61cc123564aa2493e9cda33a8	Apalache	Instance	NumLt	False	Passed	Model Under Test Equivalent Model
f256ad67cf46ad7d9e8a74f742004981a190e9ef	Apalache	Instance	NumLe	True	Passed	Model Under Test Equivalent Model
b57a4f039fb474fe2610c38b1e507b6e104d3931	Apalache	Instance	NumLe	False	Passed	Model Under Test Equivalent Model
02aa548dee7398affc5ff682b2f1c3bdaee5bc65	Apalache	Instance	DefFun	True	Passed	Model Under Test Equivalent Model
35c426480a9d884fb4a8041b6babc6cc84ea8180	Apalache	Instance	DefFun	False	Passed	Model Under Test Equivalent Model
1146bba2cb8f25cece20b6b0af0854ff32aefc94	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDefFun	True	Passed	Model Under Test Equivalent Model
164021d81a4e24baa1ce46ff4992516938ba2787	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDefFun	False	Passed	Model Under Test Equivalent Model
84a85c6123da11c1c989d246e94c22da29e6fcfc	Apalache	Instance	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
86f1824bbf2d31f530a4306a79187ad27c7c7e3d	Apalache	Instance	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
47f7c62861a150598e692760f4d32485be1ee628	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
6aa25838148b98b8f13c3b386b9341e80e2c9ba1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
884fe48fd23345eb3bae28d457a1e7414af4a87e	Apalache	Instance	Def0	True	Passed	Model Under Test Equivalent Model
18b6b46071b0a9d2dafab572c1af0d5352789783	Apalache	Instance	Def0	False	Passed	Model Under Test Equivalent Model
cde00abb4446a66f16e12f2d102294744d99baae	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef0	True	Passed	Model Under Test Equivalent Model
b12154522d052bf8787f41005f9d63688c4dfe9a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef0	False	Passed	Model Under Test Equivalent Model
70c4533f8aea963e6cfa1621e74934edcaf2dc3f	Apalache	Instance	Def1	True	Passed	Model Under Test Equivalent Model
aedae4aab3696e805b4731fd811cd6a7ebcb6028	Apalache	Instance	Def1	False	Passed	Model Under Test Equivalent Model
baf93e275fdcd9444fa6aefd2901ce312f9c0c9a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1	True	Passed	Model Under Test Equivalent Model
7b66a14838b1cc3d7572ed1bc4a274d3cbbd00a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1	False	Passed	Model Under Test Equivalent Model
5b12f80cda7d4aa88062d59f10e9645db959641c	Apalache	Instance	Def2	True	Passed	Model Under Test Equivalent Model
307ba445f804d7cd7d824622c6fa6a8aeea8cbcf	Apalache	Instance	Def2	False	Passed	Model Under Test Equivalent Model
f87d582cd829fb27856ab750ef286b4239772d53	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef2	True	Passed	Model Under Test Equivalent Model
c800cc358e23fc4c983efe9cb5914dcb2b978943	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef2	False	Passed	Model Under Test Equivalent Model
57e2c800c95177d7f3933fc9a3d5fe8a50dfdee3	Apalache	Instance	Def1Recursive	True	Passed	Model Under Test Equivalent Model
a76c313f7a4b54b2592400092997d061597d62e0	Apalache	Instance	Def1Recursive	False	Passed	Model Under Test Equivalent Model
d7fc4e1a6717cc438c49cd81e4a7dda7a90fd737	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
1d9976ae37d4dfa78d4f0bb01cb708c941662da5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
73af86021860395c8f96cbd6fc881bc24a0531d1	Apalache	Instance	Extends	True	Passed	Model Under Test Equivalent Model
2b8a0c85baf99878cab1de17842bac877be092c6	Apalache	Instance	Extends	False	Passed	Model Under Test Equivalent Model
3ae41fd48228b11701815c5e56d9cde4fe92841d	Apalache	Instance	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
19318ed6d761357925fa71ee49c79852fe3f620b	Apalache	Instance	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
dbad5d07839ec88a0c3ce8188fbcc45d9a027ef8	Apalache	Instance	Variable	True	Passed	Model Under Test Equivalent Model
9a0cf27348b3e4d2c23bc62e0743c53a9bb1fd4a	Apalache	Instance	Variable	False	Passed	Model Under Test Equivalent Model
5e643b52979b09d877d48de998d4b193c256ebfd	Apalache	Instance	Constant	True	Passed	Model Under Test Equivalent Model
0a89aca417cc1c918d3785ab6eb0e384f8cbf9ca	Apalache	Instance	Constant	False	Passed	Model Under Test Equivalent Model
50d7578199c28ac4b62993935d5525e47f094c15	Apalache	Instance	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
b9cb7fe65f5b96a1c781c71bbd57aca6004b3dda	Apalache	Instance	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
4357caa0d5ee29a7a2c02fa36f7b42fc2ce10479	Apalache	Instance	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e9cc3a09fbbf3e92ddadf3d661ac89ee33de8dfb	Apalache	Instance	ConstantRank1	False	Passed	Model Under Test Equivalent Model
af3cbb9c1babc120f62f9ba85b07ba7730cb2065	Apalache	Instance	Instance	True	Passed	Model Under Test Equivalent Model
cf9ed8d703c7d6ee8b11329a21c697470974ee81	Apalache	Instance	Instance	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
f5255dec7834d85ce7f1acc03c4adbede190c1ed	Apalache	Instance	InstanceNamed	True	Passed	Model Under Test Equivalent Model
833a99785a2b7b814eea7800bbe7c8d9c55faec0	Apalache	Instance	InstanceNamed	False	Passed	Model Under Test Equivalent Model
7ac7fba669bbf90bf6e094c4ad664092a9e42071	Apalache	Instance	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
91ecd9f9943069818924e453c493280a18f97256	Apalache	Instance	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
6696a7fd38faf14fc6650ce75078adeb37b23639	Apalache	Instance	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
a3ea98f64464e28dc8b1e67ec764a866a4a832ee	Apalache	Instance	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
727c5ff8be3bd2cf826df4ac88e80fe61d5cf7d6	Apalache	Instance	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
7109912cfe5535619d55d15ad6b7695ef7ef227b	Apalache	Instance	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
13b933f7727cff585074b9d2d7ec81874f679fa0	Apalache	Instance	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
96057f008686ceb89f9171b6a071c1c0893ca6f8	Apalache	Instance	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
7015d96abe28b4e7366273da278def5aa92c5d4f	Apalache	Instance	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
c6fb8daa095eb3153f63b0b068069e2b6291d674	Apalache	Instance	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
e2a3765897607f0a868be8e9745fcddaecd99ad8	Apalache	Instance	Enabled	True	Passed	Model Under Test Equivalent Model
e2fe61f11a149ce79d52a24823f3c14637332c70	Apalache	Instance	Enabled	False	Passed	Model Under Test Equivalent Model
24bb52eb2ac92ad02e758f209a9ed94d0cb8a8e6	Apalache	Instance	Cross2	True	Passed	Model Under Test Equivalent Model
34bd82046c6bc6b01ca4d3955ba9046416d3a353	Apalache	Instance	Cross2	False	Passed	Model Under Test Equivalent Model
30f6cc897ee95f47c644bf44d7d3009b325fd271	Apalache	Instance	Cross3	True	Passed	Model Under Test Equivalent Model
2d04aa9b79170389e73afb026634960b5a5f1174	Apalache	Instance	Cross3	False	Passed	Model Under Test Equivalent Model
ad2aec6bcde1f1c289d2b5d86a40e1d28123abf4	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))	Instance	FunSet	True	Passed	Model Under Test Equivalent Model
3f0fd760ec7fd377ebca5c8f73e8bd0d4958d2d0	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))	Instance	FunSet	False	Passed	Model Under Test Equivalent Model
86e24979ae30001643bf29584c8a10803a20d27a	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)	Instance	RecordSet	True	Passed	Model Under Test Equivalent Model
7a20bf3ba9ab56e0fafb046c5efe7ab7aa11fe90	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)	Instance	RecordSet	False	Passed	Model Under Test Equivalent Model
73260a66c8a2f5dc4d64d499ebb6cb47665f1d1a	Apalache	Instance	SetDiff	True	Passed	Model Under Test Equivalent Model
e47106dea9a680e0aa5084d49129dd8940aade93	Apalache	Instance	SetDiff	False	Passed	Model Under Test Equivalent Model
97f356e211dc0b38dfba6009a2923ca9994f9e91	Apalache	Instance	SetUnion	True	Passed	Model Under Test Equivalent Model
b658d4a6f2224c8f631f49a6fecd3aabffd6ea25	Apalache	Instance	SetUnion	False	Passed	Model Under Test Equivalent Model
67f89387d8310c0a15478f72c3d1a3c956eb3ae5	Apalache	Instance	SetIntersect	True	Passed	Model Under Test Equivalent Model
00152f6ece78e09b0784a42b8c1820e77570230b	Apalache	Instance	SetIntersect	False	Passed	Model Under Test Equivalent Model
75b7069cd90f4544db24467992cc3dfe7d758dae	Apalache	Instance	SubsetEq	True	Passed	Model Under Test Equivalent Model
5a8c25e223a6d56ca9f3245379136cd97f1b54d6	Apalache	Instance	SubsetEq	False	Passed	Model Under Test Equivalent Model
d572869da01421c0a541e368a04e1251e17ce102	Apalache	Instance	IfCond	True	Passed	Model Under Test Equivalent Model
3e28eccccaa33e6dc29a52a3c75a80cb3d231ee3	Apalache	Instance	IfCond	False	Passed	Model Under Test Equivalent Model
27c1a8532a051417a72f993617136c31117ac9fe	Apalache	Instance	IfThen	True	Passed	Model Under Test Equivalent Model
64bc6ac23bce0bf87b50b0035f07f29a73cf92c5	Apalache	Instance	IfThen	False	Passed	Model Under Test Equivalent Model
3432c0f3527f635b06fddb92c7292fb3df74b08a	Apalache	Instance	IfElse	True	Passed	Model Under Test Equivalent Model
5d85410a215cb15495beeed97761c3ef4943dfd5	Apalache	Instance	IfElse	False	Passed	Model Under Test Equivalent Model
28b8e15c811fb8a53ccc827975130cde933f15e0	Apalache	Instance	Subset	True	Passed	Model Under Test Equivalent Model
7ca71106bbbbaf830b2183ffaf2a1557b6912ab5	Apalache	Instance	Subset	False	Passed	Model Under Test Equivalent Model
3f08e7977b1579a5e0aee3cd175fdbba3ed6153f	Apalache	Instance	Domain	True	Passed	Model Under Test Equivalent Model
4dcb6a149f82e77f4a595644c187310f141ebc3c	Apalache	Instance	Domain	False	Passed	Model Under Test Equivalent Model
f14206e9f9ab218af774006a71eb94b2781fbc35	Apalache	Instance	Union	True	Passed	Model Under Test Equivalent Model
800057138936817bb00f642ae126d07ede4328ce	Apalache	Instance	Union	False	Passed	Model Under Test Equivalent Model
6c1fd42952e9f68abc14a3ee1088f0f91e65262c	Apalache	Instance	Unchanged	True	Passed	Model Under Test Equivalent Model
a8ae9fad19aac24b46665ee8870136c5542c20f6	Apalache	Instance	Unchanged	False	Passed	Model Under Test Equivalent Model
72ad127fe94b8937a1b096712d290831d5650edc	Apalache	Instance	Equivalence	True	Passed	Model Under Test Equivalent Model
c3ac457425e32a2e537ef3d65b02fe7c2867d48b	Apalache	Instance	Equivalence	False	Passed	Model Under Test Equivalent Model
95048f6df5ed05b8ae41cb40f08d3ed6fb7bc5ef	Apalache	Instance	StringEmpty	True	Passed	Model Under Test Equivalent Model
daea41845090e176c6d4137cc899c0d9601ea0f7	Apalache	Instance	StringEmpty	False	Passed	Model Under Test Equivalent Model
1dd9aebeac241e965ee6d0ff80b99e3cffb54e8a	Apalache	Instance	String	True	Passed	Model Under Test Equivalent Model
ec6d08c769f69bc30dda0224fe94c371d50da227	Apalache	Instance	String	False	Passed	Model Under Test Equivalent Model
9d3e64badf2574dd79d7c911e86267067c90ef35	Apalache	Instance	SeqLen	True	Passed	Model Under Test Equivalent Model
82477bfc218d05a72c1ab8d0033e1ce61f36df12	Apalache	Instance	SeqLen	False	Passed	Model Under Test Equivalent Model
02b2bc2653aac5053b490280b39146765593058e	Apalache	Instance	SeqConcat	True	Passed	Model Under Test Equivalent Model
90e4a75d024b79559c98f77f5dbab2d2d72c2b15	Apalache	Instance	SeqConcat	False	Passed	Model Under Test Equivalent Model
9d4e871d764c1a17572a1e227a005d33c8040a2b	Apalache	Instance	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
34767839c9846db997f675ad6a299612d2dd9984	Apalache	Instance	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
6c34c952959fc23b564edc921d28243687372428	Apalache	Instance	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
dcb0d6a218100e86b7d5c6e26fad322d9ee7f011	Apalache	Instance	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
192f8ec31453ebf46fbbe7b0264f8209ad9e83a8	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	Instance	NumRange	True	Passed	Model Under Test Equivalent Model
c7456eb0716cc21db78663a8af41e60b96db7242	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	Instance	NumRange	False	Passed	Model Under Test Equivalent Model
ebc3ccdd5d0b2db992eca50eabf6de51355f3afe	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Instance	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
c254e824f9dd99f13bd0e6b66ba232c94f6048f5	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Instance	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
8223e5d9e5a8135824a7a3b7d623cdb578b454f2	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]]	Instance	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
ffbb6c66ebfb8b96ed4e6b59cf21986d5a11ffd8	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]]	Instance	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
4ff10b349ba3338f48f634ccda09ea5c48b27b52	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Instance	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
0e80fa173ad975cbe7fb56988ddf55150dc080dd	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Instance	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
dbdb33cbd3f953c0a2e2b867d1638c4196a3433c	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Instance	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
9bdbee331362ebce31ca919ba9ac6466162e0188	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Instance	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
d4638f8c99b573c4e3e4e7a00dd94e9b194f9c18	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Instance	TlcEval	True	Passed	Model Under Test Equivalent Model
ddc4d8d3e612fca061c651b77f2985255223be9a	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Instance	TlcEval	False	Passed	Model Under Test Equivalent Model
5d7d53156524931ab57c8036fb023da29951ca34	Apalache	Instance	BagBagToSet	True	Passed	Model Under Test Equivalent Model
975ee89c81bcb34ab36b47204d3a5f1102bfb810	Apalache	Instance	BagBagToSet	False	Passed	Model Under Test Equivalent Model
edf79a3a996f58b1c0cfbb175802408861215cbf	Apalache	Instance	BagSetToBag	True	Passed	Model Under Test Equivalent Model
16a8bdbec960db45d11b6eda035885c92299f5d2	Apalache	Instance	BagSetToBag	False	Passed	Model Under Test Equivalent Model
b61a588bad8663578362385935015b4db3aa55fc	Apalache	Instance	BagBagIn	True	Passed	Model Under Test Equivalent Model
1cd9b41f454f679343cc07851a990c6b1b19e134	Apalache	Instance	BagBagIn	False	Passed	Model Under Test Equivalent Model
892429a87cf5e4b3d67536a241b09cc9d897697b	Apalache	Instance	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
6be8110eb3a3089c559d6ecd35899f8ec99b7517	Apalache	Instance	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
bbe135c47abca2e7381323d3194075be56669e6a	Apalache	Instance	BagAddBag	True	Passed	Model Under Test Equivalent Model
a29533b018b98f2b9ebfd8a767392974b5682d43	Apalache	Instance	BagAddBag	False	Passed	Model Under Test Equivalent Model
912651bf39212dc32cb87009f70a543f139ed486	Apalache	Instance	BagBagSub	True	Passed	Model Under Test Equivalent Model
8c499572b6a93b6166243aa488e0d6a5f25450ac	Apalache	Instance	BagBagSub	False	Passed	Model Under Test Equivalent Model
fb53116d3a28d1b2146222fb65bfa0291812cfd9	Apalache	Instance	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
665a20750e116452ad854746a925c147307ff099	Apalache	Instance	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f7f81158627dc6fcd03bdffd2f3b6b4bbdaeb691	Apalache	Instance	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
b94d92c40ddbc1ddbc9661ca777c7bc313395a90	Apalache	Instance	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
6f667938038e6ec84c163432e024cdb2dca4ab8e	Apalache	Instance	BagBagUnion	True	Passed	Model Under Test Equivalent Model
6de84ee0918d2b90f43017263ad9bc2545ffcd87	Apalache	Instance	BagBagUnion	False	Passed	Model Under Test Equivalent Model
e93368e62a1778829b8017d234b617eeff492728	Apalache	Instance	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
32a0714aa05f2bd10ed6073a1ee58443ee4d4266	Apalache	Instance	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
96e001da500c83b8ffdc99a9656822303548548b	Apalache	Instance	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
8e7f8c565f3efa48c035025e9d146b5f71b62290	Apalache	Instance	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
2a8306bec543f096e74cd8d60d23ec7f54b69256	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Instance	BagSubBag	True	Passed	Model Under Test Equivalent Model
109d6c4be8d12412941da434d9a5c0fd7f0b64c8	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Instance	BagSubBag	False	Passed	Model Under Test Equivalent Model
e5ef6dbdafd858f76a27f8e77b81b5cb8a2e7c3f	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)	Instance	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
340ddd92aaa8a691508c5bd10277ec5f0956456a	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)	Instance	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
2a2cc6c1cd8e830560a44777c01080433ecbc6c5	Apalache	Instance	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
19c1590b837b14fea11e51b37410e7dcbac0fe60	Apalache	Instance	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
049cbbecd732041d17fde3ed435ab1f993c50d69	Apalache	Instance	SeqHead	True	Passed	Model Under Test Equivalent Model
e463447df1eb16357fc4d196ba646fe273c72149	Apalache	Instance	SeqHead	False	Passed	Model Under Test Equivalent Model
ef311779ec41593eab15064ee3a7fd2929b88660	Apalache	Instance	SeqTail	True	Passed	Model Under Test Equivalent Model
d2fd1cc0ca2b2768b907394b943258d9bb5974cb	Apalache	Instance	SeqTail	False	Passed	Model Under Test Equivalent Model
3e5c8ba397f74a09d80567ab7a44fe466c215526	Apalache	Instance	SeqAppend	True	Passed	Model Under Test Equivalent Model
e7250b7a03989e3696a3040c3bac5b465169eb0f	Apalache	Instance	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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