\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}

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

\medskip
\begin{problems}

\problem

Consider the following description of a	state machine $\ms{A}$.

\begin{itemize}
\item
$Q$: The set of tuples consisting of: 
\begin{tabbing}
XXX\=XXX\=XXX\= \kill
\> $M$, a multiset of integers \\
\> $\ms{request}$, either $\ms{insert}$(x) or $\ms{get}$ \\
\> $\ms{response}$, either $\ms{null}$ or $\ms{OK}$ or $x$ or $\ms{error}$
\end{tabbing}

\item
$Q_0$: $M$ = $\emptyset$, $\ms{request} = $\ms{null}$, $\ms{response} = $\ms{null}$

\item
$L$: 
\begin{tabbing}
XXX\=XXX\=XXX\= \kill
\> Input transitions: $\ms{Insert(x)}$, $\ms{Get}$ \\
\> Internal transitions: $\ms{Perform\mdash insert}$, $\ms{Perform\mdash get}$\\
\> Output transitions: $\ms{Respond(r)}$
\end{tabbing}

\item
$\delta$:
 \begin{itemize}
 \item $\ms{Insert(x)}$: 
 \begin{tabbing}
 XXX\=XXX\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{null}$ \\
\>        Effect: $\ms{request}$ := $\ms{insert(x)}$
 \end{tabbing}

 \item $\ms{Get}$: 
 \begin{tabbing}
 XXX\=XXX\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{null}$ \\
\>        Effect: $\ms{request}$ := $\ms{get}$ 
 \end{tabbing}

 \item $\ms{Perform\mdash insert}$: 
 \begin{tabbing}
 XXX\=XXX\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{insert(x)}$ \\
\>        Effect: add $x$ to the multiset $M$, $\ms{response} := $\ms{OK} 
 \end{tabbing}

 \item $\ms{Perform\mdash get}$: 
 \begin{tabbing}
 XXX\=XXXXl\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{get}$ \\
\>        Effect: if $M$ is not empty \\
\>\>\>                  remove any element $x$ nondeterministically from M \\
\>\>\>                  $\ms{response}$ := $x$ \\
\>\>              else \\
\>\>\>                  $\ms{response}$ := $error$    
 \end{tabbing}

 \item $\ms{Respond(r)}$: 
 \begin{tabbing}
 XXX\=XXX\=XXX\= \kill
\>        Can occur if: $\ms{response} = r, r \not= \ms{null}$ \\
\>        Effect:  $\ms{response}$ := $\ms{null}$, $\ms{request}$ :=  $\ms{null}$
 \end{tabbing}
\end{itemize}
\end{itemize}


Now consider another machine $\ms{B}$ which differs from $\ms{A}$ only in 
its state and the $\ms{Perform}$ transitions.


\begin{itemize}
\item
$Q$: The set of tuples consisting of: 
\begin{tabbing}
XXX\=XXX\=XXX\= \kill
\> $S$, a sequence of integers \\
\> $\ms{request}$, either $\ms{insert}$(x) or $\ms{get}$ \\
\> $\ms{response}$, either $\ms{null}$ or $\ms{OK}$ or $x$ or $\ms{error}$
\end{tabbing}

\item
$\delta$:
 \begin{itemize}
 \item $\ms{Perform\mdash insert}$: 
 \begin{tabbing}
 XXX\=XXX\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{insert(x)}$ \\
\>        Effect: $S$ := $xS$ where $xS$ denotes the concatentation of $x$ and $S$ \\
\>\>              $\ms{response} := $\ms{OK} 
 \end{tabbing}

 \item $\ms{Perform\mdash get}$: 
 \begin{tabbing}
 XXX\=XXXXl\=XXX\= \kill
\>        Can occur if: $\ms{request} = \ms{get}$ \\
\>        Effect: if $S$ = $xS'$  \\
\>\>\>                  $S$ := $S'$ \\
\>\>\>                  $\ms{response}$ := $x$ \\
\>\>                 else \\
\>\>\>                  $\ms{response}$ := $error$    
 \end{tabbing}

 \end{itemize}
\end{itemize}


Answer the following questions based on the above descriptions of $\ms{A}$ and
$\ms{B}$. If your answer is yes, give an abstraction relation. If no, 
give a sample trace to justify your answer.

\ppart

Does $\ms{A}$ implement $\ms{B}$ ?

\solution{
 \medskip
 \textbf{Solution:}

No. 
Consider the following trace of $\ms{A}$'s execution.

$\ms{Insert(1)}, \ms{Respond(OK)}, \ms{Insert(2)}, \ms{Respond(OK)}, \ms{Get},
\ms{Respond(1)}$.

There's no possible execution of $\ms{B}$ that can match this trace.
}

\medskip

\ppart

Does $\ms{B}$ implement $\ms{A}$ ?

\solution{
 \medskip
 \textbf{Solution:}

Yes. 
The following is an abstraction relation from $\ms{B}$ to $\ms{A}$.

$R = \{(q_a,q_b) | q_a.request = q_b.request, q_a.response = q_b.response,
equal(q_a.M,q_b.S)\}$\\

where $M$ snd $S$ are $equal$ if they have the same number of copies of each
 distinct umber.

This problem shows why a stack ($B$) can implement a bag ($A$) but not
vice-versa.
}

\medskip

\end{problems}
\end{document}

















