[tlaplus] Re: Looking for TLA+ module from Lamport's paper

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/12379c06-f34d-4bb4-bc26-6ee900f836c2%40googlegroups.com.

Attachment: Leader.tla
Description: Binary data