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 case feature LetDef1Recursive; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
0b828af929a25386f622160062344c3009012aac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1Recursive OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
bd6b73e8b6f81e3f65e6eccf85535bcbd51c5cb9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1Recursive OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
2169d0767bb8dd6326db147b0da5d4c4a740ac98 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1Recursive MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
6f196569a8f7e11318040de7613e7be52caf915e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Replace spec with the same without comments
LetDef1Recursive MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
f4df125aa34bc6d0cb1a7a5e36425f946056df55 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
d541d0473e8a1e8e043157fa880f16f359a70432 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
4013ae863ca032ece376e70359a4f4f592230971 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
2ca4ed7d3caa9dd3d123a41c83156d9b21cf1ca3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
21ed6869b8aaacea81087bc77487576a32e4cef0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolSet True Passed
  • Model Under Test
  • Equivalent Model
fd14f14bddfb11670df89654f93006f4df1db2cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolSet False Passed
  • Model Under Test
  • Equivalent Model
1221c2a5ea9dbed26287934a55d72bc107e6dad4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive And True Passed
  • Model Under Test
  • Equivalent Model
87b1def3d0f481aa94e324083e9b15ba227064ba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive And False Passed
  • Model Under Test
  • Equivalent Model
57207de06f836a0b47e13c2f099fc3df7378f36b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1Recursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
424e047d11abbc51b5aa80c5ccf8cc246e2f317f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1Recursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
f36409ac0bba10cdddb5619228ffe17fdcf077d4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Imply True Passed
  • Model Under Test
  • Equivalent Model
c06bb656722a5110644ece8acd806995b84223f2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Imply False Passed
  • Model Under Test
  • Equivalent Model
3885c60a8893f4465b40f3560fe20a607078de8c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Not True Passed
  • Model Under Test
  • Equivalent Model
3ed3a088d637883546414ab9556d0e67cfd9dc47 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Not False Passed
  • Model Under Test
  • Equivalent Model
5229ac0530ee08c89f9f31bc4fbdb3a19f6dd3a7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1Recursive Or True Passed
  • Model Under Test
  • Equivalent Model
8d55ec711a98eafc8994acdc95c541ff17ac430e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1Recursive Or False Passed
  • Model Under Test
  • Equivalent Model
6221d2716e4a1d64f000a96c4f00717f5dcd8141 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1Recursive OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9a3efb75397dda07d41ab2abfe3fa620570358d2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1Recursive OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7936dc0163ca8acc7cd24400d82b8144ef707045 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive AndProp True Passed
  • Model Under Test
  • Equivalent Model
d58f4527f158c2200eb3692a4b27b94d815fb765 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive AndProp False Passed
  • Model Under Test
  • Equivalent Model
75f83294cead81b6012d98ea4142802f78b15106 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Boxed True Passed
  • Model Under Test
  • Equivalent Model
3b978ee554c9c5e9c8158e0e67df45ea398b4fa9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Boxed False Passed
  • Model Under Test
  • Equivalent Model
e0d2a8701894a8df9b268a0ac9b73be9de172113 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Eq True Passed
  • Model Under Test
  • Equivalent Model
92d4cbb068530c5aac68c18449762b7558d8ec37 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Eq False Passed
  • Model Under Test
  • Equivalent Model
8bf0bd2368a706195650d41587bb9c1c08ae1282 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Ne True Passed
  • Model Under Test
  • Equivalent Model
da7a8f88918852b7096ef1e1a853e68eef105c40 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Ne False Passed
  • Model Under Test
  • Equivalent Model
035a2d72df1331553632c0ca7d14552e53e69756 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Let True Passed
  • Model Under Test
  • Equivalent Model
a68be952a827fa04ba1a3d193a98d52477ba0eef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Let False Passed
  • Model Under Test
  • Equivalent Model
294d8cc5a8b19ccd5a1ddd4229f77d8344744ebd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
14ee63949a6e939a56702ad5506e55d06cbb506c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
8f009ce4d816f7dcde91a7f401a65a0a7ca37108 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set0 True Passed
  • Model Under Test
  • Equivalent Model
e5a2b5e27a004ec66a74451f663b188556b4f830 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set0 False Passed
  • Model Under Test
  • Equivalent Model
