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

Thanks a lot!

Hello,

in order to select the elements of a message buffer whose first item equals a given key, you can define the operator

FilterMsgID(buf, key) == { msg \in buf : msg[1] = key }

Your attempt does not work for multiple reasons, concerning TLC the most fundamental one is that your action does not assign a new value to the variable Rcv. Remember that TLC interprets as assignments formulas of the form

Rcv' = ...    or    Rcv' \in ...

You can use the operator FilterMsgID above in the definition of an action, for example

Rcv' = FilterMsgID(Rcv, "c1")   or   Rcv' = Rcv \ FilterMsgID(Rcv, "c1")   etc.,

depending on what your intended application is. I suggest that you separate the definition of an action and the definition of operators such as the one above: this will make your specification much more readable.

Hope this helps,
Stephan

P.S.: Please do not attach files to messages sent to the group unless absolutely necessary, such as a screenshot of the Toolbox if you report a putative Toolbox problem that would be too hard to describe in a text message. -s

On 18 Jul 2019, at 16:28, LUMING DONG <donglu...@xxxxxxxxx> wrote:

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

<捕获.PNG>

--
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 tla...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.