Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

Tests by plug feature TlcEval; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b6123830170a3a151fb060bacd43e2f7a76ce53c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
And TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ba63e80c0bbde8f95a0504a9999bdbba475ccb40 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
And TlcEval 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
538d0a11de68256521c98734bd55124f5a3bf92d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Imply TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2818b40e58fafe144a5bbac4b10beefa31dfee33 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Imply TlcEval False Passed
  • Model Under Test
  • Equivalent Model
46d341f198a078d376f09babe49386c5429b3a3b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Not TlcEval True Passed
  • Model Under Test
  • Equivalent Model
183fc80552eeba56ce7d8dcb75bef58d6ea97a4a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Not TlcEval False Passed
  • Model Under Test
  • Equivalent Model
d261caeebdbf12d9f2783fe3e86e531767511d36 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
Or TlcEval True Passed
  • Model Under Test
  • Equivalent Model
b0cb26bff6d56332e762abe75b2ee9a822d5e18c TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
Or TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a756e910690676e1a205b4430f2a28538a877c65 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
OrMultiLine TlcEval True Passed
  • Model Under Test
  • Equivalent Model
68a35d515cfac8943080d63081c4c3635f71f24a TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
  • Plug Feature: TLCEval(expr) is reduced to just expr
OrMultiLine TlcEval False Passed
  • Model Under Test
  • Equivalent Model
61feeb6995a5b8d7387ffd90993cec462b64ad0f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
AndProp TlcEval True Passed
  • Model Under Test
  • Equivalent Model
bce6ce128893dc3b64c3fc4b17d2e32212f8cd98 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
AndProp TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7996a17cf1179191b80a9ddc63e915a3210d31d5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Boxed TlcEval True Passed
  • Model Under Test
  • Equivalent Model
edd8c8c31f154e9a42e0af5aefd9bc7c152de8b3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Boxed TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4d7fe267a3a5fd8c8df5099bc9a54695f6951ca6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Eq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
747a4be5915961bd911fecb92ef54d354db18fb3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Eq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
fae71c0a7dcd3cbe831901c8e352ed8df4cd60b2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Ne TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e24f56bead7ce71843eca2bd30729778833545b5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Ne TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a8fd05265f1752a6b1be235dacbf1c854428fae8 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f69af7561d7b8ffccc368d43740eba1f159ab37a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ebe64dc95545c06eba1ee61cd122959cb57d3bba TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set0 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3e634dea6b40adbd234d7f00365565a98282b198 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set0 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
444e1570c5a4741c8f5ac48672372c2450c71f31 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set1 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c18b90a449723b44f2f64bd02c1843b84aab3c37 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set1 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ceaa8eed41e731d6c2218a0be5c7eda32fb89e28 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set2 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
731414a6df0dc6d0bda727c24f81507d53e87ac4 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set2 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ac693e1ee8a39346a6d7c739f110c60da17a82fb TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Fun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
7abccdfe448b6010fa940141cbe711d913c7f3cc TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Fun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
53a26c9d2c5bf67e93b7275bcb93e3481c17f42d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
In TlcEval True Passed
  • Model Under Test
  • Equivalent Model
9a15e016b36e38885c3a4042e4219ae854f97f2a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
In TlcEval False Passed
  • Model Under Test
  • Equivalent Model
65000dec63cbb7ad961181ce098b96ac1d87152b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NotIn TlcEval True Passed
  • Model Under Test
  • Equivalent Model
fc21f2562bcbf987b4c4cd26df6bfe102ba17c6b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NotIn TlcEval False Passed
  • Model Under Test
  • Equivalent Model
83937cdcfd170ba3cece247ef9e8ffe565d25945 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Exists TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2377837f19a8d6e252f2fe256e5d20078e2e739d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Exists TlcEval False Passed
  • Model Under Test
  • Equivalent Model
