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

Re: Model evaluator forgetting about state variable

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


   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?