\batchmode %% Suppresses most terminal output.
\documentclass{article}
\usepackage{color}
\definecolor{boxshade}{gray}{0.85}
\setlength{\textwidth}{360pt}
\setlength{\textheight}{541pt}
\usepackage{latexsym}
\usepackage{ifthen}
% \usepackage{color}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SWITCHES                                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newboolean{shading} 
\setboolean{shading}{false}
\makeatletter
 %% this is needed only when inserted into the file, not when
 %% used as a package file.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                           %
% DEFINITIONS OF SYMBOL-PRODUCING COMMANDS                                  %
%                                                                           %
%    TLA+      LaTeX                                                        %
%    symbol    command                                                      %
%    ------    -------                                                      %
%    =>        \implies                                                     %
%    <:        \ltcolon                                                     %
%    :>        \colongt                                                     %
%    ==        \defeq                                                       %
%    ..        \dotdot                                                      %
%    ::        \coloncolon                                                  %
%    =|        \eqdash                                                      %
%    ++        \pp                                                          %
%    --        \mm                                                          %
%    **        \stst                                                        %
%    //        \slsl                                                        %
%    ^         \ct                                                          %
%    \A        \A                                                           %
%    \E        \E                                                           %
%    \AA       \AA                                                          %
%    \EE       \EE                                                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\symlength}
\newcommand{\implies}{\Rightarrow}
\newcommand{\ltcolon}{\mathrel{<\!\!\mbox{:}}}
\newcommand{\colongt}{\mathrel{\!\mbox{:}\!\!>}}
\newcommand{\defeq}{\;\mathrel{\smash   %% keep this symbol from being too tall
    {{\stackrel{\scriptscriptstyle\Delta}{=}}}}\;}
\newcommand{\dotdot}{\mathrel{\ldotp\ldotp}}
\newcommand{\coloncolon}{\mathrel{::\;}}
\newcommand{\eqdash}{\mathrel = \joinrel \hspace{-.28em}|}
\newcommand{\pp}{\mathbin{++}}
\newcommand{\mm}{\mathbin{--}}
\newcommand{\stst}{*\!*}
\newcommand{\slsl}{/\!/}
\newcommand{\ct}{\hat{\hspace{.4em}}}
\newcommand{\A}{\forall}
\newcommand{\E}{\exists}
\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{%
   $\forall\hspace{-.517em}\forall\hspace{-.517em}\forall$}}%
   \forall\hspace{-.517em}\forall \hspace{-.517em}\forall\,$}}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{%
   $\exists\hspace{-.517em}\exists\hspace{-.517em}\exists$}}%
   \exists\hspace{-.517em}\exists\hspace{-.517em}\exists\,$}}
\newcommand{\whileop}{\.{\stackrel
  {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}%
  {-\hspace{-.16em}\triangleright}}}

% Commands are defined to produce the upper-case keywords.
% Note that some have space after them.
\newcommand{\ASSUME}{\textsc{assume }}
\newcommand{\ASSUMPTION}{\textsc{assumption }}
\newcommand{\AXIOM}{\textsc{axiom }}
\newcommand{\BOOLEAN}{\textsc{boolean }}
\newcommand{\CASE}{\textsc{case }}
\newcommand{\CONSTANT}{\textsc{constant }}
\newcommand{\CONSTANTS}{\textsc{constants }}
\newcommand{\ELSE}{\settowidth{\symlength}{\THEN}%
   \makebox[\symlength][l]{\textsc{ else}}}
\newcommand{\EXCEPT}{\textsc{ except }}
\newcommand{\EXTENDS}{\textsc{extends }}
\newcommand{\FALSE}{\textsc{false}}
\newcommand{\IF}{\textsc{if }}
\newcommand{\IN}{\settowidth{\symlength}{\LET}%
   \makebox[\symlength][l]{\textsc{in}}}
\newcommand{\INSTANCE}{\textsc{instance }}
\newcommand{\LET}{\textsc{let }}
\newcommand{\LOCAL}{\textsc{local }}
\newcommand{\MODULE}{\textsc{module }}
\newcommand{\OTHER}{\textsc{other }}
\newcommand{\STRING}{\textsc{string}}
\newcommand{\THEN}{\textsc{ then }}
\newcommand{\THEOREM}{\textsc{theorem }}
\newcommand{\LEMMA}{\textsc{lemma }}
\newcommand{\PROPOSITION}{\textsc{proposition }}
\newcommand{\COROLLARY}{\textsc{corollary }}
\newcommand{\TRUE}{\textsc{true}}
\newcommand{\VARIABLE}{\textsc{variable }}
\newcommand{\VARIABLES}{\textsc{variables }}
\newcommand{\WITH}{\textsc{ with }}
\newcommand{\WF}{\textrm{WF}}
\newcommand{\SF}{\textrm{SF}}
\newcommand{\CHOOSE}{\textsc{choose }}
\newcommand{\ENABLED}{\textsc{enabled }}
\newcommand{\UNCHANGED}{\textsc{unchanged }}
\newcommand{\SUBSET}{\textsc{subset }}
\newcommand{\UNION}{\textsc{union }}
\newcommand{\DOMAIN}{\textsc{domain }}
% Added for tla2tex
\newcommand{\BY}{\textsc{by }}
\newcommand{\OBVIOUS}{\textsc{obvious }}
\newcommand{\HAVE}{\textsc{have }}
\newcommand{\QED}{\textsc{qed }}
\newcommand{\TAKE}{\textsc{take }}
\newcommand{\DEF}{\textsc{ def }}
\newcommand{\HIDE}{\textsc{hide }}
\newcommand{\RECURSIVE}{\textsc{recursive }}
\newcommand{\USE}{\textsc{use }}
\newcommand{\DEFINE}{\textsc{define }}
\newcommand{\PROOF}{\textsc{proof }}
\newcommand{\WITNESS}{\textsc{witness }}
\newcommand{\PICK}{\textsc{pick }}
\newcommand{\DEFS}{\textsc{defs }}
\newcommand{\PROVE}{\settowidth{\symlength}{\ASSUME}%
   \makebox[\symlength][l]{\textsc{prove}}\@s{-4.1}}%
  %% The \@s{-4.1) is a kludge added on 24 Oct 2009 [happy birthday, Ellen]
  %% so the correct alignment occurs if the user types
  %%   ASSUME X
  %%   PROVE  Y
  %% because it cancels the extra 4.1 pts added because of the 
  %% extra space after the PROVE.  This seems to works OK.
  %% However, the 4.1 equals Parameters.LaTeXLeftSpace(1) and
  %% should be changed if that method ever changes.
\newcommand{\SUFFICES}{\textsc{suffices }}
\newcommand{\NEW}{\textsc{new }}
\newcommand{\LAMBDA}{\textsc{lambda }}
\newcommand{\STATE}{\textsc{state }}
\newcommand{\ACTION}{\textsc{action }}
\newcommand{\TEMPORAL}{\textsc{temporal }}
\newcommand{\ONLY}{\textsc{only }}              %% added by LL on 2 Oct 2009
\newcommand{\OMITTED}{\textsc{omitted }}        %% added by LL on 31 Oct 2009
\newcommand{\@pfstepnum}[2]{\ensuremath{\langle#1\rangle}\textrm{#2}}
\newcommand{\bang}{\@s{1}\mbox{\small !}\@s{1}}
%% We should format || differently in PlusCal code than in TLA+ formulas.
\newcommand{\p@barbar}{\ifpcalsymbols
   \,\,\rule[-.25em]{.075em}{1em}\hspace*{.2em}\rule[-.25em]{.075em}{1em}\,\,%
   \else \,||\,\fi}
%% PlusCal keywords
\newcommand{\p@fair}{\textbf{fair }}
\newcommand{\p@semicolon}{\textbf{\,; }}
\newcommand{\p@algorithm}{\textbf{algorithm }}
\newcommand{\p@mmfair}{\textbf{-{}-fair }}
\newcommand{\p@mmalgorithm}{\textbf{-{}-algorithm }}
\newcommand{\p@assert}{\textbf{assert }}
\newcommand{\p@await}{\textbf{await }}
\newcommand{\p@begin}{\textbf{begin }}
\newcommand{\p@end}{\textbf{end }}
\newcommand{\p@call}{\textbf{call }}
\newcommand{\p@define}{\textbf{define }}
\newcommand{\p@do}{\textbf{ do }}
\newcommand{\p@either}{\textbf{either }}
\newcommand{\p@or}{\textbf{or }}
\newcommand{\p@goto}{\textbf{goto }}
\newcommand{\p@if}{\textbf{if }}
\newcommand{\p@then}{\,\,\textbf{then }}
\newcommand{\p@else}{\ifcsyntax \textbf{else } \else \,\,\textbf{else }\fi}
\newcommand{\p@elsif}{\,\,\textbf{elsif }}
\newcommand{\p@macro}{\textbf{macro }}
\newcommand{\p@print}{\textbf{print }}
\newcommand{\p@procedure}{\textbf{procedure }}
\newcommand{\p@process}{\textbf{process }}
\newcommand{\p@return}{\textbf{return}}
\newcommand{\p@skip}{\textbf{skip}}
\newcommand{\p@variable}{\textbf{variable }}
\newcommand{\p@variables}{\textbf{variables }}
\newcommand{\p@while}{\textbf{while }}
\newcommand{\p@when}{\textbf{when }}
\newcommand{\p@with}{\textbf{with }}
\newcommand{\p@lparen}{\textbf{(\,\,}}
\newcommand{\p@rparen}{\textbf{\,\,) }}   
\newcommand{\p@lbrace}{\textbf{\{\,\,}}   
\newcommand{\p@rbrace}{\textbf{\,\,\} }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% REDEFINE STANDARD COMMANDS TO MAKE THEM FORMAT BETTER %
%                                                       %
% We redefine \in and \notin                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\_}{\rule{.4em}{.06em}\hspace{.05em}}
\newlength{\equalswidth}
\let\oldin=\in
\let\oldnotin=\notin
\renewcommand{\in}{%
   {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth][c]{$\oldin$}}}
\renewcommand{\notin}{%
   {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth]{$\oldnotin$}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                  %
% HORIZONTAL BARS:                                 %
%                                                  %
%   \moduleLeftDash    |~~~~~~~~~~                 %
%   \moduleRightDash    ~~~~~~~~~~|                %
%   \midbar            |----------|                %
%   \bottombar         |__________|                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\charwidth}\settowidth{\charwidth}{{\small\tt M}}
\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
\newcommand{\boxsep}{\charwidth}
\newlength{\boxruleht}\setlength{\boxruleht}{.5ex}
\newlength{\boxruledp}\setlength{\boxruledp}{-\boxruleht}
\addtolength{\boxruledp}{\boxrulewd}
\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
                      \hfill\mbox{}}
