Hi all,
I posted a longer version of this a couple of weeks ago that didn't get much traction — I think it asked too many things at once, so I'm narrowing it to the one question I actually need help with.
I have a working, TLC-verified Paxos variant (SynodEnergy) where nodes have an energy state (High/Low/Off) and lose in-memory vote state on Low→Off. TLC finds the expected crash-amnesia counterexample to agreement, tracked via a history variable:
That part I'm happy with. My question is about the environment model, and it's a modelling-idiom question, not a protocol one.
I want to replace the classical DLS partial-synchrony assumption (GST as an adversarial unknown constant) with an environment that cycles ergodically between a "good" set of nodes (powered, synchronous within Δ) and a "bad" set (unpowered, messages delayed arbitrarily), so the system re-enters the good regime infinitely often. Conceptually this is a Markov chain running alongside the protocol, and GST becomes a stopping time rather than a constant.
Concretely: what's the idiomatic TLA⁺ way to express "the environment returns to the good regime infinitely often" so that TLC-checkable liveness follows? My instinct is to model the environment as a non-deterministic EnvStep action over a regime variable and lean on weak/strong fairness of the good-regime transitions to get the "infinitely often" behaviour, keeping everything non-probabilistic so TLC still works. Is that the right instinct, or is there a cleaner pattern people use for regime-switching environments?
Two smaller things, only if it's easy:
Happy to share the full spec if useful. Thanks very much for any pointers.