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


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 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)