I highly recommend you watch Lamport's videos, esp. lecture 9, as it's the best description of liveness in TLA+ that I've seen http://lamport.azurewebsites.net/video/videos.html
On Friday, 3 May 2019 00:35:04 UTC-4, david streader wrote:
It is interesting that fairness in TLA+ is defined on the behaviour with regard to a single step. Where as in a world with concurrent components, say your phone and my phone, a step my phone might take could act unfairly in as much as it prevented the execution of another step on my phone. But, the steps on my phone are fair with respect to steps on your phone as my phone can never prevent your phone from performing its steps. So it would seem that fairness might be better viewed as a function of more than one step. Then steps on distinct processes by default behave fairly with respect to each other and it is only hard to implement fairness between steps on the same process.
Remember that in TLA+, there are no such thing as processes! PlusCal has them, but when it all gets down to TLA+, a process is in the eye of a beholder. You can interpret things however you want. TLA+ is only concerned with the global state of the universe. How you choose to interpret that state is up to you (and the PlusCal translation interprets it in a very specific way).
For your phone example, in TLA+, steps taken on one phone can't prevent another phone from taking a fair action. But if the TLA+ model doesn't have a clean separation between the phones, then you'll see issues.
In particular, fairness in TLA+ is all about whether an _enabled_ action will ever take place. My phone might need your phone to do something in order for my phone to become enabled (like waiting for your phone to send a response to my phone). But if we mark my phone's action as strongly fair, and the action is repeatedly enabled, then my phone will eventually take the step.
What we saw with your spec though was more akin to _both_ phones being able to take the _exact same action_, with no distinction made between which phone is taking it.
I have to admit that, when I place fairness conditions every where, I am being influenced by my past experiences formalising concurrent systems. In process algebras it is decided that every thing is fair or every thing is not fair (largely no distinction is made between strong and weak fairness). In either case, fair or unfair, liveness conditions can be preserved by selecting the appropriate semantics. Consequently I am unfamiliar with using a fairness condition to establish a liveness property.
I'll recommend again that you watch Lamport's videos. The same information is available in other sources (Specifying Systems, The Hyperbook), but the videos are my favourite source. Liveness/fairness is definitely the trickiest concept in TLA+, and I found it worth putting in the extra time to really learn it well.
Jay P.