Hyperbook section 4.6: suggested clarification

[angus....@xxxxxxxxx]

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.