Quelle  tla.sty

%%  TLA DOCUMENT STYLE
%%  (c) 1994, 1998 by Leslie Lamport
%
%  WARNING: Some normal LaTeX commands don't work as they should with
%  this style.  These are the known problems:
%  --  In tla mode, $ is fragile, so it must be \protect'ed if
%      it appears in a moving argument.
%  
%   Changes:
%     18 Nov 98 : Made \nocoloncommands the default.
%     28 Jun 98 : Changed \label so it doesn't leave an extra space.
%     13 Feb 98 : Put a little more space around :\: 
%     20 Jan 98 : Replaced \flushleft with \raggedright in module,
%                 submodule, and nomodule environments (as suggested
%                 by Karsten Loer).
%      7 Jan 98 : Added defs of \TeXAA and \restoreAA
%     24 Dec 97 : Changed def of \tla@while to correct -+->.
%     17 May 97 : Changed def of \deq to use \Delta instead of \mathchar
%                 so it works with mathtime.  (I don't remember
%                 why I originally used \mathchar.)
%      2 Mar 97 : Kludgy bug fix to make \thanks work in \maketitle.  
%      1 Feb 97 : Modified \IF\THEN\ELSE.  Added \LSE and \OTHER.
%                 Added \mbox to \CASE, etc.  Added new TLA+
%                 keywords like \EXTENDS.
%     16 Apr 96 : Minor bug fix to \LET and \IN
%     27 Dec 95 : Removed bug that caused error on blank line inside
%                 \assume or \prove argument.
%      1 Mar 95 : Made \V work with negative argument.
%     14 Oct 94 : Made equation and eqnarray environments use TLA mode
%                 Also redefined \label and \ref so they work with
%                 arbitrary labels inside TLA mode.
%
%   Last modified on Wed Nov 18 17:35:31 PST 1998 by lamport
%
%   This style calls the pf style, and the abbrev style.  These other 
%   styles should not be loaded separately.
%
%   This style puts LaTeX in TLA mode.  This mode causes the following 
%   changes to LaTeX's normal math mode:
%   
%  Characters are in the normal italic font, rather than math italic.
%  Thus $Off$ will produce something that looks like {\it Off} rather
%  than the usual formula that's supposed to equal $Of^{2}$.
%  
%  The following sequences produce the following commands when LaTeX is
%  `inside math mode', where being inside math mode means being in math
%  mode or in the argument of a command or in an environment (such as
%  \mbox or a minipage or tabular environment) that appears inside a math
%  formula.  (See below for how to customize the abbreviations.)
%  
%    ==   :  equals by definition (\deq)
%    =>   : \Rightarrow
%    :\:  : \backslash
%    []   : \Box 
%    <>   : \Diamond
%    ~>   : \leadsto
%    ~    : \lnot
%    -+-> : the TLA "while-plus" operator: an arrow with a "+" over it.
%    <--  : \longleftarrow
%    <-   : \leftarrow
%    <<   : \langle
%    >>   : \rangle
%    -->  : \longrightarrow
%    ->   : \rightarrow
%    |-   : \vdash
%    |=   : \models
%    |->  : \mapsto
%    #    : \neq
%    \/   : \lor
%    /\   : \land   (This command must be followed by a space, and must
%                   not come at the end of a line, unless the line is
%                   ended by a % )
%    "text"  :  {\rm ``{\sf text}''}  (a TLA+ string constant)
%    _.      :  \, 
%    __      :  Produces a `unit' space
%    ___     :  Produces two `unit' spaces
%    __..._  :  Produces n `unit' spaces
%           The default value of a unit space is 1em.  You can reset its 
%           value to .75em by \indentspace{.75em}.
%  
%  The style issues a \coloncommands declaration.  This declaration
%  causes LaTeX to enter colon-command mode.  In colon-command mode,
%  whenever LaTeX is inside math-mode, the string :xxx: is interpreted as
%  \xxx, for any `xxx'.  When LaTeX is inside math mode, a regular colon
%  must be followed by a space.  The declaration \nocoloncommands causes
%  LaTeX to leave colon-command mode.
%  
%  You can leave TLA mode with the \notla declaration, and re-enter it
%  with the \tla declaration.  
%  
%  In TLA mode, the following characters are active while inside math
%  mode:  
%  
%     : [ = < > " _ | / ! - #
%  
%  This means that these characters cannot be used for many purposes--
%  for example:
%  
%     You can't use [ to begin an optional argument.
%     You can't use the following with \left or \right: < > / |
%     You can't use - as a minus sign in something like \hspace{-3pt}.
%  
%  (Since \\ is often used with an optional argument for adding
%  space, the command \V is proved, where \V{.7} means \\[.7em])
%  You can make these characters inactive by a \notlachars command,
%  and reactivate them with \tlachars--for example, so you can write
%  
%       {\notlachars \sqrt[n]{2}}
%  
%  in TLA mode--so long as this doesn't appear in the argument of any
%  command.  The command \xtla{...} is equivalent to
%  
%       {\notlachars ... }
%  
%  The style also defines the following math commands (some particular
%  useful in colon-command mode):
%  
%    \A  :  \forall
%    \E  :  \exists
%    \EE :  bold \exists (TLA's temporal existential quantification)
%    \AA :  bold \forall (TLA's temporal universal quantification)
%    \X  :  \times
%   
%  Note: \TeXAA is defined to be TeX's normal \AA command.
%  The command \restoreAA redefines \AA to its normal value. appropriately
%
%  The following commands, defined here (or in the pf style) are useful
%  in formatting math formulas:
%  
%    For conjunction and disjunction lists, use the conj and disj environments;
%    use noj for a nonbulleted list.
%   
%       \begin{conj}                   /\ x = 7
%          x = 7 \\                    /\ \/ x > z                       
%          \begin{disj}                   \/ (y < foo)  =>
%             x > z \\                         x = 7
%             \begin{noj}
%               (y < foo) => \\ 
%               __x = 7
%             \end{noj}
%           \end{disj}              
%       \end{conj}
%   
%    The environments noj2, noj3, and noj4 make 2-, 3-, and 4-column
%    arrays, with columns separated by &, as usual.
%    These are array environments.
%   
%    if/then/else's are made as follows:
%      \IF{x > 0}    \\                              IF x > 0
%           \THEN    foo                               THEN foo
%           \ELSE    \IF{y > 3} \THEN y + 6 \\         ELSE IF y > 3 THEN y + 6
%                               \ELSE y + 7 \FI \\                   ELSE y + 7
%                    + 3  \FI \\                            + 3
%
%    use \LSE instead of \ELSE to suppress the line break after the
%    THEN clause.
%    
%    Let's are made as follows:
%       \LET x == ... \\
%            y == ... 
%       \IN  ...  \NI
%
%    CASE's are made with the \CASE command, which just makes the
%    "CASE"--e.g.,
%
%      \CASE \begin{noj3}
%              p & -> & xy + 7 \\
%              q & -> & xx + 33
%            \end{noj3}
%  The commands \comment{text} and \tlacomment{text} produce
%  multiline comments (lines separated by \\) that take up no
%  vertical space.  Text is "normal" in \comment (except that
%  \noTeXmath is in effect), and in TLA mode in \tlacomment 

%
%  The style provides the following environments for TLA+ specs:
%     The module, decls, and submodule environments work as 
%     indicated below:
%                           
%       \begin{module}{name}                __________| name |___________
%                                          |          |      |           |
%    
%         \begin{decls}{parameters}          PARAMETERS
%            xyz    : \VARIABLE \\            xyz : VARIABLE
%            foobar : \CONSTANT               foobar : CONSTANT
%         \end{decls}
%    
%       \midbar                            |-----------------------------|
%    
%          \begin{decls}{actions}            ACTIONS
%              ...                            ...
%          \end{decls}
%   
%          \begin{submodule}{submod}          _________| submod |________
%                                            |         |        |        |
%                ...                              ...   
%    
%          \end{submodule}                   |___________________________|
%    
%       \end{module}                       |_____________________________|
%   
%   
%    The decls environment is a tabbing environment, so lines are ended with 
%    \\, and \= , \>, \\, etc. work as usual.  However, its entries are set 
%    in math mode (so TLA-mode commands work).  Inside a module or submodule
%    environment but outside a decls environment, LaTeX is in paragraph
%    mode, with \it in effect.
%
%    The nodecls environment is like the decls environment, except it 
%    has no title (and no argument) and does not indent and does
%
%    For splitting a module across figures, there is the nomodule
%    environment, which is like the module environment but does
%    not produce the top and bottom module lines.  These lines are 
%    produced by the commands \topbar{MODULE-NAME} and \bottombar.
%
%    The following commands produce the obvious keywords:
%
%       \EXTENDS      \INSTANCE     \WITH         \LOCAL
%       \VARIABLE     \CONSTANT     \THEOREM      \CHOOSE
%       \VARIABLES    \CONSTANTS    \ASSUME       \EXCEPT
%       \UNCHANGED    \UNION        \SUBSET      \DOMAIN 
%       \BOOLEAN      \ENABLED      \TRUE         \FALSE  
%       \CHOOSE       \STRING
%
%    The following obsolete commands are left in for compatibility.
%       \IMPORT       \EXPORT       \ACTION       \STATEFCN      
%       \AS           \INCLUDE      
%
%    These are written without final "\", as in
%
%       \INSTANCE Foo \WITH Bar <- Rab
%
%    not as "\INCLUDE\ Foo \WITH\ ...".
%
%
%    The following commands are used to introduce space:
%        \s{1.2}     A 1.2em horizontal space
%        \vs{1.2}    A 1.2em vertical space, made either with a vertical strut 
%                    extending 1.2em below the line, or a \vspace{1.2em}, 
%                    depending on whether used in outer par mode or not.
%        \V{1.2}     Equivalent to \\[1.2em] (which can't be used in math
%                    mode in TLA mode).
%
%
% CUSTOMIZING THE ABBREVIATIONS
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%  You can create a new set of abbreviations.  However, it is advisable
%  to keep the current ones and just add to them.  You do this with
%  a tlabbrev environment, which is just like an abbreviate environment
%  except without the first argument.  (See abbrev.sty for documentation
%  on the abbreviate environment.)  The following tlabbrev environment
%  creates the standard abbreviations.  Modify it to add your own
%  abbreviations.
%
% \begin{tlabbrev}{:[=<-/|#"_!>}{:[=<-/|#"_!\:>}
%   \x ==   {\ensuremath{\;\;\deq\;\;}}
%   \x =>   {\ensuremath{\Rightarrow}}
%   \x =    {=}
%   \x :\:  {\ensuremath{\,\backslash}}
%   \x ::   {::}
%   \x :    {\tlacolon}
%   \x []   {\ensuremath{\Box}}
%   \x [    {[}
%   \x <>   {\ensuremath{\Diamond}}
%   \x <--  {\ensuremath{\longleftarrow}}
%   \x <-   {\ensuremath{\leftarrow}}
%   \x <<   {\ensuremath{\langle\tlathin}}
%   \x <    {\ensuremath{<}}
%   \x >>   {\ensuremath{\tlathin\rangle}}
%   \x >    {\ensuremath{>}}
%   \x -->  {\ensuremath{\longrightarrow}}
%   \x --   {--}
%   \x -+-> {\ensuremath{\tlawhilep}}
%   \x -+-  {-+-}
%   \x -+   {-+}
%   \x ->   {\ensuremath{\rightarrow}}
%   \x -    {\ensuremath{-}}
%   \x |->  {\ensuremath{\mapsto}}
%   \x |-   {\ensuremath{\vdash}}
%   \x |=   {\ensuremath{\models}}
%   \x |    {\ensuremath{|}}
%   \x #    {\ensuremath{\neq}}
%   \x ~>   {\ensuremath{\leadsto}}
%   \x ~    {\ensuremath{\lnot}}
%   \x /    {\tlaslash}
%   \x "    {\ensuremath{\tlaquote}}
%   \x _.   {\,}
%   \x __   {\tlaunder}
%   \x _    {\tlasubscript}
%   \x !    {\ensuremath{\tlathin!\tlathin}}
% \end{tlabbrev}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\input{abbrev.sty}

%% Have to redefine \abr@sanitize  and \abr@unsanitize so they
%% don't muck with $.  For efficiency, remove the mucking about
%% with  &  and %  as well
\gdef\abr@sanitize{\abr@mkother##\abr@mkother^\abr@mkother_}
\gdef\abr@unsanitize{\catcode`##6\catcode`^7\catcode`_8\relax}

