[tlaplus] Notes on understanding fairness concepts

[Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx>]

I'm a newbie to TLA+ and have been trying to familiarise myself with the fairness concepts. I made some notes along the way that really helped me see weak and strong fairness from the basics. Sharing here in case others find it useful - http://sriku.org/posts/fairness-in-tlaplus/

TL;DR - I found the ideas of "progresses" (= always eventually happens) and "stabilizes" (= eventually always happens) as intermediate concepts very useful to "chunk" the understanding of the fairness formalisations. I came across these words in a Caltech course slide deck - http://www.cds.caltech.edu/~murray/courses/afrl-sp12/L3_ltl-24Apr12.pdf (pdf link). To me, this way felt a wee bit better than the appendix section in Hillel Wayne's article on stuttering and fairness.

-Srikumar

This mail contains confidential information intended only for the individual(s) named. If you’re not the named addressee, don’t disseminate, distribute or copy this e-mail. Please notify the sender immediately and delete it from your system.If you wish not to receive such e-mails you may reply with text “Unsubscribe”.

-- 
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/7d12aefa-612b-4648-90a3-c2043fd6c727n%40googlegroups.com.