Skip to content

K
KTLA Study
Commit d7f804e2 authored by Kirill Smelkov's avatar Kirill Smelkov
Browse files
Options

.

parent a9e313d1
Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 1288 deletions
MutualExclusionSpec.toolbox/MutualExclusionSpec.log deleted 100644 → 0
View file @ a9e313d1
This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9) 10 FEB 2022 12:55
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**MutualExclusionSpec.tex
(./MutualExclusionSpec.tex
LaTeX2e <2020-10-01> patch level 4
L3 programming layer <2021-01-09> xparse <2020-03-03>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2020/04/10 v1.4m Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo
File: size10.clo 2020/04/10 v1.4m Standard LaTeX file (size option)
)
\c@part=\count177
\c@section=\count178
\c@subsection=\count179
\c@subsubsection=\count180
\c@paragraph=\count181
\c@subparagraph=\count182
\c@figure=\count183
\c@table=\count184
\abovecaptionskip=\skip47
\belowcaptionskip=\skip48
\bibindent=\dimen138
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
Package: color 2020/02/24 v1.2b Standard LaTeX Color (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package color Info: Driver file: pdftex.def on input line 147.
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
)) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info: Overwriting symbol font `lasy' in version `bold'
(Font) U/lasy/m/n --> U/lasy/b/n on input line 52.
) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
)
\symlength=\skip49
\equalswidth=\skip50
\charwidth=\skip51
\boxrulewd=\skip52
\boxlineht=\skip53
\boxruleht=\skip54
\boxruledp=\skip55
\pcalvspace=\skip56
\lcomindent=\skip57
\@xlen=\skip58
\templena=\skip59
\templenb=\skip60
\tempboxa=\box47
\vshadelen=\skip61
\boxwidth=\skip62
\multicommentdepth=\skip63
\c@pardepth=\count185
\tempsbox=\box48
\@cparht=\skip64
\@cpardp=\skip65
\xmcomlen=\skip66
\spacewidth=\skip67
\alignboxwidth=\skip68
\alignwidth=\skip69
\alignbox=\box49
\symtlaitalics=\mathgroup5
\c@tlx@ctr=\count186
(/usr/share/texlive/texmf-dist/tex/latex/tools/verbatim.sty
Package: verbatim 2020-07-07 v1.5u LaTeX2e package for verbatim enhancements
\every@verbatim=\toks15
\verbatim@line=\toks16
\verbatim@in@stream=\read2
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2020-01-29 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count187
\l__pdf_internal_box=\box50
) (./MutualExclusionSpec.aux)
\openout1 = `MutualExclusionSpec.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count188
\scratchdimen=\dimen139
\scratchbox=\box51
\nofMPsegments=\count189
\nofMParguments=\count190
\everyMPshowfont=\toks17
\MPscratchCnt=\count191
\MPscratchDim=\dimen140
\MPnumerator=\count192
\makeMPintoPDFobject=\count193
\everyMPtoPDFconversion=\toks18
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <7> on input line 942.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <5> on input line 942.
LaTeX Font Info: Trying to load font information for U+lasy on input line 94
2.
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <8> on input line 948.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <6> on input line 948.
Overfull \hbox (51.37141pt too wide) in paragraph at lines 1043--1051
[][][][]
[]
Overfull \hbox (56.19621pt too wide) in paragraph at lines 1053--1059
[][][][]
[]
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (1.33426pt too wide) in paragraph at lines 1068--1074
[][][][]
[]
Overfull \hbox (14.0878pt too wide) in paragraph at lines 1074--1079
[][][][]
[]
Overfull \hbox (73.20253pt too wide) in paragraph at lines 1081--1087
[][][][]
[]
[2] (./MutualExclusionSpec.aux) )
Here is how much of TeX's memory you used:
1309 strings out of 479304
18453 string characters out of 5869780
313203 words of memory out of 5000000
18536 multiletter control sequences out of 15000+600000
408900 words of font info for 48 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
44i,10n,50p,200b,239s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmss8.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/font
s/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmti7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmti8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/lat
xfont/lasy10.pfb>
Output written on MutualExclusionSpec.pdf (2 pages, 147797 bytes).
PDF statistics:
71 PDF objects out of 1000 (max. 8388607)
51 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
MutualExclusionSpec.toolbox/MutualExclusionSpec.tex deleted 100644 → 0
View file @ a9e313d1
\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}
MutualExclusionSpec}\moduleRightDash\@xx{}%
\@x{}%
\@y{\@s{0}%
Module \ensuremath{MutualExclusionSpec} provides general specification for
mutual-exclusion problem.
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
\ensuremath{Procs} is set of processes.
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
Every process is assumed to loop and enter into \ensuremath{\@w{cs}} state
on every interation.
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
Non-critical state is represented as \ensuremath{\@w{non-cs}}.
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
When process decides it want to enter into critical-section, it first goes
into \ensuremath{\@w{csentry}} state.
}%
\@xx{}%
\@x{ {\CONSTANT} Procs}%
\@x{ {\VARIABLES} pc}%
\@pvspace{8.0pt}%
\@x{ TypeOK \.{\defeq} pc \.{\in} [ Procs \.{\rightarrow} \{\@w{non{-}cs}
,\,\@w{csentry} ,\,\@w{cs} \} ]}%
\@pvspace{8.0pt}%
\@x{ vars \.{\defeq} {\langle} pc {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
All processes start from non-critical section.
}%
\@xx{}%
\@x{ Init \.{\defeq} pc \.{\in} [ Procs \.{\rightarrow} \{\@w{non{-}cs} \} ]}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
\ensuremath{WantCS(proc)} is action when \ensuremath{proc} decides that it
wants to enter into critical section.
}%
\@xx{}%
\@x{ WantCS ( proc ) \.{\defeq}}%
\@x{\@s{46.00} \.{\land}\@s{3.37} pc [ proc ] \.{=}\@w{non{-}cs}}%
\@x{\@s{46.00} \.{\land}\@s{3.37} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [
proc ] \.{=}\@w{csentry} ]}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
\ensuremath{EnterCS(proc)} is action when \ensuremath{proc} enters critical
section.
}%
\@xx{}%
\@x{ EnterCS ( proc ) \.{\defeq}}%
\@x{\@s{42.40} \.{\land} pc [ proc ] \.{=}\@w{csentry}}%
\@x{\@s{42.40} \.{\land} \A\, i \.{\in} Procs \.{\,\backslash\,} \{ proc \}
\.{:} pc [ i ] \.{\neq}\@w{cs}}%
\@x{\@s{42.40} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ proc ]
\.{=}\@w{cs} ]}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
\ensuremath{ExitCS(proc)} is action when \ensuremath{proc} leaves critical
section.
}%
\@xx{}%
\@x{ ExitCS ( proc ) \.{\defeq}}%
\@x{\@s{39.77} \.{\land}\@s{3.37} pc [ proc ] \.{=}\@w{cs}}%
\@x{\@s{39.77} \.{\land}\@s{3.37} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [
proc ] \.{=}\@w{non{-}cs} ]}%
\@pvspace{8.0pt}%
\@x{ Next \.{\defeq} \E\, i \.{\in} Procs \.{:} WantCS ( i ) \.{\lor} EnterCS
( i ) \.{\lor} ExitCS ( i )}%
\@pvspace{16.0pt}%
\@x{ Spec\@s{1.46} \.{\defeq} \.{\land} Init}%
\@x{\@s{39.83} \.{\land} {\Box} [ Next ]_{ vars}}%
\@x{\@s{39.83} \.{\land} \A\, i \.{\in} Procs \.{:} (\@s{45.1}}%
\@y{\@s{0}%
fairness
}%
\@xx{}%
\@x{\@s{55.04}}%
\@y{\@s{0}%
not fair for \ensuremath{WantCS \.{-}} it can pause and even hang there
}%
\@xx{}%
\@x{\@s{55.04} \.{\land} {\SF}_{ vars} ( EnterCS ( i ) )}%
\@x{\@s{55.04} \.{\land} {\SF}_{ vars} ( ExitCS ( i ) ) )}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
\ensuremath{MutualExclusion} is invariant indicating that no two processes
can be inside critical section at the same time.
}%
\@xx{}%
\@x{ MutualExclusion \.{\defeq} \A\, i ,\, j \.{\in} Procs \.{:} ( i \.{\neq}
j ) \.{\implies} {\lnot} ( ( pc [ i ] \.{=}\@w{cs} ) \.{\land} ( pc [ j ]
\.{=}\@w{cs} ) )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
Liveness is temporal property indicating that every process has a chance to
enter critical section and leaves it.
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
A process should keep on entering the critical-section unless it is stuck in
it non-critical part.
}%
\@xx{}%
\@x{ Liveness \.{\defeq} \A\, i \.{\in} Procs \.{:}}%
\@x{\@s{67.97} \.{\land}}%
\@x{\@s{84.37} \.{\lor} {\Diamond} {\Box} ( pc [ i ] \.{=}\@w{non{-}cs}
)\@s{73.84}}%
\@y{\@s{0}%
either stuck in non-\ensuremath{cs}, or
}%
\@xx{}%
\@x{\@s{84.37} \.{\lor} {\Box} {\Diamond} ( pc [ i ] \.{=}\@w{csentry}
)\@s{71.26}}%
\@y{\@s{0}%
keeps on reaching ``enter \ensuremath{cs}''
}%
\@xx{}%
\@x{\@s{67.97} \.{\land}}%
\@x{\@s{84.37} \.{\land} ( pc [ i ] \.{=}\@w{csentry} ) \.{\leadsto} ( pc [ i
] \.{=}\@w{cs} )\@s{12.29}}%
\@y{\@s{0}%
if it wants to enter, it enters \ensuremath{cs} and leaves it
}%
\@xx{}%
\@x{\@s{84.37} \.{\land} ( pc [ i ] \.{=}\@w{cs} ) \.{\leadsto} ( pc [ i ]
\.{=}\@w{non{-}cs} )}%
\@pvspace{16.0pt}%
\@x{ {\THEOREM} Spec \.{\implies} {\Box} TypeOK}%
\@x{ {\THEOREM} Spec \.{\implies} {\Box} MutualExclusion}%
\@x{ {\THEOREM} Spec \.{\implies} Liveness}%
\@pvspace{16.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{Thu}
\ensuremath{Feb} 10 12:53:17 \ensuremath{MSK} 2022 by \ensuremath{kirr
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{\,\backslash\,}\.{*}} Created \ensuremath{Wed}
\ensuremath{Feb} 09 13:11:29 \ensuremath{MSK} 2022 by \ensuremath{kirr
}%
\end{cpar}%
\end{lcom}%
\end{document}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment
GitLab Nexedi Edition | About GitLab | About Nexedi | 沪ICP备2021021310号-2 | 沪ICP备2021021310号-7