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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
70f6c7c8aa1c81fef986a3670d3c04f6af50f868 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1f0815609350a80afa7ec102ad281122de788a7a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
3d4298fd412ce12581e969343e42ef332b2a2b1d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dd203653c9d9872b6bd2c756d0207bfa719cfd13 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
45b5fae61e4db52caeaa1ea6d1566b3dc6649210 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Imply LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
0603158049a4dc7d2c8cc059c717f96f51fab8cc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Imply LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e91b4df138def45e10596847755fc55c36a18851 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ce26be14274d2dfe1c6a83911893482426372bd4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
cb846d55b38685ef3bf8cc9ad319dfad1e249263 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: LET definitions are reduced to global definitions
Or LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
71fdb9fa3cdc1902bbc05840ce7aff485ab3cebc TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: LET definitions are reduced to global definitions
Or LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2ac10ab021cad77847e839a688e6fd3ac9f1ca6f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: LET definitions are reduced to global definitions
OrMultiLine LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1a675a014d2fad3baa3ea8c14bd5f0a93d9005af TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: LET definitions are reduced to global definitions
OrMultiLine LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
8dc6a03fc55c1fc13b8c75071f810adca1dd3047 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AndProp LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6604a14425f5a38b5d9f992e0922cfc5dd2e1458 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AndProp LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0c655edcc503554e218ad77446259f1261a12590 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Boxed LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
0b0e739cec219f80033de3e5a850e0f9078dcf5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Boxed LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fa648f4ee98cd0de590e22ccd5a174525d0fc0b2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d4cf3a84b81d044f80ecdd83156823ec8f581ea8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
406f41b240332193ddb459768c5eb89c5efccf78 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dac5ec4d570530e28a667030e0a4b1836a2d0d87 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
94c76226b33f151c592ccedee097e75a132f9ae7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cd3d2278b223f8f0af72eb151b6eb0e2c300fd8f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
bd358ecf70a2dce3ebb1649a76ccbac0f8464049 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
9101ad73eb98b1030d991cbf5189f753f7d978f7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
7c96bab093953f1cfe0ad5b3482730d6146a9733 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6a5e9f8e23a6136b5016aa4ad7b2d4979e298c11 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
595733b34f9c440a2e6975b85bee5781b9eeb70a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
99900a26c556054f4168ff727ec01afe8a39fcdf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
97025aff69b9a193b96d03e1f1cd9b15c147f848 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
bb3e0c07e2c1292c1ee36ec65bab5a74ce82e4eb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
035181f57e434c5d24528312ae6b98256b0f7362 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
0d6acc2b3e4b54d0c604fffb54057170480b711a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
be1a80a1c92c6f53378edc83870b964a84905b8e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3ee72db16fec0292fce49f5b051a1a1611e01b33 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e66a77b14d21bed3817ff2dd8a71e1d5659415b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Exists LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1a2b9109ef68cd1f8ab20d75369055a62dea0bca TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Exists LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d7ad39e268c71546dea6b37493e09d35e1372b5b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Forall LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
19a8fc8bcef79ce90213fd322315a23205a8ea0f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Forall LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6a36e092eda6b98d6c463f5f830a0c23780c0054 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Choose LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
8cc5d316ae16d80b0e286867262331c375e97cd0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Choose LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a1e7cba252081615f70c921688e1c4b2f8902cd3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
4383fce64cdad43ec016dc383f6f99456d36ea0a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
8bc34a20920c633c741bcdbc4943e38f55bc952b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c11e22f10461f29f1c232e1b79481457c731c37e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ca5e7a2af9911cbc29fda2fcc4276f2d591fdec1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
a3aa265e0cda70780545544ee8923f2482616deb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fbc6f512b0f5e4faeb428728a2b28a8b6a5f09e6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
701e77b46d4abef0e65114a70148d6e99b4570bc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
49db3dedffc47c07492a9bcfb488fc2507ecb39d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1e043f23d318492e930244496ec873b45661dcbe TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d3eb208026869a2e55174ef1b35f60d0ff999c60 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
20b65807fd672d0d46729aa0aa186ee9bfe383e8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
030ad5162c5c64a8eb1197c4a537c65eabe4b5ff TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
b43529bd95805eed3e891e9eb7043d208fe9ee36 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e32856a3065734fd5fbac76192209146835f0f84 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dc30c07a9cdb6815cb63dea9936f12c92808af6b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
72eaaa552ec394f9b1021c1fe4f70a8d6154d728 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
24c1b4d00a8741293d1875c61e7ecb163581e0f1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fa19202ae3aff07841ef04d132fb268e45776411 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2FunTuple LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6d16f428a4074d20368787d1a37f984625798ca0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2FunTuple LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
991971e85931e9ff5612caeb2a07577c71c327ad TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
0f6de1c011983af2d3169a837d08d8a81f00ebd0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
cf9f121fae6dd37772c9191f74e9029be0ccb9b8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumUnaryMinus LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
01f357dc577f158d07a1a3f631661f5caf2b5cee TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumUnaryMinus LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0fb551708cdc6cd6aa5d592af3a35c8843c27398 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPlus LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
2fe4d3704c8563d7d9fdfb8d4ce8de31dd002d7c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPlus LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
eb7d77755f20be319684ecb8be5022ba9a0031aa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cc68d31a1ff99b0bb9c4345794f4539895d6b105 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d7f41f5a9233081fb5a8ccd9683471b51f0ce1dd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMul LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
a564804e0a60f6730e918568cd5418d522dc48b4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMul LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fc6c76a4f1932d5c383d89a3a36df6674bcc9c25 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
2992d53b31eeb9d3d2271bc981e1baab72a53ec8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
280363734fa9f0f64638ce13578513c1d22390db TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6e06407f6e4771288034d66ac4b7f3ba6951b7a5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
51df4359b6d85cbf5d03b0a71421fa2aac025243 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c611bf00e06136e738834c6b991c7497adec3b4c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
c4d2419000f6b1a764914161bd2ee93a654093b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGt LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
25db17bdfc73163cf9d6ec09d99f354173a90103 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGt LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
f6b9d8bd64c8ffd1a2cf2f95e112edc21bf9797a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGe LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
5b0302a6b1568a24a11adb41acad0b43dfef44ec TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGe LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2f8be6d51e4141c0f5e8f1609081a7719934b580 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLt LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6c60abd4bfe4365c50a401fd4f7999b52e56138d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLt LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
1821c9b042fa0f15645d343bdcda46e0dbb953bd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLe LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ddcff9064a20834030556121b529261bf06c5072 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLe LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
7d16ed80af4087792dbfef80122df0e03b83967a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
40a243f8db9a8d25906ec6cf8b5577a9dfb2fead TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
56114251f2dc1aa13648878c893f2be2a2fc72d0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
a52052ccafdac43d4a663a31cf0df71e0998c423 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
16c4989d5a68e6729959851a79e03b12ab68ecda TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
01574d5b3d8a55980c037a28c398f1e4731e59a7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDef1Recursive 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
c5bcc885de28ffa6253edb6f70ad7d7f7b2db683 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
628af7c56822520afeafc3dee2ea61a6d4516c32 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6cfac1e6866ed7806cfa5fab08933319d50097e1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
4fefd9bfc2d2a813bb29099dcf7d738948a2663b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
c263d9a2ab7c489c55e9d8ef82dffdc76eb3989d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3abeb4bcf2124c4553f6112fbfc89baab4ab2fe0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6e52deb433e3498eae1d8df6c89179afa5476900 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d023f5ba8c91d3ad008d411dae342846a16d102c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
35ff1c51f4e66e93bef48e7e07f8c4fadccbaf86 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3532ec35c70e1efa214f09b4457d34cd99eb68ed TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5b7dff94ec9d803babd37d297a9e553db56d7c1d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c6b3bf66fa552733fc5b9e929ab506f92e0f928d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
da8e137936e93f5f28dea840e66a7cb945bee9e7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
bc1c2f74e0156a7cdf378cf610031873ec7cedd0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDef1Recursive 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
60c63100cafe9312f5dff005951222424c966e14 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
f27c869ef46dbaa7fc58f7a25a8bf506ec1147aa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b28b73ae2d01fcbaee9572d3560bb1cd842b005b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
868321215a0b18803441ddfafbc48f49cc0a86ae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2e1652f34e554310ac423188208696c20f4337a9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
b411223600f52a3fc4d449b0c97f931b44f05ded TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
11c32706c570f9604081338ff65f341fbc6aeea8 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: LET definitions are reduced to global definitions
VariableViewExclude LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
9577064c3041f2ad7b3db98f5e19980c41cfe517 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: LET definitions are reduced to global definitions
VariableViewExclude LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b4915ad98b84088781bdd5015665987bd465cfb6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cf79686a107ec7e1b6cc11e688432a33fb5c03b6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ed63fc4ffea32c63d18a2d2c2b1c5a3b03cb907a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
e5127cf371e87847aa11242245db076132a4c439 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d7fc4e1a6717cc438c49cd81e4a7dda7a90fd737 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1d9976ae37d4dfa78d4f0bb01cb708c941662da5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
49fcd4fbbe256a5ffb8ab366ac960b88345d60dc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c37ae3cdb560ec97d29d93a34c22a084a2c31ed7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
be58ac32dd682a13c951116f5c905b4f89233196 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
14c629d8a16e3aa7a99003962ddaf876f6b798a9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
1e8e3b7ced04cb386a7912a2ddd5f3d099fb26bd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
07cafb8839364d84a246f7b8ffa71e96c625847d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
33fe408f60711c162e7553f532fc0262a01f93d4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cfd367d52df11dde4f5d2bdca87ae18a57d5b49a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
de3115f5e77f1b92bdcf0640bb2c7e99a2096fdd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
f9a3250815e177b9889c0d3ef4d76fb41c9efdd9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
f4d5277e9ee4f7630a57528aa98609076b62bc42 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
71580ed1e2dca8de146d84d49970d50f5f46fb51 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
99fdab9f0100964696e32eea7ba9b93f746ed4c5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
43986c4d852f081bbfcb638ae64f41942ed7f372 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
f542efb35ce3ca7c37453b64169f3739ebb2bdd6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Enabled LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c7774663c65d03d4bdb38891d0399b97221b811e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Enabled LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ec877c0f547b9a93b9321a3e5e6e578d139bd37a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Assume LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cfa66d7cf029ec7046a18df703423277117e3cd4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Assume LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a4fa62078b4424de1facab2eab93937ef766bd0e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AssumeNamed LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
52dd987d59010bb1443ce7c6a69dacce641b10ad TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AssumeNamed LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
af938c3c43bd463301c339a470d339d48311ba70 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
749a3b29eff22c98423cc18fc423ca8b1a580cb9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2556daccd305ef712e0242d684526c86da87b0e8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross2 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
fe214b7c9e083196989efedd9b34d342c28db05f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross2 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b08f9aa13859ab904de8ebb6a625dbabab6022ea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross3 LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c7a8c2700f77eebe44a274864e2867f5cb4bbbad TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross3 LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
22f9d2776fd75d2a9c535370d9f4c0fc458e9ef0 TLC with reduction strategy:
  • Case 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))
  • Plug Feature: LET definitions are reduced to global definitions
