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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
df69300fa5267f051d07c7331a11b2cfb04be50c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	FiniteSetsCardinality	OneLineComment	True	Passed	Model Under Test Equivalent Model
2422c558661b1ec6c8bde063b403eb255f0a2531	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	FiniteSetsCardinality	OneLineComment	False	Passed	Model Under Test Equivalent Model
6d22b774eb1c10c7aa134e4a39698431c841ff8c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	FiniteSetsCardinality	MultiLineComment	True	Passed	Model Under Test Equivalent Model
3c9184dfce4ad2791210a168f3305362a1af78cd	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	FiniteSetsCardinality	MultiLineComment	False	Passed	Model Under Test Equivalent Model
2dbaad9e2a1728dd50cd9ac7b36ada905dbc0ea5	Apalache	FiniteSetsCardinality	BoolSet	True	Passed	Model Under Test Equivalent Model
0188b51bfdfaa7a8f0dda3bfcb236f42d7276f16	Apalache	FiniteSetsCardinality	BoolSet	False	Passed	Model Under Test Equivalent Model
9f0af8c71778d9933edad9c6b2d360b151c7794d	Apalache	FiniteSetsCardinality	Let	True	Passed	Model Under Test Equivalent Model
39db5ee4ee4789cd932b08e4292f5fdd9ce0313e	Apalache	FiniteSetsCardinality	Let	False	Passed	Model Under Test Equivalent Model
351718d5c706ae72bb4d566c2b1f239405b27dfc	Apalache	FiniteSetsCardinality	SetEmpty	True	Passed	Model Under Test Equivalent Model
32a1c4913917a939446558194cab7db6abac7cc6	Apalache	FiniteSetsCardinality	SetEmpty	False	Passed	Model Under Test Equivalent Model
2f9dc7282e611192a5b895b85902a15321eb780e	Apalache	FiniteSetsCardinality	Set0	True	Passed	Model Under Test Equivalent Model
18b8d8adcc61fbc1c349d2f43e5068e669ede0a8	Apalache	FiniteSetsCardinality	Set0	False	Passed	Model Under Test Equivalent Model
c4b6a63875659ca6983e65cdda29233cb2403a1b	Apalache	FiniteSetsCardinality	Set1	True	Passed	Model Under Test Equivalent Model
cd4000fa7fadc352f1ecddfe328229563e22ca63	Apalache	FiniteSetsCardinality	Set1	False	Passed	Model Under Test Equivalent Model
6865e03554998a943227589283839b241a09befc	Apalache	FiniteSetsCardinality	Set2	True	Passed	Model Under Test Equivalent Model
59b1989ba548b10aaed4b61190296837a6550d09	Apalache	FiniteSetsCardinality	Set2	False	Passed	Model Under Test Equivalent Model
0ca3f4b0753b9f0ba7d727f4e53d27d1e20c846c	Apalache	FiniteSetsCardinality	Choose	True	Passed	Model Under Test Equivalent Model
9ab3e539c012217fa20df97f44d45f86cc6ea63f	Apalache	FiniteSetsCardinality	Choose	False	Passed	Model Under Test Equivalent Model
4383172109379fff727555eea72c6090df62385e	Apalache	FiniteSetsCardinality	FunApp	True	Passed	Model Under Test Equivalent Model
38e8fff75cd8009ad5dd2754e324591c18a49b27	Apalache	FiniteSetsCardinality	FunApp	False	Passed	Model Under Test Equivalent Model
a2335d94f64d86b93c269dd8303100433705c7ff	Apalache	FiniteSetsCardinality	Prime	True	Passed	Model Under Test Equivalent Model
4fd5c7eaa56988d4fa7dafb4571ffd3eeff52365	Apalache	FiniteSetsCardinality	Prime	False	Passed	Model Under Test Equivalent Model
8e7f98bc6d23b8577db5e05966d5020d7117a1f8	Apalache	FiniteSetsCardinality	Def0	True	Passed	Model Under Test Equivalent Model
36d6bc035e7fff1553862134e2408a372fb7d7ee	Apalache	FiniteSetsCardinality	Def0	False	Passed	Model Under Test Equivalent Model
6d0da67d01725514e0a1e2ef4f988df2634d56f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef0	True	Passed	Model Under Test Equivalent Model
fd0ab26042f150ebf5e4754fe8274ce0fe6a4048	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef0	False	Passed	Model Under Test Equivalent Model
44dc7504cc8fbf1e458f265fabf4ae851c03fc28	Apalache	FiniteSetsCardinality	Def1	True	Passed	Model Under Test Equivalent Model
0feb05c57af597ae17104a87310cf5ab10ba18d9	Apalache	FiniteSetsCardinality	Def1	False	Passed	Model Under Test Equivalent Model
bb8b7228fb7c1d7accfb6c0ec15b39f4e3d11f07	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1	True	Passed	Model Under Test Equivalent Model
4b5d1fb036fcc9ce33bb4ca40a8893b67191cf7b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1	False	Passed	Model Under Test Equivalent Model
f77f8d552df19db0c3497e817568ffc1d7105b30	Apalache	FiniteSetsCardinality	Def2	True	Passed	Model Under Test Equivalent Model
d1d91d8816935689798cc04622d8c71a3671b1c6	Apalache	FiniteSetsCardinality	Def2	False	Passed	Model Under Test Equivalent Model
895bf62bbdf872cc874e0984b61568695fe3e442	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef2	True	Passed	Model Under Test Equivalent Model
1d5c107a7ad0260407f04ab5353a3d4ab7bbea37	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef2	False	Passed	Model Under Test Equivalent Model
6e30a0296d377f209ff335bbb558390e9bbc6798	Apalache	FiniteSetsCardinality	Def1Recursive	True	Passed	Model Under Test Equivalent Model
08fc88bfa8034d1ed63dd12cafe80dca43f2aabd	Apalache	FiniteSetsCardinality	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e3ac479f2312c2efa2e95a2c03f394cf0bce2ac8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
74ead8a37cf4453f70d125d21a68c31b51966d98	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
4053c7ecddc80f794079e80c2187476dbed9b9bb	Apalache	FiniteSetsCardinality	Extends	True	Passed	Model Under Test Equivalent Model
07205014ae306ad63a8da0742346c619ec05a170	Apalache	FiniteSetsCardinality	Extends	False	Passed	Model Under Test Equivalent Model
e0aa14704aba3628dbf6282dbabe96d9729819aa	Apalache	FiniteSetsCardinality	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
883963eab7d9814a35569c6ed8844362221ae03c	Apalache	FiniteSetsCardinality	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
3c5e59ba9c0ecf46c3996c5d1ad3e897769f532f	Apalache	FiniteSetsCardinality	Variable	True	Passed	Model Under Test Equivalent Model
dea8f780f7c748d51b07f89fe08ca80477655c11	Apalache	FiniteSetsCardinality	Variable	False	Passed	Model Under Test Equivalent Model
2d51080a43ebb1c1ec32ee99a0abd9efc5d26ae2	Apalache	FiniteSetsCardinality	Constant	True	Passed	Model Under Test Equivalent Model
c71b3f2ef3d8ddf3f7f386adb55bc9495d2b7633	Apalache	FiniteSetsCardinality	Constant	False	Passed	Model Under Test Equivalent Model
afb9703ab9937044f16eb1089d5e0832230a75b8	Apalache	FiniteSetsCardinality	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2fdd0cfda9c5e9b60b2d581586fa5db9b629b64a	Apalache	FiniteSetsCardinality	ConstantRank1	False	Passed	Model Under Test Equivalent Model
cd1d036d8cc6b3c83938f1102cd3879b71fa0ea1	Apalache	FiniteSetsCardinality	Instance	True	Passed	Model Under Test Equivalent Model
b4f9dece36ed057abf61962ab022ea2cb5bb5127	Apalache	FiniteSetsCardinality	Instance	False	Passed	Model Under Test Equivalent Model
06060e4a75fed3356bc3f6275cdaddcc271695fd	Apalache	FiniteSetsCardinality	InstanceWith	True	Passed	Model Under Test Equivalent Model
a54e7557d259c513ca44a6d7043afb2bde41fe50	Apalache	FiniteSetsCardinality	InstanceWith	False	Passed	Model Under Test Equivalent Model
b3f27fb19b7c254a2e03cb01d757924b81742cdb	Apalache	FiniteSetsCardinality	InstanceNamed	True	Passed	Model Under Test Equivalent Model
cf8ed92457c0f24360463ffe71b654aa64efcb96	Apalache	FiniteSetsCardinality	InstanceNamed	False	Passed	Model Under Test Equivalent Model
8e0fde4cc78a6e3e6cae2607c64a129b146d32f8	Apalache	FiniteSetsCardinality	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
4c2484c4649848443df8b5cc90eb9c1f8eebfab1	Apalache	FiniteSetsCardinality	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
769d02bf73e12fbef72d28813d83f85500a0e18d	Apalache	FiniteSetsCardinality	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
412fbe564a83b26282b85c62287eca522f38c70e	Apalache	FiniteSetsCardinality	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
ed28556fa3138cbe3f86ffe1662cc3a5ca58e85e	Apalache	FiniteSetsCardinality	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
b6e611c6eb46a973de3ae7974e54d8c585ec987f	Apalache	FiniteSetsCardinality	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
9c2c7ce5bbaf2facb8da2d0b9263ce1e01ff4dec	Apalache	FiniteSetsCardinality	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
17d6937a8d334269379c287913ff7d929634bc1b	Apalache	FiniteSetsCardinality	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
5c9a25cce09da582a32bf1f441f6c769e74c2922	Apalache	FiniteSetsCardinality	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
82168db365758a032a722276e9b66a1dbfbebf62	Apalache	FiniteSetsCardinality	InstanceNamedWithInFolder	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
698f8c40e6820f31eebb0cac77daf5e22cb07824	Apalache	FiniteSetsCardinality	Cross3	True	Passed	Model Under Test Equivalent Model
1b4f36e9af185896d252bbf78e6c26b12ca5d069	Apalache	FiniteSetsCardinality	Cross3	False	Passed	Model Under Test Equivalent Model
123a9bd70e71da8dcf0364d5df2626988b5812ee	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))	FiniteSetsCardinality	FunSet	True	Passed	Model Under Test Equivalent Model
8fc6eb04e739bb389d38516a08ca60dbb1e2d2f9	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))	FiniteSetsCardinality	FunSet	False	Passed	Model Under Test Equivalent Model
62aaf27b0f3de3b51139c4c34847c2431029242e	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)	FiniteSetsCardinality	RecordSet	True	Passed	Model Under Test Equivalent Model
4b44149533d2b767e40fd564641eb3edcb90c321	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)	FiniteSetsCardinality	RecordSet	False	Passed	Model Under Test Equivalent Model
02f89e63461f05954ed55e142db6e85bda3058fc	Apalache	FiniteSetsCardinality	SetDiff	True	Passed	Model Under Test Equivalent Model
86af6923773a317d40e061edf835fabfefccdddd	Apalache	FiniteSetsCardinality	SetDiff	False	Passed	Model Under Test Equivalent Model
a2ac0613b33b0a22de6d6f087350609f8e7173da	Apalache	FiniteSetsCardinality	SetUnion	True	Passed	Model Under Test Equivalent Model
3d928566c481448ca6f7c6bc9a63627b525cb54e	Apalache	FiniteSetsCardinality	SetUnion	False	Passed	Model Under Test Equivalent Model
b3c7a6e4696bc3141358af4fa8efd755155a1ea8	Apalache	FiniteSetsCardinality	SetIntersect	True	Passed	Model Under Test Equivalent Model
ccfe8c1d36f495c19e5cf2eb664661e605c05430	Apalache	FiniteSetsCardinality	SetIntersect	False	Passed	Model Under Test Equivalent Model
4218054b73e9b778c75507ede6afb750427dfafe	Apalache	FiniteSetsCardinality	IfCond	True	Passed	Model Under Test Equivalent Model
9505dca16961caa88ec3aed227e62c4ebcd63817	Apalache	FiniteSetsCardinality	IfCond	False	Passed	Model Under Test Equivalent Model
18f524b764ce85f1c3df9f17d389cabfe5721d27	Apalache	FiniteSetsCardinality	IfThen	True	Passed	Model Under Test Equivalent Model
0eb0cf2d956dbf8e81566a9ede677d0b74cd0b6b	Apalache	FiniteSetsCardinality	IfThen	False	Passed	Model Under Test Equivalent Model
4e90a6ac44e47b7923308f135c99831db477d5a7	Apalache	FiniteSetsCardinality	IfElse	True	Passed	Model Under Test Equivalent Model
1199cab74f1718eedc744b83ac102628bf2a0ea5	Apalache	FiniteSetsCardinality	IfElse	False	Passed	Model Under Test Equivalent Model
bfc2ca3d0cb9d48779d7b4a45786e66b2c8a9d9a	Apalache	FiniteSetsCardinality	Subset	True	Passed	Model Under Test Equivalent Model
061b789b1147b4b81feebffb21c6341cc64a378e	Apalache	FiniteSetsCardinality	Subset	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
bfe3668e4d13fe21ed56a2019d59820e601fa5a0	Apalache	FiniteSetsCardinality	Union	True	Passed	Model Under Test Equivalent Model
b5fdf06b6cfcd7ff96309a0677f5350e41ccf670	Apalache	FiniteSetsCardinality	Union	False	Passed	Model Under Test Equivalent Model
8447f58ebacb38155d6d76093eb57786a0cd1ed7	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	FiniteSetsCardinality	NumRange	True	Passed	Model Under Test Equivalent Model
e78a902f084db59418560b535c8e8221d60b9c90	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	FiniteSetsCardinality	NumRange	False	Passed	Model Under Test Equivalent Model
7ad4a59d16a764e04c5b70bbfdfe4a428c0c8fd0	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	FiniteSetsCardinality	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
7bd472e340af2b1ac1ee2aede2ae977018e1e0ff	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	FiniteSetsCardinality	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
d292afa17d98c107a43603a893d080ce2ed1d70b	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	FiniteSetsCardinality	TlcEval	True	Passed	Model Under Test Equivalent Model
543e7a4ed40813773f4c670254e838761af2bc75	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	FiniteSetsCardinality	TlcEval	False	Passed	Model Under Test Equivalent Model
1f24178b2e6b898729a83df6cb7fae5d085f726a	Apalache	FiniteSetsCardinality	BagBagToSet	True	Passed	Model Under Test Equivalent Model
295194f49f16839ebf544b4d6a67f64205af139a	Apalache	FiniteSetsCardinality	BagBagToSet	False	Passed	Model Under Test Equivalent Model
72cd902ac2ed5f8eb64f74705c41ae5dac5e2a50	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	FiniteSetsCardinality	BagSubBag	True	Passed	Model Under Test Equivalent Model
8880666897944bea4499891c7f843073d2c97601	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	FiniteSetsCardinality	BagSubBag	False	Passed	Model Under Test Equivalent Model
7658647f8953a11414e2cd9655f83968abe314ed	Apalache	FiniteSetsCardinality	SeqHead	True	Passed	Model Under Test Equivalent Model
f786b7c02f4bbe3e7689ef59792189317103feb5	Apalache	FiniteSetsCardinality	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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