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 OrMultiLine; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b648f8aa924fb179b37240884592c4c96da949f4 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
And OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9a46870522b9ebedbf984d864042c93dd3f07fd3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
And OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
fb214610ff44d6a73ea785fd0ad3fd3e5d5fcd50 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndMultiLine OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
d34552136b61da264a1cbc04f8da51ece73482b3 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndMultiLine OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b479cc1b0b2d1bdb0f3acc6b5be233ecd67d6513 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Imply OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
3a1d23e1995b934664c7d866efada1e1f1f9f26a TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Imply OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
9a63ea7610d0176ec69c45397893b06f51adf056 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Not OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
43e86082409990c484cb3ac96e19491d92545755 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Not OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a2d294b5a6588ed709097b012d604d546316608f TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Or OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4a09a83a091675244bcc0ae9f67fae6a67affa4d TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Or OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
347b7631a57a2bc6e189257fecbd06410bd038af TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
30e6a908ebdc5112f5ca3bde2882132546b6a55b TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
05934505c1cc36769e9f4c7c5b0fee6a91a3f48b TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndProp OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
2b1c58ecf61421fac9946f6895b7c7ccf763caf2 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndProp OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3b67886b27e2d8dd9a40cc9d0c25254627c8a3dc TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Boxed OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ba72f70e0f383f34a8f5d8294b1b0d054eb04a88 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Boxed OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
294a25fedab1b3def60f6c253fb54edfdabfe82a TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Eq OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
3c91c18fe08bc56ed64cecb1d83948202cb4a2d7 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Eq OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c23ae89b9ebae83ba6aa3036a30c018f92b30b8f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Ne OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8c82e59b35522b2aab1f8eedf5fdbdc3b6ca29d7 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Ne OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
03190783de6897d460f05fb0ffbe5befd203cf2c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
cf216d66495ab7f1191f405ef79e6c972821cecf TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3ce507b577376c5db1d9d0478d5af151570517aa TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set0 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
c21395c84c0d3f9b7a07b2458ab24828baeab647 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set0 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
fe69c9fb03e3607494e5cb1293a0f944d74c4c5b TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set1 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
037f9a2a8b23e47289041c7ed2e8a61094d908e5 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set1 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c5906e353e0c095011eee7ecbf7451089dbfab9d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set2 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
f3eddac0f10530b47104a50af69d42b2ecf35de6 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set2 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
60105873835be21f3c77e781a95d119bc5ba72d3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Fun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
03c4114f138b6ac071774b0559ceab3048aa0d28 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Fun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e149b0326b5d83d249478a28346d9086e33abcfd TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
In OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9e3e03fa7be6392a221c20094b61ea70a0dd4d6e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
In OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7f8960f5d6ecfbe5b3cc045b780cd65dccac9685 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
NotIn OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
09433e9de48527957fdda99626af63a2d92eb514 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
NotIn OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
24bbb675bb5fc1caf511376925c4fc5304577e62 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Exists OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
e1bb3645fde4bca23ecbd92444368d545021ff85 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Exists OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
deeef08259d6443430e0406840ef22e120d01ec2 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Forall OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
fb10555febded4772c700fb3dcf9a67ae971319f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Forall OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
746d876c62b827599b724529871855f4349954c5 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Choose OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8f97dc89311aea3fbc0d8d7c7fb75ff7b247b253 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Choose OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ac213bc95678032bb27041b302733783529abd3e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Record OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
a3338af9a3b046e8c65e9bcdfab524c8fa912045 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Record OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
282423a3bd7f981556404a76cbb3c1637c1f6d4f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Tuple OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
70642adfb95737f0d34b9834a7cce6ac7f5b9be8 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Tuple OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
0f1635a4c2419d19ee167efd785d710120b3cee9 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
FunApp OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9b86833630eb7c6fb010d9f7dad195969aee045d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
FunApp OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b5fccd1db31504cccabc5d589c239a7b739dce05 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1Fun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
cadae42d5463b7b8b8d4eab02e90eaa20960c59c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1Fun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c93b8ccf804ccbd2b7b0a61541b81910e93def89 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1FunWithAt OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
71c069ca02055ab4ece68f84aac64a1d064ced81 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1FunWithAt OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
d051efd36b7845549d690e479cce300f56a0d309 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1Rec OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
abc9d6cc8e8034b73a1754882afa2d3df80983bc TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1Rec OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
5315a303f57f914d89279f5d473110ad683d751a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1RecWithAt OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
023178401f675ffea30a2f37e96169547016a0a1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1RecWithAt OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8c628ff8d1331476f4e3c4a0c727812b67fd47e1 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except2Fun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
85283e2fc7e1ae4ce2505c144a6639fc7b035078 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except2Fun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2bfb0a2f22ca5c25452efb2550d17306164ced0c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Prime OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8f6218b1b52f7816ed9b8c8fb99ab0f3238df6b3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Prime OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
d8583f5830cf5c2252be00b19fd0b7d7978ec61c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
DefFun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
a49b469552992cb3cdd8ab2ec1e39f74f615a355 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
DefFun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
87e46d887a50e4b05d4563f42f0ed8d05102e7af TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7792e1d4832505caf83a2c57a21c6dd1a96905a8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
377adfb3250d7bd3126c4e20aa7867460c6450ca TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
DefFunRecursive OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9bd9082f1dc4bc8f2c9057aa9dcc9695028dd693 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
DefFunRecursive OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4273a7c24caad81b309e0556ab08d50f0dcda93c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFunRecursive OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6bb109fe149c844157a5eee34dbcd64fa610b43a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDefFunRecursive OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
94e3e995b311284788728465d6ad8ae1994d9dbe TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def0 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
67e134665c097a8591ff64edd39a4cae06ad3e10 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def0 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
9aee139cddf4c2d5baee527452fbbe2d88361e38 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef0 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
e5439557618e42a9b4e110208206773839571ef4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef0 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6f158b4c448f19a3cafeeb044747e0b39562a519 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def1 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
1b954e6936655bf1858d3715bc93f400591981fe TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def1 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
490aac228ff8fd7102d993e9b8fbc2504ce7a190 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5f4c49285eed7501aca9bfc5821dbcdea39431d7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef1 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
277e22ac7d4e9c0f1091f3064d3e9eb7de3d3c15 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def2 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
fc4ffe54a90721dba806ad00cc07a65842e0728c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def2 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
9ee7638beca80e4dda782d3aa3a04fc4e7cbe3bb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef2 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8c003a288afa13c4b5f02ea4d4f8b4eaa3db11e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
LetDef2 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7b7f14dcbbd8a4ea6702295c5f646b77bd81a711 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def1Recursive OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0ea28e79d3b6775ee2d548bd1121bafee4222496 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Def1Recursive OrMultiLine 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
342004cf1e0128120088af6b2f064dc13b666e6d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Extends OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
69b1d578199c573867e5efb3e11a3eb3937ec13e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Extends OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
f90da70dc8e558703255328cfd0bd3c997a4d378 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
ExtendsInDifferentFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5a901a6a7fa64123d6edb101a1e93d5b31013b12 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
ExtendsInDifferentFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b5c5292ce409229553f3da585c1f2233aec07247 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Variable OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ad702b5fc48328e8c2441b1e07d083140b590354 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Variable OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
10fa93651b88232fbfb68c120cae8df3c75f62ef 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:
    \/ A
    \/ B
    == (A \/ B)
