\documentclass[11pt, twoside]{article}
\usepackage{epsf}

\input{macros-course}

\newcommand{\nand}{|}
\renewcommand{\implies}{\longrightarrow}
\newcommand{\mathify}[1]{\ifmmode{#1}\else\mbox{$#1$}\fi}
\newcommand{\mquote}[1]{\mathify{\textrm{``$#1$''}}}
\newcommand{\mdash}{\mathify{\textrm{-}}}

\askaboutsolutions

\begin{document}
%\handout{ps55}{Problem Set 5.5}{October 10, 2000}
\psol{5.5}{Problem Set 5.5}{October 10, 2000}

\textbf{You do not have to turn in the solutions to this Problem Set.
It is designed to help you study for the first quiz.}

-----------------------------------------------------------------------------\\

\textbf{Reading:}
Lecture notes 8-10.

\medskip
\begin{problems}

\problem
One way to implement a dynamic set, $\ms{DSet}$ is to represent the
set by a finite
sequence of elements.  The $\mathbf{add}$ operation could append the new
element to the end of the sequence \emph{whether or not it already
appears in the sequence}.  The $\mathbf{lookup}$ operation returns the
answer to whether or not any copy of the element is in the sequence.
The $\mathbf{delete}$ operation deletes the element from the sequence at
every place that it occurs.

\ppart
Define a state machine $\ms{Seq}$ corresponding to this
implementation.  In implementing the operations, you should not try to
represent individual search steps that try to locate an element in the
sequence.  Instead, let each operation perform its main computation in
one large-granularity step, which involves the entire sequence. Thus,
this description will still be rather abstract.


\solution{
\medskip
\textbf{Solution:} 

\begin{itemize}
\item 
$Q$: 
The states consist of the components: 
  \begin{itemize}
  \item $\ms{seq}$, \ a sequence (ordered) of elements
  \item $\ms{req} \in \set{\mquote{add}, \mquote{delete}, \mquote{lookup} } \union \set{\ms{null}}$ 
  \item $\ms{resp} \in \set{\mquote{OK}, \ms{null} } \union \ms{Boolean} $
  \end{itemize}
  
\item 
$Q_0$:
Initially, $\ms{seq}$ has no elements, and all the other components are
$\ms{null}$.

\item 
$L$: identical to abstract case.

\item 
$\delta$: Input, output are identical to abstract case.
  \begin{itemize}
  \item[] $\ms{perform}(\ms{add}(x))$ \\
Can occur if: $\ms{req} = \ms{add}(x)$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq} := \ms{seq}$ with $x$ appended on the end \\
$\ms{\;\;\;\;resp} := \mquote{OK}$ 

  \item[] $\ms{perform}(\ms{delete}(x))$ \\
Can occur if $\ms{req} = \ms{delete}(x)$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq} := \ms{seq}$ compressed to not include any elements equal to $x$ \\
$\ms{\;\;\;\;resp} := \mquote{OK}$ 

  \item[] $\ms{perform}(\ms{lookup}(x))$ \\
Can occur if $\ms{req} = \ms{lookup}(x)$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
if $x \in \ms{seq}$ then \\
$\ms{\;\;\;\;resp} := \ms{true}$ \\
else \\
$\ms{\;\;\;\;resp} := \ms{false}$

  \end{itemize}

\end{itemize}

}


\problempart

Prove that your $\ms{Seq}$ state machine implements the $\ms{DSet}$
labeled state machine; that is, prove that any trace of $\ms{Seq}$ is
a trace of $\ms{DSet}$. Remember that a trace is a listing of only the
input and output labels during an execution -- the externally visible
behavior. You may use the Abstraction Theorem.

\solution{
\medskip
\textbf{Solution:} 

We want to show that any trace of $Seq$ is a trace of $DSet$. 
In other words, any execution $\alpha$ of $Seq$ has a corresponding
execution $\beta$ in $DSet$ that produces the same externally visible
(input and output) labels.
\[
trace(\alpha) = trace(\beta)
\]
We show this using the Abstraction Theorem.

We need to come up with a suitable relation and prove that it
indeed is an Abstraction relation.

Define $R = \set{(q,q') | q \in Seq, q' \in DSet, q.req = q'.req,q.resp = q'.resp, unique(q.seq) = q'.set}$

where $unique(s) = \set{set of unique elements in s}$

Now we need to show that $R$ is indeed an abstraction relation. 
The possible transitions of $Seq$ are:
  \begin{itemize}
  \item[] $\ms{request}(\ms{add}(x))$ \\
		Also do a $request(\ms{add}(x))$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
		(By the abstraction relation, we know that the $req$ in
		one execution will be $null$ if and only if it is $null$ in the
		other).
  \item[] $\ms{request}(\ms{delete}(x))$ \\
		Also do a $request(\ms{delete}(x))$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \item[] $\ms{request}(\ms{lookup}(x))$ \\
		Also do a $request(\ms{lookup}(x))$. Nothing changes besides the
		identical alterations, and the labels generated are the same.

  \item[] $\ms{perform}(\ms{add}(x))$ \\
		Do a $perform(\ms{add}(x))$. While $seq$ may now have several
		copies of $x$, this is allowed by our abstraction relation.
		Otherwise, the conditions are maintained.
  \item[] $\ms{perform}(\ms{delete}(x))$ \\
		Do a $perform(\ms{add}(x))$. While $seq$ may have had several
		copies of $x$, all are deleted by the $Seq$ transition.
  \item[] $\ms{perform}(\ms{lookup}(x))$ \\
		Do a $perform(\ms{lookup}(x))$. Will find the same result in
		both $seq$ and $set$, because the abstraction relation says
		that they have the same elements.

  \item[] $\ms{respond}(\mquote{OK})$ \\
		Also do a $return(\mquote{OK})$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \item[] $\ms{respond}(b)$, $b \in Boolean$ \\
		Also do a $return(b)$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \end{itemize}

}

\problempart

Low-level implementation:

Give an implementation called $\ms{SeqLow}$ that relies on lower-level
operations for performing the searches and removals (operate at the
element-level).

\solution{
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item 
$Q$: 
The states consist of the components: 
  \begin{itemize}
  \item $\ms{seq}$, \ a sequence (ordered) of integers $seq_0$ through $seq_n$
  \item $\ms{index} \in \nats$
  \item $\ms{offset} \in \nats$
  \item $\ms{maxindex} \in \nats$
  \item $\ms{req} \in \set{\mquote{add}, \mquote{delete}, \mquote{lookup} } \union \set{\ms{null}}$ 
  \item $\ms{resp} \in \set{\mquote{OK}, \ms{null} } \union \ms{Boolean} $
  \end{itemize}
  
\item 
$Q_0$:
Initially, $\ms{seq}$ has no elements, $index = 0$, $maxindex = 0$, $offset = 0$,
and all the other components are $\ms{null}$.

\item 
$L$: Input, output identical to abstract case.
  \begin{itemize}
  \item[] Internal labels:
    \begin{itemize}
    \item[] $\ms{perform}(\ms{add}(x))$, \ \ $x \in \ints$
    \item[] $\ms{perform}(\ms{delete}(x))$, \ \ $x \in \ints$
    \item[] $\ms{perform}(\ms{lookup}(x))$, \ \ $x \in \ints$
    \end{itemize}
  \end{itemize}

\item 
$\delta$: Input, output are identical to abstract case.
  \begin{itemize}
  \item[] $\ms{perform}(\ms{add}(x))$ \\
Can occur if $\ms{req} = \mquote{add}$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq_{maxindex}} := x$ \\
$\ms{\;\;\;\;maxindex} := maxindex + 1 $ \\
$\ms{\;\;\;\;resp} := \mquote{OK}$

  \item[] $\ms{perform}(\ms{delete}(x))$ \\
Can occur if $\ms{req} = \mquote{delete}$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
if $index = maxindex$ then \\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;offset} := 0$ \\
$\ms{\;\;\;\;maxindex} := maxindex - offset$ \\
$\ms{\;\;\;\;resp} := \mquote{OK}$ \\
else if $seq_{index} = x$ then\\
$\ms{\;\;\;\;index} := index + 1$ \\
$\ms{\;\;\;\;offset} := offset + 1$ \\
else \\
$\ms{\;\;\;\;seq_{index - offset}} := seq_{index}$ \\
$\ms{\;\;\;\;index} := index + 1$ 

  \item[] $\ms{perform}(\ms{lookup}(x))$ \\
Can occur if $\ms{req} = \mquote{lookup}$ and
$\ms{resp} = \ms{null}$ \\
%Effect: \\
if $index = maxindex$ then \\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;resp} := \ms{false}$ \\
else if $seq_{index} = x$ then\\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;resp} := \ms{true}$ \\
else \\
$\ms{\;\;\;\;index} := index + 1$

  \end{itemize}

\end{itemize}

}

\problempart

Give an informal argument that $\ms{SeqLow}$ implements $\ms{Seq}$.

\solution{
  \medskip
  \textbf{Solution:} 

We must show that every sequence of $SeqLow$ is a sequence of $Seq$.
Informally, we can argue that for any execution $A$ of $SeqLow$ that 
has the same trace as an execution $B$ of $Seq$, every transition from
$A$ can be matched by some sequence of transitions from $B$. 

Again, the abstraction relation is similar to what we did earlier.
Since the exact sequence keeps changing in $SeqLow$ when we do 
a delete operation, we cannot just say that two states are related if
they have the same sequence. But we can use the same idea as before and
say that two states are related if their sequences have the same
unique elements (of course, their $req$ and $resp$ values must be 
the same too).

Input and output transitions are exactly matched. 

  \begin{itemize}
  \item[] $\ms{perform}(\ms{add}(x))$ \\
  		Also do a $\ms{perform}(\ms{add}(x))$. Will add the element to the
  		end in both cases.
  \item[] $\ms{perform}(\ms{delete}(x))$ \\
if $seq_index$ was the last occurence of $x$ or $index = maxindex$ then \\
  		Also do a $\ms{perform}(\ms{delete}(x))$. In both cases, all elements
  		that match $x$ are gone from the sequence, and the sequences of the resulting states are the same,\\
else 
		Do nothing. No observable changes; just stepping through details.
		
  \item[] $\ms{perform}(\ms{lookup}(x))$ \\
if $index = maxindex$ then \\
  		Also do a $\ms{perform}(\ms{lookup}(x))$. Will return the same value,
  		since we now know that $x$ is not equal to any $seq_{i}$ where
  		$i < maxindex$. \\
else if $seq_{index} = x$ then\\
  		Also do a $perform(\ms{lookup}(x))$. Will return the same value,
  		since we know that $x$ is equal to some $seq_{i}$ (namely,
  		$i = index$).\\
else \\
		Do nothing. No observable changes; just stepping through details.
  \end{itemize}
}



\problem Consider an ``abstract object'' that maintains a dynamic
polynomial $\ms{poly}$.  This polynomial has variable $x$, and integer
coefficients.  Initially, the polynomial is just the $0$ polynomial
(no terms).  The polynomial supports operations:
\begin{itemize}
\item $\mathbf{add\mdash term}(c,e)$, which adds the term $c x^e$
  to the maintained polynomial.
\item $\mathbf{coeff}(e)$, which asks for the coefficient of the $x^e$
  term.
\end{itemize}

\begin{problemparts}

  \problempart Model this object by a labeled state machine $\ms{ADP}$.
  The state should keep track of the polynomial (a value that is
  simply a mathematical polynomial -- you don't have to think about
  how to represent it using lower-level mathematical objects like
  numbers, matrices, sequences, etc.)  The state will also need some
  bookkeeping information to keep track of operations in progress.
  The labels should include inputs reflecting the requests and outputs
  reflecting the responses.  Your machine should ignore requests that
  arrive while an operation is active.

\solution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item $Q$: \\
 $ p \in \set{polynomials} $

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$\;\; \set{(0, null, null, null)} $

or, equivalently,

$\;\; p = 0$, $req = null$, $power = null$, $mult = null$

\item $L$:
    \begin{itemize}
    \item[] Input labels:
    	\begin{itemize}
    	\item[] $req\mdash add\mdash term(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $req\mdash coeff(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \item[] Output labels:
    	\begin{itemize}
    	\item[] $return(\mquote{OK})$
    	\item[] $return(c)$, \ \ $c \in \ints$
    	\end{itemize}
    \end{itemize}

\item $\delta$: \\
	Each is associated with (generates) the label of its namesake.
    \begin{enumerate}
    \item $req\mdash add\mdash term(c,e)$:  \\
    	Can occur anytime. \\
        if $req = null$ then \\
        $~\;\;\;\; req := \mquote{add}$ \\
        $~\;\;\;\; power := e$ \\
        $~\;\;\;\; mult := c$
    \item $req\mdash coeff(e)$:  \\
    	Can occur anytime. \\
        if $req = null$ then \\
        $~\;\;\;\; req := \mquote{find\mdash coeff}$ \\
        $~\;\;\;\; power := e$ \\
        $~\;\;\;\; mult := null$
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$. \\
        $~\;\;\;\; p := p + c \cdot x^e$ \\
        $~\;\;\;\; req := \mquote{OK}$
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$ and $power = e$. \\
        $~\;\;\;\; req := \textrm{coefficient of $x^e$ in $p$}$
    \item $return(\mquote{OK})$:  \\
    	Can occur if $req = \mquote{OK}$. \\
        $~\;\;\;\; req, power, mult := null$
    \item $return(c)$:  \\
    	Can occur if $req = c$. \\
        $~\;\;\;\; req, power, mult := null$
    \end{enumerate}

\end{itemize}


%\end{solution}
}

  \problempart List some (4--5) traces that are exhibited by your state
  machine $\ms{ADP}$.  Include at least one that involves a request arriving
  when it is not supposed to.

\solution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
%perhaps put explanations in on right?
req\mdash add\mdash term(1,1) & \\
return(\mquote{OK})  & \\
req\mdash add\mdash term(2,2) & \\
return(\mquote{OK})  & \\
req\mdash coeff(2)      & \\
return(2)  & \\
req\mdash add\mdash term(2,1) & \\
return(\mquote{OK})  & \\
req\mdash coeff(1)      & \\ 
return(3)  & \\
\end{array}
\]

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
req\mdash add\mdash term(1,1)  & \\
return(\mquote{OK})  & \\
req\mdash add\mdash term(2,2) & \\
req\mdash coeff(2)  & \\
return(\mquote{OK})  & \\
req\mdash coeff(2)  & \\
req\mdash add\mdash term(3,2)  & \\
return(2)  & \\
req\mdash coeff(2)  & \\
return(2)  & \\
\end{array}
\]

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
req\mdash add\mdash term(4,2) & \\
req\mdash add\mdash term(7,1)  & \\
return(\mquote{OK})  & \\
req\mdash coeff(3)  & \\
req\mdash coeff(2)  & \\
return(0)  & \\
req\mdash coeff(1)  & \\
return(0)  & \\
req\mdash coeff(2)  & \\
return(4)  & \\
\end{array}
\]

