\documentclass[11pt,fleqn,leqno,notitlepage]{article}

% C:\lamport\miktex\tex\latex\tla2.sty 
% C:\lamport\miktex\tex\latex\abbrev.sty
% C:\lamport\miktex\tex\latex\pf2.sty
% c:\lamport\books\fred\science.tex
% c:\lamport\books\fred\science.aux
% c:\lamport\books\fred\science.bbl
% c:\lamport\books\fred\science.ind
% c:\lamport\miktex\bibtex\bibs\mybib.bib
%
%%

\usepackage{latexsym}

\usepackage{url}
% The following definition modifies my personal myurl.sty package
% for a BibTeX bug that causes it to add a "%" in the middle of a
% \url command.  At least some versions of the url package floating
% around used to have other problems that myurl.sty doesn't have.
% But hopefully they won't affect this book, so the regular url
% package is being loaded.
%
% \renewcommand{\urlbegin}{\catcode`\~12\relax
%                        \catcode`\#12\relax
%                        \catcode`\$12\relax
%                        \catcode`\&12\relax
%                        \catcode`\_12\relax
%                        \catcode`\^12\relax
%                        \catcode`\\12\relax
%                        \catcode`\/\active
%                        \catcode`\.\active
%                        \tt
%                        \urlend}
 \usepackage{tla2}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FLOATS                       % 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\floatpagefraction{.7}
\def\bottomfraction{.7}


%%%%  To allow bigger figures at the bottom of the page.
%%%% \renewcommand{\bottomfraction}{.7}

%%%%%%%%%%%%%%%%%%%%%%%%%% Emacs macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%&1&\vspace{-#\baselineskip}%&
%&c&\textsc{#}& 
%&f&\textsf{#}& 
%&T&\texttt{#}& 
%&t&\tlabox{#}& 
%&b&\textbf{#}& 
%&V&\vspace{#em}&  
%&v&\verb|#|&  
%&m&\tlabox{#}&
%&"&"#"&  % "

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 MODIFICATION DATE                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                 %
% Defines \moddate to expand to modification date such as         %
%                                                                 %
%    5 Aug 1991                                                   %
%                                                                 %
% and \prdate to print it in a large box.  Assumes editor         %
% updates modification date in standard SRC Gnu Emacs style.      %
% (should work for any user name).                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\ypmd{%                                                       %
%                                                                 %
%                                                                 %
  Last modified on Thu 24 October 2024 at  7:42:05 PST by lamport
  endypmd}                                                        %
%                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\moddate}{\expandafter\xpmd\ypmd}                     %
\def\xpmd Last modified                                           %
on #1 #2 #3 #4 at #5:#6:#7 #8 by #9 endypmd{#2 #3 #4} %%% at #5:#6 #8} %
\newcommand{\prdate}{\noindent\fbox{\Large\moddate}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                SOME DISPLAY ENVIRONMENTS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{display}%
  {\begin{list}{}{\parsep=0pt\relax\leftmargin=\mathindent}\item[]}%
  {\end{list}}

\newenvironment{describe}[1]%
   {\begin{list}{}{\settowidth{\labelwidth}{#1}%
            \setlength{\leftmargin}{\labelwidth}%
            \addtolength{\leftmargin}{\labelsep}%
            \def\makelabel##1{##1\hfill}}}%
   {\end{list}}

%%%%%%%%%%% \newcommand{\DELETE}[1]{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%               ASSUME / PROVE STATEMENTS                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \assprove{assump}{proof} produces
%     Assume: assump
%     Prove:  pf
% in a zero-width box, where assump and pf are put in a minipage.
%
\newcommand{\assprove}[2]{%
\makebox[0pt][l]{\begin{tabular}[t]{@{}l@{\hspace{.45em}}l}
\textsc{Assume}: &
  \begin{minipage}[t]{.9\textwidth}#1\end{minipage}\\
\textsc{Prove}: & 
  \begin{minipage}[t]{.9\textwidth}#2\end{minipage}\\
\end{tabular}}}

% Defines \XF, \YF, \ZF
\newcommand{\XF}{\mbox{XF}}
\newcommand{\YF}{\mbox{YF}}
\newcommand{\ZF}{\mbox{ZF}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%               SOME ABBREVIATIONS               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\bs}{\ensuremath{\backslash}}
\newcommand{\tth}{\ensuremath{^{\mathrm{th}}}}
\newcommand{\rd}{\ensuremath{^{\mathrm{rd}}}}
\newcommand{\nd}{\ensuremath{^{\mathrm{nd}}}}
\newcommand{\st}{\ensuremath{^{\mathrm{st}}}}
\newcommand{\dd}{\,.\,.\,} % \newcommand{\TLA}[1]{TLA$^{#1}$}
\newcommand{\tlaplus}{\mbox{TLA$^{+}$\hspace{-.1em}}}
\newcommand{\getin}{\ensuremath{\,:\hspace{.08em}\in\,}}  %\hspace{-.05em}
\newcommand{\tuple}[1]{\ensuremath{\langle#1\rangle}}
\renewcommand{\o}{\circ}
\newcommand{\ov}[1]{\ensuremath{\overline{\rule{0pt}{1.25ex}#1}}}
% completion: \cmp{r} = r uparrow
\newcommand{\cmp}[1]{\ensuremath{#1^{\uparrow}}}
% I'll abbreviate \overline with \ol
\newcommand{\ol}[1]{\ensuremath{\overline{\rule{0pt}{1.25ex}#1}}}
% And $\widehat{x}}$ by \wh{x}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%             DEFINITIONS OF SYMBOLS ETC.            %%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 


% \Beh : The set of behaviors
% \Val : The set of all values
% \Sta : The set of all states.
% \Var : The set of all variables.
% \Interp : The set of all interpretations.
% \Bool : The set of all Booleans.
% \bigunion : UNION

\newcommand{\bigunion}{\ensuremath{{\displaystyle\bigcup}\,}}
\newcommand{\Beh}{\ensuremath{\mathbf{Bh}}}
\newcommand{\Sta}{\ensuremath{\mathbf{St}}}
\newcommand{\Var}{\ensuremath{\mathbf{Vr}}}
 \newcommand{\Interp}{\ensuremath{\mathcal{I}}}
\newcommand{\Bool}{\ensuremath{Bool}}
%\newcommand{\Val}{\ensuremath{\mathbf{V}}}
%%% New, fancier definition of \Val 
\newcommand{\Val}{{\begin{picture}(10,8)(44,-4)%
\put(50,0){\makebox(0,0){\textbf{V}}}%
\qbezier(48.75,-3.5)(49.25,-3.5)(49.9, -3.5)
\qbezier(45.05,3.5)(44.4,3.5)(45.75,3.5)
\qbezier(48.5,-3.5)(46.525,-.2)(45.05, 3.1)
\qbezier(48.7,-3.5)(46.725,-.2)(45.25, 3.1)
\end{picture}}}

% \Int, \Nat, and \PNat are the sets of integers, natural
% numbers, and postive integers.
\newcommand{\Nat}{\ensuremath{Nat}}
\newcommand{\Int}{\ensuremath{Int}}
\newcommand{\PNat}{\ensuremath{Nat^{+}}}
% \Real = the set of real numbers
\newcommand{\Real}{\ensuremath{\mathbf{R}}}
%%%
%% The following definition should be put inside \mbox's to avoid
%% a line break happening between the | and the boldface letter.
%%% Alternative definitions  of \Nat, \PNat, \Real, \Int, 
 \def\Nat{\rule[.63em]{.15em}{.055em}\hspace{-.15em}\rule{.1em}{.055em}%
        \rule{.065em}{.63em}\hspace{-.04em}\textbf{N}}
%
 \def\Real{\rule[.63em]{.2em}{.055em}\hspace{-.2em}\rule{.1em}{.055em}%
    \rule{.065em}{.63em}\hspace{-.04em}\textbf{R}}
 \def\Int{\rule[.63em]{.2em}{.055em}\hspace{-.2em}\rule{.1em}{.055em}%
    \rule{.065em}{.63em}\hspace{-.04em}\textbf{I}}
 \def\Beh{\rule[.63em]{.2em}{.055em}\hspace{-.2em}\rule{.1em}{.055em}%
    \rule{.065em}{.63em}\hspace{-.04em}\textbf{B}}


% \PsetP is the power set operator and \PSet{S} is
% the set of subsets of S
\newcommand{\PSetP}{\ensuremath{\mathcal{P}}}
\newcommand{\PSet}[1]{\PSetP\ensuremath{(#1)}}



%% \EN is some E symbol meaning ENABLED
%\newcommand{\EN}{\mbox{\bf \rule{.085em}{1.55ex}\s{-.05}E}}
\newcommand{\EN}{\,\mbox{\rule{.07em}{1.55ex}\s{-.03}E}}

%% \whileop produces --|>, the symbol from "Conjoining Specifications"
%% that's like -+-> but without the +
\newcommand{\whileop}{\relax
 \ifmmode \s{.1}-\hspace{-.3em}\triangleright\s{.3}
   \else $-\hspace{-.2em}\triangleright$\fi}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                  REDEFINITIONS                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% REDEFINE \DOMAIN TO TAKE AN ARGUMENT AND PRODUCE
%% THE PARENTHESES
\renewcommand{\DOMAIN}[1]{\ensuremath{\textsc{domain}(#1)}}



%% \tlabox{formula}  is equivalent to \mbox{$formula$}
%% except that tla-mode expressions like A /\ B => C are
%% typeset properly
\makeatletter
\newcommand{\tlabox}{\begingroup\tlachars\@tlabox}
\newcommand{\@tlabox}[1]{\endgroup\mbox{\let\tlacolon\midcolon\ensuremath{#1}}}
\newcommand{\midcolon}{\mskip -.5\thinmuskip:\mskip -.5\thinmuskip}
\makeatother


% \us produces __
\newcommand{\us}{\setlength{\unitlength}{.1em}
                 {\begin{picture}(6,0)
                 \put(.75,0){\line(1,0){4}}
                 \end{picture}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{\textbf{TLA\boldmath$^{^{+}}$ Notation}\V{.5}
\large  for readers of \V{.5} \Large \textbf{A Science of Computer Programs}}
\author{{Leslie Lamport}}
\date{\moddate}
\begin{document}

\maketitle

This document describes how to write formulas that appear in the book
\emph{A Science of Computer Programs} in the \tlaplus\ language.  It
explains all the notation used in the examples from the book that are
on the web.  How to write all \tlaplus\ formulas can be found 
elsewhere~\cite{lamport:tla-webpage,lamport:tlabook}.

\subsection*{Symbols}

\tlaplus\ is written in \textsc{ascii}.  (Unicode input may be
supported in the future.)  Symbols that have obvious \textsc{ascii}
versions, such as $+$, $\bs$ (set difference), and $\dd$ (integer
interval), are represented in the obvious way.  The \textsc{ascii}
versions of other symbols that are not part of larger constructs are
given in Figure~\ref{fig}.  
%
Symbols written in the book in small capitals like \TRUE, 
\textsc{then}, and \textsc{else} are written in \tlaplus\ with
ordinary capitals like \verb|TRUE|, \verb|THEN|, and \verb|ELSE|.

\begin{figure}
{\centering
\begin{tabular}{l@{\ }ll}
\multicolumn{2}{c}{\underline{Book}} & 
   \multicolumn{1}{c}{\underline{\tlaplus}} \\
%%% $\bs$ &  (set differencce) & \verb|\| \\
$~$ & (negation)           & \verb|~| \ (tilde)\\
$~>$ & (leads to)          & \verb|~>|\\
$\X$ & (Cartesian product) & \verb|\X| \\
$\#$ & (cardinality)       & \verb|Cardinality|%
 \footnotemark\\
$\Rightarrow$ & (implication) & \verb|=>| \\
$\equiv$ & (equivalence) & \verb|<=>|  \,or\, \verb|\equiv| \\
$\neq$ & (not equal to) & \verb|#| \,or\, \verb|/=| \\
$\leq$ & (less than or equal) & \verb|=<| \,or\, \verb|\leq| \\
$\geq$ & (greater than or equal) & \verb|>=| \,or\, \verb|\geq| \\ 
$\deq$ & (equals by definition) & \verb|==| \\
$\circ$ & (sequence concatenation) & \verb|\o| \\
$\oplus$ & & \verb|(+)| \\
$[]$ & (always) & \verb|[]| \\
$<>$ & (eventually)& \verb|<>| \\
$\subseteq$ & (is a subset of) & \verb|\subseteq| \\
% $[\;\,]_{v}$ & (action operator) & \verb|[ ]_v|\\
% $<<\;\,>>_{v}$ & (action operator) & \verb|<< >>_v|\\
$'$ & (prime) & \verb|'| \\
$\langle\;\,\rangle$ & (tuple notation) & \verb|<< >>|\\
$\land$ & (conjunction) & \verb|/\| \,or\, \verb|\land|\\
$\cap$ & (set intersection) & \verb|\cap| \\
$\lor$ & (disjunction) & \verb|\/| \,or\, \verb|\lor|\\
$\cup$ & (set union) & \verb|\cup| \\
$\A$ & (universal quantification)  & \verb|\A| \\
$\E$ & (existential quantification) & \verb|\E|\\
$\in$ & (is an element of) & \verb|\in| \\
$\notin$ & (is not an element of) & \verb|\notin| \\
$\div$ & (integer division) & \verb|\div| \\
%%%% \\ $\dd$ & (integer interval) & \verb|..| \\
%%%% $<-$ & (substitution) & \verb|<-| \\
%%%% $|->$ &  & \verb@|->@ \\
%%%% $\cdot$ & (action composition) & \verb|\cdot| \\
\Int & & \verb|Int|$^{2}$\\
\Nat & & \verb|Nat|$^{2}$\\
$\EN$ & & \verb|ENABLED| \V{.5}
%%%%%%%%% NOT USED
\multicolumn{3}{l}{$^{1}${\footnotesize Defined in the $FiniteSets$ module.}}\\
\multicolumn{3}{l}{$^{2}${\footnotesize Defined in the $Integers$ module.}}
\end{tabular}\par}

\caption{\textsc{Ascii} representation of symbols.} \label{fig}
\end{figure}



\subsection*{Functions}

The biggest difference between the book's notation and \tlaplus\
involves functions.  In \tlaplus, most notation for functions uses the
square brackets \texttt{[\,]}.  If $f$ is a function, the application
of $f$ to an expression $exp$, which is written in the book as
$f(exp)$, is written in \tlaplus\ as \verb|f[exp]|.  Thus, if $f$ is a
defined symbol, we can write $f(exp)$ iff $f$ is defined by
$f(p)\,\deq\,\ldots$\,.  We can write $f[exp]$ if $f$ is any
expression, but it is a meaningful expression iff $f$
is a function.  (See Section 2.6 of the book.)

Here are the other constructs involving functions:
\begin{display}
\begin{tabular}{l@{\hspace{1.75em}}l}
\multicolumn{1}{c}{\underline{Book}\ \ \ } & 
   \multicolumn{1}{c}{\underline{\tlaplus}\ \ } \V{.3}
$v \in S |-> exp$ & \verb/[v \in S |-> exp]/ \V{.3}
$f \EXCEPT exp1 |-> exp2$ &  \verb|[f EXCEPT ![exp1] = exp2]| \V{.3}
$D -> S$ & \verb|[D -> S]| \V{.3}
$\DOMAIN{f}$ & \verb|DOMAIN f| 
\end{tabular}
\end{display}
The \tlaplus\ \textsc{except} construct has generalizations that at
least partly explain its ugliness, but which were not needed in the
book.


\subsubsection*{Subscripts and Superscripts}

An expression $v$ appearing as a subscript in a formula of the book
is written in \tlaplus\ as \verb|_v|.  For example, 
$\WF_{v}(A)$ is written as \verb|WF_v(A)|.  We can also write
$[A]_{<<x,y>>}$ as \verb|[A]_<<x,y>>|.  However, if you want to write
something like $<<A>>_{s\o t}$, you'd best use parentheses and write
\verb|<<A>>_(s\o t)| to make sure it's parsed correctly.

The only mathematical notation involving superscripts that is used
by \tlaplus\ is for exponentiation.  A formula written $x^{2}$ in
the book is written in \tlaplus\ as \verb|x^2|, where the exponentiation
operator \verb|^| is defined in the $Integers$ module.

The book also uses sub- and superscripts for pedagogical purposes.
For example, when adding a stuttering variable $s$ to program $ICen2$
in Section~7.3.2, it calls the resulting program $ICen2^{s}$.  In the
\tlaplus\ representation of that example, the formula $ICen2^{s}$ is
named \verb|ICen2_s|.  Underscores ``\verb|_|'' are used in this way
for names that in the book are written with sub- or superscripts.


\subsection*{Modules and {\rm\textsc{with}}}

The smallest complete unit of a \tlaplus\ description of a program is
a module.  The scope of any declaration or definition that appears in
a module lies within that module.  A module is contained in a file,
and it ends with four or more consecutive ``\verb|=|'' characters.
Anything following the module in the file is ignored.

A module can import other modules in two ways.  The first is with an
\verb|EXTENDS| statement that must be the first non-comment in the
module.  Extending modules in this way is essentially equivalent to
copying the contents of the extended modules, including their
declarations and definitions, into the current module.  While
\verb|EXTENDS| statements can be used to decompose the definition of a
program into multiple modules, in the examples it is used mainly just
to import standard modules.  The $Integers$ standard module, which
defines the usual operators of arithmetic, is imported in this way by
almost all the modules in the example.

The second way one module can import another is by
\emph{instantiation} with an \verb|INSTANCE| statement.  The book
expresses substitution with the \textsc{with} construct, where
 \[exp \WITH v <- exp_{1}, \;w <- exp_{2}\] 
is the formula obtained by substituting the expression $exp_{1}$ for
variable $v$ and the expression $exp_{2}$ for variable $w$ in
expression $exp$.  \tlaplus\ does not have such a way to express
substitution in an individual formula.  Instead, substitution is
expressed with module instantiation.

Suppose $Mod$ is the name of a module that declares only two
identifiers, which may be variables or constants, that are named $v$
and $w$.  The statement
\begin{display}
\verb|IM == INSTANCE Mod WITH v <- |$exp_{1}$\verb|, w <- |$exp_{2}$
\end{display}
imports all the definitions from module \verb|Mod| into the current
module as follows.  If the definition of the mapping \verb|F| defined
in module \verb|Mod| were written in the book as
  \,\tlabox{F(p, q, r) \,\deq\,exp}\,,
then the mapping \verb|IM!F| would be imported into the current module
with a definition that would be written in the book as
  \[IM!F(p,q,r) == (exp \WITH v <- exp_{1},\, w <- exp_{2})\]
In general, the \verb|INSTANCE| statement must declare a substitution
for every variable and constant defined in module \verb|Mod|.  However,
if module \verb|Mod| has a declared variable or constant named
\verb|id|, and the identifier \verb|id| is declared or defined in
the current  module, then the substitution \verb|id <- id| can be omitted
in the \verb|INSTANCE| statement.

\subsection*{Proofs}

Some of the examples contain proofs that are at least partially
checked with TLAPS, the \tlaplus\ proof checker.  
The \tlaplus\ syntax for formal proofs is close to that used in the book,
except for two things:
\begin{itemize}
\item Step numbers are written like $<<3>>4$, as mentioned in the book's
Math~VIII section and Section~A.2.  

\item Paragraph proofs are replaced by proofs of the form
 \verb|BY|~$\ldots$~\verb|DEF|~$\ldots$\,.  The \verb|BY|
section lists the facts (previous proved steps theorems) that the
prover needs to use to prove the current goal.  It may also contain
\verb|PTL|, which instructs TLAPS to use temporal-logic reasoning.
(As explained in the book, most of a TLA proof consists of ordinary
math, not temporal logic.)  The \verb|DEF| section lists the defined
symbols whose definitions the prover needs to expand.
\end{itemize}

\bibliography{mybib}
\bibliographystyle{plain}

\end{document}
