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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
f2c3da97136ef70fb322ec11a1f066606f461d56 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: Replace spec with the same without comments
AndMultiLine OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
b9090aa8d87f5b087405874847cbddb5d613682f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: Replace spec with the same without comments
AndMultiLine OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
ac09633f488bdc6a5de7b4f29dd5c1178a1a6732 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: Replace spec with the same without comments
AndMultiLine MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
d6dc30ab27466c025de4222f16186a4174662e66 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: Replace spec with the same without comments
AndMultiLine MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
8004609a22053f80e20ebb56a9ebcf8e3f1c5add TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
f38f88fae71f1334f908d685e354615fab1635b4 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
9fb8920de1e19037d8891e9d7cf4186acfb2ebd2 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
0bd45bd0a3e024a6eb9e3671033ea741ed632a7b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
3b0f9b30dcd7fa9aec1bbcce8af69dd5954757c9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine And True Passed
  • Model Under Test
  • Equivalent Model
30db4bf014b0d23e9e18b2d1c8f864e28128c697 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine And 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
2ac4f878797c10c839fe3169411f7832a44c1793 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Imply True Passed
  • Model Under Test
  • Equivalent Model
f59354b3e43d014117ca992ebd865fb9be254673 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Imply False Passed
  • Model Under Test
  • Equivalent Model
f32be84bcb25b678147d2bbe2fa33ab5e139e0f1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Not True Passed
  • Model Under Test
  • Equivalent Model
fe0d36f35fa3a18fdaf969c095d824ca0d1a790d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Not 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
fb214610ff44d6a73ea785fd0ad3fd3e5d5fcd50 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndMultiLine OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
d34552136b61da264a1cbc04f8da51ece73482b3 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
AndMultiLine OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
acdceabb0555a7dba2c3e820021801563a1478bf TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Eq True Passed
  • Model Under Test
  • Equivalent Model
88f211f367bdc2c0773e80761332e649b6528850 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Eq False Passed
  • Model Under Test
  • Equivalent Model
8c00add5ed3440c3120041f6027ca4be3e082b24 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Ne True Passed
  • Model Under Test
  • Equivalent Model
fa375fcfb03641250218965713ede1315347ed65 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Ne False Passed
  • Model Under Test
  • Equivalent Model
a4d77a5af8d20fb01dffcf8fa65392cd878c7b1c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Let True Passed
  • Model Under Test
  • Equivalent Model
b2bbd1e4fbda3c2c934b85696806f2d305691470 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Let False Passed
  • Model Under Test
  • Equivalent Model
980caae626e2a6ed380ec18fd5e373284c51391e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine In True Passed
  • Model Under Test
  • Equivalent Model
8b1651bdd2b21c1ef98cb337e037f28cfbc00b3b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine In False Passed
  • Model Under Test
  • Equivalent Model
3143207a1048ebad5102a402902dbcb4143635e0 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NotIn True Passed
  • Model Under Test
  • Equivalent Model
0b8d51691c5865bbfdc5aefd32d6a72f4fa78bef TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NotIn False Passed
  • Model Under Test
  • Equivalent Model
2895119d8fb523fb3281cc62f11e1f47a529346f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Exists True Passed
  • Model Under Test
  • Equivalent Model
15a026aecb472ec964759506a0906d1761cf36c6 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Exists False Passed
  • Model Under Test
  • Equivalent Model
d075a52aa7f7e912e183fa0311eff6b09f44c7a2 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Forall True Passed
  • Model Under Test
  • Equivalent Model
9d2d7665ab38a31176307c17790b96b2b9ebdc6c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Forall False Passed
  • Model Under Test
  • Equivalent Model
3e44950b97e2dd0b9e25b419b33ec5cde67f65d9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Choose True Passed
  • Model Under Test
  • Equivalent Model
381daceab3677e92ea861892b78b6299cac34395 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Choose False Passed
  • Model Under Test
  • Equivalent Model
3b078d8ba9ca3012b8cf18e24299de44d7b94fe7 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine FunApp True Passed
  • Model Under Test
  • Equivalent Model
