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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
26fa79f8ca351171d75b9311ca686b995883faba	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Tuple	OneLineComment	True	Passed	Model Under Test Equivalent Model
55783730ae76e00b4bd38c2d69a3fd2e5b2a19bf	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Tuple	OneLineComment	False	Passed	Model Under Test Equivalent Model
812e862db26f00ce4214173e5e58c7514f32f6d3	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Tuple	MultiLineComment	True	Passed	Model Under Test Equivalent Model
219c33c1b83b8608747ca96a3b31da1dbb05374d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Tuple	MultiLineComment	False	Passed	Model Under Test Equivalent Model
ad629298d961e979e96ccd6114c7096c33c39648	Apalache	Tuple	BoolTrue	True	Passed	Model Under Test Equivalent Model
6c2fc7731b951382d425eda7b3268eebd74a1194	Apalache	Tuple	BoolTrue	False	Passed	Model Under Test Equivalent Model
af71b617f6c925b7b358c75d9f35b54372448725	Apalache	Tuple	BoolFalse	True	Passed	Model Under Test Equivalent Model
74da46e71fd9a4a94b7eb4ed132fdff8b6f15cfb	Apalache	Tuple	BoolFalse	False	Passed	Model Under Test Equivalent Model
63b021c22c29fe8c2721b1b2f26d7b2c31eaba31	Apalache	Tuple	BoolSet	True	Passed	Model Under Test Equivalent Model
9197e19d5abc642cb418727aa3e0ffd6f8193fbc	Apalache	Tuple	BoolSet	False	Passed	Model Under Test Equivalent Model
7d0cc700a1b5de035a1c59394704c3e3dc86a4bb	Apalache	Tuple	And	True	Passed	Model Under Test Equivalent Model
c8c1457d8f7191d7f00434be8972935fc2c52cfd	Apalache	Tuple	And	False	Passed	Model Under Test Equivalent Model
b9b1d4dd33cebb0724f2382d36b93925655f4ce3	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Tuple	AndMultiLine	True	Passed	Model Under Test Equivalent Model
4212267e105c67ccfd2b1d732f0f53ea9f05f89c	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Tuple	AndMultiLine	False	Passed	Model Under Test Equivalent Model
5842377af310f168ee08b9d3cee74a8650d9253d	Apalache	Tuple	Imply	True	Passed	Model Under Test Equivalent Model
31a79485dbf0934884f59d842cd2587111e3b1cf	Apalache	Tuple	Imply	False	Passed	Model Under Test Equivalent Model
7fe9cc35ff2736f1900a1d59ffec7fac2f00d4bc	Apalache	Tuple	Not	True	Passed	Model Under Test Equivalent Model
a629994cc4319d21ce547199934c3a8faabff995	Apalache	Tuple	Not	False	Passed	Model Under Test Equivalent Model
28a01c475442693eeac5f71cffb6d1449ea14964	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Tuple	Or	True	Passed	Model Under Test Equivalent Model
79df42b01dbfabc1028f849fc6f0996e281b6341	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Tuple	Or	False	Passed	Model Under Test Equivalent Model
282423a3bd7f981556404a76cbb3c1637c1f6d4f	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Tuple	OrMultiLine	True	Passed	Model Under Test Equivalent Model
70642adfb95737f0d34b9834a7cce6ac7f5b9be8	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Tuple	OrMultiLine	False	Passed	Model Under Test Equivalent Model
af4a3599fb50cffa9ca94cb3560cd629d9430fdc	Apalache	Tuple	Eq	True	Passed	Model Under Test Equivalent Model
8beb62fe934a7f6b64d01aa70486e5d10455f29f	Apalache	Tuple	Eq	False	Passed	Model Under Test Equivalent Model
b71aae35d3b7496923b3f418b97c5f064dd3b762	Apalache	Tuple	Ne	True	Passed	Model Under Test Equivalent Model
d6c2fdc837aa23619fc3136cb3913e5f36d82a75	Apalache	Tuple	Ne	False	Passed	Model Under Test Equivalent Model
5f44d699383209dae983f7021b9d4e9963284ba7	Apalache	Tuple	Let	True	Passed	Model Under Test Equivalent Model
b06f363f7a7df14c778575e9b1c57d4f2d718755	Apalache	Tuple	Let	False	Passed	Model Under Test Equivalent Model
a06d3509b3042b12f484ad8773ca68a9a3955487	Apalache	Tuple	SetEmpty	True	Passed	Model Under Test Equivalent Model
df2fe4b17e749b9b183caf04a37288bf8eb2a60b	Apalache	Tuple	SetEmpty	False	Passed	Model Under Test Equivalent Model
b08c66c4aef9f7fecb2a8e1a42412cf13899e924	Apalache	Tuple	Set0	True	Passed	Model Under Test Equivalent Model
c2baf01312a74714378bc1c384c85b47b3545310	Apalache	Tuple	Set0	False	Passed	Model Under Test Equivalent Model
b2414c01bde639a3d0f4d9e329dc08ad58d0c123	Apalache	Tuple	Set1	True	Passed	Model Under Test Equivalent Model
c6105fd0ebbcdb24d6b410982549f6bfdeef895f	Apalache	Tuple	Set1	False	Passed	Model Under Test Equivalent Model
50d76a7ffb386dba2f7c6e0661680114768d2a5d	Apalache	Tuple	Set2	True	Passed	Model Under Test Equivalent Model
58d62a5b86a27abadd571af734e6f5cd614135aa	Apalache	Tuple	Set2	False	Passed	Model Under Test Equivalent Model
9667ab6bef041f381f420746e498324129347d65	Apalache	Tuple	Fun	True	Passed	Model Under Test Equivalent Model
ad1a4a6496a70c9d978f097a5e816addaa55020f	Apalache	Tuple	Fun	False	Passed	Model Under Test Equivalent Model
25c21ddc7b263b9d3a65fc8806effc34c3831dd0	Apalache	Tuple	In	True	Passed	Model Under Test Equivalent Model
95f8301dd719ec48a1bd7285189b7ee0e5077f40	Apalache	Tuple	In	False	Passed	Model Under Test Equivalent Model
0dc405b7745772511341ff5f00e5aecbaa914b2a	Apalache	Tuple	NotIn	True	Passed	Model Under Test Equivalent Model
9f504b0ab7a7aaee16081a28bf9a7dc7755252b1	Apalache	Tuple	NotIn	False	Passed	Model Under Test Equivalent Model
b6d5387799c3c02774273822428add677ebbabe3	Apalache	Tuple	Exists	True	Passed	Model Under Test Equivalent Model
5275b153b8e3997b7202511c7650a7430b9b57e4	Apalache	Tuple	Exists	False	Passed	Model Under Test Equivalent Model
80dd892f23ac0f4b3c46a7f5fc6a8f64d7493d09	Apalache	Tuple	Forall	True	Passed	Model Under Test Equivalent Model
fc628c3060b282665e1a3bf8fb6cf641046af8a5	Apalache	Tuple	Forall	False	Passed	Model Under Test Equivalent Model
bb6d284e3b0ba9dede873a4d342122ce1d325869	Apalache	Tuple	Choose	True	Passed	Model Under Test Equivalent Model
d099b6e91f831100796e0b5824748f01340e7f72	Apalache	Tuple	Choose	False	Passed	Model Under Test Equivalent Model
b451bed4b1c90367d80577c8fc18e3acb42ff3fd	Apalache	Tuple	Record	True	Passed	Model Under Test Equivalent Model
977580a0cf99031218005bf1fbef021e4bde4c09	Apalache	Tuple	Record	False	Passed	Model Under Test Equivalent Model
16f43764269976b57ced9aca4522dc8b762c4c5f	Apalache	Tuple	Tuple	True	Passed	Model Under Test Equivalent Model
bd090276233e5f62402731dc660b8658062c5d6c	Apalache	Tuple	Tuple	False	Passed	Model Under Test Equivalent Model
17449fd4c0dd45f3cf5cad552efb781790e05592	Apalache	Tuple	TupleEmpty	True	Passed	Model Under Test Equivalent Model
b741e539363c40365ac130044551e310649128bf	Apalache	Tuple	TupleEmpty	False	Passed	Model Under Test Equivalent Model
a0155333d2e85b9d251af31d65674989009b9196	Apalache	Tuple	FunApp	True	Passed	Model Under Test Equivalent Model
5a99b3df741b170146560c947c208649f16eb956	Apalache	Tuple	FunApp	False	Passed	Model Under Test Equivalent Model
ffa5ab3dc9caa70a581b7893f64c5cf958243ba4	Apalache	Tuple	Prime	True	Passed	Model Under Test Equivalent Model
6cd42de79928deaf5ba9d67c2d8840029e9d33db	Apalache	Tuple	Prime	False	Passed	Model Under Test Equivalent Model
e6edc8fe554760dd8dbab07ff83a54e3a8435fc8	Apalache	Tuple	NumZero	True	Passed	Model Under Test Equivalent Model
6637e9226e7315f93cb511edf3dbc27cb30f2870	Apalache	Tuple	NumZero	False	Passed	Model Under Test Equivalent Model
2dd694ed9f39b93f06fc850536719138629b4085	Apalache	Tuple	NumOne	True	Passed	Model Under Test Equivalent Model
cf0d8468d54cfc784606b4c2f1eb6d1ec6aa6dca	Apalache	Tuple	NumOne	False	Passed	Model Under Test Equivalent Model
b2c57204d18f38a767c6e930b353cac8cd2d601a	Apalache	Tuple	NumMaxInt	True	Passed	Model Under Test Equivalent Model
0a49a52e9af2326e3317daedf8719bee68279ff1	Apalache	Tuple	NumMaxInt	False	Passed	Model Under Test Equivalent Model
4514fabef14e15779b9e522d44cd90c5bc0ba32a	Apalache	Tuple	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1c53d4d2369968fa351d33aae282a48083ca4c64	Apalache	Tuple	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a6b60c3dd223f5a602a6f8a1b27082e80a655312	Apalache	Tuple	NumPlus	True	Passed	Model Under Test Equivalent Model
4939f273c92e847f80f294250ce5ac789be8ecd9	Apalache	Tuple	NumPlus	False	Passed	Model Under Test Equivalent Model
0b233e8419db3e846bfd82db33ca1408739a9378	Apalache	Tuple	NumMinus	True	Passed	Model Under Test Equivalent Model
be4be70842a44a17016c4f8c9c6fdc38c3bd5141	Apalache	Tuple	NumMinus	False	Passed	Model Under Test Equivalent Model
bc342ffd4fd7d9b18801e568f8d79ddfb1250acf	Apalache	Tuple	NumMul	True	Passed	Model Under Test Equivalent Model
189f375274948672e183e3d285f4daada24c9782	Apalache	Tuple	NumMul	False	Passed	Model Under Test Equivalent Model
7c6b9fc9db704c10fccd78ff37c5e59206b42432	Apalache	Tuple	NumDiv	True	Passed	Model Under Test Equivalent Model
593baffc6ec6ce8beeaa8d3596c2976730e15bda	Apalache	Tuple	NumDiv	False	Passed	Model Under Test Equivalent Model
c8acbc3bfe9b478b5055eacfed4f86fcab658f3e	Apalache	Tuple	NumMod	True	Passed	Model Under Test Equivalent Model
75e5789253948a7a8405d957690d38178bfb4b6d	Apalache	Tuple	NumMod	False	Passed	Model Under Test Equivalent Model
9533adc9e3735f374f2e35161c3ea9bb828bd57c	Apalache	Tuple	NumPow	True	Passed	Model Under Test Equivalent Model
275359681f91d9410f3b9e6d445bcfb6d2fd3f4b	Apalache	Tuple	NumPow	False	Passed	Model Under Test Equivalent Model
c6881ac37be1382a4ccb97bbfc8363bddbf529ca	Apalache	Tuple	NumGt	True	Passed	Model Under Test Equivalent Model
45b5b623e2e91946e5f7a33d2f4300ed2d7866d4	Apalache	Tuple	NumGt	False	Passed	Model Under Test Equivalent Model
8475af864ef7a1f9e7d542d4014f431e294ba422	Apalache	Tuple	NumGe	True	Passed	Model Under Test Equivalent Model
502b0b3e13b0487be24a3a69bb1c7ea1b2da32c4	Apalache	Tuple	NumGe	False	Passed	Model Under Test Equivalent Model
ac60bcaa95408d9495234fe8c6fd85dc6228d742	Apalache	Tuple	NumLt	True	Passed	Model Under Test Equivalent Model
a8fba3ed69add55e55362f5c5f2ecfd4e4917887	Apalache	Tuple	NumLt	False	Passed	Model Under Test Equivalent Model
780f01aebab0fb32cefe97491f73ce5efba586ce	Apalache	Tuple	NumLe	True	Passed	Model Under Test Equivalent Model
b7659c7484810d6235b3b75c17a7ad548a652ec9	Apalache	Tuple	NumLe	False	Passed	Model Under Test Equivalent Model
8876dd208c6e63080d7cd2a12449bf36e7a31054	Apalache	Tuple	DefFun	True	Passed	Model Under Test Equivalent Model
b9ae0ab59a1e6991bb0f2d86cc64df5cdc0cd7eb	Apalache	Tuple	DefFun	False	Passed	Model Under Test Equivalent Model
a56e1d2308e2a9d1b0caf19e84a266570ec55bd5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDefFun	True	Passed	Model Under Test Equivalent Model
423a0e101adda578d31e9eff0db322f3bc6c62e1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDefFun	False	Passed	Model Under Test Equivalent Model
3ffa895c2f3e08330d3676e3f7a2654726006619	Apalache	Tuple	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ea775a9f64e76b3c49bbaff0879293e4bad1b115	Apalache	Tuple	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
1beec9f992a1c2db76136d4e253a53a3563f8482	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
e0def8fa59cebe52d939806ac9eba78520fb27a7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
69219c18016c35073af7ccb28e1a1c64ed263b77	Apalache	Tuple	Def0	True	Passed	Model Under Test Equivalent Model
c5251c8bfc953eb4a539d288be22c48eb8fb9c0a	Apalache	Tuple	Def0	False	Passed	Model Under Test Equivalent Model
c89ad70f5909d1634a4858ccaf0f5e71d03eaa7c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef0	True	Passed	Model Under Test Equivalent Model
7f645432c8f497ceec16e5709e7f57bb778eaaee	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef0	False	Passed	Model Under Test Equivalent Model
9e2498986cddda888e87d1e0569c34eedbecb3f0	Apalache	Tuple	Def1	True	Passed	Model Under Test Equivalent Model
d5dcf00909b610eb84e9860460ebcb1cca052e25	Apalache	Tuple	Def1	False	Passed	Model Under Test Equivalent Model
c8f59f222c310b299ad44b3c0a13b3134079e3c7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1	True	Passed	Model Under Test Equivalent Model
3687a099728547cad5d0cceb6f67fda76d67f3fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1	False	Passed	Model Under Test Equivalent Model
4751cb731462ecee57901c19b11f6b57a6587a9b	Apalache	Tuple	Def2	True	Passed	Model Under Test Equivalent Model
ff032577c389c4da86ae4d08fe4d16f122470d74	Apalache	Tuple	Def2	False	Passed	Model Under Test Equivalent Model
95dea156b252b9360aa133693936c8260a8490ea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef2	True	Passed	Model Under Test Equivalent Model
1336301780c718aebf8dcde71936080affe4939c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef2	False	Passed	Model Under Test Equivalent Model
a9ab769ce0d63a6c72c56a96f2f4bdb90e266836	Apalache	Tuple	Def1Recursive	True	Passed	Model Under Test Equivalent Model
5ac494f7dac2038fd1580b152c47ca0e0e18abd2	Apalache	Tuple	Def1Recursive	False	Passed	Model Under Test Equivalent Model
8bc34a20920c633c741bcdbc4943e38f55bc952b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
c11e22f10461f29f1c232e1b79481457c731c37e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
36179da3cdecb255a9b9c64d1083cb6f5b629117	Apalache	Tuple	Extends	True	Passed	Model Under Test Equivalent Model
0f249ff5926d5f8bebd254be3e9354e681610dd8	Apalache	Tuple	Extends	False	Passed	Model Under Test Equivalent Model
1e48acb5e1c7ba05b0474457873824bc750bb9fc	Apalache	Tuple	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
06fdaf2864b195d36f2fc90d3804c23de6d90467	Apalache	Tuple	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
4d5ada87a9459a3ef877ec250a89ca43dbd4cc0c	Apalache	Tuple	Variable	True	Passed	Model Under Test Equivalent Model
258fdd3a9e4f72ada553a3a4f167e2d577a22627	Apalache	Tuple	Variable	False	Passed	Model Under Test Equivalent Model
72710a698f04e3448b202d50b937355e113b1da4	Apalache	Tuple	Constant	True	Passed	Model Under Test Equivalent Model
b22f645a63240c3ba819cedcfd9edca70634c63e	Apalache	Tuple	Constant	False	Passed	Model Under Test Equivalent Model
d7003b02508198f5e58991c2479b40d473ab2970	Apalache	Tuple	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
caefe49b56158967039add377b56e4fa4f8230cd	Apalache	Tuple	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
707225cecdc27d6006c7797de09670acefbf0b1a	Apalache	Tuple	ConstantRank1	True	Passed	Model Under Test Equivalent Model
93fe9d3a8d62b1fbe8f6a137ae4481e08c1075d0	Apalache	Tuple	ConstantRank1	False	Passed	Model Under Test Equivalent Model
bbda4c7f9cbbf81173a1dc21ca7e69b643124798	Apalache	Tuple	Instance	True	Passed	Model Under Test Equivalent Model
a1ea917ae03ea051d23a5e2a8b8280102b8092d7	Apalache	Tuple	Instance	False	Passed	Model Under Test Equivalent Model
d0c4099917838a278106d93a4c366a53a3867132	Apalache	Tuple	InstanceWith	True	Passed	Model Under Test Equivalent Model
0c423aa30ce2e8288d3e136455d25d1c352066cf	Apalache	Tuple	InstanceWith	False	Passed	Model Under Test Equivalent Model
a72d3d754bb87c4dbbeb784b64d40ae49ba33bc9	Apalache	Tuple	InstanceNamed	True	Passed	Model Under Test Equivalent Model
33c90f086c248201ec6e8ff7f029e2b2cd3d6713	Apalache	Tuple	InstanceNamed	False	Passed	Model Under Test Equivalent Model
5e730473755d622e9fdc833f101067f5349988a0	Apalache	Tuple	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
789e04bf94c0aa45e9540e6379346fd492fade5f	Apalache	Tuple	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c7401a45a520b4aeec216d64a63dc8be8dde3166	Apalache	Tuple	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
b5b109cbac6b1d9a2b9acb47725bd3508808febc	Apalache	Tuple	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
a2079af3156cce231276a263ebc687f78940913e	Apalache	Tuple	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
93d80ba6959dca2c998868bb7b3be4dba72d9fc7	Apalache	Tuple	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
883ca002727863217797431dfef859101f820db4	Apalache	Tuple	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
ac1a3f8f0189fd960fa26af042e8cd391349d826	Apalache	Tuple	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
a31cfc8235c921b5a345e3b7daa0589d9983dc89	Apalache	Tuple	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
becf1209fec9507150f782ba9c95417f4985a998	Apalache	Tuple	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
4b8587d69d6a7a29621a34293377a539bb891a81	Apalache	Tuple	Enabled	True	Passed	Model Under Test Equivalent Model
fb5a421db009cc7daa6b956d87ac8e520d6fa375	Apalache	Tuple	Enabled	False	Passed	Model Under Test Equivalent Model
356e9807c79bb21eaeb56865048e6ca59cc5e229	Apalache	Tuple	Cross2	True	Passed	Model Under Test Equivalent Model
504943cdf3249bbd4730f08c51ee63de8fea6dbc	Apalache	Tuple	Cross2	False	Passed	Model Under Test Equivalent Model
b740ae6e99d99b0968343a41c337f9056da162aa	Apalache	Tuple	Cross3	True	Passed	Model Under Test Equivalent Model
648f4928bffe5c58e2d11f6b418abda524897d62	Apalache	Tuple	Cross3	False	Passed	Model Under Test Equivalent Model
768d0de8dfa1788229404246656910273709db00	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))	Tuple	FunSet	True	Passed	Model Under Test Equivalent Model
06c19d5200f72465e1c6fde1870f237753878b97	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))	Tuple	FunSet	False	Passed	Model Under Test Equivalent Model
69641981ea412acdd2cd50eb951473efa31fc39a	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)	Tuple	RecordSet	True	Passed	Model Under Test Equivalent Model
cffb8017ab0b9102263726a29a2df3ac8f67e7cf	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)	Tuple	RecordSet	False	Passed	Model Under Test Equivalent Model
492a9277ceefac68d063ea38c36e3e807427746a	Apalache	Tuple	SetDiff	True	Passed	Model Under Test Equivalent Model
3fcbab508bcee2919f669ef4562aefdcb7eae11b	Apalache	Tuple	SetDiff	False	Passed	Model Under Test Equivalent Model
83b7087957e0d54218e8f88b9f53ab59e338fdda	Apalache	Tuple	SetUnion	True	Passed	Model Under Test Equivalent Model
42708250cccd38c55e5f4155cebb480b56bf5d75	Apalache	Tuple	SetUnion	False	Passed	Model Under Test Equivalent Model
e884015cf6ef598ef87a4f12c9958726897b9d4b	Apalache	Tuple	SetIntersect	True	Passed	Model Under Test Equivalent Model
208dd502184bb7e39f56e4fc065ec0b4c7ea6213	Apalache	Tuple	SetIntersect	False	Passed	Model Under Test Equivalent Model
4611a026b2d4ebe6312d0ecc7b78ab189375b5d9	Apalache	Tuple	SubsetEq	True	Passed	Model Under Test Equivalent Model
b2562641e8ca5dfe14df8d27c21636daa22f863c	Apalache	Tuple	SubsetEq	False	Passed	Model Under Test Equivalent Model
add06bf8016c001fc83a4cc7c0d9cad3e29317e0	Apalache	Tuple	IfCond	True	Passed	Model Under Test Equivalent Model
8558109aebc21b5b86646141fec152fe7a9f3d4b	Apalache	Tuple	IfCond	False	Passed	Model Under Test Equivalent Model
11bfcaf26cdbe36a87b1a1f9467058c182b402ae	Apalache	Tuple	IfThen	True	Passed	Model Under Test Equivalent Model
6cbdccbf733a15752c6987536ffb89c3163a2ab4	Apalache	Tuple	IfThen	False	Passed	Model Under Test Equivalent Model
65d7d6f1b0a68b10f2af8ffafc803175db1d6572	Apalache	Tuple	IfElse	True	Passed	Model Under Test Equivalent Model
19c50c9180ea68887039bfff20b3b51a7a479d33	Apalache	Tuple	IfElse	False	Passed	Model Under Test Equivalent Model
21d5024b84b202c94a8d3d09f0dd7f698a898fb6	Apalache	Tuple	Subset	True	Passed	Model Under Test Equivalent Model
298f62286577a6b40d50c6f414d893351b7b33b6	Apalache	Tuple	Subset	False	Passed	Model Under Test Equivalent Model
f3ed111a8d1326e67420c50ca6516cbe6ad5ac52	Apalache	Tuple	Domain	True	Passed	Model Under Test Equivalent Model
bd0bae219c1b4fbd22604d9f2df93c6337d1385f	Apalache	Tuple	Domain	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
ae5b375526ef1492f56fa635a1e1a7a394ff60f5	Apalache	Tuple	Unchanged	True	Passed	Model Under Test Equivalent Model
62d706aa5812961532957cbe4352568b2cd5d1dd	Apalache	Tuple	Unchanged	False	Passed	Model Under Test Equivalent Model
59f4124d3f83f791b68a76168266bbef58877845	Apalache	Tuple	Equivalence	True	Passed	Model Under Test Equivalent Model
03d6ec41cca99ac11812e297ffe0739943f08085	Apalache	Tuple	Equivalence	False	Passed	Model Under Test Equivalent Model
37309d06c3d4c758902c51cd24092e67dec65bbf	Apalache	Tuple	StringEmpty	True	Passed	Model Under Test Equivalent Model
dd1312e89aa0bdaffe24e6f01829d47ecc4a0ecd	Apalache	Tuple	StringEmpty	False	Passed	Model Under Test Equivalent Model
455e537ee8fbfd2db28348ef757c04275da898c2	Apalache	Tuple	String	True	Passed	Model Under Test Equivalent Model
9e507c29fa869789c7ce1fbab6e4c8f2d792e116	Apalache	Tuple	String	False	Passed	Model Under Test Equivalent Model
ce41463fba3c4061219ce4b6706a88a534b64655	Apalache	Tuple	SeqLen	True	Passed	Model Under Test Equivalent Model
97517ec5860a2ef23207ff92bfeddb625fdddd16	Apalache	Tuple	SeqLen	False	Passed	Model Under Test Equivalent Model
11af5c5bbd29ba3ff9159264e6f6cdfb0f46d74a	Apalache	Tuple	SeqConcat	True	Passed	Model Under Test Equivalent Model
bb50326ba044ae57c8ccc81a0cbb1bc353802e38	Apalache	Tuple	SeqConcat	False	Passed	Model Under Test Equivalent Model
641eab039c25e6192c002c69d91c082609031cae	Apalache	Tuple	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
b61066b4c2c8d54249334c3039e89ae20d47e205	Apalache	Tuple	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b87925cc512d9a67b42d9a7e29395493209ce876	Apalache	Tuple	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
082ab9a25322b349bdc78e5af67e2706f544bbf6	Apalache	Tuple	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
740d7a51f709eddef70c59036e0a660a72d1ca88	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	Tuple	NumRange	True	Passed	Model Under Test Equivalent Model
40b91d942f31d37b0d65b28d13fed2fdec0e2f47	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	Tuple	NumRange	False	Passed	Model Under Test Equivalent Model
0db0dbcfc5c2f883fdbe09f4e831d91a3f116873	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Tuple	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
06e360c0121db482f1bd050e82e105edc1398839	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Tuple	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
218a3f8a6e922344145e1468873c778945d0819f	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]]	Tuple	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
051af3a6656dd41a97a18ef63cd0de6a781cef88	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]]	Tuple	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
2185f55e8fb9b2602a037c4ded9853def5fd1f99	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Tuple	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
2bd7f0d01401219e1a7318f353c22e0ae97706d0	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Tuple	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
7b78152ff34d8328e78830c7543ac2884abb77d9	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Tuple	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
95232a7fe8838fda3466c2a10673aa9987dfa897	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Tuple	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
a87198c32e59b0635ac3035d62df01ae341703d0	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Tuple	TlcEval	True	Passed	Model Under Test Equivalent Model
fbb4668d6ac60d60cb077e8a4db53c4dcc7e6809	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Tuple	TlcEval	False	Passed	Model Under Test Equivalent Model
962dc626dc54ac42b063a955d5d4a8e9b250d41a	Apalache	Tuple	BagBagToSet	True	Passed	Model Under Test Equivalent Model
b2d3b95c0a4fd0e460b15372485ea57f6bc01919	Apalache	Tuple	BagBagToSet	False	Passed	Model Under Test Equivalent Model
8267f4a4d07a830f9b51ae7bae607a55147284ec	Apalache	Tuple	BagSetToBag	True	Passed	Model Under Test Equivalent Model
5ca22409db65f3bcbe06301405ffb81b74660696	Apalache	Tuple	BagSetToBag	False	Passed	Model Under Test Equivalent Model
cd5694b4f17bfd4678fcfbbff22b77023e98b5af	Apalache	Tuple	BagBagIn	True	Passed	Model Under Test Equivalent Model
be697d1553a5447cc694dac6324a57a8be6d9e6e	Apalache	Tuple	BagBagIn	False	Passed	Model Under Test Equivalent Model
f126b1af4786ccab1e9e152e07c3d9c9c9b81e9e	Apalache	Tuple	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
df484dcb274d202b3da495882ae17645dcfe51f3	Apalache	Tuple	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
021f8c50e8371900a1abea679a0d917e44e83812	Apalache	Tuple	BagAddBag	True	Passed	Model Under Test Equivalent Model
ff288f228b8c035c78c34a30aafb319cfa71b7ba	Apalache	Tuple	BagAddBag	False	Passed	Model Under Test Equivalent Model
2a034421e75788ffb8dcc4261b7d70a6896ff4ee	Apalache	Tuple	BagBagSub	True	Passed	Model Under Test Equivalent Model
4b2b715781f8a6fc232f685b6fea48a1aded8937	Apalache	Tuple	BagBagSub	False	Passed	Model Under Test Equivalent Model
1d808d807512bb234edc0f452869be1d0ef9179e	Apalache	Tuple	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6520a8e766e47c4930f21ba3d9503a730ee10e35	Apalache	Tuple	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
878edb6bd8b789b7451a8686eb6b86908e9f1afb	Apalache	Tuple	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
106b6926e5ac7957fec9fd938328bd8fc234b2bf	Apalache	Tuple	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
a5cd5f06f964f426f668ec8a517a2b3324a1819d	Apalache	Tuple	BagBagUnion	True	Passed	Model Under Test Equivalent Model
c3a491ec845099f963e188332f3061de6cb87295	Apalache	Tuple	BagBagUnion	False	Passed	Model Under Test Equivalent Model
4d09ed4ae74e943d542a8b1a921103fd672539a4	Apalache	Tuple	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
da03cafd367f828bc3a1680c6bbbb236db5cd7ea	Apalache	Tuple	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
eb884c0c4dcfdd7ce27f74e8ba43952fdb83941b	Apalache	Tuple	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
150c211b2360f68978cefde954959aa595d71c9b	Apalache	Tuple	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
f8ec13c6990cd452a166c65afc51b21e9ff0cffd	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Tuple	BagSubBag	True	Passed	Model Under Test Equivalent Model
ae8710e2ef3f88fbbd2efda17fc34b004dc1982f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Tuple	BagSubBag	False	Passed	Model Under Test Equivalent Model
a877f8743dd72f13b3b157fc80a5b7e7cafa14f3	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)	Tuple	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
8bd05c9f57f41718374325764cc14d7c93078d6d	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)	Tuple	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
b8d4ae98e9ba57fa963bf6372afb211dda9fa90f	Apalache	Tuple	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
f98db16688fcc5753b9397e807e939c70e416eb3	Apalache	Tuple	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
f4a92ca39cab876c6bc445e6a5bd2a4bbcc85279	Apalache	Tuple	SeqHead	True	Passed	Model Under Test Equivalent Model
86ec29bf95bac72da2af46d6617d37b48e30ba46	Apalache	Tuple	SeqHead	False	Passed	Model Under Test Equivalent Model
47cbabfc2ff17618de02a039d9fe2df75b57492a	Apalache	Tuple	SeqTail	True	Passed	Model Under Test Equivalent Model
656471cabc670f639b4a744100dba6c2014c076d	Apalache	Tuple	SeqTail	False	Passed	Model Under Test Equivalent Model
b207a68b4dcb3023d54f2d81cd7a354de4b51307	Apalache	Tuple	SeqAppend	True	Passed	Model Under Test Equivalent Model
46ffb4e681e2efeefc2965f9076df23bfe4060e0	Apalache	Tuple	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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