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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
a69d61b93971989cf5a29292c49a20652b5cf8e1 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
And FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
69d004576353c9ade94f3286c51266628e3f1f4d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
And FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
76ca0065c180950003e64837d2f13310d8e48364 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AndMultiLine FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
7d97c51616856ccbe5884c6661e1a9ab8564da87 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AndMultiLine FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
3ff483a15352e5eaf4dbce31bd0766f4d5ed00eb TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Imply FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
5ac04196bc1310cdc07fda0dd97d7db35167edf2 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Imply FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
bc37527d552f3e7a88bf2e4b5c0b36ae789ce9e0 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Not FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f8583b3e8d953445dde1aa0c8a2336bddf98e926 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Not FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
99dea58726e93363a58db69627fe35778d04fcf2 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Or FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
cc55832eb7b1382523f5562d028034c3e5500cc1 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Or FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
28d1f990569ab2bb2705879065f72a9b9f31b68f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
OrMultiLine FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
9c76ba52dbb6b5be443c09eb641ac7021604e7ea TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
OrMultiLine FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
4b6d6a7632f2556940ece6afa51de11a8301a3c0 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AndProp FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
d20582d8916c07079aa51562031049e8d4d12512 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AndProp FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
4496829a996f0a1bb19b1707a5c956d29113dfe4 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Boxed FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
6a67605b7dab093c1370c68926e420c70671d75a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Boxed FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
a7e60bec7d4b50580a3e5edae6c21d3eccbf843f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Eq FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
c4f8f3fac9969b0a71626e1632b449f819c76787 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Eq FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
087284367b66f64fe7bb5bdc7a88505c22f5dfeb TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Ne FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
98a88225ad0ce6b5918f06346ef2110d9c919e9e TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Ne FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
7c3d45eab1e94c2d036c16db930595e85d70511b TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Let FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
30fdfb178b0379347bcde61197b9a857973f452b TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Let FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
0a97522e46892039598b29ed9f09a2fbb49acdcd TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set0 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
e35dfb6c7c619eb2bb1da8c1480172b7ddf271d1 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set0 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
823b0a93f8ddda9d977c26455f4f9d854e658084 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set1 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
46d0abb8ef3df989245343e3d76e2fdf749852e8 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set1 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
82ab2eb536554b3ef70f118280a2285c77aeee8d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set2 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
3198c7726636c52cff5556e35681de6b508117b6 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Set2 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
7cb1909027121cfe002bf30bc6d5a8c576bd41d9 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Fun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
46b4cbe6ba0a381495372bbc0d0644ed4842abb8 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Fun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
1836c75e82d3fcdb215e29ea893ce919d7579b66 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
In FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
bb16f025cb035ee4847b500a6c5d0c10023afda0 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
In FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
d6face2943b32a104dcebaa876c9425e6a2d24ca TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
NotIn FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
24a6adbe31df61f4e664b0d6356c7eede0368ded TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
NotIn FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
8878d85203d0fe50df20d9848bfdebaae190004c TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Exists FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f7df3c47d734ffc6963ab341bcb6e91eabe76900 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Exists FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
9c8c3e2444c0314ac93a722402556bb78da35ad9 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Forall FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
065b119e804df262437b3d572032e3f06f28e284 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Forall FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
91fb3139dc94b222660e173f3ef08ac9942a6c9d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Choose FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
19d342465a32bc55493e462c7aa75d1f62ba13a5 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Choose FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
6180c39ae857d434b13682d35b2bbcdf89a2b026 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Record FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
97eca99ce6dd24545c82b39232faf778e7a3036e TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Record FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
a877f8743dd72f13b3b157fc80a5b7e7cafa14f3 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Tuple FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
8bd05c9f57f41718374325764cc14d7c93078d6d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Tuple FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
b44f74e1a4ec97d9578d3383e6a19faa98d09062 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FunApp FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
c8ec5e0dba0090f97ce99ffd588fa5d884fa9b73 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FunApp FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
8455c30cfbb61215354c367a590b7a3dbfe8869a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1Fun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
a70bbbde705a3cfe1a57ccf93d27a8bc5305db17 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1Fun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
e2478e8ee00832cc7caffc3c83016a5f4cc9362a TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1FunWithAt FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
55df68b0684ac7f77f02f7dc8086450289c0a259 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1FunWithAt FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
1e9e0f36f4758c73730187aec3fc49ad6fffe5e1 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1Rec FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
201fc3c689314fcbf6e7d8fbf9914ded1b9b1451 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1Rec FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
4522f31987c35843a55f252f437297e2518fc202 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1RecWithAt FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f5dc1b68e7ec74828f7a09afb51cf534037ba2b7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1RecWithAt FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
f886ff78967100ea2e2c05537af5e102ffcb2f01 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except2Fun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
1afbbd528d7356304a48d952325d3c1f570d961a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except2Fun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
4616915118fd1a697884a006f96b6e337d1b2c61 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Prime FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
7fdcae9fd61ac3f48b3cee4d708ee5a7475151ca TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Prime FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
30b97bb4bf3ffde92524095739b0bb2033bbfb20 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
DefFun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
48942d8ea00b61b2ce617ac17a8cf63bc228b8d5 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
DefFun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
3d07794be1bb6b507aff45eeabdec658ac120fdc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
5c658aaf27bc36e83d11b661d56be51517f9ae42 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
fe9c504702a229a6cd5f8f69ee108062b9d06a38 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
DefFunRecursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
148175114adf980967121319d5e64c68aabc26e9 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
DefFunRecursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
d879faae771d1872432a468a0ed8832a267ab991 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFunRecursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
d4c7732d97003f9ceaf897563c3a8017ff8ce519 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDefFunRecursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
bca6dc2fbc2c9263b7893d7250c9f59b2773ab25 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def0 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
6f0940e3ef50b2864d90bb4c2d5bab93b3b6df70 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def0 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
362ce6c48da4c6c2c10f97c91321d6b3c2d7e063 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef0 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
3a4925effcc14a8057d907b2bec39ad214650741 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef0 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
eea628ed4e5d40ea82eb3b3c8496cbb5e1eaf36a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def1 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
21e0692306286c392a755a1ccb2e8ef3bf101802 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def1 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
09dbc5158154b4ea3841d8620cda1ece12c724f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef1 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
e14b49b7137ac711b844856cdb9b50ed04e164dd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef1 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
7ce48af7f6577b531e8da356ebb3693ef91484b4 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def2 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
73851e03531ce3310850a15a7ee925185826574d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def2 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
64d67e20ff7b7dcc6e872dd0c80bde5586c79f33 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef2 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
460e25212e66a92068de11a67f600cbf5ab8636b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef2 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
70072c1d261301b9d06d2b3b4ac71e7c4628107b TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def1Recursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f308dc4b1aac34c6d2d25c139f7f1d516a5964d8 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Def1Recursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
7a97430dfe863f60d46e81ef335862d660da165a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef1Recursive FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
c63b43b2ae93a565a5971aca9e2a91bac13f6080 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
LetDef1Recursive FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
5c18f4e8a4849021d8043aecfb8deec6d2a7af19 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Extends FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
e99029868d67cf964a40863df4cb1d44644d76f6 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Extends FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
901fa2889e6c27f2e25cbdced1ea19429dc30fde TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
ExtendsInDifferentFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
b5b39066c361a6c71de229703597379a8580cd28 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
ExtendsInDifferentFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
9dd563bb65a447eebb78863d8c628de6001058c9 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Variable FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
8628c5ef91f88a8661eb6ff295db45c6893d3d3f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Variable FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
11656944b6b5033c543ec47309433bd2c56245a1 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: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
VariableViewExclude FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
a2d75d4367f743309ab2b6e115ac9fa24dfb27a1 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: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
VariableViewExclude FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
677176c770397b8ea4f487eb50e28a2e5fb87088 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Constant FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
0aa62e3042f2c6898608d52e4624c29c0cc4bc61 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Constant FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
e9cc7e60ac90dc833dfba9905e8e75b745299b35 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
ConstantRank1 FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
ecc0b06287762ba959038428487975b484003d02 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
ConstantRank1 FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
e5ef6dbdafd858f76a27f8e77b81b5cb8a2e7c3f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Instance FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
340ddd92aaa8a691508c5bd10277ec5f0956456a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Instance FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
897f9fe0bcbc60bf12b0a55a0c88a2e4660e1ccb TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceWith FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
ed5c76336f655da44b14095a33437416581e500f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceWith FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
5c7b66049c75cfe99190ec058cbf57566c4f4adc TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamed FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
1689c03ead056f6d956aa79e07ddad8d1c9f82a1 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamed FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
99b53787fb0ed508d03f31db27ba6c1f4b26e3df TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedWith FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
4e82d59d5c48f3743217e75ef57102f5cb884d5d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedWith FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
748147525eec33b9a2982216ea344be560fbd5a8 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceInFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
8209605c6a0d166c0733fb7f7e4ab1abd3f63aff TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceInFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
75355816d73cacc4dda42e00da1cb56b526d8126 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceWithInFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
8454ebeb894590e8ef1a1a45d1426f60ce0666a1 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceWithInFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
58fd48877d4733b2518d7dd6c80bd948df6f381f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedInFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
a172352c934f6458d8ff83c01c646a2f975074d7 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedInFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
bc280fb41206e6009441dbe95783947c66910035 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedWithInFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
4f21433339461686d86ac170757e01ce5ac72ebd TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
InstanceNamedWithInFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
13da141377626b01da382d10349c9c1f20a44131 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Enabled FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
c55bab3ecd597e2a6af58c65e60b58054c39cf92 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Enabled FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
f9e21eb5fa88931576ec69275ae6a07b6410aa7e TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Assume FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
d0c6f32fea16d309c012bd6727ac6a2a55629d0d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Assume FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
fb2fef8eb69de936a063915c1a355fe894b392a9 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AssumeNamed FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
3153748bff6ab84666118245c2ea0e86af4cec4a TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
AssumeNamed FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
bfca393c69a91a7336e49655c7cc19f0d244461f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Lambda FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
cce936c6701ae43d0f8060145bd261044db5dfef TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Lambda FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
416ca4e8910fcb9275aed2e6281938b96f56b82f TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfCond FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
261f3d400205d6c01ae8491b9e6d567dd9e07064 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfCond FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
ff1f9cd1b14e6aee65fb7bae9519fc4f795fbb94 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfThen FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
570a65ce2086bd3efa6d4e3d287f7c48efaf8014 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfThen FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
a5189c310c75da7f05fea4338bce8c788a19102d TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfElse FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
339e1ef22cf320215ab23470a9e8be678c8fc0e7 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
IfElse FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
d3330548ab08d6b5195a20c8b72507eb07a2d94c TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Unchanged FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
0adda875c19ba0c50d9061c92a3b7308af607de3 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Unchanged FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
d180adbd06bd5ba1e7a04be3a3d1108690423017 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Equivalence FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
add6b46e22e133acb832de4479f9c8190d1d2adc TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Equivalence FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
236383e2647e8e063f55bc4abc371bfebc7c3240 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcSingletonFun FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
e9296e641cd13aa33cae1a8fbfe5c3d99e81397f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcSingletonFun FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
3cd1e6588ec114e494c72a010fc723b038c39152 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcEval FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
fff84e45bed951a3221991201cd0f6f9a0c89e13 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcEval FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
0a3fab7c2e7d661ae6a08da562b563b22e56e6a7 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
BagBagIn FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
92a91e75b48a634aef3f9919d215d4402445360c TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
BagBagIn FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
1f8d4632d9bf07598ecd06cac05a0674062b7223 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
BagCopiesIn FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
2bdb73f4efeba63a2bf6c868d9695b33bb89dde3 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
BagCopiesIn FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
e058605e6019ae7d49b2ac132e16e555ef5d5fc5 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
SeqAppend FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
552b82e97664f8a6e4f7458271f26bf5a9cad44e TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
SeqAppend FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model