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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
ad3db75a71571f86214250b11e81c991ccea5761	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross2	OneLineComment	True	Passed	Model Under Test Equivalent Model
5924c84b68d7644e55e3e261cea96f59fed2307b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross2	OneLineComment	False	Passed	Model Under Test Equivalent Model
3dca2b5ff818ef3afa1ca41a2e6de879cf2f9c31	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross2	MultiLineComment	True	Passed	Model Under Test Equivalent Model
31e5323d9cdb246646ed6014b787199e0772fe96	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Cross2	MultiLineComment	False	Passed	Model Under Test Equivalent Model
b2f1014d13224d761556e01cc052c61bb7b808f6	Apalache	Cross2	BoolSet	True	Passed	Model Under Test Equivalent Model
7d287f1edf058ccb38702186f2013536f80c90fd	Apalache	Cross2	BoolSet	False	Passed	Model Under Test Equivalent Model
412cde423e6452b037febc099a89486a02c2ae80	Apalache	Cross2	Let	True	Passed	Model Under Test Equivalent Model
fc8319732e1b214b93a705de1fa72ea0c35e3a99	Apalache	Cross2	Let	False	Passed	Model Under Test Equivalent Model
5925fdb7e8e9731ef5739685ae875d444b6b5a9f	Apalache	Cross2	SetEmpty	True	Passed	Model Under Test Equivalent Model
d563a53f1a0fed8cc90f1155f2e336484807e9bb	Apalache	Cross2	SetEmpty	False	Passed	Model Under Test Equivalent Model
060d17e968e35e68a41bb80760fea03b69780273	Apalache	Cross2	Set0	True	Passed	Model Under Test Equivalent Model
7cef224664596db717b3d40a0eca5f102931677d	Apalache	Cross2	Set0	False	Passed	Model Under Test Equivalent Model
8d732a1a10be322268ffcd98e6a695a72bd2bebc	Apalache	Cross2	Set1	True	Passed	Model Under Test Equivalent Model
af9857f4975232709ef6900af5bb1a4b5de6bb89	Apalache	Cross2	Set1	False	Passed	Model Under Test Equivalent Model
85d648d3ef42225dee2419b2330e07d2170a626e	Apalache	Cross2	Set2	True	Passed	Model Under Test Equivalent Model
0a2b8133e1e9192ae03abf84ebe9854ff263d605	Apalache	Cross2	Set2	False	Passed	Model Under Test Equivalent Model
1e6c3f45d8431a91cef4a8c2f6e2c66000d9253e	Apalache	Cross2	Choose	True	Passed	Model Under Test Equivalent Model
b44d9e90771fd09f60ab35a5f3d2229238716aea	Apalache	Cross2	Choose	False	Passed	Model Under Test Equivalent Model
fdfa418691a20e5c656af2925596b20e5cdce8f0	Apalache	Cross2	FunApp	True	Passed	Model Under Test Equivalent Model
82129ce4035cab735eb5ed5bdd53eba66a6f6e62	Apalache	Cross2	FunApp	False	Passed	Model Under Test Equivalent Model
c529d9531b1df4e102ee7ee207e9ce93395d30a2	Apalache	Cross2	Prime	True	Passed	Model Under Test Equivalent Model
b28765ca1b7b57fd1635c13c3fcb1f8c355bb92f	Apalache	Cross2	Prime	False	Passed	Model Under Test Equivalent Model
c9da08f043dacaa4889e0735d94b52135012c413	Apalache	Cross2	Def0	True	Passed	Model Under Test Equivalent Model
b201c47caa43f3e217a72c779c03e4c0ad57a60a	Apalache	Cross2	Def0	False	Passed	Model Under Test Equivalent Model
1b444e9e63ca0ed6493929688da2bbc7ddd4758e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef0	True	Passed	Model Under Test Equivalent Model
8d7da18b66497590c1a14af59ca6f950cd27057f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef0	False	Passed	Model Under Test Equivalent Model
8eb26e92a5ab4a8f950627c4e9618ce980d91455	Apalache	Cross2	Def1	True	Passed	Model Under Test Equivalent Model
f056e7d48d00f09cd3375c96aa595c3f9ab40f16	Apalache	Cross2	Def1	False	Passed	Model Under Test Equivalent Model
a83e230f49ed943588f0f606d6cbb1258a1c04bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1	True	Passed	Model Under Test Equivalent Model
d750e9bb675c702a405c97c1bb58e63edf027f13	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1	False	Passed	Model Under Test Equivalent Model
23a25efae439db8bbfe2762d91971020b3f61a81	Apalache	Cross2	Def2	True	Passed	Model Under Test Equivalent Model
1e85842e19e658c00a3413a0c709beb38c7bd386	Apalache	Cross2	Def2	False	Passed	Model Under Test Equivalent Model
f979b94c12819dc05e4fc901c92b694ccfaeab91	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef2	True	Passed	Model Under Test Equivalent Model
575ec76e31f9ec80b42c361567bceca62e39a903	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef2	False	Passed	Model Under Test Equivalent Model
3635b9f401e6e54882784c1334b1d155bbc971c2	Apalache	Cross2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c0e730ebc0e8d93cc509aaa1813b3278ea4e4a08	Apalache	Cross2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
2556daccd305ef712e0242d684526c86da87b0e8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
fe214b7c9e083196989efedd9b34d342c28db05f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
01ffeb41a587aa3f80262c44d115e3d1369b8baa	Apalache	Cross2	Extends	True	Passed	Model Under Test Equivalent Model
7fd8ce2931f449086cb8eb06da5099f0995ce069	Apalache	Cross2	Extends	False	Passed	Model Under Test Equivalent Model
126e88d97ff134a6d690dc322077cf9f962f9295	Apalache	Cross2	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
0f42dda5077937c4845fb56f52171fa9e702ade2	Apalache	Cross2	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
2b141afc1818e0a064790e948945172a42835c07	Apalache	Cross2	Variable	True	Passed	Model Under Test Equivalent Model
4948d17093087b7a5923b3c99d651eaa7303ebe3	Apalache	Cross2	Variable	False	Passed	Model Under Test Equivalent Model
385e7c25d438531edd8279a6c22330e12dff1e07	Apalache	Cross2	Constant	True	Passed	Model Under Test Equivalent Model
e2d6949b3275346c84d2170ccc85c1ffb1b7f256	Apalache	Cross2	Constant	False	Passed	Model Under Test Equivalent Model
426ec8df2f3291a35e2800f084325489a0a16313	Apalache	Cross2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
16ba6561695a5c3a0be3441f5607fefa91d623eb	Apalache	Cross2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
381418dcc0bc8420a1a8f319a501a3ab2f1dcf4d	Apalache	Cross2	Instance	True	Passed	Model Under Test Equivalent Model
0b4e55f1abe533473d90ab4d774a99c643089c72	Apalache	Cross2	Instance	False	Passed	Model Under Test Equivalent Model
e9a68032e446dde38672a2005bd9695e3e1a1c11	Apalache	Cross2	InstanceWith	True	Passed	Model Under Test Equivalent Model
3aff98a7c84af42578a81f12f483db47de542d6f	Apalache	Cross2	InstanceWith	False	Passed	Model Under Test Equivalent Model
ba4b9bd98ac67640d9ab23a653b661ccba7801ee	Apalache	Cross2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d9f245b61785fda80e081a0b8c70f12abfe88c55	Apalache	Cross2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
237c7df2e8ed68c7561a9b254f931ec4d893a98e	Apalache	Cross2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
ea8f087ca656c8fe2b6d94d7a5537265b748b0dd	Apalache	Cross2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8bbfc0029be83bd8cc26fc713782699fb36721f4	Apalache	Cross2	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
c78605d9e56e837968b5edad00058a9071f223c0	Apalache	Cross2	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
cb9090679fec0719d3d7946bc39d6255c629a6e1	Apalache	Cross2	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
03eeae84adeef13b0cbb6f0db99105a6f7ff3294	Apalache	Cross2	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
126b467d946c3528e2f7df2ad95b2bc336adacd0	Apalache	Cross2	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
14f858bfbdf4d369182ebc226b611299cb980d92	Apalache	Cross2	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
ae2ae7277f82b3dd12fa702a5191b30d2f7ccb42	Apalache	Cross2	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
831de61374e4c507bd073d37dd4b5c270ba9731b	Apalache	Cross2	InstanceNamedWithInFolder	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
b2a9d78fa20b244f54a1335b9d7bd3b87e3741c4	Apalache	Cross2	Cross3	True	Passed	Model Under Test Equivalent Model
4aa26f110c24ff84c5f2a77a3b0eead7f678a16d	Apalache	Cross2	Cross3	False	Passed	Model Under Test Equivalent Model
4d6831ce4634b63e62dce6513cb68e8b00fe2e72	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))	Cross2	FunSet	True	Passed	Model Under Test Equivalent Model
da6230c22e5d033ff99c214dc1d094194d9233bf	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))	Cross2	FunSet	False	Passed	Model Under Test Equivalent Model
a88edabdaa96b40451a8ae271e6c0f38c97cf63a	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)	Cross2	RecordSet	True	Passed	Model Under Test Equivalent Model
85293edf1b37c747d249f6f2525614e5a00b0e25	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)	Cross2	RecordSet	False	Passed	Model Under Test Equivalent Model
75663e937508b58b29cd29a1f6bea58309db17d8	Apalache	Cross2	SetDiff	True	Passed	Model Under Test Equivalent Model
6a5e6b3fdf9a878e2ef5f2231d0090566df548cf	Apalache	Cross2	SetDiff	False	Passed	Model Under Test Equivalent Model
f335d2e8469d11d3aae9c23790316d9f522e1ac9	Apalache	Cross2	SetUnion	True	Passed	Model Under Test Equivalent Model
e41a9e16c100c41252fed05a674ffad33f0b9ae9	Apalache	Cross2	SetUnion	False	Passed	Model Under Test Equivalent Model
c964df57912592e6ce40028adc4bbe537d05cb43	Apalache	Cross2	SetIntersect	True	Passed	Model Under Test Equivalent Model
60289c13f7eb9a531943c0caeecd341a4cb6d84f	Apalache	Cross2	SetIntersect	False	Passed	Model Under Test Equivalent Model
4f99a4cf4453e177a96848d4a5ed6ab5615ad688	Apalache	Cross2	IfCond	True	Passed	Model Under Test Equivalent Model
7be54e29d2fbad200709a341c20a4533821b5072	Apalache	Cross2	IfCond	False	Passed	Model Under Test Equivalent Model
a1649550413514bac13d24f81f180a6943ab8a16	Apalache	Cross2	IfThen	True	Passed	Model Under Test Equivalent Model
c30f66efe940b1a3175542db506ca9ee20c40d3b	Apalache	Cross2	IfThen	False	Passed	Model Under Test Equivalent Model
2a0c4beb3cc93e981c5c70dc7011777bc69377b5	Apalache	Cross2	IfElse	True	Passed	Model Under Test Equivalent Model
c888d56a4267470039e3f817f108f3b085a0b341	Apalache	Cross2	IfElse	False	Passed	Model Under Test Equivalent Model
ec8d4ebb11d7fef58cdc76680004062a08af5496	Apalache	Cross2	Subset	True	Passed	Model Under Test Equivalent Model
5079c11dae9a9ee5bec835ede4ad2a46f7d02b5b	Apalache	Cross2	Subset	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
fff35579ebb3af14d417e644328fcaa56ed56519	Apalache	Cross2	Union	True	Passed	Model Under Test Equivalent Model
b54fe0157aaff00138bd9e56a66ce98e32423d1c	Apalache	Cross2	Union	False	Passed	Model Under Test Equivalent Model
7a929eadb1e49169e8c488bd4120db4018fed3df	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	Cross2	NumRange	True	Passed	Model Under Test Equivalent Model
0df9dbe41dff6aa87f0a162509953a3a0329b43e	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	Cross2	NumRange	False	Passed	Model Under Test Equivalent Model
2bbc9f58fea2d7025ca2924d5d1f4f55aa9842b6	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Cross2	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
39661daaf0dfb0b22c87401cc1395df9a6346756	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Cross2	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
0d4cf12a2914b4da72f38f197ae507f44a1c21cd	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Cross2	TlcEval	True	Passed	Model Under Test Equivalent Model
413e9c0dadadfc8c2b7cfd9919192aba3f41e5a9	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Cross2	TlcEval	False	Passed	Model Under Test Equivalent Model
328051c68648e70dfe0b36654112b497e3dadc29	Apalache	Cross2	BagBagToSet	True	Passed	Model Under Test Equivalent Model
d58770a08e954b35a436e0c0a03f28db0f7a2866	Apalache	Cross2	BagBagToSet	False	Passed	Model Under Test Equivalent Model
871c51f7c47fcfba992f7164d15565f65b445f63	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Cross2	BagSubBag	True	Passed	Model Under Test Equivalent Model
a8a584c8bc6a1b6a61d5bbf5e1f0a19acca1761d	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Cross2	BagSubBag	False	Passed	Model Under Test Equivalent Model
720b73c889abb15182955928917752ec720bfe39	Apalache	Cross2	SeqHead	True	Passed	Model Under Test Equivalent Model
7db5afd3a0ccbfa401abd82dba5998ab4cf46730	Apalache	Cross2	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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