49870bec609dad20c1a7444cf35323dfaeadbc4e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Forall TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f2df33bf0c61fd0290456f09b915d8361e701a73 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Forall TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b77734daefcbfd81ae78895a08084f8a02a7483e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Choose TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ebb06aea0bb4aa3c3d7cb942385e82e3200652de TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Choose TlcEval False Passed
  • Model Under Test
  • Equivalent Model
75fa8c254de6772d38a5edba12e3a760c8af6888 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Record TlcEval True Passed
  • Model Under Test
  • Equivalent Model
835f09529359e3c91014584a25a145f9390a203e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Record TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a87198c32e59b0635ac3035d62df01ae341703d0 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Tuple TlcEval True Passed
  • Model Under Test
  • Equivalent Model
fbb4668d6ac60d60cb077e8a4db53c4dcc7e6809 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Tuple TlcEval False Passed
  • Model Under Test
  • Equivalent Model
260adfcc9650e8ef1c3809f8a0e63e6352fd67a5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
FunApp TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c1f5580c0bb13fead2b5d70e8573c90ee6b48c92 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
FunApp TlcEval False Passed
  • Model Under Test
  • Equivalent Model
52a3f252560d673d985e50a8572204e9a02834a8 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except0 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
076fe602c19d770d6b7b47fa13a2bc79d1d59801 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except0 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
21ee2d6ca93aa2bc47fa8435860157ab743d6c31 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1Fun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
374061f8d01aea0aeb3ee1daf86dab8722559bca TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1Fun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
cf2d3a68417253dc19a47faa33de6f8ccfa12ea8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1FunWithAt TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a3e934b36711d673387c4338b2a4c9f8feb3afb8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1FunWithAt TlcEval False Passed
  • Model Under Test
  • Equivalent Model
2ce94a41fcf02b86c7b160f52b81666f1f47d174 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1Rec TlcEval True Passed
  • Model Under Test
  • Equivalent Model
8cf3d0fd117d05f51c6364c71d0244089c0fd009 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1Rec TlcEval False Passed
  • Model Under Test
  • Equivalent Model
c3d0ae8839b5fb77bb1d0aaed32bced66851bf04 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1RecWithAt TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f23b165c6027cda24b64991e33e702ee0c68b24e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1RecWithAt TlcEval False Passed
  • Model Under Test
  • Equivalent Model
f975eea6ca81fcc31dda5112b88e50831cba2636 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except2Fun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
59c83e035368799395983feda5aa593f4349d7ab TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except2Fun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
69aead153aa658110348545fb8b82ab4f7f36d2d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except2FunTuple TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f026d5e8e331709a50c08621067f08d37124842b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except2FunTuple TlcEval False Passed
  • Model Under Test
  • Equivalent Model
9a0651d34f48909b43e686c7144caa6aef627ef3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Prime TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a071bceef9e4d7cf224491fe977253258d145261 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Prime TlcEval False Passed
  • Model Under Test
  • Equivalent Model
43e423c94aefb233f1eb3efaa8431ade2eb02c7c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumUnaryMinus TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c9b96fe860c437f0d2c29deb756f0c777283115e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumUnaryMinus TlcEval False Passed
  • Model Under Test
  • Equivalent Model
771ec1eb532f2c3ac8b5b28804e735b9a5a3ea9a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPlus TlcEval True Passed
  • Model Under Test
  • Equivalent Model
5055348ef07794f42cd2bed9b1ee85d2203d73ab TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPlus TlcEval False Passed
  • Model Under Test
  • Equivalent Model
f4010360316374d9f210b12360a45bb9083c7c72 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMinus TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e30a54b9ede0bc1553ae1ae2a8b4c660f57b21e3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMinus TlcEval False Passed
  • Model Under Test
  • Equivalent Model
2a60bd5afeeab4a6a7b796d4113299192e697abb TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMul TlcEval True Passed
  • Model Under Test
  • Equivalent Model
9d90e7dd24f36cdac001ba8968c5fbc08b712ddf TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMul TlcEval False Passed
  • Model Under Test
  • Equivalent Model
