Index


  • Introduction

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

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

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

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
9007e4240d76d755cc90d7e4e779bf88f9845480 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
ccf7a1ef81851fac45c89894f157d75bdaabcc02 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Eq LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
b7d834a1bd892a11ec595b00a23776da646ca1cb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
e5f5812b01b4a846a31f70742e677fc0e102b0a5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
c7208accf7193fdfcd1e3afb9c05bde5e395dfea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
23464eff7fad3bfeab1516c24515194cbee9dfae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
9d1ea7b8dce5ab440671ed06886b19eeda6221a3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
895cf5335bae48011e2b846b5f36c03732548ee9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set0 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
7235d592fc4d5d6f7e55ba21d99b73ab8f921119 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
9556e99412316d29350bd30bd4c46ed0bd212468 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set1 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
185faeed65c64ac1d872aab93b45a5d62c1328ee TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
8538f647a5444e29ceb8d7280fc1bbd4a1d1e4e7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
9213407c156a0dc26f2b52f760abab35ea13be20 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
181d450fbb0c9096629fffb159529c458f56a8b4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Fun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
0fefb64e4c186545ea18f247b1a6b88c2b44b07c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
f075ea0b41a4052c7fb3dd3ad4314ea4443ff463 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
In LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
fab86b6fbd287b70038e8906da0a55f58359e1d2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
8777b4b12b73c7b87da4bae7912191d1b264c5c6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NotIn LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
e700b917c7b726120686ae9e571079646efffe5f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
52d89fa79b039ded8fcfb507bad0f1b02d912725 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Record LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
a56e1d2308e2a9d1b0caf19e84a266570ec55bd5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
423a0e101adda578d31e9eff0db322f3bc6c62e1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Tuple LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
80f87a39372e13666bcbc2412abe8524b105cc65 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
5bba05752c9c6aca297aa95fe9937ffc2170a5d1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
FunApp LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
8829d3b91252f582d294c0e878707ae3f70a4f2a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
c17c3e884a9619cbc4665c64cd2ac228e381ecf0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except0 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
7e7c124bbcfce131c27b61df41070c1cd95c7ec4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
e5871d37ee431e82bc90c307d6066aec6143332c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Fun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
729ab751398e7a4e589d8dcf7144315fc99b1a91 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
6aba3f7ea1327037c31d3013b9b4086457fd4f53 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: LET definitions are reduced to global definitions
Except1FunWithAt LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
d0d687a1988dc374cb0b90f5b00e9ec09349383a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
9f7b5e98bf9f2fb18d9e4fc750187cd7bfc4a93c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except1Rec LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
3f8829160a201fe9b9771f4ff33a6460ea77ea80 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
00a322201a4b44f118db581a34944735df90ffae TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
39f2c8ca51394b76eb6f36ad488eca06a648fc70 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
36b2b8d7348be8d178f08a48209dca3e7c5dd89f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Except2Fun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
4031f1806527b26a8d072f7709e7d8cc2befd8a9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
085515d1b15ad29ed66a4af5e06ff635e1a1bff0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Prime LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
0dee11d2a21f2bb0fbf39014c6351b6d82a56b90 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
6f82132f72df83e5bd5ba7c18e73697a9535c4c2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
8dab6f486af5a5f4127bae5ae20de55ff0aec391 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
da4aea918ec9260f9e2ffd7a9873755c04a91f4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
ca185d70a38330d0d45444210ab555a9c2a2e3ce TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4fb714677a69dcf47d4f81d50e4198ac22ca9628 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
DefFunRecursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
4d236a7c8155bd39e2c4a14cdb164bb1b3139d2a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
ed7d9f70314ca05e43d01bdaea269f6e01bb6b93 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDefFunRecursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
5f264162515c6a1536b7d5304bb80e3ad54b5662 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
fc50ed36b7fb67588723f790e003b1ec7fd48c7a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def0 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
ec0fffcaabf5198ed3966af9740722d8ed9c42dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
0ac97e025a4a350b207a1246ea986a774fdf7692 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef0 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
32d3ccc35dfdffac7129149a92d1a0a0d05260db TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
0c349e3c4a7e6609e1e162b945ea5a64a547f0b8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
24eb180a12d73add4845c6666f4a13b0a2e7bf2d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
103f4cf74249797dd4bd8dd4c07b696cd3e84893 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
9c63314d5ed8348dbcceefcfd3add017c7c82d3b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4590ef08e87f6938d6b35f0f18bce4e0c3ffe7d1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def2 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
5fff3891a8814c7a29ca7a0002a3c38dbd8f7db2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
d2db52a8da0811e47177b0076c6210ce2f4fc241 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef2 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
c89dd6244cec70929fdbd0366ec9669aefbe7af6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
c7f5ca208bec615b9bd2c69755f8283afc13a000 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Def1Recursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
ab0a46e59bf8e9c55a66cd87079a8aba0e49aa79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4c09405b9aacd22f049b112ddabede8fceaeef32 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: LET definitions are reduced to global definitions
LetDef1Recursive LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
cbd069699fc7ca6c817d466c8b95df5cff48fdab TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
e820c6c290304ec089ce2a61bb6b64c511dec17b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
c7ecba7dbd5db4320cb3ec78d23f22fca75eed9a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
2383762e2d7e25acce3397921df82756c70f0ebd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ExtendsInDifferentFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
0fa7a4f8ecaaf6ae43e77a14cb15b77deeae2c26 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
f6d1a8baf12f7f9f09a3931a00be509716af2f87 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
300d25ad960d848b082f4a0f8dabdbba4617b5ad TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: LET definitions are reduced to global definitions
VariableViewExclude LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
5307997e1b62ad89b1f6a5445c838e5fbad988ca TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: LET definitions are reduced to global definitions
VariableViewExclude LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
c964414d3b81c11c7d2bff2553cc739770fbb87a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
f1dac791534a1b620db456939135bf4a24448f90 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
02366658ab8b2ab5ddd46016bc4ea9f9b7c8c123 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
f6de43026b89630a694e99c56a1ca0f3f1db23f3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
ConstantRank1 LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
1146bba2cb8f25cece20b6b0af0854ff32aefc94 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
164021d81a4e24baa1ce46ff4992516938ba2787 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
f7215298cc1aa9ffe3a5079d3e970c1cb2347c34 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
5e5ea540f45ada95fa786eddf93997d29d49fe6c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWith LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
40a4a3e4896d35bba581c94d4b419a10f776b17a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4c913cdaae68893a0efc6d4cf6272740ca179ba1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamed LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
888884fd97c4334772d5a15d94032c8429e9a1d9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
ec311ff81e68538385d52823e3532d24477bb8ab TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWith LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
2151b9e0102ab0825197243573a884f8fd989e57 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
111e5032680129fa886256ac093d3707edd1b699 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceInFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
46d26f581784f33b5b8d0f42b71080b036007561 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
00644087cd3385048e5d9cdd163689a2db54f277 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceWithInFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
d9c93df57473f0807166b097f9a6c5b1f82828a8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
aa0cb9841ed37b4637217d390487432025204d7c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedInFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
9b5eeda26137fcb00c67fee0d5e766595f6c238e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
fd57c9914323077b0224357e9087930f2edc0395 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
c046ee0870cc236f990ce24be32770e72860a833 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
d27b975951bc90629f63cba8c5f8851ac99e729b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
3a97c140a428383105adb620ec278955457d73bb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
dd02cabca41b5c4fe2a3f17ea0863bbe5abd86c8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfThen LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
82b755fd012481e9d0b2c5173ff923720de26cdc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
d61742df0f3f5445cf9563f622d1c7bcf0a681e4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfElse LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
e649b1acae504205e7a5225ea079d30bc73231f4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
b0646dc33158582d5bab2115a4c4f373635fe325 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Domain LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
968792eb9f9b19d9b5d2e54b2a1211525ba28807 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
2ee804910705d1883ea223438c8be7c52efa31c0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Unchanged LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
b33df3dea58f42e98a21a6b4f3b72609c9298a8d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
9bcfc15b527c5a268e9b623cfd907383f448982a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
b79b355fd757a272b405cfa8e125ca1c51b4b957 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
c5ca6712b1562912107a0fb117895dd2b32c1f90 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
b2ce24bb72451118c651559f486d02d70185a3ef TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
40325cef33061efa83ee2ff43ed7825adc5ce069 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
d55b10f8b4442fdfe96b35751c5eeb23383a0491 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
7954907619a8d1e220f67b74ce0c70590f0fe9fe TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagBagIn LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
8965c1d6ad1f1e75e62e723ab53b33e85dc0f086 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
d88a88c03b682c2dd9cc738b38c6d6cfe31de539 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
75bc6bad36a3001fabd6cc95db8da19561f86b36 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
4064b59c9303afeb8a0e05da6bcbd7b290a032f3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqAppend LetDefFun False Passed
  • Model Under Test
  • Equivalent Model