FM'06 Alloy Tutorial Materials

Tutorial Slides:

Session 1 - Intro & Logic (ODP) (PDF)
Session 2 - Language & Analysis (ODP) (PDF)
Session 3 - Static Modeling (ODP) (PDF)
Session 4 - Dynamic Modeling (ODP) (PDF)

files with the ".odp" extension can be opened with OpenOffice

Exercises

Properties of Binary Relations (properties.als)
Refactoring Navigation Expressions (distribution.als)
Modeling the Tube (tube.als)
I'm My Own Grandpa (grandpa.als)
Barber Paradox (barber.als)
Address Book (addressBook.als)
Leader Election in a Ring (ringElection)

Solutions

Solutions to Logic Exercises (logic_solutions.txt)
Solutions to Barber Exercise (barber_solution.als)
Sample Barber Visualization Palette (barber_solution.pal)
A Complete Course Requirements Model (courses_solutions.als)
A Complete Leader Election Model (ringElection_solution.als)

Related Alloy Materials

Alloy homepage - downloads, tutorials, papers
Quick Start - very brief overview of how to use Alloy
Online Tutorial - longer introduction to Alloy plus some advice on writing models.
Alloy 3.0 reference manual
To discuss Alloy with other users, post a message in the alloy-discuss group on yahoo.