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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
46fd0ad9377f527e9d15c4186fd8983b983e5e33	Apalache	Eq	Union	True	Passed	Model Under Test Equivalent Model
317a0bf37689164aad0393f6f95284b3911506b0	Apalache	Eq	Union	False	Passed	Model Under Test Equivalent Model
a2c8fa0534ce2544197d2de826db4add839da93f	Apalache	Ne	Union	True	Passed	Model Under Test Equivalent Model
04433599e0611cb5f74c3a8b212c401d467e9071	Apalache	Ne	Union	False	Passed	Model Under Test Equivalent Model
353ca0090b880ef9d289598d8726980ab9f3b777	Apalache	Let	Union	True	Passed	Model Under Test Equivalent Model
3e92ee09979dbd9469cb7722bd8739a8810fa501	Apalache	Let	Union	False	Passed	Model Under Test Equivalent Model
62888f98e69ee8fc9542568beb084d00dab3e9ce	Apalache	Set0	Union	True	Passed	Model Under Test Equivalent Model
e2cbe1566bbf3b32ed747a9b98bfc1fed4177d42	Apalache	Set0	Union	False	Passed	Model Under Test Equivalent Model
066f7186a2adf4a630199066458dc29af4f3fd00	Apalache	Set1	Union	True	Passed	Model Under Test Equivalent Model
778b2b76ef6616503ed19f86978044bfe3af55c0	Apalache	Set1	Union	False	Passed	Model Under Test Equivalent Model
62dd8ea4384b1f60277fe5f9ec69ab4303aa8cb7	Apalache	Set2	Union	True	Passed	Model Under Test Equivalent Model
b0af1feafcbf5e3b2120cea961e886dca7a13f3a	Apalache	Set2	Union	False	Passed	Model Under Test Equivalent Model
0409c59eabf210bababf407adfd40be255be6655	Apalache	Fun	Union	True	Passed	Model Under Test Equivalent Model
d87d2cd09cb8bfa31fa6971a9c08c6648b9df7d6	Apalache	Fun	Union	False	Passed	Model Under Test Equivalent Model
7ac4ed896e45c191b7bdb22c4d1eb9491e722b79	Apalache	In	Union	True	Passed	Model Under Test Equivalent Model
d2362710be8fd755654b962e76dd3806b9cddf20	Apalache	In	Union	False	Passed	Model Under Test Equivalent Model
d6dd6a21d49dc51ab14c9d3a1244e496590280b5	Apalache	NotIn	Union	True	Passed	Model Under Test Equivalent Model
5c69355c7f75584588ea4a23d0cfab926b880ada	Apalache	NotIn	Union	False	Passed	Model Under Test Equivalent Model
7d4b60595c73cbcd9f0fa5d63395161ce23be98b	Apalache	Record	Union	True	Passed	Model Under Test Equivalent Model
b9bec69ead4544eb7b431b35e1cceed82ab21de7	Apalache	Record	Union	False	Passed	Model Under Test Equivalent Model
d0d780b50a3a9919f1fab5f897bce24c10cb8fa5	Apalache	Tuple	Union	True	Passed	Model Under Test Equivalent Model
e7ba6dfb8ea96b398c2ee660d940adfca1d79748	Apalache	Tuple	Union	False	Passed	Model Under Test Equivalent Model
7e42949ba5bf3e834af212a766c849805aa6a0d3	Apalache	FunApp	Union	True	Passed	Model Under Test Equivalent Model
ed73c9f7776ffcda2100b25212182b2ecc1b5ec7	Apalache	FunApp	Union	False	Passed	Model Under Test Equivalent Model
0d660c11c2a7a8d76ff1885434541563181693a7	Apalache	Except1Fun	Union	True	Passed	Model Under Test Equivalent Model
41a036d713a2728e049e6e67932f4ffdbe6432ef	Apalache	Except1Fun	Union	False	Passed	Model Under Test Equivalent Model
63d1e31f9b0611536c00369d1da6ce05386ee70b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Union	True	Passed	Model Under Test Equivalent Model
1e2ce8387d0b9676d959a5343ea855996b2843e2	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Union	False	Passed	Model Under Test Equivalent Model
943836eeb012dd464b57d2f5fd8e91ca3b51615a	Apalache	Except1Rec	Union	True	Passed	Model Under Test Equivalent Model
ab7c6f6e7a8b5df0a5e2121da0559b16342cc2fd	Apalache	Except1Rec	Union	False	Passed	Model Under Test Equivalent Model
7b1e191dfdee270197caef2991376b201320f4ba	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Union	True	Passed	Model Under Test Equivalent Model
5dbe12f789b877040962206e94b09777d21f92aa	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Union	False	Passed	Model Under Test Equivalent Model
b1fd48293dc68f4b1ef2c0dc0ffaa0ed59d7fb18	Apalache	Except2Fun	Union	True	Passed	Model Under Test Equivalent Model
2d2651bc97a53f40489bc17d54980e3a6247c75f	Apalache	Except2Fun	Union	False	Passed	Model Under Test Equivalent Model
26fc51299992a301c1d0ca12df049d8aea30b3f6	Apalache	Prime	Union	True	Passed	Model Under Test Equivalent Model
c234425d52538134f302fb04ea3dca59f6a897db	Apalache	Prime	Union	False	Passed	Model Under Test Equivalent Model
109d7f90b7720696cb0340d8a730fa62417dec56	Apalache	DefFun	Union	True	Passed	Model Under Test Equivalent Model
7e5f75f9397f6f46c4413e2eb23dc292bd1a76a8	Apalache	DefFun	Union	False	Passed	Model Under Test Equivalent Model
c1ccc9a9dc6368373197822f969600ce1e51af3c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Union	True	Passed	Model Under Test Equivalent Model
fb352969a0bf0728bbf4cc7f282f2e4350c43b03	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Union	False	Passed	Model Under Test Equivalent Model
efd9420374720f39d9dca23a9f990d4df91615c9	Apalache	DefFunRecursive	Union	True	Passed	Model Under Test Equivalent Model
04f2ab9cb330371f68abe80c4863e5bdced9b955	Apalache	DefFunRecursive	Union	False	Passed	Model Under Test Equivalent Model
e82388bee8e5b34dea0a914f2bbe7a1de1483037	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Union	True	Passed	Model Under Test Equivalent Model
965cb251409aacae42cb36fbddaacc0a58f274dc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Union	False	Passed	Model Under Test Equivalent Model
fd8604de999091b61bfdc37ea09581526e2731ac	Apalache	Def0	Union	True	Passed	Model Under Test Equivalent Model
70d410ae2eccd44a25e0270e67f15ed347caa1f5	Apalache	Def0	Union	False	Passed	Model Under Test Equivalent Model
88a15e3e784fbf923b4be0c6a3ed0f3e6e3abb9b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Union	True	Passed	Model Under Test Equivalent Model
38354be8bfc5ee6c9be8d032b46f58858a94cdcd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Union	False	Passed	Model Under Test Equivalent Model
8c736528ad5af45b7f6c1c1c7b4d573d492335eb	Apalache	Def1	Union	True	Passed	Model Under Test Equivalent Model
095bff046bd8c99a08a2909598d2e0b6b2389a24	Apalache	Def1	Union	False	Passed	Model Under Test Equivalent Model
74ca2cac96598f998517fdfb86a5b732a5e36f7f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Union	True	Passed	Model Under Test Equivalent Model
fd4d16cff8669c32d051023ff25811408e7e30cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Union	False	Passed	Model Under Test Equivalent Model
39cb416b6f5fa618cf0d4cd3bb13601f8325a14d	Apalache	Def2	Union	True	Passed	Model Under Test Equivalent Model
cf437a28bbaee292f8d26ba24ae19ae8a562b501	Apalache	Def2	Union	False	Passed	Model Under Test Equivalent Model
ce8370214e87bd99bb10415af509ba04a5fe222e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Union	True	Passed	Model Under Test Equivalent Model
2356a9e71e6e398ad7d7eecafd0916eb00125a5e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Union	False	Passed	Model Under Test Equivalent Model
2ff8edfc592708981f8941ccb26a072ce2c04893	Apalache	Def1Recursive	Union	True	Passed	Model Under Test Equivalent Model
4cb9910c30cd66b8375b664a7023d8f225fdf8f3	Apalache	Def1Recursive	Union	False	Passed	Model Under Test Equivalent Model
5438966b6a7145bca5dbce5b1a2408a52ebf9933	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Union	True	Passed	Model Under Test Equivalent Model
565ad03d2d8612b1fdc08e392b58a5bcb58237cd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Union	False	Passed	Model Under Test Equivalent Model
6b1f6b5dc02ed678ca3532711549758738db274d	Apalache	Extends	Union	True	Passed	Model Under Test Equivalent Model
05455c56cecdd452500e6bf0025a97cb81d80e5b	Apalache	Extends	Union	False	Passed	Model Under Test Equivalent Model
2155588cec6bf8c48fa66cea8d3955440179f6f9	Apalache	ExtendsInDifferentFolder	Union	True	Passed	Model Under Test Equivalent Model
19f10a69e5f60893005f55d0e60cb90d8101310d	Apalache	ExtendsInDifferentFolder	Union	False	Passed	Model Under Test Equivalent Model
4535a1430129d5284f5479f4ef5478f3aa7beeaa	Apalache	Variable	Union	True	Passed	Model Under Test Equivalent Model
59cde515ceccf945193baacbbad0340a11aa3d6c	Apalache	Variable	Union	False	Passed	Model Under Test Equivalent Model
f01afc3f92cd2e9dbf3de5fe829ad88119d4c437	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Union	True	Passed	Model Under Test Equivalent Model
247d331b4d5d61e3c8b87b2b0f2aa48e214da171	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Union	False	Passed	Model Under Test Equivalent Model
a2fd03945f8a82b703865a8191afb9202d6834da	Apalache	Constant	Union	True	Passed	Model Under Test Equivalent Model
2548e12dc3285ad958cc8d1f5f3d3fe37bc0d608	Apalache	Constant	Union	False	Passed	Model Under Test Equivalent Model
9a2b69660f39adff0cfd8bb8c59578ea2398fe22	Apalache	ConstantRank1	Union	True	Passed	Model Under Test Equivalent Model
7f75dc77bd0598c2913f2b3ed1bd2260170063a8	Apalache	ConstantRank1	Union	False	Passed	Model Under Test Equivalent Model
f14206e9f9ab218af774006a71eb94b2781fbc35	Apalache	Instance	Union	True	Passed	Model Under Test Equivalent Model
800057138936817bb00f642ae126d07ede4328ce	Apalache	Instance	Union	False	Passed	Model Under Test Equivalent Model
81abc4bb60eaee125c757a0e8de8b8ea6dc4a5db	Apalache	InstanceWith	Union	True	Passed	Model Under Test Equivalent Model
51d201f5d5adecbc2e3a50b199d1abf2558602c9	Apalache	InstanceWith	Union	False	Passed	Model Under Test Equivalent Model
ba1d7e3dcd5b76875a3fbdf823bdbce80a16ccaa	Apalache	InstanceNamed	Union	True	Passed	Model Under Test Equivalent Model
903ec7221162d8693945abbca62ae8b0dec2be56	Apalache	InstanceNamed	Union	False	Passed	Model Under Test Equivalent Model
86d4331b03129fb8800c65a658e428388a15e0c0	Apalache	InstanceNamedWith	Union	True	Passed	Model Under Test Equivalent Model
b0d22741a6db52e872fbe31a6b64a48ef4ea5b93	Apalache	InstanceNamedWith	Union	False	Passed	Model Under Test Equivalent Model
c7b8bb4f7c1ed6f5aefef8375babbe6e75bf5c33	Apalache	InstanceInFolder	Union	True	Passed	Model Under Test Equivalent Model
5ece1711331c98d2892b3cee635b9c45bac37332	Apalache	InstanceInFolder	Union	False	Passed	Model Under Test Equivalent Model
041d43147a869e2b73053f3adc87750b7d945c67	Apalache	InstanceWithInFolder	Union	True	Passed	Model Under Test Equivalent Model
38b89e11c293c1eda040664a3972fd95bc27493a	Apalache	InstanceWithInFolder	Union	False	Passed	Model Under Test Equivalent Model
ff054ddc12223f91ca046f23e3cbaca401d8ea0e	Apalache	InstanceNamedInFolder	Union	True	Passed	Model Under Test Equivalent Model
a901e0fcfda929f7a85a3aed700bc5ccf77bb9c6	Apalache	InstanceNamedInFolder	Union	False	Passed	Model Under Test Equivalent Model
1bbdeb0e4bf8b77fe961a82190ed25c6fdc7414e	Apalache	InstanceNamedWithInFolder	Union	True	Passed	Model Under Test Equivalent Model
71da149f58a97d4cfa89c47be5bd3d3a96c7366c	Apalache	InstanceNamedWithInFolder	Union	False	Passed	Model Under Test Equivalent Model
9c7d4576581c44e25042dd80f4efaa3974c70779	Apalache	Lambda	Union	True	Passed	Model Under Test Equivalent Model
00be486b5f180738018bddb970be89411b8a10cd	Apalache	Lambda	Union	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
81ea9baebd6e22c8dcd8be970adabfbf40fdcc8c	Apalache	Cross3	Union	True	Passed	Model Under Test Equivalent Model
45125136f2a67fa587ac79994e04b6fa37b78928	Apalache	Cross3	Union	False	Passed	Model Under Test Equivalent Model
65c58ca61449f6cc40c2babb84d8aea883c4292c	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	Union	True	Passed	Model Under Test Equivalent Model
bb1258e589058d1cf49fef5bb22483c65d283c4f	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	Union	False	Passed	Model Under Test Equivalent Model
01a4559095e7ff16ca8cf2a8badef121d4e7b6c3	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	Union	True	Passed	Model Under Test Equivalent Model
f2e08a7329793ca3f92a1dd552c0a38d7e886036	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	Union	False	Passed	Model Under Test Equivalent Model
c42579a40ac06a96f15f6cd469396709794aa613	Apalache	SetDiff	Union	True	Passed	Model Under Test Equivalent Model
103821a97ec9a78c0c9037271b05acd332eb16e5	Apalache	SetDiff	Union	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
3b02e6eb5e59161643c4b1e555f837867278f10d	Apalache	SetIntersect	Union	True	Passed	Model Under Test Equivalent Model
55b29d6e4994d4692b5983e9c2adb87efc880cdf	Apalache	SetIntersect	Union	False	Passed	Model Under Test Equivalent Model
48f3ecc12f10d25b68cef4c22d3746a23dbef051	Apalache	SubsetEq	Union	True	Passed	Model Under Test Equivalent Model
b501527f8aa34b92e0070d71b1201c0bdcdf34c0	Apalache	SubsetEq	Union	False	Passed	Model Under Test Equivalent Model
c66090046d8827f92dd4f13d99e7dc5efd9992b0	Apalache	IfThen	Union	True	Passed	Model Under Test Equivalent Model
95e1ee4ee78b05648223c14234ecd11b6eecc3ec	Apalache	IfThen	Union	False	Passed	Model Under Test Equivalent Model
3f9169ec1f2715217d7c6b607a61be23f9125f8d	Apalache	IfElse	Union	True	Passed	Model Under Test Equivalent Model
69e902de708ca06e1544d670dbfaa1a14f75a117	Apalache	IfElse	Union	False	Passed	Model Under Test Equivalent Model
a34f149f4fb10369dee39b9cb902dfe823014e47	Apalache	Subset	Union	True	Passed	Model Under Test Equivalent Model
7b0bf74bcaaa888288231c5bb08e79609e36936d	Apalache	Subset	Union	False	Passed	Model Under Test Equivalent Model
cc0264191644f9ec2440dd33482ba53601533310	Apalache	Union	Union	True	Passed	Model Under Test Equivalent Model
1d86c5429bbd89b646e0d2188a48d6ae353ef226	Apalache	Union	Union	False	Passed	Model Under Test Equivalent Model
676c7e4bebed62fe6db3b6d58d7b18675000ec1c	Apalache	Unchanged	Union	True	Passed	Model Under Test Equivalent Model
a1f728dec85c13da31a3b84cfaa7352f390220ff	Apalache	Unchanged	Union	False	Passed	Model Under Test Equivalent Model
a81897df44fa573f3569ec8f17424158a3c4295c	Apalache	SeqSeq	Union	True	Passed	Model Under Test Equivalent Model
0322777ec0aa0970e84b58553c74353b31a437b0	Apalache	SeqSeq	Union	False	Passed	Model Under Test Equivalent Model
c9cab046eb3ee36ee56da90440e9535ab67b169c	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Union	True	Passed	Model Under Test Equivalent Model
e791e9ba362d9db38d4496f103334d7aeafb238a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Union	False	Passed	Model Under Test Equivalent Model
1c3c18c8319e0a171d965b24353de2f7728491e7	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Union	True	Passed	Model Under Test Equivalent Model
fc99661f370368d6b56d44782d6e6466512b6325	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Union	False	Passed	Model Under Test Equivalent Model
cecf1b1d345f21ad038e30ffa0247db86516eb92	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Union	True	Passed	Model Under Test Equivalent Model
1acdf143795809f513445b3290745018e092ceff	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Union	False	Passed	Model Under Test Equivalent Model
c6c70d057532438550d2d2a6029207ed9c6e8d8c	Apalache	BagSetToBag	Union	True	Passed	Model Under Test Equivalent Model
d3b302114f77a497bdd5040e6f654a6d3162b887	Apalache	BagSetToBag	Union	False	Passed	Model Under Test Equivalent Model
49f5118093c0ffd3b649498a265cc67c887863da	Apalache	BagBagIn	Union	True	Passed	Model Under Test Equivalent Model
e0617e080d8ae8f9d37e4f27f153c200b6d16a1c	Apalache	BagBagIn	Union	False	Passed	Model Under Test Equivalent Model
6cd2c419ce199eba5c2ba85146b95493cf18c1a4	Apalache	BagCopiesIn	Union	True	Passed	Model Under Test Equivalent Model
ca003a15f08ae1c0f59fce17dd5b27cc5f1df4dc	Apalache	BagCopiesIn	Union	False	Passed	Model Under Test Equivalent Model
663f5324c2166643a5fa1ba42828fc65c8d037a3	Apalache	BagBagUnion	Union	True	Passed	Model Under Test Equivalent Model
fb205cafeb906f7e448bad98c5cd99b7b6c55918	Apalache	BagBagUnion	Union	False	Passed	Model Under Test Equivalent Model
8acbc13aa5bdb017e65ee04db36edb24d821b169	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	Union	True	Passed	Model Under Test Equivalent Model
7046168ab14ff47729b51cd6ccdfb414ede46ba1	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	Union	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
9074fcd745ca56ddf8f2cbb17f05304b304a1d4a	Apalache	SeqAppend	Union	True	Passed	Model Under Test Equivalent Model
c219e32f26669d5b407a5179d6cb2cbab771f83c	Apalache	SeqAppend	Union	False	Passed	Model Under Test Equivalent Model

Index

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