Hyperbook section 4.6: suggested clarification

[angus....@gmail.com]

Hi,

When I first reached this point in the book, I added 'Termination' to the model and obtained the expected temporal property violation. However, this didn't disappear when '--fair algorithm' replaced '--algorithm'. After some consideration, I realised I needed to swap my model from 'Initial predicate and next-state relation' using 'Init' and 'Next' under 'Model Overview', to 'Temporal formula' using 'Spec'. The result described in the text was then obtained.

In retrospect, this seems obvious because this is the only place in the specification that 'WF_vars(Next)' appears. However, the rest of the text has been abundantly clear and I stumbled because I'd previously had no problem with this model configuration. Making the requirement explicit would have saved a little head-scratching!

Many thanks,
-Angus.

[Leslie Lamport]

Thanks for the problem report. I'm curious about how you created a model using "Init" and "Next" rather than "Spec" in the first place, since the default model for a specification obtained by translating a PlusCal algorithm uses "Spec".

Leslie

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.