Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
7e4192e3f823349c4d985587eedd01cf11279b25 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Eq TlcSingletonFun True Passed
4fd361cc27e752705cac924c47314105b9a86e3f TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Eq TlcSingletonFun False Passed
0d5f24a7696c6a76dac9e24224cb0eace5c2b64c TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Ne TlcSingletonFun True Passed
26ca409032849263abd7baa9703c331dd0ce09f7 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Ne TlcSingletonFun False Passed
a6b577531c74e95e0018c5c50d74d8603ceceac4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun True Passed
af7d1d44027366bd44b76d8a81cfc8b5df20a7ec TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun False Passed
64a0e0c17249f9e616e2527aac4f9e45926bdc83 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set0 TlcSingletonFun True Passed
285889414442d6d183524b4164ffe86540203a75 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set0 TlcSingletonFun False Passed
4250232c562c8e4baab5b5ac829712126f83fc01 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set1 TlcSingletonFun True Passed
e6239ea7e7d94c8839a1a2e1f0a5a1d1e8098856 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set1 TlcSingletonFun False Passed
7e4fe2f3630f5d870c3c1ddb55f9a1380a3c4335 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set2 TlcSingletonFun True Passed
702ca35b1996dc27818c7c718b159130f0f44ea6 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set2 TlcSingletonFun False Passed
bc541b36019a775dec91605582854ddcfe8ba9e1 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Fun TlcSingletonFun True Passed
b5302c037723e4b6e2af851e916b15242f72edd3 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Fun TlcSingletonFun False Passed
67217e3ee855048e108ecfa3182dd8ecf3b214b4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
In TlcSingletonFun True Passed
f0d735ae774201969656bd9c7e2d532c80646861 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
In TlcSingletonFun False Passed
da40ec0ab5a671d1dfd4338c58c4318b4574050a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
NotIn TlcSingletonFun True Passed
536c305d8dd18fd09423d85da2dc4511a5f3caa0 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
NotIn TlcSingletonFun False Passed
4e13a5415db7c602230532e489e1e2f899523d80 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Record TlcSingletonFun True Passed
f84f48d7c6e0a77620a3d04d0c01e805c7ebac21 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Record TlcSingletonFun False Passed
0db0dbcfc5c2f883fdbe09f4e831d91a3f116873 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Tuple TlcSingletonFun True Passed
06e360c0121db482f1bd050e82e105edc1398839 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Tuple TlcSingletonFun False Passed
f1f7bbc2f380a37151da9d348fa70f5cd5b38659 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
FunApp TlcSingletonFun True Passed
ac05c8155eb067947e1269fff3855e235a324b1c TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
FunApp TlcSingletonFun False Passed
27ad1b6e861e46270be8ed2d65d207d49235b7fa TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except0 TlcSingletonFun True Passed
7f0b7fdbfc251d120770059797b568538df166ff TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except0 TlcSingletonFun False Passed
f2f7cd915b704a4d8f201bc153451c8390767da4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1Fun TlcSingletonFun True Passed
d98aa6f06e0f2862b0ea41d04d64f03ee201bb87 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1Fun TlcSingletonFun False Passed
7be41c0430cbcb2dbdc7fac896a8621763667648 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1FunWithAt TlcSingletonFun True Passed
5d1162071c54d4bbca811473061f374571976747 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1FunWithAt TlcSingletonFun False Passed
ae745d2625e19588003bb490a4229e56bab2215d TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1Rec TlcSingletonFun True Passed
c1ac8a485beb259c332b222d34a9a5dd3502256d TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1Rec TlcSingletonFun False Passed
eba4732113944b35946818e951bda2da0e5308d1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1RecWithAt TlcSingletonFun True Passed
1175b21d387287e35523930b7416386dcab2659a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1RecWithAt TlcSingletonFun False Passed
afbe6de5f68b7734d9400ca2c9da990661c7a8cb TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except2Fun TlcSingletonFun True Passed
f04b457a8a463ff9712ad4d046d963c611712fa1 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except2Fun TlcSingletonFun False Passed
e17f4dc17de9e6c322eef6904149dd98a8036b13 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Prime TlcSingletonFun True Passed
242b89ce03f0045f1cdce7b3b0732a68243e58c2 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Prime TlcSingletonFun False Passed
fb0ef0bb7c7e2eb1ab390ccaa406d253e278ec04 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
DefFun TlcSingletonFun True Passed
13fc6e4a72c5039573d14032cebb18f1b0200e2f TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
DefFun TlcSingletonFun False Passed
6ef48d7d4cbc99b89e08d10929ac8981c48b39ab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFun TlcSingletonFun True Passed
91b4f4c1f3096c8961f204dfd4051e3955a23403 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFun TlcSingletonFun False Passed
414333f807eb897db44d121c749b48cd42722f6b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
DefFunRecursive TlcSingletonFun True Passed
532aeffb96da30c073ed877cfa0b90eae09671cf TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
DefFunRecursive TlcSingletonFun False Passed
f6cce6c47c7b6c27e41e43673d3643054ad52578 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFunRecursive TlcSingletonFun True Passed
39ff253469698f57f043a11b6c16a44da6d94efa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDefFunRecursive TlcSingletonFun False Passed
3f0a3732c455594c1554a75724ad7d18beed39ee TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def0 TlcSingletonFun True Passed
6c40f94f7b99de087d3ddd66ea4be63a60f6e7a3 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def0 TlcSingletonFun False Passed
2491f5d2785cf5a12aa2967643f1ea5a1c2a54cf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef0 TlcSingletonFun True Passed
dd15fea280dcce98cdb51ddd029040652af01b3b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef0 TlcSingletonFun False Passed
2dac74f1cac81dda1b36485e6ae774bae8fe384b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def1 TlcSingletonFun True Passed
654c72a1b3a8c139778f5cc0619f385397f58816 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def1 TlcSingletonFun False Passed
fff05e373aa941e465062760f79883e3e1c65952 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef1 TlcSingletonFun True Passed
cb4b1ce152d73dff3e67c9664a6d9828b3c37d1c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef1 TlcSingletonFun False Passed
757a4eb15d4a863cb0e7ca3796a07202eb29048b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def2 TlcSingletonFun True Passed
741f7effd296bb748eff26e943d4936fa3d38ef3 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def2 TlcSingletonFun False Passed
f8f89b4621de0de0e809c21433387b4d7a535896 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef2 TlcSingletonFun True Passed
c04676d708aef58380fb00ed9bce5196d9a1a31f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef2 TlcSingletonFun False Passed
2748b69fe1f68b3da7d9de1f6610c02ee6534213 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def1Recursive TlcSingletonFun True Passed
8f1475065551560fc2e98165b7d5d77550a9a593 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Def1Recursive TlcSingletonFun False Passed
10ece599fc22127d37ed7fac1c1e25445bacaac2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef1Recursive TlcSingletonFun True Passed
3f8aa050f862eef6657d5e3942eff0ee3fec6d0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
LetDef1Recursive TlcSingletonFun False Passed
72e7ec6e6c0b5b4b947c2f645f5f6629764a028b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Extends TlcSingletonFun True Passed
c24b6f88923731f1a158116512a8c4166a1cfba1 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Extends TlcSingletonFun False Passed
0efb64779381747bfe4349fd5f18d6205ceec347 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
ExtendsInDifferentFolder TlcSingletonFun True Passed
3bdb61f79e26c3c6cd6b5c650432fd9884990464 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
ExtendsInDifferentFolder TlcSingletonFun False Passed
eb38218600c4f661c6cdb38e9d5ee8b0b8ffde32 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Variable TlcSingletonFun True Passed
b6754d547937784874f059f6c7739d7bfa092534 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Variable TlcSingletonFun False Passed
75c689770229db5273ed7542a263eb5a64997c34 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: x :> y is replaced with equivalent [u \in {x} |-> y]
VariableViewExclude TlcSingletonFun True Passed
c1ec27a735d8f7cf7720aa9daa4e51b70fc74441 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: x :> y is replaced with equivalent [u \in {x} |-> y]
VariableViewExclude TlcSingletonFun False Passed
578db5d627b6b4a5ae8effa44099abd31eb9e2fb TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Constant TlcSingletonFun True Passed
2224f0c40272875b6226aaa0a400ad687c40e7f7 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Constant TlcSingletonFun False Passed
72fffe7fb318d55821a23dc52ab8f8a2431f54df TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
ConstantRank1 TlcSingletonFun True Passed
89a4e5d346563af6c93fc22cc0abb09af9e2e44e TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
ConstantRank1 TlcSingletonFun False Passed
ebc3ccdd5d0b2db992eca50eabf6de51355f3afe TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Instance TlcSingletonFun True Passed
c254e824f9dd99f13bd0e6b66ba232c94f6048f5 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Instance TlcSingletonFun False Passed
c3787d71c1dbc38704960ce73b37b72735425615 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceWith TlcSingletonFun True Passed
335fee002529e6dc8afeab31447554f4ea3899f0 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceWith TlcSingletonFun False Passed
d66716f23a2222c8120ebac8ccb212399f1dba4f TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamed TlcSingletonFun True Passed
fc60ff5c6e218f63462a05fb7e35e988a9772cbc TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamed TlcSingletonFun False Passed
d1b1192fc5d4a57ea94be68d50cd6fb5ada970b4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWith TlcSingletonFun True Passed
29faaf87a2ae4149de526ffd75b46fdf9dda4c6b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWith TlcSingletonFun False Passed
70a43eb0b8597ecbcd3a1f23ec539aaad547089d TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceInFolder TlcSingletonFun True Passed
cc223aa82f3a56ac100cce2a60d21c0387e57179 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceInFolder TlcSingletonFun False Passed
cca58c87c828f08f0a35a77056882d1dc19577eb TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceWithInFolder TlcSingletonFun True Passed
d60f96c0f7695ab038a9e23c4f112139fd39d04a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceWithInFolder TlcSingletonFun False Passed
c44f08e408952242e103a1fa3a179594dc642bc4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedInFolder TlcSingletonFun True Passed
5e34ae7bfe5e66225eaf433d42c56737db742481 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedInFolder TlcSingletonFun False Passed
8725d9c1a697f3204940733e9e63e28a1db1122a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWithInFolder TlcSingletonFun True Passed
473b79ad8740b0910d5f503afa45fad442cc4337 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWithInFolder TlcSingletonFun False Passed
04bf02a3f7ab1281965d76c0a814e35195b106c0 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Lambda TlcSingletonFun True Passed
5987bf986e8700cdb26c324dd4168251b58f7fb6 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Lambda TlcSingletonFun False Passed
8f02c75d80e2e67d0fe2a0b42f866b6ace9584c5 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
IfThen TlcSingletonFun True Passed
e511da6f6d4a1d32a8cf96562a27d02ad40bb77a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
IfThen TlcSingletonFun False Passed
55e44b110e22c6e0dc208c10b026235f8b5e3e05 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
IfElse TlcSingletonFun True Passed
dd070a8f9784d2dad1646e1b8fe3da80cb4a0ed9 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
IfElse TlcSingletonFun False Passed
6e6d7d1d46e3baca9bc0eea5d738275e31efe697 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Domain TlcSingletonFun True Passed
bf6a3abde7d7cf6b172a8664e3c4e23ea924e1d4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Domain TlcSingletonFun False Passed
b6b6764679be654f3ead094a2201a5eed2a760ed TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Unchanged TlcSingletonFun True Passed
8124cd779c4edbb79410d424003f95e3513a0511 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Unchanged TlcSingletonFun False Passed
d8cf5554b566b916814a4e48ae44069d9aea8c90 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TlcSingletonFun True Passed
b5c7b007a049e24e000bf3eacd100bab3937ff2f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TlcSingletonFun False Passed
1c9e65906ecd1a2543d02cd7075e53188719792f 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: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcExtendFun TlcSingletonFun True Passed
c4704e3d2484079984e6e1c2baedbdd2c1f95a82 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: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcExtendFun TlcSingletonFun False Passed
5a61561c25108035071ad94e5a77f9361a00b04d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcEval TlcSingletonFun True Passed
97c626a835e1834f2005b2cd9dac16e90de69d70 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcEval TlcSingletonFun False Passed
4b4a621e6538fc6e8702063bf455d35656ab32b3 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagBagIn TlcSingletonFun True Passed
fbf24e4fa7d91550c2fafdb261731a560a9b86f9 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagBagIn TlcSingletonFun False Passed
e178cfe7ec37acb26c994f1a350aba49fce6d08a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagCopiesIn TlcSingletonFun True Passed
73ecacae094305bdf3f4bc4b630e1e2384129572 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagCopiesIn TlcSingletonFun False Passed
cc4f43b75e13afb910d6b18af71ccc178cef8584 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
SeqAppend TlcSingletonFun True Passed
a6694a38d399c9a213156aed7359e05f760f3c1a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
SeqAppend TlcSingletonFun False Passed