Alloy Syntax Guide - AlchemicalChef

This guide covers Alloy syntax comprehensively. If you’re new to Alloy, start with Alloy Basics for a gentler introduction. This reference assumes you understand the core concepts: signatures, relations, facts, and the basic workflow. Alloy 6 introduced temporal operators for modeling state over time. This guide covers both classic (static) Alloy and the temporal extensions.

When to Use Alloy

Alloy excels at finding counterexamples to structural properties. Use it when you need to answer:

“Can this bad state exist?” - Alloy searches for violations
“Is this constraint sufficient?” - Alloy finds gaps
“What does this data model actually allow?” - Alloy generates instances

Alloy uses SAT-based bounded verification. It doesn’t prove properties hold for all possible sizes, it exhaustively checks within the bounds you specify (typically 3-5 atoms per signature). This is usually enough to find bugs; most flaws manifest in small counterexamples. For temporal properties like “this eventually happens” or protocol correctness over time, consider TLA+. The two tools complement each other well.

Signatures

Signatures define the types of atoms in your model. They’re like classes in OOP or tables in a database, but with relational semantics.

Basic Signatures

sig Person {}           -- A set of Person atoms
sig File {}             -- A set of File atoms
sig Empty {}            -- Can be empty (zero atoms)

Signature Modifiers

one sig Root {}           -- Exactly one atom
lone sig Config {}        -- Zero or one atom
some sig Node {}          -- At least one atom
abstract sig Entity {}    -- No direct atoms (only via extensions)

The one, lone, and some modifiers constrain cardinality:

Modifier	Meaning	Atoms
(none)	Any number	0, 1, 2, …
`one`	Exactly one	1
`lone`	At most one	0 or 1
`some`	At least one	1, 2, 3, …
`abstract`	None directly	0 (only subtypes)

Signature Extension

abstract sig Animal {}
sig Cat extends Animal {}
sig Dog extends Animal {}

Extensions create subtypes. Each Cat atom is also an Animal atom. Extensions are unique in the sense that no atom is both a Cat and a Dog.

Signature Subsets

sig Person {}
sig Employee in Person {}
sig Manager in Employee {}

The in keyword creates subsets that aren’t necessarily unique. An atom can be both an Employee and something else that extends Person.

Disjoint Subsets

sig Person {}
sig Student, Faculty in Person {}
-- Student and Faculty can overlap (a Person can be both)

-- To make them disjoint, add a fact:
fact { no Student & Faculty }
-- Or use disj in quantifiers:
-- all disj s: Student, f: Faculty | ...

To ensure subsets don’t overlap, add a disjointness fact. A Person can still be neither Student nor Faculty.

Fields and Multiplicity

Fields define relations between signatures. Every field is a relation, even “attributes” are relations to value atoms.

Field Multiplicity

sig Person {
    name: one String,        -- Exactly one name (required)
    spouse: lone Person,     -- Zero or one spouse (optional)
    children: set Person,    -- Zero or more children
    parents: some Person     -- One or more parents (at least one)
}

Keyword	Meaning	Count
`one`	Exactly one	1
`lone`	At most one	0-1
`set`	Any number	0+
`some`	At least one	1+

Without a keyword, one is assumed for simple relations. For relations with arrow (->), set is the default.

Binary Relations

Most fields are binary relations (from this signature to another):

sig File {
    parent: one Folder,      -- File -> Folder
    owner: one User          -- File -> User
}

Ternary and Higher Relations

Relations can have higher arity:

sig Person {
    -- For each Person, maps Organizations to Roles
    membership: Organization -> Role
}

sig Object {
    -- Access control: Subject -> Permission mapping
    access: Subject -> Permission
}

To use: p.membership[org] returns the roles person p has in organization org.

Relation Constraints

sig Node {
    edges: set Node
}

-- Self-loops allowed by default; prevent with fact:
fact NoSelfLoops {
    no n: Node | n in n.edges
}

-- Symmetric relation (bidirectional edges):
fact Symmetric {
    all n1, n2: Node | n1 in n2.edges implies n2 in n1.edges
}

Relational Operators

Alloy is fundamentally relational. Understanding these operators is essential.

Join (.)

The dot operator navigates relations:

sig Person {
    father: lone Person,
    mother: lone Person
}

