CSci 420/520: Homework 7

Modeling and Checking in Alloy I

Due Friday, October 28th by 1pm.

Summary

In this assignment, you will learn how to correct and modify simple models in Alloy. We provide you with an initial model for patients, doctors and prescriptions. When a patient goes to the doctor, he or she receives a prescription for a medication. So after executing the Prescribe operation, some patient should have one more prescription in their possession. We would like to also make sure that patients are not given a prescription for some medication that they already have a prescription for.

There are several problems with the specification, and we have provided assertions to demonstrate them. You should use the counterexamples that the Alloy Analyzer generates to help figure out what is wrong with the specification. You may want to tell it to layout the graphs left-to-right instead of top-to-bottom.

Note: Due to an unfortunate artifact of the way we have to explicitly specify state in Alloy, the prescriptions that a person owns cannot be stored in the Patient sig. Instead, we have put person's_prescriptions in State.

Instructions

1. Download pharmacy.als and place it into your work directory.
2. The specification for Prescribe says "one patient gets one new prescription". However, our sanity check PrescriptionsAreIncremental fails, indicating that somehow more than one prescription can be given out by the Prescribe operation. Update Prescribe at the location marked "Bug #1" so that it is correct. Be sure that PrescriptionsAreIncremental passes. You should increase the scope to get more confidence.
3. Correct the mistake labelled "Bug #2" in Prescribe that was supposed to ensure that the patient is not given a prescription that they already have. Change the line so that it makes sure that the patient is not given a prescription that has the same doctor and medication as another in the patient's possession. The UniquePrescriptions assertion should pass if you have corrected it properly.
4. Now that the model is corrected, enhance the specification by writing NoDoublePrescriptionsForMedication, which states that in a given state, a patient cannot have two prescriptions for the same medication.
5. When you are finished writing NoDoublePrescriptionsForMedication, you will see that it actually fails for a specific case that occurs in real life. The problem can be corrected by reinterpreting the purpose of patient's_prescriptions---instead of it representing the prescriptions in a patient's possession, it is a universal database that is accessible by all doctors. Using this new interpretation, update the Prescribe operation to use this shared database to ensure that NoDoublePrescriptionsForMedication is true. (Normally you would also change patient's_prescriptions to prescription_database everywhere, and document its purpose, but don't worry about it for this assignment.)
6. Complete the RevokePrescription operation. You should create your own assertions and checks to make sure that it is correct.

Grading

200 points total.

Email your updated pharmacy.als to meghan@cs.wm.edu.