16b5497a41f192e7eabc2160734b15da5f105e71 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumDiv TlcEval True Passed
  • Model Under Test
  • Equivalent Model
dfbb361a823e5c46617b5c6a98f0fdfdfb1d839f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumDiv TlcEval False Passed
  • Model Under Test
  • Equivalent Model
1295f8e107247425ebfe0ca36d72f371485c53cd TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMod TlcEval True Passed
  • Model Under Test
  • Equivalent Model
7e705d1cb29c95feefa2d46a06cb637b4621db6d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMod TlcEval False Passed
  • Model Under Test
  • Equivalent Model
016e17ffd626759d201a7a839fafe2a28629c73c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPow TlcEval True Passed
  • Model Under Test
  • Equivalent Model
eea33c0e5f9b1842394582e29246b647af1571f3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPow TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4959c9a8859853d90bec57b1e4c74db811d32651 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumGt TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e376ad229fff3a4ee61f4f2cb5a344073c638935 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumGt TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6569bc2c50644145a5ff9658eae4dbb8b6271e34 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumGe TlcEval True Passed
  • Model Under Test
  • Equivalent Model
50446ea328493383c056a00043b69c427c09c997 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumGe TlcEval False Passed
  • Model Under Test
  • Equivalent Model
25660856fceb935e18d4e0f83aefb32d8e75a6f6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumLt TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2aea08b8242b68b7841639ed4581593ce6fbdf98 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumLt TlcEval False Passed
  • Model Under Test
  • Equivalent Model
de8a82f1ea7c999372c9b2ac92a268c7c52cc37d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumLe TlcEval True Passed
  • Model Under Test
  • Equivalent Model
736b4d411b6f5701b624169f39ee63d1b7dd7272 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumLe TlcEval False Passed
  • Model Under Test
  • Equivalent Model
e6b723114c55e9446c9a45a684141f93b7591e4c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
DefFun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
07638c448a0851cf0fe7af8875612dfc90c07583 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
DefFun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
91b8d1879e80f57974277c4a54ab2046d57f4a1c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
09da2bda2e5960e6670ccbab0298d233c28affe8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
48948b226429ac9a1ad4353f62e89eaded1c77f5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
DefFunRecursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a1d58c00b41812bd5b44f770e3ba243b7c2494ab TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
DefFunRecursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
f59dbe1407f706c21e9e3db41108a8f1cdb46bf5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFunRecursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3c6b206a638adbfdd2e1334888d3a1a57b57368c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDefFunRecursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6401861223954f58c8544bb25281a42902ad0936 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def0 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
75c3603801addca109e9127cbb24c1bcd8ea9bba TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def0 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ff2ca9d2abcbc3c6d041a3773ec4a5c1cf65465f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef0 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3744ac1114f38802a4449e34f8fc1f54e7729064 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef0 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
c2b0b908cd1abd9c25f4c548ae545ae961375e3f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def1 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
b9f5888b457ec06baca8538a92cf020e72125485 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def1 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
59667ab6fe09aa1559bec815e2ffa977947a20cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2627a13db5158389e427535b5ea9356ea7120199 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
44ce1059682b5f1a11909f38e0d1c174a8a451cc TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def2 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c8ffc069b76f2d8a382d1e9599043bc18572c630 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def2 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
8816020e1666068c449df11fd2966a84557fcd4b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef2 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
35f6f46e1cb69d1bc871d890c27501cd01f60752 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef2 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
20d33143ccdd4fc6dac2efde9476ab40515dbf6e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def1Recursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
10518aaa86c8de6ceb8ef65225a93706a7f987ea TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Def1Recursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
22a5a4e3f6802e3744701c8b3b9aff12c5758db3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1Recursive TlcEval True Passed
  • Model Under Test
  • Equivalent Model
123855b043aa648504cbd1eb86289ccca4cb0bca TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: TLCEval(expr) is reduced to just expr
LetDef1Recursive TlcEval False Passed
  • Model Under Test
  • Equivalent Model
