I don't see what's going on in the example in your first email, but
judging from your second email, I expect that the _expression_ TLC is
complaining about is
/\ Print("...",
some _expression_ containing a variable x that's primed)
in a context in which TLC has not yet determined the value of x'.
If this is not the case, then we will need a complete spec to see
what's happening.
If that is the problem, consider a spec with
VARIABLE x
Init == x = 1
Next == /\ x' > 0
/\ UNCHANGED x
I trust you will understand why TLC reports an error when trying to
evaluate the first conjunct of Next. If not, you should read Section
14.2.6 of "Specifying Systems". You will then understand why TLC
reports essentially the same error with
Next == /\ Print(42, x' > 0)
/\ UNCHANGED x
However, you apparently expect this to work:
Next == /\ Print(42, x' = x)
/\ UNCHANGED x
Can you explain why?