Re: How does Fairness relate to the State Graph

   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.

It is pointless to ask what corresponds to someone's intuition of what
fairness means. We are concerned with specifying systems, not reading
people's minds. The concept of fairness in this context has been
discussed since the 70s. In 1986 Nissim Francez published a book
titled "Fairness". One of the strengths of TLA is that it is the only
formalism I know of capable of simply and elegantly expressing what
computer scientists have meant by fairness.

   So how can I explain intuitively where their intuitions have led them
   astray or at least are different to the notion of fairness embedded in
   PlusCal / TLA+?

People have difficulty understanding fairness and, more generally,
liveness. I suspect that this stems from not having a good
understanding of quantification, so they can't immediately "feel in
their gut" the difference between \A x : \E y and \E y : \A x. But
for whatever reason, you should expect that you and your students will
have difficulty with fairness. The only thing to do is to patiently
explain the WF and SF operators to your students in terms of
assertions about behaviors. Since teaching something is a great way
to learn it, at least you'll come to understand it fairly quickly.

   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.

Your students shouldn't be surprised that there are things they can
express in PlusCal that they can't express in C++. It won't surprise
them to learn that there are things they can express in TLA+ that
aren't easily expressed in PlusCal. The farther away you get from
the math that describes what's really going on, the less expressive
the language is. PlusCal looks more familiar to your students
than TLA+, and can be more convenient to use for some things--mainly
for multithreaded algorithms because it handles the pc variable for
you. But that comes at a cost. It's always possible to modify
the fairness property produced by the PlusCal translator. Remember
that if the PlusCal code is

      A : either x' = x+1 or y' = y+1 ;

you can express fairness of an A action that increments x by writing
WF_vars(A /\ x'#x).

Leslie