62422f8b177e33e9806813c14c7e3c04e50a80ab TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Extends TlcEval True Passed
  • Model Under Test
  • Equivalent Model
7dd737740d89752d6ae8983c6862f843fb86d8e9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Extends TlcEval False Passed
  • Model Under Test
  • Equivalent Model
71a1e5952ce7d403426d354e5e0ffb5f7dde9ef9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
ExtendsInDifferentFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3047704abde7895ae4441411f8ef290fe7d308d9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
ExtendsInDifferentFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b1e302d1c4e3d3f49f2ed4049628fb0ff1eb843a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Variable TlcEval True Passed
  • Model Under Test
  • Equivalent Model
db99b6fd288c92474148b85114ba8f9b0d58da62 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Variable TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a7ec85f12323155b16642644fff1b26ed4dcbb7f 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: TLCEval(expr) is reduced to just expr
VariableViewExclude TlcEval True Passed
  • Model Under Test
  • Equivalent Model
512ceec66484726c12cf93b327b87a5b0e027b34 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: TLCEval(expr) is reduced to just expr
VariableViewExclude TlcEval False Passed
  • Model Under Test
  • Equivalent Model
46af2ae2b7565d3163d148fc6c70f7198555ce06 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Constant TlcEval True Passed
  • Model Under Test
  • Equivalent Model
781dd8023fec9d21ad0b77e16de89b5dfda6d3cf TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Constant TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b02ed40d7e87edae9a2d680a99ec460b4aa1740a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
ConstantRank1 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
74b8231a09d77a737507682a6209188238deea45 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
ConstantRank1 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
d4638f8c99b573c4e3e4e7a00dd94e9b194f9c18 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Instance TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ddc4d8d3e612fca061c651b77f2985255223be9a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Instance TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ff1dcb4e356df9d66f72a6fa7028179725184e36 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceWith TlcEval True Passed
  • Model Under Test
  • Equivalent Model
05a80dccce2a7a37bdea663dd0ed8c9db943a339 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceWith TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a35a841804b2c8f2951caee720fe9629d0499036 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamed TlcEval True Passed
  • Model Under Test
  • Equivalent Model
947c70ec1a41f9b6c93dcb16a3b6096dfb209201 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamed TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7f142a19f03db6ad22d74d135413a82ce1ab37cd TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWith TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a5229d93fc6c9ad5afd218ef4f4513640d5bbf0a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWith TlcEval False Passed
  • Model Under Test
  • Equivalent Model
9c989f251eb9e661666daf8eeff60ef66a8ae3e3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceInFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a46f085f90f28c93923a2f1e96b1081a7a6bb062 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceInFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
0d1540ba54c3e81a8d072a7932664fc55750a708 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceWithInFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a626d9034d7798b5f34076a1a7818342e0d77f15 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceWithInFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
db99b259502be6e4992b276bf4a785c8b37f55bf TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedInFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
37acb4f58a9441134ea9e78c4b5a7ce0f31ef0c6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedInFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
88309d0cd53ecb23518b52781205c865443cfdc1 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWithInFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
5dc1e63ff30fe11f34b5d8eae0a199d077209f87 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWithInFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
237042bfe0f0c4db6c194a0cfeb61316df7daf91 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Enabled TlcEval True Passed
  • Model Under Test
  • Equivalent Model
12cd862cda08e6bcd774047dc9f0eaaaba9eed15 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Enabled TlcEval False Passed
  • Model Under Test
  • Equivalent Model
20319bb79c714c5c4c00b53782996c92273e9cd5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Assume TlcEval True Passed
  • Model Under Test
  • Equivalent Model
d2586b6b7f30d025f24a82d123f4517fbf97a42c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Assume TlcEval False Passed
  • Model Under Test
  • Equivalent Model
77cf29a8e2cc6d4a104bf92e6ed94d62d2d01c21 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
AssumeNamed TlcEval True Passed
  • Model Under Test
  • Equivalent Model
