Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
49f9f3a035a7ffec05ab3834d29f97c9d40308bc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFunRecursive OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
b639820b93913ce45b806fde9befb1306884194d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFunRecursive OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
af0b3e223ce0bc2dafe9562d84d1e31a536d0f82 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFunRecursive MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
05c65e46898c090ffe7fed4ab8c972ecb3ad61e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDefFunRecursive MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
e9de9f481b2433a8e9b00db8c0d343e765c5155e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
55db5cd742d62ceaeb94cb760872926ffc46ae05 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
6b34cdab45220875e07bf62d9a5f22ead3d5d389 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
94e4308a2a9c687d599f45613c9488db7eafaccf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
fdb3d7687de6fff1fc0d7cf39b00a22e8ad09aa5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolSet True Passed
  • Model Under Test
  • Equivalent Model
d428c4d152ed04a70ff92b1a6ec5b1695a4277fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolSet False Passed
  • Model Under Test
  • Equivalent Model
3e9299e95b50ddc8078cc2415fa85954141cd524 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive And True Passed
  • Model Under Test
  • Equivalent Model
4830ccb35ade38886203c58ffe3123317d1934f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive And False Passed
  • Model Under Test
  • Equivalent Model
d9194a0ce9b15acb9a77c4c6bfcc7545eeee882a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFunRecursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
c6c01a8d61c63f148e2f182c094f14eb1aa46d36 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFunRecursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4627427b276a201906bff467b87b722224f3270b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Imply True Passed
  • Model Under Test
  • Equivalent Model
86b04cbe0f60fe59d7a47d1dee7c004192ee4065 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Imply False Passed
  • Model Under Test
  • Equivalent Model
51f027a43c1eca3ee281727ed363cd522be9103d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Not True Passed
  • Model Under Test
  • Equivalent Model
b0c0c4251db18faf033e01df75fd521b2ff46c0b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Not False Passed
  • Model Under Test
  • Equivalent Model
104560ede453000a25d30095943297a413a89800 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFunRecursive Or True Passed
  • Model Under Test
  • Equivalent Model
f51504e9e2b6367a6e5626b2b7aa35ec4c2717ed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFunRecursive Or False Passed
  • Model Under Test
  • Equivalent Model
4273a7c24caad81b309e0556ab08d50f0dcda93c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFunRecursive OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6bb109fe149c844157a5eee34dbcd64fa610b43a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFunRecursive OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
0a27db658696b9fcb831955d7ad4ce02d2bc4065 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Eq True Passed
  • Model Under Test
  • Equivalent Model
2c12fff416ee3a3c062ca1f0c41ac462daa8c671 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Eq False Passed
  • Model Under Test
  • Equivalent Model
a3cc69cd868469ea98dbc61d84b42d180d8d6f5c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Ne True Passed
  • Model Under Test
  • Equivalent Model
d12b0fea7ab77feebf5cbd436791c13c27d5f3f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Ne False Passed
  • Model Under Test
  • Equivalent Model
3e41e38a2a44d1c6db6f94536e3a76c052d05ca5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Let True Passed
  • Model Under Test
  • Equivalent Model
51721c754db142855ffb06af3045d45e94a8ecd5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Let False Passed
  • Model Under Test
  • Equivalent Model
87b50a44f5339e5159b82e85702a5a746e5b74d2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
9136af6beaad0ddce818731de74124f3fa340966 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
d038477c3db9b9ff366055f0faba1711da24023f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set0 True Passed
  • Model Under Test
  • Equivalent Model
090e46c391b7d4cadd3f2cc3405740e1754a76bd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set0 False Passed
  • Model Under Test
  • Equivalent Model
e6677a6daf84263adfc8841bd7966cd7552a4f07 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set1 True Passed
  • Model Under Test
  • Equivalent Model
d8dd5eaf6c2cc53188bb5cd67f6e541ba9921f68 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set1 False Passed
  • Model Under Test
  • Equivalent Model
0b011a338e2d8e7f178b463d04e6531a344ed50f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set2 True Passed
  • Model Under Test
  • Equivalent Model
ec02b4ad0621a689541729d26b816f806afbdfdd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set2 False Passed
  • Model Under Test
  • Equivalent Model
