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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
1ac3f2e0c56116c87091197a1793281217f00a3d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetIntersect	OneLineComment	True	Passed	Model Under Test Equivalent Model
40075784b4df238c4ed0911d23c7d4c74cd68bbc	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetIntersect	OneLineComment	False	Passed	Model Under Test Equivalent Model
23a271fdb85a1e698b6d35abce1537caef0330b1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetIntersect	MultiLineComment	True	Passed	Model Under Test Equivalent Model
4fdaf4b98422ebe3087bfe34a30c05a27adfdd88	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SetIntersect	MultiLineComment	False	Passed	Model Under Test Equivalent Model
2f175b224190f5b8982b90548770b751adb5b804	Apalache	SetIntersect	BoolSet	True	Passed	Model Under Test Equivalent Model
b176889be3817d86b009c13f02d769d817017b31	Apalache	SetIntersect	BoolSet	False	Passed	Model Under Test Equivalent Model
328e0e80c5363c0b9684e4814d9473a25198e773	Apalache	SetIntersect	Let	True	Passed	Model Under Test Equivalent Model
e44d0756dbcefca492e02356f9761a3f0c3f02de	Apalache	SetIntersect	Let	False	Passed	Model Under Test Equivalent Model
4c49e9b7fcc4339d22bb928060cc77cd14f606a0	Apalache	SetIntersect	SetEmpty	True	Passed	Model Under Test Equivalent Model
b375551b9ce798c575aaf7bc1b1988672fc3c0fe	Apalache	SetIntersect	SetEmpty	False	Passed	Model Under Test Equivalent Model
8969c28e71b9d810d8325f5d6f9dd64a9e3e2f13	Apalache	SetIntersect	Set0	True	Passed	Model Under Test Equivalent Model
532740fb8b3d4e97b776f2d6fb5e1bd6991fef8c	Apalache	SetIntersect	Set0	False	Passed	Model Under Test Equivalent Model
4609a92c646015a1f4857e9b728a58a05c4c92e9	Apalache	SetIntersect	Set1	True	Passed	Model Under Test Equivalent Model
194ad938390e9a3c573efecc0b737dc847e9973b	Apalache	SetIntersect	Set1	False	Passed	Model Under Test Equivalent Model
e17e6e01642595b331fd1f77fd9e5de9dd65cb18	Apalache	SetIntersect	Set2	True	Passed	Model Under Test Equivalent Model
99e3d9ad4a8858d1e927c5ffd226eb7393dac28d	Apalache	SetIntersect	Set2	False	Passed	Model Under Test Equivalent Model
410d878dc8c30c033e755e4c5de5d623d118e28e	Apalache	SetIntersect	Choose	True	Passed	Model Under Test Equivalent Model
1b34be0229f1cb33c30fc2b820c4f1762813ade3	Apalache	SetIntersect	Choose	False	Passed	Model Under Test Equivalent Model
3bda1ba1ac3aa738b34fbbaf8339432f8a2e79d6	Apalache	SetIntersect	FunApp	True	Passed	Model Under Test Equivalent Model
2845245673c9d45b794ade2935c53697d6f296cd	Apalache	SetIntersect	FunApp	False	Passed	Model Under Test Equivalent Model
2ecbec2642fbadf7f3e339fa118bf6571499be21	Apalache	SetIntersect	Prime	True	Passed	Model Under Test Equivalent Model
53ab05cfe4c6719549d2154dedafdb50fb360316	Apalache	SetIntersect	Prime	False	Passed	Model Under Test Equivalent Model
93e3b2a051e5c2cda9ec0f6e01feda56d33711cc	Apalache	SetIntersect	Def0	True	Passed	Model Under Test Equivalent Model
baa6503572ca11da7bd54adfbadebdeee74da5da	Apalache	SetIntersect	Def0	False	Passed	Model Under Test Equivalent Model
43eb5a13725b28d5246d448eb03e8479b5adf135	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef0	True	Passed	Model Under Test Equivalent Model
b60f5a2310ddfcd7e907cc00e86ee69d3fea2ef3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef0	False	Passed	Model Under Test Equivalent Model
bca7e01b39bf0c9c260c878441cf8742d4cd1502	Apalache	SetIntersect	Def1	True	Passed	Model Under Test Equivalent Model
44fdaa4c59b234fe94d95b072c880fbd99492a8f	Apalache	SetIntersect	Def1	False	Passed	Model Under Test Equivalent Model
c1a166f95d668c7bb2d368a7b322080b8f24d467	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1	True	Passed	Model Under Test Equivalent Model
7ffd55b89a39cddee168804980c17b97a48c4ec5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1	False	Passed	Model Under Test Equivalent Model
ef50fa1a72a3bbd3fc97c0dc12dd60aad7c6f0df	Apalache	SetIntersect	Def2	True	Passed	Model Under Test Equivalent Model
42cf292128112374af165d98037855f7dedd1f11	Apalache	SetIntersect	Def2	False	Passed	Model Under Test Equivalent Model
1a4b919e89054378398c1ac4629ed753f511f7e9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef2	True	Passed	Model Under Test Equivalent Model
40963758f7cbfc74631b8149a096a53e63a486a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef2	False	Passed	Model Under Test Equivalent Model
b4e304555983afac4d271a433c8c5c2f036483fe	Apalache	SetIntersect	Def1Recursive	True	Passed	Model Under Test Equivalent Model
2b711c0c8a06a466153a3a65acaecf97060fba60	Apalache	SetIntersect	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c5fede3ad0bb03d308f106126acd42e09efe99ff	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
8138dc6a770e60de9270bf9449fe808d904d9683	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
ed6bfc24c625fbe3bdc0e7df33fd6170ee30c4bb	Apalache	SetIntersect	Extends	True	Passed	Model Under Test Equivalent Model
d01517a85db6714368cabbb79b5f40ca21af9538	Apalache	SetIntersect	Extends	False	Passed	Model Under Test Equivalent Model
acf14392760aa2970aab49bd6508745cf6440c5d	Apalache	SetIntersect	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
c1057488506fcd049ae3938236e184702b763f31	Apalache	SetIntersect	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
628a2dca21ca4ee7a1cee792ee3ba1d68b2fa9af	Apalache	SetIntersect	Variable	True	Passed	Model Under Test Equivalent Model
4b6e943f67bab0f21cb03ff383e74ee86c487e1f	Apalache	SetIntersect	Variable	False	Passed	Model Under Test Equivalent Model
af386044586415e7a279101c6d633ef2e3fe2cc7	Apalache	SetIntersect	Constant	True	Passed	Model Under Test Equivalent Model
ca062121c259cc238420a32fce68647708e6bb15	Apalache	SetIntersect	Constant	False	Passed	Model Under Test Equivalent Model
1d55a4696a9b14b89dd4dc5d91bc953741df4c40	Apalache	SetIntersect	ConstantRank1	True	Passed	Model Under Test Equivalent Model
b579306c0405a5861befd896af2f780353c955e4	Apalache	SetIntersect	ConstantRank1	False	Passed	Model Under Test Equivalent Model
7f1f9f1d8ef4d88f4481cc908adfb7c7ca6e295f	Apalache	SetIntersect	Instance	True	Passed	Model Under Test Equivalent Model
38dba3932fe344763345116e6a25860eca2f37f6	Apalache	SetIntersect	Instance	False	Passed	Model Under Test Equivalent Model
3f1c7e70a0f35cff42ae8c2d927b0a46bbb7b3cc	Apalache	SetIntersect	InstanceWith	True	Passed	Model Under Test Equivalent Model
d3b9b79183372a5822ae032b679a991013a8eee0	Apalache	SetIntersect	InstanceWith	False	Passed	Model Under Test Equivalent Model
4dd373fef54e4bb75b28c4502346a472e4e88ee9	Apalache	SetIntersect	InstanceNamed	True	Passed	Model Under Test Equivalent Model
fd4eecc6958a4ce879636d2554c459ac043fe6f3	Apalache	SetIntersect	InstanceNamed	False	Passed	Model Under Test Equivalent Model
e1fe29fb1e2cf8d051f92bf0cace68143ff0b8e8	Apalache	SetIntersect	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
066a3eefb06dcdfdb2fc10631324a2be9fb55cbf	Apalache	SetIntersect	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
eb6773daba45888250f922476004193aa21939e9	Apalache	SetIntersect	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
ce471dd3cdf6cb4bd3dfb01d6510e2d38928de30	Apalache	SetIntersect	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
9509b98931df088ddc208adb8b301428f41d36b3	Apalache	SetIntersect	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
8a21acc8e5ea4f1598de292928eb98c1d68cb50e	Apalache	SetIntersect	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
6db1d2334068fad695625f91fcaba762f5b5790b	Apalache	SetIntersect	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
f48e8ce418a9c238e363b78bcd864a78bc6b0a73	Apalache	SetIntersect	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
91e4f5022a66b76ed73d9a1b2248e213630c2deb	Apalache	SetIntersect	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
92367ac426f7339033615de1d7584b8e43c9fbee	Apalache	SetIntersect	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
45c715ae5732a5efceed52112e85d7c24560e0f4	Apalache	SetIntersect	Cross2	True	Passed	Model Under Test Equivalent Model
f9b9a863b1c6dd2c783631d9e2149d1a9c900b41	Apalache	SetIntersect	Cross2	False	Passed	Model Under Test Equivalent Model
5da8642eb95d2e7e07b9dad468046b960c0b898f	Apalache	SetIntersect	Cross3	True	Passed	Model Under Test Equivalent Model
3de63430229130b680bb290263a25e0e5f25f1b8	Apalache	SetIntersect	Cross3	False	Passed	Model Under Test Equivalent Model
64c2150e03f9750c4f30ce02f9e44f19e7d8f11d	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))	SetIntersect	FunSet	True	Passed	Model Under Test Equivalent Model
551f7f930e7e83d1848fad7e7d411d1af92c09ab	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))	SetIntersect	FunSet	False	Passed	Model Under Test Equivalent Model
5c7bfe85283f6165f95ef1ffec83e5351736aa6c	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)	SetIntersect	RecordSet	True	Passed	Model Under Test Equivalent Model
85020d3d7c8986e13d86af855d6fc24f0750088f	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)	SetIntersect	RecordSet	False	Passed	Model Under Test Equivalent Model
03f52b5376c53fc1f723759ff6c7741a93abc888	Apalache	SetIntersect	SetDiff	True	Passed	Model Under Test Equivalent Model
9c31e6421d83c8f8b99f96938e5de20425af967a	Apalache	SetIntersect	SetDiff	False	Passed	Model Under Test Equivalent Model
ad4cee448422abf5c9f7976375a013ed6aa5bfd8	Apalache	SetIntersect	SetUnion	True	Passed	Model Under Test Equivalent Model
48afde26469535b7fae51cec08275ddd20130669	Apalache	SetIntersect	SetUnion	False	Passed	Model Under Test Equivalent Model
cb623f8d4711c6a16786401647b73c263fe82e83	Apalache	SetIntersect	SetIntersect	True	Passed	Model Under Test Equivalent Model
cb4ffe72e4df1680cb31be21dafb2e4a7c8ce86b	Apalache	SetIntersect	SetIntersect	False	Passed	Model Under Test Equivalent Model
fcb89fe06a22d6302ff3fb87ddc0d9622a1a7a54	Apalache	SetIntersect	IfCond	True	Passed	Model Under Test Equivalent Model
fb3d8c25d8af47a651780365594234425f87a15e	Apalache	SetIntersect	IfCond	False	Passed	Model Under Test Equivalent Model
41439f21d2fe7380eb6f0f1ebd4612655b4db142	Apalache	SetIntersect	IfThen	True	Passed	Model Under Test Equivalent Model
66590ede403043ca7feb3e79de78dd40c684a6ac	Apalache	SetIntersect	IfThen	False	Passed	Model Under Test Equivalent Model
fba01973e1cddfc092583b015f771d4569c79d90	Apalache	SetIntersect	IfElse	True	Passed	Model Under Test Equivalent Model
a5ce28c5a29e2c2fd53dc128810a752a28291008	Apalache	SetIntersect	IfElse	False	Passed	Model Under Test Equivalent Model
e70d24a555b98da18ab1d32600552152b0211021	Apalache	SetIntersect	Subset	True	Passed	Model Under Test Equivalent Model
ccac5eabbed77da002e702370b909f4e69551305	Apalache	SetIntersect	Subset	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
3b02e6eb5e59161643c4b1e555f837867278f10d	Apalache	SetIntersect	Union	True	Passed	Model Under Test Equivalent Model
55b29d6e4994d4692b5983e9c2adb87efc880cdf	Apalache	SetIntersect	Union	False	Passed	Model Under Test Equivalent Model
a6081b76e0d91241eae9a1a5f13cf03f014a4158	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	SetIntersect	NumRange	True	Passed	Model Under Test Equivalent Model
3a609ff29f440660d2928372247cea1c3f5a43e4	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	SetIntersect	NumRange	False	Passed	Model Under Test Equivalent Model
f271ed41e273d694034078427a061d32f2ccb773	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SetIntersect	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
472d5eb641180133f154382e6ba6c0fba3be5997	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SetIntersect	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
d15809fef8c2970ff3977e6a64b70db589196de4	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SetIntersect	TlcEval	True	Passed	Model Under Test Equivalent Model
c0dfd056c6d6d812fdcd542c3cd0534ff3dbf7c9	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SetIntersect	TlcEval	False	Passed	Model Under Test Equivalent Model
bac90a0ca40c4ee61a5087283f7f5f5b87b3010f	Apalache	SetIntersect	BagBagToSet	True	Passed	Model Under Test Equivalent Model
56d8c2b38441e7690da1f0cf3f1ead6c49d63d89	Apalache	SetIntersect	BagBagToSet	False	Passed	Model Under Test Equivalent Model
7e8480c1df5e4951c6c2ac9c3eb1729f6a96032b	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SetIntersect	BagSubBag	True	Passed	Model Under Test Equivalent Model
ee70ad10bf37fb558d3f55e82bacc8762e0ec079	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SetIntersect	BagSubBag	False	Passed	Model Under Test Equivalent Model
80766efd1ad00fe9d67f4d8b58cd6a74c5557612	Apalache	SetIntersect	SeqHead	True	Passed	Model Under Test Equivalent Model
8254e24c3925464be320e66d990bd1a85d8b5144	Apalache	SetIntersect	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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