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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
2bb335496f6224ca4e09e31dbcff9eab68c6da77	Apalache	Eq	Cross2	True	Passed	Model Under Test Equivalent Model
152e231066b06663a2f08177182562d308ac338b	Apalache	Eq	Cross2	False	Passed	Model Under Test Equivalent Model
a03365fad35c5f5b5c40410d4558b5a857a28148	Apalache	Ne	Cross2	True	Passed	Model Under Test Equivalent Model
dc14621abde83c60e566d133244c02e622b69929	Apalache	Ne	Cross2	False	Passed	Model Under Test Equivalent Model
3cad38ed1cbd5ebbce148223c437de95dc2a8c7e	Apalache	Let	Cross2	True	Passed	Model Under Test Equivalent Model
9540c274709eef93d2abceee3210486c3ad0440a	Apalache	Let	Cross2	False	Passed	Model Under Test Equivalent Model
9f550f24499d2ed1754fe335de7103b137cc20fc	Apalache	Set0	Cross2	True	Passed	Model Under Test Equivalent Model
aa7f3056b901b45d7a0e25f85cbf8f12e5744cdd	Apalache	Set0	Cross2	False	Passed	Model Under Test Equivalent Model
a20a4636cddb832fc1afd537123c00eb22f943b4	Apalache	Set1	Cross2	True	Passed	Model Under Test Equivalent Model
e8c71bec3daa48276bab3da2c7053df4c8c97868	Apalache	Set1	Cross2	False	Passed	Model Under Test Equivalent Model
f321686d1da654ca6f349e9a1830623a645db0b8	Apalache	Set2	Cross2	True	Passed	Model Under Test Equivalent Model
22bcf1cc94bac734dd03d55651c43db919922f42	Apalache	Set2	Cross2	False	Passed	Model Under Test Equivalent Model
dfa36751eebefb7522f305ccf313852439ceea24	Apalache	Fun	Cross2	True	Passed	Model Under Test Equivalent Model
a08f4594577a19c9cc95d41e226f48fe7ed0137c	Apalache	Fun	Cross2	False	Passed	Model Under Test Equivalent Model
9b48bab97f695c94f7e9ab77d13e555a99611765	Apalache	In	Cross2	True	Passed	Model Under Test Equivalent Model
663b0d5250265fb9c9d591f12f506f4b8a7b48e9	Apalache	In	Cross2	False	Passed	Model Under Test Equivalent Model
75980893d9fabe871a5f3f15270d28e60bff9fc2	Apalache	NotIn	Cross2	True	Passed	Model Under Test Equivalent Model
88e7e90e5d191d7b82c7e5c17627d8a49fdfa2f3	Apalache	NotIn	Cross2	False	Passed	Model Under Test Equivalent Model
fe09de3dad08e69a6d0912d0df3c887010c9f22d	Apalache	Record	Cross2	True	Passed	Model Under Test Equivalent Model
1beda44657277a46883946e1b1ca40eb5b85d7b7	Apalache	Record	Cross2	False	Passed	Model Under Test Equivalent Model
356e9807c79bb21eaeb56865048e6ca59cc5e229	Apalache	Tuple	Cross2	True	Passed	Model Under Test Equivalent Model
504943cdf3249bbd4730f08c51ee63de8fea6dbc	Apalache	Tuple	Cross2	False	Passed	Model Under Test Equivalent Model
0d173ee986fd20474565425305c51fa46b6e4590	Apalache	FunApp	Cross2	True	Passed	Model Under Test Equivalent Model
38a3922457e7dbb24c2fc8b9de1e48152c62f7b6	Apalache	FunApp	Cross2	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
4a9bab24032ba1559d3646e7a39834d06ef3b132	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Cross2	True	Passed	Model Under Test Equivalent Model
d2f86f72a400a4b201a110c6fb6584ce4b6dbd8a	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Cross2	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
b58d86f78362c31042a32b9df6134178fdb8066f	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Cross2	True	Passed	Model Under Test Equivalent Model
a085d69614e523cf96c10605b17e62b913c6bf38	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Cross2	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
74784d2d653c2eb03695c207ff8cef195702905a	Apalache	Prime	Cross2	True	Passed	Model Under Test Equivalent Model
0a796f7d961cd3175781a3819308acf6861d2a66	Apalache	Prime	Cross2	False	Passed	Model Under Test Equivalent Model
403c2ebd6abedaf05d5571df390736e5345d641f	Apalache	DefFun	Cross2	True	Passed	Model Under Test Equivalent Model
134f5d3cd54bc0744059d2c49b06b11afd4623c7	Apalache	DefFun	Cross2	False	Passed	Model Under Test Equivalent Model
a23232685d1faaf8bef41b1f4be163a2fc229d61	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Cross2	True	Passed	Model Under Test Equivalent Model
6db2e714ccbcbca87eae7fba1f42475ed6688b65	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Cross2	False	Passed	Model Under Test Equivalent Model
a5a0b8f6b59bd647ea623d95c209c4a81d09355c	Apalache	DefFunRecursive	Cross2	True	Passed	Model Under Test Equivalent Model
4c08fa1d3a15b3855eb87384099af038b3676503	Apalache	DefFunRecursive	Cross2	False	Passed	Model Under Test Equivalent Model
c10ebf7b76047473ae694a9561d168485d4224fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Cross2	True	Passed	Model Under Test Equivalent Model
47ccec197734a29ceb3aaa53680e2b96d3515350	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Cross2	False	Passed	Model Under Test Equivalent Model
b827ea892250fe00a42ae6ddc970a97e526d99f0	Apalache	Def0	Cross2	True	Passed	Model Under Test Equivalent Model
dad8d80468fec87489f09df06e9ed5c19936a63a	Apalache	Def0	Cross2	False	Passed	Model Under Test Equivalent Model
f9ebe48103bb4fbc19776b48ba18bf6b175ddd20	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Cross2	True	Passed	Model Under Test Equivalent Model
34b2116e190a3618016c1e0e80103db1a1194c21	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Cross2	False	Passed	Model Under Test Equivalent Model
e0320857d1e6af37ea868a45948a9d68964bf4d5	Apalache	Def1	Cross2	True	Passed	Model Under Test Equivalent Model
475394aea60e80cf2da523cf4e51e4ec3244cf97	Apalache	Def1	Cross2	False	Passed	Model Under Test Equivalent Model
5e07f120e9cb98738540b748a420e11432381ee6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Cross2	True	Passed	Model Under Test Equivalent Model
50ece3b8b5d3e4899280e15d38b2a68a9de26fc2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Cross2	False	Passed	Model Under Test Equivalent Model
2fe476cecc01ab3f24040cfb23605d05fc9347a5	Apalache	Def2	Cross2	True	Passed	Model Under Test Equivalent Model
d99fe496d634eca4a383ef80f9e4ad276447c204	Apalache	Def2	Cross2	False	Passed	Model Under Test Equivalent Model
7c81b240841ca512bc000ecba75867115198fa6e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Cross2	True	Passed	Model Under Test Equivalent Model
5ce83d4b90a146986c42ebcef3d329355ead323b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Cross2	False	Passed	Model Under Test Equivalent Model
28434f038094674b834dd1bf2c5d5e619dac6f68	Apalache	Def1Recursive	Cross2	True	Passed	Model Under Test Equivalent Model
43892743957ab247cd1fc07582b577688a355124	Apalache	Def1Recursive	Cross2	False	Passed	Model Under Test Equivalent Model
13f774636da960903c9c323c15f1da13e1e674ce	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Cross2	True	Passed	Model Under Test Equivalent Model
6a750dd22e60119ddd0469d7cd5ee0b5f32bbef4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Cross2	False	Passed	Model Under Test Equivalent Model
d0f929d244e399d8f39bf19cd29e00689977d12d	Apalache	Extends	Cross2	True	Passed	Model Under Test Equivalent Model
96cf90c5c513b5578dce2a717210591de61084cf	Apalache	Extends	Cross2	False	Passed	Model Under Test Equivalent Model
134dc5e0aab4756de0ea60e4a66552bc9792934e	Apalache	ExtendsInDifferentFolder	Cross2	True	Passed	Model Under Test Equivalent Model
b4cee79def0070d951e476313f9607a826050b13	Apalache	ExtendsInDifferentFolder	Cross2	False	Passed	Model Under Test Equivalent Model
3de3fe5ddf31635e703a35918b173fbb54d68130	Apalache	Variable	Cross2	True	Passed	Model Under Test Equivalent Model
1b2ae0ecaeaa4240569a9bf95987d8f3d4fff0d9	Apalache	Variable	Cross2	False	Passed	Model Under Test Equivalent Model
0c91cc2f4e2d535ef11553e4627adc42bbc7b951	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Cross2	True	Passed	Model Under Test Equivalent Model
8874ce65878d55fd564db4c39b6970c43cea4047	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Cross2	False	Passed	Model Under Test Equivalent Model
57bd2cbd62a5de21b3b920935a7b53fbaed8e94d	Apalache	Constant	Cross2	True	Passed	Model Under Test Equivalent Model
9bf15066470575745126b1a6348f690af04c4730	Apalache	Constant	Cross2	False	Passed	Model Under Test Equivalent Model
1da76a059f93d708bdbf4be0218f38c8c79422e2	Apalache	ConstantRank1	Cross2	True	Passed	Model Under Test Equivalent Model
8029dcc3eb8b8929726860cb30d73d9d81f53fe4	Apalache	ConstantRank1	Cross2	False	Passed	Model Under Test Equivalent Model
24bb52eb2ac92ad02e758f209a9ed94d0cb8a8e6	Apalache	Instance	Cross2	True	Passed	Model Under Test Equivalent Model
34bd82046c6bc6b01ca4d3955ba9046416d3a353	Apalache	Instance	Cross2	False	Passed	Model Under Test Equivalent Model
fe8f4649f2f4e2c7e4ea9891e85a8ccfca9b9114	Apalache	InstanceWith	Cross2	True	Passed	Model Under Test Equivalent Model
8715c5a0eba88204c02dd19ceb5f39cf085c1058	Apalache	InstanceWith	Cross2	False	Passed	Model Under Test Equivalent Model
d31d305024ea1b66fc8a8671e47518b1d7540d6e	Apalache	InstanceNamed	Cross2	True	Passed	Model Under Test Equivalent Model
974bb7a10bf0ab5380fbc5b5a58e4c9e8098b8e1	Apalache	InstanceNamed	Cross2	False	Passed	Model Under Test Equivalent Model
a5446564b8ceab35aa7c8cb6988fb2be70d0f464	Apalache	InstanceNamedWith	Cross2	True	Passed	Model Under Test Equivalent Model
17ba020249c1ecdb9268970e185faad4160b18cd	Apalache	InstanceNamedWith	Cross2	False	Passed	Model Under Test Equivalent Model
75b8f0ea65d99ef5bd9dec97a2c49d7478c7a906	Apalache	InstanceInFolder	Cross2	True	Passed	Model Under Test Equivalent Model
9f312d448ef43f7a0ae905adcb528a64b1a46232	Apalache	InstanceInFolder	Cross2	False	Passed	Model Under Test Equivalent Model
4bd82f646a09c5d7d7221d8f0241233842535ed3	Apalache	InstanceWithInFolder	Cross2	True	Passed	Model Under Test Equivalent Model
c6f28de34d20614750e3b15ea48ac3362bed77c7	Apalache	InstanceWithInFolder	Cross2	False	Passed	Model Under Test Equivalent Model
118b8f66d5e8adb71fcfd3bc99c1db747e86bd57	Apalache	InstanceNamedInFolder	Cross2	True	Passed	Model Under Test Equivalent Model
c5ef6090162c17268110867c6c319c717d2cc0d2	Apalache	InstanceNamedInFolder	Cross2	False	Passed	Model Under Test Equivalent Model
18f659a24fb591457acf0352c1ee7e441a1f0743	Apalache	InstanceNamedWithInFolder	Cross2	True	Passed	Model Under Test Equivalent Model
3767fc15ecf75061580407a3643691bd39eec501	Apalache	InstanceNamedWithInFolder	Cross2	False	Passed	Model Under Test Equivalent Model
f64a4b1d07b2c43b922294aaa4c6073014cebc59	Apalache	Lambda	Cross2	True	Passed	Model Under Test Equivalent Model
68690b8f3bb2b9d820a7a3082649336792bc46b9	Apalache	Lambda	Cross2	False	Passed	Model Under Test Equivalent Model
33d0e0043ebd96e008ff7b4204504d31eb0f2619	Apalache	Cross2	Cross2	True	Passed	Model Under Test Equivalent Model
4e7775b1d4e75a4cccf83126a541d8f6148cc471	Apalache	Cross2	Cross2	False	Passed	Model Under Test Equivalent Model
df8dcffaaf2733d36eb7ba128eecb85f5ec2f2ee	Apalache	Cross3	Cross2	True	Passed	Model Under Test Equivalent Model
844f8abd903f5333fe33009758b519fdeacc052d	Apalache	Cross3	Cross2	False	Passed	Model Under Test Equivalent Model
cdfa0752a1a9abfe3a569d9d16f18b1901efd31e	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	Cross2	True	Passed	Model Under Test Equivalent Model
0a1ff74402a79050bc4793bcc0554143f9164490	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	Cross2	False	Passed	Model Under Test Equivalent Model
0e45c00eabbc3f4a5fed0fcdc746f387bf45c1af	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	Cross2	True	Passed	Model Under Test Equivalent Model
d4d76e356627df9410fee7cb30b79cbd7d29c6b2	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	Cross2	False	Passed	Model Under Test Equivalent Model
6e7ef9f9df2448f1a10d64003f6390ccd1e12cbf	Apalache	SetDiff	Cross2	True	Passed	Model Under Test Equivalent Model
879bd9822e8a0652244bdc7bf2e62b31a1e2a4ae	Apalache	SetDiff	Cross2	False	Passed	Model Under Test Equivalent Model
0c6ee13e1ed9abff3d0add31f25a62407b03a926	Apalache	SetUnion	Cross2	True	Passed	Model Under Test Equivalent Model
a530cb73ce103387228e62d3bd8c08ce3a4b9613	Apalache	SetUnion	Cross2	False	Passed	Model Under Test Equivalent Model
45c715ae5732a5efceed52112e85d7c24560e0f4	Apalache	SetIntersect	Cross2	True	Passed	Model Under Test Equivalent Model
f9b9a863b1c6dd2c783631d9e2149d1a9c900b41	Apalache	SetIntersect	Cross2	False	Passed	Model Under Test Equivalent Model
6ac8c72d431ce50768066074aa9a91cb717e2104	Apalache	SubsetEq	Cross2	True	Passed	Model Under Test Equivalent Model
bdd2e16d8dd3d3cff67ab94c94c5f98475b16092	Apalache	SubsetEq	Cross2	False	Passed	Model Under Test Equivalent Model
1436211d5c7ca258e11c6d67431fa0b377bc3436	Apalache	IfThen	Cross2	True	Passed	Model Under Test Equivalent Model
bbbc27a6805538e7a3581b28d06837e52fe2a6db	Apalache	IfThen	Cross2	False	Passed	Model Under Test Equivalent Model
2f94b1643eed8192d901c4a6ee0ab197ebe7ef34	Apalache	IfElse	Cross2	True	Passed	Model Under Test Equivalent Model
31660ecdc786018a3250f5ce1d07d3114136dad5	Apalache	IfElse	Cross2	False	Passed	Model Under Test Equivalent Model
5c2450777a041aef3d0f9a452da232c83f4a333b	Apalache	Subset	Cross2	True	Passed	Model Under Test Equivalent Model
d6d92c7c69b5ecf01beca5edfa4c8988e7b77db6	Apalache	Subset	Cross2	False	Passed	Model Under Test Equivalent Model
d48eb14d757d039e3b1ca5b4176cf09fbe38527b	Apalache	Unchanged	Cross2	True	Passed	Model Under Test Equivalent Model
399931044d316b24936b3a983d1b1b32ec68f021	Apalache	Unchanged	Cross2	False	Passed	Model Under Test Equivalent Model
73d35e6303f8197f8a10b163ed888fb5c5d325c8	Apalache	SeqSeq	Cross2	True	Passed	Model Under Test Equivalent Model
f8f6fb20d7a432b697756458b82b7b06198018a0	Apalache	SeqSeq	Cross2	False	Passed	Model Under Test Equivalent Model
b869f2e0c10ffc0eee088c134a233754d28edc51	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Cross2	True	Passed	Model Under Test Equivalent Model
c8757a40bed5287be80be978141e8035be7c2e3a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Cross2	False	Passed	Model Under Test Equivalent Model
b5cfe56d9b10614b465391dfd6e1ffe34d687b13	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Cross2	True	Passed	Model Under Test Equivalent Model
1fd49406e892ebf24ae846d66f64ee95a517f253	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Cross2	False	Passed	Model Under Test Equivalent Model
793802826d937495e8b8f784a127e3badeb17124	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Cross2	True	Passed	Model Under Test Equivalent Model
06be4169e967304abb4b51499b52b9bfcccfbc2e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Cross2	False	Passed	Model Under Test Equivalent Model
783e86572d2e99ab83207a8e2d18ecea3922a213	Apalache	BagSetToBag	Cross2	True	Passed	Model Under Test Equivalent Model
b91f6c2b3ae4531ec1520f9c1a90d4c931cd6540	Apalache	BagSetToBag	Cross2	False	Passed	Model Under Test Equivalent Model
cfcf507393e5f792110ca2657b51dccb10198fd2	Apalache	BagBagIn	Cross2	True	Passed	Model Under Test Equivalent Model
e45399d7d9db542f193762c883a4fd85ce4ada9f	Apalache	BagBagIn	Cross2	False	Passed	Model Under Test Equivalent Model
9f4ad3704bbed4a1f92f766050fd58f7f5b30d9e	Apalache	BagCopiesIn	Cross2	True	Passed	Model Under Test Equivalent Model
9c34d873f8872cec0c7fe8d304892a3c9b04ba2e	Apalache	BagCopiesIn	Cross2	False	Passed	Model Under Test Equivalent Model
56a1adbae62689317af1f5a77aa2b0c815608749	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	Cross2	True	Passed	Model Under Test Equivalent Model
6601bd2f759c2c5b2694014bacb9b82eddc6efe5	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	Cross2	False	Passed	Model Under Test Equivalent Model
fea5abb4a991ba4ec08acfbe5a478e2e375584ff	Apalache	FiniteSetsCardinality	Cross2	True	Passed	Model Under Test Equivalent Model
1c164681619589519ea305b55e122ecaabcd6cb1	Apalache	FiniteSetsCardinality	Cross2	False	Passed	Model Under Test Equivalent Model
015087e5a2aee1c9c4ccb8e0baf90b39182e191a	Apalache	SeqAppend	Cross2	True	Passed	Model Under Test Equivalent Model
9758e55a96d950da3cdf57f4d5040a8a49de08a0	Apalache	SeqAppend	Cross2	False	Passed	Model Under Test Equivalent Model

Index

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