Please prepare a hard copy of your solutions and bring it to class on the due date. In addition to answers to the questions, include screen snapshots of visualizations, and any Alloy fragments you're asked to write.

The first few questions are very easy and shouldn't take long once you get the hang of using Alloy. The Surgeon's Gloves problem is rather intricate, but will probably take only a couple of hours at most. The Elevator System problem is a significant project that should take most of your time. You should try and complete the other questions and make enough progress on the Elevator System to be able to contribute to (and learn from!) the peer review session on Wednesday February 20th.

You can obtain the Alloy Analyzer from http://sdg.lcs.mit.edu/alloy. Report any problems with the Alloy Analyzer to the email address (alloy at mit.edu).

1. Playing with an Alloy model

1. How does the constraint p.spouse.spouse = p affect whether or not persons are married?
2. Why is the constraint Person = univ [Person] needed? Why did I express it like this rather than with a cardinality operator (#Person = ...)?
3. How would the constraint all p, q: Person | p in q.shaken => q in p.shaken be written without quantifiers? Hint: remember that to refer to a field r of a signature S as a relation when it's not joined with anything, you need to write S$r.
4. Who is Paul Halmos, by the way?

B. Find a solution to the puzzle for the case in which there are 8 persons in total. Run the solver again for 6 persons, 4 persons, and so on. What answers do you get? How about for odd numbers?

C. Extend the model with the theorem that Hilary and Jocelyn shake the same hands, and check it. Does it hold?

D. The standard visualization is a bit cluttered because it shows two edges for each handshake, and two edges for each marriage. Here's a hack to make prettier diagrams. Introduce a new relation, shaken' say, that's just like shaken but for each pair of edges includes only one. Now select shaken' but not shaken to be visualized (and colour the edges and turn off the labels for good measure). You'll need to add a fact that constrains shaken' appropriately. Hint: your answer to A.3. should help.

2. Writing a Baby Model (due to David Gries)

A. Formalize the following line from a song very literally:

Everybody loves my baby, but my baby loves only me.

along with the assertion claiming that from this it follows that I am my baby. Check the theorem in a scope of 3. Hint: The theorem holds, so if you get a counterexample, your formalization is wrong.

B. Correct the formalization to express what the songwriter probably meant, and show that the theorem now has a counterexample.

3. Checking Some Properties of Relations

Express the following theorems in Alloy, and check them. Hint: you can declare concrete signatures, but it's more elegant to use a polymorphic assertion.

1. For a set s and binary relation r, s.r = ~r.s.
2. Join is associative for binary relations.
3. For sets s and t and binary relation r, (s + t).r = s.r + t.r.
4. For sets s and t and binary relation r, (s & t).r = s.r & t.r. Add a constraint on r that makes this theorem true.

4. Generating Spanning Trees

5. Surgeon's Gloves

A surgeon must operate on three patients, but has only two pairs of gloves. There must be no cross-contamination: the surgeon must not come into contact with the blood of any patient, and no patient must come into contact with the blood of another patient. The surgeon needs two hands to work. How does she do it?

Express this problem in Alloy, and use the analyzer to find a solution. Try and get a nice visualization of the solution; you may want to use the ability to project a type to show separate diagrams for each operation.

Hint: If you really want one, there's a hint here.

6. Specifying an Elevator System

Here are some assumptions you can make:

1. There's a bank of elevators, each of which serves the same collection of floors.
2. There are up and down call buttons on floors, and floor buttons within the elevators.
3. An elevator can be viewed as being at a floor or between floors; when an elevator doesn't stop at a floor, it goes from being below a floor to being above it (or vice versa), and is never at it.
4. Elevators don't change direction between floors.

You'll need to describe how button requests are serviced and when they are cancelled. Rather than writing an algorithm, you should develop a collection of rules, and investigate the consequences of certain combinations of rules. For example, you might have a NoSkipping rule which says that an elevator can't pass a floor if there's a request to stop at that floor.

You should be able to do some interesting analysis by considering only transitions from one state to another. You'll probably want to allow all elevators to move in one transition, and for buttons to be pressed at the same time. If you're ambitious, you might investigate some trace properties too. To check that nobody waiting is 'starved', for example, you could assert that there's no trace in which the system goes in a loop, returning to an old state without serving an outstanding request.

Your model should separate different constraints according to where they come from. For example, physical constraints -- such as an elevator not jumping from the 1st floor to the 3rd floor without passing the second floor -- should be recorded completely separately from policy constraints -- such as an elevator not skipping floors with outstanding requests.

This is an open-ended task, and you can make it as general as you like. But you want to aim for a description of some simple policies and some insight into their ramifications, rather than finding bugs in a complex scheme that's hard to explain.