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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3fe7cf7f8eb0a39838d671e865c48bc800f50e7d	Apalache	NotIn	BoolTrue	True	Passed	Model Under Test Equivalent Model
0d22dd64e78ef3706d50913b0fc46b889b43c981	Apalache	NotIn	BoolTrue	False	Passed	Model Under Test Equivalent Model
15d916aaf4e68f10884f641a1dd54a57758f65e6	Apalache	NotIn	BoolFalse	True	Passed	Model Under Test Equivalent Model
7ba1ea5c3b971cbfe10165867c4ad1c2e92083dd	Apalache	NotIn	BoolFalse	False	Passed	Model Under Test Equivalent Model
dbe9c80b94508f9aaeffe8a777f541e04b0da7ca	Apalache	NotIn	BoolSet	True	Passed	Model Under Test Equivalent Model
a3794dc6d2aed7a7244c071a1c140d0f51d7ba8f	Apalache	NotIn	BoolSet	False	Passed	Model Under Test Equivalent Model
6fca85d169975c0a58204d27b45bbdded8b1cb35	Apalache	NotIn	And	True	Passed	Model Under Test Equivalent Model
76d5a28a8b57e12fb2086b11782a97c29ecc2414	Apalache	NotIn	And	False	Passed	Model Under Test Equivalent Model
4b89e56a5a2ca138d467700d907890dd13c5be20	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	NotIn	AndMultiLine	True	Passed	Model Under Test Equivalent Model
a5b322e141b6d86b3fb2a214d9c56c9655311e6e	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	NotIn	AndMultiLine	False	Passed	Model Under Test Equivalent Model
d313e30d9b0c30ea46717c9cfbdaa622d008fe9e	Apalache	NotIn	Imply	True	Passed	Model Under Test Equivalent Model
053b7e9d18e031baec3458db1b6a31cf9e527dd2	Apalache	NotIn	Imply	False	Passed	Model Under Test Equivalent Model
1d3bed688f7da90a785f805c0c2433abcc4f0e06	Apalache	NotIn	Not	True	Passed	Model Under Test Equivalent Model
b6b8d714da92b5e48de717609688a8dc6caaad13	Apalache	NotIn	Not	False	Passed	Model Under Test Equivalent Model
33011b478077329e4d284216ba3e56e5a6233980	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	NotIn	Or	True	Passed	Model Under Test Equivalent Model
a28481316db034179ec9675b1ad3fa2b51832652	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	NotIn	Or	False	Passed	Model Under Test Equivalent Model
7f8960f5d6ecfbe5b3cc045b780cd65dccac9685	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	NotIn	OrMultiLine	True	Passed	Model Under Test Equivalent Model
09433e9de48527957fdda99626af63a2d92eb514	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	NotIn	OrMultiLine	False	Passed	Model Under Test Equivalent Model
0afaea84d1ae19a8dd8a69f53c942318875762e5	Apalache	NotIn	Eq	True	Passed	Model Under Test Equivalent Model
f85cf2f727574a505f332e47c0c52dbddd0f73e0	Apalache	NotIn	Eq	False	Passed	Model Under Test Equivalent Model
7c0d241bab1187307b4f8c0a28d53acee6fb64d9	Apalache	NotIn	Ne	True	Passed	Model Under Test Equivalent Model
767e893946676a3e382292878c48d71de8fda52b	Apalache	NotIn	Ne	False	Passed	Model Under Test Equivalent Model
3426f7fc4e089e42ef5ac53bb75d34dc99385a48	Apalache	NotIn	Let	True	Passed	Model Under Test Equivalent Model
07470b03a2f545da2b2ec663005294e2d5eecb71	Apalache	NotIn	Let	False	Passed	Model Under Test Equivalent Model
52dd2559f586f9063474205d5bdaebac3a403fbf	Apalache	NotIn	SetEmpty	True	Passed	Model Under Test Equivalent Model
258ae9742a778193d683be2f6f8152ff7abdbf1a	Apalache	NotIn	SetEmpty	False	Passed	Model Under Test Equivalent Model
d11404f3b4786cd29d05ea884b0aa522973e361c	Apalache	NotIn	Set0	True	Passed	Model Under Test Equivalent Model
e4143e9807728913681bbf5b9b73226f933c26a1	Apalache	NotIn	Set0	False	Passed	Model Under Test Equivalent Model
b2ba8168c2e8d84700e802418d40502a01153fdb	Apalache	NotIn	Set1	True	Passed	Model Under Test Equivalent Model
2744bd81714e13b5e52b61df4587b2049c1ab52a	Apalache	NotIn	Set1	False	Passed	Model Under Test Equivalent Model
8f1a81bc8c5209f0c3b9410f12d72c07737ba67a	Apalache	NotIn	Set2	True	Passed	Model Under Test Equivalent Model
ccb59e19ad00d3a5249ae3c7ae7ecf57f9a95faf	Apalache	NotIn	Set2	False	Passed	Model Under Test Equivalent Model
a008c7ded082d08c89a5bf3f592d8ab304824ec7	Apalache	NotIn	Fun	True	Passed	Model Under Test Equivalent Model
ba843e08d4f1d5f32e7d3f6487476854bc9b396a	Apalache	NotIn	Fun	False	Passed	Model Under Test Equivalent Model
f5e4a112dd60cbc93dcc8cee4f91d9433e8c7396	Apalache	NotIn	In	True	Passed	Model Under Test Equivalent Model
70a0c955a70634dd26e1202780a60d2e609776e1	Apalache	NotIn	In	False	Passed	Model Under Test Equivalent Model
5cc3c51b9b82b95a1bd0bd224db73d31b0031ab1	Apalache	NotIn	NotIn	True	Passed	Model Under Test Equivalent Model
64d6852eb1a1ede0808d2ec596d0eb57f9651ccf	Apalache	NotIn	NotIn	False	Passed	Model Under Test Equivalent Model
89b56861bc4aacbe6ccbc67ab7ca33c1d86d2ffb	Apalache	NotIn	Exists	True	Passed	Model Under Test Equivalent Model
63282ae70c7d4d191ab4344e6a778a1fea31571b	Apalache	NotIn	Exists	False	Passed	Model Under Test Equivalent Model
cb85b0b18d850eb83529f084098d3b63ede1770c	Apalache	NotIn	Forall	True	Passed	Model Under Test Equivalent Model
e41ff464906633cdc5124cb4704c6e79ddd0e45d	Apalache	NotIn	Forall	False	Passed	Model Under Test Equivalent Model
2b3c582e7618b858cef052ac3cfb856229512def	Apalache	NotIn	Choose	True	Passed	Model Under Test Equivalent Model
d49ca7b811000bb4ed6c3f576d28e0171a2a09b9	Apalache	NotIn	Choose	False	Passed	Model Under Test Equivalent Model
534440cbd2970aec18e5221e79c3a42f76122dfa	Apalache	NotIn	Record	True	Passed	Model Under Test Equivalent Model
4d604acc784120c62a2ef720a7cb9abfb003d5c5	Apalache	NotIn	Record	False	Passed	Model Under Test Equivalent Model
eadff6f165b7121e409230713f35467a42005559	Apalache	NotIn	Tuple	True	Passed	Model Under Test Equivalent Model
16feadbb67fe97661f7bf8393e6a82814e7cb0ab	Apalache	NotIn	Tuple	False	Passed	Model Under Test Equivalent Model
92de7ad93e782ea946b028177a1e837b67cc6845	Apalache	NotIn	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8dc2e5e62a8dbe721e419a054e108f3670532901	Apalache	NotIn	TupleEmpty	False	Passed	Model Under Test Equivalent Model
7f3ef8eae2543873ea1d99546632eea57ccbb110	Apalache	NotIn	FunApp	True	Passed	Model Under Test Equivalent Model
2951045f6c5a1779e228d9a70107cf8d12b68e53	Apalache	NotIn	FunApp	False	Passed	Model Under Test Equivalent Model
8b972ee0299d28fd90aea57e3ea256cc76e6e5e0	Apalache	NotIn	Prime	True	Passed	Model Under Test Equivalent Model
e5c620977e04152fed7ca0b13860483b3a065098	Apalache	NotIn	Prime	False	Passed	Model Under Test Equivalent Model
317bb4b592c41361c693c4023536a06b96a88df4	Apalache	NotIn	NumZero	True	Passed	Model Under Test Equivalent Model
d2ae2f369ad188c06c88431854ddee6d122daf85	Apalache	NotIn	NumZero	False	Passed	Model Under Test Equivalent Model
a58b3631148acd255308cc86ccbccad5e6fa0127	Apalache	NotIn	NumOne	True	Passed	Model Under Test Equivalent Model
60e47d9ea72cec25533f341299776290aa9c2062	Apalache	NotIn	NumOne	False	Passed	Model Under Test Equivalent Model
83e35ae6ab92d34afcd61dc7e75c6448b4162846	Apalache	NotIn	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ec5c033cdd193d2eaaf619271bec9994d7aea0fb	Apalache	NotIn	NumMaxInt	False	Passed	Model Under Test Equivalent Model
634365443c82a823b7f3e73eb7fa2d434d57d965	Apalache	NotIn	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
ecc04eadd9f8de0b62ca28f7b9cdcf223fdd6400	Apalache	NotIn	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
16243f75aa18dcb285f600f4da74de9fbb76be86	Apalache	NotIn	NumPlus	True	Passed	Model Under Test Equivalent Model
6d18cee8236e0d0edbe83ad59409d9b8eacaa285	Apalache	NotIn	NumPlus	False	Passed	Model Under Test Equivalent Model
f53d9de520c115fcef40b3d1571670f4c00c8978	Apalache	NotIn	NumMinus	True	Passed	Model Under Test Equivalent Model
a84171984250ffcd162b652761f2e4d17ef67ac8	Apalache	NotIn	NumMinus	False	Passed	Model Under Test Equivalent Model
405538bf6631d13318922172f5f67f42672118b3	Apalache	NotIn	NumMul	True	Passed	Model Under Test Equivalent Model
51596edd5d896813b28722cc37bb9608941cfafe	Apalache	NotIn	NumMul	False	Passed	Model Under Test Equivalent Model
dd41ad801dd946da6aafacfa5a7625bb0b75f7a2	Apalache	NotIn	NumDiv	True	Passed	Model Under Test Equivalent Model
57f004652a55026ebcee6e6c4cee7bcd1d2ec1e6	Apalache	NotIn	NumDiv	False	Passed	Model Under Test Equivalent Model
8c37e3bd3fb24afd0d41288b7d17ca6a62351a7e	Apalache	NotIn	NumMod	True	Passed	Model Under Test Equivalent Model
e545f64212be3a3bbd3107a0f0b71297b024d11f	Apalache	NotIn	NumMod	False	Passed	Model Under Test Equivalent Model
c77e02f41f76c04ee6dc95b6edea222dd6be2ca5	Apalache	NotIn	NumPow	True	Passed	Model Under Test Equivalent Model
64a387d2efa0384e8048ee57cd0bb38fd16987b5	Apalache	NotIn	NumPow	False	Passed	Model Under Test Equivalent Model
36150a6544484ff12547b69d00751a54a722c990	Apalache	NotIn	NumGt	True	Passed	Model Under Test Equivalent Model
33d5d85e8c9b7849dee32d7307a9520defd21582	Apalache	NotIn	NumGt	False	Passed	Model Under Test Equivalent Model
e98f501cd1850458407f01357d846f41014f817b	Apalache	NotIn	NumGe	True	Passed	Model Under Test Equivalent Model
6a3fc7a1b97025e87144e1ae34f33af62c566427	Apalache	NotIn	NumGe	False	Passed	Model Under Test Equivalent Model
d8c613e4be161f4fd4830a2f29cf52de16192727	Apalache	NotIn	NumLt	True	Passed	Model Under Test Equivalent Model
9005776bde260a9919c8852c3fb9adc5f81597f3	Apalache	NotIn	NumLt	False	Passed	Model Under Test Equivalent Model
2e1235c07463aa20655c9d85ef458827bedbd5e4	Apalache	NotIn	NumLe	True	Passed	Model Under Test Equivalent Model
2add9b8391638a802fed51e7180ddd250ef56c9e	Apalache	NotIn	NumLe	False	Passed	Model Under Test Equivalent Model
ccfe776210b47174249be7225705802e9a4ccccb	Apalache	NotIn	DefFun	True	Passed	Model Under Test Equivalent Model
a2d33795b2519e05d004c613759e5c5aa8d131fe	Apalache	NotIn	DefFun	False	Passed	Model Under Test Equivalent Model
fab86b6fbd287b70038e8906da0a55f58359e1d2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDefFun	True	Passed	Model Under Test Equivalent Model
8777b4b12b73c7b87da4bae7912191d1b264c5c6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDefFun	False	Passed	Model Under Test Equivalent Model
f48d5b5334a5c075e79218524313ecc1ef539d2f	Apalache	NotIn	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
275f83f7189345fc84a602a90464c54b786a941e	Apalache	NotIn	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
e4c4a8e62df534c7bec6d5fdd242b82391fb185f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
08df84e9d7dd85e5f2c5507c6e63f77acab0986b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
5b966b649ae7948f2b3c56ffe71596712ae1e3a0	Apalache	NotIn	Def0	True	Passed	Model Under Test Equivalent Model
1aeb663779de9ea9e4dbc3a0ce89697b88fd858c	Apalache	NotIn	Def0	False	Passed	Model Under Test Equivalent Model
d65172931a2725909b6c90ed1a400f3b6994bdf4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef0	True	Passed	Model Under Test Equivalent Model
3c905c70b79fec7077a322735bfffb6165d13a88	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef0	False	Passed	Model Under Test Equivalent Model
0a991db09f1350c44c0eac941ece65e601871f59	Apalache	NotIn	Def1	True	Passed	Model Under Test Equivalent Model
31ccec4d732f91963a9071a7ad313c02ecf3d778	Apalache	NotIn	Def1	False	Passed	Model Under Test Equivalent Model
aaa2a2cb7db9d240effcc3761589c51c9f09f28d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1	True	Passed	Model Under Test Equivalent Model
e62aa61bc3971d4b82708bf2a49c2fb67ffd30f5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1	False	Passed	Model Under Test Equivalent Model
43ed8451074f0ab1942092d54d48a61af14d9c2e	Apalache	NotIn	Def2	True	Passed	Model Under Test Equivalent Model
8483cf6cc7528fd6da1a16c34ca4d12e62cd3451	Apalache	NotIn	Def2	False	Passed	Model Under Test Equivalent Model
d50864e15e6c8d1b43b534e226ceb2fe1f568826	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef2	True	Passed	Model Under Test Equivalent Model
a88ae614a21ffea03d8f0f9a35b4f427e30d46fd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef2	False	Passed	Model Under Test Equivalent Model
622a9ba1869638a23f3df5b0d8fb8571cdb6c71f	Apalache	NotIn	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d16078f1011a3e1cbd8e20f200043086eb25b77e	Apalache	NotIn	Def1Recursive	False	Passed	Model Under Test Equivalent Model
be1a80a1c92c6f53378edc83870b964a84905b8e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
3ee72db16fec0292fce49f5b051a1a1611e01b33	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
4ce3e44eca260fa66c714b054e3f0205994253a7	Apalache	NotIn	Extends	True	Passed	Model Under Test Equivalent Model
c9e90fbce5023c581542c58979f80bd19d204d28	Apalache	NotIn	Extends	False	Passed	Model Under Test Equivalent Model
3403ce865333a0aae6f12c0e851d9ce6c67f64f5	Apalache	NotIn	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
01bf261dd0d931f052eb816d550c744cebdf9b49	Apalache	NotIn	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
937efccc46684a79ab7d6cb9bdb1913c6bfa05c4	Apalache	NotIn	Variable	True	Passed	Model Under Test Equivalent Model
e823b3f8a72b18623913f3620d47ceeeb15c6e6c	Apalache	NotIn	Variable	False	Passed	Model Under Test Equivalent Model
53af9434b42bb20a7c2d9408b26b1c982f658857	Apalache	NotIn	Constant	True	Passed	Model Under Test Equivalent Model
6296764243a0c8b92f033799b3b0b909aa629ac1	Apalache	NotIn	Constant	False	Passed	Model Under Test Equivalent Model
d17c77111e411176c75e591992dba47b47552170	Apalache	NotIn	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
60b53341cfe931d6d0b5eb1e0968baff07bb409b	Apalache	NotIn	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
3f5ee8a027335a73ea5b9401941e605ed3e792ec	Apalache	NotIn	ConstantRank1	True	Passed	Model Under Test Equivalent Model
19f1709798ecc0347dc62e7d7bd7e393627afb45	Apalache	NotIn	ConstantRank1	False	Passed	Model Under Test Equivalent Model
1c45d9b783e9e919997680a402852ac390e32bfd	Apalache	NotIn	Instance	True	Passed	Model Under Test Equivalent Model
34e3fe54718dfe7ddf3b6add0b54f768f5dccbc0	Apalache	NotIn	Instance	False	Passed	Model Under Test Equivalent Model
1ca57a5dc9bd3bf8b0a50380a90c18589ebf2c65	Apalache	NotIn	InstanceWith	True	Passed	Model Under Test Equivalent Model
3689b0ea2d05aee0e9793842ae75c90540f210e1	Apalache	NotIn	InstanceWith	False	Passed	Model Under Test Equivalent Model
d3d285bc1c6794efd5866fe8068801f28c36e2f9	Apalache	NotIn	InstanceNamed	True	Passed	Model Under Test Equivalent Model
2ab0a0fce9a619d4cd1238e1aa691a5bf9edcd4e	Apalache	NotIn	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f044ff10f0ae822e0e178fa4c29055dd81d95b49	Apalache	NotIn	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
89985e78e3be1a64e292bd5cee91375bea4f695d	Apalache	NotIn	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
81e9ae363ada3a04eb37a52e9a2536f121245c6b	Apalache	NotIn	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
26b00f2f5d5baae1393cd6c3d97d55498655940a	Apalache	NotIn	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
f0576f68bdd4847297887ee569f6ef7f1f0870bb	Apalache	NotIn	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
c4841828e9ad98ff87f171aa3a6570b5a97f6d4b	Apalache	NotIn	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
f6f67e41119b94237959e4470692bb370ec597a6	Apalache	NotIn	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
517b95e4f003b2c73007fffd160f67e5de556c52	Apalache	NotIn	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
ec3df896671d6385f9d7ed82bfd506225ee54f33	Apalache	NotIn	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
0f87fc462e2a5383a72cf32d13c84ccd3fcb719d	Apalache	NotIn	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
71ba630e2981eab53c84b0399209d0a44a125f4b	Apalache	NotIn	Enabled	True	Passed	Model Under Test Equivalent Model
fa2cd0b35463fbd7d6f8753a67c75c0aa685490e	Apalache	NotIn	Enabled	False	Passed	Model Under Test Equivalent Model
75980893d9fabe871a5f3f15270d28e60bff9fc2	Apalache	NotIn	Cross2	True	Passed	Model Under Test Equivalent Model
88e7e90e5d191d7b82c7e5c17627d8a49fdfa2f3	Apalache	NotIn	Cross2	False	Passed	Model Under Test Equivalent Model
ec3bc1bd93fc267724225588f005e3788be5f01a	Apalache	NotIn	Cross3	True	Passed	Model Under Test Equivalent Model
287e15940c10bfa5561da5102c4163f106a7f49a	Apalache	NotIn	Cross3	False	Passed	Model Under Test Equivalent Model
3bfa43b41d8ac3b98594ac5377ae6fc4664e078b	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))	NotIn	FunSet	True	Passed	Model Under Test Equivalent Model
1a464122ab66ceadef8f3984c9e3c2df9d099811	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))	NotIn	FunSet	False	Passed	Model Under Test Equivalent Model
287b02b3044dcb2307c24e3ec25b3abfd0d25d0d	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)	NotIn	RecordSet	True	Passed	Model Under Test Equivalent Model
7f2a6f140ede03c6691d0037cf0e0355de7c6954	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)	NotIn	RecordSet	False	Passed	Model Under Test Equivalent Model
ed2eb63933543af0ddc907ad6d6fb57ea24daab1	Apalache	NotIn	SetDiff	True	Passed	Model Under Test Equivalent Model
d3ac2c02c8c88fc1acfc9c19af51b45d05d3e775	Apalache	NotIn	SetDiff	False	Passed	Model Under Test Equivalent Model
a6e666479ab52b765f5338a73a1955a740f18c4a	Apalache	NotIn	SetUnion	True	Passed	Model Under Test Equivalent Model
9f342f798e25affa627378096f0e0eb4fb409651	Apalache	NotIn	SetUnion	False	Passed	Model Under Test Equivalent Model
7dc1c63df80c05c3b8e56914a28119ab3a4f681d	Apalache	NotIn	SetIntersect	True	Passed	Model Under Test Equivalent Model
2bcf97f213e5ee379da55b63baa5efecd73a0c2e	Apalache	NotIn	SetIntersect	False	Passed	Model Under Test Equivalent Model
2b4f71a53302ee0d745acdb86997af1b30ebe75b	Apalache	NotIn	SubsetEq	True	Passed	Model Under Test Equivalent Model
8dc7cfbef89d978d9704dfe217a615857608752f	Apalache	NotIn	SubsetEq	False	Passed	Model Under Test Equivalent Model
2c2de631c33ab05472737cf63f5031530df9906f	Apalache	NotIn	IfCond	True	Passed	Model Under Test Equivalent Model
0bda7928ad802de767f912b6caabde818a49198a	Apalache	NotIn	IfCond	False	Passed	Model Under Test Equivalent Model
c13ed58ade77ff02c9491e011613c342ccc36eb5	Apalache	NotIn	IfThen	True	Passed	Model Under Test Equivalent Model
52dbe711bd66c7eeae1cc2726725426d3d326d33	Apalache	NotIn	IfThen	False	Passed	Model Under Test Equivalent Model
200d1ab604365b478f9403cd721066337623e859	Apalache	NotIn	IfElse	True	Passed	Model Under Test Equivalent Model
9578d144a4c014cc192c42a4a69635327871084a	Apalache	NotIn	IfElse	False	Passed	Model Under Test Equivalent Model
a3289da7a4c977721bca42c9a01e4abfe32e69b0	Apalache	NotIn	Subset	True	Passed	Model Under Test Equivalent Model
2c5fada064435a4d6568c3c9520db8f5f72c278d	Apalache	NotIn	Subset	False	Passed	Model Under Test Equivalent Model
1d11cffdc981a77538d7c43972a6480a1db9e02b	Apalache	NotIn	Domain	True	Passed	Model Under Test Equivalent Model
99b1eb0374be5490ef6de57b7d5e73f36f6c284d	Apalache	NotIn	Domain	False	Passed	Model Under Test Equivalent Model
d6dd6a21d49dc51ab14c9d3a1244e496590280b5	Apalache	NotIn	Union	True	Passed	Model Under Test Equivalent Model
5c69355c7f75584588ea4a23d0cfab926b880ada	Apalache	NotIn	Union	False	Passed	Model Under Test Equivalent Model
f3ab4d8b603af03c143f19fb13eef97f4c094632	Apalache	NotIn	Unchanged	True	Passed	Model Under Test Equivalent Model
2d6815be13cc1b368b6653c88e5978b1ee30b7b0	Apalache	NotIn	Unchanged	False	Passed	Model Under Test Equivalent Model
e79923b0a4062622bedd2efd1e053f818459be5f	Apalache	NotIn	Equivalence	True	Passed	Model Under Test Equivalent Model
c1b86044aa5fb8f9f8e3ef08c291299d01eeff66	Apalache	NotIn	Equivalence	False	Passed	Model Under Test Equivalent Model
e24029dec0a09c1de0c50db275ed6caa475ebd62	Apalache	NotIn	StringEmpty	True	Passed	Model Under Test Equivalent Model
9a192bae1e1474a7f4786473eb78cc119d64ea59	Apalache	NotIn	StringEmpty	False	Passed	Model Under Test Equivalent Model
2755b1e00cdf674f40b8f5030f43d6b09e4db127	Apalache	NotIn	String	True	Passed	Model Under Test Equivalent Model
64178ccef1e1a18b11e31f2843d01df898e340ad	Apalache	NotIn	String	False	Passed	Model Under Test Equivalent Model
becc182c05065a2c38c09074f5403450538eb219	Apalache	NotIn	SeqLen	True	Passed	Model Under Test Equivalent Model
aadf369c06f72d800b292e2d89aa012190f70c9f	Apalache	NotIn	SeqLen	False	Passed	Model Under Test Equivalent Model
26e19ab2425e3cf239e96a23b90819115092ae87	Apalache	NotIn	SeqConcat	True	Passed	Model Under Test Equivalent Model
97ed219615adc2649add57edd4dd154be22464b9	Apalache	NotIn	SeqConcat	False	Passed	Model Under Test Equivalent Model
ccafe4ba02c3dfbf72bfccd0182bb618796f22d9	Apalache	NotIn	SeqSeq	True	Passed	Model Under Test Equivalent Model
f9c2529976d03e48875873f11ea097bdde31f21e	Apalache	NotIn	SeqSeq	False	Passed	Model Under Test Equivalent Model
f71d80fe0e422d806ae958e9fd2d0cd6e4e15120	Apalache	NotIn	NatSet	True	Passed	Model Under Test Equivalent Model
f4d2e40badf9b932ee1964eef3eeead2347268dd	Apalache	NotIn	NatSet	False	Passed	Model Under Test Equivalent Model
6d284d5152bb822207cf54e9a1be82189884beed	Apalache	NotIn	IntSet	True	Passed	Model Under Test Equivalent Model
eeb7bafedea481a6646c01c9f8c4aad09d83a91c	Apalache	NotIn	IntSet	False	Passed	Model Under Test Equivalent Model
064dd30eed6c195807520cce55c2951896b522e1	Apalache	NotIn	StringSet	True	Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)	Model Under Test Equivalent Model
bb44bba33b90384001583991619e8a9549d1930f	Apalache	NotIn	StringSet	False	Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)	Model Under Test Equivalent Model
f046944f185202ccfdf1b2d0f6e50b743a36c160	Apalache	NotIn	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
8fa20b32538e5b6a1f04e55bb7ff07182b369d55	Apalache	NotIn	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
747cef4ea71fb8d5a64c8591c27fb0df0d2e8ecd	Apalache	NotIn	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
82635a59dc65222733d1cecf69661b191decb9a4	Apalache	NotIn	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b1afc0e75a15b368cba448007376f4b0b82997ad	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	NotIn	NumRange	True	Passed	Model Under Test Equivalent Model
0bbe27b6170da985ba40978dff14e2c7cfe9057d	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	NotIn	NumRange	False	Passed	Model Under Test Equivalent Model
da40ec0ab5a671d1dfd4338c58c4318b4574050a	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	NotIn	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
536c305d8dd18fd09423d85da2dc4511a5f3caa0	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	NotIn	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
30c981bdb91a5477e1dbc0dee75c36e564939ff7	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]]	NotIn	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
7be61a7f95ea345fdbddc760ff7f4b47143bf19d	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]]	NotIn	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
bcef4cf7ed254658d4bba17ca3a6539107bf1046	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	NotIn	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
f11d9f37ccefa189b2e7f7c207563c687b7b7ced	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	NotIn	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
463c4eb866da7b6981e699b57630c1485c1f06fe	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	NotIn	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
11a3ab5d570f2133c063de73b153039b79712dd7	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	NotIn	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
65000dec63cbb7ad961181ce098b96ac1d87152b	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	NotIn	TlcEval	True	Passed	Model Under Test Equivalent Model
fc21f2562bcbf987b4c4cd26df6bfe102ba17c6b	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	NotIn	TlcEval	False	Passed	Model Under Test Equivalent Model
b2cfc4b04160a702dbb7032b73b58ab8f2c0b842	Apalache	NotIn	BagBagToSet	True	Passed	Model Under Test Equivalent Model
52d53a6284798cbfbf15169ad69ecb9687864252	Apalache	NotIn	BagBagToSet	False	Passed	Model Under Test Equivalent Model
eb95ba5c15aad8bb6a1132549f34f8c873a8700f	Apalache	NotIn	BagSetToBag	True	Passed	Model Under Test Equivalent Model
212cc5b0901634881ed03fdd5cefcd147743d2e9	Apalache	NotIn	BagSetToBag	False	Passed	Model Under Test Equivalent Model
33e9234283ef7d22d488fcd04b14121732923707	Apalache	NotIn	BagBagIn	True	Passed	Model Under Test Equivalent Model
fdccf38314d8d4f3e51c0d52bf0ace880278f0fa	Apalache	NotIn	BagBagIn	False	Passed	Model Under Test Equivalent Model
e85ebc4980486df1a798ec2e94ffe48678dccca8	Apalache	NotIn	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
fb208f0b0cab41804ff3ec67a72d5bf3a3e0071b	Apalache	NotIn	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
5bb01155d3a480fef100ab57975a6f5b3637c061	Apalache	NotIn	BagAddBag	True	Passed	Model Under Test Equivalent Model
2341b81761195c44b0e387fb202df94acb778c13	Apalache	NotIn	BagAddBag	False	Passed	Model Under Test Equivalent Model
f67a815889d8a9b071b9d58489dd203d37581aff	Apalache	NotIn	BagBagSub	True	Passed	Model Under Test Equivalent Model
34b062ca83520cdd6285ffcc61e6f2c718075e8a	Apalache	NotIn	BagBagSub	False	Passed	Model Under Test Equivalent Model
97e36ce3e2db04397b59abb3e93b08bb55457c33	Apalache	NotIn	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
bc31f19b0733049898ebd4695a0f56856655e6f1	Apalache	NotIn	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
e676266635b03f54c5058be922a1dad8ce40f374	Apalache	NotIn	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
e811105aeb9040cac802f5a76f7218166dfa384b	Apalache	NotIn	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
feb49a590a1907b507c9f4a27bf1f780ebcc1a12	Apalache	NotIn	BagBagUnion	True	Passed	Model Under Test Equivalent Model
0fd94f589d2cb0aa694db448ae9ebfef713ba9ab	Apalache	NotIn	BagBagUnion	False	Passed	Model Under Test Equivalent Model
a29d04f73297207de9abbd7ca32905a1d10f4502	Apalache	NotIn	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7e1e9f6b3047d8a460958e22d3b45d2ac8751daf	Apalache	NotIn	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
86514bab2042d3c81f559f1aac8693686f202f84	Apalache	NotIn	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
f616adbbea0213f26db396d2e912d371e837eb14	Apalache	NotIn	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
d2eae288974c2a0baa96d11a93fd8899530f6488	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	NotIn	BagSubBag	True	Passed	Model Under Test Equivalent Model
771708b597ab4260d8283319ff0f1c952e96185b	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	NotIn	BagSubBag	False	Passed	Model Under Test Equivalent Model
d6face2943b32a104dcebaa876c9425e6a2d24ca	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)	NotIn	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
24a6adbe31df61f4e664b0d6356c7eede0368ded	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)	NotIn	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
9a5654e7276846bf9a933f1c3545df787e220c49	Apalache	NotIn	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
1439f209b51f8c004b0e50e3d4e99537df669646	Apalache	NotIn	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
585c817eaf963fc83ed0d1f12662478b14a925d1	Apalache	NotIn	SeqHead	True	Passed	Model Under Test Equivalent Model
9029f18442546132906ae697e907f1992524df9f	Apalache	NotIn	SeqHead	False	Passed	Model Under Test Equivalent Model
deb3a166239fe3237942aa488adbc83106619c99	Apalache	NotIn	SeqTail	True	Passed	Model Under Test Equivalent Model
21a4293cf813bb3f9f59d291dfe8a5ef3b34e2a3	Apalache	NotIn	SeqTail	False	Passed	Model Under Test Equivalent Model
000498945f5c3cb226ca07ac4871ece923279ac7	Apalache	NotIn	SeqAppend	True	Passed	Model Under Test Equivalent Model
aed591c61ef66ed7a0a7ab72c4c0c84c8c464407	Apalache	NotIn	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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