FunSet LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
04242120262f4d0315d8ecae434e57d4ec6d2119 TLC with reduction strategy:
  • Case 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))
  • Plug Feature: LET definitions are reduced to global definitions
FunSet LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
660d45a8bfba77116d2f21e99bb0eb67d56f2d27 TLC with reduction strategy:
  • Case 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)
  • Plug Feature: LET definitions are reduced to global definitions
RecordSet LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3d320a4e750ce6f7f533af92898989172c190baf TLC with reduction strategy:
  • Case 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)
  • Plug Feature: LET definitions are reduced to global definitions
RecordSet LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
9f7a67dde75544188b3dffa54c40d9663f8e79f7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3f7d189af49ce478b938e57352c03f853ecbd888 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
cd73ac65c4c74cbc6f9abde30e14d24541864c75 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetUnion LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
96ed98303763feb2f445614ac7d809b7aef71f4c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetUnion LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
c5fede3ad0bb03d308f106126acd42e09efe99ff TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetIntersect LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
8138dc6a770e60de9270bf9449fe808d904d9683 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetIntersect LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
aad37457692d2e8a1d297ad0053ce66cc8d70ba3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SubsetEq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
e08e4d783ed7a1491bf4efccdf66e4ffb3ced22c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SubsetEq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6811f35555c4faf8b10155e4f81c2f69d72588bd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d30bc4c007047ce4954392f724653a19b9988995 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
24d76dae73e246ed4a601c6a9863c329c9de691c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c5a72f4986d27be7a33218f70779b4561868c600 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a5222dc42979acb3d005bbe2ce3edb00c8f265b2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
f32ef7df17e422f5ad6f69d6a603bf75a701359f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2e605745078af1149330ea87d6ddc905328f1ca9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
7f2cbd802c5620dba213338166aec87531d6bdeb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
bcaec5de117716367cf00f5e9b3d340d1c46673c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
bb1f88d9f188a7d654a1cf86d4374e96867ed022 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
9e625a5e04ffc2cdebd761cca62724d132bf4724 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3f1713b14e9e981b1f4b7c9f5bd03746f4e7bc3b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
aab3cae8aadd478ab78153563e9582501ff12bf4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
8c9fda13fd00e63a6367843419e68eebf770c6b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
93921b9977c76519416aa54cde06e51d0e142aff TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Equivalence LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
5f6ed5b2c3b30f600582b87cc1fc0fcf25f9df3f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Equivalence LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
4d165d942c96f52c17002f0aa671d09fef045598 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dbbea8ad6f7862ec63357d153854d9cbbd5c45c0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
bb387b2017978ba7360837570b4193ef5cbc7289 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqConcat LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1fb0d2b12bba6335ff34b986499d562f6f3fbafb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqConcat LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
adfcc24c37e64c9a507d90a113468425750fbccd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSeq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1f3ed7a0bd778195444edac754e9253e043e4d85 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSeq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
bc881b2c67d129d9cb23c35718a778199b0c5da8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSelectSeq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
72b26d311abca4c10464fd42a1f6c12b37b26f58 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSelectSeq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
40d6a9c07b3448c4b7cd9b3e1814f2d449fe20f5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSubSeq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
afed273d15478ddb7c0650ff2e8a5c2f28b49695 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSubSeq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
982ec14b6d6e7dcf37f7fbefebaadb76e7d8f65e TLC with reduction strategy:
  • Case 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
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
7522d440871408f0a459f658d82f6e784c89eb76 TLC with reduction strategy:
  • Case 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
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e6ae4ac0e8e1376ca33ab212048168178119f384 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
94539d9a718fa3c527d37c76521e8e0dbf7357e0 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b3c4540fb944fa3f68b734796ee8d94970665231 TLC with reduction strategy:
  • Case 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]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ee1cdc3113f09acce238eea8aea0415ab40447e1 TLC with reduction strategy:
  • Case 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]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
