[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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>

--
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/75d69008-60e4-4000-9c1a-76c178517d0f%40googlegroups.com.