Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b37906ac4e70e5680c1fb63457e9e611fe19c07e Apalache And Choose True Passed
3d539580b6e80bfdcd03189ac77a8330feaff301 Apalache And Choose False Passed
3e44950b97e2dd0b9e25b419b33ec5cde67f65d9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Choose True Passed
381daceab3677e92ea861892b78b6299cac34395 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Choose False Passed
469aacb3833657a369ecec4de92caa2acbc7a29c Apalache Imply Choose True Passed
44383b5816f1252f0579b4845e6ebc6ff32cdada Apalache Imply Choose False Passed
ac93ba2b50754a0fae0bbdeb852a79e43ffab502 Apalache Not Choose True Passed
92952727543bd92ecb93c1922fe032d6689f8c78 Apalache Not Choose False Passed
d1e6ba33ec21a819a6677048ac5cbc70e99d6f28 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Choose True Passed
6f333f8784ac0d311b21e7d021986cacac876b91 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Choose False Passed
d7d661699062a82d90ef41a600d610f9bcb49ffa TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Choose True Passed
f8daba6aa387b8d36959b7a7d7878b4dd62d6023 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Choose False Passed
c683c6c470beaf9083f4f62e25b12a5aeb8ecf06 Apalache AndProp Choose True Passed
a89e835f832cdd7ae08b9f1b7af9f5c0c4be239f Apalache AndProp Choose False Passed
e5758ae7a6ceb8eb382aaea28174384423cf3f8a Apalache Boxed Choose True Passed
335b4ae42f4553e41a7ec5375355817aa99882ed Apalache Boxed Choose False Passed
df76d22108d753e456f949716b58ba5f3b94f4bd Apalache Eq Choose True Passed
a97b7668d9b0c761a3bbcd874fb14be19c4560f6 Apalache Eq Choose False Passed
d27c02796e8d0ca1c31bf26452c8282ab2a44a70 Apalache Ne Choose True Passed
879757d98aeb03c8cb7b2e0e1d29971bbdd637f9 Apalache Ne Choose False Passed
a798420ab75707e589d4a511f3335b8be062a03c Apalache Let Choose True Passed
dbbd6d9fb610ac8656945bd56dece9cff949c89f Apalache Let Choose False Passed
57903e67391b59b60ea91a2f6f831f4069d92d9c Apalache Set0 Choose True Passed
c00a14d811ca8aef94c425d2de82bf0e48b51749 Apalache Set0 Choose False Passed
d91aa109c943dda9e8bc1e63d808278a973855b4 Apalache Set1 Choose True Passed
53a2bd9a0bcf81beef5080cedf067cfba94cdf19 Apalache Set1 Choose False Passed
c7bab1fadea3ed99b428f2c1f30d55a3234b7b39 Apalache Set2 Choose True Passed
7e590ebff5cbcb4b956d86cd0b969161b78f3240 Apalache Set2 Choose False Passed
d73f0c297731139e4be6ad850ea6a08d5e0edd22 Apalache Fun Choose True Passed
3ad5e1154b38e5ad3d35dfb9336fc433d56c1547 Apalache Fun Choose False Passed
bfd5c00aaa9daf1be6fdf548644ad9f00d6516cb Apalache In Choose True Passed
57e47f0fc54ad17c9d3a0e4e236b7855027ba554 Apalache In Choose False Passed
2b3c582e7618b858cef052ac3cfb856229512def Apalache NotIn Choose True Passed
d49ca7b811000bb4ed6c3f576d28e0171a2a09b9 Apalache NotIn Choose False Passed
8e8233774b3b90bc20f5698c693cb15bf40eb2ae Apalache Exists Choose True Passed
2c339cbf924a5eef0f764c72b45e2ab0d6fb29e5 Apalache Exists Choose False Passed
0ce6d5c91bc9e9b2a21ec3f6f5a2b1296cab11c0 Apalache Forall Choose True Passed
1ced9777940c9e8b4a8d373c5ef8d7cae1b2e927 Apalache Forall Choose False Passed
e6314faecb0fea7082630635280684d83f54ed5f Apalache Choose Choose True Passed
87a9b6cf1b0100ac38c165023a9f845138fc931a Apalache Choose Choose False Passed
337b2ba81682281f6f3780d1cac11aac88ae8352 Apalache Record Choose True Passed
0470c3850643baf576765e494219a9cc52ae0ca4 Apalache Record Choose False Passed
bb6d284e3b0ba9dede873a4d342122ce1d325869 Apalache Tuple Choose True Passed
d099b6e91f831100796e0b5824748f01340e7f72 Apalache Tuple Choose False Passed
590e54bad482488ea9aa6e33cf3833b3eb33e59e Apalache FunApp Choose True Passed
6fd51fe932d8b8852acb7d3d863a9bc7630b972b Apalache FunApp Choose False Passed
08cc473b80be7530a5fe24edfd0b9b979df2bbcd Apalache Except0 Choose True Passed
9bfa0fdf97b1d29409c70e7e4d541180059ac141 Apalache Except0 Choose False Passed
ed3312449751101ce68368ff3b9ab8666548d252 Apalache Except1Fun Choose True Passed
cf2792419f1920f0327734bdee1b39c009b3dac4 Apalache Except1Fun Choose False Passed
f1b37ab76ba95a54903712c63f72f17d59757fdc TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Choose True Passed
8c1f2f9af02e31e07ca49d6641ecf9a36cb32312 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Choose False Passed
71184a169377a3c4387ce0cdca217bd61b4a6f46 Apalache Except1Rec Choose True Passed
a80334906912a0b71786e30f3172dbb4667aa782 Apalache Except1Rec Choose False Passed
38c1d525cee9a10cb943da2f24d90b94dfcc9ab5 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Choose True Passed
2cf31d5a6a943319c40ba05333303426835aedf0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Choose False Passed
11bcced61cf57d867e29763053532039034a186a Apalache Except2Fun Choose True Passed
7282ee295c62424a2d36d244e7d7b183b97b8de8 Apalache Except2Fun Choose False Passed
e55071e3e6e68afdd8b47b688323ff12113dfadd Apalache Except2FunTuple Choose True Passed
ab3b58a4d29e481ae512d379ba745a2d325459cf Apalache Except2FunTuple Choose False Passed
97cabd6913b7921979337c1146228a5838d2aa58 Apalache Prime Choose True Passed
100118bd3def1b16de268c8d43c92646224a9a09 Apalache Prime Choose False Passed
dd15406a05f309f22b2bf992dfb0cf2f8a2c465a Apalache NumUnaryMinus Choose True Passed
5acc5b65db97b5f3528758e13484b13ff7dc6fef Apalache NumUnaryMinus Choose False Passed
1f3d684a5000afa4f237e722e71c779e96d37b33 Apalache NumPlus Choose True Passed
257988509e40d70a2739ec4395c5d37b6f2a6b76 Apalache NumPlus Choose False Passed
54098ee44f5e72c14366cd4007d7b6cbfdf31fff Apalache NumMinus Choose True Passed
7ca0d5a8a24c2736e5f96379b93e7fcaaf4b4cbc Apalache NumMinus Choose False Passed
629dbf2f2302d8ce561e7ad55e1472c0bdec2dff Apalache NumMul Choose True Passed
3449c32ce5f90c578f4c9634022de5670ee69761 Apalache NumMul Choose False Passed
514977d34d2d5d8c5e77a6c12e1a9471e2ed2057 Apalache NumDiv Choose True Passed
7a5c8da4e20fb9b5e5399d5660fc8c550418cb73 Apalache NumDiv Choose False Passed
06782b4273b6dab38be15b58feb8e935386cd163 Apalache NumMod Choose True Passed
548909587b11aba52ce5707f5aa5f40a4af75c78 Apalache NumMod Choose False Passed
6e7878cdc990f7bb7bfb39f678a66d8fce1bfd2f Apalache NumPow Choose True Passed
69452cd98357ee5a056069d18a14866b1258c1fb Apalache NumPow Choose False Passed
aba308bf8f93e1a40f30d3dd5eea444f559139e4 Apalache NumGt Choose True Passed
b299e82c0cb722887017712ec75c597c9d604d73 Apalache NumGt Choose False Passed
eea50aa1a56435d3b1b7ca059395604e98d083ff Apalache NumGe Choose True Passed
9ac11485e01be8840c68e7637331417b580bb889 Apalache NumGe Choose False Passed
81b5c72a21521e869418ac61814d9ca8cb2f01a6 Apalache NumLt Choose True Passed
934703817d8618a72ba8c9dd7d95896c998c77ef Apalache NumLt Choose False Passed
4bbac713bbe24088a804f03c044686c0c0ebc446 Apalache NumLe Choose True Passed
bfdde1f0b51c83e920d80018d3f51f1b5688c1b2 Apalache NumLe Choose False Passed
7f32238f10c9144a1bb335e30cf3bac06913b8aa Apalache DefFun Choose True Passed
99d957410276bd5b2134e784785260d4acb1a05c Apalache DefFun Choose False Passed
3ce4444a00f2b587a425224e54a855c458c539b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Choose True Passed
4c7fa6c49abe5836edabc4e69d15d4b0f54ebf4c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Choose False Passed
c5b43577668170539c71765c951cee0cae74e37e Apalache DefFunRecursive Choose True Passed
aa4565b12138a21d6dfb9b6bcb94b029c91fa955 Apalache DefFunRecursive Choose False Passed
7dc9209d46937b07a8f15ab67eac9a7e3ca46b6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Choose True Passed
89a7413d8308aa052d6f5822e03b3ffa7690fce0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Choose False Passed
149d7411bed992e51d51b6615d48b2c69de13028 Apalache Def0 Choose True Passed
c301a2141eae463dd1b96ff2a5ca3a98d634995a Apalache Def0 Choose False Passed
5d68db1aef61c33263b0b5b2d733f1261dca41c2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Choose True Passed
d79ce65d59d71e2d1c089cbc9be0c06471a647bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Choose False Passed
a5d2c1f71e42bc40a2aa28362a53b04a79b60395 Apalache Def1 Choose True Passed
01ceac66a575d83811ca802f1a5d42e5c7efc1f5 Apalache Def1 Choose False Passed
aa426c1b23c6106bfd38faf6ee2fc11cb1b60f5e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Choose True Passed
a60a7a96bff7a79d71a696ccac312c91aa2981c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Choose False Passed
efe9bada483fb63b1a3001aa51943a0463fbbab9 Apalache Def2 Choose True Passed
be0b091d3a9f8521438f13b395d83c022252d11e Apalache Def2 Choose False Passed
c849239cec02222df538b8f882d20536de3ee8a4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Choose True Passed
f4e668470be3897ceab0ee2fd2361f4e4c637cda TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Choose False Passed
9b824b758764f835742c9abed0078b062c6ed389 Apalache Def1Recursive Choose True Passed
4d823e5393db24d46c34bdd19072f17a70558599 Apalache Def1Recursive Choose False Passed
8e656fe944b08d165cf3eed98676367bcd332781 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Choose True Passed
0ef047e5dc1718fb44f23a949863452810071408 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Choose False Passed
2964e4a0845ce6dcd4b4967fc22a5d01cf3ce6c9 Apalache Extends Choose True Passed
4669481b5565e1a5e34ddac19b4a415d3a9f3dfd Apalache Extends Choose False Passed
71f5243f59dc9e39929b78480e92c782f1792586 Apalache ExtendsInDifferentFolder Choose True Passed
8de830c0966e63e950b461cefc16d27a46e7aa85 Apalache ExtendsInDifferentFolder Choose False Passed
be40b064d635198bb6590eed5835dff08c9b0541 Apalache Variable Choose True Passed
f0bf5794d80440be5f4a5d13b155f10f73781f8f Apalache Variable Choose False Passed
ca72d48c146d14ea1097d99066e6c86202ccde55 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Choose True Passed
078708306011867056c04cddc1103fb0249f3000 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Choose False Passed
8c172895771a9be8c81ad57128c198a7e694f8ca Apalache Constant Choose True Passed
8b33fd1777f0fe1ad89640a333f16a198b89fb99 Apalache Constant Choose False Passed
a99792b21f95b16e0ed2b359bdebda7d07d65492 Apalache ConstantRank1 Choose True Passed
6424adb1ff6e99a0e10789288981006e7fb74c43 Apalache ConstantRank1 Choose False Passed
b3fb9cac7824a23bc52b88ab14a5d4a61c9c8c61 Apalache Instance Choose True Passed
03fe765d9c7eac17dcf7483dc7a42a6701ca63b9 Apalache Instance Choose False Passed
2ecc294ef45b5821d222c21d2b1a2368a9772098 Apalache InstanceWith Choose True Passed
4e5ac940e1566e0d0328f83f27b1073b75c9fe3e Apalache InstanceWith Choose False Passed
df63483ceee25f7dfd140bf08ab0f03715e4a6e5 Apalache InstanceNamed Choose True Passed
4569460ce8b087682191da0a35f9d6166e5683fd Apalache InstanceNamed Choose False Passed
b20df7a67384cc53885de51a3630b1bafbb7e0a5 Apalache InstanceNamedWith Choose True Passed
2a5292a3edb413d3d35ddd5ace74a483fbd7de66 Apalache InstanceNamedWith Choose False Passed
e6b2a317baacebf1175d4e426ed9746056c021b0 Apalache InstanceInFolder Choose True Passed
d431545b1b5c3be2eb7e8644b118d651b0df3bda Apalache InstanceInFolder Choose False Passed
bb95aed80b354ac2e95a2712c5d4b61f85064f12 Apalache InstanceWithInFolder Choose True Passed
24bdc2aa98208b90ffc2aa811833bbb98ae87b32 Apalache InstanceWithInFolder Choose False Passed
cc7caa18acae2cbd3557a028377e6e186e7768ca Apalache InstanceNamedInFolder Choose True Passed
d7a3050dc0aa9c72e72736dd1c86df65ae317fc1 Apalache InstanceNamedInFolder Choose False Passed
6790ad306442febc54a7890a168c5d4ba5261ea4 Apalache InstanceNamedWithInFolder Choose True Passed
9c1bba5003574438870964532fbef6bc8bc90cd6 Apalache InstanceNamedWithInFolder Choose False Passed
7129c45f0e1c402b785faed75a19f387da4fd660 Apalache Enabled Choose True Passed
d8f340ea2155e72877ffae147cdda69ac7c282df Apalache Enabled Choose False Passed
c05196a9329c7177ad6b31c5281e0f26d2287f00 Apalache Assume Choose True Passed
3b04ad5777d68c0c32385956e5e38deced1dcc2b Apalache Assume Choose False Passed
76ec573715e3a992035d907dd0eea09e38841a47 Apalache AssumeNamed Choose True Passed
73f5924146df5fcf0d4906482eb5c4e14f7edaea Apalache AssumeNamed Choose False Passed
0a6094d460eeaabea885a1f97183b3f37c3662b4 Apalache Lambda Choose True Passed
d8fc305124c2318d1510ecd1f1ec812786dbede0 Apalache Lambda Choose False Passed
1e6c3f45d8431a91cef4a8c2f6e2c66000d9253e Apalache Cross2 Choose True Passed
b44d9e90771fd09f60ab35a5f3d2229238716aea Apalache Cross2 Choose False Passed
488fc35ea7feac160e8ad3be094b68aa134d8845 Apalache Cross3 Choose True Passed
c0805b15b0f022b763533ecac55d28dee12ce76a Apalache Cross3 Choose False Passed
d34e0e217912a02a6c97566457a369f8d4931430 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Choose True Passed
42d8878fbb550d59a57268d77a3efd1d4319ae3c TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Choose False Passed
940a90bd616b0cbd981304ee37461f786bb532b1 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Choose True Passed
fcf0dd8ab48b46dc7e4eafad445c7372d2ecedde TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Choose False Passed
a805a539899b05d97f630ee531e0346bce16161a Apalache SetDiff Choose True Passed
079b95763e73acf537817987bab44219413bc9a5 Apalache SetDiff Choose False Passed
2c0fbc7fcce6afa65de166ccbab56ecdbedcbb06 Apalache SetUnion Choose True Passed
37f6fc44733d004bfcbb12ba53b6059cceea8ac8 Apalache SetUnion Choose False Passed
410d878dc8c30c033e755e4c5de5d623d118e28e Apalache SetIntersect Choose True Passed
1b34be0229f1cb33c30fc2b820c4f1762813ade3 Apalache SetIntersect Choose False Passed
6041adc6c732f653989353a6fb151346f3c1caae Apalache SubsetEq Choose True Passed
e806131a1621afe4849f68e854d1afcac069115c Apalache SubsetEq Choose False Passed
03077444965e6a3027cc41b453d6975a076f8ba0 Apalache IfCond Choose True Passed
fd89f1938f68a88f2d0b3d9e823a887ac5fbdef1 Apalache IfCond Choose False Passed
7181cfb43fc6bfd689be1cd908b303a943508838 Apalache IfThen Choose True Passed
87b52fa8d5f0b36efeb0ec83ac68ef4123aee6d6 Apalache IfThen Choose False Passed
7a284ea3e13e5987c62d276e90dca50120eaddfa Apalache IfElse Choose True Passed
b0951aacbab1adcdb238a196625fdbfce8656d7f Apalache IfElse Choose False Passed
cdc3c62ef9375481dca5087bdced877a911b57cb Apalache Subset Choose True Passed
0912c8e640bcd61275c30ef65c60519c509dee2a Apalache Subset Choose False Passed
eafa16fbccc0d81cbdc1e2837492f734f768f6d6 Apalache Domain Choose True Passed
0d5d567ffe9752c11f26310fef6fdb59329e5e7e Apalache Domain Choose False Passed
d55943b1db35a9cd7a260aa9ec67dd56c7ffba46 Apalache Union Choose True Passed
f517dea81da34292b9239a18622ba909de6579a0 Apalache Union Choose False Passed
1a2ce90cbfc7090462d85dde389a82fda0bf35ff Apalache Unchanged Choose True Passed
43fb6293783f18ede51c5c4b5407623d2f421446 Apalache Unchanged Choose False Passed
2c2d3b8acef0e24078acb378fe76c58d394aa53d Apalache Equivalence Choose True Passed
1304ea1348693cc75e80ee9ead436daf3eb57de3 Apalache Equivalence Choose False Passed
2d4de8e1ba0936ee5cb0ffdc17253a0254c5ba17 Apalache SeqLen Choose True Passed
4c09309cc84934abdcf96a6c79c0591a35b5baf9 Apalache SeqLen Choose False Passed
fd366958454b1c6afe6550bf41f3a0f0fbbdb193 Apalache SeqConcat Choose True Passed
857b3801cf78029fc6b05bdf693317e6c4ccfdf9 Apalache SeqConcat Choose False Passed
2b8527a039f2637ab0c2283408008f95d9924d33 Apalache SeqSeq Choose True Passed
6a24a28b54e428ab444a0d84bfbb631b9a580bf5 Apalache SeqSeq Choose False Passed
43331bcae51ab6949708a12cdf0ad3c688566a04 Apalache SeqSelectSeq Choose True Passed
d0791c09c7b80f2dc07a9877bba4ff0f376cf973 Apalache SeqSelectSeq Choose False Passed
234188b033ded1618e0f591b8552a67858bc4d1d Apalache SeqSubSeq Choose True Passed
b759927d9666a8b5c0a6a1c00be97cd266ec679b Apalache SeqSubSeq Choose False Passed
dfb87e51b4e1b16bd0cb56dd5d39949becc89319 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Choose True Passed
d1b93c18dcde6f955dc4de712240a114c2cfe888 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Choose False Passed
68d1d10badecb31f828887b46b7a4b80b51f335c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Choose True Passed
fcd1a06aa387c70af5d80d4198e6860309fb46a8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Choose False Passed
4c33f1e79d608251865ab091caeb737805b1a1c2 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun Choose True Passed
9f070acd7bc36d9685652ed3ae629988d2fd12b1 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun Choose False Passed
8c48a668f714fe8267a80367d808f31135112af2 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Choose True Passed
54ad3d1bada91f01c5df9501ccf0c5f0dbce5d6e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Choose False Passed
4ba5b2ecd09dac9fdd917a08d3a8e9e8ed91956b TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Choose True Passed
bb7f7e4cf0e1fdf806bd68c92d319f38b3065a07 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Choose False Passed
906c0afbf9fb6dfeee89c2ca43821d112e6eef74 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Choose True Passed
5c6e67278cbfd2927579ee5be36ebf4f482c691e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Choose False Passed
4177e515dd49615b0ea25568754f57bbd05e23a8 Apalache BagBagToSet Choose True Passed
a8e90353a342cb54171efeaeebd2bdc8907f48ae Apalache BagBagToSet Choose False Passed
9940a8a6f0b407142a89300972a06dbce6135ddc Apalache BagSetToBag Choose True Passed
f85a4369962b05db3e4ba206165bf6b28a3660f8 Apalache BagSetToBag Choose False Passed
9f6e7bf0066cb3f0f601c04771f6b9d088661968 Apalache BagBagIn Choose True Passed
1c3848c8964456b83e041630854b23d5cfa06447 Apalache BagBagIn Choose False Passed
38d81d71751b91e05e5e90769763f6f2735645b7 Apalache BagAddBag Choose True Passed
77bd2fbecc89119df3cd625c9cc9d3847303aea2 Apalache BagAddBag Choose False Passed
286113d092a0818f6e35dca331fb8ef16745d4e0 Apalache BagBagSub Choose True Passed
70d6a11324bed0b9c70683b30ba86ae28bcc5ab8 Apalache BagBagSub Choose False Passed
791fe90e9483f2f7c4159fd0a6633e3b20d34ea7 Apalache BagCopiesIn Choose True Passed
89dfdca03d883084e4b003aee35bc736507069a7 Apalache BagCopiesIn Choose False Passed
5ee85e40d2f33f54284033d7cf1b059db94d7d68 Apalache BagSubsetEqBag Choose True Passed
7be6f8f475df5b3a99c3bca677c1e33b5896c6b0 Apalache BagSubsetEqBag Choose False Passed
dd09a0e8693d4cefa6e31fe51d84c470b6b25d2e Apalache BagBagUnion Choose True Passed
e79b0f7012af85b1f325f00135dd97340c80cfd0 Apalache BagBagUnion Choose False Passed
3ad023a3893582551c75ea251a1aa969b8d6164a Apalache BagBagCardinality Choose True Passed
a7fb2e741644ba3e5da35d544f473a2f2942f0f2 Apalache BagBagCardinality Choose False Passed
46f7b5f81dd46f3ca391795692da2c5573007e3a Apalache BagBagOfAll Choose True Passed
3dfe2b1de6aec9d494524ae86d69ab8fd7c3691e Apalache BagBagOfAll Choose False Passed
2a1928fff27c85ab84ce7fd2b229c49e378284cd TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Choose True Passed
0ffa6e2829fdcd8ed2fea0718e747c10ce41b55b TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Choose False Passed
f2295961761894c69f84f24a35cecc5736bc5f69 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Choose True Passed
dccee0b86e5feaab903492c97912258dfe621aba TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Choose False Passed
0ca3f4b0753b9f0ba7d727f4e53d27d1e20c846c Apalache FiniteSetsCardinality Choose True Passed
9ab3e539c012217fa20df97f44d45f86cc6ea63f Apalache FiniteSetsCardinality Choose False Passed
88498a2bfa90da3f9cbcd12b9b65df42d7712319 Apalache SeqHead Choose True Passed
508795b174bedda8882a81517e700151f67700ab Apalache SeqHead Choose False Passed
8b71a908b9019391925b4378465f59d49b1232ab Apalache SeqTail Choose True Passed
0a04b1c32f08d66076e714fc9675ddf06a5ec4c4 Apalache SeqTail Choose False Passed
ba93ae4d12617289051428cb22e4c71339a67ab5 Apalache SeqAppend Choose True Passed
0dbbc3649d41569b746d22e28bf71da4983c87e4 Apalache SeqAppend Choose False Passed