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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3840e945f36f5e0ae5515efe79ceaed1ba12933b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross3	OneLineComment	True	Passed	Model Under Test Equivalent Model
abd5803cdb28e8570f79cda5af675b5171eb3e2f	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross3	OneLineComment	False	Passed	Model Under Test Equivalent Model
1edda6f25364b9f9ad9d078fb0ce7b3b80d81853	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross3	MultiLineComment	True	Passed	Model Under Test Equivalent Model
333ba7d6c189ad4829c6d86b461766d7a06fa01c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross3	MultiLineComment	False	Passed	Model Under Test Equivalent Model
efc69a34ec7dc84fca7f2901872971a69caa15a7	Apalache	Cross3	BoolSet	True	Passed	Model Under Test Equivalent Model
abb3094badc9605e68048f99f237776b72b5fabc	Apalache	Cross3	BoolSet	False	Passed	Model Under Test Equivalent Model
15d70c98a8b4185feb58ce064a4fc50cec433833	Apalache	Cross3	Let	True	Passed	Model Under Test Equivalent Model
34135523d889da35542717d90cfb37c9741d3865	Apalache	Cross3	Let	False	Passed	Model Under Test Equivalent Model
58befa3d2d2c15771cb043a6050374892e9fa962	Apalache	Cross3	SetEmpty	True	Passed	Model Under Test Equivalent Model
f2f8001fdda4ea7657c23b34f5e510a6f58ecbbb	Apalache	Cross3	SetEmpty	False	Passed	Model Under Test Equivalent Model
f8a180468bb04ad0b7d7d5f98d18df64e40ef531	Apalache	Cross3	Set0	True	Passed	Model Under Test Equivalent Model
1d4dfda69dd30ddd48f1133bd45b41c5e38cba38	Apalache	Cross3	Set0	False	Passed	Model Under Test Equivalent Model
215b2949c6a1daa42b9b8fb66d9a8b0a04054c85	Apalache	Cross3	Set1	True	Passed	Model Under Test Equivalent Model
3cb371ab2833ef974b72d85231068bbc9ba08df4	Apalache	Cross3	Set1	False	Passed	Model Under Test Equivalent Model
fe6dc76f018fc4f8b90494dd415559dfb3b51c52	Apalache	Cross3	Set2	True	Passed	Model Under Test Equivalent Model
7c4c0e83a7fbb635245aa978e278b2202c4ead9e	Apalache	Cross3	Set2	False	Passed	Model Under Test Equivalent Model
488fc35ea7feac160e8ad3be094b68aa134d8845	Apalache	Cross3	Choose	True	Passed	Model Under Test Equivalent Model
c0805b15b0f022b763533ecac55d28dee12ce76a	Apalache	Cross3	Choose	False	Passed	Model Under Test Equivalent Model
e12f3d0e069b2349d89456f10f5d181cf436b723	Apalache	Cross3	FunApp	True	Passed	Model Under Test Equivalent Model
373ee57578f9dbee487b9129afa62a4b01a7a00c	Apalache	Cross3	FunApp	False	Passed	Model Under Test Equivalent Model
ce7eed1e617470a52064690170277e6310f0131e	Apalache	Cross3	Prime	True	Passed	Model Under Test Equivalent Model
f2f28edcecb3d6724625fa5e57f666ed77ada0cb	Apalache	Cross3	Prime	False	Passed	Model Under Test Equivalent Model
8c60ceffc6726e196f9c50c05c9a02f23c429c4d	Apalache	Cross3	Def0	True	Passed	Model Under Test Equivalent Model
e0eeb0840ba7eb72dbb1dd24b4a1ee3fbab6ced9	Apalache	Cross3	Def0	False	Passed	Model Under Test Equivalent Model
a09cd86200e827d7ddc76d833a45097f20263a89	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef0	True	Passed	Model Under Test Equivalent Model
e64746f571ae74839e0a10517c7987fecccec53d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef0	False	Passed	Model Under Test Equivalent Model
1768bb00699c669f4ac118c1335c5ffc76c41c37	Apalache	Cross3	Def1	True	Passed	Model Under Test Equivalent Model
161026385ddbbe0b24cc8c84f0057cd961fcce97	Apalache	Cross3	Def1	False	Passed	Model Under Test Equivalent Model
b0e8e795aa23c5712260c22f7faba2ad91a89383	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1	True	Passed	Model Under Test Equivalent Model
a9fa4ed9fa5e89e6548963028581bfa153272258	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1	False	Passed	Model Under Test Equivalent Model
0e3279fa43dadf21da83199ca0a0eee02da44265	Apalache	Cross3	Def2	True	Passed	Model Under Test Equivalent Model
37a98b0d942f7fdc9c01e2519c60baeeb2123544	Apalache	Cross3	Def2	False	Passed	Model Under Test Equivalent Model
3f964cce3d44fc01d51c55206754772325222704	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef2	True	Passed	Model Under Test Equivalent Model
10f1fda32bfc1d2796b13bb8147c1a8b3643695b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef2	False	Passed	Model Under Test Equivalent Model
5e0328920d0be1f6539fb05326dae02884bc556c	Apalache	Cross3	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c64602f7c9a31fed0f7223a7dc4c099d842952c9	Apalache	Cross3	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b08f9aa13859ab904de8ebb6a625dbabab6022ea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
c7a8c2700f77eebe44a274864e2867f5cb4bbbad	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
9bf4148e9cc53c3f316938841c38159ea2fd73e0	Apalache	Cross3	Extends	True	Passed	Model Under Test Equivalent Model
d54dd7493ae43634ebcb1c7bd3676e20d46e27d2	Apalache	Cross3	Extends	False	Passed	Model Under Test Equivalent Model
a1fe249d5237be21c5d6523a90b9c43f58d5e679	Apalache	Cross3	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
bf3d2cf42b8ffea9f6d9c08b3534f73ae8109b57	Apalache	Cross3	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
4ad758376907af56e72c7a1c6f5c4911bf5ec9b4	Apalache	Cross3	Variable	True	Passed	Model Under Test Equivalent Model
4124bcad2ee9b196b130d41ab73c0a9d7d28dd6e	Apalache	Cross3	Variable	False	Passed	Model Under Test Equivalent Model
1a17d2c8e0e58c0617cdd4888623c9a2f2239c80	Apalache	Cross3	Constant	True	Passed	Model Under Test Equivalent Model
dc630b2de5b4ffc6a3b9e2b6c9e58644b0c8ea49	Apalache	Cross3	Constant	False	Passed	Model Under Test Equivalent Model
f5912d2ab28fad87223afde195baf93fa3a1fbb7	Apalache	Cross3	ConstantRank1	True	Passed	Model Under Test Equivalent Model
7f5d33eda4ceaeaca9c5678122984d8fe0c579ef	Apalache	Cross3	ConstantRank1	False	Passed	Model Under Test Equivalent Model
850233e2f1d61dbfba7d58978b5b1347dd68969c	Apalache	Cross3	Instance	True	Passed	Model Under Test Equivalent Model
98d930489ff717a5cea0195aeeb953826ffa46fb	Apalache	Cross3	Instance	False	Passed	Model Under Test Equivalent Model
3fa90e7a6249ff9fe55d8f525270aea41789bbff	Apalache	Cross3	InstanceWith	True	Passed	Model Under Test Equivalent Model
c3a35c236c121e80e9236ad0e8ea7ff845f04f5f	Apalache	Cross3	InstanceWith	False	Passed	Model Under Test Equivalent Model
67ba8275b4b4f54117d32ce04d345a88d82cca0c	Apalache	Cross3	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3a0c95c7735567d922c08d0ba5394b1ed66ecac6	Apalache	Cross3	InstanceNamed	False	Passed	Model Under Test Equivalent Model
788f400514986243f529880387f4b453b8dfd7b9	Apalache	Cross3	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5084941c75a0b45a8b42f52711aa658281059163	Apalache	Cross3	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
49e9ac503ac1f648a999d202c2422d2dfb5d08fb	Apalache	Cross3	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
09f3438e44112a19a87960a075650586d44f7d26	Apalache	Cross3	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
d38b538a7018cfa2c4bd9eeb59aa7bfab9bd9442	Apalache	Cross3	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
5a828a1b1807831054d9077f9948dc8308b2145b	Apalache	Cross3	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
248862f67f839c0222f2e135b6a519b22eb93fa9	Apalache	Cross3	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
33e02f0bb1b69656145088c5bcae7baa611c1201	Apalache	Cross3	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
042b1ee7ddd715bdcbd61463abba3d0702bd962a	Apalache	Cross3	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
82ecc3bbd9ad48aeed31930f2f49cc9530a561e9	Apalache	Cross3	InstanceNamedWithInFolder	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
e8991ba6e96d383f53ced90789416071310d7147	Apalache	Cross3	Cross3	True	Passed	Model Under Test Equivalent Model
d719ca2f771961dbd34f8f96d7ead412d743ebf6	Apalache	Cross3	Cross3	False	Passed	Model Under Test Equivalent Model
6c79e0af54520fe1fc6fd2ddc755086265119664	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))	Cross3	FunSet	True	Passed	Model Under Test Equivalent Model
13462ab9d40796ee28044e6e4aeeff484e08365c	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))	Cross3	FunSet	False	Passed	Model Under Test Equivalent Model
c58ec3f504deeb0ef1281f8666556dc0cc13c18d	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)	Cross3	RecordSet	True	Passed	Model Under Test Equivalent Model
9bedad3e5d5cb6e1804ee0317d6f1667ecf70f3d	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)	Cross3	RecordSet	False	Passed	Model Under Test Equivalent Model
7235c69ffca445ecffd7b7dcfaddb75d1cebec71	Apalache	Cross3	SetDiff	True	Passed	Model Under Test Equivalent Model
04546a8de4c9dae06b5cab45f99558da9c857bcc	Apalache	Cross3	SetDiff	False	Passed	Model Under Test Equivalent Model
ee9114d94bc6a7f7b7f9ba04cae113b167cd3bca	Apalache	Cross3	SetUnion	True	Passed	Model Under Test Equivalent Model
170d10fe6c1736d651b248b2c2e29093b91d2433	Apalache	Cross3	SetUnion	False	Passed	Model Under Test Equivalent Model
f7c77e5d47bb5003db3e6ba456dad39857d75e7c	Apalache	Cross3	SetIntersect	True	Passed	Model Under Test Equivalent Model
42c097e63fe7708fc3f911bd276c8b7c9d2fc19d	Apalache	Cross3	SetIntersect	False	Passed	Model Under Test Equivalent Model
acd6cb0cd567dd6a31a5e55df87683d99d24d117	Apalache	Cross3	IfCond	True	Passed	Model Under Test Equivalent Model
c8a08a2b40e4f5da710cccfc03b646ba79e13730	Apalache	Cross3	IfCond	False	Passed	Model Under Test Equivalent Model
415810ac62b229c81b7630299940df3ab3aa582e	Apalache	Cross3	IfThen	True	Passed	Model Under Test Equivalent Model
01b3d08d469f63a0fcc4653550d3c5461b94a2d4	Apalache	Cross3	IfThen	False	Passed	Model Under Test Equivalent Model
f48f5cc1cf116d8b8dc045288688881b0f4ab8fc	Apalache	Cross3	IfElse	True	Passed	Model Under Test Equivalent Model
6ce3e2479b96e3536232ea55a69c87df93763949	Apalache	Cross3	IfElse	False	Passed	Model Under Test Equivalent Model
2cc86d609db77278cdbe36bcb5aae004c48a348c	Apalache	Cross3	Subset	True	Passed	Model Under Test Equivalent Model
a8223e6e7ce3ac238df291712db8808e54d48cb3	Apalache	Cross3	Subset	False	Passed	Model Under Test Equivalent Model
2ba8a315702dde1be0e391846a247a0d4caf929d	Apalache	Cross3	Domain	True	Passed	Model Under Test Equivalent Model
2420563bf2744bb0d457ec1312bf162bec67887e	Apalache	Cross3	Domain	False	Passed	Model Under Test Equivalent Model
81ea9baebd6e22c8dcd8be970adabfbf40fdcc8c	Apalache	Cross3	Union	True	Passed	Model Under Test Equivalent Model
45125136f2a67fa587ac79994e04b6fa37b78928	Apalache	Cross3	Union	False	Passed	Model Under Test Equivalent Model
cfe2b5b07b966c28786d10b6dbe3ddfb8eb435ea	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	Cross3	NumRange	True	Passed	Model Under Test Equivalent Model
f1f8f22d99cc7c6c1192a11e62af0e80aa899941	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	Cross3	NumRange	False	Passed	Model Under Test Equivalent Model
c2d7dbd7d25726ac46554326a281cf4190ab354d	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Cross3	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
445e183f22b06f95632b6b2af9a82bd03572f5c4	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Cross3	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
812e07c53b8bfe991b39ce5d29e541f449a1bb58	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Cross3	TlcEval	True	Passed	Model Under Test Equivalent Model
bde23f338b7aac48a3433a540d0bf2b44043b6cd	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Cross3	TlcEval	False	Passed	Model Under Test Equivalent Model
7e8627931caf5946f624867ee2843c1dd828ad79	Apalache	Cross3	BagBagToSet	True	Passed	Model Under Test Equivalent Model
cb95b92d5fefb643fe07be5acd949c0194b9fcc9	Apalache	Cross3	BagBagToSet	False	Passed	Model Under Test Equivalent Model
fd81451d45f66332724091d2ee82fbf782c44cad	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Cross3	BagSubBag	True	Passed	Model Under Test Equivalent Model
1e7641a458418484990d727970d9e80c15544165	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Cross3	BagSubBag	False	Passed	Model Under Test Equivalent Model
447f05781fc360c48e5fee6143f232f3cb4b57b3	Apalache	Cross3	SeqHead	True	Passed	Model Under Test Equivalent Model
e556480a8954fdefdefea093d464fe18f51a3be6	Apalache	Cross3	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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