Re: Unclear TLC evaluation behavior

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

OK, I think I understand the problem now. It's a combination of my misunderstanding _and_ TLC's evaluation. I understood that `Next` is simply a relation between a state and a primed state, but I was under the (misguided) impression that an _expression_ of the sort `x' = ?` always evaluates to TRUE in TLC when first encountered. That indeed doesn't make sense. What if the value is FALSE? x' wouldn't be specified. So then I tried:

Next ==

    IF Sub THEN 

        a' = ~a

    ELSE

        /\ UNCHANGED a

        /\ x' = x + 2

But this fails with the same error, and this time I believe (I hope) that the specification is complete. The reason here is that IF translates to an _expression_ containing a negation of Sub (this behavior occurs whenever a primed "assignment" is negated, like in =>), and when encountered with ~Sub, TLC can't determine the value of x' in its first occurrence, and fails with the error described in the book.

Thanks!

Ron