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.
Attachment:
signature.asc
Description: PGP signature