d8f69589e0865c6c0dc020c9afde745a3b06346e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Fun True Passed
  • Model Under Test
  • Equivalent Model
9bbb960bc531357601c4679c5741c2a5507f4b04 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Fun False Passed
  • Model Under Test
  • Equivalent Model
27201a4e35c07c7db4379d54a4204e81fd049255 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive In True Passed
  • Model Under Test
  • Equivalent Model
1c5af45cbd53dd13501d697ec06ced9204fcc9e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive In False Passed
  • Model Under Test
  • Equivalent Model
30876f925c466a8861700922bc72796d90234d3a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NotIn True Passed
  • Model Under Test
  • Equivalent Model
8ea36c388e6bd7486b500f016f201b43e7dee0a2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NotIn False Passed
  • Model Under Test
  • Equivalent Model
67cc4d81be11806033702eb1a32832fe860e3dbd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Exists True Passed
  • Model Under Test
  • Equivalent Model
72af27fbd1e56911435d8694fa1e142504e7eb89 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Exists False Passed
  • Model Under Test
  • Equivalent Model
cc9e6ed8175b38a20a60894cc1044220031255ab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Forall True Passed
  • Model Under Test
  • Equivalent Model
3c3b00a5739661b208e47d5854071de439b9818b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Forall False Passed
  • Model Under Test
  • Equivalent Model
7dc9209d46937b07a8f15ab67eac9a7e3ca46b6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Choose True Passed
  • Model Under Test
  • Equivalent Model
89a7413d8308aa052d6f5822e03b3ffa7690fce0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Choose False Passed
  • Model Under Test
  • Equivalent Model
91832baaedd278fca8c3bbd97d90f3a0fa7a3011 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Record True Passed
  • Model Under Test
  • Equivalent Model
c0560f0eb8cacb81c97a9140b8b700691031b7d2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Record False Passed
  • Model Under Test
  • Equivalent Model
358b2b3f078a67d6e0364e1dfca46370294975dd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Tuple True Passed
  • Model Under Test
  • Equivalent Model
4398d9e0c7c46c833a939437bb5fa96502103226 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Tuple False Passed
  • Model Under Test
  • Equivalent Model
45b6049de8b1003d89eee910bee9710b1bc96e0b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
f20f2d736932d05103262ac0603fcf873224170a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
f55f22b22a673f7fe25bf93f148224af808f006e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FunApp True Passed
  • Model Under Test
  • Equivalent Model
ec46b7577f7dddf9735e2d6cdded8f280c51b53f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FunApp False Passed
  • Model Under Test
  • Equivalent Model
dd06a1f777fec3fff02cf257a154ca72f2b33002 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Prime True Passed
  • Model Under Test
  • Equivalent Model
9203b5ffb93499d6bcf5e80f4b184133986f2d79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Prime False Passed
  • Model Under Test
  • Equivalent Model
01d0557657468abe5ed9e70b54903a5a98c67d5c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumZero True Passed
  • Model Under Test
  • Equivalent Model
7f2fa44ef4e8f58384e3c21bdbb7cbdb7e5e434e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumZero False Passed
  • Model Under Test
  • Equivalent Model
1f21e1afe1a44f3fe0302d1330741db7a88d544a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumOne True Passed
  • Model Under Test
  • Equivalent Model
872304384d95c53aa6d738c6bd55ba0582cf5619 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumOne False Passed
  • Model Under Test
  • Equivalent Model
3b2a1688366c7915ea1d762c03b13186d1d9b49d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
300d0875eccab917d0a3f83b4f24ed9e14666861 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
5aa9a203e75d8f28156bccd0fa6afacef65e161b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
0d3a2ac66447516fce708e7d23b97e05c88c4808 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
11b3c4f80b757ff1254daebd8acbedcbd6114eb1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumPlus True Passed
  • Model Under Test
  • Equivalent Model
7635428b7e87ded7734a70f7530950dcbcc5a9dd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumPlus False Passed
  • Model Under Test
  • Equivalent Model
