|6.898||Advanced Topics in Software Design
Exercise 1: Modelling and Analysis with Alloy
Due: Monday, February 25th at 2:30pm
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).
p.spouse.spouse = paffect whether or not persons are married?
Person = univ [Person]needed? Why did I express it like this rather than with a cardinality operator (
#Person = ...)?
all p, q: Person | p in q.shaken => q in p.shakenbe written without quantifiers? Hint: remember that to refer to a field
rof a signature
Sas a relation when it's not joined with anything, you need to write
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.
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.
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.
sand binary relation
s.r = ~r.s.
tand binary relation
(s + t).r = s.r + t.r.
tand binary relation
(s & t).r = s.r & t.r. Add a constraint on
rthat makes this theorem true.
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.
Here are some assumptions you can make:
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.