Tutorial for Alloy 3.0

Jump to: v3.0 versus v2.0 | Philosophy | File System | River Crossing | Walkthrough

Alloy is a lightweight modelling language for software design. It is amenable to a fully automatic analysis, using the Alloy Analyzer, and provides a visualizer for making sense of solutions and counterexamples it finds.

This introduction to Alloy 3.0 includes:

• a tutorial for writing declarative models in Alloy
• a walkthrough of the Alloy interface and visualizer
• tips and techniques to help you with the modeling process
• two thoroughly explained sample models which are developed as running examples
• A thorough list of differences from version 2.0

This tutorial does not:

• provide an exhaustive list of Alloy commands, although many are described in sidenotes;
• focus on the technical semantics of Alloy, although we do touch upon it in several sidenotes. Rather, we focus on getting you to a point where you can read, write, and analyze reasonably advanced models;
• give a lengthy description of the background philosophy behind modeling and declarative modeling. Chapter 0 gives a summary of these issues, but the focus of this tutorial is to teach Alloy not convincing you to use it.

For these things, consult the new reference manual.

Instructions for using this tutorial

The main text of the tutorial will appear in this frame of the window. We will use running sample models, displayed in the top-right frame. Most links appearing in the body of the tutorial load sidenotes into the bottom-right frame. Sidenotes provide supplemental information and can be skipped without impeding your understanding of the current model.

You are not expected to take this tutorial with Alloy open. When you reach the Alloy walkthrough (between Lessons I and II of Chapter 1), you will be instructed on how to use the Alloy interface. After that point, you may choose to try out the things you see. While doing so is certainly helpful, it is not required for understanding the tutorial.

The Chapters (start here)

Alloy 3.0 is slightly different from Alloy 2.0, although the core concepts and modeling techniques are the same. This brief section will discuss changes in syntax, the new type system, and show how to upgrade a 2.0 model to work under 3.0. Alloy 3.0 also has vastly improved tools for visualizing solutions, which is covered in the walkthrough.

• Chapter 0, gives background for declarative modeling, compares Alloy to its alternatives, and further introduces the tutorial.
• Chapter 1, follows the development and analysis of a simple Alloy model of a file system, This chapter includes an Alloy interface walkthrough between Lessons I and II. This will also introduce you to Alloy 3.0's improved solution visualizer.
• Chapter 2, examines a more advanced Alloy model which solves the famous River Crossing planning problem, using the Ord package for modeling ordered state.

Important Sidenotes

Browse these after working through the chapters. They stand on their own, but are not a gentle introduction to Alloy (the way the Chapters are).

• How Alloy works from the user's perspective.
• How Alloy works behind the scenes.

List of All Sidenotes

If you know just what you want, you can browse the complete list of all the sidenotes, organized roughly by topic. This is a terrible way to learn Alloy, but can be a useful Reference and can help fill in the cracks in your knowledge.

Getting Additional Help

You can get more detailed information about Alloy syntax, patterns, and case studies from Software Abstraction, a book by Daniel Jackson. You can read some of the excerpts relevant to learning Alloy, or buy the book from Amazon.com once it comes out. Alloy itself can be downloaded (for free) from the Alloy Home page.

Please feel free to direct questions and comments (about this tutorial, about Alloy in general, or about related research) to the Alloy mailing list, XalloyX@mit.edu, or to the tutorial authors, XrseaterX@mit.edu (Rob Seater) and XgdennisX@mit.edu (Greg Dennis). Remove the "X" from the beginning and end of each email address. They are merely spam protection.

Alloy was developed at MIT by the Software Design Group under the guidance of Daniel Jackson. This research was funded by grant 0086154 from the ITR program of the National Science Foundation, by a grant from NASA, and by an endowment from Doug and Pat Ross.

restart the tutorial from the beginning.