p.father          -- p's father (a Person or empty)
p.father.father   -- p's paternal grandfather
p.(father + mother)  -- p's father or mother

Join composes relations. If r: A -> B and s: B -> C, then r.s: A -> C.

Union (+)

Combines sets or relations:

Cat + Dog                    -- All cats and dogs
p.father + p.mother          -- p's parents
read + write                 -- Union of permissions

Intersection (&)

Elements in both:

Employee & Manager           -- People who are both
trusted & external           -- Trusted external entities

Difference (-)

Elements in first but not second:

Person - Employee            -- Non-employees
all - allowed                -- Forbidden items

Transpose (~)

Reverses a relation:

sig File {
    parent: one Folder
}

~parent                      -- Folder -> File (children)
f.~parent                    -- Files in folder f

If r: A -> B, then ~r: B -> A.

Transitive Closure (^)

One or more applications of a relation:

sig Folder {
    parent: lone Folder
}

f.^parent                    -- All ancestors of f
^parent                      -- The ancestor relation
n in n.^parent               -- n is its own ancestor (cycle!)

Transitive closure is powerful for reachability, ancestry, and graph analysis.

Reflexive Transitive Closure (*)

Zero or more applications (includes identity):

f.*parent                    -- f and all its ancestors
*parent                      -- The "ancestor or self" relation

The difference: ^r requires at least one step; *r includes staying in place.

Product (->)

Creates pairs:

User -> File                 -- All user-file pairs
alice -> secret              -- Specific pair
Person -> Person -> Action   -- Ternary relation

Domain Restriction (`<:`)

Limits a relation to a domain subset:

Employee <: salary           -- salary restricted to Employees
trusted <: access            -- access for trusted entities only

If r: A -> B and s: set A, then s <: r: A -> B contains only pairs where the first element is in s.

Range Restriction (`:>`)

Limits a relation to a range subset:

knows :> Employee            -- knowing relationships to Employees
access :> ReadOnly           -- access limited to read-only perms

If r: A -> B and s: set B, then r :> s: A -> B contains only pairs where the second element is in s.

Override (++)

Replaces mappings:

defaults ++ customSettings   -- custom overrides defaults
oldState ++ (key -> newValue)  -- Update specific mapping

For function-like relations, ++ updates entries. If key exists in oldState, the new value replaces it.

