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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
af9950a4b1947f2ff2f3db488b1e8e328703b1b6	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Constant	OneLineComment	True	Passed	Model Under Test Equivalent Model
3c36ea45574aeeae2161e19c98dc9865c2952892	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Constant	OneLineComment	False	Passed	Model Under Test Equivalent Model
6fb6613fefe98c0dc7e8e5961b375bd162ff815b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Constant	MultiLineComment	True	Passed	Model Under Test Equivalent Model
0dc78c89c27a89d17ce48210e2349e8ee50d8df1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Constant	MultiLineComment	False	Passed	Model Under Test Equivalent Model
86899fe6e3a44df1840e4e93271e960ef4fcb096	Apalache	Constant	BoolTrue	True	Passed	Model Under Test Equivalent Model
069e1ebe318bf7843ad86be080a042bf8621b510	Apalache	Constant	BoolTrue	False	Passed	Model Under Test Equivalent Model
90a31cfe2351c3877a9c990aff476bd6f9d98ede	Apalache	Constant	BoolFalse	True	Passed	Model Under Test Equivalent Model
290925cb1855d34e656eb10e0a817d00c36969fc	Apalache	Constant	BoolFalse	False	Passed	Model Under Test Equivalent Model
7b6e8b00a7b20e5a7709363d409508b1a9d8e88c	Apalache	Constant	BoolSet	True	Passed	Model Under Test Equivalent Model
38e2d989e55ab8e8ac17bd98a7b306faef2ffcea	Apalache	Constant	BoolSet	False	Passed	Model Under Test Equivalent Model
105c1f186698b729cabdb22674f62d6b5027f2ed	Apalache	Constant	And	True	Passed	Model Under Test Equivalent Model
b7cc29ac7b7d0ddd65a99b5d6c02cff8fbffb09e	Apalache	Constant	And	False	Passed	Model Under Test Equivalent Model
0e884d81df22b36aa5c3917557505887d402e187	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Constant	AndMultiLine	True	Passed	Model Under Test Equivalent Model
1269f819461424416d99ad6fe48babeddcaec2f0	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Constant	AndMultiLine	False	Passed	Model Under Test Equivalent Model
48f14580b43534862031078f9f3d42a1b322155d	Apalache	Constant	Imply	True	Passed	Model Under Test Equivalent Model
e2b11558c1251810bd90dd460d6f0522c055636e	Apalache	Constant	Imply	False	Passed	Model Under Test Equivalent Model
d53641767d904b3303b9383508e4f61901dec04d	Apalache	Constant	Not	True	Passed	Model Under Test Equivalent Model
ec052f170e4de95f1a12a720bf4be86003dd9a50	Apalache	Constant	Not	False	Passed	Model Under Test Equivalent Model
4493098dedcde6ed9367e1f0648205659e4e6da6	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Constant	Or	True	Passed	Model Under Test Equivalent Model
4c5cd7add6f38ea879449588a0fbb8fb7b5906d7	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Constant	Or	False	Passed	Model Under Test Equivalent Model
e9f82d8891b2651e3ccb9306c8a8cee8bf96a07f	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Constant	OrMultiLine	True	Passed	Model Under Test Equivalent Model
081883f7e778b0ed7d8983e16f01f5b6e43402cf	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Constant	OrMultiLine	False	Passed	Model Under Test Equivalent Model
51823473629f3815b382bbd624c0a0c3ad0ca75a	Apalache	Constant	Eq	True	Passed	Model Under Test Equivalent Model
1157387e2e27b35d41d3ec15133262d8304df413	Apalache	Constant	Eq	False	Passed	Model Under Test Equivalent Model
4525be6078e66fea88d0daefdf2242dc8b12b79f	Apalache	Constant	Ne	True	Passed	Model Under Test Equivalent Model
bd9c9d9cd403c62ec0dd1d1c76f23c94e61bccd1	Apalache	Constant	Ne	False	Passed	Model Under Test Equivalent Model
d9d4b1e57236056d92b1acaadfcd2add76dee40c	Apalache	Constant	Let	True	Passed	Model Under Test Equivalent Model
6eae32dcaedf5e37e8cb819cd038ff7e5012cf5e	Apalache	Constant	Let	False	Passed	Model Under Test Equivalent Model
93fcae04b17c6e853b1a2ae8ecf0add0aa3fd19f	Apalache	Constant	SetEmpty	True	Passed	Model Under Test Equivalent Model
1442e0cab4d15696675502c665cfab2224fcdd82	Apalache	Constant	SetEmpty	False	Passed	Model Under Test Equivalent Model
94582b58d0f8c6100467a78f5f863059fa20fe8b	Apalache	Constant	Set0	True	Passed	Model Under Test Equivalent Model
e11683bdc34bda821efc34d168b4a2d9747ff3f1	Apalache	Constant	Set0	False	Passed	Model Under Test Equivalent Model
8d93fc9b3a743c34fa1fd8c82891e8201164ed06	Apalache	Constant	Set1	True	Passed	Model Under Test Equivalent Model
06c8f031f4ec3e7565109935165dd9024ecd8b11	Apalache	Constant	Set1	False	Passed	Model Under Test Equivalent Model
46652d6017722908a269fd6273c67185c0623722	Apalache	Constant	Set2	True	Passed	Model Under Test Equivalent Model
13f5ec9b0125028e75391dc202eb646a062ebc34	Apalache	Constant	Set2	False	Passed	Model Under Test Equivalent Model
f5fe19425afdb9283d9b31718869f6fd618918cd	Apalache	Constant	Fun	True	Passed	Model Under Test Equivalent Model
ee457b185c60158e1676d34ff57b9acc6edd0042	Apalache	Constant	Fun	False	Passed	Model Under Test Equivalent Model
a93ecc1de2e1d9139a8f0617738558bda9e4720e	Apalache	Constant	In	True	Passed	Model Under Test Equivalent Model
9792170799911ca4b153dab021dec9c0ad241cf4	Apalache	Constant	In	False	Passed	Model Under Test Equivalent Model
ed9a736a3b9917c5e97639b28861fd33ca043789	Apalache	Constant	NotIn	True	Passed	Model Under Test Equivalent Model
c371ae08fbf90be7573b88f87bbb27468362c22a	Apalache	Constant	NotIn	False	Passed	Model Under Test Equivalent Model
2b8e71360ffc1421c50b4c63a3487ed8a7553062	Apalache	Constant	Exists	True	Passed	Model Under Test Equivalent Model
72576b9a55b71d004e33dae885041afaed092d19	Apalache	Constant	Exists	False	Passed	Model Under Test Equivalent Model
47016140ab8e03d48748468aa6ecca8f5d50d34b	Apalache	Constant	Forall	True	Passed	Model Under Test Equivalent Model
78ef43eac78a922ff92ed460b0d10f9c49f755a8	Apalache	Constant	Forall	False	Passed	Model Under Test Equivalent Model
8c172895771a9be8c81ad57128c198a7e694f8ca	Apalache	Constant	Choose	True	Passed	Model Under Test Equivalent Model
8b33fd1777f0fe1ad89640a333f16a198b89fb99	Apalache	Constant	Choose	False	Passed	Model Under Test Equivalent Model
c498b9b1c3fbd83faeeb3d6e5891b300b1149181	Apalache	Constant	Record	True	Passed	Model Under Test Equivalent Model
21a86834fa378ae3f5f5b6cad28211b55de0b964	Apalache	Constant	Record	False	Passed	Model Under Test Equivalent Model
b6812154bca3aa5b2b712564f10b2596ffff3893	Apalache	Constant	Tuple	True	Passed	Model Under Test Equivalent Model
7a4b1ad604d852c0fe149df7b992ecf7ef781744	Apalache	Constant	Tuple	False	Passed	Model Under Test Equivalent Model
ce38612b87f91d04b1ce82f26d1f14b5b11b7847	Apalache	Constant	TupleEmpty	True	Passed	Model Under Test Equivalent Model
f3d91be799b0d7e8bee63cc480356f03f77b03ce	Apalache	Constant	TupleEmpty	False	Passed	Model Under Test Equivalent Model
8638b27ed04a1d7c223dc426ca92b21a4130bd6a	Apalache	Constant	FunApp	True	Passed	Model Under Test Equivalent Model
21067629af377f84c64dd04e827e81ae2588bd09	Apalache	Constant	FunApp	False	Passed	Model Under Test Equivalent Model
9799e0e2d606182132373ff918c002e4b682357d	Apalache	Constant	NumZero	True	Passed	Model Under Test Equivalent Model
0f974caf36d4a01aa9a01efa21384f2da541754a	Apalache	Constant	NumZero	False	Passed	Model Under Test Equivalent Model
8805d4394abfa4c09e82a8fe4274381493915e85	Apalache	Constant	NumOne	True	Passed	Model Under Test Equivalent Model
5e8246122d53fdedd50d6907677fa1e6d13f1e94	Apalache	Constant	NumOne	False	Passed	Model Under Test Equivalent Model
319b308afa835cf3c39e748679c003c3c592343f	Apalache	Constant	NumMaxInt	True	Passed	Model Under Test Equivalent Model
27c55045af821b59b607db790300614edb1a2e79	Apalache	Constant	NumMaxInt	False	Passed	Model Under Test Equivalent Model
9614d483f8696f70936ab9147813fd47877da4be	Apalache	Constant	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
2aa8fe8dd097d9b68cf60a209a49ec716b5a5b5d	Apalache	Constant	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
efba448f830594eb31e640fb0bb5b093ad21ebe9	Apalache	Constant	NumPlus	True	Passed	Model Under Test Equivalent Model
564eedb63cdc3c572d7655907b2674a99dd7dbf7	Apalache	Constant	NumPlus	False	Passed	Model Under Test Equivalent Model
eda2a051dba74030f9b56b1a96136518c1f48383	Apalache	Constant	NumMinus	True	Passed	Model Under Test Equivalent Model
fe64f6f819ece95d9fe3566a06bbd250f4bc28dc	Apalache	Constant	NumMinus	False	Passed	Model Under Test Equivalent Model
102d549791acaab592a334b6e10d8896fd97fed1	Apalache	Constant	NumMul	True	Passed	Model Under Test Equivalent Model
2ade0edf85ff90400fbdf93560ea162a6253bbd3	Apalache	Constant	NumMul	False	Passed	Model Under Test Equivalent Model
b42694e42b28426b83fd819f084a3fda693c8a0d	Apalache	Constant	NumDiv	True	Passed	Model Under Test Equivalent Model
644c7c6cc78e5062e28f644510c4a49b0e133ba4	Apalache	Constant	NumDiv	False	Passed	Model Under Test Equivalent Model
d5a2f0c7ef67961bb464fa5274481c91b140ebbb	Apalache	Constant	NumMod	True	Passed	Model Under Test Equivalent Model
e71a26ede4925a0b51c02a7305a15f86f46ea57e	Apalache	Constant	NumMod	False	Passed	Model Under Test Equivalent Model
4ba48d5a2eb31001c93d93ed0d3153deb567b0d8	Apalache	Constant	NumPow	True	Passed	Model Under Test Equivalent Model
1aa8759bdcd789f835b76a700c41a1f08ba043a0	Apalache	Constant	NumPow	False	Passed	Model Under Test Equivalent Model
f98a177f83b2f346eab178e67dbe5650bdca91bd	Apalache	Constant	NumGt	True	Passed	Model Under Test Equivalent Model
c4c4711c5e94766d85f6c5f4fffdbeafcaf0e247	Apalache	Constant	NumGt	False	Passed	Model Under Test Equivalent Model
92e8fd9ba963fba4365763709dc446b2dee2db68	Apalache	Constant	NumGe	True	Passed	Model Under Test Equivalent Model
010c79d17d23c88e47fba48763b0d754adb591d2	Apalache	Constant	NumGe	False	Passed	Model Under Test Equivalent Model
7f1a8b73a90f31670ed3ced1fe9c431a8bc9d690	Apalache	Constant	NumLt	True	Passed	Model Under Test Equivalent Model
62ceb4f48f76fc3c30e58a9d28e0ee62a0b01253	Apalache	Constant	NumLt	False	Passed	Model Under Test Equivalent Model
fb22d061423d72886dc6f923409740352ac64fd0	Apalache	Constant	NumLe	True	Passed	Model Under Test Equivalent Model
8599ce19893eaccd155e845f8e7eb520bd956b71	Apalache	Constant	NumLe	False	Passed	Model Under Test Equivalent Model
f726e23748c060e9a32827307094d1100761ea85	Apalache	Constant	DefFun	True	Passed	Model Under Test Equivalent Model
ec6ad61ed65e5a95ba32a8640901318b409fa4ba	Apalache	Constant	DefFun	False	Passed	Model Under Test Equivalent Model
c964414d3b81c11c7d2bff2553cc739770fbb87a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDefFun	True	Passed	Model Under Test Equivalent Model
f1dac791534a1b620db456939135bf4a24448f90	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDefFun	False	Passed	Model Under Test Equivalent Model
5a6b671a02f158cbcf52e11947dbd85d90c8e4aa	Apalache	Constant	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ed6e9394fc54249d391f765d3f14c8b2d53f80a2	Apalache	Constant	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
7f768def52e923012ace6301cb4669c89d8cd58c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
74bd1074664aa546ffe709156d232af9372074be	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
b0a1ce531968fe999aab0137aa9e6247f133837a	Apalache	Constant	Def0	True	Passed	Model Under Test Equivalent Model
e3b95523e654f7316e21c4de16b4f213a0dedf9a	Apalache	Constant	Def0	False	Passed	Model Under Test Equivalent Model
6ba58c20f166d9b2c946223984fe932016a357fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef0	True	Passed	Model Under Test Equivalent Model
c19c025189ae862b7c254dc1ee3976ed12d48294	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef0	False	Passed	Model Under Test Equivalent Model
9033c17c7d0c24a48c8a07c8212f60f3946a8572	Apalache	Constant	Def1	True	Passed	Model Under Test Equivalent Model
cccdf7347681eea3a2a1984c393602e61ef27ecf	Apalache	Constant	Def1	False	Passed	Model Under Test Equivalent Model
e7fc62a85989456228632b620f80d2c12337a276	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1	True	Passed	Model Under Test Equivalent Model
08617236af09bdd829bddbd7b90fe9d806a89429	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1	False	Passed	Model Under Test Equivalent Model
b208dd8c9d7355f1d676f55376a0fe7d1c5d71fb	Apalache	Constant	Def2	True	Passed	Model Under Test Equivalent Model
efb9d7f91e75d64800f03b83d3a921b92441cca2	Apalache	Constant	Def2	False	Passed	Model Under Test Equivalent Model
447a0237d99b6c9743096f231a4f484acabebc7f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef2	True	Passed	Model Under Test Equivalent Model
c0984d44e62aaf077f9c8087f5b39256e8fa3d45	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef2	False	Passed	Model Under Test Equivalent Model
80b6d29fe93c8dff158fcf33d1889d5e8bf3afd7	Apalache	Constant	Def1Recursive	True	Passed	Model Under Test Equivalent Model
592e9e8a7ea4e0e83a260cc6efd924d732a4cc73	Apalache	Constant	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b4915ad98b84088781bdd5015665987bd465cfb6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
cf79686a107ec7e1b6cc11e688432a33fb5c03b6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
f54e82cd12ebca8df13adf0b4492e28aeb91c1b0	Apalache	Constant	Extends	True	Passed	Model Under Test Equivalent Model
87ba973c9c8b4968e03418b91f0ce102cc3bd56c	Apalache	Constant	Extends	False	Passed	Model Under Test Equivalent Model
ddc96dbc4b64e1786491945d72d2eafbac81f861	Apalache	Constant	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
5b049dc45cad8234e07830bb079efff1e7e54274	Apalache	Constant	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
5d5e84435804e79a68e07c0dfd5f551b250416aa	Apalache	Constant	Constant	True	Passed	Model Under Test Equivalent Model
72cb3b57850517852df9783a41d50191f9f7ec7e	Apalache	Constant	Constant	False	Passed	Model Under Test Equivalent Model
4c3a5a66fdf4956b1a64c2cd7107f19d5b513748	Apalache	Constant	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
33e7d75749a54e458135bf359b115fdda6eb9574	Apalache	Constant	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
b7817f5a80e07c45580f5f57a53e156c356251f1	Apalache	Constant	ConstantRank1	True	Passed	Model Under Test Equivalent Model
1a4a08ef829385b1c50813881464b2287c20825a	Apalache	Constant	ConstantRank1	False	Passed	Model Under Test Equivalent Model
8d32a5977f0f96d0ecbf9f8c246f9e3a1d9a3fce	Apalache	Constant	Instance	True	Passed	Model Under Test Equivalent Model
1e82095b3ff76f538578b9aa87b85fb92c540fc5	Apalache	Constant	Instance	False	Passed	Model Under Test Equivalent Model
b706147ad1f73dbed8c2fccb5e2df391498e69ab	Apalache	Constant	InstanceWith	True	Passed	Model Under Test Equivalent Model
fb6bf2991fd16870dc0e94c8ef5aca6edc08937a	Apalache	Constant	InstanceWith	False	Passed	Model Under Test Equivalent Model
99a0e5e807e7416e7979f9b15e76c01e2beef15c	Apalache	Constant	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7ab73cfff59faf78f57c95ab29c2603fae1cde00	Apalache	Constant	InstanceNamed	False	Passed	Model Under Test Equivalent Model
31642d818309d90c680641ca334c0c98da35efd6	Apalache	Constant	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
0569c8b1aa151bfe812a1d947bb5629e27914b81	Apalache	Constant	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
03886f0012832242035880e5849e2101728384bc	Apalache	Constant	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
64169b8c11814e7bc0eff3ecb4870cf46688b566	Apalache	Constant	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
166dcebeb15b2196c06555173741cb461ca9f437	Apalache	Constant	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
dc16ebc19b928f20b82c2704a0574417d4661526	Apalache	Constant	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
a4b33743c9b3a276cf393a20be879b6228d765f4	Apalache	Constant	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
08f5d6497a1283f5f9bf71240e149bb4fb3b5315	Apalache	Constant	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
8c24eb12313b3b1386cdbf4cfc17e57885d22fa7	Apalache	Constant	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
a9f39d770f2f55ea6d1e101ee4dec032796d5d91	Apalache	Constant	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
57bd2cbd62a5de21b3b920935a7b53fbaed8e94d	Apalache	Constant	Cross2	True	Passed	Model Under Test Equivalent Model
9bf15066470575745126b1a6348f690af04c4730	Apalache	Constant	Cross2	False	Passed	Model Under Test Equivalent Model
2f21bc1a04e371c732193685d3b946d15e672d88	Apalache	Constant	Cross3	True	Passed	Model Under Test Equivalent Model
a2e06e2f81ba730581eed59f45947da81d7b7277	Apalache	Constant	Cross3	False	Passed	Model Under Test Equivalent Model
0a71e982c41a8fdc506fea64674a8d6089611df5	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))	Constant	FunSet	True	Passed	Model Under Test Equivalent Model
f4f28900d03d76bd5dc28b341f096448b9a07ede	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))	Constant	FunSet	False	Passed	Model Under Test Equivalent Model
2ef80eea0e0c954aa92ed3b988ba959cc96955eb	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)	Constant	RecordSet	True	Passed	Model Under Test Equivalent Model
e1e783757670d3b2fb000d16c0ca9e139f11b2e6	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)	Constant	RecordSet	False	Passed	Model Under Test Equivalent Model
982d3317b3662c02910ccba3e8c75863842bd9ad	Apalache	Constant	SetDiff	True	Passed	Model Under Test Equivalent Model
207ddef06de8a79ba424836f1b662f392456ea05	Apalache	Constant	SetDiff	False	Passed	Model Under Test Equivalent Model
8da36dc7512c9b94c83ae9cf018ff7187b19450f	Apalache	Constant	SetUnion	True	Passed	Model Under Test Equivalent Model
0db4733b7920f45dd7bb1a6777365fd67e6ab0c1	Apalache	Constant	SetUnion	False	Passed	Model Under Test Equivalent Model
fa415e86ed0593d803cf847948dacf7c9fcff8a6	Apalache	Constant	SetIntersect	True	Passed	Model Under Test Equivalent Model
a7017cb5937fb7ab6ef1f85774f54ae67af8eedd	Apalache	Constant	SetIntersect	False	Passed	Model Under Test Equivalent Model
c7d010bc39d687b5e54d80093ec35e0b9a8fcfe2	Apalache	Constant	SubsetEq	True	Passed	Model Under Test Equivalent Model
d37a36590b8d62d8bc00fb299ef777a0de66f8bb	Apalache	Constant	SubsetEq	False	Passed	Model Under Test Equivalent Model
e478bc98aa9104da20c9eff254fbf00e12c1d401	Apalache	Constant	IfCond	True	Passed	Model Under Test Equivalent Model
aab7ee1873d503ddf564d24f20174f89240c1014	Apalache	Constant	IfCond	False	Passed	Model Under Test Equivalent Model
f813bc2d515bb7b8dbafac2b40aff5004be5eb2d	Apalache	Constant	IfThen	True	Passed	Model Under Test Equivalent Model
85f36be59da6d4e8be046849aa4f7cee1416462a	Apalache	Constant	IfThen	False	Passed	Model Under Test Equivalent Model
3d6a9416499716b53cc523d104e6e1f7fc002d09	Apalache	Constant	IfElse	True	Passed	Model Under Test Equivalent Model
e658703c97382dc11887fbcc6b027e87e33d1e02	Apalache	Constant	IfElse	False	Passed	Model Under Test Equivalent Model
ca6c1fd94417f2d9b4623434587eb479efaf6dd1	Apalache	Constant	Subset	True	Passed	Model Under Test Equivalent Model
c77e1ad5cca7382d090b1986ac49795e88a93dc8	Apalache	Constant	Subset	False	Passed	Model Under Test Equivalent Model
65279afbc1e1be09d22ff753d4afce5a9afc4895	Apalache	Constant	Domain	True	Passed	Model Under Test Equivalent Model
f7d55417b41b07e1352ed8e45cee402845e68fbc	Apalache	Constant	Domain	False	Passed	Model Under Test Equivalent Model
a2fd03945f8a82b703865a8191afb9202d6834da	Apalache	Constant	Union	True	Passed	Model Under Test Equivalent Model
2548e12dc3285ad958cc8d1f5f3d3fe37bc0d608	Apalache	Constant	Union	False	Passed	Model Under Test Equivalent Model
c7cd4b28c0098f65f12ebd1c0fd5d1a96909ab75	Apalache	Constant	Equivalence	True	Passed	Model Under Test Equivalent Model
8ff753205d8fdcfe24efbd25ee58f09d6d0b25a6	Apalache	Constant	Equivalence	False	Passed	Model Under Test Equivalent Model
0e3c4ae11c9de01c4e16a08db413c4cf60df1560	Apalache	Constant	StringEmpty	True	Passed	Model Under Test Equivalent Model
fd135a00a4caa5d48cb6f539776a1d2a9e27c5b8	Apalache	Constant	StringEmpty	False	Passed	Model Under Test Equivalent Model
4989f2eff5f66fd9599f1552a74e5addf2f9a376	Apalache	Constant	String	True	Passed	Model Under Test Equivalent Model
8471a56d80d2e5a4ca90b2f8ba11ea2dd3352808	Apalache	Constant	String	False	Passed	Model Under Test Equivalent Model
68abf4910499f1d7cd22d3e659e86fe8a50a2f77	Apalache	Constant	SeqLen	True	Passed	Model Under Test Equivalent Model
5f6d8cca86e102585073bcf71bde0116acb32975	Apalache	Constant	SeqLen	False	Passed	Model Under Test Equivalent Model
8153ff7ea68fd0a7c27bdd9508b4fbea5de3753b	Apalache	Constant	SeqConcat	True	Passed	Model Under Test Equivalent Model
65d87087b66b73d08541a6e29e9e88cd949bc4da	Apalache	Constant	SeqConcat	False	Passed	Model Under Test Equivalent Model
2206e5689b7c578f6accf457e58405fa11f42e27	Apalache	Constant	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
f02be9160f4b487b4dbce060ed3cd5866fd2e49a	Apalache	Constant	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
ab9a5a34eddd92d45db2f57abc19db6070efbb20	Apalache	Constant	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
ce5c4902ebeb36e185e29a3daae8b0203c8ab264	Apalache	Constant	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
4ce666bd2e976a677bc2dc4782d79a31fb822435	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	Constant	NumRange	True	Passed	Model Under Test Equivalent Model
8a4baa2eacbc81957fd07a24b7eba74385703b37	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	Constant	NumRange	False	Passed	Model Under Test Equivalent Model
578db5d627b6b4a5ae8effa44099abd31eb9e2fb	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Constant	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
2224f0c40272875b6226aaa0a400ad687c40e7f7	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Constant	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
f387deaeaa4ba21aee2aa0ac8b28b5b2f698a91b	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]]	Constant	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
90c00019f974d4dbc7c38701c40bdcee4f987f0d	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]]	Constant	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
45beeeb4753d06bd0f01514b1c2a16826f1f6926	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Constant	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
b657c06c52e6670765e47e057c3ee45069b3a77c	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Constant	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
d63a9cdacb9bec2a6cb9066ff1e1d7c04662cbef	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Constant	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
eaf7802795731aa84a136499e59fe376d6e22723	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Constant	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
46af2ae2b7565d3163d148fc6c70f7198555ce06	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Constant	TlcEval	True	Passed	Model Under Test Equivalent Model
781dd8023fec9d21ad0b77e16de89b5dfda6d3cf	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Constant	TlcEval	False	Passed	Model Under Test Equivalent Model
5c38a8efdd67537b339ada1cf7ebae103e9110ae	Apalache	Constant	BagBagToSet	True	Passed	Model Under Test Equivalent Model
3d9d27eb0d5aebab5ef89c69e64895097e365f76	Apalache	Constant	BagBagToSet	False	Passed	Model Under Test Equivalent Model
78d10328d630694dfcd2cf29990cba383a57595b	Apalache	Constant	BagSetToBag	True	Passed	Model Under Test Equivalent Model
775f534e916571c1dbfda94885f1c926a41fc64c	Apalache	Constant	BagSetToBag	False	Passed	Model Under Test Equivalent Model
300ca175d0ba0bf32e375dfe8b888ce43ad2e32d	Apalache	Constant	BagBagIn	True	Passed	Model Under Test Equivalent Model
21410d8c4dcc3be0fa7d0cb3833ecafa60052817	Apalache	Constant	BagBagIn	False	Passed	Model Under Test Equivalent Model
b13dc209c35b75588ddf0af11742fe933f37959c	Apalache	Constant	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
60cf328adee3184605846e30b14544d70e5de073	Apalache	Constant	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
8c2ef6d5380ef988bf72664ad21ec8a1e482a83a	Apalache	Constant	BagAddBag	True	Passed	Model Under Test Equivalent Model
a19f71e372c56bbad6fea128be6e7d9a2665fde9	Apalache	Constant	BagAddBag	False	Passed	Model Under Test Equivalent Model
3b5b96f98f7c04e106d31854ebffe299187a3a96	Apalache	Constant	BagBagSub	True	Passed	Model Under Test Equivalent Model
50a368548e55d753dd3849963846a7ca12787ef3	Apalache	Constant	BagBagSub	False	Passed	Model Under Test Equivalent Model
08d1c2553eafae97d344e4a85be329ae2fc5c63b	Apalache	Constant	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
d464eb65551fadf7d43a2b093d63fbe045aca0ee	Apalache	Constant	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
52864ab0a252c94ca9dfb56a5348fe952fd8caad	Apalache	Constant	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
4ea72fe228ee8c62e51d5fba6583b9372dbacd75	Apalache	Constant	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
67d5dfb8eb7f190867386cfcadeccb66556fd325	Apalache	Constant	BagBagUnion	True	Passed	Model Under Test Equivalent Model
adba8dd8bf1f334919822b3087a6de3d0cb6b921	Apalache	Constant	BagBagUnion	False	Passed	Model Under Test Equivalent Model
1644986eeed9a332b1c5ddfa1b2ebbed7322adca	Apalache	Constant	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
ec769e1e8401fcc95320e805f692ab5c6a15cc9d	Apalache	Constant	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
6a9768ddb8bd6bd47902075027bddda29d336786	Apalache	Constant	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
a9acdb1ef0bc14f804e06e13897542bc7228f003	Apalache	Constant	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
5c13e0d942038ccbde957509b2fae1d9605a3fcb	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Constant	BagSubBag	True	Passed	Model Under Test Equivalent Model
1e19ad6fb6c9daad009828dac5cbbb587041e69f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Constant	BagSubBag	False	Passed	Model Under Test Equivalent Model
677176c770397b8ea4f487eb50e28a2e5fb87088	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)	Constant	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
0aa62e3042f2c6898608d52e4624c29c0cc4bc61	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)	Constant	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
a8bedccf54e7e3671373518600e323e22b9cb484	Apalache	Constant	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
4eb072d2cfa3acd3211693fad5298b1fedfd5b81	Apalache	Constant	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
7d0c5acb441de688f3fdb838a121a8faa6f9cfbc	Apalache	Constant	SeqHead	True	Passed	Model Under Test Equivalent Model
45027525c9daac475db0d6f379e3d0b0d56e5fd6	Apalache	Constant	SeqHead	False	Passed	Model Under Test Equivalent Model
ed00b33cc5edde4b895e2172f222ee066625c1dc	Apalache	Constant	SeqTail	True	Passed	Model Under Test Equivalent Model
e17d71f419666b7da6d350aac89678b352ab0abb	Apalache	Constant	SeqTail	False	Passed	Model Under Test Equivalent Model
199051aea8c5d371a79630ce380e4a7664de9975	Apalache	Constant	SeqAppend	True	Passed	Model Under Test Equivalent Model
515f75e9e4f949f8cb66f5fbef2a41e172078a24	Apalache	Constant	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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