The thing I don't understand is how should I compute 'the maximum of the c(n) for all nodes n', so the maximum of 'Dist(n, Ldr(n))'.
Is this just 'Max(Dist(all_nodes))', so it depends only on Nbrs?
Also the file Leader.tla in TLC gives me:
Evaluating assumption line 62, col 8 to line 65, col 68 of module Leader failed.
Attempted to check if the value:
1
is an element of the string "Reals"
Is it okay if I change:
{MsgDelay, TODelay, Period} \subseteq {r \in Real : r > 0}
to:
{MsgDelay, TODelay, Period} \subseteq Nat
?
W dniu czwartek, 7 listopada 2019 20:24:58 UTC+1 użytkownik Leslie Lamport napisał:
I have attached Leader.tla.
Σ is defined in the two sentences beginning "Formula" on line 7
of page 58. The definition of Correctness in module Leader tells you
that c(n) equals
Period + TODelay + Dist(n, Ldr(n)) * MsgDelay
Leslie
On Wednesday, November 6, 2019 at 7:08:48 AM UTC-8, mryndzionek@... wrote:
I'm looking for the 'Leader' module from the excellent paper
Real Time is Really Simple (page 33). If the module is not available online then I think I'll be able to recreate it in toolbox, but there is one more detail I don't understand. It's the symmetry view described on page 58. What is the actual formula I need to use in TLC for Σ? Also, are there any more comprehensive materials/guidelines available regarding symmetry view settings in TLC?
The techniques described in this paper look to me as very useful for RF mesh protocol design, but I think it is crucial to fully understand the symmetry views settings in order to fully leverage model checking capabilities for such specs.
Or am I maybe overestimating the possibilities offered by these techniques and should instead look at something different?
Help is greatly appreciated.