%& latex
\documentstyle[verbatimfiles]{article}
\protect\input{psfig}

\begin{document}
\newcommand{\IR}{\mbox{\sf IR}}
\newcommand{\IG}{\mbox{\sf IG}}
\newcommand{\MR}{\mbox{\sf MR}}
\newcommand{\MG}{\mbox{\sf MG}}
\newcommand{\IE}{\mbox{\sf IE}}
\newcommand{\IX}{\mbox{\sf IX}}
\newcommand{\ME}{\mbox{\sf ME}}
\newcommand{\MX}{\mbox{\sf MX}}

\include{itc.description}

\include{itc.implementation}

\bibliographystyle{plain}
\bibliography{itc}

\appendix

\newpage
\section*{Formal verification if ITC in SMV}

{\em
This is the source file for a verification of the Island Tunnel Controller
implementation by Kathryn Fisler.  The implementation is described in
Section 2.
}

\verbatimfile{itc.smv.txt}

\newpage
\section*{VHDL description of an ITC implementation}

{\em
This is a VHDL source file for the Island Tunnel Controller by Kathryn Fisler.
The VHDL comes from a verification front end under development at
(what used to be called) AT\&T Bell Laboratories.  For details contact
{\tt kfisler@cs.indiana.edu}.
}

\verbatimfile{itc.vhdl.txt}

\end{document}
