I don't understand what you mean by fairness. You come from
the world of process algebra, and I expect that the word means
something different there. So, let me explain what fairness means.
I'll describe it in terms of TLA+, but the concepts are
language-independent. They apply to any language in which a
specification is something that is true or false on an individual
behavior, where a behavior is a sequence of states and/or actions.
The last I heard, which was quite a while ago, process algebras are
not such languages.
The meaning of a TLA+ temporal formula is a predicate on behaviors,
which are infinite sequences of states. Any such predicate can be
written as the conjunction of a safety property and a liveness
property. A safety property is one that is true for a behavior iff
it's true for every finite prefix of the behavior, where a finite
sequence of states is defined to satisfy a property iff the behavior
obtained by stuttering its final state forever satisfies the property.
A liveness property is one such that any finite sequence of states can
be completed to a behavior that satisfies the property. If S is a
safety property and L is a liveness property, we say that L is a
FAIRNESS PROPERTY FOR S if any finite sequence of states that
satisfies S can be completed to a behavior that satisfies S /\ L. A
spec written with such a fairness condition is called MACHINE CLOSED.
(More precisely, the pair (S, L) is called machine closed.) Specs
that are not machine closed are weird, because the liveness property L
disallows finite behaviors that satisfy S. We usually want to avoid
them.
In TLA+ and in many other spec languages, safety properties and
liveness properties are specified separately. In many languages,
safety is specified by some sort of code--just as PlusCal does. In
TLA+ it's expressed by a formula of the form Init /\ [][Next]_vars.
In many languages, liveness is specified by putting weak and/or strong
fairness conditions on actions. The reason we call WF and SF fairness
conditions is that the conjunction of formulas WF_vars(A) and/or
SF_vars(A) for subactions A of Next is a fairness condition for Init
/\ [][Next]_vars. A SUBACTION A of Next is an action such that, from
every reachable state, an A step is a Next step. Most practical
languages allow you to add weak/strong fairness conditions only to
particular subactions of Next. Effectively, they write the next-state
relation as the union of some particular subactions and can add
fairness conditions only to those subactions. PlusCal is such a
language. As has been observed on this group, this restriction can
make it hard to write a desired fairness condition in PlusCal. I
believe the same is true for any method that adds fairness conditions
in this way. At best, they require you to rewrite the safety part of
the spec in a less natural way to express the desired fairness
property. At worst, they can't express it. TLA+ doesn't have this
restriction, because you can write a WF or SF condition on any
subaction of Next. I have never had any trouble writing a fairness
condition that I wanted in TLA+.
There are rare situations in which you want to write a spec that is
not machine closed. You can do that easily in TLA+ with WF and SF
formulas applied to actions that are NOT subactions of Next. (I've
done that in a paper called "A Lazy Caching Proof in TLA".) Moreover,
writing a proof that one spec implements another can require adding an
auxiliary variable that produces a spec that's not machine closed.
Any language that allows you to add fairness conditions only to
subactions of the next-state action won't let you write such a spec.
Now that I have explained what fairness means, perhaps you will be
able to explain what you mean by "fairness might be better viewed as a
function of more than one step."
Leslie