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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
abc0bcca0e388a5e7c9cbe6453bf69d02b8266bd	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Choose	OneLineComment	True	Passed	Model Under Test Equivalent Model
03673d0f86a42cd970d0991226b4059373d96b0d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Choose	OneLineComment	False	Passed	Model Under Test Equivalent Model
e512987e1cf8993c1c2681772185d191cd39a65e	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Choose	MultiLineComment	True	Passed	Model Under Test Equivalent Model
4cff0f449a9777cc9293a49317c93083cee394df	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Choose	MultiLineComment	False	Passed	Model Under Test Equivalent Model
d776fc63b5110c79354eb760003f4c3fc3ae0456	Apalache	Choose	BoolTrue	True	Passed	Model Under Test Equivalent Model
80ed39a21701899ac303372ec05db6e93311f0ca	Apalache	Choose	BoolTrue	False	Passed	Model Under Test Equivalent Model
85de1265e6ddc5777839a5372c6cb145958cec88	Apalache	Choose	BoolFalse	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
e9af4b5dda8a82ec1c6e9d135089645fb4fded7d	Apalache	Choose	BoolFalse	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
cc558a2e9f56efa6d0c6a991647611410173c8f4	Apalache	Choose	And	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
c530df788f11eab722295a74084444a71942868f	Apalache	Choose	And	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
b901efb568b733dd714bac9e694455954bc40633	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Choose	AndMultiLine	True	Passed	Model Under Test Equivalent Model
6a342df13539c791f208c8a26ac5ee9901be7b12	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Choose	AndMultiLine	False	Passed	Model Under Test Equivalent Model
5337f17a1dffeab9aadb37fd3f5d2ebb928e6ce1	Apalache	Choose	Imply	True	Passed	Model Under Test Equivalent Model
588b74646247ed0be3097b8693a797c1d9bd294a	Apalache	Choose	Imply	False	Passed	Model Under Test Equivalent Model
6f4b6450456ea77d11909cabd20cdee0a7323965	Apalache	Choose	Not	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
f2f82f385106fcf3529bcb41555fcf0e475d4ab8	Apalache	Choose	Not	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
d2a828d3d9fbf0f4b75c6ebf0b720df360b5445f	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Choose	Or	True	Passed	Model Under Test Equivalent Model
ae8396fc5811c7c01d6df6da549f7d82cf51ca64	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Choose	Or	False	Passed	Model Under Test Equivalent Model
746d876c62b827599b724529871855f4349954c5	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Choose	OrMultiLine	True	Passed	Model Under Test Equivalent Model
8f97dc89311aea3fbc0d8d7c7fb75ff7b247b253	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Choose	OrMultiLine	False	Passed	Model Under Test Equivalent Model
b9c1771e458692bc8c769ca93f04ee01ee273345	Apalache	Choose	Eq	True	Passed	Model Under Test Equivalent Model
5e85f9a706cc4f526f2b9bfec6b7aef1b9791255	Apalache	Choose	Eq	False	Passed	Model Under Test Equivalent Model
34ae665676973327b27a581ad0eaa89dab85247a	Apalache	Choose	Ne	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
fef49c794ebed4050d2c975d336b40177678bffb	Apalache	Choose	Ne	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
2d63ed11de84a4bb94e3e7e63191b8b87fda08d3	Apalache	Choose	Let	True	Passed	Model Under Test Equivalent Model
aea48a836519e3ccfb96e5908e99e4248712ff27	Apalache	Choose	Let	False	Passed	Model Under Test Equivalent Model
14f7225190b3860604eaaf2d517639397379de06	Apalache	Choose	In	True	Passed	Model Under Test Equivalent Model
6210b34c8e9f740a3f13328d0dcbc64a9679f997	Apalache	Choose	In	False	Passed	Model Under Test Equivalent Model
910abb8211bdd4e49b0b5c78224ad41d8b78fad1	Apalache	Choose	NotIn	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
f33b2188a4f969e97c7a0e8e996f37d9c8b02e04	Apalache	Choose	NotIn	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
6913cd1a256636118c9a1a114581d24ef2384c62	Apalache	Choose	Exists	True	Passed	Model Under Test Equivalent Model
e7c51f80ee3b9b7f88137bcdd4d347974c939293	Apalache	Choose	Exists	False	Passed	Model Under Test Equivalent Model
04e29056043d520ed82db3386d0f148177bebe72	Apalache	Choose	Forall	True	Passed	Model Under Test Equivalent Model
2c2f0be1eae207e67cb3fbbfbb8d953f4d065634	Apalache	Choose	Forall	False	Passed	Model Under Test Equivalent Model
e6314faecb0fea7082630635280684d83f54ed5f	Apalache	Choose	Choose	True	Passed	Model Under Test Equivalent Model
87a9b6cf1b0100ac38c165023a9f845138fc931a	Apalache	Choose	Choose	False	Passed	Model Under Test Equivalent Model
5f7e166c77dc6a3e74fb480b6e119cf58b0e3420	Apalache	Choose	FunApp	True	Passed	Model Under Test Equivalent Model
d5b4ca944a18fe4a68327e76a630f85c4ce0838b	Apalache	Choose	FunApp	False	Passed	Model Under Test Equivalent Model
b9f3d8e711282828d92e27c533085dae5d539420	Apalache	Choose	Prime	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
b97daa0d0f86ec9dcc7a7729ac2289f9802425f7	Apalache	Choose	Prime	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
8947cd53ce33c1394731b7fca3beadb8eb6a1167	Apalache	Choose	NumGt	True	Passed	Model Under Test Equivalent Model
1ad2e06d9a544b0948dd5aa1a8aa5552fd38731f	Apalache	Choose	NumGt	False	Passed	Model Under Test Equivalent Model
89105e9f6e710afa6ced594c86c2a96e08d7ee7b	Apalache	Choose	NumGe	True	Passed	Model Under Test Equivalent Model
e944529958bee449b08e21dac93fb763d1b4ec9a	Apalache	Choose	NumGe	False	Passed	Model Under Test Equivalent Model
55f95aef57f44226000613b2eae7fb71e80ed346	Apalache	Choose	NumLt	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
05c14cc9b8e2d432a5d3b33fe26833d1bbcaa14c	Apalache	Choose	NumLt	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
4493f66012b2bb44826f65d0defa60c9ca91e152	Apalache	Choose	NumLe	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
fd1f4c2fa95da9521dd80b2b24cfbce6a63fbc68	Apalache	Choose	NumLe	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
2d548aa55a36296a643ad5c4f042d85e27ed85fb	Apalache	Choose	Def0	True	Passed	Model Under Test Equivalent Model
0eb0a775c1dcc2b23a5f42c364f1f687541551a7	Apalache	Choose	Def0	False	Passed	Model Under Test Equivalent Model
a0ecc9911ca733e59d4cd2dacf49c88d0be649c8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef0	True	Passed	Model Under Test Equivalent Model
9619ce95d744020d8948a239105c66dc923a8b1c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef0	False	Passed	Model Under Test Equivalent Model
ed9d7199dfab4d03329bfa58a73ed8f9c737e3e8	Apalache	Choose	Def1	True	Passed	Model Under Test Equivalent Model
83c417b4ec8595787e73c85438ec6cf4391c62c4	Apalache	Choose	Def1	False	Passed	Model Under Test Equivalent Model
35afb9f36506c3d3b580dcdafedc2ed4814db53d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1	True	Passed	Model Under Test Equivalent Model
da7e5163e3786b8d332a995cd4d2fcb0c94a051d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1	False	Passed	Model Under Test Equivalent Model
9c2125e41f7f29f49a6c96de332e4a3029302bd5	Apalache	Choose	Def2	True	Passed	Model Under Test Equivalent Model
594a463c072881f39829053f730476d56f4a1791	Apalache	Choose	Def2	False	Passed	Model Under Test Equivalent Model
793d4e2761c9b7c5fd9605911985257cf1f94424	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef2	True	Passed	Model Under Test Equivalent Model
b15c3b1cc85cfd3545678577725217b514241dc4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef2	False	Passed	Model Under Test Equivalent Model
c1d892b27fc3f942069c75141a333f7f62c003c0	Apalache	Choose	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d2901fca5f9b8c389e5f394f4bf11db6ab18aebb	Apalache	Choose	Def1Recursive	False	Passed	Model Under Test Equivalent Model
6a36e092eda6b98d6c463f5f830a0c23780c0054	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
8cc5d316ae16d80b0e286867262331c375e97cd0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
5d7a1b4244bd2f8a88143a88b20564caa7916d85	Apalache	Choose	Extends	True	Passed	Model Under Test Equivalent Model
3d1f1d28a9490474d6846a3538a1ae11f4884f92	Apalache	Choose	Extends	False	Passed	Model Under Test Equivalent Model
e4f7a6a6da51ff112e928b4fc15613f2bdeb9c77	Apalache	Choose	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
61a71c9c2f82c46a873ab4287f944324c0de6e56	Apalache	Choose	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
f6eeb2a15e9e61e36ff879bed25395dbf0dcb8a2	Apalache	Choose	Variable	True	Passed	Model Under Test Equivalent Model
57137c67126cf9425143a4a89a1a4cead80a414b	Apalache	Choose	Variable	False	Passed	Model Under Test Equivalent Model
aec99a3ff506fb71d22117eff190d47d1a16631f	Apalache	Choose	Constant	True	Passed	Model Under Test Equivalent Model
e5566e14788027609ec28153bafe73c9d8943c49	Apalache	Choose	Constant	False	Passed	Model Under Test Equivalent Model
aae12e511b8a937f651e97e3c625efdaf2b03693	Apalache	Choose	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f76fc5758e6214f4288a34f048a233291d12f933	Apalache	Choose	ConstantRank1	False	Passed	Model Under Test Equivalent Model
a99a0fa1b8071e14dcd14723677c3a7d020de893	Apalache	Choose	Instance	True	Passed	Model Under Test Equivalent Model
1d11228e1a0b03116b3844873b7e03d274c5e2d5	Apalache	Choose	Instance	False	Passed	Model Under Test Equivalent Model
4227ec31b7de640770f1eac06cf325f4b01c8714	Apalache	Choose	InstanceWith	True	Passed	Model Under Test Equivalent Model
6fd191d8169769d3ab90d97e6d2919609de0ee6c	Apalache	Choose	InstanceWith	False	Passed	Model Under Test Equivalent Model
a62ac97ee55d5e124514dd1d695392283e0ca6b6	Apalache	Choose	InstanceNamed	True	Passed	Model Under Test Equivalent Model
4bf5112759d437fdd0ae735765ccbab7ecf887da	Apalache	Choose	InstanceNamed	False	Passed	Model Under Test Equivalent Model
b45fd361cc284f10cc1b45ea7a1e68bd7dceed65	Apalache	Choose	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f93dc26fe3564dd853c521a503b762ee0f57ec87	Apalache	Choose	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
79d57173391a409318e91a89c7ee4e2450303215	Apalache	Choose	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
3d9c54bc307c5f55f41a014710e9126798a199dd	Apalache	Choose	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
a02b3fec904d9f47911944605feda9b83795cf45	Apalache	Choose	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
ee1ca11fc6fede3870c5076fe0f1ab9a0a662416	Apalache	Choose	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
7b75e84931fa7a5caf2aa4ed10ba5bd1618b46a6	Apalache	Choose	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
c4635c92bdacd5440c6169c32891425e93cc9fc0	Apalache	Choose	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
e20b9f2b416f28e3c9bce29cad360a25abf83152	Apalache	Choose	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
d9d36961d3b02fc83787835685dd20f9e143d7f9	Apalache	Choose	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
bc2627758a45f82e84982eb8e4934dda9f5663db	Apalache	Choose	Enabled	True	Passed	Model Under Test Equivalent Model
47c5c454e49f037aab45f35c718a6b0712ca3438	Apalache	Choose	Enabled	False	Passed	Model Under Test Equivalent Model
efcbb86d8e825035422ef00dabb32e954a932280	Apalache	Choose	SubsetEq	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
c2e7701c74244b41eb1004ddb9a7e058a47a0c1a	Apalache	Choose	SubsetEq	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
77453c4acdbe0cb2587ba3ec9825f3f34b79901e	Apalache	Choose	IfCond	True	Passed	Model Under Test Equivalent Model
e116dc06b2d531f54ea9e31252174a6b8a8dd0f1	Apalache	Choose	IfCond	False	Passed	Model Under Test Equivalent Model
3bfe7ad72549f553b1ce304e92dd055de7fc7a42	Apalache	Choose	IfThen	True	Passed	Model Under Test Equivalent Model
69b2d19d4832ca2664f6111a6d8943d4ae4ea4b6	Apalache	Choose	IfThen	False	Passed	Model Under Test Equivalent Model
397fcff29abf2ade9f007a53c4331d272a47bc90	Apalache	Choose	IfElse	True	Passed	Model Under Test Equivalent Model
b54dd6a225fb9816eb7e7d27f45f2c502d044175	Apalache	Choose	IfElse	False	Passed	Model Under Test Equivalent Model
454ef4523aa109624a7a3e01692258e2ffa446fd	Apalache	Choose	Unchanged	True	Passed	Model Under Test Equivalent Model
c091458edcc28b4add51b953b27332daf365eed3	Apalache	Choose	Unchanged	False	Passed	Model Under Test Equivalent Model
6c65754b60c324fac1386bc062d7a257290df344	Apalache	Choose	Equivalence	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
9580c4c94498621cae1061cf1b62dbd20530e314	Apalache	Choose	Equivalence	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
b77734daefcbfd81ae78895a08084f8a02a7483e	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Choose	TlcEval	True	Passed	Model Under Test Equivalent Model
ebb06aea0bb4aa3c3d7cb942385e82e3200652de	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Choose	TlcEval	False	Passed	Model Under Test Equivalent Model
65cf83d03843a162e4db3125fda5c3129da22212	Apalache	Choose	BagBagIn	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
8a3d42c2decdc31f60dacb204bb371dd57296414	Apalache	Choose	BagBagIn	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
60c7365b4ab7bd2051d5d3a1e2bdd53e417a28d4	Apalache	Choose	BagSubsetEqBag	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
79f8bff2282b53f2375f9055f6f0d44e921b2f5d	Apalache	Choose	BagSubsetEqBag	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
91fb3139dc94b222660e173f3ef08ac9942a6c9d	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)	Choose	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
19d342465a32bc55493e462c7aa75d1f62ba13a5	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)	Choose	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
cdfb9a899775459e4d3a26e1647a80f225898c8e	Apalache	Choose	SeqHead	True	Passed	Model Under Test Equivalent Model
73e400922f0b6bf773c7a7ce170101ab5a351874	Apalache	Choose	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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