Re: [tlaplus] Spec formula for Peterson algorithm

the corresponding TLA+ module is contained in the distribution of the TLA Proof System [1] and also available from [2] (with the temporal reasoning steps omitted because TLAPS didn't support them at the time). In short, the module has the definitions

[2] https://members.loria.fr/SMerz/papers/fm2012.html

On 26 Feb 2020, at 15:37, Mursel Musabasic <murselmurga@xxxxxxxxx> wrote:

Hi there,

I was looking for formal specification on Peterson algorithm and came across this publication (https://lamport.azurewebsites.net/pubs/tlaps.pdf) where it says, I quote:

"The temporal formula Spec is the complete specification. It characterizes behaviors (ω-sequences of states) that start in a state satisfying Init and where every pair of successive states either satisfies Next or else leaves the values of the tuple vars unchanged."

I'm having problem with understanding of tuple vars in specified formula. Can anyone explain to me how these variables (turn, flag and pc) relate to tuple vars? I can understand that some variables stays unchanged during verification, but couldn't get it in final Spec temporal formula.

Best regards,

Mursel

--
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/b23791fe-5aa0-48b4-ae13-151105e94d3f%40googlegroups.com.