\subsection*{The Island Tunnel Controller}
\markright{Informal Description}

\begin{flushright}
\begin{tabular}{l}
Steven D. Johnson and Kathryn Fisler\\
Computer Science Department\\
Indiana Univeristy\\
Bloomington, IN~47405-4101\\
USA\\
\{sjohnson, kfisler\}@cs.indiana.edu\\
\end{tabular}\end{flushright}

This problem is an elaboration of the {\em traffic light control}\/
problem and, as such, is a metaphor for coordinating access to a restricted
resource.  Concurrent entry/exit is allowed under certain conditions,
represented by a one-lane tunnel between ``The Mainland'' and ``The Island,''
that may at any time contain several vehicles, and an additional constraint
on the number of vehicles that can be on The Island.
\[
\psfig{figure=itc-picture.ps}
\]
We want to design a controller for the traffic lights at the each end
of this tunnel.  There are four sensors for detecting the presence of vehicles:
one at tunnel entrance on the island side (IE), one at tunnel exit on the
island side (IX), one at tunnel entrance on the mainland side (ME),
and one at tunnel exit on the mainland side (MX).

\subsubsection*{Environmental Properties}

The controller design may assume the following constraints on its environment,
described in terms of the behavior of vehicles that entering the system. 

\begin{itemize}
\item[\mbox{\sf E1}]
The vehicle sensors are conditioned signals, that is, clean pulses of
significant duration, which may also be assumed synchronous in clocked designs.

\item[\mbox{\sf E2}]
Every vehicle that crosses a sensor is detected and every gap between vehicles
that cross a sensor is detected.

\item[\mbox{\sf E3}]
Vehicles going into the tunnel are detected before they reach
the traffic light; vehicles leaving the tunnel are detected after they leave
the single-lane portion of the roadway.

\item[\mbox{\sf E4}]
Vehicles don't break down. They obey the traffic signals in finite time, and,
if necessary, a bound may be placed on this time.
Every vehicle that approaches the tunnel is committed to entering it.

\item[\mbox{\sf E5}]
Having arrived on The Island every vehicle eventually tires to leave.

\end{itemize}

\subsubsection*{Design Properties}

\begin{itemize}

\item[\mbox{\sf D1}]
{\em Light Behavior}.
The traffic lights each follow a
{\it red}, {\it green}, {\it red}, {\it green}, \dots\ sequence.
For simplicity, it is assumed that all vehicles can react instananeously
to a change in the traffic light, so that {\em neither\/} ``caution'' lights
nor duration timers are required, although these may be added if desired.

\item[\mbox{\sf D2}]
{\em Safety}.
At no time are there two vehicles in the tunnel that are traveling in
opposite directions.

\item[\mbox{\sf D3}]
{\em Liveness}.
Any vehicle attempting to reach or leave the island eventually succeeds.

\item[\mbox{\sf D3}]
{\em Access}.
Traffic on the island is limited.  Variants include:

\begin{itemize}

\item[\mbox{\sf D3.1}]
At no time are there more than 16 vehicles on the island.

\item[\mbox{\sf D3.2}]
At no time are there more than {\sc n} vhicles on the island, {\sc n}
a fixed but undetermined constant.

\item[\mbox{\sf D3.3}]
The system strives to keep the number of vehicles on the island below
$n$, a dynamically varying input.

\end{itemize}

\end{itemize}
