Problem Set 2: Static Alloy Model (due Wed March 9)
Now that you have developed some skills writing and analyzing models in Alloy, it's time to do something more interesting. This week's assignment is to construct a model of a subject of your own choosing. It should be a static model, meaning that there should be no modelling of mutable state. This doesn't mean that you can't specify operations that are executed dynamically (such as lookups), but there won't be an explicit notion of state.
Your model should be presented as a self-contained case study. You should assume that your reader knows Alloy, but has no knowledge of the subject of the study. The writeup should include at least the following elements:
- (1) an introduction explaining what's being studied, why it's interesting;
- (2) an informal overview of the subject, outlining the key concepts;
- (3) a detailed presentation of, and commentary on, the Alloy model;
- (4) a conclusion, explaining what was learned, and evaluating to what extent modelling and analyzing the subject was helpful.
Your model should include at least a couple of interesting simulations and at least one interesting assertion.
You should concentrate on developing the model, and only polish the writeup after the model is largely complete. The model should be small and simple: your aim is to capture the essence of your subject as succinctly as possible. As a rough guide, you should expect to develop a model that has at least 3 signatures and 3 fields, but no more than about 8 signatures and 12 fields. Use Alloy to help you check refactorings of your constraints to reduce them to a concise, elegant (and understandable!) form. If your model has become complicated and arcane, try and identify aspects of it that aren't essential, or try to find a way to take a more abstract view that will preserve the core content while removing extraneous detail.
As examples of case studies developed by students with comparable experience in Alloy, see:
- Chord: A Peer-to-Peer Protocol by Hoeteck Wee
- Case Study in Alloy Modeling: A Common Profile for Presence by Edmond Lau
Both of these took several weeks of work, and involved extensive background reading. You should be less ambitious, and pick a subject that you already have some knowledge of, and can be confident you can model in a few hours. It's better to construct a simple model and polish it into something elegant and insightful than to construct a complicated model that you don't have time to rework.
You can pick any subject that appeals to you. Here are some suggestions:
- DNS lookup: model the structure of domain names, the contents of server databases, and the algorithm for resolving lookups;
- make file: model the structure of a make file, and the calculation of which commands are to be executed given freshness data about files;
- style sheets: model the structure of hierarchical style sheets, as found in programs such as Word, InDesign, Quark, and Framemaker, paying attention in particular to how inheritance of formatting properties is handled;
- web addressing: model the way in which resources are named on the web, and the mechanisms used for resolving them;
- vote tallying: model the relationship between a collection of ballots in which candidates are ranked, and the outcome of the election under different voting strategies (such as plurality, condorcet, borda count, instant runoff voting).
Appeal for volunteers: Prof. Darko Marinov (University of Illinois at Urbana-Champaign) is conducting some research on new Alloy analyses and has asked us to provide transcripts of Alloy modelling sessions. If you are willing to donate logs of your sessions to the cause of science, please do the following: (1) download the most recent nightly build of the Alloy analyzer; (2) turn on logging under the 'experimental options' tab of the preference settings; (3) email your log files directly to Darko at (marinov at cs.uiuc.edu).
Please recall the somewhat entertaining submission instructions.