\documentstyle{article}
%\documentstyle[llncspf]{llncs}
%\documentstyle[11pt,spec92,pf]{article}

%%* "Hybrid Systems in TLA+"
%   Cleared by Sam 18 Nov 92
% Corrected 5 Jan 92 based on comments by Peter Hancock
% Corrected 6 Jan 92 based on comments by Peter Ladkin
% Minor changes 6 Apr 93 based on comments by A. Benveniste


\makeatletter
% LLNCS DOCUMENT STYLE -- version 1.1
% for LaTeX version 2.09
% last modified on Thu Nov 18 11:31:22 PST 1993 by lamport

% This style file is an adaptation of
% the original LaTeX article.sty, by:
% Frank Holzwarth, Springer-Verlag Heidelberg,
% Tiergartenstrasse 17, D-6900 Heidelberg.
%
% Modified by Leslie Lamport to
%  * remove the silly ``This article was typset using the ...'' at the
%    end.
%  * remove stretch between paragraphs.
%  * add page numbers, far enough from the text that Springer should
%    be able to cope with them.
%  * made optional argument work with the figure command
%
\typeout{Document Style `llncs', <version 1.1>}

\frenchspacing
\def~{\penalty\@M\kern3pt}

\def\thebibliography#1{\section*{References}\small\list
  {\arabic{enumi}.}{\settowidth\labelwidth{#1.}\leftmargin\labelwidth
    \advance\leftmargin\labelsep
    \usecounter{enumi}}
    \def\newblock{\hskip .11em plus .33em minus -.07em}
    \sloppy
    \sfcode`\.=1000\relax}

