Re: [tlaplus] Guarantee message passing

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hi, Andrew

I read Leslie's paper and thought about it for a while. I'm now trying to implement its concepts in my system. By adding a timeout, it would still be possible for a process to timeout, which I don't want in this case. Since I'm implementing a system with no delays (unless no one is active), I think I should specify it as Send and Receive in the same action, as Stephan said.

Now I have another question: couldn't I guarantee immediate responses in a "Send(p) and Reply(p)" system (instead of the "Act(p)" system) by adding Strong Fairness to the Reply action?

Jones

On Thursday, 18 November 2021 at 11:47:23 UTC-3 andrew...@xxxxxxxxx wrote:

One way of modeling this is as a real-time system, with upper-bound and lower-bound timers. See Leslie's paper Real Time is Really Simple.

Andrew

On Thursday, November 18, 2021 at 7:42:49 AM UTC-5 jone...@xxxxxxxxx wrote:

Hello Stephen,

I see. It's a safety property. I was worried sending and receiving a message in the same step would be incorrect in a more... concrete specification (closer to programming languages). My thinking was more in line of "how do I guarantee the next step will be a Reply step from some process after a Send step?" So it seems, in idealized networking conditions, I should Send and Receive in the same step.

Thanks,

Jones

On Thu, 18 Nov 2021 at 05:25, Stephan Merz <stepha...@xxxxxxxxx> wrote:

A process reacting immediately to a received message is a safety property, so this should be specified as part of the next-state relation, along the lines of

Act(p) == \E q \in Procs : \E msg \in msgs[q,p] :

  /\ msgs' = [msgs EXCEPT ![q,p] = @ \ {msg},

                          ![p,q] = @ \cup Answer(p, q, msg)]

  /\ ... \* update of local variables

assuming that msgs is a two-dimensional array containing the messages in transit between processes.

Stephan

On 18 Nov 2021, at 04:20, Jones Martins <jone...@xxxxxxxxx> wrote:

Hello everyone,

Sorry for keeping this too abstract. I may give an example later on if necessary.

In a process communication network, is there any way to guarantee a process to respond to some message immediately (or as soon as possible) after receiving it?

I'm dealing with timeouts, but I'm modelling a system with perfect communication (there are no delays, no lost messages). Since there are no delays, we expect other processes to respond immediately. I tried to add Strong Fairness to this "Respond" action, but it still does not guarantee anything.

Regards,

Jones

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5084e198-9a83-4961-bc96-c4cc287e07dbn%40googlegroups.com.

--

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Pq2V5769DTs/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A9F2B199-99B3-4607-BC33-E32C2747E756%40gmail.com.

-- 
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/d6da9462-5453-4be3-9d8f-e44de62f4741n%40googlegroups.com.