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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
aa4ef39b749874988479c96a1324c7871b5d2c5d	Apalache	And	Def2	True	Passed	Model Under Test Equivalent Model
6dcc60029d0cea4c5c45304f60734cfb15f549cb	Apalache	And	Def2	False	Passed	Model Under Test Equivalent Model
d4e06baef553664c4c41646bc4132d9863ef65e7	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def2	True	Passed	Model Under Test Equivalent Model
99983b509d61c3480182bb40e025aa154c7fdde1	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def2	False	Passed	Model Under Test Equivalent Model
31311ac47f01c6494d39d37fab81d4acfd0de839	Apalache	Imply	Def2	True	Passed	Model Under Test Equivalent Model
f63e3f15c0d423af8444f26064af79693b1ba363	Apalache	Imply	Def2	False	Passed	Model Under Test Equivalent Model
982f8bbdac0120ddae993c091069ffc79db12c8c	Apalache	Not	Def2	True	Passed	Model Under Test Equivalent Model
f4c60e78bc32b29757682e4fb664cb53e8f147b0	Apalache	Not	Def2	False	Passed	Model Under Test Equivalent Model
e5aa0644c9a60bd1cfb588b2b006e6da18edcd77	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def2	True	Passed	Model Under Test Equivalent Model
a4f53dc92debee69c5db09489274df8dd1e5f71e	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def2	False	Passed	Model Under Test Equivalent Model
97c04d1ddb54458a6470c50095a464ddb680e165	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def2	True	Passed	Model Under Test Equivalent Model
e642337155564a7733ce21e4efc01d8085fd7a40	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def2	False	Passed	Model Under Test Equivalent Model
fe50757c5a64d680855efceec1cc66b052f4bd3e	Apalache	AndProp	Def2	True	Passed	Model Under Test Equivalent Model
41a965e576e91e672aab096c5d3fa53792f70072	Apalache	AndProp	Def2	False	Passed	Model Under Test Equivalent Model
c3f5c6d16edfbd3fff1d0ae72497be509162e899	Apalache	Boxed	Def2	True	Passed	Model Under Test Equivalent Model
ffc34a613b07d794ba2591c96b5608d17cdc7d7c	Apalache	Boxed	Def2	False	Passed	Model Under Test Equivalent Model
f7ca9deee1143895dc69528429eab2acf6c105f6	Apalache	Eq	Def2	True	Passed	Model Under Test Equivalent Model
e4aef93ffeac4ac0914392e56e5dffd7c5a93bc2	Apalache	Eq	Def2	False	Passed	Model Under Test Equivalent Model
9534e30ec7a02a3fbde7f99dbf0a1067ce6b5e25	Apalache	Ne	Def2	True	Passed	Model Under Test Equivalent Model
b281c41573a8d0adcd5bc6ebbefdc446da9bb115	Apalache	Ne	Def2	False	Passed	Model Under Test Equivalent Model
2bfa6d0efb91e4e2988c58991e90e7e94e25dce7	Apalache	Let	Def2	True	Passed	Model Under Test Equivalent Model
6642b7ef676e4fce8c79a71f721d97821c4f203f	Apalache	Let	Def2	False	Passed	Model Under Test Equivalent Model
d95765a8db80243da51105083e87e19a0f37a595	Apalache	Set0	Def2	True	Passed	Model Under Test Equivalent Model
12fc8aa7a896f6f9b52381c674089f38c05af8d4	Apalache	Set0	Def2	False	Passed	Model Under Test Equivalent Model
b50920704e1cfdd25832393160dccb1f33b522b0	Apalache	Set1	Def2	True	Passed	Model Under Test Equivalent Model
f85e5ca88ab30d7c0a90715046dd34e538b5df24	Apalache	Set1	Def2	False	Passed	Model Under Test Equivalent Model
e96926c72504148b336a55bd0b72879b45e7b958	Apalache	Set2	Def2	True	Passed	Model Under Test Equivalent Model
2562f5dfdabc0247d0dde1209ecfeca775be2c82	Apalache	Set2	Def2	False	Passed	Model Under Test Equivalent Model
7c4ed8c5075c91e80cb8c263163482d3fd91c5d2	Apalache	Fun	Def2	True	Passed	Model Under Test Equivalent Model
c20f2180ae28b9955139954199755eaa40bd6714	Apalache	Fun	Def2	False	Passed	Model Under Test Equivalent Model
58d315a33fe7a045f11041383ffac95950871ef3	Apalache	In	Def2	True	Passed	Model Under Test Equivalent Model
4fd2b68fadbdf91e0a53d5417ab9720a5340678c	Apalache	In	Def2	False	Passed	Model Under Test Equivalent Model
43ed8451074f0ab1942092d54d48a61af14d9c2e	Apalache	NotIn	Def2	True	Passed	Model Under Test Equivalent Model
8483cf6cc7528fd6da1a16c34ca4d12e62cd3451	Apalache	NotIn	Def2	False	Passed	Model Under Test Equivalent Model
85543fd52d0f7c1090c89f03ed7dbf00d81e11d0	Apalache	Exists	Def2	True	Passed	Model Under Test Equivalent Model
a717a6c24356db1fdd31e4b40c734fed474dd7ac	Apalache	Exists	Def2	False	Passed	Model Under Test Equivalent Model
cba538ce8e7825c1e188fa668c7e8abe854c727d	Apalache	Forall	Def2	True	Passed	Model Under Test Equivalent Model
98e9ca9a5aeb690ba6cf81eede0cf8f726c2f39a	Apalache	Forall	Def2	False	Passed	Model Under Test Equivalent Model
9c2125e41f7f29f49a6c96de332e4a3029302bd5	Apalache	Choose	Def2	True	Passed	Model Under Test Equivalent Model
594a463c072881f39829053f730476d56f4a1791	Apalache	Choose	Def2	False	Passed	Model Under Test Equivalent Model
bee1db56ef48265793131d5aec92b39e093ffe28	Apalache	Record	Def2	True	Passed	Model Under Test Equivalent Model
3f976ce0089c4e5dca2da301184ab590d6830bb2	Apalache	Record	Def2	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
e64b2c2d8d53445c217da31db104755109233305	Apalache	FunApp	Def2	True	Passed	Model Under Test Equivalent Model
578c3c391d87cd6f567ac3457e15ccbfc8115656	Apalache	FunApp	Def2	False	Passed	Model Under Test Equivalent Model
06f837501c9227f0c648381e9c5f8c4d7af0aa95	Apalache	Except0	Def2	True	Passed	Model Under Test Equivalent Model
ad5a41ae7698c30f5b3acc2767e628dac9311d60	Apalache	Except0	Def2	False	Passed	Model Under Test Equivalent Model
ee7385550b265d9d8239f4ab04973faeada0fcc4	Apalache	Except1Fun	Def2	True	Passed	Model Under Test Equivalent Model
4012a4729ea572c4d238ed10d37e228c8a926858	Apalache	Except1Fun	Def2	False	Passed	Model Under Test Equivalent Model
0d27a76a14fbf2b465cb54ac7629f2d7c5576c48	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def2	True	Passed	Model Under Test Equivalent Model
62a1c5aeabdc10219bc8dbcb5280a26b0f2a5832	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def2	False	Passed	Model Under Test Equivalent Model
8d9c3779c6cf47582ce60b36a4f99388cfb8d789	Apalache	Except1Rec	Def2	True	Passed	Model Under Test Equivalent Model
75410612e8b7b909b9cc0ea41e2711521006dd29	Apalache	Except1Rec	Def2	False	Passed	Model Under Test Equivalent Model
165aa9260733a59479d2aacfbfaee920b0511682	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Def2	True	Passed	Model Under Test Equivalent Model
6da3775d8f55315afcc07552e960d788dfe19c1b	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Def2	False	Passed	Model Under Test Equivalent Model
d8963097b687979a00553418837d111b14b9a7cb	Apalache	Except2Fun	Def2	True	Passed	Model Under Test Equivalent Model
d0364a8a072b3266e393831a336f70998cec24ab	Apalache	Except2Fun	Def2	False	Passed	Model Under Test Equivalent Model
af369351db77c902c0a0cc71ffedc7aeefb80ef7	Apalache	Except2FunTuple	Def2	True	Passed	Model Under Test Equivalent Model
79d2e3bb1fd4fb42152492d73b9bce49e26fb98a	Apalache	Except2FunTuple	Def2	False	Passed	Model Under Test Equivalent Model
8e41d91557dd22de764761ac00b124cca83eb93a	Apalache	Prime	Def2	True	Passed	Model Under Test Equivalent Model
628a25f71006e8201ea85990c6ab391e66b78b47	Apalache	Prime	Def2	False	Passed	Model Under Test Equivalent Model
70a70a956964b08ef349826232b956994a459395	Apalache	NumUnaryMinus	Def2	True	Passed	Model Under Test Equivalent Model
3a429bbc398895c82d6300f077df02c0a64e567a	Apalache	NumUnaryMinus	Def2	False	Passed	Model Under Test Equivalent Model
22caf39533dee6f60fe255c5eed0c5f7cc587c60	Apalache	NumPlus	Def2	True	Passed	Model Under Test Equivalent Model
e0375b3cce12f7fdb74a32fe35df2a084e2c4c43	Apalache	NumPlus	Def2	False	Passed	Model Under Test Equivalent Model
69741fcf4fd38bdb979925cd3fccece7deb8087b	Apalache	NumMinus	Def2	True	Passed	Model Under Test Equivalent Model
013f0806fca5e0d090c74006944f0deb9c52bb01	Apalache	NumMinus	Def2	False	Passed	Model Under Test Equivalent Model
4f3569d80da10aa68f73c8787d87070f7b4ab412	Apalache	NumMul	Def2	True	Passed	Model Under Test Equivalent Model
dc877a2f0200183a75fc520e39ccf19639d8853d	Apalache	NumMul	Def2	False	Passed	Model Under Test Equivalent Model
0d1b6f1ecda216f921a069ed6efc287e8e6af3d7	Apalache	NumDiv	Def2	True	Passed	Model Under Test Equivalent Model
1452ed5c8c5922bedf6c018a77e549c71d8d4af4	Apalache	NumDiv	Def2	False	Passed	Model Under Test Equivalent Model
677d5821fcfad107bf60150ff505c2b9b686bdda	Apalache	NumMod	Def2	True	Passed	Model Under Test Equivalent Model
936c288407d898217a48823d193d5dcdd582efde	Apalache	NumMod	Def2	False	Passed	Model Under Test Equivalent Model
d2e9d251deaa8de45237ebaf54ff54eae05d3d86	Apalache	NumPow	Def2	True	Passed	Model Under Test Equivalent Model
e3bd57ca9292cccc9f643f92a949cca7100001d7	Apalache	NumPow	Def2	False	Passed	Model Under Test Equivalent Model
fab6b77e1aee441627a9c3849e0289d809132e01	Apalache	NumGt	Def2	True	Passed	Model Under Test Equivalent Model
ef9ca72a9fdce64a6ac215b551cb94c75aebc898	Apalache	NumGt	Def2	False	Passed	Model Under Test Equivalent Model
a96d1bf7758f0559b1ab8d92c4acbeafec207f13	Apalache	NumGe	Def2	True	Passed	Model Under Test Equivalent Model
d3b280da2a0497584b68e5c90451751ebabed631	Apalache	NumGe	Def2	False	Passed	Model Under Test Equivalent Model
1c73f4d06307960153a2b7ee55c41f90a2a7e84a	Apalache	NumLt	Def2	True	Passed	Model Under Test Equivalent Model
96a448df20a8c399c54a914f30c4b95d1b45955e	Apalache	NumLt	Def2	False	Passed	Model Under Test Equivalent Model
229549edaa895b859feffb343ce4bd83e6cf7a28	Apalache	NumLe	Def2	True	Passed	Model Under Test Equivalent Model
024fe68d7fbfe80bfaf4014a73fe76eb8115f995	Apalache	NumLe	Def2	False	Passed	Model Under Test Equivalent Model
6e55401c42f4fcae01244ec8eea4e4c2c10366eb	Apalache	DefFun	Def2	True	Passed	Model Under Test Equivalent Model
a5bf943ddd0a707286b93c513ea9883e5ae25de2	Apalache	DefFun	Def2	False	Passed	Model Under Test Equivalent Model
a363bb196346b01771ccb04216ad963fca3d6504	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def2	True	Passed	Model Under Test Equivalent Model
358b96cf4a88f9da57271cc6398b0c00d155a428	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def2	False	Passed	Model Under Test Equivalent Model
1cd83a2eec22979a53f62734c65f797017619052	Apalache	DefFunRecursive	Def2	True	Passed	Model Under Test Equivalent Model
1049ebaa785a422f1d9f94c0517d14c394f4c551	Apalache	DefFunRecursive	Def2	False	Passed	Model Under Test Equivalent Model
f1c27695092f2e035980c9e6bee4dc3b759089f0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def2	True	Passed	Model Under Test Equivalent Model
bb2b24cd74dee514659de57a3d19730a2007576b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def2	False	Passed	Model Under Test Equivalent Model
8aabee0c8ceff3c4296289f4a1b4897df6db5f11	Apalache	Def0	Def2	True	Passed	Model Under Test Equivalent Model
ff8d44090b86ec26ee3983a5c4143c1a830b76c8	Apalache	Def0	Def2	False	Passed	Model Under Test Equivalent Model
ff491a5774a36c50bf715f7dfebe6e2ce9b330da	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def2	True	Passed	Model Under Test Equivalent Model
06dcd5ecc0a80fe22dcfa603a49c135fc91d607b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def2	False	Passed	Model Under Test Equivalent Model
b5a8f3729171786c285d9fae888241458cfb7e06	Apalache	Def1	Def2	True	Passed	Model Under Test Equivalent Model
0f4561daf026474cac9e3740f26cec098a665e47	Apalache	Def1	Def2	False	Passed	Model Under Test Equivalent Model
74e06541e1686027f4f31d54a172a008a02c7cac	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def2	True	Passed	Model Under Test Equivalent Model
f4263cb9246c64f20e729ce9928712c844a7e23a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def2	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
c78cd0ca983e433ea11f43200b1a4e18ff054ada	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def2	True	Passed	Model Under Test Equivalent Model
5f85b72dfa0dcc52366c80b005ab58f13009280b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def2	False	Passed	Model Under Test Equivalent Model
68c685422c1d6a9b25a471ec4814f2194f2760e8	Apalache	Def1Recursive	Def2	True	Passed	Model Under Test Equivalent Model
a15b7b9d9e7a814b037887455e008564a04cd919	Apalache	Def1Recursive	Def2	False	Passed	Model Under Test Equivalent Model
2d85bd2021b52055c86c05d85f14f46d1a63586e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def2	True	Passed	Model Under Test Equivalent Model
05dae5c86c0065b1a51a69472b8a31a4e61e4551	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def2	False	Passed	Model Under Test Equivalent Model
f09513aca719e5bde83731b36d8317fd8e3c8638	Apalache	Extends	Def2	True	Passed	Model Under Test Equivalent Model
5ff9c7c0050587edeb466cf1bfb1196b2956871a	Apalache	Extends	Def2	False	Passed	Model Under Test Equivalent Model
2ddfbf6efda9a6f5a4cc93aa652b3c55fd868343	Apalache	ExtendsInDifferentFolder	Def2	True	Passed	Model Under Test Equivalent Model
4835880620cc9414523dd88354adf7208fa20e40	Apalache	ExtendsInDifferentFolder	Def2	False	Passed	Model Under Test Equivalent Model
96e9bdf90875cde60047f9575495e341c2b0f24d	Apalache	Variable	Def2	True	Passed	Model Under Test Equivalent Model
61828218d656a0b93c097c8d2871773881defeac	Apalache	Variable	Def2	False	Passed	Model Under Test Equivalent Model
04e5082f0b47424273b1d315aeceae783cdbef5a	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def2	True	Passed	Model Under Test Equivalent Model
4a8e1964cdf34fac492c4d8c43a0a31b5ce4fa13	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def2	False	Passed	Model Under Test Equivalent Model
b208dd8c9d7355f1d676f55376a0fe7d1c5d71fb	Apalache	Constant	Def2	True	Passed	Model Under Test Equivalent Model
efb9d7f91e75d64800f03b83d3a921b92441cca2	Apalache	Constant	Def2	False	Passed	Model Under Test Equivalent Model
91cf33386adfe311cbaffdf5acc1d5d283acf463	Apalache	ConstantRank1	Def2	True	Passed	Model Under Test Equivalent Model
5cbc86142d5db0fe1b4980971771a5e17925a79b	Apalache	ConstantRank1	Def2	False	Passed	Model Under Test Equivalent Model
5b12f80cda7d4aa88062d59f10e9645db959641c	Apalache	Instance	Def2	True	Passed	Model Under Test Equivalent Model
307ba445f804d7cd7d824622c6fa6a8aeea8cbcf	Apalache	Instance	Def2	False	Passed	Model Under Test Equivalent Model
33454474641e6faf4c693dd272d82f2b1e5d6be4	Apalache	InstanceWith	Def2	True	Passed	Model Under Test Equivalent Model
78c9aa430d96728ba7e82bd603823ec0499819e9	Apalache	InstanceWith	Def2	False	Passed	Model Under Test Equivalent Model
2fc0caef96f7f1ea553c7acbc6f78de97e25d534	Apalache	InstanceNamed	Def2	True	Passed	Model Under Test Equivalent Model
194e8481f33be4f73da1823b24ae53d6e0c5ac3a	Apalache	InstanceNamed	Def2	False	Passed	Model Under Test Equivalent Model
3a84b7f3cf91ac144f880abb18f8a6d6a40976b1	Apalache	InstanceNamedWith	Def2	True	Passed	Model Under Test Equivalent Model
ea7c2932ee998ec99dbd44f226e29d9684ed3738	Apalache	InstanceNamedWith	Def2	False	Passed	Model Under Test Equivalent Model
fea179969cd69f005f246e093f3e342c63a4c73d	Apalache	InstanceInFolder	Def2	True	Passed	Model Under Test Equivalent Model
6b928684f5bb023c1a49f929e66a30ce51e2e625	Apalache	InstanceInFolder	Def2	False	Passed	Model Under Test Equivalent Model
dc018d4d893ef729ed2ae0143303af256202eedb	Apalache	InstanceWithInFolder	Def2	True	Passed	Model Under Test Equivalent Model
000f1769f8301f37ed9af589c935fca660287fe2	Apalache	InstanceWithInFolder	Def2	False	Passed	Model Under Test Equivalent Model
8fd5678e0dc0f70e6438767719118ea41ff8f1b9	Apalache	InstanceNamedInFolder	Def2	True	Passed	Model Under Test Equivalent Model
c813ad5decdfa824c310fa2bf800bd959577f4c5	Apalache	InstanceNamedInFolder	Def2	False	Passed	Model Under Test Equivalent Model
709b00c4deccd45b53ec19ab5d120f7194288f9f	Apalache	InstanceNamedWithInFolder	Def2	True	Passed	Model Under Test Equivalent Model
1e94e55e9eecb60f40e1f1c8232b617ab70fb2e6	Apalache	InstanceNamedWithInFolder	Def2	False	Passed	Model Under Test Equivalent Model
eeaf65775f20b8101f178629769c22c2e7cc08c7	Apalache	Enabled	Def2	True	Passed	Model Under Test Equivalent Model
61b95e5676fb4955608a018415df0f59c84348b2	Apalache	Enabled	Def2	False	Passed	Model Under Test Equivalent Model
102fbc98a065890d073b027a591d1aaa72756f14	Apalache	Assume	Def2	True	Passed	Model Under Test Equivalent Model
e0fa808a7c3a757fd3d50fc7d0c0ffb3fd840434	Apalache	Assume	Def2	False	Passed	Model Under Test Equivalent Model
b03d721c8648a8b123cb5efbe1d5da2b9ec98a68	Apalache	AssumeNamed	Def2	True	Passed	Model Under Test Equivalent Model
59259bb91e54399bf48f04b7cc475b36712188b9	Apalache	AssumeNamed	Def2	False	Passed	Model Under Test Equivalent Model
7b7b1b08c561ff596fd9d781f05e1bf01fc3d656	Apalache	Lambda	Def2	True	Passed	Model Under Test Equivalent Model
805110db68ab2e2e981419691ed073181d4b7a8e	Apalache	Lambda	Def2	False	Passed	Model Under Test Equivalent Model
23a25efae439db8bbfe2762d91971020b3f61a81	Apalache	Cross2	Def2	True	Passed	Model Under Test Equivalent Model
1e85842e19e658c00a3413a0c709beb38c7bd386	Apalache	Cross2	Def2	False	Passed	Model Under Test Equivalent Model
0e3279fa43dadf21da83199ca0a0eee02da44265	Apalache	Cross3	Def2	True	Passed	Model Under Test Equivalent Model
37a98b0d942f7fdc9c01e2519c60baeeb2123544	Apalache	Cross3	Def2	False	Passed	Model Under Test Equivalent Model
e6393b4707a81cc68973b303163aa68e3fb595e2	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	Def2	True	Passed	Model Under Test Equivalent Model
7237df7cafc04f6e640ca39facae6553b7bf05be	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	Def2	False	Passed	Model Under Test Equivalent Model
cfea69d196ad2a6921824d8e224dc90531d72724	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	Def2	True	Passed	Model Under Test Equivalent Model
4d28e866288176552537a8ff89ecd26a771922b4	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	Def2	False	Passed	Model Under Test Equivalent Model
38bdc35b84aaa00ab5993c7014f890def2003480	Apalache	SetDiff	Def2	True	Passed	Model Under Test Equivalent Model
bcea28c4466a51d465c42a76c4f2038361bfda9f	Apalache	SetDiff	Def2	False	Passed	Model Under Test Equivalent Model
0bd115e9b3208672778437822324a0b246046ec9	Apalache	SetUnion	Def2	True	Passed	Model Under Test Equivalent Model
af44278dd663c965a2f0af35d0b02c32d32344f5	Apalache	SetUnion	Def2	False	Passed	Model Under Test Equivalent Model
ef50fa1a72a3bbd3fc97c0dc12dd60aad7c6f0df	Apalache	SetIntersect	Def2	True	Passed	Model Under Test Equivalent Model
42cf292128112374af165d98037855f7dedd1f11	Apalache	SetIntersect	Def2	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
bf2637f44401f43e81f1e97617e00766ce7fc698	Apalache	IfCond	Def2	True	Passed	Model Under Test Equivalent Model
2c5174f3111f74f00b760ca3958876b7f562e5b3	Apalache	IfCond	Def2	False	Passed	Model Under Test Equivalent Model
162ba192ebeec5565c78f0b53588485b4fa199fb	Apalache	IfThen	Def2	True	Passed	Model Under Test Equivalent Model
11af74c09e7730e15ec20b091e012d82a5e9b856	Apalache	IfThen	Def2	False	Passed	Model Under Test Equivalent Model
38585163e5f69f08f98bc3e3ea24b8b3c8bde3e2	Apalache	IfElse	Def2	True	Passed	Model Under Test Equivalent Model
1d53b240829344b8ca0d23471f34421bb31a0023	Apalache	IfElse	Def2	False	Passed	Model Under Test Equivalent Model
6376a0ef7c275da79ac517a84905647c8ef38b82	Apalache	Subset	Def2	True	Passed	Model Under Test Equivalent Model
2ccfccc029853ebebc1c8a7451177ea406176059	Apalache	Subset	Def2	False	Passed	Model Under Test Equivalent Model
fff4468113eae0559c5a792ca78355367ed33425	Apalache	Domain	Def2	True	Passed	Model Under Test Equivalent Model
4c5ca1368833b812036911d0f564a76a11eee105	Apalache	Domain	Def2	False	Passed	Model Under Test Equivalent Model
9ffbb855b191e10d083a4b51a3d3e4134cfaf750	Apalache	Union	Def2	True	Passed	Model Under Test Equivalent Model
9a068fca2d2a5e47cde60ac165f2a1df6162497c	Apalache	Union	Def2	False	Passed	Model Under Test Equivalent Model
838959dc26a00232bf6e13ebe06325ba71fd7f27	Apalache	Unchanged	Def2	True	Passed	Model Under Test Equivalent Model
e00a2330640d07f707c26438aee9918dc7b50f63	Apalache	Unchanged	Def2	False	Passed	Model Under Test Equivalent Model
d45462ebfe2a5f1b3e3a9e6935f68fb113b865ec	Apalache	Equivalence	Def2	True	Passed	Model Under Test Equivalent Model
8a8da4feee826239624636cb1a22b007031c707d	Apalache	Equivalence	Def2	False	Passed	Model Under Test Equivalent Model
b3ed065c786cb83a62f8a2bd5d4d82d04c781467	Apalache	SeqLen	Def2	True	Passed	Model Under Test Equivalent Model
b1b996b0c2162ff4413f1ab403c739f13581bcda	Apalache	SeqLen	Def2	False	Passed	Model Under Test Equivalent Model
427fb155d2e6b2e39158ede1e06a7eb0adfba8ce	Apalache	SeqConcat	Def2	True	Passed	Model Under Test Equivalent Model
a7c8ef5a9e29ec9e210102ca28869f9e8c247e12	Apalache	SeqConcat	Def2	False	Passed	Model Under Test Equivalent Model
d6f90c8af35fce14e979de7c6d3936fcda3c19e5	Apalache	SeqSeq	Def2	True	Passed	Model Under Test Equivalent Model
4d70dfc137ff755e229efe2d0de12fd717d2adaf	Apalache	SeqSeq	Def2	False	Passed	Model Under Test Equivalent Model
4b59acb993bdc0735df59382cb429ec484510ad5	Apalache	SeqSelectSeq	Def2	True	Passed	Model Under Test Equivalent Model
72fce6444c7ad77bbfe5ca0379dd9634d04d2204	Apalache	SeqSelectSeq	Def2	False	Passed	Model Under Test Equivalent Model
a397cd65a10e1a946ff46d597d99fed54f7e056a	Apalache	SeqSubSeq	Def2	True	Passed	Model Under Test Equivalent Model
78df63a1cd3c18a3ba9028100be58a65990ef9be	Apalache	SeqSubSeq	Def2	False	Passed	Model Under Test Equivalent Model
7973a89a00c2c0debf606007c09a5d0b1f96eb2e	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	Def2	True	Passed	Model Under Test Equivalent Model
da584d9492a4c4fb9fafc6034b5b29e38ac0b070	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	Def2	False	Passed	Model Under Test Equivalent Model
65539af9c5c3bf57d4a2cce2491019e85dab0815	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def2	True	Passed	Model Under Test Equivalent Model
4d7882b2fa713badeb19539c19b1ce559699b579	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def2	False	Passed	Model Under Test Equivalent Model
d49790e0e965fe483e614157465f435686a51b58	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	Def2	True	Passed	Model Under Test Equivalent Model
313c688e69048a626b0be77c89a3c481793b286b	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	Def2	False	Passed	Model Under Test Equivalent Model
4b9f4c8277ebb93052eb4a4e2da693a3fb942ae3	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def2	True	Passed	Model Under Test Equivalent Model
ccb0183917efde3adf5dbf9c78792d88aacfe60d	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def2	False	Passed	Model Under Test Equivalent Model
73f71fed5844446f8292e3511cc8d45c2e54e53d	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def2	True	Passed	Model Under Test Equivalent Model
ddca2d65a3b3856b73f230b9fea0966b36916894	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def2	False	Passed	Model Under Test Equivalent Model
b542f5e901a416bc6029511480f9423e7cab1a82	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def2	True	Passed	Model Under Test Equivalent Model
7ecac8cbf17fc5af00967d7fc8864cd548b3ab2e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def2	False	Passed	Model Under Test Equivalent Model
7c3c227648568a2bc4a4124520b0f9337090a2ff	Apalache	BagBagToSet	Def2	True	Passed	Model Under Test Equivalent Model
a1ccd5b49e31144c3824048e3350646487d03bb0	Apalache	BagBagToSet	Def2	False	Passed	Model Under Test Equivalent Model
57ae6837b39bde8a5860401912f6fd035d3b654f	Apalache	BagSetToBag	Def2	True	Passed	Model Under Test Equivalent Model
680d8f38cec84c6f069dcf524beb61df62b1fed1	Apalache	BagSetToBag	Def2	False	Passed	Model Under Test Equivalent Model
74a300f00bb4db378359931a93f53ad14890142e	Apalache	BagBagIn	Def2	True	Passed	Model Under Test Equivalent Model
62352e796d995a65bff58134c979cb09eab6a574	Apalache	BagBagIn	Def2	False	Passed	Model Under Test Equivalent Model
6bcef2f0ee04e728c76b8206666f5ec3c9887e74	Apalache	BagAddBag	Def2	True	Passed	Model Under Test Equivalent Model
b58f17b2d2d0ec0c297cee62d4c1dba1e16fdaa9	Apalache	BagAddBag	Def2	False	Passed	Model Under Test Equivalent Model
fa12f64e3b8aa820a300106f6cb5ebcdc3a4a87f	Apalache	BagBagSub	Def2	True	Passed	Model Under Test Equivalent Model
a8322ee7805329595b70cb2bea92ca14f99c51c4	Apalache	BagBagSub	Def2	False	Passed	Model Under Test Equivalent Model
4d1dfa6c0d4380414fa56414f79eab8c07fd2943	Apalache	BagCopiesIn	Def2	True	Passed	Model Under Test Equivalent Model
57d807ac5e3869bb52c59f1c28a99c1c3f8dae20	Apalache	BagCopiesIn	Def2	False	Passed	Model Under Test Equivalent Model
ada400d94054ec6839df5fae7d379caf454ad87b	Apalache	BagSubsetEqBag	Def2	True	Passed	Model Under Test Equivalent Model
c45bb74d072285df93f95d0f4a3774dc3e804631	Apalache	BagSubsetEqBag	Def2	False	Passed	Model Under Test Equivalent Model
8c321cf1c02fe241cecc4b84079804a3a0331af9	Apalache	BagBagUnion	Def2	True	Passed	Model Under Test Equivalent Model
a406b953b8b197b735c4c963b1fbf6a20acc7975	Apalache	BagBagUnion	Def2	False	Passed	Model Under Test Equivalent Model
de3ef5c0bbaf34e6aea82b39de93b1ba95e2cdc6	Apalache	BagBagCardinality	Def2	True	Passed	Model Under Test Equivalent Model
1d047777306bb6b9d566700f25a72f2b4cfff1cc	Apalache	BagBagCardinality	Def2	False	Passed	Model Under Test Equivalent Model
0407ee6b9e34dac129677f937e10dca4a61dfe5f	Apalache	BagBagOfAll	Def2	True	Passed	Model Under Test Equivalent Model
dbb96dd8bf099b9c8d38dad2e1784a75f543345a	Apalache	BagBagOfAll	Def2	False	Passed	Model Under Test Equivalent Model
f301c5277dd714944eb349606f2fbbd7028e6177	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def2	True	Passed	Model Under Test Equivalent Model
3139774c41d979a19fdb1a9cf2f9ff4ec59a9234	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def2	False	Passed	Model Under Test Equivalent Model
2f67b0de460d09772a05d9c3154d75cac289f8d5	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	Def2	True	Passed	Model Under Test Equivalent Model
38475eacd2c8bb169404d63e9ed11e8081de08ee	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	Def2	False	Passed	Model Under Test Equivalent Model
f77f8d552df19db0c3497e817568ffc1d7105b30	Apalache	FiniteSetsCardinality	Def2	True	Passed	Model Under Test Equivalent Model
d1d91d8816935689798cc04622d8c71a3671b1c6	Apalache	FiniteSetsCardinality	Def2	False	Passed	Model Under Test Equivalent Model
4b2f0ea10e9f41536bde2e9cd98fb0605c9e8aaf	Apalache	SeqHead	Def2	True	Passed	Model Under Test Equivalent Model
8f56feff41c9a75902a9d4be10fa81b55ee1049b	Apalache	SeqHead	Def2	False	Passed	Model Under Test Equivalent Model
617589e423d3766568aac482534a172146bc6810	Apalache	SeqTail	Def2	True	Passed	Model Under Test Equivalent Model
b20f244d07b99324e28da88368479902e6b99147	Apalache	SeqTail	Def2	False	Passed	Model Under Test Equivalent Model
dd6817bb25f008609b2fd2c345546c2dbcef1de6	Apalache	SeqAppend	Def2	True	Passed	Model Under Test Equivalent Model
1be1c58b17eeb3e221dd314901f0d64ae4b10eaa	Apalache	SeqAppend	Def2	False	Passed	Model Under Test Equivalent Model

Index

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