Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
30ce6ef0b28d9d8c79d764a14954df79602445a3 TLC with reduction strategy:
  • Plug 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]]
Eq TlcExtendFun True Passed
96ee10027f0a2651d91b2bf46eadc7957413f6a0 TLC with reduction strategy:
  • Plug 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]]
Eq TlcExtendFun False Passed
9c8f67871de9493e9b6cce23de4f064c095c00df TLC with reduction strategy:
  • Plug 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]]
Ne TlcExtendFun True Passed
c86e01c8f1eefc311740544b92d76d61c620692c TLC with reduction strategy:
  • Plug 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]]
Ne TlcExtendFun False Passed
da72186db927fdcac2ccd1db22592239d8ed6f7a TLC with reduction strategy:
  • Plug 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]]
Let TlcExtendFun True Passed
c6eb0f281de72c4e99ca4ff5aa668ee542f9166b TLC with reduction strategy:
  • Plug 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]]
Let TlcExtendFun False Passed
12f0fca4f400d704b2b6af4a90758e586e772980 TLC with reduction strategy:
  • Plug 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]]
Set0 TlcExtendFun True Passed
6ad6b44daff8b6bb999920886cef6fe786ffbb41 TLC with reduction strategy:
  • Plug 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]]
Set0 TlcExtendFun False Passed
9e3f033751657a1d03511c5c35d7e492e47d2202 TLC with reduction strategy:
  • Plug 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]]
Set1 TlcExtendFun True Passed
181d1acc0a674d724a1e0a2a918fd3dd3eae807c TLC with reduction strategy:
  • Plug 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]]
Set1 TlcExtendFun False Passed
2eede76c11ace992e7dbcf2b38db7d92ee934e60 TLC with reduction strategy:
  • Plug 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]]
Set2 TlcExtendFun True Passed
7aeb4f81cda6de6213f0dda96d616d0a4c1298fb TLC with reduction strategy:
  • Plug 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]]
Set2 TlcExtendFun False Passed
0c2100369b494a8430a24d16aeab235fada3435c TLC with reduction strategy:
  • Plug 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]]
Fun TlcExtendFun True Passed
18e25ade9f1c79f7e4c089e745d397ea8697356b TLC with reduction strategy:
  • Plug 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]]
Fun TlcExtendFun False Passed
ff0487250ebc8f129a5517a5f1b8e7f2a1806926 TLC with reduction strategy:
  • Plug 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]]
In TlcExtendFun True Passed
f9da2c68a726c25fb0cd9e7d583e317c9131f75b TLC with reduction strategy:
  • Plug 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]]
In TlcExtendFun False Passed
30c981bdb91a5477e1dbc0dee75c36e564939ff7 TLC with reduction strategy:
  • Plug 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]]
NotIn TlcExtendFun True Passed
7be61a7f95ea345fdbddc760ff7f4b47143bf19d TLC with reduction strategy:
  • Plug 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]]
NotIn TlcExtendFun False Passed
fc777027b3cbdfb56e62e04526f21d7ce9b97b46 TLC with reduction strategy:
  • Plug 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]]
Record TlcExtendFun True Passed
a425ba0671c01f2148d6b0169743f64d533b153b TLC with reduction strategy:
  • Plug 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]]
Record TlcExtendFun False Passed
218a3f8a6e922344145e1468873c778945d0819f TLC with reduction strategy:
  • Plug 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]]
Tuple TlcExtendFun True Passed
051af3a6656dd41a97a18ef63cd0de6a781cef88 TLC with reduction strategy:
  • Plug 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]]
Tuple TlcExtendFun False Passed
34934d8a30cd0a146df158815efe6014d80e6eb8 TLC with reduction strategy:
  • Plug 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]]
FunApp TlcExtendFun True Passed
a2963d158b541f4bb8686856735d5f7bd1749800 TLC with reduction strategy:
  • Plug 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]]
FunApp TlcExtendFun False Passed
2989e5c4db8446011d726ddcfd1b1dbd0713ca30 TLC with reduction strategy:
  • Plug 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]]
Except0 TlcExtendFun True Passed
f8be92adde07f25689097b299aeb6e5248c541bb TLC with reduction strategy:
  • Plug 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]]
Except0 TlcExtendFun False Passed
7af9c54ec1b5f14dc0a51d4f97d0efeefc76bfaf TLC with reduction strategy:
  • Plug 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]]
Except1Fun TlcExtendFun True Passed
14da98c9925d20e311f8084c479195864d353b2f TLC with reduction strategy:
  • Plug 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]]
