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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
49d681a75bb5769a1583342ce2f11940e37ee0eb TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
And Or True Passed
  • Model Under Test
  • Equivalent Model
723641895431b9b43ff120e3371541f70f22f6bb TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
And Or False Passed
  • Model Under Test
  • Equivalent Model
4edf5f2d326ea479b84ea6c39236c94eb9373e7e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AndMultiLine Or True Passed
  • Model Under Test
  • Equivalent Model
f4eb6d08a0def2529595b0068fd3200babb84646 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AndMultiLine Or False Passed
  • Model Under Test
  • Equivalent Model
cc7bd8f76451efdf97f43519587bec9ddc67622c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Imply Or True Passed
  • Model Under Test
  • Equivalent Model
87d486172bdfb787112df45b217f883f55d514d0 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Imply Or False Passed
  • Model Under Test
  • Equivalent Model
f8ece3fc347745f7ada3729642bfa883a51da770 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Not Or True Passed
  • Model Under Test
  • Equivalent Model
e84d48fa783fbd46b6e6e8292942d30ddf58520b TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Not Or False Passed
  • Model Under Test
  • Equivalent Model
01976cfc6a9b5e104eff71a7dc16c17ca9c77ec9 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Or Or True Passed
  • Model Under Test
  • Equivalent Model
660a001197641b245568dd1d40587825dfaaaa8a TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Or Or False Passed
  • Model Under Test
  • Equivalent Model
74b6e2efe45ed02aa827b3a92a82ef655a233cb5 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
OrMultiLine Or True Passed
  • Model Under Test
  • Equivalent Model
75b62c24195b25e85fec34192f360e3b912d95dc TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: A \/ B == ~(~A /\ ~B)
OrMultiLine Or False Passed
  • Model Under Test
  • Equivalent Model
ca709d829ec9aaf0774b40cc529da1db909af590 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AndProp Or True Passed
  • Model Under Test
  • Equivalent Model
f607553d63c1ea0f1e587a116d20df259fff4ce2 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AndProp Or False Passed
  • Model Under Test
  • Equivalent Model
b50cbc7ef84a896832ef699858f5b2cd6886b95b TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Boxed Or True Passed
  • Model Under Test
  • Equivalent Model
a7e7dbd874596fe80d879afaedcc740b851d47f8 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Boxed Or False Passed
  • Model Under Test
  • Equivalent Model
7968dc53ad0b8559d6c822ccc1f42308672b3569 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Eq Or True Passed
  • Model Under Test
  • Equivalent Model
82c08945aee9d0657e6dd3fee5699bcdac890d5c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Eq Or False Passed
  • Model Under Test
  • Equivalent Model
fa98a78b209227ba62df4ab92582d8037c58388a TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Ne Or True Passed
  • Model Under Test
  • Equivalent Model
add29db676ad1589af66407a8212016edcbfd555 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Ne Or False Passed
  • Model Under Test
  • Equivalent Model
ee67b6597be8da458c6fb184d86fd9657e022b98 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or True Passed
  • Model Under Test
  • Equivalent Model
474a3294934c58238f30940655e379e5a8fb9345 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or False Passed
  • Model Under Test
  • Equivalent Model
5590cd02d14a055ffcada939640321f20281f964 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set0 Or True Passed
  • Model Under Test
  • Equivalent Model
5dc2445080ca3b1b36bc357c2ba63f4698117b12 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set0 Or False Passed
  • Model Under Test
  • Equivalent Model
9fe48859e85215a7add768d75694e44b45d4aa81 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set1 Or True Passed
  • Model Under Test
  • Equivalent Model
ea19490d809e7ff55b81eefbaf756a7977b08cbf TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set1 Or False Passed
  • Model Under Test
  • Equivalent Model
7214d1ba981c6c64725a14690393f673d5dcd837 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set2 Or True Passed
  • Model Under Test
  • Equivalent Model
cedef707e29d29fc1f2d5a8d12a13ac993e2d8e1 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set2 Or False Passed
  • Model Under Test
  • Equivalent Model
