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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
21480ec6c9eee579998f10cc0f0bf30b2dc3e339	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	BagSetToBag	OneLineComment	True	Passed	Model Under Test Equivalent Model
193609da9e9ad801ac2e697bc1e7b749e44a65c4	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	BagSetToBag	OneLineComment	False	Passed	Model Under Test Equivalent Model
b91dde6d9c5bbe124c0616de5a24ed80c805ef03	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	BagSetToBag	MultiLineComment	True	Passed	Model Under Test Equivalent Model
31992c1ca73ac57875eb71e5b4940fd2ed8775ce	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	BagSetToBag	MultiLineComment	False	Passed	Model Under Test Equivalent Model
9e468f8631d813775fa643a8e48bea7db8118850	Apalache	BagSetToBag	BoolSet	True	Passed	Model Under Test Equivalent Model
210375098b924d57bf53b7961a15e93cb3bcf08d	Apalache	BagSetToBag	BoolSet	False	Passed	Model Under Test Equivalent Model
abd4666373642111302c4cc85ce8884f0bd62d24	Apalache	BagSetToBag	Let	True	Passed	Model Under Test Equivalent Model
f07f9177511d7b556c04917ff0cc46ec232c3363	Apalache	BagSetToBag	Let	False	Passed	Model Under Test Equivalent Model
b27d623df45f42f2023f2b8b1aae6108f7f0d915	Apalache	BagSetToBag	SetEmpty	True	Passed	Model Under Test Equivalent Model
c0e91072b5ac7196a6c00b0106bcf08fb8fcd5ff	Apalache	BagSetToBag	SetEmpty	False	Passed	Model Under Test Equivalent Model
94251b430ea317767e4cfb38f92bc27c2cbedbd8	Apalache	BagSetToBag	Set0	True	Passed	Model Under Test Equivalent Model
8425d44e99397e49ba32cecb030d284648649b73	Apalache	BagSetToBag	Set0	False	Passed	Model Under Test Equivalent Model
0a29ad8bf14395e3293a275a54340639ff16004a	Apalache	BagSetToBag	Set1	True	Passed	Model Under Test Equivalent Model
1e05eb222044e49ab81914235f4406d22236e629	Apalache	BagSetToBag	Set1	False	Passed	Model Under Test Equivalent Model
a09d5d19c86b4502221ac86075c35568c717261c	Apalache	BagSetToBag	Set2	True	Passed	Model Under Test Equivalent Model
9e5312599e30412ebe42eecd3cf0daef9e0db837	Apalache	BagSetToBag	Set2	False	Passed	Model Under Test Equivalent Model
9940a8a6f0b407142a89300972a06dbce6135ddc	Apalache	BagSetToBag	Choose	True	Passed	Model Under Test Equivalent Model
f85a4369962b05db3e4ba206165bf6b28a3660f8	Apalache	BagSetToBag	Choose	False	Passed	Model Under Test Equivalent Model
63aa7c3b28ff4b79c154ab8d7bcd2bc1bc5277d7	Apalache	BagSetToBag	FunApp	True	Passed	Model Under Test Equivalent Model
52cdfc4c21ee2e286265b16a960c9358fe84afbe	Apalache	BagSetToBag	FunApp	False	Passed	Model Under Test Equivalent Model
3c96ec19eb18efabcf6d41a1128049ce467ad4d7	Apalache	BagSetToBag	Prime	True	Passed	Model Under Test Equivalent Model
2a3d75c3680ec8cccaa7aa18635bea86331a773a	Apalache	BagSetToBag	Prime	False	Passed	Model Under Test Equivalent Model
2c49299c3f296b02c834e39337bda8836533593d	Apalache	BagSetToBag	Def0	True	Passed	Model Under Test Equivalent Model
0c3f57308840214cd18a6f4f516cf433bb1df007	Apalache	BagSetToBag	Def0	False	Passed	Model Under Test Equivalent Model
a2dd31f0e0ee087f036f5100e50d49f54cdad39b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef0	True	Passed	Model Under Test Equivalent Model
3f6dde82a71a35a2cffd852b9d692ed67a29cfc1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef0	False	Passed	Model Under Test Equivalent Model
bae2e66680d68afb76be543032dea47a22d84914	Apalache	BagSetToBag	Def1	True	Passed	Model Under Test Equivalent Model
afa14ef55dd93366b11f3d483619402ec6ca70e3	Apalache	BagSetToBag	Def1	False	Passed	Model Under Test Equivalent Model
296c2708619c16dba6db5d5cd8ea27bbc88af2c5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1	True	Passed	Model Under Test Equivalent Model
c78fb4c3290beb8b0f420297a447ed38a1a5d2e1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1	False	Passed	Model Under Test Equivalent Model
57ae6837b39bde8a5860401912f6fd035d3b654f	Apalache	BagSetToBag	Def2	True	Passed	Model Under Test Equivalent Model
680d8f38cec84c6f069dcf524beb61df62b1fed1	Apalache	BagSetToBag	Def2	False	Passed	Model Under Test Equivalent Model
1c89c99c3b2a55bbd05a328276c07c12a0c70188	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef2	True	Passed	Model Under Test Equivalent Model
5143d1695ee2a90eb10004a619be52aea36b7b8c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef2	False	Passed	Model Under Test Equivalent Model
3ec746cf58ae43cb4e99c8f01ffc6d80ca0829a3	Apalache	BagSetToBag	Def1Recursive	True	Passed	Model Under Test Equivalent Model
dae36bf900a04fba65a52d3207a98cc8351402a3	Apalache	BagSetToBag	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a6ffdf774a011542ac87f02eb858b9ab1ee18b0a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
8d78327f0992a85f3b28d258ca2f942a7e4ca4e3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
fbd7e981f5c2210d644268193ce3f0e4dd9e2c11	Apalache	BagSetToBag	Extends	True	Passed	Model Under Test Equivalent Model
77864d38cbe95f33db2aea76d5358d4733a538a8	Apalache	BagSetToBag	Extends	False	Passed	Model Under Test Equivalent Model
9c6f443d6cb79ef06cd8c47d2a03371be7c73e63	Apalache	BagSetToBag	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
00e448d81ad905dffe8bff97ac5b2dbc39316d66	Apalache	BagSetToBag	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
1d64af67d73182ee2d82d8152019bfdf9ebd75c4	Apalache	BagSetToBag	Variable	True	Passed	Model Under Test Equivalent Model
af865b21434cac7f9e0f08f3c04cb2f8e81bc115	Apalache	BagSetToBag	Variable	False	Passed	Model Under Test Equivalent Model
c92a046b015336c66fe254e9133234d1b058f3ca	Apalache	BagSetToBag	Constant	True	Passed	Model Under Test Equivalent Model
ef315f1d6274a35cca06855502a173df187d76d1	Apalache	BagSetToBag	Constant	False	Passed	Model Under Test Equivalent Model
86540ae656e84f30fc8575aa85a7a41dd0243ab1	Apalache	BagSetToBag	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f073e4d80676dff6110897fb55e25215af08fdde	Apalache	BagSetToBag	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c48634b29961cbe6ea9b2658968ab03d9b2a7b6d	Apalache	BagSetToBag	Instance	True	Passed	Model Under Test Equivalent Model
182efc506991d5b316d44363dc624e6bc8985dcb	Apalache	BagSetToBag	Instance	False	Passed	Model Under Test Equivalent Model
99dd97b2402cedc5b26790169bea492a7c0f6f85	Apalache	BagSetToBag	InstanceWith	True	Passed	Model Under Test Equivalent Model
becad0d7fff67180ad2c3ed40b105f328d884635	Apalache	BagSetToBag	InstanceWith	False	Passed	Model Under Test Equivalent Model
d856d962b0aeaeeb635e0bf9d832e65ce26a622f	Apalache	BagSetToBag	InstanceNamed	True	Passed	Model Under Test Equivalent Model
375ac9a209a754bf516506463322cce8294233c5	Apalache	BagSetToBag	InstanceNamed	False	Passed	Model Under Test Equivalent Model
0f5cdba97577b0a9ca8693a2af73181ef3d8c2fb	Apalache	BagSetToBag	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a2278b225b115124dd10f5499cd5c07e992bafde	Apalache	BagSetToBag	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8b1d0442379ab4d1f8b55fccfbf30048f58dea5a	Apalache	BagSetToBag	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
5f5256d6c640f3e954fde62252c2d21c4b8f5bc6	Apalache	BagSetToBag	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
e9813d95444dcf2cb4f86ab6c48624b4380877da	Apalache	BagSetToBag	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
a00c6821d6ab9e095d9a691c13169700035ca703	Apalache	BagSetToBag	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
991dece5c85560b7ff4a53bf258cce5173d083bd	Apalache	BagSetToBag	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
45fa8d228c48f24f7f4d59ca0c9f88b1d0c5b65f	Apalache	BagSetToBag	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
259dd23df6b85037f93fb70d79b6b4a2904853b4	Apalache	BagSetToBag	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
79dfb6e0e11db3ada5c44e4cedeb5a704bef4867	Apalache	BagSetToBag	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
783e86572d2e99ab83207a8e2d18ecea3922a213	Apalache	BagSetToBag	Cross2	True	Passed	Model Under Test Equivalent Model
b91f6c2b3ae4531ec1520f9c1a90d4c931cd6540	Apalache	BagSetToBag	Cross2	False	Passed	Model Under Test Equivalent Model
27eec23376db1c946ad63b0c290ff0d4fdf3cf3d	Apalache	BagSetToBag	Cross3	True	Passed	Model Under Test Equivalent Model
926200627436472577621b11f05c42fe8943a0d8	Apalache	BagSetToBag	Cross3	False	Passed	Model Under Test Equivalent Model
8841acfcf250d75432236c0d54fce790cc426f42	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))	BagSetToBag	FunSet	True	Passed	Model Under Test Equivalent Model
68b4dc9b5ac5a2f6e4edaea4a88f7efa917c82f9	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))	BagSetToBag	FunSet	False	Passed	Model Under Test Equivalent Model
63410a8ed87b24e05aaf1383802d2d62bcc6ba9b	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)	BagSetToBag	RecordSet	True	Passed	Model Under Test Equivalent Model
de6b55f1141222b020e8599c5e1c8c35dc23619f	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)	BagSetToBag	RecordSet	False	Passed	Model Under Test Equivalent Model
8064a42db5eb696897879c022338aa5d30220633	Apalache	BagSetToBag	SetDiff	True	Passed	Model Under Test Equivalent Model
1c66be964b336b589d94aee7440d4dc48473be29	Apalache	BagSetToBag	SetDiff	False	Passed	Model Under Test Equivalent Model
e6bdaebcbdbe5ef6d7364db149c12fa4db1c0854	Apalache	BagSetToBag	SetUnion	True	Passed	Model Under Test Equivalent Model
d49e5ddd83dcabd8bb5d7d78f680c0eab106a516	Apalache	BagSetToBag	SetUnion	False	Passed	Model Under Test Equivalent Model
3fd46d624f466ef81283c9158155130754fa43d2	Apalache	BagSetToBag	SetIntersect	True	Passed	Model Under Test Equivalent Model
2ce06e7d6c107f406fc5927c65c5d33be9e1c9da	Apalache	BagSetToBag	SetIntersect	False	Passed	Model Under Test Equivalent Model
8e98fffdfd67f6828bc48263483af18fbca33d52	Apalache	BagSetToBag	IfCond	True	Passed	Model Under Test Equivalent Model
bbe964f8e8d2868d8743a095fdbe0fa9ad810dd0	Apalache	BagSetToBag	IfCond	False	Passed	Model Under Test Equivalent Model
7d5b9aac7caa7b4b787c17c9a4043124f367723a	Apalache	BagSetToBag	IfThen	True	Passed	Model Under Test Equivalent Model
72048a996b2430560587f8fdf3748646cfda1cf2	Apalache	BagSetToBag	IfThen	False	Passed	Model Under Test Equivalent Model
885e2e9e1b5a1de4f14f25e83e51dacdb93ae022	Apalache	BagSetToBag	IfElse	True	Passed	Model Under Test Equivalent Model
f9df4dc6e98f35f54616237af4c321042226117d	Apalache	BagSetToBag	IfElse	False	Passed	Model Under Test Equivalent Model
9c3f76c3547e29d631d048f9afe146f9e4bb878c	Apalache	BagSetToBag	Subset	True	Passed	Model Under Test Equivalent Model
882423bf498074c809f3b36d04bd5d9243822498	Apalache	BagSetToBag	Subset	False	Passed	Model Under Test Equivalent Model
d6f6de1ff0e4ecdad2c2e7c8d975ab50958a176d	Apalache	BagSetToBag	Domain	True	Passed	Model Under Test Equivalent Model
886a55c1040b80be8491008bed7ef8a913774f2a	Apalache	BagSetToBag	Domain	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
c616d83285ec63ba60c92fdf5a624a7ee3252c61	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	BagSetToBag	NumRange	True	Passed	Model Under Test Equivalent Model
036787cf6362f83e917c0d09d9530ed93a843447	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	BagSetToBag	NumRange	False	Passed	Model Under Test Equivalent Model
8d0c5f8e7d3bba47bce5b5ddf89d066a066306a4	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	BagSetToBag	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
970326c351c6929e57e12c6d0b66e6b7c5d964ee	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	BagSetToBag	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
3ae4148c7a97a632c748fe0dbb81250f1c543bb7	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	BagSetToBag	TlcEval	True	Passed	Model Under Test Equivalent Model
17b1ad9d807293f2669e7a9764ca199d14d7e01f	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	BagSetToBag	TlcEval	False	Passed	Model Under Test Equivalent Model
3c53f32945b8f1f7a2c5861d2ec7757303cc7c9b	Apalache	BagSetToBag	BagBagToSet	True	Passed	Model Under Test Equivalent Model
121368295ef14b7b45a9019b93fe864e9e4609b2	Apalache	BagSetToBag	BagBagToSet	False	Passed	Model Under Test Equivalent Model
2e1dbc82fda724c73d7b485f5131938adc04afd4	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSetToBag	BagSubBag	True	Passed	Model Under Test Equivalent Model
d5744be9c095b4029b8245aa5736451705a42d6a	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSetToBag	BagSubBag	False	Passed	Model Under Test Equivalent Model
d4a7e7bb55a05cb3a545c175628c34c8bac2ae79	Apalache	BagSetToBag	SeqHead	True	Passed	Model Under Test Equivalent Model
6777aa2e21f5572a2ef0e66e309d11df36c5b998	Apalache	BagSetToBag	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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