\documentclass[11pt,fleqn]{article}
\listfiles
\usepackage{latexsym}
\usepackage{color} 
\usepackage{hyperref}
\usepackage{graphpap}
\usepackage{graphics}
\usepackage{tla2}
\usepackage{url}

%%%%%%%%%%%%%%%%%%%%%%%%%% Emacs macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%&1&\vspace{-#\baselineskip}%&
%&i&\tindex{#}{}%&
%&j&\ctindex{#}{}{}%&
%&c&\textsc{#}& 
%&f&\textsf{#}& 
%&T&\texttt{#}& 
%&t&\tlabox{#}& 
%&b&\textbf{#}& 
%&v&\verb|#|&  
%&o&\ov{#}&
%&m&\mathcal{#}&
%&"&"#"&  % "



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Note: To make links to a page and a section, for the label use %%
%      \hypertarget{page-label}{\label{section-label}}           %%
% and for the ref use                                            %%
%       Section~\ref{section-label}                              %%
%         (page~\hyperlink{page-label}{\pageref*{section-label}}) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\definecolor{red}{rgb}{1,0,0}

\definecolor{linkcolor}{rgb}{.35,0,.35}
\newcommand{\red}{\color{linkcolor}}

\definecolor{black}{rgb}{0,0,0}
\newcommand{\black}{\color{black}}

\definecolor{green}{rgb}{0,1,0}
\newcommand{\green}{\color{green}}

\definecolor{white}{rgb}{0,0,0}
\newcommand{\white}{\color{white}}

\hypersetup{colorlinks=true,%
            linkcolor=linkcolor,
            urlcolor=linkcolor,
            citecolor=linkcolor}

\definecolor{gray}{gray}{.6}

\newcommand{\gray}{\color{gray}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 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:57:23 PST by lamport      %
       modified on Wed 24 April 2024 at  9:36:09 PST by lblam        %
  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}             %
\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}{{\tt #1}:}%
            \setlength{\leftmargin}{\labelwidth}%
            \addtolength{\leftmargin}{\labelsep}%
            \def\makelabel##1{##1\hfill}}}%
   {\end{list}}



\newcommand{\tlaplus}{TLA$^{+}\!$}



\newcommand{\tth}{\ensuremath{^{\rm th}}}
\newcommand{\st}{\ensuremath{^{\rm st}}}
\newcommand{\nd}{\ensuremath{^{\rm nd}}}
\newcommand{\proofrule}[2]{\setlength{\arrayrulewidth}{.6pt}%
  {\ensuremath{\begin{array}[t]{@{}c@{}}%
       \begin{array}[t]{@{}l@{}} #1\raisebox{-.1em}{\strut}\end{array}\\
       \hline \raisebox{.1em}{\strut}#2\end{array}}}}
\newcommand{\implies}{\ensuremath{\Rightarrow}}

\newcommand{\first}[1]{\ensuremath{\flat#1}}
\newcommand{\bigdot}{\ensuremath{\,\mbox{\Large\bf .}\,}}

\newcommand{\ov}[1]{\ensuremath{\overline{\rule{0pt}{.6em}#1}}}
\newcommand{\ovv}[1]{\ensuremath{\overline{\rule{0pt}{.8em}#1}}}

\newcommand{\alg}[1]{\ensuremath{Alg_{#1}}}


\makeatletter
\newcommand{\tlabox}{\begingroup\tlachars\@tlabox}
\newcommand{\@tlabox}[1]{\endgroup
   \mbox{\let\tlacolon\midcolon\,\ensuremath{#1}\,}}
\newcommand{\midcolon}{\mskip -.5\thinmuskip:\mskip -.5\thinmuskip}
\newcommand{\seq}[1]{\ensuremath{\langle#1\rangle}}
\makeatother

\definecolor{lightblue}{rgb}{0,.5,.8}
\newcommand{\blue}{\color{lightblue}}
%\newcommand{\mpar}[1]{\marginpar{\raggedright\footnotesize\blue#1}}
\newcommand{\mpar}[1]{\marginpar{\raggedright\small#1}}
\newcommand{\arrow}[1]{\ensuremath{\stackrel{#1}{\longrightarrow}}}

%% COMMANDS FOR THIS PAPER

%% \EN is some E symbol meaning ENABLED
%\newcommand{\EN}{\,\mbox{\rule{.07em}{1.55ex}\s{-.03}E}}
\newcommand{\EN}{\mbox{\textsc{enabled}}}
\renewcommand{\ENABLED}{\textsc{enabled\,}}


\newcommand{\tuple}[1]{\ensuremath{\langle#1\rangle}}
%% \Nat is the  set of natural numbers

\newcommand{\Nat}{\rule[.63em]{.15em}{.055em}\hspace{-.15em}\rule
    {.1em}{.055em}\rule{.065em}{.63em}\hspace{-.04em}\textbf{N}}

%% \Init and \Next are the initial predicate and next-state relation.
\newcommand{\Init}{\ensuremath{Init}}
\newcommand{\Next}{\ensuremath{Next}}




\renewcommand{\WITH}{\,\,\mbox{\sc with}\,\,}

\title{{\bf \boldmath \tlaplus\ Versions of Examples\\
  from\\
 A Science of Concurrent Programs}}
\author{Leslie Lamport}
\date{\moddate}

\begin{document}

\maketitle

The directory containing this pdf file contains many of the examples
from the book \emph{A Science of Concurrent Programs} written in
\tlaplus.  If you have read or are reading this book but are not
familiar with \tlaplus, you should read the note in the file
\texttt{tlaplus-notation.pdf} in this directory.

The \tlaplus\ specifications all have extensions \texttt{.tla}.  For
each of those specifications, a pretty-printed version appears in the
file with the same name but extension \texttt{.pdf}.  The pdf versions
are produced automatically, so they contain occasional weird bits of
formatting.  

Most of the \texttt{.tla} files of \tlaplus\ specifications have
corresponding directories whose name ends in \texttt{.toolbox}.  If
you open them with the \tlaplus\ Toolbox, you will find predefined
models that were used to check the specifications.  Comments in the
\tlaplus\ files and in the models can help you learn \tlaplus.  See
the \tlaplus\ web site at
\begin{display}
 \href{https://lamport.azurewebsites.net/tla/tla.html}%
 {\texttt{https://lamport.azurewebsites.net/tla/tla.html}}
\end{display}
for how to install the Toolbox and other \tlaplus\ tools.

Some of the \tlaplus\ specifications have proofs.  Those specifications
have corresponding \texttt{.tlaps} directories that contain unformation
used by the TLAPS proof checker.

\begin{describe}{Increment}

\item[\texttt{Increment}:] The $Increment$ algorithm of Figure 3.5.

\item[\texttt{Fischer}:] Fischer's algorithm from Section 5.2.1.

\item[\texttt{ICen1}:] The $ICen1$ program of Figure~7.4.
\end{describe}

\end{document}

