Tutorial for Alloy Analyzer 4.0

Rob Seater and Greg Dennis

alloytools.org

Quantifiers

• all x:X | formula - every x of type X satisfies formula. If there are no X, then this statement is trivially true.

• some x:X | formula - one or more x of type X satisfy formula. If there are no X, then this statement is trivially false.

• no x:X | formula - exactly zero x of type X satisfy formula

• one x:X | formula - exactly one x of type X satisfies formula

• lone x:X | formula - either zero or one x of type X satisfies formula

Multiplicity Markings

Declarative vs. Operational (Imperative) Modeling

How to think about an Alloy model: 3 levels

Thinking about higher order relations

Relations as Ordered Tuples

equivalent ways of expressing