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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
69ca1f10610058c851b7fbc79138641110e399a7	Apalache	Eq	Cross3	True	Passed	Model Under Test Equivalent Model
ea7ee53880d5263d53b0896687722fba3cb90565	Apalache	Eq	Cross3	False	Passed	Model Under Test Equivalent Model
5472850c65ad56cf657679202e2f5fd3b3a93343	Apalache	Ne	Cross3	True	Passed	Model Under Test Equivalent Model
a2d0f29caa476d975b3468fef940ddcbe5c0bbc6	Apalache	Ne	Cross3	False	Passed	Model Under Test Equivalent Model
d5e451fa0edaeeada91799c31a11ad65c5b26e94	Apalache	Let	Cross3	True	Passed	Model Under Test Equivalent Model
6a0c4e2edc1002d392e68f84bab279e1569c7515	Apalache	Let	Cross3	False	Passed	Model Under Test Equivalent Model
2b87b4643810c9e6e0a74d814139da0c432fcc3d	Apalache	Set0	Cross3	True	Passed	Model Under Test Equivalent Model
9515fe99d00cec87078062edb5ee101def748202	Apalache	Set0	Cross3	False	Passed	Model Under Test Equivalent Model
d00107bb71b7567e868ed0e4aa454435ab6ab2d8	Apalache	Set1	Cross3	True	Passed	Model Under Test Equivalent Model
5cc8a42be395e1f61b4ca5154bb7fa7c002d4c4e	Apalache	Set1	Cross3	False	Passed	Model Under Test Equivalent Model
d8b4003c69c724ad42cc27f5f27964703aac04ad	Apalache	Set2	Cross3	True	Passed	Model Under Test Equivalent Model
e7a3acd4cd89bfecd46b5872faf3b4d9146b40a1	Apalache	Set2	Cross3	False	Passed	Model Under Test Equivalent Model
ae42a455363c2a4b28be2c5d093eab9ac09f67a5	Apalache	Fun	Cross3	True	Passed	Model Under Test Equivalent Model
5e3cc77c9e1c4a8ff8d000d9360831df61173c05	Apalache	Fun	Cross3	False	Passed	Model Under Test Equivalent Model
9cedf0d4c5e11bfe0fba469d8c22188202c3eec6	Apalache	In	Cross3	True	Passed	Model Under Test Equivalent Model
0271e2794c361f95adc5fb662aa1bc812a360cd3	Apalache	In	Cross3	False	Passed	Model Under Test Equivalent Model
ec3bc1bd93fc267724225588f005e3788be5f01a	Apalache	NotIn	Cross3	True	Passed	Model Under Test Equivalent Model
287e15940c10bfa5561da5102c4163f106a7f49a	Apalache	NotIn	Cross3	False	Passed	Model Under Test Equivalent Model
2dd9c8403891a2d1464ec8503f6bbfe3ee8ef831	Apalache	Record	Cross3	True	Passed	Model Under Test Equivalent Model
4b3592e76943fc72f55e1b3235ac5ce7ae92513a	Apalache	Record	Cross3	False	Passed	Model Under Test Equivalent Model
b740ae6e99d99b0968343a41c337f9056da162aa	Apalache	Tuple	Cross3	True	Passed	Model Under Test Equivalent Model
648f4928bffe5c58e2d11f6b418abda524897d62	Apalache	Tuple	Cross3	False	Passed	Model Under Test Equivalent Model
5158f5d6a1895dadb03a49a0199329813f6372f7	Apalache	FunApp	Cross3	True	Passed	Model Under Test Equivalent Model
521972b0ddc953bd066a9b8182adb898036361bf	Apalache	FunApp	Cross3	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
cb2c8218f4197cc08a62f6545335e63ba1bec76c	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Cross3	True	Passed	Model Under Test Equivalent Model
1e2125d1b86fc3987e4fe8e43f13c6cac04b3c62	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Cross3	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
c1961f726a54489ca91059f4367847014a22cafc	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Cross3	True	Passed	Model Under Test Equivalent Model
48a0b3c521a7726654759d147261a76f130c24b1	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Cross3	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
0652909d2f5650d9d14c917aea8e59139f6a344a	Apalache	Prime	Cross3	True	Passed	Model Under Test Equivalent Model
7f28f70aa1b72fab8927e3facd8a96f74f5f9bd0	Apalache	Prime	Cross3	False	Passed	Model Under Test Equivalent Model
89f260046f46f9195d46b8f4bebf5a8b52399ca9	Apalache	DefFun	Cross3	True	Passed	Model Under Test Equivalent Model
1ba4f231df43f6c6fc18a44e125db34724f62c5b	Apalache	DefFun	Cross3	False	Passed	Model Under Test Equivalent Model
fa04150f67b1578b812922068423e127e9456fc5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Cross3	True	Passed	Model Under Test Equivalent Model
c3ea394832c9f4e0c312d35dd4a0d746b47f5bd3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Cross3	False	Passed	Model Under Test Equivalent Model
0be8f8a0ae7a92edcd0f609dfefa1e14f0bebf10	Apalache	DefFunRecursive	Cross3	True	Passed	Model Under Test Equivalent Model
7e2c6057a587a0b397d4eedcb5969140f729909f	Apalache	DefFunRecursive	Cross3	False	Passed	Model Under Test Equivalent Model
ed66f1a3939bd9f259d40ca77cf1aec394153b74	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Cross3	True	Passed	Model Under Test Equivalent Model
260ca7e4a7c1394c1b719e08414878af8c738589	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Cross3	False	Passed	Model Under Test Equivalent Model
d99401364aa3bf303e41e86a932097ec53df8dfe	Apalache	Def0	Cross3	True	Passed	Model Under Test Equivalent Model
c086af328aa7cb8dd6c5ab274a70fe0c4db23edd	Apalache	Def0	Cross3	False	Passed	Model Under Test Equivalent Model
cd8161069913e3412bd08e47adaccef4d3607761	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Cross3	True	Passed	Model Under Test Equivalent Model
afeb95598bf45370d11c10dc82997280bb0bb6a6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Cross3	False	Passed	Model Under Test Equivalent Model
0618f662eec8d3faff02acc1e1e73c49ad99ebe1	Apalache	Def1	Cross3	True	Passed	Model Under Test Equivalent Model
2b74cedab86301219a1407517f2ae3535a6955aa	Apalache	Def1	Cross3	False	Passed	Model Under Test Equivalent Model
3f654648fc06ba8339c76da44f34570276506af7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Cross3	True	Passed	Model Under Test Equivalent Model
78d634ed246221bb96273943a73d656d4b78a994	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Cross3	False	Passed	Model Under Test Equivalent Model
e2b59b6019d43d9c052315afbb2ada97649eee4a	Apalache	Def2	Cross3	True	Passed	Model Under Test Equivalent Model
94cc36755144c0530b9f55fdb77494858ea34744	Apalache	Def2	Cross3	False	Passed	Model Under Test Equivalent Model
de0b3a6a3030bfbf755e16a9bea79b1241a9b25f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Cross3	True	Passed	Model Under Test Equivalent Model
eea23edfb00ed18d27538146559b7cdd39f5746d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Cross3	False	Passed	Model Under Test Equivalent Model
36772aad66772081331eac96ee8bc0d53c6c1224	Apalache	Def1Recursive	Cross3	True	Passed	Model Under Test Equivalent Model
766c91051ae78aa80747ef159b4dc502f470e690	Apalache	Def1Recursive	Cross3	False	Passed	Model Under Test Equivalent Model
1f0660a88e7d40798f212a3efbc7a5e97c96aef6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Cross3	True	Passed	Model Under Test Equivalent Model
75c3667ff4649995b641fb4fc5ca35b748990e8c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Cross3	False	Passed	Model Under Test Equivalent Model
b56e0dfc9c4ef0d674a3d8fb5b98629bdcd6f862	Apalache	Extends	Cross3	True	Passed	Model Under Test Equivalent Model
fdcbccd6c2970ccf31385bfd113063212e4b8ce0	Apalache	Extends	Cross3	False	Passed	Model Under Test Equivalent Model
62b84679a60ad13b8dde32e94c042998b6505094	Apalache	ExtendsInDifferentFolder	Cross3	True	Passed	Model Under Test Equivalent Model
470f18145eb2a9d4800d2d00256006307562420a	Apalache	ExtendsInDifferentFolder	Cross3	False	Passed	Model Under Test Equivalent Model
fa3b409ea0e1d5fde08da665a5e3d3a1aa09a391	Apalache	Variable	Cross3	True	Passed	Model Under Test Equivalent Model
dacd6c8fbc004fee508108aa8cf4dc49266f1610	Apalache	Variable	Cross3	False	Passed	Model Under Test Equivalent Model
f0c0a83d5ed074f0f9ac4a1de8d568a3ec2a5d9b	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Cross3	True	Passed	Model Under Test Equivalent Model
83f39696b385c365722af68968bd3b35fd1440e0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Cross3	False	Passed	Model Under Test Equivalent Model
2f21bc1a04e371c732193685d3b946d15e672d88	Apalache	Constant	Cross3	True	Passed	Model Under Test Equivalent Model
a2e06e2f81ba730581eed59f45947da81d7b7277	Apalache	Constant	Cross3	False	Passed	Model Under Test Equivalent Model
b874aeb345e9ffb80078a3c0a1e5142248876726	Apalache	ConstantRank1	Cross3	True	Passed	Model Under Test Equivalent Model
febd629f7f67ac73cfc3600c075bb819174a2877	Apalache	ConstantRank1	Cross3	False	Passed	Model Under Test Equivalent Model
30f6cc897ee95f47c644bf44d7d3009b325fd271	Apalache	Instance	Cross3	True	Passed	Model Under Test Equivalent Model
2d04aa9b79170389e73afb026634960b5a5f1174	Apalache	Instance	Cross3	False	Passed	Model Under Test Equivalent Model
05dc5af69bac28bd3cffcc82d9735eb18e96df91	Apalache	InstanceWith	Cross3	True	Passed	Model Under Test Equivalent Model
453c2dfcfeb314295ac09193c27e886a3efc93f4	Apalache	InstanceWith	Cross3	False	Passed	Model Under Test Equivalent Model
a814ca19b736216d46e3b5ea6e1eded7f0cdd9fc	Apalache	InstanceNamed	Cross3	True	Passed	Model Under Test Equivalent Model
985a0320715d43a3ecc1f6a94f2c36d757495d30	Apalache	InstanceNamed	Cross3	False	Passed	Model Under Test Equivalent Model
28555449c7a8c4ef110bcb680e990149968753b0	Apalache	InstanceNamedWith	Cross3	True	Passed	Model Under Test Equivalent Model
e4243e6dcc3676dee512440abf88543cd637a044	Apalache	InstanceNamedWith	Cross3	False	Passed	Model Under Test Equivalent Model
2f60359512ab0835ea61802cf0bebf7faaac8d62	Apalache	InstanceInFolder	Cross3	True	Passed	Model Under Test Equivalent Model
805a94ae3dc9f5f2ffe3f35983c947ef83dab602	Apalache	InstanceInFolder	Cross3	False	Passed	Model Under Test Equivalent Model
bf438dc4350263bc39ed0850901c1e5616624a15	Apalache	InstanceWithInFolder	Cross3	True	Passed	Model Under Test Equivalent Model
f0f2ce48dbf548222f7ed57ba53724db6b14190a	Apalache	InstanceWithInFolder	Cross3	False	Passed	Model Under Test Equivalent Model
a0b91e8683d30f99666f16cdbf817c63f25e5c58	Apalache	InstanceNamedInFolder	Cross3	True	Passed	Model Under Test Equivalent Model
e4171386ab1b5f0bdd3319a05ae28d2d22681e0a	Apalache	InstanceNamedInFolder	Cross3	False	Passed	Model Under Test Equivalent Model
d327ed56c41d0c066e3ef78f0bac5a7cf28a1d64	Apalache	InstanceNamedWithInFolder	Cross3	True	Passed	Model Under Test Equivalent Model
855807b0e199cfef1758334f2dae95126d42b55a	Apalache	InstanceNamedWithInFolder	Cross3	False	Passed	Model Under Test Equivalent Model
2644b2fcc898546239e2c01119da9e6e5c4263d9	Apalache	Lambda	Cross3	True	Passed	Model Under Test Equivalent Model
1260f84d403f42607c8924b12716e0d37f88cb7a	Apalache	Lambda	Cross3	False	Passed	Model Under Test Equivalent Model
b2a9d78fa20b244f54a1335b9d7bd3b87e3741c4	Apalache	Cross2	Cross3	True	Passed	Model Under Test Equivalent Model
4aa26f110c24ff84c5f2a77a3b0eead7f678a16d	Apalache	Cross2	Cross3	False	Passed	Model Under Test Equivalent Model
e8991ba6e96d383f53ced90789416071310d7147	Apalache	Cross3	Cross3	True	Passed	Model Under Test Equivalent Model
d719ca2f771961dbd34f8f96d7ead412d743ebf6	Apalache	Cross3	Cross3	False	Passed	Model Under Test Equivalent Model
053eed7b636742fdc7bf4d2c2ac75a7687557a02	TLC with reduction strategy: Case 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))	FunSet	Cross3	True	Passed	Model Under Test Equivalent Model
44a22b656153f2ebf1ab8e2166f4e6a86c0c4c31	TLC with reduction strategy: Case 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))	FunSet	Cross3	False	Passed	Model Under Test Equivalent Model
f596ef3bb455f987c996c87ae55fc1495c65901a	TLC with reduction strategy: Case 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)	RecordSet	Cross3	True	Passed	Model Under Test Equivalent Model
216c73815c5fae14cadd648c941e2b751e1989c2	TLC with reduction strategy: Case 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)	RecordSet	Cross3	False	Passed	Model Under Test Equivalent Model
30c859e738d289a7ab98d3fe451a52a90d1d1003	Apalache	SetDiff	Cross3	True	Passed	Model Under Test Equivalent Model
401b0d6342fefd117ed68ef002ec7c50cef17c95	Apalache	SetDiff	Cross3	False	Passed	Model Under Test Equivalent Model
e24fb75c892c86dc03172b9cafe8b9b47ba86289	Apalache	SetUnion	Cross3	True	Passed	Model Under Test Equivalent Model
743c7de55d223001e4cf9a5b25faf23211db1cf3	Apalache	SetUnion	Cross3	False	Passed	Model Under Test Equivalent Model
5da8642eb95d2e7e07b9dad468046b960c0b898f	Apalache	SetIntersect	Cross3	True	Passed	Model Under Test Equivalent Model
3de63430229130b680bb290263a25e0e5f25f1b8	Apalache	SetIntersect	Cross3	False	Passed	Model Under Test Equivalent Model
c06eebec5b2eb2df91ac1b749f1ef3542d59f0fb	Apalache	SubsetEq	Cross3	True	Passed	Model Under Test Equivalent Model
7ce5234403239ecb3048690a73a1c7ab2eb74518	Apalache	SubsetEq	Cross3	False	Passed	Model Under Test Equivalent Model
bf7621e493f05fddd7a394f65060072615d66907	Apalache	IfThen	Cross3	True	Passed	Model Under Test Equivalent Model
12198ca35ad1186b271ef4c59fa13f052a8ef3c1	Apalache	IfThen	Cross3	False	Passed	Model Under Test Equivalent Model
7e9c6be4b44b8c7669ddb652888b08bb361d0000	Apalache	IfElse	Cross3	True	Passed	Model Under Test Equivalent Model
44ac59c27e58dec0b5490bde785f58ab815f9250	Apalache	IfElse	Cross3	False	Passed	Model Under Test Equivalent Model
c62290d7d7e6e41fd4d5d18033ecce593a911dfe	Apalache	Subset	Cross3	True	Passed	Model Under Test Equivalent Model
1995c37b6f451db2a035d5c18ea0deddeee1c361	Apalache	Subset	Cross3	False	Passed	Model Under Test Equivalent Model
bc2de906152d7cd7940872d23844630952abb37c	Apalache	Unchanged	Cross3	True	Passed	Model Under Test Equivalent Model
b4a824abeb520d664498dd19a6f2f785b853ebfe	Apalache	Unchanged	Cross3	False	Passed	Model Under Test Equivalent Model
70a73ae264fec9021cd6f2423891218714c20b0c	Apalache	SeqSeq	Cross3	True	Passed	Model Under Test Equivalent Model
af94c56f1f06e3f4af8c194217487c6d98c405ba	Apalache	SeqSeq	Cross3	False	Passed	Model Under Test Equivalent Model
106239261bfa6ea4370b1392042a072a8041c7bc	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Cross3	True	Passed	Model Under Test Equivalent Model
249cd502124bbdc1625a55ed0c5c430220376795	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Cross3	False	Passed	Model Under Test Equivalent Model
13e92d5c59deb365f1fd3a335ddfadbb81804f3a	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Cross3	True	Passed	Model Under Test Equivalent Model
b937c9d2117c4001aa8fb97756d17727b2f17520	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Cross3	False	Passed	Model Under Test Equivalent Model
47db8c2bbb11182309f525e7cb92e88ae8a33bcf	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Cross3	True	Passed	Model Under Test Equivalent Model
b686a0555d3ceb352d9c993918ccc9aef6722978	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Cross3	False	Passed	Model Under Test Equivalent Model
27eec23376db1c946ad63b0c290ff0d4fdf3cf3d	Apalache	BagSetToBag	Cross3	True	Passed	Model Under Test Equivalent Model
926200627436472577621b11f05c42fe8943a0d8	Apalache	BagSetToBag	Cross3	False	Passed	Model Under Test Equivalent Model
f1934fe9e426e63def2efb812355b995beda1da3	Apalache	BagBagIn	Cross3	True	Passed	Model Under Test Equivalent Model
29f40126ebec693f223896e37dfdf3117130c754	Apalache	BagBagIn	Cross3	False	Passed	Model Under Test Equivalent Model
f323229ddd342866daba2bc2fc30faebf9d5ec36	Apalache	BagCopiesIn	Cross3	True	Passed	Model Under Test Equivalent Model
b061f0e1eab43908db2c12e7ee97217e08e0eb81	Apalache	BagCopiesIn	Cross3	False	Passed	Model Under Test Equivalent Model
4edffca443a2033d87f540dea9fa6bd446838c32	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Cross3	True	Passed	Model Under Test Equivalent Model
4af2ccf5b9d341e81a40f964fe3abe386ec5436a	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Cross3	False	Passed	Model Under Test Equivalent Model
698f8c40e6820f31eebb0cac77daf5e22cb07824	Apalache	FiniteSetsCardinality	Cross3	True	Passed	Model Under Test Equivalent Model
1b4f36e9af185896d252bbf78e6c26b12ca5d069	Apalache	FiniteSetsCardinality	Cross3	False	Passed	Model Under Test Equivalent Model
9ae63f69b3e7b4360f5144f627baaac8aca088c0	Apalache	SeqAppend	Cross3	True	Passed	Model Under Test Equivalent Model
6d5f48799d838c4d88456358910b3b7d1bc8a35d	Apalache	SeqAppend	Cross3	False	Passed	Model Under Test Equivalent Model

Index

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