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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
10a333c7ff76819385f7de6e7079182c765434cb	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def0	OneLineComment	True	Passed	Model Under Test Equivalent Model
0b8be833ddb7f7afd3718228af03f0c9967fa8e3	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def0	OneLineComment	False	Passed	Model Under Test Equivalent Model
baff5d76c22c76ffbb6f53422ae64604d0473073	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def0	MultiLineComment	True	Passed	Model Under Test Equivalent Model
9c04a2c5a7b978a4ced3ad50391054f941b5c82b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def0	MultiLineComment	False	Passed	Model Under Test Equivalent Model
66c2fe211966c5488914580f1180ac63582314a5	Apalache	Def0	BoolTrue	True	Passed	Model Under Test Equivalent Model
3ae0cd6e0e55f917e7bec588dfcfe1abfb73a211	Apalache	Def0	BoolTrue	False	Passed	Model Under Test Equivalent Model
0769cf6df8b0111e3ea68cf5680cf6570de1a25c	Apalache	Def0	BoolFalse	True	Passed	Model Under Test Equivalent Model
e550c24cf4ee42bf1a2be7e68d7870b9415f4118	Apalache	Def0	BoolFalse	False	Passed	Model Under Test Equivalent Model
8367af37389ac6ba6b0fb03bd92bcb6d0adac012	Apalache	Def0	BoolSet	True	Passed	Model Under Test Equivalent Model
129307f960117261ad67950110b2473ffb324003	Apalache	Def0	BoolSet	False	Passed	Model Under Test Equivalent Model
89545d8e531014711ac3b6cc7b27994dbc862f2b	Apalache	Def0	And	True	Passed	Model Under Test Equivalent Model
3a043a81bbc9421da16778de13e80ca6d2ae8f57	Apalache	Def0	And	False	Passed	Model Under Test Equivalent Model
42b70606408da10a370f3fae087ff678f268b2ea	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def0	AndMultiLine	True	Passed	Model Under Test Equivalent Model
5ef24d0b196ef1d96eb504dbd4fbc3d3755e3808	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def0	AndMultiLine	False	Passed	Model Under Test Equivalent Model
3da13f41dc3db59bc92291ffb7a812f1c0319960	Apalache	Def0	Imply	True	Passed	Model Under Test Equivalent Model
c36bd19bc490b20474d85dbd398e4d67ee87f7a4	Apalache	Def0	Imply	False	Passed	Model Under Test Equivalent Model
e25e3726fa999da58593f4ae2056fa571dc97dda	Apalache	Def0	Not	True	Passed	Model Under Test Equivalent Model
6e8c043ff9c7bc5e701297be2529e26b40389f8b	Apalache	Def0	Not	False	Passed	Model Under Test Equivalent Model
3f2cd89b13623f8d67dad35fd7507603cbf1c548	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def0	Or	True	Passed	Model Under Test Equivalent Model
ae7080da9c7b4336c4fd127fac083d3ca8f79753	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def0	Or	False	Passed	Model Under Test Equivalent Model
94e3e995b311284788728465d6ad8ae1994d9dbe	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def0	OrMultiLine	True	Passed	Model Under Test Equivalent Model
67e134665c097a8591ff64edd39a4cae06ad3e10	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def0	OrMultiLine	False	Passed	Model Under Test Equivalent Model
e982b296b1e2b40ff14a1bd5cb0c7b47ff7c4133	Apalache	Def0	AndProp	True	Passed	Model Under Test Equivalent Model
49063f62142b7a4a1ec3ce3e06f8faef7c7f3f21	Apalache	Def0	AndProp	False	Passed	Model Under Test Equivalent Model
a8ada6aa9cb0fd5000402744c25d5cf284f41a9c	Apalache	Def0	Boxed	True	Passed	Model Under Test Equivalent Model
4935456101a16ee9b74c367dd4027ceebff20f5f	Apalache	Def0	Boxed	False	Passed	Model Under Test Equivalent Model
79d1a53f91a56156dcb75118e08c93f49762e9cb	Apalache	Def0	Eq	True	Passed	Model Under Test Equivalent Model
935939b10d97385eb8eab7ea271bc664b6f011b2	Apalache	Def0	Eq	False	Passed	Model Under Test Equivalent Model
864653529079172a6c6c676464fb7405f6e64e2b	Apalache	Def0	Ne	True	Passed	Model Under Test Equivalent Model
06d487dfa7de95a82a1c24bf91e0154ca7e7851f	Apalache	Def0	Ne	False	Passed	Model Under Test Equivalent Model
6eaf62cb073d4b836e47eb3a0548c5f1fe80ba4e	Apalache	Def0	Let	True	Passed	Model Under Test Equivalent Model
32298417b45e969e21bfcdefbe4b99a5ea2ea4bb	Apalache	Def0	Let	False	Passed	Model Under Test Equivalent Model
55253a7c47481993e9f1138665595c49ed401f3d	Apalache	Def0	SetEmpty	True	Passed	Model Under Test Equivalent Model
1d8d6f5714ccc87fcb0f2dd09bd3f656a73cbd53	Apalache	Def0	SetEmpty	False	Passed	Model Under Test Equivalent Model
d7cc5d35faf695c1be9691620b2f3a43f98776b4	Apalache	Def0	Set0	True	Passed	Model Under Test Equivalent Model
55cd503b0ddcf598306b7ea35f1a2aa5e7d2b9b5	Apalache	Def0	Set0	False	Passed	Model Under Test Equivalent Model
ea00806e4061f93e7a01937e55bb05c0f9dff9f0	Apalache	Def0	Set1	True	Passed	Model Under Test Equivalent Model
119bd8821b4a3c1b26dc1b77c8c1fac891c98447	Apalache	Def0	Set1	False	Passed	Model Under Test Equivalent Model
04ab5030227aa07512503178cb6965460499e57e	Apalache	Def0	Set2	True	Passed	Model Under Test Equivalent Model
3abe61b341ef9a688d29b1623a0dff9d1c849ffa	Apalache	Def0	Set2	False	Passed	Model Under Test Equivalent Model
28bb6b493fa84a384eec6fbc71b8951be288e56c	Apalache	Def0	Fun	True	Passed	Model Under Test Equivalent Model
f57863153ae99a272b20f4632e2414c6e3418d6c	Apalache	Def0	Fun	False	Passed	Model Under Test Equivalent Model
c6586b007ff925a410c136f41648c9789c919392	Apalache	Def0	In	True	Passed	Model Under Test Equivalent Model
3300083a8a9e41228986ca7e423ec71232d0a324	Apalache	Def0	In	False	Passed	Model Under Test Equivalent Model
d7313984f72b58cf543177571188dece8fd517e6	Apalache	Def0	NotIn	True	Passed	Model Under Test Equivalent Model
797c67aeceeaf7da9bb49b54941ffc306043007b	Apalache	Def0	NotIn	False	Passed	Model Under Test Equivalent Model
d739d39a9a44b4ce6c40aa1a2a54130cc848e67c	Apalache	Def0	Exists	True	Passed	Model Under Test Equivalent Model
1b1bb161250df1a9d47e92c043388ad6caffd487	Apalache	Def0	Exists	False	Passed	Model Under Test Equivalent Model
ef8018ee282230738713d78d67285bcdb8bba6b5	Apalache	Def0	Forall	True	Passed	Model Under Test Equivalent Model
e48d1f9961322fca747ae8969022bb22efdccb13	Apalache	Def0	Forall	False	Passed	Model Under Test Equivalent Model
149d7411bed992e51d51b6615d48b2c69de13028	Apalache	Def0	Choose	True	Passed	Model Under Test Equivalent Model
c301a2141eae463dd1b96ff2a5ca3a98d634995a	Apalache	Def0	Choose	False	Passed	Model Under Test Equivalent Model
e6173c86ffd89bd15136c437ee86b9013b1187a8	Apalache	Def0	Record	True	Passed	Model Under Test Equivalent Model
9d99c6ceea4620679fbfb1e61d1afe82f7346e81	Apalache	Def0	Record	False	Passed	Model Under Test Equivalent Model
ef7fadd82457a251bb4ab98e8f4f75d4e4bbfc3c	Apalache	Def0	Tuple	True	Passed	Model Under Test Equivalent Model
44a111e6ae36fa23411a5baa345bf7af25735ece	Apalache	Def0	Tuple	False	Passed	Model Under Test Equivalent Model
4733ac85afd94283d51cb406abe269ee0d5676cc	Apalache	Def0	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8d1710d39938ea4d0e10696eae390a342923333d	Apalache	Def0	TupleEmpty	False	Passed	Model Under Test Equivalent Model
5b77d086dfb866aca7379c43d7e5164bc0c66bb1	Apalache	Def0	FunApp	True	Passed	Model Under Test Equivalent Model
faabc0be7fc4de0d30a5e564bc3db099e60d6026	Apalache	Def0	FunApp	False	Passed	Model Under Test Equivalent Model
2d23269c32be7d8c37783e53cb2f770dda845bef	Apalache	Def0	Prime	True	Passed	Model Under Test Equivalent Model
1e80c491abbe788a3516db08574ff77783e561d2	Apalache	Def0	Prime	False	Passed	Model Under Test Equivalent Model
976f35bd73906609314ae2b24b10ae8479ad8d6a	Apalache	Def0	NumZero	True	Passed	Model Under Test Equivalent Model
f35f99719a9daad6fec9aa7f908b0b8c3827b22d	Apalache	Def0	NumZero	False	Passed	Model Under Test Equivalent Model
8a1e5a07b3b11042b8814e39ec97773163c6b7e7	Apalache	Def0	NumOne	True	Passed	Model Under Test Equivalent Model
952683fa06875e23f0dd878fef470aa95fe8432c	Apalache	Def0	NumOne	False	Passed	Model Under Test Equivalent Model
971e86ecf462420feebe2c9cf2dc57c53755b262	Apalache	Def0	NumMaxInt	True	Passed	Model Under Test Equivalent Model
e2f9c5dd276184c3b3a5516ca609df2856a59bd8	Apalache	Def0	NumMaxInt	False	Passed	Model Under Test Equivalent Model
1784a87ffc8d1856602654d0d28ed7358745e73e	Apalache	Def0	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
14525ff0150bbaace4553730d39803eac88ce2fd	Apalache	Def0	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d9bf2f7804167c950652b437622ac1ff91342ddb	Apalache	Def0	NumPlus	True	Passed	Model Under Test Equivalent Model
56d4fff94c5c4fe85440970f220b56c10075109f	Apalache	Def0	NumPlus	False	Passed	Model Under Test Equivalent Model
a83e24d3a4fa635ab6f8c7699225fab32c6bbe8b	Apalache	Def0	NumMinus	True	Passed	Model Under Test Equivalent Model
e184cd7717e30451a2590a6456f0a3afad4bc50a	Apalache	Def0	NumMinus	False	Passed	Model Under Test Equivalent Model
e5fdc71f8ea77bcf51ba6febded116ed49818e71	Apalache	Def0	NumMul	True	Passed	Model Under Test Equivalent Model
25aee87a5bf2660ed3e98527d6af01843e562d65	Apalache	Def0	NumMul	False	Passed	Model Under Test Equivalent Model
9c3106fb94eba0bfc52b8c33e821274b48201b6e	Apalache	Def0	NumDiv	True	Passed	Model Under Test Equivalent Model
9ead6fe36949b93a21cc73210683ab2d77e3ad5c	Apalache	Def0	NumDiv	False	Passed	Model Under Test Equivalent Model
fddb3942509265fe17c86b3115622851cdde349e	Apalache	Def0	NumMod	True	Passed	Model Under Test Equivalent Model
18f37534edb750f74d9a01ac1ff6b940b96cdc73	Apalache	Def0	NumMod	False	Passed	Model Under Test Equivalent Model
b452f6a9685a2fba55183f3f0eb1493889e83de4	Apalache	Def0	NumPow	True	Passed	Model Under Test Equivalent Model
e8b125fa1dbf9205187bf60e0fd466fc4eb3198d	Apalache	Def0	NumPow	False	Passed	Model Under Test Equivalent Model
3b9d6b19e211810fb360678f3c3a5d995dc246fa	Apalache	Def0	NumGt	True	Passed	Model Under Test Equivalent Model
f7c2fe6002b4cec3eda5e98e365e6bc6c1e8f71d	Apalache	Def0	NumGt	False	Passed	Model Under Test Equivalent Model
f6d428a67ec4c30418cffa8fe6ab62463461cf91	Apalache	Def0	NumGe	True	Passed	Model Under Test Equivalent Model
a0f95ad1fcbbff06e8765970ea998eb8c6c235a4	Apalache	Def0	NumGe	False	Passed	Model Under Test Equivalent Model
3fb3403e09d1b16a6a774a3f37517dd1566bd4a8	Apalache	Def0	NumLt	True	Passed	Model Under Test Equivalent Model
dde129b89db0ac3c6bcdd805525d3f5a87190ed8	Apalache	Def0	NumLt	False	Passed	Model Under Test Equivalent Model
a62cd4f9a2e7815eb2fb5cc59a5f47ac613f71f7	Apalache	Def0	NumLe	True	Passed	Model Under Test Equivalent Model
ded4d1b802d399af8c412cc8346f1ef87f6600c3	Apalache	Def0	NumLe	False	Passed	Model Under Test Equivalent Model
7a2fe59cdb0fcfa0b4872cdef3c461eae7a2825d	Apalache	Def0	DefFun	True	Passed	Model Under Test Equivalent Model
a0afad5dc0e3cdd63611c18509005a94378379b7	Apalache	Def0	DefFun	False	Passed	Model Under Test Equivalent Model
5f264162515c6a1536b7d5304bb80e3ad54b5662	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDefFun	True	Passed	Model Under Test Equivalent Model
fc50ed36b7fb67588723f790e003b1ec7fd48c7a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDefFun	False	Passed	Model Under Test Equivalent Model
5b4fd581b51b9eb26f6693c095f5d48d2f271d1c	Apalache	Def0	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
20ad6cb51bc8b7df21de843541d426c6fae02d6f	Apalache	Def0	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
d288f1fa2689eb0623070ae8a95e6e075dbe60e1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
32e192106420c0870665bb6cf419b052f9b6acc5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
64962902d9a3f498344e0c2feedbb7ad949cb772	Apalache	Def0	Def0	True	Passed	Model Under Test Equivalent Model
80a9f6a090832fe2c64e5d4d1fc25e78308e1ab9	Apalache	Def0	Def0	False	Passed	Model Under Test Equivalent Model
72976850c01bbda339cec6a05745db6f71a3cf7d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef0	True	Passed	Model Under Test Equivalent Model
7c58658231cf7aee1fc87e451a8213a480883d26	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef0	False	Passed	Model Under Test Equivalent Model
d74ad7bd9b20d35d426a77e34e23e6aae94ae1a3	Apalache	Def0	Def1	True	Passed	Model Under Test Equivalent Model
8835c7cc97b4b9b9dfb9f68dee9e6797010f12d0	Apalache	Def0	Def1	False	Passed	Model Under Test Equivalent Model
9425a1b467aed7d4ae5c61bf5b208c8d84979ed0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1	True	Passed	Model Under Test Equivalent Model
4bba91890052d351429ba7de3ff74b34c66945d9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1	False	Passed	Model Under Test Equivalent Model
8aabee0c8ceff3c4296289f4a1b4897df6db5f11	Apalache	Def0	Def2	True	Passed	Model Under Test Equivalent Model
ff8d44090b86ec26ee3983a5c4143c1a830b76c8	Apalache	Def0	Def2	False	Passed	Model Under Test Equivalent Model
13faef550f2d980679692da511cf219a9eea7ca6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef2	True	Passed	Model Under Test Equivalent Model
5ba1f90100c2f699d31c5b5ed5ffe93000f77b12	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef2	False	Passed	Model Under Test Equivalent Model
4f65a980489316154e3aa3cc26b28febe0194e95	Apalache	Def0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
17a64bd5ea88c5dfea3110ffac4d16954d076d7c	Apalache	Def0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c5bcc885de28ffa6253edb6f70ad7d7f7b2db683	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
628af7c56822520afeafc3dee2ea61a6d4516c32	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
5c046a8d700572a680e1e3e305ad05b381768bc9	Apalache	Def0	Extends	True	Passed	Model Under Test Equivalent Model
5642eb8009219fd2905e047fbd6d287f73c39de8	Apalache	Def0	Extends	False	Passed	Model Under Test Equivalent Model
453be6c29ae8c86087cfd825c5a9736206a6ed00	Apalache	Def0	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
768e0884354b61bb099fe14f5d6d48995c325247	Apalache	Def0	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
1220ceb8e4c0c1936f9ecd151dede528c18ce8ef	Apalache	Def0	Variable	True	Passed	Model Under Test Equivalent Model
30150da8715891656b7ac2265bb7f828a050d056	Apalache	Def0	Variable	False	Passed	Model Under Test Equivalent Model
fb6b6901ba80c9ea238a34a3767975f383ee05d3	Apalache	Def0	Constant	True	Passed	Model Under Test Equivalent Model
3f8d0bf20c8b9c8fca132ffa26715ace108f5ecc	Apalache	Def0	Constant	False	Passed	Model Under Test Equivalent Model
b1022a0568314cfaaff1f4e159c5f466b8d1b420	Apalache	Def0	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
9fb56a78b153ef43ee4838dbbad92a821b709909	Apalache	Def0	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
ca61a4d415b64e078fb8e7f039b382e464873a03	Apalache	Def0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
135f9866e9f7592ece8eb70ecf5c9ff16f639ab2	Apalache	Def0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
731b4a1731f84584495e3abe329e7a0803912019	Apalache	Def0	Instance	True	Passed	Model Under Test Equivalent Model
4fba4efc0ec310221d01961e545b8492d3948b49	Apalache	Def0	Instance	False	Passed	Model Under Test Equivalent Model
7249c94c7b73bad6e28b54fb37661519ab1187ac	Apalache	Def0	InstanceWith	True	Passed	Model Under Test Equivalent Model
e69371e60e107a0d36689d79939171b23b6da6da	Apalache	Def0	InstanceWith	False	Passed	Model Under Test Equivalent Model
52d5f9d160b442a6edfaaeae990a5a8785838ee7	Apalache	Def0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
eef612f775a1d8938d946bdc64bf436b82a67505	Apalache	Def0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
81375a52af06174e20a2e2f8ebedaeef6f8fcf30	Apalache	Def0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
385684b6b16e6460b1cc90bec9bd6049da4531f4	Apalache	Def0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ba796252672dda62d1aeb3a7b06135a8f87e0838	Apalache	Def0	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
cde7e7691b7ae7b84b4934ff054a89ee237cbbec	Apalache	Def0	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
9d89f629b61db9b82f407aed3dd28a42e0a7d7fd	Apalache	Def0	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
f3c21630b7a93001b69997fc8349e644b4b7cd75	Apalache	Def0	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
ce606b160f92fab74347de81c093014cf6d6be15	Apalache	Def0	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
534c67ed63d0ccd36960a31e4373a3fd0767c672	Apalache	Def0	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
91dfac4ee57be3bb22454cbf369b531efb90b1d9	Apalache	Def0	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
0cafaf0e208459bef4c97be233a1e7e82a96a17f	Apalache	Def0	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
24864eac23409dd76ad0b90b8ea007dac3a68d97	Apalache	Def0	Enabled	True	Passed	Model Under Test Equivalent Model
12310c2b399662d98b67b64ae4ea7125570d1a2e	Apalache	Def0	Enabled	False	Passed	Model Under Test Equivalent Model
b827ea892250fe00a42ae6ddc970a97e526d99f0	Apalache	Def0	Cross2	True	Passed	Model Under Test Equivalent Model
dad8d80468fec87489f09df06e9ed5c19936a63a	Apalache	Def0	Cross2	False	Passed	Model Under Test Equivalent Model
d99401364aa3bf303e41e86a932097ec53df8dfe	Apalache	Def0	Cross3	True	Passed	Model Under Test Equivalent Model
c086af328aa7cb8dd6c5ab274a70fe0c4db23edd	Apalache	Def0	Cross3	False	Passed	Model Under Test Equivalent Model
02a2b2aa2b28152225adc05cf3215e7072e659cc	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))	Def0	FunSet	True	Passed	Model Under Test Equivalent Model
5992b00b5a67f06a26bf9f198d059bdbe9c752d2	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))	Def0	FunSet	False	Passed	Model Under Test Equivalent Model
010ef5a307b07178b8c1f7a1ae3fb9f0aaa6cd7b	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)	Def0	RecordSet	True	Passed	Model Under Test Equivalent Model
85ac444ca93a2dc55472607efb93277ad0ed3daa	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)	Def0	RecordSet	False	Passed	Model Under Test Equivalent Model
5a955879bdfc073bd1e633ac55d32ef6b0267f5d	Apalache	Def0	SetDiff	True	Passed	Model Under Test Equivalent Model
801324abd5e60a4095bb5a61a18c57d6fd3f0321	Apalache	Def0	SetDiff	False	Passed	Model Under Test Equivalent Model
36cbf24cb11af4dfb6f5c6fc4456f8d589562480	Apalache	Def0	SetUnion	True	Passed	Model Under Test Equivalent Model
e31ef5fd6e30a3471b9cfec20bfb4a81228f43c6	Apalache	Def0	SetUnion	False	Passed	Model Under Test Equivalent Model
b5ec427bb9d27855eb5f48e2823296dc6d634909	Apalache	Def0	SetIntersect	True	Passed	Model Under Test Equivalent Model
39b4cc44d55dfb9ab1b0e957a35df85093636dd2	Apalache	Def0	SetIntersect	False	Passed	Model Under Test Equivalent Model
8949c932947aa837b246cf524660bcd9555c369e	Apalache	Def0	SubsetEq	True	Passed	Model Under Test Equivalent Model
e27b4f1d6d532473ffaeebb3011835966e670a4c	Apalache	Def0	SubsetEq	False	Passed	Model Under Test Equivalent Model
0e9e7bb6acabd152e7d170c0f6fa77c82ba743c6	Apalache	Def0	IfCond	True	Passed	Model Under Test Equivalent Model
7e3a2dcf78f479435bd0a9b641134ca02b1f1d99	Apalache	Def0	IfCond	False	Passed	Model Under Test Equivalent Model
a5f5bd93fe5d60095e6b283403a6762cec1a5537	Apalache	Def0	IfThen	True	Passed	Model Under Test Equivalent Model
ebd6f19b630196dadd992f0976bf267528f372a0	Apalache	Def0	IfThen	False	Passed	Model Under Test Equivalent Model
02635b84ad19d35e7ec416c5353e35185326f304	Apalache	Def0	IfElse	True	Passed	Model Under Test Equivalent Model
e5c5ed96faca17439fa3b4683d12555de4686898	Apalache	Def0	IfElse	False	Passed	Model Under Test Equivalent Model
e9d30cd23359f88da0b0a41683959ef13a1f8416	Apalache	Def0	Subset	True	Passed	Model Under Test Equivalent Model
1d57decaa1bad21dc4e2a96492eabbde6c04a264	Apalache	Def0	Subset	False	Passed	Model Under Test Equivalent Model
9cd92a1a98e158e3f2b292d91ca94a06067558ac	Apalache	Def0	Domain	True	Passed	Model Under Test Equivalent Model
aa8ea950ed5ec957c971f5f1c5eb7fc424e65ea3	Apalache	Def0	Domain	False	Passed	Model Under Test Equivalent Model
fd8604de999091b61bfdc37ea09581526e2731ac	Apalache	Def0	Union	True	Passed	Model Under Test Equivalent Model
70d410ae2eccd44a25e0270e67f15ed347caa1f5	Apalache	Def0	Union	False	Passed	Model Under Test Equivalent Model
d4d54e27fc470a6ff4f2066709931a1acb9349e0	Apalache	Def0	Unchanged	True	Passed	Model Under Test Equivalent Model
4cf248d03915eb16b3c7c429ccad6939e8683460	Apalache	Def0	Unchanged	False	Passed	Model Under Test Equivalent Model
c32454af3cb22f9f0f22e6bfba48e256b7802e51	Apalache	Def0	Equivalence	True	Passed	Model Under Test Equivalent Model
ede88663ef16b722cc6030fac97a0e4717a9fa88	Apalache	Def0	Equivalence	False	Passed	Model Under Test Equivalent Model
996abb1e18f6ebbf0ceae5cb0acd64018183a1a8	Apalache	Def0	StringEmpty	True	Passed	Model Under Test Equivalent Model
7b9f1361ff47f14460952592b2caa7133615fe65	Apalache	Def0	StringEmpty	False	Passed	Model Under Test Equivalent Model
67e04ca09861a7928a6ab909820aec9473665630	Apalache	Def0	String	True	Passed	Model Under Test Equivalent Model
b22e780aa8933a2534da559157d4c2d531ed8dea	Apalache	Def0	String	False	Passed	Model Under Test Equivalent Model
71e4c5e97f0baeb17ba2bddd36c49136effad7f7	Apalache	Def0	SeqLen	True	Passed	Model Under Test Equivalent Model
5ff9b8bb06432f8bd71eafeb414acbd5372fa41b	Apalache	Def0	SeqLen	False	Passed	Model Under Test Equivalent Model
260ee2dd033f8cb0f5bcff1af791d3d6cebcc275	Apalache	Def0	SeqConcat	True	Passed	Model Under Test Equivalent Model
678935083c0812e31233e6d3a4c94ed432a4e24f	Apalache	Def0	SeqConcat	False	Passed	Model Under Test Equivalent Model
58b9caf356c49c5fefff6328caf701719aaa190e	Apalache	Def0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
e5cc19f3675e539ffe6ebfb86aaf1424d94894c4	Apalache	Def0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
0394ee365d19124e11309cf37af1a659c108d34f	Apalache	Def0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
72ce053bebab3fdfa30662d31f662ee5f12d3a8a	Apalache	Def0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d4244816f7f34baa46f18fb1ba80d04c694593ab	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	Def0	NumRange	True	Passed	Model Under Test Equivalent Model
c675ad63a6a976caba4d6d540b40fb9e5822c15d	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	Def0	NumRange	False	Passed	Model Under Test Equivalent Model
3f0a3732c455594c1554a75724ad7d18beed39ee	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def0	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
6c40f94f7b99de087d3ddd66ea4be63a60f6e7a3	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def0	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
6e008944077ea236b5ff3f6b8ecaa24c8b1b248d	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]]	Def0	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
18e350ec4ccbaea7ef2e665ed90d5dfa3ba55c86	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]]	Def0	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
f10dff435863427d398c6dcdafe0df9c9f09b32d	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def0	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
5230e3d3de3040b2926c1f204bb4d19221078f23	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def0	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
b89485a8026f6c69298d6bf8a9b6969a76d70aa8	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def0	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
46d3558df42d7bb58bdf189f56ea3454d15b7416	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def0	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
6401861223954f58c8544bb25281a42902ad0936	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def0	TlcEval	True	Passed	Model Under Test Equivalent Model
75c3603801addca109e9127cbb24c1bcd8ea9bba	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def0	TlcEval	False	Passed	Model Under Test Equivalent Model
e4d77460a362516ad23761539898df3761dbf5da	Apalache	Def0	BagBagToSet	True	Passed	Model Under Test Equivalent Model
890d6e8f66e6e82ef519590470841b5a4f760fea	Apalache	Def0	BagBagToSet	False	Passed	Model Under Test Equivalent Model
ceee3ffa03e024eff060f68967623aa0b82b977d	Apalache	Def0	BagSetToBag	True	Passed	Model Under Test Equivalent Model
1a0dae2e312beb8a61fc7566700cdab3d9246892	Apalache	Def0	BagSetToBag	False	Passed	Model Under Test Equivalent Model
5aed43d8a80aa18ab737bce42387b0415914a3f1	Apalache	Def0	BagBagIn	True	Passed	Model Under Test Equivalent Model
514dd55e4c1af60643a81894a8eda50cf18655b3	Apalache	Def0	BagBagIn	False	Passed	Model Under Test Equivalent Model
92247ec75ff8c56bd9db3dba9575f28209fb52e5	Apalache	Def0	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
1c282b49ee33cfcb2456331fcd1e8dd819878c60	Apalache	Def0	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
ee31d4b700056aa1e38b5b2c86c3f23beb6ce403	Apalache	Def0	BagAddBag	True	Passed	Model Under Test Equivalent Model
5abffac19786d48e6e048f2f3276f71a451e9b5e	Apalache	Def0	BagAddBag	False	Passed	Model Under Test Equivalent Model
35a7300d73302cec13e0f89a02db13984170dd97	Apalache	Def0	BagBagSub	True	Passed	Model Under Test Equivalent Model
ca4a857bd81604318a89209ca0c3edbfd8e4d09c	Apalache	Def0	BagBagSub	False	Passed	Model Under Test Equivalent Model
311f6859c1607a730bc93a3ef446e8ca81cce8e0	Apalache	Def0	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
e58480c2811072d8b7ea2dbcd31c6e373818e873	Apalache	Def0	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
96ce495c285577ce595330c6b503f7c64be299f8	Apalache	Def0	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
db40f0751f0e2621298b541b89faee725c285676	Apalache	Def0	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
2be703f794e5453ab58afdda1b25842a4b4e4854	Apalache	Def0	BagBagUnion	True	Passed	Model Under Test Equivalent Model
c4b2880242f6235de412eff8d40e7fdff2615fbd	Apalache	Def0	BagBagUnion	False	Passed	Model Under Test Equivalent Model
d3c011bb46c57cc177ee95e34879e27b1a7c9035	Apalache	Def0	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
1d04d9b1669f3e43b62e852bcbe9087aecac3925	Apalache	Def0	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
61eab3a62b3b3765423a31bdb1d5a9b6cb119aff	Apalache	Def0	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
84109080847331241f333a809d45ffbbd2ffdd83	Apalache	Def0	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
74b9460c569e92215f22f421a69651217f2e0432	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def0	BagSubBag	True	Passed	Model Under Test Equivalent Model
1fac4bb9e0904f74f1180ed13da5c42da1843c0f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def0	BagSubBag	False	Passed	Model Under Test Equivalent Model
bca6dc2fbc2c9263b7893d7250c9f59b2773ab25	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)	Def0	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
6f0940e3ef50b2864d90bb4c2d5bab93b3b6df70	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)	Def0	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
f2ab340cc4285f1c392bbaaf4a7c073eb038697d	Apalache	Def0	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
a97d93a792198b3df80b8ede34aa5dc760cc00aa	Apalache	Def0	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
0220ecbf114db746620694ff3b83aec5aa7f5519	Apalache	Def0	SeqHead	True	Passed	Model Under Test Equivalent Model
8b3cb7521ce40c0b5ab3aaf4d973d5814899ac30	Apalache	Def0	SeqHead	False	Passed	Model Under Test Equivalent Model
90cc3208e6f37bd64669a8cf480fbec2841516ee	Apalache	Def0	SeqTail	True	Passed	Model Under Test Equivalent Model
7300af812e9c0405e17cdcf9343e9e8d0db016cc	Apalache	Def0	SeqTail	False	Passed	Model Under Test Equivalent Model
4376ac46987a60b14fce3ba55934be8b12502600	Apalache	Def0	SeqAppend	True	Passed	Model Under Test Equivalent Model
733f494b1030927d6446db2deaa159dc1655ec89	Apalache	Def0	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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