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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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 <dongluming77@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 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/073a4ba3-a87b-4352-bf0e-7ae68d23b3e8%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
<捕获.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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1D5236BD-167C-4A12-9B69-B82D3F9B1032%40gmail.com.