1083 lines
45 KiB
TeX
1083 lines
45 KiB
TeX
\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} TCommit}\moduleRightDash\@xx{}%
|
|
\@pvspace{8.0pt}%
|
|
\begin{lcom}{0}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
This specification is explained in ``Transaction Commit'', Lecture 5 of
|
|
the TLA+ Video Course.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{ {\CONSTANT} RM\@s{24.59}}%
|
|
\@y{\@s{0}%
|
|
The set of participating resource managers
|
|
}%
|
|
\@xx{}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ {\VARIABLE} rmState\@s{10.70}}%
|
|
\@y{\@s{0}%
|
|
\ensuremath{rmState[rm]} is the state of resource manager \ensuremath{r}.
|
|
}%
|
|
\@xx{}%
|
|
\@x{}\midbar\@xx{}%
|
|
\@x{ TCTypeOK \.{\defeq}}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
The type-correctness invariant
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{\@s{8.2} rmState \.{\in} [ RM \.{\rightarrow} \{\@w{working}
|
|
,\,\@w{prepared} ,\,\@w{committed} ,\,\@w{aborted} \} ]}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ TCInit \.{\defeq}\@s{8.2} rmState \.{=} [ r \.{\in} RM
|
|
\.{\mapsto}\@w{working} ]}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
The initial predicate.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ canCommit \.{\defeq} \A\, r \.{\in} RM \.{:} rmState [ r ] \.{\in}
|
|
\{\@w{prepared} ,\,\@w{committed} \}}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
True iff all \ensuremath{RMs} are in the \ensuremath{\@w{prepared}} or
|
|
\ensuremath{\@w{committed}} state.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ notCommitted \.{\defeq} \A\, r \.{\in} RM \.{:} rmState [ r ]
|
|
\.{\neq}\@w{committed}}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
True iff no resource manager has decided to commit.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{}\midbar\@xx{}%
|
|
\begin{lcom}{0}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
We now define the actions that may be performed by the \ensuremath{RMs}, and
|
|
then
|
|
define the complete next-state action of the specification to be the
|
|
disjunction of the possible \ensuremath{RM} actions.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{ Prepare ( r ) \.{\defeq} \.{\land} rmState [ r ] \.{=}\@w{working}}%
|
|
\@x{\@s{65.81} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r
|
|
] \.{=}\@w{prepared} ]}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ Decide ( r )\@s{4.08} \.{\defeq} \.{\lor} \.{\land} rmState [ r ]
|
|
\.{=}\@w{prepared}}%
|
|
\@x{\@s{76.92} \.{\land} canCommit}%
|
|
\@x{\@s{76.92} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r
|
|
] \.{=}\@w{committed} ]}%
|
|
\@x{\@s{65.81} \.{\lor} \.{\land} rmState [ r ] \.{\in} \{\@w{working}
|
|
,\,\@w{prepared} \}}%
|
|
\@x{\@s{76.92} \.{\land} notCommitted}%
|
|
\@x{\@s{76.92} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r
|
|
] \.{=}\@w{aborted} ]}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ TCNext \.{\defeq} \E\, r \.{\in} RM \.{:} Prepare ( r ) \.{\lor} Decide
|
|
( r )}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
The next-state action.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{}\midbar\@xx{}%
|
|
\@x{ TCConsistent \.{\defeq}}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
A state predicate asserting that two \ensuremath{RMs} have not arrived at
|
|
conflicting decisions. It is an invariant of the specification.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{\@s{8.2} \A\, r1 ,\, r2 \.{\in} RM \.{:} {\lnot} \.{\land} rmState [ r1 ]
|
|
\.{=}\@w{aborted}}%
|
|
\@x{\@s{88.35} \.{\land} rmState [ r2 ] \.{=}\@w{committed}}%
|
|
\@x{}\midbar\@xx{}%
|
|
\begin{lcom}{0}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
The following part of the spec is not discussed in Video Lecture 5. It
|
|
will be explained in Video Lecture 8.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@x{ TCSpec \.{\defeq} TCInit \.{\land} {\Box} [ TCNext ]_{ rmState}}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
The complete specification of the protocol written as a temporal
|
|
formula.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{ {\THEOREM} TCSpec \.{\implies} {\Box} ( TCTypeOK \.{\land} TCConsistent
|
|
)}%
|
|
\begin{lcom}{8.2}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
This theorem asserts the truth of the temporal formula whose meaning
|
|
is that the state predicate \ensuremath{TCTypeOK \.{\land} TCInvariant} is
|
|
an invariant
|
|
of the specification \ensuremath{TCSpec}. Invariance of this conjunction is
|
|
equivalent to invariance of both of the formulas \ensuremath{TCTypeOK} and
|
|
\ensuremath{TCConsistent}.
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\@pvspace{8.0pt}%
|
|
\@x{}\bottombar\@xx{}%
|
|
\setboolean{shading}{false}
|
|
\begin{lcom}{0}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
\ensuremath{\.{\,\backslash\,}}* Modification History
|
|
\end{cpar}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
\ensuremath{\.{\,\backslash\,}}* Last modified \ensuremath{Fri}
|
|
\ensuremath{Dec} 21 17:16:06 \ensuremath{CET} 2018 by \ensuremath{veitheller
|
|
}%
|
|
\end{cpar}%
|
|
\begin{cpar}{0}{F}{F}{0}{0}{}%
|
|
\ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Fri} \ensuremath{Dec} 21
|
|
17:15:44 \ensuremath{CET} 2018 by \ensuremath{veitheller
|
|
}%
|
|
\end{cpar}%
|
|
\end{lcom}%
|
|
\end{document}
|