22a3194ae05907c352350f00a1be68e38da93bef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set1 True Passed
  • Model Under Test
  • Equivalent Model
d74e3b88c4a1cf9e84c6b819f6e70b95aa86656f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set1 False Passed
  • Model Under Test
  • Equivalent Model
9171ab6dc630406d3430a08efd65023e54dc597a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set2 True Passed
  • Model Under Test
  • Equivalent Model
750a3ca21679a74c5964a3bec229e323f3cec4b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set2 False Passed
  • Model Under Test
  • Equivalent Model
4457b72f5ad648e8ee53df9ec43e74013cd6dfaa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Fun True Passed
  • Model Under Test
  • Equivalent Model
646e80a1d55dc2b0d8e138fb9ea54d469623e07b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Fun False Passed
  • Model Under Test
  • Equivalent Model
4d499529bf560c032fee4f409bbd1a027485de43 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive In True Passed
  • Model Under Test
  • Equivalent Model
bb0147efa47f826a6cb7bb82bfb6928dd91b20d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive In False Passed
  • Model Under Test
  • Equivalent Model
bf56f702929b95385cbf4e28749feab4a0e76da4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NotIn True Passed
  • Model Under Test
  • Equivalent Model
276908096f141af336fa1749ec20a4f5a5b487e8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NotIn False Passed
  • Model Under Test
  • Equivalent Model
eb301ccfb8e602582016182acbbb81e7f48a56d9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Exists True Passed
  • Model Under Test
  • Equivalent Model
0926f5562d9edc3b3abe4c84d5c2bbbbc8c42ce7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Exists False Passed
  • Model Under Test
  • Equivalent Model
5585483ff41295925ffbbd3e91170eaaccad2ce9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Forall True Passed
  • Model Under Test
  • Equivalent Model
e886ad9b76a0592f33038b010ef5677d2efab775 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Forall False Passed
  • Model Under Test
  • Equivalent Model
8e656fe944b08d165cf3eed98676367bcd332781 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Choose True Passed
  • Model Under Test
  • Equivalent Model
0ef047e5dc1718fb44f23a949863452810071408 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Choose False Passed
  • Model Under Test
  • Equivalent Model
1f37d0a849181d78448c52e8debec40024565c9a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Record True Passed
  • Model Under Test
  • Equivalent Model
f7a24e8971e7edeadd50da6234d3aee9204ee108 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Record False Passed
  • Model Under Test
  • Equivalent Model
da0aef7078bdcb8d90fd7ced110c010fc453db01 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Tuple True Passed
  • Model Under Test
  • Equivalent Model
8121e53f07f3cb6738ee1ff80eb8454ad040f870 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Tuple False Passed
  • Model Under Test
  • Equivalent Model
f67d54ea054081fe06fc319f017c3f2fe8b82e2e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
f29e3ace815e581ad572a83e2fd9359124fd85fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
7d427b6f4e7587a3a2534381e016ba222f1734ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FunApp True Passed
  • Model Under Test
  • Equivalent Model
7eef74d9bda63b2ae416625acd217527600421a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FunApp False Passed
  • Model Under Test
  • Equivalent Model
995b80b0c0e44397fc5237a5f3a119262e5f2217 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Prime True Passed
  • Model Under Test
  • Equivalent Model
e3c582dfc01f60a19fa710b1ec871eb60125ea44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Prime False Passed
  • Model Under Test
  • Equivalent Model
e507ef90b024b2570826f642f9ff01dd5970b3ba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumZero True Passed
  • Model Under Test
  • Equivalent Model
0febed50cc6a42144e74e78a4962d43a2cde89c9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumZero False Passed
  • Model Under Test
  • Equivalent Model
d3a4b6b657a4a51d2bdbb577094a806343f1b7ae TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumOne True Passed
  • Model Under Test
  • Equivalent Model
3afbd2d8cce19af444691f20118605c7ca6662b2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumOne False Passed
  • Model Under Test
  • Equivalent Model
