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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
4f7ca26c505f244a121f61d8e78c58158cca531b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f987a74cc4c995c1885872cda735527645ce625b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef0 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
2c71034e132c870b1103eee631dbbabab7aa6df4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Imply LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3dc06e9ef7100c4686b1cb038dbf659d9ed3040a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Imply LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d42e22894b4538046f84d64ee841c11ad43aab04 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
9fbd8698755ce75ae30d3a75948b3af2c70bdf3c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
cc2627a54912af0af2bd28e8222592729c3ebaac TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: LET definitions are reduced to global definitions
Or LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
6e7ac9f7d923bd34ef17a6cf3a63a7ed2d7ccc91 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: LET definitions are reduced to global definitions
Or LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
3a20f62dc947b2a8815328a9e092cf1b1291eee3 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: LET definitions are reduced to global definitions
OrMultiLine LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
98dc6097adfa9de5b7e56fb1ef8f4ea5ee848656 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: LET definitions are reduced to global definitions
OrMultiLine LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
db5fbca5be5882372ce55486a83babf0442d8cea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AndProp LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
5df6e902f80826156290c8fbd89564f75749cad2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AndProp LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
297e429514e63ac1cc3d96c79b2fce61f6ddb1a1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Boxed LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f748ef89933ce74001770331e80c4cac10208706 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Boxed LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
cb18f7a10bbb44c2cdc6ba6aada9ed90ca5cc443 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f612a96a763d85f1a518c850ae3ea5c85b1bc126 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b3af95c5f4bf104b4224a7d9206a0dbdb5a03c1e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a9295de3697348fa931581b5463eaad11f18c07b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e3d3210278e3cabf3378f074cf17e506539ab120 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3043cd522b14362d6482121d66d5463d8b265a5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
45468fdfed6b98b96055a5be454ba816762cad49 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
62071e37121b865eef32bb23d0ac3a4542522664 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
fc2b0625295e78aacf6476473394906012d0f212 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
933b0119cd99260745750945d3b5fea56b865b06 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
4284dad668f13557a993e36d14e7c0d4ac65926e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
ba007b696ed1161d9ddffeb373053df9b63de7f2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
706ce10b8fae374b0b3581b8e4226b0fa45fff5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
d60b500f937d9a1e106cd85a01d1971e39696b75 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
29c1792fc93e5ac3e54bebb8c213e5c60e3bbfa8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
ec2a8e1875f4b36bfc5fbd207a350334b32f18b2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d65172931a2725909b6c90ed1a400f3b6994bdf4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3c905c70b79fec7077a322735bfffb6165d13a88 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
a6d584f4791c3566826ae3bd5237a136a1e0e342 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Exists LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
17a520bcf3cae1e08efcdc6348a49ceabb4d9e1a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Exists LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
66579749c168227a2f8e15642c332dc57e6482da TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Forall LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a060af23843b0bfa40e9fdd6cddc538e03e6e368 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Forall LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
a0ecc9911ca733e59d4cd2dacf49c88d0be649c8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Choose LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
9619ce95d744020d8948a239105c66dc923a8b1c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Choose LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
03cc5cc13745bc542199ff6940a42b1660caa7c6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
62117a7c70c72a2c52bd831705a314db9ae4fb11 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
c89ad70f5909d1634a4858ccaf0f5e71d03eaa7c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7f645432c8f497ceec16e5709e7f57bb778eaaee TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d398d33751cbea07cb84f3eb275f9f0db9a5c190 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f6b3656b47ce3d6d578cabda36e463466c543f12 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
158f85b7278fa76eedb6c7e08d9bb6cf2839cb88 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
89265aa11d8fd6432d29cd3c8bd50af6165302e9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
01c1681a353010cd1aee76b668e3e3fd0b44fcb4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3444e9bac2ade5cadd40de792dee67455073e15f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7f96621b5f71ba11d382f8780f908f297546af76 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
55a498c5bf3cdce3444ef7b50af7bc9edef566f9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
0b27128f5f24fb1b625f3a4de9cbe8c6547b476c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
ab462e3df338d622b709e671645b4985e2b19019 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
86721c093df02d1f8e753ee5cd73759ac82cabe3 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2c4cab3022ee9b155fe43c3b05c7634f7600a32a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
0c1efa83f9e4aba17d571376691e3ccad325d0a4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
53c07ca194df393d09b2d6d66b11f29311b1383f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
a42455c2b8715e4cc59c97c31f0164c239c47c19 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2FunTuple LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
0dee49ca859225cb8e9d0af44e94fa03b6759a72 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2FunTuple LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d18c213cb18ab9bfbe4bb6f8a512a7686e085e32 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
6da1169f1d44ff305bdfb40f916cfde3988ddbd9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
410ed91e5b560e922f4fcf29af6bbf0648b0206e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumUnaryMinus LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
1644e7b9def651d2930306f8d2cb0c931979f97c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumUnaryMinus LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
936b684c06d7340b14d647c5e6f0c9c9737686d5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPlus LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7a43bf730e3740f2f34565d3fb875215f6b4961b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPlus LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b44507507f9ad3865a9a88e3d7e708f02082dda8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fd30e4c9770d30f0fcbd49319a60fde77fa5b45a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b7c1b97cd6ee146fb7cd285ae6d623e6b49c3c04 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMul LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
d4820897f63e588c072c0b2285ac3918c0d24ed4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMul LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
20dbde3afca9f166215c9f406a8c43e328c04df6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
551fedb5faf41c0702e7e1112dda6fcf076d0746 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b2b8e2a3faa35c730e0d9af2e7a4579640202215 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
8b2535a4ba27f4c42badfb7d329695bfd3208f1a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
5cb322f34b5ef0119d5056a8693277e479388879 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
59f24b5eee2cbad24bc040b60e54032c2326aa03 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
553d4582a39f0aa92f7c101cdaab0523c0ef1da1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGt LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2d5958b56f23e8c5ff49096aba5ab3a8c8ae6646 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGt LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
9cf950fd7ef94e82d241ee8684e533af287094e5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGe LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
91b21c0918b188c39383a609eba0ea9149d4ecb2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumGe LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
be5cc5bf9607f3a71e70dfafeca62c33ed95b312 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLt LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
99396d738cf497415d8c1486417b34f06d29fa80 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLt LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
34d4d768b0ed66111a7005de050bac80688710f1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLe LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a4effaa09826be6c24afc55953fb3efffdcec223 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumLe LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
77d2ff302fac7e73f0ff1a9cda9dba32ee719d7e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f3c532fa7919f4e53eff217da0fb8f465d5e0512 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
06f8e554595a52f3e6e88c1e3b8db59093e797db TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
66bbd3c0ff6461ed274b178719c76ba3d58e678c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
304a4e7e9bc8f6b176ebf8f37a644c8c72e4d882 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e8e7b392471478eb75c423e557b72d21cc2ff6ce TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
02a2b5a44178ac4c68941fae50ed6a9351a202c5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
c1b25ac230bce711efdb2063005af94e3f42883e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
72976850c01bbda339cec6a05745db6f71a3cf7d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7c58658231cf7aee1fc87e451a8213a480883d26 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
6fa34718e9698df40031885bde641c27dc9b7410 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
dd3ed2ff5d879215f31c38170449c9241ef41f95 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b16bff2e7eae1c1fdf242bcb65ec0eb30a01c458 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
71422bf59e16f643180bb392713792c264045b0a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
6b16de1082d98ecd3c79ba74d2f5e3f47a58ede6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
c04403256589af8c489f6f99c5b48b83f6b26549 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e150b1994b29261eb5a26753c27a382e6a320f1c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e6c8c03fbd4eedec04de3fb16c449d310530d726 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
02c4a584b382523fad0b5c61d44ae12a27062789 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
5e91c605dd56dd8a4d04ccb5f8512d0a47ea11e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e8d6f9a02a56258740b89cbec859ce25d4fabccd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
eb073ed5399e2478d26c683bcb83eadfb4d9d9dd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7b4d4033c17326a4a9cd5a669e765fe901dabd5d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3eb7488e93ecfdeedd03b70afa78ba27fe3ba308 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
3bf8083574989ee37a54d29b73855352df2dbe06 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
49f7d963bd5f64ee0c424b035832f8f052a9604d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
8bc8f9a22e3302ba03e0a88934b4be19f4c8cad9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
89edb21aa6d41b12d836db3bfcc5b7a791e4bf6f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
1b7a0df2533bcf8eba8fd3d57e64c4d9c9793900 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
d490fb003ce13c15ed501ab51a9d97962051facf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
88d082aac06e05e1d8b34be01a39cfae8d9a4a30 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: LET definitions are reduced to global definitions
VariableViewExclude LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a8a5268351751b4b232b7649b6d91f5c869d38c4 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: LET definitions are reduced to global definitions
VariableViewExclude LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
6ba58c20f166d9b2c946223984fe932016a357fb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
c19c025189ae862b7c254dc1ee3976ed12d48294 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
220460d8e45dee139fa24fbf3fbe1cd377d721b6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
ffaa1f761799b1e3d88446e34b95907e0de52cc4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
cde00abb4446a66f16e12f2d102294744d99baae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
b12154522d052bf8787f41005f9d63688c4dfe9a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
f217c4e4c6b8cefd3f90c619057c9e9654404ca3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a3f59d2d3b4a2954492a79b948c433f63e45593a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
9762d19d11a67f40883afa59d5f3e1cbb94c5ee5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a1cade250705791c04a779e7e1de9a6e35e8d71a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
35a9360c08d27f327121eb0954f08c2510603e98 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
639227a5fdd37a662b9aa661bd8beebc9981c753 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
dbbd5aa455dd3113658a1f840f6a9f63bd66058a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
0d861eacdc50e3f6737ed7bb2d39dcd94128182b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
3acb384344aa20cf963493caa7dc072ebc0b669e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
d9214530ce35b2a62cb7314fc2c52885d50afc03 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b36bfae187548a910596a2c971e53278310759df TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
8802b55472e17885d45d880c928dff1234b984ab TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
0ea164dfc6ec94d31d1dcadb0c6c9741377b37b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
05f76cb89ff613ff0a161a38658723798af6d842 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
1e81a9752e0daf4a2841354fde3e187796030d9e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Enabled LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
01ca6d6a9960fbd01ab087d9ca612c9958b3f948 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Enabled LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
077311c1999faa37a5cf410cc1ed5c817ee48662 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Assume LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
b42a31ebb559dde38e55a797362070a58b1bb126 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Assume LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
f5cf721e742158b9fba23747a0b568a34410f558 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AssumeNamed LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
157dfee18841817b68d664419e593d1f99c9fa71 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
AssumeNamed LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
9922d82ea7173e762e2e989afe0807ba64d03c95 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e01f86a296d09584b56d0ed8c080a09602c86549 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
1b444e9e63ca0ed6493929688da2bbc7ddd4758e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross2 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
8d7da18b66497590c1a14af59ca6f950cd27057f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross2 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
a09cd86200e827d7ddc76d833a45097f20263a89 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross3 LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e64746f571ae74839e0a10517c7987fecccec53d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Cross3 LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
268f43ab80cf217d4c5edcad3e603b69bfaebe69 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
  • Plug Feature: LET definitions are reduced to global definitions
