\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} Voting}\moduleRightDash\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This is a high-level algorithm in which a set of processes
 cooperatively choose a value. It is a high-level abstraction of the
 Paxos consensus algorithm. Although I don\mbox{'}t remember exactly what went
 through my mind when I invented/discovered that algorithm, I\mbox{'}m pretty
 sure that this spec formalizes the way I first thought of the
 algorithm. It would have been very hard to find this algorithm had my
 mind been distracted by the irrelevant details introduced by having the
 processes communicate by messages.
\end{cpar}%
\end{lcom}%
\@x{ {\EXTENDS} Integers}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
For historical reasons, the processes that choose a value are called
 acceptors. We now declare the set \ensuremath{Value} of values, the set
 Acceptors
 of acceptors, and another set \ensuremath{Quorum} that is a set of sets of
 acceptors
 called quorums.
\end{cpar}%
\end{lcom}%
\@x{ {\CONSTANTS} Value ,\, Acceptor ,\, Quorum}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The following assumption asserts that \ensuremath{Quorum} is a set of subsets
 of the
 set \ensuremath{Acceptor}, and that any two elements of \ensuremath{Quorum}
 have at least one
 element (an acceptor) in common. Think of a quorum as a set consisting
 of a majority (more than half) of the acceptors.
\end{cpar}%
\end{lcom}%
 \@x{ {\ASSUME} \.{\land} \A\, Q \.{\in} Quorum \.{:} Q \.{\subseteq}
 Acceptor}%
 \@x{\@s{38.24} \.{\land} \A\, Q1 ,\, Q2 \.{\in} Quorum \.{:} Q1 \.{\cap} Q2
 \.{\neq} \{ \}}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Ballot is a set of ``ballot numbers''. For simplicity, we let it be the
 set of natural numbers. However, we write \ensuremath{Ballot} for that set to
 distinguish ballots from natural numbers used for other purposes.
\end{cpar}%
\end{lcom}%
\@x{ Ballot \.{\defeq} Nat}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The algorithm works by having acceptors cast votes in numbered ballots.
 Each acceptor can cast one or more votes, where each vote cast by an
 acceptor has the form \ensuremath{{\langle}b,\, v{\rangle}} indicating that
 the acceptor has voted
 for value \ensuremath{v} in ballot number \ensuremath{b}. A value is chosen
 if a quorum of
 acceptors have voted for it in the same ballot.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 We now declare the algorithm\mbox{'}s variables \mbox{'}votes\mbox{'} and
 \mbox{'}maxBal\mbox{'}. For
 each acceptor a, he value of \ensuremath{votes[a]} is the set of votes cast
 by \ensuremath{a} ;
 and \ensuremath{maxBal[a]} is an integer such that \ensuremath{a} will never
 cast any further
 vote in a ballot numbered less than \ensuremath{maxBal[a]}.
\end{cpar}%
\end{lcom}%
\@x{ {\VARIABLES} votes ,\, maxBal}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{TypeOK} asserts the ``types'' of the two variables. They are both
 functions with domain \ensuremath{Acceptor} (arrays indexed by acceptors).
 For any
 acceptor a, the value of \ensuremath{votes[a]} a set of
 \ensuremath{{\langle}ballot,\, value{\rangle}} pairs; and
 the value of \ensuremath{maxBal[a]} is either a ballot number or
 \ensuremath{\.{-}1}.
\end{cpar}%
\end{lcom}%
\@x{ TypeOK \.{\defeq}}%
 \@x{\@s{12.29} \.{\land} votes\@s{11.12} \.{\in} [ Acceptor \.{\rightarrow}
 {\SUBSET} ( Ballot \.{\times} Value ) ]}%
 \@x{\@s{12.29} \.{\land} maxBal \.{\in} [ Acceptor \.{\rightarrow} Ballot
 \.{\cup} \{ \.{-} 1 \} ]}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Next comes a sequence of definitions of concepts used to explain the
 algorithm.
\end{cpar}%
\end{lcom}%
 \@x{ VotedFor ( a ,\, b ,\, v ) \.{\defeq} {\langle} b ,\, v {\rangle}
 \.{\in} votes [ a ]}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
True iff (if and only if) acceptor a has votted for value \ensuremath{v} in
 ballot number \ensuremath{b}.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\@x{ ChosenAt ( b ,\, v ) \.{\defeq}}%
 \@x{\@s{12.29} \E\, Q \.{\in} Quorum \.{:} \A\, a \.{\in} Q \.{:} VotedFor (
 a ,\, b ,\, v )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 True iff a quorum of acceptors have all voted for value \ensuremath{v} in
 ballot
 number \ensuremath{b}.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
 \@x{ chosen \.{\defeq} \{ v \.{\in} Value \.{:} \E\, b \.{\in} Ballot \.{:}
 ChosenAt ( b ,\, v ) \}}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 Defines \ensuremath{chosen} to be the set of all values \ensuremath{v} for
 which \ensuremath{ChosenAt(b,\,
 v)} is true for some ballot number \ensuremath{b}. This is the definition of
 what
 it means for a value to be chosen under which the \ensuremath{Voting}
 algorithm
 implements the \ensuremath{Consensus} specification.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
 \@x{ DidNotVoteAt ( a ,\, b ) \.{\defeq} \A\, v \.{\in} Value \.{:} {\lnot}
 VotedFor ( a ,\, b ,\, v )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
True iff acceptor \ensuremath{a} has not voted in ballot number .
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\@x{ CannotVoteAt ( a ,\, b ) \.{\defeq} \.{\land} maxBal [ a ] \.{>} b}%
\@x{\@s{106.97} \.{\land} DidNotVoteAt ( a ,\, b )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The algorithm will not allow acceptor \ensuremath{a} to vote in ballot number
 \ensuremath{b
 } if \ensuremath{maxBal[a] \.{>} b}. Hence, \ensuremath{CannotVoteAt(a,\, b)}
 implies that \ensuremath{a} has
 not and never will vote in ballot number \ensuremath{b}.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\@x{ NoneOtherChoosableAt ( b ,\, v ) \.{\defeq}}%
\@x{\@s{12.29} \E\, Q \.{\in} Quorum \.{:}}%
 \@x{\@s{19.52} \A\, a \.{\in} Q \.{:} VotedFor ( a ,\, b ,\, v ) \.{\lor}
 CannotVoteAt ( a ,\, b )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This is true iff there is some quorum \ensuremath{Q} such that each acceptor
 \ensuremath{a
 } in \ensuremath{Q} either has voted for \ensuremath{v} in ballot
 \ensuremath{b} or has not and never will
 vote in ballot \ensuremath{b}. It implies that no value other than
 \ensuremath{v} has been or
 ever can be chosen at ballot \ensuremath{b}. This is because for a value w
 to be
 chosen at ballot \ensuremath{b}, all the acceptors in some quorum
 \ensuremath{R} must have
 voted for w in ballot \ensuremath{b}. But any two ballots have an acceptor in
 common, so some acceptor a in \ensuremath{R} that voted for w is in
 \ensuremath{Q}, and an
 acceptor in \ensuremath{Q} can only have voted for \ensuremath{v}, so w must
 equal \ensuremath{v}.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
 \@x{ SafeAt ( b ,\, v ) \.{\defeq} \A\, c \.{\in} 0 \.{\dotdot} ( b \.{-} 1 )
 \.{:} NoneOtherChoosableAt ( c ,\, v )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
True iff no value other than \ensuremath{v} has been or ever will be chosen in
 any ballot numbered less than \ensuremath{b}. We read
 \ensuremath{SafeAt(b,\, v)} as ``\ensuremath{v} is safe
 at \ensuremath{b}''.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This theorem asserts that every value is safe at ballot 0.
\end{cpar}%
\end{lcom}%
 \@x{ {\THEOREM}\@s{4.1} AllSafeAtZero\@s{4.1} \.{\defeq}\@s{4.1} \A\, v
 \.{\in} Value \.{:} SafeAt ( 0 ,\, v )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The following theorem asserts that \ensuremath{NoneOtherChoosableAt} means
 what it\mbox{'}s
 name implies. The comments after its definition essentially contain a
 proof of this theorem.
\end{cpar}%
\end{lcom}%
\@x{ {\THEOREM}\@s{4.1} ChoosableThm\@s{4.1} \.{\defeq}}%
\@x{\@s{63.22} \A\, b \.{\in} Ballot ,\, v \.{\in} Value \.{:}}%
 \@x{\@s{70.44} ChosenAt ( b ,\, v ) \.{\implies} NoneOtherChoosableAt ( b ,\,
 v )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Now comes the definition of the inductive invariant \ensuremath{Inv} that
 essentially explains why the algorithm is correct.
\end{cpar}%
\end{lcom}%
\@x{ OneValuePerBallot \.{\defeq}}%
 \@x{\@s{16.4} \A\, a1 ,\, a2 \.{\in} Acceptor ,\, b \.{\in} Ballot ,\, v1 ,\,
 v2 \.{\in} Value \.{:}}%
 \@x{\@s{23.62} VotedFor ( a1 ,\, b ,\, v1 ) \.{\land} VotedFor ( a2 ,\, b ,\,
 v2 ) \.{\implies} ( v1 \.{=} v2 )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This formula asserts that if any acceptors \ensuremath{a1} and
 \ensuremath{a2} have voted in a
 ballot \ensuremath{b}, then they voted for the same value in ballot
 \ensuremath{b}. For
 \ensuremath{a1\.{=}a2}, this implies that an acceptor can vote for at most
 one value
 in any ballot.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
 \@x{ VotesSafe \.{\defeq} \A\, a \.{\in} Acceptor ,\, b \.{\in} Ballot ,\, v
 \.{\in} Value \.{:}}%
\@x{\@s{73.15} VotedFor ( a ,\, b ,\, v ) \.{\implies} SafeAt ( b ,\, v )}%
\begin{lcom}{12.29}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This formula asserts that an acceptors can have voted in a ballot
 \ensuremath{b
} only if that value is safe at \ensuremath{b}.
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The algorithm is essentially derived by ensuring that this formula
 \ensuremath{Inv
} is always true.
\end{cpar}%
\end{lcom}%
\@x{ Inv \.{\defeq} TypeOK \.{\land} VotesSafe \.{\land} OneValuePerBallot}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This definition is used in the defining the algorithm. You should
 study it and make sure you understand what it says.
\end{cpar}%
\end{lcom}%
\@x{ ShowsSafeAt ( Q ,\, b ,\, v ) \.{\defeq}}%
\@x{\@s{8.2} \.{\land} \A\, a \.{\in} Q \.{:} maxBal [ a ] \.{\geq} b}%
 \@x{\@s{8.2} \.{\land} \E\, c\@s{0.71} \.{\in} \.{-} 1 \.{\dotdot} ( b \.{-}
 1 ) \.{:}}%
 \@x{\@s{23.41} \.{\land} ( c \.{\neq} \.{-} 1 ) \.{\implies} \E\, a \.{\in} Q
 \.{:} VotedFor ( a ,\, c ,\, v )}%
 \@x{\@s{23.41} \.{\land} \A\, d \.{\in} ( c \.{+} 1 ) \.{\dotdot} ( b \.{-} 1
 ) ,\, a \.{\in} Q \.{:} DidNotVoteAt ( a ,\, d )}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
This is the theorem that\mbox{'}s at the heart of the algorithm. It shows
 that if the algorithm has maintained the invariance of \ensuremath{Inv},
 then the
 truth of \ensuremath{ShowsSafeAt(Q,\, b,\, v)} for some quorum
 \ensuremath{Q} ensures that \ensuremath{v} is safe
 at \ensuremath{b}, so the algorithm can let an acceptor vote for
 \ensuremath{v} in ballot \ensuremath{b
} knowing \ensuremath{VotesSafe} will be preserved.
\end{cpar}%
\end{lcom}%
\@x{ {\THEOREM} ShowsSafety\@s{4.1} \.{\defeq}}%
 \@x{\@s{55.02} Inv\@s{4.1} \.{\implies}\@s{4.1} \A\, Q \.{\in} Quorum ,\, b
 \.{\in} Ballot ,\, v \.{\in} Value \.{:}}%
 \@x{\@s{102.13} ShowsSafeAt ( Q ,\, b ,\, v ) \.{\implies} SafeAt ( b ,\, v
 )}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Finally, we get to the definition of the algorithm. The initial
 predicate is obvious.
\end{cpar}%
\end{lcom}%
 \@x{ Init \.{\defeq} \.{\land} votes\@s{11.12} \.{=} [ a \.{\in} Acceptor
 \.{\mapsto} \{ \} ]}%
 \@x{\@s{35.70} \.{\land} maxBal \.{=} [ a \.{\in} Acceptor \.{\mapsto} \.{-}
 1 ]}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
An acceptor \ensuremath{a} can increase \ensuremath{maxBal[a]} at any time.
\end{cpar}%
\end{lcom}%
\@x{ IncreaseMaxBal ( a ,\, b ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} b \.{>} maxBal [ a ]}%
 \@x{\@s{16.4} \.{\land} maxBal \.{'} \.{=} [ maxBal {\EXCEPT} {\bang} [ a ]
 \.{=} b ]}%
\@x{\@s{16.4} \.{\land} {\UNCHANGED} votes}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The heart of the algorithm is the action in which an acceptor \ensuremath{a}
 votes
 for a value \ensuremath{v} in ballot number \ensuremath{b}. The enabling
 condition contains the
 following conjuncts, which ensure that the invariance of \ensuremath{Inv} is
 maintained.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
\ensuremath{\.{-} a} cannot vote in a ballot numbered less than \ensuremath{b
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{-} a} cannot already have voted in ballot number \ensuremath{b
}%
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{T}{0}{2.5}{%
-}%
No other acceptor can have voted for a value other than \ensuremath{v
} in ballot \ensuremath{b}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 - Uses Theorem \ensuremath{ShowsSafety} to ensure that \ensuremath{v} is safe
 at \ensuremath{b}.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
 In TLA+, a tuple \ensuremath{t} is a function (array) whose first element is
 \ensuremath{t[1]},
 whose second element if \ensuremath{t[2]}, and so on. Thus, a vote
 \ensuremath{vt} is the pair
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{{\langle}vt[1],\, vt[2]{\rangle}
}%
\end{cpar}%
\end{lcom}%
\@x{ VoteFor ( a ,\, b ,\, v ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land}\@s{8.35} maxBal [ a ] \.{\leq} b}%
 \@x{\@s{16.4} \.{\land}\@s{8.35} \A\, vt \.{\in} votes [ a ] \.{:} vt [ 1 ]
 \.{\neq} b}%
 \@x{\@s{16.4} \.{\land}\@s{8.35} \A\, c \.{\in} Acceptor \.{\,\backslash\,}
 \{ a \} \.{:}}%
 \@x{\@s{44.06} \A\, vt \.{\in} votes [ c ] \.{:} ( vt [ 1 ] \.{=} b )
 \.{\implies} ( vt [ 2 ] \.{=} v )}%
 \@x{\@s{16.4} \.{\land}\@s{8.35} \E\, Q \.{\in} Quorum \.{:} ShowsSafeAt ( Q
 ,\, b ,\, v )}%
 \@x{\@s{16.4} \.{\land}\@s{8.35} votes \.{'}\@s{11.12} \.{=} [ votes
 {\EXCEPT} {\bang} [ a ] \.{=} votes [ a ] \.{\cup} \{ {\langle} b ,\, v
 {\rangle} \} ]}%
 \@x{\@s{16.4} \.{\land}\@s{8.35} maxBal \.{'} \.{=} [ maxBal {\EXCEPT}
 {\bang} [ a ] \.{=} b ]}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The rest of the spec is straightforward.
\end{cpar}%
\end{lcom}%
 \@x{ Next\@s{4.1} \.{\defeq}\@s{4.1} \E\, a \.{\in} Acceptor ,\, b \.{\in}
 Ballot \.{:}}%
\@x{\@s{55.25} \.{\lor} IncreaseMaxBal ( a ,\, b )}%
\@x{\@s{55.25} \.{\lor} \E\, v \.{\in} Value \.{:} VoteFor ( a ,\, b ,\, v )}%
\@pvspace{8.0pt}%
 \@x{ Spec \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ {\langle} votes ,\,
 maxBal {\rangle}}}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This theorem asserts that \ensuremath{Inv} is an invariant of the algorithm.
 The
 high-level steps in its proof are given.
\end{cpar}%
\end{lcom}%
 \@x{ {\THEOREM}\@s{4.1} Invariance\@s{4.1} \.{\defeq}\@s{4.1} Spec
 \.{\implies} {\Box} Inv}%
\@x{\@pfstepnum{1}{1.}\  Init \.{\implies} Inv}%
\@pvspace{8.0pt}%
 \@x{\@pfstepnum{1}{2.}\  Inv \.{\land} [ Next ]_{ {\langle} votes ,\, maxBal
 {\rangle}} \.{\implies} Inv \.{'}}%
\@pvspace{8.0pt}%
\@x{\@pfstepnum{1}{3.}\  {\QED}}%
\@x{\@s{8.2} {\BY}\@pfstepnum{1}{1} ,\,\@pfstepnum{1}{2}\  {\DEF} Spec}%
\@x{}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This \ensuremath{{\INSTANCE}} statement imports definitions from module
 \ensuremath{Consensus} into
 the current module. All definition in module \ensuremath{Consensus} can be
 expanded
 to definitions containing only TLA+ primitives and the declared names
 Value and chosen. To import a definition from \ensuremath{Consensus} into the
 current module, we have to say what expressions from the current module
 are substituted for \ensuremath{Value} and chosen. The
 \ensuremath{{\INSTANCE}} statement says that
 expressions of the same name are substituted for them. (Because of
 this, the \ensuremath{{\WITH}} statement is redundant.) Note that in both
 modules,
 Value is just a declared constant. However, in the current module,
 \ensuremath{chosen} is an expression defined in terms of the variables votes
 and
 \ensuremath{maxBal} while it is a variable in module consensus. The
 ``\ensuremath{C{\bang} \.{\defeq}}'' in the
 statement means that defined identifiers are imported with
 ``\ensuremath{C{\bang}}''
 prepended to their names. Thus \ensuremath{Spec} of module
 \ensuremath{Consensus} is imported,
 with these substitutions, as \ensuremath{C{\bang}Spec}.
\end{cpar}%
\end{lcom}%
\@x{ C \.{\defeq} {\INSTANCE} Consensus}%
 \@x{\@s{39.79} {\WITH}\@s{4.1} Value \.{\leftarrow} Value ,\,\@s{4.1} chosen
 \.{\leftarrow} chosen}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 The following theorem asserts that the \ensuremath{Voting} algorithm
 implements the
 Consensus specification, where the expression \ensuremath{chosen} of the
 current
 module implements the variable \ensuremath{chosen} of
 \ensuremath{Consensus}. The high-level
 steps of the the proof are also given.
\end{cpar}%
\end{lcom}%
 \@x{ {\THEOREM}\@s{4.1} Implementation\@s{4.1} \.{\defeq}\@s{4.1}
 Spec\@s{4.1} \.{\implies} C {\bang} Spec}%
\@x{\@pfstepnum{1}{1.}\  Init \.{\implies} C {\bang} Init}%
\@pvspace{8.0pt}%
 \@x{\@pfstepnum{1}{2.}\  Inv \.{\land} Inv \.{'} \.{\land} [ Next ]_{
 {\langle} votes ,\, maxBal {\rangle}}\@s{4.1} \.{\implies} [ C {\bang} Next
 ]_{ chosen}}%
\@pvspace{8.0pt}%
\@x{\@pfstepnum{1}{3.}\  {\QED}}%
 \@x{\@s{8.2} {\BY}\@pfstepnum{1}{1} ,\,\@pfstepnum{1}{2} ,\, Invariance
 {\DEF} Spec ,\, C {\bang} Spec}%
\@pvspace{8.0pt}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
 This \ensuremath{Voting} specification comes with a \ensuremath{TLC} model
 named \ensuremath{SmallModel}.
 That model tells \ensuremath{TLC} that \ensuremath{Spec} is the
 specification, that \ensuremath{Acceptor} and
 Values should equal sets of model values with 3 acceptors and 2 values
 and \ensuremath{Quorums} should equal the indicated set of values, and that
 it
 should check theorems \ensuremath{Invariance} and
 \ensuremath{Implementation}. Observe that you
 can\mbox{'}t tell \ensuremath{TLC} simply to check those theorems; you have
 to tell \ensuremath{TLC} to
 check the properties the theorems assert that \ensuremath{Spec} satisfies.
 (Instead
 of telling \ensuremath{TLC} that \ensuremath{Inv} should be an invariant,
 you can tell it that
 the spec should satisfy the temporal property \ensuremath{{\Box}Inv}.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Even though the constants are finite sets, the spec has infinitely many
 reachable sets because a ballot number can be any element of the set
 \ensuremath{Nat} of natural numbers. The model modifies the spec so it has a
 finite
 set of reachable states by using a definition override (on the
 \ensuremath{Spec
 } Options page) to redefine \ensuremath{Ballot} to equal
 \ensuremath{0\.{\dotdot}2}. (Alternatively, we
 could override the definition of \ensuremath{Nat} to equal
 \ensuremath{0\.{\dotdot}2}.)
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Run \ensuremath{TLC} on the model. It should just take a couple of seconds.
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
After doing that, show why the assumption that any pair of quorums has
 an element in common is necessary by modifying the model so that
 assumption doesn\mbox{'}t hold. (It\mbox{'}s best to clone
 \ensuremath{SmallModel} and modify the
 clone.) Since \ensuremath{TLC} reports an error if an assumption
 isn\mbox{'}t true, you
 will have to comment out the second conjunct of the \ensuremath{{\ASSUME}}
 statement,
 which asserts that assumption. Comments can be written as follows:
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{T}{F}{7.5}{0}{}%
\ensuremath{\.{\,\backslash\,}}* This is an end-of-line comment.
\end{cpar}%
\end{lcom}%
\@x{}%
\@y{}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 To help you see what the problem is, use the Trace Explorer on the
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 Error page to show the value of \ensuremath{chosen} in each state of the
 trace.
}%
\@xx{}%
\@x{}\bottombar\@xx{}%
\end{document}
