\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} lock\_free\_stack\_ABA}\moduleRightDash\@xx{}% \@pvspace{8.0pt}% \begin{lcom}{0}% \begin{cpar}{0}{F}{F}{0}{0}{}% Copyright (c) 2017, Gene \ensuremath{Cooperman}. May be freely distributed and modified as long as this copyright notice remains. \end{cpar}% \vshade{5.0}% \begin{cpar}{0}{F}{F}{0}{0}{}% For \ensuremath{ABA} problem, see: https:\ensuremath{\.{\slsl}en.wikipedia.org}/wiki/\ensuremath{ABA\_problem }% \end{cpar}% \vshade{5.0}% \begin{cpar}{0}{T}{T}{0}{5.0}{% NOTE:}% The label \ensuremath{\@w{pop2a}} in \ensuremath{popStack()} below ``causes'' the bug to be exposed. Try deleting it. This would have the effect of atomically executing: \end{cpar}% \begin{cpar}{0}{T}{F}{5.0}{0}{}% \ensuremath{CAS( HEAD,\, local\_myhead,\, address[local\_myhead].next )}; \end{cpar}% \begin{cpar}{1}{F}{F}{0}{0}{}% because it hides the internal assembly code that first computes the register value, \ensuremath{reg\_next}, and then executes \ensuremath{CAS()}. \end{cpar}% \vshade{5.0}% \begin{cpar}{0}{F}{F}{0}{0}{}% Note that the field ``\ensuremath{onStack}'' is present only for debugging, and for assertions. Don\mbox{'}t hesitate to add extra fields and variables to ease the job of model checking. \end{cpar}% \vshade{5.0}% \begin{cpar}{0}{F}{F}{0}{0}{}% The bug is the \ensuremath{ABA} problem. When illustrating this bug, the errors in the ``Model Checking Results'' tab will have too many frames to easily read. You can then remove many of the unnecessary labels in other routines to easily see the cause of the bug: the \ensuremath{ABA} problem. \end{cpar}% \end{lcom}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% Always include these \ensuremath{PlusCal} modules for basic data types. }% \@xx{}% \@x{ {\EXTENDS} Naturals ,\, Sequences ,\, TLC ,\, FiniteSets}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% These constants will have to be assigned a value within the generated module. }% \@xx{}% \@x{ {\CONSTANTS} MAX\_ITER ,\, MAX\_STACK\_SIZE}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% \ensuremath{NUM\_THREADS} is a PRE-DEFINED constant. It cannot be changed later. }% \@xx{}% \@x{ NUM\_THREADS \.{\defeq} 2}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% \ensuremath{NULL} is a unique value (pre-defined constant) }% \@xx{}% \@x{ NULL \.{\defeq} {\CHOOSE} n \.{:} n \.{\notin} 1 \.{\dotdot} MAX\_STACK\_SIZE}% \@pvspace{8.0pt}% \pcalsymbolstrue \pcalshadingtrue \csyntaxtrue \@x{ {\p@mmalgorithm} LockFreeStack {\p@lbrace}}% \@x{ {\p@variables} retVal \.{=} [ thread \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} NULL ] ,\,}% \@x{\@s{47.76} address \.{=} [ addr\@s{1.21} \.{\in} 1 \.{\dotdot} MAX\_STACK\_SIZE \.{\mapsto}}% \@x{\@s{96.51} [ next \.{\mapsto} NULL ,\, onStack \.{\mapsto} {\FALSE} ,\, data \.{\mapsto} 0 ] ] ,\,}% \@x{\@s{47.76} initialized \.{=} {\FALSE} {\p@semicolon}}% \@x{\@s{47.76} HEAD {\p@semicolon}}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% \ensuremath{CAS}: compare-and-swap }% \@xx{}% \@x{}% \@y{\@s{0}% \ensuremath{CAS} must be a macro. This reflects that it is an assembly instruction }% \@xx{}% \@x{}% \@y{\@s{5.0}% that modifies its arguments. It must not use the call-by-value of a procedure. }% \@xx{}% \@x{}% \@y{\@s{0}% \ensuremath{CAS} is atomic. So, there are no intermediate labels. }% \@xx{}% \@x{ {\p@macro} CAS {\p@lparen} x ,\, y ,\, z {\p@rparen}}% \@x{ {\p@lbrace}}% \@x{\@s{8.2} {\p@if} {\p@lparen} x \.{=} y {\p@rparen} {\p@lbrace}}% \@x{\@s{16.4} x \.{:=} z {\p@semicolon}}% \@y{\@s{0}% swap \ensuremath{y} for \ensuremath{z} as value of \ensuremath{x }}% \@xx{}% \@x{\@s{16.4} retVal [ self ] \.{:=} {\TRUE} {\p@semicolon}}% \@x{\@s{8.2} {\p@rbrace} {\p@else} {\p@lbrace}}% \@x{\@s{21.61} retVal [ self ] \.{:=} {\FALSE} {\p@semicolon}}% \@x{\@s{8.2} {\p@rbrace} {\p@semicolon}}% \@x{ {\p@rbrace}}% \@pvspace{8.0pt}% \@x{ {\p@procedure} pushStack {\p@lparen} elt {\p@rparen}}% \@x{\@s{8.2} {\p@variable} local\_myhead {\p@semicolon}}% \@x{ {\p@lbrace}}% \@x{\@s{8.2} push1\@s{.5}\textrm{:}\@s{3} address [ elt ] . next \.{:=} HEAD {\p@semicolon}}% \@x{\@s{8.2} push2\@s{.5}\textrm{:}\@s{3} {\p@assert} address [ elt ] . onStack \.{=} {\FALSE} {\p@semicolon}}% \@x{\@s{8.2} push3\@s{.5}\textrm{:}\@s{3} address [ elt ] . onStack \.{:=} {\TRUE} {\p@semicolon}}% \@x{\@s{8.2} tryAgainPush\@s{.5}\textrm{:}\@s{3} local\_myhead \.{:=} HEAD {\p@semicolon}}% \@x{\@s{32.8} push5a\@s{.5}\textrm{:}\@s{3}\@s{3.91} address [ elt ] . next \.{:=} local\_myhead {\p@semicolon}}% \@x{\@s{32.8} push5b\@s{.5}\textrm{:}\@s{3}\@s{4.55} CAS ( HEAD ,\, local\_myhead ,\, elt ) {\p@semicolon}}% \@x{\@s{32.8} push5c\@s{.5}\textrm{:}\@s{3}\@s{4.62} {\p@if} {\p@lparen} {\lnot} retVal [ self ] {\p@rparen} {\p@lbrace}}% \@x{\@s{32.8} push5d\@s{.5}\textrm{:}\@s{3}\@s{11.84} {\p@goto} tryAgainPush {\p@semicolon}}% \@x{\@s{74.31} {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} endPush\@s{.5}\textrm{:}\@s{3}\@s{0.29} {\p@return}\@s{3.51} {\p@semicolon}}% \@x{ {\p@rbrace}}% \@pvspace{8.0pt}% \@x{ {\p@procedure} popStack {\p@lparen} {\p@rparen}}% \@x{\@s{8.2} {\p@variable} local\_myhead ,\, reg\_next ,\, elt {\p@semicolon}}% \@x{ {\p@lbrace}}% \@x{\@s{8.2} tryAgainPop\@s{.5}\textrm{:}\@s{3}}% \@x{\@s{20.5} local\_myhead \.{:=} HEAD {\p@semicolon}}% \@x{\@s{8.2} pop1\@s{.5}\textrm{:}\@s{3} {\p@if} {\p@lparen} local\_myhead \.{=} 0 {\p@rparen} {\p@lbrace}}% \@y{\@s{0}% If I believe \ensuremath{HEAD \.{=} 0}, return now. }% \@xx{}% \@x{\@s{8.2} pop1a\@s{.5}\textrm{:}\@s{3}\@s{4.1} retVal [ self ] \.{:=} NULL {\p@semicolon}}% \@x{\@s{8.2} pop1b\@s{.5}\textrm{:}\@s{3}\@s{4.74} {\p@return} {\p@semicolon}}% \@x{\@s{34.93} {\p@rbrace} {\p@semicolon}}% \@pvspace{8.0pt}% \@x{\@s{8.2} pop2\@s{.5}\textrm{:}\@s{3}\@s{5.87} reg\_next \.{:=}\@s{4.1} address [ local\_myhead ] . next {\p@semicolon}}% \@x{\@s{8.2} pop2a\@s{.5}\textrm{:}\@s{3} CAS ( HEAD ,\, local\_myhead ,\, reg\_next ) {\p@semicolon}}% \@x{\@s{8.2} pop2b\@s{.5}\textrm{:}\@s{3}\@s{0.64} {\p@if} {\p@lparen} {\lnot} retVal [ self ] {\p@rparen} {\p@lbrace}}% \@x{\@s{8.2} pop2c\@s{.5}\textrm{:}\@s{3}\@s{8.91} {\p@goto} tryAgainPop {\p@semicolon}}% \@x{\@s{40.80} {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} pop3\@s{.5}\textrm{:}\@s{3} elt \.{:=} local\_myhead {\p@semicolon}}% \@x{\@s{8.2} pop4\@s{.5}\textrm{:}\@s{3} {\p@assert} address [ elt ] . onStack \.{=} {\TRUE} {\p@semicolon}}% \@x{\@s{8.2} pop5\@s{.5}\textrm{:}\@s{3} address [ elt ] . onStack \.{:=} {\FALSE} {\p@semicolon}}% \@x{\@s{8.2} pop6\@s{.5}\textrm{:}\@s{3} retVal [ self ] \.{:=} elt {\p@semicolon}}% \@x{\@s{8.2} endPop\@s{.5}\textrm{:}\@s{3} {\p@return} {\p@semicolon}}% \@x{ {\p@rbrace}}% \@pvspace{8.0pt}% \@x{ {\p@process} {\p@lparen} thread \.{\in} 1 \.{\dotdot} NUM\_THREADS {\p@rparen}}% \@x{\@s{8.2} {\p@variable} my\_set \.{=} \{ \} ,\, myelt ,\,}% \@x{\@s{51.42} init\_thread ,\, iterations \.{=} MAX\_ITER {\p@semicolon}}% \@x{ {\p@lbrace}}% \@x{\@s{8.2} init1\@s{.5}\textrm{:}\@s{3} init\_thread \.{:=} {\CHOOSE} thr \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{:} {\TRUE} {\p@semicolon}}% \@x{\@s{8.2} init2\@s{.5}\textrm{:}\@s{3} {\p@if} {\p@lparen} self \.{=} init\_thread {\p@rparen} {\p@lbrace}}% \@y{\@s{0}% \ensuremath{\.{\slsl}} This thread will initialize global data }% \@xx{}% \@x{\@s{8.2} init4\@s{.5}\textrm{:}\@s{3}\@s{8.2} HEAD \.{:=} 0 {\p@semicolon}}% \@x{\@s{8.2} init5\@s{.5}\textrm{:}\@s{3} {\p@while} {\p@lparen} HEAD \.{<} MAX\_STACK\_SIZE {\p@rparen} {\p@lbrace}}% \@x{\@s{8.2} init6\@s{.5}\textrm{:}\@s{3}\@s{16.4} address [ HEAD\@s{10.83} \.{+} 1 ] \.{:=} [ next \.{\mapsto} HEAD ,\, onStack \.{\mapsto} {\TRUE} ,\, data \.{\mapsto} 1 ] {\p@semicolon}}% \@x{\@s{8.2} init7\@s{.5}\textrm{:}\@s{3}\@s{16.39} HEAD \.{:=} HEAD \.{+} 1 {\p@semicolon}}% \@x{\@s{45.1} {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} init8\@s{.5}\textrm{:}\@s{3}\@s{9.59} initialized \.{:=} {\TRUE} {\p@semicolon}}% \@y{\@s{0}% \ensuremath{\.{\slsl} init\_thread} will set this global var }% \@xx{}% \@x{\@s{35.50} {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} init9\@s{.5}\textrm{:}\@s{3} {\p@await} initialized {\p@semicolon}}% \@y{\@s{0}% \ensuremath{\.{\slsl}} all threads will wait for this }% \@xx{}% \@pvspace{8.0pt}% \@x{\@s{8.2} th1\@s{.5}\textrm{:}\@s{3} {\p@while} {\p@lparen} iterations \.{>} 0 {\p@rparen} {\p@lbrace}}% \@x{\@s{8.2} th2\@s{.5}\textrm{:}\@s{3}\@s{8.2} {\p@either} {\p@lbrace} {\p@if} {\p@lparen} my\_set \.{\neq} \{ \} {\p@rparen} {\p@lbrace}}% \@x{\@s{83.72}}% \@y{\@s{0}% \ensuremath{\.{\slsl}} Set \ensuremath{myelt} at random (non-deterministically) }% \@xx{}% \@x{\@s{8.2} th2a\@s{.5}\textrm{:}\@s{3}\@s{49.17} {\p@with} {\p@lparen} tmp \.{\in} my\_set {\p@rparen} {\p@lbrace} myelt \.{:=} tmp {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} th2b\@s{.5}\textrm{:}\@s{3}\@s{49.81} my\_set \.{:=} my\_set \.{\,\backslash\,} \{ myelt \} {\p@semicolon}}% \@x{\@s{8.2} th2c\@s{.5}\textrm{:}\@s{3}\@s{49.88} {\p@call} pushStack ( myelt ) {\p@semicolon}}% \@x{\@s{61.5} {\p@rbrace} {\p@rbrace}}% \@x{\@s{36.87} {\p@or} {\p@lbrace}}% \@x{\@s{8.2} th3a\@s{.5}\textrm{:}\@s{3}\@s{20.74} {\p@call} popStack ( ) {\p@semicolon}}% \@x{\@s{8.2} th3b\@s{.5}\textrm{:}\@s{3}\@s{21.38} {\p@if} {\p@lparen} retVal [ self ] \.{\neq} NULL {\p@rparen} {\p@lbrace}}% \@x{\@s{8.2} th3c\@s{.5}\textrm{:}\@s{3}\@s{29.65} my\_set \.{:=} my\_set \.{\cup} \{ retVal [ self ] \}}% \@y{\@s{0}% \ensuremath{\.{\slsl}} Add the popped \ensuremath{elt} to \ensuremath{my\_set }}% \@xx{}% \@x{\@s{55.29} {\p@rbrace} {\p@rbrace} {\p@semicolon}}% \@x{\@s{8.2} th4\@s{.5}\textrm{:}\@s{3} iterations \.{:=} iterations \.{-} 1 {\p@semicolon}}% \@x{\@s{8.2} {\p@print} iterations {\p@semicolon}}% \@x{\@s{8.2} {\p@rbrace} {\p@semicolon}}% \@y{\@s{0}% end while }% \@xx{}% \@x{ {\p@rbrace} {\p@semicolon}}% \@y{\@s{0}% end process }% \@xx{}% \@pvspace{8.0pt}% \@x{ {\p@rbrace}}% \@y{\@s{0}% \ensuremath{\.{\,\backslash\,}}* end algorithm }% \@xx{}% \pcalshadingfalse \pcalsymbolsfalse \@x{}% \@y{\@s{0}% BEGIN TRANSLATION }% \@xx{}% \@x{}% \@y{\@s{0}% Procedure variable \ensuremath{local\_myhead} of procedure \ensuremath{pushStack} at line 62 col 12 changed to \ensuremath{local\_myhead\_ }}% \@xx{}% \@x{}% \@y{\@s{0}% Procedure variable \ensuremath{elt} of procedure \ensuremath{popStack} at line 77 col 36 changed to \ensuremath{elt\_ }}% \@xx{}% \@x{ {\CONSTANT} defaultInitValue}% \@x{ {\VARIABLES} retVal ,\, address ,\, initialized ,\, HEAD ,\, pc ,\, stack ,\, elt ,\, local\_myhead\_ ,\,}% \@x{\@s{51.42} local\_myhead ,\, reg\_next ,\, elt\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{51.42} iterations}% \@pvspace{8.0pt}% \@x{ vars \.{\defeq} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, pc ,\, stack ,\, elt ,\, local\_myhead\_ ,\,}% \@x{\@s{41.61} local\_myhead ,\, reg\_next ,\, elt\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{41.61} iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ ProcSet \.{\defeq} ( 1 \.{\dotdot} NUM\_THREADS )}% \@pvspace{8.0pt}% \@x{ Init \.{\defeq}}% \@y{\@s{0}% Global variables }% \@xx{}% \@x{\@s{35.70} \.{\land} retVal \.{=} [ thread \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} NULL ]}% \@x{\@s{35.70} \.{\land} address \.{=} [ addr\@s{1.21} \.{\in} 1 \.{\dotdot} MAX\_STACK\_SIZE \.{\mapsto}}% \@x{\@s{95.56} [ next \.{\mapsto} NULL ,\, onStack \.{\mapsto} {\FALSE} ,\, data \.{\mapsto} 0 ] ]}% \@x{\@s{35.70} \.{\land} initialized \.{=} {\FALSE}}% \@x{\@s{35.70} \.{\land} HEAD \.{=} defaultInitValue}% \@x{\@s{35.70}}% \@y{\@s{0}% Procedure \ensuremath{pushStack }}% \@xx{}% \@x{\@s{35.70} \.{\land} elt \.{=} [ self \.{\in} ProcSet \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70} \.{\land} local\_myhead\_ \.{=} [ self \.{\in} ProcSet \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70}}% \@y{\@s{0}% Procedure \ensuremath{popStack }}% \@xx{}% \@x{\@s{35.70} \.{\land} local\_myhead \.{=} [ self \.{\in} ProcSet \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70} \.{\land} reg\_next \.{=} [ self \.{\in} ProcSet \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70} \.{\land} elt\_ \.{=} [ self \.{\in} ProcSet \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70}}% \@y{\@s{0}% Process thread }% \@xx{}% \@x{\@s{35.70} \.{\land} my\_set \.{=} [ self \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} \{ \} ]}% \@x{\@s{35.70} \.{\land} myelt \.{=} [ self \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70} \.{\land} init\_thread \.{=} [ self \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} defaultInitValue ]}% \@x{\@s{35.70} \.{\land} iterations \.{=} [ self \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{\mapsto} MAX\_ITER ]}% \@x{\@s{35.70} \.{\land} stack \.{=} [ self \.{\in} ProcSet \.{\mapsto} {\langle} {\rangle} ]}% \@x{\@s{35.70} \.{\land} pc \.{=} [ self \.{\in} ProcSet \.{\mapsto}\@w{init1} ]}% \@pvspace{8.0pt}% \@x{ push1 ( self ) \.{\defeq} \.{\land} pc [ self ]\@s{3.69} \.{=}\@w{push1}}% \@x{\@s{68.54} \.{\land} address \.{'} \.{=} [ address {\EXCEPT} {\bang} [ elt [ self ] ] . next \.{=} HEAD ]}% \@x{\@s{68.54} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push2} ]}% \@x{\@s{68.54} \.{\land} {\UNCHANGED} {\langle} retVal ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{142.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{142.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push2 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{push2}}% \@x{\@s{68.54} \.{\land} Assert ( address [ elt [ self ] ] . onStack \.{=} {\FALSE} ,\,}% \@x{\@s{112.24}\@w{Failure\ of\ assertion\ at\ line\ 65,\ column\ 10.} )}% \@x{\@s{68.54} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push3} ]}% \@x{\@s{68.54} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{142.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{142.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push3 ( self ) \.{\defeq} \.{\land} pc [ self ]\@s{3.69} \.{=}\@w{push3}}% \@x{\@s{68.54} \.{\land} address \.{'} \.{=} [ address {\EXCEPT} {\bang} [ elt [ self ] ] . onStack \.{=} {\TRUE} ]}% \@x{\@s{68.54} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{tryAgainPush} ]}% \@x{\@s{68.54} \.{\land} {\UNCHANGED} {\langle} retVal ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{142.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{142.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ tryAgainPush ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{tryAgainPush}}% \@x{\@s{102.93} \.{\land} local\_myhead\_ \.{'} \.{=} [ local\_myhead\_ {\EXCEPT} {\bang} [ self ] \.{=} HEAD ]}% \@x{\@s{102.93} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push5a} ]}% \@x{\@s{102.93} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\,}% \@x{\@s{176.51} stack ,\, elt ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{176.51} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push5a ( self )\@s{0.26} \.{\defeq} \.{\land} pc [ self ]\@s{3.69} \.{=}\@w{push5a}}% \@x{\@s{74.68} \.{\land} address \.{'} \.{=} [ address {\EXCEPT} {\bang} [ elt [ self ] ] . next \.{=} local\_myhead\_ [ self ] ]}% \@x{\@s{74.68} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push5b} ]}% \@x{\@s{74.68} \.{\land} {\UNCHANGED} {\langle} retVal ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{148.27} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{148.27} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push5b ( self )\@s{0.91} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{push5b}}% \@x{\@s{74.68} \.{\land} {\IF} HEAD \.{=} local\_myhead\_ [ self ]}% \@x{\@s{97.95} \.{\THEN} \.{\land} HEAD \.{'} \.{=} elt [ self ]}% \@x{\@s{129.26} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} {\TRUE} ]}% \@x{\@s{97.95} \.{\ELSE} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} {\FALSE} ]}% \@x{\@s{129.26} \.{\land} HEAD \.{'} \.{=} HEAD}% \@x{\@s{74.68} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push5c} ]}% \@x{\@s{74.68} \.{\land} {\UNCHANGED} {\langle} address ,\, initialized ,\, stack ,\, elt ,\,}% \@x{\@s{148.27} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{148.27} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push5c ( self )\@s{0.97} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{push5c}}% \@x{\@s{74.68} \.{\land} {\IF} {\lnot} retVal [ self ]}% \@x{\@s{97.95} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push5d} ]}% \@x{\@s{97.95} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{endPush} ]}% \@x{\@s{74.68} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{148.27} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{148.27} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ push5d ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{push5d}}% \@x{\@s{74.68} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{tryAgainPush} ]}% \@x{\@s{74.68} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{148.27} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{148.27} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ endPush ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{endPush}}% \@x{\@s{80.54} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . pc ]}% \@x{\@s{80.54} \.{\land} local\_myhead\_ \.{'} \.{=} [ local\_myhead\_ {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . local\_myhead\_ ]}% \@x{\@s{80.54} \.{\land} elt \.{'} \.{=} [ elt {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . elt ]}% \@x{\@s{80.54} \.{\land} stack \.{'} \.{=} [ stack {\EXCEPT} {\bang} [ self ] \.{=} Tail ( stack [ self ] ) ]}% \@x{\@s{80.54} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\,}% \@x{\@s{154.13} local\_myhead ,\, reg\_next ,\, elt\_ ,\, my\_set ,\, myelt ,\,}% \@x{\@s{154.13} init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pushStack ( self ) \.{\defeq} push1 ( self ) \.{\lor} push2 ( self ) \.{\lor} push3 ( self )}% \@x{\@s{99.40} \.{\lor} tryAgainPush ( self ) \.{\lor} push5a ( self ) \.{\lor} push5b ( self )}% \@x{\@s{99.40} \.{\lor} push5c ( self ) \.{\lor} push5d ( self ) \.{\lor} endPush ( self )}% \@pvspace{8.0pt}% \@x{ tryAgainPop ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{tryAgainPop}}% \@x{\@s{98.44} \.{\land} local\_myhead \.{'} \.{=} [ local\_myhead {\EXCEPT} {\bang} [ self ] \.{=} HEAD ]}% \@x{\@s{98.44} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop1} ]}% \@x{\@s{98.44} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\,}% \@x{\@s{172.03} elt ,\, local\_myhead\_ ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{172.03} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop1 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop1}}% \@x{\@s{63.55} \.{\land} {\IF} local\_myhead [ self ] \.{=} 0}% \@x{\@s{86.81} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop1a} ]}% \@x{\@s{86.81} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop2} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop1a ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop1a}}% \@x{\@s{69.42} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} NULL ]}% \@x{\@s{69.42} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop1b} ]}% \@x{\@s{69.42} \.{\land} {\UNCHANGED} {\langle} address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{143.01} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{143.01} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop1b ( self )\@s{0.64} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop1b}}% \@x{\@s{69.42} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . pc ]}% \@x{\@s{69.42} \.{\land} local\_myhead \.{'} \.{=} [ local\_myhead {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . local\_myhead ]}% \@x{\@s{69.42} \.{\land} reg\_next \.{'} \.{=} [ reg\_next {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . reg\_next ]}% \@x{\@s{69.42} \.{\land} elt\_ \.{'} \.{=} [ elt\_ {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . elt\_ ]}% \@x{\@s{69.42} \.{\land} stack \.{'} \.{=} [ stack {\EXCEPT} {\bang} [ self ] \.{=} Tail ( stack [ self ] ) ]}% \@x{\@s{69.42} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, elt ,\,}% \@x{\@s{143.01} local\_myhead\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{143.01} iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop2 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop2}}% \@x{\@s{63.55} \.{\land} reg\_next \.{'} \.{=} [ reg\_next {\EXCEPT} {\bang} [ self ] \.{=} address [ local\_myhead [ self ] ] . next ]}% \@x{\@s{63.55} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop2a} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, elt\_ ,\, my\_set ,\, myelt ,\,}% \@x{\@s{137.13} init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop2a ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop2a}}% \@x{\@s{69.42} \.{\land} {\IF} HEAD \.{=} local\_myhead [ self ]}% \@x{\@s{92.69} \.{\THEN} \.{\land} HEAD \.{'} \.{=} reg\_next [ self ]}% \@x{\@s{124.00} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} {\TRUE} ]}% \@x{\@s{92.69} \.{\ELSE} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} {\FALSE} ]}% \@x{\@s{124.00} \.{\land} HEAD \.{'} \.{=} HEAD}% \@x{\@s{69.42} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop2b} ]}% \@x{\@s{69.42} \.{\land} {\UNCHANGED} {\langle} address ,\, initialized ,\, stack ,\, elt ,\, local\_myhead\_ ,\,}% \@x{\@s{143.01} local\_myhead ,\, reg\_next ,\, elt\_ ,\, my\_set ,\, myelt ,\,}% \@x{\@s{143.01} init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop2b ( self )\@s{0.64} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop2b}}% \@x{\@s{69.42} \.{\land} {\IF} {\lnot} retVal [ self ]}% \@x{\@s{92.69} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop2c} ]}% \@x{\@s{92.69} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop3} ]}% \@x{\@s{69.42} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{143.01} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{143.01} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop2c ( self )\@s{0.71} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop2c}}% \@x{\@s{69.42} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{tryAgainPop} ]}% \@x{\@s{69.42} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{143.01} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{143.01} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop3 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop3}}% \@x{\@s{63.55} \.{\land} elt\_ \.{'} \.{=} [ elt\_ {\EXCEPT} {\bang} [ self ] \.{=} local\_myhead [ self ] ]}% \@x{\@s{63.55} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop4} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, my\_set ,\,}% \@x{\@s{137.13} myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop4 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop4}}% \@x{\@s{63.55} \.{\land} Assert ( address [ elt\_ [ self ] ] . onStack \.{=} {\TRUE} ,\,}% \@x{\@s{107.24}\@w{Failure\ of\ assertion\ at\ line\ 92,\ column\ 9.} )}% \@x{\@s{63.55} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop5} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop5 ( self ) \.{\defeq} \.{\land} pc [ self ]\@s{3.69} \.{=}\@w{pop5}}% \@x{\@s{63.55} \.{\land} address \.{'} \.{=} [ address {\EXCEPT} {\bang} [ elt\_ [ self ] ] . onStack \.{=} {\FALSE} ]}% \@x{\@s{63.55} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{pop6} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} retVal ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ pop6 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{pop6}}% \@x{\@s{63.55} \.{\land} retVal \.{'} \.{=} [ retVal {\EXCEPT} {\bang} [ self ] \.{=} elt\_ [ self ] ]}% \@x{\@s{63.55} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{endPop} ]}% \@x{\@s{63.55} \.{\land} {\UNCHANGED} {\langle} address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.13} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.13} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ endPop ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{endPop}}% \@x{\@s{76.06} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . pc ]}% \@x{\@s{76.06} \.{\land} local\_myhead \.{'} \.{=} [ local\_myhead {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . local\_myhead ]}% \@x{\@s{76.06} \.{\land} reg\_next \.{'} \.{=} [ reg\_next {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . reg\_next ]}% \@x{\@s{76.06} \.{\land} elt\_ \.{'} \.{=} [ elt\_ {\EXCEPT} {\bang} [ self ] \.{=} Head ( stack [ self ] ) . elt\_ ]}% \@x{\@s{76.06} \.{\land} stack \.{'} \.{=} [ stack {\EXCEPT} {\bang} [ self ] \.{=} Tail ( stack [ self ] ) ]}% \@x{\@s{76.06} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, elt ,\,}% \@x{\@s{149.65} local\_myhead\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{149.65} iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ popStack ( self ) \.{\defeq} tryAgainPop ( self ) \.{\lor} pop1 ( self ) \.{\lor} pop1a ( self )}% \@x{\@s{94.55} \.{\lor} pop1b ( self )\@s{6.25} \.{\lor} pop2 ( self ) \.{\lor} pop2a ( self )}% \@x{\@s{94.55} \.{\lor} pop2b ( self )\@s{6.25} \.{\lor} pop2c ( self ) \.{\lor} pop3 ( self )}% \@x{\@s{94.55} \.{\lor} pop4 ( self ) \.{\lor} pop5 ( self ) \.{\lor} pop6 ( self )}% \@x{\@s{94.55} \.{\lor} endPop ( self )}% \@pvspace{8.0pt}% \@x{ init1 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init1}}% \@x{\@s{64.12} \.{\land} init\_thread \.{'} \.{=} [ init\_thread {\EXCEPT} {\bang} [ self ] \.{=} {\CHOOSE} thr \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{:} {\TRUE} ]}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init2} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init2 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init2}}% \@x{\@s{64.12} \.{\land} {\IF} self \.{=} init\_thread [ self ]}% \@x{\@s{87.38} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init4} ]}% \@x{\@s{87.38} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init9} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init4 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init4}}% \@x{\@s{64.12} \.{\land} HEAD \.{'} \.{=} 0}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init5} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init5 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init5}}% \@x{\@s{64.12} \.{\land} {\IF} HEAD \.{<} MAX\_STACK\_SIZE}% \@x{\@s{87.38} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init6} ]}% \@x{\@s{87.38} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init8} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init6 ( self ) \.{\defeq} \.{\land} pc [ self ]\@s{3.69} \.{=}\@w{init6}}% \@x{\@s{64.12} \.{\land} address \.{'} \.{=} [ address {\EXCEPT} {\bang} [ HEAD \.{+} 1 ] \.{=} [ next \.{\mapsto} HEAD ,\, onStack \.{\mapsto} {\TRUE} ,\, data \.{\mapsto} 1 ] ]}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init7} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init7 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init7}}% \@x{\@s{64.12} \.{\land} HEAD \.{'} \.{=} HEAD \.{+} 1}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init5} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init8 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init8}}% \@x{\@s{64.12} \.{\land} initialized \.{'} \.{=} {\TRUE}}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{init9} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ init9 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{init9}}% \@x{\@s{64.12} \.{\land} initialized}% \@x{\@s{64.12} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th1} ]}% \@x{\@s{64.12} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{137.71} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{137.71} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th1 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th1}}% \@x{\@s{57.29} \.{\land} {\IF} iterations [ self ] \.{>} 0}% \@x{\@s{80.56} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th2} ]}% \@x{\@s{80.56} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{Done} ]}% \@x{\@s{57.29} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{130.88} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{130.88} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th2 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th2}}% \@x{\@s{57.29} \.{\land} \.{\lor} \.{\land} {\IF} my\_set [ self ] \.{\neq} \{ \}}% \@x{\@s{102.78} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th2a} ]}% \@x{\@s{102.78} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th4} ]}% \@x{\@s{68.40} \.{\lor} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th3a} ]}% \@x{\@s{57.29} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{130.88} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{130.88} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th2a ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th2a}}% \@x{\@s{63.17} \.{\land} \E\, tmp \.{\in} my\_set [ self ] \.{:}}% \@x{\@s{82.48} myelt \.{'} \.{=} [ myelt {\EXCEPT} {\bang} [ self ] \.{=} tmp ]}% \@x{\@s{63.17} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th2b} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{136.76} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{136.76} my\_set ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th2b ( self )\@s{0.64} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th2b}}% \@x{\@s{63.17} \.{\land} my\_set \.{'} \.{=} [ my\_set {\EXCEPT} {\bang} [ self ] \.{=} my\_set [ self ] \.{\,\backslash\,} \{ myelt [ self ] \} ]}% \@x{\@s{63.17} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th2c} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{136.76} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{136.76} myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th2c ( self )\@s{0.71} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th2c}}% \@x{\@s{63.17} \.{\land} \.{\land} elt \.{'} \.{=} [ elt {\EXCEPT} {\bang} [ self ] \.{=} myelt [ self ] ]}% \@x{\@s{74.28} \.{\land} stack \.{'} \.{=} [ stack {\EXCEPT} {\bang} [ self ] \.{=} {\langle} [ procedure \.{\mapsto}\@s{4.1}\@w{pushStack} ,\,}% \@x{\@s{238.48} pc\@s{31.36} \.{\mapsto}\@s{4.10}\@w{th4} ,\,}% \@x{\@s{238.48} local\_myhead\_ \.{\mapsto}\@s{4.1} local\_myhead\_ [ self ] ,\,}% \@x{\@s{238.48} elt\@s{24.59} \.{\mapsto}\@s{4.1} elt [ self ] ] {\rangle}}% \@x{\@s{235.92} \.{\circ} stack [ self ] ]}% \@x{\@s{63.17} \.{\land} local\_myhead\_ \.{'} \.{=} [ local\_myhead\_ {\EXCEPT} {\bang} [ self ] \.{=} defaultInitValue ]}% \@x{\@s{63.17} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{push1} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, local\_myhead ,\,}% \@x{\@s{136.76} reg\_next ,\, elt\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{136.76} iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th3a ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th3a}}% \@x{\@s{63.17} \.{\land} stack \.{'} \.{=} [ stack {\EXCEPT} {\bang} [ self ] \.{=} {\langle} [ procedure \.{\mapsto}\@s{4.1}\@w{popStack} ,\,}% \@x{\@s{227.37} pc\@s{31.36} \.{\mapsto}\@s{4.10}\@w{th3b} ,\,}% \@x{\@s{227.37} local\_myhead \.{\mapsto}\@s{4.1} local\_myhead [ self ] ,\,}% \@x{\@s{227.37} reg\_next\@s{4.1} \.{\mapsto}\@s{4.1} reg\_next [ self ] ,\,}% \@x{\@s{227.37} elt\_\@s{25.08} \.{\mapsto}\@s{4.10} elt\_ [ self ] ] {\rangle}}% \@x{\@s{224.81} \.{\circ} stack [ self ] ]}% \@x{\@s{63.17} \.{\land} local\_myhead \.{'} \.{=} [ local\_myhead {\EXCEPT} {\bang} [ self ] \.{=} defaultInitValue ]}% \@x{\@s{63.17} \.{\land} reg\_next \.{'} \.{=} [ reg\_next {\EXCEPT} {\bang} [ self ] \.{=} defaultInitValue ]}% \@x{\@s{63.17} \.{\land} elt\_ \.{'} \.{=} [ elt\_ {\EXCEPT} {\bang} [ self ] \.{=} defaultInitValue ]}% \@x{\@s{63.17} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{tryAgainPop} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, elt ,\,}% \@x{\@s{136.76} local\_myhead\_ ,\, my\_set ,\, myelt ,\, init\_thread ,\,}% \@x{\@s{136.76} iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th3b ( self )\@s{0.64} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th3b}}% \@x{\@s{63.17} \.{\land} {\IF} retVal [ self ] \.{\neq} NULL}% \@x{\@s{86.44} \.{\THEN} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th3c} ]}% \@x{\@s{86.44} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th4} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{136.76} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{136.76} my\_set ,\, myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th3c ( self )\@s{0.71} \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th3c}}% \@x{\@s{63.17} \.{\land} my\_set \.{'} \.{=} [ my\_set {\EXCEPT} {\bang} [ self ] \.{=} my\_set [ self ] \.{\cup} \{ retVal [ self ] \} ]}% \@x{\@s{63.17} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th4} ]}% \@x{\@s{63.17} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{136.76} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{136.76} myelt ,\, init\_thread ,\, iterations {\rangle}}% \@pvspace{8.0pt}% \@x{ th4 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{th4}}% \@x{\@s{57.29} \.{\land} iterations \.{'} \.{=} [ iterations {\EXCEPT} {\bang} [ self ] \.{=} iterations [ self ] \.{-} 1 ]}% \@x{\@s{57.29} \.{\land} PrintT ( iterations \.{'} [ self ] )}% \@x{\@s{57.29} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ] \.{=}\@w{th1} ]}% \@x{\@s{57.29} \.{\land} {\UNCHANGED} {\langle} retVal ,\, address ,\, initialized ,\, HEAD ,\, stack ,\, elt ,\,}% \@x{\@s{130.88} local\_myhead\_ ,\, local\_myhead ,\, reg\_next ,\, elt\_ ,\,}% \@x{\@s{130.88} my\_set ,\, myelt ,\, init\_thread {\rangle}}% \@pvspace{8.0pt}% \@x{ thread ( self ) \.{\defeq} init1 ( self ) \.{\lor} init2 ( self ) \.{\lor} init4 ( self ) \.{\lor} init5 ( self )}% \@x{\@s{82.88} \.{\lor} init6 ( self ) \.{\lor} init7 ( self ) \.{\lor} init8 ( self )}% \@x{\@s{82.88} \.{\lor} init9 ( self ) \.{\lor} th1 ( self )\@s{3.57} \.{\lor} th2 ( self ) \.{\lor} th2a ( self )}% \@x{\@s{82.88} \.{\lor} th2b ( self ) \.{\lor} th2c ( self ) \.{\lor} th3a ( self ) \.{\lor} th3b ( self )}% \@x{\@s{82.88} \.{\lor} th3c ( self )\@s{0.06} \.{\lor} th4 ( self )}% \@pvspace{8.0pt}% \@x{ Next \.{\defeq} ( \E\, self \.{\in} ProcSet \.{:} pushStack ( self ) \.{\lor} popStack ( self ) )}% \@x{\@s{47.82} \.{\lor} ( \E\, self \.{\in} 1 \.{\dotdot} NUM\_THREADS \.{:} thread ( self ) )}% \@x{\@s{47.82} \.{\lor}}% \@y{\@s{0}% Disjunct to prevent deadlock on termination }% \@xx{}% \@x{\@s{58.93} ( ( \A\, self \.{\in} ProcSet \.{:} pc [ self ] \.{=}\@w{Done} ) \.{\land} {\UNCHANGED} vars )}% \@pvspace{8.0pt}% \@x{ Spec\@s{1.46} \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ vars}}% \@pvspace{8.0pt}% \@x{ Termination \.{\defeq} {\Diamond} ( \A\, self \.{\in} ProcSet \.{:} pc [ self ] \.{=}\@w{Done} )}% \@pvspace{8.0pt}% \@x{}% \@y{\@s{0}% END TRANSLATION }% \@xx{}% \@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{Apr} 11 15:49:50 \ensuremath{EDT} 2019 by gene \end{cpar}% \begin{cpar}{0}{F}{F}{0}{0}{}% \ensuremath{\.{\,\backslash\,}}* Last modified Sun \ensuremath{Oct} 22 06:26:25 \ensuremath{EDT} 2017 by celestekostopulos-cooperman \end{cpar}% \begin{cpar}{0}{F}{F}{0}{0}{}% \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Fri} \ensuremath{Oct} 20 22:08:53 \ensuremath{EDT} 2017 by celestekostopulos-cooperman \end{cpar}% \end{lcom}% \end{document}