[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 13 Dec 2023 15:44:53 +0100*References*: <CABf5HMjvUJAMb5GW7wLsJPe5Y0deXqC1pr4pRzMZRAchufKOzQ@mail.gmail.com>

Hi Calvin, nice problem! The counter-example computed by TLC shows that there exists a behavior in which it is never the case that all agents are PREPARED. No fairness condition on the transitions of single agents will imply that the states of all agents are eventually aligned. Now, if you model the (initial part of each) agent as a continuous time Markov chain with two states IDLE and PREPARED and some positive transition rates (w.r.t. an exponential distribution) between those two states then you can convince yourself, and a tool such as Prism [1] can confirm, that the mass of executions of any fixed number of such agents such that at all times, at least one agent is in state IDLE, is zero. In other words, almost surely all agents will be PREPARED at some point (and continuing from there [2], they'll align again at some future point with probability 1. If you are willing to rule out such executions, you could add the assumption []<>((\A a \in Agent : state[a] = "PREPARED") \/ (\E a \in Agent : state[a] \notin {"IDLE", "PREPARED"})) to your spec, together with strong fairness for the transitions from PREPARED to DONE. The condition asserts that for as long as all agents perform the loop between IDLE and PREPARED, they'll repeatedly align on state PREPARED. Stephan [2] For the long-term analysis, you may without loss of generality assume that both states are initial.
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/9BF9D95E-0149-4206-BB77-F2897CDCBE10%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] What to do when strong fairness isn't strong enough?***From:*Andrew Helwer

**References**:**[tlaplus] What to do when strong fairness isn't strong enough?***From:*Calvin Loncaric

- Prev by Date:
**[tlaplus] Re: Advent of TLA+** - Next by Date:
**[tlaplus] Re: Advent of TLA+** - Previous by thread:
**[tlaplus] What to do when strong fairness isn't strong enough?** - Next by thread:
**Re: [tlaplus] What to do when strong fairness isn't strong enough?** - Index(es):