Except1Fun TlcExtendFun False Passed
33b66696e96053da5dea7e8b4f97cbadf0eabccd TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug 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]]
Except1FunWithAt TlcExtendFun True Passed
2ca72380a4f78347f3333b080645dd087c065710 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug 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]]
Except1FunWithAt TlcExtendFun False Passed
6a777ac0686cfd32a7c7b043f6779c3807a1ff3b TLC with reduction strategy:
  • Plug 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]]
Except1Rec TlcExtendFun True Passed
0c14d3e1a96bfc78d95f594204a6ecd36844e001 TLC with reduction strategy:
  • Plug 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]]
Except1Rec TlcExtendFun False Passed
2791ba2c9ecf0b31e183c059acc5b252e2859d13 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug 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]]
Except1RecWithAt TlcExtendFun True Passed
f3cef757cc6b8c8ab8256b5ffb515dbb8780941d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug 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]]
Except1RecWithAt TlcExtendFun False Passed
9df2a6e76a05cdc24ee667dfd2d2aab3e9562f12 TLC with reduction strategy:
  • Plug 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]]
Except2Fun TlcExtendFun True Passed
b1eef7217b76890800402662e621bb5e218fae97 TLC with reduction strategy:
  • Plug 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]]
Except2Fun TlcExtendFun False Passed
890cf5f3e02d9ce49075d68736339e6254123687 TLC with reduction strategy:
  • Plug 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]]
Prime TlcExtendFun True Passed
54bc5776674f76f25b338c274332ecea54fe5ba6 TLC with reduction strategy:
  • Plug 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]]
Prime TlcExtendFun False Passed
2c80ab17e5469f1d1e8b02d2eda31a69e631fed1 TLC with reduction strategy:
  • Plug 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]]
DefFun TlcExtendFun True Passed
fcbe8db6757323292fd83d8235847e104707d69f TLC with reduction strategy:
  • Plug 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]]
DefFun TlcExtendFun False Passed
8ce929cd8ab155693ffae8c42d31de869e4653b8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDefFun TlcExtendFun True Passed
cd07936abf2ef415adf03a04ac6f4b66d2b5deab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDefFun TlcExtendFun False Passed
11d8f2d81bdc6666d61fbbe9f43376a458a150f4 TLC with reduction strategy:
  • Plug 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]]
DefFunRecursive TlcExtendFun True Passed
fbc75c9d3fad0f729a6fa3390500e79ec41f3cd1 TLC with reduction strategy:
  • Plug 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]]
DefFunRecursive TlcExtendFun False Passed
7dbaa760d38cfb235210b0a12e7eddfcf49a8caa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDefFunRecursive TlcExtendFun True Passed
0b95f5480b59defc4698d9ad90af88f3cde4ca38 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDefFunRecursive TlcExtendFun False Passed
6e008944077ea236b5ff3f6b8ecaa24c8b1b248d TLC with reduction strategy:
  • Plug 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]]
Def0 TlcExtendFun True Passed
18e350ec4ccbaea7ef2e665ed90d5dfa3ba55c86 TLC with reduction strategy:
  • Plug 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]]
Def0 TlcExtendFun False Passed
51375abc90a826460c901cc3fe19bad7d61195b5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef0 TlcExtendFun True Passed
b6ba3329151f78fc6048b17ad03737f081894b46 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef0 TlcExtendFun False Passed
af5f603b2f83a439b9dba86ae8c10dbbbb963401 TLC with reduction strategy:
  • Plug 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]]
Def1 TlcExtendFun True Passed
78aa281be14d20f25b7ce04fca1ea4a0ad2e9d9e TLC with reduction strategy:
  • Plug 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]]
Def1 TlcExtendFun False Passed
9677dec45313effce5d2139bb7050c9fbf0c2f76 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef1 TlcExtendFun True Passed
5ec83fce35e4bebcbf8f3cce38aeea90be1abf3c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef1 TlcExtendFun False Passed
5985dfc2276a73520ab930d5729aaf6c96ccf9df TLC with reduction strategy:
  • Plug 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]]
Def2 TlcExtendFun True Passed
b1eee41470a09689a4c202b06e2b47bdd7426564 TLC with reduction strategy:
  • Plug 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]]
Def2 TlcExtendFun False Passed
c46d7a2190e65bb98f6e19ce8c920cb3fe8a7f1f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef2 TlcExtendFun True Passed
6703de9bc2ba61a0e9a7cb9d04645bc6c1ccd7bc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef2 TlcExtendFun False Passed
9405c8665d0d2ddda72f0bd44f4cde33c905054a TLC with reduction strategy:
  • Plug 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]]