a5e3c57a444e4199672402a2ab4c3a2f6b9778da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
4e5e3622796858d08f71e2281b411e06ca7c256a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6d6205fdf1c52807bd79286be28d026777a54040 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMul True Passed
  • Model Under Test
  • Equivalent Model
b7d40f6c3649e342ec3c06afc263d08c1eb7e1d2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMul False Passed
  • Model Under Test
  • Equivalent Model
b40de0437f1c3d49ded3efbe4796ee512a223c53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumDiv True Passed
  • Model Under Test
  • Equivalent Model
453bb572611113fc3a0ad2ad8ed662db48020e70 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumDiv False Passed
  • Model Under Test
  • Equivalent Model
0b48240428d0dbd4bd9d008b542907312ec1ab01 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMod True Passed
  • Model Under Test
  • Equivalent Model
a45e1d1b3627c8b5f466997eb426e66fe4883cd8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMod False Passed
  • Model Under Test
  • Equivalent Model
ace2f13b8b32e6235384ba4d62b11c805bedb273 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumPow True Passed
  • Model Under Test
  • Equivalent Model
63c25760d96dbff4a7ee75b3c4b2fa89cedf9ef6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumPow False Passed
  • Model Under Test
  • Equivalent Model
a6bcc37cad21138805723c6f3c812fdf0e481504 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
f553a591aebec9285c3eba8fab45c523eddf3aab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
4a5f09f7410ece3cae2e4e950a5b5e11b81c88b5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
00417c2cf8b66228a58b430921259b32727a9c44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
6b0176f387433f963e7c3ff9dd9c116cb28a2886 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumLt True Passed
  • Model Under Test
  • Equivalent Model
fa7800b2cd7cf11b4d88936e29edd78aa861f7d9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumLt False Passed
  • Model Under Test
  • Equivalent Model
2db862c4cf9018381116fa71ef72da4914123201 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumLe True Passed
  • Model Under Test
  • Equivalent Model
659b20b00a47a642a9ba1633a710f50eec318814 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumLe False Passed
  • Model Under Test
  • Equivalent Model
794fe50f78ba3c5c0b6250bbcd6cfeb4c84aff4f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive DefFun True Passed
  • Model Under Test
  • Equivalent Model
d45e511a076576fd7fad9e9a24d82a53f6e154b8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive DefFun False Passed
  • Model Under Test
  • Equivalent Model
4d236a7c8155bd39e2c4a14cdb164bb1b3139d2a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
ed7d9f70314ca05e43d01bdaea269f6e01bb6b93 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
f050d95ad4433564ac80fa502efe4db218623a5b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
c4e627bcc5f4eaa9a8d5455fe363167658d84512 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
37cfb9f383f89e8ed9d09ef39d9bf2ec85c7b742 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
05abaf478fa8966fad981158fe47677d7b2d3282 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
0211a733c7842fb4b6b7bbf62e9b967fb09b7bba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def0 True Passed
  • Model Under Test
  • Equivalent Model
065eae54f26810d8aa413424dd0d76af11c7744b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def0 False Passed
  • Model Under Test
  • Equivalent Model
02a2b5a44178ac4c68941fae50ed6a9351a202c5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
c1b25ac230bce711efdb2063005af94e3f42883e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
50f125c4fe2ddf37dc9769c626a069d7bdc0d315 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def1 True Passed
  • Model Under Test
  • Equivalent Model
d0538aab23e58c6b08158d4102feb8a9b556a2f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def1 False Passed
  • Model Under Test
  • Equivalent Model
a37c7b18849cbab802e58467f94f9c2a038c8630 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
9b19e03b9f880ba8129a93df21c640328a3375ff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
f1c27695092f2e035980c9e6bee4dc3b759089f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def2 True Passed
  • Model Under Test
  • Equivalent Model
bb2b24cd74dee514659de57a3d19730a2007576b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def2 False Passed
  • Model Under Test
  • Equivalent Model
6a716e31435de57d44f1e9b9e4da095d1eaa5cea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
2c95782f8d7c9983af422c833a725220784ca2bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
ae2b741ff82977eca4ca857aac6fcf873cfe08b6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1aae3ab6d7eae1534bad7ade24d5a73dbfada0d6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b6f5f3b96f22f9f8a24f64be0487b2a8eb42cc75 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
5f0e7f8e8bae71787a58cdd8491d96bdb75f328b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0146673d2b505e3ef79e7fbfbff1d2389aa524f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Extends True Passed
  • Model Under Test
  • Equivalent Model