deaae78b3e85232f4aa9ba79d1a8fed51e05d139 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine FunApp False Passed
  • Model Under Test
  • Equivalent Model
a57e7fe5d0db9460f264941881bd3a570d39a5ed TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Prime True Passed
  • Model Under Test
  • Equivalent Model
60d4299d5907a548a2a4b2f0185de9792c9fe3fd TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Prime False Passed
  • Model Under Test
  • Equivalent Model
0dfb6965b5d2d0df67181f7704503014f451084c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGt True Passed
  • Model Under Test
  • Equivalent Model
894290d42a62ac554ddba0de015253dffbdea020 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGt False Passed
  • Model Under Test
  • Equivalent Model
1d75fc45be9c0965f11801be6f9d6904f5f8dde4 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGe True Passed
  • Model Under Test
  • Equivalent Model
19c7f0b79c44ae2deb959841ad429fdb551a00da TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGe False Passed
  • Model Under Test
  • Equivalent Model
6c09f7599e00ed307aa3f9dfca8d9db14efbec9e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumLt True Passed
  • Model Under Test
  • Equivalent Model
aaab018c611942fe08e4d2410aaeb877d724429b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumLt False Passed
  • Model Under Test
  • Equivalent Model
f075b81eb2db5b476a6b7491f5a98eb0d083650a TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumLe True Passed
  • Model Under Test
  • Equivalent Model
d072b4b9eca84fa78b81f4811b92354711a9ef55 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumLe False Passed
  • Model Under Test
  • Equivalent Model
f047a721c3f524da05c9432dbe981375b8a4bda3 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def0 True Passed
  • Model Under Test
  • Equivalent Model
d959057a7a7174a9149529b4506d45b2f57b77c2 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def0 False Passed
  • Model Under Test
  • Equivalent Model
c186db44c3ae108c196807ecb80e951552050b18 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
1a42ab99f2855979882e5cdd67c5a200c8b101ac TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e97582bf9a63976a71de9b9ffac5459da5338af6 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def1 True Passed
  • Model Under Test
  • Equivalent Model
d128f73e0c4352b7ffc9d2fad7754145333b0327 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def1 False Passed
  • Model Under Test
  • Equivalent Model
633fed5d29b3be919b3d46bb8605feb431adeeb2 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
00716a25446ff30a78f4d168ffe1611163e31301 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
d4e06baef553664c4c41646bc4132d9863ef65e7 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def2 True Passed
  • Model Under Test
  • Equivalent Model
99983b509d61c3480182bb40e025aa154c7fdde1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def2 False Passed
  • Model Under Test
  • Equivalent Model
7e1ed117833ce2b7a7ec373adb2e57ccde431f48 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
38cddd79dc01d496b2b2d6d3dbded0e646335bf1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
0f57d3eaed3f37fd0bdde593ff10eeb49fb37a85 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
b39ef5e7a23d7f82abbfb07050ff55f37e88a111 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
3d4298fd412ce12581e969343e42ef332b2a2b1d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dd203653c9d9872b6bd2c756d0207bfa719cfd13 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: LET definitions are reduced to global definitions
AndMultiLine LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fee56e2c974c7cd8dc36d2c1d3274074dbfe193a TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Extends True Passed
  • Model Under Test
  • Equivalent Model
287c1e577d5827224cb2d66bc460266ccafadc69 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Extends False Passed
  • Model Under Test
  • Equivalent Model
ed7eddc202a1d13b38da92954dedfa6b8596454b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
5322f05050c15a8edcd0a2be5ddc264b41274974 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
00cfd3ab74590028ee482731fda3fb272b2a7a95 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Variable True Passed
  • Model Under Test
  • Equivalent Model
2b529315f2ce79733386a3dd7034b37f30bec50a TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Variable False Passed
  • Model Under Test
  • Equivalent Model
c8a7a08493833db470fb8163cc959c78c4b01178 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Constant True Passed
  • Model Under Test
  • Equivalent Model
9c91a0317f4c4a1f0a214d8bc96b45245d5675d1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Constant False Passed
  • Model Under Test
  • Equivalent Model