779ec65dd63d78ed1a5bfd6d400f01f10de919d8 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
9101e5d7cc4bb7a96b7d99b5d4384dc36ff60d20 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
96ff8c5ce49d80497578643feb84869a8e6da058 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: LET definitions are reduced to global definitions
TlcSortSeq LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c485fe698c9d8b5bb8535131021ce06093b1c90e TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: LET definitions are reduced to global definitions
TlcSortSeq LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a3f69eefff4704cbe8e62f73d3bc0814a225ff66 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
e3f03b2d601e50f3249d41d1c8076a08e297e61d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
2cf495188462dadece454d71c402b4d6828a6950 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagToSet LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
91b52364c3c88744eca06cf0f060c924f4bcfe39 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagToSet LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a6ffdf774a011542ac87f02eb858b9ab1ee18b0a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSetToBag LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
8d78327f0992a85f3b28d258ca2f942a7e4ca4e3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSetToBag LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0446326aad8fc6a2c1f116488ab12585bb107c24 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ca4bd400745385b50298c785d458eafd83b7cb4d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
b15526354bf41e54be99a9eaefe31ccfe0e8c8bf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagAddBag LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
8dbe788fcd61acdc4e20cff49b82deb98ebe9b12 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagAddBag LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
395488641163ce3f9bbb0262157ddcfb5393b86e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagSub LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
2c53ccd3730acd6b8f1c83c7dcf8f9a9744b788e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagSub LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5adb859c88e8ad263d6d3b90af739947fa8aa9b1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
b0fb087f2d6ab1b8935e9d045ac91abb91fa98b7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ddaa77a265c49941520833152a1ab6a84a598a16 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSubsetEqBag LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
bd0585a135fae194f1d07154dd19b0498d3a43d2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSubsetEqBag LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
f435e4d70112ada6d883cbc8834a70432dd588dc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagUnion LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
126bf1c22f275bb67ee34811f7e7e028ebe0adc6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagUnion LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5027d12f376d2a34e9454c7f5e7dbd2bd3bbd6d8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagCardinality LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
7ee0697a530a2b51fbd3c4abdf1b02549e1e117e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagCardinality LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
395bcdca632e811db063c08173f3771a5686fc3c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagOfAll LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
b4e08b496d90d4185e1eddf6057324637fc986c7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagOfAll LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ead35a576d8f8e584da99806de3472e2a1a0ed9f TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: LET definitions are reduced to global definitions
BagSubBag LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
a58d5e21ff2e1fc8dee02b222266cd67579b5cef TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: LET definitions are reduced to global definitions
BagSubBag LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
8fe390c008cf801151e722eedf223ed78ef787b0 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ee18db25f5fc9f8c89bd235617ca6c801c1c11d7 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e3ac479f2312c2efa2e95a2c03f394cf0bce2ac8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsCardinality LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
74ead8a37cf4453f70d125d21a68c31b51966d98 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsCardinality LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ebcd6b01706339a12ab6195af019b4514790af51 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d5a722b2b26932052d549473744fd418e97e5d70 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6fd63733b9187fbfb7afa85372918ee1e1f82063 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
98ed5606ad44620d96b8424ff86ce3407ce49938 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
75221bc6d4cf69554b4751d566a7f916137c16e0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
e4ea2f7e2c579a12c4ffcdb51769df4f4ecce223 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model