Fairness conditions are about what must happen in the limit, they do not express urgency. If you want to separate your receive and reply events and still require that the reply happens before the receiver performs some other actions, you'll want to explicitly block these actions and write, say,
Receive(p) == \E q \in Procs : \E msg \in msgs[q,p] :
/\ pendingReply[p] = None
/\ msgs' = [msgs EXCEPT ![q,p] = @ \ {msg}]
/\ pendingReply' = [pendingReply EXCEPT ![p] = msg]
/\ ...
Reply(p) ==
/\ pendingReply[p] # None
/\ msgs' = [msgs EXCEPT ![p,q] = @ \union {Answer(p, pendingReply[p])}]
/\ pendingReply' = [pendingReply EXCEPT ![p] = None]
/\ ...
and add the precondition "pendingReply[p] = None" to all actions of process p that you wish to block.
This is a simplified version of the timeout that Andrew suggested with an immediate deadline.
Stephan
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...@
gmail.com 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
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
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
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 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.