\def\ds@citeauthoryear{\def\thebibliography##1{\section*{References}%
    \small\list{}{\settowidth\labelwidth{}\leftmargin\parindent
    \itemindent=-\parindent
    \labelsep=\z@
    \usecounter{enumi}}%
    \def\newblock{\hskip .11em plus .33em minus -.07em}%
    \sloppy
    \sfcode`\.=1000\relax}%
    \def\@cite##1{##1}%
    \def\@lbibitem[##1]##2{\item[]\if@filesw
      {\def\protect####1{\string ####1\space}\immediate
    \write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}}%

\newif\if@envcountreset\@envcountresetfalse
\def\ds@envcountreset{\@envcountresettrue}

\def\@mbi{cmmib10}
\def\@ptsize{0} \@namedef{ds@11pt}{\def\@ptsize{1}}
\@namedef{ds@12pt}{\def\@ptsize{2}}
\def\ds@twoside{\@twosidetrue \@mparswitchtrue}
\def\ds@draft{\overfullrule
5pt}
\@options

\ds@twoside

\lineskip 1pt \normallineskip 1pt
\def\baselinestretch{1}

\def\@normalsize{\@setsize\normalsize{12pt}\xpt\@xpt
\abovedisplayskip=3 mm plus6pt minus 4pt
\belowdisplayskip=3 mm plus6pt minus 4pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt}

\mathchardef\Gamma="0100
\mathchardef\Delta="0101
\mathchardef\Theta="0102
\mathchardef\Lambda="0103
\mathchardef\Xi="0104
\mathchardef\Pi="0105
\mathchardef\Sigma="0106
\mathchardef\Upsilon="0107
\mathchardef\Phi="0108
\mathchardef\Psi="0109
\mathchardef\Omega="010A

\def\small{\@setsize\small{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\footnotesize{\@setsize\footnotesize{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\scriptsize{\@setsize\scriptsize{8.4pt}\viipt\@viipt}

\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
\def\large{\@setsize\large{13.2pt}\xipt\@xipt}
\def\Large{\@setsize\Large{14.4pt}\xiipt\@xiipt}
\def\LARGE{\@setsize\LARGE{16.8pt}\xivpt\@xivpt}
\def\huge{\@setsize\huge{22pt}\xxpt\@xxpt}
\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt}
\@normalsize

\if@twoside
   \oddsidemargin  44pt
   \evensidemargin 82pt
   \marginparwidth 107pt
\else \oddsidemargin 63pt \evensidemargin 63pt
 \marginparwidth 90pt
\fi
\marginparsep 11pt
\topmargin 11pt \headheight 12pt \headsep 13.66pt
\footheight 12pt \footskip 30pt
\textwidth 12.2truecm
\textheight 19.3truecm
\columnsep 1cc \columnseprule 0pt

\footnotesep 7.7pt
\skip\footins 9pt plus 4pt minus 2pt
\floatsep 12pt plus 2pt minus 2pt
\textfloatsep 8mm plus 2pt minus 4pt
\intextsep 8mm plus 2pt minus 2pt 
\@maxsep 8mm

\dblfloatsep 12pt plus 2pt minus 2pt
\dbltextfloatsep 20pt plus 2pt minus 4pt
\@dblmaxsep 20pt

\@fptop 0pt plus 1fil \@fpsep 8pt plus 2fil \@fpbot 0pt plus 1fil
\@dblfptop0pt plus1fil \@dblfpsep8pt plus2fil\@dblfpbot 0pt plus1fil
\marginparpush 5pt

\parskip 0pt %%%% plus 1pt %% stretch removed by LL 92-09-14
\parindent 1.5em \topsep 8pt plus 2pt minus 4pt
\partopsep 2pt plus 1pt minus 1pt \itemsep \z@
\@lowpenalty 51 \@medpenalty 151 \@highpenalty 301
\@beginparpenalty-\@lowpenalty\@endparpenalty -\@lowpenalty\@itempenalty
-\@lowpenalty

\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle\bf#1$}}
{\mbox{\boldmath$\textstyle\bf#1$}}
{\mbox{\boldmath$\scriptstyle\bf#1$}}
{\mbox{\boldmath$\scriptscriptstyle\bf#1$}}}

\def\@sect#1#2#3#4#5#6[#7]#8{\ifnum #2>\c@secnumdepth
  \def\@svsec{}\else
  \refstepcounter{#1}\edef\@svsec{\csname the#1\endcsname\quad }\fi
  \@tempskipa #5\relax
   \ifdim \@tempskipa>\z@
  \begingroup #6\relax
  \noindent{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par}
  \endgroup
    \csname #1mark\endcsname{#7}\addcontentsline
   {toc}{#1}{\ifnum #2>\c@secnumdepth \else
            \protect\numberline{\csname the#1\endcsname}\fi
          #7}\else
  \def\@svsechd{#6\hskip #3\@svsec #8\csname #1mark\endcsname
            {#7}\addcontentsline
             {toc}{#1}{\ifnum #2>\c@secnumdepth \else
               \protect\numberline{\csname the#1\endcsname}\fi
             #7}}\fi
  \@xsect{#5}}

\def\part{\par \addvspace{4ex} \@afterindentfalse \secdef\@part\@spart}

\def\@part[#1]#2{\ifnum \c@secnumdepth >\m@ne \refstepcounter{part}
\addcontentsline{toc}{part}{\thepart \hspace{1em}#1}\else
\addcontentsline{toc}{part}{#1}\fi { \parindent 0pt \raggedright
 \ifnum \c@secnumdepth >\m@ne \Large \bf
 Part\thepart\par\nobreak\fi\huge
\bf #2\markboth{}{}\par } \nobreak \vskip 3ex \@afterheading }

\def\@spart#1{{\parindent 0pt \raggedright
 \huge \bf
 #1\par} \nobreak \vskip 3ex \@afterheading }

\def\section{\@startsection {section}{1}{\z@}{-18pt plus -4pt minus
-4pt}{12pt plus 4pt minus 4pt}{\Large\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsection{\@startsection{subsection}{2}{\z@}{-18pt plus-4pt minus
 -4pt}{8pt plus 4pt minus 4pt}{\normalsize\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{-18pt plus-4pt
 minus -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\bf\boldmath}}
\def\paragraph{\@startsection{paragraph}{4}{\z@}{-12pt plus -4pt minus
 -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\it}}
\def\subparagraph#1{\typeout{LLNCS Warning: You should not use
\protect\subparagraph \space in this style.}\vskip0.5cm
You should not use $\backslash${\tt subparagraph} in this
style.\vskip0.5cm}

\setcounter{secnumdepth}{2}

\def\appendix{\par
 \setcounter{section}{0}
 \setcounter{subsection}{0}
 \def\thesection{\Alph{section}}}

\leftmargini 17pt     \leftmarginii 17pt
\leftmarginiii 17pt   \leftmarginiv 17pt
\leftmarginv 10pt       \leftmarginvi 10pt
\leftmargin\leftmargini \labelwidth\leftmargini
\advance\labelwidth-\labelsep
\labelsep 5pt
\parsep 0pt plus 1pt
\def\@listi{\leftmargin\leftmargini}
\def\@listii{\leftmargin\leftmarginii
 \labelwidth\leftmarginii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiii{\leftmargin\leftmarginiii
 \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiv{\leftmargin\leftmarginiv
 \labelwidth\leftmarginiv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listv{\leftmargin\leftmarginv
 \labelwidth\leftmarginv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listvi{\leftmargin\leftmarginvi
 \labelwidth\leftmarginvi\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}

\def\labelenumi{\arabic{enumi}.}
\def\theenumi{\arabic{enumi}}
\def\labelenumii{(\alph{enumii})}
\def\theenumii{\alph{enumii}}
\def\p@enumii{\theenumi}
\def\labelenumiii{\roman{enumiii}.}
\def\theenumiii{\roman{enumiii}}
\def\p@enumiii{\theenumi(\theenumii)}
\def\labelenumiv{\Alph{enumiv}.}
\def\theenumiv{\Alph{enumiv}}
\def\p@enumiv{\p@enumiii\theenumiii}

\def\labelitemi{\bf --}
\def\labelitemii{$\bullet$}
\def\labelitemiii{$\ast$}
\def\labelitemiv{$\cdot$}

\def\verse{\let\\=\@centercr
 \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
 \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
\let\endverse\endlist
\def\quotation{\list{}{\listparindent 1.5em
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[]}
\let\endquotation=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

\def\descriptionlabel#1{\hspace\labelsep \bf #1}
\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
 \let\makelabel\descriptionlabel}}
\let\enddescription\endlist

\def\theequation{\arabic{equation}}

\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
 \else \newpage \fi \thispagestyle{empty}\c@page\z@}
\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi}

\arraycolsep 1.4pt \tabcolsep 1.4pt \arrayrulewidth .4pt \doublerulesep
2pt
\tabbingsep \labelsep

\skip\@mpfootins = \skip\footins
\fboxsep = 3pt \fboxrule = .4pt

%\newcounter{part}
%\newcounter {section}
%\newcounter {subsection}[section]
%\newcounter {subsubsection}[subsection]
%\newcounter {paragraph}[subsubsection]

\def\thepart{\Roman{part}}
\def\thesection {\arabic{section}}
\def\thesubsection {\thesection.\arabic{subsection}}
\def\thesubsubsection {\thesubsection.\arabic{subsubsection}}
\def\theparagraph {\thesubsubsection.\arabic{paragraph}}

\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}

\def\tableofcontents{\section*{Table of Contents}
 \@starttoc{toc}}
\def\l@part#1#2{\addpenalty{\@secpenalty}
 \addvspace{2.25em plus 1pt} \begingroup
 \@tempdima 3em \parindent \z@ \rightskip \@pnumwidth \parfillskip
-\@pnumwidth
 {\Large \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
 \nobreak \endgroup}
%
\def\numberline#1{\advance\hangindent by\@tempdima%
\hbox to\@tempdima{\hss#1\enspace}}
%
\def\bf@dottedtocline#1#2#3#4#5{\ifnum #1>\c@tocdepth \else
  \vskip \z@ plus .2pt
  {\leftskip #2\relax \rightskip \@tocrmarg \parfillskip -\rightskip
    \parindent #2\relax\@afterindenttrue
   \interlinepenalty\@M
   \leavevmode
   \@tempdima #3\relax \advance\leftskip \@tempdima \hbox{}\hskip
   -\leftskip
{\bf#4}\nobreak\leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern \@dotsep
       mu$}\hfill \nobreak \hbox to\@pnumwidth{\hfil\rm #5}\par}\fi}
%
\def\l@section{\vskip2mm\bf@dottedtocline{1}{0em}{1.7em}}
\def\l@subsection{\@dottedtocline{2}{1.7em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{4em}{2em}}
\def\l@paragraph{\@dottedtocline{4}{6em}{2em}}
\def\l@subparagraph{\@dottedtocline{5}{8em}{2em}}
\def\listoffigures{\section*{List of Figures\markboth
 {List of Figures}{List of Figures}}\@starttoc{lof}}
\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
\def\listoftables{\section*{List of Tables\markboth
 {List of Tables}{List of Tables}}\@starttoc{lot}}
\let\l@table\l@figure

\def\endthebibliography{\endlist\normalsize}

\newif\if@restonecol
\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
\columnseprule \z@
\columnsep 35pt\twocolumn[\section*{Index}]
 \markboth{Index}{Index}\thispagestyle{plain}\parindent\z@
 \parskip\z@ plus .3pt\relax\let\item\@idxitem}
\def\@idxitem{\par\hangindent 40pt}
\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}

\def\footnoterule{\kern-3\p@\hrule width 2 true cm\kern 2.6\p@}

\long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
  \advance\@tempdima-1em\parshape \@ne 1em\@tempdima}\par
  \parindent 1em\noindent \hbox to \z@{\hss$^{\@thefnmark}$\ }#1}

\setcounter{topnumber}{2}
\def\topfraction{.9}
\setcounter{bottomnumber}{1}
\def\bottomfraction{.3}
\setcounter{totalnumber}{3}
\def\textfraction{.15}
\def\floatpagefraction{.85}
\setcounter{dbltopnumber}{2}
\def\dbltopfraction{.85}
\def\dblfloatpagefraction{.85}

\long\def\@makecaption#1#2{
 \vskip 10pt
 \setbox\@tempboxa\hbox{{\bf #1} #2}
 \ifdim \wd\@tempboxa >\hsize \unhbox\@tempboxa\par \else \hbox
to\hsize{\box\@tempboxa\hfil}
 \fi\vskip5pt}

\long\def\@caption#1[#2]#3{\addcontentsline{\csname
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
  the#1\endcsname}{\ignorespaces #2}}\par
  \begingroup
    \@parboxrestore
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
  \endgroup}

%\newcounter{figure}
\def\thefigure{\@arabic\c@figure}

\def\fps@figure{htbp}
\def\ftype@figure{1}
\def\ext@figure{lof}
\def\fnum@figure{Fig.\thinspace\thefigure.}
\def\figure{\@ifnextchar[{\@yfigure}{\@xfigure}}
\def\@xfigure{\@float{figure}\small\rm}
\def\@yfigure[#1]{\@float{figure}[#1]\small\rm}
\def\endfigure{\vskip-5pt\end@float}
\@namedef{figure*}{\@dblfloat{figure}}
\@namedef{endfigure*}{\end@dblfloat}

%\newcounter{table}
\def\thetable{\@arabic\c@table}
\def\fps@table{htbp}
\def\ftype@table{2}
\def\ext@table{lot}
\def\fnum@table{Table \thetable.}
\def\table{\@float{table}\small\rm}
\let\endtable\end@float
\@namedef{table*}{\@dblfloat{table}}
\@namedef{endtable*}{\end@dblfloat}

% LaTeX does not provide a command to enter the authors institute
% addresses. The \institute command is defined here.

\newcounter{@inst}
\newcounter{@auth}

\def\institute#1{\gdef\@institute{#1}}

\def\institutename{\par
 \begingroup
 \parskip=\z@
 \parindent=\z@
 \setcounter{@inst}{1}%
 \def\and{\par\stepcounter{@inst}%
 \noindent$^{\the@inst}$\enspace\ignorespaces}%
 \setbox0=\vbox{\def\thanks##1{}\@institute}%
 \ifnum\c@@inst=1\relax
 \else
   \setcounter{footnote}{\c@@inst}%
   \setcounter{@inst}{1}%
   \noindent$^{\the@inst}$\enspace
 \fi
 \ignorespaces
 \@institute\par
 \endgroup}

\def\@thanks{}

\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
   \or \dagger\or \ddagger\or
   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
   \or \ddagger\ddagger\else\@ctrerr\fi\relax}

\def\inst#1{\unskip$^{#1}$}

\def\subtitle#1{\gdef\@subtitle{#1}}
\def\@subtitle{}

\def\maketitle{\par
 \begingroup
 \parindent=\z@
 \def\thefootnote{\fnsymbol{footnote}}
 \if@twocolumn
 \twocolumn[\@maketitle]
 \else \newpage
 \global\@topnum\z@ \@maketitle \fi\thispagestyle{empty}\@thanks
 \endgroup
 \let\maketitle\relax
 \let\@maketitle\relax
 \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@subtitle{}%
 \let\thanks\relax}

\def\@maketitle{\newpage
 \begin{center}%
 {\LARGE \bf\boldmath
  \pretolerance=10000
  \@title \par}\vskip .8cm
\if!\@subtitle!\else {\Large \bf\boldmath
  \vskip -.65cm
  \pretolerance=10000
  \@subtitle \par}\vskip .8cm\fi
{\normalsize\rm\lineskip .5em
\@author\vskip.35cm}
 {\small\rm\institutename}
 \end{center}%
 }

\mark{{}{}}

% Define `abstract' environment
\def\abstract{%
\list{}{\advance\topsep by0.35cm\relax\small\rm
 \leftmargin=1cm
 \labelwidth=\z@
 \listparindent=\z@
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[\hskip\labelsep\bf Abstract.]}
\let\endabstract=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

%%% Modified by LL to print page numbers
\def\ps@headings{\def\@evenhead{\makebox[\textwidth]{\hfill 
   \raisebox{2cm}[0pt][0pt]{\fbox{\LARGE\thepage}\hspace{-2cm}}}}%
\let\@oddhead\@evenhead
\def\@evenfoot{}
\let\@oddfoot\@evenfoot
\def\sectionmark##1{}%
\def\subsectionmark##1{}}
\def\ps@myheadings{\let\@mkboth\@gobbletwo
\def\@oddhead{\hbox{}\small\rm\rightmark \hfil\thepage}%
\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\hfil
\leftmark\hbox {}}%
\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}}

\def\today{\ifcase\month\or
 January\or February\or March\or April\or May\or June\or
 July\or August\or September\or October\or November\or December\fi
 \space\number\day, \number\year}

\ps@headings \pagenumbering{arabic} \onecolumn
\if@twoside\else\raggedbottom\fi

% new environments and theorems
% borrowed form the LTMP-style of Springer-Verlag
% designed by Dr. Christoph Ender
%
% define the new theorem like environments
% define a new style of environments where it is possible to define
% the font % used as the theorem name and the fontfamily for the text.
%
% \newstytheorem{name}{thefont}{txtfont}{Text}[Counter]
% \newstytheorem{name}{thefont}{txtfont}[oldname]{Text}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
%
\def\newstytheorem#1#2#3{%
\@ifnextchar[{\che@othm{#1}{#2}{#3}}{\che@nthm{#1}{#2}{#3}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@nthm#1#2#3#4{%
\@ifnextchar[{\che@xnthm{#1}{#2}{#3}{#4}}{\che@ynthm{#1}{#2}{#3}{#4}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
% #5 - add theorem counter to reset list of another counter
%
\def\che@xnthm#1#2#3#4[#5]{\expandafter
\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}\if@envcountreset\@addtoreset{#1}{#5}\fi
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#4}{#2}{#3}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}%
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#2}{#3}{#4}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% change oldthm if oldname in specification is '*'
% then don't use a counter
% #1 - countername
% #2 - theorem font
% #3 - text font
% #4 - counter used
% #5 - string containing theorem name to print
%
\def\che@othm#1#2#3[#4]#5{\expandafter\@ifdefinable
\csname#1\endcsname%
{\@@othm@{#1}{#2}{#3}{#4}{#5}\global\@namedef{end#1}{\@endtheorem}}}
%
\def\@@othm@#1#2#3#4#5{\if *#4{\global\@namedef{the#1}{\relax}
\global\@namedef{#1}{\@bthm@{}{#5}{#2}{#3}}}\else
{\global\@namedef{the#1}{\@nameuse{the#4}}% define the counter
\global\@namedef{#1}{\che@thm{#4}{#5}{#2}{#3}}}\fi}
%
% new defs for theorem environment che 17-MAR-1989
% it improves the option possible
%
% #1 - countername  = theorem name
% #2 - string containing theorem name to print
% #3 - theorem font
% #4 - text font
\def\che@thm#1#2#3#4{\@ifnextchar({\@athm{#1}{#2}{#3}{#4}}{%
\@ifnextchar *{\@bthm{#1}{#2}{#3}{#4}}%
{\@@thm{#1}{#2}{#3}{#4}}}}
%
% \begin{thm}(A.1)[test]      results in:
% \end{thm}                               thm A.1 (test) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - is the new label
% #6 - optional string
%
\def\@athm#1#2#3#4(#5){\@ifnextchar[{%
\@aythm{#1}{#2}{#3}{#4}{#5}}{\@axthm{#1}{#2}{#3}{#4}{#5}}}
\def\@axthm#1#2#3#4#5{\@@locthmlab{#1}{#5}%
\@begintheorem{#2}{#5}{#3}{#4}\ignorespaces}
\def\@aythm#1#2#3#4#5[#6]{\@@locthmlab{#1}{#5}%
\fuh@opargbegintheorem{#2}{#5}{#6}{#3}{#4}\ignorespaces}
%
% \begin{thm}*[xytest]        results in:
% \end{thm}                               thm (xytest) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - optional string
%
\def\@bthm@#1#2#3#4{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bthm#1#2#3#4*{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bxthm#1#2#3#4{\if !#1!\relax\else\@@locthmlab{#1}{}\fi
\@@begintheorem{#2}{#3}{#4}\ignorespaces}
\def\@bythm#1#2#3#4[#5]{%
\@@opargbegintheorem{#2}{#3}{#4}{#5}\ignorespaces}
%
% define local label
%   if no number or a user specified label occured
%
\def\@@locthmlab#1#2{\expandafter\def\csname the#1\endcsname{#2}
\let\@chetempa\protect\def\protect{\noexpand\protect\noexpand}%
\edef\@currentlabel{\csname p@#1\endcsname\csname the#1\endcsname}%
\let\protect\@chetempa}
%
% #1 - counter = theorem name
% #2 - string with name
% #3 - font for theorem name and label
% #4 - font for text
\def\@@thm#1#2#3#4{\refstepcounter
    {#1}\@ifnextchar[{\che@ythm{#1}{#2}{#3}{#4}}{%
    \che@xthm{#1}{#2}{#3}{#4}}}
%
\def\che@xthm#1#2#3#4{\che@begintheorem{#2}{\csname
the#1\endcsname}{#3}{#4}\ignorespaces}
\def\che@ythm#1#2#3#4[#5]{\che@opargbegintheorem{#2}{\csname
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
%
% #1 - name of theorem
% #2 - label string
% #3 - font for name and lable
% #4 - text fomt
%
\def\che@begintheorem#1#2#3#4{#4\trivlist\item[\hskip\labelsep
#3#1\ts #2.]}
%
% #1 - name of theorem
% #2 - label string
% #3 - additonal text
% #4 - font for name and lable
% #5 - text fomt
%
\def\che@opargbegintheorem#1#2#3#4#5{#5\trivlist
\item[\hskip\labelsep#4#1\ts #2\ #3.]}
%
\def\fuh@opargbegintheorem#1#2#3{\it \trivlist
      \item[\hskip \labelsep{\bf #1\ #2\ (#3).}]}
%
\def\@@begintheorem#1#2#3{#3\trivlist\item[\hskip\labelsep
#2#1.]}
\def\@@opargbegintheorem#1#2#3#4{#3\trivlist\item[\hskip\labelsep
#2#1 #4.]}

\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
\newstytheorem{example}{\it}{\rm}{Example}[section]
\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
\newstytheorem{corollary}{\bf}{\it}[theorem]{Corollary}
\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
\newstytheorem{proof}{\it}{\rm}[*]{Proof}
\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
\newstytheorem{remark}{\it}{\rm}[*]{Remark}
\newstytheorem{exercise}{\it}{\rm}[theorem]{Exercise}
\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
\newstytheorem{solution}{\it}{\rm}[theorem]{Solution}
\newstytheorem{note}{\it}{\rm}[theorem]{Note}
\newstytheorem{question}{\it}{\rm}[theorem]{Question}

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
\gets\cr\to\cr}}}}}
\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
<\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.8pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
\def\bbbr{{\rm I\!R}} %reelle Zahlen
\def\bbbm{{\rm I\!M}}
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
\def\bbbf{{\rm I\!F}}
\def\bbbh{{\rm I\!H}}
\def\bbbk{{\rm I\!K}}
\def\bbbp{{\rm I\!P}}
\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbs{{\mathchoice
{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
\def\bbbz{{\mathchoice {\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\scriptstyle Z\kern-0.3em Z$}}
{\hbox{$\sf\scriptscriptstyle Z\kern-0.2em Z$}}}}
\def\ts{\thinspace}

\def\typeset{\vfill\small\noindent 
% modified by LL to supress LaTeX ack.
%This article was processed using
%the \LaTeX\ macro package with LLNCS style
\par}

\def\enddocument{\par\typeset
\@checkend{document}\clearpage\begingroup
\if@filesw \immediate\closeout\@mainaux
\def\global\@namedef##1##2{}\def\newlabel{\@testdef r}%
\def\bibcite{\@testdef b}\@tempswafalse\makeatletter\input \jobname.aux
\if@tempswa \@warning{Label(s) may have changed. Rerun to get
cross-references right}\fi\fi\endgroup\deadcycles\z@\@@end}

%%%%%%%%%%%% end of llncs.sty

% llncspf.sty
%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       THE pf STYLE                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  CONTENTS
%    1. Introduction
%    2. The Basic Commands
%    3. Different Styles of Numbering 
%    4. Indentation
%    5. Assumptions
%    6. Portions of a Proof
%    7. Conjunctions and Disjunctions
%    8. Miscellany
%    9. List of all Commands and Environments
%
%  1. INTRODUCTION
%
%    The pf style provides commands and environments for typesetting
%    hierarchically structured proofs.  Below is an example of what 
%    such a proof looks like, and the commands that generate it.
%    The commands are explained individually below.  Then
%
%    THE OUTPUT                         THE INPUT
%    ~~~~~~~~~~                         ~~~~~~~~~
%    Any text...                        Any text
%                                       \begin{proof}
%    1. Text of step 1.                   \step{label-1}{Text of step 1.}
%                                         \begin{proof}
%       1.1. Text of step.                  \step{label-1.1}{Text of step}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%                                      
%       1.2. Text of step.                   \step{label-1.2}{Text of step.}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%
%       1.3. QED                             \qedstep
%                                            \begin{proof}
%            1.3.1. Text of step               \step{label-1.3.1}{Text...}
%                   Proof: ... []              \begin{proof} ... \end{proof}
%                                            
%            1.3.2. QED                        \qedstep
%                   Proof: ...                 \begin{proof}...\end{proof}
%                                            \end{proof}
%                                         \end{proof}
%
%    2. Text of step 2.                   \step{label-2}{Text of step 2.}
%        Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%
%    3. QED                               \qedstep
%       Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%     
%
%   The best way to read such proofs is hierarchically.  To find out
%   how, search below for the \pfhidelevel command and the \hideqedproof
%   command.
%
%
% 2. THE BASIC COMMANDS
%
% The proof Environment:
%   Increments the proof depth, and indents the enclosed text the
%   appropriate amount.  For example, if the proof environment follows a
%   \step command that produces step number 2.6.7, then the first \step
%   command inside the environment will produce step number 2.6.7.1.
%
% \step{LABEL}{TEXT}
%    This command produces a proof step such as
%        2.6.7.1. TEXT
%    The step number 2.6.7.1 is determined by the position of the \step
%    command in the proof.  The LABEL is a symbol label used to refer to the
%    step number.  A subsequent \stepref{LABEL} command will generate the
%    step number 2.6.7.1.  The same LABEL may be re-used, but
%    not in a context where it is legal to refer to a previous step with the
%    same label.  (See the discussion of step numbering below.)
%    
%    This command is equivalent to
%           \begin{step+}{LABEL}
%              TEXT
%           \end{step+}
%    The step+ environment form is more convenient if TEXT is long or
%    complicated.
%
% \qedstep
%    This command produces something like
%    
%       2.6.7.5. QED
%    
%    If the proof of step 2.6.7 is a sequence of steps (rather than a
%    paragraph proof), then the last step in its proof is normally of this
%    form.  The "QED" in the statement simply denotes the current
%    goal---what must be proved to prove step 2.6.7.  The proof of this QED
%    step will be followed immediately by the
%    \end{proof} command that ends the proof of step 2.6.7.
%    
%    The pf style does not enforce this method of structuring proofs;
%    the proof of statement 2.6.7 could end with an ordinary \step
%    command.
%
% \pf, \qed
%    These are simple text-producing commands that normally begin and end a
%    paragraph-style proof.  However, they are not required.  Remember to
%    put a "\ " after the \pf command, and to tie the \qed command to the
%    last word of the proof with a "~".
%
% \pfsketch
%    
%    An intuitive prook sketch often introduces a multi-step proof, as in
%    
%         1.3. All odd numbers are prime.
%              Proof sketch:  The proof is by induction, with the
%              base case proved in step 1 and the induction step in
%              step 2.
%              1.3.1. The number 1 is a prime.
%                     Proof: ...
%              1.3.2. If n is an odd prime, then n+2 is prime.
%                     Proof: ...
%              1.3.3. QED
%                     Proof: 1.3.1, 1.3.2, and mathematical induction.
%    
%    This is entered as 
%    
%      \step{label-1.3}{All odd numbers  are prime}
%      \begin{proof}
%      \pfsketch\ The proof is by induction...
%       \step{label-1.3.2}{The number 1 is a prime}
%       ...
%      \end{proof}
%    
%    The \pfsketch command is, like \pf, just produces the text.  It isn't
%    required by the pf style.
%    
%
%  3. DIFFERENT STYLES OF NUMBERING 
%
%    In the long style of proof numbering, a step number is something like
%    2.6.7.5, meaning that it is the fifth step in the proof of statement
%    2.6.7, which is the seventh step in the proof of statement 2.6, which
%    is...  Statement 2.6.7.5 has the short name <4>5, meaning it is the
%    fifth statement in the current level-4 proof.  Numbering style is
%    controlled by the commands
%    
%      \pfshortnumbers{N} : Use short step numbers for all levels
%                           >= N (Default is N = 1, using only short
%                           numbers.
%    
%    These are local declarations that obey the usual scoping rules.  Thus,
%    putting a \pfshortnumbers declarations right after a \begin{proof}
%    command causes all steps in that proof to have short numbers.
%
%    Steps 2.6.7.5, 2.6.6.5, and 4.9.1.5 all have the same short numbers
%    <4>5.  However, no ambiguity arises from the use of short numbers
%    because at most one of these steps can be mentioned at any point in a
%    proof.  Let the ANCESTORS of step 2.6.7.5 be steps 2.6.7, 2.6, and 2.
%    Let the ELDER SIBLINGS of step 2.6.7.5 be steps 2.6.7.1, 2.6.7.2,
%    2.6.7.3, and 2.6.7.4.  The proof statement 2.6.7.5 may refer only
%    to steps in the following two sets:
%       (i) The elder siblings of itself and of its ancestors.
%      (ii) Itself and its ancestors.
%    The steps in (i) are the previously-proved assertions that can be used
%    in the proof of 2.6.7.5.  The assumptions of the steps in (ii) are the
%    ones that are being assumed in the proof.  (Assumptions are discussed
%    below.)
%    
%    The command \stepref{LABEL} anywhere in the proof of step 2.6.7.5 (or in
%    the step itself) produces the step number of a step lying in sets (i)
%    or (ii) having LABEL as its label (the first argument of its \step
%    command).  An error message is generated if the \step command has a
%    label that is the label of a step in set (i) or (ii).
%    
%    Note that the last step of a proof is never an elder sibling, so it
%    can't be in the set (i) for any statement.  A QED-step has no
%    assumptions, so it can't be in the set (ii) for any statement.  That is
%    why the \qedstep command does not specify a label.  Actually, \qedstep
%    is defined to equal \label{qedstepN}{...}, where N is the current
%.   level number. Thus, an error will be generated if two \qedstep commands 
%    occur in the same proof, since they will have the same labels.

%
%    Short step numbers are really nice.  They take up less space and are
%    easier to read.  They are the preferred form for long proofs.  However,
%    long step numbers are better for referring to a proof step from outside
%    the proof.  The pf style allows you to print the long numbers of steps as
%    marginal notes, something like
%    
%       Theorem:  ...
%       ...
%     2.4.5.6.         <4>6. All odd numbers greater than 2 are prime.
%     2.4.5.6.1.             <5>1. The number 3 is prime.
%       ...
%    
%    (The long numbers are printed in a smaller font, so it looks
%    better than you'd guess from this.)  The relevant commands are:
%    
%    \pfsidenumbers{N}{D} 
%       Print side numbers for proof steps of all levels \geq N, left-aligned 
%       a distance D to the left of the left margin of the text.
%    
%    \pfnosidenumbers  
%       Do not print side numbers (the default)
%
%
%  4. INDENTATION
%
%    There are two styles of indentation:
%    
%       Long Style 
%          1. XXXXX
%             1.1. XXXXX
%                  1.1.1. XXXXX
%                         1.1.1.1. XXXX
%                                  Proof: ...
%    
%       Short Style 
%          1. XXXXX
%            1.1. XXXXX
%              1.1.1. XXXXX
%                1.1.1.1. XXXX
%                  Proof: ...
%    
%    In the long style, the proof of a statement lines up with the text of
%    the statement.  In the short form, each level is indented the same
%    distance from the next higher level.  The relevant declarations
%    are
%    
%    \pflongindent 
%       Indent proofs to full width of item label
%    
%    \pfshortindent 
%       Indent proofs by the length parameter \pfindent (the default)
%
%
%  5. ASSUMPTIONS
%
%    A common form of a step is 
%        
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%    This asserts that the Prove clause follows from the Assume clause.  The
%    "QED" at the end of the proof of this step refers to the Prove clause.
%    The input to produce this is
%    
%        \step{label-4.5}{
%          \assume{\begin{enumerate}
%                    \item $n$ is an odd number
%                    \item $n>2$
%                  \end{enumumerate}}
%          \prove{$n$ is prime}}
%    
%    The relevant command syntax is
%    
%       \assume{TEXT}
%       \prove{TEXT}
%    
%    The formatting of the enumerate environment is changed to work
%    propertly inside a proof environment.  (It is actually redefined
%    to be the pfenum environment, described far below.)  Note that
%    \label and \ref command for subitem b of item 3 produces the label
%    "3b".  Note: there is an enumerate* environment that is like
%    enumerate, except it indents the items.
%     
%    
%    Another form of assumption is a Case assumption.  The statement
%    
%          <5>1. Case: n is of the form 4n+1
%    
%    means
%    
%          <5>1. Assume: n is of the form 4n+1
%                Prove:  QED
%    
%    where QED is the current goal.  A proof by cases is structured
%    as follows
%    
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%               <5>1. Assume: n equals 4m+1 for some m
%                     Prove:  QED
%                     Proof:  ... []
%    
%               <5>2. Assume: n equals 4m+3 for some m
%                     Prove:  QED
%                     Proof: ... []
%    
%               <5>3. QED
%                     Proof: By <5>1, <5>2, and assumption <4>.2 (which 
%                     states that n is odd), since any odd number has
%                     the form 4m+1 or 4m+3. []
%    
%    A case assumption is produced with a \case command, which works like
%    \assume and \prove.  It has the syntax
%    
%        \case{TEXT}
%    
%    Corresponding to the \assume, \prove, and \case commands are
%    the assume+, prove+, and case+ environments.  For example, \prove{TEXT}
%    is equivalent to \begin{prove+} TEXT \end{prove+}
%    
%    Note the reference, in the proof of <5>3, to the second conjunct of the
%    Assume clause in statement <4>5 as "assumption <4>.2".  Since a proof
%    of a step can only use assumptions in that step or its ancestors, a
%    level number suffices to identify an assumption.  The Assume clause of
%    statement <4>5 is called "assumption <4>".  The ".2" refers to the
%    second item in that clause.  As mentioned below, this use of ".2" to
%    refer to the second component of a conjunction can be used 
%    in other circumstances as well.
%    
%    When long numbering is used, assumptions must be referred to by the
%    name of the statement containing the assumption.  Thus, "assumption
%    2.6.7.5.2" could potentially mean either the Assume clause of statement
%    2.6.7.5.2, or the second item in the Assume clause of 2.6.7.5.  One way
%    to remove the ambiguity is to use something other than "." in long step
%    numbers.  The possibilities 2:6:7:5 and 2-6-7-5 don't look too good;
%    the best alternative to "." seems to be a raised period ($\cdot$).  The
%    "." is changed by redefining \pfdot, as described below.  Assumptions
%    are referred to with the following commands:
%    
%       \levelref{LABEL}
%         If \stepref{LABEL} produces <4>5, then \levelref{label} 
%         produces <4>.
%         If \stepref{LABEL} produces 2.6.7.5, then \levelref{label} also 
%         produces 2.6.7.5.
%
%       \toplevel
%         If \stepref{LABEL} produces <4>5, then \toplevel
%         produces "<0>".
%         If \stepref{LABEL} produces 2.6.7.5, then \toplevel
%         produces "0".
%
%
%  6. PORTIONS OF A PROOF
%
%    You may want to format only part of a proof--for example, you might
%    want to write the proof of statement 2.1.3 as a separate proof.  You'd
%    want something like
%    
%    2.1.3. All odd numbers are prime.
%           2.1.3.1. ...
%    
%    To do this, first imagine the shortest proof you can that has a
%    statement numbered 2.1.3: 
%    
%        1. X
%        2. X
%           2.1. X
%                2.1.1. X
%                2.1.2. X
%                2.1.3. All odd numbers are prime.
%                       2.1.3.1. ...
%    
%    Write this using the \step command and prove environment.  Now, change
%    every \step{LABEL}{X} command to \nostep{LABEL}, and change the proof
%    environments surrounding the proofs of steps 2 and 2.1 by noproof
%    environments.  This yields
%    
%        \begin{proof}
%          \nostep{label-1}
%          \nostep{label-2}
%          \begin{noproof}
%            \nostep{label-2.1}
%            \begin{noproof}
%              \nostep{label-2.1.1}
%              \nostep{label-2.1.2}
%        
%               \step{label-2.1.3} All oddnumbers are prime
%               \begin{proof}
%                  \step{label-2.1.3.1} ...
%               \end{proof}
%              \end{noproof}
%            \end{noproof}
%        \end{proof}
%    
%    which produces the desired result.  Note that the labels of the \nostep
%    commands can be used to refer to the corresponding step numbers.
%
%  7. CONJUNCTIONS AND DISJUNCTIONS
%
%    It is very convenient to write conjunctions as lists bulleted by \land.
%    This is done with the conj environment, where
%    
%     $X =  \begin{conj}    PRODUCES    X =  /\ A
%             A \\ B \\ C                    /\ B
%           \end{conj}$                      /\ C
%
%    The conj* environment is similar, except it numbers the conjuncts.
%    
%     $X = \begin{conj*}    PRODUCES    X = 1./\ A
%            A \\ B \\ C                    2./\ B
%          \end{conj*}$                     3./\ C
%
%    If X is defined in this way, then X.2 denotes the formula B.
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are implemented with the array environment.
%    They should nest properly.  They can be used only in math mode.
%
%
%  8. MISCELLANY
%
%    \pfhidelevel{N} : A counter that controls what levels of proof
%        are shown.  The command \setcounter{pfhidelevel}{2} causes
%        only level-1 and level-2 steps to be printed, and the proofs
%        of level-2 steps (including all level-3 and higher steps)
%        to be omitted.  The default value of the counter is very large.
%        The value of the counter should always be positive.
%
%   \unhideqedproof 
%   \hideqedproof   : Used in conjunction with the pfhidelevel counter.
%        The \unhideqedproof command causes one extra level of proof 
%        to be displayed for the lowest level \qedstep.  The \hideqedproof
%        returns to the default of not showing this extra level.
%       
%    \pflet  : like \prove and \assume, but with keyword "Let"
%
%    \kwfont : Selects the font for the keywords "Proof", "Assume",
%              "Prove", and "Case".  Default is \sc; you can 
%              change it by something like \renewcommand{\kwfont}{\em}
%
%    \pfdot : Defines the "." in long step numbers.  Try
%             \renewcommand{\pfdot}{\mbox{$\cdot$}} for variety.
%
%    \pfindent : The amount by which proof levels are indented in
%                the short indent option.  Changed with \setlength.
%                This is a local declaration.
%
%    \pfstepnumber{LEVEL}{NUMBER}{LONGNUMBER} :
%        Generates either <LEVEL>NUMBER or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    \pflevelnumber{LEVEL}{LONGNUMBER} :
%        Generates either <LEVEL> or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    The following parameters control vertical spacing.  
%    
%      \pftopsep  : space above first proof environment
%      \pfbotsep  : space below first proof environment
%      \pfsep     : space above and below inner proof environment
%      \stepsep   : space above and below proof step
%    
%    The last two are set to zero, and probably should remain there.  It
%    might be desirable to have vertical spacing depend more finely on the
%    level number.  This can be done using the \makefcn command (see far
%    below), and will be if there seems to be a need.  However,
%    zero extra vertical spacing seems to be fine.
%
%    \pf, \qed, \pfsketch  :  Described above.  Can be changed with 
%                             \renewcommand
%
%
%  9. LIST OF ALL COMMANDS AND ENVIRONMENTS
%
%    Text-Producting Commands            Environments
%      \pf, \pfsketch                      proof
%      \qed                                noproof
%      \step                               step+   [version of \step]        
%      \nostep                             assume+ [version of \assume]
%      \qedstep                            prove+  [version of \prove]        
%      \assume                             case+   [version of \case]        
%      \prove                              conj, conj*
%      \pflet                              disj, disj*
%      \case                               pfenum, enumerate*
%      \pfdot ["." in long names]          
%      \stepref, \levelref, \toplevel
%      \pfstepnumber, \pflevelnumber
%      
%    Declarations
%      \kwfont [keyword font]
%      \pfshortnumbers
%      \pfsidenumbers, \pfnosidenumbers
%      \pflongindent, \pfshortindent
%      \pfindent
%      \pftopsep, \pfbotsep  
%      \pfsep, \stepsep   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       SPACING                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pflongindent == Indent proofs to full width of item label
%   \pfshortindent == Indent proofs by \pfindent [the default]

\newif\if@pfLongIndent %  true if indent proof to width of label.
\@pfLongIndentfalse
\newcommand{\pflongindent}{\@pfLongIndenttrue}
\newcommand{\pfshortindent}{\@pfLongIndentfalse}

% PARAMETERS
%  \pfindent   == indentation at beginning of a proof
%  \pftopsep   == space above first proof environment
%  \pfbotsep   == space below first proof environment
%  \pfsep      == space above and below inner proof environment
%  \stepsep    == space above and below proof step
%  pfhidelevel == counter, specifying level at which proofs are hidden

\newlength{\pfindent}      
\newlength{\pftopsep}  
\newlength{\pfbotsep}  
\newlength{\pfsep}  
\newlength{\stepsep}        
\newbox{\pfbox}
\newcounter{pfhidelevel}
\setcounter{pfhidelevel}{9999}
\newcommand{\pfhidelevel}[1]{\setcounter{pfhidelevel}{#1}}

\setlength{\pfindent}{1em} 
\setlength{\pftopsep}{1ex}     % space above first proof environment
\setlength{\pfbotsep}{1ex}     % space below first proof environment
\setlength{\pfsep}{0pt}        % space above and below inner proof environment
\setlength{\stepsep}{0pt}      % space above and below proof step

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   STEP NUMBERING                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pfshortnumbers{N} == Use short step numbers for all levels >= N
%
%   \pfsidenumbers{N}{D} == print side numbers for proof steps of all
%                           levels >= N, left-aligned length D 
%                           to left of left margin
%   \pfnosidenumbers     == do not print side numbers (the default)

%\newcommand{\pflongnumbers}{\@pfLongNumberstrue}
\newcommand{\pfshortnumbers}[1]{\pfshortNumberLevel=#1\relax}

\newcount\pfshortNumberLevel \pfshortNumberLevel=0

% \@pfLongNumbersfalse}
% \newif\if@pfLongNumbers %  true if indent proof to width of label.
%\@pfLongNumbersfalse

\newcommand{\pfstepnumber}[3]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #3%
     \else $\langle#1\rangle#2$%
   \fi}

\newcommand{\pflevelnumber}[2]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #2%
     \else $\langle#1\rangle$%
   \fi}

\newif\if@pfSideNumbers %  true if putting long numbers at margin
\@pfSideNumbersfalse
\newcounter{pf@sidenumberdepth}
\newlength{\pf@sidenumberoutdent}
\newcommand{\pfsidenumbers}[2]{\@pfSideNumberstrue
     \setcounter{pf@sidenumberdepth}{#1}%
     \addtocounter{pf@sidenumberdepth}{-1}%
     \setlength{\pf@sidenumberoutdent}{#2}}
\newcommand{\pfnosidenumbers}{\@pfSideNumbersfalse}


\newcount\pfLevelCount  \pfLevelCount=0 % current level number
\newcount\pfStepCount   \pfStepCount=0  % current step number
\newcommand{\pfLongLevel}{} % The long version of current level--e.g., 2.7.5
\newcommand{\pfLongStep}{}  % The long version of current step--e.g., 2.7.5.2
\newcommand{\pfStepName}{}  % {current level name}{current step name} 

% \pfSetName ==  LongStep := current long step name
%                StepName := current step name
\newcommand{\pfSetName}{%
  \edef\pfLongStep{%
    \ifnum\pfLevelCount>\@ne
      \pfLongLevel\pfdot\the\pfStepCount
     \else\the\pfStepCount\fi}%
  \edef\pfStepName{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
    {\pfLongStep}{\pfLongStep}%
    \else
     {$\langle\the\pfLevelCount\rangle$}%
     {$\langle\the\pfLevelCount\rangle\the\pfStepCount$}%
   \fi}}

% \pfSetRef{foo} ==  IF \pf@foo UNDEFINED
%                       THEN \pf@foo := StepName 
%                       ELSE WARNING
\newcommand{\pfSetRef}[1]{%
  \@ifundefined{pf@#1}%
    {\expandafter
      \edef\csname pf@#1\endcsname{\pfStepName}}%
    {\typeout{WARNING:
         proof step "#1" (<\the\pfLevelCount>\the\pfStepCount) 
        already defined}}%
    }


\newcommand{\pfPrintStepNumber}[2]{#2}
\newcommand{\pfPrintLevelNumber}[2]{#1}

% \stepref{FOO} == Print \pf@FOO as a step number
\newcommand{\stepref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step "#1" undefined}}{\expandafter\expandafter\expandafter
 \pfPrintStepNumber\csname pf@#1\endcsname}}

\newcommand{\levelref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step #1 undefined}}%
  {\expandafter\expandafter\expandafter
 \pfPrintLevelNumber\csname pf@#1\endcsname}}

\newcommand{\toplevel}{\pflevelnumber{0}{0}}

\newlength{\pf@outdent}
\newcommand{\pfSideNumber}{%
  \if@pfSideNumbers 
   \ifnum\pfLevelCount>\value{pf@sidenumberdepth}%
    \hspace*{-\pf@outdent}%
    \makebox[0pt][l]{\footnotesize\pfLongStep}%
    \hspace*{\pf@outdent}%
    \else\fi
   \else\fi}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE pflist ENVIRONMENT                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%% The pflist environment is the same as list environment except 
%% it can be nested deeper.

\def\pflist#1#2{\ifnum \@listdepth >15\relax \@toodeep 
     \else \global\advance\@listdepth\@ne \fi
  \rightmargin \z@ \listparindent\z@ \itemindent\z@
  \csname @list\romannumeral\the\@listdepth\endcsname 
  \def\@itemlabel{#1}\let\makelabel\@mklab \@nmbrlistfalse #2\relax
  \@trivlist
  \parskip\parsep \parindent\listparindent
  \advance\linewidth -\rightmargin \advance\linewidth -\leftmargin
  \advance\@totalleftmargin \leftmargin
  \parshape \@ne \@totalleftmargin \linewidth 
  \ignorespaces}

\def\endpflist{\global\advance\@listdepth\m@ne
    \endtrivlist}

\let\@listvii=\@listv
\let\@listviii=\@listv
\let\@listix=\@listv
\let\@listx=\@listv
\let\@listxi=\@listv
\let\@listxii=\@listv
\let\@listxiii=\@listv
\let\@listxiv=\@listv
\let\@listxv=\@listv
\let\@listxvi=\@listv

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE proof ENVIRONMENT                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

\renewenvironment{proof}{%       BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel\pfdot\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \@tempcnta=\value{pfhidelevel}%
  \ifnum\@tempcnta<\@ne
    \setcounter{pfhidelevel}{1}%
    \typeout{WARNING: pfhidelevel < 1, setting to 1}%
    \@tempcnta=\@ne\fi
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi
  \else     
   \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi\fi
  \pfStepCount=\z@           %   StepCount  := 0
  \ifnum\pfLevelCount>\@ne   %   IF LevelCount > 1
   \begin{pflist}{}{%          %     THEN Begin List with
    \topsep=\pfsep\relax     %           \topsep     := \pfsep
    \itemsep=\z@             %           \itemsep    := 0
    \parsep=\z@              %           \parsep     := 0
    \partopsep=\z@           %           \partopsep  := 0
    \if@pfLongIndent         %          IF LongIndent
     \settowidth{\leftmargin}%%           THEN
      {\expandafter          %              \leftmargin := width of step name
       \pfPrintStepNumber    %                             + \labelsep
       \pfStepName.}%
     \advance\leftmargin
     \labelsep 
    \else                    %           ELSE
    \leftmargin=\pfindent    %            \leftmargin := \pfindent
    \fi\relax        
   }   \item[]
   \else \par                %     ELSE \par
    \addvspace{\pftopsep}%   %          addvspace of \pftopsep
    \parindent=\z@           %          \parindent := 0
    \parskip = \z@           %          \parskip := 0
    \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
    \let\enumerate\pfenum       %   enumerate environment <- pfenum
    \let\endenumerate\endpfenum %
 \fi
\@qedstepfalse
    }%                       % END:
  {\ifnum\pfLevelCount>\@ne  %   IF LevelCount > 1
    \end{pflist}%              %     THEN End List
   \else \par                %     ELSE \par
     \addvspace{\pfbotsep}%  %          addvspace of \pfbotsep
   \fi
  \@tempcnta=\value{pfhidelevel}%
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \end{minipage}\egroup\sbox{\pfbox}{}\@qedstepfalse\fi
  \else 
      \ifnum\pfLevelCount 
        =\@tempcnta 
        \end{minipage} 
        \egroup\sbox{\pfbox}{}\fi
 \fi}


\newenvironment{noproof}{%   % BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel.\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \pfStepCount=\z@           %   StepCount  := 0
  \par                       %   \par
  \parindent=\z@             %          \parindent := 0
  \parskip = \z@             %          \parskip := 0
  \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
  \let\enumerate\pfenum       %   enumerate environment <- pfenum
  \let\endenumerate\endpfenum %
  }%                         % END:
  {\par}                     %  \par

%% step 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     \step, \assume, ETC.                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\step}[2]{\begin{step+}{#1}#2\end{step+}}
\newif\if@qedstep %  true right after a \qedstep if in the scope of an 
                  %  \unhideqedproof declaration
\@qedstepfalse

\newif\if@unhideqedstep % set true by \unhideqproof, false by \hideqproof. 

\@unhideqedstepfalse
\newcommand{\unhideqedproof}{\@unhideqedsteptrue}
\newcommand{\hideqedproof}{\@unhideqedstepfalse}

\newcommand{\qedstep}{\step{qedstep\the\pfLevelCount}{Q.E.D.}
\if@unhideqedstep\@qedsteptrue\fi}

\newcommand{\nostep}[1]{% 
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
  }

\newenvironment{step+}[1]%
 {\endgroup                      % Move Outside environment scope
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
 \begingroup\@endpefalse         % Move inside environment scope
   \def\@currenvir{step+}%       %   by simulating \begin{step+}
 \begin{pflist}{}{%                % Begin list environment with
   \setlength
     {\pf@outdent}{\textwidth}%  %   \pf@outdent = outdent
   \addtolength                  %                 for side numbers
    {\pf@outdent}{-\linewidth}%  
   \addtolength
    {\pf@outdent}%
    {\pf@sidenumberoutdent}%
   \topsep=\stepsep\relax        %   \topsep     := \stepsep
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width of step name.
     {\expandafter
      \pfPrintStepNumber
      \pfStepName.}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep %                   + \labelsep
   \relax}%
 \item[\pfSideNumber%               % \item[ \pfSideNumber
  \expandafter                       %        StepNumber]
  \pfPrintStepNumber\pfStepName.]}%
 {\end{pflist}}

%%%%% \assume, \prove, and \case commands

\newenvironment{assume+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont Assume\/}:]}%    % \item[Assume:]]
 {\end{pflist}}

\newcommand{\assume}[1]{\begin{assume+}#1\end{assume+}}

\newcommand{\prove}[1]{\begin{prove+}#1\end{prove+}}
\newenvironment{prove+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Prove\/}:\hfill]}%     % \item[Prove:]]
 {\end{pflist}}

\newcommand{\pflet}[1]{\begin{pflet+}#1\end{pflet+}}
\newenvironment{pflet+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Let\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Let\/}:\hfill]}%     % \item[Let:]]
 {\end{pflist}}

%\newcommand{\prove}[1]{%
% \begin{pflist}{}{%                % Begin list environment with
%   \topsep=\z@                   %   \topsep     := 0
%   \itemsep=\z@                  %   \itemsep    := 0
%   \parsep=\z@                   %   \parsep     := 0
%   \partopsep=\z@                %   \partopsep  := 0
%   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
%     {{\kwfont Assume\/}:}%
%   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
%   \advance\leftmargin\labelsep  %                   + \labelsep
%   \relax}%
% \item[{\kwfont Prove\/}:\hfill]     % \item[Prove:]]
% #1
% \end{pflist}}

\newcommand{\case}[1]{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Case:"
     {{\kwfont Case\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont
           Case\/}:]             % \item[Case:]]
 #1
 \end{pflist}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       MISCELLANY                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\pf}{{\kwfont Proof\/}:}
\newcommand{\pfsketch}{{\kwfont Proof sketch\/}:}
%\newcommand{\qed}{\rule{.4em}{1.75ex}}
\renewcommand{\qed}{{\fboxsep=\z@\fbox{\rule{.5em}{0pt}\rule{0pt}{2ex}}}}
\let\kwfont=\sc
\def\pfdot{.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        STACKS                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \@push{\stack}{element}  == \stack := <<element>> :o: \stack
% \@pop{\stack}{\cmd}  == \cmd := head(\stack)
%                            \stack := tail(\stack)
% \newstack{\stack}  == \stack := emptystack
%
% \@head{\stack}{\var}  ==  \var := head(\stack)
%   Note: to push a counter value, use \the\value{ctr}
%         to push a length \foo, use \the\foo

%
\def\@push#1#2{{\let\@nil\relax\let\@elt\relax\xdef#1{#2\@elt#1}}}
\def\@pop#1#2{{\let\@nil\relax\let\@elt\relax
              \xdef#2{\expandafter\@innerhead#1}
              \xdef#1{\expandafter\@innerpop#1}}}
\def\@innerpop#1\@elt#2\@nil{#2\@nil}
\def\@head#1#2{{\let\@elt\relax\xdef#2{\expandafter\@innerhead#1}}}
\def\@innerhead#1\@elt#2\@nil{#1}
\def\newstack#1{\gdef#1{\@nil}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           LISTS OF CONJUNCTIONS AND DISJUNCTIONS            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%    \begin{conj}       ->   /\ A
%      A \\ B \\ C           /\ B
%    \end{conj}              /\ C
%
%    \begin{conj*}      ->   1./\ A
%      A \\ B \\ C           2./\ B
%    \end{conj*}             3./\ C
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are arrays; they must be used in math mode.

\newcounter{pf@conjCounter}   % counter for conj* and disj*
\newstack\pf@conj             % stack of counters

\newenvironment{conj}{%
 \begin{array}[t]{@{\land\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{disj}{%
 \begin{array}[t]{@{\lor\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{conj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\arabic{pf@conjCounter}.}
   \land\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

\newenvironment{disj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\alph{pf@conjCounter}.}
   \lor\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      ENUMERATED LISTS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% pfenum environment : In proofs, the enumerate environment 
%                      is redefined to be the pfenum environment
%
% enumerate* environment : Like pfenum, except with additional
%                          indentation.
%
% \enumindent :  The indentation for enumerate*
% pfenumdepth  : Depth of current pfenum list
% pfenum       : pfenum list counter
%
% Uses counters pfenumi, ... , pfenumiii just like the
% ordinary enumerate environment uses counters enumi, ... , enumiv.
% \pf@setEnumWidth{\cmd} : Sets \cmd to the width of the label of the
%                          item number 2 for the current enumeration level.
%
% \pf@enumLabel : prints the current pfenum label, using the
%                 pfenumi... counter.

\newcounter{pfenum}
\newcounter{pfenumdepth}
\newlength{\enumindent}
\setlength{\enumindent}{1em}

\@definecounter{pfenumi}
\@definecounter{pfenumii}
\@definecounter{pfenumiii}
%\@definecounter{pfenumiv}

\def\labelpfenumi{\thepfenumi.}    
\def\thepfenumi{\arabic{pfenumi}}     
 
\def\labelpfenumii{(\thepfenumii)}
\def\thepfenumii{\alph{pfenumii}}
\def\p@pfenumii{\thepfenumi}

\def\labelpfenumiii{\thepfenumiii.}
\def\thepfenumiii{\roman{pfenumiii}}
\def\p@pfenumiii{\thepfenumi\thepfenumii}

%\def\labelpfenumiv{\thepfenumiv.}
%\def\thepfenumiv{\Alph{pfenumiv}}     
%\def\p@pfenumiv{\p@pfenumiii\thepfenumiii}


\newcommand{\pf@setEnumWidth}[1]{%
  \settowidth{#1}{\setcounter{\@pfenumctr}{2}%
  \csname the\@pfenumctr\endcsname.%
  \setcounter{\@pfenumctr}{0}}}



\newcommand{\pf@enumLabel}{%
  \hfill\makebox[0pt][r]{\csname the\@pfenumctr\endcsname.}}

\newenvironment{pfenum}{%        % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

\newenvironment{enumerate*}{%    % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \advance\leftmargin\enumindent%                   + \enumindent
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \makefcn{\FOO}{V0}{{V1}...{Vk}} :
%      Defines \FOO{n}  ==  CASE  n = 0    -> V0
%                                 n = 1    -> V1
%                                 ...
%                                 n \geq k -> Vk
%
%      Useful when Vi is a dimension applying to a depth-i environment

\def\makefcn#1#2#3{{\let\or\relax
     \gdef\fcn@temp{}%
     \gdef\fcn@tempb{#2}%
     \@tfor\foo:=#3\do{\xdef\fcn@temp{\fcn@temp\or\foo}\xdef\fcn@tempb{\foo}}%
     \let\ifcase\relax\let\else\relax\let\fi\relax
     \xdef#1##1{\ifcase ##1 #2\fcn@temp\else\fcn@tempb\fi}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \pfif{A}{B}{C} :  if A then B    \pfIF{A}{B}{C} :  if A
%                        else C                        THEN B
%                                                      ELSE C

\newcommand{\pfmathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\pfif}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{}}
   {\bf if}\;\;#1&{\bf then}&#2\\
                 &{\bf else}&#3
   \end{array}}}}

\newcommand{\pfIF}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{}}
   {\bf if}\;\;#1\\ 
  \begin{array}[t]{@{\hspace{1em}}l@{\;\;}l@{}}
     {\bf then}&#2\\
     {\bf else}&#3
   \end{array}
  \end{array}}}}


\makeatother

% macros:
%&v&\vbl{#}&

\renewcommand{\textfraction}{.1}
\renewcommand{\floatpagefraction}{.75}
\renewcommand{\topfraction}{.85}
\renewcommand{\bottomfraction}{.85}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 MODIFICATION DATE                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                              %
% Defines \moddate to expand to the modification date like     %
%                                                              %
%    Mon  5 Aug 1991  [10:34]                                  %
%                                                              %
% and \prdate to print it in a large box.  Assumes editor      %
% updates modification date in standard SRC style.             %
% (Should work for any user name).                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\ypmd{%                                                    %
%                                                              %
%                                                              %
       modified on Tue Mar 12 15:41:49 1991 by doe             %
  endypmd}                                                     %
%                                                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\moddate}{\expandafter\xpmd\ypmd}                     %
\def\xpmd Last modified                                           %
on #1 #2 #3 #4:#5:#6 #7 #8 by #9 endypmd{#1 \ #3 #2 #8 \ [#4:#5]} %
\newcommand{\prdate}{\noindent\fbox{\Large\moddate}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Hybrid Systems in \TLA+}
\author{Leslie Lamport}
\institute{Digital Equipment Corporation\\
          Systems Research Center}
\date{\moddate}

%% \Real == the real numbers 
\newcommand{\Real}{{\bf R}}
\newcommand{\PosReal}{\mathdef{{\bf R}^{+}}}

% \TLA+  == TLA^+
% \gram
% \sqact, \anact
% \ccInterval{a}{b} = interval [a,b]
% \evolve{c}{a}{G}{A}{v} == [c+/_a G | A, v]
%  \rmod{x} == ||_ x _||
\newcommand{\approxint}{\mathdef{\Sigma}}
\newcommand{\evolve}[3]{\mbox{$[#1\!+\!\int_{#2}#3]$}}
\newcommand{\evolver}[5]{\mbox{$[#1\!=\!#2\!+\!\int#3\,|\,#4,#5]$}}
\newcommand{\mathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\rmod}[1]{\mathdef{|\!\lfloor#1\rfloor\!|}} 

\def\TLA+{\mbox{TLA$^{+}$}}
\newcommand{\gram}[1]{\mbox{\tt\protect\frenchspacing #1}}
\newcommand{\sqact}[2]{\mathdef{[\act{#1}]_{#2}}}
\newcommand{\anact}[2]{\mathdef{\langle\act{#1}\rangle_{#2}}}
\newcommand{\act}[1]{\mathdef{\makecal#1}}
\newcommand{\makecal}[1]{{\cal #1}}
%  \vbl{name}   == the program variable "name"
%  \str{chars}  = "chars"
\newcommand{\vbl}[1]{{\it #1\/}}
%\newcommand{\str}[1]{\mbox{\sf``#1''}}
\newcommand{\str}[1]{\mbox{\rm``{\sf #1}''}}
\newcommand{\ccInterval}[2]{\mathdef{\boldlb#1,#2\boldrb}}
\newcommand{\boldlp}{\mbox{\bf \protect\makebox[0pt][l]{(}\kern.25pt(}}
\newcommand{\boldrp}{\mbox{\bf \protect\makebox[0pt][l]{)}\kern.25pt)}}
\newcommand{\boldlb}{\mbox{\bf \protect\makebox[0pt][l]{[}\kern.25pt[}}
\newcommand{\boldrb}{\mbox{\bf \protect\makebox[0pt][l]{]}\kern.25pt]}}
\newcommand{\true}{{\sf true}}
\newcommand{\false}{{\sf false}}

%%%%%%%%%%%%%%%%%%%%%% spec92 commands %%%%%%%%%%%%%%%%%%%%%%
% \nomathgreater
% \nomathequal
\newcommand{\oo}{\infty}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\exists\s{-.517}\exists\s{-.517}\exists$}}\exists\s{-.517}\exists
            \s{-.517}\exists$}}
%\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
%   [0pt][l]{$\exists\!\!\!\exists\!\!\!\exists$}}\exists\!\!\!\exists
%            \!\!\!\exists$}}
\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\forall\hspace{-.025em}\!\!\!\forall
            \hspace{-.025em}\!\!\!\forall$}}\forall
             \hspace{-.025em}\!\!\!\forall\hspace{-.025em}\!\!\!\forall$}}
%% disable [[ and ]] as record delimiters
\newcommand{\speclblb}{\tt\char'133\char'133}
\newcommand{\specrbrb}{\tt\char'135\char'135}

%%%%%%%%%%%%%%%%%%%%%%%%% THe TLA environment
\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                  COMMANDS FROM spec92.sty                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
\newlength{\@charwidth}
\settowidth{\@charwidth}{{\small\tt M}}
\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
\newlength{\boxindent}\setlength{\boxindent}{22\@charwidth}
\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
\newcommand{\boxsep}{\@charwidth}
\newlength{\boxruleht}
\newlength{\boxruledp}
\newcommand{\@computerule}{%
  \setlength{\boxruleht}{.5ex}%
  \setlength{\boxruledp}{-\boxruleht}%
  \addtolength{\boxruledp}{\boxrulewd}}
\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
                      \hfill\mbox{}}

\newcommand{\@nmlineraise}{\if@botline -\boxrulewd
    \else-\boxlineht\fi}
\newcommand{\nameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{.5\baselineskip}}
\newif\if@botline

%%%%%%%%%%%%%%%%%%END COMMANDS FROM spec92.sty %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newenvironment{module}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\/} }\par
        }{\par\tlabotline\end{trivlist}}

\newenvironment{submodule}[1]{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\/} }\par
        }{\par\tlabotline\end{list}}

\newenvironment{cmodule}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf constant module} {\it #1\/} }\par
        }{\par\tlabotline\end{trivlist}}


\newcommand{\tlanameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

%%%%% Fix to \midline and \botline from spec92

\newcommand{\midbar}{\par\hspace{-\boxsep}%
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}\par}

\newcommand{\tlabotline}{\hspace{-\boxsep}%
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

\newcommand{\xtrivlist}{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}}
\def\endxtrivlist{\end{list}}

\def\xtabbing{\lineskip \z@\let\>\@rtab\let\<\@ltab\let\=\@settab
     \let\+\@tabplus\let\-\@tabminus\let\`\@tabrj\let\'\@tablab
     \let\\=\@tabcr
     \global\@hightab\@firsttab
     \global\@nxttabmar\@firsttab
     \dimen\@firsttab\@totalleftmargin
     \global\@tabpush0 \global\@rjfieldfalse
     \xtrivlist \item[]\if@minipage\else\vskip\parskip\fi
     \setbox\@tabfbox\hbox{\rlap{\indent\hskip\@totalleftmargin
       \the\everypar}}\def\@itemfudge{\box\@tabfbox}\@startline\ignorespaces}

\def\endxtabbing{\@stopline\ifnum\@tabpush > 0 \@badpoptabs \fi\endxtrivlist}

\newenvironment{decls}[1]{\par{\bf #1}\begin{xtabbing}%
  \hspace{1em}\=\+\kill}{\end{xtabbing}}

\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\mathchar"7001}{=}}}
\newcommand{\defeq}{\mathdef{\;\;\deq\;\;}}
\newcommand{\implies}{\Rightarrow}
\newcommand{\s}[1]{\hspace*{#1em}}
\newcommand{\vs}[1]{\raisebox{-#1em}{\rule{0pt}{.1pt}}}
%\newcommand{\tuple}[1]{\mathdef{\langle\,#1\,\rangle}}
\newcommand{\tuple}[1]{\mathdef{\langle#1\rangle}}
\newcommand{\e}{\Leftrightarrow}         % :e:   == \Leftrightarrow
\newcommand{\X}{\mathdef{\times}}
\newcommand{\lr}{{\speclblb}}
\newcommand{\rr}{{\specrbrb}}
\newcommand{\bs}{\mbox{\tt \symbol{'134}}}
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

%try
%\begin{titlepage}
% \maketitle 

% \vspace{3in}

% \noindent
% {\bf Warning }
% This is a hastily-written draft.  I have not had time to check it, and
% there are undoubtedly lots of errors---especially in the proof.  I am
% sending it out now because it is better than nothing, and I will not be
% able to do any further writing for a few weeks.
% \end{titlepage}

% \tableofcontents
% \clearpage

 \thispagestyle{empty}
 \mbox{}
 \vfill
 \begin{center}
 \LARGE
 \bf Hybrid Systems in \TLA+ 
 \large

 \vspace{1.5\baselineskip}
   Leslie Lamport \\ 
   {\small Digital Equipment Corporation}\\[-.2em]
   {\small Systems Research Center}\\[-.2em]
   {\small\tt lamport@src.dec.com}

\vspace{1.5\baselineskip}
%\moddate
6 April 1993

\vspace{3\baselineskip} 

%\fbox{\begin{minipage}{.75\textwidth} 
%\LARGE THIS PAGE SHOULD NOT APPEAR IN THE
%PROCEEDINGS.
%\end{minipage}}

 \end{center}
 

 \vspace{7\baselineskip} 
 
 \noindent
% All but this page 
To appear in:
Hans Rischel and Anders~P. Ravn, editors, {\em Hybrid Systems},
  Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag.
(Proceedings of a Workshop on Theory of Hybrid
Systems, held 19--21 October 1992 at Lyngby, Denmark.)
 \vfill \vfill 
 \newpage

\setcounter{page}{1}

\maketitle

\begin{abstract}
\TLA+ is a general purpose, formal specification language based on the
Temporal Logic of Actions, with no built-in primitives for specifying
real-time properties.  Here, we use \TLA+ to define operators for
specifying the temporal behavior of physical components obeying
integral equations of evolution.  These operators, together with
previously defined operators for describing timing constraints, are
used to specify a toy gas burner introduced by Ravn, Rischel, and
Hansen.  The burner is specified at three levels of abstraction, each
of the two lower-level specifications implementing the next
higher-level one.  Correctness proofs are sketched.
\end{abstract}

%try
\section{Introduction}

\TLA+ is a formal specification language based on TLA, the Temporal
Logic of Actions~\cite{lamport:newtla}.  We use \TLA+ to specify and
verify a toy hybrid system---a gas burner described by Ravn, Rischel,
and Hansen (RRH)~\cite{ravn:specifying}.  The \TLA+ specification and
proof can be compared with the one by RRH that uses the Duration
Calculus.

We do not expect \TLA+ to permit the best possible specification of
this or any other particular example.  The specification of a gas
burner is likely to be simpler in a formalism devised expressly for
the class of hybrid systems that includes the gas burner.  The
specification of a Modula-3 procedure is likely to be simpler in a
formalism for specifying Modula-3 procedures.  But, while \TLA+ may
not be the best method for specifying any particular system, we
believe it is quite good for specifying a very wide class of systems,
including gas burners and Modula-3 procedures.

There are two reasons for using \TLA+ instead of a language tailored
to the specific problem.  First, specialized languages often have
limited realms of applicability.  A language that permits a simple
specification for one gas burner might require a very complicated one
for a different kind of burner.  The Duration Calculus seems to work
well for real-time properties; but it cannot express simple liveness
properties.  A formalism like \TLA+ that, with no built-in primitives
for real-time systems or procedures, can easily specify gas burners
and Modula-3 procedures, is not likely to have difficulty with a
different kind of gas burner.

The second reason for using \TLA+ is that formalisms are easy to
invent, but practical methods are not.  A practical method must have a
precise language and robust tools.  Building tools is not easy.  It is
hard to define a language that is powerful enough to handle practical
problems and yet has a precise formal semantics.  Such a language is a
prerequisite for any sound, practical method.  The advantage of not
having to implement a new method for every problem domain is obvious.

An important criterion for choosing a formalism is how good it is for
formal verification.  A method based on a logic has an advantage over
one based on an abstract programming language (such as CSP) because
one does not have to translate from the specification language to a
logic for reasoning.  But, not all logics are equal.  TLA works well
in practice because most of the reasoning is in the domain of actions,
which is the realm of ``ordinary'' mathematical reasoning.  The use of
temporal logic is minimal and highly ritualized.  The temporal
structure of the proofs are the same, regardless of whether one is
reasoning about a mutual exclusion algorithm or a gas burner.

Modal logics, such as temporal logic and the Duration Calculus, are
more difficult to use than ordinary logic.  One reason is that the
deduction principle, from which one deduces $P\implies Q$ by assuming
$P$ and proving $Q$, is invalid for most modal logics.  
In our work on the
mechanical verification of TLA~\cite{engberg:mechanical}, we have
found formalizing temporal logic reasoning to be much more difficult
than formalizing ordinary mathematical reasoning.  Temporal logic
proofs that look simple when done by hand can be tedious to check
mechanically.  We believe that mechanical verification of TLA proofs
is feasible largely because it involves very little temporal logic.
One should be skeptical of claims that reasoning in a modal logic is
easy in the absence of experience with mechanically checked proofs.

\TLA+ is a complete language, with a precise syntax and formal
semantics.  At the moment, only a few syntactic issues remain
unresolved.  Because it is completely formal, some things are a little
more awkward to express in \TLA+ than in ``semi-formal'' methods.  For
example, most semi-formal methods, such as
Unity~\cite{chandy:parallel} and the temporal logic of Manna and
Pnueli~\cite{manna:temporal}, allow Boolean-valued variables; \TLA+
does not.  In \TLA+, one cannot declare $x$ to be a Boolean variable
and write $\Box x$, one must instead write something like
$\Box(x=\str{T})$.  Although seemingly innocuous, Boolean variables
pose the following problem.  A specification may require an array
$x[1]$, \ldots, $x[17]$ of flexible variables.  Formally, such an
array is a variable $x$ whose value is a function with domain $\{1,
\ldots, 17\}$.  If one can declare Boolean variables, then one should
also be able to declare that $x$ is a Boolean-valued array variable,
with index set $\{1, \ldots, 17\}$.  One can then write the formula 
$\Box(x[14])$.  One can also write the formula $\Box(x[i^2-23])$.  In
general, one could write the formula $\Box(x[e])$ for an arbitrary
integer-valued expression $e$.  Formalizing Boolean arrays presents
the following options:
\begin{itemize}
\item Define the meaning of $\Box(x[e])$ for any value of $e$.  Does
one consider $x[e]$ to have some special undefined value $\bot$ if $e$
is not in the domain of $x$?  If so, what is the meaning of $\Box\bot$?
Is the formula $\Box(\bot\implies\bot)$ valid?

\item Declare $\Box(x[e])$ not to be a wff (well formed formula) if
$e$ is not in the index set of $x$.
This leads to two possibilities:
\begin{itemize}
\item The class of expressions $e$ that can appear in the formula
$x[e]$ are restricted so it is syntactically impossible for the value
of $e$ not to be in the index set of $x$.  This leads to 
unnatural restrictions on formulas.

\item Whether or not a formula is a wff becomes a semantic rather than
syntactic property.  It is a strange formalism in which it is
undecidable whether a formula is a wff.
\end{itemize}
\end{itemize}
\TLA+ avoids this problem by not having Boolean-valued variables.
Neither Manna and Pnueli~\cite{manna:temporal} nor Misra and
Chandy~\cite{chandy:parallel}, in books that are hundreds of pages
long, indicate how they formalize Boolean arrays.

There are dozens of similar issues that must be resolved in designing
a complete language.  A simple informal specification might not look
so simple if it had to be written formally.  Of particular concern are
formalisms based on a type system.  It is easy to introduce the
informal notation that $\vbl{Length}(s)$ denotes the length of the
sequence $s$.  But, will the type system really allow a formal
language in which the user can define $\vbl{Length}(s)$ to denote the
length of {\em any\/} sequence $s$?  It is easy to define such a
\vbl{Length} operator in \TLA+.  However, this ability is based on a
distinction between a function and an operator---a distinction
one won't find in semi-formal methods.

Despite being completely formal, \TLA+ is simple enough for practical
applications.  A general treatment of hybrid systems requires
continuous mathematics.  Specifying the gas burner requires defining
the Riemann integral $\int_{a}^{b}f$ of the function $f$ over the
closed interval \ccInterval{a}{b}.  Assuming only the set of real
numbers with the usual arithmetic operations and ordering relations,
the entire definition takes about 15 lines.  Our example
is a toy one, and we do not claim to have formalized any significant
fraction of the mathematics that will be needed in practical
applications.  We do claim that a language that can define the Riemann
integral in 15 lines is powerful enough to express any mathematical
concepts likely to arise in real specifications.


\TLA+ specifications are written in ASCII\@.  We hope eventually to
write a program that converts an ASCII specification to input for a
text formater that produces a ``pretty-printed'' version.  The user will
specify how individual operators are formated---for example,
declaring that the \gram{Integral} operator should be formated so
\gram{Integral(a, b, f)} is printed as $\int_{a}^{b}f$, and that
\gram{[|s|]} should be printed as $|s|$.  We have simulated such a
program to produce pretty-printed \TLA+ specifications.  



%try
\vspace{.5\baselineskip}

\section{Representing Hybrid Systems with TLA}

This section describes the generic operators that can be used to
specify hybrid systems.  The precise \TLA+ definitions of some
operators is deferred to Section~\ref{sec:gas-burner}.
Figure~\ref{fig:TLA+operators} contains a complete list of all the
predefined \TLA+ constant operators---the ones that describe data
structures.  The only additional operators are TLA's action operators
(such as {\em Enabled\/}) and temporal operators (such as $\Box$).
The syntax and formal semantics of these operators, which fit on one
page, can be found in~\cite{lamport:newtla}.

\begin{figure}[tp]
% \renewcommand{\bnf}[1]{\mbox{\small $\langle\mbox{\it #1\/}\rangle$}}
\centering
\begin{tabbing}
\hspace*{1em}\=\+\kill
\bf \hspace*{-1em}Logic\\
%$\forall\, x : \mbox{\small $[\gram{BOOL} | \ldots | \gram{TEMPORAL}]$} 
%   \,:\, p$   \hspace{.5em}\=\kill
%
\true \ \ \false \ \ $\land$ \ \ $\lor$ \ \ $\lnot$ 
  \ \ $\implies$ \ \ $\e$ \\
$\forall\, x : p$  \ \ \ \ $\exists\, x : p$  \ \ \ \ 
$\forall\, x \in S : p$  \ \ \ \ $\exists\, x \in S : p$\\ 
% \ \ \ \ 
{\bf choose $x:p$}   
   \hspace{.5em} \small [Equals some $x$ satisfying $p$] 
\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Sets}\\
$=$ \ \ $\neq$ \ \ $\in$ \ \ $\notin$ 
  \ \ $\cup$ \ \ $\cap$ \ \ $\subseteq$ \ \ 
  $\bs$ {\small [set difference]}\\
$\{e_1, \ldots , e_n\}$ \hspace{.5em}\= \kill
%
$\{e_1, \ldots , e_n\}$     
  \> \small [Set consisting of elements $e_i$] \\
$\{x \in S : p\}$       
  \> \small [Set of elements $x$ in $S$ satisfying $p$] \\
$\{e : x \in S \}$       
  \> \small [Set of elements $e$ such that $x$ in $S$] \\
\bf subset $S$
  \> \small [Set of subsets of $S$] \\
\bf union $S$
  \> \small [Union of all elements of $S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Functions}\\
{[}$f;\;e_{1}\,\mapsto\,e_{2}$]
  \hspace{.5em}\= \kill
{\bf  domain} $f$\ \ \ \ $f$[$e$]  
  {\small [Function application]}\\
{[}$x \in S$~$\mapsto$\ $\!e$]
  \> \small [Function $f$ such that $f[x]=e$ for $x\in S$]\\
{[}$S$ $\rightarrow$ $T$]            
  \> \small [Set of functions $f$ with $f[x]\in T$ for $x\in S$]\\
{[}$f;\;e_{1}\,\mapsto\,e_{2}$]
  \> \small [Function $\widehat{f}$ equal to $f$ except 
             $\widehat{f}[e_{1}]=e_{2}$]\\
{[}$f;\;e : S$]
  \> \small [Set of functions $\widehat{f}$ equal to $f$ except 
             $\widehat{f}[e]\in S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Records}\\
$\lr x_1 \mapsto e_1, \ldots , x_n \mapsto e_n \rr$
  \hspace{.5em}\= \kill
 %
$e.x$     
\> \small [The $x$-component of record $e$] \\
 %
$\lr x_1 \mapsto e_1, \ldots , x_n \mapsto e_n \rr$
  \> \small [The record whose $x_i$ component is $e_i$]\\
 %
$\lr x_1 : S_1, \ldots , x_n : S_n \rr$ 
 \> \small [Set of all records with $x_i$ component in $S_i$]\\
$\lr r;\; x$~$\mapsto$\ $\!e\rr$
  \> \small [Record $\widehat{r}$ equal to $r$ except 
             $\widehat{r}.x=e$]\\
$\lr r;\; x$~$:$\ $\!S\rr$
  \> \small [Set of records $\widehat{r}$ equal to $r$ except 
             $\widehat{r}.x\in S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Tuples}\\
 $S_1 \X \ldots \X S_n$ 
 \hspace{.5em}\= \kill
%
$e[i]$  \>   \small [The $i^{\rm th}$ component of tuple $e$]\\
\tuple{e_1, \ldots , e_n}
  \> \small [The $n$-tuple whose $i^{\rm th}$ component is $e_i$]\\
$S_1 \X \ldots \X S_n$
   \> \small [The set of all $n$-tuples with $i^{\rm th}$ component in $S_i$]
 \\[.5\baselineskip]
%
{\bf \hspace*{-1em}Miscellaneous} \\
{\bf let} $x_{1}\deq e_{1}$ \ldots\ $x_{n}\deq e_{n}$ {\bf in} $e$
  \hspace{.5em}\= \kill
 %
\str{$c_1 \ldots c_n$}   
   \> \small [A literal string of $n$ characters]\\
 %
{\bf if} $p$ {\bf then} $e_1$ {\bf else} $e_2$
  \> \small [Equals $e_1$ if $p$ true, else $e_2$]\\
 %
{\bf case} $p_1 \rightarrow e_1$, \ldots\,,\ $p_n \rightarrow e_n$
  \> \small [Equals $e_i$ if $p_i$ true]
 \\
{\bf let} $x_{1}\deq e_{1}$ \ldots\ $x_{n}\deq e_{n}$ {\bf in} $e$
  \> \small [Equals $e$ in the context of the definitions]
\end{tabbing}
\vspace{-\baselineskip}
\caption[]{The constant operators of \TLA+.}
\label{fig:TLA+operators}
\end{figure}


\subsection{Real Time in TLA}

A method for writing real-time specifications in TLA is described in
\cite{abadi:old-fashioned}.  We  now review this approach and introduce
\TLA+ by defining the operators from \cite{abadi:old-fashioned} in the
\TLA+ module \vbl{RealTime} of Figure~\ref{fig:RealTime}.

The \vbl{RealTime} module first imports the module \vbl{Reals}, which
is assumed to define the set \Real\ of real numbers with its usual
arithmetic operators.\footnote{Some people mistakenly think that,
because the reals are uncountable, letting time be a real number
complicates proofs.  The axioms about the real numbers needed to prove
such real-time properties as the correctness of Fischer's
protocol~\cite{abadi:old-fashioned} form a decidable theory.} The
module declares two parameters: the (flexible) variable \vbl{now} and
the constant $\oo$.  The value of \vbl{now} represents the current
time, which can assume any value in \Real.  The constant $\oo$ is the
usual infinity of mathematicians.  (All symbols that appear in a
module's formulas are either parameters or symbols that are defined in
terms of parameters.  The {\bf import} statement includes the
parameters of the module \vbl{Reals} as parameters of \vbl{RealTime}.)

\begin{figure}[t]
\begin{module}{RealTime}
{\bf import} \vbl{Reals}
\midbar
\begin{decls}{parameters}
  \vbl{now}  : {\bf variable}\\
  $\oo$ : {\bf constant}
\end{decls}
\midbar
\begin{decls}{assumption}
  \vbl{InfinityUnReal} \defeq\ $\oo\notin\Real$
\end{decls}

\begin{decls}{temporal}
  $\vbl{RT}(v)$ \defeq\ 
   \( \begin{conj}

\vbl{now} \in Real\\
      \Box [ \begin{conj}
               \vbl{now}' \in \{r \in \Real : r > \vbl{now}\}\\
               v' = v \s{.5}]_{\vbl{now}}
            \end{conj}
         \end{conj}\) \\[.4em]
%
$\vbl{VTimer}(x    : {\bf state\ fcn},\,
              \act{A}    : {\bf action},\,
         \delta, v : {\bf state\ fcn})$  \defeq\\
\s{1}    \( \begin{conj}
             x =  \pfif{\vbl{Enabled} \anact{A}{v}}{\vbl{now+\delta}}{\oo}\\
            \Box [ x' = \pfif{(\vbl{Enabled} \anact{A}{v})'}%
                           {\pfif{\anact{A}{v}}%
                               {\vbl{now}' + \delta}{x}}%
                          {\oo\s{1}]_{\tuple{x,\,v}}}
            \end{conj}\)\\[.4em]
%
$\vbl{MaxTimer}(x)$ \defeq\ 
       $\Box[(x \neq \oo) \implies (\vbl{now}' \leq  x)]_{\vbl{now}}$\\[.4em]
%
$\vbl{MinTimer(x: {\bf state\ fcn},\, 
               \act{A} : {\bf action},\, 
               v : {\bf state\ fcn})}$ \defeq\ $\Box[\anact{A}{v} 
                 \implies (\vbl{now} \geq x)]_{v}$
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The \vbl{RealTime} module.}
\label{fig:RealTime}
\end{figure}

Next comes an assumption, named \vbl{InfinityUnReal}, which asserts
that $\oo$ is not a real number.  The keyword {\bf temporal} heads a
list of definitions of temporal formulas.  The first definition in the
list defines $\vbl{RT}(v)$ to be a formula asserting that \vbl{now} is
initially in \Real, and every step either (i)~sets the new value of
\vbl{now} to a real number greater than its current value and
(ii)~leaves the value of $v$ unchanged, or else it leaves \vbl{now}
unchanged.  (A list of formulas bulleted with $\land$ denotes their
conjunction.  The formula \sqact{A}{w} is defined to equal
$\act{A}\,\lor\,(w'=w)$; a \sqact{A}{w} step is thus either an \act{A}
step or a step that leaves $w$ unchanged.)  In representing a system
by a TLA formula, the discrete variables of the system are considered
to change instantaneously, meaning that when they change, \vbl{now}
remains unchanged.  This is asserted by the formula $\vbl{RT}(v)$ when
$v$ is the tuple whose components are the system's discrete variables.


In \cite{abadi:old-fashioned}, timing constraints are expressed through
the use of timer variables.  The formula 
  $\vbl{VTimer}(x, \act{A}, \delta, v)$ 
asserts that $x$ is a timer whose value is initially either
(i)~$\delta$ greater than the initial value of \vbl{now} or
(ii)~$\oo$, depending on whether or not action \anact{A}{v} is
enabled.  The value of $x$ is set to $\vbl{now}+\delta$ when
either (i)~\anact{A}{v} becomes enabled or (ii)~an \anact{A}{v} step
occurs that leaves \anact{A}{v} enabled, and it is set to $\oo$ when
\anact{A}{v} becomes disabled.\footnote{Another type of timer is also
defined in \cite{abadi:old-fashioned}, but it is not needed here.}
(The action $\anact{A}{v}$ is defined to equal $\act{A}\land(v'\neq
v)$; an $\anact{A}{v}$ step is thus an \act{A} step that changes $v$.)
The formula $\vbl{MaxTimer}(x)$ asserts that changing \vbl{now} cannot
make it greater than $x$.  Thus, the formula
  $\vbl{VTimer}(x, \act{A}, \delta, v)\land\vbl{MaxTimer}(x)$ 
implies that an \anact{A}{v} action cannot be continuously enabled for
more than $\delta$ seconds without having occurred.
The formula $\vbl{MinTimer}(x,\act{A},v)$
asserts that an \anact{A}{v} action cannot occur unless 
 $\vbl{now}\geq x$, so
  $\vbl{VTimer}(x, \act{A}, \delta, v)\land\vbl{MinTimer}(x,\act{A},v)$ 
implies that an \anact{A}{v} action must be enabled for at
least $\delta$ seconds before it can occur.

The definitions of \vbl{VTimer} and \vbl{MinTimer} explicitly
indicate the {\em sorts\/} of the parameters.  When no sort is
specified, the sort {\bf state fcn}, denoting a mapping from states to
values, is assumed---except in the definitions of constants, where
the default sort is {\bf constant}, denoting a constant value.

There are many ways of defining timers for expressing real-time
constraints, and they are all easily expressed in \TLA+.  The method
used in \cite{abadi:old-fashioned} is probably not optimal for the gas
burner example.  Although we might be able to simplify the
specifications in this example by defining a new kind of timer, in
practice one would use a fixed set of operators defined in a standard
module like \vbl{RealTime}.  To make the example more realistic, we have
used a pre-existing set of operators.

\subsection{Hybrid Systems} To represent hybrid systems in TLA,
continuous system variables are represented by variables that change
when \vbl{now} does.  The gas-burner specification of RRH can be
expressed using only the timers introduced in
\cite{abadi:old-fashioned}.  However, RRH's specification is somewhat
artificial, apparently chosen to avoid reasoning with continuous
mathematics.  Instead of the natural requirement that the
concentration of unburned gas never exceeds some value, RRH require
that unburned gas never be released for more than 4 seconds out of any
30-second period.  Because it poses an interesting new challenge for
\TLA+, we specify the more natural requirement and prove that it is
implied by the requirement of RRH.

The gas concentration $g$ will satisfy an integral equation of the form
 \[ g(t) = \int_{t_{0}}^{t} F(g(t))\,dt
 \]
where the function $F$ depends on the discrete variables.  A more
general situation is a continuous variable $f$ that satisfies an
equation of the form
\begin{equation} \label{eq:evolution}
  f(t) = f_{0} + \int_{t_{0}}^{t} G(f(t),t)\,dt
\end{equation}
A further generalization is to let $f$ be a function whose range is
the set of $n$-tuples of reals.  However, this generalization is
straightforward and is omitted.

For specifying hybrid systems, we define a TLA formula, 
pretty-printed as \evolver{x}{c}{G}{\act{A}}{v}, having the following
meaning:
\begin{itemize}
\item Initially, $x$ equals $c$.

\item In any step that changes \vbl{now}, the new value $x'$ of
      $x$ equals $f(\vbl{now}')$, where $f$ is the solution to
      $f(t) = x + \int_{\vbl{now}}^{t} G(f(s),s)\,ds$.

\item Any step that leaves \vbl{now} unchanged leaves 
      $x$ unchanged, unless it is an \anact{A}{v} step, in which
      case $x'$ equals zero.
\end{itemize}
Thus, \evolver{x}{c}{G}{\false}{v} asserts that $x$ represents the
solution to (\ref{eq:evolution}) with $f_{0}$ equal to $c$ and
$t_{0}$ the initial value of \vbl{now}.  The general formula
\evolver{x}{c}{G}{\act{A}}{v} adds the requirement that $x$ is reset
to 0 by an \anact{A}{v} action.  The precise definition of
\evolver{x}{c}{G}{\act{A}}{v} is given later, in the \vbl{HybridSystems}
module.

It is often useful to describe the amount of time a predicate $P$ has
been true, which is the integral over time of a step function that
equals 1 when $P$ is true and zero when it is false.  The formula
\evolver{x}{0}{\chi(P)}{\false}{v} asserts that the value of $x$
always equals this integral, where the function $\chi(P)$ is defined
by
  \[ \chi(P)(r,s) = \left\{
     \begin{array}{ll}
        1 & \mbox{if $P=\true$}\\
        0 & \mbox{if $P=\false$}
     \end{array}\right.
 \]
The formal definition of $\chi$ appears in the \vbl{HybridSystems}
module.

%try

\section{The Gas Burner} \label{sec:gas-burner}

The example system is the gas burner shown in
Figure~\ref{fig:GasBurnerSystem}.  
\begin{figure}[t]
\setlength{\unitlength}{1mm}
\begin{center}\begin{picture}(80,34)(0,8)

%pipe sections
\put(0,20){\line(1,0){15}}
\put(0,24){\line(1,0){15}}
\put(25,20){\line(1,0){10}}
\put(25,24){\line(1,0){10}}
%gas nozzle
\put(35,24){\line(5,-1){5}}
\put(35,20){\line(5,1){5}}
%CV2
\put(15,17){\line(0,1){10}}
\put(25,17){\line(0,1){10}}
\put(15,17){\line(1,1){10}}
\put(25,17){\line(-1,1){10}}
\put( 5,32){\makebox(0,0)[l]{Gas supply}}
%IT+SP
\put(42,29){\framebox(6,6){}}
\put(43,26){\line(0,1){3}}
\put(47,26){\line(0,1){3}}
\put(43,26){\line(1,0){1}}
\put(50,32){\makebox(0,0)[l]{Ignition transformer}}
\put(47,26){\line(-1,0){1}}
%FS
\put(43,17){\framebox(4,1){}}
\put(42,11){\framebox(6,6){}}
%\put(41,17){\line(1,0){2}}
%\put(49,17){\line(-1,0){2}}
%\put(41,17){\line(0,-1){5}}
%\put(49,17){\line(0,-1){5}}
\put(50,14){\makebox(0,0)[l]{Flame detector}}
%flame
\put(42,23){\line(6,1){12}}
\put(42,22){\line(1,0){12}}
\put(42,21){\line(6,-1){12}}
\put(64,22){\makebox(0,0){Flame}}
%connections
\put(0,8){\vector(1,0){30}}
\put(0,10){\makebox[0mm][l]{Heatreq signal}}

\end{picture}\end{center}
\caption{The gas burner.  (Figure taken from
\protect\cite{ravn:specifying}.)} \label{fig:GasBurnerSystem}
\end{figure}
This is the toy example of RRH\@.
Our goal is to write a specification that is in the spirit of RRH's;
the specification of a real gas burner might be much more complex.

The discrete state of the system consists of the states of the gas,
the heat-request signal, the flame, and the ignition---each of which
can be either on or off.  These state components are represented by
the four variables declared in the module \vbl{BurnerParameters} of
Figure~\ref{fig:BurnerParameters}.  A physical state in which the gas
is turned on or off will be represented by a state in which the value
of the variable \vbl{gas} is the string \str{on} or
\str{off\s{.1}}\s{-.2}.  The {\em on\/} and {\em off\/} values of the
other variables are similarly denoted by the strings \str{on} and
\str{off\s{.1}}\s{-.2}.  As is customary in TLA specifications, we
define a state function $v$ that equals the tuple of all relevant
variables.  (In \TLA+, angle brackets \tuple{\ } denote tuples.)  To
make it easier to compare our specification with theirs, we have also
defined state predicates that correspond to the Boolean variables of
RRH\@.


\begin{figure}[t]
\begin{module}{BurnerParameters}
{\bf import} \vbl{HybridSystems}, \vbl{RealTime}
\midbar
\begin{decls}{parameters}
  \vbl{gas}, \vbl{heatReq}, \vbl{flame}, \vbl{ignition} : {\bf variables}
\end{decls}
\midbar
\begin{decls}{state function}
\vbl{v} \defeq\ 
   \tuple{\vbl{gas},\; \vbl{heatReq},\; \vbl{flame},\; \vbl{ignition}}
\end{decls}
\begin{decls}{predicates}
  \vbl{Ignition} \= \defeq\ \vbl{ignition} \= \kill
  \vbl{Gas}      \defeq\ \vbl{gas}      = \str{on}\\
  \vbl{Flame}    \defeq\ \vbl{flame}    = \str{on}\\
  \vbl{Heatreq}  \defeq\ \vbl{heatReq}  = \str{on}\\
  \vbl{Ignition} \defeq\ \vbl{ignition} = \str{on}
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{Module {\em BurnerParameters\/}}
\label{fig:BurnerParameters}
\end{figure}

For convenience, the \vbl{BurnerParameters} module imports the modules
\vbl{HybridSystems} and \vbl{RealTime} that define the operators
described above.  Since the \vbl{RealTime} module also imports the real
numbers, they are transitively imported by the \vbl{BurnerParameters}
module.

We now specify the requirement that the concentration of gas remains
less than some value \vbl{MaxCon}.  We assume that the gas concentration
$g$ is described by the integral equation
 \[ g(t) = \int_{t_{0}}^{t} -\delta g(t) + \left\{
     \begin{array}{ll}
         \rho & \mbox{if gas on and flame off}\\
         0    & \mbox{otherwise}
     \end{array}\right\} dt
 \]
where $\delta$ is the rate at which gas diffuses away from the burner
and $\rho$ is the rate at which gas flows when it is turned on.

Using the TLA formula \evolver{x}{c}{G}{\act{A}}{v}, it is easy to
specify the requirement that the gas concentration is always less
than \vbl{MaxCon}.  First, the function \vbl{accumRate} that
is substituted for $G$ is defined as follows.
 \[ \mbox{\vbl{accumRate}[$r$, $s$ : \Real]  \defeq\
    $(-\delta) * r$ $+$  
        $({\bf if}\;\; \vbl{Gas} \land \lnot\vbl{Flame} \;\;{\bf then}\;\;
              \rho \;\;{\bf else}\;\; 0)$}
 \]
This defines \vbl{accumRate} to be a function whose domain is
$\Real\times\Real$ such that $\vbl{accumRate}[r,s]$ equals the
expression to the right of the $\deq$, for every pair \tuple{r,\,s} in
$\Real\times\Real$.  (In \TLA+, square brackets denote function
application.)

The formula \evolver{g}{0}{\vbl{accumRate}}{\false}{v} then asserts
that $g$ describes the gas concentration.  As usual, the temporal
formula $\Box(g < \vbl{MaxCon})$ asserts that $g$ is always
less than \vbl{MaxCon}, so the formula
 \[ \mbox{\evolver{g}{0}{\vbl{accumRate}}{\false}{v}
           $\implies$ $\Box(g < \vbl{MaxCon})$}
 \]
asserts that if $g$ is the gas concentration, then $g$ is always less
than \vbl{MaxCon}.  We want this formula to be true for an arbitrarily
chosen, ``fresh'' variable $g$, so the desired property is obtained by
universally quantifying $g$.\footnote{The symbols $\EE$ and $\AA$
denote quantification over flexible variables; $\exists$ and $\forall$
denote ordinary quantification over rigid variables.}

The complete definition of this property,
which is called \vbl{Req0}, is given in module
\vbl{GasConcentration}, shown in Figure~\ref{fig:GasConcentration}.
This module imports the \vbl{BurnerParameters} module, which defines
\vbl{Gas} and \vbl{Flame}, and declares $\delta$, $\rho$, and
\vbl{MaxCon} to be constant parameters whose values lie in the set of
positive reals.  This ``type declaration'' is a shorthand for
the {\bf assumption}
 \[ % \begin{conj}
         (\delta \in \{r \in \Real : r > 0\}) \;\land\;
         (\rho \in \{r \in \Real : r > 0\})\;\land\;
         (\vbl{MaxCon} \in \{r \in \Real : r > 0\})
  % \end{conj}
 \]
\begin{figure}[t]
\begin{module}{GasConcentration}
{\bf import} \vbl{BurnerParameters}
\midbar
\begin{decls}{parameters}
 $\delta$, $\rho$, \vbl{MaxCon} : $\{r \in \Real : r > 0\}$ {\bf const}
\end{decls}
\midbar
\begin{decls}{state function}
  \vbl{accumRate}[$r$, $s$ : \Real]  \defeq\
    $(-\delta) * r$ $+$  
        $({\bf if}\;\; \vbl{Gas} \land \lnot\vbl{Flame} \;\;{\bf then}\;\;
              \rho \;\;{\bf else}\;\; 0)$
\end{decls}
\begin{decls}{temporal}
  \vbl{Req0} \defeq\ \AA\ $g$ : 
     \evolver{g}{0}{\vbl{accumRate}}{\false}{v}
           $\implies$ $\Box(g < \vbl{MaxCon})$
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The specification of the gas-concentration requirement}
\label{fig:GasConcentration}
\end{figure}

Next, we define the three requirements given by RRH\@.  The first
requirement is
\begin{quote}
 For Safety, gas must never leak for more than 4 seconds in any period
 of at most 30 seconds.
\end{quote}
This is a requirement for the 30-second interval beginning at time
$r$, for every real $r$.  It is expressed in terms of an array $x$ of
timers, where $x[r]$ is the timer used to express the requirement for
the interval beginning at $r$.  The amount of gas that has leaked
during the interval \ccInterval{r}{r+30} is obtained by
``integrating'' the function $G(r)$ that is defined by
 \[ \mbox{\( G(r)[s, t : \Real] \) \defeq\ 
               {\bf if} $\;\vbl{Gas} \land \lnot\vbl{Flame}
                          \land (t \in \ccInterval{r}{r+30})\;$ {\bf then}
                          $\;1\;$ {\bf else} $\;0\;$}
 \] 
This defines $G$ to be an operator such that, for any $r$, the
expression $G(r)$ denotes a function with domain
$\Real\times\Real$.\footnote{A function $f$ has a domain; it is an
ordinary value.  Thus $G(7)$ and $G(7)[\sqrt{2},.5]$ both denote
values; the first is a function, the second a real number.  To define a
function, one must specify its domain.  However, $G$ is an operator,
not a function.  It is not a value, and it does not have a domain; the
symbol $G$ by itself is not a syntactically correct expression.  The
definition above defines $G(r)$ for any value of $r$, not just for real
numbers.  We had to define $G(r)$ to be a function because it appears as
a function, without any arguments, in subsequent formulas.  We could
have defined $G$ to be a function by writing
 $G[r : \Real][\ldots]$, but there is no need to make $G$ a function, 
and we didn't feel like writing the ``:~\Real''.
%
The distinction between operators and functions is another example of
the details that arise in defining a precise language with a formal
semantics.  This distinction is what allows one easily to define in
\TLA+ an operator \vbl{Length} such that $\vbl{Length}(s)$ is the
length of {\em any\/} sequence $s$.  One could not define \vbl{Length}
to be a function, since its domain would not be a set.  (Its domain
would be isomorphic to the ``set'' of all sets.)}


Using $x[r]$ as a timer, the requirement for this interval
is expressed by
 \[ \mbox{\( \evolver{x[r]}{0}{G(r)}{\false}{v} \)
            $\;\implies\;$
           \(  \Box(x[r] \leq 4))\)}     
 \]
The requirement \vbl{Req1} is obtained by quantifying over all real
numbers $r$, and then universally quantifying $x$.  The complete
definition is given in module \vbl{BurnerRequirements} in
Figure~\ref{fig:BurnerRequirements}.  
\begin{figure}[t]
\begin{module}{BurnerRequirements}
{\bf import} \vbl{BurnerParameters}
\midbar
\begin{decls}{temporal}
  \vbl{Req1} \defeq\ \=
     {\bf let} \= \( G(r)[s, t : \Real] \) \defeq\ \\
    \>   \> \s{1}%
               {\bf if} $\;\vbl{Gas} \land \lnot\vbl{Flame}
                          \land (t \in \ccInterval{r}{r+30})\;$ {\bf then}
                          $\;1\;$ {\bf else} $\;0\;$
               \\[.2em]
    \> {\bf in} \>
       \AA\ $x$ : 
            \( \forall\, r \in \Real \)
                  : \= \( \evolver{x[r]}{0}{G(r)}{\false}{v} \)
%\\\>\>\>\s{1} (\forall\, r \in \Real : 
  $\implies$
           \(  \Box(x[r] \leq 4))
           \) \\[.4em]
%
  \vbl{Req2} \defeq\ \AA\ $x$ : 
              \= \( \evolver{x}{0}{\chi(\vbl{Flame}\land\lnot\vbl{HeatReq})}%
                    {\vbl{Heatreq}'\lor\lnot\vbl{Flame}'}{v} \)\\
                \> \s{1}$\implies$ $\Box(x \leq 60)$
\end{decls}
\begin{decls}{actions}
\vbl{IgniteFailAct}(\vbl{y}) \defeq\
    \( \begin{conj}
         \vbl{Gas}\land \vbl{Ignition}\land \lnot\vbl{Flame}\\
         \vbl{y}' \neq \vbl{y}\\
         {\bf unchanged} \tuple{v,\, \vbl{now}}
      \end{conj} 
    \)\\
\vbl{Req3Reset}(\vbl{y}) \defeq\ 
 \( \vbl{Flame}' \lor (y'\neq y)
     \lor \lnot\vbl{Heatreq}' \)\vs{.5}
\end{decls}
\begin{decls}{temporal}
 \vbl{IgniteFail}(\vbl{y}) \defeq\ 
\EE\ $z$ : 
   \( \begin{conj}
        \Box\sqact{{}\vbl{IgniteFailAct}(\vbl{y})}{\vbl{y}}\\
        \vbl{VTimer}(z, \vbl{IgniteFailAct}(\vbl{y}), 1/2, \vbl{y})\\
        \vbl{MaxTimer}(z)\\
        \vbl{MinTimer}(z,\vbl{IgniteFailAct}(\vbl{y}), \vbl{y})
      \end{conj}\)\\[.2em]

 \vbl{Req3} \defeq\ \AA\ $x$, \vbl{y} :
     \= \( \begin{conj}
           \vbl{IgniteFail}(\vbl{y})\\
           \evolver{x}{0}{\chi(\vbl{Heatreq})}%
              {\vbl{Req3Reset}(\vbl{y}) }%
              {\tuple{v,\, \vbl{y}}}
           \end{conj} \)\\
    \>$\implies$ 
           $\Box(x \leq 60)$
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The three requirements of Ravn, Rischel, and Hansen.}
\label{fig:BurnerRequirements}.
\end{figure}
(Our formulas \vbl{Req1},
\vbl{Req2}, and \vbl{Req3} correspond to the formulas
$\Box\vbl{Req}_{1}$, $\Box\vbl{Req}_{2}$, and $\Box\vbl{Req}_{3}$ of
RRH.)


The second requirement is
\begin{quote}
  Heat request off shall result in the flame being off after
  60 seconds.
\end{quote}
This condition is expressed by using a variable $x$ that integrates the
amount of time the flame has been on while the heat request was
off, and is reset to zero whenever the flame goes off or the heat
request comes back on.\footnote{This requirement, which comes from
RRH, is satisfied if the heat request is always off and the flame is
always on except for flickering out briefly every 59.9 seconds.} Such a
variable $x$ satisfies the formula
 \[ \evolver{x}{0}{\chi(\vbl{Flame}\land\lnot\vbl{HeatReq})}%
                    {\vbl{Heatreq}'\lor\lnot\vbl{Flame}'}{v} 
 \]
Asserting that $x$ is always less than 60 and quantifying over $x$
yields condition \vbl{Req2} of Figure~\ref{fig:BurnerRequirements}.

The final requirement is 
\begin{quote}
Heat request shall after 60 seconds result in gas burning unless an
ignite or flame failure has occurred.  An ignite failure happens when
gas does not ignite after 0.5 seconds.  The flame fails if it
disappears while gas is supplied.
\end{quote}
A careful analysis of this condition reveals that replacing ``after
60 seconds'' by ``within 60 seconds'' makes the ``or flame failure''
redundant.  We can therefore rewrite this requirement as
\begin{quote}
Heat request shall, within 60 seconds, result in gas burning unless an
ignite failure has occurred.
\end{quote}
The obvious approach is to define a variable $x$ that integrates the
time during which the heat request is on and is reset by the presence
of a flame, an ignite failure, or the heat request being turned off.
We would then define an \vbl{IgniteFail} action,
define the action \vbl{Req3Reset} to be
 \( \vbl{Flame}' \lor
                  \vbl{IgniteFail} \lor \lnot\vbl{Heatreq}' 
 \)
and write the requirement as
 \[ \mbox{\AA\ $x$ :
     \evolver{x}{0}{\chi(\vbl{Heatreq})}%
              {\vbl{Req3Reset}}%
              {v}}
  \,\implies\,\Box(x \leq 60)
 \]
However, there is no actual \vbl{IgniteFail} action.  An ignite
failure is not a change of the discrete state variables; it is
something that is caused by the passage of time.  So, we must
introduce a variable $y$ that is changed when an ignite failure
occurs.  Since $y$ should not be a free variable of the formula, it
must be ``quantified away''.  We want $y$ to change when the ignition
and the gas have been on for precisely .5 seconds while the flame has
been off.  This is accomplished with a .5-second ``vtimer'' for the
action that changes $y$.  We define $\vbl{IgniteFailAct}(y)$ to be an
action that changes $y$ while leaving the other variables unchanged,
and is enabled precisely when the gas and ignition are on and the
flame is off.  An ignition failure happens when this action has been
continuously enabled for precisely .5 seconds.  So, we let
 \[ \vbl{IgniteFailAct}(y) \;\;\deq\;\; \begin{conj}
         \vbl{Gas}\,\land\, \vbl{Ignition}\,\land\, \lnot\vbl{Flame}\\
         (\vbl{y}' \neq \vbl{y}) \,\land\, 
         {\bf unchanged}\; \tuple{v,\, \vbl{now}}
   \end{conj} 
 \]
where {\bf unchanged} $f$ denotes $f'=f$.  The TLA formula
 \( \Box \sqact{{}\vbl{IgniteFailAct}(y)}{y}
 \)
asserts that $y$ changes only when 
 $\vbl{Gas}\land \vbl{Ignition}\land \lnot\vbl{Flame}$
is true.  To assert that this change occurs only when the
$\vbl{IgniteFailAct}(y)$ action has been enabled for precisely .5
seconds, we add a timer $z$ with both a \vbl{MaxTimer} and
\vbl{MinTimer} condition.  The temporal formula $\vbl{IgniteFail}(y)$
defined in Figure~\ref{fig:BurnerRequirements} asserts that an ignition
failure has occurred iff $y$ has changed.  The definition of
the formula \vbl{Req3} expressing the third requirement is now
straightforward and appears in Figure~\ref{fig:BurnerRequirements}.

We would like to prove the gas concentration condition \vbl{Req0} from
the three requirements of RRH. This condition actually follows from
\vbl{Req1}.  The precise theorem, expressed in \TLA+, is that
if
 \[ \vbl{MaxCon} \geq 4*\rho*(1 + (1 / (1 - \exp[(-30)*\delta])))
\]
then 
  \( \vbl{RT}(v) \land \vbl{Req1} \,\implies \vbl{Req0}\),
where $\exp$ is the usual exponential function.  Before proving this,
we finish the specification by defining the operators we have
been assuming.

%try 
\section{The Module \vbl{HybridSystems}}

The \vbl{HybridSystems} module involves the solution to an integral
equation.  Defining this requires first defining the definite
integral.  The Riemann integral of a function $f$ on an interval is
the signed area under the graph of $f$.  It is defined as the limit of
approximations obtained by breaking the interval into subintervals,
where the area under the graph of $f$ from $p$ to $q$ is approximated
by $f(p)(q-p)$.  The definition of $\int_{a}^{b}f$ appears in module
\vbl{Integration} of Figure~\ref{fig:Integration}.  The informal
meanings of the defined operators are explained below.
\begin{description}
\item[\PosReal] The set of positive reals.


\begin{figure}[tbp]
\begin{module}{Integration}
{\bf import} \vbl{Reals}
\midbar
\begin{decls}{constants}
 \PosReal\  \defeq\ $\{r \in \Real : 0 < r\}$\\[.2em]
%
  \ccInterval{a}{b} \defeq\ 
      \( \{r \in \Real : ((a \leq r) \land (r \leq b)) % \\
                          \,\lor\, ((a \geq r) \land (r \geq b)) \}
     \)\\[.2em]
%  
  $|r|$  \defeq\ {\bf \,if\,} $r < 0$ {\bf \,then\,} $-r$ 
                       {\bf \,else\,} $r$\\[.2em]
%
  $\{m \ldots n\}$ \defeq\ 
          $\{i \in \vbl{Nat} : (m \leq i) \land (i \leq n)\}$
  \\[.2em]
%
  $\vbl{Partition}(a,\, b,\, n,\, \delta)$ \defeq\ \\
%  
\s{1}\( \{\,p \in [\{0\ldots n\!+\!1\} \rightarrow \ccInterval{a}{b}] : 
%
     \begin{conj}
          (p[0] = a) \land (p[n\!+\!1] = b) \\
         \forall\, i \in \{0\ldots n\} : 
             \begin{conj}
                \begin{disj}
                  (a \leq b) \land (p[i] \leq p[i\!+\!1])\\
                  (a \geq b) \land (p[i] \geq p[i\!+\!1]) 
                 \end{disj} \\
               |p[i\!+\!1] - p[i]| < \delta     \s{3.75}\}
            \end{conj}
     \end{conj} \) \\[.4em]
%
  $\approxint(f,\,p)[n : \vbl{Nat}]$ \defeq\
    \= \( f[p[n]] * (p[n\!+\!1] - p[n]) \)\\[.1em]
    \>  \s{1}$+\;$ {\bf if}\, $n = 0$ \,{\bf then}\, 0 \,{\bf else}\,
               $\approxint(f,p)[n-1]$\\[.2em]
%
  $\int_{a}^{b}f$ \defeq\ 
    {\bf choose} $r$ : 
    \( \begin{conj}
           r \in \Real\\
        \begin{array}[t]{@{}l@{}}
         \forall\, \epsilon \in \PosReal : 
            \exists\, \delta \in \PosReal :
              \forall n \in \vbl{Nat} : \\
               \s{1}\forall\, p \in \vbl{Partition}(a,\,b,\,n,\,\delta) :
                | r - \approxint(f,\,p)[n] | < \epsilon
            \end{array}
       \end{conj} \) \\[.4em]
%

  $\evolve{c}{a}{G}[r : \Real]$ \defeq\ \\
   \s{1}\={\bf let} \= $f$ \defeq\ {\bf choose} $f$ : 
             \( \begin{conj}
                  f \in [ \ccInterval{a}{r} \rightarrow \Real]\\
                 \forall\, t \in \ccInterval{a}{r} :
                    f[t] = c + \int_{a}^{t}[s \in \Real \mapsto G[f[s],s]]
                 \end{conj} \)\\
  \> {\bf in} \> $f[r]$
\end{decls}
\begin{decls}{theorem}
%$\vbl{IntegralOfConstant}$ \defeq\ \\
%\s{1}$\forall\, G : \forall\, a, b, c, d \in \Real :$\\ 
%\s{2} $(\forall s, t \in \Real : G[s,t] = d)
%   \;\implies\; (\evolve{c}{a}{G} = [r\in \Real \mapsto c+(r-a)*d]$ \\[.4em]
$\vbl{IntegralOfStepFcn}$ \defeq\ \\
\s{1}$\forall\, G : \forall\, a, b, \delta \in \Real :
\forall\,n\in \vbl{Nat} : \forall\,p\in\vbl{Partition}(a,\, b,\, n,\, \delta):
\forall\,f\in[\Real\rightarrow\Real]:
  $\\ 
\s{2}$(\forall\,s,t\in\Real:\forall\,i\in\{0\ldots n\} :
      (p[i] < t)\land(t<p[i+1])\implies (G[s,\,t]=f(p[i])))$\\
\s{3} $\implies\;\; (\evolve{c}{a}{G}[b] = \approxint(f,\,p)[n])
$
\end{decls}

\end{module}
\vspace{-\baselineskip}
\caption{Defining integration in \TLA+.}
\label{fig:Integration}
\end{figure}

\item[\ccInterval{a}{b}] The closed interval from $a$ to $b$.  This is
an ``unsigned'' interval, where \ccInterval{a}{b} equals
\ccInterval{b}{a}.  (To avoid writing explicit domains, we have defined
\ccInterval{-}{-} to be an operator, so \ccInterval{a}{b} equals the
expression to the right of the $\deq$ even if $a$ and $b$ are not real
numbers.  However, it has the expected meaning only when $a$ and $b$
are real numbers.  This remark applies to all the operators in this
module.)

\item[$|r|$] The absolute value of $r$.

\item[$\{m \ldots n\}$] The set of natural numbers from $m$ through
$n$.  (We assume that the set \vbl{Nat} of natural numbers is imported
with the \vbl{Reals} module.)

\item[$\vbl{Partition}(a,\, b,\, n,\, \delta)$] The set of all possible
partitions of the interval \ccInterval{a}{b} into $n+1$ subintervals
each of length less than $\delta$.  Formally, a partition of an
interval \ccInterval{a}{b} into $n+1$ subintervals is a monotonic
function $p$ from $\{0\ldots n\!+\!1\}$ to \ccInterval{a}{b} such that
$p[0]=a$ and $p[n+1]=b$.  ($[S\rightarrow T]$ denotes the set of all
functions whose domain equals $S$ and whose range is a subset of $T$.)

\item[$\approxint(f,\,p)$] This is a function such that, if $p$ is a
partition of an interval into $n+1$ subintervals, then
$\approxint(f,\,p)[n]$ is the approximation $\sum_{i=0}^{n} f[p[i]]
(p[i+1]-p[i])$ to the area under $f$ on that interval defined by the
partition.  We have defined $\approxint(f,\,p)$ to be a function with
domain \vbl{Nat} to permit a recursive definition.  (In \TLA+, only
functions, not operators, can be defined recursively.  A recursive
function definition such as this can be expressed nonrecursively using
\TLA+'s {\bf choose} operator.)

\item[$\int_{a}^{b}f$] The Riemann integral\footnote{Although this
integral is commonly written $\int_{a}^{b}f(t)\,dt$, 
rigorous mathematicians usually write $\int_{a}^{b}f$.  For example,
$\int_{a}^{b}t^{2}\,dt$ is just an informal way of
denoting $\int_{a}^{b}f$ when $f$ is the function defined by
$f(t)=t^{2}$.} of the function $f$ is defined to be a real number $r$
such that, for every $\epsilon$, there is some $\delta$ such that the
approximation for every partition with subintervals of length less than
$\delta$ lies within $\epsilon$ of $r$.  (The operator {\bf choose}
denotes Hilbert's $\varepsilon$
operator~\cite{leisenring:mathematical-logic}, so 
\mbox{{\bf choose} $r : P(r)$} equals some value $r$ such that $P(r)$
is true, if such an $r$ exists; otherwise, it has an unspecified
value.)

\item[\evolve{c}{a}{G}] The function $f$ such that $f[r]$ equals
$c+\int_{a}^{r}G[f[t],t]\,dt$.  (The expression $[s\in S \mapsto
e(s)]$ denotes the function $g$ with domain $S$ such that $g[s]=e(s)$
for all $s\in S$.)
\end{description}
Finally, the module asserts the result from elementary calculus that
if $G$ is a step function on the interval \ccInterval{a}{b}, then
$\evolve{c}{a}{G}[b]$ is equal to its approximation for the
appropriate partition.  This theorem is needed for the proof of
property \vbl{Req0}.

Proving \vbl{Req0} also requires introducing the exponential function
$\exp$, where $\exp[t]=e^{t}$.  It is defined, and some
theorems about $\exp$ are asserted, in the
\vbl{Exponentials} module of Figure~\ref{fig:Exponentials}.
\begin{figure}[t]
\begin{module}{Exponentials}
{\bf import} \vbl{Integration}
\midbar
\begin{decls}{constant}
  \vbl{exp} \defeq\ \evolve{1}{0}{[r, s \in \Real \mapsto r]}
\end{decls}
\begin{decls}{theorems}
  \vbl{ExpFacts} \defeq\ 
\(\begin{conj}
    \vbl{exp}\in [\Real \mapsto \Real]\\
    \vbl{exp}[0]= 1\\
    \forall\, r \in \Real : (r > 0) \,\implies\,
                (1-r < \vbl{exp}[-r]) \land (\vbl{exp}[-r] < 1) \\
    \forall\, r, s \in \Real : \vbl{exp}[r] * \vbl{exp}[s] = \vbl{exp}[r+s]
\end{conj}\)\\
%
  \vbl{DiffusionSolution} \defeq\ \\
\s{1}\( \forall\, p, q, a, c \in \Real :
      (p \neq 0) \;\implies\;$\\
\s{2}\( \evolve{c}{a}{[r, s \in \Real \mapsto (p*r) + q]}   = \)\\
\s{3}\( [t \in \Real \mapsto
                    c*\vbl{exp}[p*(t-a)] + (q/p) * (\vbl{exp}[p*(t-a)] - 1)]\)
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The exponential function.} \label{fig:Exponentials}
\end{figure}
The theorem named \vbl{DiffusionSolution} asserts that the
solution to the equation $f(t)=c+\int_{a}^{t}(pf(t)+q)\,dt$
is
%\footnote{We are indebted to Lyle Ramshaw for this result.}
 \[ f(t) = ce^{p(t-a)} + \frac{q}{p}(e^{p(t-a)}-1)
 \]
(Such theorems could be proved with the aid of a mathematical package
such as {\em Maple} or {\em Mathematica}.)
The \vbl{HybridSystems} module is now straightforward; it appears in
Figure~\ref{fig:HybridSystems}.  


\begin{figure}[t]
\begin{module}{HybridSystems}
{\bf import} \vbl{Integration}, \vbl{RealTime}
\midbar
\begin{decls}{temporal}
\evolver{x}{c}{G}{\act{A}:{\bf action}}{v} \defeq\ 
%  \( \begin{conj}
%    x = c\\
%    \Box [ \begin{disj}
%              \begin{conj}
%               \vbl{now}' = \vbl{now}\\
%              x' = {\bf if\ } \anact{A}{v} {\bf\ then\ } 0 {\bf\ else\ } x
%              \end{conj}
%\\          \begin{conj}
%              \vbl{now}' \neq \vbl{now}\\
%              x' = \evolve{x}{\vbl{now}}{G}[\vbl{now}'] \s{1}
%                    ]_{\tuple{\vbl{now},\,x,\,v}}
%        \end{conj}
%\end{disj}
%\end{conj}\)
%
  \( \begin{conj}
    x = c\\
    \Box [ x'\,=\,
\begin{array}[t]{@{}l@{}}
{\bf if\ } \vbl{now}' = \vbl{now}\\
\s{1}\begin{array}[t]{@{}l@{}l@{}}
     {\bf then\ } & {\bf if\ } \anact{A}{v} {\bf\ then\ } 0 {\bf\ else\ } x\\
     {\bf else}   & \evolve{x}{\vbl{now}}{G}[\vbl{now}'] \s{2.25}
                    ]_{\tuple{\vbl{now},\,x,\,v}}
            \end{array}
\end{array}
\end{conj}\)
\end{decls}
%
\begin{decls}{state function}
$\chi(P : {\bf predicate})$ \defeq\ 
  {\bf if} $P$ {\bf then} 1 {\bf else} 0
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The \vbl{HybridSystems} module.} \label{fig:HybridSystems}
\end{figure}
%try

\section{The Proof of Property \vbl{Req0}}
%\vspace{.2\baselineskip}
We now sketch the proof of the result mentioned earlier, that
\vbl{Req1} implies \vbl{Req0}.  The proof requires only the theorems
explicitly asserted in the modules defined above, plus the usual
algebraic properties of arithmetic for the real numbers.

The proof is hierarchically structured, using the following notation.
The theorem to be proved is statement \pfstepnumber{0}{1}{?}.  The
proof of statement
  \index{proof style, explanation}%%%
\pfstepnumber{i}{j}{?} is either an ordinary paragraph-style proof or
the sequence of statements \pfstepnumber{i+1}{1}{?},
\pfstepnumber{i+1}{2}{?}, \ldots\ and their proofs.  
Within a proof, \pfstepnumber{k}{l}{?} denotes the most recent
statement with that number.
 % That number is meaningful only if it lies within the proof of
 % statement number \pfstepnumber{k}{l'}{?}, for some $l'>l$.
A statement has the form\\ 
 \mbox{\hspace{\leftmargini}{\sc Assume:} {\em Assumption\/} 
   \ \ {\sc Prove:} {\em Goal}}\\ 
which is abbreviated to {\em Goal\/} if there is no assumption.  The
assertion Q.E.D. in statement number \pfstepnumber{i+1}{k}{?} of the
proof of statement \pfstepnumber{i}{j}{?} denotes the goal of statement
\pfstepnumber{i}{j}{?}.  The statement\\
 \mbox{\hspace{\leftmargini}{\sc Case:} {\em Assumption\/}}\\
is an abbreviation for\\
 \mbox{\hspace{\leftmargini}{\sc Assume:} {\em Assumption\/} 
     \ \ {\sc Prove:} Q.E.D.}\\
Within the proof of statement \pfstepnumber{i}{j}{?}, assumption
\pflevelnumber{i}{?} denotes that statement's assumption.

We begin with the high-level proof, which essentially uses standard
predicate logic to reduce the problem to proving a statement with no
quantification over flexible variables.  The resulting statement,
\pfstepnumber{1}{2}{1.2}, is proved later.

\medskip

\assume{$\vbl{MaxCon} \geq 4*\rho*(1 + (1 / (1 - \exp[(-30)*\delta])))$}
\prove{$\vbl{RT}(v) \land \vbl{Req1}    
      \,\implies\, \vbl{Req0}$}
\begin{proof}
\step{1}{$\EE x : \forall\, r \in \Real : 
           \evolver{x[r]}{0}{G(r)}{\false}{v}$}
\begin{proof}%%%{1}
\pf\ Follows from a standard theorem about the validity of adding
history variables~\cite{abadi:old-fashioned}, which asserts the
validity of $\EE\,x:(x=f)\land\Box\sqact{{}x'=g}{w}$ if $x$ does not
occur in $f$ and $x'$ does not occur in $g$.
\end{proof}%%%{1}
   
\step{2}{\( \begin{conj}
       now = a \\
       \vbl{RT}(v) \\
       \forall\, r \in \Real : \evolver{x[r]}{0}{G(r)}{\false}{v}\\
       \evolver{g}{0}{\vbl{accumRate}}{\false}{v}\\
       \forall\, r \in \Real : \Box(x[r] \leq 4)
     \end{conj} \)\\
   \( \implies\;\Box(g < \vbl{MaxCon}) \)}
%\step{2}{\( \begin{conj}
%       now = a \\
%       \vbl{RT}(v) \\
%       \forall\, r \in \Real : \evolver{x[r]}{0}{G(r)}{\false}{v}\\
%     \end{conj} \)\pagebreak\\
%     \(\begin{conj}
%        \evolver{g}{0}{\vbl{accumRate}}{\false}{v}\\
%       \forall\, r \in \Real : \Box(x[r] \leq 4)
%     \end{conj} \)\\
%   \( \implies\;\Box(g < \vbl{MaxCon}) \)}
  \begin{proof}
    \pf\ Sketched below.
  \end{proof}

\qedstep
\begin{proof}%%%{3}
   \step{3.1}{\( \begin{conj}
          now = a \\
          \vbl{RT}(v) \\
          \forall\, r \in \Real : \evolver{x[r]}{0}{G(r)}{\false}{v}\\
          \forall\, r \in \Real : \Box(x[r] \leq 4)
       \end{conj}\)\\
     \( \implies \;
              (\evolver{g}{0}{\vbl{accumRate}}{\false}{v}
           \implies \Box(g < \vbl{MaxCon}))
     \)}
    \begin{proof}
        \pf\ From \stepref{2} by propositional logic.
    \end{proof}

 \step{3.2}% 
    {\( \begin{conj}
         now = a\\
        \vbl{RT}(v) \\
        \forall\, r \in \Real : \evolver{x[r]}{0}{G(r)}{\false}{v}\\
        \forall\, r \in \Real : \Box(x[r] \leq 4)
       \end{conj}\)\\
        $\implies\, \vbl{Req0}$}
        \begin{proof}
           \pf\ \stepref{3.1}, the definition of 
           \vbl{\vbl{Req0}}, and predicate logic, since $g$ does not
          occur to the left of the $\implies$.
        \end{proof}        

 \step{3.3}{\( \begin{conj}
                now = a\\
               \vbl{RT}(v) \land \vbl{Req1}
              \end{conj} \)\\
            $\implies\; \vbl{Req0}$}
        \begin{proof}
          \pf\ By \stepref{1}, \stepref{3.2}, the definition of 
         \vbl{Req1}, and simple predicate logic,
          since $x$ does not occur free in $\vbl{RT}(v)$ or \vbl{Req0}.
        \end{proof}

  \qedstep
      \begin{proof}
        \pf\ From \stepref{3.3} by simple predicate logic, using the 
        validity of 
            $\exists\, a : now = a$.
     \end{proof}

\end{proof}%%%{3}
\end{proof}

\medskip

Because it involves quantification over flexible variables, this part
of the proof cannot be handled by TLP, the mechanical verification
system for TLA based on the LP theorem
prover~\cite{engberg:mechanical}.\footnote{Mechanical checking of this
kind of reasoning with quantifiers is not hard.  However, such
reasoning is always so simple that we have not felt mechanical
verification to be worth the effort.} The rest of the proof can, in
principle, be verified using TLP\@.  However, TLP does not yet contain
the full definitional capability of \TLA+, so many of the definitions
would have to be expanded by hand.  In addition to being a possible
source of error, this translation might make the formulas so long that
verification would be impractical.  We hope that future versions of
TLP will permit the necessary definitions.


We now prove \pfstepnumber{1}{2}{1.2}.  From the definitions in
modules \vbl{HybridSystems} and \vbl{RealTime}, we can write
 \[ \begin{array}{@{}l@{}}
   \evolver{x[r]}{0}{G(r)}{\false}{v} \defeq
       (x[r] =0) \land
         \Box[\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}} \\[\jot]
   \evolver{g}{0}{\vbl{accumRate}}{\false}{v} \defeq
       (g = 0)\land
         \Box[\act{N}_{g}]_{\tuple{\vbl{now},g, v}} \\[\jot]
   \vbl{RT(v)} \defeq
     (now \in \Real) \land \Box[\act{N}_{\vbl{now}}]_{\tuple{\vbl{now}}} \\
  \end{array}
 \] 
for the appropriate actions $\act{N}_{x}(r)$, $\act{N}_{g}$, and 
$\act{N}_{\vbl{now}}$.  Let
 \[ \begin{array}{@{}l@{\defeq}l@{}}
     \vbl{Init} & (now = a) \,\land\, (g=0) \,\land\, (\vbl{now}\in\Real)
           \,\land\, (\forall\, r\in\Real : x[r]=0)\\
     \act{N} & [\act{N}_{g}]_{\tuple{\vbl{now},g, v}} \,\land\, 
            [\act{N}_{\vbl{now}}]_{\tuple{\vbl{now}}} \,\land\, 
           (\forall \,r\in\Real : 
           [\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}})\\
    J & \forall\, r \in \Real : x[r] \leq 4\\
  \end{array}
 \] 
Using the commutativity of conjunction and the fact that conjunction
distributes over $\Box$, statement \pfstepnumber{1}{2}{1.2} can be
rewritten as\footnote{This notation is rather sloppy, since
$\Box\act{N}$ is not a syntactically correct TLA formula.  We must
write $\Box[\act{N}]_{w}$ for some state function $w$.  However, it is
easy to check that $\act{N}$ equals
$[\act{N}]_{\tuple{\vbl{now},g,X,v}}$, where $X\defeq
[r\in\Real\mapsto x[r]]$.}
 \[ \vbl{Init} \land \Box \act{N} \land \Box J \;\implies\;
     \Box(g < \vbl{MaxCon}) 
 \]
TLA formulas of this form are proved with the aid of an invariant.
First, we define the trivial ``type-correctness'' part of the
invariant:
 \[ T \defeq \begin{conj}
             (\vbl{now}\in\Real)\;\land\;(g\in\Real)\\
             \forall r\in\Real: (x[r]\in\Real) \,\land\, (0\leq x[r])
            \end{conj}
 \]
The nontrivial part $I$ of the invariant is defined as follows,
where we first define \rmod{r} to be the largest number less than or
equal to $r$ that is some multiple of 30 seconds later than $a$.
 \[ \begin{array}{@{}l@{\defeq}l@{}}
      \rmod{ r }
           & {\bf choose}\; s \in \Real :
                 \begin{conj}
                      (s \leq r) \land (r < s + 30) \\
                      | s - a |/30 \in \vbl{Nat}
                 \end{conj}\\
      k & (4 * \rho)/(1 - exp[-30*\delta]) \\
      I &   g \leq (k * exp[-\delta*(\vbl{now} - 
                        \rmod{\vbl{now}})] + \rho * x[\rmod{\vbl{now}}])
    \end{array} \]
The proof of \pfstepnumber{1}{2}{1.2} is a standard invariance proof,
where we prove $\Box I$, using the hypothesis $\Box J$.  The high-level
structure of the proof is: 

\medskip
\begin{proof}
\nostep{1}
\nostep{2}
\begin{noproof}
\step{a.1}{$\vbl{Init}\land\Box\act{N}\implies\Box T$}
\begin{proof}
\pf\ This is a straightforward invariance proof and is omitted.
\end{proof}

\step{a.2}{$\vbl{Init} \land \Box \act{N} \land \Box (J \land T) \;\implies\;
     \Box(g < \vbl{MaxCon})$}
\begin{proof}
\step{2.1}{$\vbl{Init}\implies I$}
\begin{proof}
     \pf\ Trivial, because \vbl{Init} implies $g=0$.
\end{proof}
\pagebreak %%%%%%%%%%%%%%%%%%%%%%%
\step{2.2}{$J \land J' \land T \land I \land \act{N} \implies I'$}
\begin{proof}
     \pf\ Sketched below.
\end{proof}

\step{2.3}{$J \land I \implies (g \leq \vbl{MaxCon})$}
\begin{proof}
     \pf\ Follows by simple algebra from the definition of $k$ and
         assumption~\pflevelnumber{0}{0}.
\end{proof}
\qedstep
\begin{proof}
  \step{2.4.1}{$\Box(J \land T) \land I \land \Box\act{N} \,\implies\, \Box I$}
    \begin{proof}
            \pf\ \stepref{2.2} and the standard TLA invariance rule.
    \end{proof}

  \step{2.4.2}{$\Box(J\land T) \land \vbl{Init} \land \Box\act{N} \,\implies\,
               \Box I$}
    \begin{proof}
            \pf\ \stepref{2.1} and \stepref{2.4.1}.
     \end{proof}

  \step{2.4.3}{$\Box I \implies \Box(g \leq \vbl{MaxCon})$}
       \begin{proof}
            \pf\ \stepref{2.3} and simple temporal logic reasoning.
       \end{proof}

  \qedstep
   \begin{proof}
            \pf\ \stepref{2.4.2} and \stepref{2.4.3}.
    \end{proof}
\end{proof}
\end{proof}
\qedstep
\begin{proof}
\pf\ By \stepref{a.1} and \stepref{a.2}.
\end{proof}
\end{noproof}
\end{proof}
\medskip 

We have reduced our goal to proving \pfstepnumber{3}{2}{3.2}, which is
an assertion of ordinary mathematics, with no temporal operators.
(In the reasoning, primed and unprimed variables are considered to be
separate, unrelated values.)  The proof of \pfstepnumber{3}{2}{3.2} is
sketched below.  The ``algebraic calculations'', which are omitted,
constitute the heart of the proof.  They are straightforward, but writing
them out at the same level of detail as we have been using would be
extremely tedious.  Most mechanical verifiers would probably require
that they be broken into extremely small steps, though they should not
be hard to check with a mathematical package like {\em Mathematica}
or {\em Maple}.\vspace{.5\baselineskip}

%try
\begin{proof}
\nostep{1}
\nostep{2}
\begin{noproof}
\nostep{a.1}
\begin{noproof}
\nostep{2.1}
\step{2.2}{\assume{$J \land J' \land T \land I \land \act{N} $}
           \prove{$I'$}}
\begin{proof}
{\bf let} $\vbl{mid}$ \defeq\ $\rmod{\vbl{now}} + 30$

\step{<4>1}{\case{$\vbl{now}' = \vbl{now}$}}
       \begin{proof}
        \pf\ $[\act{N}_{g}]_{\tuple{\vbl{now},g, v}} 
              \land (\vbl{now}'=\vbl{now})$ implies $g'=g$,
       and $(\vbl{now}'=\vbl{now})\,\land\,
           \forall\,r:\sqact{N_{x}(r)}{\tuple{\vbl{now},\,x[r],\,v}}$
       implies $x[\rmod{\vbl{now}}]'=x[\rmod{\vbl{now}}]$,
        so $I'$ equals $I$.
        \end{proof}

\step{<4>2}{\case{$(\vbl{now}'\neq\vbl{now}) \land (v'=v)$}}
\begin{proof}%%%{<4>2}
  \step{<5>1}{$\vbl{now}' > \vbl{now}$}
       \begin{proof}
          \pf\ By $[\act{N}_{\vbl{now}}]_{\tuple{\vbl{now}}}$ (assumption
                  \levelref{2.2}).
       \end{proof}

  \step{<5>2}{\case{$\vbl{Gas} \land \lnot\vbl{Flame}$}}
       \begin{proof}%%%{<5>2}
      {\bf let} $D(s,t) 
             \defeq s*\exp[-\delta*t] + (\rho/\delta)(1 - \exp[-\delta*t])$

    \step{<6>1}{$g' = D(g, \vbl{now}'-\vbl{now})$}
         \begin{proof}
          \pf\ By $[\act{N}_{g}]_{\tuple{\vbl{now},g, v}}$ and 
          Theorem \vbl{DiffusionSolution} of module \vbl{Exponentials}.
       \end{proof}

   \step{<6>2}{\case{$\rmod{\vbl{now}'} = \rmod{\vbl{now}}$}}
      \begin{proof}
        \step{<7>1}{$x'[\rmod{\vbl{now}'}] = x[\rmod{\vbl{now}}] 
                       + (\vbl{now}' - \vbl{now})$}
            \begin{proof}
              \pf\ Case assumptions \levelref{<5>2} and \levelref{<6>2}, 
               $[\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}}$  
                 with $r=\rmod{\vbl{now}}$, and 
               Theorem \vbl{IntegralOfStepFcn} of module
               \vbl{Integration}, since 
           $\vbl{now}\in\ccInterval{\rmod{\vbl{now}}}{\rmod{\vbl{now}}+30}$.
             \end{proof}

        \qedstep
          \begin{proof}
            \pf\ {\relax Algebraic calculation}, using 
              \stepref{<6>1}, 
              \stepref{<7>1}, case assumption \levelref{<5>2},
              and 
          Theorem \vbl{ExpFacts} of module \vbl{Exponentials}.
         \end{proof}
      \end{proof}

\vspace{.2\baselineskip}
   \step{<6>3}{\case{$\rmod{\vbl{now}'} \neq  \rmod{\vbl{now}}$}}
     \begin{proof}%%%{<6>3}
      \step{<7>1}{$g' = D(D(g, \vbl{mid}-\vbl{now}), \vbl{now}'-\vbl{mid})$}
         \begin{proof}
          \pf\ By \stepref{<6>1}, since an algebraic calculation using 
             Theorem \vbl{ExpFacts} shows that
           $D(D(s,t_{1}), t_{2})=D(s,t_{1}+t_{2})$ for any
           $s,t_{1},t_{2}\in\Real$.
          \end{proof}

\vspace{.1\baselineskip}
      \step{<7>2}{$x'[\rmod{\vbl{now}}] = x[\rmod{\vbl{now}}] + \vbl{mid} -
                    \vbl{now}$}
          \begin{proof}
             \pf\ Case assumption \levelref{<4>2},  
             $[\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}}$ with
            $r=\rmod{\vbl{now}}$, and Theorem \vbl{IntegralOfStepFcn}.
          \end{proof}
\vspace{.1\baselineskip}
      \step{<7>3}{$D(g, \vbl{mid}-\vbl{now}) \leq k$}
        \begin{proof}
          \pf\ {\relax Algebraic calculation} using \stepref{<7>2},
          $J' \land I$ (Assumption \levelref{2.2}), 
          and Theorem \vbl{ExpFacts}.
        \end{proof}

\vspace{.1\baselineskip}
      \step{<7>4}{$x'[\vbl{mid}] = \vbl{now}' - \vbl{mid}$}
        \begin{proof}
         \step{<8>1}{$x'[\vbl{mid}]=\min(\vbl{now}'-\vbl{mid},\,30)$}
         \begin{proof}
          \pf\ Case assumption \levelref{<6>2},  
             $[\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}}$ with
            $r=\vbl{mid}$, and Theorem \vbl{IntegralOfStepFcn}.
          \end{proof}
         \qedstep
          \begin{proof}
            \pf\ \stepref{<8>1} and $J'$ (Assumption \levelref{2.2}).
           \end{proof}
        \end{proof}

\vspace{.1\baselineskip}
      \step{<7>5}{$\rmod{\vbl{now}'} = \vbl{mid}$}
        \begin{proof}%%%{<7>5}
         \step{<8>1}{$(\vbl{now}' - \vbl{mid}) \leq 4$}
           \begin{proof}
              \pf\ \stepref{<7>4} and $J'$ (assumption \levelref{2.2}).
           \end{proof}

          \qedstep
            \begin{proof}
            \pf\ \stepref{<5>1}, \stepref{<8>1}, 
             and the definition of \vbl{mid}.
            \end{proof}
        \end{proof}%%%{<7>5}
\vspace{.1\baselineskip}
      \qedstep
          \begin{proof}
          \pf\ {\relax Algebraic calculation} using \stepref{<7>1}, 
              \stepref{<7>3}, \stepref{<7>4}, \stepref{<7>5}, $I$ 
              (assumption \levelref{2.2}),
             and Theorem \vbl{ExpFacts}.
          \end{proof}
      \end{proof}%%%{<6>3}
\vspace{.2\baselineskip}
      \qedstep
         \begin{proof}
             \pf\ \stepref{<6>2} and \stepref{<6>3}.
          \end{proof}
   \end{proof}%%%{<5>2}

\vspace{.3\baselineskip}
   \step{<5>3}{\case{$\lnot(\vbl{Gas} \land \lnot\vbl{Flame})$}}
     \begin{proof}%%%{<5>3}
      \step{<6>1}{$g' = g*\exp[-\delta*(\vbl{now}'-\vbl{now})]$}
\vspace{.1\baselineskip}
       \begin{proof}
          \pf\ By $[\act{N}_{g}]_{\tuple{\vbl{now},g, v}}$
             and Theorem \vbl{DiffusionSolution}.
       \end{proof}
\vspace{.2\baselineskip}
      \step{<6>2}{\case{$\rmod{\vbl{now}'} = \rmod{\vbl{now}}$}}
       \begin{proof}%%%{<6>2}
        \step{<7>1}{$x'[\rmod{\vbl{now}}] = x[\rmod{\vbl{now}}]$}
           \begin{proof}
              \pf\ By $[\act{N}_{x}(r)]_{\tuple{\vbl{now},x[r], v}}$
               with $r=\rmod{\vbl{now}}$, case assumption \levelref{<6>2},
               and Theorem \vbl{IntegralOfStepFcn}.
           \end{proof}

\vspace{.1\baselineskip}
        \qedstep
           \begin{proof}
               \pf\ {\relax Algebraic calculation} using 
             \stepref{<5>1},
               \stepref{<6>1}, 
               \stepref{<7>1}, $I$,
              and Theorem \vbl{ExpFacts}.
           \end{proof}
       \end{proof}%%%{<6>2}

\vspace{.2\baselineskip}
      \step{<6>3}{\case{$\rmod{\vbl{now}'} \neq  \rmod{\vbl{now}}$}}
        \begin{proof}%%%{<6>3}
        \step{<7>1}{$\vbl{mid} \leq \rmod{\vbl{now}'}$}
          \begin{proof}
              \pf\ \stepref{<5>1} and case assumption \levelref{<6>3}. 
          \end{proof}
\vspace{.1\baselineskip}
        \step{<7>2}{$g' = g * \exp[-\delta*(\vbl{mid}-\vbl{now})] 
                       * \exp[-\delta*(\vbl{now}'-\vbl{mid})]$}
          \begin{proof}
              \pf\ \stepref{<6>1} 
              and Theorem \vbl{ExpFacts}.
          \end{proof}
\pagebreak %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
        \step{<7>3}{$g * \exp[-\delta*(\vbl{mid}-\vbl{now})] \leq k$}
          \begin{proof}
              \pf\ {\relax Algebraic calculation}, using $I$, $J$ (which implies
              $x[\rmod{\vbl{now}}] \leq 4$), 
              and Theorem \vbl{ExpFacts}  (since $\vbl{mid}>\vbl{now}$).
          \end{proof}
        \qedstep
          \begin{proof}
              \pf\ {\relax Algebraic calculation}, using 
              \stepref{<7>1}, \stepref{<7>2}, \stepref{<7>3}, $T$,
              and Theorem \vbl{ExpFacts}.
          \end{proof}
         \end{proof}%%%{<6>3}

       \qedstep
         \begin{proof}
             \pf\ \stepref{<6>2} and \stepref{<6>3}.
           \end{proof}
      \end{proof}%%%{<5>3}
  \qedstep
    \begin{proof}
          \pf\ \stepref{<5>2} and \stepref{<5>3}.
   \end{proof}

  \end{proof}%%%{<4>2}
  \qedstep
   \begin{proof}
      \pf\ \stepref{<4>1}, \stepref{<4>2}, and assumption 
           \levelref{2.2}, since 
           $[\act{N}_{\vbl{now}}]_{\vbl{now}}
                  \land (\vbl{now}' \neq  \vbl{now})$
      implies $v'=v$, by definition of 
      $\act{N}_{\vbl{now}}$.
   \end{proof}
\end{proof}
\end{noproof}
\end{noproof}
\end{proof}

%try
\section{An Implementation}

We now specify an implementation of the gas burner inspired by RRH's
``control model''.  RRH also specify an ``architecture''.  However, a
comparison of Figures 2 and 3 of \cite{ravn:specifying} reveals that
this architecture is just the same implementation expressed in a
CSP-like language.  A program in a toy language is no closer to a real
program than the corresponding \TLA+ or Duration Calculus formula is;
it just has a syntax that can fool some people into thinking it is
closer.  So, we see no reason to introduce such a toy programming
language.

The control model is described by the state-transition diagram of
Figure~\ref{fig:control-model}.  
\begin{figure}[b]
\setlength{\unitlength}{1mm}
\begin{center}
\begin{picture}(80,40)

\put(40,39){\vector(0,-1){6}}
%\put(36, 29){\mbox{\sf Idle}}
\put(40, 30){\makebox(0,0){\sf Idle}}
\put(40, 30){\oval(20,6)[t]}
\put(40, 30){\oval(20,6)[b]}
\put(50, 30){\vector(2,-1){20}}
\put(61, 25){\mbox{\small\vbl{HeatOn}}}

\put(60,  4){\makebox(0,0){\sf Ignite1}}
%\put(54,  3){\mbox{\sf Ignite1}}
\put(60,  4){\oval(20,6)[t]}
\put(60,  4){\oval(20,6)[b]}
\put(50,  4){\vector(-1,0){20}}
\put(37,  6){\mbox{\small\vbl{Out1a}}}

\put(20,  4){\makebox(0,0){\sf Ignite2}}
%\put(14,  3){\mbox{\sf Ignite2}}
\put(20,  4){\oval(20,6)[t]}
\put(20,  4){\oval(20,6)[b]}
\put(17,  7){\vector(-1,1){7}}
\put(20,  7){\vector(1,1){20}}
\put(33, 17){\mbox{\small\vbl{Out1b}}}
\put( 4,  9){\mbox{\small\vbl{FlOn}}}

%\put( 6, 16){\mbox{\sf Burn}}
\put(10, 17){\makebox(0,0){\sf Burn}}
\put(10, 17){\oval(20,6)[t]}
\put(10, 17){\oval(20,6)[b]}
\put(10, 20){\vector(2,1){20}}
\put( 6, 28){\mbox{\small\vbl{HeatOff},}}
\put( 6, 24){\mbox{\small\vbl{FlOff}}}

\put(66, 16){\mbox{\sf Purge}}
\put(70, 17){\oval(20,6)[t]}
\put(70, 17){\oval(20,6)[b]}
\put(70, 14){\vector(-1,-1){7}}
\put(68,  9){\mbox{\small\vbl{Out30}}}

\end{picture}
\end{center}
\caption{The control model, adapted from Figures 2 and 3 of
\protect\cite{ravn:specifying}.}
\label{fig:control-model}
\end{figure}
In the RRH specification, the states
of the control model are abstract states that are only loosely coupled
with states of the physical variables.  For example, the specification
of RRH asserts that the ignition and gas are turned on after the {\sf
Ignite1} state is reached.  The easiest way to duplicate the RRH
specification would be to translate the state-machine into a simple
\TLA+ formula, and then translate the ``phase requirements'' of RRH
into \TLA+ using the operators from the \vbl{HybridSystems} module.
However, we have already presented one level of specification and
verification using the \vbl{HybridSystems} module's operators, so this
would be more of the same.  Moreover, this is not the type of
specification one would naturally write with TLA\@.  In TLA, it is
more natural to write lower level specifications purely in terms of
states and transitions.  One would draw a state-transition diagram for
the \vbl{gas} and \vbl{ignition} variables---the transitions being
enabled and disabled by changes to the control state---and write a
\TLA+ specification of the resulting system.  This representation
would be the first step in refining the control model to a realistic
representation of an actual implementation.  However, developing this
specification would take more space than seems appropriate.  Instead,
we present a simplified version in which the physical variables
\vbl{gas} and \vbl{ignition} that are under the implementer's control
change simultaneously with the control state.


The module \vbl{BurnerControl} of Figure~\ref{fig:BurnerControl}
describes the time-independent behavior of the burner.  It is a
standard TLA specification; the next-state relation \act{N} is
specified as the disjunction of individual actions corresponding to
the transitions in Figure~\ref{fig:control-model}.  Note that this
module has a new parameter---the ``internal'' variable \vbl{state}.
(Internal variables are ones that are existentially quantified.)  The
only surprising part of the specification is that the \vbl{Out1b}
action can occur even if the flame is on.  Timing requirements
will prevent this action from occurring if the flame ignites
quickly enough.

\begin{figure}[t]
\begin{module}{BurnerControl}
{\bf import} \vbl{BurnerParameters}
\midbar
\begin{decls}{parameter}
\vbl{state} : {\bf variable}
\end{decls}
\midbar
\begin{decls}{predicate}
\vbl{w} \defeq\ \tuple{\vbl{gas}, \vbl{ignition}, \vbl{state}}\\
\vbl{Init} \defeq\ $w = 
  \tuple{\str{off},\,\str{off},\,\str{Idle}}$
\end{decls}
\begin{decls}{actions}
\vbl{HeatOn} 
\defeq\ 
 \( \begin{conj}
      \vbl{HeatReq} \;\land\; (\vbl{state}=\str{Idle})\\
      (\vbl{state}' = \str{Purge}) \;\land\;
      {\bf unchanged\ } \tuple{\vbl{gas},\, \vbl{ignition}}
    \end{conj}
 \)\\[.2em]
%
\vbl{Out30} 
\defeq\ 
 \( \begin{conj}
      (\vbl{state}=\str{Purge})\;\land\;
      (\vbl{state}' = \str{Ignite1})\\
      {\bf unchanged\ } \tuple{\vbl{gas},\, \vbl{ignition}}
    \end{conj}
 \)\\[.2em]
%
\vbl{Out1a} 
\defeq\ 
 \( \begin{conj}
      (\vbl{state}=\str{Ignite1})\;\land\;
      (\vbl{state}' = \str{Ignite2})\\
      (\vbl{ignition}' = \str{on}) \;\land\; (\vbl{gas}' = \str{on}) 
    \end{conj}
 \)\\[.2em]
%
\vbl{Out1b} 
\defeq\ 
 \( \begin{conj}
      (\vbl{state}=\str{Ignite2})\;\land\;
      (\vbl{state}' = \str{Idle})\\
      (\vbl{ignition}' = \str{off})\;\land\; (\vbl{gas}' = \str{off})
    \end{conj}
 \)\\[.2em]
%
\vbl{FlOn} 
\defeq\ 
 \( \begin{conj}
      (\vbl{state}=\str{Ignite2})\;\land\;\vbl{Flame}\;\land\;
      (\vbl{state}' = \str{Burn})\\
      (\vbl{ignition}' = \str{off})\;\land\;
      {\bf unchanged\ } \vbl{gas}
    \end{conj}
 \)\\[.2em]
%
\vbl{GoIdle} 
\defeq\ 
 \( \begin{conj}
(\vbl{state}=\str{Burn})\;\land\;(\lnot\vbl{Flame}\lor\lnot\vbl{HeatReq})
      \;\land\;
      (\vbl{state}' = \str{Idle})\\
      (\vbl{gas}' = \str{off})\;\land\;
      {\bf unchanged\ } \vbl{ignition}
    \end{conj}
 \)\\[.2em]
%
%
\act{N} \defeq\ 
 $\vbl{HeatOn} \;\lor\; 
   \vbl{Out30} \;\lor\;
  \vbl{Out1a} \;\lor\;
  \vbl{Out1b} \;\lor\;
 \vbl{FlOn} \;\lor\;
 \vbl{GoIdle}$
\end{decls}
\begin{decls}{temporal}
\vbl{Control} \defeq\ $\vbl{Init}\land
  \Box[\act{N}]_{w}$
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The Control Actions.}
\label{fig:BurnerControl}
\end{figure}

Next, module \vbl{BurnerPhaseReqs} of
Figure~\ref{fig:BurnerControlModel} specifies the real-time
requirements on the burner.  It contains minimum and maximum delays on
each of the transitions in Figure~\ref{fig:control-model}, which are
expressed with the operators from the \vbl{RealTime} module.  The
constraints, and the new parameters $\epsilon_{1}$ and $\epsilon_{2}$,
are taken directly from the RRH specification.  RRH's condition
\vbl{Ignite2Req} is split into two parts.  The first,
\vbl{Ignite2aReq}, asserts that an \vbl{Out1b} action cannot occur
until it has been enabled ($\vbl{state}=\str{Ignite2}$) for at least
$1$ second, and it must occur if it has been enabled for
$1+\epsilon_{1}$ seconds.  (The formula \vbl{Control} asserts that the
\vbl{Out1b} action remains enabled until an \vbl{Out1b} or \vbl{FlOn}
step occurs.)  The second part, \vbl{Ignite2bReq}, asserts that a
\vbl{FlOn} action must be continuously enabled
($\vbl{state}=\str{Ignite2}$ and  flame on) for at least
$\epsilon_{2}$ seconds before it can occur, and it must occur if it
has been continuously enabled for $\epsilon_{1}$ seconds.

\begin{figure}[t]
\begin{module}{BurnerPhaseReqs}
{\bf import} \vbl{BurnerControl}, \vbl{RealTime}
\midbar
\begin{decls}{parameters}
$\epsilon_{1}$, $\epsilon_{2}$ : \Real\ {\bf constants}
\end{decls}
\midbar
% \begin{decls}{assumption}
% \vbl{EpsilonAssumption} \defeq\ 
%     $(0<\epsilon_{1})\land(\epsilon_{1}<\epsilon_{2})$
% \end{decls}
%
\begin{decls}{temporal}
\vbl{IdleReq} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{HeatOn},\,\epsilon_{2},\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{HeatOn},\, w)\\
              \vbl{VTimer}(y,\,\vbl{HeatOn},\,\epsilon_{1},\,
                   w)\;\land\;
              \vbl{MaxTimer}(y) 
             \end{conj}
\)
\\[.2em]
%
\vbl{PurgeReq} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{Out30},\,30,\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{Out30},\, w)\\
              \vbl{VTimer}(y,\,\vbl{Out30},\,30+\epsilon_{1},\,
                   w)\;\land\;
              \vbl{MaxTimer}(y)
             \end{conj}
\)
\\[.2em]
%
\vbl{Ignite1Req} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{Out1a},\,1,\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{Out1a},\,w)\\
              \vbl{VTimer}(y,\,\vbl{Out1a},\,1+\epsilon_{1},\,
                   w)\;\land\;
              \vbl{MaxTimer}(y)
             \end{conj}
\)
\\[.2em]
%
\vbl{Ignite2aReq} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{Out1b},\,1,\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{Out1b},\,w)\\
              \vbl{VTimer}(y,\,\vbl{Out1b},\,1+\epsilon_{1},\,
                   w)\;\land\;
              \vbl{MaxTimer}(y) 
             \end{conj}
\)
\\[.2em]
%
\vbl{Ignite2bReq} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{FlOn},\,\epsilon_{2},\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{FlOn},\, w)\\
              \vbl{VTimer}(y,\,\vbl{FlOn},\,\epsilon_{1},\,w)\;\land\;
              \vbl{MaxTimer}(y) 
             \end{conj}
\)
\\[.2em]
%
\vbl{BurnReq} \defeq\ 
\(   
  \EE x,\,y : \begin{conj}
              \vbl{VTimer}(x,\,\vbl{GoIdle},\,\epsilon_{2},\,
                   w) \;\land\;
            \vbl{MinTimer}(x,\,\vbl{GoIdle},\, w)\\
              \vbl{VTimer}(y,\,\vbl{GoIdle},\,\epsilon_{1},\,
                   w)\;\land\;
              \vbl{MaxTimer}(y) 
             \end{conj}
\)
\\[.2em]
%
\vbl{PhaseReqs} \defeq\
\( \begin{array}[t]{@{}l@{}}
\vbl{IdleReq} \;\land\;
   \vbl{PurgeReq} \;\land\;
   \vbl{Ignite1Req} \;\land\;\\
   \s{1}\vbl{Ignite2aReq} \;\land\;
   \vbl{Ignite2bReq} \;\land\;
   \vbl{BurnReq} 
 \end{array}
\)
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The control model's timing requirements.}
\label{fig:BurnerControlModel}
\end{figure}

Next, module \vbl{BurnerEnvironment} in
Figure~\ref{fig:BurnerEnvironment} specifies the environment.  The
burner controls the \vbl{gas} and \vbl{ignition} variables; the
environment controls the \vbl{flame} and \vbl{heatReq} variables.  The
specification of the initial condition and next-state relation are
standard TLA\@.  Condition $\vbl{ASM}_{1}$ of RRH, that ``no gas
results in no flame within 0.1 seconds,'' is expressed as usual with a
timer.  RRH's condition $\vbl{ASM}_{2}$, that ``gas does not ignite
when the ignition transformer is not operating,'' is a time-independent
property that is encoded in the next-state relation \act{N}.

\begin{figure}[tp]
\begin{module}{BurnerEnvironment}
{\bf import} \vbl{BurnerParameters}
\midbar
\begin{decls}{predicate}
\vbl{Init} \defeq\ $\tuple{\vbl{flame}, \vbl{heatReq}}
        = \tuple{\str{off},\str{off}}$
\end{decls}
\begin{decls}{actions}
\vbl{ChangeHeatReq} \defeq\
 \( \begin{conj}
      \vbl{heatReq}' = {\bf if\ } HeatReq {\bf \ then\ } \str{off}
                          {\bf \ else\ } \str{on}\\
      {\bf unchanged\ }  \vbl{flame}
    \end{conj}
 \)\\[.2em]
%
\vbl{FlameOn} \defeq\
 \( \begin{conj}
      \lnot\vbl{Flame} \;\land\; \vbl{Gas} \;\land\; \vbl{Ignition}\;\land\;
      (\vbl{flame}' = \str{on})\\
      {\bf unchanged\ } \vbl{heatReq}
    \end{conj}
 \)\\[.2em]
%
\vbl{FlameOff} \defeq\
 \( \vbl{Flame}\;\land\;
      (\vbl{flame}' = \str{off})\;\land\;
      {\bf unchanged\ } \vbl{heatReq}
 \)\\[.2em]
\act{N} \defeq\ 
\( \vbl{ChangeHeatReq} \;\lor\;
   \vbl{FlameOn} \;\lor\;
   \vbl{FlameOff} \)
\end{decls}
\begin{decls}{temporal}
\vbl{Spec} \defeq\ \( 
\begin{conj}
\vbl{Init} \land 
           \Box[\act{N}]_{\tuple{\vbl{flame},\, \vbl{heatReq}}}\\[.2em]
%
  \EE x : \begin{conj}
         \vbl{VTimer}(x,\,\vbl{FlameOff}\land\lnot\vbl{Gas},\,1/10,\,
                   \tuple{\vbl{flame},\, \vbl{heatReq}})\\
              \vbl{MaxTimer}(x) 
             \end{conj}
\end{conj}\)
%
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{Timing assumptions on the environment.}
\label{fig:BurnerEnvironment}
\end{figure}

Finally, the pieces are put together in the \vbl{ControlModel} module
of Figure~\ref{fig:ControlModel}.  
\begin{figure}[tp]
\begin{module}{ControlModel}
{\bf import} \vbl{BurnerParameters}, \vbl{RealTime}
\midbar
\begin{decls}{parameters}
$\epsilon_{1}$, $\epsilon_{2}$ : \Real\ {\bf constants}
\end{decls}
\midbar
\begin{decls}{assumption}
 \vbl{EpsilonAssumption} \defeq\ 
     $(0<\epsilon_{1})\;\land\;(\epsilon_{2}<\epsilon_{1})
     \;\land\;(\epsilon_{1}\leq 2/3)$
 \end{decls}
\midbar
{\bf include} \vbl{BurnerPhaseReqs} {\bf as}
 $\vbl{Burner}(\vbl{state})$\\[.2em]
{\bf include} \vbl{BurnerEnvironment} {\bf as} \vbl{Env}
\vspace{.2em}
\begin{decls}{temporal}
\vbl{Spec} \defeq
\( \begin{conj}
      \EE \vbl{s} : 
                  \vbl{Burner}(\vbl{s}).\vbl{Control} \;\land\;
                  \vbl{Burner}(\vbl{s}).\vbl{PhaseReqs}\;\land\;
                  \vbl{RT}(\vbl{s})\\
       \vbl{Env.Spec}\\
      \vbl{RT}(v)
   \end{conj}
\)
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{The complete control model specification.}
\label{fig:ControlModel}
\end{figure}
The assumptions about
$\epsilon_{1}$ and $\epsilon_{2}$ are the same as RRH's, except that
our simpler specification is correct with a weaker upper bound on
$\epsilon_{1}$.  The statement
 \[ \mbox{{\bf include} \vbl{BurnerEnvironment} {\bf as} \vbl{Env}}
 \]
is equivalent to inserting all the definitions from the
\vbl{BurnerEnvironment} module, with the names of the defined symbols
preceded by ``\vbl{Env.}''.\footnote{In contrast to an imported
module, whose parameters become parameters of the importing module,
parameters of an included module are instantiated.  In this case,
there are no explicit instantiations, so the included module's
parameters are by default instantiated with parameters of the same
name.} Similarly, the statement
 \[ \mbox{{\bf include} \vbl{BurnerPhaseReqs} {\bf as}
     $\vbl{Burner}(\vbl{state})$}
 \]
is equivalent to including all the definitions of the
\vbl{BurnerPhaseReqs} environment, with defined symbols renamed by
prefacing them with
``$\vbl{Burner}(\vbl{state}).$''.  This makes
\vbl{state} a free parameter of all those defined symbols, which must
be instantiated when the symbol is used.  (Note how it is
instantiated with the bound variable $s$ in the definition of
\vbl{Spec}.) The complete specification is the conjunction of the
burner's complete specification and the environment specification,
\rule{0pt}{1.5\baselineskip}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
together with the formula $\vbl{RT}(v)$ that describes how \vbl{now}
changes and asserts that $v$ does not change when \vbl{now} does.
The burner's specification is obtained by hiding the internal state
variable in the conjunction of its time-independent specification, its
timing requirements, and the \vbl{RT}-formula asserting that the
internal state does not change when \vbl{now} does.\footnote{Note that,
since $s$ does not appear in $\vbl{RT}(v)$, the latter formula can be
moved inside the quantifier; and $\vbl{RT}(v)\land\vbl{RT}(s)$ is
equivalent to $\vbl{RT}(\tuple{v,s})$.}




The next step is to prove that the Control Model satisfies
requirements \vbl{Req1}, \vbl{Req2}, and \vbl{Req3}.  This means
proving that formula \vbl{Spec} of module \vbl{ControlModel} implies
$\vbl{Req1}\land\vbl{Req2}\land\vbl{Req3}$.  We very briefly sketch
the proof that \vbl{Spec} implies \vbl{Req1}; the other proofs are
similar.

We first reduce the problem to proving an assertion
without quantification over flexible variables.  Let
$\vbl{Burner}(s).\vbl{VControl}$ be the formula that is the same as
$\vbl{Burner}(s).\vbl{Control}$ except with the quantifiers $\EE\,x,y$
removed and each $x$ and $y$ replaced by a unique variable.  For
example, let \vbl{xIgnite1} and \vbl{yIgnite1} be substituted for
$x$ and $y$ in \vbl{Ignite1Req}.  Similarly, let \vbl{Env.VSpec} be
the formula obtained by removing the quantifier from \vbl{Env.Spec}
and substituting \vbl{xEnv} for $x$.  Simple predicate logic 
shows that, to prove $\vbl{Spec}\implies\vbl{Req1}$, it suffices to
assume $r\in\Real$ and prove $\Pi\implies \Box(z\leq 4)$, where
 \[  \Pi\defeq
      \begin{conj}
        \evolver{z}{0}{G(r)}{\false}{v}\\
        \vbl{Burner}(s).\vbl{Control}\,\land\,\vbl{Burner}(s).\vbl{VPhaseReqs}\\
        \vbl{Env.VSpec}\\
        \vbl{RT}(s)\,\land\,\vbl{RT}(v)
      \end{conj}
 \]
and $G$ is defined by the {\bf let} in the definition of \vbl{Req1}.

The proof of $\Pi\implies\Box(z\leq4)$ has the same form as the proof
of step \pfstepnumber{1}{2}{1.2} in the proof that
$\vbl{RT}(v)\land\vbl{Req1}$ implies \vbl{Req0}.  We first prove
$\Pi\implies\Box T$ for a simple invariant $T$, which expresses the
expected relations among the values of the variables.  For example,
one conjunct of $T$ is
 \[ (s=\str{Ignite1}) \implies \begin{conj}
                               \vbl{Gas}\land\vbl{Ignition}\\
                               (\vbl{yIgnite1} \in \Real) \land
                                (\vbl{now}\leq \vbl{yIgnite1}) 
                             \end{conj}
 \]
We then prove $\Pi\land\Box T\implies\Box I$ for the following
invariant $I$.
 \[ \begin{conj}
      z\leq 4\\
      (z > 0) \implies (z \leq \vbl{now} - r)\\
      (\vbl{now} \in \ccInterval{r}{r+30}) \implies
        \begin{disj}
             (s = \str{Idle})\\
             (s = \str{Purge}) \,\land\, 
            ((z > 0) \implies (\vbl{xPurge} \geq  r+30))\\
	   (s = \str{Ignite1}) \,\land\, 
		   (z + (\vbl{yIgnite1} - \vbl{now}) \leq 1 + \epsilon_{1})\\
           (s = \str{Ignite2})
                  \,\land\, (z + \vbl{yIgnite2a} - \vbl{now} 
                               \leq 2 + 2\epsilon_{1}) \\
           
            \begin{conj}
               (s = \str{Burn}) \,\land\, \vbl{Gas}\\
               \begin{disj}
                \vbl{Flame} \,\land\, (z \leq 2 + 2\epsilon_{1})\\
                \lnot\vbl{Flame} \,\land\, (z + \vbl{yBurn} - \vbl{now}
                      \leq 2 + 3\epsilon_{1})
               \end{disj}
            \end{conj}         
         \end{disj}
    \end{conj}
 \] 
The hard part of proving $\Pi\land\Box T\implies\Box I$ is the analog
of step \pfstepnumber{3}{2}{3.2} in the proof that
$\vbl{RT}(v)\land\vbl{Req1}$ implies \vbl{Req0}.  As usual, this step
involves ordinary mathematics, with no temporal operators.


%try
% \clearpage

\addcontentsline{toc}{section}{References}
\bibliographystyle{plain}
%\bibliography{mybib}
%\clearpage
\begin{thebibliography}{1}

\bibitem{abadi:old-fashioned}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock An old-fashioned recipe for real time.
\newblock Research Report~91, Digital Equipment Corporation Systems Research
  Center, 1992.
\newblock An earlier version, without proofs, appeared in \cite[pages
  1--27]{debakker:real-time}.

\bibitem{chandy:parallel}
K.~Mani Chandy and Jayadev Misra.
\newblock {\em Parallel Program Design}.
\newblock Addison-Wesley, Reading, Massachusetts, 1988.

\bibitem{debakker:real-time}
J.~W. de~Bakker, C.~Huizing, W.~P. de~Roever, and G.~Rozenberg, editors.
\newblock {\em Real-Time: Theory in Practice}, volume 600 of {\em Lecture Notes
  in Computer Science}.
\newblock Springer-Verlag, Berlin, 1992.
\newblock Proceedings of a REX Real-Time Workshop, held in The Netherlands in
  June, 1991.

\bibitem{engberg:mechanical}
Urban Engberg, Peter Gr\o{}nning, and Leslie Lamport.
\newblock Mechanical verification\\ of concurrent systems with tla.
\newblock In {\em Logics of Programs}, Lecture Notes in Computer Science,
  Berlin, Heidelberg, New York, June 1992. Springer-Verlag.

\bibitem{lamport:newtla}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock Research Report~79, Digital Equipment Corporation, Systems Research
  Center, December 1991.

\bibitem{leisenring:mathematical-logic}
A.~C. Leisenring.
\newblock {\em Mathematical Logic and Hilbert's $\varepsilon$-Symbol}.
\newblock Gordon and Breach, New York, 1969.

\bibitem{manna:temporal}
Zohar Manna and Amir Pnueli.
\newblock {\em The Temporal Logic of Concurrent Systems}.
\newblock Springer-Verlag, New York, 1991.

\bibitem{ravn:specifying}
Anders~P. Ravn, Hans Rischel, and Kirsten~M. Hansen.
\newblock Specifying and verifying requirements of real-time systems.
\newblock {\em IEEE Transactions on Software Engineering}, January 1993.
\newblock to appear.

\end{thebibliography}


\end{document}
