# [tlaplus] Re: problems debugging liveness errors.

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.