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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 14 Aug 2015 07:20:20 -0700 (PDT)*Cc*: rws...@xxxxxxxxx*References*: <23f1a0ad-03b2-44b2-a1c9-1e35162c8886@googlegroups.com>

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

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)

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 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

/\ 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

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

/\ UNCHANGED x

However, you apparently expect this to work:

Next == /\ Print(42, x' = x)

/\ UNCHANGED x

/\ UNCHANGED x

Can you explain why?

**References**:**Model evaluator forgetting about state variable***From:*rws . . .

- Prev by Date:
**Re: Model evaluator forgetting about state variable** - Next by Date:
**Some feedback from a new user** - Previous by thread:
**Re: Model evaluator forgetting about state variable** - Next by thread:
**Some feedback from a new user** - Index(es):