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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
9bd254bd2f8d58aa088440e8584273d028156c97	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfElse	OneLineComment	True	Passed	Model Under Test Equivalent Model
317158a570b33a7323432765731f790582504f82	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfElse	OneLineComment	False	Passed	Model Under Test Equivalent Model
e007ce4fefe6416d65948fda46667c0f6d8f90f3	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfElse	MultiLineComment	True	Passed	Model Under Test Equivalent Model
78dadfdb93967df73c9933829fdda1c952e71eaa	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfElse	MultiLineComment	False	Passed	Model Under Test Equivalent Model
57a8dfbe5fe297d0d6b9c3b86a29d51a541deb26	Apalache	IfElse	BoolTrue	True	Passed	Model Under Test Equivalent Model
06fa88755eb04778fda4ab676b4750ac65b50e17	Apalache	IfElse	BoolTrue	False	Passed	Model Under Test Equivalent Model
370f155ee014637f19b3c076cb107552383bb529	Apalache	IfElse	BoolFalse	True	Passed	Model Under Test Equivalent Model
2bff9282cc35e24ddc669d722433b29895731252	Apalache	IfElse	BoolFalse	False	Passed	Model Under Test Equivalent Model
604a57d74633a957f55937b98a4c6b3c9fd9302f	Apalache	IfElse	BoolSet	True	Passed	Model Under Test Equivalent Model
c238ceb46ec0c625cf557918760f8895b438c608	Apalache	IfElse	BoolSet	False	Passed	Model Under Test Equivalent Model
6454ad35d2548e657e0cd22b9ec5cd3c69180948	Apalache	IfElse	And	True	Passed	Model Under Test Equivalent Model
fdf36695c44cbc1b3d4170cc07a2698dff2d5494	Apalache	IfElse	And	False	Passed	Model Under Test Equivalent Model
7725ba77b7bf36797506aea124f3a8cd7c970027	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	IfElse	AndMultiLine	True	Passed	Model Under Test Equivalent Model
ce11007b2a5ab6b6237f905b7f181f883ec412ce	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	IfElse	AndMultiLine	False	Passed	Model Under Test Equivalent Model
a84a48e9a8606f100e8ece8011f39e6c9354a571	Apalache	IfElse	Imply	True	Passed	Model Under Test Equivalent Model
4035443a07ea8f78b805a798a9fca1f926104b4b	Apalache	IfElse	Imply	False	Passed	Model Under Test Equivalent Model
0d5408fc42709c930937894a009171dab3acef10	Apalache	IfElse	Not	True	Passed	Model Under Test Equivalent Model
db2153d34158d93b4d032ca0af6663184d7f5976	Apalache	IfElse	Not	False	Passed	Model Under Test Equivalent Model
2e8086dedbb1821396613dc0c606e74cecf1e534	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	IfElse	Or	True	Passed	Model Under Test Equivalent Model
96991571a24075fbbe1eb264155c9d444b4fc5ae	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	IfElse	Or	False	Passed	Model Under Test Equivalent Model
d66d74d6eb458c1d2c515322a6657a1022e480af	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	IfElse	OrMultiLine	True	Passed	Model Under Test Equivalent Model
2423332a4b8fe836a5b4794a1a905039febe5475	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	IfElse	OrMultiLine	False	Passed	Model Under Test Equivalent Model
e58e6a53b91c266c1b0e16a76e2b5302106ae13e	Apalache	IfElse	Eq	True	Passed	Model Under Test Equivalent Model
c019f33c12467d6c935895120d1e17776da59ce1	Apalache	IfElse	Eq	False	Passed	Model Under Test Equivalent Model
5deff266d37fab9586e80cdc6ecdb92db940e9c0	Apalache	IfElse	Ne	True	Passed	Model Under Test Equivalent Model
be97ee264181623d2d8e069903d3bbb5e4b8121f	Apalache	IfElse	Ne	False	Passed	Model Under Test Equivalent Model
64e3117a356acbbd19cd880531983f6ca2149b78	Apalache	IfElse	Let	True	Passed	Model Under Test Equivalent Model
fc4fd3b12dcef2d9113f5687b35ca0dea6a0e150	Apalache	IfElse	Let	False	Passed	Model Under Test Equivalent Model
af8038bf22c97b3a725570074cee0d0ac46d05a6	Apalache	IfElse	SetEmpty	True	Passed	Model Under Test Equivalent Model
f515cc689cbe7174398f515805e4aecc664c76b8	Apalache	IfElse	SetEmpty	False	Passed	Model Under Test Equivalent Model
05f6979663158709885af89e0786faf4cd44cdcf	Apalache	IfElse	Set0	True	Passed	Model Under Test Equivalent Model
70625b95c7967e121363a65a20f03d361e80a027	Apalache	IfElse	Set0	False	Passed	Model Under Test Equivalent Model
1fd581b9bfc95d775d99fb648a288e41ef43b992	Apalache	IfElse	Set1	True	Passed	Model Under Test Equivalent Model
fc37752c680821654c8fec8d96e48bb9e9f13711	Apalache	IfElse	Set1	False	Passed	Model Under Test Equivalent Model
8e6cc3e8790ec3517faf62472432c5c7fd1fb736	Apalache	IfElse	Set2	True	Passed	Model Under Test Equivalent Model
9c1ec197763536493fe203c9d3af264d7fa520df	Apalache	IfElse	Set2	False	Passed	Model Under Test Equivalent Model
e2260da99156650ab65c9854b22418663c5587ca	Apalache	IfElse	Fun	True	Passed	Model Under Test Equivalent Model
49555ca8d86eeca066c5ddf6721e44e491f6d776	Apalache	IfElse	Fun	False	Passed	Model Under Test Equivalent Model
7e0e6c6367e98c1e3ddfa3c53f78785f92c81c11	Apalache	IfElse	In	True	Passed	Model Under Test Equivalent Model
a393f0a6ba4fb73d123e90b644b9294c8b2218a9	Apalache	IfElse	In	False	Passed	Model Under Test Equivalent Model
afcea0c50c15534365422ae97d9984156a607b97	Apalache	IfElse	NotIn	True	Passed	Model Under Test Equivalent Model
3daa4d8375f08f327143649bb1f61f4cb0a00b8b	Apalache	IfElse	NotIn	False	Passed	Model Under Test Equivalent Model
e73ac132d11c1db2e4b73d56da435e3941d51515	Apalache	IfElse	Exists	True	Passed	Model Under Test Equivalent Model
d3bebae73f36834d51ff9b36f46af2c2f8f294f2	Apalache	IfElse	Exists	False	Passed	Model Under Test Equivalent Model
27c2fb4513f41d093ffacafc6ee17ce53bb92187	Apalache	IfElse	Forall	True	Passed	Model Under Test Equivalent Model
e64becb235b46da117356421d24eee99275ac70f	Apalache	IfElse	Forall	False	Passed	Model Under Test Equivalent Model
7a284ea3e13e5987c62d276e90dca50120eaddfa	Apalache	IfElse	Choose	True	Passed	Model Under Test Equivalent Model
b0951aacbab1adcdb238a196625fdbfce8656d7f	Apalache	IfElse	Choose	False	Passed	Model Under Test Equivalent Model
0f792d42e0966210ae48651adc8e4caaf2ffb62f	Apalache	IfElse	Record	True	Passed	Model Under Test Equivalent Model
ae38c85cdb70be95e72feff31f6fcf4682d8c47c	Apalache	IfElse	Record	False	Passed	Model Under Test Equivalent Model
eed71fe1055f3ea50d426355c97fd194643e0b78	Apalache	IfElse	Tuple	True	Passed	Model Under Test Equivalent Model
ca62bbc3a21f16d9fc592687c86ad8bea4b9a195	Apalache	IfElse	Tuple	False	Passed	Model Under Test Equivalent Model
f0a7101d75a73811af424c96f610be999f645649	Apalache	IfElse	TupleEmpty	True	Passed	Model Under Test Equivalent Model
46da69983fcee6b3fab5fa9f39026c3707896e1d	Apalache	IfElse	TupleEmpty	False	Passed	Model Under Test Equivalent Model
1e7c2f09a55503d3845ba876ad917dcdec175ebb	Apalache	IfElse	FunApp	True	Passed	Model Under Test Equivalent Model
8fd35c0f435dd5688e1aeedcc61bdd986bf6262b	Apalache	IfElse	FunApp	False	Passed	Model Under Test Equivalent Model
1f816d2c009cc706e9a795d4d188803cf84144fc	Apalache	IfElse	Prime	True	Passed	Model Under Test Equivalent Model
eb6186604a51c317c0c50cc8df60f7d701f7e274	Apalache	IfElse	Prime	False	Passed	Model Under Test Equivalent Model
af6abb23df4da8460a32aaa88f15a9c228d9bc63	Apalache	IfElse	NumZero	True	Passed	Model Under Test Equivalent Model
8c4745a205dd656c1222429f541149ae74e979af	Apalache	IfElse	NumZero	False	Passed	Model Under Test Equivalent Model
4776037556e8a96e6203d06c3ac876a951cfd4e6	Apalache	IfElse	NumOne	True	Passed	Model Under Test Equivalent Model
c051d59af9cb278ad43e1a19d3da5c99334f02bd	Apalache	IfElse	NumOne	False	Passed	Model Under Test Equivalent Model
26f03dbd5330d11c59e0137d1598b3b50a0d82cd	Apalache	IfElse	NumMaxInt	True	Passed	Model Under Test Equivalent Model
50866fc851160ecb2ae829a70be5a3d5541ca0e7	Apalache	IfElse	NumMaxInt	False	Passed	Model Under Test Equivalent Model
60d8ccab4a28ae0009303af5cb2483f3c96bb53d	Apalache	IfElse	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b2e91e8ab81daf629894f043b76bf0cdfefa6f35	Apalache	IfElse	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
fed3755b18f54cffd27ab492733e6c05b18216da	Apalache	IfElse	NumPlus	True	Passed	Model Under Test Equivalent Model
2064b321b5bc878f51c0a6fb445736500b5d6a04	Apalache	IfElse	NumPlus	False	Passed	Model Under Test Equivalent Model
37d27cce609a1df49099ebb4ad86dadc223ab49d	Apalache	IfElse	NumMinus	True	Passed	Model Under Test Equivalent Model
94609f1b020d2a7f2943844f2dce2f87721a8231	Apalache	IfElse	NumMinus	False	Passed	Model Under Test Equivalent Model
ed2524deb085cd463f6cfd987d09fa4adc818a96	Apalache	IfElse	NumMul	True	Passed	Model Under Test Equivalent Model
688845db5f235e0f2f9b577cdd052f74002e7448	Apalache	IfElse	NumMul	False	Passed	Model Under Test Equivalent Model
d1d35e50f7747e18321f9066756642aa3fb29352	Apalache	IfElse	NumDiv	True	Passed	Model Under Test Equivalent Model
8481ca159537473ad6787214b85f526c7f95ef0b	Apalache	IfElse	NumDiv	False	Passed	Model Under Test Equivalent Model
73d0e3f57dff3dbcc7545219c6e120ad4c8ab866	Apalache	IfElse	NumMod	True	Passed	Model Under Test Equivalent Model
01ffdf6a346e466355e8ab0716b8372f2b538e4a	Apalache	IfElse	NumMod	False	Passed	Model Under Test Equivalent Model
afd55931699f1e50639e212d0f89035f34424688	Apalache	IfElse	NumPow	True	Passed	Model Under Test Equivalent Model
8de5174648c24af0a5a9777ea90e8804783531e8	Apalache	IfElse	NumPow	False	Passed	Model Under Test Equivalent Model
1f92c0d24cfa98d50816ea83ce3a85cb841ed636	Apalache	IfElse	NumGt	True	Passed	Model Under Test Equivalent Model
7bfcaa8fdfe14347ffd72deb086f2a7c0cb4e5a3	Apalache	IfElse	NumGt	False	Passed	Model Under Test Equivalent Model
f3c080388e78624fad72878a08f9935cd25f8fbe	Apalache	IfElse	NumGe	True	Passed	Model Under Test Equivalent Model
c9484fa1f02da6625c2c66c6a4f06d19d2c78f9d	Apalache	IfElse	NumGe	False	Passed	Model Under Test Equivalent Model
5bd94c08f0f0c51fc9590fa982d4c3c8f5067cba	Apalache	IfElse	NumLt	True	Passed	Model Under Test Equivalent Model
98b23bcf54c2ebd93e2492172044442a418b4b43	Apalache	IfElse	NumLt	False	Passed	Model Under Test Equivalent Model
73e3261235966e01889662d8454a066d9cdba140	Apalache	IfElse	NumLe	True	Passed	Model Under Test Equivalent Model
33be60c60fd47e4ed12dcb9b0045da3b4d79ad69	Apalache	IfElse	NumLe	False	Passed	Model Under Test Equivalent Model
b7e659eb86d958432178f3aef61f6151043fe9c6	Apalache	IfElse	DefFun	True	Passed	Model Under Test Equivalent Model
13f5ad37431d216e9b91b5836bbc021c4eb052c2	Apalache	IfElse	DefFun	False	Passed	Model Under Test Equivalent Model
82b755fd012481e9d0b2c5173ff923720de26cdc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDefFun	True	Passed	Model Under Test Equivalent Model
d61742df0f3f5445cf9563f622d1c7bcf0a681e4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDefFun	False	Passed	Model Under Test Equivalent Model
02972dc1ae8703adbed855f53c8359a277966ebf	Apalache	IfElse	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
3f5407d2411c36b209e318a303c8b8ceda6cfe1b	Apalache	IfElse	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
d48f799d460f16a24de5197ce5d6b2eb39a62d4b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
11cbe2a46c9ff191cd987e35fb486eefcd375067	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
e357fbed40e56afc181012a2d01ec20f94dc3362	Apalache	IfElse	Def0	True	Passed	Model Under Test Equivalent Model
3c25591551697502c5e3891b38d11f619abbe587	Apalache	IfElse	Def0	False	Passed	Model Under Test Equivalent Model
5dfd8b147ef8248197ae7b86bda8650c6e626d40	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef0	True	Passed	Model Under Test Equivalent Model
e0f0e09792fc022039e66f49574f714a167decf9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef0	False	Passed	Model Under Test Equivalent Model
1b80c6b60aea112e4a26ae25127464d595edd7be	Apalache	IfElse	Def1	True	Passed	Model Under Test Equivalent Model
54c52ab798ba1ee894dcc3af66afa0adda16f2c9	Apalache	IfElse	Def1	False	Passed	Model Under Test Equivalent Model
de9b718d282463b12ed14acb094d6fe0ddb94284	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1	True	Passed	Model Under Test Equivalent Model
97fa22bc8a0208e86c75a9eed03f9bcdb55cf6b0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1	False	Passed	Model Under Test Equivalent Model
38585163e5f69f08f98bc3e3ea24b8b3c8bde3e2	Apalache	IfElse	Def2	True	Passed	Model Under Test Equivalent Model
1d53b240829344b8ca0d23471f34421bb31a0023	Apalache	IfElse	Def2	False	Passed	Model Under Test Equivalent Model
ffc15c8d56850594fdf6471988247bd8f0c81719	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef2	True	Passed	Model Under Test Equivalent Model
7bec2e9299fdabc9171f915f4b0141d5977c7df8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef2	False	Passed	Model Under Test Equivalent Model
f213d83d7c4c625b770ab9154c6b1eb3efadb2ec	Apalache	IfElse	Def1Recursive	True	Passed	Model Under Test Equivalent Model
051ab1fb7ae020f3551c86dfd1f54dd15f5da601	Apalache	IfElse	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a5222dc42979acb3d005bbe2ce3edb00c8f265b2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
f32ef7df17e422f5ad6f69d6a603bf75a701359f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
fb4ad2d84c8abd2c33caf5f4c527607c876a17a6	Apalache	IfElse	Extends	True	Passed	Model Under Test Equivalent Model
e02a97146499d08d4026fecdf845982cd9e690ef	Apalache	IfElse	Extends	False	Passed	Model Under Test Equivalent Model
c1f6bf5eaf050f74e0f861e868b84496b4a33b2d	Apalache	IfElse	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
e960f0c14c07f3cd95879999052a27776c27ee61	Apalache	IfElse	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
06d8b9fbcb9bcfa46167038a34560992e51933fc	Apalache	IfElse	Variable	True	Passed	Model Under Test Equivalent Model
eeaff06690c560d40912b64ece47c75b494fb0c7	Apalache	IfElse	Variable	False	Passed	Model Under Test Equivalent Model
1d599e93aabc38e36712ba035112ed2b9918d363	Apalache	IfElse	Constant	True	Passed	Model Under Test Equivalent Model
8bd2d64e819ee1559d520b3b33b53d8876c063e0	Apalache	IfElse	Constant	False	Passed	Model Under Test Equivalent Model
0d4972f58689683fdb3e768525e10fc2eadb659e	Apalache	IfElse	ConstantRank1	True	Passed	Model Under Test Equivalent Model
76b51c2ea74fd971faff2a3eeee2a085ff66a7f2	Apalache	IfElse	ConstantRank1	False	Passed	Model Under Test Equivalent Model
56784229d6a87a89ae0478f8adcbeb962972f765	Apalache	IfElse	Instance	True	Passed	Model Under Test Equivalent Model
fe9b7bcad16212c83f0e17e1991fde8dba2f3beb	Apalache	IfElse	Instance	False	Passed	Model Under Test Equivalent Model
8e85c5296ec741b98c1ce41947d64f7f9f309e97	Apalache	IfElse	InstanceWith	True	Passed	Model Under Test Equivalent Model
aa09a2dd4e13ff729df0335147907be8be4e47ee	Apalache	IfElse	InstanceWith	False	Passed	Model Under Test Equivalent Model
bc13b77c25a48ba9c7ef158d3af666bb0018fda8	Apalache	IfElse	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e24590389b658a1d56d20201eb0daa1c00d738c7	Apalache	IfElse	InstanceNamed	False	Passed	Model Under Test Equivalent Model
c4168525b0b93c8327f7075916ec2e856e9cb078	Apalache	IfElse	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
1859785d3914520f1a6d87b4dd647b790ff19eab	Apalache	IfElse	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
1acaeb91c86e9f2bd7bd60615290713ae18bd5e7	Apalache	IfElse	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
0c3169b28c202510fecaf1f3c1199b9b55966636	Apalache	IfElse	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
e2477718868a4c48752e9d634575ea50eae04c6f	Apalache	IfElse	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
9ceba54d463c445987a318d4f61a2afce6c6267f	Apalache	IfElse	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
0aaaab4e546c29ea33a135740eaeaa5594eaaee3	Apalache	IfElse	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
4c5be966d64a5c1376c598acae57e64c2215acb6	Apalache	IfElse	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
998d9e6b7e343785ca44bed9b18f9afb0bf4608b	Apalache	IfElse	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
e81119c2ceefdf8ce2847b818adffb4435fdceb1	Apalache	IfElse	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
3bbd9de54dce11bcc9825249006313b6fa74ac82	Apalache	IfElse	Enabled	True	Passed	Model Under Test Equivalent Model
b4e88c4ace7a8d4ea4ba5ae2a70e148a48aa56b3	Apalache	IfElse	Enabled	False	Passed	Model Under Test Equivalent Model
2f94b1643eed8192d901c4a6ee0ab197ebe7ef34	Apalache	IfElse	Cross2	True	Passed	Model Under Test Equivalent Model
31660ecdc786018a3250f5ce1d07d3114136dad5	Apalache	IfElse	Cross2	False	Passed	Model Under Test Equivalent Model
7e9c6be4b44b8c7669ddb652888b08bb361d0000	Apalache	IfElse	Cross3	True	Passed	Model Under Test Equivalent Model
44ac59c27e58dec0b5490bde785f58ab815f9250	Apalache	IfElse	Cross3	False	Passed	Model Under Test Equivalent Model
8fe4332ddc9b4166d3fa84278c74c593ed68743d	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))	IfElse	FunSet	True	Passed	Model Under Test Equivalent Model
2f32c0c80211a2aff2835e2ce01fe33bfe4ee1ef	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))	IfElse	FunSet	False	Passed	Model Under Test Equivalent Model
4bf7521854f458080b1146636b64afe49a779293	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)	IfElse	RecordSet	True	Passed	Model Under Test Equivalent Model
24b9564fef678bcd4799bf09c37215054595af81	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)	IfElse	RecordSet	False	Passed	Model Under Test Equivalent Model
80d29cb1fe4db5606bae77112cb1356c87f70cbe	Apalache	IfElse	SetDiff	True	Passed	Model Under Test Equivalent Model
7a1b428c6078cbd3d6a94067652e3fe45dad41f5	Apalache	IfElse	SetDiff	False	Passed	Model Under Test Equivalent Model
cede0d0cea85d24d0a16fc8fd511075ad8cfbb88	Apalache	IfElse	SetUnion	True	Passed	Model Under Test Equivalent Model
e5cb220e8188f69899794a41dc67c84cbe185479	Apalache	IfElse	SetUnion	False	Passed	Model Under Test Equivalent Model
16b48bc14b363f0788d687f4d3e4ecbe549d80fd	Apalache	IfElse	SetIntersect	True	Passed	Model Under Test Equivalent Model
e6293942c82981f2fb4fc5fc8a34723903815516	Apalache	IfElse	SetIntersect	False	Passed	Model Under Test Equivalent Model
527bb61865a3d5125388f10cc51e9741504915cc	Apalache	IfElse	SubsetEq	True	Passed	Model Under Test Equivalent Model
6b6498a0d0ac2e2c4f116c920fc552bf90903c8c	Apalache	IfElse	SubsetEq	False	Passed	Model Under Test Equivalent Model
8a732b0ce2bdcec811d100ea1f8e83a2f00e57d7	Apalache	IfElse	IfCond	True	Passed	Model Under Test Equivalent Model
b4c76bf7350ac1ce337e0808fbb10711ce4628bb	Apalache	IfElse	IfCond	False	Passed	Model Under Test Equivalent Model
ab23907dd8a405557eaad84ccd42ca9a5f256f70	Apalache	IfElse	IfThen	True	Passed	Model Under Test Equivalent Model
1d2254649cd20a169d8b3fe1dfff114cde0c1bfd	Apalache	IfElse	IfThen	False	Passed	Model Under Test Equivalent Model
c3bc88179452281350f3e4362aeac941bdc76c98	Apalache	IfElse	IfElse	True	Passed	Model Under Test Equivalent Model
b0cb6f2a1f64dc6ef41af878d2d69ebd4fcb9f7e	Apalache	IfElse	IfElse	False	Passed	Model Under Test Equivalent Model
1a9fe566d89ffd34563515faf1dcdb72db68645a	Apalache	IfElse	Subset	True	Passed	Model Under Test Equivalent Model
078557b4958912cb0296b453d8cc45fb06b8d5e6	Apalache	IfElse	Subset	False	Passed	Model Under Test Equivalent Model
684d128ea937a875f870ccdd543039241068e538	Apalache	IfElse	Domain	True	Passed	Model Under Test Equivalent Model
6d7cea976dd13b94fbd1484f8748b80fca3b53c5	Apalache	IfElse	Domain	False	Passed	Model Under Test Equivalent Model
3f9169ec1f2715217d7c6b607a61be23f9125f8d	Apalache	IfElse	Union	True	Passed	Model Under Test Equivalent Model
69e902de708ca06e1544d670dbfaa1a14f75a117	Apalache	IfElse	Union	False	Passed	Model Under Test Equivalent Model
1154b08ebc885dbd827ffd265a402d48472f62c2	Apalache	IfElse	Unchanged	True	Passed	Model Under Test Equivalent Model
27292d5de07b5e02158d328e02ab81e57754f02b	Apalache	IfElse	Unchanged	False	Passed	Model Under Test Equivalent Model
b5422a978b6f57fd05927b830fa71d449aadde07	Apalache	IfElse	Equivalence	True	Passed	Model Under Test Equivalent Model
d54dd51bc275bb1620a60355668cde9a27c33d19	Apalache	IfElse	Equivalence	False	Passed	Model Under Test Equivalent Model
1aa5579821db1f18a04109de680de53d9cc03ae4	Apalache	IfElse	StringEmpty	True	Passed	Model Under Test Equivalent Model
efe989313c0db8a44a697df025d5b61881aaeb4c	Apalache	IfElse	StringEmpty	False	Passed	Model Under Test Equivalent Model
76cbd8d6d0ebbb93566cb5923a215dfa8abcd110	Apalache	IfElse	String	True	Passed	Model Under Test Equivalent Model
7001f092255baf1421efe4db0577f80282546723	Apalache	IfElse	String	False	Passed	Model Under Test Equivalent Model
3689a0f5aa9192e6d31e99afadf9d7c3c1c61bff	Apalache	IfElse	SeqLen	True	Passed	Model Under Test Equivalent Model
68f063f7c481e9eb1125fd310e7e8aa2880185cd	Apalache	IfElse	SeqLen	False	Passed	Model Under Test Equivalent Model
6060b17184b8558ba532a4568e5a2b370467c963	Apalache	IfElse	SeqConcat	True	Passed	Model Under Test Equivalent Model
a114e9e1a551b737c2d3a72b142d2e5e13bc9bba	Apalache	IfElse	SeqConcat	False	Passed	Model Under Test Equivalent Model
eb370a4e54f4c53cb7ecd0f5c644de3e4e7cd620	Apalache	IfElse	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
0a162de42c5b28d7c01b15ab0aaecaa9737059e0	Apalache	IfElse	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
db2d10d2cb552f62e2dd96065534939376853322	Apalache	IfElse	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
9f6816afe982193225901ffdfba6fbe0ee03bbc5	Apalache	IfElse	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
6391787ac0a733f920ce8e89d4bf1785b3136cf2	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	IfElse	NumRange	True	Passed	Model Under Test Equivalent Model
532dde0e80cd1aa84ed1853418668bdf00912731	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	IfElse	NumRange	False	Passed	Model Under Test Equivalent Model
55e44b110e22c6e0dc208c10b026235f8b5e3e05	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	IfElse	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
dd070a8f9784d2dad1646e1b8fe3da80cb4a0ed9	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	IfElse	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
d1461bbc916cef6d01dacbae25b3f629f8cb34b6	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]]	IfElse	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
50d49cd68847fcfbdf20a74dd6e75aaab33b4435	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]]	IfElse	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
69cd61906479b0a575e34e11ae3a0528b5c26e9c	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	IfElse	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
18ab76c1ce1dd0d9c362baa23021ae40162ff58e	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	IfElse	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
722250c0cd34958c6ba9f7a89210cdd9b4d69389	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	IfElse	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
f66c92e500ea5280f5c53ef8531de18129dc5316	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	IfElse	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
0a75f26c6b5146e14d61325dd8ec61ffdf00df33	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	IfElse	TlcEval	True	Passed	Model Under Test Equivalent Model
1447ecad4c4320cf6d82c264e3e30f7c46232a31	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	IfElse	TlcEval	False	Passed	Model Under Test Equivalent Model
a3265e7df24dbd6a11b6ea398a8d5b08b876497b	Apalache	IfElse	BagBagToSet	True	Passed	Model Under Test Equivalent Model
1d9914411b80f01a3a6ca3f924584eeb8a00c253	Apalache	IfElse	BagBagToSet	False	Passed	Model Under Test Equivalent Model
ccda94e3a548c04537ae753c77261eec26b15c4f	Apalache	IfElse	BagSetToBag	True	Passed	Model Under Test Equivalent Model
d7900c67bf39d5677ebdf7642fa3d8e0e0f2d285	Apalache	IfElse	BagSetToBag	False	Passed	Model Under Test Equivalent Model
213cd059b697fa5767b568cea7f27024172f54d3	Apalache	IfElse	BagBagIn	True	Passed	Model Under Test Equivalent Model
30210cc5eff49d2d27870596f89ab12f89b0bc81	Apalache	IfElse	BagBagIn	False	Passed	Model Under Test Equivalent Model
dadabd2440828a70cd268dd22f126e82a0695f46	Apalache	IfElse	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
66e7d6765721c7cfc7344c7acb719bc55432e844	Apalache	IfElse	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
e8dfcfde3552ba6dfccf3def6ec470f319adb180	Apalache	IfElse	BagAddBag	True	Passed	Model Under Test Equivalent Model
e80e6cfc4b2b91bee4d7ab13b9efea6f1e0365f8	Apalache	IfElse	BagAddBag	False	Passed	Model Under Test Equivalent Model
2210ab1a939a9becaf4999f46dce9e8494bc2bf2	Apalache	IfElse	BagBagSub	True	Passed	Model Under Test Equivalent Model
815dcd6028aacb60433a24933a00a91d75a4866e	Apalache	IfElse	BagBagSub	False	Passed	Model Under Test Equivalent Model
840f17061d73be69488359f9475160aa5b75c418	Apalache	IfElse	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
5964270592fc50d8963d0e0602997f82f4d2eba1	Apalache	IfElse	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
4e5e43a5bda6d542dea7329a865d6a7f321a7b39	Apalache	IfElse	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
359667035343955c47ba3efe375ca14bd2235dc9	Apalache	IfElse	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4eea4da431132bc91b45acec631565ae4b6b1d24	Apalache	IfElse	BagBagUnion	True	Passed	Model Under Test Equivalent Model
b01a9f13af19e9ea2a72b740e78d134e97892954	Apalache	IfElse	BagBagUnion	False	Passed	Model Under Test Equivalent Model
c22585e3798855b493f135e6024b98687af2d6d9	Apalache	IfElse	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
810e497ef22193721bfd10389527ac58d8a5d17e	Apalache	IfElse	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
ea46896dcb1d199f86b9cbae4daf3ea70ea2652b	Apalache	IfElse	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
d6d3d917c2a5a1e70a8f4e5e8a3d6dd41758de29	Apalache	IfElse	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
7db0e0e6f4524b58e27dcb8fb9d5fe64f6c6e461	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	IfElse	BagSubBag	True	Passed	Model Under Test Equivalent Model
f4b660122ca8bb344af4667789fe7d524123b382	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	IfElse	BagSubBag	False	Passed	Model Under Test Equivalent Model
a5189c310c75da7f05fea4338bce8c788a19102d	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)	IfElse	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
339e1ef22cf320215ab23470a9e8be678c8fc0e7	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)	IfElse	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
ae7c566b6a6d663c51be1dbdfd72267aed564d43	Apalache	IfElse	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
a1792fa71e61a72160a41fbdba2ee8846fc04670	Apalache	IfElse	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
86a7bed360a50dd399cae098a877ea6d13f4ad94	Apalache	IfElse	SeqHead	True	Passed	Model Under Test Equivalent Model
293af290a551610f00b588dee0dab22d0a837e20	Apalache	IfElse	SeqHead	False	Passed	Model Under Test Equivalent Model
f6edac514b431c453fdc2b16c432522615ac71f1	Apalache	IfElse	SeqTail	True	Passed	Model Under Test Equivalent Model
10125f95e1e298ef8a3ea767a411b32780999303	Apalache	IfElse	SeqTail	False	Passed	Model Under Test Equivalent Model
78d7e9072debf4bef2fef9e20d3bb73efeae7ed2	Apalache	IfElse	SeqAppend	True	Passed	Model Under Test Equivalent Model
c79aa7f5c4a307ebe39a5b9a15748eb64bd918d3	Apalache	IfElse	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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