7a62d4be39ec38ea11ca27de92325548870591ef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
38f315392e0ec9fc18a59a0be5be4564dc00b9d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
1a69cdd34f5e4ef83370d9e6da0effa0ad8097ca TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
b5fcb2932903ab618ed95f9cde1b32f187eb83a0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
3386b4c6cab4727df8cc437f9981eecd2d6634a7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumPlus True Passed
  • Model Under Test
  • Equivalent Model
12599a834d5237448eff5529cc0053bf98ab81de TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumPlus False Passed
  • Model Under Test
  • Equivalent Model
c7611e99006ef9ebf54b41f79fc704064c37604b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
475b719db7997604076be7578c6eb37b2f886e4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
8eca6472a16e6b813ce529db878f1b7f182c61b7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMul True Passed
  • Model Under Test
  • Equivalent Model
264155a4fd9f55516c66afa5497dd40394259db0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMul False Passed
  • Model Under Test
  • Equivalent Model
a4cce67713a44ae3febd7180015aec85b5d1d639 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumDiv True Passed
  • Model Under Test
  • Equivalent Model
a705691e3ffe0d9fb1b114f5706bf43d682b9ffc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumDiv False Passed
  • Model Under Test
  • Equivalent Model
192233088a514a668d607af0480b65622911e9f8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMod True Passed
  • Model Under Test
  • Equivalent Model
36249ac6528232baf913df8bbe99354625c738ba TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMod False Passed
  • Model Under Test
  • Equivalent Model
c50a8bee5f81b519395aaa420ce20b7bbe9fc941 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumPow True Passed
  • Model Under Test
  • Equivalent Model
207dbf764b33f73042ba0336f034425bc2a6f74d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumPow False Passed
  • Model Under Test
  • Equivalent Model
ea0b2a8ad79a74ca8645c57ac65afab14786878a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
7f44cc0ea0cdc5ff52a02fbfe04e70195e02eaa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
b3e807548f5666a765cea5fa2439730b14992763 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
c302fc49cca0cbaa3dedda800ba56951806e0479 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
cb3b347fd49b06289f6b14d310237cbbf839675d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumLt True Passed
  • Model Under Test
  • Equivalent Model
3b888ffd6f7e2922a53a8e7c12faf5efc27a9a3a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumLt False Passed
  • Model Under Test
  • Equivalent Model
026c67d1738c65e1ead1223602ac1aff7d16a1e7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumLe True Passed
  • Model Under Test
  • Equivalent Model
4e024918c4878a7226bd1324301a376700513864 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumLe False Passed
  • Model Under Test
  • Equivalent Model
86468b5c0e17658ce3fef2875bf771ec228275c6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive DefFun True Passed
  • Model Under Test
  • Equivalent Model
9722036c2480f9143359c16f2669d412243854cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive DefFun False Passed
  • Model Under Test
  • Equivalent Model
ab0a46e59bf8e9c55a66cd87079a8aba0e49aa79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4c09405b9aacd22f049b112ddabede8fceaeef32 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
3b02b3aa92db45e49e354d19e3eeedcfae9398d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
e0fbdc38d36ef0a4d99a5f83c3e0981bfbe0a109 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
bdedbba7b98bfe5a0618c350a11a5f7a4a36079a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
85525b09af65357fa9fd53e70831ef2c61451fa2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
c067b608c54a1fe743e6d50f28e58cfd28c2fd3f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def0 True Passed
  • Model Under Test
  • Equivalent Model
af14a17fa5d25957c978e102f54d0f680d1422b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def0 False Passed
  • Model Under Test
  • Equivalent Model
7b4d4033c17326a4a9cd5a669e765fe901dabd5d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3eb7488e93ecfdeedd03b70afa78ba27fe3ba308 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
f096f3995eb65e606d2b81ae98eeac87e251e4d4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def1 True Passed
  • Model Under Test
  • Equivalent Model
14a49b6c622f317fa94bef33bb4d25b7001c95f2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def1 False Passed
  • Model Under Test
  • Equivalent Model
9a64b5a921b9e44ca397d9d16719e19f8b5644f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
8a609081ff574032d1ce1a3fa18784e4ff6bcb64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
2d85bd2021b52055c86c05d85f14f46d1a63586e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def2 True Passed
  • Model Under Test
  • Equivalent Model
05dae5c86c0065b1a51a69472b8a31a4e61e4551 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def2 False Passed
  • Model Under Test
  • Equivalent Model
