Index

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