\begin{problem}[20]\label{Zakim}

You learned about the Leonard Zakim bridge in Quiz 2 (and may have read
about it in the newspapers last week).  As in Quiz 2, the Turnpike
Authority is still concerned about the integrity of the bridge, but they
have modified their earlier policy for traffic control.  The bridge will
still be one way, and cars will still pay tolls both on entering and
exiting the bridge, but now the tolls will be different.  In particular, a
car will pay \$5 to enter onto the bridge and will pay \$3 to exit.  To be
sure that there are never too many cars on the bridge, the Authority will
let a car onto the bridge only if \emph{the difference between the amount
of money currently at the entry toll booth minus the amount at the exit
toll booth is strictly less than~\$2500}.

The Authority has asked their engineering consultants to verify that this
policy will keep the number of cars from exceeding 500.  The consultants
have decided to model this scenario with a state machine whose states are
triples of natural numbers, $(A,B,C)$, where
\begin{itemize}
\item $A$ is an amount of money at the entry booth,
\item $B$ is an amount of money at the exit booth, and
\item $C$ is a number of cars on the bridge.
\end{itemize}
Any state with $C>500$ is called a \emph{collapsed} state, which we dearly
hope to avoid.  There will be no transition out of a collapsed state.

Since the toll booth collectors may need to start off with some amount of
money in order to make change, and there may also be some number of
``official'' cars already on the bridge when it is opened to the public,
the consultants must be ready to analyze the system started at \emph{any}
state, not necessarily with a start state $(0,0,0)$.  (However, you should
assume that even official cars pay tolls when the system is running.)

\begin{problemparts}
\problempart[3] Give a mathematical model of the Authority's system for
letting cars on and off the bridge by specifying a transition relation
between states of the form $(A,B,C)$ above.  

\solution{
State $(A,B,C)$ goes to state
\begin{enumerate}
\item[(i)]
$(A+5,B,C+1)$, providing that $A-B<2500$ and $C < 500$.  This transition models
the case where a car enters the bridge.

\item[(ii)] $(A,B+3,C-1)$, providing that $0 < C \leq 500$.  This
transition models the case where a car leaves the bridge.

\end{enumerate}
}
 
\instatements{\vfill\pagebreak}


\problempart[5]\label{variables}
Characterize each of the following derived variables
\[
\renewcommand{\arraystretch}{2}
\begin{array}{|c|c|} \hline
%%A  		  & WI \\\hline 
B                 & WI \\\hline 
A+B 		  & SI \\\hline
%A-B 		  & \\\hline % N
5C-A              & \\\hline % WD
3 A - 5 B	  & \\\hline % N
B+3C              & \\\hline % WI
15C-3A + 5B       & \\\hline %C
A - 4C -B         & \\\hline %SI
\end{array}
\]
as one of the following
\begin{center}
\begin{tabular}{|ll|} \hline
constant              & C  \\  
strictly increasing   & SI \\
strictly decreasing   & SD \\
weakly increasing but not constant & WI \\
weakly decreasing but not constant & WD \\
none of the above     & N  \\\hline
\end{tabular}
\end{center}
by entering the corresponding letter-code next to the variable.

\solution{In every transition, at least one of $A$ and $B$ increases. So
their sum is strictly increasing.  $3A-5B$ can fluctuate, going up on (i)
and down on (ii).

The difference $5C-A$ doesn't change under transitions of type~(i), but
decreases under transitions of type~(ii); so is weakly decreasing.
Likewise, $B+3C$ doesn't change under transitions of type~(ii), but
increases under transitions of type~(i); so is weakly increasing.

On the other hand, $15C$ and $3A-5B$ simultaneously increase by 15 under
transition (i) or simultaneously decrease by 15 under transition (ii),
which makes their difference constant.

Finally, under (i), $A$ increases by 5, $B$ is unchanged, and $4C$
increases by 4, so $A-4C-B$ increases by $5-4 =1$.  Similarly, under (ii),
$A$ is unchanged, $4C$ decreases by 4 and $B$ increases by 3, so $A-4C-B$
increases by $-(-4) - 3 = 1$.

The completed table follows.
\[
\renewcommand{\arraystretch}{2}
\begin{array}{|c|c|} \hline
%%A  		  & WI \\\hline 
B                 & WI \\\hline 
A+B 		  & SI \\\hline 
%A-B 		  & N  \\\hline 
5C-A              & WD \\\hline
3 A - 5 B	  & N \\\hline 
B+3C              & WI \\\hline 
15C-3A + 5B       & C  \\\hline
A - 4C -B  & SI \\\hline
\end{array}
\]}

\problempart[7] Define a simple Invariant, $P$, of the transition
system which is satisfied by the state $(0,0,0)$ and is not satisfied
by any collapsed state.  That is, $P$ is a predicate on states that is
preserved by transitions from {\em any} state to another. In addition,
$P(0,0,0)$ is true, and $P(A,B,C)$ is not true whenever $C>500$.

