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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
095b4ca4872f3b14d2716667556c5164b51c5384	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set1	OneLineComment	True	Passed	Model Under Test Equivalent Model
9bdbbc9eac499d44d668e188085e3b8ebcae35c1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set1	OneLineComment	False	Passed	Model Under Test Equivalent Model
4734a65da5eb3deaab1e5792ea58e3a8f8929d0e	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set1	MultiLineComment	True	Passed	Model Under Test Equivalent Model
4e2e5766701629e46c508744f545acc20dd3f203	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set1	MultiLineComment	False	Passed	Model Under Test Equivalent Model
3bbef76af30b767feb671634193c53e0c1380a8b	Apalache	Set1	BoolTrue	True	Passed	Model Under Test Equivalent Model
c58b5fb705d1fbadb6e4c3dc2f5c688dbaa48b3e	Apalache	Set1	BoolTrue	False	Passed	Model Under Test Equivalent Model
5b6fd8afd8ff41f2841186afa74698078f137622	Apalache	Set1	BoolFalse	True	Passed	Model Under Test Equivalent Model
83d8c8fadfeb797a87a848c2be14ed5c32d71a47	Apalache	Set1	BoolFalse	False	Passed	Model Under Test Equivalent Model
a91872790a087e15171a1ff3376fe28caf5bac41	Apalache	Set1	BoolSet	True	Passed	Model Under Test Equivalent Model
0fb6e66527e1faf3810b5ec9af03b71e0c3a3726	Apalache	Set1	BoolSet	False	Passed	Model Under Test Equivalent Model
f96f1aa9f578d0280220cde9543966c7c9f58b32	Apalache	Set1	And	True	Passed	Model Under Test Equivalent Model
ae57f7023e0c1d7339c73b5e7115963f5eb111cf	Apalache	Set1	And	False	Passed	Model Under Test Equivalent Model
db42307c19e20e67baa1f96b564507668d930ee0	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set1	AndMultiLine	True	Passed	Model Under Test Equivalent Model
7c572d115656d6a0a0f874e1fec2afb5f245e0f6	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set1	AndMultiLine	False	Passed	Model Under Test Equivalent Model
ec24ffab6828b4f15ea908be854299d8285dab34	Apalache	Set1	Imply	True	Passed	Model Under Test Equivalent Model
97db7005f4c4e713ae401f9ea64ef6171775dcb8	Apalache	Set1	Imply	False	Passed	Model Under Test Equivalent Model
3b16f950f51ad09bedabb74617d0ca1e92dd29a8	Apalache	Set1	Not	True	Passed	Model Under Test Equivalent Model
ca0013887556fe0cea75e793b6bd83141a98afdf	Apalache	Set1	Not	False	Passed	Model Under Test Equivalent Model
9fe48859e85215a7add768d75694e44b45d4aa81	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set1	Or	True	Passed	Model Under Test Equivalent Model
ea19490d809e7ff55b81eefbaf756a7977b08cbf	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set1	Or	False	Passed	Model Under Test Equivalent Model
fe69c9fb03e3607494e5cb1293a0f944d74c4c5b	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set1	OrMultiLine	True	Passed	Model Under Test Equivalent Model
037f9a2a8b23e47289041c7ed2e8a61094d908e5	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set1	OrMultiLine	False	Passed	Model Under Test Equivalent Model
e7b041dc621d169298553348bd3b80dc3e455566	Apalache	Set1	Eq	True	Passed	Model Under Test Equivalent Model
42aa8932ba2149cbfce3d43143f6719082d2882f	Apalache	Set1	Eq	False	Passed	Model Under Test Equivalent Model
054fc96a7567507c4cbd77834606a0c926714f8e	Apalache	Set1	Ne	True	Passed	Model Under Test Equivalent Model
5a9af5e5eac88d01da8dd55680b671b4889c787f	Apalache	Set1	Ne	False	Passed	Model Under Test Equivalent Model
6e1968f3cf534514ac788385842d982143468ba6	Apalache	Set1	Let	True	Passed	Model Under Test Equivalent Model
d5819d5ece9a56e371d887c4b3609ac8b5227cae	Apalache	Set1	Let	False	Passed	Model Under Test Equivalent Model
1d7e8991364cff283d4ff425197abe0a9c76bf3c	Apalache	Set1	SetEmpty	True	Passed	Model Under Test Equivalent Model
bdee9024dabcee512a9165d2d43656c48e4a7172	Apalache	Set1	SetEmpty	False	Passed	Model Under Test Equivalent Model
cbf43bd7f0d18532cc30df47d0217cc7ac3d05a4	Apalache	Set1	Set0	True	Passed	Model Under Test Equivalent Model
bc83e8836a024c2edc01e79afd2174f713cdbdc1	Apalache	Set1	Set0	False	Passed	Model Under Test Equivalent Model
0748c979b2df58205e84218d394628f110b2e32a	Apalache	Set1	Set1	True	Passed	Model Under Test Equivalent Model
180511a1c23f042b40d6ace4dc7a5fe211050a9c	Apalache	Set1	Set1	False	Passed	Model Under Test Equivalent Model
294b007f12ed3df7e15a62d4b8b2ecbe109a9c58	Apalache	Set1	Set2	True	Passed	Model Under Test Equivalent Model
b1af68601a2a117614915238863db72d8bde20f6	Apalache	Set1	Set2	False	Passed	Model Under Test Equivalent Model
068a5bf745f5643234bc23c1cb114b87ec7c5215	Apalache	Set1	Fun	True	Passed	Model Under Test Equivalent Model
953cf800e333872994499560b64db4f29a77b56a	Apalache	Set1	Fun	False	Passed	Model Under Test Equivalent Model
93ea9a9abe6015ac5acc4d53a46885af2b8b8588	Apalache	Set1	In	True	Passed	Model Under Test Equivalent Model
a79f613b9a4e9a221269d99cb05167b44c6b0ff0	Apalache	Set1	In	False	Passed	Model Under Test Equivalent Model
ea500bf8080c45219d2fe02b3b6c5f641f432bf6	Apalache	Set1	NotIn	True	Passed	Model Under Test Equivalent Model
cbbe01f6c2d86600635e61b05cd336dec24c0f4e	Apalache	Set1	NotIn	False	Passed	Model Under Test Equivalent Model
d7c4c3db8ba3c54220aeac23fd4f7e44ef128347	Apalache	Set1	Exists	True	Passed	Model Under Test Equivalent Model
5c50704311e08a185bbf5235c4fa4db2173ac801	Apalache	Set1	Exists	False	Passed	Model Under Test Equivalent Model
ec5a24e115bb7913d1e02e8cb4e066cc56ef2ba9	Apalache	Set1	Forall	True	Passed	Model Under Test Equivalent Model
9cea1440fe06d23db8774f7b2959df81c057b4f9	Apalache	Set1	Forall	False	Passed	Model Under Test Equivalent Model
d91aa109c943dda9e8bc1e63d808278a973855b4	Apalache	Set1	Choose	True	Passed	Model Under Test Equivalent Model
53a2bd9a0bcf81beef5080cedf067cfba94cdf19	Apalache	Set1	Choose	False	Passed	Model Under Test Equivalent Model
26d92d686a1c85b4e441a3ba080629842415e3f9	Apalache	Set1	Record	True	Passed	Model Under Test Equivalent Model
44d6c05a8397a716986d31adaca1ef5ec5948ead	Apalache	Set1	Record	False	Passed	Model Under Test Equivalent Model
4ab458865434f77adb2f8fca1b8564e0efc15f30	Apalache	Set1	Tuple	True	Passed	Model Under Test Equivalent Model
29f165a7000b74c85489f51340331b264b116a20	Apalache	Set1	Tuple	False	Passed	Model Under Test Equivalent Model
1ca15cb78ccce5c4aa28082908f5915db44c8511	Apalache	Set1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c688f9afd2742389d9bfdb29f9e42007078cb554	Apalache	Set1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
b7112a156649efe74ed2a8bb0a80652cbcde792c	Apalache	Set1	FunApp	True	Passed	Model Under Test Equivalent Model
c5988a2fb21b7c3f69aae5d5ba0b50043bdbe199	Apalache	Set1	FunApp	False	Passed	Model Under Test Equivalent Model
5a09d0b44db5d286b677ae5bba9a7def5d743f4b	Apalache	Set1	Prime	True	Passed	Model Under Test Equivalent Model
b2efff8c391c6679f4d86c2febabd7802e1ff000	Apalache	Set1	Prime	False	Passed	Model Under Test Equivalent Model
b91affa915a5a392418a5d9cf183472b65fc0691	Apalache	Set1	NumZero	True	Passed	Model Under Test Equivalent Model
9c0f0d295d24e99b21b26a4a1595253b9ef97cc1	Apalache	Set1	NumZero	False	Passed	Model Under Test Equivalent Model
134b58509e228a57ff5defb5c5fd9e54fd5a2e94	Apalache	Set1	NumOne	True	Passed	Model Under Test Equivalent Model
3a19e8164c2bdd02527bd36bb56fdd1faa00e827	Apalache	Set1	NumOne	False	Passed	Model Under Test Equivalent Model
bb7641d1b447c3a78e855cf6eb536b3ce3bb3698	Apalache	Set1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
fdfece869844433404eb13629402574e910630c1	Apalache	Set1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
b19375e5b6d80977e0610a428257403b971d43e3	Apalache	Set1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
af462dc38d48397ca3d0b735a98a35751ad25e3b	Apalache	Set1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
2f272dc80c213e54f47ba0d64fcb819da0c953fc	Apalache	Set1	NumPlus	True	Passed	Model Under Test Equivalent Model
b2fb1e4576666494021090509c77206b04a2a5b5	Apalache	Set1	NumPlus	False	Passed	Model Under Test Equivalent Model
5e7360188f4960869519128f7a7e32e86015e841	Apalache	Set1	NumMinus	True	Passed	Model Under Test Equivalent Model
d70845bdf1515400ffc5eb565a67e5bb1e3ba378	Apalache	Set1	NumMinus	False	Passed	Model Under Test Equivalent Model
caa49a1090cc82dd988fb5249d219e0f8b232ac1	Apalache	Set1	NumMul	True	Passed	Model Under Test Equivalent Model
3a7d5936eb677d9272cb9b51b57b4b22ffa15508	Apalache	Set1	NumMul	False	Passed	Model Under Test Equivalent Model
abaed169422a1813c1e0c36fbb8b7b8808353d6e	Apalache	Set1	NumDiv	True	Passed	Model Under Test Equivalent Model
43618da2aaeca91bbbf7120152f9b01bf3522539	Apalache	Set1	NumDiv	False	Passed	Model Under Test Equivalent Model
d135c8a059728460eba81c397e5d626a76f052fe	Apalache	Set1	NumMod	True	Passed	Model Under Test Equivalent Model
c3ab31f6cc67358d870ffaac401dea32ff607e26	Apalache	Set1	NumMod	False	Passed	Model Under Test Equivalent Model
c5b9afc8dcdd755c658c60aac785820e35e9343d	Apalache	Set1	NumPow	True	Passed	Model Under Test Equivalent Model
3b607beadfdea458b0b546598efdd3fc8d344d7f	Apalache	Set1	NumPow	False	Passed	Model Under Test Equivalent Model
2b0226bd51f946c5ea1f466ea204b870ab230dd4	Apalache	Set1	NumGt	True	Passed	Model Under Test Equivalent Model
3ea4aecb7af1bd66ba5891cc9759a1d245768b78	Apalache	Set1	NumGt	False	Passed	Model Under Test Equivalent Model
7cfb28b54773b963a85b3d01f7e221f986e18f15	Apalache	Set1	NumGe	True	Passed	Model Under Test Equivalent Model
daaa62fba356f5cd53d9601c0da185c751a0f530	Apalache	Set1	NumGe	False	Passed	Model Under Test Equivalent Model
115a707d8e721b7136ede392d08e7c08707c89df	Apalache	Set1	NumLt	True	Passed	Model Under Test Equivalent Model
d69ae1c4f19b344403261bd9c70fe68004a2403d	Apalache	Set1	NumLt	False	Passed	Model Under Test Equivalent Model
8c5c9cc70d97ffb3698e126bfd89189d55104822	Apalache	Set1	NumLe	True	Passed	Model Under Test Equivalent Model
2dda2d2a781ef247a2a036863fb049385cc56be6	Apalache	Set1	NumLe	False	Passed	Model Under Test Equivalent Model
04aa7725e4e5a45e68f99d17ef06d8dda0dd46ae	Apalache	Set1	DefFun	True	Passed	Model Under Test Equivalent Model
6988767a1cdfc3e29775193ccab7cf4a46b93389	Apalache	Set1	DefFun	False	Passed	Model Under Test Equivalent Model
7235d592fc4d5d6f7e55ba21d99b73ab8f921119	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDefFun	True	Passed	Model Under Test Equivalent Model
9556e99412316d29350bd30bd4c46ed0bd212468	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDefFun	False	Passed	Model Under Test Equivalent Model
2bafd18f631db6e0eeecaeb5926a06b1e3b1cbeb	Apalache	Set1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c5e863824e59789e16ed770a097644fefc5d2593	Apalache	Set1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
70466c2465487f7cc4142e579d291b85a6e07248	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
fc803620e82085e27d53196a02967b81c4659aa0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
6e10be9af1b598c189ecf86c60c353ef3f1ad3c9	Apalache	Set1	Def0	True	Passed	Model Under Test Equivalent Model
66ebc8236348f596bbcabc86959ed16a37e65ede	Apalache	Set1	Def0	False	Passed	Model Under Test Equivalent Model
fc2b0625295e78aacf6476473394906012d0f212	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef0	True	Passed	Model Under Test Equivalent Model
933b0119cd99260745750945d3b5fea56b865b06	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef0	False	Passed	Model Under Test Equivalent Model
32dac6bf3515a36f7e0736b6d99fd4240a26a738	Apalache	Set1	Def1	True	Passed	Model Under Test Equivalent Model
df8602b620187e10c7ed9e266e7e44398ab7880a	Apalache	Set1	Def1	False	Passed	Model Under Test Equivalent Model
2eeba1c82ad649c11d51a31d561fcd831bda1bd6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1	True	Passed	Model Under Test Equivalent Model
a39c0edf9f6103e82548fd57ce4e61eda76ea6f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1	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
c926a3c8dafa9a7964ac7b11dc27e5499f68417b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef2	True	Passed	Model Under Test Equivalent Model
cefb7238e9c324a002bd1dc1c3d095bd80bb1dc0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef2	False	Passed	Model Under Test Equivalent Model
eb8bf81541b9319a5940ed23771118492ba43673	Apalache	Set1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
6d997c80f3ca93661fc543899dae3dc0c31d2364	Apalache	Set1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7c96bab093953f1cfe0ad5b3482730d6146a9733	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
6a5e9f8e23a6136b5016aa4ad7b2d4979e298c11	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
d4666d8bb7f9e857995208bf1a10cae6000d1f7e	Apalache	Set1	Extends	True	Passed	Model Under Test Equivalent Model
e94caee3623b5c63261244453e792af996af6b4a	Apalache	Set1	Extends	False	Passed	Model Under Test Equivalent Model
ab69bd28edcad20fff700dcec2afd2db1660d3b1	Apalache	Set1	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
f95adeb42c343cef4c08489e84f3ec0293d1c078	Apalache	Set1	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
ec9668936fd2c71d4d487230f61343fea70cd36f	Apalache	Set1	Variable	True	Passed	Model Under Test Equivalent Model
f62bd6501c3fbf64849f3a87eb4a0b2a828f8ccc	Apalache	Set1	Variable	False	Passed	Model Under Test Equivalent Model
f2d0a7a08248db23e908684049e753a10f2b1f20	Apalache	Set1	Constant	True	Passed	Model Under Test Equivalent Model
f09350010ab82a5fc7020abfd4583d8bc5855070	Apalache	Set1	Constant	False	Passed	Model Under Test Equivalent Model
bc8b80cf97ec4ddf4e32bd47bfb71125c9f9fb6a	Apalache	Set1	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
755aa84321536cc971a5ca1b0a1f64df7e481b0f	Apalache	Set1	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
0ba96423fa072eb702ad1817f55174efb7fe5d56	Apalache	Set1	ConstantRank1	True	Passed	Model Under Test Equivalent Model
a75edd0e190fd08d5f06004e9fd1602eaee168ec	Apalache	Set1	ConstantRank1	False	Passed	Model Under Test Equivalent Model
062458b53230ad56d4061c20366f880e84e6d58b	Apalache	Set1	Instance	True	Passed	Model Under Test Equivalent Model
f0afd17a99088a6c28fbffadad64280844f5cf13	Apalache	Set1	Instance	False	Passed	Model Under Test Equivalent Model
b471e3ca2d9e451f876067bf4e365a4f9eee373b	Apalache	Set1	InstanceWith	True	Passed	Model Under Test Equivalent Model
370e21558dbe2748e17140f7ee4fc592c7895969	Apalache	Set1	InstanceWith	False	Passed	Model Under Test Equivalent Model
ed13bf3b98129a5b6dfb8e051b39e954a05d433d	Apalache	Set1	InstanceNamed	True	Passed	Model Under Test Equivalent Model
cbb17cea71082d11512911b9318f4b05bce205c7	Apalache	Set1	InstanceNamed	False	Passed	Model Under Test Equivalent Model
c7785e7f66b6d58b65268c88659ca1e3fb0f5ed9	Apalache	Set1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c97119c56f360a7f6b88665d4977d70f4c67971c	Apalache	Set1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
cae62e74626af06db00e04c078daa6bafa717088	Apalache	Set1	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
332efddf527ec827778583d4a51b935df49f29c2	Apalache	Set1	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
f98ff0ffef581423112d19d0ea171c8bb7483ab0	Apalache	Set1	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
36dd8c847e8b8a6f51fc614b4340d6e88cfc323d	Apalache	Set1	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
d08f4749a905e67a235f83750e33660fd72f97de	Apalache	Set1	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
36219d0ee3f99c4bb37e7388428c73712e677369	Apalache	Set1	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
e4341c3c62fa74ac747a05a7f44be79ab2700a58	Apalache	Set1	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
974163270f17bbda7acc21661e3925ad3eb2ed0f	Apalache	Set1	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
4b6594b3cb34e2c090ea30b5e76c2988c46a56ca	Apalache	Set1	Enabled	True	Passed	Model Under Test Equivalent Model
6df6863271ce5dcc33815223302dfdef2552482e	Apalache	Set1	Enabled	False	Passed	Model Under Test Equivalent Model
a20a4636cddb832fc1afd537123c00eb22f943b4	Apalache	Set1	Cross2	True	Passed	Model Under Test Equivalent Model
e8c71bec3daa48276bab3da2c7053df4c8c97868	Apalache	Set1	Cross2	False	Passed	Model Under Test Equivalent Model
d00107bb71b7567e868ed0e4aa454435ab6ab2d8	Apalache	Set1	Cross3	True	Passed	Model Under Test Equivalent Model
5cc8a42be395e1f61b4ca5154bb7fa7c002d4c4e	Apalache	Set1	Cross3	False	Passed	Model Under Test Equivalent Model
d33469e4ec0ae8b9cb30a21cfa4d023b9042f5e8	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))	Set1	FunSet	True	Passed	Model Under Test Equivalent Model
5433acce9738519e3f95c8bf7d186ecfcaa3cc41	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))	Set1	FunSet	False	Passed	Model Under Test Equivalent Model
4ea6ba9060a25a11a1255be4fa3886842e531c81	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)	Set1	RecordSet	True	Passed	Model Under Test Equivalent Model
4abb7310c9fbb4577312582387fe55f3368ff9cc	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)	Set1	RecordSet	False	Passed	Model Under Test Equivalent Model
65113dc6e7a916ac9df09c264da239a2118ecaf5	Apalache	Set1	SetDiff	True	Passed	Model Under Test Equivalent Model
187b9fda1e7790a06c77482480b82ab77562fa83	Apalache	Set1	SetDiff	False	Passed	Model Under Test Equivalent Model
6a653f435720955048e8b1388937d6b0afdce48e	Apalache	Set1	SetUnion	True	Passed	Model Under Test Equivalent Model
9f0e541aa5ece8b8715962ee381ae65a916f6522	Apalache	Set1	SetUnion	False	Passed	Model Under Test Equivalent Model
c557394b0e18b05966090fd789dc3e5bfa802468	Apalache	Set1	SetIntersect	True	Passed	Model Under Test Equivalent Model
e0104becf2ab42e507ecc0b4c8f33a95d563c663	Apalache	Set1	SetIntersect	False	Passed	Model Under Test Equivalent Model
fec567fcd7dcbb8b7d1eafc5b96bee1ee29ed80d	Apalache	Set1	SubsetEq	True	Passed	Model Under Test Equivalent Model
b69ed043e998e806e15bf37a03404ec989d597ea	Apalache	Set1	SubsetEq	False	Passed	Model Under Test Equivalent Model
6c04c0e434c71d6068f3964a839132a88815fec5	Apalache	Set1	IfCond	True	Passed	Model Under Test Equivalent Model
4c0870987ee80c0efcccafbec38c0d9a3e9f64af	Apalache	Set1	IfCond	False	Passed	Model Under Test Equivalent Model
185c3a5838e2d500ab6ac1e907dc664a755a53ed	Apalache	Set1	IfThen	True	Passed	Model Under Test Equivalent Model
1b4e6c3b8084a2497a350aafdfbdebf59e1e57ac	Apalache	Set1	IfThen	False	Passed	Model Under Test Equivalent Model
2de3702389404778df46d22f483d140e943f863c	Apalache	Set1	IfElse	True	Passed	Model Under Test Equivalent Model
ec8192e776751918412238ab85c6e7f6dce13bdc	Apalache	Set1	IfElse	False	Passed	Model Under Test Equivalent Model
34474d6a3db2446d8da4e6783b58ec57f24a356e	Apalache	Set1	Subset	True	Passed	Model Under Test Equivalent Model
fa67775ca9fa29a1fa7e66a0ec1fa1460e784bdd	Apalache	Set1	Subset	False	Passed	Model Under Test Equivalent Model
1ff2edbbcde463e6a299b64b1a92ca867de315a6	Apalache	Set1	Domain	True	Passed	Model Under Test Equivalent Model
689368371a5b87d3e5763ebf9402ccd31d597cc4	Apalache	Set1	Domain	False	Passed	Model Under Test Equivalent Model
066f7186a2adf4a630199066458dc29af4f3fd00	Apalache	Set1	Union	True	Passed	Model Under Test Equivalent Model
778b2b76ef6616503ed19f86978044bfe3af55c0	Apalache	Set1	Union	False	Passed	Model Under Test Equivalent Model
853a49eaeb80074c81b20d922b56a059c2b987e1	Apalache	Set1	Unchanged	True	Passed	Model Under Test Equivalent Model
3c26770d8e2008eb0d1fb71c20f370a35b4ded2c	Apalache	Set1	Unchanged	False	Passed	Model Under Test Equivalent Model
c3f72d474d92e7ce4d387a40be57fddb201be7e6	Apalache	Set1	Equivalence	True	Passed	Model Under Test Equivalent Model
e6936ed2d8123d152e462535486d0162041ab875	Apalache	Set1	Equivalence	False	Passed	Model Under Test Equivalent Model
7a4e2235c955021083145a1d06ce8fb3d8011fae	Apalache	Set1	StringEmpty	True	Passed	Model Under Test Equivalent Model
eb791eb778beba0a7182293bc9c15a0ba23321f7	Apalache	Set1	StringEmpty	False	Passed	Model Under Test Equivalent Model
5b2e072715dae9f7978caf5b69fb6233904b02ee	Apalache	Set1	String	True	Passed	Model Under Test Equivalent Model
08b9e554c47af76d2f866936bfbf7e2ffc85703a	Apalache	Set1	String	False	Passed	Model Under Test Equivalent Model
c3b40be2dd519181b839c591f88816911f2a104c	Apalache	Set1	SeqLen	True	Passed	Model Under Test Equivalent Model
f6f84811fdea8525b0e01fdb5b93452095981d75	Apalache	Set1	SeqLen	False	Passed	Model Under Test Equivalent Model
a2b47f99b5c175b2568ba727bd79f1d54d4e38e8	Apalache	Set1	SeqConcat	True	Passed	Model Under Test Equivalent Model
7b4293b62bcae56e51e78ade148441e498c9c49d	Apalache	Set1	SeqConcat	False	Passed	Model Under Test Equivalent Model
9768e298ca19225c19dca27acea3e4fd8b56f62f	Apalache	Set1	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
6d54d2fe045a6c9ec7b1aba6872e69a683b801c3	Apalache	Set1	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
af3f812ddb50fbf4989825a242d030d95fde0ba9	Apalache	Set1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
c620abfd3c4ef61c30a81ea86c03b3a750a3e764	Apalache	Set1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
0abf2576d5926599772971faec17b7c5de972181	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	Set1	NumRange	True	Passed	Model Under Test Equivalent Model
b1e97ae2deb513b4a3533e47ff193ff2344d841b	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	Set1	NumRange	False	Passed	Model Under Test Equivalent Model
4250232c562c8e4baab5b5ac829712126f83fc01	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set1	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
e6239ea7e7d94c8839a1a2e1f0a5a1d1e8098856	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set1	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
9e3f033751657a1d03511c5c35d7e492e47d2202	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]]	Set1	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
181d1acc0a674d724a1e0a2a918fd3dd3eae807c	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]]	Set1	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
50ac5cd0b276ee1763caeac3265556a39d995d49	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set1	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
f9202d17c988c29deb2c2c94823d007fdf6b5336	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set1	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
ac718f46ef3e52a94b900e4861853ac24e515891	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set1	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
42268939beb2a4a29732bdc97d42534ce6cc6798	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set1	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
444e1570c5a4741c8f5ac48672372c2450c71f31	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set1	TlcEval	True	Passed	Model Under Test Equivalent Model
c18b90a449723b44f2f64bd02c1843b84aab3c37	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set1	TlcEval	False	Passed	Model Under Test Equivalent Model
18ed82790176261d8cbf5cfc48811f550a12a66d	Apalache	Set1	BagBagToSet	True	Passed	Model Under Test Equivalent Model
d3f9d4754def95a942da66c31054130689b52111	Apalache	Set1	BagBagToSet	False	Passed	Model Under Test Equivalent Model
f6b73db73982efe90cda49a230ec2cb374d15066	Apalache	Set1	BagSetToBag	True	Passed	Model Under Test Equivalent Model
854018eaea3a98828617a42f2a61d957dad866de	Apalache	Set1	BagSetToBag	False	Passed	Model Under Test Equivalent Model
7c89986ea7ef4405ab73c88617cea7a661be6aad	Apalache	Set1	BagBagIn	True	Passed	Model Under Test Equivalent Model
31e4f813877da5665a0bb32da48a101ad3ae6152	Apalache	Set1	BagBagIn	False	Passed	Model Under Test Equivalent Model
375200d0f432c3db59af16ec1bf375f8ce29a81b	Apalache	Set1	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
e554740caaa49d584aacd110847b1395d555c930	Apalache	Set1	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
994008ecda961f4099b38b89fda1ce3ce0172d72	Apalache	Set1	BagAddBag	True	Passed	Model Under Test Equivalent Model
4c28d1a34a40af972d936d4a312367665993b27a	Apalache	Set1	BagAddBag	False	Passed	Model Under Test Equivalent Model
b65bcc6e4985d9695240be0086fba5fcc5d6bf44	Apalache	Set1	BagBagSub	True	Passed	Model Under Test Equivalent Model
7b835dee793e6f248a28a07250adfac8ab631b86	Apalache	Set1	BagBagSub	False	Passed	Model Under Test Equivalent Model
834cb20e8d8a2051bbb1beeef825ecfe85db5b92	Apalache	Set1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
4e07ca76c44d5b9315c0a130f543b8099167d578	Apalache	Set1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
9e2ba70e24531e02574139f58061bc361582f210	Apalache	Set1	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
2124efe01cc45e70cf2cbe675ca7eb7d46c70029	Apalache	Set1	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
e7ff54ccab9b3e0282fd8da5a07c89453a9e2551	Apalache	Set1	BagBagUnion	True	Passed	Model Under Test Equivalent Model
c6bd50156027d291e3e515960c3e752013889641	Apalache	Set1	BagBagUnion	False	Passed	Model Under Test Equivalent Model
0cac0988b1f4ab31acaa36deec922c1d08ab894b	Apalache	Set1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
2fbed502e3a08f549f40ecccd11060cb44e669e4	Apalache	Set1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
ff677f7d77d1122b65c4d8ced6cc68fffb94fc27	Apalache	Set1	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
528a52c07e8938d9ec16167fda3fdb02f6d590f6	Apalache	Set1	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
f08025fe17a651ef0044ef3ff4ca80714e188193	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set1	BagSubBag	True	Passed	Model Under Test Equivalent Model
0b09eb5d1f99f0b75d44f420d49a109b50849a07	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set1	BagSubBag	False	Passed	Model Under Test Equivalent Model
823b0a93f8ddda9d977c26455f4f9d854e658084	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)	Set1	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
46d0abb8ef3df989245343e3d76e2fdf749852e8	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)	Set1	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
d95db45ec16fcbd29cf3afabb6983cf26ba8e772	Apalache	Set1	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
8f23ede8fe9ab8dfef426d872b135a8aae8927ae	Apalache	Set1	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
fa5139d0a79b17676e988d90f051ca3f66b502ce	Apalache	Set1	SeqHead	True	Passed	Model Under Test Equivalent Model
e395642614945e84d640f80dd068a17e1a63b1d6	Apalache	Set1	SeqHead	False	Passed	Model Under Test Equivalent Model
3468d92c79ee336309c1af581186e6c8c90c84fa	Apalache	Set1	SeqTail	True	Passed	Model Under Test Equivalent Model
3829e9773c414a8d3da2c5b5ca0434a57f2da936	Apalache	Set1	SeqTail	False	Passed	Model Under Test Equivalent Model
06723c972f711a2771d305ec73a9d439eff148ea	Apalache	Set1	SeqAppend	True	Passed	Model Under Test Equivalent Model
a42a6d008f84f73d17ac5db317a3c6bcdfa443af	Apalache	Set1	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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