Hi Andrew,That wasn't clear to me, then. I thought it was just a standard procedure for real-time spec actions to be enabled.After thinking about Stephen's new solution, I believe timeouts are the way to go…"Pending messages" in a spec where processes can deactivate at any moment wouldn't work (as intended) since these messages wouldn't be answered immediately. So we get to a situation where we can't distinguish between delay and impossibility of sending in a spec that doesn't allow "impossibility of sending messages" when there are other active processes.Thanks,JonesOn Tue, 30 Nov 2021 at 13:27, Andrew Helwer <andrew...@xxxxxxxxx> wrote:Just because you add timeouts in your spec doesn't mean it's possible for a process to timeout (unless you want that); if you look at the implementation of the Tick operator which advances time, it will only advance by some quantity if advancing doesn't cause an upper-bound timer to reach zero. This is equivalent to encoding an assumption in your system that no process will ever timeout.Of course if later you want to model timeout failures that is also easy to do; you just modify the Tick operator.Andrew--On Monday, November 29, 2021 at 4:32:51 PM UTC-5 jone...@xxxxxxxxx wrote: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.
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/abf0103d-84dc-40d8-a0a9-c9c3bca82f04n%40googlegroups.com.