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

[Abib Duut <k.aduut@xxxxxxxxx>]

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.