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

*From*: angus....@xxxxxxxxx*Date*: Sat, 25 Apr 2015 17:25:04 -0700 (PDT)

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.

**Follow-Ups**:**RE: [tlaplus] Hyperbook section 4.6: suggested clarification***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Re: Can not edit "What is the model" and "What is the behavior spec?"** - Next by Date:
**RE: [tlaplus] Hyperbook section 4.6: suggested clarification** - Previous by thread:
**Re: [tlaplus] Re: Can not edit "What is the model" and "What is the behavior spec?"** - Next by thread:
**RE: [tlaplus] Hyperbook section 4.6: suggested clarification** - Index(es):