1bfaf8ee13bcbf1deb222e63baf799d753f5eafd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Extends False Passed
  • Model Under Test
  • Equivalent Model
e650e41b81d7993a2e5ac8e037cb39510b04147a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
28bbae232a43987c6541b6d8b545665e68fc9329 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
d7680b1ef0f372319eac4394a745197c786b0374 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Variable True Passed
  • Model Under Test
  • Equivalent Model
8813b9f4b5fc345e606e0c6dec0357cf83cee3f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Variable False Passed
  • Model Under Test
  • Equivalent Model
7097dd1f25ed2b403f4b710b3b5653fd8b8b2e25 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Constant True Passed
  • Model Under Test
  • Equivalent Model
03cb836786ec57cf178a6dc3dcc14dfe1e528801 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Constant False Passed
  • Model Under Test
  • Equivalent Model
be74da9984dae1663adeaa7be7bdce8040f4707d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
17a63fd6e6ff5ed8507d45c6a723855c6427b74f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
ea3e1d9b1d4c6e612083a9148bc2a34287534bf4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
66142f6879248950669978c9f726617c55e0537f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b9e81cf83e40b61d6a3b92e5a17e5f9b61c3b93b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Instance True Passed
  • Model Under Test
  • Equivalent Model
bb072ef5b0ab160445192137b1031443d876764e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Instance False Passed
  • Model Under Test
  • Equivalent Model
32deb89df0224bd94cb979336bbba8043d577ca9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
39f59b22675cbd7bc1f6b4f9cfa6d6bb2d4f9fb5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
f076b455248395d563c0a555d02c38559a4d9a81 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
f62a998da5003190cfdc34c27dbee8b288f031e6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
08491c511895c87a43c331b323e34d503de23f52 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
76660961b16756c460fc92173acc79cf415143af TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
0377d73f5c36f73418dee46cf1824ed7bdd90f53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
811b7c4c596e1ea3851dcee445d7c557c4f0ad6e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
4a3164409ca62ab8f808638588657fb6e1020069 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6cdbaf32bd9c26581801e22c54aee1653c0859ed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
7464c896e1f0775716617fb343b18e0f000ec538 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
b5eb8714ec57987c03a7e1a35b08af66e6f57df9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
88ffc75a8d8057289ae897a2ec56e2ae7cd922d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
96bfe33fc38b18511d5b6dc8bd2ee8a2ad0c1efe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
7eaf4de68d372fdf273dd426239399c19bb6436e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Enabled True Passed
  • Model Under Test
  • Equivalent Model
e3f6b119c5af76afc448f6bb40b3d796b84343cc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Enabled False Passed
  • Model Under Test
  • Equivalent Model
c10ebf7b76047473ae694a9561d168485d4224fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
47ccec197734a29ceb3aaa53680e2b96d3515350 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
ed66f1a3939bd9f259d40ca77cf1aec394153b74 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross3 True Passed
  • Model Under Test
  • Equivalent Model
260ca7e4a7c1394c1b719e08414878af8c738589 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross3 False Passed
  • Model Under Test
  • Equivalent Model
2b151421f62479e52094db1adcdb00694cbd9234 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))
LetDefFunRecursive FunSet True Passed
  • Model Under Test
  • Equivalent Model
84fc592f4d9204b3f953f432e1b6f57809f10b62 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))
LetDefFunRecursive FunSet False Passed
  • Model Under Test
  • Equivalent Model
753ae0485c7aa97298d16c3bf6ef26e7f17c136c 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)
LetDefFunRecursive RecordSet True Passed
  • Model Under Test
  • Equivalent Model
7ee56ed08ad878d6d1516c47823568d2ea0e1565 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)
LetDefFunRecursive RecordSet False Passed
  • Model Under Test
  • Equivalent Model
948e258b0ac2cf1d578e8aff05a6caafc21c97c6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetDiff True Passed
  • Model Under Test
  • Equivalent Model
