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

Thanks a lot!

在 2019年7月20日星期六 UTC+8上午1:10:03，Stephan Merz写道：

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
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!

<捕获.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.
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/073a4ba3-a87b-4352-bf0e-7ae68d23b3e8%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
<捕获.PNG>