7749a22f7dd6a0a6ece081b7623d249e78dafd8e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Fun Or True Passed
  • Model Under Test
  • Equivalent Model
74fc99049471ab639c35827af8231dff9f5c567f TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Fun Or False Passed
  • Model Under Test
  • Equivalent Model
28658ad66d625ba1839d528a0bcc79439de86ffd TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
In Or True Passed
  • Model Under Test
  • Equivalent Model
bf286efd5a8a2d6e05c79080eff22e5ebb1f21da TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
In Or False Passed
  • Model Under Test
  • Equivalent Model
33011b478077329e4d284216ba3e56e5a6233980 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
NotIn Or True Passed
  • Model Under Test
  • Equivalent Model
a28481316db034179ec9675b1ad3fa2b51832652 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
NotIn Or False Passed
  • Model Under Test
  • Equivalent Model
cc0f90d95a246a7c8c55ce28c4b02ff3b6139308 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Exists Or True Passed
  • Model Under Test
  • Equivalent Model
0ad62d05ed9820dd33f66ac76446808ac69b9f5d TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Exists Or False Passed
  • Model Under Test
  • Equivalent Model
1ac187464571e494bc9fd0637f4d88567712c9dc TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Forall Or True Passed
  • Model Under Test
  • Equivalent Model
2307edd1bdb35fe43aa7123a0ccf7765b70d4067 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Forall Or False Passed
  • Model Under Test
  • Equivalent Model
d2a828d3d9fbf0f4b75c6ebf0b720df360b5445f TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Choose Or True Passed
  • Model Under Test
  • Equivalent Model
ae8396fc5811c7c01d6df6da549f7d82cf51ca64 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Choose Or False Passed
  • Model Under Test
  • Equivalent Model
1e323f28649776e9fb1d27ab98221d5dd2e850a3 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Record Or True Passed
  • Model Under Test
  • Equivalent Model
6a70e56b7bfbd31ab62f23a4ec224134ad7912ba TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Record Or False Passed
  • Model Under Test
  • Equivalent Model
28a01c475442693eeac5f71cffb6d1449ea14964 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Tuple Or True Passed
  • Model Under Test
  • Equivalent Model
79df42b01dbfabc1028f849fc6f0996e281b6341 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Tuple Or False Passed
  • Model Under Test
  • Equivalent Model
117f7260d32e527630770f19d3ecd71fea66a6cc TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
FunApp Or True Passed
  • Model Under Test
  • Equivalent Model
7f9e192f3c67601009bdd397c3606b3e92ca5e79 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
FunApp Or False Passed
  • Model Under Test
  • Equivalent Model
a0108e8f132159b178cd7d65196300ee19e09a90 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1Fun Or True Passed
  • Model Under Test
  • Equivalent Model
ba733b0c9d7572ef23412608b36f02a5585d45dd TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1Fun Or False Passed
  • Model Under Test
  • Equivalent Model
e273705b20dedd03eb2fde32e992475caf213339 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1FunWithAt Or True Passed
  • Model Under Test
  • Equivalent Model
0efe73310b03618003053f60ef6842a40276665f TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1FunWithAt Or False Passed
  • Model Under Test
  • Equivalent Model
b8f56178ac16749d9a68a4ab01dfaf2b56398003 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1Rec Or True Passed
  • Model Under Test
  • Equivalent Model
fc8b0865a8db8938fb5f4660e19123903dbe2a9c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1Rec Or False Passed
  • Model Under Test
  • Equivalent Model
9d7bacba6ae918adae38ccd5402de46342b29e1f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1RecWithAt Or True Passed
  • Model Under Test
  • Equivalent Model
8e7d9e1d194cc347c98da06ece25859fa1510c57 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1RecWithAt Or False Passed
  • Model Under Test
  • Equivalent Model
b27782010d41a938e0a9f92b501f348a80c84bda TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except2Fun Or True Passed
  • Model Under Test
  • Equivalent Model
