\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{What is Strong Fairness?}
\file{strong-fairness2}
\makeindex
\begin{popup}
\subsection*{What is Strong Fairness?}
  \tindex{1}{strong fairness}%
  \ctindex{1}{fairness!strong}{fairness-strong}%
  \tindex{1}{strongly fair}%
  \ctindex{1}{fair!strongly}{fair-strongly}%
  \ctindex{1}{SF@\icmd{SF}}{SF}%

  \vspace{-\baselineskip}%

Naming a property \emph{weak fairness} suggests that there is also a
property named \emph{strong fairness}.  Strong fairness of an action
$A$, written $\SF_{vars}(A)$, is the condition obtained by replacing~3b 
with:
\begin{enumerate}
\item[3b$'$.] If the behavior is infinite, then there is no $n$ such
that the infinite behavior $s_{n}->s_{n+1}-> \cdots$ has no $A$ steps
but $A$ is enabled in infinitely many of its states.
\end{enumerate}
This is stronger than 3b because the condition \emph{$A$ enabled in
infinitely many states} in 3b$'$ that must not hold is weaker than the
corresponding condition \emph{$A$ enabled in
all states} that must not hold in 3b.

\medskip

Weak fairness is a more common requirement than strong
fairness---though for many specifications, the two conditions are
equivalent.  For example, weak and strong fairness are equivalent for
the actions $Producer$ and $Consumer$ of algorithm $Alternation$.
This is because conditions 1 and~2 imply that an infinite behavior
must have infinitely many $Producer$ and $Consumer$ actions.
\end{popup}
\makepopup