University of Washington
Spring 2004
instructor: Rob DeLine
ta: Miryung Kim
due Wed 21 Apr 2004
This assignment will give you the opportunity to practice abstracting both the requirements for a system to be built (using problem frames) and a system's high-level behavior (using Alloy). You are to work alone on this assignment. You may ask your classmates for clarifications about the assignment, but not discuss solutions. You should feel free to consult the course readings, the lecture notes, and general material from the library or internet that describes problem frames and Alloy. You should not consult the library or internet for solutions to these assignment questions or similar questions, since that would rob you of the opportunity to hone your abstraction skills. Finally, please monitor the course mailing list for possible questions and clarifications about the assignment.
You are welcome to use either Alloy 2.0 or Alloy 2.1 beta for this assignment. Personally, I find version 2.0 significantly less buggy.
Note: The percentage for each problem not only represents the degree to which its solution counts toward the total grade, but also indicates my belief about how hard the problem is. If you like doing easier problems before harder problems, you should do the problems in order of increasing percentage.
In the second lecture, we briefly discussed the Patient Monitoring problem in class. This question explores the problem in more depth. Here's the wording of the problem that we saw in lecture:
A patient monitoring program is required for the ICU (intensive care unit) in a hospital. Each patient is monitored by an analog device which measures factors such as pulse, temperature, blood pressure, and skin resistance. The program reads these factors on a periodic basis (specified for each patient) and stores the factors in a database. For each patient, safe ranges for each factor are also specified by medical staff. If a factor falls outside a patient’s safe range, or if an analog device fails, the nurses’ station is notified.
1A. List every entity (person, object) from the problem statement that might potentially be a domain in a problem context description.
1B. Draw a problem context diagram for the problem. As you recall from lecture, this involves drawing a box for each relevant domain. For each domain, be sure to indicate whether the domain is a machine, causal, biddable or lexical domain. Then, draw a line between any two (or more) domains that share phenomena of interest. For each line, describe what the shared phenomena are.
1C. Are there entities in your list in 1A that you decided to omit from the context diagram in 1B? For each omitted entity, briefly describe why you chose to omit it.
1D. In lecture, we studied six different problem frames:
The problem context diagram you drew for part 1B represents the whole Patient Monitoring problem, which we will now break down into subproblems. Identify three parts of the Patient Monitoring problem that can be viewed as instances of problem frames. (You could use a single problem frame three times, or three different problem frames, or something in between.)
For each of the three parts of the problem that you match to a problem frame, draw a problem diagram that shows only those domains and shared phenomena from your context diagram that are part of the problem frame. As you recall from lecture, a problem diagram is like a context diagram but also includes a dotted bubble for the requirements, with dotted edges from the requirement to the affected domains (with arrowheads where appropriate). The requirements themselves should be described in a few English sentences. For each problem diagram, be sure to indicate how this subproblem can be seen as an instance of its problem frame, namely indicate which domain in your subproblem corresponds to which domain in the problem frame and indicate which phenomena in the subproblem corresponds to which phenomena in the problem frame.
Note: describing the entire Patient Monitoring problem would take many problem diagrams, so you should not expect that the three problem diagrams that you choose will cover the entire problem.
You are a teaching assistant for an undergraduate programming course. The professor has given the students an assignment to write a program that plays Tic-Tac-Toe (Noughts and Crosses). To test the students' programs, the professor wrote a checking problem, which given a final 3x3 Tic-Tac-Toe board will tell whether the board is a legal board and whether X or O won the game.
To test the checking program, the professor has asked you for a test suite. This problem is to use Alloy as a constraint engine to generate such a test suite consisting of at least ten tests. Each tests consists of (1) the contents of the board (whether there is an X, O, or blank in each of the nine squares), (2) whether the board is legal, and (3) whether the board shows X or O or neither as the winner.
Whenever you execute an Alloy "run" command on a function, it will generate a set of function inputs that makes that function evaluate to true. Each test in your test suite will be an Alloy function ("fun"), which, when executed with the "run" command, will produce an instance of a set of parameters that encode the three pieces of information in the test (the board, the legality, and the winner). Be sure to comment your Alloy file to describe how your definitions encode these three pieces of information. This problem does not involve any kind of input or output. To use your test suite, the processor will "execute" each of your functions in turn and use Alloy's user interface to extract the contents of the test, given your encoding. Also, when using the test suite, the professor will use each instance once as-is and once with X and O reversed on the board. Therefore, your test suite can focus on X or O without loss of generality. (Therefore, the professor will get 20 tests out of the 10 you produce.)
In theory, Alloy is totally nondeterministic and can produce many instances for different runs of the same function. Therefore, in theory, your test suite could simply define what it means to be a legal board and count on Alloy to produce as many legal boards as you like. In practice, Alloy tends to produce the same instance over and over again for the same function. Therefore to get some variety in your tests, you should create additional functions that add side conditions on the boards to artificially force Alloy to choose boards that are different from one another. For instance, if Alloy always places an X in the same square, you might write a function that constrains that square not to be X.
This question and the subsequent question are intentionally open-ended and are intended to give you practice at abstracting both what parts of a system's behavior are important and what properties of that behavior you would like to demonstrate.
3A. This part of the question is to create a model of the undo and redo commands from an editor of your choice. I would suggest either the Undo/Repeat commands of Microsoft Word, PowerPoint, or Visio, the Undo/Redo commands of Microsoft Visual Studio, or the Undo command of Gnu Emacs. Begin by playing with this feature in the editor of your choice. You should ask yourself questions about this feature to increase your understanding, for instance: Which commands are available (not grayed out) in the editor's initial state? When I make a single edit, which commands are available? Once a command becomes available, is there a sequence of operations that will make it unavailable again? and so on. (You should not include answers to these questions in your write-up. Such questions are just for your own understanding.) The undo or undo/redo commands can be surprisingly subtle, so you might need to play with the editor for a while to fully understand the feature.
Once you understand how these commands work in your chosen editor, write an English description of the editor and its undo or undo/redo commands. This description should describe the state the editor maintains and how the commands affect this state.
3B. Using your English description of the editor and its command from 3A, write an Alloy specification of this editor. Your specification will include at least one sig that represents the editor's state and functions that represent the undo command and the redo command (if your editor has redo).
3C. Write down (in English) three properties that the undo or undo/redo commands should obey.
3D. Encode your three properties from 3B as Alloy assertions and run Alloy to look for counterexamples to these assertions. If the assertion produces a counterexample, there are three possibilities: (1) your specification does not match the behavior of the real editor; (2) your assertion is not a reasonable property for the undo/redo commands to obey; or (3) there is a bug in the real editor. The first two choices are the most likely and you should correct your Alloy specification accordingly. If you think your assertion generates a counterexample for the third reason, write a few sentences describing why you think the behavior is a bug.
The ultimate goals of any specification language is to describe real systems and to demonstrate properties of those systems. In this problem you will write a specification of an influencial research file system from the early 1990s, called Coda. Start by reading "Disconnected operation in the Coda file system", by Kistler and Satyanarayanan. You should particularly focus on Section 4, which describes, at a high level, how Coda works. In a nutshell, Coda divides the world into clients, which access files, and servers, which store them. A client keeps a cached copy of a file that it accesses so that the file is still available whenever the connection between the client and server is down. Whenever the connection between client and server is re-established, the Coda file system (semi)automatically submits back to the server any local changes to the cached files, so that other clients can see the changes.
4A. The problem is to write an Alloy specification that demonstrates how Coda behaves. You will need at least some sigs that represent the following entities:
You will need functions that represent at least these actions:
To simplify things, you should consider only a single client, a single server, and a single file stored in a single volume.
4B.Write three Alloy assertions that test three properties that Coda should obey. As with problem 3, these properties are your choice. For example, here is an example property that you are free to use: if a client writes to a file while it is disconnected, those changes are visible to other clients after reconnection (because the changes get copied to the server). Also, as with problem 3, if Alloy finds a counterexample to your assertion, you should strongly consider whether this is a bug in your model or your assertion before concluding that you have found a bug in Coda or its description in the research paper. (However, if you do find a bug in Coda or its description, that would be an interesting result!)
Finally, any requests for clarifications on this assignment should be posted to the class mailing list, so that all students can benefit from the replies.