I Defined a Message Buf with the format as below:
Message = {<<"c1",{"event2"}>>,<<"c2",{"event3"}>>,<<"c1",{"event1"}>>}
Once the Meesage got by the receiver with the ID of "c1", it should only choose the Subset with Element key as "c1".
That's just a example, the true object is let each receiver only choose the correponding Subset.
I want to write a general function to fufill the duty, but found it is very difficult. Because the TLA+ funcion is usually used for Sequence and Tuple.
So I tried to write the following _expression_ in the NEXT state formular
to update the receiver's state. But it not work, TLC report error!
RxChoseMsg(Rcv,k) == /\ (\A n \in Rcv[k]': (n \in Message ))
/\ (\A m \in Rcv[k]': (m[1] = k))
/\ (\A i \in Message :(
IF i[1] = k
THEN
i \in Rcv[k]'
ELSE
i \notinRcv[k]'))
I am awaiting for the solution, thanks!