\newcommand{\@computerule}{%
  \setlength{\boxruleht}{.5ex}%
  \setlength{\boxruledp}{-\boxruleht}%
  \addtolength{\boxruledp}{\boxrulewd}}

\newcommand{\bottombar}{\hspace{-\boxsep}%
  \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}%
  \boxrule
  \raisebox{-\boxrulewd}[0pt][0pt]{%
      \rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

\newcommand{\moduleLeftDash}%
   {\hspace*{-\boxsep}%
     \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule\hspace*{.4em }}

\newcommand{\moduleRightDash}%
    {\hspace*{.4em}\boxrule
    \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}}%\vspace{.2em}

\newcommand{\midbar}{\hspace{-\boxsep}\raisebox{-.5\boxlineht}[0pt][0pt]{%
   \rule[.5ex]{\boxrulewd}{\boxlineht}}\boxrule\raisebox{-.5\boxlineht%
   }[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% FORMATING COMMANDS                                                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PLUSCAL SHADING                                                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% The TeX pcalshading switch is set on to cause PlusCal shading to be
% performed.  This changes the behavior of the following commands and
% environments to cause full-width shading to be performed on all lines.
% 
%   \tstrut \@x cpar mcom \@pvspace
% 
% The TeX pcalsymbols switch is turned on when typesetting a PlusCal algorithm,
% whether or not shading is being performed.  It causes symbols (other than
% parentheses and braces and PlusCal-only keywords) that should be typeset
% differently depending on whether they are in an algorithm to be typeset
% appropriately.  Currently, the only such symbol is "||".
%
% The TeX csyntax switch is turned on when typesetting a PlusCal algorithm in
% c-syntax.  This allows symbols to be format differently in the two syntaxes.
% The "else" keyword is the only one that is.

\newif\ifpcalshading \pcalshadingfalse
\newif\ifpcalsymbols \pcalsymbolsfalse
\newif\ifcsyntax     \csyntaxtrue

% The \@pvspace command makes a vertical space.  It uses \vspace
% except with \ifpcalshading, in which case it sets \pvcalvspace
% and the space is added by a following \@x command.
%
\newlength{\pcalvspace}\setlength{\pcalvspace}{0pt}%
\newcommand{\@pvspace}[1]{%
  \ifpcalshading
     \par\global\setlength{\pcalvspace}{#1}%
  \else
     \par\vspace{#1}%
  \fi
}

% The lcom environment was changed to set \lcomindent equal to
% the indentation it produces.  This length is used by the
% cpar environment to make shading extend for the full width
% of the line.  This assumes that lcom environments are not
% nested.  I hope TLATeX does not nest them.
%
\newlength{\lcomindent}%
\setlength{\lcomindent}{0pt}%

%\tstrut: A strut to produce inter-paragraph space in a comment.
%\rstrut: A strut to extend the bottom of a one-line comment so
%         there's no break in the shading between comments on 
%         successive lines.
\newcommand\tstrut%
  {\raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{1.15em}}}%
   \global\setlength{\vshadelen}{0pt}}
\newcommand\rstrut{\raisebox{-.25em}{\rule{0pt}{1.15em}}%
 \global\setlength{\vshadelen}{0pt}}


% \.{op} formats operator op in math mode with empty boxes on either side.
% Used because TeX otherwise vary the amount of space it leaves around op.
\renewcommand{\.}[1]{\ensuremath{\mbox{}#1\mbox{}}}

% \@s{n} produces an n-point space
\newcommand{\@s}[1]{\hspace{#1pt}}           

% \@x{txt} starts a specification line in the beginning with txt
% in the final LaTeX source.
\newlength{\@xlen}
\newcommand\xtstrut%
  {\setlength{\@xlen}{1.05em}%
   \addtolength{\@xlen}{\pcalvspace}%
    \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\@xlen}}}%
   \global\setlength{\vshadelen}{0pt}%
   \global\setlength{\pcalvspace}{0pt}}

\newcommand{\@x}[1]{\par
  \ifpcalshading
  \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}%
  \fi
  \mbox{$\mbox{}#1\mbox{}$}}  

% \@xx{txt} continues a specification line with the text txt.
\newcommand{\@xx}[1]{\mbox{$\mbox{}#1\mbox{}$}}  

% \@y{cmt} produces a one-line comment.
\newcommand{\@y}[1]{\mbox{\footnotesize\hspace{.65em}%
  \ifthenelse{\boolean{shading}}{%
      \shadebox{#1\hspace{-\the\lastskip}\rstrut}}%
               {#1\hspace{-\the\lastskip}\rstrut}}}

% \@z{cmt} produces a zero-width one-line comment.
\newcommand{\@z}[1]{\makebox[0pt][l]{\footnotesize
  \ifthenelse{\boolean{shading}}{%
      \shadebox{#1\hspace{-\the\lastskip}\rstrut}}%
               {#1\hspace{-\the\lastskip}\rstrut}}}


% \@w{str} produces the TLA+ string "str".
\newcommand{\@w}[1]{\textsf{``{#1}''}}             


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SHADING                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\graymargin{1}
  % The number of points of margin in the shaded box.

% \definecolor{boxshade}{gray}{.85}
% Defines the darkness of the shading: 1 = white, 0 = black
% Added by TLATeX only if needed.

% \shadebox{txt} puts txt in a shaded box.
\newlength{\templena}
\newlength{\templenb}
\newsavebox{\tempboxa}
\newcommand{\shadebox}[1]{{\setlength{\fboxsep}{\graymargin pt}%
     \savebox{\tempboxa}{#1}%
     \settoheight{\templena}{\usebox{\tempboxa}}%
     \settodepth{\templenb}{\usebox{\tempboxa}}%
     \hspace*{-\fboxsep}\raisebox{0pt}[\templena][\templenb]%
        {\colorbox{boxshade}{\usebox{\tempboxa}}}\hspace*{-\fboxsep}}}

% \vshade{n} makes an n-point inter-paragraph space, with
%  shading if the `shading' flag is true.
\newlength{\vshadelen}
\setlength{\vshadelen}{0pt}
\newcommand{\vshade}[1]{\ifthenelse{\boolean{shading}}%
   {\global\setlength{\vshadelen}{#1pt}}%
   {\vspace{#1pt}}}

\newlength{\boxwidth}
\newlength{\multicommentdepth}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE cpar ENVIRONMENT                                                      %
% ^^^^^^^^^^^^^^^^^^^^                                                      %
% The LaTeX input                                                           %
%                                                                           %
%   \begin{cpar}{pop}{nest}{isLabel}{d}{e}{arg6}                            %
%     XXXXXXXXXXXXXXX                                                       %
%     XXXXXXXXXXXXXXX                                                       %
%     XXXXXXXXXXXXXXX                                                       %
%   \end{cpar}                                                              %
%                                                                           %
% produces one of two possible results.  If isLabel is the letter "T",      %
% it produces the following, where [label] is the result of typesetting     %
% arg6 in an LR box, and d is is a number representing a distance in        %
% points.                                                                   %
%                                                                           %
%   prevailing |<-- d -->[label]<- e ->XXXXXXXXXXXXXXX                      %
%         left |                       XXXXXXXXXXXXXXX                      %
%       margin |                       XXXXXXXXXXXXXXX                      %
%                                                                           %
% If isLabel is the letter "F", then it produces                            %
%                                                                           %
%   prevailing |<-- d -->XXXXXXXXXXXXXXXXXXXXXXX                            %
%         left |         <- e ->XXXXXXXXXXXXXXXX                            %
%       margin |                XXXXXXXXXXXXXXXX                            %
%                                                                           %
% where d and e are numbers representing distances in points.               %
%                                                                           %
% The prevailing left margin is the one in effect before the most recent    %
% pop (argument 1) cpar environments with "T" as the nest argument, where   %
% pop is a number \geq 0.                                                   %
%                                                                           %
% If the nest argument is the letter "T", then the prevailing left          %
% margin is moved to the left of the second (and following) lines of        %
% X's.  Otherwise, the prevailing left margin is left unchanged.            %
%                                                                           %
% An \unnest{n} command moves the prevailing left margin to where it was    %
% before the most recent n cpar environments with "T" as the nesting        %
% argument.                                                                 %
%                                                                           %
% The environment leaves no vertical space above or below it, or between    %
% its paragraphs.  (TLATeX inserts the proper amount of vertical space.)    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcounter{pardepth}
\setcounter{pardepth}{0}

% \setgmargin{txt} defines \gmarginN to be txt, where N is \roman{pardepth}.
% \thegmargin equals \gmarginN, where N is \roman{pardepth}.
\newcommand{\setgmargin}[1]{%
  \expandafter\xdef\csname gmargin\roman{pardepth}\endcsname{#1}}
\newcommand{\thegmargin}{\csname gmargin\roman{pardepth}\endcsname}
\newcommand{\gmargin}{0pt}

\newsavebox{\tempsbox}

\newlength{\@cparht}
\newlength{\@cpardp}
\newenvironment{cpar}[6]{%
  \addtocounter{pardepth}{-#1}%
  \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}%
                                 \begin{minipage}[t]{\linewidth}}{}%
  \begin{list}{}{%
     \edef\temp{\thegmargin}
     \ifthenelse{\equal{#3}{T}}%
       {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}%
        \addtolength{\leftmargin}{#4pt}}%
       {\setlength{\leftmargin}{#4pt}%
        \addtolength{\leftmargin}{#5pt}%
        \addtolength{\leftmargin}{\temp}%
        \setlength{\itemindent}{-#5pt}}%
      \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}%
                                 \setgmargin{\the\leftmargin}}{}%
      \setlength{\labelwidth}{0pt}%
      \setlength{\labelsep}{0pt}%
      \setlength{\itemindent}{-\leftmargin}%
      \setlength{\topsep}{0pt}%
      \setlength{\parsep}{0pt}%
      \setlength{\partopsep}{0pt}%
      \setlength{\parskip}{0pt}%
      \setlength{\itemsep}{0pt}
      \setlength{\itemindent}{#4pt}%
      \addtolength{\itemindent}{-\leftmargin}}%
   \ifthenelse{\equal{#3}{T}}%
      {\item[\tstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}]
        }%
      {\item[\tstrut\hspace{\temp}]%
         }%
   \footnotesize}
 {\hspace{-\the\lastskip}\tstrut
 \end{list}%
  \ifthenelse{\boolean{shading}}%
          {\end{minipage}%
           \end{lrbox}%
           \ifpcalshading
             \setlength{\@cparht}{\ht\tempsbox}%
             \setlength{\@cpardp}{\dp\tempsbox}%
             \addtolength{\@cparht}{.15em}%
             \addtolength{\@cpardp}{.2em}%
             \addtolength{\@cparht}{\@cpardp}%
            % I don't know what's going on here.  I want to add a
            % \pcalvspace high shaded line, but I don't know how to
            % do it.  A little trial and error shows that the following
            % does a reasonable job approximating that, eliminating
            % the line if \pcalvspace is small.
            \addtolength{\@cparht}{\pcalvspace}%
             \ifdim \pcalvspace > .8em
               \addtolength{\pcalvspace}{-.2em}%
               \hspace*{-\lcomindent}%
               \shadebox{\rule{0pt}{\pcalvspace}\hspace*{\textwidth}}\par
               \global\setlength{\pcalvspace}{0pt}%
               \fi
             \hspace*{-\lcomindent}%
             \makebox[0pt][l]{\raisebox{-\@cpardp}[0pt][0pt]{%
                 \shadebox{\rule{0pt}{\@cparht}\hspace*{\textwidth}}}}%
             \hspace*{\lcomindent}\usebox{\tempsbox}%
             \par
           \else
             \shadebox{\usebox{\tempsbox}}\par
           \fi}%
           {}%
  }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE ppar ENVIRONMENT                                                       %
% ^^^^^^^^^^^^^^^^^^^^                                                       %
% The environment                                                            %
%                                                                            %
%   \begin{ppar} ... \end{ppar}                                              %
%                                                                            %
% is equivalent to                                                           %
%                                                                            %
%   \begin{cpar}{0}{F}{F}{0}{0}{} ... \end{cpar}                             %
%                                                                            %
% The environment is put around each line of the output for a PlusCal        %
% algorithm.                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newenvironment{ppar}{%
%  \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}%
%                                 \begin{minipage}[t]{\linewidth}}{}%
%  \begin{list}{}{%
%     \edef\temp{\thegmargin}
%        \setlength{\leftmargin}{0pt}%
%        \addtolength{\leftmargin}{\temp}%
%        \setlength{\itemindent}{0pt}%
%      \setlength{\labelwidth}{0pt}%
%      \setlength{\labelsep}{0pt}%
%      \setlength{\itemindent}{-\leftmargin}%
%      \setlength{\topsep}{0pt}%
%      \setlength{\parsep}{0pt}%
%      \setlength{\partopsep}{0pt}%
%      \setlength{\parskip}{0pt}%
%      \setlength{\itemsep}{0pt}
%      \setlength{\itemindent}{0pt}%
%      \addtolength{\itemindent}{-\leftmargin}}%
%      \item[\tstrut\hspace{\temp}]}%
% {\hspace{-\the\lastskip}\tstrut
% \end{list}%
%  \ifthenelse{\boolean{shading}}{\end{minipage}  
%                                 \end{lrbox}%
%                                 \shadebox{\usebox{\tempsbox}}\par}{}%
%  }

 %%% TESTING
 \newcommand{\xtest}[1]{\par
 \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}%
 \mbox{$\mbox{}#1\mbox{}$}} 

% \newcommand{\xxtest}[1]{\par
% \makebox[0pt][l]{\shadebox{\xtstrut{#1}\hspace*{\textwidth}}}%
% \mbox{$\mbox{}#1\mbox{}$}} 

%\newlength{\pcalvspace}
%\setlength{\pcalvspace}{0pt}
% \newlength{\xxtestlen}
% \setlength{\xxtestlen}{0pt}
% \newcommand\xtstrut%
%   {\setlength{\xxtestlen}{1.15em}%
%    \addtolength{\xxtestlen}{\pcalvspace}%
%     \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\xxtestlen}}}%
%    \global\setlength{\vshadelen}{0pt}%
%    \global\setlength{\pcalvspace}{0pt}}
   
   %%%% TESTING
   
   %% The xcpar environment
   %%  Note: overloaded use of \pcalvspace for testing.
   %%
%   \newlength{\xcparht}%
%   \newlength{\xcpardp}%
   
%   \newenvironment{xcpar}[6]{%
%  \addtocounter{pardepth}{-#1}%
%  \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}%
%                                 \begin{minipage}[t]{\linewidth}}{}%
%  \begin{list}{}{%
%     \edef\temp{\thegmargin}%
%     \ifthenelse{\equal{#3}{T}}%
%       {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}%
%        \addtolength{\leftmargin}{#4pt}}%
%       {\setlength{\leftmargin}{#4pt}%
%        \addtolength{\leftmargin}{#5pt}%
%        \addtolength{\leftmargin}{\temp}%
%        \setlength{\itemindent}{-#5pt}}%
%      \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}%
%                                 \setgmargin{\the\leftmargin}}{}%
%      \setlength{\labelwidth}{0pt}%
%      \setlength{\labelsep}{0pt}%
%      \setlength{\itemindent}{-\leftmargin}%
%      \setlength{\topsep}{0pt}%
%      \setlength{\parsep}{0pt}%
%      \setlength{\partopsep}{0pt}%
%      \setlength{\parskip}{0pt}%
%      \setlength{\itemsep}{0pt}%
%      \setlength{\itemindent}{#4pt}%
%      \addtolength{\itemindent}{-\leftmargin}}%
%   \ifthenelse{\equal{#3}{T}}%
%      {\item[\xtstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}]%
%        }%
%      {\item[\xtstrut\hspace{\temp}]%
%         }%
%   \footnotesize}
% {\hspace{-\the\lastskip}\tstrut
% \end{list}%
%  \ifthenelse{\boolean{shading}}{\end{minipage}  
%                                 \end{lrbox}%
%                                 \setlength{\xcparht}{\ht\tempsbox}%
%                                 \setlength{\xcpardp}{\dp\tempsbox}%
%                                 \addtolength{\xcparht}{.15em}%
%                                 \addtolength{\xcpardp}{.2em}%
%                                 \addtolength{\xcparht}{\xcpardp}%
%                                 \hspace*{-\lcomindent}%
%                                 \makebox[0pt][l]{\raisebox{-\xcpardp}[0pt][0pt]{%
%                                      \shadebox{\rule{0pt}{\xcparht}\hspace*{\textwidth}}}}%
%                                 \hspace*{\lcomindent}\usebox{\tempsbox}%
%                                 \par}{}%
%  }
%  
% \newlength{\xmcomlen}
%\newenvironment{xmcom}[1]{%
%  \setcounter{pardepth}{0}%
%  \hspace{.65em}%
%  \begin{lrbox}{\alignbox}\sloppypar%
%      \setboolean{shading}{false}%
%      \setlength{\boxwidth}{#1pt}%
%      \addtolength{\boxwidth}{-.65em}%
%      \begin{minipage}[t]{\boxwidth}\footnotesize
%      \parskip=0pt\relax}%
%       {\end{minipage}\end{lrbox}%
%       \setlength{\xmcomlen}{\textwidth}%
%       \addtolength{\xmcomlen}{-\wd\alignbox}%
%       \settodepth{\alignwidth}{\usebox{\alignbox}}%
%       \global\setlength{\multicommentdepth}{\alignwidth}%
%       \setlength{\boxwidth}{\alignwidth}%
%       \global\addtolength{\alignwidth}{-\maxdepth}%
%       \addtolength{\boxwidth}{.1em}%
%       \raisebox{0pt}[0pt][0pt]{%
%        \ifthenelse{\boolean{shading}}%
%          {\hspace*{-\xmcomlen}\shadebox{\rule[-\boxwidth]{0pt}{0pt}%
%                                 \hspace*{\xmcomlen}\usebox{\alignbox}}}%
%          {\usebox{\alignbox}}}%
%       \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par}
% % a multi-line comment, whose first argument is its width in points.
%  
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE lcom ENVIRONMENT                                                       %
% ^^^^^^^^^^^^^^^^^^^^                                                       %
% A multi-line comment with no text to its left is typeset in an lcom        % 
% environment, whose argument is a number representing the indentation       % 
% of the left margin, in points.  All the text of the comment should be      % 
% inside cpar environments.                                                  % 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{lcom}[1]{%
  \setlength{\lcomindent}{#1pt} % Added for PlusCal handling.
  \par\vspace{.2em}%
  \sloppypar
  \setcounter{pardepth}{0}%
  \footnotesize
  \begin{list}{}{%
    \setlength{\leftmargin}{#1pt}
    \setlength{\labelwidth}{0pt}%
    \setlength{\labelsep}{0pt}%
    \setlength{\itemindent}{0pt}%
    \setlength{\topsep}{0pt}%
    \setlength{\parsep}{0pt}%
    \setlength{\partopsep}{0pt}%
    \setlength{\parskip}{0pt}}
    \item[]}%
  {\end{list}\vspace{.3em}\setlength{\lcomindent}{0pt}%
 }


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE mcom ENVIRONMENT AND \mutivspace COMMAND                              %
% ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^                              %
%                                                                           %
% A part of the spec containing a right-comment of the form                 %
%                                                                           %
%      xxxx (*************)                                                 %
%      yyyy (* ccccccccc *)                                                 %
%      ...  (* ccccccccc *)                                                 %
%           (* ccccccccc *)                                                 %
%           (* ccccccccc *)                                                 %
%           (*************)                                                 %
%                                                                           %
% is typeset by                                                             %
%                                                                           %
%     XXXX \begin{mcom}{d}                                                  %
%            CCCC ... CCC                                                   %
%          \end{mcom}                                                       %
%     YYYY ...                                                              %
%     \multivspace{n}                                                       %
%                                                                           %
% where the number d is the width in points of the comment, n is the        %
% number of xxxx, yyyy, ...  lines to the left of the comment.              %
% All the text of the comment should be typeset in cpar environments.       %
%                                                                           %
% This puts the comment into a single box (so no page breaks can occur      %
% within it).  The entire box is shaded iff the shading flag is true.       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\xmcomlen}%
\newenvironment{mcom}[1]{%
  \setcounter{pardepth}{0}%
  \hspace{.65em}%
  \begin{lrbox}{\alignbox}\sloppypar%
      \setboolean{shading}{false}%
      \setlength{\boxwidth}{#1pt}%
      \addtolength{\boxwidth}{-.65em}%
      \begin{minipage}[t]{\boxwidth}\footnotesize
      \parskip=0pt\relax}%
       {\end{minipage}\end{lrbox}%
       \setlength{\xmcomlen}{\textwidth}%       % For PlusCal shading
       \addtolength{\xmcomlen}{-\wd\alignbox}%  % For PlusCal shading
       \settodepth{\alignwidth}{\usebox{\alignbox}}%
       \global\setlength{\multicommentdepth}{\alignwidth}%
       \setlength{\boxwidth}{\alignwidth}%      % For PlusCal shading
       \global\addtolength{\alignwidth}{-\maxdepth}%
       \addtolength{\boxwidth}{.1em}%           % For PlusCal shading
      \raisebox{0pt}[0pt][0pt]{%
        \ifthenelse{\boolean{shading}}%
          {\ifpcalshading
             \hspace*{-\xmcomlen}%
             \shadebox{\rule[-\boxwidth]{0pt}{0pt}\hspace*{\xmcomlen}%
                          \usebox{\alignbox}}%
           \else
             \shadebox{\usebox{\alignbox}}
           \fi
          }%
          {\usebox{\alignbox}}}%
       \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par}
 % a multi-line comment, whose first argument is its width in points.


% \multispace{n} produces the vertical space indicated by "|"s in 
% this situation
%   
%     xxxx (*************)
%     xxxx (* ccccccccc *)
%      |   (* ccccccccc *)
%      |   (* ccccccccc *)
%      |   (* ccccccccc *)
%      |   (*************)
%
% where n is the number of "xxxx" lines.
\newcommand{\multivspace}[1]{\addtolength{\multicommentdepth}{-#1\baselineskip}%
 \addtolength{\multicommentdepth}{1.2em}%
 \ifthenelse{\lengthtest{\multicommentdepth > 0pt}}%
    {\par\vspace{\multicommentdepth}\par}{}}

%\newenvironment{hpar}[2]{%
%  \begin{list}{}{\setlength{\leftmargin}{#1pt}%
%                 \addtolength{\leftmargin}{#2pt}%
%                 \setlength{\itemindent}{-#2pt}%
%                 \setlength{\topsep}{0pt}%
%                 \setlength{\parsep}{0pt}%
%                 \setlength{\partopsep}{0pt}%
%                 \setlength{\parskip}{0pt}%
%                 \addtolength{\labelsep}{0pt}}%
%  \item[]\footnotesize}{\end{list}}
%    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%    % Typesets a sequence of paragraphs like this:                         %
%    %                                                                      %
%    %      left |<-- d1 --> XXXXXXXXXXXXXXXXXXXXXXXX                       %
%    %    margin |           <- d2 -> XXXXXXXXXXXXXXX                       %
%    %           |                    XXXXXXXXXXXXXXX                       %
%    %           |                                                          %
%    %           |                    XXXXXXXXXXXXXXX                       %
%    %           |                    XXXXXXXXXXXXXXX                       %
%    %                                                                      %
%    % where d1 = #1pt and d2 = #2pt, but with no vspace between            %
%    % paragraphs.                                                          %
%    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Commands for repeated characters that produce dashes.              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \raisedDash{wd}{ht}{thk} makes a horizontal line wd characters wide, 
% raised a distance ht ex's above the baseline, with a thickness of 
% thk em's.
\newcommand{\raisedDash}[3]{\raisebox{#2ex}{\setlength{\alignwidth}{.5em}%
  \rule{#1\alignwidth}{#3em}}}

% The following commands take a single argument n and produce the
% output for n repeated characters, as follows
%   \cdash:    -
%   \tdash:    ~
%   \ceqdash:  =
%   \usdash:   _
\newcommand{\cdash}[1]{\raisedDash{#1}{.5}{.04}}
\newcommand{\usdash}[1]{\raisedDash{#1}{0}{.04}}
\newcommand{\ceqdash}[1]{\raisedDash{#1}{.5}{.08}}
\newcommand{\tdash}[1]{\raisedDash{#1}{1}{.08}}

\newlength{\spacewidth}
\setlength{\spacewidth}{.2em}
\newcommand{\e}[1]{\hspace{#1\spacewidth}}
%% \e{i} produces space corresponding to i input spaces.


%% Alignment-file Commands

\newlength{\alignboxwidth}
\newlength{\alignwidth}
\newsavebox{\alignbox}

% \al{i}{j}{txt} is used in the alignment file to put "%{i}{j}{wd}"
% in the log file, where wd is the width of the line up to that point,
% and txt is the following text.
\newcommand{\al}[3]{%
  \typeout{\%{#1}{#2}{\the\alignwidth}}%
  \cl{#3}}

%% \cl{txt} continues a specification line in the alignment file
%% with text txt.
\newcommand{\cl}[1]{%
  \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}%
  \settowidth{\alignboxwidth}{\usebox{\alignbox}}%
  \addtolength{\alignwidth}{\alignboxwidth}%
  \usebox{\alignbox}}

% \fl{txt} in the alignment file begins a specification line that
% starts with the text txt.
\newcommand{\fl}[1]{%
  \par
  \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}%
  \settowidth{\alignwidth}{\usebox{\alignbox}}%
  \usebox{\alignbox}}



  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Ordinarily, TeX typesets letters in math mode in a special math italic    %
% font.  This makes it typeset "it" to look like the product of the         %
% variables i and t, rather than like the word "it".  The following         %
% commands tell TeX to use an ordinary italic font instead.                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ifx\documentclass\undefined
\else
  \DeclareSymbolFont{tlaitalics}{\encodingdefault}{cmr}{m}{it}
  \let\itfam\symtlaitalics
\fi

\makeatletter
\newcommand{\tlx@c}{\c@tlx@ctr\advance\c@tlx@ctr\@ne}
\newcounter{tlx@ctr}
\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7061\relax
\mathcode`a=\tlx@c \mathcode`b=\tlx@c \mathcode`c=\tlx@c \mathcode`d=\tlx@c
\mathcode`e=\tlx@c \mathcode`f=\tlx@c \mathcode`g=\tlx@c \mathcode`h=\tlx@c
\mathcode`i=\tlx@c \mathcode`j=\tlx@c \mathcode`k=\tlx@c \mathcode`l=\tlx@c
\mathcode`m=\tlx@c \mathcode`n=\tlx@c \mathcode`o=\tlx@c \mathcode`p=\tlx@c
\mathcode`q=\tlx@c \mathcode`r=\tlx@c \mathcode`s=\tlx@c \mathcode`t=\tlx@c
\mathcode`u=\tlx@c \mathcode`v=\tlx@c \mathcode`w=\tlx@c \mathcode`x=\tlx@c
\mathcode`y=\tlx@c \mathcode`z=\tlx@c
\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7041\relax
\mathcode`A=\tlx@c \mathcode`B=\tlx@c \mathcode`C=\tlx@c \mathcode`D=\tlx@c
\mathcode`E=\tlx@c \mathcode`F=\tlx@c \mathcode`G=\tlx@c \mathcode`H=\tlx@c
\mathcode`I=\tlx@c \mathcode`J=\tlx@c \mathcode`K=\tlx@c \mathcode`L=\tlx@c
\mathcode`M=\tlx@c \mathcode`N=\tlx@c \mathcode`O=\tlx@c \mathcode`P=\tlx@c
\mathcode`Q=\tlx@c \mathcode`R=\tlx@c \mathcode`S=\tlx@c \mathcode`T=\tlx@c
\mathcode`U=\tlx@c \mathcode`V=\tlx@c \mathcode`W=\tlx@c \mathcode`X=\tlx@c
\mathcode`Y=\tlx@c \mathcode`Z=\tlx@c
\makeatother

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                THE describe ENVIRONMENT                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% It is like the description environment except it takes an argument
% ARG that should be the text of the widest label.  It adjusts the
% indentation so each item with label LABEL produces
%%      LABEL             blah blah blah
%%      <- width of ARG ->blah blah blah
%%                        blah blah blah
\newenvironment{describe}[1]%
   {\begin{list}{}{\settowidth{\labelwidth}{#1}%
            \setlength{\labelsep}{.5em}%
            \setlength{\leftmargin}{\labelwidth}% 
            \addtolength{\leftmargin}{\labelsep}%
            \addtolength{\leftmargin}{\parindent}%
            \def\makelabel##1{\rm ##1\hfill}}%
            \setlength{\topsep}{0pt}}%% 
                % Sets \topsep to 0 to reduce vertical space above
                % and below embedded displayed equations
   {\end{list}}

%   For tlatex.TeX
\usepackage{verbatim}
\makeatletter
\def\tla{\let\%\relax%
         \@bsphack
         \typeout{\%{\the\linewidth}}%
             \let\do\@makeother\dospecials\catcode`\^^M\active
             \let\verbatim@startline\relax
             \let\verbatim@addtoline\@gobble
             \let\verbatim@processline\relax
             \let\verbatim@finish\relax
             \verbatim@}
\let\endtla=\@esphack

\let\pcal=\tla
\let\endpcal=\endtla
\let\ppcal=\tla
\let\endppcal=\endtla

% The tlatex environment is used by TLATeX.TeX to typeset TLA+.
% TLATeX.TLA starts its files by writing a \tlatex command.  This
% command/environment sets \parindent to 0 and defines \% to its
% standard definition because the writing of the log files is messed up
% if \% is defined to be something else.  It also executes
% \@computerule to determine the dimensions for the TLA horizonatl
% bars.
\newenvironment{tlatex}{\@computerule%
                        \setlength{\parindent}{0pt}%
                       \makeatletter\chardef\%=`\%}{}


% The notla environment produces no output.  You can turn a 
% tla environment to a notla environment to prevent tlatex.TeX from
% re-formatting the environment.

\def\notla{\let\%\relax%
         \@bsphack
             \let\do\@makeother\dospecials\catcode`\^^M\active
             \let\verbatim@startline\relax
             \let\verbatim@addtoline\@gobble
             \let\verbatim@processline\relax
             \let\verbatim@finish\relax
             \verbatim@}
\let\endnotla=\@esphack

\let\nopcal=\notla
\let\endnopcal=\endnotla
\let\noppcal=\notla
\let\endnoppcal=\endnotla

%%%%%%%%%%%%%%%%%%%%%%%% end of tlatex.sty file %%%%%%%%%%%%%%%%%%%%%%% 
% last modified on Fri  3 August 2012 at 14:23:49 PST by lamport

\begin{document}
\tlatex
\setboolean{shading}{true}
\@x{}\moduleLeftDash\@xx{ {\MODULE} IPOFifo\_pqs}\moduleRightDash\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This module defines the abstract program \ensuremath{IPOFifo\_pqs} described
 in
 Section 7.6.3 of ``A Science of Concurrent Programs'' by \ensuremath{Leslie}
 \ensuremath{Lamport}.
 This program is obtained by obtained by adding auxiliary variables to
 program \ensuremath{IPOFifo} defined in module \ensuremath{IIPOFifo}, The
 module also defines the
 refinement mapping under which \ensuremath{IPOFifi\_pqs} implements program
 \ensuremath{IFifo} of
 module \ensuremath{IFifo}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Here are the three auxiliary variables, in the order in which they are
 added.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{2.5}{0}{}%
Prophecy Variable \ensuremath{p
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\cdash{20}
\end{cpar}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 The prophecy sequence variable \ensuremath{p} is explained in Section 7.6.3.1
 of the
 boook. It predicts the order in which the elements of \ensuremath{elts} will
 be
 dequeued--that is, the sequence of elements that will be dequeued by an
 \ensuremath{EndPODeq} action. A prediction is appended to \ensuremath{p}
 when an element is
 added to \ensuremath{elts}. Note that \ensuremath{p} is a sequence of data,
 identifier pairs not
 just a sequencce of data items. It predicts the element that the
 \ensuremath{EndPODeq} action removes from \ensuremath{elts}, not just the
 data value the Dequeue
 operation returns.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Like most prophecy variables, most of the the predictions \ensuremath{p} can
 make
 can\mbox{'}t possibly be right. Sometimes their impossibility can be
 determined even when the prophecy is made. Logically, that makes no
 difference. An impossible prediction just prevents dequeue operations
 from performing their \ensuremath{EndPODeq} actions. Such prophecies would
 be ruled
 out by a fairness requirement on the \ensuremath{EndPODeq} action.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{2.5}{0}{}%
History Variable \ensuremath{qBar
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\cdash{22}
\end{cpar}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 As described in Section 7.6.3.2, \ensuremath{qBar} is a sequence of datums
 (elements
 of \ensuremath{Data \.{\times} Ids} that equals \ensuremath{pg \.{\circ} eb}
 , where \ensuremath{pg} is the sequence of
 datums that can be removed from the set \ensuremath{elts} by dequeue
 operations even
 if no further enqueue operations are initiated, and \ensuremath{eb} is a
 (hopefully
 empty) sequence of datums in \ensuremath{elts} that can never be removed
 from \ensuremath{elts
} by any dequeue operation.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{50.0}{0}{}%
\cdash{13}
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 Here is a description of how the hisory variable \ensuremath{qBar} is added
 that \ensuremath{I
} wrote before writing the book. It\mbox{'}s more detailed than the one in the
 book, and \ensuremath{I}\mbox{'}m leaving it here because it might help some
 readers to
 understand its definition.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The value of \ensuremath{qBar} is a sequence of elements that is
 approximately the
 value that the refinement mapping assigns to the variable \ensuremath{queue}
 of
 \ensuremath{Fifo} (except it contains not just the \ensuremath{Data} values
 that are in \ensuremath{queue
} but also the identifier associated with that data value). It is not
 exactly the value that implements \ensuremath{queue} because elements
 aren\mbox{'}t added
 to it at the right time. (Stuttering variables will be added later to
 allow defining a refinement mapping that adds the elements to
 \ensuremath{queue
} at the right time.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 To see how to construct \ensuremath{qBar}, let\mbox{'}s pretend we know the
 entire infinite
 sequence \ensuremath{PP} of predictions that will be made by the prophecy
 variable
 P. Call \ensuremath{PP} correct iff it permits a behavior with infinitely
 many
 Dequeue operations (and hence infinitely many Enqueue operations). If
 \ensuremath{PP} is correct, then \ensuremath{p} must always be a subsequence
 of \ensuremath{PP} of length
 equal to the number of elements in elt. We construct \ensuremath{qBar} so
 that, in
 this case, it is the largest prefix of \ensuremath{p} all of whose elements
 are
 already in \ensuremath{elts}. For example, suppose \ensuremath{PP} equals
 \ensuremath{p1}, \ensuremath{p2}, \ensuremath{\backslash}ldots.
 Initially \ensuremath{elts \.{=} \{\}} and \ensuremath{p \.{=} qBar \.{=}
 {\langle} {\rangle}}. Consider the following
 sequence of \ensuremath{BeginPOEnq} and \ensuremath{EndPODeq} actions, with
 the values they add
 or remove from \ensuremath{elts}, and the values of \ensuremath{elts},
 \ensuremath{p}, and \ensuremath{qBar} they produce.
 (We can ignore the \ensuremath{EndPOEnq} and \ensuremath{BeginPODeq}
 actions.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{5.0}{0}{}%
 \ensuremath{BeginPOEnq} of \ensuremath{p2}: \ensuremath{elts \.{=} \{p2\}},
 \ensuremath{p \.{=} {\langle}p1{\rangle}}, \ensuremath{qBar \.{=} {\langle}
 {\rangle}
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{BeginPOEnq} of \ensuremath{p1}: \ensuremath{elts \.{=} \{p1,\,
 p2\}}, \ensuremath{p \.{=} {\langle}p1,\, p2{\rangle}}, \ensuremath{qBar
 \.{=} {\langle}p1,\,p2{\rangle}
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{EndPODeq} of \ensuremath{p2}: \ensuremath{elts \.{=} \{p2\}},
 \ensuremath{p \.{=} {\langle}p2{\rangle}}, \ensuremath{qBar \.{=}
 {\langle}p2{\rangle}
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{BeginPOEnq} of \ensuremath{p7}: \ensuremath{elts \.{=} \{p2,\,
 p7\}}, \ensuremath{p \.{=} {\langle}p2,\, p3{\rangle}}, \ensuremath{qBar
 \.{=} {\langle}p2{\rangle}
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 Note that two elements have been appended to \ensuremath{qBar} at the same
 time.
 Since \ensuremath{Fifo} appends elements to \ensuremath{queue} one at a
 time, we will need a
 stuttering variable to add an extra step so that under the refinement
 mapping they are added one at a time to \ensuremath{queue} .
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 If \ensuremath{PP} is correct, then the elements \ensuremath{p3}, \.{\dots} ,
 \ensuremath{p7} must be enqueued (not
 necessarily in that order) before \ensuremath{p7} can be dequeued. But
 \ensuremath{p} controls
 only the order in which \ensuremath{EndPODeq\_p} actions can dequeue
 elements. It
 doesn\mbox{'}t restrict \ensuremath{EndPODeq\_p} actions. Suppose the
 \ensuremath{EndPOEnq\_p} action for
 the \ensuremath{BeginPOEnq\_p} action that enqueued \ensuremath{p7} is now
 executed. Since that
 action has to implement the \ensuremath{EndDeq} action of \ensuremath{Fifo}
 (because it changes
 the interface variable \ensuremath{enq} the way the \ensuremath{EndDeq}
 action does), \ensuremath{p7} must be
 appended to \ensuremath{qBar} before the \ensuremath{EndPODeq} action
 occurs. (We will use a
 stuttering variable to add the necessary step.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 At that point, it\mbox{'}s still possible for \ensuremath{p2} to be dequeued,
 but any
 further dequeueing should be impossible. Therefore, \ensuremath{PP} is not
 correct.
 Let\mbox{'}s see why further dequeueing is impossible. Since the predictions
 of \ensuremath{PP} determine what elements can be dequeued, for further
 dequeueing
 to occur, \ensuremath{p3} must be the next element dequeued. This means that
 \ensuremath{p3
 } must be enqueued and added to \ensuremath{elts}. However, \ensuremath{p7}
 is still in \ensuremath{elts} and
 its \ensuremath{EndPOEnq} operation has occcurred, so \ensuremath{p7
 \.{\prec} p3} must hold. This
 implies that \ensuremath{p7} must be dequeued before \ensuremath{p3} is,
 something that the
 predictions of \ensuremath{PP} do not predict. So, \ensuremath{p3} and any
 elements other than
 \ensuremath{p2} (which is in \ensuremath{qBar}) can never be dequeued and
 hence never removed
 from \ensuremath{qBar}. So elements can keep being enqueued and appended to
 \ensuremath{qBar} by
 the \ensuremath{EndPOEnq} actions, but once \ensuremath{p2} is dequeued (if
 it ever is) no
 further dequeue operations can finish.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The value of \ensuremath{qBar} always equals the concatenation of these two
 sequences (either or both of which could be empty) of elements in
 \ensuremath{elts}:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{10.0}{2.5}{%
Dequeueable:}%
A prefix of the predictions in \ensuremath{p} that
 could at that point be dequeued by a sequence
 of \ensuremath{EndPODeq} actions.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{T}{10.0}{2.5}{%
Nondequeuable:}%
A sequence of elements of \ensuremath{elts} that cannot be
 dequeued by a sequence of \ensuremath{EndPODeq} actions,
 and were added to \ensuremath{elts} by an Enqueue operation
 that has completed.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
A sequence of predictions can be dequeued if it satisfies the following
 two conditions:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{10.0}{0}{}%
- Each of them predicts an element that is currently in \ensuremath{elts}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{-} No} two of them predict the same element.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
-}%
 If \ensuremath{el1} is in the sequence of predictions and \ensuremath{el2
 \.{\prec} el1} for
 some \ensuremath{el2 \.{\in} elts}, then \ensuremath{el2} must be in the
 sequence and precede
 \ensuremath{el1} in it.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
 An element \ensuremath{e} in \ensuremath{elts} is appended to the
 \ensuremath{Nondequable} part of \ensuremath{qBar} by the
 \ensuremath{EndPOEnq\_p} action of the enqueue operation that added
 \ensuremath{e} to \ensuremath{elts} if \ensuremath{e} is
 not already in \ensuremath{qBar}. (If \ensuremath{e} is already in
 \ensuremath{qBar}, it must be in the
 Dequeueable part.) It has to be in \ensuremath{qBar} at that point because
 the
 \ensuremath{EndPOEnq\_p} action must implement the \ensuremath{EndEnq}
 action of \ensuremath{Fifo}, and that
 value is in \ensuremath{queue} when the \ensuremath{EndEnq} step occurs. (A
 stuttering step
 must be added before the \ensuremath{EndPOEnq} action so that, under the
 refinement
 mapping, the value is added to \ensuremath{queue} before that step.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 A \ensuremath{BeginPOEnq} action that adds \ensuremath{e} should append
 \ensuremath{e} to \ensuremath{qBar} iff
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
(1) The \ensuremath{Nondequeueable} part of \ensuremath{qBar} is empty and
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
(2)}%
 Appending \ensuremath{e} to \ensuremath{qBar} makes \ensuremath{qBar} a
 prefix of sequence \ensuremath{p} of
 predictions that is dequeueable.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
Condition (2) holds iff (1) holds and
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
(a)}%
 \ensuremath{e} is the prediction in the new value of \ensuremath{p} (the
 value after
 execution of the \ensuremath{BeginPOEnq} action) that comes immediately after
 the prefix of \ensuremath{p} that equals \ensuremath{qBar}, and
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{T}{0}{2.5}{%
(\ensuremath{b})}%
 there is no element \ensuremath{ee} in elt that is not in \ensuremath{qBar}
 such that
 \ensuremath{ee \.{\prec} e}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 However, condition (\ensuremath{b}) is impossible if (1) holds, since
 \ensuremath{ee \.{\prec} e} can
 hold iff the \ensuremath{EndPOEnq} action of the enqueue operation that
 added \ensuremath{ee} to
 \ensuremath{elts} has already occurred. But since \ensuremath{ee} is not in
 \ensuremath{qBar}, it was not in
 \ensuremath{qBar} when that action occurred, so the action would have
 appended \ensuremath{ee} to
 the \ensuremath{Nondequeueable} part of \ensuremath{qBar}, contradicting
 (1). Therefore the
 \ensuremath{EndPOEnq} action that adds \ensuremath{e} to \ensuremath{elts}
 must append it to the end of \ensuremath{qBar
} iff conditions (1) and (\ensuremath{2a}) hold.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We saw in the example above that enqueueing \ensuremath{p1} caused both
 \ensuremath{p1} and \ensuremath{p2} to
 be appended to \ensuremath{qBar}. In general, when the
 \ensuremath{Nondequeueable} part of \ensuremath{qBar
 } is empty, appending any element \ensuremath{e} to \ensuremath{qBar} should
 also cause the next
 element in \ensuremath{p} to be appended to \ensuremath{qBar} if it is in
 \ensuremath{elts}. Therefore, if
 condition (1) holds, a \ensuremath{BeginPOEnq} action should set
 \ensuremath{qBar} to \ensuremath{qBar \.{\circ}
 seq}, where \ensuremath{seq} is the maximal subsequence of \ensuremath{p}
 that follows the prefix
 \ensuremath{qBar} of \ensuremath{p}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Finally, because the dequeueable prefix of \ensuremath{qBar} can be defined
 as a
 state function, there\mbox{'}s no need to keep it in a history variable.
 Instead of adding the history variable \ensuremath{qBar}, we add a history
 variable
 h whose value is the nondequeueable suffix of \ensuremath{qBar}. We can then
 consider \ensuremath{qBar} to be a state function whose value equals the
 dequeueable
 prefix of \ensuremath{p} and the sequence \ensuremath{q}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{60.0}{0}{}%
\cdash{22}
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{F}{2.5}{0}{}%
Stuttering Variable \ensuremath{s
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\cdash{21}
\end{cpar}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
As explained in Section 7.6.3.3, we need to add stuttering steps in
 three places to \ensuremath{POFifo\_pq} to be able to define a refinement
 mapping
 under which \ensuremath{POFifo} implements \ensuremath{Fifo}:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
-}%
Immediately before an \ensuremath{EndPODeq\_pq} step we need to add one
 stuttering step.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{T}{0}{2.5}{%
-}%
immediately before an \ensuremath{EndPOEnq} step that appends an element to
 \ensuremath{qBar} not in \ensuremath{pg}, we need to execute one stuttering
 step.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{F}{0}{7.5}{}%
- Immediately after a \ensuremath{BeginPOEnq\_pq} step we need to add as one
 stuttering step for every element added to \ensuremath{qBar}. That is, a
 number
 of stuttering steps equal to amount by which the \ensuremath{BeginPOEnq} step
 increases the length of \ensuremath{qBar}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
We can add the required number of stuttering steps after every
 \ensuremath{BeginPOEnq\_pq} step with a stuttering variable \ensuremath{s}
 as follows.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 1. The condition \ensuremath{s \.{=} 0} is conjoined to the initial-state
 predicate.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
2. Replace the \ensuremath{BeginPOEnq\_pq(e)} action by
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{15.0}{0}{}%
 \ensuremath{\.{\lor}} (\ensuremath{s \.{=} 0}) \ensuremath{\.{\land}
 BeginPOEnq\_pq(e) \.{\land}} (\ensuremath{s\.{'} \.{=} exp})
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{\.{\lor}} (\ensuremath{s \.{>} 0}) \ensuremath{\.{\land}}
 (\ensuremath{s\.{'} \.{=} s\.{-}1}) \ensuremath{\.{\land} {\UNCHANGED}
 POv\_pq
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{F}{7.5}{0}{}%
where the expression \ensuremath{exp} is the number of stuttering steps to
 be added.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
3. Replace each of the other three subactions A of \ensuremath{PONext\_pq} by
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{15.0}{0}{}%
 (\ensuremath{s \.{=} 0}) \ensuremath{\.{\land}} A \ensuremath{\.{\land}}
 (\ensuremath{s\.{'} \.{=} s})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 We can add a single stuttering step before every \ensuremath{EndPOEnq\_pq(d)}
 step
 with a stuttering variable \ensuremath{s} in the same way, except replacing
 step 2
 by:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 2. \ensuremath{\.{\lor} \.{\land}} (\ensuremath{s \.{=} 0})
 \ensuremath{\.{\land} {\ENABLED} EndPODeq\_pq(d)
}%
\end{cpar}%
\begin{cpar}{0}{T}{F}{17.5}{0}{}%
 \ensuremath{\.{\land}} (\ensuremath{s\.{'} \.{=} 1}) \ensuremath{\.{\land}
 {\UNCHANGED} POv\_pq
}%
\end{cpar}%
\begin{cpar}{1}{T}{F}{10.0}{0}{}%
\ensuremath{\.{\lor} \.{\land}} (\ensuremath{s \.{=} 1})
\end{cpar}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
\ensuremath{\.{\land} EndPODeq\_pq(d) \.{\land}} (\ensuremath{s\.{'} \.{=} 0})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
 We need a stuttering step before an \ensuremath{EndPOEnq\_pq(e)} step iff the
 step
 appends an element to \ensuremath{q}. It doesn\mbox{'}t hurt always to add
 the step, since
 an extra stuttering step does no harm. However, it\mbox{'}s a bit more
 convenient not to do that. We can add the stuttering step iff
 necessary by replacing step 2 with:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 2. \ensuremath{\.{\lor} \.{\land}} (\ensuremath{s \.{=} 0})
 \ensuremath{\.{\land} {\ENABLED} EndPOEnq\_pq(e)
}%
\end{cpar}%
\begin{cpar}{0}{T}{T}{17.5}{2.5}{%
\ensuremath{\.{\land} {\IF}} \.{\dots}}%
 \ensuremath{\.{\THEN}} (\ensuremath{s\.{'} \.{=} 1}) \ensuremath{\.{\land}
 {\UNCHANGED} POv\_pq
} \ensuremath{\.{\ELSE} EndPOEnq(e) \.{\land}} (\ensuremath{s\.{'} \.{=} s})
\end{cpar}%
\begin{cpar}{1}{T}{F}{10.0}{0}{}%
\ensuremath{\.{\lor} \.{\land}} (\ensuremath{s \.{=} 1})
\end{cpar}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
\ensuremath{\.{\land} EndPOEnq\_pq(e) \.{\land}} (\ensuremath{s\.{'} \.{=} 0})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
In order to use those stuttering steps in defining the refinement
 mapping, we want the stuttering variable to contain information about
 the action to which it\mbox{'}s adding stuttering steps. Those could be added
 later with another history variable, but they can be put directly into
 \ensuremath{s} by making \ensuremath{s} a tuple one component of which is
 doing the counting down
 and the other components are storing the information. One such piece
 of information is the process taking the stuttering steps.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Instead of adding these three kinds of stuttering steps with three
 different variables, we use a single stuttering variable with a
 component that indicates what kind of action it\mbox{'}s adding the steps to.
\end{cpar}%
\end{lcom}%
\@x{ {\EXTENDS} IPOFifo ,\, Integers ,\, Sequences ,\, TLC}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We will need the assumption on \ensuremath{NoData} to implement the constant
 of the
 same name in \ensuremath{Fifo}.
\end{cpar}%
\end{lcom}%
\@x{ {\CONSTANT} NoData}%
\@x{ {\ASSUME}\@s{4.1} NoData \.{\notin} Data}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{T}{F}{5.0}{0}{}%
***************************************************************************
\end{cpar}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 If \ensuremath{I} were writing this for myself, \ensuremath{I} would probably
 add these three
 auxiliary variables all at once. However, for pedagogical reasons, we
 will add them one at a time to obtain three different abstract
 programs. We first add the prophecy variable \ensuremath{p} to
 \ensuremath{POFifo} to obtain the
 abstract program \ensuremath{POFifo\_p}.
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
***************************************************************************
\end{cpar}%
\end{lcom}%
\@x{ {\VARIABLE} p}%
\@x{ POv\_p \.{\defeq} {\langle} POv ,\, p {\rangle}}%
\@pvspace{8.0pt}%
\@x{ POTypeOK\_p \.{\defeq} POTypeOK \.{\land} ( p \.{\in} Seq ( Datums ) )}%
\@pvspace{8.0pt}%
 \@x{ POInit\_p \.{\defeq} POInit\@s{7.35} \.{\land} p \.{=} {\langle}
 {\rangle}}%
\@pvspace{8.0pt}%
\@x{ BeginPOEnq\_p ( e ) \.{\defeq} \.{\land} BeginPOEnq ( e )}%
 \@x{\@s{99.01} \.{\land} \E\, el \.{\in} Datums \.{:} p \.{'} \.{=} Append (
 p ,\, el )}%
\@pvspace{8.0pt}%
 \@x{ EndPOEnq\_p ( e ) \.{\defeq}\@s{4.1} EndPOEnq ( e ) \.{\land} ( p \.{'}
 \.{=} p )}%
\@pvspace{8.0pt}%
 \@x{ BeginPODeq\_p ( d ) \.{\defeq} BeginPODeq ( d ) \.{\land} ( p \.{'}
 \.{=} p )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The rules for adding a prophecy sequence variable would require us to
 define \ensuremath{EndPODeq\_p(d)} by rewriting the definition of
 \ensuremath{EndPODeq(d)} to have
 the form
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{EndPODeq(d) \.{\defeq} \E\, el \.{\in} Datums} :
 \ensuremath{A(el,\,d)
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
and defining
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{EndPODeq\_p(d) \.{\defeq} A(p[1],\, d) \.{\land}}
 (\ensuremath{p\.{'} \.{=} Tail(p)})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
We can do this by definining \ensuremath{A(el,\,d)} to be
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{EndPODeq(d) \.{\land}} (\ensuremath{elts\.{'} \.{=} elts
 \.{\,\backslash\,} \{el\}})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
This definition of \ensuremath{A(el,\,d)} yields the following definition of
 \ensuremath{EndPODeq\_p(d)}.
\end{cpar}%
\end{lcom}%
 \@x{ EndPODeq\_p ( d ) \.{\defeq}\@s{4.1} EndPODeq ( d ) \.{\land} ( elts
 \.{'} \.{=} elts \.{\,\backslash\,} \{ p [ 1 ] \} ) \.{\land} ( p \.{'}
 \.{=} Tail ( p ) )}%
\@pvspace{8.0pt}%
 \@x{ PONext\_p \.{\defeq} \.{\lor} \E\, e\@s{0.79} \.{\in} EnQers \.{:}
 BeginPOEnq\_p ( e )\@s{4.12} \.{\lor} EndPOEnq\_p ( e )}%
 \@x{\@s{64.52} \.{\lor} \E\, d \.{\in} DeQers\@s{0.25} \.{:} BeginPODeq\_p (
 d )\@s{4.10} \.{\lor} EndPODeq\_p ( d )}%
\@pvspace{8.0pt}%
 \@x{ POFifo\_p\@s{2.53} \.{\defeq} POInit\_p \.{\land} {\Box} [ PONext\_p ]_{
 POv\_p}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We next add the history variable \ensuremath{qBar}. First we define the
 dequeueable
 prefix \ensuremath{pg} of \ensuremath{p}. Remember that it is the largest
 prefix satisfying this
 condition:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{10.0}{0}{}%
- Each element of it is in \ensuremath{elts}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{-} No} two of them predict the same element.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
-}%
 If \ensuremath{el1} is in the prefix and \ensuremath{el2 \.{\prec} el1} for
 some \ensuremath{el2 \.{\in} elts},
 then \ensuremath{el2} must precede \ensuremath{el1} in the prefix
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
 It\mbox{'}s tricky to get the definition right, so to check it \ensuremath{I}
 gave two two
 definitions. The first comes directly from this definition, the second
 is a recursive definition that is more efficiently executed by
 \ensuremath{TLC}.
 (Checking them against one another revealed several errors in both of
 them before they agreed.) The first definition requires the definition
 of \ensuremath{SetMax(S)} to be the maximum of a set of integers, defined to
 equal 0
 if \ensuremath{S} is the empty set.
\end{cpar}%
\end{lcom}%
 \@x{ SetMax ( S ) \.{\defeq} {\IF} S \.{=} \{ \} \.{\THEN} 0 \.{\ELSE}
 {\CHOOSE} n \.{\in} S \.{:} \A\, m \.{\in} S \.{:} n \.{\geq} m}%
\@pvspace{8.0pt}%
 \@x{ prefix ( seq ,\, n ) \.{\defeq} [ j \.{\in} 1 \.{\dotdot} n \.{\mapsto}
 seq [ j ] ]}%
\@pvspace{8.0pt}%
 \@x{ canDeque ( seq ) \.{\defeq} \A\, i \.{\in} 1 \.{\dotdot} Len ( seq )
 \.{:}}%
\@x{\@s{93.42} \.{\land} p [ i ] \.{\in} elts}%
 \@x{\@s{93.42} \.{\land} \A\, j\@s{3.64} \.{\in} 1 \.{\dotdot} ( i \.{-} 1
 )\@s{4.1} \.{:} p [ j ] \.{\neq} p [ i ]}%
\@x{\@s{93.42} \.{\land} \A\, e\@s{2.80} \.{\in} elts \.{:}}%
 \@x{\@s{111.76} e\@s{2.80} \.{\prec} p [ i ] \.{\implies} \E\, j \.{\in} 1
 \.{\dotdot} ( i \.{-} 1 ) \.{:} e \.{=} p [ j ]}%
\@pvspace{16.0pt}%
 \@x{ pg \.{\defeq} \.{\LET} n \.{\defeq} SetMax ( \{ m \.{\in} 1 \.{\dotdot}
 Len ( p ) \.{:} canDeque ( prefix ( p ,\, m ) ) \} )}%
\@x{\@s{28.97} \.{\IN} prefix ( p ,\, n )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The state predicate \ensuremath{pgE} is defined by the recursive definition
 of \ensuremath{pg
 } that is more efficiently executed by \ensuremath{TLC}. It evaluates
 \ensuremath{maxdq(n,\,S)
 } recursively, starting with \ensuremath{maxdq(0,\,\{\})}, and reaching
 \ensuremath{maxdq(n,\,S)} for \ensuremath{n \.{>}
 0} iff the first \ensuremath{n} elements of \ensuremath{p} are dequeueable,
 where \ensuremath{S} is the set of
 elements in \ensuremath{p}. The recursion stops when \ensuremath{n} is the
 length of \ensuremath{p} or
 element \ensuremath{n\.{+}1} of \ensuremath{p} is not dequeueable.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 When model checking the program, we have \ensuremath{TLC} substitute
 \ensuremath{pgE} for \ensuremath{pg}.
\end{cpar}%
\end{lcom}%
\@x{ pgE \.{\defeq} \.{\LET} {\RECURSIVE} maxdq ( \_ ,\, \_ )}%
\@x{\@s{72.87} maxdq ( n ,\, S ) \.{\defeq} {\IF} n \.{=} Len ( p )}%
\@x{\@s{147.38} \.{\THEN} n}%
\@x{\@s{147.38} \.{\ELSE} \.{\LET} e \.{\defeq} p [ n \.{+} 1 ]}%
\@x{\@s{178.69} \.{\IN} {\IF} \.{\land} e \.{\in} elts \.{\,\backslash\,} S}%
 \@x{\@s{211.25} \.{\land} \A\, ee \.{\in} elts \.{\,\backslash\,} ( S
 \.{\cup} \{ e \} ) \.{:}}%
\@x{\@s{233.68} {\lnot} ( ee \.{\prec} e )}%
\@x{\@s{207.29} \.{\THEN} maxdq ( n \.{+} 1 ,\, S \.{\cup} \{ e \} )}%
\@x{\@s{207.29} \.{\ELSE} n}%
 \@x{\@s{48.37} \.{\IN} [ i \.{\in} 1 \.{\dotdot} maxdq ( 0 ,\, \{ \} )
 \.{\mapsto} p [ i ] ]}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Define \ensuremath{appendToH(e)} the formula that, when executing an
 \ensuremath{EndPOEnq(e)
} action, is true iff that action should append the datum enqueued by
 enqueuer \ensuremath{e} to \ensuremath{q}. This is the case iff that datum
 is in \ensuremath{elts} but is not
 in the sequence \ensuremath{pg}.
\end{cpar}%
\end{lcom}%
\@x{ appendToH ( e ) \.{\defeq} \.{\land} adding [ e ] \.{\in} elts}%
 \@x{\@s{82.74} \.{\land} \A\, i \.{\in} 1 \.{\dotdot} Len ( pg ) \.{:} pg [ i
 ] \.{\neq} adding [ e ]}%
\@pvspace{8.0pt}%
\@x{ {\VARIABLE} qBar}%
\@pvspace{8.0pt}%
\@x{ POv\_pq \.{\defeq} {\langle} POv ,\, p ,\, qBar {\rangle}}%
\@pvspace{8.0pt}%
 \@x{ POTypeOK\_pq \.{\defeq} POTypeOK\_p \.{\land} ( qBar \.{\in} Seq (
 Datums ) )}%
\@pvspace{8.0pt}%
 \@x{ POInit\_pq \.{\defeq} POInit\_p \.{\land} ( qBar \.{=} {\langle}
 {\rangle} )}%
\@pvspace{8.0pt}%
 \@x{ BeginPOEnq\_pq ( e ) \.{\defeq} BeginPOEnq\_p ( e ) \.{\land}\@s{4.1} (
 qBar \.{'} \.{=} qBar )}%
\@pvspace{8.0pt}%
\@x{ EndPOEnq\_pq ( e ) \.{\defeq}\@s{4.1} \.{\land} EndPOEnq\_p ( e )}%
\@x{\@s{100.55} \.{\land} qBar \.{'} \.{=} {\IF} appendToH ( e )}%
\@x{\@s{140.61} \.{\THEN} Append ( qBar ,\, adding [ e ] )}%
\@x{\@s{140.61} \.{\ELSE} qBar}%
\@pvspace{8.0pt}%
 \@x{ BeginPODeq\_pq ( d ) \.{\defeq} BeginPODeq\_p ( d ) \.{\land} ( qBar
 \.{'} \.{=} qBar )}%
\@pvspace{8.0pt}%
 \@x{ EndPODeq\_pq ( d ) \.{\defeq} EndPODeq\_p ( d ) \.{\land} ( qBar \.{'}
 \.{=} qBar )}%
\@pvspace{8.0pt}%
 \@x{ PONext\_pq \.{\defeq} \.{\lor} \E\, e\@s{0.79} \.{\in} EnQers \.{:}
 BeginPOEnq\_pq ( e )\@s{4.12} \.{\lor} EndPOEnq\_pq ( e )}%
 \@x{\@s{68.86} \.{\lor} \E\, d \.{\in} DeQers\@s{0.25} \.{:} BeginPODeq\_pq (
 d )\@s{4.10} \.{\lor} EndPODeq\_pq ( d )}%
\@pvspace{8.0pt}%
 \@x{ IPOFifo\_pq \.{\defeq} POInit\_pq \.{\land} {\Box} [ PONext\_pq ]_{
 POv\_pq}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
We now add stuttering variable \ensuremath{s} as described above. Instead of
 writing an expression ENABLED A for the two actions A having a
 stuttering step added before them, \ensuremath{I} have ``evaluated'' that
 \ensuremath{{\ENABLED}
} expression.
\end{cpar}%
\end{lcom}%
\@x{ {\VARIABLE} s}%
\@pvspace{8.0pt}%
\@x{ POv\_pqs \.{\defeq} {\langle} POv ,\, p ,\, qBar ,\, s {\rangle}}%
\@pvspace{8.0pt}%
\@x{ POTypeOK\_pqs \.{\defeq} \.{\land} POTypeOK\_pq}%
 \@x{\@s{89.20} \.{\land} s \.{\in} \{ {\langle} 0 {\rangle} \} \.{\cup} ( Nat
 \.{\times} \{\@w{BeginEnq} \} \.{\times} EnQers )}%
 \@x{\@s{127.65} \.{\cup} ( Nat \.{\times} \{\@w{EndEnq} \}\@s{0.52}
 \.{\times} EnQers )}%
 \@x{\@s{127.65} \.{\cup} ( Nat \.{\times} \{\@w{EndDeq} \} \.{\times} DeQers
 \.{\times} Datums )}%
\@pvspace{8.0pt}%
 \@x{ POInit\_pqs \.{\defeq} POInit\_pq\@s{3.88} \.{\land} ( s \.{=} {\langle}
 0 {\rangle} )}%
\@pvspace{8.0pt}%
\@x{ BeginPOEnq\_pqs ( e ) \.{\defeq} \.{\lor} \.{\land} s [ 1 ] \.{=} 0}%
\@x{\@s{118.49} \.{\land} BeginPOEnq\_pq ( e )}%
 \@x{\@s{118.49} \.{\land} s \.{'} \.{=} {\langle} Len ( pg \.{'} ) \.{-} Len
 ( pg ) ,\,\@w{BeginEnq} ,\, e {\rangle}}%
 \@x{\@s{107.38} \.{\lor} \.{\land} ( s [ 1 ] \.{>} 0 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{BeginEnq} ) \.{\land} ( s [ 3 ] \.{=} e )}%
 \@x{\@s{118.49} \.{\land} ( s \.{'} \.{=} {\langle} s [ 1 ] \.{-} 1
 ,\,\@w{BeginEnq} ,\, e {\rangle} )}%
\@x{\@s{118.49} \.{\land} {\UNCHANGED} POv\_pq}%
\@pvspace{8.0pt}%
 \@x{ EndPOEnq\_pqs ( e ) \.{\defeq}\@s{4.1} \.{\lor} \.{\land} ( s [ 1 ]
 \.{=} 0 ) \.{\land} ( enq [ e ] \.{\neq} Done )}%
\@x{\@s{115.69} \.{\land}\@s{4.1} {\IF} appendToH ( e )}%
 \@x{\@s{139.10} \.{\THEN}\@s{4.1} \.{\land} s \.{'} \.{=} {\langle} 1
 ,\,\@w{EndEnq} ,\, e {\rangle}}%
\@x{\@s{174.51} \.{\land} {\UNCHANGED} POv\_pq}%
\@x{\@s{139.10} \.{\ELSE}\@s{4.10} \.{\land} EndPOEnq\_pq ( e )}%
\@x{\@s{174.51} \.{\land} s \.{'} \.{=} s}%
 \@x{\@s{104.58} \.{\lor} \.{\land} ( s [ 1 ] \.{=} 1 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{EndEnq} )\@s{4.1} \.{\land} ( s [ 3 ] \.{=} e )}%
\@x{\@s{115.69} \.{\land} EndPOEnq\_pq ( e )}%
\@x{\@s{115.69} \.{\land} s \.{'} \.{=} {\langle} 0 {\rangle}}%
\@pvspace{8.0pt}%
 \@x{ BeginPODeq\_pqs ( d ) \.{\defeq}\@s{4.1} ( s [ 1 ] \.{=} 0 ) \.{\land}
 BeginPODeq\_pq ( d )\@s{4.1} \.{\land} ( s \.{'} \.{=} s )}%
\@pvspace{8.0pt}%
 \@x{ EndPODeq\_pqs ( d ) \.{\defeq} \.{\lor} \.{\land} ( s [ 1 ] \.{=} 0 )
 \.{\land} ( deq [ d ] \.{=} Busy ) \.{\land}\@s{4.1} ( pg \.{\neq} {\langle}
 {\rangle} )}%
\@x{\@s{111.62} \.{\land} s \.{'} \.{=} {\langle} 1 ,\,\@w{EndDeq} ,\, d}%
\@y{%
 , \ensuremath{Head(pg)
}}%
\@xx{ {\rangle}}%
\@x{\@s{111.62} \.{\land} {\UNCHANGED} POv\_pq}%
 \@x{\@s{100.51} \.{\lor} \.{\land} ( s [ 1 ] \.{=} 1 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{EndDeq} )\@s{4.1} \.{\land} ( s [ 3 ] \.{=} d )}%
\@x{\@s{111.62} \.{\land} EndPODeq\_pq ( d )}%
\@x{\@s{111.62} \.{\land} s \.{'} \.{=} {\langle} 0 {\rangle}}%
\@pvspace{8.0pt}%
 \@x{ PONext\_pqs \.{\defeq} \.{\lor} \E\, e\@s{0.79} \.{\in} EnQers \.{:}
 BeginPOEnq\_pqs ( e )\@s{4.12} \.{\lor} EndPOEnq\_pqs ( e )}%
 \@x{\@s{72.89} \.{\lor} \E\, d \.{\in} DeQers\@s{0.25} \.{:} BeginPODeq\_pqs
 ( d )\@s{4.10} \.{\lor} EndPODeq\_pqs ( d )}%
\@pvspace{8.0pt}%
 \@x{ IPOFifo\_pqs \.{\defeq} POInit\_pqs \.{\land} {\Box} [ PONext\_pqs ]_{
 POv\_pqs}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We now define the state function \ensuremath{queueBar},
 \ensuremath{deqInnerBar}, and \ensuremath{enqInnerBar
 } so that \ensuremath{POFifo\_pqs} implements \ensuremath{Fifo} under a
 refinement mapping that
 implements the internal variables queue, \ensuremath{deqInner}, and
 \ensuremath{enqInner} with
 these state functions.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
First, we define the sequence \ensuremath{queuE} of elements whose data values
 define \ensuremath{queueBar}. It equals \ensuremath{qBar}, except that:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
-}%
 When adding stuttering steps after \ensuremath{BeginPOEnq\_pq}, the elements
 at the
 end of \ensuremath{pg} have to be appended one at a time by those stuttering
 steps.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{T}{0}{2.5}{%
-}%
The head of \ensuremath{pg} has to be removed by the stutterng step added
 before \ensuremath{EndPODeq\_pq}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{T}{0}{2.5}{%
-}%
The last element of \ensuremath{qBar} has to be appended by a stuttering step
 added before \ensuremath{EndPOEnq\_pq}.
\end{cpar}%
\end{lcom}%
\@x{ queuE \.{\defeq}}%
\@x{\@s{12.29} ( {\IF} s [ 1 ] \.{>} 0}%
\@x{\@s{24.38} \.{\THEN} {\IF} s [ 2 ] \.{=}\@w{BeginEnq}}%
 \@x{\@s{63.89} \.{\THEN}\@s{4.1} [ i \.{\in} 1 \.{\dotdot} ( Len ( pg ) \.{-}
 s [ 1 ] ) \.{\mapsto} pg [ i ] ]}%
\@x{\@s{63.89} \.{\ELSE} {\IF} s [ 2 ] \.{=}\@w{EndDeq}}%
\@x{\@s{103.41} \.{\THEN} Tail ( pg )}%
\@x{\@s{103.41} \.{\ELSE} pg}%
\@x{\@s{24.38} \.{\ELSE} pg )}%
\@x{\@s{12.29} \.{\circ}}%
 \@x{\@s{12.29} ( {\IF} ( s [ 1 ] \.{>} 0 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{EndEnq} )}%
\@x{\@s{24.38} \.{\THEN} Append ( qBar ,\, adding [ s [ 3 ] ] )}%
\@x{\@s{24.38} \.{\ELSE} qBar )}%
\@pvspace{8.0pt}%
 \@x{ queueBar \.{\defeq} [ i \.{\in} 1 \.{\dotdot} Len ( queuE ) \.{\mapsto}
 queuE [ i ] [ 1 ] ]}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The state predicates \ensuremath{deqInnerBar} and \ensuremath{enqInnerBar}
 that are substituted
 for variables \ensuremath{deq} and \ensuremath{enq} of the \ensuremath{Fifo}
 program by the refinement mapping
 are defined so that they make \ensuremath{deq} and \ensuremath{enq} change
 their values the way
 they are supposed to when \ensuremath{queueBar} changes. I found it
 straightforward
 to write the definitions, but having the model checker to find errors
 helped.
\end{cpar}%
\end{lcom}%
\@x{ deqInnerBar\@s{1.02} \.{\defeq} [ d \.{\in} DeQers \.{\mapsto}}%
\@x{\@s{83.99} {\IF} deq [ d ] \.{=} Busy}%
 \@x{\@s{92.19} \.{\THEN} {\IF} ( s [ 1 ] \.{>} 0 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{EndDeq} ) \.{\land} ( s [ 3 ] \.{=} d )}%
\@x{\@s{131.70} \.{\THEN} Head ( pg ) [ 1 ]}%
\@x{\@s{131.70} \.{\ELSE} NoData}%
\@x{\@s{92.19} \.{\ELSE} deq [ d ] ]}%
\@pvspace{16.0pt}%
\@x{ enqInnerBar \.{\defeq} [ e \.{\in} EnQers \.{\mapsto}}%
\@x{\@s{83.19} {\IF} \.{\lor} enq [ e ] \.{=} Done}%
 \@x{\@s{95.35} \.{\lor} \E\, i \.{\in} 1 \.{\dotdot} Len ( queuE ) \.{:}
 adding [ e ] \.{=} queuE [ i ]}%
\@x{\@s{95.35} \.{\lor} adding [ e ] \.{\notin} elts}%
 \@x{\@s{95.35} \.{\lor} ( s [ 1 ] \.{>} 0 ) \.{\land} ( s [ 2 ]
 \.{=}\@w{EndDeq} ) \.{\land} ( adding [ e ] \.{=} Head ( p ) )}%
\begin{lcom}{106.46}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This disjunct is needed because there is one
 case in which the stuttering step after
 \ensuremath{BeginPOEnq(e)} that implements the \ensuremath{DoEnq(e)} of
 \ensuremath{IFifo} has occurred, the \ensuremath{EndPOEnq(e)} step has
 not occurred, and \ensuremath{adding[e]} is neither in \ensuremath{elts
} nor in \ensuremath{queuE}. That\mbox{'}s when the stuttering step
 before the \ensuremath{EndPODeq(d)} step that dequeues
 \ensuremath{adding[e]} has occurred, removing \ensuremath{adding[e]} from
 \ensuremath{queuE}, but the following \ensuremath{EndPODeq(d)} step has
 not occurred. In such a state, only this
 conjunct of the \ensuremath{{\IF}} condition is true.
\end{cpar}%
\end{lcom}%
\@x{\@s{91.39} \.{\THEN} Done}%
\@x{\@s{91.39} \.{\ELSE} Busy ]}%
\@pvspace{8.0pt}%
\begin{lcom}{4.1}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Finally, we define \ensuremath{F{\bang}IFifo} to equal \ensuremath{IFifo}
 \ensuremath{{\WITH}} \ensuremath{queue \.{\leftarrow} queueBar}, \.{\dots}
 and assert that \ensuremath{IPOFifo\_pqs} implies \ensuremath{F{\bang}Fifo}.
\end{cpar}%
\end{lcom}%
 \@x{\@s{4.1} F \.{\defeq} {\INSTANCE} IFifo {\WITH} queue \.{\leftarrow}
 queueBar ,\, deqInner \.{\leftarrow} deqInnerBar ,\,}%
\@x{\@s{138.79} enqInner \.{\leftarrow} enqInnerBar}%
\@pvspace{8.0pt}%
\@x{\@s{4.1} {\THEOREM} IPOFifo\_pqs \.{\implies} F {\bang} IFifo}%
\@x{\@s{4.1}}\bottombar\@xx{}%
\end{document}
