[tlaplus] How to choose dedicated Subset from the original Set

[dongluming77@xxxxxxxxx]

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 was awaiting for the solution, thanks!

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8cb2d6db-30be-48ca-981d-c80f89d7fd8c%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.