FunSet LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
0540723223eac3c8371093cfe65e0762a89dc861 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
  • Plug Feature: LET definitions are reduced to global definitions
FunSet LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
89df8873fcd7def05debff7491306f42038faeca TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
  • Plug Feature: LET definitions are reduced to global definitions
RecordSet LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
712b341ba91960177a675eeb733b4248866de78a TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
  • Plug Feature: LET definitions are reduced to global definitions
RecordSet LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
687a57397018fade20b90a617e951ca36fbfa00a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
31b936798ab75817a8b7a8895e9dfbed3d0375cf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
2c90c185aff54a254102e6804fc668a604acaf0c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetUnion LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
794ad744ff8a682b90465d002f9bc8a86106bb0c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetUnion LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
43eb5a13725b28d5246d448eb03e8479b5adf135 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetIntersect LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
b60f5a2310ddfcd7e907cc00e86ee69d3fea2ef3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetIntersect LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e992552ed10a4be0693ff3dd9400272ab53868e3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SubsetEq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
0c16198ae48dec71693500ee14452644a281507a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SubsetEq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
76d04b2905fb69b65d9bc491c462cb1829cc0876 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3226cb4e0bca038c2bb8ac5ef3045b70ce34ae32 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
70320147be06b5bd5c41606615373503d917d5db TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
67a398e4ecab0d5af4e90facdac50b1886072ce8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
5dfd8b147ef8248197ae7b86bda8650c6e626d40 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e0f0e09792fc022039e66f49574f714a167decf9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
2e769c061a72501e203b6d534278e775bc10ca52 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
b06810b75c7d8df84568df2cb78458cf70c4e9fa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
69dc0045e5cb063274ab0af61993117f4f9a4627 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
49040e40ee967f4f32675368146b632e4f26aeb4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
c621815596eb791e3719529ee05498e5338d4cdc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
5221ee1ee658157cf35c3688c14082eb63692982 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
36fc78817411522e3967925f5371c6bf1e08604c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f419f75565a4fffca9749f6c1d9d7e23ba140ec7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
9a9242a0849a01b72e948d5ba5841276ba7321dc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Equivalence LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
1f59d407d6dd1ec140d459b021ba687703395e57 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Equivalence LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
183c4f8d8ea4e771b454fee0bdd6107e4c6beee0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
23e0b63acd2c920e6552dc427ff7441ad98d9071 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7378bdb8410120a56d76ae16ec74fcd9e41ea391 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqConcat LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
93a751e55e8b21ff966cfe56dedf75bbcd1b6b57 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqConcat LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
dcf34520e8eab4094332194615a3a1224523f686 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSeq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2ca9b0d3fd8a0c8aeebb6a16275ca9ede96118b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSeq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
da646df2eac0ecf0f3b2f4d5e70f4b02ff2c6f5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSelectSeq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
ddd7d53f8af3c3fe4740084e7a51bfc384891ffb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSelectSeq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d93b1e15b4febeccaaaceb1c58c33899f5e96053 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSubSeq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7b8bded5feb7525b85f09a92fb8195153ea255fd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqSubSeq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
ccf8cd5e78d8072423c172dab66d48513fd4ed6f TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2c9d27907897e8de1ffb41ec7711ad0518487588 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7126b5f34183bdcbeb98805f15a3f4fe579dec09 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
dc97071356a6ee4dca52130d5e557f4ebb6911cc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
c9fba643e410fa824c96263c9f5c7711af84b413 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
e568ce79f8915c60f821496ed6be343450da226b TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
8286112fa5cb033a55aea17520b429b4a013c9c1 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a5a6bb6546ddb57ee4320482f02bd2f88989ffbd TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7665ad68d5505a0edff5f032d297816b25bcca8d TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: LET definitions are reduced to global definitions
TlcSortSeq LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fead12dad7b0a0ac7a671a6aedaf8507776e1ab3 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: LET definitions are reduced to global definitions
TlcSortSeq LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
8a063ba0f15c347573e871efec8cf3ae43eeaca8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
8926a21adc570c61365050605e36f963deac172e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
10687f28bd857a5f1e615fab7887cfc9b09d162c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagToSet LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
62767b2b3fddd2049fa37bb83dff67675ebd114f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagToSet LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
a2dd31f0e0ee087f036f5100e50d49f54cdad39b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSetToBag LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3f6dde82a71a35a2cffd852b9d692ed67a29cfc1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSetToBag LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
99c0885221a34db80353dc044702a99b6bb9be83 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
55f386bb1d78e673eb4bf1acd7e73a8e615fcbc0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
62b84c8886c11060a2cc35a98039271c95cd81df TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagAddBag LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
1cfd998aeae44ccea5ca9437b48c4556ce33e17b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagAddBag LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
909c4c22b62c7bbc2f3c26b12775204122ba7d76 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagSub LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
79f5f0ff4be18c08d6253fdb6ed98c5f5ed37cdc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagSub LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
ec8a1b540ccf3add5894a120777f6b36f5b362f0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
d60e267dee738dc3dd46e84967ea831e2526dd55 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
261d7cef2301c6af623b9fca5cbb5d007b011062 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSubsetEqBag LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
632efc756a64f5b84a0e512a0c62fdcdcd683419 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagSubsetEqBag LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
98233bb172043e221edec76b18ab044d3969d651 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagUnion LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
9e7c41dae8536e1b7d4aed03d3fcec0e21b66200 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagUnion LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
59994fe93332f162ad3a68592596fd7c5c914234 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagCardinality LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
9b7ef6ee85d5a58b29f97cabe14c0013e1d6eaf6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagCardinality LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d167f59167505ae02918c9584134ef6be49fa59d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagOfAll LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
cf09e0ceac0cf69aaddc66b1deb97c03d24e0585 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagOfAll LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d45d3088346380456a6d6eda83e19e8f07fd9637 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: LET definitions are reduced to global definitions
BagSubBag LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
82edad8fd51cead3c57221751a99e3e6b82ae02a TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: LET definitions are reduced to global definitions
BagSubBag LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
6d2f7778acb875228a89b76fc3738dd9d323d6f9 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fff93bdcc3888176fb291272e9a55d839d2eb574 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
6d0da67d01725514e0a1e2ef4f988df2634d56f4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsCardinality LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fd0ab26042f150ebf5e4754fe8274ce0fe6a4048 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsCardinality LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7a854ce0f13483c6fb8ce84104587d394d65271c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2b83de403fff2e3942b6443bb91acb552771c8d2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
416df4a48f7ffca450c137c62bccbfffea40c9a1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7831ff9c37b93cdec6517f8ebd3f6ba69d17300e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
b7d8da2b5a75b6f984f432a685fa9803696ea596 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3c0af8b97444caaf4f1a1eb1d0a2a73bc9ca9a95 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDef0 False Passed
  • Model Under Test
  • Equivalent Model