b62906cb308d7afa36fd96e452a1d5c8e92c9a8e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except2Fun Or False Passed
  • Model Under Test
  • Equivalent Model
9507de26dc8e0bf188fea1cb7eb6ee7e7eb6bfd4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Prime Or True Passed
  • Model Under Test
  • Equivalent Model
5cd58aaf02555a39c1575b8813d25965a13d0d99 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Prime Or False Passed
  • Model Under Test
  • Equivalent Model
575c9ed479a0244a4ce400c8b658fb0498bd7f53 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
DefFun Or True Passed
  • Model Under Test
  • Equivalent Model
07bde52891a653e69fe075b2002e5e4a3056b519 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
DefFun Or False Passed
  • Model Under Test
  • Equivalent Model
1074f0e546ba358ded8ac1df785a3259bd3537e0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFun Or True Passed
  • Model Under Test
  • Equivalent Model
6e82693f0daec9a899f443f319cdd9d30ab69bec TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFun Or False Passed
  • Model Under Test
  • Equivalent Model
046e4ad83fc913a72c8de7a18e3a975543bcf6d2 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
DefFunRecursive Or True Passed
  • Model Under Test
  • Equivalent Model
f973b85c54e71bfb9d812b92092c38305e93c829 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
DefFunRecursive Or False Passed
  • Model Under Test
  • Equivalent Model
104560ede453000a25d30095943297a413a89800 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFunRecursive Or True Passed
  • Model Under Test
  • Equivalent Model
f51504e9e2b6367a6e5626b2b7aa35ec4c2717ed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDefFunRecursive Or False Passed
  • Model Under Test
  • Equivalent Model
3f2cd89b13623f8d67dad35fd7507603cbf1c548 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def0 Or True Passed
  • Model Under Test
  • Equivalent Model
ae7080da9c7b4336c4fd127fac083d3ca8f79753 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def0 Or False Passed
  • Model Under Test
  • Equivalent Model
8f9f417b9d82881d3d4fc556673c2806f350b1f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef0 Or True Passed
  • Model Under Test
  • Equivalent Model
05cfef42439d7bdc292895b89533337f65b1940f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef0 Or False Passed
  • Model Under Test
  • Equivalent Model
37b395effc67f9f6b2584b7c093a016b95f8b077 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def1 Or True Passed
  • Model Under Test
  • Equivalent Model
37fe98d66dfbc59b3623e82b167996c7fa8a3d6a TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def1 Or False Passed
  • Model Under Test
  • Equivalent Model
efffb1262ba47fdd78e96d76624e09eaa3651348 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1 Or True Passed
  • Model Under Test
  • Equivalent Model
68cdce34411be61e9c6e57b166fe8eddbaa75872 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef1 Or False Passed
  • Model Under Test
  • Equivalent Model
ebe665b9981ea54040d8674ce970901f0b6008e7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def2 Or True Passed
  • Model Under Test
  • Equivalent Model
ec52f8540356a7b90fc58691e9386ffd785d1f6d TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def2 Or False Passed
  • Model Under Test
  • Equivalent Model
bcdf0b1874808673ac30fda485a8929f7b5b1c35 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef2 Or True Passed
  • Model Under Test
  • Equivalent Model
513b4a76f370acc6522214d2ab2e1d8f1bb28e83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: A \/ B == ~(~A /\ ~B)
LetDef2 Or False Passed
  • Model Under Test
  • Equivalent Model
3c86cdcb2ff5181cbadaeb4b9d851d186a38533e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def1Recursive Or True Passed
  • Model Under Test
  • Equivalent Model
372a0cffb3214223c037e15d7a790c4c63b4bc06 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Def1Recursive Or 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
30b3691afa2770c7a8fc1c3ce53cca5aa02d4fa7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Extends Or True Passed
  • Model Under Test
  • Equivalent Model
a5fe71d96396d83fbda6e4ee5879dfff62497b13 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Extends Or False Passed
  • Model Under Test
  • Equivalent Model
