Looking for TLA+ module from Lamport's paper

[mrynd...@gmail.com]

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.

[Leslie Lamport]

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

[mrynd...@gmail.com]

Thank you very much Leslie!

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

?

[Leslie Lamport]

I don't remember how Dist and Ldr are defined, so I don't know how to represent the set of all values  Dist(n, Ldr(n)) for nodes in n, or how to define the maximum of that set.  If you can't figure these things out, I'm sure someone in the group can explain it to you.  But, since Dist takes two arguments, it couldn't very well be written Max(Dist(all_nodes)).

I believe the paper talks about the use of discrete time, which involves replacing Reals by Ints, though I doubt if Nat is a suitable replacement for {r \in Real : r > 0}.

[mrynd...@gmail.com]

Okay, thanks again! I'try to figure this out myself. It will be an excellent exercise.