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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
e98eed489c6e4d88c0fb400a73deb5cf7d4bfd26	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	ConstantRank1	OneLineComment	True	Passed	Model Under Test Equivalent Model
30fd8ae33ec3ad1897042aae241fc5ff27efb6db	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	ConstantRank1	OneLineComment	False	Passed	Model Under Test Equivalent Model
113cb6fbc1a25321a28eba095ba2225624489049	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	ConstantRank1	MultiLineComment	True	Passed	Model Under Test Equivalent Model
1a3a124a0406fe55997cb57938edbbf0dc714d83	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	ConstantRank1	MultiLineComment	False	Passed	Model Under Test Equivalent Model
91a6c3fab779a32883214f9fed7e608cfc9d7e2c	Apalache	ConstantRank1	BoolTrue	True	Passed	Model Under Test Equivalent Model
39f01450c267eca7ddb64cc9ffe8ee8bd23e66ea	Apalache	ConstantRank1	BoolTrue	False	Passed	Model Under Test Equivalent Model
8a53be181bfc52e45d54259ff9e32ef1259ab05a	Apalache	ConstantRank1	BoolFalse	True	Passed	Model Under Test Equivalent Model
abe6cbd06db1ab6bfbe4f223540ef66cee7158a6	Apalache	ConstantRank1	BoolFalse	False	Passed	Model Under Test Equivalent Model
b5af8245bed8213fba673bfa42c9ff39c1bc5f9d	Apalache	ConstantRank1	BoolSet	True	Passed	Model Under Test Equivalent Model
614adbc36211770826f238501f69350aab4bf6a1	Apalache	ConstantRank1	BoolSet	False	Passed	Model Under Test Equivalent Model
2a93d2d25c35132bd4d82ee9be0983ba1b9af77d	Apalache	ConstantRank1	And	True	Passed	Model Under Test Equivalent Model
59114fc8bcd249335780b10db41f681165fe42c6	Apalache	ConstantRank1	And	False	Passed	Model Under Test Equivalent Model
75d468260d311fdd64782d2a15a55356aae61db8	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	ConstantRank1	AndMultiLine	True	Passed	Model Under Test Equivalent Model
649b2c7b5a1ac489fac77f9810f9802c3aca163d	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	ConstantRank1	AndMultiLine	False	Passed	Model Under Test Equivalent Model
c5ce94d5353f8560e585542ebbcf2ada17770264	Apalache	ConstantRank1	Imply	True	Passed	Model Under Test Equivalent Model
5acb6e06ef10ab725d8d22a91303499730526305	Apalache	ConstantRank1	Imply	False	Passed	Model Under Test Equivalent Model
009c74d7c74476a0c3f5671e997d7916ccd6cccb	Apalache	ConstantRank1	Not	True	Passed	Model Under Test Equivalent Model
9316b4c2b916b37b5c75be6e3c9660c4bf56a12d	Apalache	ConstantRank1	Not	False	Passed	Model Under Test Equivalent Model
489962ec7040bd01f5336b0beb1acb36f2d32873	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	ConstantRank1	Or	True	Passed	Model Under Test Equivalent Model
d747e5ed605ceef11117055767dcde8fc0298d52	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	ConstantRank1	Or	False	Passed	Model Under Test Equivalent Model
6125218131d98d2b341c39b7dff4f67d645a63e6	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	ConstantRank1	OrMultiLine	True	Passed	Model Under Test Equivalent Model
6ff0606262d54bab9fcfbee320b7d857fb26f5a7	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	ConstantRank1	OrMultiLine	False	Passed	Model Under Test Equivalent Model
312ef687aa998afe4d6ab67a64ba423130751d04	Apalache	ConstantRank1	Eq	True	Passed	Model Under Test Equivalent Model
6f451a7f0d00409d80e9f15d23f345dbf55ac903	Apalache	ConstantRank1	Eq	False	Passed	Model Under Test Equivalent Model
beb054b4de9325f8dee2a10b632da5ef447c8e65	Apalache	ConstantRank1	Ne	True	Passed	Model Under Test Equivalent Model
c5a7d183ca7aba1f93d3e4746de6787fdf7e3412	Apalache	ConstantRank1	Ne	False	Passed	Model Under Test Equivalent Model
c7f2c8b838e8bd65dbb241ccc3a851cb1da6d05c	Apalache	ConstantRank1	Let	True	Passed	Model Under Test Equivalent Model
b93a6b2cb6a78bc76c92929da81bbb4de682e8aa	Apalache	ConstantRank1	Let	False	Passed	Model Under Test Equivalent Model
4a11b3d8e3fd4a58aaf63dfb6f30676b2ab935a4	Apalache	ConstantRank1	SetEmpty	True	Passed	Model Under Test Equivalent Model
bb6cfca72e3a038eb2a47b50f4379901f00ec36f	Apalache	ConstantRank1	SetEmpty	False	Passed	Model Under Test Equivalent Model
778d644674d61cb383e2f14969dcf1c18ebcee8e	Apalache	ConstantRank1	Set0	True	Passed	Model Under Test Equivalent Model
ac0bf5fc0c1fd283149bbd191e69a471e1553d80	Apalache	ConstantRank1	Set0	False	Passed	Model Under Test Equivalent Model
ffa7b3dc422d89a2065d4db6cc2749b2080816e8	Apalache	ConstantRank1	Set1	True	Passed	Model Under Test Equivalent Model
4f819e927ce7c2b5e883f53425f32b3feaccd8d9	Apalache	ConstantRank1	Set1	False	Passed	Model Under Test Equivalent Model
6bb75e8c7d3cec138c32ea785cdd50cd77e6882a	Apalache	ConstantRank1	Set2	True	Passed	Model Under Test Equivalent Model
38deba176cdbf83bb6d6ae6f844b231fa4bbb23d	Apalache	ConstantRank1	Set2	False	Passed	Model Under Test Equivalent Model
01a27a53f9569f5424031e1bc033532ee4a57241	Apalache	ConstantRank1	Fun	True	Passed	Model Under Test Equivalent Model
0bc53621141d0374c72daca0c3ed782e5030de92	Apalache	ConstantRank1	Fun	False	Passed	Model Under Test Equivalent Model
fa18214ca2017d550e6469c2efa06acb4c1731de	Apalache	ConstantRank1	In	True	Passed	Model Under Test Equivalent Model
26c5555bdb0620134e583e2246a3ac360c77f8c4	Apalache	ConstantRank1	In	False	Passed	Model Under Test Equivalent Model
99baa549a33446f3c9e871c0cf0f6bde933bf22d	Apalache	ConstantRank1	NotIn	True	Passed	Model Under Test Equivalent Model
a7f3bdfa9a4b285990803ff062323a7456fc2ec0	Apalache	ConstantRank1	NotIn	False	Passed	Model Under Test Equivalent Model
83aaf308c8c1fa630b334739a3f65b657a349327	Apalache	ConstantRank1	Exists	True	Passed	Model Under Test Equivalent Model
1a9b4c2d0e042bc8ddb84271d783173d600e0d78	Apalache	ConstantRank1	Exists	False	Passed	Model Under Test Equivalent Model
4591f6d132751ba8e1aa09a2e7dade308024dd33	Apalache	ConstantRank1	Forall	True	Passed	Model Under Test Equivalent Model
464a4cbafad05d3db29f4aa3983d0837242df721	Apalache	ConstantRank1	Forall	False	Passed	Model Under Test Equivalent Model
a99792b21f95b16e0ed2b359bdebda7d07d65492	Apalache	ConstantRank1	Choose	True	Passed	Model Under Test Equivalent Model
6424adb1ff6e99a0e10789288981006e7fb74c43	Apalache	ConstantRank1	Choose	False	Passed	Model Under Test Equivalent Model
e06a96858137602afc0dd395fb4273fbbd3e2bc6	Apalache	ConstantRank1	Record	True	Passed	Model Under Test Equivalent Model
a058d5367e6a1a9bbf3e8b651b50f312c03f1e27	Apalache	ConstantRank1	Record	False	Passed	Model Under Test Equivalent Model
369910e6efca2a7a8006285c6a133807badb825d	Apalache	ConstantRank1	Tuple	True	Passed	Model Under Test Equivalent Model
3da398f011920c269c698e9fe19dc85bc7722ee9	Apalache	ConstantRank1	Tuple	False	Passed	Model Under Test Equivalent Model
84aebb5c09f7c82a7075b11566375092ed970003	Apalache	ConstantRank1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
b01d182f6ad1eec22dd7384dd2588ae01b86d9c8	Apalache	ConstantRank1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4b75764c20ae5159dbfaa69837e77a84f26911dd	Apalache	ConstantRank1	FunApp	True	Passed	Model Under Test Equivalent Model
ef9377292acc5d253a71f7d64ef3bf93178e7c8e	Apalache	ConstantRank1	FunApp	False	Passed	Model Under Test Equivalent Model
2aeed6fb7fd9ec27b5f8e119a50c7b726f779ac9	Apalache	ConstantRank1	NumZero	True	Passed	Model Under Test Equivalent Model
8814b66ed4c88b73c57d51fa5cd22ccba47244c7	Apalache	ConstantRank1	NumZero	False	Passed	Model Under Test Equivalent Model
af0b3c14e8e969e977888f077fa95b607c12b989	Apalache	ConstantRank1	NumOne	True	Passed	Model Under Test Equivalent Model
bfdab92683b7ff4e232b8dba93cb8d2594c7809a	Apalache	ConstantRank1	NumOne	False	Passed	Model Under Test Equivalent Model
d7bf61c07c618f8482a79eb8b0e161a0fa30f924	Apalache	ConstantRank1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
9a1b0740a9085e635efdf0101adba9dbf09cc879	Apalache	ConstantRank1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
615bac2bb0d75a5ff9e7cefb33d7f369320c71e1	Apalache	ConstantRank1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
ccd3adfd40455f3c00364f79eb7777f4e8819015	Apalache	ConstantRank1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a4bea1861376bf7447f0c38e9cfdaeab42791a3c	Apalache	ConstantRank1	NumPlus	True	Passed	Model Under Test Equivalent Model
01fba18cc1909412732039ce239227d5c301707a	Apalache	ConstantRank1	NumPlus	False	Passed	Model Under Test Equivalent Model
9a891b5e67c5a3177768f95687f97ac818b078cf	Apalache	ConstantRank1	NumMinus	True	Passed	Model Under Test Equivalent Model
df1ef18a0401394424bd685240227dd72950743d	Apalache	ConstantRank1	NumMinus	False	Passed	Model Under Test Equivalent Model
1ab638419ac5249b2524e0fe17436864960b9a80	Apalache	ConstantRank1	NumMul	True	Passed	Model Under Test Equivalent Model
ad2d14db82586f56b36066937bc18bf7a81d0d77	Apalache	ConstantRank1	NumMul	False	Passed	Model Under Test Equivalent Model
5fb6334a29582cf3d373d82d59cd045f1e96921a	Apalache	ConstantRank1	NumDiv	True	Passed	Model Under Test Equivalent Model
725779d1d74849642e06cd0647751a96a0a4784d	Apalache	ConstantRank1	NumDiv	False	Passed	Model Under Test Equivalent Model
32202bfa7b25cfcb3f8ef223a40e99f2eaf6a8af	Apalache	ConstantRank1	NumMod	True	Passed	Model Under Test Equivalent Model
b273a27a24f09aa9ca13954d0511383c9c9bfa8b	Apalache	ConstantRank1	NumMod	False	Passed	Model Under Test Equivalent Model
e21db4d00020545161a8e03c29299447b3841e54	Apalache	ConstantRank1	NumPow	True	Passed	Model Under Test Equivalent Model
785d0495be1dad82f5ef59aa61aac6b9007f3967	Apalache	ConstantRank1	NumPow	False	Passed	Model Under Test Equivalent Model
74db11316a265f0cae095a7d1f006e4ea025d7c6	Apalache	ConstantRank1	NumGt	True	Passed	Model Under Test Equivalent Model
41dec343144b55e3ddddecfd5ce4477c4453c62b	Apalache	ConstantRank1	NumGt	False	Passed	Model Under Test Equivalent Model
d8fe5d064787bbaf66f3e2281832d1dc8d146d19	Apalache	ConstantRank1	NumGe	True	Passed	Model Under Test Equivalent Model
06099c50e51b55fc04053173940d3a39d3381a75	Apalache	ConstantRank1	NumGe	False	Passed	Model Under Test Equivalent Model
2e404789546f7537b2608ec2ed5d6fb5828d1f22	Apalache	ConstantRank1	NumLt	True	Passed	Model Under Test Equivalent Model
a35d5c806b9d0264c4fbdb9085ef3b1123e57592	Apalache	ConstantRank1	NumLt	False	Passed	Model Under Test Equivalent Model
1058b11458109201b9260ed2d00c95b1e6407634	Apalache	ConstantRank1	NumLe	True	Passed	Model Under Test Equivalent Model
41dc3b2552985a10b0ecc6e828f3d07bd034370e	Apalache	ConstantRank1	NumLe	False	Passed	Model Under Test Equivalent Model
8571f7f40e1a61a5e18f9d8bf906bc0d54334522	Apalache	ConstantRank1	DefFun	True	Passed	Model Under Test Equivalent Model
f5363138cf0314affa30d91b84b322659c1c5c37	Apalache	ConstantRank1	DefFun	False	Passed	Model Under Test Equivalent Model
02366658ab8b2ab5ddd46016bc4ea9f9b7c8c123	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDefFun	True	Passed	Model Under Test Equivalent Model
f6de43026b89630a694e99c56a1ca0f3f1db23f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDefFun	False	Passed	Model Under Test Equivalent Model
11b7877695a5ec510f905708523dc1fbc00dfe0d	Apalache	ConstantRank1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
af5bd03ad4cd6f29b8fdea199b421bfecdc63ef4	Apalache	ConstantRank1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
ff9496f7889d90cee199cc96195fdbd4d0b11a90	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
5a0416dbdaea238f0d2fb9df41f901d6acdd17a5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
961e54ea949c9b3438cf7949939bad84ac2177b5	Apalache	ConstantRank1	Def0	True	Passed	Model Under Test Equivalent Model
fc282dc52ef089ca4ec6a54c29d41eb158d7eeef	Apalache	ConstantRank1	Def0	False	Passed	Model Under Test Equivalent Model
220460d8e45dee139fa24fbf3fbe1cd377d721b6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef0	True	Passed	Model Under Test Equivalent Model
ffaa1f761799b1e3d88446e34b95907e0de52cc4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef0	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
412f369bed01a73e25eaf07ea26e77e8cc72ecf2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1	True	Passed	Model Under Test Equivalent Model
ab90fcb285b8d3cd351626fc3d2a12b8e44092e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1	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
1295b666bb9ab78219106db4a15d68ce04203bf5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef2	True	Passed	Model Under Test Equivalent Model
c80022b142a535abb9c793c0b978b09c6489ea3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef2	False	Passed	Model Under Test Equivalent Model
42d47b52ffdc46e2226cd8125fa5a2dbecdc7d9c	Apalache	ConstantRank1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
32b910c14e20d3ad962824bfc4d7eb08a30fb0a5	Apalache	ConstantRank1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ed63fc4ffea32c63d18a2d2c2b1c5a3b03cb907a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
e5127cf371e87847aa11242245db076132a4c439	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
364fd7e5290c7788d77ecd9f401e9155b876df38	Apalache	ConstantRank1	Extends	True	Passed	Model Under Test Equivalent Model
469a2d37c1ddd12e7737faa9c362ca3776310cea	Apalache	ConstantRank1	Extends	False	Passed	Model Under Test Equivalent Model
74079cfcba562e2584c42d266515efdaea8103d8	Apalache	ConstantRank1	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
cb6df7cf849135be9bece27430ad826b5faf8dc9	Apalache	ConstantRank1	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
bdd246705e9267bc8a6601324d9a657e964c3234	Apalache	ConstantRank1	Constant	True	Passed	Model Under Test Equivalent Model
11cbddc3d98256f3304a281d08e8472aa63cf6e2	Apalache	ConstantRank1	Constant	False	Passed	Model Under Test Equivalent Model
60033f061357b206874f647b7bfdfe77b7ed32f4	Apalache	ConstantRank1	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
c3fcbbb9c63a3178297ee28abb4cba8bb7f3138f	Apalache	ConstantRank1	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
2f0bb8c183b4afc95546b875ffc45beb24e13230	Apalache	ConstantRank1	ConstantRank1	True	Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point	Model Under Test Equivalent Model
fddb90daec356c4b98a52883ae4cff1fb9b6875e	Apalache	ConstantRank1	ConstantRank1	False	Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point	Model Under Test Equivalent Model
578c37a18eef6cab28410acbeb174d5ec210de92	Apalache	ConstantRank1	Instance	True	Passed	Model Under Test Equivalent Model
062a7c407be297f887864bf880253c98335c4a7c	Apalache	ConstantRank1	Instance	False	Passed	Model Under Test Equivalent Model
280c7ecc3e33c7a6c76407a0c82f1d47255655c1	Apalache	ConstantRank1	InstanceWith	True	Passed	Model Under Test Equivalent Model
762645772f5978ba91fec08bc222009f946b1855	Apalache	ConstantRank1	InstanceWith	False	Passed	Model Under Test Equivalent Model
543c932130753c0e552dfabb2e8f5370a37449b9	Apalache	ConstantRank1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d2c051f568a4f4e6f63b6a48e73227ce60660dd3	Apalache	ConstantRank1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
6f85350bc9046961504b7f66673fc1ed709ca0c1	Apalache	ConstantRank1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
936ae4b7e449ea5b036bbf8845a88a6a930e9a09	Apalache	ConstantRank1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
07cb4275bf8330dfeb87e33d3e313dbd5a577c83	Apalache	ConstantRank1	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
a7441c39542c8bdefa73494ac06996d1b53f7009	Apalache	ConstantRank1	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
a7405257f50f166279bb6239e3671a9391ee265f	Apalache	ConstantRank1	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
3882c51886831ccb717106aa28340f267628354c	Apalache	ConstantRank1	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
4c1e688953ae50e8ae495f427b8bfea9f483537c	Apalache	ConstantRank1	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
ebe7fdf1ad154548a476fd9730d2131f6d92d6ac	Apalache	ConstantRank1	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
6f269942f6d5f85fb7773590cbe54b451da13e64	Apalache	ConstantRank1	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
8559ea61511115893495b8a8d2c5482077e58480	Apalache	ConstantRank1	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
1da76a059f93d708bdbf4be0218f38c8c79422e2	Apalache	ConstantRank1	Cross2	True	Passed	Model Under Test Equivalent Model
8029dcc3eb8b8929726860cb30d73d9d81f53fe4	Apalache	ConstantRank1	Cross2	False	Passed	Model Under Test Equivalent Model
b874aeb345e9ffb80078a3c0a1e5142248876726	Apalache	ConstantRank1	Cross3	True	Passed	Model Under Test Equivalent Model
febd629f7f67ac73cfc3600c075bb819174a2877	Apalache	ConstantRank1	Cross3	False	Passed	Model Under Test Equivalent Model
5c4f727b41244b9e90184966c1ac0ffb2ac24ae1	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))	ConstantRank1	FunSet	True	Passed	Model Under Test Equivalent Model
47d0e44681b22c40857b1bebb39c1fe76f987f45	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))	ConstantRank1	FunSet	False	Passed	Model Under Test Equivalent Model
630d32b1411e20e1ef78449fd71f63138eeea01c	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)	ConstantRank1	RecordSet	True	Passed	Model Under Test Equivalent Model
e38a180fff2cdf754215fb218cdf1f9b30e1e494	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)	ConstantRank1	RecordSet	False	Passed	Model Under Test Equivalent Model
da859dc05970ff8da2f78bcc3993dc17cd84eab1	Apalache	ConstantRank1	SetDiff	True	Passed	Model Under Test Equivalent Model
710ad12a46f397f66a758ff5e0c48acff7f9609e	Apalache	ConstantRank1	SetDiff	False	Passed	Model Under Test Equivalent Model
bc5a100d8af8eeca2dba342a127a9b81aa379a2b	Apalache	ConstantRank1	SetUnion	True	Passed	Model Under Test Equivalent Model
af01141991cc99b07e78be47c30a6e4721e44365	Apalache	ConstantRank1	SetUnion	False	Passed	Model Under Test Equivalent Model
4facaa1165903c0a7e5561a8f6e53188c6dece9a	Apalache	ConstantRank1	SetIntersect	True	Passed	Model Under Test Equivalent Model
7c85599dc307953d478b70f262ee63fad78fa328	Apalache	ConstantRank1	SetIntersect	False	Passed	Model Under Test Equivalent Model
999637f394812dd97a54cd2a5840dad65d848f8f	Apalache	ConstantRank1	SubsetEq	True	Passed	Model Under Test Equivalent Model
64a9b363a11fab3b481ec76b73bd2965074b9184	Apalache	ConstantRank1	SubsetEq	False	Passed	Model Under Test Equivalent Model
da110be380ee154794af80f1536220821b7af359	Apalache	ConstantRank1	IfCond	True	Passed	Model Under Test Equivalent Model
18e68f6f50311e98152d4739eaf5b6eb4ad3b7c9	Apalache	ConstantRank1	IfCond	False	Passed	Model Under Test Equivalent Model
5624d05076f56ebbf370a24cfb0709c9c00f5f45	Apalache	ConstantRank1	IfThen	True	Passed	Model Under Test Equivalent Model
b1f9e22786b22190ea389073b82c8c52b217b21b	Apalache	ConstantRank1	IfThen	False	Passed	Model Under Test Equivalent Model
8f01478b2e34d58e87e51576b6af3c9774ea48c2	Apalache	ConstantRank1	IfElse	True	Passed	Model Under Test Equivalent Model
3a42dbb2854211d89533767b2caead93a294088f	Apalache	ConstantRank1	IfElse	False	Passed	Model Under Test Equivalent Model
61ffa1fdc1e84edc0907f94fd63c458a24109360	Apalache	ConstantRank1	Subset	True	Passed	Model Under Test Equivalent Model
92886dec7a58db5ac013bbcfe2a8098716f10e2e	Apalache	ConstantRank1	Subset	False	Passed	Model Under Test Equivalent Model
4ce032dcde2cce3adfa9eeb1d6da522a6b47b60e	Apalache	ConstantRank1	Domain	True	Passed	Model Under Test Equivalent Model
f0dd7652d45bf99d7b29eaecead3a711f2788ac8	Apalache	ConstantRank1	Domain	False	Passed	Model Under Test Equivalent Model
9a2b69660f39adff0cfd8bb8c59578ea2398fe22	Apalache	ConstantRank1	Union	True	Passed	Model Under Test Equivalent Model
7f75dc77bd0598c2913f2b3ed1bd2260170063a8	Apalache	ConstantRank1	Union	False	Passed	Model Under Test Equivalent Model
c4313981955be6d7d3921175e996cf465dd7721c	Apalache	ConstantRank1	Equivalence	True	Passed	Model Under Test Equivalent Model
d0956c54d49213ddbe00970bff9ffcd3659ff069	Apalache	ConstantRank1	Equivalence	False	Passed	Model Under Test Equivalent Model
c95f2a258865366f56a98ea09b1b776619185e49	Apalache	ConstantRank1	StringEmpty	True	Passed	Model Under Test Equivalent Model
0322149c3652b170021202bb2c48bab91b1f0b7b	Apalache	ConstantRank1	StringEmpty	False	Passed	Model Under Test Equivalent Model
9bae3d131693641339543685ca62084729f020c2	Apalache	ConstantRank1	String	True	Passed	Model Under Test Equivalent Model
536a7df20bd8bea044c06fdfa834117ca23a6e87	Apalache	ConstantRank1	String	False	Passed	Model Under Test Equivalent Model
74dfda55d33cdcd030ebf7f37c3d5250b01fc3ab	Apalache	ConstantRank1	SeqLen	True	Passed	Model Under Test Equivalent Model
dbd8f391a1a9a117aaa4d93460ceab5ad4601c47	Apalache	ConstantRank1	SeqLen	False	Passed	Model Under Test Equivalent Model
6447548a96b696c47ed1b36a14581266369fac2a	Apalache	ConstantRank1	SeqConcat	True	Passed	Model Under Test Equivalent Model
4df250f34488bac2a3cb98c08870c9cfc3d33591	Apalache	ConstantRank1	SeqConcat	False	Passed	Model Under Test Equivalent Model
7f313049a1486005fae87ad25dcf6966959b39e0	Apalache	ConstantRank1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
661d4eca6fa1ab10dd56a222892cbb8e99fa35fe	Apalache	ConstantRank1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
8df24c7fde91f3736afb75b64ebca477c370effb	Apalache	ConstantRank1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
f6854f719118bd5dfaff13cc5052dae476a908bb	Apalache	ConstantRank1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
8ad7514091e54da35048b5e6b1a8059e8b008f6f	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	ConstantRank1	NumRange	True	Passed	Model Under Test Equivalent Model
84c7b06189bda9afd6f18fc21fbb0343e3c71a3a	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	ConstantRank1	NumRange	False	Passed	Model Under Test Equivalent Model
72fffe7fb318d55821a23dc52ab8f8a2431f54df	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	ConstantRank1	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
89a4e5d346563af6c93fc22cc0abb09af9e2e44e	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	ConstantRank1	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
26cfaa0b63600a2628af807411959254e2817b17	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]]	ConstantRank1	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
eeed5b524e7450e83cebc9d61535c45469a35586	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]]	ConstantRank1	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
94065538dacd924e42f041fb0349bc3aef5f4acc	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	ConstantRank1	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
443977cd8e3b79fea68573ea24eb907846f243b3	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	ConstantRank1	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
862904681e50269c15fb19cb2c3d71b6dc18400b	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	ConstantRank1	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
2132a8b8e709d76b9403582e1152973696f422e7	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	ConstantRank1	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
b02ed40d7e87edae9a2d680a99ec460b4aa1740a	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	ConstantRank1	TlcEval	True	Failed:	Model Under Test Equivalent Model
74b8231a09d77a737507682a6209188238deea45	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	ConstantRank1	TlcEval	False	Failed:	Model Under Test Equivalent Model
6eab65d49ede7d3d42bbe6db99dbf846cee3802e	Apalache	ConstantRank1	BagBagToSet	True	Passed	Model Under Test Equivalent Model
0ff353ad8365ef64b1fedf495b429d7b69a887af	Apalache	ConstantRank1	BagBagToSet	False	Passed	Model Under Test Equivalent Model
5ec655e8f61fb1e896629d789274a3c6e947c311	Apalache	ConstantRank1	BagSetToBag	True	Passed	Model Under Test Equivalent Model
b86f14ffc1737b8946c3a788e9e87bcd854e8862	Apalache	ConstantRank1	BagSetToBag	False	Passed	Model Under Test Equivalent Model
9a86b84b5c600b2fbddb1b5683e72c307fb2b738	Apalache	ConstantRank1	BagBagIn	True	Passed	Model Under Test Equivalent Model
79c0ad9dff627718a4e562b865c9397a40a9de27	Apalache	ConstantRank1	BagBagIn	False	Passed	Model Under Test Equivalent Model
388b1dfd0ab26efad90edcbbd8a0bb4490b0b346	Apalache	ConstantRank1	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
22ee5de6b262cbf39e83ef745af1b08bd9eae013	Apalache	ConstantRank1	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
39b6aa268b05017ad13c7b4069c7074c1c013c36	Apalache	ConstantRank1	BagAddBag	True	Passed	Model Under Test Equivalent Model
92b059001b7a533e548ec2fcfab7a09565dfb21a	Apalache	ConstantRank1	BagAddBag	False	Passed	Model Under Test Equivalent Model
7ca606a95d793c7379c5d370c645da55f0f168ae	Apalache	ConstantRank1	BagBagSub	True	Passed	Model Under Test Equivalent Model
a02e2969bd33c232695bb09b61385db1f5f1ab6a	Apalache	ConstantRank1	BagBagSub	False	Passed	Model Under Test Equivalent Model
e5b8c4e60391f68fa9daf81e13483163389fa1d0	Apalache	ConstantRank1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b26e4ed9c98d86cf82708d2e68d0a033750a60e6	Apalache	ConstantRank1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
30a3f4b50045ae81e1cb9c317946ae963734256f	Apalache	ConstantRank1	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
6823e1398fdb14dbcef9fb44a04ae151159b6bcb	Apalache	ConstantRank1	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
f5c80d09f80e372338e60374f50eb470f3af0af5	Apalache	ConstantRank1	BagBagUnion	True	Passed	Model Under Test Equivalent Model
02f1e320b11bbafcb3275737049681171dffae4a	Apalache	ConstantRank1	BagBagUnion	False	Passed	Model Under Test Equivalent Model
dee5a636628eeea259793993e68902f5df9a7790	Apalache	ConstantRank1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
26a79f2b46484d1aa07cd1e4c743f6f15e06c85c	Apalache	ConstantRank1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
49eab2d4425daaadcce21b790d02030d2bd37300	Apalache	ConstantRank1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
ef888b4405913a1c678df7115489c37cd836ffc8	Apalache	ConstantRank1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8958f2c45477d7be3718bd67952ecad6cf9699c8	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	ConstantRank1	BagSubBag	True	Passed	Model Under Test Equivalent Model
3eacfb20493472ab048dfffb4af8ffb3d6db9e0c	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	ConstantRank1	BagSubBag	False	Passed	Model Under Test Equivalent Model
e9cc7e60ac90dc833dfba9905e8e75b745299b35	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)	ConstantRank1	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
ecc0b06287762ba959038428487975b484003d02	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)	ConstantRank1	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
250c5b8d1005325e4bd806cd0e5d197843ee2715	Apalache	ConstantRank1	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
1c6f4676a833e757001ba47ce1f33e352961a7b8	Apalache	ConstantRank1	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
0fcce1aff30f44cd0c8d5554d7b2e7c0a4ad6989	Apalache	ConstantRank1	SeqHead	True	Passed	Model Under Test Equivalent Model
05782dea8c4d9f34c132ca0d782ae2b10e286381	Apalache	ConstantRank1	SeqHead	False	Passed	Model Under Test Equivalent Model
d9508b0d4ebc1c5124a3089aed3b06cc1557e74a	Apalache	ConstantRank1	SeqTail	True	Passed	Model Under Test Equivalent Model
1217720be320fc300cd64e1563e6c9068d7fbae6	Apalache	ConstantRank1	SeqTail	False	Passed	Model Under Test Equivalent Model
04496550f6dc3723a69022966517f2c415ac1138	Apalache	ConstantRank1	SeqAppend	True	Passed	Model Under Test Equivalent Model
50c2e36de55a0591aec864d70f904fcf5f52e614	Apalache	ConstantRank1	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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