6e5f8d63f544ad01f436c6dd049db070f6c6220c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetDiff False Passed
  • Model Under Test
  • Equivalent Model
360c7d7b254ed789c4f5ee8c96ca0eff2c65fd44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetUnion True Passed
  • Model Under Test
  • Equivalent Model
95cfde5f3cd28bc778f36c80d9788d640303227c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetUnion False Passed
  • Model Under Test
  • Equivalent Model
659e7e609d6d7b60e3d06fbc5933f4bed1123ca7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
4e2887604beadd6d40e3f52b445396635ff512d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
334094e853d8240f092b30d0b5ee61e2d9077aff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
0a9f3c9ed2ebf74569c29c29fdf9d5a9d899edb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
0ad789fc9ab9c4a57b193e8042b6460b75851446 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfCond True Passed
  • Model Under Test
  • Equivalent Model
2a7614a708b23fb033bf1d6ab8d1f24fc7b7455b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfCond False Passed
  • Model Under Test
  • Equivalent Model
df1ec8f1fe8aa2f833d85b29c41f384d1c1b8800 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfThen True Passed
  • Model Under Test
  • Equivalent Model
0cde363a24f070859b353f99458ad78ce27ccf1e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfThen False Passed
  • Model Under Test
  • Equivalent Model
55c80016d2d61051186e857ef9216cadc3e35d03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfElse True Passed
  • Model Under Test
  • Equivalent Model
53d20d3a82c2a23f9b76375f9b7bd6a16bd9cf9b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfElse False Passed
  • Model Under Test
  • Equivalent Model
80c0044f1466c51178dd02f4658770a2b1557075 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Subset True Passed
  • Model Under Test
  • Equivalent Model
36924ecf4ed614465d21a6d2c3e29dadb5fbae6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Subset False Passed
  • Model Under Test
  • Equivalent Model
f863172f48c80e975c8a02736c400ef1193ff7a6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Domain True Passed
  • Model Under Test
  • Equivalent Model
bd38558edd993e6ef5ce830e706947627350ab0e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Domain False Passed
  • Model Under Test
  • Equivalent Model
e82388bee8e5b34dea0a914f2bbe7a1de1483037 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Union True Passed
  • Model Under Test
  • Equivalent Model
965cb251409aacae42cb36fbddaacc0a58f274dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Union False Passed
  • Model Under Test
  • Equivalent Model
f387690ca3f73ef2bb6d6f211b5c1228d7c06004 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5e9c10fd09d4bffad98cff453d0c48f0b12dda34 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
e582103006f9e9d7ab642902bf8d1b5f2aa83291 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Equivalence True Passed
  • Model Under Test
  • Equivalent Model
5f7091de24c9076d29df55f3021e23e443e9e759 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Equivalence False Passed
  • Model Under Test
  • Equivalent Model
33f41b2874faca6f5f2944e63b970ab538fe132d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
02639a4094a0913172b0fd5dded811ac3be4b7b9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
b07c6e4dbfb85716806df7205753792080b38a8d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive String True Passed
  • Model Under Test
  • Equivalent Model
a453f243910a104a4d4a6532ea52cf2cb135de8d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive String False Passed
  • Model Under Test
  • Equivalent Model
b34fd5b3dc659702f083e4522d42737022194373 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqLen True Passed
  • Model Under Test
  • Equivalent Model
0cb269d2e55f87e41c5958440a7b0e0bdf7bcb94 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqLen False Passed
  • Model Under Test
  • Equivalent Model
d83558b77d7c3fa19ee8d209ced10b73ba75cdd1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
74e7e9e87abb9f9516a9a07757a7edf56f86ec23 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
b60863e8fa523f6bb3019189fc7cf9c5ed7f49e6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
8ffd89fe74c97ea3dc3206c17a0b38a3443d4c58 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
65fe7eb6aaa96e1bb7382c5b550cf298fed4f9be TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
2074e5159df30e86682d9c224dec923284946ffc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
fe5c9af7c3b32c9b5f26ac780dbda4c5606f586a 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
LetDefFunRecursive NumRange True Passed
  • Model Under Test
  • Equivalent Model
