CMU 15-671Models of Software SystemsFall 1995
State Machines
Garlan & Wing Homework 5 Due: 27 September 1995

Problem 1. 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 putting in a coin, which changes the state of the machine, and 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:

1. What happens if you try to put in a penny or a quarter?
2. What happens if there are no M&M's left in the jar?
3. What happens if no more coins can fit in the dispenser?
4. What happens if you run out of dimes?
5. Is it possible for you to get anything but M&M's?

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.

B. Now consider the the M&M machine in the Moose.

1. Does your state machine description of the machine change? If so, how? If not, why not?
2. Do your answers to any of the four questions in Part A change? If so, how and why? If not, why not?
3. 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?

Problem 2.

The following problem description, very slightly modified, is sometimes referred to as ``Kemmerer's library problem.''

Consider a small library system with the following actions:

1. Check out a copy of a book. Return a copy of a book.
2. Add a copy of a book to the library. Remove a copy of a book from the library.
3. Get the list of books by a particular author or in a particular subject area.
4. Find out the list of books currently checked out by a particular borrower.
5. Find out what borrower last checked out a particular copy of a book.

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:

1. All copies in the library must be available for checkout or be checked out.
2. No copy of a book may be both available and checked out at the same time.
3. A borrower may not have more than a predefined number of books checked out at one time.
4. A borrower may not have more than one copy of the same book checked out at one time.

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!

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.

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.

1. Is there a difference between a book and a copy of a book?
2. Can a user be both a staff person and an ordinary borrower?
3. Can two different users have different copies of the same book?
4. What assumptions do you need to make about the initial state of the library?

C. Formally characterize each of the four invariants as an predicate. For each, show that your actions preserve it.

• About this document ...