Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
a7bc60f9b447d597bdd3f70635ee8545f2ba4a4d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFun OneLineComment True Passed
e1a1e2f14f7ce29198ec94be501fe00b9481b18e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFun OneLineComment False Passed
2ebf8af55ce40a27b71b222f57caa37803b04c8f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFun MultiLineComment True Passed
22a746f1f3e865ab9236e7a52377b809e4765f53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFun MultiLineComment False Passed
872806ab1a847f5318d35dbc9ff1074bc0ea3148 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolTrue True Passed
6cf02c126ba3bf517ae8079b25365ef1257f0a3c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolTrue False Passed
97f90e2b51b238aa985f21dc4fa02d3cf20d688b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolFalse True Passed
1440e6784c506a7f48eabcf6ef623ce24ba43a10 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolFalse False Passed
bf1dfd240d08f07914885706133650b3c992322b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolSet True Passed
4102330f9c19624f3d7750f1285c06597efded9d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolSet False Passed
ec9581169ad99de87afbda406716d11e68d07472 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun And True Passed
85da523b1e71e66d170c5021f07c233210ab5d9e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun And False Passed
06da5173198df5fa6b7f70afc087086de96df05c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFun AndMultiLine True Passed
80558a1f84a7fc37dacd6064777bc09c99004a71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFun AndMultiLine False Passed
59baedc4a969284b29481dcb51fb5657cee74973 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Imply True Passed
2388d984ddc24bf2001faea441d95f285a5ad728 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Imply False Passed
942807f3d88d407f7e9e53ba5e97e194625b23e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Not True Passed
5d581b66b9dbddcad75fb46f823c21101ef11aed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Not False Passed
1074f0e546ba358ded8ac1df785a3259bd3537e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFun Or True Passed
6e82693f0daec9a899f443f319cdd9d30ab69bec TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFun Or False Passed
87e46d887a50e4b05d4563f42f0ed8d05102e7af TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFun OrMultiLine True Passed
7792e1d4832505caf83a2c57a21c6dd1a96905a8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFun OrMultiLine False Passed
f64606b534edf76148c157412836ff0b90891f89 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Eq True Passed
4331ac87826b259c0bf08d62ea1c49165f7da138 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Eq False Passed
4db608c5a50d269b4f8f49886a1a2e37adfc93c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Ne True Passed
2429a0e0119b5ccc1d00a6e66763fbf10f017d13 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Ne False Passed
5772072deefc46afb7de8f46a9cbbf9c4246fe84 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Let True Passed
97d6915d61a85403a3cb0ed9d591d125afe51db8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Let False Passed
3f78e571d57354fe6ed003bdf649a72315014b6d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetEmpty True Passed
22c92320291ba7b9d005792b5d13d9641b8514f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetEmpty False Passed
857cb621310c3e7fcc7ef51c26950f977d80e372 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set0 True Passed
0f83dcdb0977052510ff5f48e1dc1117dcf5d0eb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set0 False Passed
908949efdb50c9c5c062812feab74ffd3f4df685 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set1 True Passed
e5787f039c62b8dee60d83c2d4aacc0c5b43082e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set1 False Passed
ab4865f1c856ffd737bee2a649457706c20bb497 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set2 True Passed
6fb4d752e0db44a6771f50d1fac510148ed65750 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set2 False Passed
a5f196f8fd60029ef30f313fd323973c8ba9ca0e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Fun True Passed
227fab258e673224cc7e6b7b02b05a3abf5786c1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Fun False Passed
ef3231dce5011fc5bb40ff8ee57ab0a1293f0d1b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun In True Passed
b006c82f553328d4c2e93e4ed2550f39bf438505 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun In False Passed
d8438bf58466e39791d67f857dd1c7a4bef8d944 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NotIn True Passed
b5ee44b2b55acf7cc10142bf0905326d93a53200 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NotIn False Passed
324abd0b181a961b2f7ab08247780c6097ad5b0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Exists True Passed
a8f898e840d084959ebe021b06550238ae27ed47 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Exists False Passed
6484db4623585ca6a5fd62844e264009f4df2d09 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Forall True Passed
646e0276932db3f7b67cde41ee674697e806d253 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Forall 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
3d8288e870e59ecd2bed38dd0901495629dd6dcb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Record True Passed
272d75ab27a98192ab7a1638db92188ac1e61c2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Record False Passed
98b4fae6b36746d718b3caf40900a3d8aed4a094 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Tuple True Passed
460ee2f1595630ff0afd9076686fb86850a45f35 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Tuple False Passed
234936037c911c27784692dbdc5a83f8fb349f85 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun TupleEmpty True Passed
078fda8e72fbcc55f215f4dafaa8aa89970f7941 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun TupleEmpty False Passed
554a52588a2cb65e72260b4fa4e547faaf04843d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FunApp True Passed
d7ebc22fe5587c379de453b2b621d370b2848a66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FunApp False Passed
5a7bf6e4f3bce3084b9df7e2f94988e869ebd5cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Prime True Passed
461592241f4e3d4d712c4a75626c6a45da3e6924 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Prime False Passed
9fe1a768eef3e891c642c400e6080b79d2b46dd8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumZero True Passed
6b34f92659140aa3e96390ebf2eb15a52d059e3d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumZero False Passed
6c46c822b63bae115e452928e5f029113ab976d6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumOne True Passed
f891c9b613a2659962345e7ccd7d7057770f6b74 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumOne False Passed
c8a758c1e9c187be5ed288af88c8d0e6f8741209 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMaxInt True Passed
01f030c18546f64c26c216220cf0a3e9a715e1fd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMaxInt False Passed
d374c6293a3c5ebd499fb356e7ec996b3e7d7179 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumUnaryMinus True Passed
7f06224aecd9c06e13cf14ef942bd86436732ee1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumUnaryMinus False Passed
6224a7108e44af9737395a58dfb9a5239d4ba928 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumPlus True Passed
e0204cba09bc49b48bd0d95dcdc504e361b4436f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumPlus False Passed
c2134b41f732b05bf207308a50afb9d829479d68 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMinus True Passed
3ad0630a5ea9e8ccfb8b291bb2324bd89c88cd71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMinus False Passed
71cd891cd19190ade9d7ce017f8ac0fd86e08826 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMul True Passed
046b2990820d4fbb9d8bb26bc44ec35b744d3a8f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMul False Passed
882c224d0d67bb3e2d8052565ec15594bafb95cf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumDiv True Passed
50b1077991b259fc636297db671012687cd11685 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumDiv False Passed
b28c1c2bcaa36ff60a8ecbd7b649bea61f1796d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMod True Passed
7dc34878a0ba86919eb6dd4c71c8aa4e90f4c1a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMod False Passed
2c1d90056fd2da649cfd1ee58de356e993a296ee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumPow True Passed
1ac259598737c5958c0dbf543ef2641c2661b817 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumPow False Passed
1831559c4169aaf22de0311ee6920e0d833e1150 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGt True Passed
de3956a77925e158e43a66b175c82f3ee1c911a0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGt False Passed
2319f20e3430dcca196b1422f27723d2508731bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGe True Passed
5b4e857d710481bb97ea8cc375452e79d2ed78da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGe False Passed
8e40faef99fc42c249a8aa1c4d5d884d0d78f9a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumLt True Passed
9f783e2668a949c22b3bef377230c576de575402 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumLt False Passed
010e34e3f630173288af2baadaf9237bc1ae0d25 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumLe True Passed
c8b200600dc2d45e0801e5174e68acdb1b385c46 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumLe False Passed
67b5861f7bd91b71fdd67d7e2888a79d3bc791c7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun DefFun True Passed
b7719ba3cc64dc1c743d87d2cf06149882840c4f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun DefFun False Passed
8dab6f486af5a5f4127bae5ae20de55ff0aec391 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFun True Passed
da4aea918ec9260f9e2ffd7a9873755c04a91f4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFun False Passed
b3dce058374d06ac1b809700698877e7ebf70bca TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun DefFunRecursive True Passed
7fd10fcf12ba649d36ce183a2b06cdef993fd5be TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun DefFunRecursive False Passed
9c75233798461e7ad930d0f65230747b535094c3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFunRecursive True Passed
1e8742ec17e40ca1c9f6c7b323186e054e0aca6d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFunRecursive False Passed
c626f8c79377727181994469df926d7dd918d7b7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def0 True Passed
386e8cb10cc4d33e1c9c072d6a39c1be3f9be780 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def0 False Passed
06f8e554595a52f3e6e88c1e3b8db59093e797db TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef0 True Passed
66bbd3c0ff6461ed274b178719c76ba3d58e678c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef0 False Passed
1b10246345557cd5a74df282051aff448a01f171 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def1 True Passed
14b2286a0bf3bb68ba001cba2dab58e2f8d0d2a1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def1 False Passed
a54f1f4054b48366ecf41dceebc2cb844bfd6deb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1 True Passed
03eaf14a78384e6232bca6a5630cdceb059a66ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1 False Passed
a363bb196346b01771ccb04216ad963fca3d6504 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def2 True Passed
358b96cf4a88f9da57271cc6398b0c00d155a428 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def2 False Passed
78aa4b28974675448e708a413f0e2f25a6edf8eb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef2 True Passed
143ca82637fd318d7ffaefc995f4ba425eca91e9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef2 False Passed
084fa3888e7d644b3212f851233ae46fafa8f89c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def1Recursive True Passed
f7a2d0262a4374daf8e035f800023008f0beec80 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def1Recursive False Passed
56114251f2dc1aa13648878c893f2be2a2fc72d0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1Recursive True Passed
a52052ccafdac43d4a663a31cf0df71e0998c423 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1Recursive False Passed
c3b3c630192d024d47ff2d6868a1aadb55b08452 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Extends True Passed
73fd2c63bee22f9c079c22a60f61193d6270076b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Extends False Passed
fd3b7993a5b4ab23531ec367ab4eb17b2afdc3fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ExtendsInDifferentFolder True Passed
ec087ea719204a14758012e0a06d8583944639dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ExtendsInDifferentFolder False Passed
177f5ec3c578dd61eb2f0fb10dd1591b0181b40e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Variable True Passed
1311b937140ae1ee5ae8c2f903e17c906b6a50f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Variable False Passed
f49efdc23a48a06191d7a20ee04076d472138c31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Constant True Passed
02af59e6148e33352e7238c3c6d849223520c839 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Constant False Passed
959719f2e9fa022659067892c4c647e1822177e6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantModelValue True Passed
4cacbac8facdb5951de08d56a9c3b0f199624bf9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantModelValue False Passed
1c0293c1b76463ee2dc9d8570a2d1c003f827906 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantRank1 True Passed
a90511896f92dfda876cfe55e9bdfa1a7a4f6272 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantRank1 False Passed
f66e8b878b12c2cdac9468137f334bd2f1c2bf66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Instance True Passed
c591d97770b4dd3244e84a79c6643014269362ef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Instance False Passed
26938c19d4d472ba874277f640425783d95b7944 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWith True Passed
3786dc73ececfdd1209c0c60e2aba2df1e46ce71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWith False Passed
b6255bf5cb67a185cb5927db74a9e6cf8e716abe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamed True Passed
2144308ad9cd6bc6c866df4066a23023acb7074d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamed False Passed
bf33b92972fedb4ba0886f9727d2e92d449d7ed6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedWith True Passed
adf35c44a462737e9fb525c73fc689f58ef65157 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedWith False Passed
a001d0a144e9148e21f584f45d35d18b4038dbff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceInFolder True Passed
5e75123a73e780b91c6700de9c7c4855a6653a5a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceInFolder False Passed
e67bc14b32f7385e36b769cc544ca325a0fe10e2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWithInFolder True Passed
fe440ebf5df653ec39f4dad6026ee7e4bb550372 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWithInFolder False Passed
20fb39ed052b98955ce829ceef7dd8324a7e3d49 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedInFolder True Passed
d21b930603545b9dc825f2340b4c1bd367874906 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedInFolder False Passed
a47b83ef0278f896de98cfffa016fe79b51dc3a4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedWithInFolder True Passed
0f8e69b2ca94bb368efa59140851f49b919560ca TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceNamedWithInFolder False Passed
c29cd2a94791cd3c87250848caa799972e942780 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Enabled True Passed
8dc107fa0d1bef56b3aed9e99e9102999935f441 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Enabled False Passed
a23232685d1faaf8bef41b1f4be163a2fc229d61 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross2 True Passed
6db2e714ccbcbca87eae7fba1f42475ed6688b65 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross2 False Passed
fa04150f67b1578b812922068423e127e9456fc5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross3 True Passed
c3ea394832c9f4e0c312d35dd4a0d746b47f5bd3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross3 False Passed
905b836338ad2f2dae7eabbbbf669e7c4e98c2ff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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))
LetDefFun FunSet True Passed
789d614a2e490ec94dc4dbbdd63f3adef6b71415 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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))
LetDefFun FunSet False Passed
80bfa3cdb189ca5f89dfebccef2bc0df1c912042 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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)
LetDefFun RecordSet True Passed
ff725806e4d33116d6922afc92bb5ea5b4608c95 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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)
LetDefFun RecordSet False Passed
f1920a7af2ebe47a8bc272ddfd6704ab05e8dca6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetDiff True Passed
78cb87a69d457ae4a410c0c1d0009c134df75434 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetDiff False Passed
d779f621c1371e2a91309283d720804ec9b26bd7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetUnion True Passed
bea83dd33b45bb61f1c54822cd9f412a34bc5270 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetUnion False Passed
c95a719eadadab199056417ab262f8e7687934e7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetIntersect True Passed
e9e04ab8c672057124980f3a2e85c5d7ddefd1e3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SetIntersect False Passed
f9e33b17c46e84d2d2534e0c281c2d7f7d3e3d23 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SubsetEq True Passed
7cba8823e8cc2da70ec97d9c1ee6380149de2a42 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SubsetEq False Passed
73f61e6298ad50e1b5e09d91f5b066d0d0baec2f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfCond True Passed
5d1c01f28a38b8519719821e04efeb73f710f5f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfCond False Passed
3f72b46535aa86e4bb84b3eecc6cf7a185befbcf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfThen True Passed
09b926d75aa20fa7669d4cf590e34793c518dc50 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfThen False Passed
e41107d6f1a8883680d1ed3e2c7042b7ed773aea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfElse True Passed
5dd8f07d8b8bf189190f3ab8b0ef80d7399ae1e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfElse False Passed
7f351314e614fcdc717ae26744a8b606f2750821 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Subset True Passed
c22145116d0f0242ed7fee64efdc1a4ca6def195 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Subset False Passed
f015d2156759b47b637e2b04d68af55d2fa4a4fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Domain True Passed
1759fa6dde43831731fb42452b54f19b334a1137 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Domain False Passed
c1ccc9a9dc6368373197822f969600ce1e51af3c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Union True Passed
fb352969a0bf0728bbf4cc7f282f2e4350c43b03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Union False Passed
9440b5dd8149f894adaba563cd16b05703c7f5de TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Unchanged True Passed
aeceed33926cab4ec9b8ff07e55800001f31bb80 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Unchanged False Passed
7422eb62cfff19829b5c8116dcf22f48a656d3d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Equivalence True Passed
b73abdac1fbbca67c8e77e8f62412f754ce1de2a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Equivalence False Passed
17fbcedf134b50702d99a542783913541d6bf6f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun StringEmpty True Passed
8680379173c99cacabe6d00d72539823d804fb51 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun StringEmpty False Passed
3e560d7c9dbdd3c38a8b520ca2de087298b70657 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun String True Passed
d5e696eb8c5d8f3d6862d8209e398fc5d18b23b7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun String False Passed
ee2b3fb4cd8c86caacc7be5a4476f0a909d8878c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqLen True Passed
72bb32f24902d83d30ccb3410811a3fb6679f589 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqLen False Passed
62525f05999f3e054e9fe63247452fd359e6b7f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqConcat True Passed
269a07961efb5bc4b81534268d2aa5c8384a8909 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqConcat False Passed
fc0d0ce2d316ee062469dcdd7f60a87f1b3403aa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqSelectSeq True Passed
cef28e0bfbb4e190e83a65cee5c1ff9491926cef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqSelectSeq False Passed
b890259fb43fa60431288528955bade1d38f138a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqSubSeq True Passed
d79ddaf54fabd0470d714c6364ed91e25776df85 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqSubSeq False Passed
99a0216dd56cafa21e7b8e1fdda20385dded8afe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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
LetDefFun NumRange True Passed
766ab7d3e27ed8391d08108c270cae55fe2f607a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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
LetDefFun NumRange False Passed
6ef48d7d4cbc99b89e08d10929ac8981c48b39ab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFun TlcSingletonFun True Passed
91b4f4c1f3096c8961f204dfd4051e3955a23403 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFun TlcSingletonFun False Passed
8ce929cd8ab155693ffae8c42d31de869e4653b8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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]]
LetDefFun TlcExtendFun True Passed
cd07936abf2ef415adf03a04ac6f4b66d2b5deab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • 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]]
LetDefFun TlcExtendFun False Passed
06e98bc92af7f4a62cc43d7ccadb6ee37eeb0923 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFun TlcPermuteFun True Passed
1567311d8c2d65f4717f4054a04ebdfe299403ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFun TlcPermuteFun False Passed
3fb98a8025697a31d2346cdeb7362d26f1990e1e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFun TlcSortSeq True Passed
7647ccac77297478e04793af48f821f17c04279c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFun TlcSortSeq False Passed
91b8d1879e80f57974277c4a54ab2046d57f4a1c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFun TlcEval True Passed
09da2bda2e5960e6670ccbab0298d233c28affe8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFun TlcEval False Passed
4f25234ca9c4f58899ee76e5608e90556949a64c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagToSet True Passed
30bda84894e04d0bc4f79dc0822b4be24823bd15 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagToSet False Passed
e7a3b50ae3de0a3c98ab15f30fa214bca39f5971 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagSetToBag True Passed
f501ab29565bbb7a82e006c2ae91e4909fdd1782 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagSetToBag False Passed
71eb88cdb6147a592f2a5bc794ea9b9beee3f8fa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagIn True Passed
9f996c22766a340417a46e2a82e0c61da98e7b82 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagIn False Passed
c16d6678b4e676b8d72d0729cbf943ed33705e2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagEmptyBag True Passed
00ab0e2f26876d168a99f3def3e0d3970ab7bd79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagEmptyBag False Passed
786f42cff3b332be04395dc77d5d8ebf97a30309 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagAddBag True Passed
94aaba9486fc20f5e430401e7e765519a1a3848d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagAddBag False Passed
61fc76c6444b7b4618d73be83493b3eecfc6b8df TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagSub True Passed
e009020e5c9b689ece0c306c1bef95f5990a2567 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagSub False Passed
340ab6b11a1e8e043d1d4193f2ca22110945aec2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagCopiesIn True Passed
6ebeacc3568e4de68856ecd0f35951092e212686 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagCopiesIn False Passed
02149e5f86266d3b4ff835f707af2bafdec6d142 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagSubsetEqBag True Passed
98fdea14c2baae0607154856dc83cb137209050b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagSubsetEqBag False Passed
f9e8b132d2dbe748158dfcc1a649bacebdc6bb41 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagUnion True Passed
285d35a3d65085d0822292d1ab0948c70ebcc67d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagUnion False Passed
4348ad8772e8fab211ce6a38fb90915f466707e7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagCardinality True Passed
b5f30a142a0c1f4465cc90857519d32760ef48fd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagCardinality False Passed
fe3ab3d3d1332302c6c4fc83a491da1123d39c8b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagOfAll True Passed
01dcb3ce04583cc4b4d3a30263528a0a52b9b753 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagOfAll False Passed
c606132d195d5ec687e396e262d2a531b9246c8a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFun BagSubBag True Passed
42e9066e753d92766bc13c7d71583a163ab678d6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFun BagSubBag False Passed
3d07794be1bb6b507aff45eeabdec658ac120fdc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFun FiniteSetsIsFiniteSet True Passed
5c658aaf27bc36e83d11b661d56be51517f9ae42 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFun FiniteSetsIsFiniteSet False Passed
d73f57d87c65e97af83fbe24aac3107fa052f69d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FiniteSetsCardinality True Passed
43a423659d7a979df90bf1242701a7fb39076ccc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FiniteSetsCardinality False Passed
8fc43dc032129265718d0b7c09c3e64339beed68 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqHead True Passed
da1b36df620cd74d6f5d265792015f285a626f25 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqHead False Passed
ddd26ff2688cfc715f08f2e700d981ceb63889cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqTail True Passed
76c1ee8793efc20ffc574ad5a59875aab80a2497 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqTail False Passed
c4736b3d573e0235ca258ac57c22e72218b47f1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqAppend True Passed
0211d0a4aa4b77b92c887076297948437a423f88 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SeqAppend False Passed