help understanding TLC error

[Marko Schuetz-Schmuck]

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

[Stephan Merz]

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

> --
> 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+u...@googlegroups.com.
> 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.

[Marko Schuetz-Schmuck]

Stephan Merz <stepha...@gmail.com> writes:

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

Yes. Thanks.

Marko

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2E52D050-80BD-479B-B79E-7BBDF2F50B97%40gmail.com.

--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681