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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
433d19bdf2d3e5440582972c3c1d2d1f447163d1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SubsetEq	OneLineComment	True	Passed	Model Under Test Equivalent Model
c4fb79019144f536729e47f2387c6b0f25000aad	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SubsetEq	OneLineComment	False	Passed	Model Under Test Equivalent Model
92ff4120933121d70c358fac1cbf03ad753534d0	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SubsetEq	MultiLineComment	True	Passed	Model Under Test Equivalent Model
fddb0b5f4facda3f7a7cf8ff64cabd10c70b88f7	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	SubsetEq	MultiLineComment	False	Passed	Model Under Test Equivalent Model
dae6b4f02db89b960c87b540d9134ea46042949d	Apalache	SubsetEq	BoolSet	True	Passed	Model Under Test Equivalent Model
0871c5aff01d67008d7fa313c650b01aaf53652b	Apalache	SubsetEq	BoolSet	False	Passed	Model Under Test Equivalent Model
106fac0428ee39a3732484eae971d1411ca71c65	Apalache	SubsetEq	Let	True	Passed	Model Under Test Equivalent Model
ba5f33ccd9a3533bbe44695553afea02a8fd99bd	Apalache	SubsetEq	Let	False	Passed	Model Under Test Equivalent Model
ac8bd261d27fe9e3f2210843a1234810a1090ff7	Apalache	SubsetEq	SetEmpty	True	Passed	Model Under Test Equivalent Model
f288603a08ad5e1b16a18cb114bd04322a8e8aff	Apalache	SubsetEq	SetEmpty	False	Passed	Model Under Test Equivalent Model
383b6071b147d15a6b5b76b19f1aa092aed663bd	Apalache	SubsetEq	Set0	True	Passed	Model Under Test Equivalent Model
fe452adee410e9797eedec6ffc8e46ddcd9ed069	Apalache	SubsetEq	Set0	False	Passed	Model Under Test Equivalent Model
33f6a62ddbf47d6871f8fa8cc3c09e314420a1a9	Apalache	SubsetEq	Set1	True	Passed	Model Under Test Equivalent Model
74f08d36d4172264cd41659ced866e9aff9ad4c1	Apalache	SubsetEq	Set1	False	Passed	Model Under Test Equivalent Model
2d86faaf48756bfefa2bf8a104d9d58c24f3525a	Apalache	SubsetEq	Set2	True	Passed	Model Under Test Equivalent Model
a321fe1dd9147eb0cbf9e7468519c4fdf113bc4c	Apalache	SubsetEq	Set2	False	Passed	Model Under Test Equivalent Model
6041adc6c732f653989353a6fb151346f3c1caae	Apalache	SubsetEq	Choose	True	Passed	Model Under Test Equivalent Model
e806131a1621afe4849f68e854d1afcac069115c	Apalache	SubsetEq	Choose	False	Passed	Model Under Test Equivalent Model
d77a7fd0a37a947ea3971429251c2ec5898c6d60	Apalache	SubsetEq	FunApp	True	Passed	Model Under Test Equivalent Model
2bce7e58419c27b80304836a633e0781f00f02b6	Apalache	SubsetEq	FunApp	False	Passed	Model Under Test Equivalent Model
62a14a85805b8bbad45d7662f508d10bb0bafda7	Apalache	SubsetEq	Prime	True	Passed	Model Under Test Equivalent Model
559fd77953a515ad68488554733ec7cb51618e36	Apalache	SubsetEq	Prime	False	Passed	Model Under Test Equivalent Model
964e852f8d5be63ab8d4957bea2993e69dee1233	Apalache	SubsetEq	Def0	True	Passed	Model Under Test Equivalent Model
3056d99863b375a8a63dd8e7ceb54c96c30d8d30	Apalache	SubsetEq	Def0	False	Passed	Model Under Test Equivalent Model
e992552ed10a4be0693ff3dd9400272ab53868e3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef0	True	Passed	Model Under Test Equivalent Model
0c16198ae48dec71693500ee14452644a281507a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef0	False	Passed	Model Under Test Equivalent Model
875a87caa2b4beefea4f4949f7587818a3157b67	Apalache	SubsetEq	Def1	True	Passed	Model Under Test Equivalent Model
66f58ad3a42753ce8e82ba1024760de3260b9b31	Apalache	SubsetEq	Def1	False	Passed	Model Under Test Equivalent Model
550c63bd7ae157229ba9346f954d013cf7895e0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1	True	Passed	Model Under Test Equivalent Model
98d32d5cc77d718e96aa04fcb5fe31931d6f0037	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1	False	Passed	Model Under Test Equivalent Model
4d722f586a057525ac8f029eb68b9db8c4b41f13	Apalache	SubsetEq	Def2	True	Passed	Model Under Test Equivalent Model
65043bf0b4d7dc9e6fa755fc73b41994ad0e5a82	Apalache	SubsetEq	Def2	False	Passed	Model Under Test Equivalent Model
34811ce2021d3a94f297dd5a368555e0df2d80e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef2	True	Passed	Model Under Test Equivalent Model
ebd9fdb1fb7a54b6c8c8fbb54652d3966aea7603	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef2	False	Passed	Model Under Test Equivalent Model
99a24bdac04d029232fdf18a1340589add5fe89f	Apalache	SubsetEq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
167bc6111dc8a6863ca67e024cf9a001fa8450c9	Apalache	SubsetEq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
aad37457692d2e8a1d297ad0053ce66cc8d70ba3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
e08e4d783ed7a1491bf4efccdf66e4ffb3ced22c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
0a956c2a26b94132fa471b107ec0bc6035abec9a	Apalache	SubsetEq	Extends	True	Passed	Model Under Test Equivalent Model
0530807e6873569c97b650a249df02bc1b78324f	Apalache	SubsetEq	Extends	False	Passed	Model Under Test Equivalent Model
7042ff6acd610e57e331f0f560bcaca736343693	Apalache	SubsetEq	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
960e44c959d91f712361864bfd689237946693f5	Apalache	SubsetEq	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
b8756ba92a9643fba5e7f9869f1136d34b14e0cb	Apalache	SubsetEq	Variable	True	Passed	Model Under Test Equivalent Model
42b7372043c3c12107d839c297df6a7c68841076	Apalache	SubsetEq	Variable	False	Passed	Model Under Test Equivalent Model
ed94fe845c78a14910437291d972515e000f4727	Apalache	SubsetEq	Constant	True	Passed	Model Under Test Equivalent Model
3e96633d2ce4e7960a9e3be9893f577848d845f7	Apalache	SubsetEq	Constant	False	Passed	Model Under Test Equivalent Model
4f3f115b7e191fff4d383f739521241ecb93b20b	Apalache	SubsetEq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
46b38f55f3892bdee50e0c3e83d1f86b9a25f428	Apalache	SubsetEq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9e6b95f0ba1ad74a4eaf40ce7093489b1ad8d07e	Apalache	SubsetEq	Instance	True	Passed	Model Under Test Equivalent Model
6cd6614060d3b99f07758e065bec47306793849b	Apalache	SubsetEq	Instance	False	Passed	Model Under Test Equivalent Model
59cdb713174c3e082921fe4a55aa9f5c60c5635d	Apalache	SubsetEq	InstanceWith	True	Passed	Model Under Test Equivalent Model
eb6fe61f090fd80f27fbd7724350a6aee1bf2513	Apalache	SubsetEq	InstanceWith	False	Passed	Model Under Test Equivalent Model
783a277d313b0b85d187cca5e914f55032d80979	Apalache	SubsetEq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
e10de991293579fd23702f938cc298eadc4dbf4f	Apalache	SubsetEq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
19630b1935c8108e87757da07e3de21cd4439e7c	Apalache	SubsetEq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b4a0f257cbfa9a3a90f46599fffa299ae749a816	Apalache	SubsetEq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
e3b82560a6890976a9b5ca5d92eaf71cd22de810	Apalache	SubsetEq	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
e4581b6afd36400db6430aa794968c8180fb6ca0	Apalache	SubsetEq	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
c2e57f3894f2817eac3d0edf1d5fd4f3c3863338	Apalache	SubsetEq	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
4c03b2c23eef94c4c79a00c1d400a38b97cc9894	Apalache	SubsetEq	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
30531a0d02e194347bdef82891cd8a26cb838c27	Apalache	SubsetEq	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
29543c91f40b11ea1819a4f78ec5265e74f11aa4	Apalache	SubsetEq	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
eabd42589898d3cf7cd6fa04543bb9d01e3efa45	Apalache	SubsetEq	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
fd9bd760a5e18d1c76392d85c590a00f8c29a3cb	Apalache	SubsetEq	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
6ac8c72d431ce50768066074aa9a91cb717e2104	Apalache	SubsetEq	Cross2	True	Passed	Model Under Test Equivalent Model
bdd2e16d8dd3d3cff67ab94c94c5f98475b16092	Apalache	SubsetEq	Cross2	False	Passed	Model Under Test Equivalent Model
c06eebec5b2eb2df91ac1b749f1ef3542d59f0fb	Apalache	SubsetEq	Cross3	True	Passed	Model Under Test Equivalent Model
7ce5234403239ecb3048690a73a1c7ab2eb74518	Apalache	SubsetEq	Cross3	False	Passed	Model Under Test Equivalent Model
f39aca427600f2325d750cd06fc2e57ae0ccb1dd	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))	SubsetEq	FunSet	True	Passed	Model Under Test Equivalent Model
10eba1c07ee03bc28be52b706f8203975bc76fe5	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))	SubsetEq	FunSet	False	Passed	Model Under Test Equivalent Model
ce3736807013f4ee9e93f04dbaef0a4362fe5d58	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)	SubsetEq	RecordSet	True	Passed	Model Under Test Equivalent Model
2f55258a3ff3640a4e2f939880b02b071fda71c0	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)	SubsetEq	RecordSet	False	Passed	Model Under Test Equivalent Model
34d760a54bb4ad3fc0f4892b6c84efa2e9d9ef6f	Apalache	SubsetEq	SetDiff	True	Passed	Model Under Test Equivalent Model
907f64c05bb99e9c5a76fccb8a33100beb2f2cc5	Apalache	SubsetEq	SetDiff	False	Passed	Model Under Test Equivalent Model
e8340dd3c92194ec39aaae29e05b4adba169488e	Apalache	SubsetEq	SetUnion	True	Passed	Model Under Test Equivalent Model
f247d34f6faf773913b7e0bfc82ab632d9237045	Apalache	SubsetEq	SetUnion	False	Passed	Model Under Test Equivalent Model
0408ad26db43877167b9f8695a0f723775e542ff	Apalache	SubsetEq	SetIntersect	True	Passed	Model Under Test Equivalent Model
576f246b8e11f1425a190f8b5fbc75e826e0f54c	Apalache	SubsetEq	SetIntersect	False	Passed	Model Under Test Equivalent Model
9f13afcd1db8cb952f1510eac6812be2edf2b613	Apalache	SubsetEq	IfCond	True	Passed	Model Under Test Equivalent Model
a44fb8cec0587c753bbc1c65b22ff951586b7c86	Apalache	SubsetEq	IfCond	False	Passed	Model Under Test Equivalent Model
dd5685adf45589f689b7e32ca681c9f44be15061	Apalache	SubsetEq	IfThen	True	Passed	Model Under Test Equivalent Model
189bb0e5114370d39dc509da7dfca8f19ff84679	Apalache	SubsetEq	IfThen	False	Passed	Model Under Test Equivalent Model
80dcd5cb020229486aa344d05a8a05d2d508318d	Apalache	SubsetEq	IfElse	True	Passed	Model Under Test Equivalent Model
7a2336fb371740bb174a5b94a8552eb2e58d3eaa	Apalache	SubsetEq	IfElse	False	Passed	Model Under Test Equivalent Model
c9604330b704159560a7de45b2eae40cfa7cf140	Apalache	SubsetEq	Subset	True	Passed	Model Under Test Equivalent Model
23684752f31df6d3e342d1aaa773daefb2d37011	Apalache	SubsetEq	Subset	False	Passed	Model Under Test Equivalent Model
e7b74da05d907a05abe31980b8af26873cdd74de	Apalache	SubsetEq	Domain	True	Passed	Model Under Test Equivalent Model
9b7280586fd480dd0160110f945164e3c060aa71	Apalache	SubsetEq	Domain	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
080ad0b59351be7fbe14bfa89aaf70ed56ed77be	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	SubsetEq	NumRange	True	Passed	Model Under Test Equivalent Model
3b420ca80819744a1133a6b97a173f040a05a542	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	SubsetEq	NumRange	False	Passed	Model Under Test Equivalent Model
8d23ee4aec165ccbedac5f5089100ad0da263d86	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SubsetEq	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
de19a172057fdcfceb06e56815c7042fda457e04	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SubsetEq	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
77c38e06131043a9bf9af679c02d392f399bb0c6	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SubsetEq	TlcEval	True	Passed	Model Under Test Equivalent Model
cb469be5cc62a9f04c24af9584d73b04cfd87ae1	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SubsetEq	TlcEval	False	Passed	Model Under Test Equivalent Model
1c8e86fd3cad88a70f6b1cddfa07d19da514a13d	Apalache	SubsetEq	BagBagToSet	True	Passed	Model Under Test Equivalent Model
c28f87f30d44b9e124154fa8e24b2bdb55fe7607	Apalache	SubsetEq	BagBagToSet	False	Passed	Model Under Test Equivalent Model
036057fab3f2ac3113aa671946cf4366566fc462	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SubsetEq	BagSubBag	True	Passed	Model Under Test Equivalent Model
124100261710fd29b544e54c3d8a48e61bff3b85	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SubsetEq	BagSubBag	False	Passed	Model Under Test Equivalent Model
1ce7b6b2fd2777a6e9d70dbe053821c3f58964a2	Apalache	SubsetEq	SeqHead	True	Passed	Model Under Test Equivalent Model
360bedfb27df4f4a0801acccbe1ae8689d78d98f	Apalache	SubsetEq	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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