\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} Paxos}\moduleRightDash\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This is a high-level specification of the \ensuremath{Paxos} consensus
 algorithm.
 It refines the spec in module \ensuremath{Voting}, which you should read
 before
 reading this module. In the \ensuremath{Paxos} consensus algorithm, acceptors
 communicate by sending messages. There are additional processes called
 leaders. The specification here essentially considers there to be a
 separate leader for each ballot number. We can consider ``leader'' to be
 a role, where in an implementation there will be a finite number of
 leader processes each of which plays infinitely many of these leader
 roles.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Note: The algorithm described here is the \ensuremath{Paxos} consensus
 algorithm.
 It is the crucial component of the \ensuremath{Paxos} algorithm, which
 implements a
 fault-tolerant state machine using a sequence of instances of the
 consensus algorithm. The \ensuremath{Paxos} algorithm is sometimes called
 \ensuremath{MultiPaxos}, with the \ensuremath{Paxos} consensus algorithm
 being incorrectly called
 the \ensuremath{Paxos} algorithm. I\mbox{'}m afraid I have contributed to
 this confusion
 by being lazy and calling the module ``\ensuremath{Paxos}'' instead of
 ``\ensuremath{PaxosConsensus}''. But incarnations of this module have already
 appeared, so I\mbox{'}m reluctant to change its name now.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\@x{ {\EXTENDS} Integers}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The constants and the assumptions about them are the same as for the
 Voting algorithm. However, the second conjunct of the assumption,
 which asserts that any two quorums have a non-empty intersection, is
 not needed for the \ensuremath{Paxos} consensus algorithm to implement the
 \ensuremath{Voting
 } algorithm. The \ensuremath{Voting} algorithm, and it, do not satisfy
 consensus
 without that assumption.
\end{cpar}%
\end{lcom}%
\@x{ {\CONSTANTS} Value ,\, Acceptor ,\, Quorum}%
\@pvspace{8.0pt}%
 \@x{ {\ASSUME}\@s{4.1} \.{\land} \A\, Q \.{\in} Quorum \.{:} Q \.{\subseteq}
 Acceptor}%
 \@x{\@s{42.34} \.{\land} \A\, Q1 ,\, Q2 \.{\in} Quorum \.{:} Q1 \.{\cap} Q2
 \.{\neq} \{ \}}%
\@pvspace{8.0pt}%
\@x{ Ballot \.{\defeq}\@s{4.1} Nat}%
\@pvspace{8.0pt}%
\@x{ None \.{\defeq} {\CHOOSE} v \.{:} v \.{\notin} Ballot}%
\begin{lcom}{8.2}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This defines \ensuremath{None} to be an unspecified value that is not a ballot
 number.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We now define \ensuremath{Message} toe be the set of all possible messages
 that can
 be sent in the algorithm. In TLA+, the expression
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
(1) [\ensuremath{type \.{\mapsto} \@w{1a}}, \ensuremath{bal \.{\mapsto} b}]
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 is a record \ensuremath{r} with two components, a \ensuremath{type}
 component, \ensuremath{r.type}, that
 equals \ensuremath{\@w{1a}} and whose \ensuremath{bal} component,
 \ensuremath{r.bal}, that equals \ensuremath{b}. The
 expression
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
(2) [type : \ensuremath{\{\@w{1a}\}}, \ensuremath{bal} : \ensuremath{Ballot}]
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 is the set of all records \ensuremath{r} with a components \ensuremath{type}
 and \ensuremath{bal} such that
 \ensuremath{r.type} is an element of \ensuremath{\{\@w{1a}\}} and
 \ensuremath{r.bal} is an element of \ensuremath{Ballot}.
 Since \ensuremath{\@w{1a}} is the only element of \ensuremath{\{\@w{1a}\}},
 formula (2) is the set of all
 elements (1) such that \ensuremath{b \.{\in} Ballot}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The function of each type of message in the set \ensuremath{Message} is
 explained
 below with the action that can send it.
\end{cpar}%
\end{lcom}%
\@x{ Message \.{\defeq}}%
 \@x{\@s{28.7} [ type\@s{2.83} \.{:} \{\@w{1a} \} ,\, bal\@s{1.93} \.{:}
 Ballot ]}%
 \@x{\@s{8.2} \.{\cup}\@s{9.38} [ type\@s{2.83} \.{:} \{\@w{1b} \} ,\, acc
 \.{:} Acceptor ,\, bal \.{:} Ballot ,\,}%
 \@x{\@s{31.47} mbal \.{:} Ballot \.{\cup} \{ \.{-} 1 \} ,\, mval \.{:} Value
 \.{\cup} \{ None \} ]}%
 \@x{\@s{8.2} \.{\cup}\@s{9.38} [ type\@s{2.83} \.{:} \{\@w{2a} \} ,\,
 bal\@s{1.93} \.{:} Ballot ,\, val \.{:} Value ]}%
 \@x{\@s{8.2} \.{\cup}\@s{9.38} [ type\@s{2.83} \.{:} \{\@w{2b} \} ,\, acc
 \.{:} Acceptor ,\, bal \.{:} Ballot ,\, val \.{:} Value ]}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
We now declare the following variables:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{7.5}{2.5}{%
\ensuremath{maxBal \.{-}}}%
Is the same as the variable of that name in the \ensuremath{Voting
} algorithm.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{T}{F}{7.5}{0}{}%
\ensuremath{maxVBal
}%
\end{cpar}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
\ensuremath{maxVal \.{-}}}%
 As in the \ensuremath{Voting} algorithm, a vote is a
 \ensuremath{{\langle}ballot,\, value{\rangle}
 } pair. The pair \ensuremath{{\langle}maxVBal[a],\, maxVal\{a] is}
 \ensuremath{the} \ensuremath{vote} \ensuremath{with
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{the} \ensuremath{largest} \ensuremath{ballot} \ensuremath{number}
 \ensuremath{cast} \ensuremath{by} \ensuremath{acceptor} \ensuremath{a . Tt}
 \ensuremath{equals
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{{\langle}\.{-}1,\, None{\rangle} if} \ensuremath{a}
 \ensuremath{has} \ensuremath{not} \ensuremath{cast} \ensuremath{any}
 \ensuremath{vote.
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 \ensuremath{msgs \.{-} The} \ensuremath{set} \ensuremath{of} \ensuremath{all}
 \ensuremath{messages} \ensuremath{that} \ensuremath{have} \ensuremath{been}
 \ensuremath{sent.
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 \ensuremath{Messages} \ensuremath{are} \ensuremath{added} \ensuremath{to}
 \ensuremath{msgs} \ensuremath{when} \ensuremath{they} \ensuremath{are}
 \ensuremath{sent} \ensuremath{and} \ensuremath{are} \ensuremath{never}
 \ensuremath{removed.
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{An} \ensuremath{operation} \ensuremath{that} \ensuremath{is}
 \ensuremath{performed} \ensuremath{upon} \ensuremath{receipt}
 \ensuremath{of} \ensuremath{a} \ensuremath{message} \ensuremath{is}
 \ensuremath{represented
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{by} \ensuremath{an} \ensuremath{action} \ensuremath{that}
 \ensuremath{is} \ensuremath{enabled} \ensuremath{when} \ensuremath{the}
 \ensuremath{message} \ensuremath{is} \ensuremath{in} \ensuremath{msgs. This
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{simplifies} \ensuremath{the} \ensuremath{spec} \ensuremath{in}
 \ensuremath{the} \ensuremath{following} \ensuremath{ways\.{:}
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{5.0}{0}{}%
 \ensuremath{\.{-} A} \ensuremath{message} \ensuremath{can} \ensuremath{be}
 \ensuremath{broadcast} \ensuremath{to} \ensuremath{multiple}
 \ensuremath{recipients} \ensuremath{by} \ensuremath{just} \ensuremath{adding
}%
\end{cpar}%
\begin{cpar}{0}{T}{F}{5.0}{0}{}%
 \ensuremath{(a} \ensuremath{single} \ensuremath{copy} \ensuremath{of) it}
 \ensuremath{to} \ensuremath{msgs.
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 \ensuremath{\.{-} Never} \ensuremath{removing} \ensuremath{the}
 \ensuremath{message} \ensuremath{automatically} \ensuremath{allows}
 \ensuremath{the} \ensuremath{possibility} \ensuremath{of
}%
\end{cpar}%
\begin{cpar}{0}{T}{F}{5.0}{0}{}%
 \ensuremath{the} \ensuremath{same} \ensuremath{message} \ensuremath{being}
 \ensuremath{received} \ensuremath{twice.
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
 \ensuremath{Since} \ensuremath{we} \ensuremath{are} \ensuremath{considering}
 \ensuremath{only} \ensuremath{safety,\, there} \ensuremath{is}
 \ensuremath{no} \ensuremath{need} \ensuremath{to} \ensuremath{explicitly
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{model} \ensuremath{message} \ensuremath{loss. The}
 \ensuremath{safety} \ensuremath{part} \ensuremath{of} \ensuremath{the}
 \ensuremath{spec} \ensuremath{says} \ensuremath{only} \ensuremath{what
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{messages} \ensuremath{may} \ensuremath{be} \ensuremath{received}
 \ensuremath{and} \ensuremath{does} \ensuremath{not} \ensuremath{assert}
 \ensuremath{that} \ensuremath{any} \ensuremath{message} \ensuremath{actually
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{is} \ensuremath{received. Thus,\, there} \ensuremath{is}
 \ensuremath{no} \ensuremath{difference} \ensuremath{between} \ensuremath{a}
 \ensuremath{lost} \ensuremath{message} \ensuremath{and
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 \ensuremath{one} \ensuremath{that} \ensuremath{is} \ensuremath{never}
 \ensuremath{received.
}%
\end{cpar}%
\end{lcom}%
\@x{ {\VARIABLES} maxBal ,\, maxVBal ,\, maxVal ,\, msgs}%
 \@x{ vars \.{\defeq} {\langle} maxBal ,\, maxVBal ,\, maxVal ,\, msgs
 {\rangle}}%
\begin{lcom}{8.2}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
It\mbox{'}s convenient to name the tuple of all variables in a spec.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The invariant that describes the ``types'' of the variables.
\end{cpar}%
\end{lcom}%
 \@x{ TypeOK \.{\defeq} \.{\land} maxBal\@s{7.43} \.{\in} [ Acceptor
 \.{\rightarrow} Ballot \.{\cup} \{ \.{-} 1 \} ]}%
 \@x{\@s{56.14} \.{\land} maxVBal \.{\in} [ Acceptor \.{\rightarrow} Ballot
 \.{\cup} \{ \.{-} 1 \} ]}%
 \@x{\@s{56.14} \.{\land} maxVal\@s{7.80} \.{\in} [ Acceptor \.{\rightarrow}
 Value \.{\cup} \{ None \} ]}%
\@x{\@s{56.14} \.{\land} msgs \.{\subseteq} Message}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The initial predicate should be obvious from the descriptions of the
 variables given above.
\end{cpar}%
\end{lcom}%
 \@x{ Init \.{\defeq} \.{\land} maxBal\@s{7.43} \.{=} [ a \.{\in} Acceptor
 \.{\mapsto} \.{-} 1 ]}%
 \@x{\@s{35.70} \.{\land} maxVBal \.{=} [ a \.{\in} Acceptor \.{\mapsto} \.{-}
 1 ]}%
 \@x{\@s{35.70} \.{\land} maxVal\@s{7.80} \.{=} [ a \.{\in} Acceptor
 \.{\mapsto} None ]}%
\@x{\@s{35.70} \.{\land} msgs \.{=} \{ \}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
We now define the subactions of the next-state actions. We begin by
 defining an action that will be used in those subactions. The action
 \ensuremath{Send(m)} asserts that message \ensuremath{m} is added to the set
 \ensuremath{msgs}.
\end{cpar}%
\end{lcom}%
\@x{ Send ( m ) \.{\defeq} msgs \.{'} \.{=} msgs \.{\cup} \{ m \}}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The ballot \ensuremath{b} leader can perform actions \ensuremath{Phase1a(b)}
 and \ensuremath{Phase2a(b)}. In
 the \ensuremath{Phase1a(b)} action, it sends to all acceptors a phase
 \ensuremath{1a} message (a
 message \ensuremath{m} with \ensuremath{m.type \.{=} \@w{1a}}) that begins
 ballot \ensuremath{b}. Remember that the
 same process can perform the role of leader for many different ballot
 numbers \ensuremath{b}. In practice, it will stop playing the role of leader
 of
 ballot \ensuremath{b} when it begins a higher-numbered ballot. (Remember the
 definition of [\ensuremath{type \.{\mapsto} \@w{1a}}, \ensuremath{bal
 \.{\mapsto} b}] from the comment preceding the
 definition of \ensuremath{Message}.)
\end{cpar}%
\end{lcom}%
 \@x{ Phase1a ( b ) \.{\defeq} \.{\land} Send ( [ type \.{\mapsto}\@w{1a} ,\,
 bal \.{\mapsto} b ] )}%
 \@x{\@s{69.22} \.{\land} {\UNCHANGED} {\langle} maxBal ,\, maxVBal ,\, maxVal
 {\rangle}}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Note that there is no enabling condition to prevent sending the
 phase \ensuremath{1a} message a second time. Since messages are never removed
 from msg, performing the action a second time leaves msg and all the
 other spec variables unchanged, so it\mbox{'}s a stuttering step. Since
 stuttering steps are always allowed, there\mbox{'}s no reason to try to
 prevent them.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Upon receipt of a ballot \ensuremath{b} phase \ensuremath{1a} message,
 acceptor a can perform a
 \ensuremath{Phase1b(a)} action only if \ensuremath{b \.{>} maxBal[a]}. The
 action sets \ensuremath{maxBal[a]} to
 \ensuremath{b} and sends a phase \ensuremath{1b} message to the leader
 containing the values of
 \ensuremath{maxVBal[a]} and \ensuremath{maxVal[a]}. This action implements
 the
 \ensuremath{IncreaseMaxBal(a,\,b)} action of the \ensuremath{Voting}
 algorithm for \ensuremath{b \.{=} m.bal}.
\end{cpar}%
\end{lcom}%
\@x{ Phase1b ( a ) \.{\defeq}}%
\@x{\@s{8.2} \.{\land} \E\, m \.{\in} msgs \.{:}}%
\@x{\@s{26.53} \.{\land} m . type \.{=}\@w{1a}}%
\@x{\@s{26.53} \.{\land} m . bal \.{>} maxBal [ a ]}%
 \@x{\@s{26.53} \.{\land} maxBal \.{'} \.{=} [ maxBal {\EXCEPT} {\bang} [ a ]
 \.{=} m . bal ]}%
 \@x{\@s{26.53} \.{\land} Send ( [ type \.{\mapsto}\@w{1b} ,\, acc \.{\mapsto}
 a ,\, bal \.{\mapsto} m . bal ,\,}%
 \@x{\@s{70.39} mbal \.{\mapsto} maxVBal [ a ] ,\, mval \.{\mapsto} maxVal [ a
 ] ] )}%
\@x{\@s{8.2} \.{\land} {\UNCHANGED} {\langle} maxVBal ,\, maxVal {\rangle}}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 In the \ensuremath{Phase2a(b,\, v)} action, the ballot \ensuremath{b} leader
 sends a type \ensuremath{\@w{2a}
 } message asking the acceptors to vote for \ensuremath{v} in ballot number
 \ensuremath{b}. The
 enabling conditions of the action--its first two conjuncts--ensure that
 three of the four enabling conditions of action \ensuremath{VoteFor(a,\,
 b,\, v)} in
 module \ensuremath{Voting} will be true when acceptor a receives that
 message.
 Those three enabling conditions are the second through fourth conjuncts
 of that action.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The first conjunct of \ensuremath{Phase2a(b,\, v)} asserts that at most one
 phase \ensuremath{2a
 } message is ever sent for ballot \ensuremath{b}. Since an acceptor will vote
 for a
 value in ballot \ensuremath{b} only when it receives the appropriate phase
 \ensuremath{2a
 } message, the phase \ensuremath{2a} message sent by this action this ensures
 that
 these two enabling conjuncts of \ensuremath{VoteFor(a,\,b,\,v)} will be true
 forever:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{10.0}{0}{}%
\ensuremath{\.{\land} \A\, vt \.{\in} votes[a]} : \ensuremath{vt[1] \.{\neq} b
}%
\end{cpar}%
\begin{cpar}{0}{T}{F}{0}{12.5}{}%
\ensuremath{\.{\land} \A\, c \.{\in} Acceptor \.{\,\backslash\,} \{a\}} :
 \ensuremath{\A\, vt \.{\in} votes[c]} : (\ensuremath{vt[1] \.{=} b})
 \ensuremath{\.{\implies}} (\ensuremath{vt[2] \.{=} v})
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{2}{F}{F}{0}{0}{}%
 The second conjunct of the \ensuremath{Phase2a(b,\, v)} action is the heart
 of the
 \ensuremath{Paxos} consensus algorithm. It\mbox{'}s a bit complicated, but
 I\mbox{'}ve tried a
 number of times to write it in \ensuremath{English}, and it\mbox{'}s much
 easier to
 understand when written in mathematics. The
 \ensuremath{\.{\LET}}/\ensuremath{\.{\IN}} construct locally
 defines \ensuremath{Q1} to be the set of phase \ensuremath{1b} messages sent
 in ballot number \ensuremath{b
 } by acceptors in quorum \ensuremath{Q}; and it defines \ensuremath{Q1bv} to
 be the subset of those
 messages indicating that the sender had voted in some ballot (which
 must have been numbered less than \ensuremath{b}). You should study the
 \ensuremath{\.{\IN}} clause
 to convince yourself that it equals \ensuremath{ShowsSafeAt(Q,\, b,\, v)},
 defined in
 module \ensuremath{Voting}, using the values of \ensuremath{maxBal[a]},
 \ensuremath{maxVBal[a]}, and \ensuremath{maxVal[a]
 a} sent in its phase \ensuremath{1b} message to describe what votes it had
 cast
 when it sent that message. Moreover, since \ensuremath{a} will no longer
 cast any
 votes in ballots numbered less than \ensuremath{b}, the \ensuremath{\.{\IN}}
 clause implies that
 \ensuremath{ShowsSafeAt(Q,\, b,\, v)} is still true and will remain true
 forever.
 Hence, this conjunct of \ensuremath{Phase2a(b,\, v)} checks the enabling
 condition
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{\.{\land} \E\, Q \.{\in} Quorum} : \ensuremath{ShowsSafeAt(Q,\,
 b,\, v)
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 of module \ensuremath{Voting}\mbox{'}s \ensuremath{VoteFor(a,\, b,\, v)}
 action.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The type \ensuremath{\@w{2a}} message sent by this action therefore tells
 every
 acceptor \ensuremath{a} that, when it receives the message, all the enabling
 conditions of \ensuremath{VoteFor(a,\, b,\, v)} but the first,
 \ensuremath{maxBal[a] \.{\leq} b}, are
 satisfied.
\end{cpar}%
\end{lcom}%
\@x{ Phase2a ( b ,\, v ) \.{\defeq}}%
 \@x{\@s{8.2} \.{\land} {\lnot} \E\, m \.{\in} msgs\@s{7.89} \.{:} m . type
 \.{=}\@w{2a} \.{\land} m . bal \.{=} b}%
\@x{\@s{8.2} \.{\land} \E\, Q \.{\in} Quorum \.{:}}%
 \@x{\@s{26.53} \.{\LET} Q1b \.{\defeq} \{ m \.{\in} msgs\@s{6.20} \.{:}
 \.{\land} m . type \.{=}\@w{1b}}%
\@x{\@s{148.25} \.{\land} m . acc \.{\in} Q}%
\@x{\@s{148.25} \.{\land} m . bal\@s{1.57} \.{=} b \}}%
\@x{\@s{51.03} Q1bv \.{\defeq} \{ m \.{\in} Q1b \.{:} m . mbal \.{\geq} 0 \}}%
 \@x{\@s{26.53} \.{\IN}\@s{4.09} \.{\land} \A\, a \.{\in} Q \.{:} \E\, m
 \.{\in} Q1b \.{:} m . acc \.{=} a}%
\@x{\@s{51.03} \.{\land} \.{\lor} Q1bv \.{=} \{ \}}%
\@x{\@s{62.14} \.{\lor} \E\, m\@s{7.71} \.{\in} Q1bv \.{:}}%
\@x{\@s{81.45} \.{\land} m . mval \.{=} v}%
 \@x{\@s{81.45} \.{\land} \A\, mm \.{\in} Q1bv \.{:} m . mbal \.{\geq} mm .
 mbal}%
 \@x{\@s{8.2} \.{\land} Send ( [ type \.{\mapsto}\@w{2a} ,\, bal \.{\mapsto} b
 ,\, val \.{\mapsto} v ] )}%
 \@x{\@s{8.2} \.{\land} {\UNCHANGED} {\langle} maxBal ,\, maxVBal ,\, maxVal
 {\rangle}}%
\@pvspace{16.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The \ensuremath{Phase2b(a)} action describes what acceptor \ensuremath{a}
 does when it receives
 a phase \ensuremath{2a} message \ensuremath{m}, which is sent by the leader
 of ballot \ensuremath{m.bal
 } asking acceptors to vote for \ensuremath{m.val} in that ballot. Acceptor
 \ensuremath{a} acts
 on that request, voting for \ensuremath{m.val} in ballot number
 \ensuremath{m.bal}, iff \ensuremath{m.bal \.{\geq}
 maxBal[a]}, which means that \ensuremath{a} has not participated in any
 ballot
 numbered greater than \ensuremath{m.bal}. Thus, this enabling condition of
 the
 \ensuremath{Phase2b(a)} action together with the receipt of the phase
 \ensuremath{2a} message \ensuremath{m
 } implies that the \ensuremath{VoteFor(a,\, m.bal,\, m.val)} action of module
 \ensuremath{Voting} is
 enabled and can be executed. The \ensuremath{Phase2b(a)} message updates
 \ensuremath{maxBal[a]},
 \ensuremath{maxVBal[a]}, and \ensuremath{maxVal[a]} so their values mean
 what they were claimed
 to mean in the comments preceding the variable declarations.
\end{cpar}%
\end{lcom}%
\@x{ Phase2b ( a ) \.{\defeq}}%
\@x{\@s{8.2} \E\, m \.{\in} msgs \.{:}}%
\@x{\@s{19.52} \.{\land} m . type \.{=}\@w{2a}}%
\@x{\@s{19.52} \.{\land} m . bal \.{\geq} maxBal [ a ]}%
 \@x{\@s{19.52} \.{\land} maxBal \.{'} \.{=} [ maxBal {\EXCEPT} {\bang} [ a ]
 \.{=} m . bal ]}%
 \@x{\@s{19.52} \.{\land} maxVBal \.{'} \.{=} [ maxVBal {\EXCEPT} {\bang} [ a
 ] \.{=} m . bal ]}%
 \@x{\@s{19.52} \.{\land} maxVal \.{'} \.{=} [ maxVal {\EXCEPT} {\bang} [ a ]
 \.{=} m . val ]}%
 \@x{\@s{19.52} \.{\land} Send ( [ type \.{\mapsto}\@w{2b} ,\, acc \.{\mapsto}
 a ,\,}%
\@x{\@s{56.51} bal \.{\mapsto} m . bal ,\, val \.{\mapsto} m . val ] )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The definitions of \ensuremath{Next} and \ensuremath{Spec} are what we expect
 them to be.
\end{cpar}%
\end{lcom}%
 \@x{ Next \.{\defeq} \.{\lor} \E\, b\@s{0.64} \.{\in} Ballot \.{:} \.{\lor}
 Phase1a ( b )}%
\@x{\@s{112.86} \.{\lor} \E\, v \.{\in} Value \.{:} Phase2a ( b ,\, v )}%
 \@x{\@s{39.83} \.{\lor} \E\, a \.{\in} Acceptor \.{:} Phase1b ( a ) \.{\lor}
 Phase2b ( a )}%
\@pvspace{8.0pt}%
\@x{ Spec\@s{1.46} \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ vars}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We define \ensuremath{votes} to be the function such that
 \ensuremath{votes[a]} is the set of
 pairs \ensuremath{{\langle}b,\, v{\rangle}} such that acceptor
 \ensuremath{a} has voted for \ensuremath{v} in ballot number
 \ensuremath{b} by sending executing the \ensuremath{Phase2b(a)} action to
 send the appropriate
 type \ensuremath{\@w{2b}} message. The \ensuremath{Paxos} consensus
 algorithm implements the \ensuremath{Voting
 } algorithm by implementing the variable \ensuremath{votes} of module
 \ensuremath{Voting} with
 the expression \ensuremath{votes} of the current module, and implementing the
 variable \ensuremath{maxBal} of module \ensuremath{Voting} with the variable
 of the same name of
 the current module.
\end{cpar}%
\end{lcom}%
\@x{ votes \.{\defeq}}%
\@x{\@s{8.2} [ a \.{\in} Acceptor \.{\mapsto}}%
 \@x{\@s{20.95} \{ {\langle} m . bal ,\, m . val {\rangle} \.{:} m \.{\in} \{
 mm \.{\in} msgs \.{:} \.{\land} mm . type \.{=}\@w{2b}}%
\@x{\@s{185.55} \.{\land} mm . acc \.{=} a \} \} ]}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The following \ensuremath{{\INSTANCE}} statement omits the redundant clause
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{{\WITH}} \ensuremath{votes \.{\leftarrow} votes},
 \ensuremath{maxBal \.{\leftarrow} maxBal},
\end{cpar}%
\begin{cpar}{0}{T}{F}{12.5}{0}{}%
 \ensuremath{Value \.{\leftarrow} Value}, \ensuremath{Acceptor \.{\leftarrow}
 Acceptor}, \ensuremath{Quorum \.{\leftarrow} Quorum
}%
\end{cpar}%
\end{lcom}%
\@x{ V \.{\defeq} {\INSTANCE} Voting}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The inductive invariant \ensuremath{Inv} explains why the \ensuremath{Paxos}
 consensus algorithm
 implements the \ensuremath{Voting} algorithm. It is defined after the
 \ensuremath{{\INSTANCE}
 } statement because it uses the operator \ensuremath{V{\bang}ShowsSafeAt}
 imported by that
 statement.
\end{cpar}%
\end{lcom}%
\@x{ Inv \.{\defeq}}%
\@x{\@s{4.1} \.{\land} TypeOK}%
 \@x{\@s{4.1} \.{\land} \A\, a\@s{3.06} \.{\in} Acceptor \.{:} maxBal [ a ]
 \.{\geq} maxVBal [ a ]}%
 \@x{\@s{4.1} \.{\land} \A\, a\@s{3.06} \.{\in} Acceptor \.{:} {\IF} maxVBal [
 a ] \.{=} \.{-} 1}%
\@x{\@s{99.78} \.{\THEN} maxVal [ a ] \.{=} None}%
 \@x{\@s{99.78} \.{\ELSE} {\langle} maxVBal [ a ] ,\, maxVal [ a ] {\rangle}
 \.{\in} votes [ a ]}%
\@x{\@s{4.1} \.{\land} \A\, m \.{\in} msgs \.{:}}%
 \@x{\@s{22.43} \.{\land} ( m . type \.{=}\@w{1b} ) \.{\implies} \.{\land}
 maxBal [ m . acc ] \.{\geq} m . bal}%
\@x{\@s{120.22} \.{\land} ( m . mbal \.{\geq} 0 ) \.{\implies}}%
 \@x{\@s{135.22} {\langle} m . mbal ,\, m . mval {\rangle} \.{\in} votes [ m .
 acc ]}%
 \@x{\@s{22.43} \.{\land} ( m . type \.{=}\@w{2a} )\@s{0.36} \.{\implies}
 \.{\land} \E\, Q \.{\in} Quorum \.{:}}%
\@x{\@s{138.56} V {\bang} ShowsSafeAt ( Q ,\, m . bal ,\, m . val )}%
 \@x{\@s{120.22} \.{\land} \A\, mm \.{\in} msgs \.{:} \.{\land} mm . type
 \.{=}\@w{2a}}%
\@x{\@s{199.12} \.{\land} mm . bal\@s{4.95} \.{=} m . bal}%
\@x{\@s{199.12} \.{\implies} mm . val \.{=} m . val}%
 \@x{\@s{22.43} \.{\land} ( m . type \.{=}\@w{2b} ) \.{\implies} \.{\land}
 maxVBal [ m . acc ] \.{\geq} m . bal}%
 \@x{\@s{120.22} \.{\land} \E\, mm \.{\in} msgs \.{:} \.{\land} mm . type
 \.{=}\@w{2a}}%
\@x{\@s{199.12} \.{\land} mm . bal\@s{5.34} \.{=} m . bal}%
\@x{\@s{199.12} \.{\land} mm . val\@s{4.82} \.{=} m . val}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The following two theorems assert that \ensuremath{Inv} is an invariant of
 the \ensuremath{Paxos} cconsensus algorithm and that this algorithm
 implements
 the \ensuremath{Voting} algorithm with the declared variables and constants
 of that algorithm implemented by the correspondingly-named expressions
 in the current module.
\end{cpar}%
\end{lcom}%
 \@x{ {\THEOREM} Invariance\@s{4.1} \.{\defeq}\@s{4.1} Spec \.{\implies}
 {\Box} Inv}%
\@pvspace{8.0pt}%
 \@x{ {\THEOREM} Implementation\@s{4.1} \.{\defeq}\@s{4.1} Spec \.{\implies} V
 {\bang} Spec}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The \ensuremath{{\ASSUME}} statement of this module trivial implies trivially
 implies
 the instantiated version of the \ensuremath{{\ASSUME}} statement of module
 \ensuremath{Voting}.
 (Because the \ensuremath{{\INSTANCE}} statement substitutes the constants of
 the
 current module for the constants of the same name in module
 \ensuremath{Voting}, the
 imported assumption is the same as the assumption of the current
 module.) Hence, this theorem imported from module \ensuremath{Voting} is
 true in the
 current module
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
 \ensuremath{{\THEOREM}} \ensuremath{V{\bang}Implementation \.{\defeq}
 V{\bang}Spec \.{\implies} V{\bang}C{\bang}Spec
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 Theorems \ensuremath{Implementation} and \ensuremath{V{\bang}Implementation}
 imply
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
\ensuremath{{\THEOREM}} \ensuremath{Spec \.{\implies} V{\bang}C{\bang}Spec
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 This theorem asserts that the \ensuremath{Paxos} consensus algorithm
 implements the
 Consensus specification by substituting for the variable \ensuremath{chosen}
 of
 the \ensuremath{Consensus} specification the value
 \ensuremath{V{\bang}chosen} of the current module.
 The expression \ensuremath{V{\bang}chosen} is obtained by substituting the
 expression
 \ensuremath{votes} of the current module for the variable \ensuremath{votes}
 of module \ensuremath{Voting
} in the expression \ensuremath{chosen} of module \ensuremath{Voting}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
In other words, as we should expect, ``implements'' is a transitive
 relation--under a suitable understanding of what transitivity means in
 this situation.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This current module is distributed with two models, \ensuremath{TinyModel} and
 \ensuremath{SmallModel}. \ensuremath{SmallModel} is the same as the model by
 that name for the
 Voting specification. \ensuremath{TinyModel} is the same except it defines
 \ensuremath{Ballot
 } to contain only two elements. Run \ensuremath{TLC} on these models. You
 should
 find that it takes a couple of seconds to run \ensuremath{TinyModel} and two
 or
 three minutes to run \ensuremath{SmallModel}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Next, try the same thing you did with the \ensuremath{Voting} algorithm:
 Modify the
 models so the assumption that any pair of quorums has an element in
 common is no longer true. (Again, it\mbox{'}s best to modify clones of the
 models.) This time, running \ensuremath{TLC} will not find an error. The
 correctness of theorems \ensuremath{Invariance} and
 \ensuremath{Implementation} does not depend
 on that assumption. The \ensuremath{Paxos} consensus algorithm still
 correctly
 implements the \ensuremath{Voting} algorithm; but the \ensuremath{Voting}
 algorithm is incorrect
 if the assumption does not hold.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Now go back to the original \ensuremath{SmallModel}, in which the quorum
 assumption
 holds. The sets \ensuremath{Acceptor} and \ensuremath{Value} are symmetry
 sets for the spec.
 (See the ``Model Values and Symmetry'' help page to find out what that
 means.) Try editing the values substituted for \ensuremath{Acceptor} and/or
 \ensuremath{Value} by
 selecting the ``Symmetry set'' option and comparing the number of
 reachable states \ensuremath{TLC} found and the time it took. (Remember to
 use
 cloned models.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 When you have other things to do while \ensuremath{TLC} is running, try
 increasing
 the size of the model a very little bit at a time and see how the
 running time increases. You\mbox{'}ll find that it increases exponentially
 with the numbers of acceptors, values, and ballots.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Fortunately, exhaustively checking a small model is very effective at
 finding errors. Since the \ensuremath{Paxos} consensus algorithm has been
 proved
 correct, and that proof has been read by many people, I\mbox{'}m sure that
 the
 basic algorithm is correct. Checking this spec on \ensuremath{SmallModel}
 makes me
 quite confident that there are no ``coding errors'' in this TLA+
 specification of the algorithm.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 For checking safety properties, \ensuremath{TLC} can obtain close to linear
 speedup
 using dozens of processors. After designing a new distributed
 algorithm, you will have plenty of time to run \ensuremath{TLC} while the
 algorithm
 is being implemented and the implementation tested. Use that time to
 run it for as long as you can on the largest \ensuremath{machine(s)} that
 you can.
 Testing the implementation is unlikely to find subtle errors in the
 algorithm.
\end{cpar}%
\end{lcom}%
\@x{}\bottombar\@xx{}%
\end{document}