fd778bb0029d4ccf1b88318a26f5fca0d8808cf1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3113f710c346730e825ef53409ae8c0db727ba83 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c027ff59d61d9120e19d2d64f84b07eedd67cd0e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Instance True Passed
  • Model Under Test
  • Equivalent Model
b1664b39579a59d030c02d89b7426dbaeb2cf07d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Instance False Passed
  • Model Under Test
  • Equivalent Model
a09721b75b35c97a122e4fbe066def6aef67549b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
95a21e3ea82e7b4334298512f651c9e0c4c06901 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
a73b85d6046af86f899d1e82b583ac889941efc8 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
733690ff800b973935b8535e3fd072206525484c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
98d5fa954bcc5d0ba01b0fccff2441745db4c14c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
92ac3ecfc3215e3198b23f003deccc198620c25d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
5cfd8e1024773fd0f159f3f94ad57ab1df93e4d4 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
794868b1f9bf640d1defef599627cf777b7e707d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9cc93938d7081cc2082dac686df77f085b994aac TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c534a7ee17103a32e34567f5c499abb8109abecd TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
5c22d7c27e5b05256a57cfa00ddf93d7259d0a39 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
7c05f1fd69fbe64cca4babb8c4130f7beaa22567 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
703f0c257ba37f4d70142115f8029952c24d0228 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
758351a528f92a2b056bab227ec3fc6818534282 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b9ce2a896a273827551099e440f7c5dc7259307d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Enabled True Passed
  • Model Under Test
  • Equivalent Model
91f37ec336d8e31e8e8b59ec07d0987c77e82609 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Enabled False Passed
  • Model Under Test
  • Equivalent Model
468b08c81ef3e9ea45411bd83957fd833c85505f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
e914847c456ca3d7e2ac11f092bab3119eedd11e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
9843a1da5fc5dae1d863dde765086d7adfbbe22f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfCond True Passed
  • Model Under Test
  • Equivalent Model
a582ed1ada7c4a63ed62178f8ec29f79d310f6a7 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfCond False Passed
  • Model Under Test
  • Equivalent Model
d0825be062af7674d7e6418c65710d917b260505 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfThen True Passed
  • Model Under Test
  • Equivalent Model
5bcc82d2f98a53898bf27a1a298b268dda72898b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfThen False Passed
  • Model Under Test
  • Equivalent Model
50fad3ddd29b66a10714428d021eae8c36a243e0 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfElse True Passed
  • Model Under Test
  • Equivalent Model
9d404faea7ff867ab7a4436fae1582986b0a13e9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfElse False Passed
  • Model Under Test
  • Equivalent Model
56e9bb0e5da832b2707fc98d20352a31b3fe686b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Unchanged True Passed
  • Model Under Test
  • Equivalent Model
e380fbe9c82c8530d911c34a5a81ca4b2ddfaa10 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d3c813fabd7097faa8e7f8c70ba54c044f0d6324 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Equivalence True Passed
  • Model Under Test
  • Equivalent Model
dd6b933683a274a6b3981d548b02539e2d45dfd9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Equivalence False Passed
  • Model Under Test
  • Equivalent Model
8d655f49a8fae2e9029460a672da9d591a09b684 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
AndMultiLine TlcEval True Passed
  • Model Under Test
  • Equivalent Model
d86bd9c7635792e009f445b4a5419a362052f03c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
AndMultiLine TlcEval False Passed
  • Model Under Test
  • Equivalent Model
1e277176ea3587c0985bce12f063f8cb50e87d2b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
4ed928469be561f5365e9107d312ac3147b8445d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
d9eddf370a2cf7d27d9d62b9a352c49d28c20861 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
ad13e4967849b22c5de21548e09dab431c37d580 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BagSubsetEqBag 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
5df9e18740e3de073766419123217f4f503bc440 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SeqHead True Passed
  • Model Under Test
  • Equivalent Model
7a675f6bf3bdc44f5148bd03afbd706ece424de0 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SeqHead False Passed
  • Model Under Test
  • Equivalent Model