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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
2a75d19dc0ef18765aeabfb7b8746bb421d34cfe	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set0	OneLineComment	True	Passed	Model Under Test Equivalent Model
546bdae216de27623a6879f9db8449a5c58ebbb5	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set0	OneLineComment	False	Passed	Model Under Test Equivalent Model
dc9f2b08167dd6a88736d9dc41925224156dee97	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set0	MultiLineComment	True	Passed	Model Under Test Equivalent Model
5f7b3d086ead1edd71fafa250bb33ee3449e059c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set0	MultiLineComment	False	Passed	Model Under Test Equivalent Model
3fea1e63913d156d3c02b58e59f895ff08c93d26	Apalache	Set0	BoolTrue	True	Passed	Model Under Test Equivalent Model
ea828b9a8a2a0670b6c39fba3cc573af44823780	Apalache	Set0	BoolTrue	False	Passed	Model Under Test Equivalent Model
6a8a731387a90c014efbbc0f72cd0c9dc485d7fb	Apalache	Set0	BoolFalse	True	Passed	Model Under Test Equivalent Model
223582b991e35721bbd09df58c58cfcceebfcfe9	Apalache	Set0	BoolFalse	False	Passed	Model Under Test Equivalent Model
1b0bf38e95b37505c4b33c424016e692c1148fad	Apalache	Set0	BoolSet	True	Passed	Model Under Test Equivalent Model
c3ff5d5b9a40124679ad6319ecf106f50d4f4aa0	Apalache	Set0	BoolSet	False	Passed	Model Under Test Equivalent Model
5aaa4a3ade9f8b2d4907cfa9161f3239fb5976fd	Apalache	Set0	And	True	Passed	Model Under Test Equivalent Model
03d542f84f353571b4a37ece8753addc933b9c3c	Apalache	Set0	And	False	Passed	Model Under Test Equivalent Model
3824a891d4f104c4031d7e4dd2aa83b7ba15b53f	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set0	AndMultiLine	True	Passed	Model Under Test Equivalent Model
4822be4379631319f18e361b1b8136d8de0d8e45	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set0	AndMultiLine	False	Passed	Model Under Test Equivalent Model
974726411a029c85628d232bdf66e4050d383f5f	Apalache	Set0	Imply	True	Passed	Model Under Test Equivalent Model
4a9cdb852577c041e8989ad6f2846d10707de65d	Apalache	Set0	Imply	False	Passed	Model Under Test Equivalent Model
f9b6889d0f93c692c862a0aa471253c712f911dc	Apalache	Set0	Not	True	Passed	Model Under Test Equivalent Model
61989fb6ae65577da5e525df4fd044abe5eb53e5	Apalache	Set0	Not	False	Passed	Model Under Test Equivalent Model
5590cd02d14a055ffcada939640321f20281f964	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set0	Or	True	Passed	Model Under Test Equivalent Model
5dc2445080ca3b1b36bc357c2ba63f4698117b12	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set0	Or	False	Passed	Model Under Test Equivalent Model
3ce507b577376c5db1d9d0478d5af151570517aa	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set0	OrMultiLine	True	Passed	Model Under Test Equivalent Model
c21395c84c0d3f9b7a07b2458ab24828baeab647	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set0	OrMultiLine	False	Passed	Model Under Test Equivalent Model
8be88f8a832e4b494790fac1ceda01781748751e	Apalache	Set0	Eq	True	Passed	Model Under Test Equivalent Model
2a1cfbb316fd79367f8954142e6c79781e564331	Apalache	Set0	Eq	False	Passed	Model Under Test Equivalent Model
cf790474d72d04bb7023fb2c40f2ef8a87b7d219	Apalache	Set0	Ne	True	Passed	Model Under Test Equivalent Model
9106e59ba344d28e8858708b4ba20257a1dcb9c6	Apalache	Set0	Ne	False	Passed	Model Under Test Equivalent Model
c907133d532a08027e4dc85c6c48f3517fc3ffe2	Apalache	Set0	Let	True	Passed	Model Under Test Equivalent Model
2091701479cfc47fe9b2800590fdbb98471ac477	Apalache	Set0	Let	False	Passed	Model Under Test Equivalent Model
fc1663c544eb16df514919ace9baefda83dec23d	Apalache	Set0	SetEmpty	True	Passed	Model Under Test Equivalent Model
bfebbac5b90d2f307a24fefdef3d406fc45bad38	Apalache	Set0	SetEmpty	False	Passed	Model Under Test Equivalent Model
114a7aef3f2619e6d3f6559c225bc16771bdb870	Apalache	Set0	Set0	True	Passed	Model Under Test Equivalent Model
962b5fd24388c100f1258ef545038ba8a77a0bc8	Apalache	Set0	Set0	False	Passed	Model Under Test Equivalent Model
6b1e4a526251991016fb6e38e9824defc7a99cff	Apalache	Set0	Set1	True	Passed	Model Under Test Equivalent Model
4f0ab6230a54595f041b4074953f84c07146a939	Apalache	Set0	Set1	False	Passed	Model Under Test Equivalent Model
402c3eaf82f1221421935f164a868f9a0c09202a	Apalache	Set0	Set2	True	Passed	Model Under Test Equivalent Model
ea977177471455ad26781c7fa0d0426b8e64efe3	Apalache	Set0	Set2	False	Passed	Model Under Test Equivalent Model
dd6101838d1e5d1c6fb8100bf5baa5ac3ef7a7ad	Apalache	Set0	Fun	True	Passed	Model Under Test Equivalent Model
95d295ffd651922c26a1ee7d81366afd48425819	Apalache	Set0	Fun	False	Passed	Model Under Test Equivalent Model
0c75d253f0230c2bd0aa1535a09457778a3d8230	Apalache	Set0	In	True	Passed	Model Under Test Equivalent Model
8145565c6c4fe5f1b8314ca0f0c52a7e45601285	Apalache	Set0	In	False	Passed	Model Under Test Equivalent Model
e340854c97f8489faadf2c0427594b2b873a4d19	Apalache	Set0	NotIn	True	Passed	Model Under Test Equivalent Model
8e107f584b693852bea97de22f692796775dd119	Apalache	Set0	NotIn	False	Passed	Model Under Test Equivalent Model
b685357743842335043cea92d0868e0baecfc233	Apalache	Set0	Exists	True	Passed	Model Under Test Equivalent Model
b1b8930b99b5f7117f74106708913a06cdecef4a	Apalache	Set0	Exists	False	Passed	Model Under Test Equivalent Model
81e76652a4bef1155986b8bfdb51e77a0f5c477a	Apalache	Set0	Forall	True	Passed	Model Under Test Equivalent Model
5e696be424ee288558976865443cc1b27367d1b3	Apalache	Set0	Forall	False	Passed	Model Under Test Equivalent Model
57903e67391b59b60ea91a2f6f831f4069d92d9c	Apalache	Set0	Choose	True	Passed	Model Under Test Equivalent Model
c00a14d811ca8aef94c425d2de82bf0e48b51749	Apalache	Set0	Choose	False	Passed	Model Under Test Equivalent Model
eaeeec4f1b66721a2aaf39c3c83081ed317cb061	Apalache	Set0	Record	True	Passed	Model Under Test Equivalent Model
8be82c045d3f2a88fee7d3efdf16ba1ec83fd4b2	Apalache	Set0	Record	False	Passed	Model Under Test Equivalent Model
b8e563a860af138b970ff136a52d41d3c9947ae3	Apalache	Set0	Tuple	True	Passed	Model Under Test Equivalent Model
da48a085f7e32f9f02a8f3ffba3cf28c4ccb4710	Apalache	Set0	Tuple	False	Passed	Model Under Test Equivalent Model
04c17e8e6fe23e008726c1f1a138b2c99c061762	Apalache	Set0	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d22e31d8a26163360beaba40c15e41e22ccbe605	Apalache	Set0	TupleEmpty	False	Passed	Model Under Test Equivalent Model
e3e4395aec1cfc495133a60b613b93898c5cd965	Apalache	Set0	FunApp	True	Passed	Model Under Test Equivalent Model
c81026f1a282e5f06661838f32b9ca6e69951bcf	Apalache	Set0	FunApp	False	Passed	Model Under Test Equivalent Model
744d62474fa1aea30d06e0571f94efd9451b7158	Apalache	Set0	Prime	True	Passed	Model Under Test Equivalent Model
484602886fdab596252b41868959306da6e4ca4f	Apalache	Set0	Prime	False	Passed	Model Under Test Equivalent Model
15ef555f15f184dd49e5092ee825f143fa6aa19e	Apalache	Set0	NumZero	True	Passed	Model Under Test Equivalent Model
9822fa94aa959ece11bc1bcb30711fbdf285283c	Apalache	Set0	NumZero	False	Passed	Model Under Test Equivalent Model
24273c722543e0436ff0449826749f410ffa6415	Apalache	Set0	NumOne	True	Passed	Model Under Test Equivalent Model
65730c94f354fc6130bfc5da7980f977b004da13	Apalache	Set0	NumOne	False	Passed	Model Under Test Equivalent Model
df73aba831a2ffbe3b30b5ff53e7b4eed2d8dbbc	Apalache	Set0	NumMaxInt	True	Passed	Model Under Test Equivalent Model
976c3e554aeacdde82010a03919fcc09fe10d2e3	Apalache	Set0	NumMaxInt	False	Passed	Model Under Test Equivalent Model
3a91d86f30267c84cae30143105a175df2ade8d0	Apalache	Set0	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5fa3b7f600ddebce2a1b4c183802f3fb5358aa72	Apalache	Set0	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
1a2740f26dc14e8331a15c472b54add4efba2a4c	Apalache	Set0	NumPlus	True	Passed	Model Under Test Equivalent Model
8adc4dce77512286969ee636eb6ef19f23cf0dd1	Apalache	Set0	NumPlus	False	Passed	Model Under Test Equivalent Model
9cabf640d93535a2d8ce12308948fac6c694c453	Apalache	Set0	NumMinus	True	Passed	Model Under Test Equivalent Model
6626ec8c649b248de16b6b6fe4c404c0c0dadcae	Apalache	Set0	NumMinus	False	Passed	Model Under Test Equivalent Model
5e43d6a65a967489da8327a3f773c1b95bec3474	Apalache	Set0	NumMul	True	Passed	Model Under Test Equivalent Model
8943b5765827bfa84aac6f5acd9c0c3fb427f3e6	Apalache	Set0	NumMul	False	Passed	Model Under Test Equivalent Model
a5eb16aa60c35830145f9fa90c3704dd2fb3c9d2	Apalache	Set0	NumDiv	True	Passed	Model Under Test Equivalent Model
64784fc6bda8b64c27b837b695f7c572d33b5f90	Apalache	Set0	NumDiv	False	Passed	Model Under Test Equivalent Model
c753825e8e4c09965cbdffa9847d8e88950a3810	Apalache	Set0	NumMod	True	Passed	Model Under Test Equivalent Model
d299417aa9b51c984b50bea2e3b4984eb61f4851	Apalache	Set0	NumMod	False	Passed	Model Under Test Equivalent Model
01c1a153322ac5db02ee8fc178c346434acbe0b1	Apalache	Set0	NumPow	True	Passed	Model Under Test Equivalent Model
18643fe48e0fde598eaf4803d235a3554e21691a	Apalache	Set0	NumPow	False	Passed	Model Under Test Equivalent Model
6641e96b9e42f9edbc9a4f3a95af42aa3914ab5d	Apalache	Set0	NumGt	True	Passed	Model Under Test Equivalent Model
dfd7c61d97dba61758aeab4f25164ec2fd157393	Apalache	Set0	NumGt	False	Passed	Model Under Test Equivalent Model
3a31565e0cf1e27b566a8963995c86b97db8ee96	Apalache	Set0	NumGe	True	Passed	Model Under Test Equivalent Model
bf3ced58835a81cf2be84cf601c5e938db6c5a16	Apalache	Set0	NumGe	False	Passed	Model Under Test Equivalent Model
e578cbe4aa33d56439df95625a0a855206776a06	Apalache	Set0	NumLt	True	Passed	Model Under Test Equivalent Model
4c3da86a660970c2b069ce8d0f627554fab1d0d9	Apalache	Set0	NumLt	False	Passed	Model Under Test Equivalent Model
2e02dcef5539fcd9fdfc433e67c969b61d25932c	Apalache	Set0	NumLe	True	Passed	Model Under Test Equivalent Model
8041755549c8d70b62133f55dbf3f7eacdcf7ce5	Apalache	Set0	NumLe	False	Passed	Model Under Test Equivalent Model
acd7fd01a0eeb93f14760c2715ae3a974618fa8e	Apalache	Set0	DefFun	True	Passed	Model Under Test Equivalent Model
0c9db84a8c8ba08a575f8ecd448a28124a810a89	Apalache	Set0	DefFun	False	Passed	Model Under Test Equivalent Model
9d1ea7b8dce5ab440671ed06886b19eeda6221a3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDefFun	True	Passed	Model Under Test Equivalent Model
895cf5335bae48011e2b846b5f36c03732548ee9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDefFun	False	Passed	Model Under Test Equivalent Model
4dc600eb1dbf5ef9d98fa05c4bdb26885c6b4bfa	Apalache	Set0	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
882aabb13c0c90b407a6b9e6864b6862913dcc10	Apalache	Set0	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
dfe2abe1b0340b145545e3caa86ef7800c50cbe9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
4f06603ada3f90adea1085e650479b1c15d3ff84	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
5b84ab34ee0894f3f816ce3bd3181ecd1ff62f25	Apalache	Set0	Def0	True	Passed	Model Under Test Equivalent Model
629141aa041e31c3cc314d1c4538791a225eaf23	Apalache	Set0	Def0	False	Passed	Model Under Test Equivalent Model
45468fdfed6b98b96055a5be454ba816762cad49	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef0	True	Passed	Model Under Test Equivalent Model
62071e37121b865eef32bb23d0ac3a4542522664	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef0	False	Passed	Model Under Test Equivalent Model
36eb50ea2b85e33b161793fdc4a3b636b6dcd215	Apalache	Set0	Def1	True	Passed	Model Under Test Equivalent Model
956ffc61d40820c844c8b07e57d4eb40b7d54940	Apalache	Set0	Def1	False	Passed	Model Under Test Equivalent Model
31ec59b8f4c906c4058b6919f8fd23d21051e355	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1	True	Passed	Model Under Test Equivalent Model
08290c5068ef2902a68ac2a526386c558c329c04	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1	False	Passed	Model Under Test Equivalent Model
d95765a8db80243da51105083e87e19a0f37a595	Apalache	Set0	Def2	True	Passed	Model Under Test Equivalent Model
12fc8aa7a896f6f9b52381c674089f38c05af8d4	Apalache	Set0	Def2	False	Passed	Model Under Test Equivalent Model
53767fede3cb7026371bafbf5f8e18ce3540cab3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef2	True	Passed	Model Under Test Equivalent Model
6e7322b33656f90b87ac6ae4349fa9589ebe2eaf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef2	False	Passed	Model Under Test Equivalent Model
a35935b230447432d1fcfe3522ce9b8e3aecb0dd	Apalache	Set0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3c70daf1567cf8b51e9e2b6c5096ddedcb0c416a	Apalache	Set0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
bd358ecf70a2dce3ebb1649a76ccbac0f8464049	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
9101ad73eb98b1030d991cbf5189f753f7d978f7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
f299d375df6795e7106e63e57a9c5f8bf7028e49	Apalache	Set0	Extends	True	Passed	Model Under Test Equivalent Model
6b979661cc2f97009360049b04c35f125081bad2	Apalache	Set0	Extends	False	Passed	Model Under Test Equivalent Model
130b7a796f1e9f53d87400ee86391494ed7614ed	Apalache	Set0	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
9dc559b6da601079dd0abdce7435a1eb7e2d6d40	Apalache	Set0	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
464e80f4ee99c08f00abb9f377561f8fc54fec75	Apalache	Set0	Variable	True	Passed	Model Under Test Equivalent Model
44f63926131902138838a9bee46f87a992a9caa7	Apalache	Set0	Variable	False	Passed	Model Under Test Equivalent Model
1bdd74791f67fa5f1ec498b82851beda6b8b0fd2	Apalache	Set0	Constant	True	Passed	Model Under Test Equivalent Model
c850ee40575f6fd44ed86c8155f764e7fe2aca3d	Apalache	Set0	Constant	False	Passed	Model Under Test Equivalent Model
f23a080b0ee169f7b905ea5b0dd4475fed479d95	Apalache	Set0	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
d9846276c6586430edbeba1d5f706cda046c07b2	Apalache	Set0	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
dbc861e1e3dd71a2945f9cd4c940741110810d51	Apalache	Set0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
0d74f7c5c26b51f1e9bad6d8a52de6a337f5fc8d	Apalache	Set0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9f290ce27cc9f8bc89369e3838d6dd6755a61340	Apalache	Set0	Instance	True	Passed	Model Under Test Equivalent Model
72abfee38998ef9175c2d4f4a87ac1bd6c300647	Apalache	Set0	Instance	False	Passed	Model Under Test Equivalent Model
888c3b50fc397818071fca241331b3fa4671cee6	Apalache	Set0	InstanceWith	True	Passed	Model Under Test Equivalent Model
b5b32006f2869b2685f2e7e68b7903c7a82acedd	Apalache	Set0	InstanceWith	False	Passed	Model Under Test Equivalent Model
3818e79663731b4d047adcd76a29503b723fb1ca	Apalache	Set0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8ed54246892be586ce44380cebd716e798566337	Apalache	Set0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
e0c1479c4d58b7a9420340b2b50a379b6c15393b	Apalache	Set0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c60df8df490b01e1ed447d8d288325960112d9f3	Apalache	Set0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
1c97f35a59f4489dacdb384597c69bc9dad68695	Apalache	Set0	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
983695a3fdab57fbbb4e59daa6e27e629f8b93e0	Apalache	Set0	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
01dd27251c59b83acec672934fc3fca73c34b43d	Apalache	Set0	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
8a31607dfaa337e8f006a16d4da88f2b4a9372ea	Apalache	Set0	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
6e5752f58543bd754d6f9463ed233565a520cb20	Apalache	Set0	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
94f6330d12423d9ff08b5037e1df6e6250576675	Apalache	Set0	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
d799035ffde5aff0d4e24d1266506cbba7311146	Apalache	Set0	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
0d13bc8f96f213b52cf633b4077a953556effed2	Apalache	Set0	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
638709aca5c1f12df5f4e82a18d8e65df4499fe1	Apalache	Set0	Enabled	True	Passed	Model Under Test Equivalent Model
e2ad43367bc91f772aba59834a2da850e3eadcf2	Apalache	Set0	Enabled	False	Passed	Model Under Test Equivalent Model
9f550f24499d2ed1754fe335de7103b137cc20fc	Apalache	Set0	Cross2	True	Passed	Model Under Test Equivalent Model
aa7f3056b901b45d7a0e25f85cbf8f12e5744cdd	Apalache	Set0	Cross2	False	Passed	Model Under Test Equivalent Model
2b87b4643810c9e6e0a74d814139da0c432fcc3d	Apalache	Set0	Cross3	True	Passed	Model Under Test Equivalent Model
9515fe99d00cec87078062edb5ee101def748202	Apalache	Set0	Cross3	False	Passed	Model Under Test Equivalent Model
124bf344ebd3b0643be04ed8681dfebcaed69da0	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))	Set0	FunSet	True	Passed	Model Under Test Equivalent Model
bd80928604054486a305843641ad7c12fec48671	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))	Set0	FunSet	False	Passed	Model Under Test Equivalent Model
9aafae2107f57479d4adf06c404082f0ee7d9efc	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)	Set0	RecordSet	True	Passed	Model Under Test Equivalent Model
c4ff4f894d8d55c3b06c1661415528a0c25dd397	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)	Set0	RecordSet	False	Passed	Model Under Test Equivalent Model
29166a472054aaeb7ba3a4722b323b5fa5617eeb	Apalache	Set0	SetDiff	True	Passed	Model Under Test Equivalent Model
3e06953c8f19a527393303ab791f3f5613518968	Apalache	Set0	SetDiff	False	Passed	Model Under Test Equivalent Model
ce11141db2857f5330526855cf522a75edd76728	Apalache	Set0	SetUnion	True	Passed	Model Under Test Equivalent Model
a00b491a71ef47b10998ce69377604d34946e641	Apalache	Set0	SetUnion	False	Passed	Model Under Test Equivalent Model
a4ac1f50bbaaec1571fa045527da333e11459760	Apalache	Set0	SetIntersect	True	Passed	Model Under Test Equivalent Model
a16209419f85ae6f7eccc29834e8c6b0d4eedbb8	Apalache	Set0	SetIntersect	False	Passed	Model Under Test Equivalent Model
97aa34fd492dd0514b6239ba9555225b43efa27f	Apalache	Set0	SubsetEq	True	Passed	Model Under Test Equivalent Model
c591d6e9fdfeb24dd7fce0f5de3c066a65c8fef8	Apalache	Set0	SubsetEq	False	Passed	Model Under Test Equivalent Model
e5c3a6cdcf6319659d82ca90140ff0fc496b043c	Apalache	Set0	IfCond	True	Passed	Model Under Test Equivalent Model
e7304e5a050014edb85863e2c07970372db72f4f	Apalache	Set0	IfCond	False	Passed	Model Under Test Equivalent Model
76bbbe502a970fa526833ec658d12433139f96fd	Apalache	Set0	IfThen	True	Passed	Model Under Test Equivalent Model
1d95054241c9267de36e2dc7cceed7ad1ea9cc1a	Apalache	Set0	IfThen	False	Passed	Model Under Test Equivalent Model
9e3db955e990c3c3a16e15474a33de4f6c1dabde	Apalache	Set0	IfElse	True	Passed	Model Under Test Equivalent Model
763b4372acded9e33e4bcac91a77f4a4878f52eb	Apalache	Set0	IfElse	False	Passed	Model Under Test Equivalent Model
2e819c6ebd512f4459776e7015f81372eb04a2ac	Apalache	Set0	Subset	True	Passed	Model Under Test Equivalent Model
aef2e0fafdddd096941b430c154d9f7315f5f12e	Apalache	Set0	Subset	False	Passed	Model Under Test Equivalent Model
d0192b3b4b2927c474fb50e211bd8a1b1dfa371c	Apalache	Set0	Domain	True	Passed	Model Under Test Equivalent Model
df65ef845020bd9da7a8d51fa860c7d745dc121f	Apalache	Set0	Domain	False	Passed	Model Under Test Equivalent Model
62888f98e69ee8fc9542568beb084d00dab3e9ce	Apalache	Set0	Union	True	Passed	Model Under Test Equivalent Model
e2cbe1566bbf3b32ed747a9b98bfc1fed4177d42	Apalache	Set0	Union	False	Passed	Model Under Test Equivalent Model
cea96c30d6a302ebea4a12be0d4181ced7573a05	Apalache	Set0	Unchanged	True	Passed	Model Under Test Equivalent Model
84d08675b51acfedc14f5916dbaf8e9ab7b6ca2f	Apalache	Set0	Unchanged	False	Passed	Model Under Test Equivalent Model
665fcd55daadaecf66dd2511ae59b2cb64648c99	Apalache	Set0	Equivalence	True	Passed	Model Under Test Equivalent Model
c8662f3ddfddd82f4c34288e65e15157fc7fc45f	Apalache	Set0	Equivalence	False	Passed	Model Under Test Equivalent Model
28038315e91d14b841a47af71fe00a5ff2f5e145	Apalache	Set0	StringEmpty	True	Passed	Model Under Test Equivalent Model
5e5f72f734c9abba12d77d5ce33a6896b6cb3f6b	Apalache	Set0	StringEmpty	False	Passed	Model Under Test Equivalent Model
340e231df507d2e7c0abc2b8b76d62fcfc9e6bb0	Apalache	Set0	String	True	Passed	Model Under Test Equivalent Model
d80571b51c90e25c64c197613ee09af8d30b315f	Apalache	Set0	String	False	Passed	Model Under Test Equivalent Model
99eaada77545876aa977173c51fb836d780f7dcc	Apalache	Set0	SeqLen	True	Passed	Model Under Test Equivalent Model
9c1bb3ab10af1b767227069fc5680f45710c389f	Apalache	Set0	SeqLen	False	Passed	Model Under Test Equivalent Model
f9a2085ac3d218de371c34cdfdf03e2d7f8317c8	Apalache	Set0	SeqConcat	True	Passed	Model Under Test Equivalent Model
808fa026a4a2791baa94707dc8fbb0b577e387e7	Apalache	Set0	SeqConcat	False	Passed	Model Under Test Equivalent Model
9c59e90ccae8e4973f8f3f30d3586cae2b1b90df	Apalache	Set0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
1c41ff0260fb3135a5fd9b033cc2015deb351905	Apalache	Set0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
d9f734b711e395b8ff2824c36c63621161a95dc2	Apalache	Set0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
3edf0b5a04801b4de661939cd5c3f485cdd9a080	Apalache	Set0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
842f9a1d7df7a78d8245c6d59f84b77e58ff0b80	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	Set0	NumRange	True	Passed	Model Under Test Equivalent Model
fbd1576790eeae0d2a56f651d1260f3c9db97061	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	Set0	NumRange	False	Passed	Model Under Test Equivalent Model
64a0e0c17249f9e616e2527aac4f9e45926bdc83	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set0	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
285889414442d6d183524b4164ffe86540203a75	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set0	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
12f0fca4f400d704b2b6af4a90758e586e772980	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]]	Set0	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
6ad6b44daff8b6bb999920886cef6fe786ffbb41	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]]	Set0	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
7d51baf9b39e0150dc1c1a12c5d6747b744e3848	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set0	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
abf528726a99d4f5c9a874054e6db36cf4d30bd1	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set0	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
460c6181575433a5e71e7edffbe269a0b4763884	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set0	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
ca702a74ddff802c30f4f524762b805c9c4ed6b6	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set0	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
ebe64dc95545c06eba1ee61cd122959cb57d3bba	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set0	TlcEval	True	Passed	Model Under Test Equivalent Model
3e634dea6b40adbd234d7f00365565a98282b198	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set0	TlcEval	False	Passed	Model Under Test Equivalent Model
4aeadc295d4952203a2e76ae54bf07275b291a34	Apalache	Set0	BagBagToSet	True	Passed	Model Under Test Equivalent Model
ade24372c3109ab7e1fc9b90b81a4b9172d89d79	Apalache	Set0	BagBagToSet	False	Passed	Model Under Test Equivalent Model
c498b44194ce62a1a0a5e7a5272228798bb19238	Apalache	Set0	BagSetToBag	True	Passed	Model Under Test Equivalent Model
d403c02d1b2941f480f023174a6b0a1b486ec94b	Apalache	Set0	BagSetToBag	False	Passed	Model Under Test Equivalent Model
33cb8dff1d4f6807b66ce35fb85bf97942d29890	Apalache	Set0	BagBagIn	True	Passed	Model Under Test Equivalent Model
a1e71fffb2480c12df7cfa5b50356f8cb4eafc9c	Apalache	Set0	BagBagIn	False	Passed	Model Under Test Equivalent Model
50f5dfc5ae592293ade9b4ca65d442c4841eb3a9	Apalache	Set0	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
bbda287fe455385e627fbec4fb52efe2126807f7	Apalache	Set0	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
c1ccc5652abeb0908e354627bb5100eb6025ea49	Apalache	Set0	BagAddBag	True	Passed	Model Under Test Equivalent Model
ebec4dc5ee2e2c52252d7df2683c81399027c10e	Apalache	Set0	BagAddBag	False	Passed	Model Under Test Equivalent Model
1150af6ee5879337be923e3f5f14a089c88f1a8d	Apalache	Set0	BagBagSub	True	Passed	Model Under Test Equivalent Model
89483fa8bf3c16c19a2d0dd816d9b29f95f4cf8d	Apalache	Set0	BagBagSub	False	Passed	Model Under Test Equivalent Model
ac896e83e8365df29abf99e05feff0a4718ea36a	Apalache	Set0	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6c03dd6aa75f99884b07856447652d0d8b147ca9	Apalache	Set0	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
4360e0d08c4fcd1b637afbd722edde6286ad67b1	Apalache	Set0	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
ae170741a3cadc61cb5b98862af4f8dcac926828	Apalache	Set0	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
da31de903ca2ace4b6cac8d275393f284bb7624a	Apalache	Set0	BagBagUnion	True	Passed	Model Under Test Equivalent Model
3a586c38b220c3d8483b6660377434fc3ff8728b	Apalache	Set0	BagBagUnion	False	Passed	Model Under Test Equivalent Model
68cbb81b3ad0c30d5248c1616062c3e011275d1e	Apalache	Set0	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
4e002e12008613e9b17117b896514967f812c559	Apalache	Set0	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
9d3b65c997260d821e1fdda0d41b14e02b44cceb	Apalache	Set0	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9716e16434df6b47736b72c47f3cd83d3904b4f3	Apalache	Set0	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
7714428ec67e594065d2787a787cc2df8c15136f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set0	BagSubBag	True	Passed	Model Under Test Equivalent Model
00b66de7a3472cf13cc58e50bcb7a68b1d349734	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set0	BagSubBag	False	Passed	Model Under Test Equivalent Model
0a97522e46892039598b29ed9f09a2fbb49acdcd	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)	Set0	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
e35dfb6c7c619eb2bb1da8c1480172b7ddf271d1	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)	Set0	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
168e68ce940dfec3f8e6c3d433e9fcb029869a17	Apalache	Set0	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
f60f48310e4c378c4db41b7ec6a40e4c16ec7400	Apalache	Set0	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
0dc8a7f4dd0f54ba23d542c9051efc85de37c7b5	Apalache	Set0	SeqHead	True	Passed	Model Under Test Equivalent Model
a01d629ce6ef92c9e38ad6702ed28e10e6ae574f	Apalache	Set0	SeqHead	False	Passed	Model Under Test Equivalent Model
fbf77ae647369b8ca123bab34bd436a97a6f21a9	Apalache	Set0	SeqTail	True	Passed	Model Under Test Equivalent Model
a8e3a12562b368b4fd678746bddf88651fb24788	Apalache	Set0	SeqTail	False	Passed	Model Under Test Equivalent Model
e07d47d003041fa2998ca886e856a731f082df19	Apalache	Set0	SeqAppend	True	Passed	Model Under Test Equivalent Model
31b49e5d7b3607785c694d925ba2e61ca209f8f8	Apalache	Set0	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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