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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
eee1ba85df7022277c9e55ce9b1bae461e314742	Apalache	And	NotIn	True	Passed	Model Under Test Equivalent Model
66d160461a63d7905b9613901c3c9b4f6d923372	Apalache	And	NotIn	False	Passed	Model Under Test Equivalent Model
3143207a1048ebad5102a402902dbcb4143635e0	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NotIn	True	Passed	Model Under Test Equivalent Model
0b8d51691c5865bbfdc5aefd32d6a72f4fa78bef	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NotIn	False	Passed	Model Under Test Equivalent Model
1ed7ca65a3445defef6a676a8b3133acaef81962	Apalache	Imply	NotIn	True	Passed	Model Under Test Equivalent Model
5d2b6e5bded3630d5b423914e63ead931c9951b3	Apalache	Imply	NotIn	False	Passed	Model Under Test Equivalent Model
1f5a5cb2293754d9015a23b81103f9145e79befa	Apalache	Not	NotIn	True	Passed	Model Under Test Equivalent Model
72573c4f07ac2bb995ebc9699a505bbaaa1aa856	Apalache	Not	NotIn	False	Passed	Model Under Test Equivalent Model
528c7c588dfe173dedece2024cb16e4477746ebc	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NotIn	True	Passed	Model Under Test Equivalent Model
d289ff1ee67088335d0b372a94d21730d6dc67f6	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NotIn	False	Passed	Model Under Test Equivalent Model
f7ad3d51adb3cc4702e9bda74ef62a5fe34bd182	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NotIn	True	Passed	Model Under Test Equivalent Model
7d0b6168e27bac0c427cf8b4a1446e010562902e	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NotIn	False	Passed	Model Under Test Equivalent Model
69a37baed46e3ce18ad3152091c24c53856363a7	Apalache	AndProp	NotIn	True	Passed	Model Under Test Equivalent Model
c7bbf9ea4589559f7ab8acfb5a8a91d35d3dc471	Apalache	AndProp	NotIn	False	Passed	Model Under Test Equivalent Model
ff2f68ebbc4c52472570c2751600e9ee97e41850	Apalache	Boxed	NotIn	True	Passed	Model Under Test Equivalent Model
2e74565d7dc68e62f66fa24f461dadf96fba7125	Apalache	Boxed	NotIn	False	Passed	Model Under Test Equivalent Model
ab5df77fb6e2568287b863ab2326443a4b156e05	Apalache	Eq	NotIn	True	Passed	Model Under Test Equivalent Model
78885706e30fa41d7c5919488ac36e92a65e1ec0	Apalache	Eq	NotIn	False	Passed	Model Under Test Equivalent Model
c96fb7146c64a51e3921f4efc81a7ed30aea3c31	Apalache	Ne	NotIn	True	Passed	Model Under Test Equivalent Model
340e7e9cb60e3556cb0bb3591232ef6d20397eac	Apalache	Ne	NotIn	False	Passed	Model Under Test Equivalent Model
98e3356685f785c882aaa53fa4ad3246c0bee7f1	Apalache	Let	NotIn	True	Passed	Model Under Test Equivalent Model
f50a5badbefd638945edc5b71b0739c7175ac673	Apalache	Let	NotIn	False	Passed	Model Under Test Equivalent Model
e340854c97f8489faadf2c0427594b2b873a4d19	Apalache	Set0	NotIn	True	Passed	Model Under Test Equivalent Model
8e107f584b693852bea97de22f692796775dd119	Apalache	Set0	NotIn	False	Passed	Model Under Test Equivalent Model
ea500bf8080c45219d2fe02b3b6c5f641f432bf6	Apalache	Set1	NotIn	True	Passed	Model Under Test Equivalent Model
cbbe01f6c2d86600635e61b05cd336dec24c0f4e	Apalache	Set1	NotIn	False	Passed	Model Under Test Equivalent Model
1c1b514c7db1636e816586b00099a05fae6f7bdd	Apalache	Set2	NotIn	True	Passed	Model Under Test Equivalent Model
fdb75b3b4f724d6222a0d2cead5fda5aaaed85f1	Apalache	Set2	NotIn	False	Passed	Model Under Test Equivalent Model
1bfd3d9e4f3be26e7a9788a00b5da291c2f50d7b	Apalache	Fun	NotIn	True	Passed	Model Under Test Equivalent Model
77a05adcd9a1393feeec2ea50186521b8fa45f71	Apalache	Fun	NotIn	False	Passed	Model Under Test Equivalent Model
456dec3fab2e8e98f2f419c7611329596b796731	Apalache	In	NotIn	True	Passed	Model Under Test Equivalent Model
10179ce0ff73a4944cd467dcc3c8eb2e27d2978b	Apalache	In	NotIn	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
38f82774379bc72569da49066f02992f0465e87f	Apalache	Exists	NotIn	True	Passed	Model Under Test Equivalent Model
c53868d21b28a0f3401076648fda4a2bf79db959	Apalache	Exists	NotIn	False	Passed	Model Under Test Equivalent Model
4dc7205527ce5820efba6326d5035ec7f1808728	Apalache	Forall	NotIn	True	Passed	Model Under Test Equivalent Model
caabe42270996a302d085b774cff4a7b13422fc0	Apalache	Forall	NotIn	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
0b12d02e052cd1f8cae27a42d4f745edb26758f2	Apalache	Record	NotIn	True	Passed	Model Under Test Equivalent Model
74b0e20374ffa4931501f22e63935f22f77c0101	Apalache	Record	NotIn	False	Passed	Model Under Test Equivalent Model
0dc405b7745772511341ff5f00e5aecbaa914b2a	Apalache	Tuple	NotIn	True	Passed	Model Under Test Equivalent Model
9f504b0ab7a7aaee16081a28bf9a7dc7755252b1	Apalache	Tuple	NotIn	False	Passed	Model Under Test Equivalent Model
69517f5a04a46f437bc10b64b919ab49316206ec	Apalache	FunApp	NotIn	True	Passed	Model Under Test Equivalent Model
f708613bf0af7918792d0a093acde6bd4040fe83	Apalache	FunApp	NotIn	False	Passed	Model Under Test Equivalent Model
bfb0244d387b593c81eb25f52443e0b0119c1f88	Apalache	Except1Fun	NotIn	True	Passed	Model Under Test Equivalent Model
f704a9d214b14a75e0ec6a7eb6168f739897c6e6	Apalache	Except1Fun	NotIn	False	Passed	Model Under Test Equivalent Model
37de4f31399858c9aa6a38a8584f6dba975d10cc	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NotIn	True	Passed	Model Under Test Equivalent Model
e05f33b556069697c15fb0f3237c8418329f6234	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NotIn	False	Passed	Model Under Test Equivalent Model
7148f9d80e78547066ef1044e93a5efef261223f	Apalache	Except1Rec	NotIn	True	Passed	Model Under Test Equivalent Model
e792626c69061450bff659c14860be8885e48ef2	Apalache	Except1Rec	NotIn	False	Passed	Model Under Test Equivalent Model
d08e1020e6c2afd21ab302ea45e3522c67fc0815	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NotIn	True	Passed	Model Under Test Equivalent Model
6eb603ef7ea825e0e0940099e6e0de86c3709f84	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NotIn	False	Passed	Model Under Test Equivalent Model
e70449cc1a98b4c834d0444ab389aab60faad5e4	Apalache	Except2Fun	NotIn	True	Passed	Model Under Test Equivalent Model
1502032a69636fff6a7acfec13eabadbae552fa9	Apalache	Except2Fun	NotIn	False	Passed	Model Under Test Equivalent Model
beadff560b2cdacdc72fabe4e8d1a19798340d44	Apalache	Prime	NotIn	True	Passed	Model Under Test Equivalent Model
8b2cf484b18bb1ede9b23c65392cc744e7ae33d1	Apalache	Prime	NotIn	False	Passed	Model Under Test Equivalent Model
c105657ea63ba9af23b8e0c7dd9a5f1eef2ce177	Apalache	DefFun	NotIn	True	Passed	Model Under Test Equivalent Model
d75b1bf5b48b3b210435327cb85efcf297f8b533	Apalache	DefFun	NotIn	False	Passed	Model Under Test Equivalent Model
d8438bf58466e39791d67f857dd1c7a4bef8d944	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NotIn	True	Passed	Model Under Test Equivalent Model
b5ee44b2b55acf7cc10142bf0905326d93a53200	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NotIn	False	Passed	Model Under Test Equivalent Model
0e1640ac5788d45e87211a0781d8c6330f061731	Apalache	DefFunRecursive	NotIn	True	Passed	Model Under Test Equivalent Model
e179bc261f1792fe212730f98549a0e01daefa90	Apalache	DefFunRecursive	NotIn	False	Passed	Model Under Test Equivalent Model
30876f925c466a8861700922bc72796d90234d3a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NotIn	True	Passed	Model Under Test Equivalent Model
8ea36c388e6bd7486b500f016f201b43e7dee0a2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NotIn	False	Passed	Model Under Test Equivalent Model
d7313984f72b58cf543177571188dece8fd517e6	Apalache	Def0	NotIn	True	Passed	Model Under Test Equivalent Model
797c67aeceeaf7da9bb49b54941ffc306043007b	Apalache	Def0	NotIn	False	Passed	Model Under Test Equivalent Model
8d9aa3dcd70eeb714bf0d3c534888b4da3d977c9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NotIn	True	Passed	Model Under Test Equivalent Model
27c07f6e054ba11583d8b5bb390ca3d11c11fc80	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NotIn	False	Passed	Model Under Test Equivalent Model
06d42f8c76d8980f196c75eb395cad0c1655b703	Apalache	Def1	NotIn	True	Passed	Model Under Test Equivalent Model
351ba44d780524a2887fba01b6dc3d02f3415225	Apalache	Def1	NotIn	False	Passed	Model Under Test Equivalent Model
06610d686817b239b89dffcc3c4063407a02b71c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NotIn	True	Passed	Model Under Test Equivalent Model
27018e7d26ac66864b2a6e3d42318897fdbf529c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NotIn	False	Passed	Model Under Test Equivalent Model
a06fd380e34bad656b6942616923a13f07c018f0	Apalache	Def2	NotIn	True	Passed	Model Under Test Equivalent Model
53d14fe57732f4fdb1dd2edca804ffa08ee8c1e9	Apalache	Def2	NotIn	False	Passed	Model Under Test Equivalent Model
ed5ec3e5d78f056f2a84c2bb81e3df2505ebf991	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NotIn	True	Passed	Model Under Test Equivalent Model
f38321bae52082cd8958c453f73c93e96c4ce4e4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NotIn	False	Passed	Model Under Test Equivalent Model
c54762180727e8d1156a79721281723e776b88cb	Apalache	Def1Recursive	NotIn	True	Passed	Model Under Test Equivalent Model
21fd4e75a9ee8fa8edcc0e4af46a3c01e63d3851	Apalache	Def1Recursive	NotIn	False	Passed	Model Under Test Equivalent Model
bf56f702929b95385cbf4e28749feab4a0e76da4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NotIn	True	Passed	Model Under Test Equivalent Model
276908096f141af336fa1749ec20a4f5a5b487e8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NotIn	False	Passed	Model Under Test Equivalent Model
05f59a8ff0114ca8e6d3286050d0f1756e195625	Apalache	Extends	NotIn	True	Passed	Model Under Test Equivalent Model
b946b97866900b336ffd63a5f948901a0e08b05a	Apalache	Extends	NotIn	False	Passed	Model Under Test Equivalent Model
3b600c3e6ebeb2ea31a6d7aaf0a4f60e6a7952c0	Apalache	ExtendsInDifferentFolder	NotIn	True	Passed	Model Under Test Equivalent Model
e1eff0568441b8bb6a184df17826f1f4f064f9a5	Apalache	ExtendsInDifferentFolder	NotIn	False	Passed	Model Under Test Equivalent Model
49bd6ff1fbe9b0cc165879a58df924eeb069d71f	Apalache	Variable	NotIn	True	Passed	Model Under Test Equivalent Model
58d712a5d5715fa8b8e4c4dc02847b82f9554a3f	Apalache	Variable	NotIn	False	Passed	Model Under Test Equivalent Model
bf11a78f9d4e3de6a850ce0d1214f888053efb8e	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NotIn	True	Passed	Model Under Test Equivalent Model
cb33cc0abecea0bd53238ecdf15fbfcf7838f268	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NotIn	False	Passed	Model Under Test Equivalent Model
ed9a736a3b9917c5e97639b28861fd33ca043789	Apalache	Constant	NotIn	True	Passed	Model Under Test Equivalent Model
c371ae08fbf90be7573b88f87bbb27468362c22a	Apalache	Constant	NotIn	False	Passed	Model Under Test Equivalent Model
99baa549a33446f3c9e871c0cf0f6bde933bf22d	Apalache	ConstantRank1	NotIn	True	Passed	Model Under Test Equivalent Model
a7f3bdfa9a4b285990803ff062323a7456fc2ec0	Apalache	ConstantRank1	NotIn	False	Passed	Model Under Test Equivalent Model
b58aeb69b496faaf5c1970574660b0f4a433af88	Apalache	Instance	NotIn	True	Passed	Model Under Test Equivalent Model
773cbd220d8e716764bc21e9749990de33412a41	Apalache	Instance	NotIn	False	Passed	Model Under Test Equivalent Model
a1084e43064c70eab0db484954f09c8fb5d49310	Apalache	InstanceWith	NotIn	True	Passed	Model Under Test Equivalent Model
7cdb3277ca7c0a248b25fa83c3364ad4bb5fc3f2	Apalache	InstanceWith	NotIn	False	Passed	Model Under Test Equivalent Model
35e5142dced7199b2f5c070bba60acf41b9f0905	Apalache	InstanceNamed	NotIn	True	Passed	Model Under Test Equivalent Model
15c17cc5cce1f1021f66034e5c1cfd21f5c3da63	Apalache	InstanceNamed	NotIn	False	Passed	Model Under Test Equivalent Model
80e57d253aa2b9e19142fee4ae786026e08a1df8	Apalache	InstanceNamedWith	NotIn	True	Passed	Model Under Test Equivalent Model
56eabd7af7327468a67b2e548c0291ce0ddef95f	Apalache	InstanceNamedWith	NotIn	False	Passed	Model Under Test Equivalent Model
89605595254f402e5b414f630d9c18c8c1771528	Apalache	InstanceInFolder	NotIn	True	Passed	Model Under Test Equivalent Model
fc6685871f0baf832664a216cbaaa57cffbf6ec0	Apalache	InstanceInFolder	NotIn	False	Passed	Model Under Test Equivalent Model
67950e9ebafa70d4d2e6533799ed56624651d222	Apalache	InstanceWithInFolder	NotIn	True	Passed	Model Under Test Equivalent Model
d2040ab34d875c572910d2a6ee53ccc0dbb798f4	Apalache	InstanceWithInFolder	NotIn	False	Passed	Model Under Test Equivalent Model
8a93c1434e14bc37983c026fd04cb1ad9533d738	Apalache	InstanceNamedInFolder	NotIn	True	Passed	Model Under Test Equivalent Model
70a85897e28dfe6fd2007de8577339d9efa28d76	Apalache	InstanceNamedInFolder	NotIn	False	Passed	Model Under Test Equivalent Model
c11d7accc8e74a0fee2d53e3b1e8c7209c9fce65	Apalache	InstanceNamedWithInFolder	NotIn	True	Passed	Model Under Test Equivalent Model
95c9b01eb2abc6d293a7dd8b73308919be240f4d	Apalache	InstanceNamedWithInFolder	NotIn	False	Passed	Model Under Test Equivalent Model
f5e6368168df6219190193c4943cee118d2f3c59	Apalache	Enabled	NotIn	True	Passed	Model Under Test Equivalent Model
89cb0538b9513bd1a4775748573793bf7fc9c956	Apalache	Enabled	NotIn	False	Passed	Model Under Test Equivalent Model
51d55bf898256dce6f782cfcabc4fad5b213cd8c	Apalache	Assume	NotIn	True	Passed	Model Under Test Equivalent Model
c5ef6eec654badfb46954fbd5fc921b7dfdb412e	Apalache	Assume	NotIn	False	Passed	Model Under Test Equivalent Model
5d5e474a582b30c272514a6498d50f695e323c2d	Apalache	AssumeNamed	NotIn	True	Passed	Model Under Test Equivalent Model
0deb3f13fb9bca1f9a0da80ce875f9e30142e409	Apalache	AssumeNamed	NotIn	False	Passed	Model Under Test Equivalent Model
e39dbb7195c8a96f29a1a2de2afe73930f9ffc31	Apalache	Lambda	NotIn	True	Passed	Model Under Test Equivalent Model
47c7f0a48d4a3518ea936f4e8d3e0da5b30947de	Apalache	Lambda	NotIn	False	Passed	Model Under Test Equivalent Model
2554d3e18971170866f1b656dd9ab9af86b9b025	Apalache	IfCond	NotIn	True	Passed	Model Under Test Equivalent Model
e029e60af36a3e8da8d3383c42b186bdeaef9ad2	Apalache	IfCond	NotIn	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
afcea0c50c15534365422ae97d9984156a607b97	Apalache	IfElse	NotIn	True	Passed	Model Under Test Equivalent Model
3daa4d8375f08f327143649bb1f61f4cb0a00b8b	Apalache	IfElse	NotIn	False	Passed	Model Under Test Equivalent Model
fc860f6e8786856a5efe0dbd5bf6761f6eed538c	Apalache	Unchanged	NotIn	True	Passed	Model Under Test Equivalent Model
074de848c60abb1d4a8475d5a64702e6a54b8aad	Apalache	Unchanged	NotIn	False	Passed	Model Under Test Equivalent Model
828e5626794050a5429df68c2e5fe2b76e57183c	Apalache	Equivalence	NotIn	True	Passed	Model Under Test Equivalent Model
5fbc79603196bdfa7bacdbbab477ed0a1bf124c0	Apalache	Equivalence	NotIn	False	Passed	Model Under Test Equivalent Model
b12417e1a57e1dfac6cb0ddf10287142ca6c812b	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NotIn	True	Passed	Model Under Test Equivalent Model
5da4017a811f5b35ee0c09199ae2271430f93825	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NotIn	False	Passed	Model Under Test Equivalent Model
170c209d32ee0e62f04677356e16c27251f31080	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NotIn	True	Passed	Model Under Test Equivalent Model
8b31f01d78eb25d77b0db305254d168e1d9b9d13	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NotIn	False	Passed	Model Under Test Equivalent Model
3bca67b07d57f1f9754b14dbdebd8ea8d7ff43cb	Apalache	BagBagIn	NotIn	True	Passed	Model Under Test Equivalent Model
e85b6fbd9f23789fc73666cdbe14d07db79a7366	Apalache	BagBagIn	NotIn	False	Passed	Model Under Test Equivalent Model
6ff1380f6ccf78ea9aaada46429509318c46cb07	Apalache	BagCopiesIn	NotIn	True	Passed	Model Under Test Equivalent Model
c9f8edb56d94b27490be53520b0e36571cbb3f11	Apalache	BagCopiesIn	NotIn	False	Passed	Model Under Test Equivalent Model
0a9086f1bd57722291e407595bfec052385f1bc9	Apalache	SeqAppend	NotIn	True	Passed	Model Under Test Equivalent Model
7899d5845031f1eef0d093bf13c8d2fad3a65275	Apalache	SeqAppend	NotIn	False	Passed	Model Under Test Equivalent Model

Index

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