[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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


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