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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
dd80968ec746decb8e6ebe405beca3cf91cd0e97	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1	OneLineComment	True	Passed	Model Under Test Equivalent Model
507bc6f6de200b2642df9dc5683bada1eba8c130	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1	OneLineComment	False	Passed	Model Under Test Equivalent Model
6170127e9e27daa576a6867730b20925f636a5b6	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1	MultiLineComment	True	Passed	Model Under Test Equivalent Model
e5bd5b29bc2f597bda67256acd6e62241ec9251c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1	MultiLineComment	False	Passed	Model Under Test Equivalent Model
d5ab2c5538d30760fda1472bd2640bc8e80d4f34	Apalache	Def1	BoolTrue	True	Passed	Model Under Test Equivalent Model
73ed24839f128909c916f2a984a456ba3714bf27	Apalache	Def1	BoolTrue	False	Passed	Model Under Test Equivalent Model
63a6965e320c77c34094ca144b902cf9d07b79c8	Apalache	Def1	BoolFalse	True	Passed	Model Under Test Equivalent Model
8e3dceac7856ac3f42895d2f3963744da2e50bc8	Apalache	Def1	BoolFalse	False	Passed	Model Under Test Equivalent Model
59a0860a91e746da4e2ec868962c41c1357f6a64	Apalache	Def1	BoolSet	True	Passed	Model Under Test Equivalent Model
fc49f0cd779e6a0a508a7050566dd4e3183be4fd	Apalache	Def1	BoolSet	False	Passed	Model Under Test Equivalent Model
7f776639b1b78fab1036f26266fc998f1d0e15b8	Apalache	Def1	And	True	Passed	Model Under Test Equivalent Model
9c3f454a94001ee9c3c812479073ea9cc71eb561	Apalache	Def1	And	False	Passed	Model Under Test Equivalent Model
d1cccda168e87509554629d265387c34ea43d8c7	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def1	AndMultiLine	True	Passed	Model Under Test Equivalent Model
eeb503cc579f1be531b544d887b63e880cb3cece	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def1	AndMultiLine	False	Passed	Model Under Test Equivalent Model
ad4e92dce466deb320745897c28efa9ecd1c671b	Apalache	Def1	Imply	True	Passed	Model Under Test Equivalent Model
9817360065de5fa02e4999ddacc84cd51fb4dcde	Apalache	Def1	Imply	False	Passed	Model Under Test Equivalent Model
b8eb1a420db359a882b2edb725aa38e1d50dbb17	Apalache	Def1	Not	True	Passed	Model Under Test Equivalent Model
9254870bf23a7263621c1dd2527f210512e54673	Apalache	Def1	Not	False	Passed	Model Under Test Equivalent Model
37b395effc67f9f6b2584b7c093a016b95f8b077	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def1	Or	True	Passed	Model Under Test Equivalent Model
37fe98d66dfbc59b3623e82b167996c7fa8a3d6a	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def1	Or	False	Passed	Model Under Test Equivalent Model
6f158b4c448f19a3cafeeb044747e0b39562a519	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def1	OrMultiLine	True	Passed	Model Under Test Equivalent Model
1b954e6936655bf1858d3715bc93f400591981fe	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def1	OrMultiLine	False	Passed	Model Under Test Equivalent Model
e92348a84e044ab29a1a46d7e04fb2f0cf931f79	Apalache	Def1	AndProp	True	Passed	Model Under Test Equivalent Model
2c78896c3562525053d6a2351b9212c366c2de1e	Apalache	Def1	AndProp	False	Passed	Model Under Test Equivalent Model
b2764bdde952b581ea57a9b4cc3c9d15e04cefa9	Apalache	Def1	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
41b3104fca3384e9525d42ba801375965de689db	Apalache	Def1	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
0c61d7ed4fcd4d16ee042cd23aa31d1cb8756eda	Apalache	Def1	Eq	True	Passed	Model Under Test Equivalent Model
2c2c2f8c153fb9d2033742893a6d1d3fa7f9f7df	Apalache	Def1	Eq	False	Passed	Model Under Test Equivalent Model
97f238e69ee350bb864c9d9938e2cc602f0ff5ef	Apalache	Def1	Ne	True	Passed	Model Under Test Equivalent Model
aacfecdac09094444831a9e9de82c74527cb0196	Apalache	Def1	Ne	False	Passed	Model Under Test Equivalent Model
275dd483d9ef6cd4cf8e87ebd6945eddd892dc19	Apalache	Def1	Let	True	Passed	Model Under Test Equivalent Model
bc4423d71190f984db3cfa49207e68ecb1ca86e6	Apalache	Def1	Let	False	Passed	Model Under Test Equivalent Model
7f368df6855ac7d8e28ab699c020c95072ed8899	Apalache	Def1	SetEmpty	True	Passed	Model Under Test Equivalent Model
6003cf967d2ca652cea374a5ea60f7160e3c32b9	Apalache	Def1	SetEmpty	False	Passed	Model Under Test Equivalent Model
e28bd3a42e058f717b04c127a4def461a6d4ec74	Apalache	Def1	Set0	True	Passed	Model Under Test Equivalent Model
85f62bff8d39d8b6577236ce3fd23e1635784e0a	Apalache	Def1	Set0	False	Passed	Model Under Test Equivalent Model
4d9d144d677bf798c55ab70d4488c7bc9a55eb85	Apalache	Def1	Set1	True	Passed	Model Under Test Equivalent Model
74905f1ad84615425f92401b83a3c5c40efdc630	Apalache	Def1	Set1	False	Passed	Model Under Test Equivalent Model
c676b62faa75596d351782856ca25d571950afdf	Apalache	Def1	Set2	True	Passed	Model Under Test Equivalent Model
e431d12862eb5d74d3d71a00f43e12bfdef3a309	Apalache	Def1	Set2	False	Passed	Model Under Test Equivalent Model
a5b7b505753066060433563c4662ba92459413f1	Apalache	Def1	Fun	True	Passed	Model Under Test Equivalent Model
f2b032d7f36eea9b381df60c17cd71a6c8487c0f	Apalache	Def1	Fun	False	Passed	Model Under Test Equivalent Model
8c48c2ce27d95e36026732cf344aa00772584b4d	Apalache	Def1	In	True	Passed	Model Under Test Equivalent Model
cc55cd2c6f00d2200a27dcba102b2684c7d4fe6b	Apalache	Def1	In	False	Passed	Model Under Test Equivalent Model
06d42f8c76d8980f196c75eb395cad0c1655b703	Apalache	Def1	NotIn	True	Passed	Model Under Test Equivalent Model
351ba44d780524a2887fba01b6dc3d02f3415225	Apalache	Def1	NotIn	False	Passed	Model Under Test Equivalent Model
ac81c5edd195b333d629d3a4a5c0cff2899d8f3f	Apalache	Def1	Exists	True	Passed	Model Under Test Equivalent Model
27de23117c5b9f302c7c359570e821c9c69b3b63	Apalache	Def1	Exists	False	Passed	Model Under Test Equivalent Model
312ab1038e9a6b09e7f413aa0a657d723e29363f	Apalache	Def1	Forall	True	Passed	Model Under Test Equivalent Model
fb872562f201dd26bc7c583e45ca71d29e0f0131	Apalache	Def1	Forall	False	Passed	Model Under Test Equivalent Model
a5d2c1f71e42bc40a2aa28362a53b04a79b60395	Apalache	Def1	Choose	True	Passed	Model Under Test Equivalent Model
01ceac66a575d83811ca802f1a5d42e5c7efc1f5	Apalache	Def1	Choose	False	Passed	Model Under Test Equivalent Model
c7ddf93285d9a9c8f44dbfbabcb0f524a27cc59d	Apalache	Def1	Record	True	Passed	Model Under Test Equivalent Model
60acf39604d66e747583a5aea4a6279a28c86116	Apalache	Def1	Record	False	Passed	Model Under Test Equivalent Model
ddda5e8ce1230e033bd7b0dffc14892ffc34930f	Apalache	Def1	Tuple	True	Passed	Model Under Test Equivalent Model
d73777aef916ae2e14d51199e9679600c1b864ba	Apalache	Def1	Tuple	False	Passed	Model Under Test Equivalent Model
b8377c78ae8df4c710eefc8c2b147982de7edaae	Apalache	Def1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
ec5b32414851a72be5fece50ddc0b0af6e71dcdc	Apalache	Def1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
64c6d0c61889ab297ad6087a6b99c45551a49140	Apalache	Def1	FunApp	True	Passed	Model Under Test Equivalent Model
f2ff4ced1bc3454ee9bde30fe0b92bbe3f32522e	Apalache	Def1	FunApp	False	Passed	Model Under Test Equivalent Model
ca6b95fc307ed909030494d452081ad2f2697b24	Apalache	Def1	Prime	True	Passed	Model Under Test Equivalent Model
bdf315726129a0a178264a4aeb030a6079435947	Apalache	Def1	Prime	False	Passed	Model Under Test Equivalent Model
1f72d0f1ccfc8e5ed0f0b373f560020e46bc51de	Apalache	Def1	NumZero	True	Passed	Model Under Test Equivalent Model
48b7db5835658a46be82bcc1212cd040b98661c1	Apalache	Def1	NumZero	False	Passed	Model Under Test Equivalent Model
42a18cdbfe483090678b209983f0587465859faf	Apalache	Def1	NumOne	True	Passed	Model Under Test Equivalent Model
123cd7e7e78ad45e05cf5cff30782def8519a38d	Apalache	Def1	NumOne	False	Passed	Model Under Test Equivalent Model
e13f1e1f0d56550fd80a2745cc8c90159f7b318e	Apalache	Def1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
30b08072f48c5792e5d92df0ebee7d80e25726c4	Apalache	Def1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
240c7348f0019fdf6656fdee9f866a7b452fa0a3	Apalache	Def1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e46486331f5fae2c76b9d53d38ce7e7c7e775e4b	Apalache	Def1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a8e1db3a345c1e51c32a9621c83405ab965613be	Apalache	Def1	NumPlus	True	Passed	Model Under Test Equivalent Model
ce5728a3262819d0c494cc4df7849bcfe19c293b	Apalache	Def1	NumPlus	False	Passed	Model Under Test Equivalent Model
afb20ee727ea482b96ae6bd0b7b4a032d882eb25	Apalache	Def1	NumMinus	True	Passed	Model Under Test Equivalent Model
c059369daaa32b840ae754c1904a39691edba538	Apalache	Def1	NumMinus	False	Passed	Model Under Test Equivalent Model
4c072b3b26d5b5fbad6b8216bb077146a7387d43	Apalache	Def1	NumMul	True	Passed	Model Under Test Equivalent Model
e962fa347470fff34c5b8fbad4a2d4713eb00ea5	Apalache	Def1	NumMul	False	Passed	Model Under Test Equivalent Model
f9c589ac95c4f59cdcbd7ca0f2a90f51567d30f8	Apalache	Def1	NumDiv	True	Passed	Model Under Test Equivalent Model
2f784ea80c6132622b8ba91e9df8c6026d207462	Apalache	Def1	NumDiv	False	Passed	Model Under Test Equivalent Model
791d4e601c0f6fb539ad194c33727b53e7d8906a	Apalache	Def1	NumMod	True	Passed	Model Under Test Equivalent Model
8e0c15f24724787e15a63638a6bcb8ad85efbdcf	Apalache	Def1	NumMod	False	Passed	Model Under Test Equivalent Model
b2d9d4bf52c454751587cf6975856a44a012d578	Apalache	Def1	NumPow	True	Passed	Model Under Test Equivalent Model
bfcc554d6d07692a1c3b4ed64033825b606a1ce3	Apalache	Def1	NumPow	False	Passed	Model Under Test Equivalent Model
0625251670b585605ae9b0fab466ffc184158cc4	Apalache	Def1	NumGt	True	Passed	Model Under Test Equivalent Model
b7b5db548e983635811e1a17c80eb430187b990c	Apalache	Def1	NumGt	False	Passed	Model Under Test Equivalent Model
ba33ba2acabed7abe45165df2a7a084742bb5154	Apalache	Def1	NumGe	True	Passed	Model Under Test Equivalent Model
7cf0470a59ea5e3ce99cb95c3791adcde38eceb8	Apalache	Def1	NumGe	False	Passed	Model Under Test Equivalent Model
8240736cf52e014cfe3fd3f26da1c8282f379483	Apalache	Def1	NumLt	True	Passed	Model Under Test Equivalent Model
98be8f91718090dd076575b78e168fdd0991a726	Apalache	Def1	NumLt	False	Passed	Model Under Test Equivalent Model
3824c7952a66252642eb716438e1ecb3fa6a8924	Apalache	Def1	NumLe	True	Passed	Model Under Test Equivalent Model
7d2c249cf23f556e8f01a55c7075a5301baa24e3	Apalache	Def1	NumLe	False	Passed	Model Under Test Equivalent Model
9896c3bfd98371454c1b028fe64d0232d21e963c	Apalache	Def1	DefFun	True	Passed	Model Under Test Equivalent Model
98f86f187368a7603bd5acaa7b714294ab255ef4	Apalache	Def1	DefFun	False	Passed	Model Under Test Equivalent Model
32d3ccc35dfdffac7129149a92d1a0a0d05260db	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDefFun	True	Passed	Model Under Test Equivalent Model
0c349e3c4a7e6609e1e162b945ea5a64a547f0b8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDefFun	False	Passed	Model Under Test Equivalent Model
ecc46143ca53f1f394eb5bfcd9d9e244a634dc1e	Apalache	Def1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
efb4e80e6554d5bf33566b9a3641c0dd48572497	Apalache	Def1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
59bbd678f2d9966059836f24ce0e6f13500815ae	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
e8a756e52b6a6012d8434eaca3ea1674d4888daa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
4093b068199c3a07a1c7ce2b7e20a06be31000eb	Apalache	Def1	Def0	True	Passed	Model Under Test Equivalent Model
03dbfd8da02eaef70596cb2073acfbc02c903b3a	Apalache	Def1	Def0	False	Passed	Model Under Test Equivalent Model
b16bff2e7eae1c1fdf242bcb65ec0eb30a01c458	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef0	True	Passed	Model Under Test Equivalent Model
71422bf59e16f643180bb392713792c264045b0a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef0	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
39faccbae2b8b2f4c2ab966692deb1f835debcea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1	True	Passed	Model Under Test Equivalent Model
6a9fe1337266e778d84903a4c7d43b8280de39f0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1	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
15fd8352436b24c720fd1013bb5c41c379674161	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef2	True	Passed	Model Under Test Equivalent Model
8a77ced032342bf9d979b7f3ded84c1c827b8d93	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef2	False	Passed	Model Under Test Equivalent Model
b4fbba4d895a8c87751176e066d3bac459034c7c	Apalache	Def1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b96185cd2e25fd5b5db6e5eb274694f6f5d146b6	Apalache	Def1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c263d9a2ab7c489c55e9d8ef82dffdc76eb3989d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
3abeb4bcf2124c4553f6112fbfc89baab4ab2fe0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
3a05c928cafecfb4ea48c702f4a942be6fa0db2b	Apalache	Def1	Extends	True	Passed	Model Under Test Equivalent Model
7ec01dbe998b67f509b274a996280e6a44831830	Apalache	Def1	Extends	False	Passed	Model Under Test Equivalent Model
d2f9bf4069a06ab7599c42618565e61ff0300a2c	Apalache	Def1	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
d10e88aa9e3930f69cd9fed3750cef1a3ea60713	Apalache	Def1	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
d6edc0482dc0fe51f657c7ff07ec5d070fe9b8d0	Apalache	Def1	Variable	True	Passed	Model Under Test Equivalent Model
ddda8fa643cc059d0539b5f7587d201b598dd474	Apalache	Def1	Variable	False	Passed	Model Under Test Equivalent Model
9903f0eff835545930a923674a4412c108914939	Apalache	Def1	Constant	True	Passed	Model Under Test Equivalent Model
161213d9ed29eeb9e5124d3282a33a70e83c7e87	Apalache	Def1	Constant	False	Passed	Model Under Test Equivalent Model
ab4653feb8e086e869ca4fa3d879a1f7536b37c0	Apalache	Def1	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
9e0451f6c522ca7068c2ec9494d34110a03ddabb	Apalache	Def1	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
02640d4cebd3814e5eb0c6da60c07ec17a75dc89	Apalache	Def1	ConstantRank1	True	Passed	Model Under Test Equivalent Model
95698b2ffb904d7f6f9a1d046cb8ced281d1e893	Apalache	Def1	ConstantRank1	False	Passed	Model Under Test Equivalent Model
263e0c7ae4764930461e32749ac3304f1e68422d	Apalache	Def1	Instance	True	Passed	Model Under Test Equivalent Model
41760e766de13787ef8612843abee133227e1fe0	Apalache	Def1	Instance	False	Passed	Model Under Test Equivalent Model
ca1d327bf78b8f58f6a9af79fb779bd0e1d1f6b2	Apalache	Def1	InstanceWith	True	Passed	Model Under Test Equivalent Model
657b9f30aa0022cdf60b7b68201c5aa8a82a80e4	Apalache	Def1	InstanceWith	False	Passed	Model Under Test Equivalent Model
0fb0cc8878929fc173372715c38cc5baac417d23	Apalache	Def1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
43e0addc28bbc00b6c25bd716c2d086dcfe1741b	Apalache	Def1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
0aff824aa2aee5fd009f6fac03352dd4f53c8373	Apalache	Def1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
61ba432282000c2daf56f0cc4992593da25138e0	Apalache	Def1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9bd5c37e5be3df06014efd9a41e27269e72e650e	Apalache	Def1	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
a765aede3510372b63dfb2ed7e920a50b991d9f8	Apalache	Def1	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
4808f4ea12b31c5c8406be74e8abb60d6a19a5fa	Apalache	Def1	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
447fdfd9ff74c384d0aa678fa9746dcf57ca50b7	Apalache	Def1	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
f5a3a872b73853eafc2bad9008429d87be6adaf6	Apalache	Def1	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
deaa409ab2291597399b568808d0166c5c915dfb	Apalache	Def1	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
2ccde5feda1337be9e83557c93ca86408883d72d	Apalache	Def1	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
47b5bc8d89308244479804671625f239f709760d	Apalache	Def1	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
cfc4116e031495f37c9242cdfb0f7d8052514641	Apalache	Def1	Enabled	True	Passed	Model Under Test Equivalent Model
dd51ea6886abe6219eff697b3519491a834ad827	Apalache	Def1	Enabled	False	Passed	Model Under Test Equivalent Model
e0320857d1e6af37ea868a45948a9d68964bf4d5	Apalache	Def1	Cross2	True	Passed	Model Under Test Equivalent Model
475394aea60e80cf2da523cf4e51e4ec3244cf97	Apalache	Def1	Cross2	False	Passed	Model Under Test Equivalent Model
0618f662eec8d3faff02acc1e1e73c49ad99ebe1	Apalache	Def1	Cross3	True	Passed	Model Under Test Equivalent Model
2b74cedab86301219a1407517f2ae3535a6955aa	Apalache	Def1	Cross3	False	Passed	Model Under Test Equivalent Model
20c2f6284247bf02db553ea03bb38a2d259c4844	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))	Def1	FunSet	True	Passed	Model Under Test Equivalent Model
cbd6145300dac6e257c38d3b760534f3899ba94d	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))	Def1	FunSet	False	Passed	Model Under Test Equivalent Model
c3516e049ffe6a756c23e58d33587c11ab1c283f	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)	Def1	RecordSet	True	Passed	Model Under Test Equivalent Model
f6a2aad2a2d66604737772de2b8292e2cabb894d	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)	Def1	RecordSet	False	Passed	Model Under Test Equivalent Model
fc3b592e0a46be08ccb8bf16bd73e22a0d6a8264	Apalache	Def1	SetDiff	True	Passed	Model Under Test Equivalent Model
4765998dbfc7d370a282266a1ba3b77bf5e928c8	Apalache	Def1	SetDiff	False	Passed	Model Under Test Equivalent Model
afb7840ec2bbad6a315c80807015a18a482a4908	Apalache	Def1	SetUnion	True	Passed	Model Under Test Equivalent Model
54d9a3ed6cb3e5294564a3974d85b57ec9dcf46c	Apalache	Def1	SetUnion	False	Passed	Model Under Test Equivalent Model
3a937651f7121892d709b95774a48fd1694fab7b	Apalache	Def1	SetIntersect	True	Passed	Model Under Test Equivalent Model
8d70b289578361fae57486179d39a4c653fb93c0	Apalache	Def1	SetIntersect	False	Passed	Model Under Test Equivalent Model
fcff809e0e0261e6bbf5811c8630237b99a36a86	Apalache	Def1	SubsetEq	True	Passed	Model Under Test Equivalent Model
9390a4f961de0be59055656c9fc91492f360c487	Apalache	Def1	SubsetEq	False	Passed	Model Under Test Equivalent Model
79b624dc87221e4c02b59bf48722225fb1285551	Apalache	Def1	IfCond	True	Passed	Model Under Test Equivalent Model
929ca68e4a38e621c79623c21bf17eebec219834	Apalache	Def1	IfCond	False	Passed	Model Under Test Equivalent Model
91eca33a4521d550073970e4977777ac7fa37e0d	Apalache	Def1	IfThen	True	Passed	Model Under Test Equivalent Model
e6337964ec553bd8eebdd124fee3c3e01b154605	Apalache	Def1	IfThen	False	Passed	Model Under Test Equivalent Model
7a3370238ec62e28045d3fc59e6002894fb42f65	Apalache	Def1	IfElse	True	Passed	Model Under Test Equivalent Model
c50eea1fca898d2c2dc4e184f0ad793efae2bb2b	Apalache	Def1	IfElse	False	Passed	Model Under Test Equivalent Model
8d01c41eca61b746a4437b65732b21482131d64f	Apalache	Def1	Subset	True	Passed	Model Under Test Equivalent Model
0056aa995a02d7c2c0b5dfacdfa3b1061c606703	Apalache	Def1	Subset	False	Passed	Model Under Test Equivalent Model
7b92e108538d9287e29f3d493c97ed301c61148d	Apalache	Def1	Domain	True	Passed	Model Under Test Equivalent Model
837c9388994ff8c20956a6f4f1219da64b47b796	Apalache	Def1	Domain	False	Passed	Model Under Test Equivalent Model
8c736528ad5af45b7f6c1c1c7b4d573d492335eb	Apalache	Def1	Union	True	Passed	Model Under Test Equivalent Model
095bff046bd8c99a08a2909598d2e0b6b2389a24	Apalache	Def1	Union	False	Passed	Model Under Test Equivalent Model
ab17cf2f98df7844660d8706512f020a5c41e1b5	Apalache	Def1	Unchanged	True	Passed	Model Under Test Equivalent Model
95b6677e6499d7ef1a6651ed177c3b32a01231a3	Apalache	Def1	Unchanged	False	Passed	Model Under Test Equivalent Model
b4938e4d7d38442fe7f295f26cdc6009df687e0b	Apalache	Def1	Equivalence	True	Passed	Model Under Test Equivalent Model
19c40587b5c30e8e67ac2a8f346665bb6f109f11	Apalache	Def1	Equivalence	False	Passed	Model Under Test Equivalent Model
3c138ce75469a7e3154af9f15b29aed00313aeb1	Apalache	Def1	StringEmpty	True	Passed	Model Under Test Equivalent Model
bb6bd55a0cd0e27e59fd91aaa99cf4ce3c927693	Apalache	Def1	StringEmpty	False	Passed	Model Under Test Equivalent Model
b8cf41322e8694d7b87c94a04293ffaf243dd4f0	Apalache	Def1	String	True	Passed	Model Under Test Equivalent Model
0418e2022a45c8d20c6b45e0d47eb8db4e3176f7	Apalache	Def1	String	False	Passed	Model Under Test Equivalent Model
c6fd04dac62f826f96eb478a054b9e529080b9c6	Apalache	Def1	SeqLen	True	Passed	Model Under Test Equivalent Model
c7a4eaab357269a4360ec76a045887229a5fe0b6	Apalache	Def1	SeqLen	False	Passed	Model Under Test Equivalent Model
8ed8cd8abc40925309defcfe44c9b64f75e9820f	Apalache	Def1	SeqConcat	True	Passed	Model Under Test Equivalent Model
3ea8757a8ed777223ad4e3af4d845498ef3b3aee	Apalache	Def1	SeqConcat	False	Passed	Model Under Test Equivalent Model
6d66a1733a02619b49553b1bea833a08e93c1849	Apalache	Def1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
a74cd0e79928c5dc26221929e5fa019d93057f96	Apalache	Def1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
823b4f7fc52c582e47303f7422f9f5fd75d3073f	Apalache	Def1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
5f5decf7f000f47f15d898a164e5cfa1b2372a11	Apalache	Def1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
88fa8aa1712df2d777a03f218e01ae4001b940fb	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	Def1	NumRange	True	Passed	Model Under Test Equivalent Model
5f7bb867b441350b390a1bb3f87cc39c8f232e86	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	Def1	NumRange	False	Passed	Model Under Test Equivalent Model
2dac74f1cac81dda1b36485e6ae774bae8fe384b	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def1	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
654c72a1b3a8c139778f5cc0619f385397f58816	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def1	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
af5f603b2f83a439b9dba86ae8c10dbbbb963401	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]]	Def1	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
78aa281be14d20f25b7ce04fca1ea4a0ad2e9d9e	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]]	Def1	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
b4e10863010c68c4ef3b7a15b7ffc8c5578e5172	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def1	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
3c589d00f752e182c0faf4f955c4d60136541162	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def1	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
c88e57fd86a06c0051851319580ecd0d250a2b3a	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def1	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
e407aba7dd3270d1d726ba789eb7493e7fd7bfe2	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def1	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
c2b0b908cd1abd9c25f4c548ae545ae961375e3f	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def1	TlcEval	True	Passed	Model Under Test Equivalent Model
b9f5888b457ec06baca8538a92cf020e72125485	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def1	TlcEval	False	Passed	Model Under Test Equivalent Model
b9611b5f31c3dd8b5dd163fcdafa9e709f9f2b1b	Apalache	Def1	BagBagToSet	True	Passed	Model Under Test Equivalent Model
31d851321039d3b7a3167b2b1ba74e0e2c3b4360	Apalache	Def1	BagBagToSet	False	Passed	Model Under Test Equivalent Model
a99cf7c70ed1c5c26adac6dc38e99e9e5d73fadb	Apalache	Def1	BagSetToBag	True	Passed	Model Under Test Equivalent Model
fba5be1f2041ea534137a7cb0c9666c1333d0880	Apalache	Def1	BagSetToBag	False	Passed	Model Under Test Equivalent Model
49a6848e5a881104f938be4950979cac73c5d398	Apalache	Def1	BagBagIn	True	Passed	Model Under Test Equivalent Model
0d17cd6f039e1ce7e0be9941f8aa0730706fa483	Apalache	Def1	BagBagIn	False	Passed	Model Under Test Equivalent Model
2d5c339aaa8614713472b38c5eff50ed422305f1	Apalache	Def1	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
fb40b356f03a41a6130c8fd1b7a2ba2f9ddcab56	Apalache	Def1	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
ec63c8d7c5492b58a7367bc8869b3a66562134e2	Apalache	Def1	BagAddBag	True	Passed	Model Under Test Equivalent Model
0104fb2908fa8fe66c86e0b1f279e81cb16cfdce	Apalache	Def1	BagAddBag	False	Passed	Model Under Test Equivalent Model
8991a0afa3694735e5a028848f0167bc7741f869	Apalache	Def1	BagBagSub	True	Passed	Model Under Test Equivalent Model
09de55403d23ae491c485532200219cca9cbb42b	Apalache	Def1	BagBagSub	False	Passed	Model Under Test Equivalent Model
dc89be145e573921bdfe81ccf7ce1f6550485cfe	Apalache	Def1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
c10560ac6b3b4cb9ffa7a7d3cccba20b81c7333e	Apalache	Def1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
2d7b49195e2c26216a096e21e559173a6815172e	Apalache	Def1	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
a6ab4d59c22ddc907013b22d89454123d2c5a229	Apalache	Def1	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
471b536e6f21a40a8b0249a285aaa2383e3398c2	Apalache	Def1	BagBagUnion	True	Passed	Model Under Test Equivalent Model
6ed6c2a156a592f3fa6e65b03a694af699734938	Apalache	Def1	BagBagUnion	False	Passed	Model Under Test Equivalent Model
8d7c63a76bb49e5308f000d7c8a7b47887ffa122	Apalache	Def1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
ea93565d5ee7cdd29314748ea9b38a216fe3b8b0	Apalache	Def1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
6f2d543df1dd1a0ee00569cac8abeda42aa59438	Apalache	Def1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
3fb5ccbac9172713d309e4a5957fa5918260d32b	Apalache	Def1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
41486844dfe15d55ff783473ff0b1cb22b24fffb	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def1	BagSubBag	True	Passed	Model Under Test Equivalent Model
7555c65b8beb14abdf3d40a72193e98f9682681b	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def1	BagSubBag	False	Passed	Model Under Test Equivalent Model
eea628ed4e5d40ea82eb3b3c8496cbb5e1eaf36a	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)	Def1	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
21e0692306286c392a755a1ccb2e8ef3bf101802	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)	Def1	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
ee25b57d68d610b93d8141783ee5d45eb56f63b0	Apalache	Def1	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
51e4e4919d410515570e1d189e087762850b9429	Apalache	Def1	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
b526b5bbb0c3ddefabd0f396dd0c3817216b3a39	Apalache	Def1	SeqHead	True	Passed	Model Under Test Equivalent Model
1e9200949a4b43c0f9ec43a5e2dd6de3311acbbf	Apalache	Def1	SeqHead	False	Passed	Model Under Test Equivalent Model
70ea49ce445407f60bae052f194315e31caa1a55	Apalache	Def1	SeqTail	True	Passed	Model Under Test Equivalent Model
55ef4ec6f5cc895f4abdebfd464d9ec5091b8047	Apalache	Def1	SeqTail	False	Passed	Model Under Test Equivalent Model
fde633b3e7ecf2b798c4fe93edfc43d9f93535f8	Apalache	Def1	SeqAppend	True	Passed	Model Under Test Equivalent Model
99f5cac9a3e44f5ce4ed2174273aad6f3490902f	Apalache	Def1	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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