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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
28ebbde43ea69ba9ff3fbe5434f073356583b36e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
And AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5bf6b0e52cbfc93805a74870e26bdb10fc20e262 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
And AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
452ddfc706c7f0768ac31b7445bbc130d36ac5ed TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9ada0f6681676fc0d3e4d09b6184b42ef3ba829d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2166af4e30e556090f245f2e84ac087f0764ab6a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Imply AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
e7cfc59dffa81587459fab6f5d8d2c54cdd3bf73 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Imply AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
716ba9a108d71bd104d4f0ee2ec51fe99a053d11 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Not AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4a79bb923b62e11a5c720dd25e8e826e65cae582 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Not AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7a685404f5ebce0603bb3ff4f5baed5d1576f802 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Or AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7151ea0fa4a2d1c8100c68c751dce5e63bf1551e TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Or AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
01365742af7f3e843d23f99d8413235491a84d82 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
OrMultiLine AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
71d313934a1443623bb8030395f5408d9ab7e9c8 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
OrMultiLine AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a52e9b0e02ded6194b832ef9d4320e1e03dd0a8d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AndProp AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
21c2dd05a176ba21cc8733a7d3668a20b760c57d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AndProp AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a036bfc2b99a7f58376bbffa0687a381e1233dbd TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Boxed AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
3530c92ddb47c2812c03545c3ff195290b8db27e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Boxed AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4a6faac8cd68cb38f581f0f2786b1c1adb061fc7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Eq AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
15635b144f4d81dddfdbe8dfbc1f4139f39ccdf6 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Eq AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ea7192d813e7231eed323bfd276d724182e59cde TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Ne AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
00415bb28d3e52a00629a8accfa1a42bf79d8719 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Ne AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
040790120d4c3ab24af47ab00381776b60b8a6b4 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ccea67a010bc7fb12ded5345dbb137aece52527a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3824a891d4f104c4031d7e4dd2aa83b7ba15b53f TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set0 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4822be4379631319f18e361b1b8136d8de0d8e45 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set0 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
db42307c19e20e67baa1f96b564507668d930ee0 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set1 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7c572d115656d6a0a0f874e1fec2afb5f245e0f6 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set1 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
be452db73c83632fba375cfba2bc0613d44768a7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set2 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7ad18c88cf14cc1a73a6de58dc769c8ca37c64ce TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set2 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
981cc72fc963ab4203f81e48c186582019790c38 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Fun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6915537b22020036c2deb12034a5740ab0b212a8 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Fun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
16fc86ea87cbbb64604bce770acd2bcdca69a82f TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
In AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
b3354d4f9e7775220f8063a755982dd7ceb2e6e1 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
In AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4b89e56a5a2ca138d467700d907890dd13c5be20 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
NotIn AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
a5b322e141b6d86b3fb2a214d9c56c9655311e6e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
NotIn AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8636c774642e823c7b946d8fd70cbb84a97bbd00 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Exists AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
1766e75b122742fdd1bef416c53f3f6dc014d52c TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Exists AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
0cf1f2a6e1f22944c0fb3796a08b6aabb2109956 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Forall AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
b9c73d82c3b949908518a3c82b9160241a487217 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Forall AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b901efb568b733dd714bac9e694455954bc40633 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Choose AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6a342df13539c791f208c8a26ac5ee9901be7b12 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Choose AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
83fd1741fceacbd0fbc8b5b9077cef406b044048 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Record AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
031946ddf099a0103086caad2a614e1120740bd5 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Record AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
b9b1d4dd33cebb0724f2382d36b93925655f4ce3 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Tuple AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4212267e105c67ccfd2b1d732f0f53ea9f05f89c TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Tuple AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6e8545802c4355608e0c5b84644db0a19bad66fe TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
FunApp AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
66348926e10cea2841d82cf669a2c90d8f961ea1 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
FunApp AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8aceef69ef647416aeab598af3454a71174a5edd TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1Fun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
3e4395aa5111436fd853c5d8d95b95d0834e98f9 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1Fun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3e9896da4e40330189e0a15d8e6a10433ac36b8f TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1FunWithAt AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
fbcc2f659585a63210e2ac25f032dea68f8de900 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1FunWithAt AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
3eae21c5b6a93f1db02257a87d2daee688c5e4bb TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1Rec AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
372371b3c778b1d426fa6d566ba4c60fb2d3b838 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1Rec AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
533ec007b2468498b0cf7bfce431fbe07b0a3870 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1RecWithAt AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
258d3787aa5007b44de8b5d927454c0e0b0ea447 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1RecWithAt AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
be6bc03f5ec034469a2c4c2fd9cb5ef5a88a076a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except2Fun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
3770235c36f017cd02c54222e25400046c3be08c TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except2Fun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6db1b01792a4dfd8610063d6be18705d31afc4f2 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Prime AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
f1f79cb3fb2101e4c6cce8add8a9b939a1da3217 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Prime AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
5242c8b4c8bf355ada3479f8192e5e97247ad037 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
DefFun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
6a87e6aeedcbdaea8e6ff65e6ce165bf269a1460 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
DefFun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
06da5173198df5fa6b7f70afc087086de96df05c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
80558a1f84a7fc37dacd6064777bc09c99004a71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4cdc4117680947896e7fc3dd735950d9522cf2ac TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
DefFunRecursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
bd99bdbc7c582df9388d4eed2edbfd65b85b2427 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
DefFunRecursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
d9194a0ce9b15acb9a77c4c6bfcc7545eeee882a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFunRecursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
c6c01a8d61c63f148e2f182c094f14eb1aa46d36 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDefFunRecursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
42b70606408da10a370f3fae087ff678f268b2ea TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def0 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5ef24d0b196ef1d96eb504dbd4fbc3d3755e3808 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def0 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c5dc2082848082eba6e2cb7e6a011f0f3625cab7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef0 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
91493098bd8f81220d2ae089015f1c446d601705 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef0 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
d1cccda168e87509554629d265387c34ea43d8c7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def1 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
eeb503cc579f1be531b544d887b63e880cb3cece TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def1 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
15350e7ca5f7524d955b3906e57ff375296c126a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
d5479b4eaf7d1378c416506e53eddba18afb9f1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
c4c957d5a5c6997e1b1d24262281840567fe391d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def2 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7b8b7a3397945e80f85f6e1dd6a50a6085017bb2 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def2 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
066cf7a3755cd12e58addefcb1b9e504dacc00d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef2 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ab2c4b6c8215a04e21c0a513db9e5f0fb973a932 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef2 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
90ac98052e419c83dd8e635e070f81193ce2e6bb TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def1Recursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
baec8af64a5260961d6d763f605d4d40a242aa38 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Def1Recursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
57207de06f836a0b47e13c2f099fc3df7378f36b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1Recursive AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
424e047d11abbc51b5aa80c5ccf8cc246e2f317f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
LetDef1Recursive AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
fe9af42f0b9c2e15887909dc86bec4ea0a78ba25 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Extends AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
61beb5672f0e0dc888e13231c4d93df161a8f58e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Extends AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
68dd73eedd2022f05e3eee279cf7619dc0f00262 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
ExtendsInDifferentFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
f49a6692352a33c4d1f7e95be39c279061af6fe4 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
ExtendsInDifferentFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2e351f497444f7df3613636f3d94494306e5617a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Variable AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8ae6c25b51c5cd18f793c9814312e132eb8e917b TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Variable AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
720c073285dc6dffa117e32c89ef844ff95e9f2c 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 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0e8dfb18f21315e5e7eccef1b40442f1819717ec 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 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
0e884d81df22b36aa5c3917557505887d402e187 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Constant AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
1269f819461424416d99ad6fe48babeddcaec2f0 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Constant AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
75d468260d311fdd64782d2a15a55356aae61db8 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
ConstantRank1 AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
649b2c7b5a1ac489fac77f9810f9802c3aca163d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
ConstantRank1 AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8aa6a92ff19c2fca8f1bc9fc7b4b87691f4688a9 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Instance AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
bf5e20338f46cfd46ee77a31413fef32b1f25edc TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Instance AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2556edc9db7d4c172e7c38b195afb6108fd76da6 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceWith AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
0dcad25f23138e4d15a87e3f28c946bf694f584d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceWith AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ad11b9569a6c4f1b72d61fd46f2e6529b6ef4a77 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamed AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4a87a1abd6d82d6f9c4c5a4c4111821caf98e53e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamed AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
338d734f058be0c044f76920936f2bb11b544a3c TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWith AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8f82178cb44c611d9846c3ba2a4e61d5a771491e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWith AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a17fb9778936e38f2ea845bd44e0e45c2449a8c7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceInFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
caf2a8ab9f82cb5d7799cea45b75a9649045ab55 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceInFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4d678f45408d78238b20044541acf1af3ea4d2fd TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceWithInFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
94d7a2a72e25fe3768dee2ddd8e473c6062bbdfc TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceWithInFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e92bfc5321510b3225b685b2ff3e8cef41f1c921 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedInFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
b3a4fbd916602ccd34288cfc1442c63fa79845f6 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedInFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
8c08e3b2ec449f6dbf03c7dbaa5f0c3f1be19b35 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWithInFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
00689f02984de5e4e77a018e564f9efa05e5b0cb TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWithInFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
fc40a23a7cfcf3b4b1a4cfd1174c6e78d8b4faec TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Enabled AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7584c8631a4dad88b160ffa72bef7471f80977b5 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Enabled AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
825ea29f35db45f630203d753cd025eb5d495ae1 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Assume AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
f80e9519746f84b68b52e7f911a0220fbca1e924 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Assume AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
75e9dda9f4756343bbba2fd9a4d58fb43353968e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AssumeNamed AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
43233d682e864ec3b456f45637ab0d82d81a809e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
AssumeNamed AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
46445949b0e87133a8641c23e5fbc244d3caf689 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Lambda AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
154d4bb5f4bf87dd5f213811d778390693820520 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Lambda AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
64a3be96f34a9e2a89e3cc63e8e5d0dffe15def7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfCond AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ac375deb815573158173961773cdfadeed8ae534 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfCond AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
538d3c5fccfcccc96573c4b9ea8df44195e05763 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfThen AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
68431bc0bc122f01221c8b4588de073c147fdeb0 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfThen AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7725ba77b7bf36797506aea124f3a8cd7c970027 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfElse AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ce11007b2a5ab6b6237f905b7f181f883ec412ce TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfElse AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ce77f0585d7f22a3faa9bacbc4f1c24311082775 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Unchanged AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ad3b7ec9cdce87c4d387b4dda7f8867494241836 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Unchanged AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
ace6d76ed1d26598a5d1b8feca21db2b45703d2b TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Equivalence AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
dcc2ad6b2e66aa7f6b810fc1f06109d59cd5e938 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Equivalence AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
619a2aef1c693bb624cd41d078b07970e91c876a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcSingletonFun AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9ac6c9ecac3913770a3bfde26ebad9a5f630ec14 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcSingletonFun AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2337288fb60b027bc2b8b2fc4b6ca9d874ee089b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcEval AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
a09a45b2a2c5ac11e35dc23868d33e9f3804ae20 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcEval AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
02d52c5e76c8c66af60036a438afef68ddee7ed5 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagBagIn AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
b29b6c695b83a88987a7d070767b10ff950a28de TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagBagIn AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
78dee6ce2bfe819f1b024fbf31ddc4767694ec99 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagCopiesIn AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
d9ac6991a4529d55931ae01e59d6276f780c296d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagCopiesIn AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
0fe0dea1c994a033b09092a2ba2e845f0a69b9ec TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
SeqAppend AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
7059aaf7cb884aea6a86bf5c1f7c9a5e85429897 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
SeqAppend AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model