\documentstyle[fuzz]{article}

\input{./handout}

\begin{document}

\handout{7A}{27 September 1995}{Telephone Net}


\subsection*{Preliminaries}

We begin by adding a new operator to the Mathematical Tool-kit. $disj$ is
a predicate which is true of a sets of sets, $S$, if and only if no two
distinct sets in $S$ intersect.

%%prerel disj

\begin{gendef}[X]
    disj \_: \power (\power (\power X))
\where
    \forall S: \power (\power X) @ \\
\t1	disj~S \iff (\forall i,j: S @ i \neq j \implies i \cap j = \empty)
\end{gendef}

\subsection*{Basic Telephone Net}

We take the type $PHONE$ to be a given, or primitive type. A phone
connection is simply a set of phones, and we define 
$CON$ to represent the type of all possible phone connections.

\begin{zed}
    [PHONE] 
\also
    CON == \power PHONE
\end{zed}

We now define the schema $TN$ to model a telephone net. It consists of
a set of connections, $cons$, and a set of requests, $reqs$. We require
that all connections are also requests and that no phone is simultaneously
in two distinct connections.
\begin{schema}{TN}
    reqs, cons: \power CON
\where
    cons \subseteq reqs \\
    disj~cons
\end{schema}

\subsection*{Efficient Telephone Net}

An {\em efficient} telephone net is a telephone net for which it is not
possible to connect an unsatisfied request without violating the telephone
net invariant.

\begin{schema}{EfficientTN}
    TN
\where
    \lnot (\exists r: reqs \setminus cons @ disj~(cons \cup \{ r \}))
\end{schema}

This schema expresses a property of maximality about the connections: it
is not possible to enlarge the set of connections.

\subsection*{Operations}

All operations that we plan to define for a telephone net will share
certain properties. We capture these once and for all in the schema
$Event$, which states that an operation will not disconnect any
connections provided they are still requested after the operation.

\begin{schema}{Event}
    \Delta EfficientTN
\where
    \forall c: CON @
	c \in (cons \cap reqs') \implies c \in cons'
\end{schema}

The operation $Call$ adds a request to the set of requests of a telephone
net.

\begin{schema}{Call}
    Event \\
    ph?, dialed?: PHONE
\where
    reqs' = reqs \cup \{ \{ph?, dialed? \} \}
\end{schema}

Given the maximality constraint on TN it is possible to infer from this
operation that if neither phone is already connected, the request will
be connected. (Exercise for the reader.)

The next operation, $Hangup$, terminates a  connnection (if any)
involving the phone $ph?$.

\begin{schema}{Hangup}
    Event \\
    ph?: PHONE
\where
    reqs' = reqs \setminus \{ c: cons | ph? \in c \}
\end{schema}

Finally, we define an operation $Busy$, which tells whether a phone is
involved in a connection.

\begin{zed}
    YesOrNo ::= YES | NO
\end{zed}

\begin{schema}{Busy}
    Event \\
    ph?: PHONE \\
    busy!: YesOrNo
\where
    reqs' = reqs \\
    busy! = YES \iff ph? \in \bigcup cons
\end{schema} 

It is possible to show that $cons$ does not change as a result of this
operation. (Exercise for the reader.)


\end{document}