No proof is required.

\instatements{\newpage}

\solution{
Invariant: $3A - 5B = 15C \land C \leq 500$.

The invariant obviously holds at the state $(0,0,0)$ and does not hold in
any collapsed state.  To verify the Invariant, assume $(A,B,C)$ satisfies
the Invariant and has a transition to $(A',B',C')$.  We check that
$(A',B',C')$ satisfies the Invariant by considering the two kinds of
transitions.

Transition (i) (a car enters the bridge): so
\[
15C' = 15(C + 1) = 15C + 15 = 3A -  5B + 15 = 3(A+5) - 5B = 3A' - 5B'
\]
The transition is possible only if $A-B < 2500$.  But this
implies
\[
15C = 3A -  5B \leq 3(A-B) < 7500,
\]
so $C' = C+1 < 7500/15 + 1 = 501$ and so $C' \leq 500$, as required.

Transition (ii) (a car leaves the bridge): so
\[
15C' = 15(C - 1) = 15C - 15= 3A-5B - 15 = 3A - 5(B+3) = 3A' - 5B'.
\]
In addition, $C' < C \leq 500$ so $C' \leq 500$.
}

\problempart[5] A clever MIT intern working for the Turnpike Authority
agrees that when the system starts in state $(0,0,0)$ the Turnpike's
bridge management policy will be \emph{safe}: the bridge will not
collapse.  But she warns her boss that the policy makes system
\emph{deadlock} inevitable, that is, traffic will eventually be unable to
move even though the bridge has not collapsed.  Explain more precisely in
terms of system transitions what the intern means, and briefly, but
clearly, justify her claim.

\solution{The interns means that any sequence of transitions starting from
$(0,0,0)$ will arrive at a state in which no transition is possible, even
though there are no cars on the bridge.  This happens because every time a
car enters and then exits the bridge the value of $A-B$ increases by 2.
So after 1250 cars have entered the bridge, no further car can enter the
bridge because $A-B\geq 2500$; after that, cars can only exit the bridge.
So in exactly 2500 transitions, the system deadlocks with the bridge empty
and no cars allowed on.  In fact, deadlock inevitably occurs starting from
\emph{any} state, unless the bridge collapses first.}

\iffalse

Let $D$ be the derived variable
\[
D \eqdef
\begin{cases}
2500 - A + B + 4C &\text{ if there is a transition from state $(A,B,C)$},\\
0 & \text{otherwise}.
\end{cases}     
Prove that $D$ is a strictly decreasing, natural number-valued variable.
In your proof, you may not assume any of the properties you designated in
part~(\ref{variables}) unless you prove them too.

\solution{
We gave a proof in part~(\ref{variables}) that $(A - 4C - B)$ is strictly
increasing.  Hence , $D = 2500 - A + B + 4C$ is strictly decreasing.  So all
that remains is showing that it is nonnegative.

But there is a transition from $(A,B,C)$ only if $

In part (b), we proved that if the bridge is standing, then it will
never collpse.  Therefore, $C \leq 500$ or $2C \leq 1000$.  Since $A - 2C - B$ 
is strictly increasing by 1 at each transition, $A - 2C - B$
will exceed 2500 after at most $(2500 + 1000 +
|Initial-value(A-2C-B)|)$ number of transitions.

Therefore,  $3500 + |Initial-value(A-2C-B)|-(A-2C-B)$ is nonnegative.

}

\problempart[0]

Prove that the system deadlocks (i.e. the bridge has fewer than 500
cars but no car can enter) regardless of what initial state it takes
(if it doesn't collapse first).

\solution{

The derived variable $D$ is a strictly decreasing integer-valued and
non-negative variable.  Eventually it will reach a minimum where it
can no longer decrease which implies termination.  No transition is
possible and the system deadlocks.

%We define a new derived variable $K-(A-2C-B)$, where K is $2500 +
%1000 + |Initial-value(A-2C-B)|$

%In part (b), we proved that if the bridge is standing, then it will
%never collpse.  Therefore, $C \leq 500$ or $2C \leq 1000$.  Since $A - 2C - B$ 
%is strictly increasing by 1 at each transition, $A - 2C - B$
%will exceed 2500 after at most $(2500 + 1000 +
%|Initial-value(A-2C-B)|) = K$

%Therefore,  $K-(A-2C-B)$ is nonnegative.

%Additionally, since $(A-2C-B)$ is strictly increasing by 1 at each
%transition, $K-(A-2C-B)$ must be strictly decreasing integer-valued.

}
\fi


\instatements{\newpage}


\instatements{\vfill\pagebreak}

\end{problemparts}
\end{problem}

