6.898 Advanced Topics in Software Design
Spring 2002
Exercise 1: Modelling and Analysis with Alloy
Hint for Halmos Gloves Problem

There are 4 things that need covering (3 patients and one surgeon). The gloves offer 4 resources. The formalization of this problem is a little trickier -- much trickier than the handshake problem. You'll need to express the constraints that the surgeon has to be able to handle the patients (via gloves); to express how contamination is passed on; and the no-contamination condition itself. You might want to associate with each operation a before and after state, each of which carries a contamination relation that says what has contaminated what.