My last reply was a little rushed as it was literally 15mins before giving a lecture on fairness. So again many thanks.
You say that
strong fairness is rarely used and may be hard to implement. In order to establish certain liveness conditions weak fairness will not suffice and then its strong fairness or some bespoke temporal logic restriction. Consequently I only use strong fairness when I see no viable option.
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.
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.
There are many aspects to TLA+ that work very smoothly but liveness checking in TLA+ I still find a painstaking and error prone task. Hopefully more practice will help. regards david
On Friday, 3 May 2019 08:54:16 UTC+12, david streader wrote:
Many thanks
Initially I thought that, in order to establish strong fairness you only needed to restrict a step when there was a choice between two transitions of the same step. That is when a step itself was nondeterministic. But I can see that even with deterministic steps all you need is the exiting step to be some where in the loop then you need to restrict the step.
Strong Fairness in TLA+ is quite different from that in process algebras such as Fair Failure semantics. It is interesting that liveness conditions are so hard to verify in TLA+ whereas in process algebras they are, by default, what are normally specified and verified.
Finally I am getting the differences between process algebra and TLA+
regards david
On Friday, 3 May 2019 06:03:42 UTC+12, Jay Parlar wrote:
One final comment: I'd be wary of the number of strongly fair labels you've placed in your spec. My understanding is that strong fairness is rarely used, as it's difficult to implement actual systems that satisfy it. It definitely has its place, but it's not common. Placing it on every process and label in your spec is most likely not the correct course of action.
I understand doing it given your initial assumption that "looping forever was prohibited by these strong fairness clauses", but as we've shown, your assumption was incorrect.
I just don't want you or your students to think that the right way to approach these specs is by marking everything as strongly fair.