[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] What's wrong with the following behaviors?

I defined a array to descibe a set of  ordered  message queues.

CONSTANT SRVLET,  \* The set of resource tcfs client

  S2CMsgQ,     \* The Msg Queue of Server to Client TCFS Messages

TCFSInit ==  /\ S2CMsgQ = [Cli \in SRVLET |-> <<>>] 

Then, in a certain Scenario f the NEXT state,  I want to  append a dedicated message to each of the QUEUE in the arrary :

 /\ ( \A m \in SRVLET : S2CMsgQ[m] ' = Append(S2CMsgQ[m],[type |-> "sub notify",                    \* Send subed notify message to all  cli
                                          SubedList |-> GetValue(m)])) 

But the TlC report the folowing  runtime error:

In evaluation, the identifier S2CMsgQ is either undefined or not an operator.
line 113, col 54 to line 113, col 60 of module TCFSProtocol    .

I am really confused and need your advice.                          

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/c2161717-9392-4a27-abe4-bbe5b40a047a%40googlegroups.com.