Cardinality (#)

Counts elements:

#Person                      -- Number of persons
#(p.friends)                 -- Number of p's friends
#File > 0                    -- At least one file exists

Quantifiers

Quantifiers express properties over sets.

Universal (all)

all p: Person | p.age >= 0
all f: File | one f.parent
all x, y: Node | x.edge = y implies y.edge = x

Every element satisfies the condition.

Existential (some)

some p: Person | p.age > 100
some f: File | no f.parent
some x, y: Node | x != y and x in y.edge

At least one element satisfies the condition.

None (no)

no p: Person | p.age < 0
no f: Folder | f in f.^parent
no disj x, y: Node | x.edge = y.edge

No element satisfies the condition. Equivalent to not some.

Unique (one)

one p: Person | p.name = "Alice"
one f: File | f.size = max[File.size]

Exactly one element satisfies the condition.

At Most One (lone)

lone p: Person | p.role = CEO
lone f: File | no f.parent

Zero or one element satisfies the condition.

Disjoint Quantification

all disj x, y: Person | x.id != y.id
some disj a, b, c: Node | a->b + b->c in edge

The disj modifier ensures quantified variables are distinct.

Logical Operators

Combine quantified expressions:

-- Conjunction
all p: Person | p.age >= 0 and p.age <= 150

-- Disjunction
all f: File | f.public or some f.owner

-- Implication
all p: Person | p.employed implies some p.salary

-- Biconditional
all x: Node | x.root iff no x.parent

-- Negation
all p: Person | not p in p.^parent

Operator	Meaning
`and`	Both true
`or`	At least one true
`implies` / `=>`	If-then
`iff` / `<=>`	If and only if
`not` / `!`	Negation

Facts, Predicates, Functions, Assertions

These organize constraints and queries.

Facts

Facts are constraints that always hold. Alloy only considers instances satisfying all facts.

fact NoSelfEmployment {
    no p: Person | p in p.manages
}

fact AcyclicHierarchy {
    all p: Person | p not in p.^manages
}

-- Anonymous fact (no name)
fact {
    all f: File | some f.owner
}

Facts constrain the search space. Use them for invariants that define your model.

Predicates

Predicates are named, parameterized formulas. They can be true or false.

pred isManager[p: Person] {
    some p.manages
}

pred canAccess[u: User, f: File] {
    f in u.owns or f in u.sharedWith
}

pred wellFormed {
    all f: File | some f.parent
    no f: Folder | f in f.^parent
}

Use predicates to define reusable conditions or as targets for run commands.

Functions

Functions return values (sets/relations). They’re expressions, not constraints.

fun parents[p: Person]: set Person {
    p.father + p.mother
}

fun ancestors[p: Person]: set Person {
    p.^(father + mother)
}

fun commonFriends[p1, p2: Person]: set Person {
    p1.friends & p2.friends
}

-- Functions can return relations
fun familyRelation: Person -> Person {
    father + mother + ~father + ~mother
}

Assertions

Assertions are properties you claim should hold. The check command searches for violations.

assert NoOrphans {
    all f: File | some f.parent or f in RootFolder
}

assert TransitiveClosure {
    all p: Person | p.ancestor = p.^parent
}

assert PermissionConsistency {
    all u: User, f: File |
        canRead[u, f] implies canAccess[u, f]
}

Unlike facts, assertions don’t constrain the model, they query it.

Comprehensions

Set comprehensions build sets from expressions.

Basic Comprehension

{ p: Person | p.age > 21 }           -- Adults
{ f: File | no f.owner }             -- Unowned files
{ x: Node | x in x.^next }           -- Nodes in cycles

Expression Comprehension

{ p: Person, f: File | f in p.owns } -- Ownership pairs
{ x, y: Node | x->y in edges }       -- Edge pairs

In Predicates and Functions

fun adults: set Person {
    { p: Person | p.age >= 18 }
}

pred allFilesOwned {
    no { f: File | no f.owner }
}

Let Expressions

let binds names to expressions for clarity and reuse.

pred complexCondition[p: Person] {
    let parents = p.father + p.mother,
        siblings = parents.~(father + mother) - p |
    some siblings and #parents = 2
}

fun reachable[start: Node]: set Node {
    let direct = start.edges,
        indirect = direct.^edges |
    direct + indirect
}

Let bindings are purely syntactic, they don’t affect semantics.

Commands

Commands tell the Analyzer what to do.

Run

The run command searches for instances.

run {}                           -- Any valid instance
run { some File }                -- Instance with files
run wellFormed                   -- Instance where predicate holds
run { #Person = 3 }              -- Exactly 3 persons

Check

The check command searches for assertion violations.

check NoOrphans                  -- Find counterexample
check PermissionConsistency      -- Verify property
check { all f: File | some f.owner }  -- Inline assertion

Scope

Bounds limit the search space. By default, bounds mean “at most N atoms” (0 to N), not “exactly N.”

run {} for 5                     -- 0 to 5 of each signature
run {} for 3 File, 2 Folder      -- 0-3 Files, 0-2 Folders
run {} for exactly 3 Person      -- Exactly 3 (not 0 to 3)
run {} for 5 but 2 Int           -- 5 default, but 2-bit integers (-2 to 1)

check NoOrphans for 10           -- Check with 0-10 atoms per signature
check NoOrphans for 3 but 5 File -- 0-3 default, 0-5 files

Use exactly when you need a specific count. Without it, Alloy explores all sizes up to the bound, which is usually what you want for finding counterexamples.

Expect

Expect indicates anticipated results (for documentation/testing).

run {} for 3 expect 1            -- Expect satisfiable
check NoOrphans expect 0         -- Expect no counterexample

Module System

Modules organize specifications into reusable units.

Basic Modules

module filesystem

sig File { ... }
sig Folder { ... }

Opening Modules

module main

open filesystem                  -- Import all from filesystem
open util/ordering[Time]         -- Parameterized utility module
open util/relation               -- Relation utilities

Private Declarations

module internal

private sig Helper {}            -- Not visible when opened
sig Public {}                    -- Visible

Parameterized Modules

module graph[Node]

sig Edge {
    src, dst: one Node
}

pred connected[n1, n2: Node] {
    n2 in n1.^(~src.dst)
}

Usage:

open graph[Computer]             -- Instantiate with Computer

Standard Library

Alloy includes utility modules:

open util/ordering[State]        -- Total ordering on State
open util/relation               -- Relation predicates
open util/ternary                -- Ternary relation utilities
open util/boolean                -- Boolean operations
open util/integer                -- Integer operations
open util/sequence[Elem]         -- Sequences

Temporal Operators (Alloy 6)

Alloy 6 introduced temporal logic for modeling state over time.

Variable Fields

sig Buffer {
    var contents: set Data,      -- Changes over time
    capacity: one Int            -- Static (no var)
}

The var keyword marks mutable relations.

Priming

The prime operator (') refers to the next state:

pred addData[b: Buffer, d: Data] {
    d not in b.contents          -- Precondition
    b.contents' = b.contents + d -- Postcondition
}

Temporal Quantifiers

-- Future-time operators
always P                         -- P holds in every future state
eventually P                     -- P holds in some future state
after P                          -- P holds in the next state
P until Q                        -- P holds until Q becomes true
P releases Q                     -- Q holds until P becomes true (or forever)

-- Past-time operators
historically P                   -- P held in all past states
once P                           -- P held at some past state
before P                         -- P held in the previous state
P since Q                        -- P has held since Q was true

Traces and Liveness

-- Specification: initial state + transitions
fact Traces {
    init
    always trans
}

pred init {
    no Buffer.contents
}

pred trans {
    some b: Buffer, d: Data | addData[b, d]
    or stutter
}

pred stutter {
    contents' = contents
}

-- Liveness: something eventually happens
assert EventuallyFull {
    always (some b: Buffer | eventually #b.contents = b.capacity)
}

Temporal Example: Mutex

module mutex

abstract sig Process {
    var state: one State
}

abstract sig State {}
one sig Idle, Waiting, Critical extends State {}

one sig P1, P2 extends Process {}

pred init {
    all p: Process | p.state = Idle
}

pred requestAccess[p: Process] {
    p.state = Idle
    p.state' = Waiting
    all other: Process - p | other.state' = other.state
}

pred enterCritical[p: Process] {
    p.state = Waiting
    no other: Process - p | other.state = Critical
    p.state' = Critical
    all other: Process - p | other.state' = other.state
}

pred exitCritical[p: Process] {
    p.state = Critical
    p.state' = Idle
    all other: Process - p | other.state' = other.state
}

pred stutter {
    all p: Process | p.state' = p.state
}

pred trans {
    (some p: Process | requestAccess[p] or enterCritical[p] or exitCritical[p])
    or stutter
}

fact Traces {
    init
    always trans
}

-- Safety: mutual exclusion
assert MutualExclusion {
    always (lone p: Process | p.state = Critical)
}

-- Liveness: no starvation (if waiting, eventually critical)
-- Note: This will fail without fairness constraints - one process can
-- repeatedly enter/exit while another waits forever
assert NoStarvation {
    all p: Process | always (p.state = Waiting implies eventually p.state = Critical)
}

check MutualExclusion for 5 steps
check NoStarvation for 10 steps

Built-in Relations and Constants

Universal Set

univ                             -- All atoms
Person in univ                   -- Always true
univ - Person                    -- All non-Person atoms

Empty Set

none                             -- Empty set
no x implies x = none            -- Equivalence

Identity Relation

iden                             -- Identity: x->x for all x
r & iden                         -- Self-loops in r
r - iden                         -- Remove self-loops

Integer Operations

-- Arithmetic
plus[x, y]                       -- x + y
minus[x, y]                      -- x - y
mul[x, y]                        -- x * y
div[x, y]                        -- x / y
rem[x, y]                        -- x % y

-- Comparison
x < y, x > y, x <= y, x >= y

-- Aggregation
sum[s]                           -- Sum of integer set
max[s], min[s]                   -- Maximum/minimum

-- Integer set
Int                              -- All integers in scope

Note: Alloy uses bounded integers. The default is 4-bit, giving a range of -8 to 7. Use for N Int to set bitwidth (e.g., for 5 Int gives 5-bit integers: -16 to 15). Integer overflow wraps silently, so increase bitwidth if your model uses larger numbers.

Common Patterns

State Machine

abstract sig State {}
one sig S1, S2, S3 extends State {}

sig Machine {
    var current: one State
}

pred transition[m: Machine, from, to: State] {
    m.current = from
    m.current' = to
}

Graph Reachability

sig Node {
    edges: set Node
}

fun reachable[n: Node]: set Node {
    n.*edges
}

pred connected {
    all n1, n2: Node | n2 in reachable[n1]
}

pred acyclic {
    no n: Node | n in n.^edges
}

Ownership / Containment

sig Container {
    contains: set Item
}

sig Item {
    inside: lone Container
}

fact Consistency {
    all c: Container, i: Item |
        i in c.contains iff i.inside = c
}

fact SingleOwner {
    all i: Item | lone i.inside
}

Access Control

sig Subject {}
sig Object {}
sig Permission {}

sig AccessMatrix {
    access: Subject -> Object -> Permission
}

pred canAccess[s: Subject, o: Object, p: Permission] {
    some am: AccessMatrix | p in am.access[s][o]
}

Ordered Elements

open util/ordering[Time]

sig Time {}

sig Event {
    when: one Time
}

pred before[e1, e2: Event] {
    lt[e1.when, e2.when]
}

fact EventOrder {
    all e1, e2: Event | e1 != e2 implies
        (before[e1, e2] or before[e2, e1])
}

Complete Example: Key-Value Store

A specification combining multiple concepts:

module kvstore

sig Key {}
sig Value {}

sig Store {
    var data: Key -> lone Value
}

one sig TheStore extends Store {}

pred init {
    no TheStore.data
}

pred put[k: Key, v: Value] {
    TheStore.data' = TheStore.data ++ (k -> v)
}

pred get[k: Key, v: Value] {
    v = TheStore.data[k]
    TheStore.data' = TheStore.data  -- Frame condition
}

pred delete[k: Key] {
    TheStore.data' = TheStore.data - (k -> Value)
}

pred trans {
    (some k: Key, v: Value | put[k, v])
    or (some k: Key | delete[k])
    or (TheStore.data' = TheStore.data)  -- Stutter
}

fact Traces {
    init
    always trans
}

-- Each key maps to at most one value
assert Functional {
    always all k: Key | lone TheStore.data[k]
}

-- If we put k->v and don't delete or overwrite, it stays
assert PutPersists {
    all k: Key, v: Value |
        always (put[k, v] and after always (not delete[k] and not (some v': Value - v | put[k, v'])))
            implies after always TheStore.data[k] = v
}

-- Delete removes the key
assert DeleteRemoves {
    all k: Key |
        always (delete[k] implies after no TheStore.data[k])
}

check Functional for 3 but 5 steps
check PutPersists for 3 but 8 steps
check DeleteRemoves for 3 but 5 steps

run { eventually some TheStore.data } for 3 but 5 steps

Quick Reference

Signature Modifiers

Modifier	Meaning
`one`	Exactly one atom
`lone`	Zero or one atom
`some`	At least one atom
`abstract`	No direct atoms
`extends`	Disjoint subtype
`in`	Subset (possibly overlapping)

Field Multiplicity

Keyword	Meaning
`one`	Exactly one
`lone`	Zero or one
`some`	One or more
`set`	Zero or more (default)

Relational Operators

Operator	Name	Purpose
`.`	Join	Navigate relations
`+`	Union	Combine sets
`&`	Intersection	Common elements
`-`	Difference	Remove elements
`~`	Transpose	Reverse relation
`^`	Transitive closure	One+ steps
`*`	Reflexive transitive closure	Zero+ steps
`->`	Product	Create tuples
`<:`	Domain restriction	Filter by domain
`:>`	Range restriction	Filter by range
`++`	Override	Replace mappings
`#`	Cardinality	Count elements

Logical Operators

Operator	Meaning
`and`	Conjunction
`or`	Disjunction
`not` / `!`	Negation
`implies` / `=>`	Implication
`iff` / `<=>`	Biconditional

Quantifiers

Quantifier	Meaning
`all`	For every
`some`	There exists
`no`	For none
`one`	Exactly one
`lone`	At most one

Temporal Operators (Alloy 6)

Operator	Meaning
`'`	Next state value
`always`	In all future states
`eventually`	In some future state
`after`	In the next state
`until`	P holds until Q
`releases`	Q holds until P (or forever)
`historically`	In all past states
`once`	In some past state
`before`	In the previous state
`since`	P has held since Q

Commands

Command	Purpose
`run P`	Find instance where P holds
`run {} for N`	Find any instance with scope N
`check A`	Find counterexample to assertion A
`check A for N`	Check with scope N

Where to Go Next

This guide covered Alloy syntax comprehensively. For practical application:

Alloy Basics — If you skipped it, the gentle introduction provides context
MacAlloy — Native macOS tool for running specifications
AD Security Model — Real-world Alloy for Active Directory security
Software Abstractions — Daniel Jackson’s definitive book
Alloy Documentation — Official reference

The best way to learn is to model something you care about. Start small, run frequently, and let the Analyzer show you what your model actually allows.

Overview

TLA+

Alloy

AD Tier Model Specifications

Binary Analysis Series

Malware Analysis

Aviation Systems Series

Tools

​When to Use Alloy

​Signatures

​Basic Signatures

​Signature Modifiers

​Signature Extension

​Signature Subsets

​Disjoint Subsets

​Fields and Multiplicity

​Field Multiplicity

​Binary Relations

​Ternary and Higher Relations

​Relation Constraints

​Relational Operators

​Join (.)

​Union (+)

​Intersection (&)

​Difference (-)

​Transpose (~)

​Transitive Closure (^)

​Reflexive Transitive Closure (*)

​Product (->)

​Domain Restriction (<:)

​Range Restriction (:>)

​Override (++)

​Cardinality (#)

​Quantifiers

​Universal (all)

​Existential (some)

​None (no)

​Unique (one)

​At Most One (lone)

​Disjoint Quantification

​Logical Operators

​Facts, Predicates, Functions, Assertions

​Facts

​Predicates

​Functions

​Assertions

​Comprehensions

​Basic Comprehension

​Expression Comprehension

​In Predicates and Functions

​Let Expressions

​Commands

​Run

​Check

​Scope

​Expect

​Module System

​Basic Modules

​Opening Modules

​Private Declarations

​Parameterized Modules

​Standard Library

​Temporal Operators (Alloy 6)

​Variable Fields

​Priming

​Temporal Quantifiers

​Traces and Liveness

​Temporal Example: Mutex

​Built-in Relations and Constants

​Universal Set

​Empty Set

​Identity Relation

​Integer Operations

​Common Patterns

​State Machine

​Graph Reachability

​Ownership / Containment

​Access Control

​Ordered Elements

​Complete Example: Key-Value Store

When to Use Alloy

Signatures

Basic Signatures

Signature Modifiers

Signature Extension

Signature Subsets

Disjoint Subsets

Fields and Multiplicity

Field Multiplicity

Binary Relations

Ternary and Higher Relations

Relation Constraints

Relational Operators

Join (.)

Union (+)

Intersection (&)

Difference (-)

Transpose (~)

Transitive Closure (^)

Reflexive Transitive Closure (*)

Product (->)

Domain Restriction (`<:`)

Range Restriction (`:>`)

Override (++)

Cardinality (#)

Quantifiers

Universal (all)

Existential (some)

None (no)

Unique (one)

At Most One (lone)

Disjoint Quantification

Logical Operators

Facts, Predicates, Functions, Assertions

Facts

Predicates

Functions

Assertions

Comprehensions

Basic Comprehension

Expression Comprehension

In Predicates and Functions

Let Expressions

Commands

Run

Check

Scope

Expect

Module System

Basic Modules

Opening Modules

Private Declarations

Parameterized Modules

Standard Library

Temporal Operators (Alloy 6)

Variable Fields

Priming

Temporal Quantifiers

Traces and Liveness

Temporal Example: Mutex

Built-in Relations and Constants

Universal Set

Empty Set

Identity Relation

Integer Operations

Common Patterns

State Machine

Graph Reachability

Ownership / Containment

Access Control

Ordered Elements

Complete Example: Key-Value Store

Quick Reference

Signature Modifiers

Field Multiplicity

Relational Operators

Logical Operators

Quantifiers

Temporal Operators (Alloy 6)

Commands