Alloy 4 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)
A Complete Course Requirements Model (courses_solutions.als)
A Complete Leader Election Model (ringElection_solution.als)