Unclear TLC evaluation behavior

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

While writing a specification I came across a TLC evaluation strategy that isn't clear to me. I've reproduced it in the following trivial (and nonsensical) spec:

    VARIABLE x, a

    vars == <<x, a>>

    TypeOK == /\ x \in Nat

                       /\ a \in BOOLEAN

          

    Init == x = 1 /\ a = TRUE

    Sub == x' = x + 1

    Next == (omitted)

    Spec == Init /\ [][Next]_vars

When I define Next as 

    Next == 

        IF Sub THEN 

            a' = ~a

        ELSE

            UNCHANGED a

and run TLC, I get the error "In evaluation, the identifier x is either undefined or not an operator", which points to the x' token of Sub. The same happens when I define next as

    Next == 

        Sub => a' = ~a

When I define Next to be

    Next == 

        LET p == Sub IN

        a' = ~a

I get the error "Successor state is not completely specified by the next-state action" (this could perhaps be explained by lazy evaluation).

Reading about TLC's evaluation rules in chapter 14 of "the book", I couldn't find something that would explain this behavior. Does TLC only evaluate primed assignments when written as simple conjuncts or disjuncts?

Ron