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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6dc71c238045b0dc3657853615b9f059ac33233b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Eq	OneLineComment	True	Passed	Model Under Test Equivalent Model
daa7dc4e273ae25bcc513de14b5100620d181e60	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Eq	OneLineComment	False	Passed	Model Under Test Equivalent Model
897ed18e31cf060285095a29cc31d80d777dc33c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Eq	MultiLineComment	True	Passed	Model Under Test Equivalent Model
d1c7fb5470e2aa5f921ff60487335e9325fec334	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Eq	MultiLineComment	False	Passed	Model Under Test Equivalent Model
9b33484778609a0a78ef2dae93ea8780283e5604	Apalache	Eq	BoolTrue	True	Passed	Model Under Test Equivalent Model
94dc14331d9da5603c31466dffc5b4cca2094178	Apalache	Eq	BoolTrue	False	Passed	Model Under Test Equivalent Model
1433cf727e0e566bdfdca64b1b72b30a32716461	Apalache	Eq	BoolFalse	True	Passed	Model Under Test Equivalent Model
24f15a44b2df798de8c821d6fe3f677722ac1808	Apalache	Eq	BoolFalse	False	Passed	Model Under Test Equivalent Model
e323c8b2a99782aadc7866fe13f16b632fec3612	Apalache	Eq	BoolSet	True	Passed	Model Under Test Equivalent Model
5093886a35ee872a4d4a6f0bb859f764c4a6e5b0	Apalache	Eq	BoolSet	False	Passed	Model Under Test Equivalent Model
0ec84299f7fddfabfcee8fb2acc5c06f30c38b91	Apalache	Eq	And	True	Passed	Model Under Test Equivalent Model
3e7a0c3ee40e61d8477341b5d3bf29fd13b00d90	Apalache	Eq	And	False	Passed	Model Under Test Equivalent Model
4a6faac8cd68cb38f581f0f2786b1c1adb061fc7	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Eq	AndMultiLine	True	Passed	Model Under Test Equivalent Model
15635b144f4d81dddfdbe8dfbc1f4139f39ccdf6	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Eq	AndMultiLine	False	Passed	Model Under Test Equivalent Model
0ed43111accabcef96f31cbed105f8b6384be0cd	Apalache	Eq	Imply	True	Passed	Model Under Test Equivalent Model
e16f2fbff8773467f147c11badb6ca05814c26a7	Apalache	Eq	Imply	False	Passed	Model Under Test Equivalent Model
9ef3a20352e38aeb37af37ad4360a385eac25d23	Apalache	Eq	Not	True	Passed	Model Under Test Equivalent Model
0d0029507005791253d40c91b936f9e9d409c19c	Apalache	Eq	Not	False	Passed	Model Under Test Equivalent Model
7968dc53ad0b8559d6c822ccc1f42308672b3569	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Eq	Or	True	Passed	Model Under Test Equivalent Model
82c08945aee9d0657e6dd3fee5699bcdac890d5c	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Eq	Or	False	Passed	Model Under Test Equivalent Model
294a25fedab1b3def60f6c253fb54edfdabfe82a	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Eq	OrMultiLine	True	Passed	Model Under Test Equivalent Model
3c91c18fe08bc56ed64cecb1d83948202cb4a2d7	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Eq	OrMultiLine	False	Passed	Model Under Test Equivalent Model
1544af60aa50630d850f07faeb0190982b7b7124	Apalache	Eq	Eq	True	Passed	Model Under Test Equivalent Model
fded8a3b4a9b663e5287156e0c4e447089c06829	Apalache	Eq	Eq	False	Passed	Model Under Test Equivalent Model
159616899eea774ec145e8e412b7fbef1676e9d2	Apalache	Eq	Ne	True	Passed	Model Under Test Equivalent Model
fa1047c610c5e9ec868407b40b0ba34fa062dd38	Apalache	Eq	Ne	False	Passed	Model Under Test Equivalent Model
3ccc55201f881efba3b0efbf2eabc5a203bc82e9	Apalache	Eq	Let	True	Passed	Model Under Test Equivalent Model
1c0eefaa83f5c7769f47f02f7bd607c7b9fc574d	Apalache	Eq	Let	False	Passed	Model Under Test Equivalent Model
f28dad383edc1e93affb4e0947630b3e440e49ea	Apalache	Eq	SetEmpty	True	Passed	Model Under Test Equivalent Model
3cca914cd39ebfc678a7df136f94fc06c20b63f4	Apalache	Eq	SetEmpty	False	Passed	Model Under Test Equivalent Model
df8676b4148b62a371d682eaa1103c2cb1cec466	Apalache	Eq	Set0	True	Passed	Model Under Test Equivalent Model
80ac7e6c5beddd5bf14b43b87a8dfdb77dad27f7	Apalache	Eq	Set0	False	Passed	Model Under Test Equivalent Model
01ed4385a97083bac252f551ca17a0a9906e7496	Apalache	Eq	Set1	True	Passed	Model Under Test Equivalent Model
d48f6693357a7f716fc7df53407291552eec13c1	Apalache	Eq	Set1	False	Passed	Model Under Test Equivalent Model
c7aa1ffbc51a3a92153bd6f7d11f35282b7b57e8	Apalache	Eq	Set2	True	Passed	Model Under Test Equivalent Model
865fa781444739a80b044344544a1db182f8c50c	Apalache	Eq	Set2	False	Passed	Model Under Test Equivalent Model
72de2bde056cb070c7a21970143538deeddc43b5	Apalache	Eq	Fun	True	Passed	Model Under Test Equivalent Model
e76e8a3e8c69568ed8111c82e921fe4b4820fdfe	Apalache	Eq	Fun	False	Passed	Model Under Test Equivalent Model
ae87cf7c2498a847095de10fbad6d4d50cc7247e	Apalache	Eq	In	True	Passed	Model Under Test Equivalent Model
260c32951c09e042a65e3a7d68d9a2ab80e3f013	Apalache	Eq	In	False	Passed	Model Under Test Equivalent Model
ab5df77fb6e2568287b863ab2326443a4b156e05	Apalache	Eq	NotIn	True	Passed	Model Under Test Equivalent Model
78885706e30fa41d7c5919488ac36e92a65e1ec0	Apalache	Eq	NotIn	False	Passed	Model Under Test Equivalent Model
d6a8e19db585546d21b71e6c96a3676eb13291a1	Apalache	Eq	Exists	True	Passed	Model Under Test Equivalent Model
2f1227faf1e9fea2b3e9f297afb8f90620f36a73	Apalache	Eq	Exists	False	Passed	Model Under Test Equivalent Model
2c07af2ca8c5cb29424c37d33931b55e731d1431	Apalache	Eq	Forall	True	Passed	Model Under Test Equivalent Model
d2fe0d6b02bab357ad65326cdfccc5e29d524e32	Apalache	Eq	Forall	False	Passed	Model Under Test Equivalent Model
df76d22108d753e456f949716b58ba5f3b94f4bd	Apalache	Eq	Choose	True	Passed	Model Under Test Equivalent Model
a97b7668d9b0c761a3bbcd874fb14be19c4560f6	Apalache	Eq	Choose	False	Passed	Model Under Test Equivalent Model
22e9c43ba9d033366f88556260faded9d4b2a847	Apalache	Eq	Record	True	Passed	Model Under Test Equivalent Model
e4a24ad2e44fc2b1a9e947e62b2adc92cc759ba9	Apalache	Eq	Record	False	Passed	Model Under Test Equivalent Model
fc824adefe860dfe3caca66313e11a9493bd04a2	Apalache	Eq	Tuple	True	Passed	Model Under Test Equivalent Model
89d7d2d5167ba4fbb449f47480493528dcbf1715	Apalache	Eq	Tuple	False	Passed	Model Under Test Equivalent Model
3db8c45c9d7b192d7c849a7611ebbb9dbecf9775	Apalache	Eq	TupleEmpty	True	Passed	Model Under Test Equivalent Model
416f30977f6e439a0041f5bd79d68bbdfbc9a105	Apalache	Eq	TupleEmpty	False	Passed	Model Under Test Equivalent Model
d6bade8a45f80452d15f94be0501a0d23fdfdddc	Apalache	Eq	FunApp	True	Passed	Model Under Test Equivalent Model
431784ed49fca48bef28c80891b0c7cbbcc498bb	Apalache	Eq	FunApp	False	Passed	Model Under Test Equivalent Model
63600974cbb5cd4e06289882572808f550a2690a	Apalache	Eq	Prime	True	Passed	Model Under Test Equivalent Model
91af409318633e11c1baa55490cb79005226ffa6	Apalache	Eq	Prime	False	Passed	Model Under Test Equivalent Model
6bc89f8c035d41d77f5af9372809c55cdc02bbbe	Apalache	Eq	NumZero	True	Passed	Model Under Test Equivalent Model
99bd7064f26c39cfa4a88aedcbfe768222db6aed	Apalache	Eq	NumZero	False	Passed	Model Under Test Equivalent Model
a2e4f9d9e0e8f322d1ce8e7e10f2986fca6a7810	Apalache	Eq	NumOne	True	Passed	Model Under Test Equivalent Model
bfa34abdc896f7ea9744b075166688627c73a748	Apalache	Eq	NumOne	False	Passed	Model Under Test Equivalent Model
cdbe8f1c6ae66cdde9b2aab3b890a350110f00b4	Apalache	Eq	NumMaxInt	True	Passed	Model Under Test Equivalent Model
bceaecbf977d9a64f3c89c51484b7e1dc657ed16	Apalache	Eq	NumMaxInt	False	Passed	Model Under Test Equivalent Model
53c6018de4e70e63008e83dccaef467574ab5eb0	Apalache	Eq	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
075d067b3ff4b19d551122a5624cba2e7e91c678	Apalache	Eq	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
ea85a75714b02907d998ad5818526102ba5a4238	Apalache	Eq	NumPlus	True	Passed	Model Under Test Equivalent Model
1983b8f9a7e57585404f36213378778c2f4c7ce1	Apalache	Eq	NumPlus	False	Passed	Model Under Test Equivalent Model
14674c082bef6f2fe6b5d5aad1e729e74dca1358	Apalache	Eq	NumMinus	True	Passed	Model Under Test Equivalent Model
58e88970ffd2351740c3833b0b50847dd063507a	Apalache	Eq	NumMinus	False	Passed	Model Under Test Equivalent Model
09791361b11768c4b463d41d2e5bf0a91c7f0814	Apalache	Eq	NumMul	True	Passed	Model Under Test Equivalent Model
105f57f6f6e3d3ec47cbea5f494f72b29de76c73	Apalache	Eq	NumMul	False	Passed	Model Under Test Equivalent Model
32c862a2d78f9a58254b1b89e9165ba6923fd19e	Apalache	Eq	NumDiv	True	Passed	Model Under Test Equivalent Model
b3826fa6ecc8aec5641dc3c8aef4f91aa4252195	Apalache	Eq	NumDiv	False	Passed	Model Under Test Equivalent Model
6ec3b5255a459eb1cbed2afbfb2339fdc716d930	Apalache	Eq	NumMod	True	Passed	Model Under Test Equivalent Model
4debe9e5f9c105128cb4f01513ba5f9540481e41	Apalache	Eq	NumMod	False	Passed	Model Under Test Equivalent Model
260a23fe97426360aa388d6c42058d7ecb65fe36	Apalache	Eq	NumPow	True	Passed	Model Under Test Equivalent Model
c0ad36e205a59ac11ffdeb10f19a070cab00b7f4	Apalache	Eq	NumPow	False	Passed	Model Under Test Equivalent Model
cd7925380674696d526754e58d3aad63a9a04e01	Apalache	Eq	NumGt	True	Passed	Model Under Test Equivalent Model
07baff831cfda1d5a12573325e958bfc8cffaa76	Apalache	Eq	NumGt	False	Passed	Model Under Test Equivalent Model
5db78246c3945d4e5fddacf0fef7e48bd181379c	Apalache	Eq	NumGe	True	Passed	Model Under Test Equivalent Model
5466518c8ca9787dd72dbeee9553e2de1833582a	Apalache	Eq	NumGe	False	Passed	Model Under Test Equivalent Model
3beadce93403e76d4ea1eeff315bb6a3a6fe1b2b	Apalache	Eq	NumLt	True	Passed	Model Under Test Equivalent Model
b4bf76bb15fc9b89705b523bc0db82fb41287bce	Apalache	Eq	NumLt	False	Passed	Model Under Test Equivalent Model
cb91b14ec8590f9d30d1cc929b87408342bf0c6a	Apalache	Eq	NumLe	True	Passed	Model Under Test Equivalent Model
185ff3a6b7a3b4640b62f6a1c59193b9cf580245	Apalache	Eq	NumLe	False	Passed	Model Under Test Equivalent Model
ff837de03037a26bf8f212b5008abda0745ddb38	Apalache	Eq	DefFun	True	Passed	Model Under Test Equivalent Model
86da3b905b7b6c5d0d8469ece1eda1f44430272d	Apalache	Eq	DefFun	False	Passed	Model Under Test Equivalent Model
9007e4240d76d755cc90d7e4e779bf88f9845480	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDefFun	True	Passed	Model Under Test Equivalent Model
ccf7a1ef81851fac45c89894f157d75bdaabcc02	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDefFun	False	Passed	Model Under Test Equivalent Model
d54c5e8e653828dc90971b10ff892c35c3389290	Apalache	Eq	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ac6175c5351c5c620a04f082801fd7391868efc1	Apalache	Eq	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
0eed44bdb4cbdaf8131aeaf2836f7a41126ce92c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
af1933e3500007a4b058184466c959645360164f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
d2af982bc8c0d820c11c11897d2d3119b1ab76f2	Apalache	Eq	Def0	True	Passed	Model Under Test Equivalent Model
5ab18365101b48afcaddf7a61844bf4c7cd1945d	Apalache	Eq	Def0	False	Passed	Model Under Test Equivalent Model
cb18f7a10bbb44c2cdc6ba6aada9ed90ca5cc443	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef0	True	Passed	Model Under Test Equivalent Model
f612a96a763d85f1a518c850ae3ea5c85b1bc126	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef0	False	Passed	Model Under Test Equivalent Model
04b33e67b9e22a6fde28c48f489da9f79c279646	Apalache	Eq	Def1	True	Passed	Model Under Test Equivalent Model
978e2929ed83fe5f6b3189a4152c9319f49d1d04	Apalache	Eq	Def1	False	Passed	Model Under Test Equivalent Model
1205d99ab8b8a541f0a224ac417d5cb15e66cbd1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1	True	Passed	Model Under Test Equivalent Model
e6e66626c0531dadbc2e225ee56ecdbfaca3e4bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1	False	Passed	Model Under Test Equivalent Model
f7ca9deee1143895dc69528429eab2acf6c105f6	Apalache	Eq	Def2	True	Passed	Model Under Test Equivalent Model
e4aef93ffeac4ac0914392e56e5dffd7c5a93bc2	Apalache	Eq	Def2	False	Passed	Model Under Test Equivalent Model
91d17acf55d5b0b2f127d7a24ccac39c30c4e925	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef2	True	Passed	Model Under Test Equivalent Model
e92294d46bf7b5e42fdd61f509d88ff891f65557	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef2	False	Passed	Model Under Test Equivalent Model
fe2f3fffe9cb0415125a3f432ae57498cdb82994	Apalache	Eq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f8706d31d6c59361fd55e5629d863d4d52e089a6	Apalache	Eq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
fa648f4ee98cd0de590e22ccd5a174525d0fc0b2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
d4cf3a84b81d044f80ecdd83156823ec8f581ea8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
f723df95e536c3759a85cdc962b4b98149caafb4	Apalache	Eq	Extends	True	Passed	Model Under Test Equivalent Model
78cd90f2da344a66de5bd2df13554aebe6c429c3	Apalache	Eq	Extends	False	Passed	Model Under Test Equivalent Model
5058a7b4a3048a285aef1d2dc754fb08278ac5e3	Apalache	Eq	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
a89ada9742ac3b2d3ce40aa0422d347d94bba951	Apalache	Eq	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
f304f06946f7929a3c784400f9f2aa5f78a961b5	Apalache	Eq	Variable	True	Passed	Model Under Test Equivalent Model
17ee2442cc93692931bfc1d836f1aa6920707310	Apalache	Eq	Variable	False	Passed	Model Under Test Equivalent Model
8ef541073e9371ac43ee93ea8c78080463642a16	Apalache	Eq	Constant	True	Passed	Model Under Test Equivalent Model
b46d7d65b7b4a03d939f86c6eb01b3a7e57c381b	Apalache	Eq	Constant	False	Passed	Model Under Test Equivalent Model
26db2b4023bbf3ccf69b2db3b2f5ab9dc2b5114a	Apalache	Eq	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
534257e3fbe90320aa0e8092e98adfa4158eb81b	Apalache	Eq	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
68534a5d56ab699737204fc5f8b0929cb3fe2055	Apalache	Eq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
449b590ae2331729a8e948de9a08396c29d3920d	Apalache	Eq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
467714980793b40bf83689774ee1c11078c90648	Apalache	Eq	Instance	True	Passed	Model Under Test Equivalent Model
100a19eb630ccc0b302a2f9131030bfb1244bbd4	Apalache	Eq	Instance	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
045bcbc1a51d43f32d22057af5f415687f534d8d	Apalache	Eq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0eecb1ba94a8a9ca4f34c834f1bd5de3508f5cbe	Apalache	Eq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
da7f556c51ff2432d0b3f8ecb58780e3d89b1572	Apalache	Eq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a35d292ab1fd9faa51b60bb174251bf9dae5ca17	Apalache	Eq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
13e81d88d84063c2b4e44d9a41fc456a1b9148c1	Apalache	Eq	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
5399228d71bf254cb838949c959f12754571cc0d	Apalache	Eq	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
16b25bb72035b1e06c089134d54e9edbc97e91de	Apalache	Eq	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
deb683b4c4656d12c109dde2131a34593d6daf2e	Apalache	Eq	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
e6570fe675585dbe8f6aa0622f33b74b80a08b65	Apalache	Eq	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
519516d7bb5515ee4e5ce37127a7cddce6e34a48	Apalache	Eq	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
361d956656479473db2dc99dc6539fbba8c2ead2	Apalache	Eq	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
394a1f244d58180b378f0056fbf91b44372f6f4f	Apalache	Eq	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
642c976e3e9e355ac985d67464226b476983531e	Apalache	Eq	Enabled	True	Passed	Model Under Test Equivalent Model
0d6911e351e1785c9cec483220b8bed8abd16a6e	Apalache	Eq	Enabled	False	Passed	Model Under Test Equivalent Model
2bb335496f6224ca4e09e31dbcff9eab68c6da77	Apalache	Eq	Cross2	True	Passed	Model Under Test Equivalent Model
152e231066b06663a2f08177182562d308ac338b	Apalache	Eq	Cross2	False	Passed	Model Under Test Equivalent Model
69ca1f10610058c851b7fbc79138641110e399a7	Apalache	Eq	Cross3	True	Passed	Model Under Test Equivalent Model
ea7ee53880d5263d53b0896687722fba3cb90565	Apalache	Eq	Cross3	False	Passed	Model Under Test Equivalent Model
ec010c862c7e811b12ca61bf0120eed3ea94ecfa	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))	Eq	FunSet	True	Passed	Model Under Test Equivalent Model
df676af14e4dbaaf1dfc5faa907a70c2d024e4d0	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))	Eq	FunSet	False	Passed	Model Under Test Equivalent Model
18ec875dd06d22999ec14de7fcc6df066b485933	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)	Eq	RecordSet	True	Passed	Model Under Test Equivalent Model
a477c4a747bd062c524b47bfb9b8cf4a6714d21b	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)	Eq	RecordSet	False	Passed	Model Under Test Equivalent Model
f7cbfa54a703259e4377be1cea6f5e5d89e58099	Apalache	Eq	SetDiff	True	Passed	Model Under Test Equivalent Model
a56449f2d74f052b88e8292dc337b451ac386364	Apalache	Eq	SetDiff	False	Passed	Model Under Test Equivalent Model
ba90a33408be44ea7736d70e58a3be820ed5a3f6	Apalache	Eq	SetUnion	True	Passed	Model Under Test Equivalent Model
26b4a1652c3a93a38e0a4a823258bc76310d9fdb	Apalache	Eq	SetUnion	False	Passed	Model Under Test Equivalent Model
81a63d0a1f4151d765b29bb507a81dc9184993b9	Apalache	Eq	SetIntersect	True	Passed	Model Under Test Equivalent Model
e3e31586b91422608f06bc5bcaff84cea217db4d	Apalache	Eq	SetIntersect	False	Passed	Model Under Test Equivalent Model
0abba89e5e10558101e8f811ed19355ad92689dc	Apalache	Eq	SubsetEq	True	Passed	Model Under Test Equivalent Model
cc15e1de5aef65266e07a310c4f65d32f311074d	Apalache	Eq	SubsetEq	False	Passed	Model Under Test Equivalent Model
1a92bb20164455556738adf8a53909ade39bf162	Apalache	Eq	IfCond	True	Passed	Model Under Test Equivalent Model
ace5d1be65e6fb8cc3e9804ad3e3991612ec5e1e	Apalache	Eq	IfCond	False	Passed	Model Under Test Equivalent Model
36a4bdfc7d26ec3df38af516db24e025abf3eb7c	Apalache	Eq	IfThen	True	Passed	Model Under Test Equivalent Model
a553a350d872bcb4ec149775ad0b6a72df9dcac5	Apalache	Eq	IfThen	False	Passed	Model Under Test Equivalent Model
05d5859b9f395a07c1bfe2beb93a7e27e264dd87	Apalache	Eq	IfElse	True	Passed	Model Under Test Equivalent Model
f77e424630070ba41f8cd9fef1f3897375457051	Apalache	Eq	IfElse	False	Passed	Model Under Test Equivalent Model
1875ad1352b9a2952d6d3064428c0f020644a006	Apalache	Eq	Subset	True	Passed	Model Under Test Equivalent Model
3a103bd0d016c22a5358f6c62dfd4b7c5caf3589	Apalache	Eq	Subset	False	Passed	Model Under Test Equivalent Model
28c14286d7863ef45f383b5631f6b8c7a3bcec13	Apalache	Eq	Domain	True	Passed	Model Under Test Equivalent Model
2a419ba84623bb9640c6e62d94e679620961a0be	Apalache	Eq	Domain	False	Passed	Model Under Test Equivalent Model
46fd0ad9377f527e9d15c4186fd8983b983e5e33	Apalache	Eq	Union	True	Passed	Model Under Test Equivalent Model
317a0bf37689164aad0393f6f95284b3911506b0	Apalache	Eq	Union	False	Passed	Model Under Test Equivalent Model
d7299d457d2fe786d4d11083f22ee50a107243af	Apalache	Eq	Unchanged	True	Passed	Model Under Test Equivalent Model
9f4b4cdfd50b572803f52300f1af2e4bf46170d2	Apalache	Eq	Unchanged	False	Passed	Model Under Test Equivalent Model
97ba1e97f818a8b175dad45972c094488c3ba872	Apalache	Eq	Equivalence	True	Passed	Model Under Test Equivalent Model
e273b13dad17bed1aa5705707640126be4d8ceab	Apalache	Eq	Equivalence	False	Passed	Model Under Test Equivalent Model
b5efa75fb72adc55ec45be3982174ea225920f7a	Apalache	Eq	StringEmpty	True	Passed	Model Under Test Equivalent Model
1ad9d1dfb1264e58b85b22309012c1037941c18a	Apalache	Eq	StringEmpty	False	Passed	Model Under Test Equivalent Model
20fa84c7f6043f643932fd03beb9f8adbdbea3f3	Apalache	Eq	String	True	Passed	Model Under Test Equivalent Model
452d7e1c1cca6037731cfe9334305336ec743fde	Apalache	Eq	String	False	Passed	Model Under Test Equivalent Model
bd3e98798a0fff4e8e75e24995e45df809bf4512	Apalache	Eq	SeqLen	True	Passed	Model Under Test Equivalent Model
a882d822aa2e6f8740f5e68c31fed02efa72597d	Apalache	Eq	SeqLen	False	Passed	Model Under Test Equivalent Model
a4fa2167cb1fae3759135f7fec206820d9f5c5e4	Apalache	Eq	SeqConcat	True	Passed	Model Under Test Equivalent Model
5dc2e1706042e4f8be8e08e16fd2d749011208b0	Apalache	Eq	SeqConcat	False	Passed	Model Under Test Equivalent Model
d2264019d545a58a8e329e8c95cbe31a9bd452c2	Apalache	Eq	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
036395d9a932a162f931801bf3e53fb5dfc92b6e	Apalache	Eq	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
87d7ad80cc295cd0433ff8c2254f14fbb3c18833	Apalache	Eq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
7e7bf8ee5cce63f7d36e275ec0a691a818b7fee4	Apalache	Eq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b6a08ddda604e93b216a9cd6dce04e475f9654c2	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	Eq	NumRange	True	Passed	Model Under Test Equivalent Model
6aa387872ef6457b701d4c0e5cafc83a9da14d58	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	Eq	NumRange	False	Passed	Model Under Test Equivalent Model
7e4192e3f823349c4d985587eedd01cf11279b25	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Eq	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
4fd361cc27e752705cac924c47314105b9a86e3f	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Eq	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
30ce6ef0b28d9d8c79d764a14954df79602445a3	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]]	Eq	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
96ee10027f0a2651d91b2bf46eadc7957413f6a0	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]]	Eq	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
aca48e45d87cf75011fc82fa38fe24636e885d8d	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Eq	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
f6ffa8aa0bae12d3ab99db2736bc26fc0edb83b3	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Eq	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
08071da95ac6b7094f601b95481bb8f9a2cd1227	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Eq	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
981212db543634f51de8d5dfe8cc32889373a2e8	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Eq	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
4d7fe267a3a5fd8c8df5099bc9a54695f6951ca6	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Eq	TlcEval	True	Passed	Model Under Test Equivalent Model
747a4be5915961bd911fecb92ef54d354db18fb3	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Eq	TlcEval	False	Passed	Model Under Test Equivalent Model
72a3ddfb48cd7b57d0c2915e9764747360f29fbf	Apalache	Eq	BagBagToSet	True	Passed	Model Under Test Equivalent Model
0401badf294c9f38ddedf19c52b18778d5e1aeaf	Apalache	Eq	BagBagToSet	False	Passed	Model Under Test Equivalent Model
65cd704c85b0c0d873d223ca43caf6120a4a7740	Apalache	Eq	BagSetToBag	True	Passed	Model Under Test Equivalent Model
9ee8df4fe7dc1d5c2c7fe800a50264f8fddef1f0	Apalache	Eq	BagSetToBag	False	Passed	Model Under Test Equivalent Model
180879fe8d10cfbeaf710c87c0550965644e815b	Apalache	Eq	BagBagIn	True	Passed	Model Under Test Equivalent Model
42f3de3dd8e5b3f85bdd54b3df7bf7b7135861d4	Apalache	Eq	BagBagIn	False	Passed	Model Under Test Equivalent Model
155f70e395b3ce8b526ff797aeacd273f12b731c	Apalache	Eq	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
b6f7e576256230d4cacd0f528328a925e7e8e5ea	Apalache	Eq	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
b3c57f522af3095a0aa277488f4433f5faf43bba	Apalache	Eq	BagAddBag	True	Passed	Model Under Test Equivalent Model
6475e2f78eac85fd0150e5920f7569dfb1282495	Apalache	Eq	BagAddBag	False	Passed	Model Under Test Equivalent Model
e49446460fd7c9deff05afd65340834998d09572	Apalache	Eq	BagBagSub	True	Passed	Model Under Test Equivalent Model
de1d648b9eced0db6b2aaa02af8aeeae8f3ceee3	Apalache	Eq	BagBagSub	False	Passed	Model Under Test Equivalent Model
e1425f3fa0f71ae3499af100fe43bd7f10ee1d1f	Apalache	Eq	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
ef72445567d59f1721435b76621c1c115d1b9e81	Apalache	Eq	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
513b7ed6ce6891bad180df53ca7208b3896dd0e0	Apalache	Eq	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
698cf305ef0d3cbd2b1b21f6968be203995046ed	Apalache	Eq	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
3e7adadcaf9a4e2af5e8b511a9fb219868f90159	Apalache	Eq	BagBagUnion	True	Passed	Model Under Test Equivalent Model
0cced50e6052405e0ff65b81c61f052659259e4f	Apalache	Eq	BagBagUnion	False	Passed	Model Under Test Equivalent Model
421d7ef2247747f6fa1597a872e1b320a6571aec	Apalache	Eq	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
d727f8d352e46a01545bfd139593af26421b935f	Apalache	Eq	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
36e4807aae9e3f3e7a45849806f736d7ec23170d	Apalache	Eq	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b5d4a242ee4dd096380d4e8c7b352fac177c221c	Apalache	Eq	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
68a53ec436bfc1123f438d843a5b6eb9e8f3f02b	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Eq	BagSubBag	True	Passed	Model Under Test Equivalent Model
9144cff674efdc7cc04d68c5d62293364fae646d	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Eq	BagSubBag	False	Passed	Model Under Test Equivalent Model
a7e60bec7d4b50580a3e5edae6c21d3eccbf843f	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)	Eq	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
c4f8f3fac9969b0a71626e1632b449f819c76787	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)	Eq	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
d39891b7b0ca63838bcb128fbf84c00ef30c9388	Apalache	Eq	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
75add522955ca3b00eaeb21f5e48589ca5a88105	Apalache	Eq	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
d4d119843a6e27001e2f01fef854b01ffc4a77ab	Apalache	Eq	SeqHead	True	Passed	Model Under Test Equivalent Model
92542d1eb208311198b8025f1fffc390c48a6f53	Apalache	Eq	SeqHead	False	Passed	Model Under Test Equivalent Model
f4520e56f9fae6f02ff8978fece2961c9c5054b5	Apalache	Eq	SeqTail	True	Passed	Model Under Test Equivalent Model
e0df7913a45914e27fe1d695a62ec3df96bc805d	Apalache	Eq	SeqTail	False	Passed	Model Under Test Equivalent Model
638aa6ef91772a2eb217d54a38c1f71519499738	Apalache	Eq	SeqAppend	True	Passed	Model Under Test Equivalent Model
26c346784ddf4fd30a62d9d8bf4ba1d4f859e81f	Apalache	Eq	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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