\subsection*{An ITC implementation}

This implementation of the Island Tunnel Controller was conceived by
Kathryn Fisler during work on visual inference research
\cite{Fisler-Johnson-CHDL95,Fisler-VIL96}.  It involves three processes,
described below using {\em algorithmic state machine}\/ (ASM) diagrams as
developed in the textbook {\em The Art of Digital Design}
\cite{ProsserWinkel87c}.
A globally clocked synchronous model is assumed.

Additional control and status signals for the three-process solutions include
the following:
IGL and IRL are the green and red lights for the island, IU indicates that the
island is using the tunnel, IR indicates that the island is requesting
the tunnel, IY indicates that the island is being instructed to
release control of the tunnel, and IG indicates that the island has
been granted control of the tunnel.

A similar set of signals has been defined for the mainland.

TC is a count of the number of cars
presently inside the tunnel and IC is a count of the number of cars
presently on the island.

In its intial/reset state, both light controllers are in their {\sf Red}
control states, both counters are zero, and no vehicles are in the system.
Alternatively, the counters correctly reflect what vehicles are in the
system.

\begin{figure}\label{fig:ARCs}
\[\psfig{figure=itc.kf.arch.ps,width=.75\textwidth}\]
\caption{Three-process architecture of the Island Tunnel Control problem.}
\end{figure}

\begin{figure}\label{fig:ASMs}
\begin{itemize}
\item {\bf Island Light Controller} \[\psfig{figure=islandasmsm.eps}\]
\item {\bf Mainland Light Controller} \[\psfig{figure=mainlandasmsm.eps}\]
\item {\bf Tunnel Controller} \[\psfig{figure=tunnelasmsm.eps}\]
\end{itemize}
\caption{Three-process implementation of the Island Tunnel Control problem.}
\end{figure}
