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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6a5196554d5510c73a2621b89e2c93b45dd1a391	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFun	OneLineComment	True	Passed	Model Under Test Equivalent Model
0d3b12f186ca9e0405cc8760ec08234bcd9c8aa1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFun	OneLineComment	False	Passed	Model Under Test Equivalent Model
2e508ce5b224837e3ac51d50f0a8e73651c9683d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFun	MultiLineComment	True	Passed	Model Under Test Equivalent Model
197ebd31820e6c3b9e6329fc889faa435cf6fd3e	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFun	MultiLineComment	False	Passed	Model Under Test Equivalent Model
42730151aafc9097578e849b5fff20af5dc56272	Apalache	DefFun	BoolTrue	True	Passed	Model Under Test Equivalent Model
1d87e0eecefb36e8b1318f9d8172dcabd7d4b746	Apalache	DefFun	BoolTrue	False	Passed	Model Under Test Equivalent Model
9a5bd8fc221cab88ffc9ff48a3eded87a2a8fca9	Apalache	DefFun	BoolFalse	True	Passed	Model Under Test Equivalent Model
efdca00234252421c0a41f8b6e551b4256371d1d	Apalache	DefFun	BoolFalse	False	Passed	Model Under Test Equivalent Model
7f19de57983f12a3b2675a5217cb68370594209d	Apalache	DefFun	BoolSet	True	Passed	Model Under Test Equivalent Model
8978b915b58fdc2db65d18c0297187c3e6cfce2a	Apalache	DefFun	BoolSet	False	Passed	Model Under Test Equivalent Model
e79b7f1c6900dd5c3ab1eb0f4b3bcb13ef0a4965	Apalache	DefFun	And	True	Passed	Model Under Test Equivalent Model
3d1713cb7a6f01f834e9cece80accb72fe90406d	Apalache	DefFun	And	False	Passed	Model Under Test Equivalent Model
5242c8b4c8bf355ada3479f8192e5e97247ad037	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	DefFun	AndMultiLine	True	Passed	Model Under Test Equivalent Model
6a87e6aeedcbdaea8e6ff65e6ce165bf269a1460	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	DefFun	AndMultiLine	False	Passed	Model Under Test Equivalent Model
aa50994199909ca887136f4a8aea328ad73eebe8	Apalache	DefFun	Imply	True	Passed	Model Under Test Equivalent Model
840e13a0b2688e2e02d4007bf7e58a5123baa44e	Apalache	DefFun	Imply	False	Passed	Model Under Test Equivalent Model
951781c18032422457c42dc250fc53a8a85acd60	Apalache	DefFun	Not	True	Passed	Model Under Test Equivalent Model
0c78a63878af135d2ea0894c884f7229ca9885ff	Apalache	DefFun	Not	False	Passed	Model Under Test Equivalent Model
575c9ed479a0244a4ce400c8b658fb0498bd7f53	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	DefFun	Or	True	Passed	Model Under Test Equivalent Model
07bde52891a653e69fe075b2002e5e4a3056b519	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	DefFun	Or	False	Passed	Model Under Test Equivalent Model
d8583f5830cf5c2252be00b19fd0b7d7978ec61c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	DefFun	OrMultiLine	True	Passed	Model Under Test Equivalent Model
a49b469552992cb3cdd8ab2ec1e39f74f615a355	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	DefFun	OrMultiLine	False	Passed	Model Under Test Equivalent Model
75eca5dbffd6ad298aea818081b7f0b7d364eeba	Apalache	DefFun	Eq	True	Passed	Model Under Test Equivalent Model
fdc733bf0510269d0f68b65ba33380dd347ef0ce	Apalache	DefFun	Eq	False	Passed	Model Under Test Equivalent Model
c89550f85063552a66e4c7878b482ed71ea9c26b	Apalache	DefFun	Ne	True	Passed	Model Under Test Equivalent Model
bf0e8ec1ea6f9c88dd2f5b4a01c3d1d0dc2eaa02	Apalache	DefFun	Ne	False	Passed	Model Under Test Equivalent Model
06bc6ffae460b4d0d8accc6bee84bcbccca69672	Apalache	DefFun	Let	True	Passed	Model Under Test Equivalent Model
acb67a134c0892c45dab739fc6ef2af05557ab5b	Apalache	DefFun	Let	False	Passed	Model Under Test Equivalent Model
80ea62efaa5ad3345c987d98e94afaa74a57a11f	Apalache	DefFun	SetEmpty	True	Passed	Model Under Test Equivalent Model
2d2c9e8d2a87e5528a36b819990681e058c0adb9	Apalache	DefFun	SetEmpty	False	Passed	Model Under Test Equivalent Model
cd84e5dbb291b16a7587dde3644074fce16fa6f0	Apalache	DefFun	Set0	True	Passed	Model Under Test Equivalent Model
6280c3402c19df8d5695596492b9a0a805c28319	Apalache	DefFun	Set0	False	Passed	Model Under Test Equivalent Model
6c08c127c61cc43512e00ae402c5cd81ba269247	Apalache	DefFun	Set1	True	Passed	Model Under Test Equivalent Model
b28bd361d0fef4fdec91e752a489490e65f1fa62	Apalache	DefFun	Set1	False	Passed	Model Under Test Equivalent Model
0d41736bbe1f9b94c23892d2757503ef0f611921	Apalache	DefFun	Set2	True	Passed	Model Under Test Equivalent Model
afa43d95c08839e39ce1d71a8f1d3bb015b7f1c0	Apalache	DefFun	Set2	False	Passed	Model Under Test Equivalent Model
5476f1cbbf90cbd079f862859d3bd7849eaddfb6	Apalache	DefFun	Fun	True	Passed	Model Under Test Equivalent Model
585cfd3726ffa19ef188e4329c5a672c925220b2	Apalache	DefFun	Fun	False	Passed	Model Under Test Equivalent Model
07c363524226feed1247f53028afc3a7ca13ec8c	Apalache	DefFun	In	True	Passed	Model Under Test Equivalent Model
117ed40d8372f63a2c8f32ef4336b4615ebfa434	Apalache	DefFun	In	False	Passed	Model Under Test Equivalent Model
c105657ea63ba9af23b8e0c7dd9a5f1eef2ce177	Apalache	DefFun	NotIn	True	Passed	Model Under Test Equivalent Model
d75b1bf5b48b3b210435327cb85efcf297f8b533	Apalache	DefFun	NotIn	False	Passed	Model Under Test Equivalent Model
ee7828a2e5b5e5a4d4c2151ff8d2e0d224fc8f57	Apalache	DefFun	Exists	True	Passed	Model Under Test Equivalent Model
4125c3ae7bcf6d165b73d47abae26552e161faaa	Apalache	DefFun	Exists	False	Passed	Model Under Test Equivalent Model
2a480c618ac3c1aad75296844cd0da33fe2db9d6	Apalache	DefFun	Forall	True	Passed	Model Under Test Equivalent Model
4a1761cef757b9ad4bb6ba98ec89992c3fda7d03	Apalache	DefFun	Forall	False	Passed	Model Under Test Equivalent Model
7f32238f10c9144a1bb335e30cf3bac06913b8aa	Apalache	DefFun	Choose	True	Passed	Model Under Test Equivalent Model
99d957410276bd5b2134e784785260d4acb1a05c	Apalache	DefFun	Choose	False	Passed	Model Under Test Equivalent Model
9ed63d33ee9d5a54141a6252a87cedf8ca509fe1	Apalache	DefFun	Record	True	Passed	Model Under Test Equivalent Model
65b5ce397aac20d536071f7b7e61d68c5fd18dff	Apalache	DefFun	Record	False	Passed	Model Under Test Equivalent Model
d0032f7ba44b88d955a739fc933388a4f01d4422	Apalache	DefFun	Tuple	True	Passed	Model Under Test Equivalent Model
e2cdfb000a90d76a7c11fc8bf7c0b3eee3586d4e	Apalache	DefFun	Tuple	False	Passed	Model Under Test Equivalent Model
c086dca0bde6d0c05a585b74ff98c91e21250626	Apalache	DefFun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4f370fe07ccf538abd51622c24ebc16fa0c93b19	Apalache	DefFun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
823ab31ad4e2e7a1b475452dcba1927581c56aa1	Apalache	DefFun	FunApp	True	Passed	Model Under Test Equivalent Model
36f489eab67c1a4f9ae630db78a7d1da1ea81e63	Apalache	DefFun	FunApp	False	Passed	Model Under Test Equivalent Model
6a29a041aa0a3b80a672ddb24b9958a3d1fa17ba	Apalache	DefFun	Prime	True	Passed	Model Under Test Equivalent Model
f15058c86ea98faa2ef00f4e3d1dbe8c104008de	Apalache	DefFun	Prime	False	Passed	Model Under Test Equivalent Model
f131342f30596956ba608c8c9ac5ab68b5d4cc13	Apalache	DefFun	NumZero	True	Passed	Model Under Test Equivalent Model
b93db1fd90504974f22e30e6720f8ffcfaab6836	Apalache	DefFun	NumZero	False	Passed	Model Under Test Equivalent Model
ebd6675d8e5b1ab55143dccef775f18889b2d510	Apalache	DefFun	NumOne	True	Passed	Model Under Test Equivalent Model
e429763411c94fc7ec38b51cc22357c9022c1ee7	Apalache	DefFun	NumOne	False	Passed	Model Under Test Equivalent Model
e2d1e6b56bbbee342450b62c499e92a9b5fefdfc	Apalache	DefFun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
59b5acd76397ecaeffbd0ad2f6169f1895ea24fa	Apalache	DefFun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
8e15d56f85d08c91ef45b2f111c3fba2f54f2910	Apalache	DefFun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e56032cc84c984e46b1a0e9b664fd672e3f7dc26	Apalache	DefFun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
70bdb2f7eda1e75c29d3a3550eed143f21bf29d2	Apalache	DefFun	NumPlus	True	Passed	Model Under Test Equivalent Model
3acf953d34894a48e842b263bccde90b6046ddba	Apalache	DefFun	NumPlus	False	Passed	Model Under Test Equivalent Model
bea94f2df2397481de05c545d9eb39592c50c511	Apalache	DefFun	NumMinus	True	Passed	Model Under Test Equivalent Model
e96b6108fca0285e60af28f20e0b9eca55505bf9	Apalache	DefFun	NumMinus	False	Passed	Model Under Test Equivalent Model
097e82d930f8c83d89665149039bac08e19afc6b	Apalache	DefFun	NumMul	True	Passed	Model Under Test Equivalent Model
eb03d5ef8c0529edaaafd734169ab125a1cfe484	Apalache	DefFun	NumMul	False	Passed	Model Under Test Equivalent Model
b1f13a2a7821af669abb809c3b0058a00cb91fb8	Apalache	DefFun	NumDiv	True	Passed	Model Under Test Equivalent Model
c3899ffeca48026ab24fc3a00aeaa682145dd02e	Apalache	DefFun	NumDiv	False	Passed	Model Under Test Equivalent Model
1df72a62a1d7749cd85418186a764da717fbfb3d	Apalache	DefFun	NumMod	True	Passed	Model Under Test Equivalent Model
cb37779c0d2bd90feb0d9d5c7338f252aabb9054	Apalache	DefFun	NumMod	False	Passed	Model Under Test Equivalent Model
7a307aae2043d75609ba9e4fbc91d54a01173280	Apalache	DefFun	NumPow	True	Passed	Model Under Test Equivalent Model
96e8c2b3731f8e8715f8c67688a9e68e87b66ba1	Apalache	DefFun	NumPow	False	Passed	Model Under Test Equivalent Model
e1f2440750627bf848a2e5f0755af16848e066db	Apalache	DefFun	NumGt	True	Passed	Model Under Test Equivalent Model
95b6d64e9ce03383b908a27617eda8ac3023ca33	Apalache	DefFun	NumGt	False	Passed	Model Under Test Equivalent Model
f4e051edc5c1c0708ed69f7a6d6b3f5f8699539a	Apalache	DefFun	NumGe	True	Passed	Model Under Test Equivalent Model
d52e838a567029cf98d839afdd7a786fd7a8ea6e	Apalache	DefFun	NumGe	False	Passed	Model Under Test Equivalent Model
c91ca7f4e9cd4117c53823d4b1303f16fea9f0c0	Apalache	DefFun	NumLt	True	Passed	Model Under Test Equivalent Model
29d0fb0d8d9c622c966929f9a1772866411803f7	Apalache	DefFun	NumLt	False	Passed	Model Under Test Equivalent Model
15ef75fdbc0cd67c9460be186016da1a57e4e0f7	Apalache	DefFun	NumLe	True	Passed	Model Under Test Equivalent Model
904585de29fe5308a2b16c9d4cb8452198526c3d	Apalache	DefFun	NumLe	False	Passed	Model Under Test Equivalent Model
b10e65556690ff7d16e7ffba97d90cdcb9870196	Apalache	DefFun	DefFun	True	Passed	Model Under Test Equivalent Model
e9cfdcb914d2ecd56fbcf33824e41dd2205f115c	Apalache	DefFun	DefFun	False	Passed	Model Under Test Equivalent Model
0dee11d2a21f2bb0fbf39014c6351b6d82a56b90	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDefFun	True	Passed	Model Under Test Equivalent Model
6f82132f72df83e5bd5ba7c18e73697a9535c4c2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDefFun	False	Passed	Model Under Test Equivalent Model
9efd7b350dc6132bec71b789f64f97ac1323be37	Apalache	DefFun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
3b38398cc64eadd5ac3dffd699728329a5039d11	Apalache	DefFun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
cdfd71d85f61b363f1f467e656fae2ec19492ca9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
570f634c78139e6d186278dc89f68e9393206afa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
a9ef7106a085aca5597a552bbf0e7229c74d1eea	Apalache	DefFun	Def0	True	Passed	Model Under Test Equivalent Model
c26eb145ab2df38e41363f9e4178e2e09f796c73	Apalache	DefFun	Def0	False	Passed	Model Under Test Equivalent Model
77d2ff302fac7e73f0ff1a9cda9dba32ee719d7e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef0	True	Passed	Model Under Test Equivalent Model
f3c532fa7919f4e53eff217da0fb8f465d5e0512	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef0	False	Passed	Model Under Test Equivalent Model
aaf7028d0855d58835fee1c78618c0fbb02f9384	Apalache	DefFun	Def1	True	Passed	Model Under Test Equivalent Model
1e61d5ed056a0e9c30059438bf69941adccb33f1	Apalache	DefFun	Def1	False	Passed	Model Under Test Equivalent Model
0274b30d711546e1ae445a396b5b401b32a810b4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1	True	Passed	Model Under Test Equivalent Model
99b034adf88bc44b0d77fe2e07c8d08f316ec779	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1	False	Passed	Model Under Test Equivalent Model
6e55401c42f4fcae01244ec8eea4e4c2c10366eb	Apalache	DefFun	Def2	True	Passed	Model Under Test Equivalent Model
a5bf943ddd0a707286b93c513ea9883e5ae25de2	Apalache	DefFun	Def2	False	Passed	Model Under Test Equivalent Model
e1ccae3728c21d81705e06c24721c49ce7947731	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef2	True	Passed	Model Under Test Equivalent Model
6a1155c5499b87d9a6cb333cfbad67d7ca365c02	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef2	False	Passed	Model Under Test Equivalent Model
7d0ac65f923fe941e11f734468d369ced03b33be	Apalache	DefFun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b38d2b93f29d841264b57bd2f8ec7f149b757d38	Apalache	DefFun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7d16ed80af4087792dbfef80122df0e03b83967a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
40a243f8db9a8d25906ec6cf8b5577a9dfb2fead	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
e91d91e6b20b22bf3d84d0cbb5dd86a1b81d7d83	Apalache	DefFun	Extends	True	Passed	Model Under Test Equivalent Model
b2608378afe33c3678ae2ab07e57603547bb5a6d	Apalache	DefFun	Extends	False	Passed	Model Under Test Equivalent Model
ca168b7fa9a29d2252f71d9abbb1d6f8c1170258	Apalache	DefFun	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
bfaeea8b474f88dfde6e45759de48957f16f06ad	Apalache	DefFun	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
3042ec0e53403780249d2f61479b044eb41c235c	Apalache	DefFun	Variable	True	Passed	Model Under Test Equivalent Model
957408cadee0226c39a31f0f3221d682885fedc2	Apalache	DefFun	Variable	False	Passed	Model Under Test Equivalent Model
d690d6c17fcc428987bbd65357da4cf4b9efc6d2	Apalache	DefFun	Constant	True	Passed	Model Under Test Equivalent Model
83a1beb8256d9c75fc8229d50148beb98f0e44a9	Apalache	DefFun	Constant	False	Passed	Model Under Test Equivalent Model
848000cd7a918814ea503ebd539736ad8e69d174	Apalache	DefFun	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
5a25b2712dd41040644450c83c3f974cc2615c78	Apalache	DefFun	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
28c4351c65b090353d8119226f7643764164292d	Apalache	DefFun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
5276954c8a6deba4546580bbfc606ca6104c3663	Apalache	DefFun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
350a11aa4d0c7543ff88c7d4b68748d9e66c0bd1	Apalache	DefFun	Instance	True	Passed	Model Under Test Equivalent Model
2698c8ebeefa4aa08fbd4a461d7e5184ec613fa8	Apalache	DefFun	Instance	False	Passed	Model Under Test Equivalent Model
3b51606862c1adb794ac714a0d07a0309a96ec80	Apalache	DefFun	InstanceWith	True	Passed	Model Under Test Equivalent Model
371be8f9e9fe50dba74a56e0c5584d1669dcfcd0	Apalache	DefFun	InstanceWith	False	Passed	Model Under Test Equivalent Model
d2b94ba4f8ffe944ed2f8055532dcdbf605ec78c	Apalache	DefFun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3b5aa6cee5b4d1351205fc9d9eebc488699a3f2d	Apalache	DefFun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
2ab53761bf6bfb973b8799633e4054d3ea2c7d28	Apalache	DefFun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
13359dfbc8f03b921859081d0c0c6375e3072104	Apalache	DefFun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d697df3b125b41b0aa6b0b923d835dfc736caf41	Apalache	DefFun	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
aaa3835d0e12a4a749147f966659dd00e0affcaf	Apalache	DefFun	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
b87c574d65e83e44af95f8c95d5721cfe97f8ae3	Apalache	DefFun	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
587f7041a43d9190807dbf49dfe4ac27c0299280	Apalache	DefFun	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
f6c966bd3e6f77d6ffaa35c39d4af1a83d0244f5	Apalache	DefFun	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
5518c98b492f4778b663eb3905d5c354f0bb75bc	Apalache	DefFun	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
86911060b80f7a5b1cb635967f749e3eb6c1c148	Apalache	DefFun	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
4630f68317bcbd23bfdf79f452adf93daf9a5f41	Apalache	DefFun	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
7a459e1f0071bca3d91dc7e5535d2bc6f2259d7d	Apalache	DefFun	Enabled	True	Passed	Model Under Test Equivalent Model
8f262d49d36bd754455ad81c95d0dd465f4395e0	Apalache	DefFun	Enabled	False	Passed	Model Under Test Equivalent Model
403c2ebd6abedaf05d5571df390736e5345d641f	Apalache	DefFun	Cross2	True	Passed	Model Under Test Equivalent Model
134f5d3cd54bc0744059d2c49b06b11afd4623c7	Apalache	DefFun	Cross2	False	Passed	Model Under Test Equivalent Model
89f260046f46f9195d46b8f4bebf5a8b52399ca9	Apalache	DefFun	Cross3	True	Passed	Model Under Test Equivalent Model
1ba4f231df43f6c6fc18a44e125db34724f62c5b	Apalache	DefFun	Cross3	False	Passed	Model Under Test Equivalent Model
65b710cdcae8e939b51194650b539508bb5b55fa	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))	DefFun	FunSet	True	Passed	Model Under Test Equivalent Model
3fc540f6eed80de547dd2f6a13c8c9d5922ef594	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))	DefFun	FunSet	False	Passed	Model Under Test Equivalent Model
8d5308a64698120513caeb95542c59716e764bd6	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)	DefFun	RecordSet	True	Passed	Model Under Test Equivalent Model
ab886376e0ef4a1b23a70c77a4fbd6097dca05c5	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)	DefFun	RecordSet	False	Passed	Model Under Test Equivalent Model
e27a09cfccb9f9c123dc5d1d17a8b649a8736571	Apalache	DefFun	SetDiff	True	Passed	Model Under Test Equivalent Model
0b59877206d35c3ed1454fa4fe1c123dfa3ad29a	Apalache	DefFun	SetDiff	False	Passed	Model Under Test Equivalent Model
4992b9ed2201c888a6bc1332c7168ae751b88c05	Apalache	DefFun	SetUnion	True	Passed	Model Under Test Equivalent Model
e633a4eed98f79637b64435ca1b9c5c09b6bfffa	Apalache	DefFun	SetUnion	False	Passed	Model Under Test Equivalent Model
cc0ef04245ef4ad65384aee078280cda729c7804	Apalache	DefFun	SetIntersect	True	Passed	Model Under Test Equivalent Model
b80dc7a121ecbbbc1409144ea65aa7f265ea2d4e	Apalache	DefFun	SetIntersect	False	Passed	Model Under Test Equivalent Model
a80c8590f3e3db87625e0fa99aab4e21b4d3bda9	Apalache	DefFun	SubsetEq	True	Passed	Model Under Test Equivalent Model
07e22fd6bd16b9e8f9c2701b7ec85b29d1f94388	Apalache	DefFun	SubsetEq	False	Passed	Model Under Test Equivalent Model
0e1f44eb0133a04b92daed03669ca405d0d49301	Apalache	DefFun	IfCond	True	Passed	Model Under Test Equivalent Model
514b5d287edb62a82c89d769dea89047d5d7cbac	Apalache	DefFun	IfCond	False	Passed	Model Under Test Equivalent Model
becf9751cab3640de9f971c7bfa56d2e8b0238b1	Apalache	DefFun	IfThen	True	Passed	Model Under Test Equivalent Model
653923068849a9684d1449d67340d9e7b79bcc34	Apalache	DefFun	IfThen	False	Passed	Model Under Test Equivalent Model
a6de274474e5fa00c1ff721844b68363cf290f2c	Apalache	DefFun	IfElse	True	Passed	Model Under Test Equivalent Model
cc482dd0f7ccc9fc28523e56406047593833c67c	Apalache	DefFun	IfElse	False	Passed	Model Under Test Equivalent Model
b531181a979b0ed476949c75093ebeda84452855	Apalache	DefFun	Subset	True	Passed	Model Under Test Equivalent Model
00a9c11cd8a64061cdbdd858e2ed8d47760bdf11	Apalache	DefFun	Subset	False	Passed	Model Under Test Equivalent Model
bb07a9ce08aab5caddbbe3c00770a23cf551a9c3	Apalache	DefFun	Domain	True	Passed	Model Under Test Equivalent Model
e4345fae85f546575dbddff586a6f0e0b6875f0e	Apalache	DefFun	Domain	False	Passed	Model Under Test Equivalent Model
109d7f90b7720696cb0340d8a730fa62417dec56	Apalache	DefFun	Union	True	Passed	Model Under Test Equivalent Model
7e5f75f9397f6f46c4413e2eb23dc292bd1a76a8	Apalache	DefFun	Union	False	Passed	Model Under Test Equivalent Model
8138183f4bfb47c916156333fe82d496dc0e6a12	Apalache	DefFun	Unchanged	True	Passed	Model Under Test Equivalent Model
ae53f137c6fc6fb892a7261d9ce0ea53f7d317d5	Apalache	DefFun	Unchanged	False	Passed	Model Under Test Equivalent Model
ac2cfba44260060722cc9330f938043c761a9760	Apalache	DefFun	Equivalence	True	Passed	Model Under Test Equivalent Model
90dc83808ed02c75042dbdb0b366d1f49436b5c5	Apalache	DefFun	Equivalence	False	Passed	Model Under Test Equivalent Model
5057c59fd59266e81c12c4eec101c88ffec9f916	Apalache	DefFun	StringEmpty	True	Passed	Model Under Test Equivalent Model
c02034df589c4a81b2cfda5af96af40f55731975	Apalache	DefFun	StringEmpty	False	Passed	Model Under Test Equivalent Model
b92f0855cf6163016ef83a53f6dbf019ef9b474e	Apalache	DefFun	String	True	Passed	Model Under Test Equivalent Model
d6e6f4e7649882ced7647a5dff3462bdf3602ba6	Apalache	DefFun	String	False	Passed	Model Under Test Equivalent Model
5e655a0317a2c34fe6db6d9204b71bfc419e9c57	Apalache	DefFun	SeqLen	True	Passed	Model Under Test Equivalent Model
3ad2c5f8224fbb673c20a4778b26a9e24b2268b7	Apalache	DefFun	SeqLen	False	Passed	Model Under Test Equivalent Model
358dd8b141f009994f0592915df07b8eee89260c	Apalache	DefFun	SeqConcat	True	Passed	Model Under Test Equivalent Model
7d7b52176c7aaa43d9e6c102f24caf7d439da680	Apalache	DefFun	SeqConcat	False	Passed	Model Under Test Equivalent Model
4899934771de3887c364bad91f0f48ddf7d3beee	Apalache	DefFun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
04cb2573f37bd8b157d38fd705928a424ad161c0	Apalache	DefFun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
94d3f31a8aa47a46b3fa005073eab3d08895f6ae	Apalache	DefFun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e2daec3167329dc77daa63bc27dfea2a0385c3be	Apalache	DefFun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
9df96645c80e54d7c1df5de0c4c23335b003b21b	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	DefFun	NumRange	True	Passed	Model Under Test Equivalent Model
107e8f95361bb555eca66075237795a81a6ed8e2	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	DefFun	NumRange	False	Passed	Model Under Test Equivalent Model
fb0ef0bb7c7e2eb1ab390ccaa406d253e278ec04	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	DefFun	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
13fc6e4a72c5039573d14032cebb18f1b0200e2f	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	DefFun	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
2c80ab17e5469f1d1e8b02d2eda31a69e631fed1	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]]	DefFun	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
fcbe8db6757323292fd83d8235847e104707d69f	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]]	DefFun	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
d7a333efee59dbccd9fb16a3061f8ff78d937e71	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	DefFun	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
5dda33e2554cf5b4b996af2db03c3eec08fe72f6	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	DefFun	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
c30a7bd9f90125e8f6a26d783503dca27e3b0d6a	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	DefFun	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
7bdab4cf17ba8c587284d103b48cad70a0624b5f	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	DefFun	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
e6b723114c55e9446c9a45a684141f93b7591e4c	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	DefFun	TlcEval	True	Passed	Model Under Test Equivalent Model
07638c448a0851cf0fe7af8875612dfc90c07583	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	DefFun	TlcEval	False	Passed	Model Under Test Equivalent Model
87d6f79a8b30b489b35685deb5019a971af94121	Apalache	DefFun	BagBagToSet	True	Passed	Model Under Test Equivalent Model
0ae16da1a558cec90451f8a65696f0a700ef2a7a	Apalache	DefFun	BagBagToSet	False	Passed	Model Under Test Equivalent Model
fa849e9cfe179a5e246dba65ff96bf6ff3b1da50	Apalache	DefFun	BagSetToBag	True	Passed	Model Under Test Equivalent Model
27c65d75fff968c50dabebfa99aaaeab476aa7db	Apalache	DefFun	BagSetToBag	False	Passed	Model Under Test Equivalent Model
8e7cd6faf85c6bc869e87de1d26efb53e7b18406	Apalache	DefFun	BagBagIn	True	Passed	Model Under Test Equivalent Model
bd8cb8b8318fa43a451efb58e6150969c736813a	Apalache	DefFun	BagBagIn	False	Passed	Model Under Test Equivalent Model
8e3e90b628ee9010f2d9831465a2995e4d63d474	Apalache	DefFun	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
9b2afc85e721c2939c82b6a3212641da9fd25cba	Apalache	DefFun	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
e17295fab81042728240a858a4f0e28bdcf2d95a	Apalache	DefFun	BagAddBag	True	Passed	Model Under Test Equivalent Model
f806d69a59cd82428dc742ad51269cd0b0eb9290	Apalache	DefFun	BagAddBag	False	Passed	Model Under Test Equivalent Model
7bac3a35d4f17eb37c0043924071c785879e7365	Apalache	DefFun	BagBagSub	True	Passed	Model Under Test Equivalent Model
27eda85ad4e43b869a1a29a1d2b1159887bb2cdc	Apalache	DefFun	BagBagSub	False	Passed	Model Under Test Equivalent Model
acfeb0182f3261c1d3cabcc4cb73c2323b8c7ecb	Apalache	DefFun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
d9d4490783bb4b75709b957b15f35d34e695f8b7	Apalache	DefFun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
fc70cd1e0d8b92c8cdd15032d5fe2202548888ae	Apalache	DefFun	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
2270e801c5926f51c3163d0e20070e2bbd69b6d2	Apalache	DefFun	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
c7fe0f86277d3c219d977ee43eb7a0d28b6e16a4	Apalache	DefFun	BagBagUnion	True	Passed	Model Under Test Equivalent Model
a3d01f1b1d31fd72deb1d6b3d93def9322496a2b	Apalache	DefFun	BagBagUnion	False	Passed	Model Under Test Equivalent Model
a773a91315683b3f8b3612f695441e4b74115196	Apalache	DefFun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
79b59ff6d5cd94cb8abeeffaa9b28ca8cba38c8c	Apalache	DefFun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
cf1d5cb0d2c11071b9e8f75b272a737aefe4fa97	Apalache	DefFun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
dbc1543d8456e389571c9e24f175305902346133	Apalache	DefFun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
496e5eb8884c6d19059670384c270505432dcc26	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	DefFun	BagSubBag	True	Passed	Model Under Test Equivalent Model
3bbb70eaabac13b7862cc943d768a00533e4336d	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	DefFun	BagSubBag	False	Passed	Model Under Test Equivalent Model
30b97bb4bf3ffde92524095739b0bb2033bbfb20	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)	DefFun	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
48942d8ea00b61b2ce617ac17a8cf63bc228b8d5	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)	DefFun	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
1d01180776000a53f19ae738e58cac9a35a033bb	Apalache	DefFun	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
b2a92251b1bb5cbee4439797f4ec341ed58789d6	Apalache	DefFun	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
0ce96891874d5762f64e4e554bad8e0efdafa703	Apalache	DefFun	SeqHead	True	Passed	Model Under Test Equivalent Model
97363a7f07e8428b2bdbb2623388ddbcb7506e10	Apalache	DefFun	SeqHead	False	Passed	Model Under Test Equivalent Model
1f9ac648800f5e536c327acd425d8a5470b9add6	Apalache	DefFun	SeqTail	True	Passed	Model Under Test Equivalent Model
e88c9ecfd06fd23fbfe4a9a5f1e9c6e338dced23	Apalache	DefFun	SeqTail	False	Passed	Model Under Test Equivalent Model
fa4f46b6bfc9755fd7a5a9c7fdf088a6e6e51423	Apalache	DefFun	SeqAppend	True	Passed	Model Under Test Equivalent Model
a69e096f7abda6c6a75f4dd1fee9d618251a5459	Apalache	DefFun	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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