Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
dc8138142d31b05a2b0ec0ef30c0951c945175b8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1 OneLineComment True Passed
fc5c707e978a0a5c4ca2cbea116c6c7168b1bcac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1 OneLineComment False Passed
5eb3ea62b7233fd9c668fb2e5c52e6aa58bdfed7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1 MultiLineComment True Passed
da89fa7b6026d9ad2959d2a09ef8d5acf3b3eed5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1 MultiLineComment False Passed
eb85d2793bc509d21d46adc08f2ff14073b0afcf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolTrue True Passed
8cff8775c30d2219d89241e1a2bd9c9ee81e2616 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolTrue False Passed
55df86dbf80ada2ceb8cdda249fa224600299ed8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolFalse True Passed
1ca0794a32c0edb2a94d52e8580e9bb2afd10993 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolFalse False Passed
e1cab0bf2fd879d751b210c9b5002ea271cac2e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolSet True Passed
0429e99ba55f0d256b1479764dc764bdb03beb9a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolSet False Passed
fb5059d04468edd8c277ade1c82eafb29596d536 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 And True Passed
dda05781d09e2f0aaae766bfeb2181f79fac6b3d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 And False Passed
15350e7ca5f7524d955b3906e57ff375296c126a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1 AndMultiLine True Passed
d5479b4eaf7d1378c416506e53eddba18afb9f1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1 AndMultiLine False Passed
6310145efe8acaa0692cac29c9b1411f053b5cef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Imply True Passed
ca454aaeb4b18aaa282fddb02c42d09879d6e968 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Imply False Passed
abee8024c5fa8b5411d45c242effe4916475a9f7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Not True Passed
326d0298ef24da0b5d7cab35372fb89b2b5e34ea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Not False Passed
efffb1262ba47fdd78e96d76624e09eaa3651348 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1 Or True Passed
68cdce34411be61e9c6e57b166fe8eddbaa75872 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1 Or False Passed
490aac228ff8fd7102d993e9b8fbc2504ce7a190 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1 OrMultiLine True Passed
5f4c49285eed7501aca9bfc5821dbcdea39431d7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1 OrMultiLine False Passed
2112b0bba636c82d6fbe0b86194638c240586d30 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 AndProp True Failed:
312db9b5717cbea8662e5b029f351565eb5c4ce7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 AndProp False Failed:
d369dc83ff2a09bdbbf5ebead912c851aa096528 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Boxed True Passed
c37e9ee02851013fa72d288184b7b1a3cab45c0d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Boxed False Passed
f3221eaaacbefa4305359651cf0aa5f0399dd17e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Eq True Passed
a06f07cc96ea67303db199a9053c05ada4b46ad1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Eq False Passed
ea7ebc1a3f70fb86d2507f37117c9326e60d6d41 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Ne True Passed
4d0c0572eeb7d41a186334029d41c01c7b3e4adf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Ne False Passed
22f80d73c46a9a5f757a1fa39e5bb5245e48c6bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Let True Passed
fc3d0bab8f467b824a34552f075b7f9a70d7bcb8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Let False Passed
63fae67ec6e9b7da20cae58deb30b100d2b82d26 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetEmpty True Passed
ca621011c8acde57eb9a60fc9616015b1ff51fe8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetEmpty False Passed
100f0c611bcbf784fd75c683e36b8d2598fea499 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set0 True Passed
1022e6ab381588b76e515d41a995011d1a996ccb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set0 False Passed
5e1fb2e6d4b08dc187890e70b23fa8da742ef619 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set1 True Passed
e6bbf11c85063e4bbd50d88aa27a9c6d080d32eb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set1 False Passed
11b839e20e8e00b9754470aa189fa420b64951f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set2 True Passed
163070e978a06b35bd0a3562cd881163199672d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set2 False Passed
3b89fd242124155cb31c06881071f2fd88c151d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Fun True Passed
357b3c91ae17a4b51975ce69d4bde61b547e86a1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Fun False Passed
9a52dcd1e30e61a805ade484b67cca247ad2abc0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 In True Passed
c36225bfb4e713319b427040c483ffab2ce5d460 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 In False Passed
06610d686817b239b89dffcc3c4063407a02b71c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NotIn True Passed
27018e7d26ac66864b2a6e3d42318897fdbf529c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NotIn False Passed
bcd3e40d9a1962aee490cdd3076a283772f80a60 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Exists True Passed
3586ae638a3458b96c356e1b808e6a8a73ac44b5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Exists False Passed
afcec437da7c0bb1e0adee3f927db76b9db909e8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Forall True Passed
57dd3171665ebe8841d398b67d649263980997f9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Forall 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
1ba774e9d036a09a8e5a24231ad50fec443aa6fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Record True Passed
e81736ed26a95d2f5a472da72c2fbd64c7bfb268 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Record False Passed
83dff96783c591fef8cc20dd231593f22ed2859c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Tuple True Passed
a067c877dc5326802c5fb231357c6955f8824b79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Tuple False Passed
abc58d2dacbdc205b8aa69aa9b46376877daf85a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 TupleEmpty True Passed
d26d8b5d4d5ccdb9066da33cb89050d95ad3d41e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 TupleEmpty False Passed
1bbf8ed3327362487cbe044624fe9050992b5c7b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FunApp True Passed
89e33cc6fdf3c8d8a72aafe991ddd7d8106d1f03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FunApp False Passed
f7132d280c46e3db8eb9dcff91504d17354eb8f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Prime True Passed
e8142ff980648af20d971858a870279713a15a4c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Prime False Passed
033f91da5daab223f44d61be243a6230bd780aa7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumZero True Passed
51e68c32137b86d415449dd49e473739c0d62064 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumZero False Passed
e13691787d41c31e01a8626b4ae7650ff41db20c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumOne True Passed
6a9a07638e9b64016528ac727dc7430dd88d4541 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumOne False Passed
b88bb74977d56434caf22660993c1c1b207fcaac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMaxInt True Passed
92627e227f6ac5d656d590ff24c43518e3c0132f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMaxInt False Passed
aa8cc88e1781ce0dd54c56be925ed426462ffb48 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumUnaryMinus True Passed
9070b4a56ed6266a4f8d414e768f8462e6772f9f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumUnaryMinus False Passed
84ad8d699e5341105a96ff44be37c97d79e3bc6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumPlus True Passed
7b14412132c0d1d915f00c5fcc97ce5b9fc9d477 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumPlus False Passed
6b3ff0bdaa5e78f28031505a4f8a6ef5168b5201 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMinus True Passed
90ffed440230a9e59f4d5c9f073b1216c4694c5c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMinus False Passed
ff624153f54d70704f7a7166c59d395f07da738f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMul True Passed
9c298240c23a3fa345f83bb5de003151ce4f088a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMul False Passed
96334eb2a6fb817172548c6854abf8f7310e18a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumDiv True Passed
25f9c6922b35e630aaa35b3ca038337e473bfd3c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumDiv False Passed
7a92081fd430c43bed4bf94f618a7d3d890872a5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMod True Passed
a70b5430ba8acbf7a5dc6d5080e58d855bf71858 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMod False Passed
e2550e40efb8daee96210dd625c326e13a3d1854 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumPow True Passed
7d49a252b3fde1dfc06269b59da8025730ef2d30 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumPow False Passed
79c3c79f42a2e6b9369b787479ba71b777859f81 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGt True Passed
3b26f0b27877e62ce57c9758891ae254d7b3b471 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGt False Passed
bcecedd60843204f9b26cee96df0a3bc689a643b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGe True Passed
0492c0ede8553bc9ec25fbe6feb7759a69af5c91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGe False Passed
2f06a69402ad8aa34a2de559e50b69dc165b24fc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumLt True Passed
7461545bc20fd4b7e0f6b16c4df07f0b4f7fcc5f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumLt False Passed
d8bf0181492c45c3a08514e1c9b38d1288cd48fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumLe True Passed
1c6cc90f9d6e2fb3a5b3f99d61500bf8402fd825 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumLe False Passed
af8b40a5a0a73f26cf4ad6cb6014d36095617bff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 DefFun True Passed
dc58cc30d04d54a9706d118ddd8f34cfeb11d8f8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 DefFun False Passed
24eb180a12d73add4845c6666f4a13b0a2e7bf2d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFun True Passed
103f4cf74249797dd4bd8dd4c07b696cd3e84893 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFun False Passed
eda37c8d968deb6630193643150916a499e8eae2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 DefFunRecursive True Passed
ba2a72639363f18529f703b9a5535bb40b34cea5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 DefFunRecursive False Passed
d94144a651ea9a9e439c6ed48dc58257cf4afb4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFunRecursive True Passed
cd691e1c744cc3a3de2e13704366189d08f64d00 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFunRecursive False Passed
4026b0981b097f75a698b3dc0a2b6648544522c1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def0 True Passed
ae2345efad578627ad665a7ae4786159e8277550 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def0 False Passed
6b16de1082d98ecd3c79ba74d2f5e3f47a58ede6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef0 True Passed
c04403256589af8c489f6f99c5b48b83f6b26549 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef0 False Passed
0b5365190bb695037e91377429d13fb44f498161 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def1 True Passed
dc43172f9d91a3923df1f1c25cd0954a3135e036 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def1 False Passed
8d9dda7f61a8c2f80172ca08ad32617796abf4c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1 True Passed
bff47f74743bfbacb29da3890306e7214fa38ee0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1 False Passed
74e06541e1686027f4f31d54a172a008a02c7cac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def2 True Passed
f4263cb9246c64f20e729ce9928712c844a7e23a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def2 False Passed
5e1fbb024c2acd63747fd61b872b7bc55aee2620 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef2 True Passed
b99cb7194223154ba878784da14ffa31cbb47108 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef2 False Passed
c0db27afa615cd6f13f55e44791f97d7d2f213b3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def1Recursive True Passed
3ec1209c2beb6c65d28ca5396a82b1ad93b0f5ae TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def1Recursive False Passed
6e52deb433e3498eae1d8df6c89179afa5476900 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1Recursive True Passed
d023f5ba8c91d3ad008d411dae342846a16d102c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1Recursive False Passed
d300749b4c6c806aade6904cd2271a39535b17b3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Extends True Passed
89b9877d604c025c3fa757659aecb4a06623e889 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Extends False Passed
5e98496d1efbe61a5a6dae86d43c9b7526e94f16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ExtendsInDifferentFolder True Passed
9102822bdb030181b16acf3651497bd2cc52e8c3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ExtendsInDifferentFolder False Passed
4b47dfdc77ad8ccbc18e55c386718a33d7a554fa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Variable True Passed
b2220381aba4e6c6e90211bab1511ffc7ba26add TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Variable False Passed
ddb31b1c64d97e6a4df4c37c136edc8025b71baa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Constant True Passed
b6b9b96a9ac144331d2ceb4bbd204aacdc2e9631 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Constant False Passed
9ac14504e2ec9430d9b649a392e045dd970a8c26 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantModelValue True Passed
c96994c68b952c43ff61673e3596c59805e07734 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantModelValue False Passed
f8789d0acee781b6d19f971714c8c3520d0117f5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantRank1 True Passed
f3ff79e9fcb329c551f3d59dbb8d72d9de4fb31c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantRank1 False Passed
d10a9ffd011441149590bd08fc7bc7d61ecd776e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Instance True Passed
dcd1e43fb715204df212e6846b7653b74ba120d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Instance False Passed
a838827ddd15c59450ab8d5c1e882009752535bd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWith True Passed
94693b6b179b12e589fe91a8a27166cfd7a9312a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWith False Passed
fc967a58fe53f8448268e05bdd3a309d288722f5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamed True Passed
bc281a8f330907a5450cb08c8126ec4788896a88 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamed False Passed
03003163005233277a9e8fc77761817cd34b28cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedWith True Passed
1b5468dcfb66a8a876951f243f6da7f95b54953f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedWith False Passed
76cd2e7ca7d9560885ed35af51f793afd44912a2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceInFolder True Passed
d60932465786f2aa833d521909eaba30270b9c94 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceInFolder False Passed
50985dec2d392bdb8f91d4c7cba4f157aeefe929 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWithInFolder True Passed
97b4f801b90e46df5977ab3f599ba3b2eb2dd142 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWithInFolder False Passed
6fc40b8198097a4f8c1e382e87e7138ab0557b80 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedInFolder True Passed
a04095c2edd083dcad4542759e38539c1c27e0fc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedInFolder False Passed
217a1cbb873c79302d54b784b4522a4c33c974d0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedWithInFolder True Passed
c66bb37b7ef75cc7ce8f8da2baee0cccf19aba83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceNamedWithInFolder False Passed
3f33567b2b1126d471db23dd0102b6c569a33d7f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Enabled True Passed
e18c3913315276259c1ce205c646c66f3a6d4a64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Enabled False Passed
5e07f120e9cb98738540b748a420e11432381ee6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross2 True Passed
50ece3b8b5d3e4899280e15d38b2a68a9de26fc2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross2 False Passed
3f654648fc06ba8339c76da44f34570276506af7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross3 True Passed
78d634ed246221bb96273943a73d656d4b78a994 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross3 False Passed
c5e435e7c047ebac49c8c5479c823791da43cb45 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))
LetDef1 FunSet True Passed
c9b91f0aba43d2f9a3a587fe41a8bed1d18c447a 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))
LetDef1 FunSet False Passed
9afed542bc358395323bb0e3234c293cfd6ba7a9 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)
LetDef1 RecordSet True Passed
8e8aa54ad664f6b5599d4fe2c8b56ae0a4c13e9f 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)
LetDef1 RecordSet False Passed
01d3f136d1df13227b7dabc88c8f118e84465d84 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetDiff True Passed
c19c08b2ce6b3244b17f4ea9f44946bcd73935e8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetDiff False Passed
29aef3541b2f2b2ff1f841893e4fd42cc2dd3f32 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetUnion True Passed
62fe15e2d59f6b7097f86adefc2211d951e662b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetUnion False Passed
e48b7e6a64d98a2b9018c344a83fca5e46fa7377 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetIntersect True Passed
6a79957be51cf6efe2bfe048f62d6b30bb698cae TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SetIntersect False Passed
ee1c53143a8029593f3df12ed0221e5a0b62fca3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SubsetEq True Passed
88b569803c1bda88093843d7a1a38a4ad7a8a957 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SubsetEq False Passed
b448206fa91594fa08e12712562a9a5475d15e15 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfCond True Passed
341237aea599739eb28b614217622b85f47e8270 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfCond False Passed
0c3cc313882e349aea2c280809beaafdc19bf302 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfThen True Passed
7318f6c3e8ab91dc3e138b87ffffa4bd5592580c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfThen False Passed
e17489f1238588d7d331406386bb8ab28c93ea45 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfElse True Passed
1a63db77801f1bda6a842210bc4cf2f93c83cbd1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfElse False Passed
9b9da29360dbb71bd259362ad04d81458ff9f2b4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Subset True Passed
b66ebee914bf46fac75cc3a5be91c668cf5f9f16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Subset False Passed
1cb05ba7e6beb1c48fae3fa7cbbb3c1f41671f7c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Domain True Passed
c80e9bd151a52f4d141e255b543843939d61480d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Domain False Passed
74ca2cac96598f998517fdfb86a5b732a5e36f7f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Union True Passed
fd4d16cff8669c32d051023ff25811408e7e30cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Union False Passed
4a77b0cc736fc70bbbbbb18fe8df86c9318c033b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Unchanged True Passed
9c85931c6d618633e6e8619e1e0d6c2b2d15533c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Unchanged False Passed
984f406c0f713d7c343ebea8875070f197d39dfb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Equivalence True Passed
06e7c75dc450d1d5e285fef8fa650727cd76e905 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Equivalence False Passed
5e49df479f0f7109cc2b1b262cfb7bea0f3dcb53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 StringEmpty True Passed
4b12374ae9c103354d4df15ab03b8dcd1375f2f8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 StringEmpty False Passed
176072e50e58f811a41f52873e3033440d4ebcc7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 String True Passed
ebf98a50de770b802f4d53d01c597d887cc5c501 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 String False Passed
60258c4cf0f7103144fedaf5e08056358a0c19e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqLen True Passed
7426260e8dfe188b66ccb208555216aa3677de0b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqLen False Passed
8b3d61751d90bb8c1e91857aacec555861c6c3f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqConcat True Passed
8c20b0697476682986b91703bba5b894796ffb64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqConcat False Passed
9342f474dfe01adf76913fccba186e4a630efcfe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqSelectSeq True Passed
5fc3a3935d307010ad1f6545533667833b25acb0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqSelectSeq False Passed
67b4d42c6cad76e6478fa11732cc9dd6d4e7be18 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqSubSeq True Passed
e161ce89ff95e7d5a2c047f6f5c633e6e0cba17a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqSubSeq False Passed
96acd31e906c1912b24de5a04eabe85dfd07f410 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
LetDef1 NumRange True Passed
fe714e66bcc86fb419eb848a8d387aacd5caf7a5 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
LetDef1 NumRange False Passed
fff05e373aa941e465062760f79883e3e1c65952 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]
LetDef1 TlcSingletonFun True Passed
cb4b1ce152d73dff3e67c9664a6d9828b3c37d1c 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]
LetDef1 TlcSingletonFun False Passed
9677dec45313effce5d2139bb7050c9fbf0c2f76 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]]
LetDef1 TlcExtendFun True Passed
5ec83fce35e4bebcbf8f3cce38aeea90be1abf3c 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]]
LetDef1 TlcExtendFun False Passed
b0683d07525e5f41f8a8dd4ffdb1506b865257e7 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 }
LetDef1 TlcPermuteFun True Passed
2f646f41c5d805c0c4dfba0b953efe293c37a67d 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 }
LetDef1 TlcPermuteFun False Passed
3816397713537ea2d3074ba69821549d68eb2ab2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1 TlcSortSeq True Passed
08ea9a20a6965f46d0aeff434d10542052bd99a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1 TlcSortSeq False Passed
59667ab6fe09aa1559bec815e2ffa977947a20cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1 TlcEval True Passed
2627a13db5158389e427535b5ea9356ea7120199 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1 TlcEval False Passed
5f0294d254973d152c4b431e2b3beaf4d58f6cb9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagToSet True Passed
0970a196ae86933c98b9316c5e89827ac3719fb4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagToSet False Passed
15c9a7e348e51602598d4eababef11d83d9ded8f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagSetToBag True Passed
415ee645fc609d5ce8fe33b4a39e829d2bc79087 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagSetToBag False Passed
a6850ad0af5427b9e5095d382c32a6e819a2839c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagIn True Passed
79b3dc74e35749c1514f7131587a2dcb6310b0b8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagIn False Passed
f33f3d6aac037b52011654172350a1c558c95d15 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagEmptyBag True Passed
901f6771b0feaa366f57f76e6001909c1d26ebc2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagEmptyBag False Passed
0738ccae2bf4e13a0309e22a08169bb68dbe08a5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagAddBag True Passed
96896d96d1ad803c361f0924609183c5f89cf604 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagAddBag False Passed
14b72d0e07389985d6132e361779baa973cdf49d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagSub True Passed
c657cd04d0caa0602310cafd2c0b2f0a8f60064f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagSub False Passed
0815a071e4db7bddd1fa99ee63d291482ac68689 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagCopiesIn True Passed
c12a66768c7580a6259bb7cd471150fa63e92302 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagCopiesIn False Passed
79ccde906d8f45828b4843e4a7249e5a2756d822 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagSubsetEqBag True Passed
3c4404d81236492c987ff30ebab98387e8790016 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagSubsetEqBag False Passed
471ef9e3d0f98a7c2c8ca9091e4f6f74bf32c6ce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagUnion True Passed
b4f758cefae2a382723847526cb3479662c0638d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagUnion False Passed
5667e7be0ea4f9428721e72a601e1d42efdc9399 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagCardinality True Passed
37f7919f92f0ea1983d276d73cea8c7a3f4b76f2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagCardinality False Passed
13b4380d83c842dfb67f8c7879a837ff30bac0bb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagOfAll True Passed
4d2b5d9691b5d61577af85c1605bab8fef509a8c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagOfAll False Passed
e915c592f4d5360a36c06fbf7b1ba4cb1fc4d018 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1 BagSubBag True Passed
808bf460a4e5ccf8577cbaf3c2ad0de298b279e2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1 BagSubBag False Passed
09dbc5158154b4ea3841d8620cda1ece12c724f3 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)
LetDef1 FiniteSetsIsFiniteSet True Passed
e14b49b7137ac711b844856cdb9b50ed04e164dd 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)
LetDef1 FiniteSetsIsFiniteSet False Passed
de31ba87244136cc9d647dd98cd62a17a66bd5f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FiniteSetsCardinality True Passed
37046b9f96c255f78e11666de7432cfd2152f1be TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FiniteSetsCardinality False Passed
d47e13a13512d6543410f2dc65aa7705bb20db94 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqHead True Passed
7ffa03bb86488d08fe771e5fb1c436540b7200f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqHead False Passed
aafa03dee3dc69e3ab7f77bbed42c1ab7821b97f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqTail True Passed
219030e342244b2f7e9bad043e123a9b7b3d53e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqTail False Passed
26db714723df9b8c6f67015657d864a71e3d76ea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqAppend True Passed
0b8ec3806d6f9c23935ca9db26ded59a05a7e439 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SeqAppend False Passed