I defined a array to descibe a set of ordered message queues.
CONSTANT SRVLET, \* The set of resource tcfs client
VARIABLES
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.