Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
afc39f3cf63909917892d5051418da74a223f603 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef2 OneLineComment True Passed
2bac84092cd96d7d0f487a83e42c0cf74458e1a6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef2 OneLineComment False Passed
373d0137bc5d761d8ae58f1061df5c3e1a5f63ff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef2 MultiLineComment True Passed
9d8f2713c709a03ed9ef501ff1739f3250014638 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef2 MultiLineComment False Passed
dd34e8ec17e2e9d8b9be375ec60ec73032d3f240 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolTrue True Passed
86aab253c9892d8aff1b67f259e06c61b568f65c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolTrue False Passed
f3b142e80a5ee54cb33258112ac50dab2b1c11f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolFalse True Passed
f55c7c5a92a024f2f9a38c42f495a9603953e012 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolFalse False Passed
f6e079a3f069a3f0766b8af6475066910a35cab0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolSet True Passed
044bd080c61752c0293edfa061756bde64c7bbe4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolSet False Passed
94a2ad2f82228a6691a04a9120003d65b10cd9e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 And True Passed
f0c3af74ba4e643f2ed61a6e66a0b021f65fbced TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 And False Passed
066cf7a3755cd12e58addefcb1b9e504dacc00d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef2 AndMultiLine True Passed
ab2c4b6c8215a04e21c0a513db9e5f0fb973a932 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef2 AndMultiLine False Passed
7cd094aa5389af4cf2fb40fe0e831f42bd4103de TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Imply True Passed
cf2c709c8d3997642c829bd7b1b86cb8bcde5ad3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Imply False Passed
1723780b0dd96417494df067a13034d4288f0572 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Not True Passed
ce27716b5a1ed370b28d56684016c92fc61031da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Not False Passed
bcdf0b1874808673ac30fda485a8929f7b5b1c35 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef2 Or True Passed
513b4a76f370acc6522214d2ab2e1d8f1bb28e83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef2 Or False Passed
9ee7638beca80e4dda782d3aa3a04fc4e7cbe3bb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef2 OrMultiLine True Passed
8c003a288afa13c4b5f02ea4d4f8b4eaa3db11e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef2 OrMultiLine False Passed
9a9813ee23635864d7d4ff91c0abb4e5c6265657 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 AndProp True Failed:
0ecca02f55aafe32d10a9660c512d9ac59d42235 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 AndProp False Failed:
94f8afacdb326515d95ee73277d0a8f12d187457 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Boxed True Passed
080a286036b7f56e8556efe40e4fc912b6301a94 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Boxed False Passed
a89d3153f4763e22bc0cb440f13eac554c462dcf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Eq True Passed
4dc329644837ae1c1e89d3b5309b870b1b21f261 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Eq False Passed
81fa06a7d6574045fd0ffba7fd27e4421abf1818 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Ne True Passed
8c4dcf55d89b4d43e86a1494274fab20f9c14220 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Ne False Passed
0e9a1291e0008fb0293669e2a50d9cd8b63226f2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Let True Passed
b36b1d8365fd3534ad587e3a9087ec93dd25fcc9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Let False Passed
22f0a4f2c7139754fb08a16f09af3c027240136e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetEmpty True Passed
cd10b748b5581a076cfa9fc6b5e96ce85f07874d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetEmpty False Passed
7fe1d24d6540ee50c028320ca4be749f1aeeb5fa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set0 True Passed
e56436740982a7ed1bd0c53757e9a8fa5a70f818 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set0 False Passed
c9fa2b89098529d1b81426e0eadab5e89b645ad3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set1 True Passed
f324121853306122b9446991972dd4a550988227 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set1 False Passed
b9dc496ec39a9df0f49b6dcd69ac7c4e55674485 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set2 True Passed
a1fa45bc75656739a1c0c8066826170d0f4b2f0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set2 False Passed
e66f8a356f5eee48d9b88d0c5b931d8ceda055eb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Fun True Passed
8c09a9e76366323ec02bc04d1b1f0355559d840e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Fun False Passed
7e9c9ef4f3c645a18241474d07be77950f64edf2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 In True Passed
7784d91f84968b4b1536ce4ef6f0bd7a0cc81f5e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 In False Passed
ed5ec3e5d78f056f2a84c2bb81e3df2505ebf991 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NotIn True Passed
f38321bae52082cd8958c453f73c93e96c4ce4e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NotIn False Passed
437f34dd639a50d2b0d6a241e147eaf94a005a1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Exists True Passed
8805f467c4e7dfce221fa9450eeabb615b3afedf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Exists False Passed
f36fbcc85ef11b4520758033db43fa23795783a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Forall True Passed
0353715276e71112c93d2188ab8ce4ae4a64abd7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Forall False Passed
c849239cec02222df538b8f882d20536de3ee8a4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Choose True Passed
f4e668470be3897ceab0ee2fd2361f4e4c637cda TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Choose False Passed
0e3a87d69d748d69962b2f0fc8130e56a774f569 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Record True Passed
401c87da8afabf5d9a780aeccfd249e147607462 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Record False Passed
86c8fe9ec788b353b7cde51574955f26b177ee49 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Tuple True Passed
fd9d4dd52a30f6508e15708903e5f4796ba84cb4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Tuple False Passed
a1f4441bdb8e3a2942c0e032a68c9181f2d9caa7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 TupleEmpty True Passed
8f0c93a2f301edf4095bf3f274313ed4b3c33974 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 TupleEmpty False Passed
c899c492a028973f24bdb55b2e142d8065790578 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FunApp True Passed
0d92f3cd35ba1f305291d36bb2501b1cb5aacdaf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FunApp False Passed
c068418e1ae21b7734a9034a9539c55e42f7390b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Prime True Passed
fb1c6729357902ddb257b1ac04fed419f974b281 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Prime False Passed
fb7b24ee9397c31af51ba8afce85e590858f99c8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumZero True Passed
357220bb135089124ea96aa42cf837bf003438fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumZero False Passed
c9e477901a426e9fa5ca5a67783e01c6ae672cfb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumOne True Passed
9348139755819cc01e0c947889dc5a8e09c754e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumOne False Passed
f5240504c1576a222b44aceadf7edb9179d970fd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMaxInt True Passed
545035af919b19272a48dd7eec306fbaa207ba16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMaxInt False Passed
cd853123b8dfc45934271a5e9540db9f70423076 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumUnaryMinus True Passed
da542e1e08361ed6dd3e8acefc3eb209663d9ab5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumUnaryMinus False Passed
a9760dffcf70b65816fb215f66dceda79dd65f8d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumPlus True Passed
8952f51105602fb61ac22fd93995b78dd3f072fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumPlus False Passed
98446430fe34208dbf57e773d77dbc7e33d1e4cd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMinus True Passed
8d55abe31ce6b017f1ff44c389ef34b6ba8e7fd8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMinus False Passed
29b6189de536b4afadc2b453d1d901891588ebac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMul True Passed
4a6be93dbb95c9b193a48654625fdc2319223a17 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMul False Passed
f43a7b42cea16b7b1044c643924bedf375acd9c2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumDiv True Passed
c663781064b7d313539284cea589a140361ed849 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumDiv False Passed
00156b14409d2472b63948829cb7d2d8542df988 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMod True Passed
acf56084a7b2195881dc4e02baf0c1b5d60aa719 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMod False Passed
ba7a7f1d4e250b1a30d7bc0a4ee2c3d047587a6d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumPow True Passed
dff85e894df0626f9494bfa519318f014edca2fc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumPow False Passed
8d34e3821bcfe27bd201ac525498a86282759345 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGt True Passed
29de02c9898fd7075375688b358ccfe5099115f8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGt False Passed
095c8d6ddf6bd95094e855b2b3704f0bca105bb2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGe True Passed
571433af2f70c8add46effa949a4029737a3c573 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGe False Passed
b125752067c1139fb9c09619a99b01bc6b76f982 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumLt True Passed
c095465afce3c9c5545fd6b980c21a0fe8d7e5fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumLt False Passed
821cd4f79d6b084c30c342d451782a9aac28eab0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumLe True Passed
a15a3a4329e533f9e53fd1b252c71375e2fb2945 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumLe False Passed
bb40d25c5fe3e632973083e86e542b10ddba95f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 DefFun True Passed
17c19e3c58980130644d093df66584949008f5c7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 DefFun False Passed
5fff3891a8814c7a29ca7a0002a3c38dbd8f7db2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFun True Passed
d2db52a8da0811e47177b0076c6210ce2f4fc241 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFun False Passed
0a75374c94729e5e22d64950ee0ce466e79d8ac0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 DefFunRecursive True Passed
9d3c1bbefe2a4a68f0543fd065d2212a69361fcb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 DefFunRecursive False Passed
4a88f2177fea5ffeaabfe091560a77fed87599df TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFunRecursive True Passed
de2b13f1f01a3babd3db8b5da0150caa3d6c6fe9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFunRecursive False Passed
2fc7d2b8a3fa6703bf06a481786240891c189cb5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def0 True Passed
6201ad1b19e568c5339977764ec801698f7d0bea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def0 False Passed
02c4a584b382523fad0b5c61d44ae12a27062789 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef0 True Passed
5e91c605dd56dd8a4d04ccb5f8512d0a47ea11e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef0 False Passed
2b09f774ef8a5106cee5f8d40072935a42f90c2c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def1 True Passed
65780d089d5b50f0ee662840d014c1215eb58a49 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def1 False Passed
bfe7fabedd4cc290fa0748d0383757ef606aaf9f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1 True Passed
66e1ad43d716f9347594580764bc50d14e6e2e20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1 False Passed
c78cd0ca983e433ea11f43200b1a4e18ff054ada TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def2 True Passed
5f85b72dfa0dcc52366c80b005ab58f13009280b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def2 False Passed
994663dd468b92047f0fe0a0fadc55eddae4e9b2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef2 True Passed
4596192ec69f6f3ca65c59272e3ad0ba0f7a8d48 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef2 False Passed
be4d008105e256cadd37495a86b38347d7d2ce30 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def1Recursive True Passed
589c41efeb1f5c8e770a39cd23a5138517a5f010 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def1Recursive False Passed
5b7dff94ec9d803babd37d297a9e553db56d7c1d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1Recursive True Passed
c6b3bf66fa552733fc5b9e929ab506f92e0f928d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1Recursive False Passed
597d92ce49db58e6a2ec6da73b38cafe95aa15ec TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Extends True Passed
7efcbc502dfd2fd024bc4235b868057d1b83d214 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Extends False Passed
256cabf620529995f54179484556406f8f6fbcbc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ExtendsInDifferentFolder True Passed
e6d639186ff048b5929b8a69ff060e8f7fd0cb6f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ExtendsInDifferentFolder False Passed
4f3b8cc7d7ff7a5633a71153b8804ea187ae321b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Variable True Passed
be7bfc4efb1d99520f79e3a8e8c9df64368aa532 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Variable False Passed
fe9fcf564b6c4d5127831f7d8ef70347800d1fa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Constant True Passed
44019ac5eed98e3e4d3f1c1dd7824a0efc992a31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Constant False Passed
4918f157c50f3b7e10a6891c18801235fe04a214 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantModelValue True Passed
64669e6cc4452e42d90921e2636b2c1613bfa852 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantModelValue False Passed
cfd5e4a34bbda2a0deda790a430887c968d2cc72 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantRank1 True Passed
b75ab081f5267b4897857a8545e90c247a757e70 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantRank1 False Passed
dd0b83f5962ef9b05f596575b6adaa416a8f41d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Instance True Passed
b77ca9f45ea8daf30fcdff4239c022cc9ac81f43 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Instance False Passed
b44754dce79e5a78f62f56546178a1fd3eff9c20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWith True Passed
7dab05feecc1bea1b7d8d681f652052a11f18278 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWith False Passed
a347a2f83b43dc9a2806eda4a8a477b60c1b517e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamed True Passed
20d776da3e641b535b40b7fb2cf319bfe0ed5402 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamed False Passed
7fe7499713f05651352b11f23b125ac1f83d5f30 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedWith True Passed
ea84216f9b958aef254dd3a5106a86f139e272da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedWith False Passed
831082975f207bb144043febf333a5861d1171fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceInFolder True Passed
140c3366fee0c388ef3bb9d6d71fbeaa5b35cd98 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceInFolder False Passed
2ca777b2f28e5249cd0eddb16a16570c3f0f8d11 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWithInFolder True Passed
4fe7ee846b59470b7b0772e246c761d01bc8df78 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWithInFolder False Passed
97a0977fdc20b8f6aeef21c52c4cddb9c2174db5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedInFolder True Passed
85b7d5be1ed1d9e8fb0d5b4638b2115a06d899d2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedInFolder False Passed
5c814f88a2ccc6a7e68181d36820412718ca08f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedWithInFolder True Passed
c8dc246365c6725ab30b79dc52bb00f3cdac0ac1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceNamedWithInFolder False Passed
cc5dd1b39eaa85dfa8ddb9e7cd84d46725555d02 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Enabled True Passed
0c155ce09e28c2d11595e105671a377b9c87ddb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Enabled False Passed
7c81b240841ca512bc000ecba75867115198fa6e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross2 True Passed
5ce83d4b90a146986c42ebcef3d329355ead323b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross2 False Passed
de0b3a6a3030bfbf755e16a9bea79b1241a9b25f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross3 True Passed
eea23edfb00ed18d27538146559b7cdd39f5746d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross3 False Passed
4a8b1b23e8ba8bbbe3c98854a1e3b152ed159798 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))
LetDef2 FunSet True Passed
64a408dc832c07e6296057ea026adbd69e70f01f 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))
LetDef2 FunSet False Passed
81cf2290e3b89d0f896b171367b0e0873e4122df 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)
LetDef2 RecordSet True Passed
3c54dd9e7992ce5dfac79ae3567c7a4291cb4913 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)
LetDef2 RecordSet False Passed
f1183d2e3cad782bf8bf5cc69a5c0189ad1ce801 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetDiff True Passed
92af10eff04e23b1bbc91f57b942defe689121cd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetDiff False Passed
930d81a7f505466faa5e08fad530e92174e14c31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetUnion True Passed
a36d136616ec3f293e2192de0dfb90c3e61e6ee8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetUnion False Passed
d9ad004fd991f29e6b463f2f733c023d1e721f20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetIntersect True Passed
e4c9d35512c929fab18200c4d4a23801c132350d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SetIntersect False Passed
e98772d34b75c00102d32ce1e11b8d4c42ef466c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SubsetEq True Passed
c602e95afb65070372f8fa5100d420c9ef747c2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SubsetEq False Passed
d5b7da85c46ebbe539268be60856593ab32ba717 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfCond True Passed
f96b00a9a8634d2df0b65c64e4c38c058eb166a7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfCond False Passed
c42263c0a7594c14ac43e222e8f694fcb9ada74a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfThen True Passed
8bc02b5a0a677f824d71b05c02ac641127c63d51 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfThen False Passed
a5f0a01f651922bb2feb2427916ac9497a12a012 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfElse True Passed
46fada806ba491f4bc1be0b995ff31bfe189caa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfElse False Passed
5e6cdd6c975eb796a50e45fc67bb32bc6919fb77 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Subset True Passed
7eb98081297f950aa3d04274d6bb7fe14b196e05 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Subset False Passed
7b93cd475f057dc4a9db0d5ad76bf686aec3fb11 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Domain True Passed
d2a5bcb1f30ef80fdd9db1d311483fd5dcb264fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Domain False Passed
ce8370214e87bd99bb10415af509ba04a5fe222e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Union True Passed
2356a9e71e6e398ad7d7eecafd0916eb00125a5e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Union False Passed
67a1ad6d0c7d483d1019a16abf21ce8682c4551a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Unchanged True Passed
3b0f1e57213db9b76eec1639b4601eccca753e48 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Unchanged False Passed
2350f2cdb5214e8db9cd5e8f54940be617b289c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Equivalence True Passed
b283bef96ddfd6192dfede6532708f916155ba18 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Equivalence False Passed
d7260db9d6dab62a3a3bcd6922fa70bb120ee6f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 StringEmpty True Passed
122df577c8204d58203f3762970b8e1b5a84e15c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 StringEmpty False Passed
5fc4da03893b56c86931c8f385630367a3f46dab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 String True Passed
50c6db9a8cee6043b10b24c829fd09250f02406b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 String False Passed
e2e65caf3d0157bb85628a2c05eea5f0ac2f97b2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqLen True Passed
73e06833eb583e2d188e971da2cb18362ed47d6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqLen False Passed
8076a4ff704ae9db293f975e198490b41ecf8767 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqConcat True Passed
a4c3122079db1a6c9acf712e0e197f0bb74bcdfd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqConcat False Passed
4477e25a4b5a941edaf34f8a629422058b69265c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqSelectSeq True Passed
fee4033cdb7f4a8732f6027724b2772459b7b981 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqSelectSeq False Passed
f2efa24a641c7cfc87da3ee3639ce20ed60f20ff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqSubSeq True Passed
4692e2f01e2baf174ad7b5399309bf145e5c92f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqSubSeq False Passed
e99a59d2f48995b8de880286d86ff31e37c0aadf 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
LetDef2 NumRange True Passed
d8928f7445303ef3fe68b560032a8b5dd05d0667 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
LetDef2 NumRange False Passed
f8f89b4621de0de0e809c21433387b4d7a535896 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]
LetDef2 TlcSingletonFun True Passed
c04676d708aef58380fb00ed9bce5196d9a1a31f 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]
LetDef2 TlcSingletonFun False Passed
c46d7a2190e65bb98f6e19ce8c920cb3fe8a7f1f 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]]
LetDef2 TlcExtendFun True Passed
6703de9bc2ba61a0e9a7cb9d04645bc6c1ccd7bc 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]]
LetDef2 TlcExtendFun False Passed
f53aac28c3f753854330692370f133c36c8f449c 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 }
LetDef2 TlcPermuteFun True Passed
f1ad1ab41ab2934c2c2c6252756eea6a43d2c4a5 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 }
LetDef2 TlcPermuteFun False Passed
a657c7c36ca25cc2792e3e6c4d39a1e0ae9a35e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef2 TlcSortSeq True Passed
3e3a10f09000589e659202285c79cf71d04d8591 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef2 TlcSortSeq False Passed
8816020e1666068c449df11fd2966a84557fcd4b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef2 TlcEval True Passed
35f6f46e1cb69d1bc871d890c27501cd01f60752 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef2 TlcEval False Passed
c54ce5c6d5092916a0af079370db2ca05609ac86 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagToSet True Passed
7cb46146c92f520b3c94723d98c4301d62e60266 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagToSet False Passed
6cf38e0c099708d0ddb5c09596f352d6b84e3fc6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagSetToBag True Passed
27c3edfae9d881988a166dd39b8ff1aafc84f095 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagSetToBag False Passed
b1494bad60e777a6da920a67e1bf7abaef4a1dc7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagIn True Passed
88c4e839ed709c9dca985a48a4aa75a584a2483d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagIn False Passed
b9c92f8c495266f1f3fecbe26f792acd3806ef65 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagEmptyBag True Passed
565a02d2b70b93048c3a514f36176ed089d983a7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagEmptyBag False Passed
31ba213488f001af7dcf64ab0445e8c7a4be4948 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagAddBag True Passed
a3157fb8ae3d0c348de9819b3e8a11593da63fb2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagAddBag False Passed
a21fbf2f7d056d94ce7282b713e9f4b1612e5404 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagSub True Passed
7d8af7d6178e20cbd96c4feaeb2937edc725e970 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagSub False Passed
27a2486fb9f99b915ce8608363cc69afe246fa24 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagCopiesIn True Passed
faaa723f1b7429e258c2870e2d2a3aa3afb2da37 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagCopiesIn False Passed
fdd64b6131d862e1e3d943c333fa7c6807a77bf0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagSubsetEqBag True Passed
81ebccc624e56cac2a804c3061244449917a0c77 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagSubsetEqBag False Passed
ad47f0a63bd6cb03c8d970c6c10efed46e5ab821 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagUnion True Passed
379b2509cfac85de5bf80faf7c9537ef8b74e09d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagUnion False Passed
7b80498de02c943a5975477948258984c9ce6713 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagCardinality True Passed
973363af56eab48fc38bfc7a4cedd553d5d16602 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagCardinality False Passed
d3604fb7e322bf6248f930560b2a591264ae6699 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagOfAll True Passed
1c228b9859ee618d50c7343fab96bf0d1882f49a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagOfAll False Passed
92825c400223f3a8225857d85fe1ea3cdce57e51 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef2 BagSubBag True Passed
701912fe40c82080471de25f3dbc2a89c17362da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef2 BagSubBag False Passed
64d67e20ff7b7dcc6e872dd0c80bde5586c79f33 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)
LetDef2 FiniteSetsIsFiniteSet True Passed
460e25212e66a92068de11a67f600cbf5ab8636b 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)
LetDef2 FiniteSetsIsFiniteSet False Passed
654364a0ae52f7fadafc400bdeeb7cb1a4859d53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FiniteSetsCardinality True Passed
f8e16d66a2b968fe89e42f584d643b52ce697450 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FiniteSetsCardinality False Passed
7d76e38f6aca67af7868094b77d94c2bc06a5ab7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqHead True Passed
2dc1bfa406e1cc195c9bceae8b76ae9bbdbac28f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqHead False Passed
c82e2e80d0847fcea6b01b28c5fdfe8afce4d47e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqTail True Passed
4f3af0cb0e5b5e924ee33eabdbe3490a6b228e8b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqTail False Passed
1a45dd82a4dcc3ccb774e30b2d64b5386828577c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqAppend True Passed
f4362461c7aa01e30f36a45187a3118dfb969c64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SeqAppend False Passed