6fd32b43a83b4751cd76c670313203fbd6be3d9a TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
ExtendsInDifferentFolder Or True Passed
  • Model Under Test
  • Equivalent Model
5091ba380972c10aabcd1920c7420f2e43b5f593 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
ExtendsInDifferentFolder Or False Passed
  • Model Under Test
  • Equivalent Model
c42c88756a82a749707e80c12a2b0ff407edf3d4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Variable Or True Passed
  • Model Under Test
  • Equivalent Model
b4ecd0a6c9c359297c58ccbbdeaf75d9fe1152c7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Variable Or False Passed
  • Model Under Test
  • Equivalent Model
2a8f91d5a560047dc5a4ba3fdd709bc7bf78121c 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 Or True Passed
  • Model Under Test
  • Equivalent Model
3f17f68c2df0de5f29f4ba2f279af10f0bd5907a 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 Or False Passed
  • Model Under Test
  • Equivalent Model
4493098dedcde6ed9367e1f0648205659e4e6da6 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Constant Or True Passed
  • Model Under Test
  • Equivalent Model
4c5cd7add6f38ea879449588a0fbb8fb7b5906d7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Constant Or False Passed
  • Model Under Test
  • Equivalent Model
489962ec7040bd01f5336b0beb1acb36f2d32873 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
ConstantRank1 Or True Passed
  • Model Under Test
  • Equivalent Model
d747e5ed605ceef11117055767dcde8fc0298d52 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
ConstantRank1 Or False Passed
  • Model Under Test
  • Equivalent Model
d06b570cc13c914145560b53135b68721f68a480 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Instance Or True Passed
  • Model Under Test
  • Equivalent Model
24fab264efb9a4ee2a4ce0a2c4451c58932b6b50 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Instance Or False Passed
  • Model Under Test
  • Equivalent Model
63a0a83cc8e826b0ed800880aa971362236e478e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceWith Or True Passed
  • Model Under Test
  • Equivalent Model
92fcf41af16d055ad4b39abbe4ffeeee78f30a90 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceWith Or False Passed
  • Model Under Test
  • Equivalent Model
0d0b03f21cbad87e25fef552117bafb41cfda0d4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamed Or True Passed
  • Model Under Test
  • Equivalent Model
3e43e21ebface81b045b30bb43ab2d815313d8c6 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamed Or False Passed
  • Model Under Test
  • Equivalent Model
510ac217b0383eb143bf47371f7c0b57373dd2d6 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWith Or True Passed
  • Model Under Test
  • Equivalent Model
5ab736b82def45e4f28886d13ba670e3aad119a4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWith Or False Passed
  • Model Under Test
  • Equivalent Model
56f7f0be8402995b3fdcb62b612b87a48eed20bf TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceInFolder Or True Passed
  • Model Under Test
  • Equivalent Model
78764cdf421a83cf950740695b6bc102586970f4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceInFolder Or False Passed
  • Model Under Test
  • Equivalent Model
a7fc64128cc0b182b448666cbef178a169628475 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceWithInFolder Or True Passed
  • Model Under Test
  • Equivalent Model
2df3687599696385c407bdf4b87723a5ebba3075 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceWithInFolder Or False Passed
  • Model Under Test
  • Equivalent Model
7486e2ac0b54c405f655af8fa9eb3672e236e3dc TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedInFolder Or True Passed
  • Model Under Test
  • Equivalent Model
7c7ea30d9d9d2a339d08cc7fbc1f3596c6d4aa1d TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedInFolder Or False Passed
  • Model Under Test
  • Equivalent Model
532a47f513f605ad307cbdb3b122cf75392c30f4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWithInFolder Or True Passed
  • Model Under Test
  • Equivalent Model
5602698e722e59a2dde6c42b4893d4fa803ff769 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWithInFolder Or False Passed
  • Model Under Test
  • Equivalent Model
a0b767d5f28b5e27b01a71fa5af25e752f61b517 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Enabled Or True Passed
  • Model Under Test
  • Equivalent Model