0852698edff567831613c068222bc363842a1bff 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
LetDefFunRecursive NumRange False Passed
  • Model Under Test
  • Equivalent Model
f6cce6c47c7b6c27e41e43673d3643054ad52578 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]
LetDefFunRecursive TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
39ff253469698f57f043a11b6c16a44da6d94efa 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]
LetDefFunRecursive TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
7dbaa760d38cfb235210b0a12e7eddfcf49a8caa 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]]
LetDefFunRecursive TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
0b95f5480b59defc4698d9ad90af88f3cde4ca38 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]]
LetDefFunRecursive TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
97bbb16a1e72321f8d26ecfc130b75814f6a6277 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 }
LetDefFunRecursive TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
98f32334b6a55d95e2a002f803fd82d7e45b4a02 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 }
LetDefFunRecursive TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
d578807a491ab58547ea86c892f3e0d778691b31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFunRecursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
d120424d04a6cafbfa74e4dd9aac90d70f077ec2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFunRecursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
f59dbe1407f706c21e9e3db41108a8f1cdb46bf5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFunRecursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3c6b206a638adbfdd2e1334888d3a1a57b57368c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFunRecursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
1302d9fdc6b08f3f1c1f3db20612e8ccb1136ecf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
6330ff032a8b5746e5ec45c3e0a936ce5cfdcd67 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
f9ea2cc1120ca25ca74fb09dd58844b5f469d6ba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
bf12185be0eb650d2cdf4849ca22d663a6cc11d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
1b0a5b63477d165c3b36c50259259523a36b6d65 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
9577baf162353e005fb70156b3c0eaf2672aafc8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
b59669bb5602bc293eca2b94e6191649a86ecbb5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
383a8a8f9067b3747ad4a7f2df97da4a1bab0ec6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
9e57dccfe1ca67b129cdd031f7c3bc1b4bf4f209 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
f96b8674bb4c4a28710bf6251411d0e7c7deb509 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
7c58e70766a02a7eef340bf2510f1cf830c361cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
ffb98226156e20acce930f2f5535b27e8e726e03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
94810192e8e5d7f6804a2acbfa70d97e69728798 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
1e28c6e194df4a344ba5fbba96339e3f2c791f16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
184d8afdb643014e9019d52c3680f668cb424dfb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
bce2e29c1aa85ce83a4297667f20c6c3df2f2984 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
9ea01c0fc2e540fd38e30194fa6a0fe9477c5088 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
a4f9aac4ae8f6f0c30424ae7195883edbe06eab7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
34c33b5fc3ba79672541989d8b9a7a457f33c514 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
874f366514ad453aa4499d5b90cb26f7246fc009 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
b9856ff0433d8073e624da43499051f277b4b5d9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
c0a150b689e0086c61140fd137c602c488a4e83e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
53435144d8f31bf43eb60ea34ccd761b5b76c526 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFunRecursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
8d3a78fe512601a56829c4b10605f43540194672 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFunRecursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
d879faae771d1872432a468a0ed8832a267ab991 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)
LetDefFunRecursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
d4c7732d97003f9ceaf897563c3a8017ff8ce519 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)
LetDefFunRecursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
fa23b8d9d2178853d57b5ee67ce88a137162c467 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
358d8a75c7c4117f02fdf74520e9509b7902b81b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
39a7d965b5f6359eb99145c4fe888d2527b1a759 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqHead True Passed
  • Model Under Test
  • Equivalent Model
52f787c447fdbdf0ddde27757ee0bf178d2eb229 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqHead False Passed
  • Model Under Test
  • Equivalent Model
2f8ba48e4c239d1cd5d6b4999a3437d9b6ddd2ff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqTail True Passed
  • Model Under Test
  • Equivalent Model
5bd09c68835c7af7cbf47727cf3602bda75070df TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqTail False Passed
  • Model Under Test
  • Equivalent Model
5bb7c90fbce016b85bf6fcaef996fd35f35963dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
b3a91c500258012fc9ddb7f9fa1a6855f6802479 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SeqAppend False Passed
  • Model Under Test
  • Equivalent Model