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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b11e34ce74ce9c105697a60df2d8f053e2de3a31	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetUnion	OneLineComment	True	Passed	Model Under Test Equivalent Model
32672135af031c1c465ffff6131b5057daf4bd23	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetUnion	OneLineComment	False	Passed	Model Under Test Equivalent Model
6b3aeddb153d094cff314f108b4f7f6c5df6443e	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetUnion	MultiLineComment	True	Passed	Model Under Test Equivalent Model
7113b65d46008377d2d784a4a22052e0afbad877	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetUnion	MultiLineComment	False	Passed	Model Under Test Equivalent Model
86d1eee35a0a1c184908f4622084b6626f99ec8d	Apalache	SetUnion	BoolSet	True	Passed	Model Under Test Equivalent Model
a4fa22c33c365342be06365bf9debd868d5e4871	Apalache	SetUnion	BoolSet	False	Passed	Model Under Test Equivalent Model
0962e39f811d6e7be63b811a097d682703251d66	Apalache	SetUnion	Let	True	Passed	Model Under Test Equivalent Model
c5e5e1b73a40a39c4d69e39fd9222ce7d82bc3bf	Apalache	SetUnion	Let	False	Passed	Model Under Test Equivalent Model
f41ba3173ab09448f0058fcc84666b557be10faf	Apalache	SetUnion	SetEmpty	True	Passed	Model Under Test Equivalent Model
2bb14b084306a184860d3ebfb05ac28aab9ae783	Apalache	SetUnion	SetEmpty	False	Passed	Model Under Test Equivalent Model
0950d10ef4ed2cfba026a51abb51d597db0a81ac	Apalache	SetUnion	Set0	True	Passed	Model Under Test Equivalent Model
b97e032ee820f9f383fbe98aa26e6cb59d80f6ac	Apalache	SetUnion	Set0	False	Passed	Model Under Test Equivalent Model
26af49a9f6a873769108cbe8f42322e263a74d6b	Apalache	SetUnion	Set1	True	Passed	Model Under Test Equivalent Model
f94dd0d88458c0cb2ba28c6031eb7ce7c30c2743	Apalache	SetUnion	Set1	False	Passed	Model Under Test Equivalent Model
e782231b3783f1f0cbb0362d6f6557cfaaa6dc16	Apalache	SetUnion	Set2	True	Passed	Model Under Test Equivalent Model
6044bab7fd7b8c6dce57880102a929cc12511f88	Apalache	SetUnion	Set2	False	Passed	Model Under Test Equivalent Model
2c0fbc7fcce6afa65de166ccbab56ecdbedcbb06	Apalache	SetUnion	Choose	True	Passed	Model Under Test Equivalent Model
37f6fc44733d004bfcbb12ba53b6059cceea8ac8	Apalache	SetUnion	Choose	False	Passed	Model Under Test Equivalent Model
2334b461227c5033cfa96043f5c3480bf12947e5	Apalache	SetUnion	FunApp	True	Passed	Model Under Test Equivalent Model
878e6246a2793dcc6f39a39a443cca1eebe52406	Apalache	SetUnion	FunApp	False	Passed	Model Under Test Equivalent Model
391e0b725cba9f8ff10dc127834f17a6f56922a2	Apalache	SetUnion	Prime	True	Passed	Model Under Test Equivalent Model
230bb7d8da2aae1966617efbc7c79630c7a6c650	Apalache	SetUnion	Prime	False	Passed	Model Under Test Equivalent Model
45703cce322b22cb9fa780f6fbb7a5d35c10d9f5	Apalache	SetUnion	Def0	True	Passed	Model Under Test Equivalent Model
d66b93097e05f669d1f8d4ced0f7ddac9a890a93	Apalache	SetUnion	Def0	False	Passed	Model Under Test Equivalent Model
2c90c185aff54a254102e6804fc668a604acaf0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef0	True	Passed	Model Under Test Equivalent Model
794ad744ff8a682b90465d002f9bc8a86106bb0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef0	False	Passed	Model Under Test Equivalent Model
9c2173f734d97b99aeca39903301e9e51c393b31	Apalache	SetUnion	Def1	True	Passed	Model Under Test Equivalent Model
4788e7cf059f13b8fded2207d6d4033c3f61c6fd	Apalache	SetUnion	Def1	False	Passed	Model Under Test Equivalent Model
f12cc3dcc5d6677f783404c24cde411fd7dca71a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1	True	Passed	Model Under Test Equivalent Model
cfa39744ac2266c752152e69a3fa37353c72465b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1	False	Passed	Model Under Test Equivalent Model
0bd115e9b3208672778437822324a0b246046ec9	Apalache	SetUnion	Def2	True	Passed	Model Under Test Equivalent Model
af44278dd663c965a2f0af35d0b02c32d32344f5	Apalache	SetUnion	Def2	False	Passed	Model Under Test Equivalent Model
f63e83f175379f2ce897a9a3e9525b2e787932d0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef2	True	Passed	Model Under Test Equivalent Model
6468182e79a6cf3d7478207f256193a02e648119	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef2	False	Passed	Model Under Test Equivalent Model
7f754562d8a58e0399721d8f0baddf475df73227	Apalache	SetUnion	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b4d7dde28b8a602741482a571d0b1c31866fda7e	Apalache	SetUnion	Def1Recursive	False	Passed	Model Under Test Equivalent Model
cd73ac65c4c74cbc6f9abde30e14d24541864c75	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
96ed98303763feb2f445614ac7d809b7aef71f4c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
6f0070786a657af571a4ee6e6061ec5f9458df4a	Apalache	SetUnion	Extends	True	Passed	Model Under Test Equivalent Model
483094d398d354b4019a31c0c6e57abacf57064b	Apalache	SetUnion	Extends	False	Passed	Model Under Test Equivalent Model
5f84a934bed590feb7abcf7c107bbd68dc441331	Apalache	SetUnion	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
6487e112981e63641bec4442a1a1597cbf8248a7	Apalache	SetUnion	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
2849af095158fb26b2ee04eec61e0f72f5e82458	Apalache	SetUnion	Variable	True	Passed	Model Under Test Equivalent Model
c3cdaa037fa895d579bbfd0ea89fe67f7de6f2ea	Apalache	SetUnion	Variable	False	Passed	Model Under Test Equivalent Model
ac82e340201cb1188c52f708147c00205549c5fd	Apalache	SetUnion	Constant	True	Passed	Model Under Test Equivalent Model
5421614295135363ed3e4f560ca65ddd11e92d00	Apalache	SetUnion	Constant	False	Passed	Model Under Test Equivalent Model
66ada128343813c98b3682f218b5bb4eced24c87	Apalache	SetUnion	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ebf5c60a1fa2548a66208c723681651f28e32ddb	Apalache	SetUnion	ConstantRank1	False	Passed	Model Under Test Equivalent Model
991aeb9f3e43f5f1f7ab0807e143b0ee49f0eb75	Apalache	SetUnion	Instance	True	Passed	Model Under Test Equivalent Model
923fcac56b49ce935847350911b6158fbc610c3e	Apalache	SetUnion	Instance	False	Passed	Model Under Test Equivalent Model
341d9336376c1735f29c9e671388ba37291b2a63	Apalache	SetUnion	InstanceWith	True	Passed	Model Under Test Equivalent Model
a8633cc2c44c02e5b727d20ef530b9afee40edd3	Apalache	SetUnion	InstanceWith	False	Passed	Model Under Test Equivalent Model
d3e5d197d6e4336b87d6289c0fa7f10ec520a2b7	Apalache	SetUnion	InstanceNamed	True	Passed	Model Under Test Equivalent Model
dac7810c9f602ad4e5e0d913a6f22ac8b0b14d21	Apalache	SetUnion	InstanceNamed	False	Passed	Model Under Test Equivalent Model
dc6ab01420ca7bfa24abd29dd84d1f2831a9f1e8	Apalache	SetUnion	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
9c72909226a7872b0e7261ef8e00497fa62ade8a	Apalache	SetUnion	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
38d2af1e2641336fc5f781708df15146abac171c	Apalache	SetUnion	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
e7f411f2a02d3e5720f2c2271639425db64f2d9b	Apalache	SetUnion	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
8bd1c89a49d2ab517545b8c6d547b23c83acf919	Apalache	SetUnion	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
e3ab56bd16764b49bff222eb7904fc8f7197f0b7	Apalache	SetUnion	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
fd742262c975013a0d7d34f53f966ccad0c71a9b	Apalache	SetUnion	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
4a6affe1c83eb1b51bf105db6095d599066e90ad	Apalache	SetUnion	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
37d9add65a8d5e12eec2da6127018cd210bc872d	Apalache	SetUnion	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
b73713dd10947fee0fd2c17654d02337268c7d61	Apalache	SetUnion	InstanceNamedWithInFolder	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
e24fb75c892c86dc03172b9cafe8b9b47ba86289	Apalache	SetUnion	Cross3	True	Passed	Model Under Test Equivalent Model
743c7de55d223001e4cf9a5b25faf23211db1cf3	Apalache	SetUnion	Cross3	False	Passed	Model Under Test Equivalent Model
47152f832c01564f3207e9b3cc3a5824fb86fcb4	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))	SetUnion	FunSet	True	Passed	Model Under Test Equivalent Model
8aea9ef7193b3e98ad2eaaa188009bb03a2a915a	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))	SetUnion	FunSet	False	Passed	Model Under Test Equivalent Model
62c21fe45b56275c8a25075248b461f345377a21	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)	SetUnion	RecordSet	True	Passed	Model Under Test Equivalent Model
74ade862c47ccf07888694df9e61dfcb52001019	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)	SetUnion	RecordSet	False	Passed	Model Under Test Equivalent Model
ab4a0b2f8835ea139bfef2d958fa89b00e552182	Apalache	SetUnion	SetDiff	True	Passed	Model Under Test Equivalent Model
22db9fbc9d3df842c8b558023ef0d7067eca1b8d	Apalache	SetUnion	SetDiff	False	Passed	Model Under Test Equivalent Model
f1f8aeffd36e46ccc98cc7cb10c20428789b5d77	Apalache	SetUnion	SetUnion	True	Passed	Model Under Test Equivalent Model
cc080b61c09cb1518a6a9caf50e86bc92c014c5d	Apalache	SetUnion	SetUnion	False	Passed	Model Under Test Equivalent Model
1d66dd0aef4964f33eb7b1f2a24e7e1ef2593dc4	Apalache	SetUnion	SetIntersect	True	Passed	Model Under Test Equivalent Model
e7ecbf0b7b563664b5ba6c86ea8f23b854ff8e27	Apalache	SetUnion	SetIntersect	False	Passed	Model Under Test Equivalent Model
09881ee8078a5f97e63dada96f98ead2112677ec	Apalache	SetUnion	IfCond	True	Passed	Model Under Test Equivalent Model
f7bf07297e239c70e16cd2309d2de86ff186dbb1	Apalache	SetUnion	IfCond	False	Passed	Model Under Test Equivalent Model
8db252af25f2685c38ef0d57067e66d464cf009a	Apalache	SetUnion	IfThen	True	Passed	Model Under Test Equivalent Model
de3e3be8620a4acfbdefaee4b941c1662e202301	Apalache	SetUnion	IfThen	False	Passed	Model Under Test Equivalent Model
67adb565327a9837c2cce660bb5185d6b5a782ec	Apalache	SetUnion	IfElse	True	Passed	Model Under Test Equivalent Model
324cf0028b094fd185212e6b4104c5d7d7946c0c	Apalache	SetUnion	IfElse	False	Passed	Model Under Test Equivalent Model
3dbf797f191cd13166210303543c152c54fc65b6	Apalache	SetUnion	Subset	True	Passed	Model Under Test Equivalent Model
4335ec0bb7d5e2cfd6bc965e673eea83f9d0610c	Apalache	SetUnion	Subset	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
1cd7e4158234fd54d0a55cd015de5e3d02266f72	Apalache	SetUnion	Union	True	Passed	Model Under Test Equivalent Model
d764de13ca2826a0b650d7c947e5552d8e09cf27	Apalache	SetUnion	Union	False	Passed	Model Under Test Equivalent Model
347a83d9d54a97fa3dc809735c0481014335f8f9	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	SetUnion	NumRange	True	Passed	Model Under Test Equivalent Model
ad35adf44741d319e9439de86782f632f03c5695	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	SetUnion	NumRange	False	Passed	Model Under Test Equivalent Model
5c13574b8ca0a0dc991e7dd6186ce0475e941f0c	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SetUnion	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
85e47bb03e855f69c7bea5486d7cad1c5674634b	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SetUnion	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
6bb34df9ce07d92c3c84faf01c9c9ff1ad02ee12	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SetUnion	TlcEval	True	Passed	Model Under Test Equivalent Model
636b47ad4ba48ad2a6c507d38061225c450bca6b	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SetUnion	TlcEval	False	Passed	Model Under Test Equivalent Model
1faf3e30f07c1ea91c9cdeca4e5a94a0a71da2fe	Apalache	SetUnion	BagBagToSet	True	Passed	Model Under Test Equivalent Model
6287eb60272ff7fc6b32127edc96f1f6d4fe3c73	Apalache	SetUnion	BagBagToSet	False	Passed	Model Under Test Equivalent Model
4aae2948f25e4e914981ef2a7c51d038448b5177	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SetUnion	BagSubBag	True	Passed	Model Under Test Equivalent Model
2e7495fc4d610f98c008fcde5ef7b832568b646e	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SetUnion	BagSubBag	False	Passed	Model Under Test Equivalent Model
b193c6541fe455447bfed7baf57796d4db9e24c3	Apalache	SetUnion	SeqHead	True	Passed	Model Under Test Equivalent Model
c30d18fbb181b0bdc4b8bebfde1b49473202d1f8	Apalache	SetUnion	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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