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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
87ca53aebbb46ff1d3ab2eed9957b653265cf2fb	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfThen	OneLineComment	True	Passed	Model Under Test Equivalent Model
4663a3a9fac24f166ac8f048ed522f7123592d18	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfThen	OneLineComment	False	Passed	Model Under Test Equivalent Model
f1e308d620647c5a91cfa3b5badfbed8d5b18652	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfThen	MultiLineComment	True	Passed	Model Under Test Equivalent Model
5173e7626e5a0a732705116d8e9d939e420b73c8	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	IfThen	MultiLineComment	False	Passed	Model Under Test Equivalent Model
bdd3572d389b4747ccbe88b72a4e3df314e39be2	Apalache	IfThen	BoolTrue	True	Passed	Model Under Test Equivalent Model
5817176dba841a888697c74cd6af9279e761dfad	Apalache	IfThen	BoolTrue	False	Passed	Model Under Test Equivalent Model
73338903b4f9f82e4164e6677dc2613dac15fcdc	Apalache	IfThen	BoolFalse	True	Passed	Model Under Test Equivalent Model
5426724b9437cca0127cbf17ec7894c21df5478f	Apalache	IfThen	BoolFalse	False	Passed	Model Under Test Equivalent Model
f96071e450cb80494058d93a3fe3fa44e5e0b2e9	Apalache	IfThen	BoolSet	True	Passed	Model Under Test Equivalent Model
090afb0b25c94df771fc4076f660160df0b5fb78	Apalache	IfThen	BoolSet	False	Passed	Model Under Test Equivalent Model
a2af0a53b1686b16361152d46dc57d34fd718c4a	Apalache	IfThen	And	True	Passed	Model Under Test Equivalent Model
9ae75749d9dd835090a4d3018142b86ed4800993	Apalache	IfThen	And	False	Passed	Model Under Test Equivalent Model
538d3c5fccfcccc96573c4b9ea8df44195e05763	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	IfThen	AndMultiLine	True	Passed	Model Under Test Equivalent Model
68431bc0bc122f01221c8b4588de073c147fdeb0	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	IfThen	AndMultiLine	False	Passed	Model Under Test Equivalent Model
f8b66d7b31c76b6b43bf541d19f4cc5dc6037e74	Apalache	IfThen	Imply	True	Passed	Model Under Test Equivalent Model
0b19b459c47a55dfe26e65826da606958e0aa73f	Apalache	IfThen	Imply	False	Passed	Model Under Test Equivalent Model
f9120c3685048682711edb5d8b05d141dea0821d	Apalache	IfThen	Not	True	Passed	Model Under Test Equivalent Model
fa32b0575038e4d2a7dabe1e0e98f8da64ac83f8	Apalache	IfThen	Not	False	Passed	Model Under Test Equivalent Model
a16effed6f7e276faf0b4cd97988fe827ff25b9b	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	IfThen	Or	True	Passed	Model Under Test Equivalent Model
b56f1f9999a355ffbce23da80493aa569f79c9d3	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	IfThen	Or	False	Passed	Model Under Test Equivalent Model
b05008cfcf54c4668ca6dc4fdd720efa3abb5df3	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	IfThen	OrMultiLine	True	Passed	Model Under Test Equivalent Model
0d3f04b7d4c23175315993ebf58b98a32c39d753	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	IfThen	OrMultiLine	False	Passed	Model Under Test Equivalent Model
d4d6b92ef738f7529fe6ffc5d7cddf6c1d9e96ed	Apalache	IfThen	Eq	True	Passed	Model Under Test Equivalent Model
98f34b15fa0333547528af689a1fd07b3521a02c	Apalache	IfThen	Eq	False	Passed	Model Under Test Equivalent Model
172927294ba97cd756fa6954830a30ad1e69cc88	Apalache	IfThen	Ne	True	Passed	Model Under Test Equivalent Model
6c6e89c4bf23a22347a275b4965472696a2ae468	Apalache	IfThen	Ne	False	Passed	Model Under Test Equivalent Model
20fadf5a0766645024a836236aefba00f78b4b34	Apalache	IfThen	Let	True	Passed	Model Under Test Equivalent Model
a714a6965268547ee2ab13402d3d66afe28b0957	Apalache	IfThen	Let	False	Passed	Model Under Test Equivalent Model
b65e8326de71d88dabdedb2ae772abbb175e4e88	Apalache	IfThen	SetEmpty	True	Passed	Model Under Test Equivalent Model
e3edf2331f8772790d563819e8e0402b2fdc1aa8	Apalache	IfThen	SetEmpty	False	Passed	Model Under Test Equivalent Model
f4b0f5587d39953f1cea52921a8d246e5603e321	Apalache	IfThen	Set0	True	Passed	Model Under Test Equivalent Model
5d6efe4fc8aeff15400b743d4848506f82312e88	Apalache	IfThen	Set0	False	Passed	Model Under Test Equivalent Model
5d42827a24eb341449faf1a5f4d98479c84163b2	Apalache	IfThen	Set1	True	Passed	Model Under Test Equivalent Model
27e081b43ee503d55e31b8f0dd54bf1646cd019b	Apalache	IfThen	Set1	False	Passed	Model Under Test Equivalent Model
15404a3d9f37d76d4507fc871bcea245e7a72614	Apalache	IfThen	Set2	True	Passed	Model Under Test Equivalent Model
2d8f7e4df2c95bd6879a18765e4fb3e9f8ac2f91	Apalache	IfThen	Set2	False	Passed	Model Under Test Equivalent Model
42c157a889a9f3db2908f1d614676892be666aa7	Apalache	IfThen	Fun	True	Passed	Model Under Test Equivalent Model
6c11ac0ca817acccb22d91893ad6e664fb3ce91d	Apalache	IfThen	Fun	False	Passed	Model Under Test Equivalent Model
8d63379d117ad8fae6a020881feb54ec1242dd5e	Apalache	IfThen	In	True	Passed	Model Under Test Equivalent Model
4e7a377ea14ca4e1667f872d4ea2e0f03f9dc816	Apalache	IfThen	In	False	Passed	Model Under Test Equivalent Model
9215d414bf5cb57e01ae31e05fda20648802c7b4	Apalache	IfThen	NotIn	True	Passed	Model Under Test Equivalent Model
adb17a6d968e4293d086ddb3dbefb4519f34e551	Apalache	IfThen	NotIn	False	Passed	Model Under Test Equivalent Model
fb6f718803f912148eb1d392d28bf71e64d91b10	Apalache	IfThen	Exists	True	Passed	Model Under Test Equivalent Model
61fafc0ad631ae658edcb082d08bbbbf47c01415	Apalache	IfThen	Exists	False	Passed	Model Under Test Equivalent Model
ffaffb31738962b888826aecaf1d37e0a3401d8c	Apalache	IfThen	Forall	True	Passed	Model Under Test Equivalent Model
0ffa69c0b8bd99ea88919fe1d3c8d9dfe9958954	Apalache	IfThen	Forall	False	Passed	Model Under Test Equivalent Model
7181cfb43fc6bfd689be1cd908b303a943508838	Apalache	IfThen	Choose	True	Passed	Model Under Test Equivalent Model
87b52fa8d5f0b36efeb0ec83ac68ef4123aee6d6	Apalache	IfThen	Choose	False	Passed	Model Under Test Equivalent Model
981525c0bc1b923b4dbe1fea08b84bf791d19e00	Apalache	IfThen	Record	True	Passed	Model Under Test Equivalent Model
223f3e42939f04fea306adab044b6809f680fed9	Apalache	IfThen	Record	False	Passed	Model Under Test Equivalent Model
aff2970601ce70953e692c039335869fcf8c4fe7	Apalache	IfThen	Tuple	True	Passed	Model Under Test Equivalent Model
6c35a210fa200576c615b912f46e483f6bacf205	Apalache	IfThen	Tuple	False	Passed	Model Under Test Equivalent Model
4eb3d2768d1257ee2fbacfbcedc387788836cafa	Apalache	IfThen	TupleEmpty	True	Passed	Model Under Test Equivalent Model
34acba4f3333b637de07190e280134a2d8d8403a	Apalache	IfThen	TupleEmpty	False	Passed	Model Under Test Equivalent Model
a65d058a75557f37b20b1248befb98ea90b04035	Apalache	IfThen	FunApp	True	Passed	Model Under Test Equivalent Model
b8aededf6a3a52a2121bc057c0a24d9369735106	Apalache	IfThen	FunApp	False	Passed	Model Under Test Equivalent Model
a3d5ed39f814923334df841a0931500b2138303d	Apalache	IfThen	Prime	True	Passed	Model Under Test Equivalent Model
2faf483918c4f92f009a6d7a740cef01154c4641	Apalache	IfThen	Prime	False	Passed	Model Under Test Equivalent Model
afe70384e2ddad64a4bd05c1709fc93dfeae7b0a	Apalache	IfThen	NumZero	True	Passed	Model Under Test Equivalent Model
220c015179ff8d0c99042b31f18557d40c7d40ce	Apalache	IfThen	NumZero	False	Passed	Model Under Test Equivalent Model
8c8a18805716bc5b66c6fbb1a05a3ef8d49396b0	Apalache	IfThen	NumOne	True	Passed	Model Under Test Equivalent Model
1a4b3468459d95928f9a499308ec923ecd57d8c3	Apalache	IfThen	NumOne	False	Passed	Model Under Test Equivalent Model
b4d6da9481e99d1ef2d4879765428beed4b8871a	Apalache	IfThen	NumMaxInt	True	Passed	Model Under Test Equivalent Model
a617b7f6a1e7c8c3dc76a4a4d8fb2979edb8bd6a	Apalache	IfThen	NumMaxInt	False	Passed	Model Under Test Equivalent Model
daf48378b9d5b578b17e8683a95d781bcaa50a0b	Apalache	IfThen	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
54d0b5e77c7004cd37c10972bc57e6ae64c2129c	Apalache	IfThen	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d1a71f4581cd5d71e5de73e23b33a8cfd4a5b836	Apalache	IfThen	NumPlus	True	Passed	Model Under Test Equivalent Model
9237150795936630b7e431828a7e182dc857ed25	Apalache	IfThen	NumPlus	False	Passed	Model Under Test Equivalent Model
6d61d8c6856c421af459afc4bdfa3eca2f6ab53d	Apalache	IfThen	NumMinus	True	Passed	Model Under Test Equivalent Model
68033ef4dc1c444269896118e98822dd2b695b0f	Apalache	IfThen	NumMinus	False	Passed	Model Under Test Equivalent Model
8cf688c19c2f661009c7852c24c7b672c22836a3	Apalache	IfThen	NumMul	True	Passed	Model Under Test Equivalent Model
9bdc575b897c602a7e9284f18d98e2b2ef6fb1ef	Apalache	IfThen	NumMul	False	Passed	Model Under Test Equivalent Model
99d0939459f199fef2a31325b5a49caf92c75e9c	Apalache	IfThen	NumDiv	True	Passed	Model Under Test Equivalent Model
3c06e4622f28266db9cd380c08554ea34d3b5a47	Apalache	IfThen	NumDiv	False	Passed	Model Under Test Equivalent Model
02eb85d7253349f85c06fa9793db26c6551a06a6	Apalache	IfThen	NumMod	True	Passed	Model Under Test Equivalent Model
94b8341223281ce26747964cd77cd468cdd2ab16	Apalache	IfThen	NumMod	False	Passed	Model Under Test Equivalent Model
08801ae78c11e89c92524bcf14ee67ae4c404dbb	Apalache	IfThen	NumPow	True	Passed	Model Under Test Equivalent Model
9226c23aed5ee8d96536613092d6ee0d54a38d4b	Apalache	IfThen	NumPow	False	Passed	Model Under Test Equivalent Model
be410545a8ab684683211e5d4c0fa9b79da4604c	Apalache	IfThen	NumGt	True	Passed	Model Under Test Equivalent Model
73476054bf9f1aeabcce6a6cee8b3f8245d98ace	Apalache	IfThen	NumGt	False	Passed	Model Under Test Equivalent Model
14d605d4ae3d68556a60436433ccc06617111ac6	Apalache	IfThen	NumGe	True	Passed	Model Under Test Equivalent Model
772a43d23e54a1d8f28facccb1065fd456b4ce73	Apalache	IfThen	NumGe	False	Passed	Model Under Test Equivalent Model
88cf1a2c180507fc97050c99f3de09b0c857b5b8	Apalache	IfThen	NumLt	True	Passed	Model Under Test Equivalent Model
490d8d43112cef093579802a76ad489d161e611c	Apalache	IfThen	NumLt	False	Passed	Model Under Test Equivalent Model
5449ac38427d4ecc9ea8f2aa8cd8ec183b8f9b72	Apalache	IfThen	NumLe	True	Passed	Model Under Test Equivalent Model
c48bc6ebfe7bf2d79616923c2554e22585200bc2	Apalache	IfThen	NumLe	False	Passed	Model Under Test Equivalent Model
03b6c5dc9cadbad48bf76974c586b6c76cb1cce8	Apalache	IfThen	DefFun	True	Passed	Model Under Test Equivalent Model
7c203628a9057b7335dcf9047549f587faed2fe8	Apalache	IfThen	DefFun	False	Passed	Model Under Test Equivalent Model
3a97c140a428383105adb620ec278955457d73bb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDefFun	True	Passed	Model Under Test Equivalent Model
dd02cabca41b5c4fe2a3f17ea0863bbe5abd86c8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDefFun	False	Passed	Model Under Test Equivalent Model
8780140b5517082be0f86dab9cb62fe0027d12db	Apalache	IfThen	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
b978e2514b0aadce49459deed17314287a1ffa0b	Apalache	IfThen	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
0260b4eb78ce87a4b3e1f47da1b9ad5dbe8e112f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
79ddaf3dd93afd6a1ed7f004af71290501db9a14	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
c021427f1410229d3f7323f9d843f1ac9aeb51f5	Apalache	IfThen	Def0	True	Passed	Model Under Test Equivalent Model
50127b25dd1f52b5ec3865de05e7c917302b6795	Apalache	IfThen	Def0	False	Passed	Model Under Test Equivalent Model
70320147be06b5bd5c41606615373503d917d5db	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef0	True	Passed	Model Under Test Equivalent Model
67a398e4ecab0d5af4e90facdac50b1886072ce8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef0	False	Passed	Model Under Test Equivalent Model
b1a159cb8de304f13ed313cc2df5317a4a5c31fb	Apalache	IfThen	Def1	True	Passed	Model Under Test Equivalent Model
095faca44b70fee181d74693f41d0d99e763b812	Apalache	IfThen	Def1	False	Passed	Model Under Test Equivalent Model
97c86da4afb118b03f244500832ebc276dcd20a3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1	True	Passed	Model Under Test Equivalent Model
1213239916f5db3d5fdd41ede4ad3a767fcbd2fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1	False	Passed	Model Under Test Equivalent Model
162ba192ebeec5565c78f0b53588485b4fa199fb	Apalache	IfThen	Def2	True	Passed	Model Under Test Equivalent Model
11af74c09e7730e15ec20b091e012d82a5e9b856	Apalache	IfThen	Def2	False	Passed	Model Under Test Equivalent Model
fd54da8b0f55265f27d426774ba07f07dadcefb8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef2	True	Passed	Model Under Test Equivalent Model
2d1fedb4989a6a95031224e45e979092f2a6fa97	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef2	False	Passed	Model Under Test Equivalent Model
e230b0f0940fd5e27ceaf556b46af75921979904	Apalache	IfThen	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d522db8ae6887fd664ff39ab95fe6f787d8136d7	Apalache	IfThen	Def1Recursive	False	Passed	Model Under Test Equivalent Model
24d76dae73e246ed4a601c6a9863c329c9de691c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
c5a72f4986d27be7a33218f70779b4561868c600	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
9a2cf0232f6e66126e146d2d787e5cde2b1e96a4	Apalache	IfThen	Extends	True	Passed	Model Under Test Equivalent Model
0a0dbb9a2f9d7c961d05594c18da391a83bf6ea7	Apalache	IfThen	Extends	False	Passed	Model Under Test Equivalent Model
883341efb1897b496cc42548b6c913359b9e2694	Apalache	IfThen	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
66ee3db8754d38e9e5d7bc17213dd241a3da90e4	Apalache	IfThen	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
6d8a1dfb70a5e72f4980f7e24a901c8d30ddd284	Apalache	IfThen	Variable	True	Passed	Model Under Test Equivalent Model
a78687d8ecc611143411a1c510dd1f578ee85062	Apalache	IfThen	Variable	False	Passed	Model Under Test Equivalent Model
933b23c130b0246419e82cfcc65f620534392135	Apalache	IfThen	Constant	True	Passed	Model Under Test Equivalent Model
1f26d0ef466db125d43f9f6b7dbaa4df63313a76	Apalache	IfThen	Constant	False	Passed	Model Under Test Equivalent Model
c915e75da2d887cab3a50e422d8b3cceb9352e62	Apalache	IfThen	ConstantRank1	True	Passed	Model Under Test Equivalent Model
d64d6c8925a5681740971be6ba969885e151f375	Apalache	IfThen	ConstantRank1	False	Passed	Model Under Test Equivalent Model
6dd2e6e75c573cfd915a885fda1b208286662d35	Apalache	IfThen	Instance	True	Passed	Model Under Test Equivalent Model
ceeff3cc5ce89751581092596b3b52cd0b209f99	Apalache	IfThen	Instance	False	Passed	Model Under Test Equivalent Model
3eb5b782aa76a242b3ff4910264ef492eb114183	Apalache	IfThen	InstanceWith	True	Passed	Model Under Test Equivalent Model
1ae0f65f58d0332c8b6f0726c75b88133736251c	Apalache	IfThen	InstanceWith	False	Passed	Model Under Test Equivalent Model
d7dba212ca0e03c86defafde4c6e27092357cabb	Apalache	IfThen	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f3bee8200384bc47b6b98e0a359497bb20a8d08b	Apalache	IfThen	InstanceNamed	False	Passed	Model Under Test Equivalent Model
008eecb34ccfbae1ca1a7ad15cc52a4af8a64a1d	Apalache	IfThen	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
bea960e7e4a5b82c5ab167aef9d59dcb0583b86c	Apalache	IfThen	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9c22be4e49bb1bcb4a63ee0faa8c211530a9fda1	Apalache	IfThen	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
aeef8a769cbaaa38b8eb3d546a9a61cc1532ee44	Apalache	IfThen	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
0b56b008a168d2711996c45557d3a02008ea9769	Apalache	IfThen	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
f170aab80ac985216d5138f979f98cfc3b2e4ce9	Apalache	IfThen	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
1b24447137c1305999d52d86acb43f4f82e958bc	Apalache	IfThen	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
651c3d1c558df6c7516bf1486824025653e0d77d	Apalache	IfThen	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
7dfae994be4073877c67f12b3c0dd9857ef41f13	Apalache	IfThen	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
7c0965980d84aa60af4eded30398bb4f82e2a635	Apalache	IfThen	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
bb1fd94701673b11cb16b70897b9d75b3fd583bb	Apalache	IfThen	Enabled	True	Passed	Model Under Test Equivalent Model
2b4c81b46ee96390ad35eb099060cd43daa26413	Apalache	IfThen	Enabled	False	Passed	Model Under Test Equivalent Model
1436211d5c7ca258e11c6d67431fa0b377bc3436	Apalache	IfThen	Cross2	True	Passed	Model Under Test Equivalent Model
bbbc27a6805538e7a3581b28d06837e52fe2a6db	Apalache	IfThen	Cross2	False	Passed	Model Under Test Equivalent Model
bf7621e493f05fddd7a394f65060072615d66907	Apalache	IfThen	Cross3	True	Passed	Model Under Test Equivalent Model
12198ca35ad1186b271ef4c59fa13f052a8ef3c1	Apalache	IfThen	Cross3	False	Passed	Model Under Test Equivalent Model
af2e6d6c50904619573190e761cd3e58609c3d85	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))	IfThen	FunSet	True	Passed	Model Under Test Equivalent Model
9c985b8bb97347dfc28c90b16995c1f49c6810ed	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))	IfThen	FunSet	False	Passed	Model Under Test Equivalent Model
c79c7291622e4b7740895b11b53a55275bb5b6fc	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)	IfThen	RecordSet	True	Passed	Model Under Test Equivalent Model
5338328404219e7c20e67e18bfeb5aaab633884f	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)	IfThen	RecordSet	False	Passed	Model Under Test Equivalent Model
eb0cdb9ec39fecb14bd2f92af791394af8240693	Apalache	IfThen	SetDiff	True	Passed	Model Under Test Equivalent Model
3724b2ed485cf75e6266e17b704d0f52fb3aa53b	Apalache	IfThen	SetDiff	False	Passed	Model Under Test Equivalent Model
92eb0df6770924975e8308acaff101c086a6b7b6	Apalache	IfThen	SetUnion	True	Passed	Model Under Test Equivalent Model
76b740a606e9d9e2a8486c88b97594d6649ba636	Apalache	IfThen	SetUnion	False	Passed	Model Under Test Equivalent Model
bb5f2507a990ddca89aa5c3c6ddb8bb7c7f472e8	Apalache	IfThen	SetIntersect	True	Passed	Model Under Test Equivalent Model
2d2e9d3f7e36580b1dbd7a2791e3c04f5f6d288e	Apalache	IfThen	SetIntersect	False	Passed	Model Under Test Equivalent Model
aa4acbe020bbcc018ea3c98ea43b889a42677914	Apalache	IfThen	SubsetEq	True	Passed	Model Under Test Equivalent Model
b4b04f78f7f8ecd8dfd7e707c7cdc50158eca505	Apalache	IfThen	SubsetEq	False	Passed	Model Under Test Equivalent Model
2148f4386fb1b5d548aaaec62c170af32235051f	Apalache	IfThen	IfCond	True	Passed	Model Under Test Equivalent Model
fbf31ec92b399bb41936aac2e10d9d58182576ef	Apalache	IfThen	IfCond	False	Passed	Model Under Test Equivalent Model
998b9b6228b992aa0455bd192c3623c2e10a8dc6	Apalache	IfThen	IfThen	True	Passed	Model Under Test Equivalent Model
7cc1ac09ab633f4eb4de6281c0da2a924134946a	Apalache	IfThen	IfThen	False	Passed	Model Under Test Equivalent Model
991d54d1c096e42e8f366d998972167744037908	Apalache	IfThen	IfElse	True	Passed	Model Under Test Equivalent Model
98865629ae3c3119cb19c56ec807b101952851bb	Apalache	IfThen	IfElse	False	Passed	Model Under Test Equivalent Model
7abfbf743f38547c69ea39ea9ef739f0348ccb19	Apalache	IfThen	Subset	True	Passed	Model Under Test Equivalent Model
0b86f4ab58d9a7ccbefadc500be065fdee824ade	Apalache	IfThen	Subset	False	Passed	Model Under Test Equivalent Model
ffbda22dc1d1d8a5bc15786ff682e3d75990fac4	Apalache	IfThen	Domain	True	Passed	Model Under Test Equivalent Model
386f24529c31b2545e972f92a218cf2cba1a63c8	Apalache	IfThen	Domain	False	Passed	Model Under Test Equivalent Model
c66090046d8827f92dd4f13d99e7dc5efd9992b0	Apalache	IfThen	Union	True	Passed	Model Under Test Equivalent Model
95e1ee4ee78b05648223c14234ecd11b6eecc3ec	Apalache	IfThen	Union	False	Passed	Model Under Test Equivalent Model
0aa0cdca90ceb3d2123cb623856f938780ce0a5a	Apalache	IfThen	Unchanged	True	Passed	Model Under Test Equivalent Model
17aedf256a7e207c8a00b713180f0ac7c0a20025	Apalache	IfThen	Unchanged	False	Passed	Model Under Test Equivalent Model
004ff7bbacd598f59daf65ed5b3fe5ad2c78044b	Apalache	IfThen	Equivalence	True	Passed	Model Under Test Equivalent Model
4bfe0d09592bfcf05097f0dbddb910e4fcc5eafd	Apalache	IfThen	Equivalence	False	Passed	Model Under Test Equivalent Model
ea4210e29870ae9dcbc16a55d479133cfa0f7209	Apalache	IfThen	StringEmpty	True	Passed	Model Under Test Equivalent Model
3afa1159b4adb74a5d5ecb40a84b25b10ac6d424	Apalache	IfThen	StringEmpty	False	Passed	Model Under Test Equivalent Model
d9ee1314d95d666cd94dfe3b0d232e022353d56a	Apalache	IfThen	String	True	Passed	Model Under Test Equivalent Model
e37eb0ab7576a721d9c59ba45a8879845bfa4b0a	Apalache	IfThen	String	False	Passed	Model Under Test Equivalent Model
26aac5f135d015f0173978f04c4122bbca4f847b	Apalache	IfThen	SeqLen	True	Passed	Model Under Test Equivalent Model
3712d9d0526789a74072498d9bc3c11953675991	Apalache	IfThen	SeqLen	False	Passed	Model Under Test Equivalent Model
6a237f3ca89787c994a7bb6b29b935dfdf3d3b2c	Apalache	IfThen	SeqConcat	True	Passed	Model Under Test Equivalent Model
a966a103fe685a188a41119696b91c77ed6ecb19	Apalache	IfThen	SeqConcat	False	Passed	Model Under Test Equivalent Model
11a4fb8816fe4c611a67aa8041fbb1be6294d88f	Apalache	IfThen	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b3ad32c6b644a1f4e0928d641b633c7cd1e658c4	Apalache	IfThen	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
cf109c3ef7842d82cee1f668a32509399cfcb25f	Apalache	IfThen	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
15face7766c80da2d4e26e74f8438a48099d01c8	Apalache	IfThen	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
5c696916a0d74d418489de551b06dcfa3f651b28	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	IfThen	NumRange	True	Passed	Model Under Test Equivalent Model
f74551cd7ee40524fa1de73b7a3c280a822a1827	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	IfThen	NumRange	False	Passed	Model Under Test Equivalent Model
8f02c75d80e2e67d0fe2a0b42f866b6ace9584c5	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	IfThen	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
e511da6f6d4a1d32a8cf96562a27d02ad40bb77a	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	IfThen	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
8aae0a0ca42942c59f6a2abe92b47673e47af3c3	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]]	IfThen	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
24040fe1a0fd21c360481c3239ab0fc31bdbec82	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]]	IfThen	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
304fbe4fa2ae3aa9b5efd24f9340536fed25a07b	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	IfThen	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
daec552f0cbfd4dd7cddad54ced35cb2210613bb	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	IfThen	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
33d5947194f6a5ed283c9dc06e9cd89c4cd53f96	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	IfThen	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
82799a91bc0ebf9b39840b0884d8fd5e011f8d45	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	IfThen	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
4e85052869c2a20a8b35dc7bfbb1e90de8f55a20	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	IfThen	TlcEval	True	Passed	Model Under Test Equivalent Model
c14f9dec0229d7bc089110b89f1df83a3e0fff77	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	IfThen	TlcEval	False	Passed	Model Under Test Equivalent Model
58e6aa6283932bf9fd69ce0fad8cecba3f0a7c7d	Apalache	IfThen	BagBagToSet	True	Passed	Model Under Test Equivalent Model
cf942e0d47ef33bbe48cc0e9c2943d953dcd8c0e	Apalache	IfThen	BagBagToSet	False	Passed	Model Under Test Equivalent Model
6366314a600f9ed894e625e1c40c35eb82821ff7	Apalache	IfThen	BagSetToBag	True	Passed	Model Under Test Equivalent Model
e16e404d6fe6541cb72f44684f9a423a7fb62ef4	Apalache	IfThen	BagSetToBag	False	Passed	Model Under Test Equivalent Model
ee3257d399fb06f4d99f8229111f18c0d062765f	Apalache	IfThen	BagBagIn	True	Passed	Model Under Test Equivalent Model
0a3da56f75eb942a6058306d8d2c7438f1b8bcfa	Apalache	IfThen	BagBagIn	False	Passed	Model Under Test Equivalent Model
576f40dd64477da866552bf332e3a9ff81a582c9	Apalache	IfThen	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
8072374a01ad174b9ba2d6d8d17512dd6dd7004e	Apalache	IfThen	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
68d97566390bfdce7caaf29e3a70042e5eb8886d	Apalache	IfThen	BagAddBag	True	Passed	Model Under Test Equivalent Model
f73ddea4869f352588737dab6155b2d9b0bf4439	Apalache	IfThen	BagAddBag	False	Passed	Model Under Test Equivalent Model
2c7ef9df7611102c9debc9e8f3252fa6fd794156	Apalache	IfThen	BagBagSub	True	Passed	Model Under Test Equivalent Model
c49627f9815736c32c54f7cf8054e65b8b073961	Apalache	IfThen	BagBagSub	False	Passed	Model Under Test Equivalent Model
f0f05917f283b2487f0b3d277d6953573f3cb57c	Apalache	IfThen	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6742b65d6a183cfca3f0dfd6b39db87fa6371f50	Apalache	IfThen	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
4380932ff944b79a00edd30439d80ecde02c0963	Apalache	IfThen	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
e27bdb6d417779a7b7f76438b94fbf14349dbc6d	Apalache	IfThen	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4a8fd92e7e0a99f7a5d075b411fe6595ab786dba	Apalache	IfThen	BagBagUnion	True	Passed	Model Under Test Equivalent Model
03f7e8a651886ec8cdf1dcb1df5ef3e7fb2d14b8	Apalache	IfThen	BagBagUnion	False	Passed	Model Under Test Equivalent Model
e65ecd5cfaf91020dbcd9b699a34a72c544a54f4	Apalache	IfThen	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8e03a4ca99a108bd27e1bacf34561fd0f27a628d	Apalache	IfThen	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
f68398bca4f7aaad0508abba4bd41e31ae247677	Apalache	IfThen	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
be6b03b2a973897cb2aabc410668dabe4df1271e	Apalache	IfThen	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
45f5344fd3468e468952c699b27a9dfe2f481dc2	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	IfThen	BagSubBag	True	Passed	Model Under Test Equivalent Model
b3fe96e4eb836168272641c90d5b121fef287c06	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	IfThen	BagSubBag	False	Passed	Model Under Test Equivalent Model
ff1f9cd1b14e6aee65fb7bae9519fc4f795fbb94	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)	IfThen	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
570a65ce2086bd3efa6d4e3d287f7c48efaf8014	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)	IfThen	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
b119129e8f822293d6ac578f9713856c63605291	Apalache	IfThen	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
b7b266df2de611aaac460a466b3a90ba37e878bf	Apalache	IfThen	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
8acdc0137969bf2324116b79384dccf97c9ccf28	Apalache	IfThen	SeqHead	True	Passed	Model Under Test Equivalent Model
0f74dd6d76dd1a81a4052277fd38f3f577604690	Apalache	IfThen	SeqHead	False	Passed	Model Under Test Equivalent Model
e172c730f9c6133566465f3489c57cc3ff4040de	Apalache	IfThen	SeqTail	True	Passed	Model Under Test Equivalent Model
839cc2f32fe9419ac03f3952335051b68578cb28	Apalache	IfThen	SeqTail	False	Passed	Model Under Test Equivalent Model
112e2598ae021d2d2cd440981babec7cb6e5c84e	Apalache	IfThen	SeqAppend	True	Passed	Model Under Test Equivalent Model
5a633de8c43de798a09ce2afd72b96f214a7b7b0	Apalache	IfThen	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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