Notes on understanding fairness concepts

[Srikumar Subramanian]

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