Re: [tlaplus] Idiomatic TLA⁺ for 'environment returns to good regime infinitely often

Hello,

using an environment action together with a suitable (probably weak) fairness hypothesis sounds like a sound model.

Verifying "almost-sure" (probability 1) properties of finite Markov chains typically does not require using a probabilistic model checker. See [1, section 3, qualitative reachability] and the references therein for more information.

Hope this helps,

Stephan

[1] https://dl.acm.org/doi/pdf/10.1145/2933575.2934574

On 29 Aug 2026, at 18:50, Abib Duut <k.aduut@xxxxxxxxx> wrote:

Hi all,
I have a TLC-verified Paxos variant where I want to replace the classical GST partial-synchrony assumption with an environment that cycles between a "good" regime (synchronous) and a "bad" regime (arbitrary delays), returning to good infinitely often.
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 a non-deterministic EnvStep action over a regime variable, using weak/strong fairness on the good-regime transitions to get "infinitely often," keeping everything non-probabilistic so TLC still works — is that right, or is there a cleaner pattern?
Two smaller things if easy:

Any existing specs modelling regime-switching or environment fairness I should read first?

If I later want the almost-sure liveness statement (completes with prob 1), is the accepted path to hand the model to PRISM/Storm, or has anyone done a TLA⁺-side treatment?

Happy to share the full spec. Thanks for any pointers.

--
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 visit https://groups.google.com/d/msgid/tlaplus/812f5269-42f5-4039-8fef-504f30d8ee15n%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 visit https://groups.google.com/d/msgid/tlaplus/D04C3CA1-DB4A-41CB-88ED-8E7F9445D301%40gmail.com.