Re: [tlaplus] help understanding TLC error

[Stephan Merz <stephan.merz@xxxxxxxxx>]

For TLC to be able to evaluate an action, the first occurrence of a primed variable should be of the form

x' = ....     or     x' \in ....

Later occurrences refer to the value assigned to that variable by this initial "assignment".

In your spec, the first occurrence of carts' appears in the expression carts'[c], and TLC attempts to retrieve the value of carts from the (partly constructed) successor state, but doesn't find a variable of that name. Hence the error message.

Hope this helps,
Stephan

> On 27 Sep 2019, at 17:52, 'Marko Schuetz-Schmuck' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
> 
> Dear All,
> 
> I'm puzzled as to why TLC gives me an error when checking the
> following. I'm aware that the two lines before the commented-out line
> and the commented-out line are not equivalent. What I don't understand
> is why TLC give the error message:
> 
> In evaluation, the identifier carts is either undefined or not an operator.
> line 12, col 45 to line 12, col 49 of module Dummy1
> 
> The location is the first occurrence of carts' in the Next action.
> 
> Thanks in advance for help with this.
> 
> Best regards,
> 
> Marko
> 
> ------------------------------- MODULE Dummy1 -------------------------------
> EXTENDS Integers, Sequences
> VARIABLES carts, count, item 
> Customer == 1..3
> MaxBag == 10
> Items == 1..10
> Init == 
>  /\ carts = [c \in Customer |-> <<>>] 
>  /\ count = 1
>  /\ item = 1
> Next == 
>  /\ \A c \in Customer \ {(count % 3) + 1}: carts'[c] = carts[c]
>  /\ carts'[(count % 3) + 1] = carts[(count % 3) + 1]  \o <<item, count>>
>  \*  /\ carts' = [carts EXCEPT ![(count % 3) + 1] = @ \o <<item, count>>] \* this does not cause an error
>  /\ count' = count + 1
>  /\ item' = item + 1
> =============================================================================
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/874l0xwxc2.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2E52D050-80BD-479B-B79E-7BBDF2F50B97%40gmail.com.