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.