\documentstyle[twocolumn,twoside]{IEEEtran}

\makeatletter

% file pf.sty
%
% last modified on Thu Jan 18 16:42:04 PST 1996 by lamport

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       THE pf STYLE                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  CONTENTS
%    1. Introduction
%    2. The Basic Commands
%    3. Different Styles of Numbering 
%    4. Indentation
%    5. Assumptions
%    6. Portions of a Proof
%    7. Conjunctions and Disjunctions
%    8. Miscellany
%    9. List of all Commands and Environments
%
%  1. INTRODUCTION
%
%    The pf style provides commands and environments for typesetting
%    hierarchically structured proofs.  Below is an example of what 
%    such a proof looks like, and the commands that generate it.
%    The commands are explained individually below.  Then
%
%    THE OUTPUT                         THE INPUT
%    ~~~~~~~~~~                         ~~~~~~~~~
%    Any text...                        Any text
%                                       \begin{proof}
%    1. Text of step 1.                   \step{label-1}{Text of step 1.}
%                                         \begin{proof}
%       1.1. Text of step.                  \step{label-1.1}{Text of step}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%                                      
%       1.2. Text of step.                   \step{label-1.2}{Text of step.}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%
%       1.3. QED                             \qedstep
%                                            \begin{proof}
%            1.3.1. Text of step               \step{label-1.3.1}{Text...}
%                   Proof: ... []              \begin{proof} ... \end{proof}
%                                            
%            1.3.2. QED                        \qedstep
%                   Proof: ...                 \begin{proof}...\end{proof}
%                                            \end{proof}
%                                         \end{proof}
%
%    2. Text of step 2.                   \step{label-2}{Text of step 2.}
%        Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%
%    3. QED                               \qedstep
%       Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%     
%
%   The best way to read such proofs is hierarchically.  To find out
%   how, search below for the \pfhidelevel command and the \hideqedproof
%   command.
%
%
% 2. THE BASIC COMMANDS
%
% The proof Environment:
%   Increments the proof depth, and indents the enclosed text the
%   appropriate amount.  For example, if the proof environment follows a
%   \step command that produces step number 2.6.7, then the first \step
%   command inside the environment will produce step number 2.6.7.1.
%
% \step{LABEL}{TEXT}
%    This command produces a proof step such as
%        2.6.7.1. TEXT
%    The step number 2.6.7.1 is determined by the position of the \step
%    command in the proof.  The LABEL is a symbol label used to refer to the
%    step number.  A subsequent \stepref{LABEL} command will generate the
%    step number 2.6.7.1.  The same LABEL may be re-used, but
%    not in a context where it is legal to refer to a previous step with the
%    same label.  (See the discussion of step numbering below.)
%    
%    This command is equivalent to
%           \begin{step+}{LABEL}
%              TEXT
%           \end{step+}
%    The step+ environment form is more convenient if TEXT is long or
%    complicated.
%
% \qedstep
%    This command produces something like
%    
%       2.6.7.5. QED
%    
%    If the proof of step 2.6.7 is a sequence of steps (rather than a
%    paragraph proof), then the last step in its proof is normally of this
%    form.  The "QED" in the statement simply denotes the current
%    goal---what must be proved to prove step 2.6.7.  The proof of this QED
%    step will be followed immediately by the
%    \end{proof} command that ends the proof of step 2.6.7.
%    
%    The pf style does not enforce this method of structuring proofs;
%    the proof of statement 2.6.7 could end with an ordinary \step
%    command.
%
% \pf, \qed
%    These are simple text-producing commands that normally begin and end a
%    paragraph-style proof.  However, they are not required.  Remember to
%    put a "\ " after the \pf command, and to tie the \qed command to the
%    last word of the proof with a "~".
%
% \pfsketch
%    
%    An intuitive prook sketch often introduces a multi-step proof, as in
%    
%         1.3. All odd numbers are prime.
%              Proof sketch:  The proof is by induction, with the
%              base case proved in step 1 and the induction step in
%              step 2.
%              1.3.1. The number 1 is a prime.
%                     Proof: ...
%              1.3.2. If n is an odd prime, then n+2 is prime.
%                     Proof: ...
%              1.3.3. QED
%                     Proof: 1.3.1, 1.3.2, and mathematical induction.
%    
%    This is entered as 
%    
%      \step{label-1.3}{All odd numbers  are prime}
%      \begin{proof}
%      \pfsketch\ The proof is by induction...
%       \step{label-1.3.2}{The number 1 is a prime}
%       ...
%      \end{proof}
%    
%    The \pfsketch command is, like \pf, just produces the text.  It isn't
%    required by the pf style.
%    
%
%  3. DIFFERENT STYLES OF NUMBERING 
%
%    In the long style of proof numbering, a step number is something like
%    2.6.7.5, meaning that it is the fifth step in the proof of statement
%    2.6.7, which is the seventh step in the proof of statement 2.6, which
%    is...  Statement 2.6.7.5 has the short name <4>5, meaning it is the
%    fifth statement in the current level-4 proof.  Numbering style is
%    controlled by the commands
%    
%      \pfshortnumbers{N} : Use short step numbers for all levels
%                           >= N (Default is N = 1, using only short
%                           numbers.
%    
%    These are local declarations that obey the usual scoping rules.  Thus,
%    putting a \pfshortnumbers declarations right after a \begin{proof}
%    command causes all steps in that proof to have short numbers.
%
%    Steps 2.6.7.5, 2.6.6.5, and 4.9.1.5 all have the same short numbers
%    <4>5.  However, no ambiguity arises from the use of short numbers
%    because at most one of these steps can be mentioned at any point in a
%    proof.  Let the ANCESTORS of step 2.6.7.5 be steps 2.6.7, 2.6, and 2.
%    Let the ELDER SIBLINGS of step 2.6.7.5 be steps 2.6.7.1, 2.6.7.2,
%    2.6.7.3, and 2.6.7.4.  The proof statement 2.6.7.5 may refer only
%    to steps in the following two sets:
%       (i) The elder siblings of itself and of its ancestors.
%      (ii) Itself and its ancestors.
%    The steps in (i) are the previously-proved assertions that can be used
%    in the proof of 2.6.7.5.  The assumptions of the steps in (ii) are the
%    ones that are being assumed in the proof.  (Assumptions are discussed
%    below.)
%    
%    The command \stepref{LABEL} anywhere in the proof of step 2.6.7.5 (or in
%    the step itself) produces the step number of a step lying in sets (i)
%    or (ii) having LABEL as its label (the first argument of its \step
%    command).  An error message is generated if the \step command has a
%    label that is the label of a step in set (i) or (ii).
%    
%    Note that the last step of a proof is never an elder sibling, so it
%    can't be in the set (i) for any statement.  A QED-step has no
%    assumptions, so it can't be in the set (ii) for any statement.  That is
%    why the \qedstep command does not specify a label.  Actually, \qedstep
%    is defined to equal \label{qedstepN}{...}, where N is the current
%.   level number. Thus, an error will be generated if two \qedstep commands 
%    occur in the same proof, since they will have the same labels.

%
%    Short step numbers are really nice.  They take up less space and are
%    easier to read.  They are the preferred form for long proofs.  However,
%    long step numbers are better for referring to a proof step from outside
%    the proof.  The pf style allows you to print the long numbers of steps as
%    marginal notes, something like
%    
%       Theorem:  ...
%       ...
%     2.4.5.6.         <4>6. All odd numbers greater than 2 are prime.
%     2.4.5.6.1.             <5>1. The number 3 is prime.
%       ...
%    
%    (The long numbers are printed in a smaller font, so it looks
%    better than you'd guess from this.)  The relevant commands are:
%    
%    \pfsidenumbers{N}{D} 
%       Print side numbers for proof steps of all levels \geq N, left-aligned 
%       a distance D to the left of the left margin of the text.
%    
%    \pfnosidenumbers  
%       Do not print side numbers (the default)
%
%
%  4. INDENTATION
%
%    There are two styles of indentation:
%    
%       Long Style 
%          1. XXXXX
%             1.1. XXXXX
%                  1.1.1. XXXXX
%                         1.1.1.1. XXXX
%                                  Proof: ...
%    
%       Short Style 
%          1. XXXXX
%            1.1. XXXXX
%              1.1.1. XXXXX
%                1.1.1.1. XXXX
%                  Proof: ...
%    
%    In the long style, the proof of a statement lines up with the text of
%    the statement.  In the short form, each level is indented the same
%    distance from the next higher level.  The relevant declarations
%    are
%    
%    \pflongindent 
%       Indent proofs to full width of item label
%    
%    \pfshortindent 
%       Indent proofs by the length parameter \pfindent (the default)
%
%
%  5. ASSUMPTIONS
%
%    A common form of a step is 
%        
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%    This asserts that the Prove clause follows from the Assume clause.  The
%    "QED" at the end of the proof of this step refers to the Prove clause.
%    The input to produce this is
%    
%        \step{label-4.5}{
%          \assume{\begin{enumerate}
%                    \item $n$ is an odd number
%                    \item $n>2$
%                  \end{enumumerate}}
%          \prove{$n$ is prime}}
%    
%    The relevant command syntax is
%    
%       \assume{TEXT}
%       \prove{TEXT}
%    
%    The formatting of the enumerate environment is changed to work
%    propertly inside a proof environment.  (It is actually redefined
%    to be the pfenum environment, described far below.)  Note that
%    \label and \ref command for subitem b of item 3 produces the label
%    "3b".  Note: there is an enumerate* environment that is like
%    enumerate, except it indents the items.
%     
%    
%    Another form of assumption is a Case assumption.  The statement
%    
%          <5>1. Case: n is of the form 4n+1
%    
%    means
%    
%          <5>1. Assume: n is of the form 4n+1
%                Prove:  QED
%    
%    where QED is the current goal.  A proof by cases is structured
%    as follows
%    
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%               <5>1. Assume: n equals 4m+1 for some m
%                     Prove:  QED
%                     Proof:  ... []
%    
%               <5>2. Assume: n equals 4m+3 for some m
%                     Prove:  QED
%                     Proof: ... []
%    
%               <5>3. QED
%                     Proof: By <5>1, <5>2, and assumption <4>.2 (which 
%                     states that n is odd), since any odd number has
%                     the form 4m+1 or 4m+3. []
%    
%    A case assumption is produced with a \case command, which works like
%    \assume and \prove.  It has the syntax
%    
%        \case{TEXT}
%    
%    Corresponding to the \assume, \prove, and \case commands are
%    the assume+, prove+, and case+ environments.  For example, \prove{TEXT}
%    is equivalent to \begin{prove+} TEXT \end{prove+}
%    
%    Note the reference, in the proof of <5>3, to the second conjunct of the
%    Assume clause in statement <4>5 as "assumption <4>.2".  Since a proof
%    of a step can only use assumptions in that step or its ancestors, a
%    level number suffices to identify an assumption.  The Assume clause of
%    statement <4>5 is called "assumption <4>".  The ".2" refers to the
%    second item in that clause.  As mentioned below, this use of ".2" to
%    refer to the second component of a conjunction can be used 
%    in other circumstances as well.
%    
%    When long numbering is used, assumptions must be referred to by the
%    name of the statement containing the assumption.  Thus, "assumption
%    2.6.7.5.2" could potentially mean either the Assume clause of statement
%    2.6.7.5.2, or the second item in the Assume clause of 2.6.7.5.  One way
%    to remove the ambiguity is to use something other than "." in long step
%    numbers.  The possibilities 2:6:7:5 and 2-6-7-5 don't look too good;
%    the best alternative to "." seems to be a raised period ($\cdot$).  The
%    "." is changed by redefining \pfdot, as described below.  Assumptions
%    are referred to with the following commands:
%    
%       \levelref{LABEL}
%         If \stepref{LABEL} produces <4>5, then \levelref{label} 
%         produces <4>.
%         If \stepref{LABEL} produces 2.6.7.5, then \levelref{label} also 
%         produces 2.6.7.5.
%
%       \toplevel
%         If \stepref{LABEL} produces <4>5, then \toplevel
%         produces "<0>".
%         If \stepref{LABEL} produces 2.6.7.5, then \toplevel
%         produces "0".
%
%
%  6. PORTIONS OF A PROOF
%
%    You may want to format only part of a proof--for example, you might
%    want to write the proof of statement 2.1.3 as a separate proof.  You'd
%    want something like
%    
%    2.1.3. All odd numbers are prime.
%           2.1.3.1. ...
%    
%    To do this, first imagine the shortest proof you can that has a
%    statement numbered 2.1.3: 
%    
%        1. X
%        2. X
%           2.1. X
%                2.1.1. X
%                2.1.2. X
%                2.1.3. All odd numbers are prime.
%                       2.1.3.1. ...
%    
%    Write this using the \step command and prove environment.  Now, change
%    every \step{LABEL}{X} command to \nostep{LABEL}, and change the proof
%    environments surrounding the proofs of steps 2 and 2.1 by noproof
%    environments.  This yields
%    
%        \begin{proof}
%          \nostep{label-1}
%          \nostep{label-2}
%          \begin{noproof}
%            \nostep{label-2.1}
%            \begin{noproof}
%              \nostep{label-2.1.1}
%              \nostep{label-2.1.2}
%        
%               \step{label-2.1.3} All oddnumbers are prime
%               \begin{proof}
%                  \step{label-2.1.3.1} ...
%               \end{proof}
%              \end{noproof}
%            \end{noproof}
%        \end{proof}
%    
%    which produces the desired result.  Note that the labels of the \nostep
%    commands can be used to refer to the corresponding step numbers.
%
%  7. CONJUNCTIONS AND DISJUNCTIONS
%
%    It is very convenient to write conjunctions as lists bulleted by \land.
%    This is done with the conj environment, where
%    
%     $X =  \begin{conj}    PRODUCES    X =  /\ A
%             A \\ B \\ C                    /\ B
%           \end{conj}$                      /\ C
%
%    The conj* environment is similar, except it numbers the conjuncts.
%    
%     $X = \begin{conj*}    PRODUCES    X = 1./\ A
%            A \\ B \\ C                    2./\ B
%          \end{conj*}$                     3./\ C
%
%    If X is defined in this way, then X.2 denotes the formula B.
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are implemented with the array environment.
%    They should nest properly.  They can be used only in math mode.
%
%
%  8. MISCELLANY
%
%    \pfhidelevel{N} : A counter that controls what levels of proof
%        are shown.  The command \setcounter{pfhidelevel}{2} causes
%        only level-1 and level-2 steps to be printed, and the proofs
%        of level-2 steps (including all level-3 and higher steps)
%        to be omitted.  The default value of the counter is very large.
%        The value of the counter should always be positive.
%
%   \unhideqedproof 
%   \hideqedproof   : Used in conjunction with the pfhidelevel counter.
%        The \unhideqedproof command causes one extra level of proof 
%        to be displayed for the lowest level \qedstep.  The \hideqedproof
%        returns to the default of not showing this extra level.
%       
%    \pflet  : like \prove and \assume, but with keyword "Let"
%
%    \kwfont : Selects the font for the keywords "Proof", "Assume",
%              "Prove", and "Case".  Default is \sc; you can 
%              change it by something like \renewcommand{\kwfont}{\em}
%
%    \pfdot : Defines the "." in long step numbers.  Try
%             \renewcommand{\pfdot}{\mbox{$\cdot$}} for variety.
%
%    \pfindent : The amount by which proof levels are indented in
%                the short indent option.  Changed with \setlength.
%                This is a local declaration.
%
%    \pfstepnumber{LEVEL}{NUMBER}{LONGNUMBER} :
%        Generates either <LEVEL>NUMBER or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    \pflevelnumber{LEVEL}{LONGNUMBER} :
%        Generates either <LEVEL> or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    The following parameters control vertical spacing.  
%    
%      \pftopsep  : space above first proof environment
%      \pfbotsep  : space below first proof environment
%      \pfsep     : space above and below inner proof environment
%      \stepsep   : space above and below proof step
%    
%    The last two are set to zero, and probably should remain there.  It
%    might be desirable to have vertical spacing depend more finely on the
%    level number.  This can be done using the \makefcn command (see far
%    below), and will be if there seems to be a need.  However,
%    zero extra vertical spacing seems to be fine.
%
%    \pf, \qed, \pfsketch  :  Described above.  Can be changed with 
%                             \renewcommand
%
%
%  9. LIST OF ALL COMMANDS AND ENVIRONMENTS
%
%    Text-Producting Commands            Environments
%      \pf, \pfsketch                      proof
%      \qed                                noproof
%      \step                               step+   [version of \step]        
%      \nostep                             assume+ [version of \assume]
%      \qedstep                            prove+  [version of \prove]        
%      \assume                             case+   [version of \case]        
%      \prove                              conj, conj*
%      \pflet                              disj, disj*
%      \case                               pfenum, enumerate*
%      \pfdot ["." in long names]          
%      \stepref, \levelref, \toplevel
%      \pfstepnumber, \pflevelnumber
%      
%    Declarations
%      \kwfont [keyword font]
%      \pfshortnumbers
%      \pfsidenumbers, \pfnosidenumbers
%      \pflongindent, \pfshortindent
%      \pfindent
%      \pftopsep, \pfbotsep  
%      \pfsep, \stepsep   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       SPACING                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pflongindent == Indent proofs to full width of item label
%   \pfshortindent == Indent proofs by \pfindent [the default]

\newif\if@pfLongIndent %  true if indent proof to width of label.
\@pfLongIndentfalse
\newcommand{\pflongindent}{\@pfLongIndenttrue}
\newcommand{\pfshortindent}{\@pfLongIndentfalse}

% PARAMETERS
%  \pfindent   == indentation at beginning of a proof
%  \pftopsep   == space above first proof environment
%  \pfbotsep   == space below first proof environment
%  \pfsep      == space above and below inner proof environment
%  \stepsep    == space above and below proof step
%  pfhidelevel == counter, specifying level at which proofs are hidden

\newlength{\pfindent}      
\newlength{\pftopsep}  
\newlength{\pfbotsep}  
\newlength{\pfsep}  
\newlength{\stepsep}        
\newbox{\pfbox}
\newcounter{pfhidelevel}
\setcounter{pfhidelevel}{9999}
\newcommand{\pfhidelevel}[1]{\setcounter{pfhidelevel}{#1}}

\setlength{\pfindent}{1em} 
\setlength{\pftopsep}{1ex}     % space above first proof environment
\setlength{\pfbotsep}{1ex}     % space below first proof environment
\setlength{\pfsep}{0pt}        % space above and below inner proof environment
\setlength{\stepsep}{0pt}      % space above and below proof step

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   STEP NUMBERING                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pfshortnumbers{N} == Use short step numbers for all levels >= N
%
%   \pfsidenumbers{N}{D} == print side numbers for proof steps of all
%                           levels >= N, left-aligned length D 
%                           to left of left margin
%   \pfnosidenumbers     == do not print side numbers (the default)

%\newcommand{\pflongnumbers}{\@pfLongNumberstrue}
\newcommand{\pfshortnumbers}[1]{\pfshortNumberLevel=#1\relax}

\newcount\pfshortNumberLevel \pfshortNumberLevel=0

% \@pfLongNumbersfalse}
% \newif\if@pfLongNumbers %  true if indent proof to width of label.
%\@pfLongNumbersfalse

\newcommand{\pfstepnumber}[3]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #3%
     \else $\langle#1\rangle#2$%
   \fi}

\newcommand{\pflevelnumber}[2]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #2%
     \else $\langle#1\rangle$%
   \fi}

\newif\if@pfSideNumbers %  true if putting long numbers at margin
\@pfSideNumbersfalse
\newcounter{pf@sidenumberdepth}
\newlength{\pf@sidenumberoutdent}
\newcommand{\pfsidenumbers}[2]{\@pfSideNumberstrue
     \setcounter{pf@sidenumberdepth}{#1}%
     \addtocounter{pf@sidenumberdepth}{-1}%
     \setlength{\pf@sidenumberoutdent}{#2}}
\newcommand{\pfnosidenumbers}{\@pfSideNumbersfalse}


\newcount\pfLevelCount  \pfLevelCount=0 % current level number
\newcount\pfStepCount   \pfStepCount=0  % current step number
\newcommand{\pfLongLevel}{} % The long version of current level--e.g., 2.7.5
\newcommand{\pfLongStep}{}  % The long version of current step--e.g., 2.7.5.2
\newcommand{\pfStepName}{}  % {current level name}{current step name} 

% \pfSetName ==  LongStep := current long step name
%                StepName := current step name
\newcommand{\pfSetName}{%
  \edef\pfLongStep{%
    \ifnum\pfLevelCount>\@ne
      \pfLongLevel\pfdot\the\pfStepCount
     \else\the\pfStepCount\fi}%
  \edef\pfStepName{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
    {\pfLongStep}{\pfLongStep}%
    \else
     {$\langle\the\pfLevelCount\rangle$}%
     {$\langle\the\pfLevelCount\rangle\the\pfStepCount$}%
   \fi}}

% \pfSetRef{foo} ==  IF \pf@foo UNDEFINED
%                       THEN \pf@foo := StepName 
%                       ELSE WARNING
\newcommand{\pfSetRef}[1]{%
  \@ifundefined{pf@#1}%
    {\expandafter
      \edef\csname pf@#1\endcsname{\pfStepName}}%
    {\typeout{WARNING:
         proof step "#1" (<\the\pfLevelCount>\the\pfStepCount) 
        already defined}}%
    }


\newcommand{\pfPrintStepNumber}[2]{#2}
\newcommand{\pfPrintLevelNumber}[2]{#1}

% \stepref{FOO} == Print \pf@FOO as a step number
\newcommand{\stepref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step "#1" undefined}}{\expandafter\expandafter\expandafter
 \pfPrintStepNumber\csname pf@#1\endcsname}}

\newcommand{\levelref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step #1 undefined}}%
  {\expandafter\expandafter\expandafter
 \pfPrintLevelNumber\csname pf@#1\endcsname}}

\newcommand{\toplevel}{\pflevelnumber{0}{0}}

\newlength{\pf@outdent}
\newcommand{\pfSideNumber}{%
  \if@pfSideNumbers 
   \ifnum\pfLevelCount>\value{pf@sidenumberdepth}%
    \hspace*{-\pf@outdent}%
    \makebox[0pt][l]{\footnotesize\pfLongStep}%
    \hspace*{\pf@outdent}%
    \else\fi
   \else\fi}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE pflist ENVIRONMENT                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%% The pflist environment is the same as list environment except 
%% it can be nested deeper.

\def\pflist#1#2{\ifnum \@listdepth >15\relax \@toodeep 
     \else \global\advance\@listdepth\@ne \fi
  \rightmargin \z@ \listparindent\z@ \itemindent\z@
  \csname @list\romannumeral\the\@listdepth\endcsname 
  \def\@itemlabel{#1}\let\makelabel\@mklab \@nmbrlistfalse #2\relax
  \@trivlist
  \parskip\parsep \parindent\listparindent
  \advance\linewidth -\rightmargin \advance\linewidth -\leftmargin
  \advance\@totalleftmargin \leftmargin
  \parshape \@ne \@totalleftmargin \linewidth 
  \ignorespaces}

\def\endpflist{\global\advance\@listdepth\m@ne
    \endtrivlist}

\let\@listvii=\@listv
\let\@listviii=\@listv
\let\@listix=\@listv
\let\@listx=\@listv
\let\@listxi=\@listv
\let\@listxii=\@listv
\let\@listxiii=\@listv
\let\@listxiv=\@listv
\let\@listxv=\@listv
\let\@listxvi=\@listv

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE proof ENVIRONMENT                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

\newenvironment{proof}{%       BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel\pfdot\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \@tempcnta=\value{pfhidelevel}%
  \ifnum\@tempcnta<\@ne
    \setcounter{pfhidelevel}{1}%
    \typeout{WARNING: pfhidelevel < 1, setting to 1}%
    \@tempcnta=\@ne\fi
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi
  \else     
   \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi\fi
  \pfStepCount=\z@           %   StepCount  := 0
  \ifnum\pfLevelCount>\@ne   %   IF LevelCount > 1
   \begin{pflist}{}{%          %     THEN Begin List with
    \topsep=\pfsep\relax     %           \topsep     := \pfsep
    \itemsep=\z@             %           \itemsep    := 0
    \parsep=\z@              %           \parsep     := 0
    \partopsep=\z@           %           \partopsep  := 0
    \if@pfLongIndent         %          IF LongIndent
     \settowidth{\leftmargin}%%           THEN
      {\expandafter          %              \leftmargin := width of step name
       \pfPrintStepNumber    %                             + \labelsep
       \pfStepName.}%
     \advance\leftmargin
     \labelsep 
    \else                    %           ELSE
    \leftmargin=\pfindent    %            \leftmargin := \pfindent
    \fi\relax        
   }   \item[]
   \else \par                %     ELSE \par
    \addvspace{\pftopsep}%   %          addvspace of \pftopsep
    \parindent=\z@           %          \parindent := 0
    \parskip = \z@           %          \parskip := 0
    \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
    \let\enumerate\pfenum       %   enumerate environment <- pfenum
    \let\endenumerate\endpfenum %
 \fi
\@qedstepfalse
    }%                       % END:
  {\ifnum\pfLevelCount>\@ne  %   IF LevelCount > 1
    \end{pflist}%              %     THEN End List
   \else \par                %     ELSE \par
     \addvspace{\pfbotsep}%  %          addvspace of \pfbotsep
   \fi
  \@tempcnta=\value{pfhidelevel}%
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \end{minipage}\egroup\sbox{\pfbox}{}\@qedstepfalse\fi
  \else 
      \ifnum\pfLevelCount 
        =\@tempcnta 
        \end{minipage} 
        \egroup\sbox{\pfbox}{}\fi
 \fi}


\newenvironment{noproof}{%   % BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel.\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \pfStepCount=\z@           %   StepCount  := 0
  \par                       %   \par
  \parindent=\z@             %          \parindent := 0
  \parskip = \z@             %          \parskip := 0
  \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
  \let\enumerate\pfenum       %   enumerate environment <- pfenum
  \let\endenumerate\endpfenum %
  }%                         % END:
  {\par}                     %  \par

%% step 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     \step, \assume, ETC.                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\step}[2]{\begin{step+}{#1}#2\end{step+}}
\newif\if@qedstep %  true right after a \qedstep if in the scope of an 
                  %  \unhideqedproof declaration
\@qedstepfalse

\newif\if@unhideqedstep % set true by \unhideqproof, false by \hideqproof. 

\@unhideqedstepfalse
\newcommand{\unhideqedproof}{\@unhideqedsteptrue}
\newcommand{\hideqedproof}{\@unhideqedstepfalse}

\newcommand{\qedstep}{\step{qedstep\the\pfLevelCount}{Q.E.D.}
\if@unhideqedstep\@qedsteptrue\fi}

\newcommand{\nostep}[1]{% 
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
  }

\newenvironment{step+}[1]%
 {\endgroup                      % Move Outside environment scope
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
 \begingroup\@endpefalse         % Move inside environment scope
   \def\@currenvir{step+}%       %   by simulating \begin{step+}
 \begin{pflist}{}{%                % Begin list environment with
   \setlength
     {\pf@outdent}{\textwidth}%  %   \pf@outdent = outdent
   \addtolength                  %                 for side numbers
    {\pf@outdent}{-\linewidth}%  
   \addtolength
    {\pf@outdent}%
    {\pf@sidenumberoutdent}%
   \topsep=\stepsep\relax        %   \topsep     := \stepsep
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width of step name.
     {\expandafter
      \pfPrintStepNumber
      \pfStepName.}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep %                   + \labelsep
   \relax}%
 \item[\pfSideNumber%               % \item[ \pfSideNumber
  \expandafter                       %        StepNumber]
  \pfPrintStepNumber\pfStepName.]}%
 {\end{pflist}}

%%%%% \assume, \prove, and \case commands

\newenvironment{assume+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont Assume\/}:]}%    % \item[Assume:]]
 {\end{pflist}}

\newcommand{\assume}[1]{\begin{assume+}#1\end{assume+}}

\newcommand{\prove}[1]{\begin{prove+}#1\end{prove+}}
\newenvironment{prove+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Prove\/}:\hfill]}%     % \item[Prove:]]
 {\end{pflist}}

\newcommand{\pflet}[1]{\begin{pflet+}#1\end{pflet+}}
\newenvironment{pflet+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Let\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Let\/}:\hfill]}%     % \item[Let:]]
 {\end{pflist}}

%\newcommand{\prove}[1]{%
% \begin{pflist}{}{%                % Begin list environment with
%   \topsep=\z@                   %   \topsep     := 0
%   \itemsep=\z@                  %   \itemsep    := 0
%   \parsep=\z@                   %   \parsep     := 0
%   \partopsep=\z@                %   \partopsep  := 0
%   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
%     {{\kwfont Assume\/}:}%
%   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
%   \advance\leftmargin\labelsep  %                   + \labelsep
%   \relax}%
% \item[{\kwfont Prove\/}:\hfill]     % \item[Prove:]]
% #1
% \end{pflist}}

\newcommand{\case}[1]{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Case:"
     {{\kwfont Case\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont
           Case\/}:]             % \item[Case:]]
 #1
 \end{pflist}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       MISCELLANY                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\pf}{{\kwfont Proof\/}:}
\newcommand{\pfsketch}{{\kwfont Proof sketch\/}:}
%\newcommand{\qed}{\rule{.4em}{1.75ex}}
\newcommand{\qed}{{\fboxsep=\z@\fbox{\rule{.5em}{0pt}\rule{0pt}{2ex}}}}
\let\kwfont=\sc
\def\pfdot{.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        STACKS                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \@push{\stack}{element}  == \stack := <<element>> :o: \stack
% \@pop{\stack}{\cmd}  == \cmd := head(\stack)
%                            \stack := tail(\stack)
% \newstack{\stack}  == \stack := emptystack
%
% \@head{\stack}{\var}  ==  \var := head(\stack)
%   Note: to push a counter value, use \the\value{ctr}
%         to push a length \foo, use \the\foo

%
\def\@push#1#2{{\let\@nil\relax\let\@elt\relax\xdef#1{#2\@elt#1}}}
\def\@pop#1#2{{\let\@nil\relax\let\@elt\relax
              \xdef#2{\expandafter\@innerhead#1}
              \xdef#1{\expandafter\@innerpop#1}}}
\def\@innerpop#1\@elt#2\@nil{#2\@nil}
\def\@head#1#2{{\let\@elt\relax\xdef#2{\expandafter\@innerhead#1}}}
\def\@innerhead#1\@elt#2\@nil{#1}
\def\newstack#1{\gdef#1{\@nil}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           LISTS OF CONJUNCTIONS AND DISJUNCTIONS            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%    \begin{conj}       ->   /\ A
%      A \\ B \\ C           /\ B
%    \end{conj}              /\ C
%
%    \begin{conj*}      ->   1./\ A
%      A \\ B \\ C           2./\ B
%    \end{conj*}             3./\ C
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are arrays; they must be used in math mode.

\newcounter{pf@conjCounter}   % counter for conj* and disj*
\newstack\pf@conj             % stack of counters

\newenvironment{conj}{%
 \begin{array}[t]{@{\land\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{disj}{%
 \begin{array}[t]{@{\lor\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{conj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\arabic{pf@conjCounter}.}
   \land\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

\newenvironment{disj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\alph{pf@conjCounter}.}
   \lor\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      ENUMERATED LISTS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% pfenum environment : In proofs, the enumerate environment 
%                      is redefined to be the pfenum environment
%
% enumerate* environment : Like pfenum, except with additional
%                          indentation.
%
% \enumindent :  The indentation for enumerate*
% pfenumdepth  : Depth of current pfenum list
% pfenum       : pfenum list counter
%
% Uses counters pfenumi, ... , pfenumiii just like the
% ordinary enumerate environment uses counters enumi, ... , enumiv.
% \pf@setEnumWidth{\cmd} : Sets \cmd to the width of the label of the
%                          item number 2 for the current enumeration level.
%
% \pf@enumLabel : prints the current pfenum label, using the
%                 pfenumi... counter.

\newcounter{pfenum}
\newcounter{pfenumdepth}
\newlength{\enumindent}
\setlength{\enumindent}{1em}

\@definecounter{pfenumi}
\@definecounter{pfenumii}
\@definecounter{pfenumiii}
%\@definecounter{pfenumiv}

\def\labelpfenumi{\thepfenumi.}    
\def\thepfenumi{\arabic{pfenumi}}     
 
\def\labelpfenumii{(\thepfenumii)}
\def\thepfenumii{\alph{pfenumii}}
\def\p@pfenumii{\thepfenumi}

\def\labelpfenumiii{\thepfenumiii.}
\def\thepfenumiii{\roman{pfenumiii}}
\def\p@pfenumiii{\thepfenumi\thepfenumii}

%\def\labelpfenumiv{\thepfenumiv.}
%\def\thepfenumiv{\Alph{pfenumiv}}     
%\def\p@pfenumiv{\p@pfenumiii\thepfenumiii}


\newcommand{\pf@setEnumWidth}[1]{%
  \settowidth{#1}{\setcounter{\@pfenumctr}{2}%
  \csname the\@pfenumctr\endcsname.%
  \setcounter{\@pfenumctr}{0}}}



\newcommand{\pf@enumLabel}{%
  \hfill\makebox[0pt][r]{\csname the\@pfenumctr\endcsname.}}

\newenvironment{pfenum}{%        % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

\newenvironment{enumerate*}{%    % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \advance\leftmargin\enumindent%                   + \enumindent
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \makefcn{\FOO}{V0}{{V1}...{Vk}} :
%      Defines \FOO{n}  ==  CASE  n = 0    -> V0
%                                 n = 1    -> V1
%                                 ...
%                                 n \geq k -> Vk
%
%      Useful when Vi is a dimension applying to a depth-i environment

\def\makefcn#1#2#3{{\let\or\relax
     \gdef\fcn@temp{}%
     \gdef\fcn@tempb{#2}%
     \@tfor\foo:=#3\do{\xdef\fcn@temp{\fcn@temp\or\foo}\xdef\fcn@tempb{\foo}}%
     \let\ifcase\relax\let\else\relax\let\fi\relax
     \xdef#1##1{\ifcase ##1 #2\fcn@temp\else\fcn@tempb\fi}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \pfif{A}{B}{C} :  if A then B    \pfIF{A}{B}{C} :  if A
%                        else C                        THEN B
%                                                      ELSE C

\newcommand{\pfmathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\pfif}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{}}
   {\bf if}\;\;#1&{\bf then}&#2\\
                 &{\bf else}&#3
   \end{array}}}}

\newcommand{\pfIF}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{}}
   {\bf if}\;\;#1\\ 
  \begin{array}[t]{@{\hspace{1em}}l@{\;\;}l@{}}
     {\bf then}&#2\\
     {\bf else}&#3
   \end{array}
  \end{array}}}}

%%%%%%%%%% end pf.sty

%%%%%%%% file bezier.sty

% bezier.sty  17-Dec-85
% BEZIER DOCUMENT-STYLE OPTION - released 30 December 1993
%    for LaTeX version 2.09
% Copyright (C) 1985, 1993 by Leslie Lamport

%  Modified 30 December 1993 to move each plotted point left by
%  1/2 the line width, so it should line up properly with other
%  picture elements.

%  In a picture environment, writing
%
%       \bezier{N}(AX,AY)(BX,BY)(CX,CY)
%
%  plots a quadratic Bezier curve from (AX,AY) to (CX,CY), with (BX,BY) as
%  the third Bezier point, using N+1 equally spaced points.
%
%  \bezier{N}(AX,AY)(BX,BY)(CX,CY) ==
%    BEGIN
%      @sc  := N
%      @scp := @sc+1
%      \@xb := 2 * (BX - AX) * \unitlength
%      \@xa := ((CX-AX)*\unitlength - \@xb)/@sc
%      \@yb := 2 * (BY - AY) * \unitlength
%      \@ya := ((CY-AY)*\unitlength - \@yb)/@sc
%      \@pt := square rule of width \@wholewidth
%      @t := 0
%      WHILE @t < @scp
%        DO  \@x := ((@t*\@xa + @xb) / @sc) * t
%            \@y := ((@t*\@ya + @yb) / @sc) * t
%            plot pt with relative coords (\@x,\@y)
%            @t := @t+1
%        OD

\newcounter{@sc}
\newcounter{@scp}
\newcounter{@t}
\newlength{\@x}
\newlength{\@xa}
\newlength{\@xb}
\newlength{\@y}
\newlength{\@ya}
\newlength{\@yb}
\newsavebox{\@pt}
\def\bezier#1(#2,#3)(#4,#5)(#6,#7){\c@@sc#1\relax
 \c@@scp\c@@sc \advance\c@@scp\@ne
 \@xb #4\unitlength \advance\@xb -#2\unitlength \multiply\@xb \tw@
 \@xa #6\unitlength \advance\@xa -#2\unitlength
 \advance\@xa -\@xb \divide\@xa\c@@sc
 \@yb #5\unitlength \advance\@yb -#3\unitlength \multiply\@yb \tw@
 \@ya #7\unitlength \advance\@ya -#3\unitlength
 \advance\@ya -\@yb \divide\@ya\c@@sc
 \setbox\@pt\hbox{\hskip -\@halfwidth \vrule height\@halfwidth 
  depth\@halfwidth  width\@wholewidth}\c@@t\z@ 
 \put(#2,#3){\@whilenum{\c@@t<\c@@scp}\do
 {\@x\c@@t\@xa \advance\@x\@xb \divide\@x\c@@sc \multiply\@x\c@@t 
 \@y\c@@t\@ya \advance\@y\@yb \divide\@y\c@@sc \multiply\@y\c@@t 
 \raise \@y \hbox to \z@{\hskip \@x\unhcopy\@pt\hss}\advance\c@@t\@ne}}}

%%%% end file bezier.sty
\makeatother

%\documentstyle[11pt,titlepage,bezier,pf,makeidx]{article}
%%* "TLA in Pictures"
%   Approved by Sam, 14 Jan 94
%   Changed 18 Jan 94, replacing QC by Q in Section 4.2.
%   Corrected 28 Jan 94: added missing \Box to Figure 4
%     (Error found by Peter Hancock.)
%   Corrected 22 Feb 94 based on errors found by Paul Harter
%     * (A) in Section 3.2 was wrong as stated.  Changed to
%       result about particular formulas \Delta and \widehat{\Delta}.
%     * Changed incorrect figure reference in second bullet of 
%       itemized list in Section 5.
%   Modified 27 August in response to comments by Cynthia Hibbard.

%\makeindex

% FOR SRC Report--
%    \oddsidemargin   .47in     %   Left margin on odd-numbered pages.
%    \evensidemargin 1.06in     %   Left margin on even-numbered pages.


%   \topmargin       .47in    %    Nominal distance from top of page to top of
%   \headheight        0pt    %    Height of box containing running head.
%   \headsep           0pt    %    Space between running head and text.
%  \topskip = 10pt           %    '\baselineskip' for first line of page.
% Bottom of page:
%   \footheight       12pt  %    Height of box containing running foot.
%   \footskip        1.5cm    %    Distance from baseline of box containing 
%                             %    foot to baseline of last line of text.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 MODIFICATION DATE                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                 %
% Defines \moddate to expand to modification date such as         %
%                                                                 %
%    Mon  5 Aug 1991  [10:34]                                     %
%                                                                 %
% and \prdate to print it in a large box.  Assumes editor         %
% updates modification date in standard SRC Gnu Emacs style.      %
% (should work for any user name).                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\ypmd{%                                                       %
%                                                                 %
%                                                                 %
  endypmd}                                                        %
%                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\moddate}{\expandafter\xpmd\ypmd}                     %
\def\xpmd Last modified                                           %
on #1 #2 #3 #4:#5:#6 #7 #8 by #9 endypmd{#1 \ #3 #2 #8 \ [#4:#5]} %
\newcommand{\prdate}{\noindent\fbox{\Large\moddate}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{TLA in Pictures}
\author{Leslie Lamport}
\date{\moddate}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       LOGIC                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 
%  \true, \false == booleans
%  \deq          == equals by definition
%  \implies      == =>
% \act{exp} : Formats exp in math mode, with the first
%                character in \cal style.  Thus,
%                \act{A_1} -> ${\cal A}_1$
%
% \sqact{A}{v}  == [A]_v   (formatted like \act)
% \anact{A}{v}  == <A>_v   (formatted like \act)
% \unchanged{f} == f'=f
% \enabled{A}   == enabled predicate of A
% \WF{f}{A}     == WF_f(A)
% \SF{f}{A}     == SF_f(A)
% \tuple{x}     == <x>
% \EE           == existential quantification over a flexible variable
% \vbl{foo}     == foo formatted as a variable
% \rvbl{foo}    == foo formatted as a rigid variable
% \str{abc}    == the string "abc"

\newcommand{\mathdef}[1]{\relax\ifmmode #1\else $#1$\fi}

\newcommand{\true}{{\it true}}
\newcommand{\false}{{\it false}}
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\newcommand{\implies}{\Rightarrow}
\newcommand{\act}[1]{\mathdef{\makecal#1}}
\newcommand{\makecal}[1]{{\cal #1}}
\newcommand{\sqact}[2]{\mathdef{[\act{#1}]_{#2}}}
\newcommand{\anact}[2]{\mathdef{\langle\act{#1}\rangle_{#2}}}
\newcommand{\WF}[2]{\mathdef{{\rm WF}_{#1}(#2)}}
\newcommand{\SF}[2]{\mathdef{{\rm SF}_{#1}(#2)}}
\newcommand{\enabled}[1]{\mathdef{{\it Enabled}\,#1}}
\newcommand{\unchanged}[1]{\mathdef{#1'=#1}}
\newcommand{\tuple}[1]{\mathdef{\langle#1\rangle}}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\exists\s{-.517}\exists\s{-.517}\exists$}}\exists\s{-.517}\exists
            \s{-.517}\exists$}}
\newcommand{\s}[1]{\hspace*{#1em}}


\newcommand{\vbl}[1]{{\it #1\/}}
\newcommand{\rvbl}[1]{{\sf #1}}
\newcommand{\str}[1]{\mbox{\sf``#1''}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%            \dbar - THE DIJKSTRA BAR                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dbar}{\usebox{\dbarbox}}
\newsavebox{\dbarbox}
\sbox{\dbarbox}{\setlength{\unitlength}{.09em}
\begin{picture}(4,8)
\put(0,0){\framebox(4,8){}}
\end{picture}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     FORMATING                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\reason}[1]{\hspace{1em}\mbox{\small
  \begin{tabular}{@{}l@{}}\makebox[0pt][r]{[\hspace{.2em}}#1\hspace{.2em}]%
      \end{tabular}}}
\newcommand{\vjot}{\rule[-\jot]{0pt}{1pt}}
\newcommand{\vjjot}{\rule[-2\jot]{0pt}{1pt}}
%% A colon for math formulas without so much space around it:
\newcommand{\midcolon}{\mskip -.5\thinmuskip:\mskip -.5\thinmuskip}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     EMACS MACROS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%&v&\vbl{#}&

\begin{document}
%try
\maketitle

\begin{abstract}
Predicate-action diagrams, which are similar to standard
state-transition diagrams, are precisely defined as formulas of TLA
(the Temporal Logic of Actions).  We explain how these diagrams can be
used to describe aspects of a specification---and those descriptions
then proved correct---even when the complete specification cannot be
written as a diagram.  We also use the diagrams to illustrate proofs.
\end{abstract}

\begin{keywords}
Concurrency,
specification,
state-transition diagrams,
temporal logic.
\end{keywords}

\section{Introduction}  

Pictures aid understanding.  A simple flowchart is easier to
understand than the equivalent programming-language text.  However,
complex pictures are confusing.  A large, 
 \index{spaghetti}%
spaghetti-like flowchart is
harder to understand than a properly structured program text.

Pictures are inadequate for specifying complex systems, but they can
help us understand particular aspects of a system.  For a picture to
provide more than an informal comment, there must be a formal
connection between the complete specification and the picture.  The
assertion that the picture is a correct description of (some aspect
of) the system must be a precise mathematical statement.

We use TLA (the Temporal 
 \index{temporal logic of actions}%
Logic of Actions) to specify systems.  In TLA, a specification is a
logical formula describing all possible correct behaviors of the
system.  As an aid to understanding TLA formulas, we introduce here a
type of picture called a {\em predicate-action diagram}.  These
diagrams are similar to the various kinds of state-transition diagrams
that have been used for years to describe systems, starting with
  \index{Mealy and Moore machines}%
Mealy and 
%  \index{Moore machine}%
Moore machines~\cite{mealy:method,moore:gedanken}.  We relate these
pictures to TLA specifications by interpreting a predicate-action
diagram as a TLA formula.  A diagram denoting formula $D$ is a correct
description of a system with specification $S$ iff (if and only if)
$S$ implies $D$.  We therefore provide a precise statement of what it
means for a diagram to describe a specification.

We use predicate-action diagrams in three ways that we believe are new
for a precisely defined formal notation:
\begin{itemize}
\item To describe aspects of a specification even when it is not
feasible to write the complete specification as a diagram.

\item To draw different diagrams that provide complementary views of
the same system.

\item To illustrate formal correctness proofs.
\end{itemize}

Section~\ref{sec:TLA} is a brief review of TLA; a more leisurely
introduction to TLA appears in~\cite{lamport:newtla}.
Section~\ref{sec:std} describes predicate-action diagrams, using an
$n$-input Muller C-element as an example.  It shows how diagrams are
used to describe aspects of a complete specification, and to provide
complementary views of a system.  Section~\ref{sec:proof} gives
another example of how predicate-action diagrams are used to describe
a system, and shows how they are used to illustrate a proof.

%try
\section{TLA} \label{sec:TLA} \index{TLA|(}%

We now describe the syntax and semantics of TLA\@.  The description is
illustrated with the formulas defined in Figure~\ref{fig:phi}.  (The
symbol 
  \index{+3deq@$\deq$}%
$\deq$ means {\em equals by definition}.)  

\begin{figure}[b]
\index{+2Fi@$\Phi$}%%
 \index{M@\act{M}}%%
\centering
\begin{minipage}{\textwidth}
\small
\begin{tabbing}
\( \vbl{Init}_{\Phi} \;\;\deq\;\; (x=0) \;\land\; (y=0) \)\\[.1\baselineskip]
\( \act{M_{1}} \;\;\deq\;\; (x'=x+1) \;\land\; (y'=y) \)\\[.1\baselineskip]
% \hspace{2em}
\( \act{M_{2}} \;\;\deq\;\; (y' = y+1) \; \land\; (x'=x) \)\\[.1\baselineskip]
%
\( \act{M} \;\;\deq\;\; \act{M_{1}} \lor \act{M_{2}} \)\\[.1\baselineskip]
\( \Phi \;\;\deq\;\; \vbl{Init}_{\Phi}
       \,\land\, \Box\sqact{M}{\tuple{x,\,y}}
       \,\land\, \WF{\tuple{x,\,y}}{\act{M_{1}}} 
       \,\land\, \WF{\tuple{x,\,y}}{\act{M_{2}}} 
\)
\end{tabbing}
\end{minipage}
\caption{The TLA formula $\Phi$ describing a 
         simple program that repeatedly increments $x$ or $y$.} 
\label{fig:phi}
\end{figure}

We assume an infinite set of 
  \index{variable}%
variables (such as $x$ and $y$) and a
class of semantic values.  Our variables are the 
  \index{flexible variable}\index{variable!flexible}%
flexible variables of temporal logic, which are analogous to variables
in a programming language.  TLA also includes the
  \index{rigid variable}\index{variable!rigid}%
rigid variables of predicate logic, which are analogous to constant
parameters of a program, but we ignore them here.  The class of values
includes numbers,
  \index{strings}%
strings, sets, and functions.

A 
 \index{state}%
{\em state} is an assignment of values to variables.  A 
  \index{behavior}%
{\em behavior}
is an infinite sequence of states.  Semantically, a TLA formula is
true or false of a behavior.  Syntactically, TLA formulas are built up
from state functions using Boolean operators ($\lnot$, $\land$,
$\lor$,
 \index{+3implies@$\implies$}%
$\implies$ [implication], and 
  \index{+3equiv@$\equiv$}%
$\equiv$ [equivalence])
and the operators 
  \index{+2p@$'$ (prime)}%
$'$ and 
  \index{+2box@$\Box$}%
$\Box$, as described below.  TLA also has a
hiding operator 
  \index{+2e@$\EE$}%
$\EE$, which we do not use here.

A {\em state 
  \index{state function}%
function\/} is a nonBoolean expression built from
variables, constants, and constant operators.  Semantically, it
assigns a value to each state---for example $x+1$ assigns to state $s$
one plus the value that $s$ assigns to the variable $x$.  A {\em state
 \index{state predicate}%
predicate\/} (often called just a 
  \index{predicate}%
{\em predicate\/}) is a Boolean expression built from variables,
constants, and constant operators such as $+$.  Semantically, it is
true or false for a state---for example the predicate
$\vbl{Init}_{\Phi}$ is true of state $s$ iff $s$ assigns the value
zero to both $x$ and $y$.

An 
  \index{action}%
{\em action\/} is a Boolean expression containing primed and
unprimed variables.  Semantically, an action is true or false of a
pair of states, with primed variables referring to the second
state---for example, action $\act{M}_{1}$ is true for \tuple{s,\,t}
iff the value that state $t$ assigns to $x$ equals one plus the value
that state $s$ assigns to $x$, and the values assigned to $y$ by
states $s$ and $t$ are equal.  A pair of states satisfying an action
\act{A} is called an \act{A} 
  \index{step}%
{\em step}.  Thus, an $\act{M}_{1}$ step is one that increments $x$ by
one and leaves $y$ unchanged.

If $f$ is a state function or state predicate, we write 
  \index{+2p@$'$ (prime)}%
$f'$ for the
expression obtained by priming all the variables of 
 %the ``the'' removed, 24 Aug 95
$f$.  For
example $(x + 1)'$ equals $x'+1$, and $\vbl{Init}_{\Phi}'$ equals
$(x'=0)\land(y'=0)$.  For an action \act{A} and a state function $v$,
we define 
  \index{+5me@$\sqact{{}\ldots}{\ldots}$}%
\sqact{A}{v} to equal $\act{A}\lor(v'=v)$, so a \sqact{A}{v} step is
either an \act{A} step or a step that leaves the value of $v$
unchanged.  Thus, a $\sqact{M_{1}}{\tuple{x,y}}$ step is one that
increments $x$ by one and leaves $y$ unchanged, or else leaves the
ordered pair \tuple{x,y} unchanged.  Since a tuple is unchanged iff
each component is unchanged, a $\sqact{M_{1}}{\tuple{x,y}}$ step is
one that increments $x$ by one and leaves $y$ unchanged, or else
leaves both $x$ and $y$ unchanged.  We define
  \index{+5mf@$\anact{{}\ldots}{\ldots}$}%
\anact{A}{v} to equal
$\act{A}\land(v'\neq v)$, so an \anact{M_{1}}{\tuple{x,y}} step is an
$\act{M}_{1}$ step that changes $x$ or~$y$.  Since an $\act{M}_{1}$
step leaves $y$ unchanged, an \anact{M_{1}}{\tuple{x,y}} step is a
step that increments $x$ by 1, changes the value of $x$, and leaves
$y$ unchanged.

We say that an action \act{A} is 
  \index{enabled}%
{\em enabled\/} in state $s$ iff
there exists a state $t$ such that \tuple{s,\,t} is an \act{A} step.
For example, $\act{M}_{1}$ is enabled iff it is possible to take a
step that increments $x$ by one, changes $x$, and leaves $y$
unchanged.  Since $x+1\neq x$ for any natural number $x$, action
\anact{M_{1}}{\tuple{x,y}} is enabled in any state in which $x$ is a
natural number.  If 
  \index{+2i@$\infty$}%
$\infty+1$ equals $\infty$, then
\anact{M_{1}}{\tuple{x,y}} is not enabled in a state in which $x$
equals $\infty$.

A TLA formula is true or false of a behavior.  A predicate is true of
a behavior iff it is true of the first state.  An action is true of a
behavior iff it is true of the first pair of states.  As usual in
temporal logic, if $F$ is a formula then 
    \index{+2box@$\Box$}%
$\Box F$ is the formula meaning that $F$ is always true.  Thus,
$\Box\vbl{Init}_{\phi}$ is true of a behavior iff $x$ and $y$ equal
zero for every state in the behavior.  The formula
$\Box\sqact{M}{\tuple{x,y}}$ is true of a behavior iff each step 
  \index{step!of a behavior}%
(pair of successive states) of the behavior is a
\sqact{M}{\tuple{x,y}} step.

Using $\Box$ and ``enabled'' predicates, we can define 
  \index{fairness}%
fairness operators 
 \index{WF}%
WF and 
 \index{SF}%
SF\@.  The {\em 
  \index{weak fairness}\index{fairness!weak}%
weak fairness\/} formula \WF{v}{\act{A}} asserts of a behavior that
there are infinitely many \anact{A}{v} steps, or there are infinitely
many states in which \anact{A}{v} is not enabled.  In other words,
\WF{v}{\act{A}} asserts that if \anact{A}{v} becomes enabled forever,
then infinitely many \anact{A}{v} steps occur.  The {\em strong
  \index{strong fairness}\index{fairness!strong}%
fairness\/} formula \SF{v}{\act{A}} asserts that either there are
infinitely many \anact{A}{v} steps, or there are only finitely many
states in which \anact{A}{v} is enabled.  In other words,
\SF{v}{\act{A}} asserts that if \anact{A}{v} is enabled infinitely
often, then infinitely many \anact{A}{v} steps occur.

The standard form of a TLA specification is
 $\vbl{Init} \land\Box\sqact{N}{v}\land L$, 
where \vbl{Init} is a predicate, \act{N} is an action, $v$ is a state
function, and $L$ is a conjunction of fairness conditions.  This
formula asserts of a behavior that (i)~\vbl{Init} is true for the
initial state, (ii)~every step of the behavior is an \act{N} step or
leaves $v$ unchanged, and (iii)~$L$ holds.  Formula $\Phi$ of
Figure~\ref{fig:phi} is in this form, asserting that (i)~initially $x$
and $y$ both equal zero, (ii)~every step either increments $x$ by one
and leaves $y$ unchanged, increments $y$ by one and leaves $x$
unchanged, or leaves both $x$ and $y$ unchanged, and (iii)~the
fairness condition
 $\WF{\tuple{x,\,y}}{\act{M_{1}}} 
       \land \WF{\tuple{x,\,y}}{\act{M_{2}}}$ holds.
Formula \WF{\tuple{x,\,y}}{\act{M_{1}}} asserts that there are
infinitely many \anact{M_{1}}{\tuple{x,y}} steps or
\anact{M_{1}}{\tuple{x,y}} is infinitely often not enabled.  Since (i)
and (ii) imply that $x$ is always a natural number,
\anact{M_{1}}{\tuple{x,y}} is always enabled.  Hence,
\WF{\tuple{x,\,y}}{\act{M_{1}}} implies that there are infinitely many
\anact{M_{1}}{\tuple{x,y}} steps, so $x$ is incremented infinitely
often.  Similarly, \WF{\tuple{x,\,y}}{\act{M_{2}}} implies that $y$ is
incremented infinitely often.  Putting this all together, we see that
$\Phi$ is true of a behavior iff (i)~$x$ and $y$ are initially zero,
(ii)~every step increments either $x$ or $y$ by one and leaves the
other unchanged or else leaves both $x$ and $y$ unchanged, and
(iii)~both $x$ and $y$ are incremented infinitely many times.

The formula $\vbl{Init} \land\Box\sqact{N}{v}$ is a 
  \index{safety}%
safety property~\cite{alpern:defining}.  It describes what steps are
allowed, but it does not require anything to happen.  (The formula is
satisfied by a behavior satisfying the initial condition in which no
variables ever change.)  Fairness conditions are used to specify that
something must happen.%
 \index{TLA|)}
%try

\section{Predicate-Action Diagrams} \label{sec:std}
 \index{predicate-action diagram|(}


\subsection{An Example}

We take as an example a 
 \index{Muller C-element}\index{C-element}%
Muller C-element~\cite{seitz:system-timing}.  This is a circuit with
$n$ binary inputs $\vbl{in}[1],\ldots,\vbl{in}[n]$ and one binary
output \vbl{out}, as shown in Figure~\ref{fig:c-element}.  As the
figure indicates, we are considering the closed system consisting of
the C-element together with its environment.  Initially, all the
inputs and the output are equal.  The output becomes 0 when all the
inputs are 0, and it becomes 1 when all the inputs are 1.  After an
input changes, it must remain stable until the output changes.


\begin{figure}
\centering
\begin{picture}(170,119)(-30,-19)
%\makegrid(-200,-100)(400,200)
\thicklines
\put(0,0){\framebox(30,100){\it\shortstack{E\\n\\v\\i\\r\\o\\n\\m\\e\\n\\t}}}
\put(80,0){\framebox(30,100){\it\shortstack{C\\[3pt]- 
             \\[3pt] E\\l\\e\\m\\e\\n\\t}}}
%
\put(55,85){\makebox(0,0)[b]{$\vbl{in}[1]$}}
\put(55,25){\makebox(0,0)[b]{$\vbl{in}[n]$}}
\put(55,-12){\makebox(0,0)[t]{\vbl{out}}}
\put(30,80){\vector(1,0){50}}
\put(30,20){\vector(1,0){50}}
\put(55,55){\makebox(0,0){\LARGE$\vdots$}}
%
\put(110,50){\line(1,0){20}}
\put(130,40){\oval(20,20)[tr]}
\put(140,40){\line(0,-1){40}}
\put(130,0){\oval(20,20)[br]}
\put(130,-10){\line(-1,0){150}}
\put(-20,0){\oval(20,20)[bl]}
\put(-30,0){\line(0,1){40}}
\put(-20,50){\vector(1,0){20}}
\put(-20,40){\oval(20,20)[tl]}
%\put(110,50){\line(1,0){30}}
%\put(140,50){\line(0,-1){60}}
%\put(140,-10){\line(-1,0){170}}
%\put(-30,-10){\line(0,1){60}}
%\put(-30,50){\vector(1,0){30}}
%\put(115,52){\makebox(0,0)[lb]{\vbl{out}}}
\end{picture}
\caption{A Muller C-element.}
\label{fig:c-element}
\end{figure}


The behavior of a 2-input C-element and its environment is described
by the predicate-action diagram of Figure~\ref{fig:inout2}(a), where $C$
is defined by%
  \index{C@$C(i,j,k)$}%
 \[ C(i,j,k) \;\deq\; (\vbl{in}[1]=i)\land(\vbl{in}[2]=j)\land(\vbl{out}=k)
 \]
The short arrows, with no originating node, identify the nodes labeled
$C(0,0,0)$ and $C(1,1,1)$ as initial nodes.  They indicate that the
C-element starts in a state satisfying $C(0,0,0)$ or $C(1,1,1)$.  The
arrows connecting nodes indicate possible state transitions.  For
example, from a state satisfying $C(1,1,1)$, it is possible for the
system to go to a state satisfying either $C(0,1,1)$ or $C(1,0,1)$.
More precisely, these arrows indicate all steps in which the triple
\tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}} changes---that is,
transitions in which at least one of $\vbl{in}[1]$, $\vbl{in}[2]$, and
\vbl{out} changes.  Steps that change other variables---for example,
variables representing circuit elements inside the environment---but
leave \tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}} unchanged are also
possible.


\begin{figure*}[tb] \small
\setlength{\unitlength}{.98pt}%


(a) A predicate-action diagram.
\vspace{.5\baselineskip}

\begin{centering}
\normalsize
\begin{picture}(365,105)(-10,-60)
\normalsize
%\makegrid(0,-100)(400,200)
\thicklines\small
\newcommand{\coval}[5]{\put(#1,#2){\makebox(0,0){$C(#3,#4,#5)$}}
                       \put(#1,#2){\oval(50,20)}}
\coval{25}{0}000
\coval{80}{35}100
\coval{80}{-35}010
\coval{135}{0}110
%
\coval{215}{0}111
\coval{270}{35}011
\coval{270}{-35}101
\coval{325}{0}001
%
\put(47,8){\vector(1,2){10}}
\put(47,-8){\vector(1,-2){10}}
\put(102,27){\vector(1,-2){10}}
\put(102,-27){\vector(1,2){10}}
%
\put(160,0){\vector(1,0){30}}
%
%\put(350,0){\line(1,0){5}}
\put(350,-5){\oval(10,10)[tr]}
\put(355,-5){\line(0,-1){50}}
\put(350,-60){\line(-1,0){355}}
\put(350,-55){\oval(10,10)[br]}
\put(-10,-55){\line(0,1){50}}
\put(-5,-55){\oval(10,10)[bl]}
\put(-5,0){\vector(1,0){5}}
\put(-5,-5){\oval(10,10)[tl]}
%\put(350,0){\line(1,0){5}}
%\put(355,0){\line(0,-1){60}}
%\put(355,-60){\line(-1,0){365}}
%\put(-10,-60){\line(0,1){60}}
%\put(-10,0){\vector(1,0){10}}
%
\put(237,8){\vector(1,2){10}}
\put(237,-8){\vector(1,-2){10}}
\put(292,27){\vector(1,-2){10}}
\put(292,-27){\vector(1,2){10}}
%
%\put(-7,18){\vector(1,-1){10}}
\put(-8,19){\vector(1,-1){11}}
\put(182,19){\vector(1,-1){11}}
\end{picture}

\end{centering}
\vspace{\baselineskip}

(b) The corresponding TLA formula.
\vspace{.5\baselineskip}

\begin{centering} %\small
 \(\begin{conj}
     C(0,0,0)\lor C(1,1,1) \\[\jot]
     \Box\sqact{{}C(0,0,0) \,\implies\, C(1,0,0)'\lor C(0,1,0)'}%
     {\tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}}} \\[\jot]
    \Box
    \sqact{{}C(1,0,0)\,\implies\, C(1,1,0)'}%
     {\tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}}}\\
     \multicolumn{1}{@{\hspace{1em}}l@{}}{\ldots}\\[\jot]
    \Box
    \sqact{{}C(0,0,1) \,\implies\, C(0,0,0)'}%
     {\tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}}}
   \end{conj}
 \)

\end{centering}

\caption{Predicate-Action diagram of \tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}}
for a 2-input C-element, and the corresponding TLA formula.}
\label{fig:inout2}
\end{figure*}

The predicate-action diagram of Figure~\ref{fig:inout2}(a) looks like
a standard state-transition diagram.  However, we interpret it
formally not as a conventional state machine, but as the TLA formula
of Figure~\ref{fig:inout2}(b).\footnote{A list of formulas bulleted by
  \index{+7and@$\land$ (list bulleted by)}%
  \index{+7or@$\lor$ (list bulleted by)}%
$\land$ or $\lor$ denotes their conjunction or disjunction; 
$\land$ and $\lor$ are also used as ordinary infix operators.} 
This formula has the form
$\vbl{Init}\land\bigwedge_{o}F_{o}$, where \vbl{Init} is a state
predicate and there is one conjunct $F_{o}$ for each node~$o$.  The
predicate \vbl{Init} is $C(0,0,0)\lor C(1,1,1)$.  Each $F_{o}$
describes the possible state changes starting from a state described
by node $o$.  For example, the formula $F_{o}$ for the node labeled
$C(1,1,0)$ is
 \[ \Box 
    \sqact{{}C(1,1,0) \,\implies\, C(1,1,1)' }%
     {\tuple{\vbl{in}[1],\vbl{in}[2],\vbl{out}}}
 \] 
A predicate-action diagram represents a safety property; it does not
include any fairness conditions.

Figure~\ref{fig:inout2}(a) is a reasonable way to describe a 2-input
C-element.  However, the corresponding diagram for a 3-input C-element
would be quite complicated; and there is no way to draw such a diagram
for an $n$-input circuit.  The general specification is written
directly as a TLA formula in Figure~\ref{fig:TLA-C-element}.  The
array of inputs is represented formally by a variable \vbl{in} whose
value is a function with domain $\{1,\ldots,\rvbl{n}\}$, where square
brackets denote function application.  (Formally, \rvbl{n} is a rigid
variable---one whose value is constant throughout a behavior.)  We
introduce two pieces of notation for representing functions:
\begin{itemize}
\item 
  \index{+5na@$[\ldots \,\mapsto\, \ldots]$}%
$[i\in S\mapsto e(i)]$ denotes the function $f$
with domain $S$ such that $f[i]$ equals $e(i)$ for every
$i$ in $S$.

\item 
  \index{+5nb@$[\ldots \,{\bf except}\, \ldots]$}%
$[f\;{\bf except}\; ![i] = e]$ denotes the function $g$ that is
the same as $f$ except that $g[i]$ equals $e$.
\end{itemize}
The formulas defined in Figure~\ref{fig:TLA-C-element} have the
following interpretation.
\begin{description}
\item[$\vbl{Init}_{C}$] A state predicate asserting that 
\vbl{out} is either $0$ or $1$, and that \vbl{in} is the function
with domain $\{1,\ldots,\rvbl{n}\}$ such that
$\vbl{in}[i]$ equals \vbl{out} for all $i$ in its domain.

\item[$\vbl{Input}(i)$] An action that is enabled iff
$\vbl{in}[i]$ equals \vbl{out}.  It complements
$\vbl{in}[i]$, leaves $\vbl{in}[j]$ unchanged for
$j\neq i$, and leaves \vbl{out} unchanged.  (The symbol
$i$ is a parameter.)

\item[\vbl{Output}] An action that is enabled iff all the $\vbl{in}[i]$ are
different from \vbl{out}. It complements \vbl{out} and leaves \vbl{in}
unchanged.  

\item[\vbl{Next}] An action that is the disjunction of \vbl{Output}
and all the $\vbl{Input}(i)$ actions, for $i\in\{1,\ldots,\rvbl{n}\}$.  Thus,
a \vbl{Next} step is either an \vbl{Output} step or an
$\vbl{Input}(i)$ step for some input line $i$.

\item[$\Pi_{C}$] A temporal formula that is the specification of the
C-element (together with its environment).  It asserts that
(i)~$\vbl{Init}_{C}$ holds initially, (ii)~every step is either a
\vbl{Next} step or else leaves \tuple{\vbl{in},\vbl{out}} unchanged,
and (iii)~\vbl{Output} cannot be enabled forever without an
\vbl{Output} step occurring.  The fairness condition (iii) requires
the output to change if all the inputs have; inputs are not required
to change.  (Since predicate-action diagrams describe only
safety properties, the fairness condition is irrelevant to our 
explanation of the diagrams.)
\end{description}
%
%
%
\begin{figure}
\index{+2PiC@$\Pi_{C}$}%%
\centering\small
\( \begin{array}{@{}l@{\;\;\deq\;\;}l@{}}
       \vbl{Init}_{C}    & \begin{conj}
                           \vbl{out} \in \{0,1\}\\
                           \vbl{in} = [i\in \{1,\ldots, \rvbl{n}\} 
                                            \mapsto \vbl{out}]
                           \vjot
                        \end{conj} \\
       \vbl{Input}(i) & \begin{conj}
                           \vbl{in}[i] = \vbl{out}\\
                           \vbl{in}' = [\vbl{in} \;{\bf except}\;
                                         ![i] = 1-\vbl{in}[i]\,]\\
                           \vbl{out}'=\vbl{out} \vjot
                        \end{conj}\\
       \vbl{Output}   &  \begin{conj}
                          \forall i \in \{1,\ldots,\rvbl{n}\} : 
                             \vbl{in}[i]\neq \vbl{out}\\
                           \vbl{out}'= 1-\vbl{out}\\
                           \vbl{in}' = \vbl{in} \vjot
                         \end{conj}
                       \\
       \vbl{Next}     & \vbl{Output} \,\lor\,
           \exists\,i\in \{1,\ldots, \rvbl{n}\} : \vbl{Input}(i)
                           \\[\jot]
    \Pi_{C}  & \vbl{Init}_{C} \land 
                            \Box\sqact{{}\vbl{Next}}{\tuple{\vbl{in},\vbl{out}}}
                \land \WF{\tuple{\vbl{in},\vbl{out}}}{\vbl{Output}}
   \end{array}
\)
\caption{A TLA specification of an \rvbl{n}-input C-element.}
\label{fig:TLA-C-element}
\end{figure}
%
%
The specification $\Pi_{C}$ is short and precise.  However, it is not
as reader-friendly as a predicate-action diagram.  We therefore use
diagrams to help explain the specification, beginning with the
predicate-action diagram of Figure~\ref{fig:inouti}.  It is a 
  \index{diagram|see{predicate-action diagram}}%
  \index{predicate-action diagram!of a state function}%
diagram {\em
of\/} the state function \tuple{\vbl{in}[i],\vbl{out}}, meaning that
it describes transitions that change \tuple{\vbl{in}[i],\vbl{out}}.
It is a diagram 
   \index{predicate-action diagram!for a formula}%
{\em for\/} the formula $\Pi_{C}$, meaning that it
represents a formula that is implied by $\Pi_{C}$.  The diagram shows
the synchronization between the C-element's $i$th input and its
output.

\begin{figure}
\centering
\begin{picture}(200,120)(-105,-60)
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\newcommand{\inouti}[4]{\put(#1,#2){\makebox(0,0){%
      \(\begin{array}{@{\land\;}l@{\,=\,}l@{}}
            \vbl{in}[i] & #3\\
            \vbl{out} & #4
         \end{array}\)}}
         \put(#1,#2){\oval(60,30)}}
\inouti{-65}{0}00
\inouti{0}{45}10
\inouti{65}{0}11
\inouti{0}{-45}01
%
\put(-39,11){\vector(2,3){14}} %% other endpoint = (-25,31)
\put(24,32){\vector(2,-3){14}}
\put(39,-11){\vector(-2,-3){14}} %% other endpoint = (-25,31)
\put(-24,-32){\vector(-2,3){14}}
%
\put(-105,0){\vector(1,0){10}}
\put(105,0){\vector(-1,0){10}}
\end{picture}
\caption{A predicate-action diagram of \tuple{\vbl{in}[i],\vbl{out}}
for the specification $\Pi_{C}$ of an \rvbl{n}-input C-element, where
$1\leq i\leq \rvbl{n}$.}
\label{fig:inouti}
\end{figure}

We can draw many different predicate-action diagrams for the same
specification.  Figure~\ref{fig:inouti-2} shows another diagram of
\tuple{\vbl{in}[i],\vbl{out}} for $\Pi_{C}$.  
%
\begin{figure}
\centering
%\begin{picture}(190,34)(-100,-17)
\begin{picture}(190,44)(-100,-17)
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\put(-60,0){\makebox(0,0){$\vbl{in}[i]=\vbl{out}$}}
\put(-60,0){\oval(60,25)}
\put(60,0){\makebox(0,0){$\vbl{in}[i]\neq\vbl{out}$}}
\put(60,0){\oval(60,25)}
%
\put(-100,0){\vector(1,0){10}}
\bezier{75}(-32,8)(0,25)(32,8)
\put(32,8){\vector(2,-1){0}}
\bezier{75}(-32,-8)(0,-25)(32,-8)
\put(-32,-8){\vector(-2,1){0}}
\end{picture}
\caption{Another predicate-action diagram of \tuple{\vbl{in}[i],\vbl{out}}
for $\Pi_{C}$, where $1\leq i\leq 
 \rvbl{n}$.}  %% n -> \rvbl{n} -- 24 Aug 95
\label{fig:inouti-2}
\end{figure}
%
It is simpler than the one in Figure~\ref{fig:inouti}, but it contains
less information.  It does not indicate that the values of
$\vbl{in}[i]$ and \vbl{out} are always 0 or 1, and it does not show
which variable is changed by each transition.  The latter information
is added in the diagram of Figure~\ref{fig:inouti-3}(a), where each
transition is labeled with an action.  The label $\vbl{Input}(i)$ on
the left-to-right arrow indicates that a transition from a state
satisfying $\vbl{in}[i]=\vbl{out}$ to a state satisfying
$\vbl{in}[i]\neq\vbl{out}$ is an $\vbl{Input}(i)$ step.  This diagram
represents the TLA formula of Figure~\ref{fig:inouti-3}(b).

\begin{figure} \small
(a) A predicate-action diagram of \tuple{\vbl{in}[i],\vbl{out}}.
\vspace{.5\baselineskip}

\begin{centering}
\begin{picture}(190,56)(-100,-28)
%\makegrid(-200,-100)(400,200)
\normalsize
\thicklines%%\small
\put(-60,0){\makebox(0,0){$\vbl{in}[i]=\vbl{out}$}}
\put(-60,0){\oval(60,25)}
\put(60,0){\makebox(0,0){$\vbl{in}[i]\neq\vbl{out}$}}
\put(60,0){\oval(60,25)}
%
\put(-100,0){\vector(1,0){10}}
\bezier{75}(-32,8)(0,25)(32,8)
\put(32,8){\vector(2,-1){0}}
\bezier{75}(-32,-8)(0,-25)(32,-8)
\put(-32,-8){\vector(-2,1){0}}
%
\put(0,20){\makebox(0,0)[b]{\footnotesize$\vbl{Input}(i)$}}
\put(0,-20){\makebox(0,0)[t]{\footnotesize\vbl{Output}}}
\end{picture}

\end{centering}

\vspace{\baselineskip}
(b) The corresponding TLA formula.
\vspace{.5\baselineskip}

\begin{centering}%%\small
\( \begin{conj}
      \vbl{in}[i]=\vbl{out}\\[\jot]
      \Box\sqact{{}(\vbl{in}[i]=\vbl{out}) \implies
                    \vbl{Input}(i)  \land (\vbl{in}'[i]\neq\vbl{out}')
                }{\tuple{\vbl{in}[i],\vbl{out}}\vjot}\vjot\\
      \Box\sqact{{}(\vbl{in}[i]\neq\vbl{out}) \implies
                    \vbl{Output}  \land (\vbl{in}'[i]=\vbl{out}')
                }{\tuple{\vbl{in}[i],\vbl{out}}}
    \end{conj}
\)

\end{centering}

\caption{A more informative predicate-action diagram of 
\tuple{\vbl{in}[i],\vbl{out}} 
for $\Pi_{C}$, and the corresponding TLA formula.}
\label{fig:inouti-3}
\end{figure}

Even more information is conveyed by a predicate-action diagram of
\tuple{\vbl{in},\vbl{out}}, which also shows transitions that leave
$\vbl{in}[i]$ and \vbl{out} unchanged but change $\vbl{in}[j]$ for
some $j\neq i$.  Such a diagram is drawn in
Figure~\ref{fig:inouti-4}(a).  Figure~\ref{fig:inouti-4}(b) gives the
corresponding TLA formula.

\begin{figure} \small
(a) A predicate-action diagram of \tuple{\vbl{in},\vbl{out}}.
\vspace{.5\baselineskip}

\begin{centering}
\begin{picture}(190,75)(-100,-28)
\normalsize
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\put(-60,0){\makebox(0,0){$\vbl{in}[i]=\vbl{out}$}}
\put(-60,0){\oval(60,25)}
\put(60,0){\makebox(0,0){$\vbl{in}[i]\neq\vbl{out}$}}
\put(60,0){\oval(60,25)}
%
\put(-100,0){\vector(1,0){10}}
\bezier{75}(-32,8)(0,25)(32,8)
\put(32,8){\vector(2,-1){0}}
\bezier{75}(-32,-8)(0,-25)(32,-8)
\put(-32,-8){\vector(-2,1){0}}
\put(0,20){\makebox(0,0)[b]{\footnotesize$\vbl{Input}(i)$}}
\put(0,-20){\makebox(0,0)[t]{\footnotesize\vbl{Output}}}
%
\bezier{100}(-65,12.5)(-82.5,38.5)(-60,38.5)
\bezier{100}(-55,12.5)(-42.5,38.5)(-60,38.5)
\put(-65,12.5){\vector(1,-2){0}}
\put(-60,40.5){\makebox(0,0)[b]{\footnotesize$\exists\,j\neq i:\vbl{Input}(j)$}}
%
\bezier{100}(65,12.5)(82.5,38.5)(60,38.5)
\bezier{100}(55,12.5)(42.5,38.5)(60,38.5)
\put(55,12.5){\vector(1,-2){0}}
\put(60,40.5){\makebox(0,0)[b]{\footnotesize$\exists\,j\neq i:\vbl{Input}(j)$}}
\end{picture}

\end{centering}

\vspace{.5\baselineskip}

(b) The corresponding TLA formula.
\vspace{.5\baselineskip}

\begin{centering} %%\small
\( \begin{conj}
      \vbl{in}[i]=\vbl{out}\\[\jot]
      \Box \left[ \begin{array}{@{}l@{}}
(\vbl{in}[i]=\vbl{out}) \implies \\[.2em]
             \hspace*{1em}\left( \begin{array}{@{\lor\;}l}
                      \vbl{Input}(i) \land 
                             (\vbl{in}'[i]\neq\vbl{out}')\\
                      (\exists\,j\neq i:\vbl{Input}(j)) \land 
                                      (\vbl{in}'[i]
                         =\vbl{out}')
                    \end{array}
             \right)
                  \end{array}
           \right]_{\tuple{\vbl{in},\vbl{out}}\vjot}\vjot\\
       \Box \left[ \begin{array}{@{}l@{}}
                (\vbl{in}[i]\neq\vbl{out}) \implies\\[.2em]
             \hspace*{1em}\left( \begin{array}{@{\lor\;}l}
                      \vbl{Output}  \land (\vbl{in}'[i]=\vbl{out}')\\
                      (\exists\,j\neq i:\vbl{Input}(j)) \land (\vbl{in}'[i]
                        \neq\vbl{out}')
                    \end{array}
             \right)
            \end{array}
           \right]_{\tuple{\vbl{in},\vbl{out}}}  
    \end{conj}
\)

\end{centering}
\caption{A  predicate-action diagram of 
\tuple{\vbl{in},\vbl{out}}
for $\Pi_{C}$, and the corresponding TLA formula, where
$1\leq i\leq\rvbl{n}$.}
\label{fig:inouti-4}
\end{figure}



There are innumerable predicate-action diagrams that can be drawn for
a specification.  Figure~\ref{fig:yet-another} shows yet another
diagram for the C-element specification $\Pi_{C}$.  Since we are not
relying on these diagrams as our specification, but simply to help
explain the specification, we can show as much or as little
information in them as we wish.  We can draw multiple diagrams to
illustrate different aspects of a system.  Actual specifications are
written as TLA formulas, which are much more expressive than pictures.


\begin{figure}
\centering
\begin{picture}(190,75)(-100,-28)
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\put(-60,0){\makebox(0,0){$\vbl{in}[i]=\vbl{out}$}}
\put(-60,0){\oval(60,25)}
\put(60,0){\makebox(0,0){$\vbl{in}[i]\neq\vbl{out}$}}
\put(60,0){\oval(60,25)}
%
\put(-100,0){\vector(1,0){10}}
\bezier{75}(-32,8)(0,25)(32,8)
\put(32,8){\vector(2,-1){0}}
\bezier{75}(-32,-8)(0,-25)(32,-8)
\put(-32,-8){\vector(-2,1){0}}
\put(0,20){\makebox(0,0)[b]{\footnotesize$\vbl{in}'[i]=1-\vbl{in}[i]$}}
\put(0,-20){\makebox(0,0)[t]{\footnotesize$\vbl{out}'=1-\vbl{out}$}}
%
\bezier{100}(-65,12.5)(-82.5,38.5)(-60,38.5)
\bezier{100}(-55,12.5)(-42.5,38.5)(-60,38.5)
\put(-65,12.5){\vector(1,-2){0}}
%\put(-60,40.5){\makebox(0,0)[b]{\footnotesize$\exists\,j\neq 
%                 i:\vbl{Input}(j)$}}
%
\bezier{100}(65,12.5)(82.5,38.5)(60,38.5)
\bezier{100}(55,12.5)(42.5,38.5)(60,38.5)
\put(55,12.5){\vector(1,-2){0}}
%\put(60,40.5){\makebox(0,0)[b]{\footnotesize$\exists\,j\neq i:\vbl{Input}(j)$}}
\end{picture}

\caption{Yet another predicate-action diagram of \tuple{\vbl{in},\vbl{out}}
for $\Pi_{C}$.}
\label{fig:yet-another}
\end{figure}

%try
\subsection{A Formal Treatment}


\subsubsection{Definition} \label{sec:definition}

We first define precisely the TLA formula
represented by a diagram.  Formally, a predicate-action diagram
consists of a directed graph, with a subset of the nodes identified as
initial nodes, where each node is labeled by a state predicate and
each edge is labeled by an action.  We assume a given diagram of a
state function $v$ and introduce the following notation.
\begin{tabbing}
  \hspace{\parindent}\=\+ $E(n)$ \= \kill
    \index{N@$N$}%
  $N$           \> The set of nodes.                         \\
    \index{I@$I$}%
  $I$           \> The set of initial nodes.                 \\
    \index{E@$E(\ldots)$}%
  $E(n)$        \> The set of edges originating at node $n$. \\
    \index{d@$d(\ldots)$}%
  $d(e)$        \> The destination node of edge $e$.         \\
    \index{P+@$P_{n}$}%
  $P_{n}$       \> The predicate labeling node $n$.          \\
    \index{E+@$\act{E}_{e}$}%
  $\act{E}_{e}$ \> The action labeling edge $e$.
\end{tabbing}
The formula 
  \index{+2Delta@$\Delta$}%
$\Delta$ represented by the diagram 
is defined as follows.%
  \index{InitDelta@$\vbl{Init}_{\Delta}$}%
  \index{A@$\act{A}_{n}$}%
 \[ \begin{array}{@{}l@{\;\;\deq\;\;}l@{}}
      \vbl{Init}_{\Delta}  & \exists\, n\in I : P_{n}\\[\jot]
      \act{A}_{n} & \exists\, e \in E(n) : \act{E}_{e}\land P_{d(e)}'\\[\jot]
      \Delta & \vbl{Init}_{\Delta} \,\land\, \forall n \in N : 
             \Box\sqact{{}P_{n}\implies\act{A}_{n}}{v}
   \end{array}
 \]
When no explicit label is attached to an edge $e$, we take
$\act{E}_{e}$ to be \true.  When no set of initial nodes is explicitly
indicated, we take $I$ to be $N$.  With the usual convention for
quantification over an empty set, $\act{A}_{n}$ is defined to equal
\false\ if there are no edges originating at node $n$.


\subsubsection{Another Interpretation}

Another possible interpretation of the predicate-action diagram
is the formula 
  \index{+2DeltaHat@$\widehat{\Delta}$}%
$\widehat{\Delta}$, defined by
  \[  \widehat{\Delta} \;\;\deq\;\; \vbl{Init}_{\Delta} \,\land\, 
             \Box\sqact{{}\exists\,n \in N : P_{n}\land\act{A}_{n}}{v}
  \]
This is perhaps a more obvious interpretation---especially if the
diagram is viewed as a description of a next-state relation.  We now
show that $\Delta$ always implies $\widehat{\Delta}$, and that the
converse implication holds if the predicates labeling the nodes are
disjoint.

\vspace{\topsep} \noindent 
(A)  $\Delta$ implies $\widehat{\Delta}$.\\[.25\baselineskip]
%
{\em Proof\/}: A simple invariance proof, using rule INV1 
of \cite[Figure 5, page 888]{lamport:newtla},
shows that
 $\Delta$ implies 
$\Box(\exists\,n \in N : P_{n})$. 
We then have:
\begin{eqnarray*}
    \Delta & \deq &
    \vbl{Init}_{\Delta}\;\land\;
        \forall\,n\in N:\Box\sqact{{}P_{n}\implies\act{A}_{n}}{v}
    \\
     & \equiv & 
    \begin{array}[t]{@{}l@{}}
      \vbl{Init}_{\Delta}\;\land\;
       \Box(\sqact{{}\exists\,n\in N:P_{n}}{v})\; \\
        \hspace*{1em}\mbox{}\;\land\;
           \forall\,n\in N:\Box\sqact{{}P_{n}\implies\act{A}_{n}}{v}
    \end{array} \\[-\jot]
     &  & \reason{because 
                  $\Delta$ implies $\Box(\exists\,n\in N:P_{n})$}\\
     & \equiv &  
       \vbl{Init}_{\Delta}\;\land\;
        \Box [ \begin{array}[t]{@{}l@{}}
                (\exists\,n\in N:P_{n}) \\
        \hspace*{1em}\mbox{}\;\land\;
              \forall\,n\in N:(P_{n}\implies\act{A}_{n})]_{v}
               \end{array}
\\[-\jot]
     &  & \reason{because $\Box$ distributes over conjunction and $\forall$, 
                  and\\
                  $[X]_v \land \forall n \in N : [Y_n]_{v}$ is 
                  equivalent to \\ $[X \land \forall n \in N : Y_n]_{v}$}
           \\
     & \implies & \vbl{Init}_{\Delta}\;\land\;
        \Box \sqact{{}\exists\,n\in N:P_{n}\land\act{A}_{n}}{v}\\[-\jot]
     &  & \reason{by predicate logic, since $\act{B}\implies\act{C}$
                 implies $\Box\sqact{B}{v}\implies\Box\sqact{C}{v}$}\\
    & \deq & \widehat{\Delta} 
\end{eqnarray*}

\noindent 
(B)  If $\lnot(P_{m}\land P_{n})$ holds for all $m$, $n$ in $N$ with
    $m\neq n$, then $\widehat{\Delta}$ implies $\Delta$.\\[.25\baselineskip]
%
{\em Proof\/}:  By propositional logic, the hypothesis implies
 \[ (\exists\,n\in N:P_{n}\land\act{A}_{n})
     \,\implies\,
    (\forall\,n\in N: P_{n}\implies\act{A}_{n})
 \]
The result then follows from simple temporal reasoning, essentially by
the reverse of the string of equivalences and implication used to
prove (A).~\dbar

 \vspace{\topsep} 
We usually label the nodes of a predicate-action
diagram with disjoint predicates, in which case (A) and (B) imply that
the interpretations $\Delta$ and $\widehat{\Delta}$ are equivalent.
Diagrams with nondisjoint node labels may occasionally be useful;
$\Delta$ is the more convenient interpretation of such diagrams.


\subsection{Proving a Predicate-Action Diagram}

Saying that a diagram is a predicate-action diagram for a
specification $\Pi$ asserts that $\Pi$ implies the formula $\Delta$
represented by the diagram.  Formula $\Pi$ will usually have the form
 $\vbl{Init}_{\Pi}\,\land\, \Box\sqact{M}{u} \,\land\, L$,
where $L$ is a fairness condition.  Formula $\Delta$ equals
 $\vbl{Init}_{\Delta}\,\land\,\forall n \in N : 
     \Box\sqact{{}P_{n}\implies\act{A}_{n}}{v}$.
To prove 
$\Pi\implies\Delta$, we prove:
\begin{enumerate}
\item $\vbl{Init}_{\Pi} \;\implies\; \vbl{Init}_{\Delta}$
\item $\vbl{Init}_{\Pi}\,\land\,\Box\sqact{M}{u}  \;\implies\;
      \Box\sqact{{}P_{n}\implies\act{A}_{n}}{v}$, for each node $n$.
\end{enumerate}
The first condition is an assertion about predicates; it is generally
easy to prove.  To prove the second condition, one usually finds an
invariant \vbl{Inv} such that
$\vbl{Init}_{\Pi}\,\land\,\Box\sqact{M}{u}$ implies $\Box\vbl{Inv}$,
so $\Pi$ implies $\Box\sqact{M\land \vbl{Inv}}{u}$.  The second
condition is then proved by showing that \sqact{M\land
\vbl{Inv}}{u} implies \sqact{{}P_{n}\implies\act{A}_{n}}{v}, for each
node $n$.  Usually, $u$ and $v$ are tuples and every component
of $v$ is a component of $u$, so \unchanged{u} implies \unchanged{v}.
In this case, one need show only that $\act{M}\land \vbl{Inv}$ implies
\sqact{{}P_{n}\implies\act{A}_{n}}{v}, for each $n$.  By definition of
$\act{A}_{n}$, this means proving
  \[ P_{n}\land \act{M}\land \vbl{Inv} \;\implies\;
     (\exists\,m\in E(n) : \act{E}_{m}\land P_{d(m)}') \,\lor\,
      (\unchanged{v})
  \]
for each node $n$.  This formula asserts that an \act{M} step that
starts with $P_{n}$ and \vbl{Inv} true and changes $v$ is an
$\act{E}_{m}$ step that ends in a state satisfying $P_{d(m)}$, for
some edge $m$ originating at node $n$.%
 \index{predicate-action diagram|)}


%try
\section{Illustrating Proofs} \label{sec:proof}

In TLA, there is no distinction between a specification and a
property; they are both formulas.  Verification means proving that one
formula implies another.  A practical, relatively complete set of
rules for proving such implications is described
in~\cite{lamport:newtla}.  We show here how predicate-action diagrams
can be used to illustrate these proofs.  We take as our example the
same one treated in~\cite{lamport:newtla}, that the specification
$\Psi$ defined in Section~\ref{sec:another} below implies the
specification $\Phi$ defined in Section~\ref{sec:TLA} above.


\subsection{Another Specification} \label{sec:another}

We define a TLA formula 
  \index{+2Y@$\Psi$}%%
$\Psi$ describing a program with two
processes, each of which repeatedly loops through the sequence of
operations $P(\vbl{sem})$; \vbl{in\-cre\-ment}; $V(\vbl{sem})$, where
one process increments $x$ by one and the other increments $y$ by one.
Here, 
  \index{P@$P(\ldots)$}%
$P(\vbl{sem})$ and 
  \index{V@$V(\ldots)$}%
$V(\vbl{sem})$ denote the usual operations on
a semaphore 
  \index{sem@\vbl{sem}}%
\vbl{sem}.  To describe this program formally, we
introduce a variable 
  \index{pc@\vbl{pc}}%
\vbl{pc} that indicates the control state.  Each
process has three control points, which we call 
    \index{+2q@\str{\ldots}}%
\str{a}, \str{b}, and
\str{g}.  (Quotes indicate 
  \index{strings}%
string values.)

We motivate the definition of $\Psi$ with the three predicate-action
diagrams for $\Psi$ in Figure~\ref{fig:2-diagrams}.  In these
diagrams, the predicate 
    \index{PC@\vbl{PC}}%%
$\vbl{PC}(p,q)$ asserts that control is at $p$
in process~1 and at $q$ in process~2.  Figure~\ref{fig:2-diagrams}(a)
shows how 
%
%
\begin{figure*} 
\centering
\hspace*{1.5em}{\small (a)}\hfill\mbox{}\\[-\baselineskip]
\begin{picture}(290,130)(-145,-65)
%\makegrid(-200,-100)(400,200)
\thicklines\small
\newcommand{\pcval}[4]{\put(#1,#2){\makebox(0,0){$\vbl{PC}(\str{#3},\str{#4})$}}
                       \put(#1,#2){\oval(60,20)}}
\pcval{-100}{0}aa
\pcval{0}{30}ba
\pcval{0}{-30}ab
\pcval{110}{30}ga
\pcval{110}{-30}ag
%
\put(30,30){\vector(1,0){50}}
\put(55,33){\makebox(0,0)[b]{$x'=x+1$}}
%
\put(-71,5){\vector(2,1){42}}
\put(-45,20){\makebox(0,0)[br]{$P(\vbl{sem})$}}
%
\put(140,42.5){\oval(10,25)[r]}
\put(140,55){\line(-1,0){275}}
\put(-135,42.5){\oval(10,25)[lt]}
\put(-140,45){\line(0,-1){25}}
\bezier{75}(-140,20)(-140,15)(-129,5)
\put(-129,5){\vector(1,-1){0}}
\put(2.5,59){\makebox(0,0)[b]{ $V(\vbl{sem})$}} %% top
%
\put(30,-30){\vector(1,0){50}}
\put(55,-33){\makebox(0,0)[t]{$y'=y+1$}}     
%
\put(-71,-5){\vector(2,-1){42}}
\put(-45,-20){\makebox(0,0)[tr]{$P(\vbl{sem})$}} 
%
\put(140,-42.5){\oval(10,25)[r]}
\put(140,-55){\line(-1,0){275}}
\put(-135,-42.5){\oval(10,25)[lb]}
\put(-140,-45){\line(0,1){25}}
\bezier{75}(-140,-20)(-140,-15)(-129,-5)
\put(-129,-5){\vector(1,1){0}}
\put(2.5,-57){\makebox(0,0)[t]{$V(\vbl{sem})$}} %% bottom
%
\put(-145,0){\vector(1,0){15}}
\end{picture}
%
\vspace{1.25\baselineskip}
%

\hspace*{1.5em}{\small (b)}\hfill\mbox{}\\[-\baselineskip]
\begin{picture}(290,130)(-145,-65)
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\newcommand{\pcval}[4]{\put(#1,#2){\makebox(0,0){\small
                                    $\vbl{PC}(\str{#3},\str{#4})$}}
                       \put(#1,#2){\oval(60,20)}}
\pcval{-100}{0}aa
\pcval{0}{30}ba
\pcval{0}{-30}ab
\pcval{110}{30}ga
\pcval{110}{-30}ag
%
\put(30,30){\vector(1,0){50}}
\put(55,33){\makebox(0,0)[b]{$\beta_{1}$}}
%
\put(-71,5){\vector(2,1){42}}
\put(-45,20){\makebox(0,0)[br]{$\alpha_{1}$}}
%
\put(140,42.5){\oval(10,25)[r]}
\put(140,55){\line(-1,0){275}}
\put(-135,42.5){\oval(10,25)[lt]}
\put(-140,45){\line(0,-1){25}}
\bezier{75}(-140,20)(-140,15)(-129,5)
\put(-129,5){\vector(1,-1){0}}
\put(2.5,59){\makebox(0,0)[b]{ $\gamma_{1}$}} %% top
%
\put(30,-30){\vector(1,0){50}}
\put(55,-33){\makebox(0,0)[t]{$\beta_{2}$}}     
%
\put(-71,-5){\vector(2,-1){42}}
\put(-45,-20){\makebox(0,0)[tr]{$\alpha_{2}$}} 
%
\put(140,-42.5){\oval(10,25)[r]}
\put(140,-55){\line(-1,0){275}}
\put(-135,-42.5){\oval(10,25)[lb]}
\put(-140,-45){\line(0,1){25}}
\bezier{75}(-140,-20)(-140,-15)(-129,-5)
\put(-129,-5){\vector(1,1){0}}
\put(2.5,-57){\makebox(0,0)[t]{$\gamma_{2}$}} %% bottom
%
\put(-145,0){\vector(1,0){15}}
\end{picture}

\vspace{1.25\baselineskip}


\hspace*{1.5em}{\small (c)}\hfill\mbox{}\\[-\baselineskip]
\begin{picture}(190,66)(-100,-28)
%\makegrid(-200,-100)(400,200)
\thicklines%%\small
\put(-60,0){\makebox(0,0){$\vbl{sem}=1$}}
\put(-60,0){\oval(60,25)}
\put(60,0){\makebox(0,0){$\vbl{sem}=0$}}
\put(60,0){\oval(60,25)}
%
\put(-100,0){\vector(1,0){10}}
\bezier{75}(-32,8)(0,25)(32,8)
\put(32,8){\vector(2,-1){0}}
\bezier{75}(-32,-8)(0,-25)(32,-8)
\put(-32,-8){\vector(-2,1){0}}
\put(0,20){\makebox(0,0)[b]{\small
                              $\alpha_{1}\lor\alpha_{2}$}}
\put(0,-20){\makebox(0,0)[t]{\small
                              $\gamma_{1}\lor\gamma_{2}$}}
\bezier{100}(65,12.5)(82.5,38.5)(60,38.5)
\bezier{100}(55,12.5)(42.5,38.5)(60,38.5)
\put(55,12.5){\vector(1,-2){0}}
\put(76,30){\makebox(0,0)[l]{\small
                               $\beta_{1}\lor\beta_{2}$}}
%\put(60,40.5){\makebox(0,0)[b]{\small$\beta_{1}\lor\beta_{2}$}}
\end{picture}

\caption{Three predicate-action diagrams of \tuple{x,y,\vbl{pc},\vbl{sem}}
         for $\Psi$.}
\label{fig:2-diagrams}
\end{figure*}
%
%
the control state changes when the $P(\vbl{sem})$, $V(\vbl{sem})$, and
{\em increment\/} actions are performed.  Variables other than
\vbl{pc} not mentioned in an edge label are left unchanged by the
indicated steps---for example, steps described by the edge labeled
$x'=x+1$ leave $y$ and \vbl{sem} unchanged---but this is not 
asserted by the diagram.  The next-state action 
  \index{N+@\act{N}}%
\act{N} is written as
the disjunction $\act{N}_{1}\lor\act{N}_{2}$ of the next-state actions
of each process; and each $\act{N}_{i}$ is written as the disjunction
$\alpha_{i}\lor\beta_{i}\lor\gamma_{i}$.
Figure~\ref{fig:2-diagrams}(b) illustrates this decomposition.
Finally, the predicate-action diagram of
Figure~\ref{fig:2-diagrams}(c) describes how the semaphore variable
\vbl{sem} changes.

To write the specification $\Psi$, we let \vbl{pc} be a function with
domain $\{1,2\}$, with $\vbl{pc}[i]$ indicating where control resides
in process~$i$.  The formula $\vbl{PC}(p, q)$ can then be defined by
  \index{PC@\vbl{PC}}%%
 \[ \vbl{PC}(p, q) \;\;\deq\;\; (\vbl{pc}[1]=p)\,\land\,(\vbl{pc}[2]=q)
 \]
The semaphore actions $P$ and $V$ are defined by%
  \index{P@$P(\ldots)$}\index{V@$V(\ldots)$}%
 \[  \begin{array}{@{}l@{}}
   P(\vbl{sem}) \;\;\deq\;\; \begin{conj}
                                  0 < \vbl{sem} \\ 
                                  \vbl{sem}'=\vbl{sem}-1
                               \end{conj}
 \\
%    \hspace{2em}
   V(\vbl{sem}) \;\;\deq\;\; \vbl{sem}'=\vbl{sem}+1
     \end{array}
 \]
Missing from Figure~\ref{fig:2-diagrams} are a specification of the
initial values of $x$ and $y$, which we take to be zero, and a fairness
condition.  One could augment predicate-action diagrams with some
notation for indicating fairness conditions.  However, the conditions
that are easy to represent with a diagram are not expressive enough to
describe the variety of fairness requirements that arise in practice.
The WF and SF formulas, which are expressive enough, are not easy to
represent graphically.  So, we have not attempted to represent
fairness in our diagrams.  We take as the fairness condition for our
specification $\Psi$ strong fairness on the next-state action
$\act{N}_{i}$ of each process.  The complete definition of $\Psi$
appears in Figure~\ref{fig:psi}.


\begin{figure*}
  \index{+2Y@$\Psi$}%%
  \index{N+@\act{N}}%
\centering
\small
%
\(\begin{array}[t]{@{}l@{}}
     \vbl{Init}_{\Psi} \;\;\deq\;\;
        \begin{array}[t]{@{\land\;\;}l@{}}
           \vbl{pc} = [i\in\{1,2\} \mapsto \str{a}]\\
           (x=0) \,\land\, (y=0)\\
           \vbl{sem}=1 \vjjot
        \end{array}
 \\
     \alpha_{i} \;\;\deq\;\;
        \begin{array}[t]{@{\land\;\;}l@{}}
           (\vbl{pc}[i] = \str{a}) \land (0<\vbl{sem}) \\
           \vbl{pc}' = [\vbl{pc}\;{\bf except}\; ![i]=\str{b}]\\
           \vbl{sem}' = \vbl{sem}-1 \\
           \unchanged{\tuple{x,\,y}} \vjjot
        \end{array}
 \\
     \gamma_{i} \;\;\deq\;\;
        \begin{array}[t]{@{\land\;\;}l@{}}
           \vbl{pc}[i] = \str{g}\\
           \vbl{pc}' = [\vbl{pc}\;{\bf except}\; ![i]=\str{a}]\\
           \vbl{sem}' = \vbl{sem}+1 \\           
           \unchanged{\tuple{x,\,y}} \vjjot
        \end{array}
% \\[\jot]
%     \makebox[0pt][l]{\(
%           \Psi \;\;\deq\;\; \vbl{Init}_{\Psi}\,\land\,\Box\sqact{N}{w}
%                      \,\land\, \SF{w}{\act{N}_{1}} \land \SF{w}{\act{N}_{2}}
%                 \)}
\end{array}
%
\hspace{2em}
%
  \begin{array}[t]{@{}l@{}}
     \beta_{1} \;\;\deq\;\;
        \begin{array}[t]{@{\land\;\;}l@{}}
           \vbl{pc}[1] = \str{b}\\
           \vbl{pc}' = [\vbl{pc}\;{\bf except}\; ![1]=\str{g}]\\
           x'= x+1\\
           \unchanged{\tuple{y,\,\vbl{sem}}} \vjjot\\
         \end{array}
  \\
     \beta_{2} \;\;\deq\;\;
        \begin{array}[t]{@{\land\;\;}l@{}}
           \vbl{pc}[2] = \str{b}\\
           \vbl{pc}' = [\vbl{pc}\;{\bf except}\; ![2]=\str{g}]\\
            y'= y+1\\
            \unchanged{\tuple{x,\,\vbl{sem}}} \vjjot\\
         \end{array}
 \\
     \act{N}_{i} \;\;\deq\;\; \alpha_{i}\lor\beta_{i}\lor\gamma_{i}
 \\[.5\jot]
     \act{N} \;\;\deq\;\; \act{N_{1}} \lor \act{N_{2}}
 \\[.5\jot]
     w \;\;\deq\;\; \tuple{x, y, \vbl{sem}, \vbl{pc}}\end{array}
\) \\[\jot]
\( \Psi \;\;\deq\;\; \vbl{Init}_{\Psi}\,\land\,\Box\sqact{N}{w}
                      \,\land\, \SF{w}{\act{N}_{1}} \land \SF{w}{\act{N}_{2}}\)

\caption{The specification $\Psi$.} \label{fig:psi}
\end{figure*}


%try
\subsection{An Illustrated Proof}

The proof of $\Psi\implies\Phi$ is broken into the proof of three conditions:
\begin{enumerate}
 \item $\vbl{Init}_{\Psi}\implies\vbl{Init}_{\Phi}$
 \item $\vbl{Init}_{\Psi}\,\land\,\Box\sqact{N}{w} \,\implies\,
           \Box\sqact{M}{\tuple{x,y}}$
 \item $\Psi\implies\WF{\tuple{x,y}}{\act{M}_{i}}$, for $i=1,2$
\end{enumerate}
We illustrate the proofs of conditions 2 and 3 with the
predicate-action diagram of \tuple{x,y,\vbl{sem},\vbl{pc}} for $\Psi$
in Figure~\ref{fig:std-for-Psi}, where \vbl{Q} is defined by
    \index{Q@\vbl{Q}}%%
 \[ \vbl{Q}_{i}(p,q) \;\;\deq\;\; 
     \begin{conj}
        \vbl{PC}(p,q)\\
        sem \;=\; i\\
        (x\in\vbl{Nat})\land (y\in\vbl{Nat})
     \end{conj}
 \]
and \vbl{Nat} is the set of natural numbers.


\begin{figure*}
\centering
\begin{picture}(290,137)(-145,-65)
%\begin{picture}(290,132)(-145,-65)
%\makegrid(-200,-100)(400,200)
\thicklines\footnotesize
\newcommand{\pcval}[5]{\put(#1,#2){\makebox(0,0){%
                                    $\vbl{Q}_{#5}(\str{#3},\str{#4})$}}
                       \put(#1,#2){\oval(60,20)}}
\pcval{-100}{0}aa1
\pcval{0}{30}ba0
\pcval{0}{-30}ab0
\pcval{110}{30}ga0
\pcval{110}{-30}ag0
%
\put(30,30){\vector(1,0){50}}
\put(55,33){\makebox(0,0)[b]{$\act{M}_{1}$}}
%
\put(-71,5){\vector(2,1){42}}
\put(-45,20){\makebox(0,0)[br]{\unchanged{\tuple{x,y}}}}
%
\put(140,42.5){\oval(10,25)[r]}
\put(140,55){\line(-1,0){275}}
\put(-135,42.5){\oval(10,25)[lt]}
\put(-140,45){\line(0,-1){25}}
\bezier{75}(-140,20)(-140,15)(-129,5)
\put(-129,5){\vector(1,-1){0}}
\put(2.5,59){\makebox(0,0)[b]{\unchanged{\tuple{x,y}}}}
%
\put(30,-30){\vector(1,0){50}}
\put(55,-33){\makebox(0,0)[t]{$\act{M}_{2}$}}
%
\put(-71,-5){\vector(2,-1){42}}
\put(-45,-20){\makebox(0,0)[tr]{\unchanged{\tuple{x,y}}}}
%
\put(140,-42.5){\oval(10,25)[r]}
\put(140,-55){\line(-1,0){275}}
\put(-135,-42.5){\oval(10,25)[lb]}
\put(-140,-45){\line(0,1){25}}
\bezier{75}(-140,-20)(-140,-15)(-129,-5)
\put(-129,-5){\vector(1,1){0}}
\put(2.5,-57){\makebox(0,0)[t]{\unchanged{\tuple{x,y}}}}
%
\put(-145,0){\vector(1,0){15}}
\end{picture}
\caption{Another  predicate-action diagram of \tuple{x,y,\vbl{sem},\vbl{pc}}
         for  $\Psi$.}
\label{fig:std-for-Psi}
\end{figure*}


First, we must show that the diagram in Figure~\ref{fig:std-for-Psi}
is a predicate-action diagram for $\Psi$.  This is easy using
the definition in Section~\ref{sec:definition}; no
invariant is needed.  For example, the condition to be proved for the
node labeled $\vbl{Q}_{0}(\str{b},\str{a})$ is that an \act{N} step that
starts with $\vbl{Q}_{0}(\str{b},\str{a})$ true is an $\act{M}_{1}$ step
(one that increments $x$ and leaves $y$ unchanged) that makes
$\vbl{Q}_{0}(\str{g},\str{a})$ true.  This follows easily from the
definitions of \vbl{Q} and \act{N}, since an \act{N} step starting
with $\vbl{PC}(\str{b},\str{a})$ true must be a $\beta_{1}$ step.

To prove condition 2, it suffices to prove that every step allowed by
the diagram of Figure~\ref{fig:std-for-Psi} is a
\sqact{M}{\tuple{x,y}} step.  The steps not shown explicitly by the
diagram are ones that leave $w$ unchanged.  Such steps leave
\tuple{x,y} unchanged, so they are \sqact{M}{\tuple{x,y}} steps.  The
actions labeling all the edges of the diagram imply
\sqact{M}{\tuple{x,y}}, so all the steps shown explicitly by the
diagram are also \sqact{M}{\tuple{x,y}} steps.  This proves
condition~2.

We now sketch the proof of condition~3.  To prove
\WF{\tuple{x,y}}{\act{M}_{i}}, it suffices to show that infinitely
many \anact{M_{i}}{\tuple{x,y}} steps occur.  We first observe that
each of the predicates labeling a node in the diagram implies that
either \anact{N_{1}}{w} or \anact{N_{2}}{w} is enabled.  The fairness
condition of $\Psi$ then implies that a behavior cannot remain forever
at any node, but must keep moving through the diagram.  Hence, the
behavior must infinitely often pass through the
$\vbl{Q}_{1}(\str{a},\str{a})$ node.  The predicate
$\vbl{Q}_{1}(\str{a},\str{a})$ implies that both \anact{N_{1}}{w} and
\anact{N_{2}}{w} are enabled.  Hence, the fairness condition
$\SF{w}{\act{N}_{1}} \land \SF{w}{\act{N}_{2}}$ implies that
infinitely many \anact{N_{1}}{w} steps and infinitely many
\anact{N_{2}}{w} steps must occur.  Action \anact{N_{1}}{w} is enabled
only in the three nodes of the top loop.  Taking infinitely many
\anact{N_{1}}{w} steps is therefore possible only by going around the
top loop infinitely many times, which implies that infinitely many
$\act{M}_{1}$ steps occur, each starting in a state with
$\vbl{Q}_{0}(\str{b},\str{a})$ true.  %% "true" added 24 Aug 95
Since $\vbl{Q}_{0}(\str{b},\str{a})$
implies $x\in\vbl{Nat}$, an $\act{M}_{1}$ step starting with
$\vbl{Q}_{0}(\str{b},\str{a})$ true changes $x$, so it is an
\anact{M_{1}}{\tuple{x,y}} step.  Hence, infinitely many
\anact{M_{1}}{\tuple{x,y}} steps occur.  Similarly, taking infinitely
many \anact{N_{2}}{w} steps implies that infinitely many
\anact{M_{2}}{\tuple{x,y}} steps occur.  This completes the proof of
condition~3.

Using the predicate-action diagram does not simplify the proof.  If we
were to make the argument given above rigorous, we would go through
precisely the same steps as in the proof described
in~\cite{lamport:newtla}.  However, the diagram does allow us to
visualize the proof, which can help us to understand it.

%try

\section{Conclusion}

We have described three uses of diagrams that we believe are new
for diagrams with a precise formal semantics:
\begin{itemize}
\item To describe particular aspects of a complex specification with a
simple diagram.  An $n$-input C-element cannot be specified with a
simple picture.  However, we explained the specification with 
diagrams describing the synchronization between the output and each
individual input.

\item To provide complementary views of the same system.  Diagrams (b)
and (c) of Figure~\ref{fig:2-diagrams} look quite different, but they are
diagrams for the same specification.

\item To illustrate proofs.  The disjunction of the predicates
labeling the nodes in Figure~\ref{fig:std-for-Psi} equals the
invariant $I$ of the proof in Section~7.2 of~\cite{lamport:newtla}.
The diagram provides a graphical representation of the invariance
proof.
\end{itemize}

TLA differs from traditional specification methods in two important
ways.  First, all TLA specifications are interpreted over the same set
of states.  Instead of assigning values just to the variables that
appear in the specification, a state assigns values to all of the
infinite number of variables that can appear in any specification.
Second, TLA specifications are invariant under stuttering.  
A formula can neither require nor rule out finite sequences of
steps that do not change any variables mentioned in the formula.  (The
state-function subscripts in TLA formulas are there to guarantee
invariance under stuttering.)

These two differences lead to two major differences between
traditional state-transition diagrams and predicate-action diagrams.
In traditional diagrams, each node represents a single state.  Because
states in TLA assign values to an infinite number of variables, it is
impossible to describe a single state with a formula.  Any formula can
specify the values of only a finite number of variables.  To draw
diagrams of TLA formulas, we let each node represent a predicate,
which describes a set of states.  In traditional diagrams, every
possible state change is indicated by an edge.  Because TLA formulas
are invariant under stuttering, we draw diagrams of particular state
functions---usually tuples of variables.

TLA differs from most specification methods because it is a logic.  It
uses simple logical operations like implication and conjunction
instead of more complicated automata-based notions of simulation and
composition~\cite{abadi:conjoining}.  Everything we have done with
predicate-action diagrams can be done with state-transition diagrams
in any purely state-based formalism.  However, conventional formalisms
must use some notion of homomorphism between diagrams to describe what
is expressed in TLA as logical implication.

Most formalisms employing state-transition diagrams are not purely
state-based, but use both states and events.  Nodes represent
states, and edges describe input and output events.  The meaning of a
diagram is the sequence of events it allows; the states are
effectively hidden.  In TLA, there are only states, not events.
Systems are described in terms of changes to interface variables
rather than in terms of interface events.  Variables
describing the internal state are hidden
with the existential quantifier \EE\ described
in~\cite{lamport:newtla}.  Changes to any variable, whether internal
or interface, can be indicated by node labels or edge labels.  Hence,
a purely state-based approach like TLA allows more flexibility in how
diagrams are drawn than a method based on states and events.

%try
\bibliographystyle{ieeetr}
%\bibliography{mybib}

\begin{thebibliography}{1}

\bibitem{mealy:method}
G.~H. Mealy, ``A method for synthesizing sequential circuits,'' {\em Bell
  System Technical Journal}, vol.~34, pp.~1045--1079, Sept. 1955.

\bibitem{moore:gedanken}
E.~F. Moore, ``Gedanken-experiments on sequential machines,'' in {\em Automata
  Studies} (C.~E. Shannon and J.~McCarthy, eds.), pp.~129--153, Princeton, New
  Jersey: Princeton University Press, 1956.

\bibitem{lamport:newtla}
L.~Lamport, ``The temporal logic of actions,'' {\em ACM Trans. Programming
  Languages and Systems}, vol.~16, pp.~872--923, May 1994.

\bibitem{alpern:defining}
B.~Alpern and F.~B. Schneider, ``Defining liveness,'' {\em Information
  Processing Letters}, vol.~21, pp.~181--185, Oct. 1985.

\bibitem{seitz:system-timing}
C.~Mead and L.~Conway, {\em Introduction to VLSI Systems}, ch.~7.
\newblock Reading, Massachusetts: Addison-Wesley, 1980.

\bibitem{abadi:conjoining}
M.~Abadi and L.~Lamport, ``Conjoining specifications,'' Research Report 118,
  Digital Equipment Corporation, Systems Research Center, 1993.
\newblock To appear in {\em ACM Transactions on Programming Languages and
  Systems}.

\end{thebibliography}


\begin{biography}{Leslie Lamport}
Leslie Lamport attended the Bronx High School of Science, where he
took a course in mechanical drawing.  He later received a Ph.D. in
mathematics from Brandeis University, where he studied the propagation
of singularities in the Cauchy problem for analytic partial
differential equations.  Since 1985, he has been a member of Digital
Equipment Corporation's Systems Research Laboratory, where he has
written several biographical sketches.
\end{biography}

\end{document}
