\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|
 Copyright (C) 1995 by William D. Young.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 William D. Young PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL William D. Young BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

;; >> Might try to relax the assumption that there is only
;;    one train and it always is going in the same direction. 

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{verbatim};; SOME SUBSIDIARY LEMMAS

\end{verbatim}\begin{tabbing}{\sc Theorem}:  not-lessp-sub1 \\ \index{not-lessp-sub1}
({\it{x\/}} $\not<$ {\it{y\/}}) $\rightarrow$ (({\it{x\/}} $<$ ({\it{y\/}} $-\;1$)) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
\=\+(({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}}))) \\ 
$\wedge$$\;\;\;\;$((($1\;+$ {\it{x\/}}) $+$ {\it{y\/}}) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-add1-sub1 \\ \index{difference-add1-sub1}
({\it{x\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $-$ ($1\;+$ {\it{y\/}})) $=$ (({\it{x\/}} $-$ {\it{y\/}}) $-\;1$))
\end{tabbing}

\begin{verbatim};; THE SYSTEM
;; Our simple control system consists of three distinct components.
;; The train is an part of the environment; it produces in a way that 
;; we cannot control but subject to certain constraints that we specify.
;; The gate is our controlled system and responds to a series of commands
;; generated by the controller.  The controller is a device that inputs
;; a series of sensor readings from the environment, giving the position of 
;; the train.  It generates a series of actuator commands for the gate.
;; 
;; Our task is to model the system comprised of these three components.

;; GATE SIMULATION
;; The gate is the controlled system, so we consider that it responds 
;; reliably to a series of commands that are generated by the control 
;; algorithm.  These commands come in the form of a sequence of atoms
;; 'open and 'close.   The simulation of the gate tells us its state
;; at each moment of time.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  choose-time-intro \\ \index{choose-time-intro}
\=\+({\it{min\/}} $\leq$ {\it{max\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{choose-time}}\,({\it{min\/}}, {\it{max\/}}, {\it{oracle\/}})\index{choose-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{choose-time}}\,({\it{min\/}}, {\it{max\/}}, {\it{oracle\/}})\index{choose-time} $\not<$ {\it{min\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{max\/}} $\not<$ {\rm{choose-time}}\,({\it{min\/}}, {\it{max\/}}, {\it{oracle\/}})\index{choose-time}))\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it choose-time\/}.

\begin{tabbing}{\sc Theorem}:  lessp-sub1-choose-sub1-max \\ \index{lessp-sub1-choose-sub1-max}
\=\+((({\it{max\/}} $-\;1$) $<$ {\it{x\/}}) $\wedge$ ({\it{min\/}} $\leq$ {\it{max\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\rm{choose-time}}\,({\it{min\/}}, {\it{max\/}}, {\it{oracle\/}})\index{choose-time} $-\;1$) $<$ {\it{x\/}}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{verbatim};; The gate can be in 4 states: open, closed, going-up, going-down.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  gate-parameters-intro \\ \index{gate-parameters-intro}
\=\+({\sc{gate-closing-min-time}}\index{gate-closing-min-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\sc{gate-closing-max-time}}\index{gate-closing-max-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\sc{gate-closing-max-time}}\index{gate-closing-max-time}) \\ 
$\wedge$$\;\;\;\;$({\sc{gate-closing-max-time}}\index{gate-closing-max-time} $\not<$ {\sc{gate-closing-min-time}}\index{gate-closing-min-time}) \\ 
$\wedge$$\;\;\;\;$({\sc{gate-opening-min-time}}\index{gate-opening-min-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\sc{gate-opening-max-time}}\index{gate-opening-max-time}) \\ 
$\wedge$$\;\;\;\;$({\sc{gate-opening-max-time}}\index{gate-opening-max-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\sc{gate-opening-max-time}}\index{gate-opening-max-time} $\not<$ {\sc{gate-opening-min-time}}\index{gate-opening-min-time})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it gate-closing-min-time\/}, {\it gate-closing-max-time\/}, {\it gate-opening-min-time\/}, and {\it gate-opening-max-time\/}.

\begin{verbatim};; The gate state is a pair (current-state . n) where n is the time that 
;; the gate will remain in that state.  This is only required for going
;; up and going down and tells us how long they can expect to be in that
;; condition unless they are given a countervening order.  This doesn't 
;; take into account some anomolous situations as , for example, when we
;; may have just told the gate to close and immediately tell it to open, 
;; so that it has only a short distance to move.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gate-positionp} \\  
{\rm{gate-positionp}}\,({\it{x\/}})\index{gate-positionp} $=$ ({\it{x\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{open}}{\tt{ }}{\tt{closed}}{\tt{ }}{\tt{going-up}}{\tt{ }}{\tt{going-down}}{\tt{)}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gate-current-state}$\;\;$
{\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state} $=$ {\rm{car}}\,({\it{state\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gate-state-duration}$\;\;$
{\rm{gate-state-duration}}\,({\it{state\/}})\index{gate-state-duration} $=$ {\rm{cdr}}\,({\it{state\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{open} \\  
{\rm{open}}\,({\it{state\/}})\index{open} $=$ ({\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state} $=$ {\tt{'}}{\tt{open}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{closed} \\  
{\rm{closed}}\,({\it{state\/}})\index{closed} $=$ ({\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state} $=$ {\tt{'}}{\tt{closed}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{going-up} \\  
{\rm{going-up}}\,({\it{state\/}})\index{going-up} $=$ ({\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state} $=$ {\tt{'}}{\tt{going-up}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{going-down} \\  
{\rm{going-down}}\,({\it{state\/}})\index{going-down} $=$ ({\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state} $=$ {\tt{'}}{\tt{going-down}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gate-state-accessors \\ \index{gate-state-accessors}
\=\+({\rm{gate-current-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{gate-current-state} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{gate-state-duration}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{gate-state-duration} $=$ {\it{y\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{legal-gate-statep} \\  
\=\+{\rm{legal-gate-statep}}\,({\it{x\/}})\index{legal-gate-statep} \\ 
$=$$\;\;\;\;$(\=\+{\rm{gate-positionp}}\,({\rm{gate-current-state}}\,({\it{x\/}})\index{gate-current-state})\index{gate-positionp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{going-up}}\,({\it{x\/}})\index{going-up} $\vee$ {\rm{going-down}}\,({\it{x\/}})\index{going-down}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{gate-state-duration}}\,({\it{x\/}})\index{gate-state-duration} $\in\;${\bf{N}}${}$))\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable gate-current-state.

\addvspace{18pt}

\noindent{\sc Event}:   Disable gate-state-duration.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{compute-going-down-state} \\  
\=\+{\rm{compute-going-down-state}}\,({\it{state\/}})\index{compute-going-down-state} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{n\/}}{\bf $\;$ be$\;\;$}{\rm{gate-state-duration}}\,({\it{state\/}})\index{gate-state-duration}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\tt{'}}{\tt{closed}}, {\tt{0}}) \\ 
{\bf else }{\rm{cons}}\,({\tt{'}}{\tt{going-down}}, {\it{n\/}} $-\;1$)$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{compute-going-up-state} \\  
\=\+{\rm{compute-going-up-state}}\,({\it{state\/}})\index{compute-going-up-state} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{n\/}}{\bf $\;$ be$\;\;$}{\rm{gate-state-duration}}\,({\it{state\/}})\index{gate-state-duration}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\tt{'}}{\tt{open}}, {\tt{0}}) \\ 
{\bf else }{\rm{cons}}\,({\tt{'}}{\tt{going-up}}, {\it{n\/}} $-\;1$)$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gate-next-state} \\  
\=\+{\rm{gate-next-state}}\,({\it{cmd\/}}, {\it{state\/}}, {\it{oracle\/}})\index{gate-next-state} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\it{cmd\/}}: \\ 
{\bf case = }{\it{close\/}} \\ 
{\bf then }\=\+{\bf case on }{\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state}: \\ 
{\bf case = }{\it{open\/}} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\tt{'}}{\tt{going-down}}, \\ 
{\rm{choose-time}}\,(\=\+{\sc{gate-closing-min-time}}\index{gate-closing-min-time}, \\ 
{\sc{gate-closing-max-time}}\index{gate-closing-max-time}, \\ 
{\it{oracle\/}})\-\index{choose-time} $-\;1$)\- \\ 
{\bf case = }{\it{closed\/}} \\ 
{\bf $\;\;$then }{\it{state\/}} \\ 
{\bf case = }{\it{going-up\/}} \\ 
{\bf $\;\;$then }{\rm{cons}}\,(\=\+{\tt{'}}{\tt{going-down}}, \\ 
{\rm{choose-time}}\,(\=\+{\sc{gate-closing-min-time}}\index{gate-closing-min-time}, \\ 
{\sc{gate-closing-max-time}}\index{gate-closing-max-time}, \\ 
{\it{oracle\/}})\-\index{choose-time} $-\;1$)\- \\ 
{\bf case = }{\it{going-down\/}} \\ 
{\bf $\;\;$then }{\rm{compute-going-down-state}}\,({\it{state\/}})\index{compute-going-down-state} \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\- \\ 
{\bf case = }{\it{open\/}} \\ 
{\bf $\;\;$then }\=\+{\bf case on }{\rm{gate-current-state}}\,({\it{state\/}})\index{gate-current-state}: \\ 
{\bf case = }{\it{open\/}} \\ 
{\bf then }{\it{state\/}} \\ 
{\bf case = }{\it{closed\/}} \\ 
{\bf $\;\;$then }{\rm{cons}}\,(\=\+{\tt{'}}{\tt{going-up}}, \\ 
{\rm{choose-time}}\,(\=\+{\sc{gate-opening-min-time}}\index{gate-opening-min-time}, \\ 
{\sc{gate-opening-max-time}}\index{gate-opening-max-time}, \\ 
{\it{oracle\/}})\-\index{choose-time} $-\;1$)\- \\ 
{\bf case = }{\it{going-up\/}} \\ 
{\bf $\;\;$then }{\rm{compute-going-up-state}}\,({\it{state\/}})\index{compute-going-up-state} \\ 
{\bf case = }{\it{going-down\/}} \\ 
{\bf $\;\;$then }{\rm{cons}}\,(\=\+{\tt{'}}{\tt{going-up}}, \\ 
{\rm{choose-time}}\,(\=\+{\sc{gate-opening-min-time}}\index{gate-opening-min-time}, \\ 
{\sc{gate-opening-max-time}}\index{gate-opening-max-time}, \\ 
{\it{oracle\/}})\-\index{choose-time} $-\;1$)\- \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\- \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{verbatim};; TRAIN BEHAVIOR
;; The train provides our input to the system.  The gate must act in
;; response to the train.  It can do so only if the behavior of the 
;; train meets certain reasonable criteria.  Therefore, the specification
;; of the train consists of a set of constraints on the possible traces of 
;; the train behavior as sensed by input sensors along the track.  The
;; train can be in one of 4 states: approaching the crossing, 
;; in the crossing, past the crossing (or outside of our field of view).
;; We assume that the sensors are accurate (debounced) and that trains are
;; sufficiently widely separated. 

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{train-positionp} \\  
{\rm{train-positionp}}\,({\it{x\/}})\index{train-positionp} $=$ ({\it{x\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{approaching}}{\tt{ }}{\tt{in-gate}}{\tt{ }}{\tt{elsewhere}}{\tt{)}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{approaching}$\;\;$
{\rm{approaching}}\,({\it{x\/}})\index{approaching} $=$ ({\it{x\/}} $=$ {\tt{'}}{\tt{approaching}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{in-gate}$\;\;$
{\rm{in-gate}}\,({\it{x\/}})\index{in-gate} $=$ ({\it{x\/}} $=$ {\tt{'}}{\tt{in-gate}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{elsewhere}$\;\;$
{\rm{elsewhere}}\,({\it{x\/}})\index{elsewhere} $=$ ({\it{x\/}} $=$ {\tt{'}}{\tt{elsewhere}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{legal-next-positions} \\  
\=\+{\rm{legal-next-positions}}\,({\it{x\/}})\index{legal-next-positions} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\it{x\/}}: \\ 
{\bf case = }{\it{elsewhere\/}} \\ 
{\bf then }{\tt{'}}{\tt{(}}{\tt{elsewhere}}{\tt{ }}{\tt{approaching}}{\tt{)}} \\ 
{\bf case = }{\it{approaching\/}} \\ 
{\bf $\;\;$then }{\tt{'}}{\tt{(}}{\tt{approaching}}{\tt{ }}{\tt{in-gate}}{\tt{)}} \\ 
{\bf case = }{\it{in-gate\/}} \\ 
{\bf $\;\;$then }{\tt{'}}{\tt{(}}{\tt{in-gate}}{\tt{ }}{\tt{elsewhere}}{\tt{)}} \\ 
{\bf otherwise }{\bf{nil}}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{legal-transitionp} \\  
{\rm{legal-transitionp}}\,({\it{x\/}}, {\it{y\/}})\index{legal-transitionp} $=$ ({\it{y\/}} $\in$ {\rm{legal-next-positions}}\,({\it{x\/}})\index{legal-next-positions})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{legal-train-trace1} \\  
\=\+{\rm{legal-train-trace1}}\,({\it{trace\/}})\index{legal-train-trace1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{trace\/}} $=$ {\bf{nil}} \\ 
{\bf else }\=\+{\rm{train-positionp}}\,({\rm{car}}\,({\it{trace\/}}))\index{train-positionp} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{trace\/}})) \\ 
{\bf then }{\rm{legal-transitionp}}\,({\rm{car}}\,({\it{trace\/}}), {\rm{cadr}}\,({\it{trace\/}}))\index{legal-transitionp} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;${\rm{legal-train-trace1}}\,({\rm{cdr}}\,({\it{trace\/}}))\index{legal-train-trace1}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  train-constraints \\ \index{train-constraints}
\=\+({\sc{approaching-min-time}}\index{approaching-min-time} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\sc{approaching-min-time}}\index{approaching-min-time} $\not<$ ($1\;+$ {\sc{gate-closing-max-time}}\index{gate-closing-max-time}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it approaching-min-time\/}.

\begin{tabbing}{\sc Definition}:\index{seq-long-enough} \\  
\=\+{\rm{seq-long-enough}}\,({\it{x\/}}, {\it{trace\/}}, {\it{seen-so-far\/}}, {\it{min\/}})\index{seq-long-enough} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{seen-so-far\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{trace\/}}) $=$ {\it{x\/}} \\ 
{\bf then }{\rm{seq-long-enough}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{trace\/}}), {\tt{1}}, {\it{min\/}})\index{seq-long-enough} \\ 
{\bf else }{\rm{seq-long-enough}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{trace\/}}), {\tt{0}}, {\it{min\/}})\index{seq-long-enough}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{min\/}} $\leq$ {\it{seen-so-far\/}} \\ 
{\bf elseif }{\rm{car}}\,({\it{trace\/}}) $=$ {\it{x\/}} \\ 
{\bf then }{\rm{seq-long-enough}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{trace\/}}), $1\;+$ {\it{seen-so-far\/}}, {\it{min\/}})\index{seq-long-enough} \\ 
{\bf else }\=\+({\it{min\/}} $\leq$ {\it{seen-so-far\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{seq-long-enough}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{trace\/}}), {\tt{0}}, {\it{min\/}})\index{seq-long-enough}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{approaches-long-enough} \\  
\=\+{\rm{approaches-long-enough}}\,({\it{trace\/}}, {\it{seen-so-far\/}})\index{approaches-long-enough} \\ 
$=$$\;\;\;\;${\rm{seq-long-enough}}\,(\=\+{\tt{'}}{\tt{approaching}}, \\ 
{\it{trace\/}}, \\ 
{\it{seen-so-far\/}}, \\ 
{\sc{approaching-min-time}}\index{approaching-min-time})\-\index{seq-long-enough}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{distance-to-gate} \\  
\=\+{\rm{distance-to-gate}}\,({\it{trace\/}})\index{distance-to-gate} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }$1\;+$ ($1\;+$ {\sc{approaching-min-time}}\index{approaching-min-time}) \\ 
{\bf elseif }{\rm{in-gate}}\,({\rm{car}}\,({\it{trace\/}}))\index{in-gate}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{distance-to-gate}}\,({\rm{cdr}}\,({\it{trace\/}}))\index{distance-to-gate}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable approaches-long-enough.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{legal-train-trace} \\  
\=\+{\rm{legal-train-trace}}\,({\it{trace\/}}, {\it{n\/}})\index{legal-train-trace} \\ 
$=$$\;\;\;\;$({\rm{legal-train-trace1}}\,({\it{trace\/}})\index{legal-train-trace1} $\wedge$ {\rm{approaches-long-enough}}\,({\it{trace\/}}, {\it{n\/}})\index{approaches-long-enough})\-
\end{tabbing}

\begin{verbatim};; CONTROLLER
;; The controller takes as input a sequence of readings from the track
;; sensors telling where the train is.  It's output is a sequence of 
;; actuator commands of the form 'open or 'close.  The gate responds to 
;; these.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{control-output} \\  
\=\+{\rm{control-output}}\,({\it{input\/}})\index{control-output} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{input\/}} $=$ {\tt{'}}{\tt{elsewhere}}$\;\;${\bf then }{\tt{'}}{\tt{open}} \\ 
{\bf else }{\tt{'}}{\tt{close}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; THE SYSTEM

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gate-behavior} \\  
\=\+{\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{next-state\/}}{\bf $\;$ be$\;\;$}{\rm{gate-next-state}}\,(\=\+{\rm{control-output}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{control-output}, \\ 
{\it{gate-state\/}}, \\ 
{\it{train-trace\/}})\-\index{gate-next-state}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\it{next-state\/}}, \\ 
{\rm{gate-behavior}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\it{next-state\/}})\index{gate-behavior})\-$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  approaches-stay-long-enough \\ \index{approaches-stay-long-enough}
\=\+(\=\+{\rm{approaches-long-enough}}\,({\it{train-trace\/}}, {\it{approaching-time\/}})\index{approaches-long-enough} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{approaches-long-enough}}\,({\rm{cdr}}\,({\it{train-trace\/}}), $1\;+$ {\it{approaching-time\/}})\index{approaches-long-enough}\-
\end{tabbing}

\begin{verbatim};; Now we state safety properties of this system.  In particular,
;; we devise constraints that assure that the gate will always be
;; closed when the train is in the gate.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  approaches-long-enough-zero \\ \index{approaches-long-enough-zero}
\=\+{\rm{listp}}\,({\it{train-trace\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{approaches-long-enough}}\,({\it{train-trace\/}}, {\it{approaching-time\/}})\index{approaches-long-enough} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{approaching-time\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}} \\ 
{\bf then }{\rm{approaches-long-enough}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\tt{1}})\index{approaches-long-enough} \\ 
{\bf else }{\rm{approaches-long-enough}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\tt{0}})\index{approaches-long-enough}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}} \\ 
{\bf then }{\rm{approaches-long-enough}}\,(\=\+{\rm{cdr}}\,({\it{train-trace\/}}), \\ 
$1\;+$ {\it{approaching-time\/}})\-\index{approaches-long-enough} \\ 
{\bf else }\=\+{\rm{approaches-long-enough}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\tt{0}})\index{approaches-long-enough} \\ 
$\wedge$$\;\;\;\;$({\it{approaching-time\/}} $\not<$ {\sc{approaching-min-time}}\index{approaching-min-time})\-$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{distance-to-gate-induction} \\  
\=\+{\rm{distance-to-gate-induction}}\,({\it{train-trace\/}}, {\it{n\/}})\index{distance-to-gate-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{train-trace\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}} \\ 
{\bf then }{\rm{distance-to-gate-induction}}\,({\rm{cdr}}\,({\it{train-trace\/}}), $1\;+$ {\it{n\/}})\index{distance-to-gate-induction} \\ 
{\bf else }{\rm{distance-to-gate-induction}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\tt{0}})\index{distance-to-gate-induction}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distance-to-gate-first-approaching \\ \index{distance-to-gate-first-approachi!ng}
\=\+(\=\+{\rm{listp}}\,({\it{train-trace\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}}) \\ 
$\wedge$$\;\;\;\;${\rm{approaches-long-enough}}\,({\it{train-trace\/}}, {\it{n\/}})\index{approaches-long-enough})\- \\ 
$\rightarrow$$\;\;\;\;$({\sc{approaching-min-time}}\index{approaching-min-time} $<$ ({\it{n\/}} $+$ ($1\;+$ {\rm{distance-to-gate}}\,({\it{train-trace\/}})\index{distance-to-gate})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distance-to-gate-first-approaching2 \\ \index{distance-to-gate-first-approachi!ng2}
\=\+(\=\+{\rm{listp}}\,({\it{train-trace\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{train-trace\/}}) $=$ {\tt{'}}{\tt{approaching}}) \\ 
$\wedge$$\;\;\;\;${\rm{approaches-long-enough}}\,({\it{train-trace\/}}, {\tt{0}})\index{approaches-long-enough})\- \\ 
$\rightarrow$$\;\;\;\;$(({\sc{approaching-min-time}}\index{approaching-min-time} $-\;1$) $<$ {\rm{distance-to-gate}}\,({\it{train-trace\/}})\index{distance-to-gate})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-statep} \\  
\=\+{\rm{good-statep}}\,({\it{train-state\/}}, {\it{gate-state\/}}, {\it{distance-to-gate\/}}, {\it{time-elsewhere\/}})\index{good-statep} \\ 
$=$$\;\;\;\;$(\=\+(\=\+{\rm{going-down}}\,({\it{gate-state\/}})\index{going-down} \\ 
$\rightarrow$$\;\;\;\;$({\rm{gate-state-duration}}\,({\it{gate-state\/}})\index{gate-state-duration} $<$ {\sc{gate-closing-max-time}}\index{gate-closing-max-time}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{going-up}}\,({\it{gate-state\/}})\index{going-up} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gate-state-duration}}\,({\it{gate-state\/}})\index{gate-state-duration} \\ 
$<$$\;\;\;\;${\sc{gate-opening-max-time}}\index{gate-opening-max-time})\-)\- \\ 
$\wedge$$\;\;\;\;$\=\+{\bf case on }{\it{train-state\/}}: \\ 
{\bf case = }{\it{in-gate\/}} \\ 
{\bf then }{\rm{closed}}\,({\it{gate-state\/}})\index{closed} \\ 
{\bf case = }{\it{approaching\/}} \\ 
{\bf $\;\;$then }\=\+{\rm{closed}}\,({\it{gate-state\/}})\index{closed} \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{going-down}}\,({\it{gate-state\/}})\index{going-down} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{gate-state-duration}}\,({\it{gate-state\/}})\index{gate-state-duration} \\ 
$<$$\;\;\;\;${\it{distance-to-gate\/}})\-)\- \\ 
$\vee$$\;\;\;\;$({\sc{gate-closing-max-time}}\index{gate-closing-max-time} $<$ {\it{distance-to-gate\/}})\- \\ 
{\bf case = }{\it{elsewhere\/}} \\ 
{\bf $\;\;$then }\=\+(\=\+({\sc{gate-opening-max-time}}\index{gate-opening-max-time} $<$ {\it{time-elsewhere\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{open}}\,({\it{gate-state\/}})\index{open})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{closed}}\,({\it{gate-state\/}})\index{closed} $\wedge$ ({\it{time-elsewhere\/}} $\simeq {\tt{0}}$)) \\ 
$\vee$$\;\;\;\;${\rm{open}}\,({\it{gate-state\/}})\index{open} \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{going-up}}\,({\it{gate-state\/}})\index{going-up} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{gate-state-duration}}\,({\it{gate-state\/}})\index{gate-state-duration} \\ 
$\leq$$\;\;\;\;$(\=\+{\sc{gate-opening-max-time}}\index{gate-opening-max-time} \\ 
$-$$\;\;\;\;${\it{time-elsewhere\/}})\-)\-)\-)\-\- \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{su-invariant} \\  
\=\+{\rm{su-invariant}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{su-invariant} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{gate-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+{\rm{good-statep}}\,(\=\+{\rm{car}}\,({\it{train-trace\/}}), \\ 
{\rm{car}}\,({\it{gate-trace\/}}), \\ 
{\rm{distance-to-gate}}\,({\it{train-trace\/}})\index{distance-to-gate}, \\ 
{\it{time-elsewhere\/}})\-\index{good-statep} \\ 
$\wedge$$\;\;\;\;${\rm{su-invariant}}\,(\=\+{\rm{cdr}}\,({\it{train-trace\/}}), \\ 
{\rm{cdr}}\,({\it{gate-trace\/}}), \\ 
\=\+{\bf if }{\rm{elsewhere}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{elsewhere} \\ 
{\bf then }$1\;+$ {\it{time-elsewhere\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\index{su-invariant}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{controller-induction} \\  
\=\+{\rm{controller-induction}}\,({\it{train-trace\/}}, {\it{gate-state\/}}, {\it{time-approaching\/}}, {\it{time-elsewhere\/}})\index{controller-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{train-trace\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{controller-induction}}\,(\=\+{\rm{cdr}}\,({\it{train-trace\/}}), \\ 
{\rm{gate-next-state}}\,(\=\+{\rm{control-output}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{control-output}, \\ 
{\it{gate-state\/}}, \\ 
{\it{train-trace\/}})\-\index{gate-next-state}, \\ 
\=\+{\bf if }\=\+{\rm{car}}\,({\it{train-trace\/}}) \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{approaching}}\- \\ 
{\bf then }$1\;+$ {\it{time-approaching\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-, \\ 
\=\+{\bf if }\=\+{\rm{car}}\,({\it{train-trace\/}}) \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{elsewhere}}\- \\ 
{\bf then }$1\;+$ {\it{time-elsewhere\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\index{controller-induction}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-su-invariant \\ \index{controller-su-invariant}
\=\+(\=\+{\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace} \\ 
$\wedge$$\;\;\;\;${\rm{legal-gate-statep}}\,({\it{gate-state\/}})\index{legal-gate-statep} \\ 
$\wedge$$\;\;\;\;${\rm{good-statep}}\,(\=\+{\rm{car}}\,({\it{train-trace\/}}), \\ 
{\it{gate-state\/}}, \\ 
{\rm{distance-to-gate}}\,({\it{train-trace\/}})\index{distance-to-gate}, \\ 
{\it{time-elsewhere\/}})\-\index{good-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{su-invariant}}\,(\=\+{\it{train-trace\/}}, \\ 
{\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior}, \\ 
{\it{time-elsewhere\/}})\-\index{su-invariant}\-
\end{tabbing}

\begin{verbatim};; Now we define the desired safety and utility properties and prove that
;; they follow from the su-invariant property.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{safety} \\  
\=\+{\rm{safety}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{in-gate}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{in-gate} \\ 
{\bf then }\=\+{\rm{closed}}\,({\rm{car}}\,({\it{gate-trace\/}}))\index{closed} \\ 
$\wedge$$\;\;\;\;${\rm{safety}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\rm{cdr}}\,({\it{gate-trace\/}}))\index{safety}\- \\ 
{\bf else }{\rm{safety}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\rm{cdr}}\,({\it{gate-trace\/}}))\index{safety}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  su-invariant-implies-safety \\ \index{su-invariant-implies-safety}
\=\+{\rm{su-invariant}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{su-invariant} \\ 
$\rightarrow$$\;\;\;\;${\rm{safety}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{utility} \\  
\=\+{\rm{utility}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{utility} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{train-trace\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{elsewhere}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{elsewhere} \\ 
{\bf then }\=\+\=\+{\bf if }{\sc{gate-opening-max-time}}\index{gate-opening-max-time} $<$ {\it{time-elsewhere\/}} \\ 
{\bf then }{\rm{open}}\,({\rm{car}}\,({\it{gate-trace\/}}))\index{open} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;${\rm{utility}}\,(\=\+{\rm{cdr}}\,({\it{train-trace\/}}), \\ 
{\rm{cdr}}\,({\it{gate-trace\/}}), \\ 
$1\;+$ {\it{time-elsewhere\/}})\-\index{utility}\- \\ 
{\bf else }{\rm{utility}}\,({\rm{cdr}}\,({\it{train-trace\/}}), {\rm{cdr}}\,({\it{gate-trace\/}}), {\tt{0}})\index{utility}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  su-invariant-implies-utility \\ \index{su-invariant-implies-utility}
\=\+{\rm{su-invariant}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{su-invariant} \\ 
$\rightarrow$$\;\;\;\;${\rm{utility}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{utility}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-maintains-safety-and-utility \\ \index{controller-maintains-safety-and!-utility}
\=\+(\=\+{\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace} \\ 
$\wedge$$\;\;\;\;${\rm{legal-gate-statep}}\,({\it{gate-state\/}})\index{legal-gate-statep} \\ 
$\wedge$$\;\;\;\;${\rm{good-statep}}\,(\=\+{\rm{car}}\,({\it{train-trace\/}}), \\ 
{\it{gate-state\/}}, \\ 
{\rm{distance-to-gate}}\,({\it{train-trace\/}})\index{distance-to-gate}, \\ 
{\it{time-elsewhere\/}})\-\index{good-statep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{safety}}\,({\it{train-trace\/}}, {\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior})\index{safety} \\ 
$\wedge$$\;\;\;\;${\rm{utility}}\,(\=\+{\it{train-trace\/}}, \\ 
{\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior}, \\ 
{\it{time-elsewhere\/}})\-\index{utility})\-\-
\end{tabbing}

\begin{verbatim};; We now characterize an initial state and show that our invariant 
;; is true in that initial state.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{initial-statep} \\  
\=\+{\rm{initial-statep}}\,({\it{train-state\/}}, {\it{gate-state\/}})\index{initial-statep} \\ 
$=$$\;\;\;\;$(\=\+({\it{train-state\/}} $=$ {\tt{'}}{\tt{elsewhere}}) \\ 
$\wedge$$\;\;\;\;$({\rm{gate-current-state}}\,({\it{gate-state\/}})\index{gate-current-state} $=$ {\tt{'}}{\tt{open}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-safety \\ \index{controller-safety}
\=\+(\=\+{\rm{initial-statep}}\,({\rm{car}}\,({\it{train-trace\/}}), {\it{gate-state\/}})\index{initial-statep} \\ 
$\wedge$$\;\;\;\;${\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{safety}}\,({\it{train-trace\/}}, {\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior})\index{safety}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-utility \\ \index{controller-utility}
\=\+(\=\+{\rm{initial-statep}}\,({\rm{car}}\,({\it{train-trace\/}}), {\it{gate-state\/}})\index{initial-statep} \\ 
$\wedge$$\;\;\;\;${\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{utility}}\,(\=\+{\it{train-trace\/}}, \\ 
{\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior}, \\ 
{\it{time-elsewhere\/}})\-\index{utility}\-
\end{tabbing}

\begin{verbatim};; AN ALTERNATIVE SPECIFICATION
;; The criticism may be raised that our specification functions
;; SAFETY and UTILITY are harder to understand than the alternatives
;; available in some other specification languages, using quantifiers
;; for example.  We offer alternative versions SAFETY2 and UTILITY2
;; that are in a quantified style and prove that they are 
;; consequences of our versions.  

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{x\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }$1\;+$ {\it{x\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{get} \\  
\=\+{\rm{get}}\,({\it{n\/}}, {\it{lst\/}})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{car}}\,({\it{lst\/}}) \\ 
{\bf else }{\rm{get}}\,({\it{n\/}} $-\;1$, {\rm{cdr}}\,({\it{lst\/}}))\index{get}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{safety2} \\  
\=\+{\rm{safety2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety2} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{i\/}}$\;$({\rm{in-gate}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{in-gate} $\rightarrow$ {\rm{closed}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{closed})\index{forall}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  safety2-suff \\ \index{safety2-suff}
\=\+(\=\+{\rm{in-gate}}\,({\rm{get}}\,({\rm{i}}\,({\it{gate-trace\/}}, {\it{train-trace\/}})\index{i}, {\it{train-trace\/}})\index{get})\index{in-gate} \\ 
$\rightarrow$$\;\;\;\;${\rm{closed}}\,({\rm{get}}\,({\rm{i}}\,({\it{gate-trace\/}}, {\it{train-trace\/}})\index{i}, {\it{gate-trace\/}})\index{get})\index{closed})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{safety2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety2}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  safety2-necc \\ \index{safety2-necc}
\=\+($\neg$ ({\rm{in-gate}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{in-gate} $\rightarrow$ {\rm{closed}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{closed})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{safety2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety2})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{get-induct} \\  
\=\+{\rm{get-induct}}\,({\it{i\/}}, {\it{x\/}}, {\it{y\/}})\index{get-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{get-induct}}\,({\it{i\/}} $-\;1$, {\rm{cdr}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{y\/}}))\index{get-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  safety-implies-safety2-get \\ \index{safety-implies-safety2-get}
\=\+({\rm{safety}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety} $\wedge$ {\rm{in-gate}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{in-gate}) \\ 
$\rightarrow$$\;\;\;\;${\rm{closed}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{closed}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  safety-implies-safety2 \\ \index{safety-implies-safety2}
{\rm{safety}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety} $\rightarrow$ {\rm{safety2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}})\index{safety2}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-safety2 \\ \index{controller-safety2}
\=\+(\=\+{\rm{initial-statep}}\,({\rm{car}}\,({\it{train-trace\/}}), {\it{gate-state\/}})\index{initial-statep} \\ 
$\wedge$$\;\;\;\;${\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{safety2}}\,({\it{train-trace\/}}, {\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior})\index{safety2}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{time-elsewhere} \\  
\=\+{\rm{time-elsewhere}}\,({\it{i\/}}, {\it{found-so-far\/}}, {\it{train-trace\/}})\index{time-elsewhere} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{found-so-far\/}} \\ 
{\bf elseif }{\rm{elsewhere}}\,({\rm{car}}\,({\it{train-trace\/}}))\index{elsewhere} \\ 
{\bf then }{\rm{time-elsewhere}}\,({\it{i\/}} $-\;1$, $1\;+$ {\it{found-so-far\/}}, {\rm{cdr}}\,({\it{train-trace\/}}))\index{time-elsewhere} \\ 
{\bf else }{\rm{time-elsewhere}}\,({\it{i\/}} $-\;1$, {\tt{0}}, {\rm{cdr}}\,({\it{train-trace\/}}))\index{time-elsewhere}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{utility2} \\  
\=\+{\rm{utility2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{n\/}})\index{utility2} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{i\/}}$\;$(\=\+(\=\+{\rm{elsewhere}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{elsewhere} \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{gate-opening-max-time}}\index{gate-opening-max-time} \\ 
$<$$\;\;\;\;${\rm{time-elsewhere}}\,({\it{i\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{time-elsewhere})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{open}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{open})\-\index{forall}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  utility2-suff \\ \index{utility2-suff}
\=\+(\=\+(\=\+{\rm{elsewhere}}\,({\rm{get}}\,({\rm{i-1}}\,({\it{gate-trace\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{i-1}, {\it{train-trace\/}})\index{get})\index{elsewhere} \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{gate-opening-max-time}}\index{gate-opening-max-time} \\ 
$<$$\;\;\;\;${\rm{time-elsewhere}}\,({\rm{i-1}}\,({\it{gate-trace\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{i-1}, {\it{n\/}}, {\it{train-trace\/}})\index{time-elsewhere})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{open}}\,({\rm{get}}\,({\rm{i-1}}\,({\it{gate-trace\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{i-1}, {\it{gate-trace\/}})\index{get})\index{open})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{utility2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{n\/}})\index{utility2}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  utility2-necc \\ \index{utility2-necc}
\=\+($\neg$ (\=\+(\=\+{\rm{elsewhere}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{elsewhere} \\ 
$\wedge$$\;\;\;\;$({\sc{gate-opening-max-time}}\index{gate-opening-max-time} $<$ {\rm{time-elsewhere}}\,({\it{i\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{time-elsewhere}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{open}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{open})\-) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{utility2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{n\/}})\index{utility2})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{get-induct2} \\  
\=\+{\rm{get-induct2}}\,({\it{i\/}}, {\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{get-induct2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{get-induct2}}\,(\=\+{\it{i\/}} $-\;1$, \\ 
{\rm{cdr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\it{y\/}}), \\ 
\=\+{\bf if }{\rm{elsewhere}}\,({\rm{car}}\,({\it{x\/}}))\index{elsewhere}$\;\;${\bf then }$1\;+$ {\it{n\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\index{get-induct2}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  utility-implies-utility2-get \\ \index{utility-implies-utility2-get}
\=\+(\=\+{\rm{utility}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{n\/}})\index{utility} \\ 
$\wedge$$\;\;\;\;${\rm{elsewhere}}\,({\rm{get}}\,({\it{i\/}}, {\it{train-trace\/}})\index{get})\index{elsewhere} \\ 
$\wedge$$\;\;\;\;$({\sc{gate-opening-max-time}}\index{gate-opening-max-time} $<$ {\rm{time-elsewhere}}\,({\it{i\/}}, {\it{n\/}}, {\it{train-trace\/}})\index{time-elsewhere}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{open}}\,({\rm{get}}\,({\it{i\/}}, {\it{gate-trace\/}})\index{get})\index{open}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  utility-implies-utility2 \\ \index{utility-implies-utility2}
\=\+{\rm{utility}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{utility} \\ 
$\rightarrow$$\;\;\;\;${\rm{utility2}}\,({\it{train-trace\/}}, {\it{gate-trace\/}}, {\it{time-elsewhere\/}})\index{utility2}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  controller-utility2 \\ \index{controller-utility2}
\=\+(\=\+{\rm{initial-statep}}\,({\rm{car}}\,({\it{train-trace\/}}), {\it{gate-state\/}})\index{initial-statep} \\ 
$\wedge$$\;\;\;\;${\rm{legal-train-trace}}\,({\it{train-trace\/}}, {\it{time-approaching\/}})\index{legal-train-trace})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{utility2}}\,(\=\+{\it{train-trace\/}}, \\ 
{\rm{gate-behavior}}\,({\it{train-trace\/}}, {\it{gate-state\/}})\index{gate-behavior}, \\ 
{\it{time-elsewhere\/}})\-\index{utility2}\-
\end{tabbing}

%\end{list}
\printindex
\end{document}
