Hi Ron
Unfortunately I do not understand TLA+ as well as I understand operational semantics. My problem is trying to understand the relation between PlusCal and the State Graphs. You may well be correct that there is no easy way to use Temporal Logic to define fairness the way I think is natural from the perspective of the operational semantics. When using TLC to model check the finite state approximations of the potentially infinite state State Machines it would seem helpful to provide fairness analysis on these approximations and it is easy enough to check such fairness on the State Graph even if it is hard to formulate in temporal logic.
One question remains would it be reasonable for an engineer (say one of my students) to expect my simple algorithm to terminate given fair behavior. If so that would mean the technical definition of fairness in TLA+ is at odds with this engineer's intuitions. So how can I explain intuitively where their intuitions have lead them astray or at least are different to the notion of fairness embedded in PlusCal / TLA+? I could say fairness is only understandable at the TLA+ code level and not at the PlusCal level but this would not be very helpful to the student.
As it stands, and with the limit of my understanding, It appears that either... or... is inherently unfair (because of the way steps are built by the translation) but this is a little unfortunate and before I tell my students this I would like to know if I have made some mistake.
p.s. many thanks for the help with this.