Def1Recursive TlcExtendFun True Passed
5ecf6c3cf94308e1004c8d4e1c35dab4592bdec3 TLC with reduction strategy:
  • Plug 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]]
Def1Recursive TlcExtendFun False Passed
6229de3c1dad426c7b02b4f253e0555d49c70a83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef1Recursive TlcExtendFun True Passed
1073f5e04816f3caac22307d3c26f8580b0a7f59 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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]]
LetDef1Recursive TlcExtendFun False Passed
ca4c8f50cf310bea51af0a2c6fee615b6a57f7ff TLC with reduction strategy:
  • Plug 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]]
Extends TlcExtendFun True Passed
52e0062cd02602b8df71f6a9dca5a0180b3518ed TLC with reduction strategy:
  • Plug 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]]
Extends TlcExtendFun False Passed
0890ed3c016b5458eb5c414627d72d1e2c90f4a4 TLC with reduction strategy:
  • Plug 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]]
ExtendsInDifferentFolder TlcExtendFun True Passed
27fb4c6ea59eb15b48bc343ec9ac7cca3b6b5ca9 TLC with reduction strategy:
  • Plug 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]]
ExtendsInDifferentFolder TlcExtendFun False Passed
20df195daebbb1f4fdeb37868178f58ec721fe19 TLC with reduction strategy:
  • Plug 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]]
Variable TlcExtendFun True Passed
087cfe26df2b5d0cf167f95ac4fab92276b7835d TLC with reduction strategy:
  • Plug 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]]
Variable TlcExtendFun False Passed
b57a2e7fce7621f943f7684240e21a865ce0eeb5 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: 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]]
VariableViewExclude TlcExtendFun True Passed
34eee12a1d4c139682d74bdb51cfc86f3fb0063a 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: 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]]
VariableViewExclude TlcExtendFun False Passed
f387deaeaa4ba21aee2aa0ac8b28b5b2f698a91b TLC with reduction strategy:
  • Plug 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]]
Constant TlcExtendFun True Passed
90c00019f974d4dbc7c38701c40bdcee4f987f0d TLC with reduction strategy:
  • Plug 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]]
Constant TlcExtendFun False Passed
26cfaa0b63600a2628af807411959254e2817b17 TLC with reduction strategy:
  • Plug 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]]
ConstantRank1 TlcExtendFun True Passed
eeed5b524e7450e83cebc9d61535c45469a35586 TLC with reduction strategy:
  • Plug 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]]
ConstantRank1 TlcExtendFun False Passed
8223e5d9e5a8135824a7a3b7d623cdb578b454f2 TLC with reduction strategy:
  • Plug 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]]
Instance TlcExtendFun True Passed
ffbb6c66ebfb8b96ed4e6b59cf21986d5a11ffd8 TLC with reduction strategy:
  • Plug 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]]
Instance TlcExtendFun False Passed
32d3c65063f7a23926047975e7014c4fd67b506c TLC with reduction strategy:
  • Plug 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]]
InstanceWith TlcExtendFun True Passed
f4c59589bbe23919b32f248ff5f30534417309b3 TLC with reduction strategy:
  • Plug 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]]
InstanceWith TlcExtendFun False Passed
5b545364aa61122430d838595a23a3a40a82ae92 TLC with reduction strategy:
  • Plug 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]]
InstanceNamed TlcExtendFun True Passed
6724b1de8d9933a67f2e9e0d673064fbfb939e2e TLC with reduction strategy:
  • Plug 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]]
InstanceNamed TlcExtendFun False Passed
d515391af49b46e2eab0240813660541ea716b3d TLC with reduction strategy:
  • Plug 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]]
InstanceNamedWith TlcExtendFun True Passed
69599d3d497edcfe18edb4e5a9227e65ee536321 TLC with reduction strategy:
  • Plug 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]]
InstanceNamedWith TlcExtendFun False Passed
fe50b1f70dc11eda52b1c8862032f7d1ef264b2d TLC with reduction strategy:
  • Plug 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]]
InstanceInFolder TlcExtendFun True Passed
7f0de71eba0cf4ee98f6b0e6eb50952ebfa6a6ed TLC with reduction strategy:
  • Plug 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]]
InstanceInFolder TlcExtendFun False Passed
948f0bb0d2880613af01cde81cad18b7866f9ade TLC with reduction strategy:
  • Plug 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]]
