diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiter.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiter.pdf index 86d3227..fe0f48f 100644 Binary files a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiter.pdf and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiter.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.pdf index 756d67e..af16168 100644 Binary files a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.pdf and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.tla index 19f4c26..6c01c01 100644 --- a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.tla +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.tla @@ -1,14 +1,11 @@ ---------------------------- MODULE AbsJupiterH ---------------------------- -(* -AbsJupiter with a history of all list states across the system. -*) -EXTENDS AbsJupiter +EXTENDS AbsJupiter ------------------------------------------------------------- VARIABLE list varsH == <> - -TypeOKH == TypeOK /\ (list \subseteq List) ------------------------------------------------------------- +TypeOKH == TypeOK /\ (list \subseteq List) + InitH == Init /\ list = {InitState} DoH(c) == Do(c) /\ list' = list \cup {state'[c]} @@ -36,5 +33,5 @@ WLSpec == \* The weak list specification THEOREM SpecH => WLSpec ============================================================================= \* Modification History -\* Last modified Mon Dec 31 20:38:09 CST 2018 by hengxin -\* Created Sat Dec 15 09:00:46 CST 2018 by hengxin +\* Last modified Tue Jan 01 10:22:57 CST 2019 by hengxin +\* Created Sat Dec 15 09:00:46 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/.project b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/.project index 9c64e4d..510286d 100755 --- a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/.project +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/.project @@ -40,6 +40,11 @@ 1 PARENT-1-PROJECT_LOC/JupiterCtx.tla + + JupiterH.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla + JupiterInterface.tla 1 diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.pdf new file mode 100644 index 0000000..fe0f48f Binary files /dev/null and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.tex b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.tex new file mode 100644 index 0000000..b143ff9 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiter.tex @@ -0,0 +1,1137 @@ +\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{\makebox[0pt][r]{\scriptsize 1\hspace{1em}}}\moduleLeftDash\@xx{ + {\MODULE} AbsJupiter}\moduleRightDash\@xx{}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + Abstract \ensuremath{Jupiter}, inspired by the \ensuremath{COT} algorithm + proposed by Sun and Sun; see \ensuremath{TPDS\.{'}}2009. +\end{cpar}% +\end{lcom}% +\@x{\makebox[0pt][r]{\scriptsize 5\hspace{1em}} {\EXTENDS} JupiterSerial}% +\@x{\makebox[0pt][r]{\scriptsize 6\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 7\hspace{1em}} {\VARIABLES}}% +\@x{\makebox[0pt][r]{\scriptsize 8\hspace{1em}}\@s{16.4} copss\@s{8.2}}% +\@y{\@s{0}% + \ensuremath{copss[r]}: the state space (\ensuremath{i.e}., a set) of Cops + maintained at replia \ensuremath{r \.{\in} Replica +}}% +\@xx{}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 10\hspace{1em}} vars \.{\defeq} {\langle} + intVars ,\, ctxVars ,\, serialVars ,\, copss {\rangle}}% +\@x{\makebox[0pt][r]{\scriptsize 11\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 12\hspace{1em}} TypeOK \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 13\hspace{1em}}\@s{16.4} \.{\land}\@s{9.74} + TypeOKInt}% + \@x{\makebox[0pt][r]{\scriptsize 14\hspace{1em}}\@s{16.4} \.{\land}\@s{9.74} + TypeOKCtx}% + \@x{\makebox[0pt][r]{\scriptsize 15\hspace{1em}}\@s{16.4} \.{\land}\@s{9.74} + TypeOKSerial}% + \@x{\makebox[0pt][r]{\scriptsize 16\hspace{1em}}\@s{16.4} \.{\land}\@s{9.74} + Comm ( Cop ) {\bang} TypeOK}% + \@x{\makebox[0pt][r]{\scriptsize 17\hspace{1em}}\@s{16.4} \.{\land}\@s{9.74} + copss \.{\in} [ Replica \.{\rightarrow} {\SUBSET} Cop ]}% +\@x{\makebox[0pt][r]{\scriptsize 18\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 19\hspace{1em}} Init \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 20\hspace{1em}}\@s{16.4} \.{\land} InitInt}% +\@x{\makebox[0pt][r]{\scriptsize 21\hspace{1em}}\@s{16.4} \.{\land} InitCtx}% + \@x{\makebox[0pt][r]{\scriptsize 22\hspace{1em}}\@s{16.4} \.{\land} + InitSerial}% + \@x{\makebox[0pt][r]{\scriptsize 23\hspace{1em}}\@s{16.4} \.{\land} Comm ( + Cop ) {\bang} Init}% + \@x{\makebox[0pt][r]{\scriptsize 24\hspace{1em}}\@s{16.4} \.{\land} copss + \.{=} [ r \.{\in} Replica \.{\mapsto} \{ \} ]}% +\@x{\makebox[0pt][r]{\scriptsize 25\hspace{1em}}}\midbar\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 26\hspace{1em}} {\RECURSIVE} xForm ( \_ ,\, + \_ )}% + \@x{\makebox[0pt][r]{\scriptsize 27\hspace{1em}} xForm ( cop ,\, r ) + \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 28\hspace{1em}}\@s{16.4} \.{\LET} ctxDiff + \.{\defeq} ds [ r ] \.{\,\backslash\,} cop . ctx\@s{4.1}}% +\@y{\@s{0}% + \ensuremath{{\THEOREM}}: \ensuremath{cop.ctx \.{\subseteq} ds[r] +}}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 29\hspace{1em}}\@s{36.79} {\RECURSIVE} + xFormHelper ( \_ ,\, \_ ,\, \_ )}% + \@x{\makebox[0pt][r]{\scriptsize 30\hspace{1em}}\@s{40.89} xFormHelper ( coph + ,\, ctxDiffh ,\, copssr ) \.{\defeq}}% +\@y{\@s{0}% + \ensuremath{copssr}: state space generated during transformation +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 31\hspace{1em}}\@s{57.29} {\IF} ctxDiffh + \.{=} \{ \} \.{\THEN} [ xcop \.{\mapsto} coph ,\, xcopss \.{\mapsto} copssr + ]}% + \@x{\makebox[0pt][r]{\scriptsize 32\hspace{1em}}\@s{57.29} \.{\ELSE} \.{\LET} + foph \.{\defeq} {\CHOOSE} op \.{\in} ctxDiffh \.{:}}% +\@y{\@s{0}% + the first \ensuremath{op} in serial +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 33\hspace{1em}}\@s{159.36} \A\, opprime + \.{\in} ctxDiffh \.{\,\backslash\,} \{ op \} \.{:} tb ( op ,\, opprime ,\, + serial [ r ] )}% + \@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}\@s{109.01} fcophDict + \.{\defeq} \{ op \.{\in} copssr \.{:} op . oid \.{=} foph \.{\land} op . ctx + \.{=} coph . ctx \}}% + \@x{\makebox[0pt][r]{\scriptsize 35\hspace{1em}}\@s{109.01} fcoph\@s{1.57} + \.{\defeq} {\CHOOSE} op \.{\in} fcophDict \.{:} {\TRUE}}% +\@y{\@s{0}% + \ensuremath{{\THEOREM}}: \ensuremath{Cardinality(fophDict) \.{=} 1 +}}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 36\hspace{1em}}\@s{109.01} xcoph \.{\defeq} + COT ( coph ,\, fcoph )}% + \@x{\makebox[0pt][r]{\scriptsize 37\hspace{1em}}\@s{113.11} xfcoph \.{\defeq} + COT ( fcoph ,\, coph )}% + \@x{\makebox[0pt][r]{\scriptsize 38\hspace{1em}}\@s{92.71} \.{\IN} + xFormHelper ( xcoph ,\, ctxDiffh \.{\,\backslash\,} \{ foph \} ,\, copssr + \.{\cup} \{ xcoph ,\, xfcoph \} )}% + \@x{\makebox[0pt][r]{\scriptsize 39\hspace{1em}}\@s{20.5} \.{\IN} xFormHelper + ( cop ,\, ctxDiff ,\, copss [ r ] )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 41\hspace{1em}} Perform ( cop ,\, r ) + \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 42\hspace{1em}}\@s{16.4} \.{\LET} xform + \.{\defeq} xForm ( cop ,\, r )\@s{4.1}}% +\@y{\@s{0}% + [\ensuremath{xcop}, \ensuremath{xcopss}] +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 43\hspace{1em}}\@s{20.5} \.{\IN} \.{\land} + state \.{'}\@s{2.11} \.{=} [ state {\EXCEPT} {\bang} [ r ]\@s{2.11} \.{=} + Apply ( xform . xcop . op ,\, @ ) ]}% + \@x{\makebox[0pt][r]{\scriptsize 44\hspace{1em}}\@s{40.89} \.{\land} copss + \.{'} \.{=} [ copss {\EXCEPT} {\bang} [ r ] \.{=} xform . xcopss \.{\cup} \{ + cop \} ]}% +\@x{\makebox[0pt][r]{\scriptsize 45\hspace{1em}}}\midbar\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 46\hspace{1em}} DoOp ( c ,\, op )\@s{5.43} + \.{\defeq}}% +\@y{\@s{0}% + Client \ensuremath{c \.{\in} Client} processes a locally generated operation + \ensuremath{op}. +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 47\hspace{1em}}\@s{26.06} \.{\LET} cop + \.{\defeq} [ op \.{\mapsto} op ,\, oid \.{\mapsto} [ c \.{\mapsto} c ,\, seq + \.{\mapsto} cseq \.{'} [ c ] ] ,\, ctx \.{\mapsto} ds [ c ] ]}% + \@x{\makebox[0pt][r]{\scriptsize 48\hspace{1em}}\@s{30.16} \.{\IN} \.{\land} + Perform ( cop ,\, c )}% + \@x{\makebox[0pt][r]{\scriptsize 49\hspace{1em}}\@s{50.56} \.{\land} Comm ( + Cop ) {\bang} CSend ( cop )}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 51\hspace{1em}} Do ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 52\hspace{1em}}\@s{22.34} \.{\land} DoCtx ( + c )}% + \@x{\makebox[0pt][r]{\scriptsize 53\hspace{1em}}\@s{22.34} \.{\land} DoSerial + ( c )}% + \@x{\makebox[0pt][r]{\scriptsize 54\hspace{1em}}\@s{22.34} \.{\land} DoInt ( + DoOp ,\, c )}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 56\hspace{1em}} Rev ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 57\hspace{1em}}\@s{20.94} \.{\land} Comm ( + Cop ) {\bang} CRev ( c )}% + \@x{\makebox[0pt][r]{\scriptsize 58\hspace{1em}}\@s{20.94} \.{\land} Perform + ( Head ( cincoming [ c ] ) ,\, c )}% + \@x{\makebox[0pt][r]{\scriptsize 59\hspace{1em}}\@s{20.94} \.{\land} + RevSerial ( c )}% + \@x{\makebox[0pt][r]{\scriptsize 60\hspace{1em}}\@s{20.94} \.{\land} RevCtx ( + c )}% + \@x{\makebox[0pt][r]{\scriptsize 61\hspace{1em}}\@s{20.94} \.{\land} RevInt ( + c )}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 63\hspace{1em}} SRev \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 64\hspace{1em}}\@s{16.4} \.{\land} Comm ( + Cop ) {\bang} SRev}% + \@x{\makebox[0pt][r]{\scriptsize 65\hspace{1em}}\@s{16.4} \.{\land} \.{\LET} + cop \.{\defeq} Head ( sincoming )}% + \@x{\makebox[0pt][r]{\scriptsize 66\hspace{1em}}\@s{31.61} \.{\IN} \.{\land} + Perform ( cop ,\, Server )}% + \@x{\makebox[0pt][r]{\scriptsize 67\hspace{1em}}\@s{52.01} \.{\land} Comm ( + Cop ) {\bang} SSendSame ( cop . oid . c ,\, cop )}% + \@x{\makebox[0pt][r]{\scriptsize 68\hspace{1em}}\@s{16.4} \.{\land} + SRevSerial}% +\@x{\makebox[0pt][r]{\scriptsize 69\hspace{1em}}\@s{16.4} \.{\land} SRevCtx}% +\@x{\makebox[0pt][r]{\scriptsize 70\hspace{1em}}\@s{16.4} \.{\land} SRevInt}% +\@x{\makebox[0pt][r]{\scriptsize 71\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 72\hspace{1em}} Next \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 73\hspace{1em}}\@s{16.4} \.{\lor} \E\, c + \.{\in} Client \.{:} Do ( c ) \.{\lor} Rev ( c )}% +\@x{\makebox[0pt][r]{\scriptsize 74\hspace{1em}}\@s{16.4} \.{\lor} SRev}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 76\hspace{1em}} Fairness \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 77\hspace{1em}}\@s{16.4} {\WF}_{ vars} ( + SRev \.{\lor} \E\, c \.{\in} Client \.{:} Rev ( c ) )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 79\hspace{1em}} Spec \.{\defeq} Init + \.{\land} {\Box} [ Next ]_{ vars}}% +\@y{\@s{0}% + \ensuremath{\.{\land} Fairness +}}% +\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 80\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 81\hspace{1em}} Compactness \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 82\hspace{1em}}\@s{16.4} Comm ( Cop ) + {\bang} EmptyChannel \.{\implies} Cardinality ( Range ( copss ) ) \.{=} 1}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 84\hspace{1em}} {\THEOREM} Spec \.{\implies} + Compactness}% +\@x{\makebox[0pt][r]{\scriptsize 85\hspace{1em}}}\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{Mon} + \ensuremath{Dec} 31 20:27:49 \ensuremath{CST} 2018 by \ensuremath{hengxin +}% +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Wed} \ensuremath{Dec} 05 + 19:55:52 \ensuremath{CST} 2018 by \ensuremath{hengxin +}% +\end{cpar}% +\end{lcom}% +\end{document} diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.pdf index 756d67e..af16168 100755 Binary files a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.pdf and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.tex b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.tex index ee189b0..1ee3b4d 100755 --- a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.tex +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/AbsJupiterH.tex @@ -941,75 +941,70 @@ \setboolean{shading}{true} \@x{\makebox[0pt][r]{\scriptsize 1\hspace{1em}}}\moduleLeftDash\@xx{ {\MODULE} AbsJupiterH}\moduleRightDash\@xx{}% -\begin{lcom}{0}% -\begin{cpar}{0}{F}{F}{0}{0}{}% -\ensuremath{AbsJupiter} with a history of all list states across the system. -\end{cpar}% -\end{lcom}% -\@x{\makebox[0pt][r]{\scriptsize 5\hspace{1em}} {\EXTENDS} AbsJupiter}% -\@x{\makebox[0pt][r]{\scriptsize 6\hspace{1em}}}\midbar\@xx{}% -\@x{\makebox[0pt][r]{\scriptsize 7\hspace{1em}} {\VARIABLE} list}% - \@x{\makebox[0pt][r]{\scriptsize 8\hspace{1em}} varsH \.{\defeq} {\langle} +\@x{\makebox[0pt][r]{\scriptsize 2\hspace{1em}} {\EXTENDS} AbsJupiter}% +\@x{\makebox[0pt][r]{\scriptsize 3\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 4\hspace{1em}} {\VARIABLE} list}% + \@x{\makebox[0pt][r]{\scriptsize 5\hspace{1em}} varsH \.{\defeq} {\langle} vars ,\, list {\rangle}}% -\@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 10\hspace{1em}} TypeOKH \.{\defeq} TypeOK +\@x{\makebox[0pt][r]{\scriptsize 6\hspace{1em}}}\midbar\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 7\hspace{1em}} TypeOKH \.{\defeq} TypeOK \.{\land} ( list \.{\subseteq} List )}% -\@x{\makebox[0pt][r]{\scriptsize 11\hspace{1em}}}\midbar\@xx{}% - \@x{\makebox[0pt][r]{\scriptsize 12\hspace{1em}} InitH \.{\defeq} Init +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 9\hspace{1em}} InitH \.{\defeq} Init \.{\land} list \.{=} \{ InitState \}}% \@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 14\hspace{1em}} DoH ( c ) \.{\defeq} Do ( c + \@x{\makebox[0pt][r]{\scriptsize 11\hspace{1em}} DoH ( c ) \.{\defeq} Do ( c ) \.{\land} list \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% \@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 16\hspace{1em}} RevH ( c ) \.{\defeq} Rev ( + \@x{\makebox[0pt][r]{\scriptsize 13\hspace{1em}} RevH ( c ) \.{\defeq} Rev ( c ) \.{\land} list \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% \@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 18\hspace{1em}} SRevH \.{\defeq} SRev + \@x{\makebox[0pt][r]{\scriptsize 15\hspace{1em}} SRevH \.{\defeq} SRev \.{\land} list \.{'} \.{=} list \.{\cup} \{ state \.{'} [ Server ] \}}% -\@x{\makebox[0pt][r]{\scriptsize 19\hspace{1em}}}\midbar\@xx{}% -\@x{\makebox[0pt][r]{\scriptsize 20\hspace{1em}} NextH \.{\defeq}}% - \@x{\makebox[0pt][r]{\scriptsize 21\hspace{1em}}\@s{16.4} \.{\lor} \E\, c +\@x{\makebox[0pt][r]{\scriptsize 16\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 17\hspace{1em}} NextH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 18\hspace{1em}}\@s{16.4} \.{\lor} \E\, c \.{\in} Client \.{:} DoH ( c ) \.{\lor} RevH ( c )}% -\@x{\makebox[0pt][r]{\scriptsize 22\hspace{1em}}\@s{16.4} \.{\lor} SRevH}% +\@x{\makebox[0pt][r]{\scriptsize 19\hspace{1em}}\@s{16.4} \.{\lor} SRevH}% \@pvspace{8.0pt}% -\@x{\makebox[0pt][r]{\scriptsize 24\hspace{1em}} FairnessH \.{\defeq}}% - \@x{\makebox[0pt][r]{\scriptsize 25\hspace{1em}}\@s{16.4} {\WF}_{ varsH} ( +\@x{\makebox[0pt][r]{\scriptsize 21\hspace{1em}} FairnessH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 22\hspace{1em}}\@s{16.4} {\WF}_{ varsH} ( SRevH \.{\lor} \E\, c \.{\in} Client \.{:} RevH ( c ) )}% \@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 27\hspace{1em}} SpecH \.{\defeq} InitH + \@x{\makebox[0pt][r]{\scriptsize 24\hspace{1em}} SpecH \.{\defeq} InitH \.{\land} {\Box} [ NextH ]_{ varsH}}% \@y{\@s{0}% \ensuremath{\.{\land} FairnessH }}% \@xx{}% -\@x{\makebox[0pt][r]{\scriptsize 28\hspace{1em}}}\midbar\@xx{}% -\@x{\makebox[0pt][r]{\scriptsize 29\hspace{1em}} WLSpec \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 25\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 26\hspace{1em}} WLSpec \.{\defeq}}% \@y{\@s{0}% The weak list specification }% \@xx{}% - \@x{\makebox[0pt][r]{\scriptsize 30\hspace{1em}}\@s{16.4} Comm ( Cop ) + \@x{\makebox[0pt][r]{\scriptsize 27\hspace{1em}}\@s{16.4} Comm ( Cop ) {\bang} EmptyChannel}% - \@x{\makebox[0pt][r]{\scriptsize 31\hspace{1em}}\@s{45.78} \.{\implies} \A\, + \@x{\makebox[0pt][r]{\scriptsize 28\hspace{1em}}\@s{45.78} \.{\implies} \A\, l1 ,\, l2 \.{\in} list \.{:}}% - \@x{\makebox[0pt][r]{\scriptsize 32\hspace{1em}}\@s{65.44} \.{\land} + \@x{\makebox[0pt][r]{\scriptsize 29\hspace{1em}}\@s{65.44} \.{\land} Injective ( l1 )}% - \@x{\makebox[0pt][r]{\scriptsize 33\hspace{1em}}\@s{65.44} \.{\land} + \@x{\makebox[0pt][r]{\scriptsize 30\hspace{1em}}\@s{65.44} \.{\land} Injective ( l2 )}% - \@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}\@s{65.44} \.{\land} + \@x{\makebox[0pt][r]{\scriptsize 31\hspace{1em}}\@s{65.44} \.{\land} Compatible ( l1 ,\, l2 )}% \@pvspace{8.0pt}% - \@x{\makebox[0pt][r]{\scriptsize 36\hspace{1em}} {\THEOREM} SpecH + \@x{\makebox[0pt][r]{\scriptsize 33\hspace{1em}} {\THEOREM} SpecH \.{\implies} WLSpec}% -\@x{\makebox[0pt][r]{\scriptsize 37\hspace{1em}}}\bottombar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}}\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{Mon} - \ensuremath{Dec} 31 20:38:09 \ensuremath{CST} 2018 by \ensuremath{hengxin + \ensuremath{\.{\,\backslash\,}}* Last modified \ensuremath{Tue} + \ensuremath{Jan} 01 10:22:57 \ensuremath{CST} 2019 by \ensuremath{hengxin }% \end{cpar}% \begin{cpar}{0}{F}{F}{0}{0}{}% diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.pdf new file mode 100644 index 0000000..e214bdc Binary files /dev/null and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.tex b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.tex new file mode 100644 index 0000000..e2983b3 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/JupiterH.tex @@ -0,0 +1,1042 @@ +\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{\makebox[0pt][r]{\scriptsize 1\hspace{1em}}}\moduleLeftDash\@xx{ + {\MODULE} JupiterH}\moduleRightDash\@xx{}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + Jupiter with a history variable (\ensuremath{i.e}., list) collecting all list + states across the system. +\end{cpar}% +\end{lcom}% +\@x{\makebox[0pt][r]{\scriptsize 5\hspace{1em}} {\EXTENDS} JupiterInterface}% +\@x{\makebox[0pt][r]{\scriptsize 6\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 7\hspace{1em}} {\CONSTANTS}}% +\@x{\makebox[0pt][r]{\scriptsize 8\hspace{1em}}\@s{16.4} TypeOK ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 9\hspace{1em}}\@s{16.4} Init ,\, Next ,\,}% + \@x{\makebox[0pt][r]{\scriptsize 10\hspace{1em}}\@s{16.4} Do ( \_ ) ,\, Rev ( + \_ ) ,\, SRev ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 11\hspace{1em}}\@s{16.4} Msg ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 12\hspace{1em}}\@s{16.4} Vars}% +\@x{\makebox[0pt][r]{\scriptsize 13\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 14\hspace{1em}} {\VARIABLES} list}% + \@x{\makebox[0pt][r]{\scriptsize 15\hspace{1em}} varsH \.{\defeq} {\langle} + Vars ,\, list {\rangle}}% +\@x{\makebox[0pt][r]{\scriptsize 16\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 17\hspace{1em}} TypeOKH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 18\hspace{1em}}\@s{16.4} \.{\land} TypeOK}% + \@x{\makebox[0pt][r]{\scriptsize 19\hspace{1em}}\@s{16.4} \.{\land} ( list + \.{\subseteq} List )}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 21\hspace{1em}} InitH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 22\hspace{1em}}\@s{16.4} \.{\land} Init}% + \@x{\makebox[0pt][r]{\scriptsize 23\hspace{1em}}\@s{16.4} \.{\land} list + \.{=} \{ InitState \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 25\hspace{1em}} DoH ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 26\hspace{1em}}\@s{25.62} \.{\land} Do ( c + )}% + \@x{\makebox[0pt][r]{\scriptsize 27\hspace{1em}}\@s{25.62} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 29\hspace{1em}} RevH ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 30\hspace{1em}}\@s{25.05} \.{\land} Rev ( c + )}% + \@x{\makebox[0pt][r]{\scriptsize 31\hspace{1em}}\@s{25.05} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 33\hspace{1em}} SRevH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}\@s{16.4} \.{\land} SRev}% + \@x{\makebox[0pt][r]{\scriptsize 35\hspace{1em}}\@s{16.4} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ Server ] \}}% +\@x{\makebox[0pt][r]{\scriptsize 36\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 37\hspace{1em}} NextH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 38\hspace{1em}}\@s{16.4} \.{\lor} \E\, c + \.{\in} Client \.{:} DoH ( c ) \.{\lor} RevH ( c )}% +\@x{\makebox[0pt][r]{\scriptsize 39\hspace{1em}}\@s{16.4} \.{\lor} SRevH}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 41\hspace{1em}} FairnessH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 42\hspace{1em}}\@s{16.4} {\WF}_{ varsH} ( + SRevH \.{\lor} \E\, c \.{\in} Client \.{:} RevH ( c ) )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 44\hspace{1em}} SpecH \.{\defeq} InitH + \.{\land} {\Box} [ NextH ]_{ varsH}}% +\@y{\@s{0}% + \ensuremath{\.{\land} FairnessH +}}% +\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 45\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 46\hspace{1em}} WLSpec \.{\defeq}}% +\@y{\@s{0}% + The weak list specification +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 47\hspace{1em}}\@s{16.4} Comm ( Msg ) + {\bang} EmptyChannel}% + \@x{\makebox[0pt][r]{\scriptsize 48\hspace{1em}}\@s{45.78} \.{\implies} \A\, + l1 ,\, l2 \.{\in} list \.{:}}% + \@x{\makebox[0pt][r]{\scriptsize 49\hspace{1em}}\@s{65.44} \.{\land} + Injective ( l1 )}% + \@x{\makebox[0pt][r]{\scriptsize 50\hspace{1em}}\@s{65.44} \.{\land} + Injective ( l2 )}% + \@x{\makebox[0pt][r]{\scriptsize 51\hspace{1em}}\@s{65.44} \.{\land} + Compatible ( l1 ,\, l2 )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 53\hspace{1em}} {\THEOREM} SpecH + \.{\implies} WLSpec}% +\@x{\makebox[0pt][r]{\scriptsize 54\hspace{1em}}}\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{Tue} + \ensuremath{Jan} 01 10:08:34 \ensuremath{CST} 2019 by \ensuremath{hengxin +}% +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Tue} \ensuremath{Jan} 01 + 09:56:25 \ensuremath{CST} 2019 by \ensuremath{hengxin +}% +\end{cpar}% +\end{lcom}% +\end{document} diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.tla new file mode 100644 index 0000000..59bdbaa --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.tla @@ -0,0 +1,6 @@ +---------------------------- MODULE AbsJupiterH2 ---------------------------- +EXTENDS AbsJupiter, JupiterH +============================================================================= +\* Modification History +\* Last modified Tue Jan 01 10:50:23 CST 2019 by hengxin +\* Created Tue Jan 01 10:43:55 CST 2019 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.project b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.project new file mode 100644 index 0000000..97cf2ec --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.project @@ -0,0 +1,79 @@ + + + AbsJupiterH2 + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + AbsJupiter.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiter.tla + + + AbsJupiterH2.tla + 1 + PARENT-1-PROJECT_LOC/AbsJupiterH2.tla + + + CSComm.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/CSComm.tla + + + FunctionUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/FunctionUtils.tla + + + JupiterCtx.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterCtx.tla + + + JupiterH.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla + + + JupiterInterface.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterInterface.tla + + + JupiterSerial.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterSerial.tla + + + OT.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/OT.tla + + + OpOperators.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/OpOperators.tla + + + SequenceUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/SequenceUtils.tla + + + SetUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/SetUtils.tla + + + diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.settings/org.lamport.tla.toolbox.prefs b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..86afbda --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/AbsJupiterH2.tla +eclipse.preferences.version=1 diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiter.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiter.tla new file mode 100644 index 0000000..3aaa1b8 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiter.tla @@ -0,0 +1,88 @@ +----------------------------- MODULE AbsJupiter ----------------------------- +(* +Abstract Jupiter, inspired by the COT algorithm proposed by Sun and Sun; see TPDS'2009. +*) +EXTENDS JupiterSerial +----------------------------------------------------------------------------- +VARIABLES + copss \* copss[r]: the state space (i.e., a set) of Cops maintained at replia r \in Replica + +vars == <> +----------------------------------------------------------------------------- +TypeOK == + /\ TypeOKInt + /\ TypeOKCtx + /\ TypeOKSerial + /\ Comm(Cop)!TypeOK + /\ copss \in [Replica -> SUBSET Cop] +----------------------------------------------------------------------------- +Init == + /\ InitInt + /\ InitCtx + /\ InitSerial + /\ Comm(Cop)!Init + /\ copss = [r \in Replica |-> {}] +----------------------------------------------------------------------------- +RECURSIVE xForm(_, _) +xForm(cop, r) == + LET ctxDiff == ds[r] \ cop.ctx \* THEOREM: cop.ctx \subseteq ds[r] + RECURSIVE xFormHelper(_, _, _) + xFormHelper(coph, ctxDiffh, copssr) == \* copssr: state space generated during transformation + IF ctxDiffh = {} THEN [xcop |-> coph, xcopss |-> copssr] + ELSE LET foph == CHOOSE op \in ctxDiffh: \* the first op in serial + \A opprime \in ctxDiffh \ {op}: tb(op, opprime, serial[r]) + fcophDict == {op \in copssr: op.oid = foph /\ op.ctx = coph.ctx} + fcoph == CHOOSE op \in fcophDict: TRUE \* THEOREM: Cardinality(fophDict) = 1 + xcoph == COT(coph, fcoph) + xfcoph == COT(fcoph, coph) + IN xFormHelper(xcoph, ctxDiffh \ {foph}, copssr \cup {xcoph, xfcoph}) + IN xFormHelper(cop, ctxDiff, copss[r]) + +Perform(cop, r) == + LET xform == xForm(cop, r) \* [xcop, xcopss] + IN /\ state' = [state EXCEPT ![r] = Apply(xform.xcop.op, @)] + /\ copss' = [copss EXCEPT ![r] = xform.xcopss \cup {cop}] +----------------------------------------------------------------------------- +DoOp(c, op) == \* Client c \in Client processes a locally generated operation op. + LET cop == [op |-> op, oid |-> [c |-> c, seq |-> cseq'[c]], ctx |-> ds[c]] + IN /\ Perform(cop, c) + /\ Comm(Cop)!CSend(cop) + +Do(c) == + /\ DoCtx(c) + /\ DoSerial(c) + /\ DoInt(DoOp, c) + +Rev(c) == + /\ Comm(Cop)!CRev(c) + /\ Perform(Head(cincoming[c]), c) + /\ RevSerial(c) + /\ RevCtx(c) + /\ RevInt(c) + +SRev == + /\ Comm(Cop)!SRev + /\ LET cop == Head(sincoming) + IN /\ Perform(cop, Server) + /\ Comm(Cop)!SSendSame(cop.oid.c, cop) + /\ SRevSerial + /\ SRevCtx + /\ SRevInt +----------------------------------------------------------------------------- +Next == + \/ \E c \in Client: Do(c) \/ Rev(c) + \/ SRev + +Fairness == + WF_vars(SRev \/ \E c \in Client: Rev(c)) + +Spec == Init /\ [][Next]_vars \* /\ Fairness +----------------------------------------------------------------------------- +Compactness == + Comm(Cop)!EmptyChannel => Cardinality(Range(copss)) = 1 + +THEOREM Spec => Compactness +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 20:27:49 CST 2018 by hengxin +\* Created Wed Dec 05 19:55:52 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiterH2.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiterH2.tla new file mode 100644 index 0000000..59bdbaa --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/AbsJupiterH2.tla @@ -0,0 +1,6 @@ +---------------------------- MODULE AbsJupiterH2 ---------------------------- +EXTENDS AbsJupiter, JupiterH +============================================================================= +\* Modification History +\* Last modified Tue Jan 01 10:50:23 CST 2019 by hengxin +\* Created Tue Jan 01 10:43:55 CST 2019 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/CSComm.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/CSComm.tla new file mode 100644 index 0000000..7cd4728 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/CSComm.tla @@ -0,0 +1,54 @@ +------------------------------- MODULE CSComm ------------------------------- +(* +Specification of communication in a Client-Server system model. +*) +EXTENDS SequenceUtils +----------------------------------------------------------------------------- +CONSTANTS + Client, \* the set of clients + Server, \* the (unique) server + Msg \* the set of messages +----------------------------------------------------------------------------- +VARIABLES + cincoming, \* cincoming[c]: incoming channel at client c \in Client + sincoming \* incoming channel at the Server +----------------------------------------------------------------------------- +TypeOK == + /\ cincoming \in [Client -> Seq(Msg)] + /\ sincoming \in Seq(Msg) +----------------------------------------------------------------------------- +Init == + /\ cincoming = [c \in Client |-> <<>>] + /\ sincoming = <<>> + +EmptyChannel == Init +----------------------------------------------------------------------------- +CSend(msg) == \* A client sends a message msg to the Server. + /\ sincoming' = Append(sincoming, msg) + /\ UNCHANGED cincoming + +CRev(c) == \* Client c receives and consumes a message from the Server. + /\ cincoming[c] # <<>> + /\ cincoming' = [cincoming EXCEPT ![c] = Tail(@)] + /\ UNCHANGED sincoming +----------------------------------------------------------------------------- +(* +SRev/SSend below is often used as a subaction. +No UNCHANGED in their definitions. +*) +SRev == \* The Server receives and consumes a message. + /\ sincoming # <<>> + /\ sincoming' = Tail(sincoming) + +SSend(c, cmsg) == \* The Server sents a message cmsg to each client other than c \in Client. + /\ cincoming' = [cl \in Client |-> + IF cl = c + THEN cincoming[cl] + ELSE Append(cincoming[cl], cmsg[cl])] + +SSendSame(c, msg) == \* The Server broadcasts the message msg to all clients other than c \in Client. + /\ SSend(c, [cl \in Client |-> msg]) +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 19:04:29 CST 2018 by hengxin +\* Created Sun Jun 24 10:25:34 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/FunctionUtils.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/FunctionUtils.tla new file mode 100644 index 0000000..49a9f4b --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/FunctionUtils.tla @@ -0,0 +1,10 @@ +-------------------- MODULE FunctionUtils -------------------- +Range(f) == {f[a] : a \in DOMAIN f} + +Injective(f) == \A a, b \in DOMAIN f: (a # b) => (f[a] # f[b]) + +Surjective(f, B) == \A b \in B: \E a \in DOMAIN f: f[a] = b +============================================================================= +\* Modification History +\* Last modified Tue Dec 04 19:38:21 CST 2018 by hengxin +\* Created Tue Aug 28 10:35:49 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterCtx.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterCtx.tla new file mode 100644 index 0000000..151b007 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterCtx.tla @@ -0,0 +1,47 @@ +----------------------------- MODULE JupiterCtx ----------------------------- +(* +Definitions and operators for context-based Jupiter protocols, +including AbsJupiter, CJupiter, and XJupiter. +*) +EXTENDS JupiterInterface +----------------------------------------------------------------------------- +VARIABLES + cseq, \* cseq[c]: local sequence number at client c \in Client + ds \* ds[r]: document state (a set of Oids) of replica r \in Replica + +ctxVars == <> +----------------------------------------------------------------------------- +Oid == [c: Client, seq: Nat] \* operation identifier +Cop == [op: Op \cup {Nop}, oid: Oid, ctx: SUBSET Oid] \* contexted-based op + +ClientOf(cop) == cop.oid.c + +COT(lcop, rcop) == \* OT of two Cop(s). + [lcop EXCEPT !.op = Xform(lcop.op, rcop.op), !.ctx = @ \cup {rcop.oid}] + +UpdateDS(r, oid) == \* update ds[r] to include new oid \in Oid + ds' = [ds EXCEPT ![r] = @ \cup {oid}] +----------------------------------------------------------------------------- +TypeOKCtx == + /\ cseq \in [Client -> Nat] + /\ ds \in [Replica -> SUBSET Oid] + +InitCtx == + /\ cseq = [c \in Client |-> 0] + /\ ds = [r \in Replica |-> {}] + +DoCtx(c) == + /\ cseq' = [cseq EXCEPT ![c] = @ + 1] + /\ UpdateDS(c, [c |-> c, seq |-> cseq'[c]]) + +RevCtx(c) == + /\ UpdateDS(c, Head(cincoming[c]).oid) + /\ UNCHANGED cseq + +SRevCtx == + /\ UpdateDS(Server, Head(sincoming).oid) + /\ UNCHANGED cseq +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 18:52:44 CST 2018 by hengxin +\* Created Wed Dec 05 20:03:50 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterH.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterH.tla new file mode 100644 index 0000000..a39cb05 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterH.tla @@ -0,0 +1,57 @@ +------------------------------ MODULE JupiterH ------------------------------ +(* +Jupiter with a history variable (i.e., list) collecting all list states across the system. +*) +EXTENDS JupiterInterface +------------------------------------------------------------- +CONSTANTS + TypeOKImpl, + InitImpl, NextImpl, + DoImpl(_), RevImpl(_), SRevImpl, + Msg, + Vars +------------------------------------------------------------- +VARIABLES list +varsH == <> +------------------------------------------------------------- +TypeOKH == + /\ TypeOKImpl + /\ (list \subseteq List) + +InitH == + /\ InitImpl + /\ list = {InitState} + +DoH(c) == + /\ DoImpl(c) + /\ list' = list \cup {state'[c]} + +RevH(c) == + /\ RevImpl(c) + /\ list' = list \cup {state'[c]} + +SRevH == + /\ SRevImpl + /\ list' = list \cup {state'[Server]} +------------------------------------------------------------- +NextH == + \/ \E c \in Client: DoH(c) \/ RevH(c) + \/ SRevH + +FairnessH == + WF_varsH(SRevH \/ \E c \in Client: RevH(c)) + +SpecH == InitH /\ [][NextH]_varsH \* /\ FairnessH +------------------------------------------------------------- +WLSpec == \* The weak list specification + Comm(Msg)!EmptyChannel + => \A l1, l2 \in list: + /\ Injective(l1) + /\ Injective(l2) + /\ Compatible(l1, l2) + +THEOREM SpecH => WLSpec +============================================================================= +\* Modification History +\* Last modified Tue Jan 01 10:48:21 CST 2019 by hengxin +\* Created Tue Jan 01 09:56:25 CST 2019 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterInterface.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterInterface.tla new file mode 100644 index 0000000..148bcf2 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterInterface.tla @@ -0,0 +1,76 @@ +-------------------------- MODULE JupiterInterface -------------------------- +(* +This module declares the parameters and defines the operators that describe +the interface of a family of Jupiter specs. +*) +EXTENDS Integers, SequenceUtils, OT +----------------------------------------------------------------------------- +CONSTANTS + Char, \* the set of characters + Client, \* the set of client replicas + Server, \* the (unique) server replica + InitState \* the initial state of each replica + +ASSUME \* We assume that all inserted elements are unique. + /\ Range(InitState) \cap Char = {} \* due to the uniqueness requirement +---------------------------------------------------------------------- +VARIABLES + state, \* state[r]: state (the list content) of replica r \in Replica + cincoming, \* cincoming[c]: incoming channel at the client c \in Client + sincoming, \* incoming channel at the Server + chins \* a set of chars allowed to insert; this is for model checking + +intVars == <> +---------------------------------------------------------------------- +Comm(Msg) == INSTANCE CSComm + +Replica == Client \cup {Server} + +List == Seq(Char \cup Range(InitState)) \* all possible lists +MaxLen == Cardinality(Char) + Len(InitState) \* the max length of lists in any state + +ClientNum == Cardinality(Client) +Priority == CHOOSE f \in [Client -> 1 .. ClientNum] : Injective(f) +----------------------------------------------------------------------------- +(* +The set of all operations. Note: The positions are indexed from 1. +*) +Rd == [type: {"Rd"}] +Del == [type: {"Del"}, pos: 1 .. MaxLen] +Ins == [type: {"Ins"}, pos: 1 .. (MaxLen + 1), ch: Char, pr: 1 .. ClientNum] \* pr: priority + +Op == Ins \cup Del \* Now we don't consider Rd operations +----------------------------------------------------------------------------- +TypeOKInt == + /\ state \in [Replica -> List] + /\ chins \subseteq Char + +InitInt == + /\ state = [r \in Replica |-> InitState] + /\ chins = Char + +DoIns(DoOp(_, _), c) == \* Client c \in Client generates an "Ins" operation. + \E ins \in {op \in Ins: + /\ op.pos \in 1 .. (Len(state[c]) + 1) + /\ op.ch \in chins /\ op.pr = Priority[c]}: + /\ DoOp(c, ins) + /\ chins' = chins \ {ins.ch} \* We assume that all inserted elements are unique. + +DoDel(DoOp(_, _), c) == \* Client c \in Client generates a "Del" operation. + \E del \in {op \in Del: op.pos \in 1 .. Len(state[c])}: + /\ DoOp(c, del) + /\ UNCHANGED chins + +DoInt(DoOp(_, _), c) == \* Client c \in Client issues an operation. + \/ DoIns(DoOp, c) + \/ DoDel(DoOp, c) + +RevInt(c) == \* Client c \in Client receives a message from the Server. + /\UNCHANGED chins + +SRevInt == \* The Server receives a message. + /\ UNCHANGED chins +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 20:27:25 CST 2018 by hengxin +\* Created Tue Dec 04 19:01:01 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterSerial.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterSerial.tla new file mode 100644 index 0000000..d3bd0bd --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/JupiterSerial.tla @@ -0,0 +1,53 @@ +--------------------------- MODULE JupiterSerial --------------------------- +(* +This module contains definitions and operators for Jupiter protocols, +i.e., AbsJupiter and CJupiter, +which utilizes the serialization order at the Server to guide OTs. +*) +EXTENDS JupiterCtx +----------------------------------------------------------------------------- +(* +tb: Is cop1 totally ordered before cop2? +This can be determined according to the serial view (sv) of any replica. +*) +tb(cop1, cop2, sv) == + LET pos1 == FirstIndexOfElementSafe(sv, cop1) + pos2 == FirstIndexOfElementSafe(sv, cop2) + IN IF pos1 # 0 /\ pos2 # 0 \* at the server or both are remote operations + THEN pos1 < pos2 + ELSE IF pos1 = 0 /\ pos2 = 0 \* at a client: both are local operations (not happen in CJupiter) + THEN cop1.seq < cop2.seq + ELSE pos1 # 0 \* at a client: one is a remote operation and the other is a local operation +----------------------------------------------------------------------------- +VARIABLES + serial, \* serial[r]: the serial view of replica r \in Replica about the Server + cincomingSerial, sincomingSerial + +serialVars == <> +commSerial == INSTANCE CSComm WITH Msg <- Seq(Oid), + cincoming <- cincomingSerial, sincoming <- sincomingSerial +----------------------------------------------------------------------------- +TypeOKSerial == + /\ serial \in [Replica -> Seq(Oid)] + /\ commSerial!TypeOK + +InitSerial == + /\ serial = [r \in Replica |-> <<>>] + /\ commSerial!Init + +DoSerial(c) == + UNCHANGED <> + +RevSerial(c) == + /\ commSerial!CRev(c) + /\ serial' = [serial EXCEPT ![c] = Head(cincomingSerial[c])] + +SRevSerial == + /\ LET cop == Head(sincoming) + IN /\ serial' = [serial EXCEPT ![Server] = Append(@, cop.oid)] + /\ commSerial!SSendSame(cop.oid.c, serial'[Server]) + /\ UNCHANGED <> +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 18:54:56 CST 2018 by hengxin +\* Created Wed Dec 05 21:03:01 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.cfg b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.cfg new file mode 100644 index 0000000..14ea8d0 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.cfg @@ -0,0 +1,55 @@ +\* MV CONSTANT declarations +CONSTANTS +c1 = c1 +c2 = c2 +\* MV CONSTANT declarations +CONSTANTS +a = a +b = b +\* CONSTANT declarations +CONSTANT Server = Server +\* MV CONSTANT definitions +CONSTANT +Client <- const_154631124155631000 +\* MV CONSTANT definitions +CONSTANT +Char <- const_154631124155632000 +\* SYMMETRY definition +SYMMETRY symm_154631124155633000 +\* CONSTANT definitions +CONSTANT +Msg <- const_154631124155634000 +\* CONSTANT definitions +CONSTANT +InitState <- const_154631124155635000 +\* CONSTANT definitions +CONSTANT +SRevImpl <- const_154631124155636000 +\* CONSTANT definitions +CONSTANT +Vars <- const_154631124155637000 +\* CONSTANT definitions +CONSTANT +InitImpl <- const_154631124155638000 +\* CONSTANT definitions +CONSTANT +TypeOKImpl <- const_154631124155639000 +\* CONSTANT definitions +CONSTANT +NextImpl <- const_154631124155640000 +\* CONSTANT definitions +CONSTANT +RevImpl <- const_154631124155641000 +\* CONSTANT definitions +CONSTANT +DoImpl <- const_154631124155642000 +\* CONSTANT definition +CONSTANT +Nop = Nop +\* SPECIFICATION definition +SPECIFICATION +spec_154631124155644000 +\* INVARIANT definition +INVARIANT +inv_154631124155645000 +\* Generated on Tue Jan 01 10:54:01 CST 2019 \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.tla new file mode 100644 index 0000000..18e1893 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/MC.tla @@ -0,0 +1,84 @@ +---- MODULE MC ---- +EXTENDS AbsJupiterH2, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +c1, c2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +a, b +---- + +\* MV CONSTANT definitions Client +const_154631124155631000 == +{c1, c2} +---- + +\* MV CONSTANT definitions Char +const_154631124155632000 == +{a, b} +---- + +\* SYMMETRY definition +symm_154631124155633000 == +Permutations(const_154631124155632000) +---- + +\* CONSTANT definitions @modelParameterConstants:0Msg +const_154631124155634000 == +Cop +---- + +\* CONSTANT definitions @modelParameterConstants:3InitState +const_154631124155635000 == +<<>> +---- + +\* CONSTANT definitions @modelParameterConstants:4SRevImpl +const_154631124155636000 == +SRev +---- + +\* CONSTANT definitions @modelParameterConstants:5Vars +const_154631124155637000 == +vars +---- + +\* CONSTANT definitions @modelParameterConstants:7InitImpl +const_154631124155638000 == +Init +---- + +\* CONSTANT definitions @modelParameterConstants:8TypeOKImpl +const_154631124155639000 == +TypeOK +---- + +\* CONSTANT definitions @modelParameterConstants:9NextImpl +const_154631124155640000 == +Next +---- + +\* CONSTANT definitions @modelParameterConstants:10RevImpl(c) +const_154631124155641000(c) == +Rev(c) +---- + +\* CONSTANT definitions @modelParameterConstants:11DoImpl(c) +const_154631124155642000(c) == +Do(c) +---- + +\* SPECIFICATION definition @modelBehaviorSpec:0 +spec_154631124155644000 == +SpecH +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154631124155645000 == +WLSpec +---- +============================================================================= +\* Modification History +\* Created Tue Jan 01 10:54:01 CST 2019 by hengxin diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OT.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OT.tla new file mode 100644 index 0000000..4980ff3 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OT.tla @@ -0,0 +1,73 @@ +--------------------------------- MODULE OT --------------------------------- +(* +This module contains the basic OT (Operational Transformation) functions +for two operations and general ones involving operation sequences. +*) +EXTENDS OpOperators, SetUtils +----------------------------------------------------------------------------- +XformII(lins, rins) == \* lins is transformed against rins + IF lins.pos < rins.pos + THEN lins + ELSE IF lins.pos > rins.pos + THEN [lins EXCEPT !.pos = @ + 1] + ELSE IF lins.ch = rins.ch + THEN Nop + ELSE IF lins.pr > rins.pr + THEN [lins EXCEPT !.pos = @+1] + ELSE lins + +XformID(ins, del) == \* ins is transformed against del + IF ins.pos <= del.pos + THEN ins + ELSE [ins EXCEPT !.pos = @-1] + +XformDI(del, ins) == \* del is transformed against ins + IF del.pos < ins.pos + THEN del + ELSE [del EXCEPT !.pos = @+1] + +XformDD(ldel, rdel) == \* ldel is transformed against rdel + IF ldel.pos < rdel.pos + THEN ldel + ELSE IF ldel.pos > rdel.pos + THEN [ldel EXCEPT !.pos = @-1] + ELSE Nop + +Xform(lop, rop) == \* lop is transformed against rop + CASE lop = Nop \/ rop = Nop -> lop + [] lop.type = "Ins" /\ rop.type = "Ins" -> XformII(lop, rop) + [] lop.type = "Ins" /\ rop.type = "Del" -> XformID(lop, rop) + [] lop.type = "Del" /\ rop.type = "Ins" -> XformDI(lop, rop) + [] lop.type = "Del" /\ rop.type = "Del" -> XformDD(lop, rop) +----------------------------------------------------------------------------- +(* +Generalized OT functions on operation sequences. +*) +RECURSIVE XformOpOps(_, _, _) +XformOpOps(xform(_,_), op, ops) == \* Transform an operation op against an operation sequence ops. + IF ops = <<>> + THEN op + ELSE XformOpOps(xform, xform(op, Head(ops)), Tail(ops)) + +RECURSIVE XformOpOpsX(_, _,_) +XformOpOpsX(xform(_, _), op, ops) == \* Transform an operation op against an operation sequence ops. + IF ops = <<>> + THEN <> \* Maintain and return the intermediate transformed operations. + ELSE <> \o XformOpOpsX(xform, xform(op, Head(ops)), Tail(ops)) + +XformOpsOp(xform(_, _), ops, op) == \* Transform an operation sequence ops against an operation op. + LET opX == XformOpOpsX(xform, op, ops) + IN [i \in 1 .. Len(ops) |-> xform(ops[i], opX[i])] +(* +Transforms an operation sequence ops1 against another operation sequence ops2; +see Definition 2.13 of the paper "Imine@TCS06". +*) +RECURSIVE XformOpsOps(_, _,_) +XformOpsOps(xform(_, _), ops1, ops2) == + IF ops2 = <<>> + THEN ops1 + ELSE XformOpsOps(xform, XformOpsOp(xform, ops1, Head(ops2)), Tail(ops2)) +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 19:45:16 CST 2018 by hengxin +\* Created Sun Jun 24 15:57:48 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OpOperators.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OpOperators.tla new file mode 100644 index 0000000..2989bbe --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/OpOperators.tla @@ -0,0 +1,23 @@ +---------------------------- MODULE OpOperators ---------------------------- +(* +Operators for Op. +*) +EXTENDS Naturals, Sequences, SequenceUtils +----------------------------------------------------------------------------- +Nop == PickNone(Nat) + +Apply(op, l) == \* Apply an operation op on the list l. + CASE op = Nop -> l + [] op.type = "Rd" -> l + [] op.type = "Del" -> DeleteElement(l, op.pos) \* Last(l) is deleted if pos > Len(l) + [] op.type = "Ins" -> InsertElement(l, op.ch, op.pos) \* Append(l, ch) if pos > Len(l) + +RECURSIVE ApplyOps(_, _) \* Apply an operation sequence ops on the list l. +ApplyOps(ops, l) == + IF ops = <<>> + THEN l + ELSE Apply(Last(ops), ApplyOps(AllButLast(ops), l)) +============================================================================= +\* Modification History +\* Last modified Mon Dec 31 19:21:16 CST 2018 by hengxin +\* Created Tue Aug 28 14:58:54 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SequenceUtils.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SequenceUtils.tla new file mode 100644 index 0000000..28aee24 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SequenceUtils.tla @@ -0,0 +1,183 @@ +-------------------- MODULE SequenceUtils -------------------- +(* +Copyright: https://github.com/bringhurst/tlaplus/blob/master/org.lamport.tla.toolbox.uitest/farsite/AdditionalSequenceOperators.tla +*) + +EXTENDS FiniteSets, Sequences, SetUtils, FunctionUtils +LOCAL INSTANCE Naturals + +(* +IsSequenceOfSetElements is a predicate that is true when the specified +sequence contains all and only elements of the specified set. + +IsSortedSequenceOfSetElements is a predicate that is true when the + +IsSequenceOfSetElements is true and the sequence is also sorted in increasing order. +*) + +Prepend(s,e) == <> \o s + +First(seq) == seq[1] + +Last(seq) == seq[Len(seq)] + +AllButFirst(seq) == [i \in 1..(Len(seq)-1) |-> seq[(i+1)]] + +AllButLast(seq) == [i \in 1..(Len(seq)-1) |-> seq[i]] + +DoesSeqPrefixSeq(seq1,seq2)== + /\ Len(seq1)\leq Len(seq2) + /\ (\A i \in 1..Len(seq1):seq1[i]=seq2[i]) + +DoesSeqProperlyPrefixSeq(seq1,seq2)== + /\ Len(seq1)seq[i]IF i> + THEN <<>> + ELSE LET h == Head(seq) + IN IF h \in R + THEN <> \o Retain(Tail(seq), R) + ELSE Retain(Tail(seq), R) +(****************************************************************) +(* It requires that index >= 1. *) +(* *) +(* If index > Len(seq) + 1, then it appends the element to seq. *) +(* *) +(* (ADDED by hengxin; July 04, 2018) *) +(****************************************************************) +InsertElement(seq, elem, index) == + [i \in 1 .. (Len(seq) + 1) |-> IF i < index + THEN IF i = (Len(seq) + 1) + THEN elem + ELSE seq[i] + ELSE IF i = index + THEN elem + ELSE seq[(i-1)]] \* i > index + +IsSorted2Partition(n,seq1,seq2)== + /\ seq1 \in Seq(1..n) + /\ seq2 \in Seq(1..n) + /\ n=Len(seq1)+Len(seq2) + /\ (\A i \in DOMAIN seq1,j \in DOMAIN seq1:iseq1[i]seq2[i]>. *) +(* *) +(* Copyright: https://www.learntla.com/libraries/sequences/ *) +(****************************************************************) +SeqMaxLen(S, n) == UNION {[1 .. m -> S] : m \in 0 .. n} + +(****************************************************************) +(* Map on a sequence. *) +(* *) +(* Copyright: https://www.learntla.com/libraries/sequences/ *) +(****************************************************************) +SeqMap(Op(_), seq) == [x \in DOMAIN seq |-> Op(seq[x])] + +PermsWithin(S) == {s \in UNION {[1 .. m -> S] : m \in 0 .. Cardinality(S)} : Cardinality(Range(s)) = Cardinality(DOMAIN s)} + +(****************************************************************) +(* All possible permutations generated based on sequence T. *) +(* *) +(* Copyright: https://learntla.com/tla/functions/ *) +(****************************************************************) +PermutationKey(n) == {key \in [1..n -> 1..n] : Range(key) = 1..n} +PermutationsOf(T) == { [x \in 1..Len(T) |-> T[P[x]]] : P \in PermutationKey(Len(T))} +(****************************************************************) +(* Get the index of the first occurrence of elem in seq. *) +(* *) +(* Precondition: elem \in SeqImage(seq). *) +(* *) +(* ADDED by hengxin; Aug. 12, 2018 *) +(****************************************************************) +RECURSIVE FirstIndexOfElement(_,_) +FirstIndexOfElement(seq, elem) == + IF Head(seq) = elem + THEN 1 + ELSE 1 + FirstIndexOfElement(Tail(seq), elem) + +(* +Get the index of the first occurence of elem in seq. +It returns 0 if elem does not occur in seq. +*) +RECURSIVE FirstIndexOfElementSafe(_,_) +FirstIndexOfElementSafe(seq, elem) == + LET RECURSIVE FirstIndexOfElementSafeHelper(_,_,_) + FirstIndexOfElementSafeHelper(seqh, elemh, fail) == + IF seqh = <<>> + THEN 0-fail + ELSE IF Head(seqh) = elemh + THEN 1 + ELSE 1 + FirstIndexOfElementSafeHelper(Tail(seqh), elemh, fail + 1) + IN FirstIndexOfElementSafeHelper(seq, elem, 0) +(****************************************************************) +(* Check if two sequences are compatible. *) +(* *) +(* Precondition: No duplication in each individual sequence. *) +(* *) +(* Two sequences are compatible if and only if for any two common elements *) +(* in both sequences, the relative order of them in the two *) +(* sequences are the same. *) +(* *) +(* ADDED by hengxin; Aug. 12, 2018 *) +(****************************************************************) +Compatible(seq1, seq2) == + \/ seq1 = seq2 + \/ LET commonElements == Range(seq1) \cap Range(seq2) + IN \A e1, e2 \in commonElements: + \/ e1 = e2 + \/ FirstIndexOfElement(seq1, e1) < FirstIndexOfElement(seq1, e2) + <=> FirstIndexOfElement(seq2, e1) < FirstIndexOfElement(seq2, e2) + +(****************************************************************) +(* The length of the longest common subsequence of two sequences seq1 and seq2. *) +(* *) +(* ADDED by hengxin; Aug. 12, 2018 *) +(****************************************************************) +RECURSIVE LCS(_,_) +LCS(seq1, seq2) == + IF seq1 = <<>> \/ seq2 = <<>> + THEN 0 + ELSE IF Last(seq1) = Last(seq2) + THEN 1 + LCS(AllButLast(seq1), AllButLast(seq2)) + ELSE MaxOfSet({LCS(AllButLast(seq1), seq2), LCS(seq1, AllButLast(seq2))}) + +LCSCompatible(seq1, seq2) == + Compatible(seq1, seq2) <=> LCS(seq1, seq2) = Cardinality(Range(seq1) \cap Range(seq2)) + +LCSCompatibleTest(S) == + \A seq1, seq2 \in PermsWithin(S): LCSCompatible(seq1, seq2) +============================================================================= +\* Modification History +\* Last modified Tue Dec 04 19:42:23 CST 2018 by hengxin +\* Created Tue Jul 03 15:21:02 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SetUtils.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SetUtils.tla new file mode 100644 index 0000000..d7c3f23 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH/SetUtils.tla @@ -0,0 +1,54 @@ +----------------------- MODULE SetUtils ----------------------- +(***************************************************************************) +(* Copyright: https://www.learntla.com/libraries/sets/ *) +(***************************************************************************) +EXTENDS TLC +LOCAL INSTANCE Naturals + +(***************************************************************************) +(* Pick an element from the set S. *) +(***************************************************************************) +Pick(S) == CHOOSE s \in S : TRUE +(***************************************************************************) +(* Pick an element that is not in the set S. *) +(***************************************************************************) +PickNone(S) == CHOOSE s : s \notin S + +RECURSIVE SetReduce(_, _, _) +SetReduce(Op(_, _), S, value) == + IF S = {} + THEN value + ELSE LET s == Pick(S) + IN SetReduce(Op, S \ {s}, Op(s, value)) +(***************************************************************************) +(* This version will report an error if *) +(* the operation applied is not commutative as required. *) +(***************************************************************************) +RECURSIVE SetReduceSafe(_, _, _) +SetReduceSafe(Op(_, _), S, value) == + IF S = {} + THEN value + ELSE LET s == Pick(S) + IN IF Op(s, value) = Op(value, s) + THEN SetReduceSafe(Op, S \ {s}, Op(s, value)) + ELSE Assert(FALSE, "Op is not commutative.") + +Sum(S) == + LET sum(a, b) == a + b + IN SetReduce(sum, S, 0) + +IsMin(set,min) == + /\ min \in set + /\ (\A x \in set:min \leq x) + +IsMax(set,max) == + /\ max \in set + /\ (\A x \in set:max \geq x) + +MinOfSet(set) == CHOOSE min \in set:(\A x \in set: min \leq x) + +MaxOfSet(set) == CHOOSE max \in set:(\A x \in set: max \geq x) +============================================================================= +\* Modification History +\* Last modified Tue Dec 04 19:43:16 CST 2018 by hengxin +\* Created Fri Jul 06 13:21:26 CST 2018 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH2___AbsJupiterH.launch b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH2___AbsJupiterH.launch new file mode 100644 index 0000000..fa21eec --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH2.toolbox/AbsJupiterH2___AbsJupiterH.launch @@ -0,0 +1,60 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.pdf new file mode 100644 index 0000000..d301e1c Binary files /dev/null and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla new file mode 100644 index 0000000..a39cb05 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla @@ -0,0 +1,57 @@ +------------------------------ MODULE JupiterH ------------------------------ +(* +Jupiter with a history variable (i.e., list) collecting all list states across the system. +*) +EXTENDS JupiterInterface +------------------------------------------------------------- +CONSTANTS + TypeOKImpl, + InitImpl, NextImpl, + DoImpl(_), RevImpl(_), SRevImpl, + Msg, + Vars +------------------------------------------------------------- +VARIABLES list +varsH == <> +------------------------------------------------------------- +TypeOKH == + /\ TypeOKImpl + /\ (list \subseteq List) + +InitH == + /\ InitImpl + /\ list = {InitState} + +DoH(c) == + /\ DoImpl(c) + /\ list' = list \cup {state'[c]} + +RevH(c) == + /\ RevImpl(c) + /\ list' = list \cup {state'[c]} + +SRevH == + /\ SRevImpl + /\ list' = list \cup {state'[Server]} +------------------------------------------------------------- +NextH == + \/ \E c \in Client: DoH(c) \/ RevH(c) + \/ SRevH + +FairnessH == + WF_varsH(SRevH \/ \E c \in Client: RevH(c)) + +SpecH == InitH /\ [][NextH]_varsH \* /\ FairnessH +------------------------------------------------------------- +WLSpec == \* The weak list specification + Comm(Msg)!EmptyChannel + => \A l1, l2 \in list: + /\ Injective(l1) + /\ Injective(l2) + /\ Compatible(l1, l2) + +THEOREM SpecH => WLSpec +============================================================================= +\* Modification History +\* Last modified Tue Jan 01 10:48:21 CST 2019 by hengxin +\* Created Tue Jan 01 09:56:25 CST 2019 by hengxin \ No newline at end of file diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.project b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.project new file mode 100644 index 0000000..2d18b29 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.project @@ -0,0 +1,64 @@ + + + JupiterH + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + AJupiter.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.tla + + + CSComm.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/CSComm.tla + + + FunctionUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/FunctionUtils.tla + + + JupiterH.tla + 1 + PARENT-1-PROJECT_LOC/JupiterH.tla + + + JupiterInterface.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterInterface.tla + + + OT.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/OT.tla + + + OpOperators.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/OpOperators.tla + + + SequenceUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/SequenceUtils.tla + + + SetUtils.tla + 1 + /home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/SetUtils.tla + + + diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.settings/org.lamport.tla.toolbox.prefs b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..bcb6042 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/JupiterH.tla +eclipse.preferences.version=1 diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.pdf b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.pdf new file mode 100644 index 0000000..d301e1c Binary files /dev/null and b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.pdf differ diff --git a/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.tex b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.tex new file mode 100644 index 0000000..12d1128 --- /dev/null +++ b/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.toolbox/JupiterH.tex @@ -0,0 +1,1042 @@ +\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{\makebox[0pt][r]{\scriptsize 1\hspace{1em}}}\moduleLeftDash\@xx{ + {\MODULE} JupiterH}\moduleRightDash\@xx{}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + Jupiter with a history variable (\ensuremath{i.e}., list) collecting all list + states across the system. +\end{cpar}% +\end{lcom}% +\@x{\makebox[0pt][r]{\scriptsize 5\hspace{1em}} {\EXTENDS} JupiterInterface}% +\@x{\makebox[0pt][r]{\scriptsize 6\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 7\hspace{1em}} {\CONSTANTS}}% +\@x{\makebox[0pt][r]{\scriptsize 8\hspace{1em}}\@s{16.4} TypeOK ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 9\hspace{1em}}\@s{16.4} Init ,\, Next ,\,}% + \@x{\makebox[0pt][r]{\scriptsize 10\hspace{1em}}\@s{16.4} Do ( \_ ) ,\, Rev ( + \_ ) ,\, SRev ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 11\hspace{1em}}\@s{16.4} Msg ,\,}% +\@x{\makebox[0pt][r]{\scriptsize 12\hspace{1em}}\@s{16.4} Vars}% +\@x{\makebox[0pt][r]{\scriptsize 13\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 14\hspace{1em}} {\VARIABLES} list}% + \@x{\makebox[0pt][r]{\scriptsize 15\hspace{1em}} varsH \.{\defeq} {\langle} + Vars ,\, list {\rangle}}% +\@x{\makebox[0pt][r]{\scriptsize 16\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 17\hspace{1em}} TypeOKH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 18\hspace{1em}}\@s{16.4} \.{\land} TypeOK}% + \@x{\makebox[0pt][r]{\scriptsize 19\hspace{1em}}\@s{16.4} \.{\land} ( list + \.{\subseteq} List )}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 21\hspace{1em}} InitH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 22\hspace{1em}}\@s{16.4} \.{\land} Init}% + \@x{\makebox[0pt][r]{\scriptsize 23\hspace{1em}}\@s{16.4} \.{\land} list + \.{=} \{ InitState \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 25\hspace{1em}} DoH ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 26\hspace{1em}}\@s{25.62} \.{\land} Do ( c + )}% + \@x{\makebox[0pt][r]{\scriptsize 27\hspace{1em}}\@s{25.62} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 29\hspace{1em}} RevH ( c ) \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 30\hspace{1em}}\@s{25.05} \.{\land} Rev ( c + )}% + \@x{\makebox[0pt][r]{\scriptsize 31\hspace{1em}}\@s{25.05} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ c ] \}}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 33\hspace{1em}} SRevH \.{\defeq}}% +\@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}\@s{16.4} \.{\land} SRev}% + \@x{\makebox[0pt][r]{\scriptsize 35\hspace{1em}}\@s{16.4} \.{\land} list + \.{'} \.{=} list \.{\cup} \{ state \.{'} [ Server ] \}}% +\@x{\makebox[0pt][r]{\scriptsize 36\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 37\hspace{1em}} NextH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 38\hspace{1em}}\@s{16.4} \.{\lor} \E\, c + \.{\in} Client \.{:} DoH ( c ) \.{\lor} RevH ( c )}% +\@x{\makebox[0pt][r]{\scriptsize 39\hspace{1em}}\@s{16.4} \.{\lor} SRevH}% +\@pvspace{8.0pt}% +\@x{\makebox[0pt][r]{\scriptsize 41\hspace{1em}} FairnessH \.{\defeq}}% + \@x{\makebox[0pt][r]{\scriptsize 42\hspace{1em}}\@s{16.4} {\WF}_{ varsH} ( + SRevH \.{\lor} \E\, c \.{\in} Client \.{:} RevH ( c ) )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 44\hspace{1em}} SpecH \.{\defeq} InitH + \.{\land} {\Box} [ NextH ]_{ varsH}}% +\@y{\@s{0}% + \ensuremath{\.{\land} FairnessH +}}% +\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 45\hspace{1em}}}\midbar\@xx{}% +\@x{\makebox[0pt][r]{\scriptsize 46\hspace{1em}} WLSpec \.{\defeq}}% +\@y{\@s{0}% + The weak list specification +}% +\@xx{}% + \@x{\makebox[0pt][r]{\scriptsize 47\hspace{1em}}\@s{16.4} Comm ( Msg ) + {\bang} EmptyChannel}% + \@x{\makebox[0pt][r]{\scriptsize 48\hspace{1em}}\@s{45.78} \.{\implies} \A\, + l1 ,\, l2 \.{\in} list \.{:}}% + \@x{\makebox[0pt][r]{\scriptsize 49\hspace{1em}}\@s{65.44} \.{\land} + Injective ( l1 )}% + \@x{\makebox[0pt][r]{\scriptsize 50\hspace{1em}}\@s{65.44} \.{\land} + Injective ( l2 )}% + \@x{\makebox[0pt][r]{\scriptsize 51\hspace{1em}}\@s{65.44} \.{\land} + Compatible ( l1 ,\, l2 )}% +\@pvspace{8.0pt}% + \@x{\makebox[0pt][r]{\scriptsize 53\hspace{1em}} {\THEOREM} SpecH + \.{\implies} WLSpec}% +\@x{\makebox[0pt][r]{\scriptsize 54\hspace{1em}}}\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{Tue} + \ensuremath{Jan} 01 10:37:37 \ensuremath{CST} 2019 by \ensuremath{hengxin +}% +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Tue} \ensuremath{Jan} 01 + 09:56:25 \ensuremath{CST} 2019 by \ensuremath{hengxin +}% +\end{cpar}% +\end{lcom}% +\end{document}