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

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

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.