Of course, there are many more traces. The important thing about this
system is that requests will be dropped if there is still a pending
request that has not generated a $return$ -- the value of $req$ will
not be $null$ when they come in.

%\end{solution}
}

  \problempart Describe in words an implementation of your state
  machine $\ms{ADP}$.  The state of this implementation should involve
  lower-level mathematical objects like numbers, matrices, sequences,
  etc.

\solution{
%\begin{solution}

% I do not really know what is adequate here!

  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] Keep an array $poly$ such that the $i$th entry holds the
coefficient of $x^i$ in $p$. The array size will have to grow as necessary,
or there will be a limit on the terms of the polynomial. 
$comp\mdash add\mdash term(c,e)$ will simply be $poly[e] := poly[e] + c$.
$comp\mdash coeff(e)$ will be $req := poly[e]$.

\item[Using Ordered Pairs: ] Keep a set $terms$ of ordered pairs $(i, c)$ 
mapping the $i$th entry to the coefficient of $x^i$ in $p$.
$comp\mdash add\mdash term(c,e)$ will be more complex, unless we just add
the pair and sum all pairs with like first components on lookup. We will 
have to search through for an existing pair with a matching first component.
This will require more internal state. $comp\mdash coeff(e)$ will be a
similar search for the right pair, returning $0$ if none is found.

