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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b41e3a2563e7102b6d5dfb68171eec82da16e18f	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Fun	OneLineComment	True	Passed	Model Under Test Equivalent Model
0c8ffa34134c13095da8fc00fc5b4171c185a20e	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Fun	OneLineComment	False	Passed	Model Under Test Equivalent Model
47f869c646cee7843e41df8041610aaa3486d829	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Fun	MultiLineComment	True	Passed	Model Under Test Equivalent Model
e61088a9bc1ba0cb6519cca017b9beebca6d4505	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Fun	MultiLineComment	False	Passed	Model Under Test Equivalent Model
9945aaa080825ebbc27a182aab23409a3e711c64	Apalache	Except1Fun	BoolTrue	True	Passed	Model Under Test Equivalent Model
a0b86474790744ab419ad2ce21e10af970db4714	Apalache	Except1Fun	BoolTrue	False	Passed	Model Under Test Equivalent Model
5fe36f301b5c68b14c5fbfda7868a58680b4cd51	Apalache	Except1Fun	BoolFalse	True	Passed	Model Under Test Equivalent Model
bb38fb00b68364db31a172800c8f3c0c1da52b2c	Apalache	Except1Fun	BoolFalse	False	Passed	Model Under Test Equivalent Model
64cece7efba20fd81ab0d7cf68d0862e9757a483	Apalache	Except1Fun	BoolSet	True	Passed	Model Under Test Equivalent Model
e1db0a04cff159a69af251a29eac76941d0c0917	Apalache	Except1Fun	BoolSet	False	Passed	Model Under Test Equivalent Model
ba2ca2d336de0ddaa7fdebd3e79eb3fad39238cf	Apalache	Except1Fun	And	True	Passed	Model Under Test Equivalent Model
4d2cff560c49e8c03609f708200bdd8cd05bc9ff	Apalache	Except1Fun	And	False	Passed	Model Under Test Equivalent Model
8aceef69ef647416aeab598af3454a71174a5edd	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except1Fun	AndMultiLine	True	Passed	Model Under Test Equivalent Model
3e4395aa5111436fd853c5d8d95b95d0834e98f9	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except1Fun	AndMultiLine	False	Passed	Model Under Test Equivalent Model
f5c35e381f22a9dde66adaa734faf2afff5f376d	Apalache	Except1Fun	Imply	True	Passed	Model Under Test Equivalent Model
792a0444181b53ac5d1a06590974e344329b1c29	Apalache	Except1Fun	Imply	False	Passed	Model Under Test Equivalent Model
f0d887f774e10c62e02b8b9b54d5cfbf0c3956e2	Apalache	Except1Fun	Not	True	Passed	Model Under Test Equivalent Model
591e98ed958b2b6ec167764f6f9c978a93f8a62e	Apalache	Except1Fun	Not	False	Passed	Model Under Test Equivalent Model
a0108e8f132159b178cd7d65196300ee19e09a90	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except1Fun	Or	True	Passed	Model Under Test Equivalent Model
ba733b0c9d7572ef23412608b36f02a5585d45dd	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except1Fun	Or	False	Passed	Model Under Test Equivalent Model
b5fccd1db31504cccabc5d589c239a7b739dce05	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except1Fun	OrMultiLine	True	Passed	Model Under Test Equivalent Model
cadae42d5463b7b8b8d4eab02e90eaa20960c59c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except1Fun	OrMultiLine	False	Passed	Model Under Test Equivalent Model
3b090b08c143d8014ca8a2660b1a4a5afa612085	Apalache	Except1Fun	Eq	True	Passed	Model Under Test Equivalent Model
eccd60ebc5be9410b560c61a9717a7382a60dade	Apalache	Except1Fun	Eq	False	Passed	Model Under Test Equivalent Model
c4b6a3d7c0b7a335f4112a6e15f716eb048593ee	Apalache	Except1Fun	Ne	True	Passed	Model Under Test Equivalent Model
80ee70f30544c1b711105d9223f5c4bbebaa58f8	Apalache	Except1Fun	Ne	False	Passed	Model Under Test Equivalent Model
ed1f4d51e70139e7a1e8d6b995d382b31a789141	Apalache	Except1Fun	Let	True	Passed	Model Under Test Equivalent Model
d27eb606dec72c536fbe157f7bc6c6edb74f4382	Apalache	Except1Fun	Let	False	Passed	Model Under Test Equivalent Model
acc9529531df61de46e735c2991336606093a1ed	Apalache	Except1Fun	SetEmpty	True	Passed	Model Under Test Equivalent Model
7716a7e7730472705df34755afd80083cfc4bf66	Apalache	Except1Fun	SetEmpty	False	Passed	Model Under Test Equivalent Model
ae98c0d2d80f264310eb14a91e82566aa236f906	Apalache	Except1Fun	Set0	True	Passed	Model Under Test Equivalent Model
3123b3aa3fa4019eba684e06c73745f5cfc02a08	Apalache	Except1Fun	Set0	False	Passed	Model Under Test Equivalent Model
474fe47219f91dca08030e69bbea18a524bab803	Apalache	Except1Fun	Set1	True	Passed	Model Under Test Equivalent Model
afb30d049f321adc12e3aa7fcce09aed8dcd4606	Apalache	Except1Fun	Set1	False	Passed	Model Under Test Equivalent Model
1ef88b6d80a58c4433d8c752322575a7ef52b391	Apalache	Except1Fun	Set2	True	Passed	Model Under Test Equivalent Model
8252e897684d7037cda6d4376f6e6bb41e19b6cf	Apalache	Except1Fun	Set2	False	Passed	Model Under Test Equivalent Model
e322b7df9f2f8fe24bf5ee60f1268df1b31fad5d	Apalache	Except1Fun	Fun	True	Passed	Model Under Test Equivalent Model
32d41e363f590102915d92475f04d489eceea742	Apalache	Except1Fun	Fun	False	Passed	Model Under Test Equivalent Model
c9bf9079b3157217cad6b02b760b7fba7c839524	Apalache	Except1Fun	In	True	Passed	Model Under Test Equivalent Model
7979e69b39cc831ae05cc48be4bc6e0b98326eaa	Apalache	Except1Fun	In	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
7ba6485b5279838460f2e4616de86519325c3e7d	Apalache	Except1Fun	Exists	True	Passed	Model Under Test Equivalent Model
64f8d4a1f8953ceb344f78c5f9e4941b3b124653	Apalache	Except1Fun	Exists	False	Passed	Model Under Test Equivalent Model
b9ad83f962b21b5c22c0f9f29ffb206ab0285062	Apalache	Except1Fun	Forall	True	Passed	Model Under Test Equivalent Model
c18a2df18df7bcb94584de759bd7a4069f5564c9	Apalache	Except1Fun	Forall	False	Passed	Model Under Test Equivalent Model
ed3312449751101ce68368ff3b9ab8666548d252	Apalache	Except1Fun	Choose	True	Passed	Model Under Test Equivalent Model
cf2792419f1920f0327734bdee1b39c009b3dac4	Apalache	Except1Fun	Choose	False	Passed	Model Under Test Equivalent Model
40795b2146648c593de0146fdc9db079aad87ac1	Apalache	Except1Fun	Record	True	Passed	Model Under Test Equivalent Model
27b99f8735ff952cd24d1aa238eb1c5f3df29a94	Apalache	Except1Fun	Record	False	Passed	Model Under Test Equivalent Model
205b6c594d04e06e4d230c3b54512bc6524a6814	Apalache	Except1Fun	Tuple	True	Passed	Model Under Test Equivalent Model
a470867e4aaf7461e57e903fc6dc6e782f1dfa6b	Apalache	Except1Fun	Tuple	False	Passed	Model Under Test Equivalent Model
7d01c8c08b1d4cac9bd7a4720a4a4d2e0c555a1e	Apalache	Except1Fun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d01631db577a1df9c2f5239961068655ff62863a	Apalache	Except1Fun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
8bcf8d2e40cd3c08a7b8196b8827ffcdfa873198	Apalache	Except1Fun	FunApp	True	Passed	Model Under Test Equivalent Model
35232392003964841d9b3a4219e9f3ce6a539083	Apalache	Except1Fun	FunApp	False	Passed	Model Under Test Equivalent Model
31e956943743cbfae444713338580e09050a87ff	Apalache	Except1Fun	Prime	True	Passed	Model Under Test Equivalent Model
361b4726c24116a2a545d4e81a3b9f78872a4b54	Apalache	Except1Fun	Prime	False	Passed	Model Under Test Equivalent Model
04580a52ebcc7599a7f8c96c1d73d32341deafc7	Apalache	Except1Fun	NumZero	True	Passed	Model Under Test Equivalent Model
e4ffb5ff8f93f513ae4f2ee34d6ea35be39842db	Apalache	Except1Fun	NumZero	False	Passed	Model Under Test Equivalent Model
3612df7db23830bdf9fafce8475c81bec16edb97	Apalache	Except1Fun	NumOne	True	Passed	Model Under Test Equivalent Model
f90982902627be8c0bfd427a860677468599dc59	Apalache	Except1Fun	NumOne	False	Passed	Model Under Test Equivalent Model
cffc639f9f0844873dd8cb06dda26c384f8196d0	Apalache	Except1Fun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
4cd1180faaccbd609bc6b45adb1ae378b2b9a967	Apalache	Except1Fun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
a0f9413b76e5ebab3ed3a00f36c89bbf22959b2a	Apalache	Except1Fun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
52724095821212b3960acee4dccf3744d25584da	Apalache	Except1Fun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a97cba1cc825c722170d48902a63342333f1bdba	Apalache	Except1Fun	NumPlus	True	Passed	Model Under Test Equivalent Model
5182bbe9b6c811e116417dedccb6783d59928410	Apalache	Except1Fun	NumPlus	False	Passed	Model Under Test Equivalent Model
eeb29330a616dbd2b2f74ebc648d38225115cfea	Apalache	Except1Fun	NumMinus	True	Passed	Model Under Test Equivalent Model
03683e438f54e5da32328fdf0bdce41951f58dcd	Apalache	Except1Fun	NumMinus	False	Passed	Model Under Test Equivalent Model
a3d043a722993e015c5b4126550171a985e80715	Apalache	Except1Fun	NumMul	True	Passed	Model Under Test Equivalent Model
b9546f4e34401da251b69b0c645a976dc1b5d166	Apalache	Except1Fun	NumMul	False	Passed	Model Under Test Equivalent Model
87e344b687410ebb8d2582ef2c4bd6227bc64fa5	Apalache	Except1Fun	NumDiv	True	Passed	Model Under Test Equivalent Model
7691f2323ae838641a7abc9c4a42168dbf69bc1d	Apalache	Except1Fun	NumDiv	False	Passed	Model Under Test Equivalent Model
9034a60883d209ed0e2db6f71601f22306879363	Apalache	Except1Fun	NumMod	True	Passed	Model Under Test Equivalent Model
a0f97be00d37534c6d92b64507b8b0842854fc78	Apalache	Except1Fun	NumMod	False	Passed	Model Under Test Equivalent Model
251555d56d0b4994d61a23336b3ed813a6bfb3a4	Apalache	Except1Fun	NumPow	True	Passed	Model Under Test Equivalent Model
b80cab2ac8718f42ca94e9bd5290d68c129e15a0	Apalache	Except1Fun	NumPow	False	Passed	Model Under Test Equivalent Model
960a9ca6cb49e5adc61316516980b143b34ef1b5	Apalache	Except1Fun	NumGt	True	Passed	Model Under Test Equivalent Model
09f76d2b1e9646a8316f858acdbc4c4a5d73686b	Apalache	Except1Fun	NumGt	False	Passed	Model Under Test Equivalent Model
41c03947041946a879391c28a845a391a67dfe22	Apalache	Except1Fun	NumGe	True	Passed	Model Under Test Equivalent Model
c43bcaa0a98f41ede9aabb4636c9d99507412beb	Apalache	Except1Fun	NumGe	False	Passed	Model Under Test Equivalent Model
19fa160f1e84b949cd357094c9e9064427c5116c	Apalache	Except1Fun	NumLt	True	Passed	Model Under Test Equivalent Model
7babeac9df52c31b58707fc7902ddf2d01f2621c	Apalache	Except1Fun	NumLt	False	Passed	Model Under Test Equivalent Model
85668276ecb25837e61fb2c56b0edd513a677ab1	Apalache	Except1Fun	NumLe	True	Passed	Model Under Test Equivalent Model
26405a1ac29cb4de57ef0ee2418f3ae3ea6f0dea	Apalache	Except1Fun	NumLe	False	Passed	Model Under Test Equivalent Model
4b9437d54569183987e43acaea4c3132e532b4ac	Apalache	Except1Fun	DefFun	True	Passed	Model Under Test Equivalent Model
2016104c608eb18c9bab0db18bde57860ed230f5	Apalache	Except1Fun	DefFun	False	Passed	Model Under Test Equivalent Model
7e7c124bbcfce131c27b61df41070c1cd95c7ec4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDefFun	True	Passed	Model Under Test Equivalent Model
e5871d37ee431e82bc90c307d6066aec6143332c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDefFun	False	Passed	Model Under Test Equivalent Model
0b89261df606041a51c75d2eec967992c1340ea1	Apalache	Except1Fun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
13c59c9a29dd3987fadf1b2648e381773d39ad58	Apalache	Except1Fun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
a7ac41805e8117625e491362c8b49bf4b2d28dbc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
f065732b275b4b940b8ff59a439ddc7d59495f4e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
5de6210550ae75b2eb1a3b896eea77ca490cce3f	Apalache	Except1Fun	Def0	True	Passed	Model Under Test Equivalent Model
33ded0b76d567db843f88f8bab1ebac403272257	Apalache	Except1Fun	Def0	False	Passed	Model Under Test Equivalent Model
01c1681a353010cd1aee76b668e3e3fd0b44fcb4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef0	True	Passed	Model Under Test Equivalent Model
3444e9bac2ade5cadd40de792dee67455073e15f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef0	False	Passed	Model Under Test Equivalent Model
d9393f6506dcc4dadd8bd85458f8d6d02d828e34	Apalache	Except1Fun	Def1	True	Passed	Model Under Test Equivalent Model
8902f5d1d661cd13dc723546b9c2b4e232555d27	Apalache	Except1Fun	Def1	False	Passed	Model Under Test Equivalent Model
c78af8afda30555fac2ce3b4e04c0b79e291af10	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1	True	Passed	Model Under Test Equivalent Model
a6a7769a534255e59a6c9b646115e7b64e2e5884	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1	False	Passed	Model Under Test Equivalent Model
ee7385550b265d9d8239f4ab04973faeada0fcc4	Apalache	Except1Fun	Def2	True	Passed	Model Under Test Equivalent Model
4012a4729ea572c4d238ed10d37e228c8a926858	Apalache	Except1Fun	Def2	False	Passed	Model Under Test Equivalent Model
753db5a2d36dc4611effcb284e2975b19f8b7c07	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef2	True	Passed	Model Under Test Equivalent Model
fe4104148a794423935fd32225f7b3eca07c1584	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef2	False	Passed	Model Under Test Equivalent Model
36d721a7f6817b19a9675fa2804195e1386f7294	Apalache	Except1Fun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
7adffe5fe45449ad8aae22ba296c96207a6b1574	Apalache	Except1Fun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
49db3dedffc47c07492a9bcfb488fc2507ecb39d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
1e043f23d318492e930244496ec873b45661dcbe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
030cbb70c23305cda0b8148b7e4d40b3ee118d49	Apalache	Except1Fun	Extends	True	Passed	Model Under Test Equivalent Model
243d088743f587f0781c384ec24531ca900d2a63	Apalache	Except1Fun	Extends	False	Passed	Model Under Test Equivalent Model
26c848e80b0b28c7b5c4108f55558fbf2740af47	Apalache	Except1Fun	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
e2cf2250abbcaf4c9b5991a4ff8dc74baee23c73	Apalache	Except1Fun	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
8c00702f66259010cb14bed905c97ffa40254d28	Apalache	Except1Fun	Variable	True	Passed	Model Under Test Equivalent Model
4860a6f010088501853eea3eeb8a8821281e69f3	Apalache	Except1Fun	Variable	False	Passed	Model Under Test Equivalent Model
5571804e115ae405a51f992b2eea3dde5608c4cb	Apalache	Except1Fun	Constant	True	Passed	Model Under Test Equivalent Model
7e8346f3f147f192c89853ca0199585265230190	Apalache	Except1Fun	Constant	False	Passed	Model Under Test Equivalent Model
4ca3238aa4ad7ecb343c3b9dbdef6a57cb4a2b5b	Apalache	Except1Fun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
65265f0b39f1c909626de1c80560e364f1b48286	Apalache	Except1Fun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
38ca7ddd5de1b18131368bad914538c6230636d0	Apalache	Except1Fun	Instance	True	Passed	Model Under Test Equivalent Model
c5ea3173a315dc4802fcf7eb5ebe8110774eb6c5	Apalache	Except1Fun	Instance	False	Passed	Model Under Test Equivalent Model
70183e98326068c81d96ab24cf13fc35e9d00f9b	Apalache	Except1Fun	InstanceWith	True	Passed	Model Under Test Equivalent Model
1d0ed7218107380e2f98d5b364172c78e62838ca	Apalache	Except1Fun	InstanceWith	False	Passed	Model Under Test Equivalent Model
8ac4341e9bd07a36f2cda098f30e7fb56c88c96b	Apalache	Except1Fun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
92281c5dac73ab436037d69adbf39454f4221291	Apalache	Except1Fun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fce4c0e13b916373f5a19ceb99c1168e27ba0be7	Apalache	Except1Fun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
d0251913d9d823f682b078916ce0027296a7b8e0	Apalache	Except1Fun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
457c4c62043fb8e103a208a00ff0a6f5608a22e5	Apalache	Except1Fun	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
99a21ddf1bd0b94413885938254c8252b15963f5	Apalache	Except1Fun	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
d9270d5f45079c7adc9e47b3365cf785e0c556ef	Apalache	Except1Fun	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
a1788f13815e6062faebb1105d0c0a907b5143b0	Apalache	Except1Fun	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
d2f51b34043415671e312b95fee6cb461199acb9	Apalache	Except1Fun	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
624c4663f01c93971c29bf82028679bb8eaa2708	Apalache	Except1Fun	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
2a12083c64837f36921160035d2cd679cf85ac66	Apalache	Except1Fun	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
e024cc8c3539af2278052850ac9210ad866d9cbb	Apalache	Except1Fun	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
4e07f865d562d1017315de9a97af0463bcbc5568	Apalache	Except1Fun	Enabled	True	Passed	Model Under Test Equivalent Model
81bfb37b4326fa6c3805948c61ee4958b6855c32	Apalache	Except1Fun	Enabled	False	Passed	Model Under Test Equivalent Model
d147b9f16506daccbeff4526cc91e21896f017f8	Apalache	Except1Fun	Cross2	True	Passed	Model Under Test Equivalent Model
d55913f0c94f837a6fa09709901d377840ab3d5f	Apalache	Except1Fun	Cross2	False	Passed	Model Under Test Equivalent Model
0d9a474d4ff60b66576200356c183a20e7140ea3	Apalache	Except1Fun	Cross3	True	Passed	Model Under Test Equivalent Model
ce51e0df13b6df286c7650dcd183475edf3a2459	Apalache	Except1Fun	Cross3	False	Passed	Model Under Test Equivalent Model
46003da17d532f3a50f74af4d7fc4d6deac4df43	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))	Except1Fun	FunSet	True	Passed	Model Under Test Equivalent Model
e246a27fcef4f0182fb6b45f6dd597e35615fb85	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))	Except1Fun	FunSet	False	Passed	Model Under Test Equivalent Model
e261ff1b64e5fa65852960d51540f2a7c0e8aa3e	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)	Except1Fun	RecordSet	True	Passed	Model Under Test Equivalent Model
32c7c553bb1ca1a4915ea3df8dba4c0164c445bb	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)	Except1Fun	RecordSet	False	Passed	Model Under Test Equivalent Model
e6edc36f2c48cb205cb22a1feccfd1d002f4b848	Apalache	Except1Fun	SetDiff	True	Passed	Model Under Test Equivalent Model
e7efd49389605376a6d7b7fb712b69398ce97f9c	Apalache	Except1Fun	SetDiff	False	Passed	Model Under Test Equivalent Model
82724a8ced0eaf2e71f99f26d1cb6de0120af1a6	Apalache	Except1Fun	SetUnion	True	Passed	Model Under Test Equivalent Model
6782d9873792abce686fce27da7ff29dc48b8fa7	Apalache	Except1Fun	SetUnion	False	Passed	Model Under Test Equivalent Model
57dfd5a87e38c42efa2f3d781d12bc1af327d0b5	Apalache	Except1Fun	SetIntersect	True	Passed	Model Under Test Equivalent Model
1723fec30176402ab51a20eb6be6902b2721c1e2	Apalache	Except1Fun	SetIntersect	False	Passed	Model Under Test Equivalent Model
9d52b7eeb408ac9c77bf16585db1b30313a24199	Apalache	Except1Fun	SubsetEq	True	Passed	Model Under Test Equivalent Model
a830ed8fb7b9bf957951fe6dd4d32a6edc4ede68	Apalache	Except1Fun	SubsetEq	False	Passed	Model Under Test Equivalent Model
420e7140f82eafb47ca30b72d14f24a437c54f5e	Apalache	Except1Fun	IfCond	True	Passed	Model Under Test Equivalent Model
70e49d4d6e2c25c548ddc0bcf5b64b7a58ea5379	Apalache	Except1Fun	IfCond	False	Passed	Model Under Test Equivalent Model
3acd9e02ff3eba70b4c59df01169103ea8c9edcd	Apalache	Except1Fun	IfThen	True	Passed	Model Under Test Equivalent Model
122cba913d2e220c10c0183c8b89b5571c498b57	Apalache	Except1Fun	IfThen	False	Passed	Model Under Test Equivalent Model
52e0726f5c91ffa3f25cafe9517a769c22019449	Apalache	Except1Fun	IfElse	True	Passed	Model Under Test Equivalent Model
fbd8f713e3015969ba4fe8ed82947ffe4e986a00	Apalache	Except1Fun	IfElse	False	Passed	Model Under Test Equivalent Model
af9109c6f6b1158ed71de4adaaceb0c68b44d149	Apalache	Except1Fun	Subset	True	Passed	Model Under Test Equivalent Model
4b41dccac6e3c980523de133d251922f1a42f8d0	Apalache	Except1Fun	Subset	False	Passed	Model Under Test Equivalent Model
dea4f1e1eba34590923a18abb1c63a88d0e68ddd	Apalache	Except1Fun	Domain	True	Passed	Model Under Test Equivalent Model
f3d3a42620868a2df7bff079e217cff3985e31cd	Apalache	Except1Fun	Domain	False	Passed	Model Under Test Equivalent Model
0d660c11c2a7a8d76ff1885434541563181693a7	Apalache	Except1Fun	Union	True	Passed	Model Under Test Equivalent Model
41a036d713a2728e049e6e67932f4ffdbe6432ef	Apalache	Except1Fun	Union	False	Passed	Model Under Test Equivalent Model
2b2e80104ea3d0bdde0a8fdc512e0ca3afff8f21	Apalache	Except1Fun	Unchanged	True	Passed	Model Under Test Equivalent Model
914c76c287b410aaeccc9f044ef4dab3c15da7cd	Apalache	Except1Fun	Unchanged	False	Passed	Model Under Test Equivalent Model
e9488527d2565c20919aa817253e705e57eb69ce	Apalache	Except1Fun	Equivalence	True	Passed	Model Under Test Equivalent Model
78fc1df0f22062fd99086f72ee53dcb803aa753d	Apalache	Except1Fun	Equivalence	False	Passed	Model Under Test Equivalent Model
067cfdb163560b2f3c4da254340cc0810e801a4e	Apalache	Except1Fun	StringEmpty	True	Passed	Model Under Test Equivalent Model
8aad4bfab15ca04969bfef33221de5739145d124	Apalache	Except1Fun	StringEmpty	False	Passed	Model Under Test Equivalent Model
58cebb4190f3a1ea4e9c65da77656627e408bc6b	Apalache	Except1Fun	String	True	Passed	Model Under Test Equivalent Model
40d095cc4d050456a212ebc4b5ed9b09b4cd3301	Apalache	Except1Fun	String	False	Passed	Model Under Test Equivalent Model
9a9da1e179e443e82283c690a48d3cdf68a203c6	Apalache	Except1Fun	SeqLen	True	Passed	Model Under Test Equivalent Model
11b1de98ae6295be422d0f7cb440304af3cc0727	Apalache	Except1Fun	SeqLen	False	Passed	Model Under Test Equivalent Model
d9ed32645d2a0e603706bf1d878f456712fcadf6	Apalache	Except1Fun	SeqConcat	True	Passed	Model Under Test Equivalent Model
251af34439095ef9278a735d2405f5b0b9ea46f3	Apalache	Except1Fun	SeqConcat	False	Passed	Model Under Test Equivalent Model
f59c6b67fbc30bff8a54a5d1c9965a72c3826d6c	Apalache	Except1Fun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
d4ac9749d4ef4008fbba90ad8125e6850dcbb2ef	Apalache	Except1Fun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
4c75caf0f44633c5cf6226b4bc02daa891e8fe62	Apalache	Except1Fun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
daa1bea8f3bab7c6875a779fe55d769ee13bcfad	Apalache	Except1Fun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
acbe110769e5b88e54a747b5f3608c4e0bf06c36	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	Except1Fun	NumRange	True	Passed	Model Under Test Equivalent Model
5fa29621da36106c085f7cc492e1997587f5893f	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	Except1Fun	NumRange	False	Passed	Model Under Test Equivalent Model
f2f7cd915b704a4d8f201bc153451c8390767da4	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except1Fun	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
d98aa6f06e0f2862b0ea41d04d64f03ee201bb87	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except1Fun	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
7af9c54ec1b5f14dc0a51d4f97d0efeefc76bfaf	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]]	Except1Fun	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
14da98c9925d20e311f8084c479195864d353b2f	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]]	Except1Fun	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
d5047435e801342cd03b4f109d483214e08788dd	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except1Fun	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
7335a4cc64e20f4ce292a0cfbd7b315605cc7e4a	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except1Fun	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
1e3e1b183989384166f38fd7af2338243ec0a8e4	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except1Fun	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
8c8386e006fb12a3f97978ba94f5a18b72897559	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except1Fun	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
21ee2d6ca93aa2bc47fa8435860157ab743d6c31	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except1Fun	TlcEval	True	Passed	Model Under Test Equivalent Model
374061f8d01aea0aeb3ee1daf86dab8722559bca	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except1Fun	TlcEval	False	Passed	Model Under Test Equivalent Model
dff652ff8ace80b84d6a45e2369d9719f95ad891	Apalache	Except1Fun	BagBagToSet	True	Passed	Model Under Test Equivalent Model
5952d091047bb0b5a5a6bc0cac98bec277eaab78	Apalache	Except1Fun	BagBagToSet	False	Passed	Model Under Test Equivalent Model
9fdbc5d13569847e6d242a6764b97c88a90bdccf	Apalache	Except1Fun	BagSetToBag	True	Passed	Model Under Test Equivalent Model
8896c209d0ee68d110ffb52debe274bbccb3d4e9	Apalache	Except1Fun	BagSetToBag	False	Passed	Model Under Test Equivalent Model
dad37f3fcbf3b2f8a322f638826fd77255dfce7a	Apalache	Except1Fun	BagBagIn	True	Passed	Model Under Test Equivalent Model
cc5825bf95af876fdc7afd78d440849828f0a98b	Apalache	Except1Fun	BagBagIn	False	Passed	Model Under Test Equivalent Model
0c68065f31471a4f3a19666757adae4061c17aa2	Apalache	Except1Fun	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
387bc6b1006999598cd3c35720890b9e2e7a7880	Apalache	Except1Fun	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
69b5ae1002c0d70f81d662210ed6e7fdbe295ffc	Apalache	Except1Fun	BagAddBag	True	Passed	Model Under Test Equivalent Model
9cf64b251fda08ff33aeb404b61215ef7e12f5e7	Apalache	Except1Fun	BagAddBag	False	Passed	Model Under Test Equivalent Model
244f71bbe13aead53a9613dd1128747350bdb94d	Apalache	Except1Fun	BagBagSub	True	Passed	Model Under Test Equivalent Model
ba77803b2b68b1ad83a947ea7c26d791753c0856	Apalache	Except1Fun	BagBagSub	False	Passed	Model Under Test Equivalent Model
16bee4a98e257be6c991772adced0280e86bf8b7	Apalache	Except1Fun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
098a15eecfa858e56bb76eec74fb803ac5e0466f	Apalache	Except1Fun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
252270cfc3c2f4cf239f914df1b4e54cf1fe924c	Apalache	Except1Fun	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
1ae8fceaf4bf3c839b72d29dd3beb527b18c32cd	Apalache	Except1Fun	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
c129a0be954ddd87237db4821152941312bc5b1f	Apalache	Except1Fun	BagBagUnion	True	Passed	Model Under Test Equivalent Model
50dcb89961d61d83c68603a6104ae834341c39e8	Apalache	Except1Fun	BagBagUnion	False	Passed	Model Under Test Equivalent Model
811966a2c47c4a91a6a3dcdab620f25cdc55d1aa	Apalache	Except1Fun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
713e40f1da4960fa1db74848b47f290aa91ece84	Apalache	Except1Fun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
948388ad5bc6db8350bdf1512a7d9913fc3aab3c	Apalache	Except1Fun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
207f715b3cceb85e62ff816e9c051e48d5e3727d	Apalache	Except1Fun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
899d3a33dd37a3b6a8f26171f14c66c77031d7ca	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except1Fun	BagSubBag	True	Passed	Model Under Test Equivalent Model
0a3a986a18c845713ca2c15f952dc5ac99b99c52	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except1Fun	BagSubBag	False	Passed	Model Under Test Equivalent Model
8455c30cfbb61215354c367a590b7a3dbfe8869a	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)	Except1Fun	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
a70bbbde705a3cfe1a57ccf93d27a8bc5305db17	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)	Except1Fun	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
411fb75eac084015f4f78435b05afa6b36927219	Apalache	Except1Fun	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
d1f5e85ca8a79bef8e66a5a7cf21a3dc9acdf46d	Apalache	Except1Fun	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
314e23c84b3483297cea1e375ab766d9b8926fd5	Apalache	Except1Fun	SeqHead	True	Passed	Model Under Test Equivalent Model
0f9eec7852e047b0e473ff0c22454298d80dab9a	Apalache	Except1Fun	SeqHead	False	Passed	Model Under Test Equivalent Model
4ace3759f4b4824d03fe8fbf6af407a90a2713e3	Apalache	Except1Fun	SeqTail	True	Passed	Model Under Test Equivalent Model
49b45d467ac86e8aa2c6265a4c851d4a353f0881	Apalache	Except1Fun	SeqTail	False	Passed	Model Under Test Equivalent Model
e156cd1e7d5f8ec7a92c7bf98f1e8aa56ad7b824	Apalache	Except1Fun	SeqAppend	True	Passed	Model Under Test Equivalent Model
158404d90e72eab4f71080cd10c8bb39fab8b9e2	Apalache	Except1Fun	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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