328e27fb12bf28cebb73f7ad3ad58bcebccb0fc3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
d98a3514eb62b4235f1908cb23df09e9023d4735 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
b759100cbf91d767d81d06f523c6696384207514 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ae723c42aacab051d1fc7efdc38c11b9951c0f67 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
1d0cfb70fddc566f6cf6013d1fa78c3a7678a4c1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
fa7d3eb1af45f6781eca0663058d505c0d153291 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
677da16c7d2d96661306f6eaea472ec12dea3985 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Extends True Passed
  • Model Under Test
  • Equivalent Model
47574bd665babdf147c5fe1b48732f316bb5e761 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Extends False Passed
  • Model Under Test
  • Equivalent Model
ca310d746170e3d2b481a32d0f59d34cc780c3d0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d9cfd396e5e1cc08d09bf7ba5c0ca03903ace31e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
18c1d2adca6b1e0362ab439ba4bc17d8b5553b91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Variable True Passed
  • Model Under Test
  • Equivalent Model
8f0e2a44f9358407a07b18b91a502cdd1192efe3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Variable False Passed
  • Model Under Test
  • Equivalent Model
16ba014d8a4d4d24bfecfd7ae3ff98790189e04d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Constant True Passed
  • Model Under Test
  • Equivalent Model
2797d02a3553fe5e834bfcad48e53f1c00a99906 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Constant False Passed
  • Model Under Test
  • Equivalent Model
3f69a4187db2bd8c662cc23297d1ba723f33b48f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
824f0196de385fe651e42d54087d49f574c0eea9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
709d35b6464a209e966586b6bb5c86fc58c18eb1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
bd0c3a2bf69b32f5109819f6ec6289ac35a26a66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4661403ca15c277778ff54722a7fe82819c3243a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Instance True Passed
  • Model Under Test
  • Equivalent Model
ed7c8a37f5df9dd1afa8a409cf6b07e2db40bc8d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Instance False Passed
  • Model Under Test
  • Equivalent Model
330e983de7325be96854b844fc2b500ba49f166f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
fea5b26c2ab4291597b9fad19f083432aad1de19 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
f383334fcdc7761f454062c44fe5d92512a24dae TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
79650477c5bc90e01f7f08363220061ea691e850 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
4ae1c7c0cddf7a812780eb931ce8da6d1d38851f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
c0933bb39ac31352bda6efd7e3554df53c1c4073 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
c659ccb9f1843cee91cb020ef7fa00105fe4e1c0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
d3a81407792dd11e3915e4128e3472636cfb7040 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
bb6646bc7f16c052e8e115fcbf7c16d495065543 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7731e6382f59e572332f4dc4d82448491b43b5d1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8971f8b5e0f6164d00df84b82a32981dc36cd572 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
4ba3ea3718242345d3bd9395f72904a08ba6e1ee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
22a86ef1c46d56f4c3e61d80208f4b68720b489a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
863dcd8a42b04bac34f4947e4688675ab478d59c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9995b806be2568520bafd36719c1fbfa2b62bf8b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Enabled True Passed
  • Model Under Test
  • Equivalent Model
00441b3fbc8e1e574302d5a2df7fe373a61094bd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Enabled False Passed
  • Model Under Test
  • Equivalent Model
13f774636da960903c9c323c15f1da13e1e674ce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
6a750dd22e60119ddd0469d7cd5ee0b5f32bbef4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
1f0660a88e7d40798f212a3efbc7a5e97c96aef6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross3 True Passed
  • Model Under Test
  • Equivalent Model
75c3667ff4649995b641fb4fc5ca35b748990e8c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross3 False Passed
  • Model Under Test
  • Equivalent Model
5f9c31e44b7599af2061091b4720ef8ff5ae9bb4 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))
LetDef1Recursive FunSet True Passed
  • Model Under Test
  • Equivalent Model
4756206c9971cde3aabe16628477cf76bc5eba56 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))
LetDef1Recursive FunSet False Passed
  • Model Under Test
  • Equivalent Model
cba15d2cc3017573ced4e30b85ffbcbca9956e1d 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)
LetDef1Recursive RecordSet True Passed
  • Model Under Test
  • Equivalent Model
