[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Notes on understanding fairness concepts

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.


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.