A series of four and a half lectures on Alloy, aimed at students with an interest
in a mathematical approach to modelling. No background required beyond elementary logic.
The elevator case study was replaced by the bakery example at the last minute (since
it had been discussed by John Rushby in his lectures). In that example, the modelling
of a procss in the critical section as holding no ticket is bogus and has to be fixed
(but the general structure of the model, and the trace-based analysis still holds).

Introduction [PDF, animated] [PDF, for printing]

Logic [PDF, animated] [PDF, for printing]

Language [PDF, animated] [PDF, for printing]

Analysis [PDF, animated] [PDF, for printing]

Bakery [PDF, animated] [PDF, for printing]

Elevator [PDF, animated] [PDF, for printing]