f1d80ab16d399cca45153f16df0481b937d610d1 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)
LetDef1Recursive RecordSet False Passed
  • Model Under Test
  • Equivalent Model
014316ce4ddd69dfa40c8d69bf1e757b7575c64a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetDiff True Passed
  • Model Under Test
  • Equivalent Model
9412c5b4eca3a43d61f639fc7dcf0634fd505df0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetDiff False Passed
  • Model Under Test
  • Equivalent Model
f5d7704224b131d8c7aa9bc686ba012b71f9a24c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetUnion True Passed
  • Model Under Test
  • Equivalent Model
df97fd47af8d87b84eb2d698d64dff55d848bf56 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetUnion False Passed
  • Model Under Test
  • Equivalent Model
8cf06580be52a00facd6d5f2333d6f2053456125 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
1747e3cf5547d998968fa2276e26da30ec144836 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
eb9e79071ff8f654ab89584c49451f757ef360d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
4d6497ba28223bd4ac4bc664036456c61a28e011 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
25fb96c3a788fa7905eeb0c1d97c3d2c8e8e34d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfCond True Passed
  • Model Under Test
  • Equivalent Model
fb42309104dccd73835b3812b44e779f4096c892 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfCond False Passed
  • Model Under Test
  • Equivalent Model
cf44f25309ad26580ae9c26325e54b38b0cb1c25 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfThen True Passed
  • Model Under Test
  • Equivalent Model
8578d611ef5ceb4391fd967fc23619596abcf9bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfThen False Passed
  • Model Under Test
  • Equivalent Model
be208ee4b8e6f45180b862bb9a286d28f1e58679 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfElse True Passed
  • Model Under Test
  • Equivalent Model
6966821ef3182c34396ce3299470a33b566fc834 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfElse False Passed
  • Model Under Test
  • Equivalent Model
bc8311c59b6d5f9402c77ed7f4a4aa0e53b3a360 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Subset True Passed
  • Model Under Test
  • Equivalent Model
e570f762b76893627f7fbf7f36522e8a4168ebfc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Subset False Passed
  • Model Under Test
  • Equivalent Model
13caea5255d0230fcc3ac37d92467ae421077620 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Domain True Passed
  • Model Under Test
  • Equivalent Model
c919b3362de97a5c35def5f0d87ae60f42568fff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Domain False Passed
  • Model Under Test
  • Equivalent Model
5438966b6a7145bca5dbce5b1a2408a52ebf9933 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Union True Passed
  • Model Under Test
  • Equivalent Model
565ad03d2d8612b1fdc08e392b58a5bcb58237cd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Union False Passed
  • Model Under Test
  • Equivalent Model
04f4c9102c930ba6d65c3043e3af24eed88e1f92 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
058225963d808c1bd7e6b29571f36560740bd042 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
2d3f5c7dbcd0305b978ad717cd54d492cc160ded TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Equivalence True Passed
  • Model Under Test
  • Equivalent Model
bf39d7ced6b4b262e7aacf02255c59eade9de420 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Equivalence False Passed
  • Model Under Test
  • Equivalent Model
87f25c2c42b2a6621e3d52d39ff32b7bde8a1e8c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
3da03d388bff596149c99b40977fb36c8ded4b3f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
3fc67d95af17798a7b9885a9bfdbe2d31523ab37 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive String True Passed
  • Model Under Test
  • Equivalent Model
033146f5c9d36457283c8d7cdb889066b86b0c91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive String False Passed
  • Model Under Test
  • Equivalent Model
9bae6e5067e25d8c6feff240840a4bdc6fe62006 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqLen True Passed
  • Model Under Test
  • Equivalent Model
ebb79db7fa92c3ff553763100fb7e9681ef153f7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqLen False Passed
  • Model Under Test
  • Equivalent Model
dbe0ac354ab243ae7aa2f5b60b4a3127ab8dbd32 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
7a2e0101226923838324d59553c932ece817e269 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
8f4fa34b514e94975382642bd058b942844c0d28 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
6cb4f4f2b337e7056421b7b686dd959cea54b869 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
8e03142d2cccf1eb29b9a8d8d26b0d01e68e2c67 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
fa30e12bfdb1b3320b721460d28299c3eed702fc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
d5ebfe1a297a23807572727a4173193e527dba91 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
LetDef1Recursive NumRange True Passed
  • Model Under Test
  • Equivalent Model
