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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
1ffb78d3b4e2cb96c3b4e8ffaf9080bc141a1d3c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except2Fun	OneLineComment	True	Passed	Model Under Test Equivalent Model
536b633cc942f54746dce367b025635e53d65be9	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except2Fun	OneLineComment	False	Passed	Model Under Test Equivalent Model
bda974e53a5ffc152870ef5683b65b9b07f15cf8	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except2Fun	MultiLineComment	True	Passed	Model Under Test Equivalent Model
2930943ee7605e477a06de32c0669d7c4332eb7c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Except2Fun	MultiLineComment	False	Passed	Model Under Test Equivalent Model
f23f84687bbb98ac0fa680c58520c6ebcb2af63f	Apalache	Except2Fun	BoolTrue	True	Passed	Model Under Test Equivalent Model
bad899983cb54a0e740c5447f21b6528949602c2	Apalache	Except2Fun	BoolTrue	False	Passed	Model Under Test Equivalent Model
ac8a25242a2b2a19fdcc769aaeb7f056f4fefe3b	Apalache	Except2Fun	BoolFalse	True	Passed	Model Under Test Equivalent Model
bca68203bf3dfb077e68ce29b4ba875dbf2c994d	Apalache	Except2Fun	BoolFalse	False	Passed	Model Under Test Equivalent Model
54c311e0b468e524727cad058f7a2e433e58dcdf	Apalache	Except2Fun	BoolSet	True	Passed	Model Under Test Equivalent Model
e52a83e7f357cad5c9fc23107a5b30178fa67e87	Apalache	Except2Fun	BoolSet	False	Passed	Model Under Test Equivalent Model
5c3e045cde5492750a5a4461c83e2f79919ff9d9	Apalache	Except2Fun	And	True	Passed	Model Under Test Equivalent Model
c3f539a6598d9bbe63c92237372958b5a6ba2d97	Apalache	Except2Fun	And	False	Passed	Model Under Test Equivalent Model
be6bc03f5ec034469a2c4c2fd9cb5ef5a88a076a	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except2Fun	AndMultiLine	True	Passed	Model Under Test Equivalent Model
3770235c36f017cd02c54222e25400046c3be08c	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Except2Fun	AndMultiLine	False	Passed	Model Under Test Equivalent Model
5746e5f8bec59a11b46f1001d0316d745c80c798	Apalache	Except2Fun	Imply	True	Passed	Model Under Test Equivalent Model
397ab9bd406371023214b3cf6a5323672463b97d	Apalache	Except2Fun	Imply	False	Passed	Model Under Test Equivalent Model
d15ba9c7f0130f3bcdb322ec6f3ed173213393e3	Apalache	Except2Fun	Not	True	Passed	Model Under Test Equivalent Model
8214e1e03135f71d993eaf1f9f96e1b91c62dfda	Apalache	Except2Fun	Not	False	Passed	Model Under Test Equivalent Model
b27782010d41a938e0a9f92b501f348a80c84bda	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except2Fun	Or	True	Passed	Model Under Test Equivalent Model
b62906cb308d7afa36fd96e452a1d5c8e92c9a8e	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Except2Fun	Or	False	Passed	Model Under Test Equivalent Model
8c628ff8d1331476f4e3c4a0c727812b67fd47e1	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except2Fun	OrMultiLine	True	Passed	Model Under Test Equivalent Model
85283e2fc7e1ae4ce2505c144a6639fc7b035078	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Except2Fun	OrMultiLine	False	Passed	Model Under Test Equivalent Model
522aba5c2696f8c0e11baf939ca4043e40fba420	Apalache	Except2Fun	Eq	True	Passed	Model Under Test Equivalent Model
842d6241903f0001a12527ab340b2e07dccc395e	Apalache	Except2Fun	Eq	False	Passed	Model Under Test Equivalent Model
bbf46aaf0772f67a75bbc192d0021ca77aebf9a3	Apalache	Except2Fun	Ne	True	Passed	Model Under Test Equivalent Model
78c1667453613671657e348add7286c1d281c5d0	Apalache	Except2Fun	Ne	False	Passed	Model Under Test Equivalent Model
84a11bfe508d3c2ca7c51e27a2b9c35e06f2538e	Apalache	Except2Fun	Let	True	Passed	Model Under Test Equivalent Model
65a8d83958a6d3571b44ef57bd99ef9ddee9e770	Apalache	Except2Fun	Let	False	Passed	Model Under Test Equivalent Model
8ce56bedb8e684866b039a93426f4cde37f567df	Apalache	Except2Fun	SetEmpty	True	Passed	Model Under Test Equivalent Model
7ebea55c5d2813dfd7887b8c6272e2bf44db2bdf	Apalache	Except2Fun	SetEmpty	False	Passed	Model Under Test Equivalent Model
c77bbdec6d25a53364d1009ec91509c0bbad86b5	Apalache	Except2Fun	Set0	True	Passed	Model Under Test Equivalent Model
e5ca6213871e4d37bea4a9f51d18b628cb5fc876	Apalache	Except2Fun	Set0	False	Passed	Model Under Test Equivalent Model
f19c8fd31c886c9c548abf7d3fec541a63c18e66	Apalache	Except2Fun	Set1	True	Passed	Model Under Test Equivalent Model
8525be60e9217ca22fda9d5cf6c6459f47dab337	Apalache	Except2Fun	Set1	False	Passed	Model Under Test Equivalent Model
42c5d06a9a22523df67423c4760c1e454d189c4e	Apalache	Except2Fun	Set2	True	Passed	Model Under Test Equivalent Model
715c5b9c3ea80f11a4ce094ceb2a275cc639ef80	Apalache	Except2Fun	Set2	False	Passed	Model Under Test Equivalent Model
96c2043aef17277ee4f03115d0f2952511e9a8f8	Apalache	Except2Fun	Fun	True	Passed	Model Under Test Equivalent Model
117db562640098399b193cb22c9f5078bdcc238b	Apalache	Except2Fun	Fun	False	Passed	Model Under Test Equivalent Model
76b839f27367c1ce788174b0197f77fde6fb5a8d	Apalache	Except2Fun	In	True	Passed	Model Under Test Equivalent Model
11e423f23d2aeb001b24ac7fe72055065e985599	Apalache	Except2Fun	In	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
25b6e4b0860943d216a5ea53acdce3291968821b	Apalache	Except2Fun	Exists	True	Passed	Model Under Test Equivalent Model
2492aaf31955c9a42fd4e14e562c35c673a08901	Apalache	Except2Fun	Exists	False	Passed	Model Under Test Equivalent Model
4ef63918a3beb56eb8d2244e354194993aa48a6f	Apalache	Except2Fun	Forall	True	Passed	Model Under Test Equivalent Model
bf414449c2da4816a2341142e566812fb14848c9	Apalache	Except2Fun	Forall	False	Passed	Model Under Test Equivalent Model
11bcced61cf57d867e29763053532039034a186a	Apalache	Except2Fun	Choose	True	Passed	Model Under Test Equivalent Model
7282ee295c62424a2d36d244e7d7b183b97b8de8	Apalache	Except2Fun	Choose	False	Passed	Model Under Test Equivalent Model
dc0664a2c2ac0ba604234f61f2e729597873a070	Apalache	Except2Fun	Record	True	Passed	Model Under Test Equivalent Model
4d952bfd6c1b8b36250dffd1e3f6505a4cf3b1c4	Apalache	Except2Fun	Record	False	Passed	Model Under Test Equivalent Model
b713e9a82ea36c35a31f1c6e7efbe37a593e04cd	Apalache	Except2Fun	Tuple	True	Passed	Model Under Test Equivalent Model
60842e429ecc137e9ba5e11ab1b6b606b7c02e88	Apalache	Except2Fun	Tuple	False	Passed	Model Under Test Equivalent Model
448986f8c3af71d94441b2eb16632370d9df7dde	Apalache	Except2Fun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
0a81e6a66a869be46fdad839df19f379c9316c32	Apalache	Except2Fun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
ef1c7ef93bc7d143e99ba4d007e3ef42333cf0a0	Apalache	Except2Fun	FunApp	True	Passed	Model Under Test Equivalent Model
5769f6de4ee36e32098e7ec0f0367a1a8dd09f93	Apalache	Except2Fun	FunApp	False	Passed	Model Under Test Equivalent Model
0b5baef17c1c54d6fdd454a0ef765664d714699b	Apalache	Except2Fun	Prime	True	Passed	Model Under Test Equivalent Model
2a486c2ba07b019026d0bcc24e1a870dab617dfd	Apalache	Except2Fun	Prime	False	Passed	Model Under Test Equivalent Model
fcbb5c2935e8f28d93aece697c190f47ae88f109	Apalache	Except2Fun	NumZero	True	Passed	Model Under Test Equivalent Model
b26e777ee832fb45d139659764d4d39125212989	Apalache	Except2Fun	NumZero	False	Passed	Model Under Test Equivalent Model
9302dff320c4a7b95123a9fe1266b5b2db68c8e8	Apalache	Except2Fun	NumOne	True	Passed	Model Under Test Equivalent Model
bf107314bcff05090bc3acd6d608d62e8bbdbb25	Apalache	Except2Fun	NumOne	False	Passed	Model Under Test Equivalent Model
fde425ba57d933fbe464ed4614e4eae0611e487f	Apalache	Except2Fun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
fb9eceb5b5d4607772ecb8de65f9c93e2b468c61	Apalache	Except2Fun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
a05e047ea50a14100ea732d5aed64aa96243655a	Apalache	Except2Fun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
8f6e01c7b76a97c5dd5ce879003faed45b062ef5	Apalache	Except2Fun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
810efe13e8895804a9403b62c215c66dcc95951f	Apalache	Except2Fun	NumPlus	True	Passed	Model Under Test Equivalent Model
d4c28b1e76eb4f0e5bbe816c90deb0d852f9171b	Apalache	Except2Fun	NumPlus	False	Passed	Model Under Test Equivalent Model
a346609af44e95d044e6cf3c4a57195218f07dcb	Apalache	Except2Fun	NumMinus	True	Passed	Model Under Test Equivalent Model
0ddbbba13e9bfc69a8b582222d46057df6df4608	Apalache	Except2Fun	NumMinus	False	Passed	Model Under Test Equivalent Model
f75b74b6174c1af757f45c78590dd5dd3a5d6442	Apalache	Except2Fun	NumMul	True	Passed	Model Under Test Equivalent Model
e6b879b2051fff98ca999a77a8e3920485e85ad9	Apalache	Except2Fun	NumMul	False	Passed	Model Under Test Equivalent Model
739f8cbd4896c9db379bce6a5251a9fb717756e0	Apalache	Except2Fun	NumDiv	True	Passed	Model Under Test Equivalent Model
cc14397e86d4378f0f170c7c8a36687af1a6c07b	Apalache	Except2Fun	NumDiv	False	Passed	Model Under Test Equivalent Model
3f6f705395b9b7c9c8da4c3796d869fabec70d21	Apalache	Except2Fun	NumMod	True	Passed	Model Under Test Equivalent Model
021bc6f26c169d63d432cd774d1c34f985f9d5cc	Apalache	Except2Fun	NumMod	False	Passed	Model Under Test Equivalent Model
ba48179e669cfbc21144dc9666a8cd8f60e1e940	Apalache	Except2Fun	NumPow	True	Passed	Model Under Test Equivalent Model
8ae1d2aff03ecb2ee593bb90c39d8be266be0507	Apalache	Except2Fun	NumPow	False	Passed	Model Under Test Equivalent Model
909f82b594d6ae1e57406e69773b028eb2d72abf	Apalache	Except2Fun	NumGt	True	Passed	Model Under Test Equivalent Model
df3ff5b6232b52ba46520fb102a25419995f6f13	Apalache	Except2Fun	NumGt	False	Passed	Model Under Test Equivalent Model
7a1ed246b0cf10d041550a31791b9c24befeab39	Apalache	Except2Fun	NumGe	True	Passed	Model Under Test Equivalent Model
7e62939b75a3b0e5ab6389d5691d9d3be97e8212	Apalache	Except2Fun	NumGe	False	Passed	Model Under Test Equivalent Model
ef7e7c852958ccbf037d9fbf754d2f36a7d606ec	Apalache	Except2Fun	NumLt	True	Passed	Model Under Test Equivalent Model
a93b6407373617676617f5c2a15145a07bbcae0a	Apalache	Except2Fun	NumLt	False	Passed	Model Under Test Equivalent Model
fd03cfb226cbc625ef16054534e5ad238e94bc0d	Apalache	Except2Fun	NumLe	True	Passed	Model Under Test Equivalent Model
37c218aabeb73ac6877f2d5c029f6511d65c1245	Apalache	Except2Fun	NumLe	False	Passed	Model Under Test Equivalent Model
dfbd636f891ac0330c64df6440b7802ebcf75caf	Apalache	Except2Fun	DefFun	True	Passed	Model Under Test Equivalent Model
cb4ba33fa627e47ac05e7104994efa7ef1243844	Apalache	Except2Fun	DefFun	False	Passed	Model Under Test Equivalent Model
39f2c8ca51394b76eb6f36ad488eca06a648fc70	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDefFun	True	Passed	Model Under Test Equivalent Model
36b2b8d7348be8d178f08a48209dca3e7c5dd89f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDefFun	False	Passed	Model Under Test Equivalent Model
1a6afa488893224bb332b49e780468a531508b5f	Apalache	Except2Fun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
fcbf5e3640cf03a9de95ffbfaded05249ab5ea73	Apalache	Except2Fun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
52c0a44d1c89dce0667d89db832a34bce1db6db2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
08e4f46e108614184deedb11366978ac91690084	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
dd96f3f11c8ea85691458ea20f56df8c8541bfe3	Apalache	Except2Fun	Def0	True	Passed	Model Under Test Equivalent Model
9cf77670849c851602ee8f039ccfdeabfc8fafa8	Apalache	Except2Fun	Def0	False	Passed	Model Under Test Equivalent Model
0c1efa83f9e4aba17d571376691e3ccad325d0a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef0	True	Passed	Model Under Test Equivalent Model
53c07ca194df393d09b2d6d66b11f29311b1383f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef0	False	Passed	Model Under Test Equivalent Model
15e6ee661ac741e3324356c62ef5d4a7c65c5f4f	Apalache	Except2Fun	Def1	True	Passed	Model Under Test Equivalent Model
3dcc9b3c99f480742dc944f3d346ed5f9786bf4d	Apalache	Except2Fun	Def1	False	Passed	Model Under Test Equivalent Model
c0f06be3fead67e4acdb14b37a518bc472a4cc06	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1	True	Passed	Model Under Test Equivalent Model
3c0dc8f885b0986fa4cfe2d62ba11e04af2ea948	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1	False	Passed	Model Under Test Equivalent Model
d8963097b687979a00553418837d111b14b9a7cb	Apalache	Except2Fun	Def2	True	Passed	Model Under Test Equivalent Model
d0364a8a072b3266e393831a336f70998cec24ab	Apalache	Except2Fun	Def2	False	Passed	Model Under Test Equivalent Model
d41bc6eac38934bb0b03e4fee5b373ec50fd0075	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef2	True	Passed	Model Under Test Equivalent Model
7eacc06275342fee4b820f742b2f867a58336d95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef2	False	Passed	Model Under Test Equivalent Model
37f5fa7593cd47007548ddbce0d15105ce33a7bb	Apalache	Except2Fun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
40425520a1bcb2f2393e2e3ec4fb6b65da243360	Apalache	Except2Fun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
72eaaa552ec394f9b1021c1fe4f70a8d6154d728	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
24c1b4d00a8741293d1875c61e7ecb163581e0f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
af66e6ce6eaadb7c3fed265d81d913802fb91317	Apalache	Except2Fun	Extends	True	Passed	Model Under Test Equivalent Model
975c8f53fd58ea3da82546ac7c67574a2f694a10	Apalache	Except2Fun	Extends	False	Passed	Model Under Test Equivalent Model
6a5c3bbaf983eea82df35ec78678d533c35acb2a	Apalache	Except2Fun	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
dad693f6ef56a2c844baf18eb2ed2a50ab817fe9	Apalache	Except2Fun	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
74e819edabfd2cfe075ca44241769eae8ada173c	Apalache	Except2Fun	Variable	True	Passed	Model Under Test Equivalent Model
408f3108b3899176809b394e37310031d19cf0ee	Apalache	Except2Fun	Variable	False	Passed	Model Under Test Equivalent Model
5538db2148d9a53814d85e7a5157bb9f61e0bb23	Apalache	Except2Fun	Constant	True	Passed	Model Under Test Equivalent Model
2818e7960e1f5d5d31fe7d2b08a1739623759a4b	Apalache	Except2Fun	Constant	False	Passed	Model Under Test Equivalent Model
c73ab9b1ff74db60cfe179d531a35f17673882e5	Apalache	Except2Fun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
37d71a712725188d07866ff6a6348184bc45ef10	Apalache	Except2Fun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
148ef11a29134cec07df22a40759c364b5ab4ddd	Apalache	Except2Fun	Instance	True	Passed	Model Under Test Equivalent Model
0f5171b2e78138a1e71f6b7f8f23917e7b80a1fa	Apalache	Except2Fun	Instance	False	Passed	Model Under Test Equivalent Model
e15cc420344d913b3174398109272ddc03e5efee	Apalache	Except2Fun	InstanceWith	True	Passed	Model Under Test Equivalent Model
09a1109bee874264be530a61f74fb51b086f4a9e	Apalache	Except2Fun	InstanceWith	False	Passed	Model Under Test Equivalent Model
bebf1bf838348d79bc78a63184728e72ef0a1816	Apalache	Except2Fun	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0fa43a4109539a13289dfe2b0e10632a9ff579ff	Apalache	Except2Fun	InstanceNamed	False	Passed	Model Under Test Equivalent Model
97bffc9fc03ff8b32c8390d7cb6f0f37b1ae7d1a	Apalache	Except2Fun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8eae7059920ae3fb05654a91b9f54bcef7606ff0	Apalache	Except2Fun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
b7c799973f4410f9d1a127d01797ee6c0c0786d7	Apalache	Except2Fun	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
533a3c681660bfceb86b7c994d18aa9fa56bd5b3	Apalache	Except2Fun	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
910c09175c41efa3499b2d304455c7616921bbbb	Apalache	Except2Fun	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
e9238eb624f92c2d94cd06bdc5a0b21f3fa1004f	Apalache	Except2Fun	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
4034e6fd23ad18ec688ecc27358b63d7954d5313	Apalache	Except2Fun	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
591c2f3aafc7e83293560e95d54affa75de8ecb5	Apalache	Except2Fun	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
393eaea9237520171d75beddc68a24fd58609a7e	Apalache	Except2Fun	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
6761bb0a6369fed68964350d134c9d3cb4867f3c	Apalache	Except2Fun	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
e23eb6f30867b3fc6a7add003019246031209746	Apalache	Except2Fun	Enabled	True	Passed	Model Under Test Equivalent Model
c002810502fadb18c6d940c3b07e81db022158a5	Apalache	Except2Fun	Enabled	False	Passed	Model Under Test Equivalent Model
b79ae6facd0ea8cbbf8e17b30f5e53fe9f86c890	Apalache	Except2Fun	Cross2	True	Passed	Model Under Test Equivalent Model
2aeaa139c4ba479a5909532864255e4a1b392f6f	Apalache	Except2Fun	Cross2	False	Passed	Model Under Test Equivalent Model
5dfdaec4b64b2d80d3c15ee2aa61a0dc325b3a37	Apalache	Except2Fun	Cross3	True	Passed	Model Under Test Equivalent Model
8f9ea8834c7c1b120b13cce3194d77b9970ea6d6	Apalache	Except2Fun	Cross3	False	Passed	Model Under Test Equivalent Model
d0244dfe7881a08aa6b5c06c982ddf384e1425f1	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))	Except2Fun	FunSet	True	Passed	Model Under Test Equivalent Model
be56c6fc45de1cda522bde33b9a4f4c51712eaf2	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))	Except2Fun	FunSet	False	Passed	Model Under Test Equivalent Model
f310e647bd106dffc472c3af33c8ae0c196e6d64	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)	Except2Fun	RecordSet	True	Passed	Model Under Test Equivalent Model
c44093972b345fa5bfb6c24a808653e656485259	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)	Except2Fun	RecordSet	False	Passed	Model Under Test Equivalent Model
576bf1a06c7ccd18cabc7eca9f66503c6185116e	Apalache	Except2Fun	SetDiff	True	Passed	Model Under Test Equivalent Model
97725caca949912e50357eca3b5103443ef5c85e	Apalache	Except2Fun	SetDiff	False	Passed	Model Under Test Equivalent Model
c18bce094fb6e8cf00968019f29498a8e53e579a	Apalache	Except2Fun	SetUnion	True	Passed	Model Under Test Equivalent Model
aa57397fd8e5c9f53b54226c3cb09876bd4f5647	Apalache	Except2Fun	SetUnion	False	Passed	Model Under Test Equivalent Model
f218f575dbcce9fcbf048b0c35368ff96092b104	Apalache	Except2Fun	SetIntersect	True	Passed	Model Under Test Equivalent Model
2600bca9fde494fea79e69916e08ef38be098840	Apalache	Except2Fun	SetIntersect	False	Passed	Model Under Test Equivalent Model
30d55acd9cf0ed349e39b1dd01d498f0dbc94a77	Apalache	Except2Fun	SubsetEq	True	Passed	Model Under Test Equivalent Model
9f861880b81e4e76dd1ee48e59dda780cd51db2f	Apalache	Except2Fun	SubsetEq	False	Passed	Model Under Test Equivalent Model
94c4adf8616713ccee143a1c10e2e41b19961349	Apalache	Except2Fun	IfCond	True	Passed	Model Under Test Equivalent Model
8946faf9d1c1be958803c200226a2a7ee669b6e0	Apalache	Except2Fun	IfCond	False	Passed	Model Under Test Equivalent Model
21e18939400651c51d7e4f66e2b6b6402b72983f	Apalache	Except2Fun	IfThen	True	Passed	Model Under Test Equivalent Model
c16962b6b5c8c7770500829f1d5d5d5a3f8142de	Apalache	Except2Fun	IfThen	False	Passed	Model Under Test Equivalent Model
7da240f7bfaa1d35ed843a39cdb844ca8f1c5715	Apalache	Except2Fun	IfElse	True	Passed	Model Under Test Equivalent Model
f01edfd0365413092670b1258c991e13f7365d8d	Apalache	Except2Fun	IfElse	False	Passed	Model Under Test Equivalent Model
4783790b8100a9c6916caafb48693f71f7b320d6	Apalache	Except2Fun	Subset	True	Passed	Model Under Test Equivalent Model
11dc6b099f14d60fc19f37b2480f21a4616f4a81	Apalache	Except2Fun	Subset	False	Passed	Model Under Test Equivalent Model
2e8183497912c0d0daac3d007518b1bc53a319cb	Apalache	Except2Fun	Domain	True	Passed	Model Under Test Equivalent Model
4f078ddba69ff7d359aecb747b9dac10d709f25a	Apalache	Except2Fun	Domain	False	Passed	Model Under Test Equivalent Model
b1fd48293dc68f4b1ef2c0dc0ffaa0ed59d7fb18	Apalache	Except2Fun	Union	True	Passed	Model Under Test Equivalent Model
2d2651bc97a53f40489bc17d54980e3a6247c75f	Apalache	Except2Fun	Union	False	Passed	Model Under Test Equivalent Model
b8c2153b1266a635b7d4eb2c35f04cc66f5cae67	Apalache	Except2Fun	Unchanged	True	Passed	Model Under Test Equivalent Model
2d9398f9ddc8c0dd2053c41ee41ae9d6bd708933	Apalache	Except2Fun	Unchanged	False	Passed	Model Under Test Equivalent Model
d4623085e9cb8d3de69e9aa355999be1b6026411	Apalache	Except2Fun	Equivalence	True	Passed	Model Under Test Equivalent Model
bf52fbbb97a70c30b187e7d19ddb23cf35ff4ffc	Apalache	Except2Fun	Equivalence	False	Passed	Model Under Test Equivalent Model
e925959bb32491494b3931403d2cd16a40d97168	Apalache	Except2Fun	StringEmpty	True	Passed	Model Under Test Equivalent Model
f35673ee4b74a21994dc3d4bb5dbe1acab6f4ef1	Apalache	Except2Fun	StringEmpty	False	Passed	Model Under Test Equivalent Model
ba0888613ca22b3a1aa9085295acdb3a62ea1508	Apalache	Except2Fun	String	True	Passed	Model Under Test Equivalent Model
ae5ee85c0842e06cc61a5cc1eaa357341d252cdd	Apalache	Except2Fun	String	False	Passed	Model Under Test Equivalent Model
c4b44af6d6ef757abc73bdb9a442c4979b8e8cce	Apalache	Except2Fun	SeqLen	True	Passed	Model Under Test Equivalent Model
17e436e3eb96fce2f270dd85665f95d68218aedc	Apalache	Except2Fun	SeqLen	False	Passed	Model Under Test Equivalent Model
6745cee984910016d616f0733183f4eb7a8a2064	Apalache	Except2Fun	SeqConcat	True	Passed	Model Under Test Equivalent Model
b91e4bd8d17124138c5f5ce95518980f03b56b55	Apalache	Except2Fun	SeqConcat	False	Passed	Model Under Test Equivalent Model
45d8f4f6067f677409261345f2136349212771a4	Apalache	Except2Fun	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
dc922bff4a8e7c091757bcd1b87ec783651deae6	Apalache	Except2Fun	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
c8bc88df4e8106f9444969bb94e45555bac24d0d	Apalache	Except2Fun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
79254888cda7e5474b02ab230542b2b6cabf22e6	Apalache	Except2Fun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c9937a7f0956d16fd7703ceee552f6d71a3510e6	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	Except2Fun	NumRange	True	Passed	Model Under Test Equivalent Model
ae8982496fad355a92909420425754558f756218	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	Except2Fun	NumRange	False	Passed	Model Under Test Equivalent Model
afbe6de5f68b7734d9400ca2c9da990661c7a8cb	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except2Fun	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
f04b457a8a463ff9712ad4d046d963c611712fa1	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except2Fun	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
9df2a6e76a05cdc24ee667dfd2d2aab3e9562f12	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]]	Except2Fun	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
b1eef7217b76890800402662e621bb5e218fae97	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]]	Except2Fun	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
b1637be5986efafbcf5afc2d6bc45762d1130e7c	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except2Fun	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
7a916adabd28c171f9e19b74c7187054ae57fc08	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Except2Fun	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
85e1e7bd913eef3b48b358a836719e418c21fceb	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except2Fun	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
f63f60dd88d1e21cb85e4887541b9318a7e9d921	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except2Fun	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
f975eea6ca81fcc31dda5112b88e50831cba2636	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except2Fun	TlcEval	True	Passed	Model Under Test Equivalent Model
59c83e035368799395983feda5aa593f4349d7ab	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except2Fun	TlcEval	False	Passed	Model Under Test Equivalent Model
bec26bcc74b29f29cbbc5c4b644a6e475d68f177	Apalache	Except2Fun	BagBagToSet	True	Passed	Model Under Test Equivalent Model
52ce1182015d294bf1d924dd6fc032deea868339	Apalache	Except2Fun	BagBagToSet	False	Passed	Model Under Test Equivalent Model
369b284d5ed2e621a250098d8956c1c6babc08fd	Apalache	Except2Fun	BagSetToBag	True	Passed	Model Under Test Equivalent Model
297910eefae8df7ce55ece195424becb52a030c3	Apalache	Except2Fun	BagSetToBag	False	Passed	Model Under Test Equivalent Model
05c42942a5428dc90cf99e7f3e09b44d7dc31efd	Apalache	Except2Fun	BagBagIn	True	Passed	Model Under Test Equivalent Model
71f7e735428c9ea9b5d6dffe09e25aaa9346f9c0	Apalache	Except2Fun	BagBagIn	False	Passed	Model Under Test Equivalent Model
3ebff44d0418627dcc3f89c704944bbaedc01bde	Apalache	Except2Fun	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
dd957dc58140235b13ebd12588ba7ea8b87ea4b2	Apalache	Except2Fun	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
e24195bcbd3c0c3f2c9cbfcc57ba440e167efb33	Apalache	Except2Fun	BagAddBag	True	Passed	Model Under Test Equivalent Model
486711dcce9cfde36b76c3efa3496fe8636e880d	Apalache	Except2Fun	BagAddBag	False	Passed	Model Under Test Equivalent Model
22cdbcca7d27a551e89d7cc8a5603b426f255dd2	Apalache	Except2Fun	BagBagSub	True	Passed	Model Under Test Equivalent Model
f8b43af09d73e472b66398e4e1459e625786ae89	Apalache	Except2Fun	BagBagSub	False	Passed	Model Under Test Equivalent Model
0e691a2f82666d16689670ca162a33b9d2e3b547	Apalache	Except2Fun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
61affb31eb22a75de483c9c783a20f66c54da51e	Apalache	Except2Fun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
c2f786f1c69396cd6161e82d61d55c946556ba9d	Apalache	Except2Fun	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
58c7726987b24819594eaf77a5c29041dac044d3	Apalache	Except2Fun	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
e835306dcf9195a290b767c4acca2b013b8b3b4c	Apalache	Except2Fun	BagBagUnion	True	Passed	Model Under Test Equivalent Model
bd7a6e463234d09309d915de18e02951a57934f3	Apalache	Except2Fun	BagBagUnion	False	Passed	Model Under Test Equivalent Model
12f96ecc2c0ef5f04e77ef0cfa7584176a176520	Apalache	Except2Fun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8c93eac6fd943e48a87e7a152d1403b864afa847	Apalache	Except2Fun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
fbae0449d7abb899da21d70fe7e8e5d23f01868f	Apalache	Except2Fun	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
64669de3ef80d2b23daf94f47dcff4e5d9aec83e	Apalache	Except2Fun	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
61a2632b7f4792c495a8bb3c8c464ba759dcdc78	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except2Fun	BagSubBag	True	Passed	Model Under Test Equivalent Model
bd3d6293511cc35ca3f06f5091e2b4669300cf3a	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Except2Fun	BagSubBag	False	Passed	Model Under Test Equivalent Model
f886ff78967100ea2e2c05537af5e102ffcb2f01	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)	Except2Fun	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
1afbbd528d7356304a48d952325d3c1f570d961a	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)	Except2Fun	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
e4ad0b2cced8df2e6c4b21987bbd7b2a3b57b4e3	Apalache	Except2Fun	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
a6f2bf306357013bc21028365f16ab2b4d1581da	Apalache	Except2Fun	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
f05bd0c07bd80e156af6f4953c96d574f734f80a	Apalache	Except2Fun	SeqHead	True	Passed	Model Under Test Equivalent Model
96cdd7758ff3ba605e2bde1c3946384c03e78e28	Apalache	Except2Fun	SeqHead	False	Passed	Model Under Test Equivalent Model
8e38806eb2b791a8a5f251ea877ee6dfd5096238	Apalache	Except2Fun	SeqTail	True	Passed	Model Under Test Equivalent Model
b1ce641d43117366c18476322f3e6c862e0a8c70	Apalache	Except2Fun	SeqTail	False	Passed	Model Under Test Equivalent Model
bd8747da00d90f7028bf3f6178f2abe81bded4a1	Apalache	Except2Fun	SeqAppend	True	Passed	Model Under Test Equivalent Model
59b5d9eaf7c38a31139c329c23963848dba7510f	Apalache	Except2Fun	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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