Re: [tlaplus] Guarantee message passing

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.