Re-framing an earlier question: idiom for a Markov-modulated environment alongside a protocol spec

28 views

Skip to first unread message

Abib Duut

unread,

Aug 24, 2026, 9:11:50 AM (11 days ago) Aug 24

to tlaplus

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:

SafetyInv == Cardinality(chosenHist) <= 1

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:

Any existing specs modelling regime-switching or environment fairness conditions I should read first?
If I later want the actual almost-sure liveness statement (consensus completes with prob 1), is the accepted path to hand the model to PRISM/Storm, or has anyone done a TLA⁺-side treatment?