Re: [tlaplus] Declared variables found undefined during evaluation

[Zixian Cai <fzcz...@xxxxxxxxx>]

It makes sense now. Thanks Leslie and Stephan.

> On 24 Aug 2018, at 06:45, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
> 
> Just to clarify Stephan's response:  The spec you wrote is, I believe, legal TLA+ and means what you expect it to mean.  However, TLC will handle the liveness property only if P is a constant.
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.