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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
0a43cfa60a614d03971b70dee55b814415e7792a	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def2	OneLineComment	True	Passed	Model Under Test Equivalent Model
be75c4709a8dc716c50cf14e34b789e9e1415552	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def2	OneLineComment	False	Passed	Model Under Test Equivalent Model
0d6b7d1e24ee37f500210bcf96456618015761df	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def2	MultiLineComment	True	Passed	Model Under Test Equivalent Model
6ba27d064cb835631a36395ad5a205dbd6995f90	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def2	MultiLineComment	False	Passed	Model Under Test Equivalent Model
843d02b0614ae567199a6731f5ed3688b027acd1	Apalache	Def2	BoolTrue	True	Passed	Model Under Test Equivalent Model
65a6a61d8b8c546a80ed53f784c69f901f5d6b9f	Apalache	Def2	BoolTrue	False	Passed	Model Under Test Equivalent Model
8862f9830bbacf04a9866d0aee72915d3629e29b	Apalache	Def2	BoolFalse	True	Passed	Model Under Test Equivalent Model
70e04f1e4295738e4346770d9c775cba57e2da9e	Apalache	Def2	BoolFalse	False	Passed	Model Under Test Equivalent Model
9926f24301468c1aaf3d8b0d3b714b62150bde47	Apalache	Def2	BoolSet	True	Passed	Model Under Test Equivalent Model
e14f08753f5bebbbf6650cfa235139fceead595f	Apalache	Def2	BoolSet	False	Passed	Model Under Test Equivalent Model
03137c8cb78812556d84ba314d1c7acaabccf920	Apalache	Def2	And	True	Passed	Model Under Test Equivalent Model
38b43ab0ea035342d321fde55d19d3229496efad	Apalache	Def2	And	False	Passed	Model Under Test Equivalent Model
c4c957d5a5c6997e1b1d24262281840567fe391d	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def2	AndMultiLine	True	Passed	Model Under Test Equivalent Model
7b8b7a3397945e80f85f6e1dd6a50a6085017bb2	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def2	AndMultiLine	False	Passed	Model Under Test Equivalent Model
f87b8ed937f11bc7ade14275d8b2c3037d0d1a74	Apalache	Def2	Imply	True	Passed	Model Under Test Equivalent Model
1fe93a337ba6fcd333cbf4074119da433a16dc43	Apalache	Def2	Imply	False	Passed	Model Under Test Equivalent Model
0d734bbc05c0a98d7d5ddd677f9abce9df24d4bc	Apalache	Def2	Not	True	Passed	Model Under Test Equivalent Model
49d4f3584348c6739018c020548a9287d258958f	Apalache	Def2	Not	False	Passed	Model Under Test Equivalent Model
ebe665b9981ea54040d8674ce970901f0b6008e7	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def2	Or	True	Passed	Model Under Test Equivalent Model
ec52f8540356a7b90fc58691e9386ffd785d1f6d	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def2	Or	False	Passed	Model Under Test Equivalent Model
277e22ac7d4e9c0f1091f3064d3e9eb7de3d3c15	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def2	OrMultiLine	True	Passed	Model Under Test Equivalent Model
fc4ffe54a90721dba806ad00cc07a65842e0728c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def2	OrMultiLine	False	Passed	Model Under Test Equivalent Model
2f397f0fa3802908bc21ab4d0407fe3a26c15ced	Apalache	Def2	AndProp	True	Failed:	Model Under Test Equivalent Model
90efe6221f398ee6d776cc94ee96246dcb7eb8c4	Apalache	Def2	AndProp	False	Failed:	Model Under Test Equivalent Model
147e8a4cffe636b65800f847b08f93ff7768dd49	Apalache	Def2	Boxed	True	Failed: There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property	Model Under Test Equivalent Model
1374059dc9765e9c8f151f32751f7a17f4a2d57b	Apalache	Def2	Boxed	False	Failed: There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property	Model Under Test Equivalent Model
75241bc808d9c9c561a9b5af5261a0660bbfb2c9	Apalache	Def2	Eq	True	Passed	Model Under Test Equivalent Model
dcc0eeac153577e76b0521abcb66e8ce7cb842c9	Apalache	Def2	Eq	False	Passed	Model Under Test Equivalent Model
6f2d23249bcc7cc8488eaecd22e598a38acb60e1	Apalache	Def2	Ne	True	Passed	Model Under Test Equivalent Model
aa2af6fcfa4b9a29417b7c0610d9dd40ffdfe587	Apalache	Def2	Ne	False	Passed	Model Under Test Equivalent Model
22911c9ab54123c87c28cb2c0e726af2885ac4d2	Apalache	Def2	Let	True	Passed	Model Under Test Equivalent Model
ada3394cc53eb7f77a09e64bcbf2a38cd07124af	Apalache	Def2	Let	False	Passed	Model Under Test Equivalent Model
56cb4368213ccda4cd5c09c7de873b958dfa50fa	Apalache	Def2	SetEmpty	True	Passed	Model Under Test Equivalent Model
cd13ba34e6e39bdadd93a0f5887bcfee65b6e73f	Apalache	Def2	SetEmpty	False	Passed	Model Under Test Equivalent Model
2545cf28d8031d7e8c93561044460763941e58de	Apalache	Def2	Set0	True	Passed	Model Under Test Equivalent Model
1ab507a02834e94a51d2ef7d0485ff8fd3b528f0	Apalache	Def2	Set0	False	Passed	Model Under Test Equivalent Model
e8ab6a857dcdd0ce7906f3e9320e5896affa7ae8	Apalache	Def2	Set1	True	Passed	Model Under Test Equivalent Model
1e37385d7a078665f66692f93301a8c92785b32e	Apalache	Def2	Set1	False	Passed	Model Under Test Equivalent Model
ccfa875b7e0860e624d426ae33c67e5b6a230ddc	Apalache	Def2	Set2	True	Passed	Model Under Test Equivalent Model
d8662c476d529de05eca6b9cc2a000007350b921	Apalache	Def2	Set2	False	Passed	Model Under Test Equivalent Model
6c676e2ec96cc21249b7f577e09cab1e4a18cf79	Apalache	Def2	Fun	True	Passed	Model Under Test Equivalent Model
81c769a82304e9d560a9267dcf7e35151f4c70ae	Apalache	Def2	Fun	False	Passed	Model Under Test Equivalent Model
1f755318f0bd448374ff1c22eb15853614eff938	Apalache	Def2	In	True	Passed	Model Under Test Equivalent Model
9cbc475e0720aa5ebb65fd265719ce36fb1a5198	Apalache	Def2	In	False	Passed	Model Under Test Equivalent Model
a06fd380e34bad656b6942616923a13f07c018f0	Apalache	Def2	NotIn	True	Passed	Model Under Test Equivalent Model
53d14fe57732f4fdb1dd2edca804ffa08ee8c1e9	Apalache	Def2	NotIn	False	Passed	Model Under Test Equivalent Model
734902e311f007e601207404b9fbfc19fe99a58c	Apalache	Def2	Exists	True	Passed	Model Under Test Equivalent Model
5d877915a231dd54a10161c575f13538d1bb537d	Apalache	Def2	Exists	False	Passed	Model Under Test Equivalent Model
14641efef82e056ba06df86afd00b7612db2fb33	Apalache	Def2	Forall	True	Passed	Model Under Test Equivalent Model
0099bdd96bd0adcf79d195afec6e2c1a28dfe820	Apalache	Def2	Forall	False	Passed	Model Under Test Equivalent Model
efe9bada483fb63b1a3001aa51943a0463fbbab9	Apalache	Def2	Choose	True	Passed	Model Under Test Equivalent Model
be0b091d3a9f8521438f13b395d83c022252d11e	Apalache	Def2	Choose	False	Passed	Model Under Test Equivalent Model
5fde76db0d2788517a7b3c83873837dd67da10d0	Apalache	Def2	Record	True	Passed	Model Under Test Equivalent Model
29f7c473113b4f5d85bf91988e94d74248be7120	Apalache	Def2	Record	False	Passed	Model Under Test Equivalent Model
acd2d4a56eca2f1139e64d0dc1881ebd112fc09c	Apalache	Def2	Tuple	True	Passed	Model Under Test Equivalent Model
0bf54481db5452602d95897585df304ffe420578	Apalache	Def2	Tuple	False	Passed	Model Under Test Equivalent Model
8a5bfdecc0ddf65cfbbd26285176bbb76f542b3d	Apalache	Def2	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c1fc90a14deb9ad9611717d07906ef2835c41004	Apalache	Def2	TupleEmpty	False	Passed	Model Under Test Equivalent Model
c19975da39e34f7b3588eb2125ab2a45a24146f3	Apalache	Def2	FunApp	True	Passed	Model Under Test Equivalent Model
ce222959d11e319a65228d6aecb20f19814a9e45	Apalache	Def2	FunApp	False	Passed	Model Under Test Equivalent Model
c4ad70bd08f3224499d444cd370e9fee04c61d1c	Apalache	Def2	Prime	True	Passed	Model Under Test Equivalent Model
913bb88e0dabc5801f4d27c54856c82b52180004	Apalache	Def2	Prime	False	Passed	Model Under Test Equivalent Model
1f40f6f4a3a520546dec933e64a5c160d84d0ab8	Apalache	Def2	NumZero	True	Passed	Model Under Test Equivalent Model
7e7b3a11ce41fbb3ff7826bb04b2b2724737e88c	Apalache	Def2	NumZero	False	Passed	Model Under Test Equivalent Model
f343b7230ad175055b83c4b381c5979ccb719db4	Apalache	Def2	NumOne	True	Passed	Model Under Test Equivalent Model
a1e806b1d950e651907c8267abaa301da3ca0575	Apalache	Def2	NumOne	False	Passed	Model Under Test Equivalent Model
505949019f12adb89b9a26a0cedeaf1d476b92c8	Apalache	Def2	NumMaxInt	True	Passed	Model Under Test Equivalent Model
5e080b7b44d703a774316b001d8ba85ea9c0d2dd	Apalache	Def2	NumMaxInt	False	Passed	Model Under Test Equivalent Model
da5c798475b3e07793d8d8c018e3be6777d7c814	Apalache	Def2	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
60962becb77474f5693e8a5d2e3d84495eb58e0f	Apalache	Def2	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
50821a7152e7633a91ab330796b8c836300d4a22	Apalache	Def2	NumPlus	True	Passed	Model Under Test Equivalent Model
cd5d2e7f3614b2c48b5861c11666edc089aa74b1	Apalache	Def2	NumPlus	False	Passed	Model Under Test Equivalent Model
509f8dea8877904c6adefa3c5e04c1d6fce04d3a	Apalache	Def2	NumMinus	True	Passed	Model Under Test Equivalent Model
b2fab82c17df80d442ef6e2b09ce7f86f227ed50	Apalache	Def2	NumMinus	False	Passed	Model Under Test Equivalent Model
64e36c0f3a75acbcc318e7969165bd331f45503d	Apalache	Def2	NumMul	True	Passed	Model Under Test Equivalent Model
c2571560d653662059e566f89994ecb8fc8e4355	Apalache	Def2	NumMul	False	Passed	Model Under Test Equivalent Model
87f7c5c4d67005ef6631ff1a21555746c3f988b6	Apalache	Def2	NumDiv	True	Passed	Model Under Test Equivalent Model
45e41dbc006133071ecf8244f8830ab61f8c3913	Apalache	Def2	NumDiv	False	Passed	Model Under Test Equivalent Model
af6efdec00336a2dd8a87a43a3981c6ed86e6608	Apalache	Def2	NumMod	True	Passed	Model Under Test Equivalent Model
9c38ae4ddf1fc093b701a5e55b660c98244cc397	Apalache	Def2	NumMod	False	Passed	Model Under Test Equivalent Model
2d2793eaa2d8cfb18ddd53d15954638338aff8ac	Apalache	Def2	NumPow	True	Passed	Model Under Test Equivalent Model
60bdcbb811a5415af037c754829d4a7ac0368619	Apalache	Def2	NumPow	False	Passed	Model Under Test Equivalent Model
a837f052846decb45a5828c2f4aedb331dd3288e	Apalache	Def2	NumGt	True	Passed	Model Under Test Equivalent Model
ccc48def7f936c126a308c9b1a5fa7e02d5d1c82	Apalache	Def2	NumGt	False	Passed	Model Under Test Equivalent Model
a41a411a1451abac9eef6a87e9319a6c9e71fcf1	Apalache	Def2	NumGe	True	Passed	Model Under Test Equivalent Model
d7524c0aef0d29dab1d97d4387712709b3cfaded	Apalache	Def2	NumGe	False	Passed	Model Under Test Equivalent Model
0ab292c729f6953158d809145c6d25d39b212e73	Apalache	Def2	NumLt	True	Passed	Model Under Test Equivalent Model
863e7e9cf435a1128cff3be4d25915af68421adb	Apalache	Def2	NumLt	False	Passed	Model Under Test Equivalent Model
7bd152a2ac7e341c0b5fbd5fb23ccccbc90b89f4	Apalache	Def2	NumLe	True	Passed	Model Under Test Equivalent Model
79a0caff2b35314ded504a565e9f3150c6c190a7	Apalache	Def2	NumLe	False	Passed	Model Under Test Equivalent Model
8ec0857ab1662591954e732e1a6e76e81800af37	Apalache	Def2	DefFun	True	Passed	Model Under Test Equivalent Model
ad3657825096944a086bc59fce0b84d56516d1d8	Apalache	Def2	DefFun	False	Passed	Model Under Test Equivalent Model
9c63314d5ed8348dbcceefcfd3add017c7c82d3b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDefFun	True	Passed	Model Under Test Equivalent Model
4590ef08e87f6938d6b35f0f18bce4e0c3ffe7d1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDefFun	False	Passed	Model Under Test Equivalent Model
11eab07035be22d4ba5176aa95e1f2a78e247547	Apalache	Def2	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c442d92911b870e7aca35aed9d0b9f52d5e6cfb4	Apalache	Def2	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
f85a5d7f96256a5f28be499556a17e0e63cafafc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
a59353e1e9b2771d9058ed00a0975d1000ef23b1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
a9dc4ddf938e4e0a15ef4992389cde15681cb292	Apalache	Def2	Def0	True	Passed	Model Under Test Equivalent Model
3380455cb55bc4755f17c2e1f680a0a6aa2524c4	Apalache	Def2	Def0	False	Passed	Model Under Test Equivalent Model
e150b1994b29261eb5a26753c27a382e6a320f1c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef0	True	Passed	Model Under Test Equivalent Model
e6c8c03fbd4eedec04de3fb16c449d310530d726	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef0	False	Passed	Model Under Test Equivalent Model
4f7dff44674ac3bf60821a11520c7dc5c272c904	Apalache	Def2	Def1	True	Passed	Model Under Test Equivalent Model
8e0f40420214dbaa346ffb4c2399f875b48761ea	Apalache	Def2	Def1	False	Passed	Model Under Test Equivalent Model
e2bd1b9761a99988f83db9a2e754a85cecf02b3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1	True	Passed	Model Under Test Equivalent Model
2fd546bd9fbe1b9d5694946fb81b3b22eb16d778	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1	False	Passed	Model Under Test Equivalent Model
9610d77a0d777dea600be2d3618395459dc4b4af	Apalache	Def2	Def2	True	Passed	Model Under Test Equivalent Model
655f96f3e676dc265de8e30d5d4a1dd8bb349f28	Apalache	Def2	Def2	False	Passed	Model Under Test Equivalent Model
47596f079f48816589345499ac8d3efc5f0c799c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef2	True	Passed	Model Under Test Equivalent Model
97433d558057bdcf1b47e19f1cfdf3b841565f0e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef2	False	Passed	Model Under Test Equivalent Model
886dbe487d19f5085994d56d2a94f9f2412581db	Apalache	Def2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
af818a3b8170cd55dc552bee878d84c7e5374956	Apalache	Def2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
35ff1c51f4e66e93bef48e7e07f8c4fadccbaf86	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
3532ec35c70e1efa214f09b4457d34cd99eb68ed	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
0b8d3eeb156e6404b8267888b25dd371648440db	Apalache	Def2	Extends	True	Passed	Model Under Test Equivalent Model
c4f42ff1fe38eb7ce257572c612b7d4806cda436	Apalache	Def2	Extends	False	Passed	Model Under Test Equivalent Model
05de0a4c79932e4f13843eb3871d275c94dbd6a2	Apalache	Def2	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
78ad3449460deaa076101c9a2104cf9c5b9682df	Apalache	Def2	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
f5ffdcc192b654c511dfe1547cea6b3c43b263e4	Apalache	Def2	Variable	True	Passed	Model Under Test Equivalent Model
aae4189fe4a6c3c92b2ea089334884cdb6b43836	Apalache	Def2	Variable	False	Passed	Model Under Test Equivalent Model
63f11c4391bef89f03302708a499d73fb1bf0a9b	Apalache	Def2	Constant	True	Passed	Model Under Test Equivalent Model
29194c0ca895d1bdee2f0a07721977301f11a81b	Apalache	Def2	Constant	False	Passed	Model Under Test Equivalent Model
9abe9da6d0107f2b7836fba04629ca560074008c	Apalache	Def2	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
e4a3ea94f0d9a014448565b7a5b46f334bd1dca2	Apalache	Def2	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
4cec99b460a522eaa437a76659511157105b5e87	Apalache	Def2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
61fa30f69767e6de44c58411acfa0e2607637348	Apalache	Def2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f0e6da1d8c2a37117863e1f5da5c56f80719831f	Apalache	Def2	Instance	True	Passed	Model Under Test Equivalent Model
5fd18f7379a02b0b52bda563781da23c7b04cb36	Apalache	Def2	Instance	False	Passed	Model Under Test Equivalent Model
fcc316fb579142497afbf39ae49d5ea25fe4bfdd	Apalache	Def2	InstanceWith	True	Passed	Model Under Test Equivalent Model
eeb1d274dbd3046343fc5f283c710a850c18d526	Apalache	Def2	InstanceWith	False	Passed	Model Under Test Equivalent Model
ef7bc06d187fda5be568d1a665d9424c45047aae	Apalache	Def2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6121df629a4c820f1b699ae1c3cc1f0e269023aa	Apalache	Def2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5752d1922be794e90cbe9dd03d7e141091624faa	Apalache	Def2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8d20b08a1cebee29ae264362539cc57de33244f9	Apalache	Def2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
f9b6fe0166cfff174e65050a478551b1380874e5	Apalache	Def2	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
c0703757ca11b4e4a75c9718f836e9f825e967bd	Apalache	Def2	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
00ac9e72d4e134034bb8abe36fe5ff980bd43248	Apalache	Def2	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
226c89d57443f61c6f5fca59812e2962356e5b13	Apalache	Def2	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
46eaf6b3a202ea4b36c8e84dce6a50b387a1fcad	Apalache	Def2	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
8a5fe19240758ae8a4430fd39ce5d71ef41dde42	Apalache	Def2	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
07eb2e0cd6c7994fc29b65a72ab1175036adb035	Apalache	Def2	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
915202f38b696f86946f0b61b42288f8b6f4a83d	Apalache	Def2	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
d14e2a8ed65209964b1c61fed2a8afdf211e8229	Apalache	Def2	Enabled	True	Passed	Model Under Test Equivalent Model
c41d77004b232a189557e72df5e4b0320e12b8ce	Apalache	Def2	Enabled	False	Passed	Model Under Test Equivalent Model
2fe476cecc01ab3f24040cfb23605d05fc9347a5	Apalache	Def2	Cross2	True	Passed	Model Under Test Equivalent Model
d99fe496d634eca4a383ef80f9e4ad276447c204	Apalache	Def2	Cross2	False	Passed	Model Under Test Equivalent Model
e2b59b6019d43d9c052315afbb2ada97649eee4a	Apalache	Def2	Cross3	True	Passed	Model Under Test Equivalent Model
94cc36755144c0530b9f55fdb77494858ea34744	Apalache	Def2	Cross3	False	Passed	Model Under Test Equivalent Model
c1435a4c56f3b7fc6f833d5017a9e94ca77a4934	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))	Def2	FunSet	True	Passed	Model Under Test Equivalent Model
f7bba2dbfc4ef9a5e9c4679af535b66ba53c40ce	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))	Def2	FunSet	False	Passed	Model Under Test Equivalent Model
30d302330b4c188f08fff9230a0c54f7b387adde	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)	Def2	RecordSet	True	Passed	Model Under Test Equivalent Model
cf43c8409064f75c8df2b91b8a7f77aa6da6d122	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)	Def2	RecordSet	False	Passed	Model Under Test Equivalent Model
1c96e887e7267c21436ce26e23065b7cc93bb164	Apalache	Def2	SetDiff	True	Passed	Model Under Test Equivalent Model
43f024544c48bdf2bdf1aa3382c37d2da078f321	Apalache	Def2	SetDiff	False	Passed	Model Under Test Equivalent Model
819658afbbcfe1fc7cf04ec5e2dd20aed0d5fb54	Apalache	Def2	SetUnion	True	Passed	Model Under Test Equivalent Model
f2af1047b34c18b73b1241daaf0cc2600fad8322	Apalache	Def2	SetUnion	False	Passed	Model Under Test Equivalent Model
5aa9eda2e6b76d58126dd9b9f7db80b4effe0d1a	Apalache	Def2	SetIntersect	True	Passed	Model Under Test Equivalent Model
47f1d55e416f93bb337eee36b0def05bcc0fa8ab	Apalache	Def2	SetIntersect	False	Passed	Model Under Test Equivalent Model
0b7b47bfc760086539f2b75e1b35dc31da2dd2b7	Apalache	Def2	SubsetEq	True	Passed	Model Under Test Equivalent Model
ade048e30d16eb694211b7239fb2777c378550a2	Apalache	Def2	SubsetEq	False	Passed	Model Under Test Equivalent Model
2a5064f12a3ba0fa3b6dd8640b6d0cf0a50da1c3	Apalache	Def2	IfCond	True	Passed	Model Under Test Equivalent Model
42444f5d6bb35565b9b856437c962c30cfc347b6	Apalache	Def2	IfCond	False	Passed	Model Under Test Equivalent Model
3aa194f654755e3d83ab97ab76ab804a33e74d80	Apalache	Def2	IfThen	True	Passed	Model Under Test Equivalent Model
7cae04d802d9f8920865f06e0ca90d278d8172d6	Apalache	Def2	IfThen	False	Passed	Model Under Test Equivalent Model
07b433735b473dadc3920255e79dcd7c355f2fc8	Apalache	Def2	IfElse	True	Passed	Model Under Test Equivalent Model
66d32294bfca4af863836a156bf522f3d312da75	Apalache	Def2	IfElse	False	Passed	Model Under Test Equivalent Model
6f7d7f6e1bc850def3287d828f7ebebd4e8dc027	Apalache	Def2	Subset	True	Passed	Model Under Test Equivalent Model
bf161336fbd1d19a34f07befdb0be4c72e04d9aa	Apalache	Def2	Subset	False	Passed	Model Under Test Equivalent Model
6938e91ae31d69e441ea3ddf085864293faa47ce	Apalache	Def2	Domain	True	Passed	Model Under Test Equivalent Model
f86456e375091ecf8d689d642f95b8ca7d6395ee	Apalache	Def2	Domain	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
92246f4f5486d446b81e91b2b598c1749986a715	Apalache	Def2	Unchanged	True	Passed	Model Under Test Equivalent Model
35b2d2907c19ed4f70d69ab800469bbe9ba57bcd	Apalache	Def2	Unchanged	False	Passed	Model Under Test Equivalent Model
e9e0dad6062c57ceed970aa1d75dc3cc0e685db9	Apalache	Def2	Equivalence	True	Passed	Model Under Test Equivalent Model
05f464b5c8e365ce8fc370c92ad3df7b769707e9	Apalache	Def2	Equivalence	False	Passed	Model Under Test Equivalent Model
93648165f9336a85fbdb5ca7ea821ff59d9b2d1f	Apalache	Def2	StringEmpty	True	Passed	Model Under Test Equivalent Model
87d612263db866433beb6de2c0d1146a272fc5d6	Apalache	Def2	StringEmpty	False	Passed	Model Under Test Equivalent Model
edac4f7bf84888f6865e9d9a33907f8ab392213b	Apalache	Def2	String	True	Passed	Model Under Test Equivalent Model
32b908aca74a67976ed216cf589ba39463b4eb45	Apalache	Def2	String	False	Passed	Model Under Test Equivalent Model
9620f490d98fd71863be9084da626cd1da6d15e1	Apalache	Def2	SeqLen	True	Passed	Model Under Test Equivalent Model
95143c4d7303280f8814c2166d72d27abb04ae83	Apalache	Def2	SeqLen	False	Passed	Model Under Test Equivalent Model
db2eca54ef7663c0001fd7058187bf5a6f999678	Apalache	Def2	SeqConcat	True	Passed	Model Under Test Equivalent Model
ad422d7876902915b6bd55975397178e6cbf9816	Apalache	Def2	SeqConcat	False	Passed	Model Under Test Equivalent Model
29b72352e353fcd5b7e54f3104afdd61739627f4	Apalache	Def2	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a0274fefb9975a3124c878787412e784a6eece82	Apalache	Def2	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
4c2bb855f38d9f453cfbc8b4bb32983d3e653859	Apalache	Def2	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e3cd709498abaff57448d6f5eee062d2bebc3c32	Apalache	Def2	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
62b71f13c4c18a392adca55b5243fe4b1ccfaac5	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	Def2	NumRange	True	Passed	Model Under Test Equivalent Model
ef115f76f97bd0323ea612f9b9feba99125902a0	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	Def2	NumRange	False	Passed	Model Under Test Equivalent Model
757a4eb15d4a863cb0e7ca3796a07202eb29048b	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def2	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
741f7effd296bb748eff26e943d4936fa3d38ef3	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def2	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
5985dfc2276a73520ab930d5729aaf6c96ccf9df	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Def2	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
b1eee41470a09689a4c202b06e2b47bdd7426564	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Def2	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
cdd4c8f6b6768d673426c9abc9d2ec2cfc15245a	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def2	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
96ff50c0eefe8a00c20e00fa5f13363a6bf6e8d7	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def2	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
f073767a0be044aaee212991b2682b7ca4c77d70	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def2	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
cc4b9ddf044194d0bde8f43e46bd2585fca3394a	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def2	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
44ce1059682b5f1a11909f38e0d1c174a8a451cc	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def2	TlcEval	True	Passed	Model Under Test Equivalent Model
c8ffc069b76f2d8a382d1e9599043bc18572c630	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def2	TlcEval	False	Passed	Model Under Test Equivalent Model
54729ecfd9404f0e9dd464e2dd135381ad57f909	Apalache	Def2	BagBagToSet	True	Passed	Model Under Test Equivalent Model
0080b33a1a5101043e300c68e14e5eadf0d01823	Apalache	Def2	BagBagToSet	False	Passed	Model Under Test Equivalent Model
b6a3f49d52bdca27ef6d68c4875484984a95da13	Apalache	Def2	BagSetToBag	True	Passed	Model Under Test Equivalent Model
6bab95cf6c72efffaa48430a547848a5d6802f91	Apalache	Def2	BagSetToBag	False	Passed	Model Under Test Equivalent Model
0ce1b0a7f1b43b92550976dd0bbcd437331d081b	Apalache	Def2	BagBagIn	True	Passed	Model Under Test Equivalent Model
154469579c898ec753b801bfba189900a5cef82b	Apalache	Def2	BagBagIn	False	Passed	Model Under Test Equivalent Model
0b77f4c5213cae0c2113fd77c67f4255d4fe3ff9	Apalache	Def2	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
7e7165d9d19b8f78bff91ea946cac2394aebb33d	Apalache	Def2	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
2cba9ab9392ace3128d3eaffa9f21b58da1354ca	Apalache	Def2	BagAddBag	True	Passed	Model Under Test Equivalent Model
815dd45f2c34e92bf06a24c1ba86de0ef2ee45b0	Apalache	Def2	BagAddBag	False	Passed	Model Under Test Equivalent Model
92a099dfae86cc51a0413744d542e4319098f79d	Apalache	Def2	BagBagSub	True	Passed	Model Under Test Equivalent Model
8b36b8282d5a155a427a93e4d624a0620058f35f	Apalache	Def2	BagBagSub	False	Passed	Model Under Test Equivalent Model
794a0a57b654e7fc936842924c8326fe1b5ec947	Apalache	Def2	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
2470cd751c9848ce76997be47277ee1eeef5f45e	Apalache	Def2	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
0b8956f133536f400823b14df172c3e214f3606c	Apalache	Def2	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
bb9a8c693571b84d294a89f2b2c9efcd06e4213c	Apalache	Def2	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
8f3cf1a04409842750b15b0ba6f0bbcde4ff2aa0	Apalache	Def2	BagBagUnion	True	Passed	Model Under Test Equivalent Model
889fcf52483cd9b31f1aab78b34a240975a82c14	Apalache	Def2	BagBagUnion	False	Passed	Model Under Test Equivalent Model
bf3ff4e456d50185c5cf0f31c634f3cd14be5de2	Apalache	Def2	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
a63539ff92a3c29e91d00f59ad61bf6fa7d0d279	Apalache	Def2	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
1d4a25eb5fdba69d2eb86432472c0a83105a274a	Apalache	Def2	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
11175529657fef33aaccf74f03ba70bec3dbbc9e	Apalache	Def2	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
180e679660f905f76a72e02cf940738a9bb2757a	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def2	BagSubBag	True	Passed	Model Under Test Equivalent Model
34ba1569b059241b1ab7a9ce19eb7ff630d9431f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def2	BagSubBag	False	Passed	Model Under Test Equivalent Model
7ce48af7f6577b531e8da356ebb3693ef91484b4	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Def2	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
73851e03531ce3310850a15a7ee925185826574d	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Def2	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
4ef496c2d41a128c4ed5705def6be858b7f47c29	Apalache	Def2	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
0355b4fa1d2efa250a4be73d9e69526ade93757b	Apalache	Def2	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
b70103f7ebc6a092543c770f503696dc8a57ddd0	Apalache	Def2	SeqHead	True	Passed	Model Under Test Equivalent Model
06b80920a37ac5b4bc398c6f4dbbc115cf877711	Apalache	Def2	SeqHead	False	Passed	Model Under Test Equivalent Model
17ea59f1d1ecfec961e3a86480c1521d1e4781eb	Apalache	Def2	SeqTail	True	Passed	Model Under Test Equivalent Model
ddd4d20b831882982c7015bcc5b5c3379809f0a8	Apalache	Def2	SeqTail	False	Passed	Model Under Test Equivalent Model
ef7c9a82e1a4bd1445a92e0af274f6f7f56a8bff	Apalache	Def2	SeqAppend	True	Passed	Model Under Test Equivalent Model
94892b3c49573deee792f6bd06930640667422fa	Apalache	Def2	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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