| 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+unsubscribe@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/A9F2B199-99B3-4607-BC33-E32C2747E756%40gmail.com.
|