5be3af0cfce25265f6a3c64f03a1fda33f39505d 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
LetDef1Recursive NumRange False Passed
  • Model Under Test
  • Equivalent Model
10ece599fc22127d37ed7fac1c1e25445bacaac2 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]
LetDef1Recursive TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
3f8aa050f862eef6657d5e3942eff0ee3fec6d0c 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]
LetDef1Recursive TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
6229de3c1dad426c7b02b4f253e0555d49c70a83 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]]
LetDef1Recursive TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
1073f5e04816f3caac22307d3c26f8580b0a7f59 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]]
LetDef1Recursive TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
9e6cff00756ba2c5189036463814155db908c221 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 }
LetDef1Recursive TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
6d6a835e1e9ecc4de8e96220708abbd26da6dace 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 }
LetDef1Recursive TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
4288d0e795c7b6274204e70dee53fa781a6e1964 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1Recursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
5f90f48e1cbbe75ce3d4af7a78b2e569699f4130 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1Recursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
22a5a4e3f6802e3744701c8b3b9aff12c5758db3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1Recursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
123855b043aa648504cbd1eb86289ccca4cb0bca TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1Recursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
5c7cdd1115d929c21d1697b3e159fb368f190602 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
058b383ee3fb77f9380d5dd63c072a3b9eda7b0d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
6bae505c6adf40f89a16b0e436d08ccb22e3e8e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
1d0a9dcdc9b696e866e69852c011fa6ea44ccefc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
f5e262eef73a045723e217b5598cda039b34d016 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
cfe40a3e5f821ab5ebfb0616b9ac0d80708bdbcb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
8c820111e377436e7befa455415df632b3a061d4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
28b429e1c81c836dfd7e2b719600094855407224 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
597daf1ebdf2a4d086de9e2c85ce83d7704ba90b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
9adb729733855062b26fdb357db088f7a4fa3da2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
e26306245ccf8481417232b8a94c3465581590de TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
be8cded459350d695d8b78b5ea8edf0f53f44318 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
b1bde81490b89f13af6da695ef5859e22ee61d91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
a66ea9e129c184fad4d814a39e903bdee8117714 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
82971dcab5344f2d953f751c180a86323ea05bf2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
d11c40304edf807e3da857f0292ef0614a0d3a26 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
f973e4ae57f3f78f7a27c3ef9c9b886e64a77768 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
b0a93882cc6e29c5d0c131dd7df6c4b087e4f44c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
1ad424329aba3b789cfa570d7d79b441b0cf347a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
a673fd9de319b65d9a063ebfc3692418586c9341 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
48c1edd28c9bb3d0677875cff3188c81ec47778d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
3a8c5f07514191dfefe7b629ef05a31e84f148aa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
2408092993c01d3e8ebfe7b59814675521c3096c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1Recursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
fcabf2a336d57ea4da87f94926d23f2fedb8594d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1Recursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7a97430dfe863f60d46e81ef335862d660da165a 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)
LetDef1Recursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
c63b43b2ae93a565a5971aca9e2a91bac13f6080 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)
LetDef1Recursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
467e917c37493d3c7b780eea97c4a22b47415de0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
ccf66f81744a6ae2c4b2827b31cdd5ea116e8b5e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
852bf909a8d48261418a09dfb030bdd3388c755a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqHead True Passed
  • Model Under Test
  • Equivalent Model
8dda9eeb05692e93e6e54d57c600bec73b6af96b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqHead False Passed
  • Model Under Test
  • Equivalent Model
51847f603687cfec26c847ece7a0e13b3fd2fb64 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqTail True Passed
  • Model Under Test
  • Equivalent Model
f6f9033deac6d93adcca8d685ccc1bbbebe0e027 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqTail False Passed
  • Model Under Test
  • Equivalent Model
0e3aed9597dabb937c8a912cfbcbc4b1364e6537 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
31079c1aca6a6424a0ed6836160eb604ccf3cda9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SeqAppend False Passed
  • Model Under Test
  • Equivalent Model