Hi Leslie
Many people are well aware of what fairness means. Unfortunately they how they interpret the details of this depends upon their formal background. Personally I have more of a background in operational semantics than in temporal logic. Although TLA+ rests on Classical and Temporal Logic there is a State Graph that I had been applying by operational semantics understanding to.
Let us take fairness to mean "if an event is offered infinitely often then it must be taken in a finite number of steps". On the State Graph what is fair behavior depends upon how you interpret "an event is offered" this, in operational semantic, is often thought to mean that the loops in the operational semantics that can be exited will eventually be exited.
Clearly this is not the interpretation in the PlusCal TLA+ translation where it is not the individual transitions of the State Graph that are offered but the labeled steps.
Certainly I had not picked up on the inherent non determinism of either.. or.. and my intention was to build an algorithm that any fair behavior of would terminate.
I am not trying to say there is anything wrong with the interpretation "an event is offered" as being a labeled step it simply was not my original understanding. Given that this is how TLA+ works you can say I was trying to encode an PlusCal algorithm that performed either of two steps that had different labels. I am still not sure if this is possible in plusCal.
I agree completely with Leslie
"The translation doesn't make anything happen. "
and had certainly not meant to give the translation with any agency. All that I intended was that : the State Graph is a formal representation of the State Machine that gives meaning to the PlusCal/TLA+ syntax. As, I assume, TLA+ is rich enough to define either any State Machine, or at least the state machines we are considering, then the State Graph that I outlined could be defined as a TLA+ translation of either.. or... (or some new command either+ .. or ..)
This would allow exactly the same definition and implementation of fairness but to give an alternative result by virtue of the state graph branching with different named steps.
kind regards david