067a48a3ccc9ed21b960388afb3833185a65b455 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
AssumeNamed TlcEval False Passed
  • Model Under Test
  • Equivalent Model
95cfafb2d46d111fb7082455114a0c02404f42be TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Lambda TlcEval True Passed
  • Model Under Test
  • Equivalent Model
cda654c44e128b9c8b0eba6a1ba4d8b1e05cbbc3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Lambda TlcEval False Passed
  • Model Under Test
  • Equivalent Model
0d4cf12a2914b4da72f38f197ae507f44a1c21cd TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Cross2 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
413e9c0dadadfc8c2b7cfd9919192aba3f41e5a9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Cross2 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
812e07c53b8bfe991b39ce5d29e541f449a1bb58 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Cross3 TlcEval True Passed
  • Model Under Test
  • Equivalent Model
bde23f338b7aac48a3433a540d0bf2b44043b6cd TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Cross3 TlcEval False Passed
  • Model Under Test
  • Equivalent Model
bf5d349570bda817b69970851c3b0d5a7e00fa6e 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: TLCEval(expr) is reduced to just expr
FunSet TlcEval True Passed
  • Model Under Test
  • Equivalent Model
28bf299036d1da4903eb6ab3c2eb9f727c536e4d 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: TLCEval(expr) is reduced to just expr
FunSet TlcEval False Passed
  • Model Under Test
  • Equivalent Model
8535cd64b26be1f622e7824e0f65d99125f36383 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: TLCEval(expr) is reduced to just expr
RecordSet TlcEval True Passed
  • Model Under Test
  • Equivalent Model
0cedc9d68507c120bbb72bb54d6dc6247c2ac5d6 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: TLCEval(expr) is reduced to just expr
RecordSet TlcEval False Passed
  • Model Under Test
  • Equivalent Model
92a08a9601ffa0ce05edafbed778c15e2a656889 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetDiff TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3c1152c687361f06ba846eb9990f2a851b9544f5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetDiff TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6bb34df9ce07d92c3c84faf01c9c9ff1ad02ee12 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetUnion TlcEval True Passed
  • Model Under Test
  • Equivalent Model
636b47ad4ba48ad2a6c507d38061225c450bca6b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetUnion TlcEval False Passed
  • Model Under Test
  • Equivalent Model
d15809fef8c2970ff3977e6a64b70db589196de4 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetIntersect TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c0dfd056c6d6d812fdcd542c3cd0534ff3dbf7c9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetIntersect TlcEval False Passed
  • Model Under Test
  • Equivalent Model
77c38e06131043a9bf9af679c02d392f399bb0c6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SubsetEq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
cb469be5cc62a9f04c24af9584d73b04cfd87ae1 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SubsetEq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
9379488003dae16839bb725de1106efba2634933 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfCond TlcEval True Passed
  • Model Under Test
  • Equivalent Model
6016ce3244b9a12836c763d55dd064faa636661c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfCond TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4e85052869c2a20a8b35dc7bfbb1e90de8f55a20 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfThen TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c14f9dec0229d7bc089110b89f1df83a3e0fff77 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfThen TlcEval False Passed
  • Model Under Test
  • Equivalent Model
0a75f26c6b5146e14d61325dd8ec61ffdf00df33 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfElse TlcEval True Passed
  • Model Under Test
  • Equivalent Model
1447ecad4c4320cf6d82c264e3e30f7c46232a31 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfElse TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b87bfdfe18dac67265a3ebb1ab6535ae493fc771 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Subset TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ada447683e30b8f0770368ad4443ac74159e2fba TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Subset TlcEval False Passed
  • Model Under Test
  • Equivalent Model
473ef9590017e60e1fe84f85b95488ea38c0c4f2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Domain TlcEval True Passed
  • Model Under Test
  • Equivalent Model
d376d89e9483f3b7995f05b8c16bbbafe41cb80a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Domain TlcEval False Passed
  • Model Under Test
  • Equivalent Model