InstanceWithInFolder TlcExtendFun True Passed
f0dea2f10029b95e06860c4e48f3dd6d46c5635c TLC with reduction strategy:
  • Plug 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]]
InstanceWithInFolder TlcExtendFun False Passed
e14045061c0a3fd2561db5596432a8d4d7d2d611 TLC with reduction strategy:
  • Plug 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]]
InstanceNamedInFolder TlcExtendFun True Passed
09740a987146a983eef97641c16b592665ed907c TLC with reduction strategy:
  • Plug 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]]
InstanceNamedInFolder TlcExtendFun False Passed
8b01f9c3e1ec42b6799c365a0e1e0b2829c8f765 TLC with reduction strategy:
  • Plug 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]]
InstanceNamedWithInFolder TlcExtendFun True Passed
b4542c7ce705bdd559536202f1cf7dea24d6ca18 TLC with reduction strategy:
  • Plug 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]]
InstanceNamedWithInFolder TlcExtendFun False Passed
5dd00e1480f3caaa9edb4708174de031d7a4fa91 TLC with reduction strategy:
  • Plug 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]]
Lambda TlcExtendFun True Passed
dca746bfb474e76a9d3fd16cfdf9c88d6c3d97a1 TLC with reduction strategy:
  • Plug 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]]
Lambda TlcExtendFun False Passed
8aae0a0ca42942c59f6a2abe92b47673e47af3c3 TLC with reduction strategy:
  • Plug 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]]
IfThen TlcExtendFun True Passed
24040fe1a0fd21c360481c3239ab0fc31bdbec82 TLC with reduction strategy:
  • Plug 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]]
IfThen TlcExtendFun False Passed
d1461bbc916cef6d01dacbae25b3f629f8cb34b6 TLC with reduction strategy:
  • Plug 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]]
IfElse TlcExtendFun True Passed
50d49cd68847fcfbdf20a74dd6e75aaab33b4435 TLC with reduction strategy:
  • Plug 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]]
IfElse TlcExtendFun False Passed
c373fe34f0249be404ebfdd4ebfe338f72911d3e TLC with reduction strategy:
  • Plug 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]]
Domain TlcExtendFun True Passed
412d2f11722a9dbe1a6086bc8fba52ea7ba8832d TLC with reduction strategy:
  • Plug 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]]
Domain TlcExtendFun False Passed
00d60feebec5a26a2a054d6bdc4fd5bfdf0e9a42 TLC with reduction strategy:
  • Plug 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]]
Unchanged TlcExtendFun True Passed
e8e823b105a418a9121aa47c9d1c20c5bbb3f964 TLC with reduction strategy:
  • Plug 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]]
Unchanged TlcExtendFun False Passed
8ce7e62b5da2deef59b4be60c1a4306523765d38 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug 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]]
TlcSingletonFun TlcExtendFun True Passed
9caf35544817f14a1f69f6b4b8291e6a0f243b8d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug 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]]
TlcSingletonFun TlcExtendFun False Passed
a9ee7b5257ddb2472336f4f4edf715afce8c4dab 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: 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]]
TlcExtendFun TlcExtendFun True Passed
3c0b7b539f8b56ee00e701ca9a52177ed5de8afb 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: 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]]
TlcExtendFun TlcExtendFun False Passed
6931eb1f55ace7c9e1b25d74b3997a30a502e503 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug 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]]
TlcEval TlcExtendFun True Passed
ccd9f84ce74cc67f90539778de00bdb4bf7ed5f6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug 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]]
TlcEval TlcExtendFun False Passed
dcefd1afd839d96a1173e477b5f1dde091123767 TLC with reduction strategy:
  • Plug 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]]
BagBagIn TlcExtendFun True Passed
a2c26289c174438aa81ae1f85b5c64633c2ba11f TLC with reduction strategy:
  • Plug 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]]
BagBagIn TlcExtendFun False Passed
a9db3b955c9145268579e5c8b399d0cb63995202 TLC with reduction strategy:
  • Plug 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]]
BagCopiesIn TlcExtendFun True Passed
2cb9d5988534212b66f55663a52d1839067f7cbb TLC with reduction strategy:
  • Plug 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]]
BagCopiesIn TlcExtendFun False Passed
bf459686ec4bfe15b2f2d03e5569e6e28ceb8b61 TLC with reduction strategy:
  • Plug 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]]
SeqAppend TlcExtendFun True Passed
32564d813fa07265b4af32bcd83f25c01a50b5a2 TLC with reduction strategy:
  • Plug 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]]
SeqAppend TlcExtendFun False Passed