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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
05134cbb72d18d184f14ec211429f33373016ae7	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Rec	OneLineComment	True	Passed	Model Under Test Equivalent Model
f913b854e5ae8e0df4e2ecf4db7fe5e328aafca5	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Rec	OneLineComment	False	Passed	Model Under Test Equivalent Model
1a0c76d4f78a11a081045e4894dad9c7138bdc72	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Rec	MultiLineComment	True	Passed	Model Under Test Equivalent Model
94b0d277b68b1b3973b8183ee9541c8286bcaf02	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except1Rec	MultiLineComment	False	Passed	Model Under Test Equivalent Model
781041cd2d14f0b7a9b526172d77f954612875a4	Apalache	Except1Rec	BoolTrue	True	Passed	Model Under Test Equivalent Model
c7ef981488f80064ec01249de39750cc14f34f64	Apalache	Except1Rec	BoolTrue	False	Passed	Model Under Test Equivalent Model
0bbb99bff32f0c519f117e8640791ae2c825ca3e	Apalache	Except1Rec	BoolFalse	True	Passed	Model Under Test Equivalent Model
06b896fe0c875f43def73ab54c422f6bb5afed94	Apalache	Except1Rec	BoolFalse	False	Passed	Model Under Test Equivalent Model
4cc68ea6208c5961cb6575fc3fe932bb8989492b	Apalache	Except1Rec	BoolSet	True	Passed	Model Under Test Equivalent Model
ffae13946bf371a968f56e35ce48c56ac2f4690e	Apalache	Except1Rec	BoolSet	False	Passed	Model Under Test Equivalent Model
32bb17411ffa2a39a7239fc859758d867c95e33f	Apalache	Except1Rec	And	True	Passed	Model Under Test Equivalent Model
f4af101b90c31328e6bbf22688d76b875e9fd592	Apalache	Except1Rec	And	False	Passed	Model Under Test Equivalent Model
3eae21c5b6a93f1db02257a87d2daee688c5e4bb	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except1Rec	AndMultiLine	True	Passed	Model Under Test Equivalent Model
372371b3c778b1d426fa6d566ba4c60fb2d3b838	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except1Rec	AndMultiLine	False	Passed	Model Under Test Equivalent Model
9fe9c654546c214234ff939c7c5a2f43840261d4	Apalache	Except1Rec	Imply	True	Passed	Model Under Test Equivalent Model
12aa58cae5c3f220f991736cd3877ee5ba3a6b0f	Apalache	Except1Rec	Imply	False	Passed	Model Under Test Equivalent Model
141d59aba9bdc82afd2b9ae0c731c91547115eb6	Apalache	Except1Rec	Not	True	Passed	Model Under Test Equivalent Model
758178f118a885c453c33cf35e5af0137ecb42ac	Apalache	Except1Rec	Not	False	Passed	Model Under Test Equivalent Model
b8f56178ac16749d9a68a4ab01dfaf2b56398003	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except1Rec	Or	True	Passed	Model Under Test Equivalent Model
fc8b0865a8db8938fb5f4660e19123903dbe2a9c	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except1Rec	Or	False	Passed	Model Under Test Equivalent Model
d051efd36b7845549d690e479cce300f56a0d309	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except1Rec	OrMultiLine	True	Passed	Model Under Test Equivalent Model
abc9d6cc8e8034b73a1754882afa2d3df80983bc	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except1Rec	OrMultiLine	False	Passed	Model Under Test Equivalent Model
09ddb70fb7931a9d7367997ff16fa581be2fe231	Apalache	Except1Rec	Eq	True	Passed	Model Under Test Equivalent Model
a9c12bb016884091855ede6a45d218d3e8ead95b	Apalache	Except1Rec	Eq	False	Passed	Model Under Test Equivalent Model
44f5ac7c2cd7d3a25430a86956c1e22e9f5c944d	Apalache	Except1Rec	Ne	True	Passed	Model Under Test Equivalent Model
3decdfb4b44154f2daf92672bc46009f0022dced	Apalache	Except1Rec	Ne	False	Passed	Model Under Test Equivalent Model
f4c34b524c5937e1ce6d31808e013d4399f163aa	Apalache	Except1Rec	Let	True	Passed	Model Under Test Equivalent Model
005a21fe1055b214e222e4a3794696bc3e9eaac7	Apalache	Except1Rec	Let	False	Passed	Model Under Test Equivalent Model
46e554d844ccf8a731cf78bc40eccaf20da7fba0	Apalache	Except1Rec	SetEmpty	True	Passed	Model Under Test Equivalent Model
1a24eae1b8530c3a9af8ea8261c88edd63dfe58b	Apalache	Except1Rec	SetEmpty	False	Passed	Model Under Test Equivalent Model
2b5d55448f3826280fb92d5fc49b4279d30da452	Apalache	Except1Rec	Set0	True	Passed	Model Under Test Equivalent Model
1d6eebba78f50e68da37384e790c9f62371ce336	Apalache	Except1Rec	Set0	False	Passed	Model Under Test Equivalent Model
7becc42d69fec8950342c3a6e1efb755832037ee	Apalache	Except1Rec	Set1	True	Passed	Model Under Test Equivalent Model
88961b160f6cfd571849c3524d7dd1987c8b638c	Apalache	Except1Rec	Set1	False	Passed	Model Under Test Equivalent Model
51893b3886b57eb473d4e95254727fac5acc74cc	Apalache	Except1Rec	Set2	True	Passed	Model Under Test Equivalent Model
ba96bdfa28a81b9ecbea3ab0c9a7b5091146c6c6	Apalache	Except1Rec	Set2	False	Passed	Model Under Test Equivalent Model
d0123ebad18988b0055d211babd8fcfa77ae48a5	Apalache	Except1Rec	Fun	True	Passed	Model Under Test Equivalent Model
9046f27dca006771f1eb58ad348ce82350224ab3	Apalache	Except1Rec	Fun	False	Passed	Model Under Test Equivalent Model
b92e286f4787c9d70fdd4a432b849fc4914e114c	Apalache	Except1Rec	In	True	Passed	Model Under Test Equivalent Model
6a4d36e8081d526eed8569af1782c4db3fdda5f0	Apalache	Except1Rec	In	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
1aa2b58c2c5875206d9ec2d3c51c93cd429fb26c	Apalache	Except1Rec	Exists	True	Passed	Model Under Test Equivalent Model
0f3775313e435bd7a539b1c76cadcded0a8b68c2	Apalache	Except1Rec	Exists	False	Passed	Model Under Test Equivalent Model
7d26a3d013604f931dcaf338fd63607cfe386f77	Apalache	Except1Rec	Forall	True	Passed	Model Under Test Equivalent Model
bce381f587fa89742c21e4898f849aeaa54b0e2f	Apalache	Except1Rec	Forall	False	Passed	Model Under Test Equivalent Model
71184a169377a3c4387ce0cdca217bd61b4a6f46	Apalache	Except1Rec	Choose	True	Passed	Model Under Test Equivalent Model
a80334906912a0b71786e30f3172dbb4667aa782	Apalache	Except1Rec	Choose	False	Passed	Model Under Test Equivalent Model
f565cf2e12d1534a6d0da545d5d512fe20e20a69	Apalache	Except1Rec	Record	True	Passed	Model Under Test Equivalent Model
26e10a2e3ef91719ca01962733047de1b7b20eee	Apalache	Except1Rec	Record	False	Passed	Model Under Test Equivalent Model
782f35e7eeb48ebcf8e1b1bda9ff1e3c6f1597ac	Apalache	Except1Rec	Tuple	True	Passed	Model Under Test Equivalent Model
6a86ca45422cda66cf50c0cfadf4d788de5cd126	Apalache	Except1Rec	Tuple	False	Passed	Model Under Test Equivalent Model
923f322eb292dbe2463c2f6d4092865171621cc7	Apalache	Except1Rec	TupleEmpty	True	Passed	Model Under Test Equivalent Model
67bc1c9b696bbacbe53d04b8f45123d770aa1fbd	Apalache	Except1Rec	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4a04820fa02a60cedf65f02c0f68c597ec1e2b20	Apalache	Except1Rec	FunApp	True	Passed	Model Under Test Equivalent Model
81617e59678ac0ef84d67598c22dc5dcfd73cb0a	Apalache	Except1Rec	FunApp	False	Passed	Model Under Test Equivalent Model
64143ff95512cae9349337eb6c3de45f40506fa7	Apalache	Except1Rec	Prime	True	Passed	Model Under Test Equivalent Model
a9857992f3475995821b8defc7b17d9dc259189b	Apalache	Except1Rec	Prime	False	Passed	Model Under Test Equivalent Model
954c6ed9d0f278d2cf126f6967329e43c71bf6a7	Apalache	Except1Rec	NumZero	True	Passed	Model Under Test Equivalent Model
01f1969d8be22af9dcf614b8a23cc96b99a320c2	Apalache	Except1Rec	NumZero	False	Passed	Model Under Test Equivalent Model
38983cfcf317f89eb60436b364f9195bbcba3b41	Apalache	Except1Rec	NumOne	True	Passed	Model Under Test Equivalent Model
9ef8223f9d74a6915ad06f57c71fa074d8c0ffc5	Apalache	Except1Rec	NumOne	False	Passed	Model Under Test Equivalent Model
718910f223d682e9c90cd591cc14dc709f44077a	Apalache	Except1Rec	NumMaxInt	True	Passed	Model Under Test Equivalent Model
67950a08ad632560c22d6c88ed44783e6b1b1b98	Apalache	Except1Rec	NumMaxInt	False	Passed	Model Under Test Equivalent Model
e22f5b8cc136a251a5021a62b2dd8e9bd985fda5	Apalache	Except1Rec	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
006388eb5ee4a1b5dc20623a9fa5374e137f871f	Apalache	Except1Rec	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
7e3c5fa9f422eb02f94c1329f4ee40a382253c91	Apalache	Except1Rec	NumPlus	True	Passed	Model Under Test Equivalent Model
6f876d2acc2239a23e98e747feb86a986975674c	Apalache	Except1Rec	NumPlus	False	Passed	Model Under Test Equivalent Model
a24724c83bfa85a3a7d1845cc26237c352e592c4	Apalache	Except1Rec	NumMinus	True	Passed	Model Under Test Equivalent Model
729fc29d4cb467c6cdeba40177d02330ceb629fb	Apalache	Except1Rec	NumMinus	False	Passed	Model Under Test Equivalent Model
0db12a11fca2eb2b366d7b0942a50a3f670fb5fa	Apalache	Except1Rec	NumMul	True	Passed	Model Under Test Equivalent Model
15d595d14584d6d5c40e0fa70453a9a9bb4a526a	Apalache	Except1Rec	NumMul	False	Passed	Model Under Test Equivalent Model
4b4c70be5690844be43a5ea8ff729ce91427159a	Apalache	Except1Rec	NumDiv	True	Passed	Model Under Test Equivalent Model
0c7c5aabc1025dfe567d73e89102315bb0f830db	Apalache	Except1Rec	NumDiv	False	Passed	Model Under Test Equivalent Model
06e78fe7da78f9a2a74d845b9b18c564922c8d3b	Apalache	Except1Rec	NumMod	True	Passed	Model Under Test Equivalent Model
784af1d79308b2226fdf89eb5ca6c29c7e8095ba	Apalache	Except1Rec	NumMod	False	Passed	Model Under Test Equivalent Model
03df9fad4bbdd53c32c0fe765e2422dbb6a623be	Apalache	Except1Rec	NumPow	True	Passed	Model Under Test Equivalent Model
754dfeb57724e5e1261ae47158d3d589531682bc	Apalache	Except1Rec	NumPow	False	Passed	Model Under Test Equivalent Model
74fcc675b01469993224b37170c972a67cdab7a8	Apalache	Except1Rec	NumGt	True	Passed	Model Under Test Equivalent Model
f27c285a39c2999e7bc5d27753885bbb67b9d080	Apalache	Except1Rec	NumGt	False	Passed	Model Under Test Equivalent Model
f66138abac0ec73e13f75beb2c4d25e2e116c61d	Apalache	Except1Rec	NumGe	True	Passed	Model Under Test Equivalent Model
0ea9cf552df9dd87d6544028337bc24de8bc88cc	Apalache	Except1Rec	NumGe	False	Passed	Model Under Test Equivalent Model
998e33ae50a792339e9476539b73c356d5d72cca	Apalache	Except1Rec	NumLt	True	Passed	Model Under Test Equivalent Model
a43b7bd6f818db366b58e6aed36ee1a3f44b00a3	Apalache	Except1Rec	NumLt	False	Passed	Model Under Test Equivalent Model
295a36a343911a31636b65d7f253284a820bac98	Apalache	Except1Rec	NumLe	True	Passed	Model Under Test Equivalent Model
78f5afdbe72482f43651386f587026ae050565d3	Apalache	Except1Rec	NumLe	False	Passed	Model Under Test Equivalent Model
4fb85e0fe456e1c23fd933f53e089d6e261fe1a9	Apalache	Except1Rec	DefFun	True	Passed	Model Under Test Equivalent Model
69b84655c0fb72545ab4db5f8f9b0c5bb8949e7e	Apalache	Except1Rec	DefFun	False	Passed	Model Under Test Equivalent Model
d0d687a1988dc374cb0b90f5b00e9ec09349383a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDefFun	True	Passed	Model Under Test Equivalent Model
9f7b5e98bf9f2fb18d9e4fc750187cd7bfc4a93c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDefFun	False	Passed	Model Under Test Equivalent Model
23bb2eaad08c4fd8f87fa308ed10fc70a43879c2	Apalache	Except1Rec	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
609f5bf93810fe40d25b1fbcf0f8982520027e93	Apalache	Except1Rec	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
8542d89371924d1f6b9bfbc3ad2f40a6e2bec5b9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
031bab3a4e26cdad640f199ef556214e532e622b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
b4e1cdb9e1fb5f3d66bea0f499455ab32d1cf741	Apalache	Except1Rec	Def0	True	Passed	Model Under Test Equivalent Model
e680e45a7bae9cdc75e9b7c00d0f1cda0bc4401d	Apalache	Except1Rec	Def0	False	Passed	Model Under Test Equivalent Model
0b27128f5f24fb1b625f3a4de9cbe8c6547b476c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef0	True	Passed	Model Under Test Equivalent Model
ab462e3df338d622b709e671645b4985e2b19019	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef0	False	Passed	Model Under Test Equivalent Model
0dc7f34aeb2132e7afd2f0a0472fc8f8e95a7d52	Apalache	Except1Rec	Def1	True	Passed	Model Under Test Equivalent Model
2092a052f4f30eeeb4ce5b3fc2eb60e33d9739dd	Apalache	Except1Rec	Def1	False	Passed	Model Under Test Equivalent Model
d38998780fe932cbf655427c41dfdd9aff21435c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1	True	Passed	Model Under Test Equivalent Model
3d0c4d9b6b80a14b1401d03cd4ea41d2e8a7aa74	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1	False	Passed	Model Under Test Equivalent Model
8d9c3779c6cf47582ce60b36a4f99388cfb8d789	Apalache	Except1Rec	Def2	True	Passed	Model Under Test Equivalent Model
75410612e8b7b909b9cc0ea41e2711521006dd29	Apalache	Except1Rec	Def2	False	Passed	Model Under Test Equivalent Model
5ce587ce48856f88826a831548ab56f3885008ac	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef2	True	Passed	Model Under Test Equivalent Model
a7f127ee8a11ebcf219a2982732795297409a777	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef2	False	Passed	Model Under Test Equivalent Model
4fe2c10696550d126e22f8f4d940e06215fe4638	Apalache	Except1Rec	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b8d4aa8802eceec85fd8cce115e8aceacdefe5ca	Apalache	Except1Rec	Def1Recursive	False	Passed	Model Under Test Equivalent Model
030ad5162c5c64a8eb1197c4a537c65eabe4b5ff	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
b43529bd95805eed3e891e9eb7043d208fe9ee36	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
e9a928c548ff31d8ca46e5cd351fdc835a5a303e	Apalache	Except1Rec	Extends	True	Passed	Model Under Test Equivalent Model
d5bd14947e96ba0ce153bd20e80042e3b26066de	Apalache	Except1Rec	Extends	False	Passed	Model Under Test Equivalent Model
05c4dbd74b64ff1832dc3fb258b60745d66a187f	Apalache	Except1Rec	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
95ac3881cba6867a6d18f84dfe97b2692169bda0	Apalache	Except1Rec	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
528ca3e98cdcd17036d19e3e2910908a754bed5a	Apalache	Except1Rec	Variable	True	Passed	Model Under Test Equivalent Model
2cc74eb605b3e778c6a7c3898d23f30cd02ab692	Apalache	Except1Rec	Variable	False	Passed	Model Under Test Equivalent Model
19c96ae118d9dfdffc49cf24afbbff1a96d9f4e7	Apalache	Except1Rec	Constant	True	Passed	Model Under Test Equivalent Model
da78073e6c96b61705887df26e5559e42c3814ed	Apalache	Except1Rec	Constant	False	Passed	Model Under Test Equivalent Model
589112f4a0317a41a1023a936d9c38077fd1d707	Apalache	Except1Rec	ConstantRank1	True	Passed	Model Under Test Equivalent Model
549d41ac6eb7ca954d5884e6c00fdd7c624693f6	Apalache	Except1Rec	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f40c9f6a4b2fcafa609f96b67dc63841cdbc86f4	Apalache	Except1Rec	Instance	True	Passed	Model Under Test Equivalent Model
55b453c9f6eee0d7880e39a77fca51fcb6a20930	Apalache	Except1Rec	Instance	False	Passed	Model Under Test Equivalent Model
7c4fb7a7ec0e700f8d4d1297f414f5dbc82179ce	Apalache	Except1Rec	InstanceWith	True	Passed	Model Under Test Equivalent Model
1be279e008a26dceb104aca5a98ec8e42330a994	Apalache	Except1Rec	InstanceWith	False	Passed	Model Under Test Equivalent Model
6b49eda84b4f808368941e770fb4da801bc92628	Apalache	Except1Rec	InstanceNamed	True	Passed	Model Under Test Equivalent Model
24d6c3cf38e17e99a23a8a13e82a158496abcb99	Apalache	Except1Rec	InstanceNamed	False	Passed	Model Under Test Equivalent Model
05b29b170dc36e96b3cc6178bc2dce9d26b63ef5	Apalache	Except1Rec	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b89be97e1820fd139ffa2f8ca15f0b1812ad6c9d	Apalache	Except1Rec	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
fce049c32e2d5596c214477bf2daf777ed7487f1	Apalache	Except1Rec	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
159a73370d132f9c341149abb1ca504644aca161	Apalache	Except1Rec	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
f7caff23f7453843e6f0eb0ca35cbd06d232bf61	Apalache	Except1Rec	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
6b0d6e228bdb590460d54fd5519e21c8aeb3c194	Apalache	Except1Rec	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
e22d6263c3ccf3ef41f46e32e91a13835ffcb5e8	Apalache	Except1Rec	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
73e1bf9d040d847b2bb0c1e63050ff1fa870457a	Apalache	Except1Rec	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
c539548b1671d3b9bc12c8d0c3592629f2ec4413	Apalache	Except1Rec	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
ed2f00374d7ab38fcc4b629e73ed2c2fd5977e7b	Apalache	Except1Rec	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
930513d8c910be2e5fbf8117465c829de69719d0	Apalache	Except1Rec	Enabled	True	Passed	Model Under Test Equivalent Model
68fe3374645a5e3e781b661cd33fa838a0685387	Apalache	Except1Rec	Enabled	False	Passed	Model Under Test Equivalent Model
17efcc310847df67b39434410eed44001a6e3cfb	Apalache	Except1Rec	Cross2	True	Passed	Model Under Test Equivalent Model
fe22b0c9498448282795e71b1647e57fb8d70a2f	Apalache	Except1Rec	Cross2	False	Passed	Model Under Test Equivalent Model
b666b3b12d74977bcf647bfa16df8989baee53bd	Apalache	Except1Rec	Cross3	True	Passed	Model Under Test Equivalent Model
3be9169c1b8c6e5946472cbae10ff2f0dec68c96	Apalache	Except1Rec	Cross3	False	Passed	Model Under Test Equivalent Model
a95c2994cae465ed429e0390568defbdc000e57b	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))	Except1Rec	FunSet	True	Passed	Model Under Test Equivalent Model
a6d8b11d46044a79847556c8f66978d5b4288ebe	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))	Except1Rec	FunSet	False	Passed	Model Under Test Equivalent Model
27fa2994eb356a8c28cf5944f279b0ef3c117489	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)	Except1Rec	RecordSet	True	Passed	Model Under Test Equivalent Model
e3f1fdeb6b073fcd29eec0c6a0f669e43b143b9e	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)	Except1Rec	RecordSet	False	Passed	Model Under Test Equivalent Model
667a3c4e5430ce6a71c08baa328b4ab3952018da	Apalache	Except1Rec	SetDiff	True	Passed	Model Under Test Equivalent Model
2f718bd63b503e1a32802b8fc38cd00ab207bb5d	Apalache	Except1Rec	SetDiff	False	Passed	Model Under Test Equivalent Model
da92380fec7cc8855b787fba53e3dcf76fc0bd44	Apalache	Except1Rec	SetUnion	True	Passed	Model Under Test Equivalent Model
cdeeff3cc473e1b1d62314a699649146ca794715	Apalache	Except1Rec	SetUnion	False	Passed	Model Under Test Equivalent Model
e39c1275a6bc5952facda2d2b04639cf548b5d4b	Apalache	Except1Rec	SetIntersect	True	Passed	Model Under Test Equivalent Model
ab1e61bbc89f4bb156799437c4e274b8683a8291	Apalache	Except1Rec	SetIntersect	False	Passed	Model Under Test Equivalent Model
61ebd580b8c840279b696e63f3c4eeffc03849f4	Apalache	Except1Rec	SubsetEq	True	Passed	Model Under Test Equivalent Model
da403a25e38ee00a8db839ec66fbc9784b7852ac	Apalache	Except1Rec	SubsetEq	False	Passed	Model Under Test Equivalent Model
3d5be81a7c1ab416e2b32c90adcbe4665f66a060	Apalache	Except1Rec	IfCond	True	Passed	Model Under Test Equivalent Model
3aecdb7a799e93758d8b6cef8096f78d68c1a613	Apalache	Except1Rec	IfCond	False	Passed	Model Under Test Equivalent Model
227262dfbdd8f7d0bcd89b57f3b24db40c07eb90	Apalache	Except1Rec	IfThen	True	Passed	Model Under Test Equivalent Model
72657d90d3a4f9ae6291424bc33fc9752406ddd6	Apalache	Except1Rec	IfThen	False	Passed	Model Under Test Equivalent Model
7c6e80395fa57a594aeb520ddfbaa922dd729779	Apalache	Except1Rec	IfElse	True	Passed	Model Under Test Equivalent Model
73bf8411a043864de1eb6dc2509d0a20189af56a	Apalache	Except1Rec	IfElse	False	Passed	Model Under Test Equivalent Model
8453926e4f75b347c677a4dc2fb38a85bfbd0c0a	Apalache	Except1Rec	Subset	True	Passed	Model Under Test Equivalent Model
1b9e154fc3c423adf38cdcb2c16d60750fab1ea0	Apalache	Except1Rec	Subset	False	Passed	Model Under Test Equivalent Model
9647165a7a7b6e700909c7c082384412874a3985	Apalache	Except1Rec	Domain	True	Passed	Model Under Test Equivalent Model
b5bf6dc7bd9eb66abd73b80cc0c970b372dd067a	Apalache	Except1Rec	Domain	False	Passed	Model Under Test Equivalent Model
943836eeb012dd464b57d2f5fd8e91ca3b51615a	Apalache	Except1Rec	Union	True	Passed	Model Under Test Equivalent Model
ab7c6f6e7a8b5df0a5e2121da0559b16342cc2fd	Apalache	Except1Rec	Union	False	Passed	Model Under Test Equivalent Model
4fd81201b48fb61c800f3720b08dd761e08f0a32	Apalache	Except1Rec	Unchanged	True	Passed	Model Under Test Equivalent Model
c67a7760db8a5c2dc2d51e43b57b95d323d9f3fa	Apalache	Except1Rec	Unchanged	False	Passed	Model Under Test Equivalent Model
f89097d284804118ba5e8dbe6606c20df59c4472	Apalache	Except1Rec	Equivalence	True	Passed	Model Under Test Equivalent Model
9e8625ab105098fe676fbf22723c3851823a2005	Apalache	Except1Rec	Equivalence	False	Passed	Model Under Test Equivalent Model
8763d89ae66c4bd6c54b97b51b2f1dc7276e4d62	Apalache	Except1Rec	StringEmpty	True	Passed	Model Under Test Equivalent Model
469275ac2afababc13ad31cb7c42c267a6a18962	Apalache	Except1Rec	StringEmpty	False	Passed	Model Under Test Equivalent Model
58790d249a10416a52ab1e4a25fcc609ef611998	Apalache	Except1Rec	String	True	Passed	Model Under Test Equivalent Model
1a3860808fc6b04924aea500c86c296c3a81c219	Apalache	Except1Rec	String	False	Passed	Model Under Test Equivalent Model
ca64ac782b474625606d0c415d52766cf6dc94cb	Apalache	Except1Rec	SeqLen	True	Passed	Model Under Test Equivalent Model
f7f373ec2e27408af75e9f80ade2aaf616bbf255	Apalache	Except1Rec	SeqLen	False	Passed	Model Under Test Equivalent Model
01274723f9f1b8ee9a741ca97dc0791101162d9a	Apalache	Except1Rec	SeqConcat	True	Passed	Model Under Test Equivalent Model
ae6ce36e3ca7915f525f89796d9e480ab392319c	Apalache	Except1Rec	SeqConcat	False	Passed	Model Under Test Equivalent Model
8a81e1fc5b26452ccc72f66e5e06e45ea636bff6	Apalache	Except1Rec	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
d9a284c3fc9468a8a85a94b55c94d49b486c9602	Apalache	Except1Rec	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
e02e385a00d3766d52b5a9165e136dad8f8ac79e	Apalache	Except1Rec	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
0cd39fd2a5a652e6f57b83f6ad543ee2bd260ebd	Apalache	Except1Rec	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
3507c1a05d1782fa8c60a727c6dac8abc1ffacaa	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	Except1Rec	NumRange	True	Passed	Model Under Test Equivalent Model
4c0079944e48b84be1e0846f605050ee32a82dc3	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	Except1Rec	NumRange	False	Passed	Model Under Test Equivalent Model
ae745d2625e19588003bb490a4229e56bab2215d	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except1Rec	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
c1ac8a485beb259c332b222d34a9a5dd3502256d	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except1Rec	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
6a777ac0686cfd32a7c7b043f6779c3807a1ff3b	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]]	Except1Rec	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
0c14d3e1a96bfc78d95f594204a6ecd36844e001	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]]	Except1Rec	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
3544fef96c0cb34887d2cab1e4c6a127ddc9a65d	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except1Rec	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
cc3e9f14c5a90f6a12dc15cbd75e7d137ee1caed	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except1Rec	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
bde9aab0ff1fcac0160f3194fb6989bbfc97fa9c	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except1Rec	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
b1cf9ea8305c37eec4f338582243e6c3e2fc0da2	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except1Rec	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
2ce94a41fcf02b86c7b160f52b81666f1f47d174	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except1Rec	TlcEval	True	Passed	Model Under Test Equivalent Model
8cf3d0fd117d05f51c6364c71d0244089c0fd009	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except1Rec	TlcEval	False	Passed	Model Under Test Equivalent Model
3b1a80fcbe696045116b6afb75b2cbc42124853f	Apalache	Except1Rec	BagBagToSet	True	Passed	Model Under Test Equivalent Model
7415a2d03763346c90418f2313bbab00d1ed47b9	Apalache	Except1Rec	BagBagToSet	False	Passed	Model Under Test Equivalent Model
786a589f3c938993cf9aa8e4d74290f1e7e5dd76	Apalache	Except1Rec	BagSetToBag	True	Passed	Model Under Test Equivalent Model
32e1df63fa4b8088dc26310e58d4bf693c7c1a05	Apalache	Except1Rec	BagSetToBag	False	Passed	Model Under Test Equivalent Model
73ffcdab5ec19cd2b685a7d48c7b25f3ae6c0af2	Apalache	Except1Rec	BagBagIn	True	Passed	Model Under Test Equivalent Model
d88ff9e00628837f07e6ffb30577e4a76b5ec4fa	Apalache	Except1Rec	BagBagIn	False	Passed	Model Under Test Equivalent Model
1b97a868fbcf31b78b46e87feb315977d1d8ee57	Apalache	Except1Rec	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
c9c13a2f248b97eeac7df7945ae83a4431a24692	Apalache	Except1Rec	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
a06a5e4f8acace964e89b0cf273098d17a26ec28	Apalache	Except1Rec	BagAddBag	True	Passed	Model Under Test Equivalent Model
6c561403cb560803a5b0c48c4e0588cdf73f2fe2	Apalache	Except1Rec	BagAddBag	False	Passed	Model Under Test Equivalent Model
1e46f2fd9b6c4b2da5d5a4a6c92fc591de19dd71	Apalache	Except1Rec	BagBagSub	True	Passed	Model Under Test Equivalent Model
e4c310f7ea31752fe0be78ca4a363a6bc7af258f	Apalache	Except1Rec	BagBagSub	False	Passed	Model Under Test Equivalent Model
094a395228a36d3a8f1ea03e4851227a2f49592a	Apalache	Except1Rec	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
01316e662e7e805167811bfd8e52857a47d93e71	Apalache	Except1Rec	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
42e330a06c9e3328fa90b617a6246c18af95c8fe	Apalache	Except1Rec	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
4508f82bf1352616016255eddea77a31067fd309	Apalache	Except1Rec	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
2e25a6e5af6f6cfb9b41d6363c0dd5c1fb4e40ae	Apalache	Except1Rec	BagBagUnion	True	Passed	Model Under Test Equivalent Model
d4328d17e337bce6b5b02b96d7b1d9e3af103c18	Apalache	Except1Rec	BagBagUnion	False	Passed	Model Under Test Equivalent Model
ad3c745b6b00fb585ff3360c8a52400d7adbf705	Apalache	Except1Rec	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
f4981e4a7614412ca9e44187ba5b9d4f0a9c36f0	Apalache	Except1Rec	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
66192dce7d6aba1746fde3eaef2d8cb1f9f5dbff	Apalache	Except1Rec	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
d085908bd3ce869ebd95dc62fe6350a843c01649	Apalache	Except1Rec	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
9a954aa94550491671b877afd0583a5974087b32	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except1Rec	BagSubBag	True	Passed	Model Under Test Equivalent Model
63977fcb0ac64a632be7ea6075841ecc2004aa4a	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except1Rec	BagSubBag	False	Passed	Model Under Test Equivalent Model
1e9e0f36f4758c73730187aec3fc49ad6fffe5e1	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)	Except1Rec	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
201fc3c689314fcbf6e7d8fbf9914ded1b9b1451	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)	Except1Rec	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
676ad343961d9efbdbc48f8032b3ccae513e10ad	Apalache	Except1Rec	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
251f7688a9afc971b0e6a5ac539e5f440d433fdb	Apalache	Except1Rec	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
9bdbef6d2c332a1baef9eb4dc541b17e707102c4	Apalache	Except1Rec	SeqHead	True	Passed	Model Under Test Equivalent Model
4fa1643ce601beae2b014a0ba26d0541590a8324	Apalache	Except1Rec	SeqHead	False	Passed	Model Under Test Equivalent Model
26b3544024670e7f9aea20ecb35da31a75a13cdf	Apalache	Except1Rec	SeqTail	True	Passed	Model Under Test Equivalent Model
3c0cbc40202614c54d6d94c9d736cbfa4b2f8828	Apalache	Except1Rec	SeqTail	False	Passed	Model Under Test Equivalent Model
dc7af58ce8853374e2e76c7ce3fe5eb048349782	Apalache	Except1Rec	SeqAppend	True	Passed	Model Under Test Equivalent Model
b4095a93786bd8fde7ef8dab5e3118058eeed29b	Apalache	Except1Rec	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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