0be6ec10ec195891d753bc55d8e0fa974c195ff5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Union TlcEval True Passed
  • Model Under Test
  • Equivalent Model
6dd9c443dbc1381a83ec7da5ce83076d55d9f7dc TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Union TlcEval False Passed
  • Model Under Test
  • Equivalent Model
8fbdc2ca01409032e36d1b38f9a14c27eb7a75d3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Unchanged TlcEval True Passed
  • Model Under Test
  • Equivalent Model
c27a99a06016bcab67f1d7d202dab5df59209d5e TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Unchanged TlcEval False Passed
  • Model Under Test
  • Equivalent Model
360e60859e381eb1b49275324ceadd0b2eb6f8ac TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Equivalence TlcEval True Passed
  • Model Under Test
  • Equivalent Model
956722c9c239be1689c93879909d9e3d84d710e7 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Equivalence TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a4d6b9bca1609113226737f0213b5016cc60e31a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqLen TlcEval True Passed
  • Model Under Test
  • Equivalent Model
74eeb5eff07603d6bc8413681633a4f7c5f645b6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqLen TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7055b261671721229c3c50f90cf99aa515e3dc38 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqConcat TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e5fb6a7014497f2cc9eef45ec04d49c3e8259053 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqConcat TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7c04912a77ffbd8a00e5bde97d90f73cb8ae35f7 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSeq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2552da0bc856a40ad3c35d30191078f2bfc9e5f2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSeq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4e34c94f68a18448e2e6710e6062bdcd01e4848f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSelectSeq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
df6161c4ab60105496ec3e7e4c3f0c84936bcc0b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSelectSeq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
eeacd5151e46d1952eae028cbd54d5df62783447 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSubSeq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
360fedd5ea70e7d1d8d35efd6112171bb7ff9041 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqSubSeq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4084a94abab568ebe34df92687b47102f4e5666f 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: TLCEval(expr) is reduced to just expr
NumRange TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3d5fa25714fefc450bc959f74907c56867859930 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: TLCEval(expr) is reduced to just expr
NumRange TlcEval False Passed
  • Model Under Test
  • Equivalent Model
374c3462f59ba155b098477b88cdd38849b3c295 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSingletonFun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
a478651420f7e036325f6db622315c2eac02ea42 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSingletonFun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
58173320c39c18d7e01e50c4094703df7db82e09 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: TLCEval(expr) is reduced to just expr
TlcExtendFun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e869aeb65dfefff5939900c2a89a62f98d27a464 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: TLCEval(expr) is reduced to just expr
TlcExtendFun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
8b271be15df2aa19459fff7cdca2c3f207a3cf6f TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcPermuteFun TlcEval True Passed
  • Model Under Test
  • Equivalent Model
fb0808c8f39a811e3fc466baec7724cc183d2d3b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcPermuteFun TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7820e0cd162583e31f1af32b8cbe0853c44d48d9 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSortSeq TlcEval True Passed
  • Model Under Test
  • Equivalent Model
43d3e5aabba3dfb677acf9c4a65a7aaf8a32feea TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSortSeq TlcEval False Passed
  • Model Under Test
  • Equivalent Model
bb30911c94fcba2e5953a72f23062a4dd832d962 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcEval TlcEval True Passed
  • Model Under Test
  • Equivalent Model
2923b9df5763d9cc48f675caef161744f1a2b9cb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcEval TlcEval False Passed
  • Model Under Test
  • Equivalent Model
e0dc6d5ec97021acf5affbb711401fe670026e12 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagToSet TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ccf90c4da0e44a9a418998a8f6b431149ce154a3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagToSet TlcEval False Passed
  • Model Under Test
  • Equivalent Model
3ae4148c7a97a632c748fe0dbb81250f1c543bb7 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSetToBag TlcEval True Passed
  • Model Under Test
  • Equivalent Model
17b1ad9d807293f2669e7a9764ca199d14d7e01f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSetToBag TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7e48827f4167b955e9b8aab82ea76609847e0d81 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagIn TlcEval True Passed
  • Model Under Test
  • Equivalent Model
