Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
9124a040053b6d82af1df658cbdcd1c665aa5cce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef0 OneLineComment True Passed
87ef7fada4ec0ec3c47cf784a364e1e1d500534a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef0 OneLineComment False Passed
6f62643d015fecbd5900eaa0a52ba291e6006afd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef0 MultiLineComment True Passed
57b3723e9cfb61f428d4aecb3cf9f46b556fe08d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef0 MultiLineComment False Passed
243fcf7d03cc54d9fb84e884fdc7b3c3d2e68256 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolTrue True Passed
ddc1a8aa230a9c1d1c6ded395beb2fca275b5e26 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolTrue False Passed
8e77fd0535e1ec0fea9ab609eb8da2a7f87ecd57 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolFalse True Passed
db28d00d3f8bff9e2891591f2b6efe6541c2aa17 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolFalse False Passed
b5387215d34b3a5d00841f81890925e41e4b398a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolSet True Passed
4f37077cffb759fbe469bbcb486926c5a624eabc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolSet False Passed
ef8be8c8737efecd864f41b346f4144be2b70b1e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 And True Passed
ba1a817abec98c3c08fb7b75bfe3055adf2f5216 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 And False Passed
c5dc2082848082eba6e2cb7e6a011f0f3625cab7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef0 AndMultiLine True Passed
91493098bd8f81220d2ae089015f1c446d601705 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef0 AndMultiLine False Passed
47a496a6716fbff269ae93978de0a8d04d479902 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Imply True Passed
112a0e5ae950f5c443acaccd94495e6e47eefb37 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Imply False Passed
8654e294bc5e5f214c5fc5791ac4734f13474c7f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Not True Passed
29bb1d48f2d9da0c87bc3e06ddc2d5198ca984da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Not False Passed
8f9f417b9d82881d3d4fc556673c2806f350b1f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef0 Or True Passed
05cfef42439d7bdc292895b89533337f65b1940f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef0 Or False Passed
9aee139cddf4c2d5baee527452fbbe2d88361e38 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef0 OrMultiLine True Passed
e5439557618e42a9b4e110208206773839571ef4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef0 OrMultiLine False Passed
cbf625d7ebd32ca51354206ea7f489ac19c209ba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 AndProp True Passed
d6630e5b22bd85f14b7d037af247629cc21c42c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 AndProp False Passed
ebfc33eff1b8ad16fe92ed6a179ac451d0dac89e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Boxed True Failed: TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error
a1dc6ecff969a30f8b2a4fd310b4f54b0b3ff77a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Boxed False Failed: TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error
5ffda0770366c85b6b78396eca3b272384eed95b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Eq True Passed
266cb47c07926770e8190b53398d03df2e5acf35 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Eq False Passed
1eca6826ec01f2ee6e9b4dcc312298ccdd1772f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Ne True Passed
5c739aeb1c631c6aa084954dda8f3eb00b721f1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Ne False Passed
d0364d21e6c99192f891cdbb2ccdc78841b442ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Let True Passed
c363b39269a9de4b14b0c43aaa7906f1a2c982ad TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Let False Passed
42fc26662c7efd33195d6792853c4297d93ef011 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetEmpty True Passed
fe09c44128f5e57502bb2472fe5e9cf3b7d991ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetEmpty False Passed
a82b1d18c9afdd6a101762cee7a03af041805693 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set0 True Passed
3148ce013e5f5003dfc5995235854febfcc99b11 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set0 False Passed
abcdff8bdc8013ec5aa6ccbb7cef354be821fb71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set1 True Passed
434d9d99a1b1cfe5c4ca76463df967b26347efb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set1 False Passed
5b64e2c83ab900cf6910ffcb0b623b315e644948 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set2 True Passed
b27ef13055407ca9bf18440486575e6020bc3d79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set2 False Passed
4be665db0f76de4d89309e52ffef51d063825ece TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Fun True Passed
e85d76370b4d4b16e618a00e4ab92030719ea538 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Fun False Passed
d2e56eab8e683b1c45e2a4e16d36d7e1dae28eee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 In True Passed
e29733d95adaad3d6ba4a43b7ab2cffa8f837f30 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 In False Passed
8d9aa3dcd70eeb714bf0d3c534888b4da3d977c9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NotIn True Passed
27c07f6e054ba11583d8b5bb390ca3d11c11fc80 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NotIn False Passed
d7e5536e6a550fcf128050f39553db0f3356c14d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Exists True Passed
41ab87c4881041bfded302e381416b9b7b31734a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Exists False Passed
198a555126d7940481dee7d3dbf5f513f9d33f44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Forall True Passed
8fd4c1ad9ad122c53dad4abd736a62adc5a8d673 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Forall 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
46a02b061569509969d5655d9dc8b9678b0419f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Record True Passed
61440374d8026d10c40a0f7c87b0b5bcf0ff04e8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Record False Passed
219718866511b9086460f8d4d48c15e009ac0545 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Tuple True Passed
7ad519f21e65eb905df7c918d51939a59333cc67 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Tuple False Passed
09ef2acb4e296a01c1607e433d9719d1b0c9864b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 TupleEmpty True Passed
21a33231ddeee88e8cf2d4ea68c3410dfdc5ef1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 TupleEmpty False Passed
45826a23aae893d4615f6fe74ef600d6118a5820 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FunApp True Passed
9ac299359336c8651641f268228a23f063e870b4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FunApp False Passed
184c335f538091b8680465d20fe199e30b2300ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Prime True Passed
2d8e09c9dbfc82db275096b6f123cbf3ce4f759d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Prime False Passed
6c80284b5cb8f6bfda7273b3e41eff31063d777c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumZero True Passed
18e0d35d98145448e1db563d61d3892646886524 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumZero False Passed
6e2a4268622a2d8353f60beef830ff398b0240e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumOne True Passed
e10de84ba9ba4378867ff11cfe719127efed5145 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumOne False Passed
eecd05d6dc142a68e9f3a144ed6e9fb207d272f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMaxInt True Passed
b7085d744184f54559637bf44cef711a7e526194 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMaxInt False Passed
f379f8cb5678f31ff0b592aa6eb2888ece551b66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumUnaryMinus True Passed
609e63ced72f1459acbf7f2026de59695002757c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumUnaryMinus False Passed
4f4e42a8e4dff8c749f1454967f42ee58074cbe0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumPlus True Passed
ba5ef2ef2fe37dd01509ee52b491736f1bb47056 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumPlus False Passed
3eeccf496c7c621fc80b4880caa10de36caa4ecf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMinus True Passed
f67147a0883e31be1bf1dc99274c83a2c6744caa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMinus False Passed
1a2d5befc34ae7f1eb64020e42776f22457cb0d1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMul True Passed
ae52593fa454c976192d6c93e1fc7825b05a1d98 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMul False Passed
c9e2f96cdcdc3ffff3557a9c93e5d3c9a81e2190 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumDiv True Passed
22811d783d9a6f2a1dea34a8b41b2fddf84610a2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumDiv False Passed
ed4cdc938a75c3f29c14c5584c7d31e43c7e6a20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMod True Passed
97c4d41931c08688c2f49fad5208bfd6cfa655dd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMod False Passed
e0494793002d80fdadb8563337fd13739322b5fa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumPow True Passed
354e01a7387d30b25db9de611c98d114ef58a03d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumPow False Passed
0f5cf71febb1d5bcf6e25e8b52b98106b3c35ff2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGt True Passed
87f5579b3bccf6bfe4b1552ef0bb14cbe4150bd9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGt False Passed
f7a9a04da8f51e8385bb76b3e09f6bb7bf2f1315 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGe True Passed
f15e1806631f0628c26840095e369f6c7c177f86 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGe False Passed
bc45ec19919a9f7c2bd4837a8eb161be60d0c7c8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumLt True Passed
f60b455cc782fe3e0bfe6142e6e4b8c33036929c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumLt False Passed
9c801fa85815155fcee1d4c2c352039f6d0e8cc2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumLe True Passed
dd6b9decb81c911b8c13bc31a9786b745d196a2a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumLe False Passed
3d296633d38eb2e8a81948154cf6293ddfc81497 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 DefFun True Passed
0bcf4f721821b263afd5ff04f254a63310ce657a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 DefFun False Passed
ec0fffcaabf5198ed3966af9740722d8ed9c42dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFun True Passed
0ac97e025a4a350b207a1246ea986a774fdf7692 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFun False Passed
b761d26c5ceaa378d4f6db750185fef554c01d4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 DefFunRecursive True Passed
2fd0173f7ae31cf4a32d97d5d6bbad26f36dad7d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 DefFunRecursive False Passed
9fd8e209066b716ee77e641bb0514d657c66e0ee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFunRecursive True Passed
36361d01dacbd335e4352e5f7cc4d0373835cdb6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFunRecursive False Passed
31d546a74ebce4b21c2e623529bd4bdeef07525a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def0 True Passed
d8a65e1e2830a1aea4a924485b9bf76fd1f4eff7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def0 False Passed
6fa34718e9698df40031885bde641c27dc9b7410 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef0 True Passed
dd3ed2ff5d879215f31c38170449c9241ef41f95 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef0 False Passed
a0e360af0245dcdbf1b7b34a8080779a8c2685e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def1 True Passed
4a4a089498262d11819a145da12693c108530bd9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def1 False Passed
f28afb5c96845b022353df8aab4a6bf03b7aa720 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1 True Passed
5abf08f900b8840a42b8959c4ebe982df5c36571 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1 False Passed
ff491a5774a36c50bf715f7dfebe6e2ce9b330da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def2 True Passed
06dcd5ecc0a80fe22dcfa603a49c135fc91d607b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def2 False Passed
0254854f531d7d7390bd4ec24fe7e0240c519db9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef2 True Passed
1bc9eb825489ea59d31b4aed1c818384d68dcc4f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef2 False Passed
a993b96e1ab6bc824bac4f58a4199330fdd4f47a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def1Recursive True Passed
16c920966f79ca8c90069a9b3484aa31df4ee0b9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def1Recursive False Passed
6cfac1e6866ed7806cfa5fab08933319d50097e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1Recursive True Passed
4fefd9bfc2d2a813bb29099dcf7d738948a2663b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1Recursive False Passed
6452f4e62ca9ca96aeb61648f013d1d85067a313 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Extends True Passed
e3dd862656237f7d04f2d2958b64342dee31af0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Extends False Passed
12440f22e89e0c781ed35b60e043ffb610b53f96 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ExtendsInDifferentFolder True Passed
7ba96ea5ef29219a0dc884a15e10c7b5c1a1439d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ExtendsInDifferentFolder False Passed
71dccf6cc7a9dd4a3b192c01effc0866e352e01f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Variable True Passed
59dfa0efb7f35ea96833d773093bfc6edced2b2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Variable False Passed
4397356b437e2202bc0a3d361e3bfe9009d587e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Constant True Passed
2ed3ea142a949dd9590103ef25b9948a0a00cf9b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Constant False Passed
a850ebb25ddb878e194ae0230ef484b02459ade5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantModelValue True Passed
ce65a90dfc860f2576e4e1263b8bac119fbd581b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantModelValue False Passed
c0bbb48bb07b6567ac50b3b4de2759b75d820f4c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantRank1 True Passed
91b2183e978a9312bd726869850c404b89334a9d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantRank1 False Passed
c37f0443a813a3e0974a7f3c34abf10e19f6fcf8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Instance True Passed
52a83398bb8e39c1e0c17f0e2f43e72c9410b86d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Instance False Passed
dc6e6ea913d103bfc4586b1e3a5a348ec90dbc54 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWith True Passed
01f6b7f8a65dbb277135df5317bcda7d03a48967 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWith False Passed
4b3902e1a3dcdb5ad63b943868b948be06884cbb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamed True Passed
f85a1347ebcec96752041af2debef02a8ad277cc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamed False Passed
d603e15c374a260ab248ee129bc3c0c8167e0243 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedWith True Passed
5f4cd1625ade66e51c06f1ea54d05d1ac09bc6ed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedWith False Passed
8e328870cbf94813b147baa3d7e31f318e4651fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceInFolder True Passed
46c753c3e709dd81698b656953c8e128aa140c83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceInFolder False Passed
dd06d85041c0663442ff0ee8eb07733c60bdb2c6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWithInFolder True Passed
35b8e949bdafb041d5238c6c112ffcd83184f202 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWithInFolder False Passed
3db89303443aff456269ef301d1f71dc5c6fa76f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedInFolder True Passed
c441a15f08133c3cbdeb3a965b9778651fa97733 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedInFolder False Passed
0313b6ce0e7899e1a9dedaaad97c4bbec76afbeb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedWithInFolder True Passed
7194bdd9ae2406eb8c6d4ead222b6dc42b9b73f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceNamedWithInFolder False Passed
fbf510b76e52dcd2d8a77bf7e0e30849557a8332 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Enabled True Passed
b6552e3ebab4fcf93fb3432bd5fcf541595366e6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Enabled False Passed
f9ebe48103bb4fbc19776b48ba18bf6b175ddd20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross2 True Passed
34b2116e190a3618016c1e0e80103db1a1194c21 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross2 False Passed
cd8161069913e3412bd08e47adaccef4d3607761 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross3 True Passed
afeb95598bf45370d11c10dc82997280bb0bb6a6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross3 False Passed
3b19ca7e7711e85fbf39ff1dbda612599db997e4 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))
LetDef0 FunSet True Passed
20889ed8f210587361e0d897c01f9592cd50dd8c 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))
LetDef0 FunSet False Passed
b968ee9abe05478e33c2db27ca2350f676a42a41 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)
LetDef0 RecordSet True Passed
ec66ba4960c1729f1885dcb3cfc79efe0869b542 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)
LetDef0 RecordSet False Passed
e0148dfa042811157b67a25e43fdb7622a4167b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetDiff True Passed
309c588d470b0352c590236bc9c71a5bef1c5b83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetDiff False Passed
e8d261f046769d64a2d0d83593d4326545577e52 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetUnion True Passed
fe1d1ad04e8e7f175fafe7353f87e46be7962891 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetUnion False Passed
b6585a94c5927d5b19007b865f3f34851111e654 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetIntersect True Passed
6e448b781071199722e7a42b3416e46d12477e12 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SetIntersect False Passed
efb1763a7190591c70d89e79e116f42a40b8b798 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SubsetEq True Passed
96f66918403db3cf22146a3172c1511bd7d9f912 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SubsetEq False Passed
a57d5f62703eb61d3904d7cd19489ae5ba71c087 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfCond True Passed
3a2d5f98d34750d17c68c2cbfbd3b7b2fa8901e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfCond False Passed
cf7cbdca40456888b6ceea0d2d920f9a175ec306 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfThen True Passed
8f89234840ac1cdd1aa70524c0bada3a0a3a4be0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfThen False Passed
6463bae6262718440facd0b18517a63bb2473f8b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfElse True Passed
209e8ce8815bf22161f4519e27065d05669ff3ee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfElse False Passed
b56a98a392f43bd323b7ef80a2fa551599491787 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Subset True Passed
a5670a6c70c1cdc8596550d85a57b9c65b555e90 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Subset False Passed
8ecc21bda8529393926bb019195687199a42c187 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Domain True Passed
92a538c68b24a62ded630851100ac9315be13d23 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Domain False Passed
88a15e3e784fbf923b4be0c6a3ed0f3e6e3abb9b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Union True Passed
38354be8bfc5ee6c9be8d032b46f58858a94cdcd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Union False Passed
ee19198331c030d2531dfac52ae97108783b52b3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Unchanged True Passed
5d80b29fe0b90e964c62436f3970fbca78d5a3f9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Unchanged False Passed
7c189626fa78da584e5a72d031073aa3a258d3a5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Equivalence True Passed
acc0404dcae61cca816824fbb47dde815f8872da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Equivalence False Passed
efba7c08367e694c4efa84f937396c4c76b43bef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 StringEmpty True Passed
7750696ed1e1fc21dae591e7164d76562bbf8aa1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 StringEmpty False Passed
7407e3c03edd92f6f1cc5af10111c63482cd2bb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 String True Passed
139c5ef3aedd1379c51e3cf08d9c12278813a44c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 String False Passed
d5bfb852660adc0a7c9cd24ee3896dff2be42e0e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqLen True Passed
e065e1feb54b5c474b3c0ee8ebcd75f59e8e853f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqLen False Passed
45622d9d3664a443f19b8f5b4a8d044f17a9154e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqConcat True Passed
a8428c18ec6f18a1504a2e925bf473408541b118 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqConcat False Passed
cab37156c097f1780f03fdf3f44ca51390fa61a4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqSelectSeq True Passed
74850950ad7cfc35cc3c7ba0aef674aa44ea69fd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqSelectSeq False Passed
d829657be7e0d0e58210f67f632e519fdd6c27ef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqSubSeq True Passed
16fa414dfbe1734c02b6ae1abb6fede6bf9b322e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqSubSeq False Passed
fdc3e5ed8f1e065d4b25ffe8f64b1641aefc8cda 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
LetDef0 NumRange True Passed
86cd320061daec0e2c5026c1d02c1f90edd5e9d2 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
LetDef0 NumRange False Passed
2491f5d2785cf5a12aa2967643f1ea5a1c2a54cf 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]
LetDef0 TlcSingletonFun True Passed
dd15fea280dcce98cdb51ddd029040652af01b3b 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]
LetDef0 TlcSingletonFun False Passed
51375abc90a826460c901cc3fe19bad7d61195b5 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]]
LetDef0 TlcExtendFun True Passed
b6ba3329151f78fc6048b17ad03737f081894b46 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]]
LetDef0 TlcExtendFun False Passed
2a9cd0347bfaff4a1aa3396b51ef53cf075b9da6 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 }
LetDef0 TlcPermuteFun True Passed
b41016f06de2df64d2716715b3bb2761f36ffff7 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 }
LetDef0 TlcPermuteFun False Passed
43777adf5c78aa28ea3d61a3e7f484109fe45ec0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef0 TlcSortSeq True Passed
f81bccf8db2b7794d11906baccc2b3afb6c36640 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef0 TlcSortSeq False Passed
ff2ca9d2abcbc3c6d041a3773ec4a5c1cf65465f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef0 TlcEval True Passed
3744ac1114f38802a4449e34f8fc1f54e7729064 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef0 TlcEval False Passed
dab65c582f4efb842b1710ed3d1123621b5f6102 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagToSet True Passed
5ae7839784af7a588a0b3f6b053dd7c04dc95d62 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagToSet False Passed
4f5e2c94f255918638a84fa0c9887f7bbeeb1e79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagSetToBag True Passed
e2c39b1c313c12e969d9401ba8de77eb05761eaf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagSetToBag False Passed
b423f4c424d6d282ff3d9655101bc1cd4319dd4b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagIn True Passed
81ab5cc8bddad8e7d04e24ea61e40312d30b493f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagIn False Passed
f6d7dd7a606ba94f3d13e7da79d6e6fcc0994af3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagEmptyBag True Passed
f0909d68ba06683aed7c88dd0873abc124c3efee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagEmptyBag False Passed
8d8347dd300a827ca02c44044fbab8d94dea61cf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagAddBag True Passed
a3e6b7c17e630f03f2dce4af84e6359a45c90282 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagAddBag False Passed
6caf08717bca7da2e029433467582c0090685d35 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagSub True Passed
ff4ab2eb02998fc0c45e0fbb974dcbb14c43dccb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagSub False Passed
f8512358057eea792a75b5cb6e650709de609926 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagCopiesIn True Passed
eb7ed5011355a206f7feb5f85529a473f8886c3c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagCopiesIn False Passed
a3cbe2cc10c5052f19fa913ebb302e5e6efe906f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagSubsetEqBag True Passed
76bf5654285dc337496329d4296092e8d6c1a55b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagSubsetEqBag False Passed
fca62a2cd3f484b1ededc6740b62392f11587893 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagUnion True Passed
4c7efaa859f3d7a9de967018c3befc48a08b3f88 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagUnion False Passed
886f3ee3ca2183797c2146a0c9b956cf152df58b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagCardinality True Passed
02567ec778d8f82030dc554d9ee7aab9a057858c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagCardinality False Passed
17d745f1cfee6b201eb5f22ea637dc241c076887 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagOfAll True Passed
3d46ba645c687292090314b07200f2d7903073d4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagOfAll False Passed
4c1ebe4305a22ee668e834b110013a621431c92c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef0 BagSubBag True Passed
62ef01e5a9a4c06e938337c4883bc39be14dd209 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef0 BagSubBag False Passed
362ce6c48da4c6c2c10f97c91321d6b3c2d7e063 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)
LetDef0 FiniteSetsIsFiniteSet True Passed
3a4925effcc14a8057d907b2bec39ad214650741 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)
LetDef0 FiniteSetsIsFiniteSet False Passed
fd8e1394fc1daaf14100f1a594bf1716c3802ea8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FiniteSetsCardinality True Passed
78292c7e8ab7a846f1538654175941efad4f20ce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FiniteSetsCardinality False Passed
2381f305b9efd5d804ca9c064a05cd4de322b60e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqHead True Passed
2bc29aff69f3f177621f014216a6e050639c5a64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqHead False Passed
040ae552d87d3042e98039f485b6385f625c4a79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqTail True Passed
8d3ce4fd03c3ac803e4002a187f79747eab6d21b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqTail False Passed
cc05fe817b8925279f62ba715a8715ef02809010 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqAppend True Passed
54532ff20edbf71d3c05babb99630820b11febcf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SeqAppend False Passed