Tests by plug feature Def1; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
44bf54955398767fc7cfc64839e1b9ec207ce71d	Apalache	And	Def1	True	Passed	Model Under Test Equivalent Model
52984650b5621b880542b7b92c29bab28df7b2b7	Apalache	And	Def1	False	Passed	Model Under Test Equivalent Model
e97582bf9a63976a71de9b9ffac5459da5338af6	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def1	True	Passed	Model Under Test Equivalent Model
d128f73e0c4352b7ffc9d2fad7754145333b0327	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def1	False	Passed	Model Under Test Equivalent Model
1ef80585e15bc8fe3f60e54f56a876a645af0e64	Apalache	Imply	Def1	True	Passed	Model Under Test Equivalent Model
33ff1638639ea7e8feabc7ebdb269e059435f1c4	Apalache	Imply	Def1	False	Passed	Model Under Test Equivalent Model
8aac44bc278a43688f036e43f3a0f0f91ad2cefd	Apalache	Not	Def1	True	Passed	Model Under Test Equivalent Model
c81f9abf51be8f6b5a6227d8a95d3726c97b4774	Apalache	Not	Def1	False	Passed	Model Under Test Equivalent Model
af3e878eb5789fe9b1fab78e5a3eee3eae858c20	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def1	True	Passed	Model Under Test Equivalent Model
fb00e1911acbc36d80ba600195ae4afd6836e2fc	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def1	False	Passed	Model Under Test Equivalent Model
c1fdd4e43023b8710366467fd4988cdde3f9ba53	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def1	True	Passed	Model Under Test Equivalent Model
1a417d0bca01a79a7695d1f645929bca5f287089	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def1	False	Passed	Model Under Test Equivalent Model
6431e3c5f37ff1007b53056a8d01a74c585a627c	Apalache	AndProp	Def1	True	Passed	Model Under Test Equivalent Model
e9860959e99970a8ae5d663bfcd257ec4cbdb439	Apalache	AndProp	Def1	False	Passed	Model Under Test Equivalent Model
12dd1d403cc57e218c24568939cd3afbb8e7b017	Apalache	Boxed	Def1	True	Passed	Model Under Test Equivalent Model
a3837a41512caf13a5baeabada4b8e20e5a6268f	Apalache	Boxed	Def1	False	Passed	Model Under Test Equivalent Model
04b33e67b9e22a6fde28c48f489da9f79c279646	Apalache	Eq	Def1	True	Passed	Model Under Test Equivalent Model
978e2929ed83fe5f6b3189a4152c9319f49d1d04	Apalache	Eq	Def1	False	Passed	Model Under Test Equivalent Model
f79c6e77fa86fb2f1b8d1bcb88fd260d559982ad	Apalache	Ne	Def1	True	Passed	Model Under Test Equivalent Model
c2767441bad3fce0366e175f3b9911dd76ab680f	Apalache	Ne	Def1	False	Passed	Model Under Test Equivalent Model
282ae46252aa369e97af588199f41d0a258a97d0	Apalache	Let	Def1	True	Passed	Model Under Test Equivalent Model
d68dba880710cf727935f65d9def6c095243e78f	Apalache	Let	Def1	False	Passed	Model Under Test Equivalent Model
36eb50ea2b85e33b161793fdc4a3b636b6dcd215	Apalache	Set0	Def1	True	Passed	Model Under Test Equivalent Model
956ffc61d40820c844c8b07e57d4eb40b7d54940	Apalache	Set0	Def1	False	Passed	Model Under Test Equivalent Model
32dac6bf3515a36f7e0736b6d99fd4240a26a738	Apalache	Set1	Def1	True	Passed	Model Under Test Equivalent Model
df8602b620187e10c7ed9e266e7e44398ab7880a	Apalache	Set1	Def1	False	Passed	Model Under Test Equivalent Model
763d88dd9f18955c8e2810025de09a6e96d6ea8f	Apalache	Set2	Def1	True	Passed	Model Under Test Equivalent Model
e3b6703ba1071e04df0e2e8f4b4df477eef09bd2	Apalache	Set2	Def1	False	Passed	Model Under Test Equivalent Model
d278653066e62b173a14304aad5a43ee8fc083e2	Apalache	Fun	Def1	True	Passed	Model Under Test Equivalent Model
8d417e3ffd06c3cce21551cfc7357d47c892e31d	Apalache	Fun	Def1	False	Passed	Model Under Test Equivalent Model
de06326e11f56f2ccf4f879cad71db3937537b8f	Apalache	In	Def1	True	Passed	Model Under Test Equivalent Model
7c21521f946accc87ca5149dfaee4323cbc221ff	Apalache	In	Def1	False	Passed	Model Under Test Equivalent Model
0a991db09f1350c44c0eac941ece65e601871f59	Apalache	NotIn	Def1	True	Passed	Model Under Test Equivalent Model
31ccec4d732f91963a9071a7ad313c02ecf3d778	Apalache	NotIn	Def1	False	Passed	Model Under Test Equivalent Model
cd3a64e17c9c981a743626fbd7e48bbc16df6138	Apalache	Exists	Def1	True	Passed	Model Under Test Equivalent Model
3c722091382a378fdd91cbcb8094de7e10e69215	Apalache	Exists	Def1	False	Passed	Model Under Test Equivalent Model
3824290ee255daf7443640e770cdae786140faf1	Apalache	Forall	Def1	True	Passed	Model Under Test Equivalent Model
f93c27aedffed6c73e65876eb9ee84e48e4ecfdf	Apalache	Forall	Def1	False	Passed	Model Under Test Equivalent Model
ed9d7199dfab4d03329bfa58a73ed8f9c737e3e8	Apalache	Choose	Def1	True	Passed	Model Under Test Equivalent Model
83c417b4ec8595787e73c85438ec6cf4391c62c4	Apalache	Choose	Def1	False	Passed	Model Under Test Equivalent Model
a1f05f858015536db1fc3ba1db51b8e71cde92b7	Apalache	Record	Def1	True	Passed	Model Under Test Equivalent Model
97e2091916951acb9ab11d5625975a1dac795b35	Apalache	Record	Def1	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
74db2085bf55e1adf2595ef8b61f8d1a97f65d2f	Apalache	FunApp	Def1	True	Passed	Model Under Test Equivalent Model
1b069fd0c4d3976d3e59271a2182f6e6c94a14c5	Apalache	FunApp	Def1	False	Passed	Model Under Test Equivalent Model
b7cea052623ee1c0876f28c6bdde18c912e6a198	Apalache	Except0	Def1	True	Passed	Model Under Test Equivalent Model
6de6590ed819ecd4ca0c5bfb0e02014290d7bd4c	Apalache	Except0	Def1	False	Passed	Model Under Test Equivalent Model
d9393f6506dcc4dadd8bd85458f8d6d02d828e34	Apalache	Except1Fun	Def1	True	Passed	Model Under Test Equivalent Model
8902f5d1d661cd13dc723546b9c2b4e232555d27	Apalache	Except1Fun	Def1	False	Passed	Model Under Test Equivalent Model
2714b7cbafaecddeda2c3c4df91cfb99eea76b17	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def1	True	Passed	Model Under Test Equivalent Model
6db07fe72d8f8d51753912869b111c2385a429ec	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def1	False	Passed	Model Under Test Equivalent Model
0dc7f34aeb2132e7afd2f0a0472fc8f8e95a7d52	Apalache	Except1Rec	Def1	True	Passed	Model Under Test Equivalent Model
2092a052f4f30eeeb4ce5b3fc2eb60e33d9739dd	Apalache	Except1Rec	Def1	False	Passed	Model Under Test Equivalent Model
8b73d2e15f7dd0f9c4ca0b60730311f35e206d93	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Def1	True	Passed	Model Under Test Equivalent Model
4404e5a37c30f64e08144ba92785890156b8ec0d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Def1	False	Passed	Model Under Test Equivalent Model
15e6ee661ac741e3324356c62ef5d4a7c65c5f4f	Apalache	Except2Fun	Def1	True	Passed	Model Under Test Equivalent Model
3dcc9b3c99f480742dc944f3d346ed5f9786bf4d	Apalache	Except2Fun	Def1	False	Passed	Model Under Test Equivalent Model
698bdefb72b31a5b1c3650dcbf1cca6d0533c983	Apalache	Except2FunTuple	Def1	True	Passed	Model Under Test Equivalent Model
c47e7aace5ffc09a3e967b60fdf1c5d4e72f0117	Apalache	Except2FunTuple	Def1	False	Passed	Model Under Test Equivalent Model
a6806906ac35b3c22d9b344df02aaa203069a560	Apalache	Prime	Def1	True	Passed	Model Under Test Equivalent Model
eca1245946d3ef807b68fc5428739a25aec5d170	Apalache	Prime	Def1	False	Passed	Model Under Test Equivalent Model
9227a649e20e0c0dad64d09948bbe7766ec7c2ce	Apalache	NumUnaryMinus	Def1	True	Passed	Model Under Test Equivalent Model
bdb662d21d02a106529b2228de8baaa7d25a8cd5	Apalache	NumUnaryMinus	Def1	False	Passed	Model Under Test Equivalent Model
c277f15de6dd07a63ff49ccdb5e002cb6a141135	Apalache	NumPlus	Def1	True	Passed	Model Under Test Equivalent Model
b2eb1889390bf59f9c15204f5515ce9884b471ba	Apalache	NumPlus	Def1	False	Passed	Model Under Test Equivalent Model
1ca177f827c35679c1571018d7f833be65feacb4	Apalache	NumMinus	Def1	True	Passed	Model Under Test Equivalent Model
54a3ec919e174166d0bd6dc90a7900dd1949092f	Apalache	NumMinus	Def1	False	Passed	Model Under Test Equivalent Model
133fa1915b50d806a15dadbccd049ba2e442fc9c	Apalache	NumMul	Def1	True	Passed	Model Under Test Equivalent Model
bb76fa4463bb61880e96b3142cd2ee6005d34120	Apalache	NumMul	Def1	False	Passed	Model Under Test Equivalent Model
7b0cccd08ae6c6f6e37e9a42b0039a8e60fb3989	Apalache	NumDiv	Def1	True	Passed	Model Under Test Equivalent Model
62723af3c119b0ea62953f7e17619e0b1975df07	Apalache	NumDiv	Def1	False	Passed	Model Under Test Equivalent Model
46b0749080c1151f5b0831f61b15fb3e62a43487	Apalache	NumMod	Def1	True	Passed	Model Under Test Equivalent Model
0971b961300483f3935a76043ffc561e604a31cc	Apalache	NumMod	Def1	False	Passed	Model Under Test Equivalent Model
49e70b0766b50ed63b89b195e445381f28b669da	Apalache	NumPow	Def1	True	Passed	Model Under Test Equivalent Model
578e7b329528106c6c472d7bf3bb785039bda2de	Apalache	NumPow	Def1	False	Passed	Model Under Test Equivalent Model
c6788ff4a005715b81ed931c99bced15244fc1a7	Apalache	NumGt	Def1	True	Passed	Model Under Test Equivalent Model
d015df0e4c9512c848e966cb818cf0bc1c93e03e	Apalache	NumGt	Def1	False	Passed	Model Under Test Equivalent Model
599ba04d22af4faa9b5ffda4480ff51da7f8e58a	Apalache	NumGe	Def1	True	Passed	Model Under Test Equivalent Model
cdf74dc8aaaf9d6382604bbf02243cb9e23665f4	Apalache	NumGe	Def1	False	Passed	Model Under Test Equivalent Model
f0f9df9a0ca7ff0d30e55a90be8521fff287fbf8	Apalache	NumLt	Def1	True	Passed	Model Under Test Equivalent Model
483a5cbdbeaa7fa43a57f17602c01e276157f38e	Apalache	NumLt	Def1	False	Passed	Model Under Test Equivalent Model
d91e7e741a070a99f38f837f9c20ec63800cbb30	Apalache	NumLe	Def1	True	Passed	Model Under Test Equivalent Model
b157b890a1a798bfc81e8cdd3d517bc57fb30280	Apalache	NumLe	Def1	False	Passed	Model Under Test Equivalent Model
aaf7028d0855d58835fee1c78618c0fbb02f9384	Apalache	DefFun	Def1	True	Passed	Model Under Test Equivalent Model
1e61d5ed056a0e9c30059438bf69941adccb33f1	Apalache	DefFun	Def1	False	Passed	Model Under Test Equivalent Model
1b10246345557cd5a74df282051aff448a01f171	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def1	True	Passed	Model Under Test Equivalent Model
14b2286a0bf3bb68ba001cba2dab58e2f8d0d2a1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def1	False	Passed	Model Under Test Equivalent Model
17315f2f6d7b8de3e65d8d6d039e62293df7fd23	Apalache	DefFunRecursive	Def1	True	Passed	Model Under Test Equivalent Model
ec2b673eb8e72bf5f050138737a9e6448c587ac1	Apalache	DefFunRecursive	Def1	False	Passed	Model Under Test Equivalent Model
50f125c4fe2ddf37dc9769c626a069d7bdc0d315	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def1	True	Passed	Model Under Test Equivalent Model
d0538aab23e58c6b08158d4102feb8a9b556a2f6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def1	False	Passed	Model Under Test Equivalent Model
d74ad7bd9b20d35d426a77e34e23e6aae94ae1a3	Apalache	Def0	Def1	True	Passed	Model Under Test Equivalent Model
8835c7cc97b4b9b9dfb9f68dee9e6797010f12d0	Apalache	Def0	Def1	False	Passed	Model Under Test Equivalent Model
a0e360af0245dcdbf1b7b34a8080779a8c2685e1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def1	True	Passed	Model Under Test Equivalent Model
4a4a089498262d11819a145da12693c108530bd9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def1	False	Passed	Model Under Test Equivalent Model
93deb1a7de83d32d4c239d41ff6945abfbae449e	Apalache	Def1	Def1	True	Passed	Model Under Test Equivalent Model
f68a0916a8f652f985788c38ec1548746177192f	Apalache	Def1	Def1	False	Passed	Model Under Test Equivalent Model
0b5365190bb695037e91377429d13fb44f498161	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def1	True	Passed	Model Under Test Equivalent Model
dc43172f9d91a3923df1f1c25cd0954a3135e036	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def1	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
2b09f774ef8a5106cee5f8d40072935a42f90c2c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def1	True	Passed	Model Under Test Equivalent Model
65780d089d5b50f0ee662840d014c1215eb58a49	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def1	False	Passed	Model Under Test Equivalent Model
8d7bcd5917e00313967f398d17a9b83fdff9a081	Apalache	Def1Recursive	Def1	True	Passed	Model Under Test Equivalent Model
2d122504c15c2cdf959a7aaaa7345ab7ac052523	Apalache	Def1Recursive	Def1	False	Passed	Model Under Test Equivalent Model
f096f3995eb65e606d2b81ae98eeac87e251e4d4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def1	True	Passed	Model Under Test Equivalent Model
14a49b6c622f317fa94bef33bb4d25b7001c95f2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def1	False	Passed	Model Under Test Equivalent Model
3383029495256d671d509a01a06a46c4437a188b	Apalache	Extends	Def1	True	Passed	Model Under Test Equivalent Model
8de2eaabae95f3177bf0dd2d28b01c63fdffdba9	Apalache	Extends	Def1	False	Passed	Model Under Test Equivalent Model
34bdaba291533c9c7526c0ca2d91fcb51e028ee6	Apalache	ExtendsInDifferentFolder	Def1	True	Passed	Model Under Test Equivalent Model
6e6a040e7d92d8b4afb9a449fb1fa6f54660db30	Apalache	ExtendsInDifferentFolder	Def1	False	Passed	Model Under Test Equivalent Model
88630e96451b4d23ec98708d9df503df51d2eccc	Apalache	Variable	Def1	True	Passed	Model Under Test Equivalent Model
255df1d3666a8de0744e38b37d79f920f0ab68e7	Apalache	Variable	Def1	False	Passed	Model Under Test Equivalent Model
84b5292f73fee1d71bbc4e12724dda85fa6a39dc	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def1	True	Passed	Model Under Test Equivalent Model
65259b0a4640bd69410e455a284482010719ebb0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def1	False	Passed	Model Under Test Equivalent Model
9033c17c7d0c24a48c8a07c8212f60f3946a8572	Apalache	Constant	Def1	True	Passed	Model Under Test Equivalent Model
cccdf7347681eea3a2a1984c393602e61ef27ecf	Apalache	Constant	Def1	False	Passed	Model Under Test Equivalent Model
09445790549206e78193b839ded98c4c6c3b3bae	Apalache	ConstantRank1	Def1	True	Passed	Model Under Test Equivalent Model
814bea409c0c697e49102906b0eb306bcb6a747e	Apalache	ConstantRank1	Def1	False	Passed	Model Under Test Equivalent Model
70c4533f8aea963e6cfa1621e74934edcaf2dc3f	Apalache	Instance	Def1	True	Passed	Model Under Test Equivalent Model
aedae4aab3696e805b4731fd811cd6a7ebcb6028	Apalache	Instance	Def1	False	Passed	Model Under Test Equivalent Model
875c65914585372966d5a722e3b8b1435c39b5e8	Apalache	InstanceWith	Def1	True	Passed	Model Under Test Equivalent Model
7661a55853702736f7d0eba17ce401c2947d8d69	Apalache	InstanceWith	Def1	False	Passed	Model Under Test Equivalent Model
ac94082a334ea6756fa7bbaade49e5d2818d8d3e	Apalache	InstanceNamed	Def1	True	Passed	Model Under Test Equivalent Model
054c20bce257a4109162dc62377b5f78711519c4	Apalache	InstanceNamed	Def1	False	Passed	Model Under Test Equivalent Model
5e00256fea95fa5597ef751a70b65580acece839	Apalache	InstanceNamedWith	Def1	True	Passed	Model Under Test Equivalent Model
573b4c5d7e52f81e2cb908f27a15e6f9600c12d3	Apalache	InstanceNamedWith	Def1	False	Passed	Model Under Test Equivalent Model
015de582b26beb30fd5ab90498482f8b9616e8f2	Apalache	InstanceInFolder	Def1	True	Passed	Model Under Test Equivalent Model
6cce7ecc91d6cefdd8f2c274aa0659171eb9463d	Apalache	InstanceInFolder	Def1	False	Passed	Model Under Test Equivalent Model
89f5dae9a00812b4958c9c070ab0e0f35407e9a6	Apalache	InstanceWithInFolder	Def1	True	Passed	Model Under Test Equivalent Model
877dc18efd77392c2a40b912744ee7357f4dc6f6	Apalache	InstanceWithInFolder	Def1	False	Passed	Model Under Test Equivalent Model
e4377ea249c10ca92748c149a03b8795dd011e51	Apalache	InstanceNamedInFolder	Def1	True	Passed	Model Under Test Equivalent Model
947ba44932e0e7a08e924305be8c0c2c54782060	Apalache	InstanceNamedInFolder	Def1	False	Passed	Model Under Test Equivalent Model
2b5c2c6c1b24bc4f97df3d94064fc45504092f8a	Apalache	InstanceNamedWithInFolder	Def1	True	Passed	Model Under Test Equivalent Model
308131e76fc7faaaae35b33e53a1c1b2f6b9f8c2	Apalache	InstanceNamedWithInFolder	Def1	False	Passed	Model Under Test Equivalent Model
b382cb2a2fed60fbe78e51095c20b381a2adc86c	Apalache	Enabled	Def1	True	Passed	Model Under Test Equivalent Model
9eca1fb3a207d068c9d7abd8a048b30b4c7f87e8	Apalache	Enabled	Def1	False	Passed	Model Under Test Equivalent Model
b7f2bd019911ce4e06ffe40ea2dd97af9397df6e	Apalache	Assume	Def1	True	Passed	Model Under Test Equivalent Model
a36cd012155c56d6ae23666317628a4441d9c580	Apalache	Assume	Def1	False	Passed	Model Under Test Equivalent Model
865be380e2f445c390b6db636023e4ce508d7860	Apalache	AssumeNamed	Def1	True	Passed	Model Under Test Equivalent Model
d1454cfc113d02e26807c393800b576419239709	Apalache	AssumeNamed	Def1	False	Passed	Model Under Test Equivalent Model
43c602a079fe36f4da4643b1b13ed9c2b924ce99	Apalache	Lambda	Def1	True	Passed	Model Under Test Equivalent Model
81e5d55607dbfc17b8985585bb9bf6a51691cfb0	Apalache	Lambda	Def1	False	Passed	Model Under Test Equivalent Model
8eb26e92a5ab4a8f950627c4e9618ce980d91455	Apalache	Cross2	Def1	True	Passed	Model Under Test Equivalent Model
f056e7d48d00f09cd3375c96aa595c3f9ab40f16	Apalache	Cross2	Def1	False	Passed	Model Under Test Equivalent Model
1768bb00699c669f4ac118c1335c5ffc76c41c37	Apalache	Cross3	Def1	True	Passed	Model Under Test Equivalent Model
161026385ddbbe0b24cc8c84f0057cd961fcce97	Apalache	Cross3	Def1	False	Passed	Model Under Test Equivalent Model
51afc128ad371a977ebb8a26c754ecab942a9ed2	TLC with reduction strategy: Case 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))	FunSet	Def1	True	Passed	Model Under Test Equivalent Model
9f60e2bb92fe644d057a573575f220a7a7d11853	TLC with reduction strategy: Case 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))	FunSet	Def1	False	Passed	Model Under Test Equivalent Model
dc5bd24f81e137dd05997e6c70dc96599eb26ece	TLC with reduction strategy: Case 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)	RecordSet	Def1	True	Passed	Model Under Test Equivalent Model
8046ebd619b8b863b925a720a74276bea700902d	TLC with reduction strategy: Case 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)	RecordSet	Def1	False	Passed	Model Under Test Equivalent Model
27d97aeb296a24ee8e9ee88ea67d9699308cbbe8	Apalache	SetDiff	Def1	True	Passed	Model Under Test Equivalent Model
a2f22082256d509abf69e690d3897aaf2157d8c7	Apalache	SetDiff	Def1	False	Passed	Model Under Test Equivalent Model
9c2173f734d97b99aeca39903301e9e51c393b31	Apalache	SetUnion	Def1	True	Passed	Model Under Test Equivalent Model
4788e7cf059f13b8fded2207d6d4033c3f61c6fd	Apalache	SetUnion	Def1	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
875a87caa2b4beefea4f4949f7587818a3157b67	Apalache	SubsetEq	Def1	True	Passed	Model Under Test Equivalent Model
66f58ad3a42753ce8e82ba1024760de3260b9b31	Apalache	SubsetEq	Def1	False	Passed	Model Under Test Equivalent Model
d6780d2405d7439c84658ee0d6be966b65c0e77b	Apalache	IfCond	Def1	True	Passed	Model Under Test Equivalent Model
bd0673462a66bf728daa823208967446d97461e9	Apalache	IfCond	Def1	False	Passed	Model Under Test Equivalent Model
b1a159cb8de304f13ed313cc2df5317a4a5c31fb	Apalache	IfThen	Def1	True	Passed	Model Under Test Equivalent Model
095faca44b70fee181d74693f41d0d99e763b812	Apalache	IfThen	Def1	False	Passed	Model Under Test Equivalent Model
1b80c6b60aea112e4a26ae25127464d595edd7be	Apalache	IfElse	Def1	True	Passed	Model Under Test Equivalent Model
54c52ab798ba1ee894dcc3af66afa0adda16f2c9	Apalache	IfElse	Def1	False	Passed	Model Under Test Equivalent Model
861407c23f36f47168f7a192300818c110fa17f5	Apalache	Subset	Def1	True	Passed	Model Under Test Equivalent Model
1a72cb144ef3de4bdae7a0874aaa996401c4fc4f	Apalache	Subset	Def1	False	Passed	Model Under Test Equivalent Model
a251da9021f0f21b97f2423b108d307e8a23312f	Apalache	Domain	Def1	True	Passed	Model Under Test Equivalent Model
b1c8f21cac1b86663aa19fc35303ae4c8c41ca3e	Apalache	Domain	Def1	False	Passed	Model Under Test Equivalent Model
abf4b27daadd74f7605fcd70a3bb041178680b0c	Apalache	Union	Def1	True	Passed	Model Under Test Equivalent Model
a39ec1210e0186f0d819014c2cf08dc6248a26b6	Apalache	Union	Def1	False	Passed	Model Under Test Equivalent Model
ffc1e5bebd25c1f77f8cddf5699278727605d6a7	Apalache	Unchanged	Def1	True	Passed	Model Under Test Equivalent Model
cd09d08ad2e47f571da0984b5d1d98fa09cd1a9d	Apalache	Unchanged	Def1	False	Passed	Model Under Test Equivalent Model
91a3c48b73df2ddea00f855c98dc4a6b0c4bd7e2	Apalache	Equivalence	Def1	True	Passed	Model Under Test Equivalent Model
8d1ef29b6987b3976407176ec28a6fdd65e5971e	Apalache	Equivalence	Def1	False	Passed	Model Under Test Equivalent Model
bd52b4cd6653d64f8e12ffb7b0ad0a547ffe6bf3	Apalache	SeqLen	Def1	True	Passed	Model Under Test Equivalent Model
b66563678e4a65eb1778e3d9a85621d8c96594d1	Apalache	SeqLen	Def1	False	Passed	Model Under Test Equivalent Model
8148b6f1315ebf84a82c32f1c76b1d47cc0f9790	Apalache	SeqConcat	Def1	True	Passed	Model Under Test Equivalent Model
7f5318fbf9c129c54e0562c3a46fe7fa8ba49f59	Apalache	SeqConcat	Def1	False	Passed	Model Under Test Equivalent Model
1171e3e66a46c23ee7d1baa4f6bcacecfa6c8590	Apalache	SeqSeq	Def1	True	Passed	Model Under Test Equivalent Model
70e22a049258d0441da2930764c260a180ebe998	Apalache	SeqSeq	Def1	False	Passed	Model Under Test Equivalent Model
cc2859097c9efd4276de9bdb0efe029704e041ed	Apalache	SeqSelectSeq	Def1	True	Passed	Model Under Test Equivalent Model
0eb4fa791d2c82b86fc8a6053d5c98dab4543492	Apalache	SeqSelectSeq	Def1	False	Passed	Model Under Test Equivalent Model
c06e0952c28b9e3fa7658007502819bd0fd29b05	Apalache	SeqSubSeq	Def1	True	Passed	Model Under Test Equivalent Model
5c814dac5eca60d3aa983dd99af96c776706e5d0	Apalache	SeqSubSeq	Def1	False	Passed	Model Under Test Equivalent Model
fe822799e79c0450770189efc7cc658601a05683	TLC with reduction strategy: Case 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	NumRange	Def1	True	Passed	Model Under Test Equivalent Model
026c1d1dac8f0a44f3705c46afa12050ec5c5934	TLC with reduction strategy: Case 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	NumRange	Def1	False	Passed	Model Under Test Equivalent Model
fcd0526573ebd9c529c29b93fba35efaebf97eb8	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def1	True	Passed	Model Under Test Equivalent Model
e4a014f086a79a6f7e2bae2746a01d9ec15c0ceb	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def1	False	Passed	Model Under Test Equivalent Model
2c8bbbdf27935dbc0e83595e428f24fba2647ae5	TLC with reduction strategy: Case 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]]	TlcExtendFun	Def1	True	Passed	Model Under Test Equivalent Model
ba15eeee35ad07465d251ca7541879cdb3111a79	TLC with reduction strategy: Case 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]]	TlcExtendFun	Def1	False	Passed	Model Under Test Equivalent Model
8b9d248f06527c60d131d33acef18b77b49ccd7e	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def1	True	Passed	Model Under Test Equivalent Model
eff1caf06bba3b01df771af4f26d6f718629fb07	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def1	False	Passed	Model Under Test Equivalent Model
9e5e0208e2dbaf1c9c02b7c8a8f7aa21d1fbd5fb	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def1	True	Passed	Model Under Test Equivalent Model
8d2bd574ae1c2d78c10e5859282d46b513a9752a	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def1	False	Passed	Model Under Test Equivalent Model
981e2656c3da961cddfa73f2c387a5d71bb43934	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def1	True	Passed	Model Under Test Equivalent Model
d55b1561bafc8752526f462d03096fbcb6efca37	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def1	False	Passed	Model Under Test Equivalent Model
3fa4f5417aea6ea61931955cc56ec6b795e11cf0	Apalache	BagBagToSet	Def1	True	Passed	Model Under Test Equivalent Model
e343d0d44219bd3084f8a0b300185ea2ddbda4e6	Apalache	BagBagToSet	Def1	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
df22404e838522fa84244dc4c03251f4d73e23f5	Apalache	BagBagIn	Def1	True	Passed	Model Under Test Equivalent Model
4ff0936785a5d974dd4b73974be575ad8a2136dc	Apalache	BagBagIn	Def1	False	Passed	Model Under Test Equivalent Model
d8b3c79987d085869523c3b03d78ad916a3e8327	Apalache	BagAddBag	Def1	True	Passed	Model Under Test Equivalent Model
e7a551b10a2426f35186caaf1c7c95e44d547e49	Apalache	BagAddBag	Def1	False	Passed	Model Under Test Equivalent Model
a211b295a35e8463862c0b6d9f5812bab836b89a	Apalache	BagBagSub	Def1	True	Passed	Model Under Test Equivalent Model
2359446310fb3cf243843a98ef228bf3b89d5628	Apalache	BagBagSub	Def1	False	Passed	Model Under Test Equivalent Model
3f687bd4a13259edf54131dd5a2c592b0f74018b	Apalache	BagCopiesIn	Def1	True	Passed	Model Under Test Equivalent Model
3b3db5746e3f19723a63733372be65a4f495f690	Apalache	BagCopiesIn	Def1	False	Passed	Model Under Test Equivalent Model
d8b6c5ecaced8ef28944205a7da3fbd2faadeb51	Apalache	BagSubsetEqBag	Def1	True	Passed	Model Under Test Equivalent Model
33d1b1b3bcd017894bb523bee56e763afadb75c2	Apalache	BagSubsetEqBag	Def1	False	Passed	Model Under Test Equivalent Model
865c24560f87bcf6292c887fc14ab8f97f8ca470	Apalache	BagBagUnion	Def1	True	Passed	Model Under Test Equivalent Model
39e5cdb468d86dbd73a933e37d21f73cf34331c7	Apalache	BagBagUnion	Def1	False	Passed	Model Under Test Equivalent Model
4d1b75e622333b86196a3a1a994dd0a900a4fdf6	Apalache	BagBagCardinality	Def1	True	Passed	Model Under Test Equivalent Model
d272df9e1deae2da6dad3ed8946147fcae08f94d	Apalache	BagBagCardinality	Def1	False	Passed	Model Under Test Equivalent Model
b591fdafc735a26d183d265d5c207f9ddbc41956	Apalache	BagBagOfAll	Def1	True	Passed	Model Under Test Equivalent Model
9f756fe24bb862f98d6e2ca530119a7fb28943a9	Apalache	BagBagOfAll	Def1	False	Passed	Model Under Test Equivalent Model
dc24aec9e2f3190651f0fd7b89fc07caa1844ced	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def1	True	Passed	Model Under Test Equivalent Model
161e0d3d17bcdb81b4067ea11736ade0669d6b44	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def1	False	Passed	Model Under Test Equivalent Model
e65af7f6953e11ce63bd4863a007aa4860ddbbdb	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Def1	True	Passed	Model Under Test Equivalent Model
c266843fcacf8cb51425c8439ede996086277209	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Def1	False	Passed	Model Under Test Equivalent Model
44dc7504cc8fbf1e458f265fabf4ae851c03fc28	Apalache	FiniteSetsCardinality	Def1	True	Passed	Model Under Test Equivalent Model
0feb05c57af597ae17104a87310cf5ab10ba18d9	Apalache	FiniteSetsCardinality	Def1	False	Passed	Model Under Test Equivalent Model
49f2b21ccdfe66889390388dc6090c61395cb5ab	Apalache	SeqHead	Def1	True	Passed	Model Under Test Equivalent Model
697074930e5b5003ee29f831a054be64e40d2693	Apalache	SeqHead	Def1	False	Passed	Model Under Test Equivalent Model
ca6b4816528c57a161fe37bb892e62ec37203ca3	Apalache	SeqTail	Def1	True	Passed	Model Under Test Equivalent Model
d09ba199431597a36f2620d91d219d1a652fd882	Apalache	SeqTail	Def1	False	Passed	Model Under Test Equivalent Model
c6de1ef2bcdd48bd3637a01580c75c831f08068d	Apalache	SeqAppend	Def1	True	Passed	Model Under Test Equivalent Model
f5adec961eb02aa86d0efc23da6807813c7df1a3	Apalache	SeqAppend	Def1	False	Passed	Model Under Test Equivalent Model

Index

Tests by plug feature Def1; CLI Option: -workers 1