\end{description}

%\end{solution}
}

  \problempart Formalize your implementation as a labeled state
  machine $\ms{Imp}$.  It should have the same external labels as your
  labeled state machine $\ms{ADP}$.

\solution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] Assume that we ignore the bounds of the array.

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
For all (many) $i \in \nats$,  \\
$~\;\;\; poly[i] \in \ints $

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$poly[i] = 0 \textrm{for all $i$}$, $req = null$, $power = null$, $mult = null$

\item $L$: Same as before.

\item $\delta$: Same as before for input and output. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$. \\
        $~\;\;\;\; poly[e] := poly[e] + c$ \\
        $~\;\;\;\; req := \mquote{OK}$
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$ and $power = e$. \\
        $~\;\;\;\; req := poly[e]$
    \end{itemize}
\end{itemize}


\item[Using Unique Ordered Pairs: ]

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
A linked list $terms$ of the form $(i, m, next)$
with $i \in \nats$, $m \in \ints$, $next \in terms \union \set{null}$.

$firstterm \in terms$

$curterm \in terms \union \set{null}$

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$firstterm = (0, 0, null)$, $curterm = firstterm$,  $terms = \set{firstterm}$,
$req = null$, $power = null$, $mult = null$

\item $L$: Same as before for input and output labels.
    \begin{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash sum\mdash next(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash sum \mdash default(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash next(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash default(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \end{itemize}

\item $\delta$:  Input, output transitions same as before. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm \neq null$, $curterm.i = e$ \\    	
        $~\;\;\;\; curterm.m := curterm.m + c$ \\
        $~\;\;\;\; req := \mquote{OK}$ \\
        $~\;\;\;\; curterm := firstterm$
    \item $comp\mdash sum \mdash next(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm \neq null$, $curterm.i \neq e$ \\    	
        $~\;\;\;\; curterm := curterm.next $ 
    \item $comp\mdash sum \mdash default(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm = null$ \\
        $~\;\;\;\; firstterm := (e, c, firstterm) $ \\
        $~\;\;\;\; req := \mquote{OK} $ \\
        $~\;\;\;\; curterm := firstterm$

    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, $curterm.i = e$ \\
        $~\;\;\;\; req := curterm.m$ \\
        $~\;\;\;\; curterm := firstterm$
    \item $comp\mdash coeff \mdash next(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, $curterm.i \neq e$ \\    	
        $~\;\;\;\; curterm := curterm.next $ 
    \item $comp\mdash coeff \mdash default(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm = null$ \\    	
        $~\;\;\;\; req := 0$ \\
        $~\;\;\;\; curterm := firstterm$

%    \item $return(\mquote{OK})$:  \\
%    	Can occur if $req = \mquote{OK}$. \\
%        $~\;\;\;\; req, power, mult := null$ 
%    \item $return(c)$:  \\
%    	Can occur if $req = c$. \\
%        $~\;\;\;\; req, power, mult := null$
    \end{itemize}
\end{itemize}

Note that we implicitly added a new term to $terms$ every time we
expanded the linked list.

\item[Using Multiple Ordered Pairs: ]

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
A linked list $terms$ of the form $(i, m, next)$
with $i \in \nats$, $m \in \ints$, $next \in terms \union \set{null}$.

$firstterm \in terms$

$curterm \in terms \union \set{null}$

$total \in \ints$

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$firstterm = (0, 0, null)$, $curterm = firstterm$,  $terms = \set{firstterm}$,
$total = 0$,
$req = null$, $power = null$, $mult = null$

\item $L$: Same as before for input and output labels.
    \begin{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash next(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash end(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \end{itemize}

\item $\delta$:  Input, output transitions same as before. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$ \\
        $~\;\;\;\; firstterm := (e, c, curterm)$ \\
        $~\;\;\;\; req := \mquote{OK}$ 
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, and $curterm.i = e$ \\
        $~\;\;\;\; total := total + curterm.m$ \\
        $~\;\;\;\; curterm := curterm.next $
    \item $comp\mdash coeff \mdash next(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, and $curterm.i \neq e$ \\
        $~\;\;\;\; curterm := curterm.next $
    \item $comp\mdash coeff \mdash end(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	and $curterm = null$ \\
        $~\;\;\;\; req := total$ \\
        $~\;\;\;\; curterm := firstterm$ \\
        $~\;\;\;\; total := 0$
%    \item $return(\mquote{OK})$:  \\
%    	Can occur if $req = \mquote{OK}$. \\
%        $~\;\;\;\; req, power, mult := null$
%    \item $return(c)$:  \\
%    	Can occur if $req = c$. \\
%        $~\;\;\;\; req, power, mult := null$
    \end{itemize}
\end{itemize}

\end{description}

%\end{solution}
}

  \problempart Argue that your implementation $\ms{Imp}$ is correct,
  in the sense that every trace of $\ms{Imp}$ is also a trace of
  $\ms{ADP}$.

\solution{
%\begin{solution}

  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] This is the easiest.

	The abstraction relation is obvious: All corresponding elements
have the same values and for every term $cx^i$ in $p$, $poly[i] = c$.
Only the  differing transitions are nontrivial to examine.
(Otherwise, the executions are identical and the abstraction relation
is clearly preserved). However, even $comp\mdash sum$ and 
$comp\mdash coeff$ are easily accounted for: if an execution of
$Imp$ is extended by either, extend an execution of $ADP$ with the
same trace using the same transition. $comp\mdash sum$ preserves the
abstraction relation by performing matching arithmetic.
$comp\mdash coeff$ preserves the abstraction relation because $p$
and $poly$ are in correspondence and will set $req$ to the same value.

\item[Using Unique Pairs: ] Somewhat tricky to do formally.

	The abstraction relation is: elements of the same name have the 
same values; every non-zero term in $p$ has exactly one corresponding
triplet in $terms$, and every zero-coefficient term in $p$ either has
no corresponding triplet or has a triplet with a second component of
$0$.

We need other elements of an invariant:
In $Imp$, $firstterm$ begins a linked list that reaches all terms in $terms$;
there are no terms with $i = mult$ `between' $firstterm$ and
$curterm$; no two terms have the same $i$ component; if $req$ is not
\mquote{find\mdash coeff} or \mquote{add\mdash term} 
then $curterm = firstterm$.

Input and output transitions have a simple identity correspondence.
Roughly, if the last transition of the partial execution of $Imp$ is:
\begin{itemize}
   	\item[] $\mathbf{comp\mdash sum(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. Both set $req$ to
   		\mquote{OK}; the assignments keep the polynomial structures 
   		aligned. (We use the fact that the IH tells us that no other 
   		element of $terms$ represents the same exponent here). Although
   		$req$ is changed, $curterm$ is set to $firstterm$. Nothing
   		else is changed.
   	\item[] $\mathbf{comp\mdash sum\mdash next(c,e)}$ \\
   		do nothing. No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash sum \mdash default(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. If there are no
   		terms after $curterm$, and no terms with $i = mult$ between
   		$firstterm$ and $curterm$, then there must be no terms at all
   		with $i = mult$. So adding in the new term did not violate
   		uniqueness. The new $firstterm$ is connected to all of the
   		elements of $terms$ because the old $firstterm$ was.
   	\item[] $\mathbf{comp\mdash coeff(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. Must be the correct
   		coefficient because $p$ and $terms$ are in correspondence and
   		no two terms have the same $i$ component.
   	\item[] $\mathbf{comp\mdash coeff \mdash next(e)}$ \\
		do nothing.  No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash coeff \mdash default(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. If there are no
   		terms after $curterm$, and no terms with $i = mult$ between
   		$firstterm$ and $curterm$, then there must be no terms at all
   		with $i = mult$. By the correspondence between $p$ and $terms$,
   		the coefficient must be $0$ in both $ADP$ and $Imp$.
\end{itemize}

Although the steps are not filled in, the above is a basic reasoning
that traces of $Imp$ can be matched by traces of $ADP$.

\item[Using Multiple Pairs: ] Slightly trickier to do formally.

	The abstraction relation is: elements of the same name have the 
same values; every term in $p$ has a coefficient equal to the sum of
$m$ in all triplets $(i, m, next)$ in $terms$ with $i$ equal to that
coefficient.

We need other elements of an invariant:
In $Imp$, $firstterm$ begins a linked list that reaches all terms in $terms$;
$total$ is the sum of $m$ in all triplets $(i, m, next)$ between 
$firstterm$ and $curterm$; if $req$ is not
\mquote{find\mdash coeff} then $curterm = firstterm$.

Input and output transitions have a simple identity correspondence.
Roughly, if the last transition of the partial execution of $Imp$ is:
\begin{itemize}
   	\item[] $\mathbf{comp\mdash sum(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. Both set $req$ to
   		\mquote{OK}. The assignments keep the polynomial structures 
   		aligned by adding in the new coefficient.
   		The new $firstterm$ is connected to all of the
   		elements of $terms$ because the old $firstterm$ was.
   		Nothing else is changed.
   	\item[] $\mathbf{comp\mdash coeff(e)}$ \\
		do nothing. $total$ is appropriately increased, since $curterm$
		is advanced beyond the term that is contributing.
   	\item[] $\mathbf{comp\mdash coeff \mdash next(e)}$ \\
		do nothing.  No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash coeff \mdash end(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. If there are no
   		terms after $curterm$, then all terms with $i = mult$ are between
   		$firstterm$ and $curterm$. Thus, $total$ must be the proper
   		coefficient of term $e$. Since $p$ and $terms$ are in correspondence,
   		$Imp$ and $ADP$ will update $req$ to the same value.
\end{itemize}

\end{description}
	
%\end{solution}
}

\end{problemparts}

\problem
Prove the Abstraction Theorem:\\
\hspace*{0.85in} A implements B {\bf iff} there is an abstraction relation from A to B

\solution{
  \medskip
  \textbf{Solution:} 

($\Leftarrow$) 
(By induction)

\begin{proof}
Assume R is an abstraction relation from A to B.

Given an arbitrary execution $a$ of A, construct a corresponding execution $b$
for B inductively as follows:

For B's start state, pick a start state that's related to A's start state, ie,
pick $q^{b}_0$ such that \\
($q^{a}_0$,$q^{b}_0$) $\in$ R.

For each successive transition in A's execution, $q_a \rightarrow {q_a}'$, 
replace it by a (possibly empty) sequence of transitions $q_b \leadsto {q_b}'$ 
such that (${q_a}',{q_b}'$) $\in$ R. This is guaranteed since R is an 
abstraction relation.

Now it's straightforward to prove that the traces of the two executions are the same. 

Let P(n): The traces of the n-length prefix of A's execution and the {\em corresponding} part
of B's execution are the same.

P(0) is trivially true.

P(n-1) and the fact that the sequence of B's execution corresponding to the $n^{th}$
transition of A has the same trace implies P(n).

Since this is true for any execution of A it follows that A implements B.
\end{proof}

($\Rightarrow$)
(By contradiction)
\begin{proof}
Assume there exists {\bf no} abstraction relation from A to B.

In particular, R = A x B is also not an abstraction relation.

This implies that $\exists q_a, q_b, l$ such that $q_a \stackrel{l}{\rightarrow} {q_a}'$ and \\
$\forall s$($q_b \stackrel{s}{\leadsto} {q_b}' \Rightarrow$ Trace(s) $\not=$ Trace(l)).

Now we intend to show an execution of A whose trace is different from any execution of B's.

Consider an execution of A that ends in $q_a$ such that the only execution of B that matches
its trace ends in $q_b$ (If this is not possible, we have two cases. Either no execution of
B can match A's trace, in which case we are done. Or B's executions always end in states
other than $q_b$ in which case there's no need for $q_a$ and $q_b$ to be related to each 
other and we can start the arguement all over again with R - {($q_a$,$q_b$)}).

Now we extend A's execution with the transition $l$. From our choice of $q_a$ and
$q_b$ it's obvious that B cannot match the trace of this transition. 

Thus, we now have an execution of A whose trace is different from any execution of B.

Hence, A does not implement B.
\end{proof}
}


\problem
Seeing how annoyingly slow the Student Center elevator is, the MIT
Administration has decided to give you, the students in 6.042,
the job of designing the elevator system for
the new LCS building. Your first task is to specify the behavior of
the elevator at an abstract level. 

\ppart

Assume you have $n$ floors. \\
The inputs to the elevator controller are
of three types: 
\begin{itemize}
\item $\ms{up(i)}$ (Person on $i^{th}$ floor wants to go up)
\item $\ms{down(i)}$ (Person on $i^{th}$ floor wants to go down)
\item $\ms{press(i)}$ (Person inside the elevator wants to go to the $i^{th}$ floor)
\end{itemize}

The controller has two outputs:
\begin{itemize}
\item $\ms{open}$ (The elevator door opens at current floor)
\item $\ms{close}$ (The elevator door closes at current floor)
\end{itemize}

The controller also has two internal transitions:
\begin{itemize}
\item $\ms{goUp}$ (Causes the elevator to go up one floor)
\item $\ms{goDown}$ (Causes the elevator to go down one floor)
\end{itemize}

The internal state consists of:
\begin{itemize}
\item $\ms{floor}$ (The floor that the elevator is currently on)
\item $\ms{requests}$  (The set of all pending floor numbers)
\item $\ms{isClosed}$ (Yes, if door is closed, No otherwise)
\end{itemize}

Specify the basic behavior that you'd expect from this elevator 
controller (there is no unique solution; come up with something
that you feel is reasonable).

\solution{
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item
$Q$: The states consist of the components $\ms{floor}$, $\ms{requests}$ and
$\ms{isClosed}$

\item
$Q_0$: $\ms{floor} = 1$ and $\ms{requests} = \emptyset$ and $\ms{isClosed} = Yes$

\item 
$L$:
 \begin{itemize}
 \item[] Input labels:
	\begin{itemize}
	\item[] $\ms{up(i)}, \ms{down(i)}, \ms{press(i)}$
	\end{itemize}
 \item[] Internal labels:
        \begin{itemize}
        \item[] $\ms{goUp}, \ms{goDown}$  
        \end{itemize}
 \item[] Output labels:
	\begin{itemize}
	\item[] $\ms{open}, \ms{close}$
	\end{itemize}
 \end{itemize}

\item
$\delta$: \\
 Each transition is associated with the label of its namesake.
 \begin{enumerate}
 \item $\ms{up(i)}$, $\ms{down(i)}$, $\ms{press(i)}$: \\
	Can occur anytime. \\ 
	if $\ms{floor} \not= i$ or $\ms{isClosed} = Yes$ then \\
	$~\;\;\;\; \ms{requests} := \ms{requests}\; \cup $ \{i\} 
 \item $\ms{goUp}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\exists i \in \ms{requests} \left(i>\ms{floor}\right)$. \\ 
        $\ms{floor}$ := $\ms{floor}$ + 1;
 \item $\ms{goDown}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\exists i \in \ms{requests} \left(i<\ms{floor}\right)$. \\
        $\ms{floor}$ := $\ms{floor}$ - 1;
 \item $\ms{open}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\exists i \in \ms{requests} \left(i=\ms{floor}\right)$. \\
        $\ms{isClosed}$ := No; \\
        $\ms{requests}$ := $\ms{requests}$ - \{i\};
 \item $\ms{close}$: \\
        Can occur if $\ms{isClosed}$ = No \\
        $\ms{isClosed}$ := Yes;
 \end{enumerate}

\end{itemize}

Note that this description is non-deterministic. 

}

\ppart
You must have noticed that the behavior (transitions) of the elevator
depends on the service policy. Specify the behavior when the elevator
follows a greedy policy (ie, the elevator services the request closest
to its current position)

\solution{
  \medskip
  \textbf{Solution:} 

Only the $\ms{goUp}$ and $\ms{goDown}$ transitions are modified.

\begin{enumerate}
 \item $\ms{goUp}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\exists i \in \ms{requests} \left(i>\ms{floor} \wedge |i-\ms{floor}|\; is \;minimum\right)$. \\
        $\ms{floor}$ := $\ms{floor}$ + 1 ;
 \item $\ms{goDown}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\exists i \in \ms{requests} \left(i<\ms{floor} \wedge |\ms{floor}-i|\; is \;minimum\right)$. \\
        $\ms{floor}$ := $\ms{floor}$ - 1;
\end{enumerate}

}

\ppart
This policy might be lead to {\em starvation} of certain requests (as is
common at the Student Center). Show a 
trace where a request might be denied service for an arbitrary long 
period of time.

\solution{
  \medskip
  \textbf{Solution:} 

Here's the trace of a scenario where a person on the $n^{th}$ floor 
wants to come down but is frustrated by a guy who keeps hopping between
the $1^{st}$ and $2^{nd}$ floors.

$\ms{down(n)},\ms{up(1)},\ms{open},\ms{close},\ms{press(2)},\ms{open},
\ms{close},\ms{press(1)},\ms{open},\ms{close},\ms{press(2)}$ \ldots

} 

\ppart
Let's modify the service policy to take care of this problem. The elevator
will keep going in one direction till it has serviced all requests for that
direction. Then it reverses direction and keeps going the other way. Specify
the behavior of the elevator under this policy. Argue its correctness.

(Hint: In order to implement this policy, you'll need to add additional 
variables to the state. In particular, you'll have to keep track of the
current direction of the elevator. It might also be helpful to split the
set of requests into an {\em up} set and a {\em down} set)

\solution{
  \medskip
  \textbf{Solution:} 
\begin{itemize}
\item
$Q$: The states now consist of the components $\ms{floor}$, $\ms{upRequests}$,
$\ms{downRequests}$,$\ms{isClosed}$ and $\ms{dir}$

\item
$Q_0$: $\ms{floor} = 1$, $\ms{upRequests},\ms{downRequests} = \emptyset$, $\ms{isClosed} = Yes$, $\ms{dir} = Up$

\item 
$L$: \\
 Same as before with the following additional internal transition:
 \begin{itemize}
 \item[] $\ms{reverseDir}$ (for switching directions of the elevator)
 \end{itemize}

\item
$\delta$: 
 \begin{enumerate}
 \item $\ms{up(i)}$: \\
	Can occur anytime. \\ 
	if $\ms{floor} \not= i$ or $\ms{isClosed} = Yes$ then \\
	$~\;\;\;\; \ms{upRequests} := \ms{upRequests}\; \cup $ \{i\} 
 \item $\ms{down(i)}$: \\
	Can occur anytime. \\ 
	if $\ms{floor} \not= i$ or $\ms{isClosed} = Yes$ then \\
	$~\;\;\;\; \ms{downRequests} := \ms{downRequests}\; \cup $ \{i\} 
 \item $\ms{press(i)}$: \\
	Can occur anytime. \\ 
	if $\ms{floor} \not= i$ or $\ms{isClosed} = Yes$ then \\
        $~\;\;$ if i $\ge \ms{floor}$ then \\
	$~\;\;\;\; \ms{upRequests} := \ms{upRequests}\; \cup $ \{i\} \\
        $~\;\;$ else \\
	$~\;\;\;\; \ms{downRequests} := \ms{downRequests}\; \cup $ \{i\} \\
 \item $\ms{goUp}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\ms{dir}$ = Up and $\ms{upRequests} \not= \emptyset$
        $\ms{floor}$ := $\ms{floor}$ + 1;
 \item $\ms{goDown}$: \\
        Can occur if $\ms{isClosed}$ = Yes and $\ms{dir}$ = Down and $\ms{downRequests} \not= \emptyset$
        $\ms{floor}$ := $\ms{floor}$ - 1;
 \item $\ms{reverseDir}$: \\
        Can occur if ($\ms{dir}$ = Up and $\ms{upRequests} = \emptyset$) or ($\ms{dir}$ = Down and $\ms{downRequests} = \emptyset$)
        $\ms{dir} := opposite(\ms{dir})$;
 \item $\ms{open}$: \\
        Can occur if $\ms{isClosed}$ = Yes and ($\ms{condition1}$ or $\ms{condition2}$) \\
        where $\ms{condition1}$ = ($\ms{dir}$ = Up and $\exists i \in \ms{upRequests} \left(i=\ms{floor}\right)$) \\
        and $\ms{condition2}$ =  ($\ms{dir}$ = Down and $\exists i \in \ms{downRequests} \left(i=\ms{floor}\right)$) \\
        $\ms{isClosed}$ := No; \\
        if $\ms{condition1}$ then \\
        $~\;\;\;\; \ms{upRequests} := \ms{upRequests}$ - \{i\}; \\
        else \\
        $~\;\;\;\; \ms{downRequests} := \ms{downRequests}$ - \{i\}; \\
 \item $\ms{close}$: \\
        Can occur if $\ms{isClosed}$ = No \\
        $\ms{isClosed}$ := Yes;
 \end{enumerate}

\end{itemize}

Incidentally, this strategy is commonly used in different applications
such as disk scheduling where it goes under the not so surprising name
of the {\em elevator algorithm} !

}
\end{problems}
\end{document}

