VariableViewExclude OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
175c657d41b7c83e4cb1728cd303f022b11fa7ef 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:
    \/ A
    \/ B
    == (A \/ B)
VariableViewExclude OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e9f82d8891b2651e3ccb9306c8a8cee8bf96a07f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Constant OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
081883f7e778b0ed7d8983e16f01f5b6e43402cf TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Constant OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6125218131d98d2b341c39b7dff4f67d645a63e6 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
ConstantRank1 OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6ff0606262d54bab9fcfbee320b7d857fb26f5a7 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
ConstantRank1 OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ee66ac75d25134b8da1591e933c44aa9a10fde88 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Instance OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
16e9cb74777c3da9ab037c7fec82ddf3c6015d26 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Instance OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6566809c82696ec1437b58f9ad1dc3541735ef4c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceWith OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
b70bf5ae1cf8b103fe10579a3b809915d7e3fcb6 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceWith OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8b7708c86aef8ed35b047152037059736c92f95d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamed OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
fd307780ad6e0cdbc00f924cd50983d26bf52f0d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamed OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a47144b036c3c372c63e714fa5450f2fc8cc3143 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWith OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0ae7bb0ae61b5b49b3a1718d247759ecf7cf4739 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWith OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c2dd0ba253868e730069a5128440fe487166c04e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceInFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
611b650936b84901a08213c023001a11a944802b TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceInFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8b5aa4097fecbd0bcec3c17873b4e511cbcc197a TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceWithInFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
529cfda56647f0263ece2dfc243c38e1e56527e7 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceWithInFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b1d4308daa89090b34945fa9e5e24b46928ed6d2 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedInFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
2bba3264c0d6e90e6de783ccc8e5b6bb03e8b102 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedInFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
fed7dae33296b23a6495a7e4bd6896d52057f113 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWithInFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5064009770321e000f8499eabe84ccf6ce74f7a4 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWithInFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
898b38422efe231f327253a96c03687cfc2ed8ce TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Enabled OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
20012c629a6d49dca37b1e12a441e0088c1fbe0e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Enabled OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3309262ca11facc33bcef5f3554595b39dd0006c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Assume OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0878f5c13d86e7d3b61ad9708996c9ab4303650b TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Assume OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e9e59dd840653e40ef55f06aaf041571de7ca97b TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AssumeNamed OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
765fc106a3fa2568cab6d20b1f5018097ddc8b56 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AssumeNamed OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
1ef347f4354a39cf223212284b51745863760157 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Lambda OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
84e2dc3090f15ce856f9590f927d56456a5f45ed TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Lambda OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c6dcea75d114441f44bbfa1544c605efdfaa5db8 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfCond OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
75dd5329f688fb10c63fec5bc708a8d534a5a883 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfCond OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b05008cfcf54c4668ca6dc4fdd720efa3abb5df3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfThen OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0d3f04b7d4c23175315993ebf58b98a32c39d753 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfThen OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
d66d74d6eb458c1d2c515322a6657a1022e480af TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfElse OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
2423332a4b8fe836a5b4794a1a905039febe5475 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfElse OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e5f630dde641fb0af090c64db2414e4d3abaf659 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Unchanged OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5c77e7583531794722ce6064b960203fffd1b1b9 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Unchanged OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
625fe8473a7ee013409713e58de3369706a74cf4 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Equivalence OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
cd48ad0f3829cfab94ba118230f367813cd4cdc0 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Equivalence OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
08ecfa6f33c4f7331c0f59e1282478e95cfbb0dc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcSingletonFun OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
a1e3c5795677ed9bb7967c31e5642f6086d31427 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcSingletonFun OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
aff1fbadf438a5722ee0534a58332c49193e31ae TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcEval OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
060c4614afbb24d6f6e60b8c724491ff11de03fc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcEval OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a9ef8e4229e82d3e95c44f8f5445f8678e2d68b3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagBagIn OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
aba058c311292c2955a7e82a9945a195e8ba0c72 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagBagIn OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
761d77474cdb8685708bbdb6175781801859686e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagCopiesIn OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
085ddc5d9e80666d2f0b2286071abe234e82131d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagCopiesIn OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
374d6a6fb90027416d262ce7766d497f2150b067 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
SeqAppend OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
2a4b0d606bf170293f25fda9769731d6b494a635 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
SeqAppend OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model