\documentstyle[epsf]{article}

\input{./handout}

\begin{document}

\homework{5}{27 September 1995}{State Machines}{}

\problem{1} 
\vspace{.2in}

\noindent A. Model the M\&M dispenser on the third floor of Wean Hall.  Write a
4-tuple description and draw out a state transition diagram.

Intuitively, you, the hungry customer, are the ``environment'' of this
machine.  The dispenser is the ``system''.  Remember you are modeling
the dispenser and its interactions with the customer.  You don't have
to model the customer.

So, your set of actions should include {\em putting in a coin}, which
changes the state of the machine, and {\em turning the knob}, which has an
effect on the environment (dispensing M\&M's!) and changes the state
of the machine.

According to your state machine description:
\begin{enumerate}
\item What happens if you try to put in a penny or a quarter?

\item What happens if there are no M\&M's left in the jar?

\item What happens if no more coins can fit in the dispenser?

\item What happens if you run out of dimes?

\item Is it possible for you to get anything but M\&M's?
\end{enumerate}
For each of the above questions, what in the state machine description
tells you the answer precisely?
Notice, your answer to any of these questions could be ``I don't know'';
if this is the case, again say what
in the state machine description says why that's the answer.

\vspace{.2in}
\noindent B. Now consider the
the M\&M machine in the Moose.
\begin{enumerate}
\item Does your state machine description
of the machine change?  If so, how?  If not, why not?

\item
Do your answers to any of the four questions in Part A change?
If so, how and why?  If not, why not?

\item Would you answers to (1) and (2) change if you modeled the
customer
as part of the system?  If so, how and why?  If not, why not?
\end{enumerate}

\newpage
\problem{2}

\vspace{.2in}
\noindent The following problem description, very slightly modified, is sometimes referred
to as ``Kemmerer's library problem.''

\begin{verse}
Consider a small library system
with the following actions:
\begin{enumerate}
\item Check out a copy of a book.  Return a copy of a book.

\item Add a copy of a book to the library.  Remove a copy of a book
from the library.

\item Get the list of books by a particular author or in a particular
subject area.

\item Find out the list of books currently checked out by a particular
borrower.

\item Find out what borrower last checked out a particular copy of a
book.
\end{enumerate}

There are two types of users: staff users and ordinary borrowers.
Actions listed in 2, 4, and 5 are restricted to staff users, except
that ordinary borrowers can perform action 4 to find out the list
of books currently borrowed by themselves.

The library system must satisfy the following invariants:
\begin{enumerate}
\item All copies in the library must be available for checkout or be
checked
out.

\item No copy of a book may be both available and checked out at the
same time.

\item A borrower may not have more than a predefined number of books
checked out at one time.

\item A borrower may not have more than one copy of the same book
checked out at one time.
\end{enumerate}
\end{verse}

\vspace{.2in}
\noindent
Since the above description is written in English, there
are some natural ambiguities and you will need to resolve them
in your formalization below.
Thus, you may find that in doing Parts A-C, you iterate through
different solutions for Part A.  This is perfectly normal and in fact,
expected!

\vspace{.2in}
\noindent A. Write a state machine description of the library system.
Use pre- and post-conditions
to specify the actions.
Use a balance of both pre-conditions and exceptional termination conditions to best
characterize the behavior of a library in real life.
See the middle
of p. 9 of Handout 5 for the template to use to describe your actions.

\vspace{.2in}
\noindent B. 
Given your formalization of the library in Part A, answer the
following questions and explain your answer by referring to your
state machine description.
\begin{enumerate}
\item Is there a difference between a book and a copy of a book?

\item Can a user be both a staff person and an ordinary borrower?

\item Can two different users have different copies of the same book?

\item What assumptions do you need to make about the initial state of
the library?

\end{enumerate}

\vspace{.2in}
\noindent C. Formally characterize each of the four invariants as an predicate.
For each, show that your actions preserve it.

\end{document}