Hi, AndrewI 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?JonesOn 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.AndrewOn 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,JonesOn 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 variablesassuming that msgs is a two-dimensional array containing the messages in transit between processes.StephanOn 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.