6aa95382a31b80f4e46a30c21e567449d53522a3 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Enabled Or False Passed
  • Model Under Test
  • Equivalent Model
b513a9e49035f2cd5901bce5c87818bb0a4846f5 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Assume Or True Passed
  • Model Under Test
  • Equivalent Model
dd43b4deb41df4c1dbdc688dad04153e885932c6 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Assume Or False Passed
  • Model Under Test
  • Equivalent Model
453c991064e2d3ba9b0a6fb3402c0d0374a41bc1 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AssumeNamed Or True Passed
  • Model Under Test
  • Equivalent Model
e49e3e75a4262706c3f6992d16824b0ed92b24c1 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
AssumeNamed Or False Passed
  • Model Under Test
  • Equivalent Model
90d9739bd1d6afe8cae660f6ebbcda3911a58b87 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Lambda Or True Passed
  • Model Under Test
  • Equivalent Model
fec5d9cc99c80bb0ba6f7ae1b0f33a3112449845 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Lambda Or False Passed
  • Model Under Test
  • Equivalent Model
278439f6dbde013cc4a56108adc791b2b4bf5b0e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfCond Or True Passed
  • Model Under Test
  • Equivalent Model
8cd80d8693e5017a0f7f7b4f3a8edb8c7f03068c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfCond Or False Passed
  • Model Under Test
  • Equivalent Model
a16effed6f7e276faf0b4cd97988fe827ff25b9b TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfThen Or True Passed
  • Model Under Test
  • Equivalent Model
b56f1f9999a355ffbce23da80493aa569f79c9d3 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfThen Or False Passed
  • Model Under Test
  • Equivalent Model
2e8086dedbb1821396613dc0c606e74cecf1e534 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfElse Or True Passed
  • Model Under Test
  • Equivalent Model
96991571a24075fbbe1eb264155c9d444b4fc5ae TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfElse Or False Passed
  • Model Under Test
  • Equivalent Model
e33310394c96ca0f2cf25ab9efb233e4e48e9907 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Unchanged Or True Passed
  • Model Under Test
  • Equivalent Model
4549f67ddb9f740722e147a68525b86aedbe8414 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Unchanged Or False Passed
  • Model Under Test
  • Equivalent Model
a3f33c80b4f03108dca2de1a0b788cfd1451f601 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Equivalence Or True Passed
  • Model Under Test
  • Equivalent Model
192c5b6b8cd7309659a300fb707b4546b00ac32a TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Equivalence Or False Passed
  • Model Under Test
  • Equivalent Model
73bdc2d0da8179f6cd34d921915bf500e74cee49 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcSingletonFun Or True Passed
  • Model Under Test
  • Equivalent Model
7984a19022d1484bc13a0663763e638d117dfe6e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcSingletonFun Or False Passed
  • Model Under Test
  • Equivalent Model
f2be1b679f497b89258b35ece61b5e31453a32bc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcEval Or True Passed
  • Model Under Test
  • Equivalent Model
88ba92ae36fd1a468921c93ee0a6d01ab96cc025 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcEval Or False Passed
  • Model Under Test
  • Equivalent Model
4d1f84f21f82d9075fd8ec56e345d0957486dc53 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagBagIn Or True Passed
  • Model Under Test
  • Equivalent Model
f9a076ca0125035987754bb0572c6a21b64d2020 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagBagIn Or False Passed
  • Model Under Test
  • Equivalent Model
722e4d2697d7de57edd217c16c552c0244b2338c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagCopiesIn Or True Passed
  • Model Under Test
  • Equivalent Model
6715336ea8c6932cd8d999ed3a113f505313daa7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagCopiesIn Or False Passed
  • Model Under Test
  • Equivalent Model
37bbb8979dd034391bd301e9b362f81020469ff4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
SeqAppend Or True Passed
  • Model Under Test
  • Equivalent Model
31eeb45e923e58469ad04563c8c235f75a2d8862 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
SeqAppend Or False Passed
  • Model Under Test
  • Equivalent Model