eae35f41bb69f13165c18d72462cc2f192a072eb TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagIn TlcEval False Passed
  • Model Under Test
  • Equivalent Model
18e9132a99e0c3f3986fa97e74cb7f02fdd220d9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagAddBag TlcEval True Passed
  • Model Under Test
  • Equivalent Model
9f44cc203e2d7693a9165d96b93196d63ca87ff7 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagAddBag TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a59eaec5c9b77c15e2d251c19598dcd6c30512fe TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagSub TlcEval True Passed
  • Model Under Test
  • Equivalent Model
0984bc73275f6666cd8fb8245b6db78b5e07da2c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagSub TlcEval False Passed
  • Model Under Test
  • Equivalent Model
a524b277f4e52d96458cbd365906ee4c5d3c327b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagCopiesIn TlcEval True Passed
  • Model Under Test
  • Equivalent Model
8cb4e20d05400a508dd6e29078ae362d4ce55829 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagCopiesIn TlcEval False Passed
  • Model Under Test
  • Equivalent Model
57b87131b3fdac2422231aaf8ba310294d92c5f2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSubsetEqBag TlcEval True Passed
  • Model Under Test
  • Equivalent Model
698be23b6985fddec8b65776a235baa0affac498 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSubsetEqBag TlcEval False Passed
  • Model Under Test
  • Equivalent Model
ae81c598a476733cd189f6701eddb802f0acac64 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagUnion TlcEval True Passed
  • Model Under Test
  • Equivalent Model
167ad80e93128c686faf70aff367cf14bc880cf0 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagUnion TlcEval False Passed
  • Model Under Test
  • Equivalent Model
dfebf10793ff03edc75b90ae3292d29e3e8c69bf TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagCardinality TlcEval True Passed
  • Model Under Test
  • Equivalent Model
b7d08b37d1fd01cd28c35f168a4121fc55c29594 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagCardinality TlcEval False Passed
  • Model Under Test
  • Equivalent Model
9c6040e502178f9854f68cf5e09cfb86719ce448 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagOfAll TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3bc9b2e2a892acbe9f805f1a9978ba42a11a8cf1 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagBagOfAll TlcEval False Passed
  • Model Under Test
  • Equivalent Model
af77a65333d25dfc851bfb9f1bc36f7e8edac680 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSubBag TlcEval True Passed
  • Model Under Test
  • Equivalent Model
5771b8317f5861fbbefaba248a1ff2374c068fd5 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagSubBag TlcEval False Passed
  • Model Under Test
  • Equivalent Model
0805939686d6928dbe2f9a6928805db423e932a6 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: TLCEval(expr) is reduced to just expr
FiniteSetsIsFiniteSet TlcEval True Passed
  • Model Under Test
  • Equivalent Model
337fadb8cb2cad6c748bca55589bec1d1837e345 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: TLCEval(expr) is reduced to just expr
FiniteSetsIsFiniteSet TlcEval False Passed
  • Model Under Test
  • Equivalent Model
d292afa17d98c107a43603a893d080ce2ed1d70b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
FiniteSetsCardinality TlcEval True Passed
  • Model Under Test
  • Equivalent Model
543e7a4ed40813773f4c670254e838761af2bc75 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
FiniteSetsCardinality TlcEval False Passed
  • Model Under Test
  • Equivalent Model
fe5bd15db5b3457a65bcddaddf801f3ce0461027 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqHead TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3cd99092241890859b893cf73e65d0a7469f74f4 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqHead TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b26e9858028a62c87835e03ecdcf8e6c4ad74d6d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqTail TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f34df48ea918a9faaefae42307802abbf7065d26 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqTail TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6ebe99d533bbf589a6fd818056fd31e7b2fbfc8f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqAppend TlcEval True Passed
  • Model Under Test
  • Equivalent Model
981d3595ae9a4751d0d5769cb3c408f8197c02c2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqAppend TlcEval False Passed
  • Model Under Test
  • Equivalent Model