%% \noTeXmath
%% \TeXmath
%%   The \noTeXmath command makes all letters in math mode come
%%   from the text italic font (family 4) rather than the usual math
%%   italic family.  Thus $Word$ is just an italic word, not a
%%   weird math formula.  Useful when math symbols are mostly
%%   multiletter. \TeXmath resets to normal.

% 
%%
%% Redefine Math Mode commands to use \tla@everymath
%%  Changed 14 Oct 94 to redefine \equation and \eqnarray as well.
%%
%%  (Can't use \everymath because $ apparently gives next character its 
%%  catcode before executing \everymath)

\def\tla@math{\relax\ifmmode $\else $\tla@everymath\fi}
\let\@begmath\(
\let\@begdispmath\[
\let\@begeqn\equation
\let\@begeqnarray\eqnarray
\def\tla@everymath{}  %% initialization

\catcode`$\active
\let$\tla@math
\def\({\@begmath\tla@everymath}
\def\[{\@begdispmath\tla@everymath}
\def\equation{\@begeqn\tla@everymath}
\def\eqnarray{\tla@everymath\@begeqnarray}

%% Redefine \label and \ref

\let\@oldlabel\label
\def\label{\@bsphack\begingroup\notla\@xlabel}
\def\@xlabel#1{\@oldlabel{#1}\endgroup\@esphack}

\let\@oldref\ref
\def\ref{\begingroup\notla\@xref}
\def\@xref#1{\@oldref{#1}\endgroup}

\newenvironment{tlabbrev}{\begin{abbreviate}{tla@abbrev}}{\end{abbreviate}}


\begin{tlabbrev}{:[=<-/|#"_!>}{:[=<-/|#"_!\:>}
  \x ==   {\ensuremath{\;\;\deq\;\;}}
  \x =>   {\ensuremath{\Rightarrow}}
  \x =    {=}
  \x :\:  {\ensuremath{\,\backslash}\,}
  \x ::   {::}
  \x :    {\tlacolon}
  \x []   {\ensuremath{\Box}}
  \x [    {[}
  \x <>   {\ensuremath{\Diamond}}
  \x <--  {\ensuremath{\longleftarrow}}
  \x <-   {\ensuremath{\leftarrow}}
  \x <<   {\ensuremath{\langle\tlathin}}
  \x <    {\ensuremath{<}}
  \x >>   {\ensuremath{\tlathin\rangle}}
  \x >    {\ensuremath{>}}
  \x -->  {\ensuremath{\longrightarrow}}
  \x --   {--}
  \x -+-> {\ensuremath{\tlawhilep}}
  \x -+-  {-+-}
  \x -+   {-+}
  \x ->   {\ensuremath{\rightarrow}}
  \x -    {\ensuremath{-}}
  \x |->  {\ensuremath{\mapsto}}
  \x |-   {\ensuremath{\vdash}}
  \x |=   {\ensuremath{\models}}
  \x |    {\ensuremath{|}}
  \x #    {\ensuremath{\neq}}
  \x ~>   {\ensuremath{\leadsto}}
  \x ~    {\ensuremath{\lnot}}
  \x /    {\tlaslash}
  \x "    {\ensuremath{\tlaquote}}
  \x _.   {\,}
  \x __   {\tlaunder}
  \x _    {\tlasubscript}
  \x !    {\ensuremath{\tlathin!\tlathin}}
\end{tlabbrev}

%% -+-> : 
\def\tla@while{-\hspace{-.16em}\triangleright}
\def\tlawhilep{\stackrel
  {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}{\tla@while}}

%% \tlachars 
%% \notlachars 
%%    Sets / unsets the catcodes of the following characters to active
%%    :  [  =  <  -  /  |  #  "  _   ! 

\let\tlachars\tla@abbrevact
\let\notlachars\notla@abbrev



\newif\if@tlamode
\@tlamodetrue

%%%%  The following definitions are made with TLA catcodes activated and 
%%%%  with "." catcoded to mean "#".

\begingroup
\catcode`?6\relax
\tlachars

%% :
\gdef\tla@cmdcolon?1:{\ensuremath{\csname ?1\endcsname}}

%% "
\gdef\tlaquote?1"{\mbox{\rm``{\sf ?1}''}}



%% _ : 
  \gdef\tlaunder{\hspace*{\tla@indentspace}%
                         \@nsifnextchar{_}{\tla@spaceunder}{}}
  \gdef\tla@spaceunder_{\hspace*{\tla@indentspace}%
                         \@nsifnextchar{_}{\tla@spaceunder}{}}

\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%  end of active characters  %%%%%%%%%%%%%%%%%


%% \optional
\newcommand{\xtla}{\begingroup \notlachars \@xtla}
\newcommand{\@xtla}[1]{#1\endgroup}


%% :
%% \coloncommands
%% \nocoloncommands
%%    Declarations that enable or disable the interpreting of :...: as 
%%    commands in TLA mode. However, :\: is always interpreted as \backslash
%%    in TLA mode.  The default is \coloncommands.
\newcommand{\coloncommands}{%
  \def\tlacolon{\@ifspace{\tla@realcolon}{\tla@cmdcolon}}} 
\newcommand{\nocoloncommands}{\def\tlacolon{\tla@realcolon}}

\coloncommands  %% THE DEFAULT
\def\tla@realcolon{\ifmmode \,:\,\else{\rm :}\fi}

%% [   makes [] : \Box       %%% must be changed if ] is made active
%\def\tla@lb{\@nsifnextchar{]}{\tla@lbx}{[}}
%\def\tla@lbx]{\ensuremath{\Box}}

%% =   
%\def\tla@realeq{=}

%% <
%\def\tla@reallt{\ensuremath{<}}

%% >
%\def\tla@realgt{\ensuremath{>}}

%% !
%\def\tla@bang{\ensuremath{\tlathin!\tlathin}}

%% / : defines \tlaslash so \tlaslash\ expands to \land
\def\tlaslash{\@nsifnextchar{\ }{\tla@slashx}{/}}
\def\tla@slashx\ {\ensuremath{\land}}

% The following was a valiant attempt to make /\ work when
% not followed by a space.  However, it doesn't work if the /\ is
% inside a command argument, in which case the following "\..." has already
% been tokenized before the "/" gets a chance to look at what's ahead.
% (Isn't TeX wonderful?)
%   \def\@makebsother{\catcode`\\=12\relax}
%   \def\@makebsescape{\catcode`\\=0\relax}
%   \begingroup
%   \catcode`?=0\relax
%   \@makebsother
%   ?gdef?tlaslash
%         {?@makebsother?@nsifnextchar{\}{?tla@slashx}{?@makebsescape/}}
%   ?gdef?tla@slashx\{?@makebsescape?ensuremath{?land}}
%   ?endgroup



%% -
%\def\tla@realminus{-}

%%_
\def\tlasubscript#1{\ensuremath{\mbox{}_{#1}}}

%% |
%\def\tla@realvert{\ensuremath{|}}



%% # produces \neq
%\def\tla@hash{\ensuremath{\neq}}


%% \tla ==  Make characters active;
%%          
\def\tla{\@tlamodetrue
          \def\tla@everymath{%
                \noTeXmath
                 \tla@abbrev
                \def\/{\lor}}%
           \tla@abbrev
           \notla@abbrev
         \ifmmode\tla@everymath\fi}

\def\notla{\def\tla@everymath{}%
  \@tlamodefalse
  \TeXmath
  \def\/{\@italcor}%
  \let~\@realtilde
  \notlachars}



%%% MISCELLANY
%% \ensuremath: the LaTeX2e command
%
\def\ensuremath#1{\relax\ifmmode #1\else $#1$\fi}

% \@italcor = normal \/
% \@realtilde = normal ~
\let\@italcor\/ %%%%% \/ redefined to \or
\let\@realtilde~

% SPACING
%
% \tlathin : a math-mode space 1/2 the width of \,
%
\def\tlathin{\mskip.5\thinmuskip}
\def\indentspace#1{\def\tla@indentspace{#1}}
\indentspace{1em}


% \@ifspace{A}{B} executes A if the next token is a space token,
% else it executes B and replaces next token.
%

\def\@ifspace#1#2{\def\@tempa{#1}\def\@tempb{#2}\futurelet\@tempc\@ifspacex}
\def\@ifspacex{\ifx\@sptoken\@tempc\let\@tempd\@tempa\else
     \let\@tempd\@tempb\fi\@tempd}

% \@nsifnextchar like \@ifnextchar, except it doesn't skip over
% space tokens.
\def\@nsifnextchar#1#2#3{\let\@tempe #1\def\@tempa{#2}\def\@tempb{#3}\futurelet
    \@tempc\@ifnsnch}
\def\@ifnsnch{\ifx \@tempc \@tempe\let\@tempd\@tempa\else\let\@tempd\@tempb\fi
      \@tempd}

%%%%%%%%%%%%%%%%%%%%%%%%%%%% MATH SYMBOLS %%%%%%%%%%%%%%%%%%%
%
%\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\mathchar"7001}{=}}}
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\def\A{\forall\,}
\def\E{\exists\,}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\exists\s{-.517}\exists\s{-.517}\exists$}}\exists\s{-.517}\exists
            \s{-.517}\exists\,$}}
\let\TeXAA=\AA
\newcommand{\restoreAA}{\let\AA=\TeXAA}

\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\forall\s{-.517}\forall\s{-.517}\forall$}}\forall\s{-.517}\forall
            \s{-.517}\forall\,$}}
\newcommand{\X}{\ensuremath{\times}}

%%%%%%%%%%%%%%%% INITIALZE

%%%%%%%%%%% LOAD pf.sty %%%%%%%%%%%%%%%
\typeout{Loading pf style}
\input{pf.sty}
\tla


% Redefine conj and disj to leave more space, and \pf to remove
% \/.

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

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

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

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

\renewcommand{\pf}{{\kwfont Proof\@italcor}:}

%%%%%%%%%%%%% redefine some pf.sty commands with $ having its normal definition
\begingroup
\catcode`$3\relax

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

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

\gdef\pfSetName{%
  \edef\pfLongStep{%
    \ifnum\pfLevelCount>\@ne
      \pfLongLevel\pfdot\the\pfStepCount
     \else\the\pfStepCount\fi}%
  \edef\pfStepName{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
    {\pfLongStep}{\pfLongStep}%
    \else
     {$\langle\the\pfLevelCount\rangle$}%
     {$\langle\the\pfLevelCount\rangle\the\pfStepCount$}%
   \fi}}
\endgroup

%% Redefine \step, \assume, \prove, \pflet, and \case  so their arguments
%% have characters made active.

\let\tla@stepy\step
\renewcommand{\step}[1]{\begingroup\if@tlamode\tlachars\fi\tla@stepx{#1}}
\newcommand{\tla@stepx}[2]{\endgroup\tla@stepy{#1}{#2}}
%% 27 Dec 95 -- changed \def to \newcommand

\let\tla@assumey\assume
\renewcommand{\assume}{\begingroup\if@tlamode\tlachars\fi\tla@assumex}
\newcommand{\tla@assumex}[1]{\endgroup\tla@assumey{#1}}

\let\tla@provey\prove
\renewcommand{\prove}{\begingroup\if@tlamode\tlachars\fi\tla@provex}
\newcommand{\tla@provex}[1]{\endgroup\tla@provey{#1}}

\let\tla@casey\case
\renewcommand{\case}{\begingroup\if@tlamode\tlachars\fi\tla@casex}
\newcommand{\tla@casex}[1]{\endgroup\tla@casey{#1}}

\let\tla@pflety\pflet
\renewcommand{\pflet}{\begingroup\if@tlamode\tlachars\fi\tla@pfletx}
\newcommand{\tla@pfletx}[1]{\endgroup\tla@pflety{#1}}


%%%%%%%%%%%%%%  Module formatting commands

%%%% noj, if/then/else %%%%%%%%%%%%%%%%%%
% \def\IF#1{\begin{array}[t]{@{}l@{}l@{}l@{}}%
%             \@ifnextchar{\\}%
%               {\makebox[.6em][l]{{\bf if\, }$#1$}}{\mbox{{\bf if }$#1$ }}}
% \def\THEN{&\mbox{\bf \,then }&\begin{array}[t]{@{}l@{}}}
% \def\ELSE{\end{array}\\ &\mbox{\bf \,else }&\begin{array}[t]{@{}l@{}}}
% \def\FI{\end{array}\end{array}}
%%%
\newcommand{\gobbleone}[1]{}
\def\IF#1{\@ifnextchar{\\}%
           {\begin{array}[t]{@{\hspace{.6em}}l@{}l@{}}
              \multicolumn{2}{@{}l}{\mbox{{\sc if\, }$#1$}}\\
            \gobbleone}%
           {\mbox{{\sc if }$#1$ }%
             \begin{array}[t]{@{}l@{}l@{}}}}
\def\THEN{\mbox{\sc \,then }&\begin{array}[t]{@{}l@{}}}
\def\ELSE{\end{array}\\\mbox{\sc \,else }&\begin{array}[t]{@{}l@{}}}
\def\FI{\end{array}\end{array}}
\def\LSE{\mbox{\sc\ \,else }}

\newenvironment{noj}{\begin{array}[t]{@{}l@{}}}{\end{array}}
\newenvironment{noj2}{\begin{array}[t]{@{}l@{\;\;}l@{}}}{\end{array}}
\newenvironment{noj3}{\begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{}}}{\end{array}}
\newenvironment{noj4}%
  {\begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{\;\;}l@{}}}{\end{array}}

%\newenvironment{noj}{\begin{array}[t]{@{}l@{}}}%
%                    {\end{array}}


%%%% let %%%%%%%%
%% \LET and \IN corrected 16 Apr 96 to add \mbox's.
%% Correction suggested by Denis Roegel
\newcommand{\LET}{\begin{array}[t]{@{}l@{\;\;}l@{}} \mbox{\bf let}% 
                              &\begin{array}[t]{@{}l@{}}} 
\newcommand{\IN}{\end{array}\\\mbox{\bf in}&\begin{array}[t]{@{}l@{}}}

% \newcommand{\LET}{\begin{array}[t]{@{}l@{\;\;}l@{}} {\bf let}% 
%                              &\begin{array}[t]{@{}l@{}}} 
% \newcommand{\IN}{\end{array}\\{\bf in}&\begin{array}[t]{@{}l@{}}}
\newcommand{\NI}{\end{array}\end{array}}

%%%% case %%%
%\newcommand{\CASE}{{\bf case\ }}
\newcommand{\CASE}{\mbox{\bf case\ }}
\newcommand{\OTHER}{\mbox{\bf other}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                  COMMANDS FROM spec92.sty                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
\newlength{\@charwidth}
\settowidth{\@charwidth}{{\small\tt M}}
\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
\newlength{\boxindent}\setlength{\boxindent}{22\@charwidth}
\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
\newcommand{\boxsep}{\@charwidth}
\newlength{\boxruleht}
\newlength{\boxruledp}
\newcommand{\@computerule}{%
  \setlength{\boxruleht}{.5ex}%
  \setlength{\boxruledp}{-\boxruleht}%
  \addtolength{\boxruledp}{\boxrulewd}}
\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
                      \hfill\mbox{}}

\newcommand{\@nmlineraise}{\if@botline -\boxrulewd
    \else-\boxlineht\fi}
\newcommand{\nameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{.5\baselineskip}}
\newif\if@botline

%%%%%%%%%%%%%%%%%%END COMMANDS FROM spec92.sty %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\topbar}[1]{\tlanameline{\ 
     {\sc module} {\it #1\@italcor} }\par}

\newenvironment{nomodule}{\begin{trivlist}\raggedright\@computerule
            \item[]\it
            \catcode`_=\active\relax
        }{\par\end{trivlist}}

\newenvironment{module}[1]{\begin{trivlist}\raggedright\@computerule
            \item[]\tlanameline{\ {\sc module} {\it #1\@italcor} }\par\it
            \catcode`_=\active\relax
        }{\par\bottombar\end{trivlist}}


\newenvironment{submodule}[1]{\par
        \vspace{-.5em}%%%%%%%%%%%  space at top of submodule
    \begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}\raggedright\@computerule
            \item[]\tlanameline{\ {\sc module} {\it #1\@italcor} }\par
        }{\par\bottombar\end{list}}


\newcommand{\tlanameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}%
          \vspace{.2em}%%% EXTRA SPACE BELOW TOP LINE OF MODULE
               }

%%%%% Fix to \midline and \botline from spec92

\newcommand{\midbar}{\par\hspace{-\boxsep}%
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}%
         \vspace{-.2em}%%% SPACE BELOW \midbar
                \par}

\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{\xtrivlist}{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%     
       \partopsep=0pt%
       \itemsep=0pt}}
\def\endxtrivlist{\end{list}}

\let\@@startfield\@startfield
\let\@@stopfield\@stopfield

%% need to change \@tabcr because its look-ahead at the next
%  character causes that character to be prematurely cat-coded.
%
\def\tla@tabcr{\@stopline\@startline\ignorespaces}

\def\xtabbing{\lineskip \z@\let\>\@rtab\let\<\@ltab\let\=\@settab
     \def\@startfield{\@@startfield\(}
     \def\@stopfield{\)\@@stopfield}
     \let\+\@tabplus
     \let\-\@tabminus
     \let\`\@tabrj\let\'\@tablab
     \let\\=\tla@tabcr
     \global\@hightab\@firsttab
     \global\@nxttabmar\@firsttab
     \dimen\@firsttab\@totalleftmargin
     \global\@tabpush0 \global\@rjfieldfalse
     \xtrivlist \item[]\if@minipage\else\vskip\parskip\fi
     \setbox\@tabfbox\hbox{\rlap{\indent\hskip\@totalleftmargin
       \the\everypar}}\def\@itemfudge{\box\@tabfbox}\@startline\ignorespaces}

\def\endxtabbing{\@stopline\ifnum\@tabpush > 0 \@badpoptabs \fi\endxtrivlist}

\newenvironment{decls}[1]{\par
      \addvspace{.4em}%%%  EXTRA SPACE ABOVE decls ENVIRONMENT
{\bf #1}\begin{xtabbing}%
  \hspace{1em}\=\+\kill}{\end{xtabbing}}

\newenvironment{nodecls}{\par
      \addvspace{.4em}%%%  EXTRA SPACE ABOVE nodecls ENVIRONMENT
\begin{xtabbing}}{\end{xtabbing}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%% KEYWORDS %%%%%%%%%%%%%%%%%%
%
\newcommand{\tlacomment}{\begingroup\tlachars\@comment}
%\newcommand{\@tlacomment}[1]{\endgroup\mbox{\footnotesize\rm #1}}
\newcommand{\comment}{\begingroup\notlachars\@comment}
\newcommand{\@comment}[1]{\endgroup
    \raisebox{0pt}[0pt][0pt]{\footnotesize\rm %
       \begin{tabular}[t]{@{}l@{}}#1\end{tabular}}}
%\newcommand{\@comment}[1]{\endgroup
%    \mbox{\footnotesize\rm \raisebox{0pt}[0pt][0pt]{%
%       \begin{tabular}[t]{@{}l@{}}#1\end{tabular}}}}
\newcommand{\EXTENDS}{\mbox{\sc extends }}
\newcommand{\INSTANCE}{\mbox{\sc instance }}
\newcommand{\THEOREM}{\mbox{\sc theorem }}
\newcommand{\ASSUME}{\mbox{\sc assume }}
\newcommand{\LOCAL}{\mbox{\sc local }}
\newcommand{\VARIABLE}{\mbox{\sc variable }}
\newcommand{\VARIABLES}{\mbox{\sc variables }}
\newcommand{\CONSTANT}{\mbox{\sc constant }}
\newcommand{\CONSTANTS}{\mbox{\sc constants }}
\newcommand{\WITH}{\,\mbox{\bf with }}
\newcommand{\BOOLEAN}{\mbox{\sc boolean}}
\newcommand{\UNION}{\mbox{\sc union }}
\newcommand{\TRUE}{\mbox{\sc true}}
\newcommand{\FALSE}{\mbox{\sc false}}
\newcommand{\UNCHANGED}{\mbox{\sc unchanged }}
\newcommand{\EXCEPT}{\mbox{\sc\ except }}
\newcommand{\CHOOSE}{\mbox{\sc choose }}
\newcommand{\STRING}{\mbox{\sc string}}
\newcommand{\ENABLED}{\mbox{\sc Enabled\s{.2}}}
\newcommand{\DOMAIN}{\mbox{\sc domain\s{.2}}}
\newcommand{\SUBSET}{\mbox{\sc subset\s{.2}}}
\newcommand{\WF}{\mbox{\rm WF}}
\newcommand{\SF}{\mbox{\rm SF}}
% obsolete
\newcommand{\ACTION}{\mbox{\sc action}}
\newcommand{\STATEFCN}{\mbox{\sc state fcn}}
\newcommand{\IMPORT}{\mbox{\bf import }}
\newcommand{\EXPORT}{\mbox{\bf export }}
\newcommand{\INCLUDE}{\mbox{\bf include }}
\newcommand{\AS}{\,\mbox{\bf as }}

%%%%%%%%%%%%%%%%%%%%%%% SPACE COMMANDS %%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\s}{\begingroup\notlachars\tla@s}
\newcommand{\tla@s}[1]{\endgroup\hspace*{#1em}}
\newcommand{\vs}{\begingroup\notlachars\tla@vs}
\newcommand{\tla@vs}[1]{\endgroup\ifinner
                       \raisebox{-.34em}{\raisebox{-#1em}{\rule{0pt}{.1pt}}}
                      \else \vspace{#1em}\fi}
%%% 1 Mar 95 : Made \V work with negative argument.
\newcommand{\V}{\begingroup\notlachars\tla@V}
\def\tla@V#1{\endgroup\ifdim #1em<\z@\\[#1em]\else\vs{#1}\\\fi} 

%%%%%%%%%%%%%%%%%%%% Fixing \maketitle %%%%%%%%%%%%%%%%%%%%%%%

% For some unfathomable reason, a \maketitle command with a \thanks
% doesn't work in tla mode.  The kludge to fix this is to redefine
% \maketitle to {\notla \maketitle}.  This kludge will fail if
% \maketitle is redefined by some package loaded after the tla package.

\let\@savedmaketitle=\maketitle
\def\maketitle{{\notla\@savedmaketitle}}

\nocoloncommands