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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
28c14286d7863ef45f383b5631f6b8c7a3bcec13	Apalache	Eq	Domain	True	Passed	Model Under Test Equivalent Model
2a419ba84623bb9640c6e62d94e679620961a0be	Apalache	Eq	Domain	False	Passed	Model Under Test Equivalent Model
1ce922ec88d72adba97132ffecbfb8bffb61e76a	Apalache	Ne	Domain	True	Passed	Model Under Test Equivalent Model
dc391e0cafbfb78050edbed54b1f187e388ded3c	Apalache	Ne	Domain	False	Passed	Model Under Test Equivalent Model
30158e1b34b749cb2984eea202c10e8a9d2a3285	Apalache	Let	Domain	True	Passed	Model Under Test Equivalent Model
32aa710f43cbb68cf8c4d4b801a3cd871188a2ca	Apalache	Let	Domain	False	Passed	Model Under Test Equivalent Model
d0192b3b4b2927c474fb50e211bd8a1b1dfa371c	Apalache	Set0	Domain	True	Passed	Model Under Test Equivalent Model
df65ef845020bd9da7a8d51fa860c7d745dc121f	Apalache	Set0	Domain	False	Passed	Model Under Test Equivalent Model
1ff2edbbcde463e6a299b64b1a92ca867de315a6	Apalache	Set1	Domain	True	Passed	Model Under Test Equivalent Model
689368371a5b87d3e5763ebf9402ccd31d597cc4	Apalache	Set1	Domain	False	Passed	Model Under Test Equivalent Model
7e64a3fc9c96b3f6863b20ba9ea5faa4c9378d4e	Apalache	Set2	Domain	True	Passed	Model Under Test Equivalent Model
fefc391a8c1618ca551cbcda975d50715e51cd41	Apalache	Set2	Domain	False	Passed	Model Under Test Equivalent Model
17ca1067ca886cc4cce2d6a688da54d30f2823fb	Apalache	Fun	Domain	True	Passed	Model Under Test Equivalent Model
9d4c0f19dc0ebd6aa81c9ed90bd4870f8b006d11	Apalache	Fun	Domain	False	Passed	Model Under Test Equivalent Model
bec563c1b452a050895632ba40b41408dda890ef	Apalache	In	Domain	True	Passed	Model Under Test Equivalent Model
308785cb3b4c38f969981c1e3e023cbef1c89307	Apalache	In	Domain	False	Passed	Model Under Test Equivalent Model
1d11cffdc981a77538d7c43972a6480a1db9e02b	Apalache	NotIn	Domain	True	Passed	Model Under Test Equivalent Model
99b1eb0374be5490ef6de57b7d5e73f36f6c284d	Apalache	NotIn	Domain	False	Passed	Model Under Test Equivalent Model
178badaca50d3d59aa84379825802d90e1f29350	Apalache	Record	Domain	True	Passed	Model Under Test Equivalent Model
945aec7a6e32e265252eef7319cce315d20ae589	Apalache	Record	Domain	False	Passed	Model Under Test Equivalent Model
f3ed111a8d1326e67420c50ca6516cbe6ad5ac52	Apalache	Tuple	Domain	True	Passed	Model Under Test Equivalent Model
bd0bae219c1b4fbd22604d9f2df93c6337d1385f	Apalache	Tuple	Domain	False	Passed	Model Under Test Equivalent Model
cef96115cc95c6afa28a6418da0f5e25e875937e	Apalache	FunApp	Domain	True	Passed	Model Under Test Equivalent Model
20c4cf703d5a31233eecf2fc8f09d81a5fb393fa	Apalache	FunApp	Domain	False	Passed	Model Under Test Equivalent Model
dea4f1e1eba34590923a18abb1c63a88d0e68ddd	Apalache	Except1Fun	Domain	True	Passed	Model Under Test Equivalent Model
f3d3a42620868a2df7bff079e217cff3985e31cd	Apalache	Except1Fun	Domain	False	Passed	Model Under Test Equivalent Model
fd08938b3d2fcb3860f544ec64fa24598cc90b5a	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Domain	True	Passed	Model Under Test Equivalent Model
438db43ae84651514f2418295bf5a1899e4a2c57	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Domain	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
2441fedef58a1aceccf8c39d31c54eabddfc0f81	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Domain	True	Passed	Model Under Test Equivalent Model
2c97eef4c9960fec4a3c55821557fff9b8635867	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Domain	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
ff92bcb8e34b9d497c89f13df8cea226cbd3e108	Apalache	Prime	Domain	True	Passed	Model Under Test Equivalent Model
bacc76631983d7b97114d266237dc3b4de3fd6c5	Apalache	Prime	Domain	False	Passed	Model Under Test Equivalent Model
bb07a9ce08aab5caddbbe3c00770a23cf551a9c3	Apalache	DefFun	Domain	True	Passed	Model Under Test Equivalent Model
e4345fae85f546575dbddff586a6f0e0b6875f0e	Apalache	DefFun	Domain	False	Passed	Model Under Test Equivalent Model
f015d2156759b47b637e2b04d68af55d2fa4a4fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Domain	True	Passed	Model Under Test Equivalent Model
1759fa6dde43831731fb42452b54f19b334a1137	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Domain	False	Passed	Model Under Test Equivalent Model
2066b0b55632f2bf5e66c14be07aba65da7e82d4	Apalache	DefFunRecursive	Domain	True	Passed	Model Under Test Equivalent Model
4f7ae2579572c359283da8f2f3b9e09c6a869f52	Apalache	DefFunRecursive	Domain	False	Passed	Model Under Test Equivalent Model
f863172f48c80e975c8a02736c400ef1193ff7a6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Domain	True	Passed	Model Under Test Equivalent Model
bd38558edd993e6ef5ce830e706947627350ab0e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Domain	False	Passed	Model Under Test Equivalent Model
9cd92a1a98e158e3f2b292d91ca94a06067558ac	Apalache	Def0	Domain	True	Passed	Model Under Test Equivalent Model
aa8ea950ed5ec957c971f5f1c5eb7fc424e65ea3	Apalache	Def0	Domain	False	Passed	Model Under Test Equivalent Model
8ecc21bda8529393926bb019195687199a42c187	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Domain	True	Passed	Model Under Test Equivalent Model
92a538c68b24a62ded630851100ac9315be13d23	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Domain	False	Passed	Model Under Test Equivalent Model
7b92e108538d9287e29f3d493c97ed301c61148d	Apalache	Def1	Domain	True	Passed	Model Under Test Equivalent Model
837c9388994ff8c20956a6f4f1219da64b47b796	Apalache	Def1	Domain	False	Passed	Model Under Test Equivalent Model
1cb05ba7e6beb1c48fae3fa7cbbb3c1f41671f7c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Domain	True	Passed	Model Under Test Equivalent Model
c80e9bd151a52f4d141e255b543843939d61480d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Domain	False	Passed	Model Under Test Equivalent Model
6938e91ae31d69e441ea3ddf085864293faa47ce	Apalache	Def2	Domain	True	Passed	Model Under Test Equivalent Model
f86456e375091ecf8d689d642f95b8ca7d6395ee	Apalache	Def2	Domain	False	Passed	Model Under Test Equivalent Model
7b93cd475f057dc4a9db0d5ad76bf686aec3fb11	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Domain	True	Passed	Model Under Test Equivalent Model
d2a5bcb1f30ef80fdd9db1d311483fd5dcb264fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Domain	False	Passed	Model Under Test Equivalent Model
63b38980542b218032898ffb27e1be81b1906561	Apalache	Def1Recursive	Domain	True	Passed	Model Under Test Equivalent Model
e5e6127489ca52b92d98fd6be8f676e715783e25	Apalache	Def1Recursive	Domain	False	Passed	Model Under Test Equivalent Model
13caea5255d0230fcc3ac37d92467ae421077620	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Domain	True	Passed	Model Under Test Equivalent Model
c919b3362de97a5c35def5f0d87ae60f42568fff	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Domain	False	Passed	Model Under Test Equivalent Model
0bb2149e8465f60010d7f2840d25a7edde1d0d88	Apalache	Extends	Domain	True	Passed	Model Under Test Equivalent Model
14a8b886d46ef85f1c48370bcfca97c31bce7208	Apalache	Extends	Domain	False	Passed	Model Under Test Equivalent Model
180d0227a282f0f90f275151dd076dd9e09e155a	Apalache	ExtendsInDifferentFolder	Domain	True	Passed	Model Under Test Equivalent Model
01a07f3239587c55557d652da34cde7cd63c0d6c	Apalache	ExtendsInDifferentFolder	Domain	False	Passed	Model Under Test Equivalent Model
dce02843cf5000aa7661b3b7ef6af6ce87ede82e	Apalache	Variable	Domain	True	Passed	Model Under Test Equivalent Model
fc6322cec14b452e58909ae13760653a0f8c78d1	Apalache	Variable	Domain	False	Passed	Model Under Test Equivalent Model
bfb9c7e24ed51c8022cc77b886555e235c6d435f	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Domain	True	Passed	Model Under Test Equivalent Model
6206b640815082addba30c850d9da8b1034761cd	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Domain	False	Passed	Model Under Test Equivalent Model
65279afbc1e1be09d22ff753d4afce5a9afc4895	Apalache	Constant	Domain	True	Passed	Model Under Test Equivalent Model
f7d55417b41b07e1352ed8e45cee402845e68fbc	Apalache	Constant	Domain	False	Passed	Model Under Test Equivalent Model
4ce032dcde2cce3adfa9eeb1d6da522a6b47b60e	Apalache	ConstantRank1	Domain	True	Passed	Model Under Test Equivalent Model
f0dd7652d45bf99d7b29eaecead3a711f2788ac8	Apalache	ConstantRank1	Domain	False	Passed	Model Under Test Equivalent Model
3f08e7977b1579a5e0aee3cd175fdbba3ed6153f	Apalache	Instance	Domain	True	Passed	Model Under Test Equivalent Model
4dcb6a149f82e77f4a595644c187310f141ebc3c	Apalache	Instance	Domain	False	Passed	Model Under Test Equivalent Model
6bc8e36637ae32655f5071293e178e514e356cc7	Apalache	InstanceWith	Domain	True	Passed	Model Under Test Equivalent Model
ebb46259b8c1175c08475f7d278bfd52a6ea4de8	Apalache	InstanceWith	Domain	False	Passed	Model Under Test Equivalent Model
b460f588ed9bca69fa8c61bc8a25ab67177359b0	Apalache	InstanceNamed	Domain	True	Passed	Model Under Test Equivalent Model
a9532438b01a7aae05ed19810ef6f8a8a91da1c6	Apalache	InstanceNamed	Domain	False	Passed	Model Under Test Equivalent Model
0d4b183bea392f2948abd464e5a11b97f53b69b1	Apalache	InstanceNamedWith	Domain	True	Passed	Model Under Test Equivalent Model
e4450f2805cfbda869684580a6f18f91b3713597	Apalache	InstanceNamedWith	Domain	False	Passed	Model Under Test Equivalent Model
30c304b8cb4370a4f8fd360971e13cbd0bf94485	Apalache	InstanceInFolder	Domain	True	Passed	Model Under Test Equivalent Model
d1da00e40babfb61ff82d5da65482becc5a4e026	Apalache	InstanceInFolder	Domain	False	Passed	Model Under Test Equivalent Model
cfaf30d502b77fb0f22e274ababef38999bad201	Apalache	InstanceWithInFolder	Domain	True	Passed	Model Under Test Equivalent Model
3b9ba2ebce367996519fe30559e526f3205b87bb	Apalache	InstanceWithInFolder	Domain	False	Passed	Model Under Test Equivalent Model
8332a8235e3e64b275c368c474684a222f09b39b	Apalache	InstanceNamedInFolder	Domain	True	Passed	Model Under Test Equivalent Model
a41048b14483e0b5414fe8a466a53ab715002f93	Apalache	InstanceNamedInFolder	Domain	False	Passed	Model Under Test Equivalent Model
c7e881bb198ef0a5c204a17d2bad5d52c0d3d5c1	Apalache	InstanceNamedWithInFolder	Domain	True	Passed	Model Under Test Equivalent Model
bf89382248bc8e06d617561c9100987f83f09c50	Apalache	InstanceNamedWithInFolder	Domain	False	Passed	Model Under Test Equivalent Model
a1a941f533080657135a40448b5de865d7d64165	Apalache	Lambda	Domain	True	Passed	Model Under Test Equivalent Model
e2f4f79bee5c04415b74fd793f750f12adc1a400	Apalache	Lambda	Domain	False	Passed	Model Under Test Equivalent Model
477f5cf0eb6ee210519e7ba66d117e9d723761c1	Apalache	Cross2	Domain	True	Passed	Model Under Test Equivalent Model
794fa85fa9638715ec3655f00eb0fafe1c88c153	Apalache	Cross2	Domain	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
7889a78dcb54167f354b6752d017dceb4c39f321	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	Domain	True	Passed	Model Under Test Equivalent Model
bf7c78c9ba6587cb26b3f0aa066c0456cb2960e2	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	Domain	False	Passed	Model Under Test Equivalent Model
521f4e36a997d035381c50bf794b9ba7cfe4b5ed	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	Domain	True	Passed	Model Under Test Equivalent Model
a4f99c6ce584c3dc4b9fdbd689cf4fb38f3f9e93	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	Domain	False	Passed	Model Under Test Equivalent Model
38819ad0219940f4532aed003d03832847e7d2e9	Apalache	SetDiff	Domain	True	Passed	Model Under Test Equivalent Model
2b7640c187cb3eec3606292e612da1c4c4753d08	Apalache	SetDiff	Domain	False	Passed	Model Under Test Equivalent Model
37529111b394a8ca04bb2338bcd0b0b121e450df	Apalache	SetUnion	Domain	True	Passed	Model Under Test Equivalent Model
3cf6ac93cbd1bdcaccdbbbf2964ceb20d3fce6fc	Apalache	SetUnion	Domain	False	Passed	Model Under Test Equivalent Model
277d435c2a12a7e4bf32030fa37df477faa8f638	Apalache	SetIntersect	Domain	True	Passed	Model Under Test Equivalent Model
e69d0be771ebde16f3bcef67e4798273ff8a03d7	Apalache	SetIntersect	Domain	False	Passed	Model Under Test Equivalent Model
e7b74da05d907a05abe31980b8af26873cdd74de	Apalache	SubsetEq	Domain	True	Passed	Model Under Test Equivalent Model
9b7280586fd480dd0160110f945164e3c060aa71	Apalache	SubsetEq	Domain	False	Passed	Model Under Test Equivalent Model
ffbda22dc1d1d8a5bc15786ff682e3d75990fac4	Apalache	IfThen	Domain	True	Passed	Model Under Test Equivalent Model
386f24529c31b2545e972f92a218cf2cba1a63c8	Apalache	IfThen	Domain	False	Passed	Model Under Test Equivalent Model
684d128ea937a875f870ccdd543039241068e538	Apalache	IfElse	Domain	True	Passed	Model Under Test Equivalent Model
6d7cea976dd13b94fbd1484f8748b80fca3b53c5	Apalache	IfElse	Domain	False	Passed	Model Under Test Equivalent Model
9aac4c2bdf05bc36ef979865a3128fa5ba2c2591	Apalache	Subset	Domain	True	Passed	Model Under Test Equivalent Model
c0be6f023414a7ae2d9036ac8095794c44f70097	Apalache	Subset	Domain	False	Passed	Model Under Test Equivalent Model
cd96adcc1acb43463a75813b11f9a5dad8020e18	Apalache	Union	Domain	True	Passed	Model Under Test Equivalent Model
1ebe17190d44f404566cea43d71daaf91f7f0ecc	Apalache	Union	Domain	False	Passed	Model Under Test Equivalent Model
4b48970a3bf447cf9d889b092a9aae95900a4360	Apalache	Unchanged	Domain	True	Passed	Model Under Test Equivalent Model
5f222c49307290dedbc4a4e2778d8d2d7a058a67	Apalache	Unchanged	Domain	False	Passed	Model Under Test Equivalent Model
3a64ad467a95389db49fda5e51a2aa4b7ab30c2b	Apalache	SeqSeq	Domain	True	Passed	Model Under Test Equivalent Model
fd934c0a2b54321bf22be7bc5cc7337e8cea76e4	Apalache	SeqSeq	Domain	False	Passed	Model Under Test Equivalent Model
2848add887442d497f249cceedf3b33b26535fcb	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Domain	True	Passed	Model Under Test Equivalent Model
0a352e865a2944591b6b57c781027dafb65f0910	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Domain	False	Passed	Model Under Test Equivalent Model
6322c0562b8dc31a5b00c550ba9c775d65668949	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Domain	True	Passed	Model Under Test Equivalent Model
b9bda0f0fd8d8c5df85a028253b21f4b42fc41ce	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Domain	False	Passed	Model Under Test Equivalent Model
62edd618da1becc4819246d9ff6a982da2a2a4f8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Domain	True	Passed	Model Under Test Equivalent Model
c081d2c8a5a4daf0a5ff793ae2c267e047726f34	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Domain	False	Passed	Model Under Test Equivalent Model
d6f6de1ff0e4ecdad2c2e7c8d975ab50958a176d	Apalache	BagSetToBag	Domain	True	Passed	Model Under Test Equivalent Model
886a55c1040b80be8491008bed7ef8a913774f2a	Apalache	BagSetToBag	Domain	False	Passed	Model Under Test Equivalent Model
e1512d4ae9c46a3bbc91e903c1c157dbb7ad6bad	Apalache	BagBagIn	Domain	True	Passed	Model Under Test Equivalent Model
8080925e08c9fa5bfd182a953fc2eaba4a0cadbc	Apalache	BagBagIn	Domain	False	Passed	Model Under Test Equivalent Model
158e1bb9298e8aca03107539c6e447ab6eee8779	Apalache	BagCopiesIn	Domain	True	Passed	Model Under Test Equivalent Model
c627d3091c15abd341b43da003cc590353d93e7a	Apalache	BagCopiesIn	Domain	False	Passed	Model Under Test Equivalent Model
8d981e923e046602eac9e9573da0f12a8c071931	Apalache	BagBagUnion	Domain	True	Passed	Model Under Test Equivalent Model
d875314d96184ebdef9a5bb1443ab6306314197e	Apalache	BagBagUnion	Domain	False	Passed	Model Under Test Equivalent Model
d9ecd9f50450fafb80ab3944550a5b3af8509cac	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	Domain	True	Passed	Model Under Test Equivalent Model
f481f47354061e47cc38f9d6a5f7e513b67589bb	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	Domain	False	Passed	Model Under Test Equivalent Model
b74a0ad2d4f91f05446422e02f14df2a8fcc4495	Apalache	FiniteSetsCardinality	Domain	True	Passed	Model Under Test Equivalent Model
bbd08a53f703d05519cf2dbfff6c0e5a750894ac	Apalache	FiniteSetsCardinality	Domain	False	Passed	Model Under Test Equivalent Model
612ef64f6e11fcaae61698293db0eb3ecdb89332	Apalache	SeqAppend	Domain	True	Passed	Model Under Test Equivalent Model
ca4ea3ec42b35c1adc0b80154c123c11e482ac08	Apalache	SeqAppend	Domain	False	Passed	Model Under Test Equivalent Model

Index

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