Stephan Merz <stephan.merz@xxxxxxxxx> 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
> 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.
--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
--
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/871rw1wsnl.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
Attachment:
signature.asc
Description: PGP signature