alloy-more

name	alloy-more
description	Write, review, and validate formal specifications of system designs, state machines, protocols, and algorithms using the Alloy 6 modeling language (more details)
license	MIT
metadata	{"domain":"formal-methods","language":"alloy"}

Alloy Formal Modeling Skill

1. Purpose and When to Use

Load this skill when the user wants to:

• Model a system design, data structure, state machine, protocol, or algorithm formally
• Review, debug, or extend an existing .als specification
• Review, debug, or extend an existing .md file that contains alloy code blocks
• Check properties such as safety invariants, liveness conditions, or protocol correctness
• Explore design alternatives via bounded model checking

What is Alloy

Alloy is a formal modeling language. Its core principle is everything is a relation -- signatures, fields, and variables are all mathematical relations (sets of tuples). The Alloy Analyzer performs bounded model checking by translating specifications to SAT problems and searching for instances or counterexamples within a finite scope. Alloy 6 adds native support for behavioral modeling with mutable state and linear temporal logic (LTL).

Reference: Practical Alloy and alloytools.org.

---

2. Workflows

2.1 Writing a New Specification

Follow these steps when authoring an Alloy model from scratch:

1. Understand the domain. Ask about entities, relationships, invariants, and whether the system has dynamic behavior (state changes over time).
2. Choose the modeling approach.
   • Structural only: static relationships, constraints, and properties (no var).
   • Behavioral: mutable state with temporal logic (uses var, always, eventually, events).
3. Write the structural skeleton. Declare signatures and fields with explicit multiplicities. Add facts for domain constraints.
4. Validate early. Add a run {} command and mentally trace through the expected instances after every structural addition. If the Analyzer is available, run it.
5. If behavioral: add var declarations, an init predicate, event predicates (each with guard, effect, and frame conditions), a stutter predicate, and a transitions fact.
6. Write properties. Express safety as assert { always P } and liveness as assert { fairness implies eventually P }.
7. Add check commands with appropriate scopes and expect annotations to document expected outcomes.
8. Run the Analyzer if available (see Section 8).

2.2 Reviewing an Existing Specification

When reviewing .als files, check for these issues categorized by severity:

Critical (likely bugs):

• Missing frame conditions in event predicates (unmaintained var relations change freely)
• Missing stuttering event in the transitions disjunction
• Liveness assertions without fairness assumptions (likely vacuously satisfied)
• always P where after always P was intended (contradicts current state)

Structural issues:

• Over-constrained facts making the spec unsatisfiable -- run run {} to verify non-trivial instances exist
• Insufficient scope on check commands (default 3 atoms / 10 steps may hide bugs)
• Use of util/ordering where flexible scope is needed (it forces exact scope)
• Scope inheritance surprises (singleton one sig consuming parent scope budget)

Subtle issues:

• Subset in operator vacuously true when LHS is empty -- use some X & Y instead
• Quantifying over mutable sets outside always (evaluates only at initial state)
• Implicit field multiplicity (always write one, set, etc. explicitly)

---

3. Alloy 6 Language Reference

3.1 Signatures and Fields

Signatures declare sets of atoms. Fields declare relations between signatures.

// Signature modifiers:
sig Object {}                        // top-level signature
abstract sig Object {}               // abstract: must be partitioned by extensions
one sig Root extends Dir {}          // singleton: exactly one atom
some sig Config {}                   // at least one atom
lone sig Optional {}                 // zero or one atom

// Extension hierarchy (disjoint partitioning):
abstract sig Object {}
sig Dir extends Object {
  entries : set Entry                 // zero or more Entries per Dir
}
sig File extends Object {}           // disjoint from Dir

// Fields as relations:
sig Entry {
  object : one Object,               // exactly one Object per Entry
  name   : one Name                  // exactly one Name per Entry
}

Subset signatures (non-disjoint subsets, declared with in):

sig uploaded in File {}              // subset of File, not necessarily disjoint
sig trashed in uploaded {}           // subset of uploaded
sig A in B + C {}                    // subset of the union B + C

Mutable declarations (Alloy 6 -- value changes across states):

var sig uploaded in File {}          // mutable subset signature
sig Node {
  succ : one Node,                   // immutable field
  var inbox : set Id,                // mutable field
  var outbox : set Id                // mutable field
}

Higher-arity fields (ternary and beyond):

sig Node {
  var inbox : Type -> Node           // ternary: Node -> Type -> Node
}

Signature facts (constraints scoped to each atom of the signature):

sig Dir extends Object {
  entries : set Entry
} {
  all disj e1, e2 : entries | e1.name != e2.name   // implicit `this`
}

Field multiplicities:

Keyword	Meaning
one	Exactly one target per source atom
lone	Zero or one target
some	One or more targets
set	Zero or more targets (unrestricted)

Always state multiplicity explicitly, even when one is the default.

3.2 The Many Uses of disj

The disj keyword appears in four distinct contexts in Alloy:

1. In quantifiers -- bind distinct variables:

all disj x, y : Key | no x.lock & y.lock
// x and y are always different Key atoms

This replaces the verbose all x, y : Key | x != y implies ... pattern.

2. On field declarations -- injectivity constraint:

sig Key {
  lock : disj some Lock
}
// No two Keys share a Lock. Equivalent to:
//   all disj x, y : Key | no x.lock & y.lock
// If lock is var, this holds in every state.

3. Between field names -- per-atom disjointness:

sig Key {
  disj lock, lock2 : one Lock
}
// For each Key atom, lock and lock2 map to different Lock atoms.

4. As a predicate -- n-way disjointness test:

all disj x, y, z, w : Key |
  disj[x.lock, y.lock, z.lock, w.lock]
// disj[] accepts any number of arguments.

3.3 Relational Logic Operators

Set operators (operands must have the same arity):

Operator	Meaning
+	Union
&	Intersection
-	Difference

Relational operators:

Operator	Name	Notes
.	Dot-join (composition)	n-ary . m-ary = (n+m-2)-ary; cannot compose two unary
[]	Box join	R[S] = S.R (alternative syntax)
->	Cartesian product	Builds higher-arity relations
~	Transpose	Binary relations only
^	Transitive closure	Binary relations only
*	Reflexive-transitive closure	*R = ^R + iden
<:	Domain restriction	Left operand must be unary
:>	Range restriction	Right operand must be unary
++	Override	Same arity; replaces tuples matching first column

Dot-join examples (the most important operator):

e.name            // name of entry e (forward navigation)
d.entries         // set of entries in directory d
entries.e         // set of directories containing entry e (backward)
d.entries.object  // objects in entries of d (chained)
Entry.name        // all names of all entries (join on entire sig)

Atomic formulas (cardinality checks on expressions):

Keyword	Meaning
no R	R is empty (zero tuples)
some R	R is non-empty
lone R	R has at most one tuple
one R	R has exactly one tuple

Comparison formulas:

Operator	Meaning
R in S	R is a subset of S (vacuously true if R is empty)
R = S	R equals S
R != S	R does not equal S

Boolean connectives:

Symbol	Keyword	Meaning
!	not	Negation
&&	and	Conjunction
||	or	Disjunction
=>	implies	Implication (optional else clause)
<=>	iff	Biconditional

P implies Q else T means (P and Q) or (not P and T).

Quantifiers:

Quantifier	Meaning
all x : S | F	F true for every x in S
some x : S | F	F true for at least one x in S
no x : S | F	F false for all x in S
lone x : S | F	F true for at most one x in S
one x : S | F	F true for exactly one x in S

Quantifiers can range over any expression, not just signatures:

all d : Dir, disj x, y : d.entries | x.name != y.name

Other expression constructs:

• let name = expr | formula -- name a sub-expression
• { x : S | F } -- set comprehension (builds a relation)
• { x : A, y : B | F } -- multi-variable set comprehension (binary relation)

Predefined relations:

Relation	Meaning
none	Empty unary set
univ	Set of all atoms
iden	Identity relation on univ (all atoms to themselves)

To restrict iden to a signature: A <: iden or iden & (A -> A).

Operator precedence (highest to lowest):

1. Unary: ~, ^, *, !/not, no/some/lone/one (on expressions)
2. Dot-join: .
3. Box join: []
4. Restriction: <:, :>
5. Arrow product: ->
6. Override: ++
7. Intersection: &
8. Union/difference: +, -
9. Comparison: in, =, !=, <, >, =<, >=
10. Negation: not, !
11. Conjunction: and, &&
12. Implication: implies/=> (with optional else)
13. Biconditional: iff, <=>
14. Quantifiers: all, some, no, lone, one
15. Let: let
16. Temporal sequence: ; (lowest precedence)

3.4 Facts, Predicates, Functions, Assertions

// Fact: always assumed true, constrains all instances
fact no_shared_entries {
  all e : Entry | lone entries.e
}

// Predicate: reusable named formula, true only when invoked
pred reachable [o : Object] {
  o in Root + Root.^(entries.object)
}

// Function: reusable named expression returning a relation
fun descendants [o : Object] : set Object {
  o.^(entries.object)
}

// Assertion: property to verify (negated internally by check)
assert no_partitions {
  all o : Object | reachable[o]
}

3.5 Commands

Two forms:

// Inline constraint
run show { some Dir } for 4
check safety { always some_property } for 6

// Named reference (predicate or assertion)
run reachable for 4
check no_partitions for 6

Pitfall: check no_partitions {} checks the empty constraint (always true), NOT the assertion. Omit the braces: check no_partitions.

Scope syntax:

Syntax	Meaning
for N	Default scope of N atoms per top-level signature (default: 3)
for N but M Sig	Override scope for specific signature
for N but exactly M Sig	Exact scope (not upper bound)
for 3 Object, 2 Name	All scopes specified explicitly
for N but K steps	Bound trace prefix to K steps (default: 10)
for N but 1.. steps	Unbounded temporal model checking

Documenting expected outcomes:

check bad_property for 6 expect 1    // expect counterexample found
check good_property for 6 expect 0   // expect no counterexample

Scope inheritance rules:

• Overall scope applies to top-level signatures only.
• one sig Root extends Dir consumes 1 atom from Dir's scope budget.
• If all extensions have exact scopes, parent scope auto-increases to their sum.

3.6 Temporal Operators (Alloy 6)

Future-time operators:

Operator	Meaning
after F	F holds in the next state
always F	F holds in current and all future states
eventually F	F holds in current or some future state
F until G	G becomes true eventually, F holds until then
F releases G	G holds until and including when F becomes true, or G holds forever

Past-time operators:

Operator	Meaning
before F	F held in the previous state (false at state 0)
once F	F held in some past state (including current)
historically F	F held in all past states (including current)
F since G	G was true at some past point, F has held since
F triggered G	G has held since F was last true, or G has always held

Prime operator: expr' evaluates expr in the next state. Equivalent to after expr. Double prime '' means two states ahead.

Sequence operator: P ; Q means P and after Q. Lowest precedence of all operators. Useful for encoding trace scenarios.

Key rules:

• Top-level formulas (outside temporal operators) are evaluated at state 0.
• Past-time operators at the top level degenerate: historically P at state 0 is just P.
• Past-time operators are only useful inside future-time operators (e.g., always (... once ...)).
• before is always false at state 0.
• Alloy traces are infinite (finite behavior is modeled via stuttering self-loops).

3.7 Module System

module mymodule                      // optional module declaration

open util/ordering[Id]               // import with type parameter
open util/relation as rel            // import with alias
open mylib/graph[Node]               // parametrized module instantiation

Parametrized modules:

module graph[node]
pred dag [r : node -> node] {
  all n : node | n not in n.^r
}

Import with: open graph[Object].

Private declarations:

private one sig Aux { helper : A -> B }

Private elements are inaccessible from importing modules.

Standard library modules:

• util/ordering[T] -- provides first, last, next, lt, gt, etc. Caveat: forces exact scope on T.
• util/relation -- dom, ran, total, surjective, etc.
• util/graph[T] -- graph predicates.

3.8 Reserved Keywords

These identifiers cannot be used as signature, field, predicate, or function names. Using them produces cryptic parse errors.

Category	Keywords
Declarations	sig, extends, in, abstract, one, lone, some, var, enum
Definitions	pred, fun, fact, assert, let
Commands	run, check, for, but, expect, exactly, steps
Logical	all, no, not, and, or, implies, else, iff, disj
Temporal	always, eventually, after, before, until, releases, since, triggered, once, historically
Relational	set, seq, none, univ, iden, Int
Modules	module, open, as, private

Common trap: seq is reserved (it refers to Alloy's sequence type). If you need a "sequence number" field, use seqNum, seqNo, or idx instead.

// WRONG: parse error
sig Event { seq : one Int }

// RIGHT: rename to avoid the reserved word
sig Event { seqNum : one Int }

---

4. Specification Styles

Alloy supports three specification styles. Prefer navigational as the default.

Navigational style (preferred): Minimal quantification, heavy use of . for relation navigation.

// "Every entry belongs to at most one directory"
all e : Entry | lone entries.e

Pointwise / first-order style: Explicit quantification over individual atoms and tuple membership.

// Same constraint, pointwise:
all x, y : Dir, e : Entry |
  x->e in entries and y->e in entries implies x = y

Pointfree style: No quantifiers at all; purely relational operators.

// Same constraint, pointfree:
entries.~entries in iden

Pointfree is elegant but often opaque. Use it only when the navigational form is more complex.

---

5. Canonical Patterns and Idioms

5.1 Structural Patterns

Reachability via transitive closure:

fun descendants [o : Object] : set Object {
  o.^(entries.object)         // transitive closure of navigation
}
fun allReachable : set Object {
  Root.*(entries.object)      // reflexive-transitive: includes Root itself
}

Override pattern (updating a relation for one key):

entries' = entries ++ (d -> newEntries)
// Replaces d's entries, keeps all other directories' entries unchanged

Total ordering without util/ordering (avoids exact scope limitation):

sig Node {
  next : lone Node
}
one sig first, last in Node {}
fact ordering {
  no next.first           // nothing precedes first
  no last.next            // nothing follows last
  Node - first in first.^next  // all nodes reachable from first
}

5.2 Behavioral Modeling Template

The canonical structure for any behavioral Alloy model:

// --- State ---
var sig uploaded in File {}
sig File {
  var shared : set Token
}

// --- Initial state ---
pred init {
  no uploaded
  all f : File | no f.shared
}

// --- Events (each has guard + effect + frame conditions) ---
pred upload [f : File] {
  // Guard
  f not in uploaded
  // Effect
  uploaded' = uploaded + f
  // Frame conditions (EVERY other mutable relation)
  shared' = shared
}

// --- Stuttering (mandatory) ---
pred stutter {
  uploaded' = uploaded
  shared' = shared
}

// --- Transition system ---
fact transitions {
  init and always (
    (some f : File | upload[f])
    or (some f : File | delete[f])
    or stutter
  )
}

Frame condition discipline: Every event predicate must explicitly state relation' = relation for every mutable relation it does not modify. Omitting a frame condition leaves the relation unconstrained -- the most common source of bugs.

Stuttering is mandatory. It ensures:

1. Composability with concurrent systems
2. Finite behaviors extend to infinite traces (required by Alloy's semantics)
3. Deadlocked states do not make liveness properties vacuously true

5.3 Protocol Design Patterns

Ring topology:

sig Node {
  succ : one Node
}
fact ring {
  all n : Node | Node in n.^succ
}

Messages as tuples (recommended approach):

abstract sig Type {}
one sig Candidate, Elect extends Type {}

sig Node {
  succ : one Node,
  var inbox : Type -> Node    // each tuple IS a message
}

No message atoms needed. No scope issues. Order-of-magnitude faster analysis. Use this when message structure is simple (1-2 fields).

Messages as signatures (when messages have complex structure):

abstract sig Message { payload : one Node }
sig CandidateMsg, ElectedMsg extends Message {}

Requires generator axioms and uniqueness to avoid scope problems:

fact generator {
  all n : Node | some m : CandidateMsg | m.payload = n
  all n : Node | some m : ElectedMsg | m.payload = n
}
fact unique {
  all disj m1, m2 : CandidateMsg | m1.payload != m2.payload
  all disj m1, m2 : ElectedMsg | m1.payload != m2.payload
}

Derived state via temporal functions (eliminates frame conditions for computed properties):

fun Elected : set Node {
  { n : Node | once (before (some (Elect -> n) & n.inbox)
                     and no (Elect -> n) & n.inbox) }
}

5.4 Verification Patterns

Safety (something bad never happens):

assert shared_are_accessible {
  always (shared.Token in uploaded - trashed)
}
check shared_are_accessible for 5

Liveness (something good eventually happens -- requires fairness):

pred fairness {
  all n : Node |
    (eventually always enabled[n]) implies
    (always eventually acts[n])
}
assert eventually_elected {
  fairness implies eventually (some Elected)
}
check eventually_elected for 4 but 20 steps

Undo property:

assert restore_undoes_delete {
  all f : File | always (
    delete[f] and after restore[f] implies
    uploaded'' = uploaded and trashed'' = trashed
  )
}

One-shot property:

assert single_download {
  all t : Token | always (
    download[t] implies after always not download[t]
  )
}

Releases pattern (action blocked until precondition recurs):

assert empty_after_restore {
  all f : File | always (
    delete[f] implies
    after ((restore[f] or upload[f]) releases not delete[f])
  )
}

Inductive invariant (dramatically faster than unbounded temporal check):

pred inv { shared.Token in uploaded - trashed }

// Refactor init and transitions as predicates (not facts) for induction
pred next {
  (some f : File | upload[f]) or
  (some f : File | delete[f]) or
  stutter
}

assert initiation { init implies inv }
assert preservation { (inv and next) implies after inv }

check initiation for 10 but 1 steps
check preservation for 10 but 2 steps

When to prefer the inductive approach:

• When the model uses integer arithmetic (Int fields, plus, minus, mul). Temporal checks with integers are extremely expensive because the SAT encoding multiplies bitwidth across every step. A check at scope 3 with 5-bit integers and 10 steps can easily time out (5+ minutes), while the equivalent inductive check at scope 10 with 2 steps finishes in seconds.
• When temporal checks time out at reasonable scopes. The inductive approach reduces a temporal safety property to two small bounded checks: initiation (1 step) proves the invariant holds initially, and preservation (2 steps) proves any single transition preserves it. Together they imply the property holds at all reachable states.
• Integer scope note: for N Int means N bits (including sign bit), not N atoms. 5 Int gives the range -16..15. Always set integer bitwidth wide enough to avoid silent overflow.

5.5 Event Depiction Idiom

Makes events visible in the Analyzer's trace visualizer.

enum Event { UploadEv, DeleteEv, RestoreEv, StutterEv }

fun upload_happens : Event -> File {
  { e : UploadEv, f : File | upload[f] }
}
fun delete_happens : Event -> File {
  { e : DeleteEv, f : File | delete[f] }
}
fun stutter_happens : set Event {
  { e : StutterEv | stutter }
}

// Aggregate for visualization and transition simplification
fun events : set Event {
  stutter_happens +
  (upload_happens + delete_happens).File
}

// Simplify the transitions fact:
fact transitions { init and always some events }

// Check mutual exclusion of events:
check at_most_one { always lone events } for 3

No performance penalty -- derived functions are only computed during visualization unless referenced in formulas.

5.6 Encoding Trace Scenarios

Use the ; (sequence) operator to describe specific execution traces:

Event-oriented style (simplest):

run scenario {
  some f : File, t : Token {
    upload[f] ; share[f, t] ; download[t] ; delete[f] ; always stutter
  }
} for 1 File, 1 Token

State-oriented style (most precise):

run scenario {
  some f : File, disj t0, t1 : Token {
    File = f and Token = t0 + t1
    no uploaded ; uploaded = f ; uploaded = f ; always no uploaded
    no shared   ; no shared    ; shared = f->t0 ; always no shared
  }
} for 1 File, 2 Token

Always constrain the tail of the trace (e.g., always stutter) to prevent unexpected continuations.

---

6. Common Pitfalls

Pitfall 1: Missing frame conditions

Unmaintained mutable relations change arbitrarily between states.

// WRONG: shared can change freely during upload
pred upload [f : File] {
  f not in uploaded
  uploaded' = uploaded + f
}

// RIGHT: explicitly preserve all other mutable relations
pred upload [f : File] {
  f not in uploaded
  uploaded' = uploaded + f
  trashed' = trashed
  shared' = shared
}

Pitfall 2: Missing stuttering in transitions

Without stuttering, deadlocked states have no valid infinite continuations, making the entire specification vacuously true for properties about those states.

// WRONG: deadlock if no event is enabled
fact transitions {
  init and always (some f : File | upload[f] or delete[f])
}

// RIGHT: always include stutter
fact transitions {
  init and always (
    (some f : File | upload[f] or delete[f])
    or stutter
  )
}

Pitfall 3: always P when you mean after always P

Inside an event predicate, always P includes the current state, which may contradict the event's own effect.

// WRONG: says download[t] is false NOW (contradicts itself)
pred download [t : Token] {
  ...
  always not download[t]
}

// RIGHT: prohibition starts in the next state
pred download [t : Token] {
  ...
  after always not download[t]
}

Pitfall 4: Liveness without fairness

Liveness properties are trivially satisfied by infinite stuttering unless fairness excludes it.

// WRONG: satisfied by never doing anything
assert progress { eventually some uploaded }
check progress

// RIGHT: add fairness as a premise
pred fairness { always eventually (some f : File | upload[f]) or no (File - uploaded) }
assert progress { fairness implies eventually some uploaded }
check progress

Pitfall 5: Over-constrained facts

Adding too many constraints can make the specification unsatisfiable, causing all check commands to trivially pass (no counterexample can exist if no instance exists).

// Always validate satisfiability after modifying facts:
run sanity_check {} for 5
// If this finds no instance, the spec is over-constrained.

Pitfall 6: Insufficient scope

The default scope of 3 atoms and 10 steps may hide counterexamples.

// Passes at scope 3, fails at scope 5:
check no_partitions for 3        // no counterexample (false confidence)
check no_partitions for 5        // counterexample found!

// For liveness, increase step bound:
check liveness_prop for 4 but 30 steps

Pitfall 7: util/ordering forces exact scope

open util/ordering[Id] forces the scope of Id to be exact, preventing analysis at smaller sizes.

// If flexible scope matters, declare ordering manually:
sig Id {
  next : lone Id
}
one sig first, last in Id {}
fact ordering {
  no next.first
  no last.next
  Id - first in first.^next
}

Pitfall 8: Quantifying over mutable sets outside always

Top-level formulas are evaluated at state 0 only.

// WRONG: Elected is likely empty at state 0
all n : Elected | some n.inbox

// RIGHT: place inside always so it re-evaluates each state
always (all n : Elected | some n.inbox)

Pitfall 9: Subset in is vacuously true when LHS is empty

The in operator means subset, not membership. An empty set is a subset of everything.

// WRONG: true even when Root has zero atoms (lone sig)
Root in Dir

// RIGHT: use intersection to test non-empty overlap
some Root & Dir

// Or be explicit about non-emptiness:
some Root and Root in Dir

Pitfall 10: Not validating after modifying facts

After strengthening any fact, always run an unconstrained run command to ensure the specification is still satisfiable.

// Add this as a standing validation command:
run show {} for 5

If the Analyzer reports "No instance found" for an unconstrained run, the facts are contradictory.

Pitfall 11: Higher-order quantification is not supported

Alloy's SAT-based analyzer only supports first-order quantification -- quantifying over individual atoms. Quantifying over sets of atoms (some x : set Sig | ...) is second-order and triggers a "cannot skolemize" error or silent analysis failure.

// WRONG: higher-order quantification (quantifying over sets)
pred step [s : Sim] {
  some newEvents : set Event |
    newEvents = processAction[s]
}

// RIGHT: restructure to avoid set-valued quantification
// Option A: use lone/one if at most one result
pred step [s : Sim] {
  some newEvent : Event |
    newEvent = processAction[s]
}

// Option B: use a helper signature to hold the set
sig ActionResult {
  produced : set Event
}
pred step [s : Sim, ar : ActionResult] {
  ar.produced = processAction[s]
}

// Option C: use lone when "zero or one" suffices
sig ActionResult {
  descriptor : lone EventDescriptor
}

Rule of thumb: If you find yourself writing some x : set Sig, redesign the model. Introduce a helper signature with a set-valued field, or decompose the logic so each quantified variable binds a single atom.

Pitfall 12: after is a formula operator, not an expression operator

The temporal operator after applies only to formulas (boolean). It cannot wrap a function call or relational expression. Use the prime operator (') to get next-state values of expressions.

fun peekNext [s : Sim] : lone Event {
  { e : s.queue | e.time = min[s.queue.time] }
}

// WRONG: after cannot wrap a fun call (expression)
pred peek_stable [s : Sim] {
  after peekNext[s] = peekNext[s]
}

// RIGHT: use primed relations inside a set comprehension
pred peek_stable [s : Sim] {
  { e : s.queue' | e.time = min[s.queue'.time] }
  =
  { e : s.queue | e.time = min[s.queue.time] }
}

// Also RIGHT: use after on the whole formula
pred peek_stable [s : Sim] {
  after (peekNext[s] = peekNext[s])
}
// But note: this compares next-state with next-state (both shifted),
// which is a tautology. See Pitfall 14 for this subtlety.

Summary: after F where F is a formula -- valid. after expr where expr returns a relation -- parse error. Use expr' (prime on the mutable relation inside the expression) instead.

Pitfall 13: Predicate branching with conjoined no/some guards

When modeling conditional behavior in a predicate (e.g., "if a field is empty do X, otherwise do Y"), a conjunction of an implication and an existential quantifier over the same field creates an unsatisfiable predicate when the field is empty.

sig ActionResult {
  descriptor : lone EventDescriptor
}

// WRONG: when no ar.descriptor, the `some d` branch is false,
// making the entire conjunction unsatisfiable
pred step [ar : ActionResult] {
  no ar.descriptor implies {
    queue' = queue - currentEvent
  }
  some d : ar.descriptor | {
    queue' = queue - currentEvent + makeEvent[d]
  }
}

// RIGHT: use explicit disjunction with guards inside each branch
pred step [ar : ActionResult] {
  {
    no ar.descriptor
    queue' = queue - currentEvent
  }
  or
  {
    some d : ar.descriptor | {
      queue' = queue - currentEvent + makeEvent[d]
    }
  }
}

Why it fails: some d : ar.descriptor | P is false when ar.descriptor is empty -- there is no d to witness the existential. Conjoining this with no ar.descriptor implies Q means: when the descriptor is absent, Q holds and false -- contradiction. Use or-branches with the guard condition inside each branch.

Pitfall 14: Temporal operators shift evaluation uniformly

All temporal operators (always, eventually, after, until, etc.) shift the evaluation state for all sub-expressions uniformly. There is no way to "freeze" an outer reference at the current state while shifting an inner reference to a future state within a single temporal operator.

sig Sim {
  var curTime : one Int
}

// WRONG: both curTime references evaluate at the SAME future state
// This is the tautology  t > t  which is always false
assert time_advances {
  eventually (Sim.curTime > Sim.curTime)
}

// WRONG: let does NOT help -- the binding is also shifted
assert time_advances {
  let t = Sim.curTime |
    eventually (Sim.curTime > t)
}
// Inside `eventually`, both Sim.curTime and t evaluate at the shifted state

// RIGHT: use after with prime to compare adjacent states
assert time_advances_per_step {
  always (not stutter implies Sim.curTime' > Sim.curTime)
}

// RIGHT: use past-time operators inside future-time context
assert time_advances_past {
  always (not stutter implies Sim.curTime > (before Sim.curTime))
}
// `before` looks back one state from the current evaluation point

Key insight: To compare values across different states, use either: (1) the prime operator (expr' vs expr) to compare adjacent states, or (2) past-time operators (before, once, historically) inside a future-time context to look backward from the shifted evaluation point. Never rely on let bindings or nested temporal operators to "capture" a value from an outer state.

---

7. Complete Examples

Example A: Structural -- File System

A model of a hierarchical file system with directories, files, entries, and names. Demonstrates structural modeling, transitive closure, and property verification.

module filesystem

// --- Signatures ---

abstract sig Object {}

sig Dir extends Object {
  entries : set Entry
}

sig File extends Object {}

one sig Root extends Dir {}

sig Entry {
  object : one Object,
  name : one Name
}

sig Name {}

// --- Facts ---

// Every entry belongs to at most one directory
fact no_shared_entries {
  all e : Entry | lone entries.e
}

// No two entries in the same directory share a name
fact unique_names {
  all d : Dir, disj e1, e2 : d.entries | e1.name != e2.name
}

// Every non-Root object is referenced by exactly one entry
fact no_dangling_objects {
  Entry.object = Object - Root
}

// No object is its own descendant (acyclicity)
fact acyclic {
  all o : Object | o not in descendants[o]
}

// Every object is reachable from Root
fact all_reachable {
  Object = Root + descendants[Root]
}

// --- Functions ---

fun descendants [o : Object] : set Object {
  o.^(entries.object)
}

fun contents [d : Dir] : set Object {
  d.entries.object
}

// --- Predicates ---

pred empty_dir [d : Dir] {
  no d.entries
}

// --- Assertions ---

// The file system has no partitions (everything is connected)
assert no_partitions {
  all o : Object | o in Root + descendants[Root]
}

// Root is never contained in another directory
assert root_is_top {
  no entries.object.Root
}

// --- Commands ---

run show {} for 4
run show_empty { some d : Dir | empty_dir[d] } for 4

check no_partitions for 6 expect 0
check root_is_top for 6 expect 0

Example B: Behavioral -- File Sharing Application

A model of a cloud file sharing app where files can be uploaded, deleted, restored, shared via tokens, and downloaded. Demonstrates mutable state, temporal logic, frame conditions, safety/liveness, and the event depiction idiom.

module filesharing

// --- Signatures ---

sig File {
  var shared : set Token
}

sig Token {}

var sig uploaded in File {}
var sig trashed in uploaded {}

// --- Initial state ---

pred init {
  no uploaded
  no trashed
  no shared
}

// --- Events ---

pred upload [f : File] {
  // Guard
  f not in uploaded
  // Effects
  uploaded' = uploaded + f
  // Frame conditions
  trashed' = trashed
  shared' = shared
}

pred delete [f : File] {
  // Guard
  f in uploaded - trashed
  // Effects
  trashed' = trashed + f
  // Frame conditions
  uploaded' = uploaded
  shared' = shared
}

pred restore [f : File] {
  // Guard
  f in trashed
  // Effects
  trashed' = trashed - f
  // Frame conditions
  uploaded' = uploaded
  shared' = shared
}

pred share [f : File, t : Token] {
  // Guard
  f in uploaded - trashed
  historically t not in File.shared        // token never used before
  // Effects
  shared' = shared + f -> t
  // Frame conditions
  uploaded' = uploaded
  trashed' = trashed
}

pred download [t : Token] {
  // Guard
  some shared.t & (uploaded - trashed)     // file is accessible
  // Effects (no state change -- read-only action)
  uploaded' = uploaded
  trashed' = trashed
  shared' = shared
}

pred empty {
  // Guard
  some trashed
  // Effects
  uploaded' = uploaded - trashed
  trashed' = trashed - trashed             // i.e., no trashed'
  shared' = shared - trashed -> Token      // remove shares of trashed files
}

pred stutter {
  uploaded' = uploaded
  trashed' = trashed
  shared' = shared
}

// --- Transition system ---

fact transitions {
  init and always (
    (some f : File | upload[f] or delete[f] or restore[f])
    or (some f : File, t : Token | share[f, t])
    or (some t : Token | download[t])
    or empty
    or stutter
  )
}

// --- Safety properties ---

assert shared_are_accessible {
  always (shared.Token in uploaded - trashed)
}

assert trashed_are_uploaded {
  always (trashed in uploaded)
}

// --- Liveness properties ---

pred fairness_on_empty {
  (eventually always some trashed) implies
  (always eventually empty)
}

assert trash_eventually_emptied {
  fairness_on_empty implies always eventually no trashed
}

// --- Undo property ---

assert restore_undoes_delete {
  all f : File | always (
    delete[f] and after restore[f] implies
    uploaded'' = uploaded and trashed'' = trashed and shared'' = shared
  )
}

// --- One-shot property ---

assert single_download_per_token {
  all t : Token | always (
    download[t] implies after always not download[t]
  )
}

// --- Event depiction (for visualization) ---

enum Event { UploadEv, DeleteEv, RestoreEv, ShareEv, DownloadEv, EmptyEv, StutterEv }

fun upload_happens : Event -> File {
  { e : UploadEv, f : File | upload[f] }
}
fun delete_happens : Event -> File {
  { e : DeleteEv, f : File | delete[f] }
}
fun restore_happens : Event -> File {
  { e : RestoreEv, f : File | restore[f] }
}
fun share_happens : Event -> File -> Token {
  { e : ShareEv, f : File, t : Token | share[f, t] }
}
fun download_happens : Event -> Token {
  { e : DownloadEv, t : Token | download[t] }
}
fun empty_happens : set Event {
  { e : EmptyEv | empty }
}
fun stutter_happens : set Event {
  { e : StutterEv | stutter }
}

fun events : set Event {
  empty_happens + stutter_happens
  + (upload_happens + delete_happens + restore_happens).File
  + download_happens.Token
  + (share_happens.Token).File
}

// --- Commands ---

run show {} for 3 but 10 steps
run scenario_share_then_delete {
  some f : File, t : Token {
    upload[f] ; share[f, t] ; delete[f] ; download[t] ; always stutter
  }
} for 2 but 8 steps expect 0      // download should fail: file is trashed

check shared_are_accessible for 5 but 15 steps expect 0
check trashed_are_uploaded for 5 but 15 steps expect 0
check restore_undoes_delete for 4 but 10 steps expect 0
check trash_eventually_emptied for 3 but 20 steps

Example C: Protocol -- Leader Election on a Ring

A model of the Chang-Roberts leader election protocol on a unidirectional ring. Demonstrates the messages-as-tuples pattern, derived state via temporal functions, ring topology, safety and liveness with fairness.

module leaderelection

// --- Network topology ---

sig Id {
  gt : set Id                           // manual total order (avoids util/ordering)
}

abstract sig Type {}
one sig Candidate, Elect extends Type {}

sig Node {
  succ : one Node,
  id : one Id,
  var inbox : Type -> Id,
  var outbox : Type -> Id
}

// --- Topology constraints ---

fact ring {
  all n : Node | Node in n.^succ       // succ forms a connected ring
}

fact unique_ids {
  all disj n1, n2 : Node | n1.id != n2.id
}

fact id_ordering {
  all i : Id | i not in i.^gt           // irreflexive
  all disj i, j : Id | i in j.gt or j in i.gt  // total
  all i, j, k : Id | (i in j.gt and j in k.gt) implies i in k.gt  // transitive
}

// --- Derived state ---

// A node is elected when an Elect message bearing its own id
// is consumed from its inbox (was present, now absent).
fun Elected : set Node {
  { n : Node | once (
    before (some (Elect -> n.id) & n.inbox)
    and no (Elect -> n.id) & n.inbox
  )}
}

// --- Initial state ---

pred init {
  no inbox
  no outbox
}

// --- Events ---

pred initiate [n : Node] {
  // Guard: node has not yet sent a candidate message
  historically no (Candidate -> n.id) & n.outbox
  // Effects
  outbox' = outbox + n -> Candidate -> n.id
  inbox' = inbox + n.succ -> Candidate -> n.id
  // (message appears in successor's inbox)
}

pred process [n : Node, t : Type, i : Id] {
  // Guard: message is in inbox
  t -> i in n.inbox
  // Remove from inbox
  let msg_removed = inbox - n -> t -> i |
  let new_outbox = outbox |
  {
    // Candidate message: forward if sender id > my id
    t = Candidate implies {
      i in n.id.gt implies {
        // Sender id is greater: forward the candidate
        inbox' = msg_removed + n.succ -> Candidate -> i
        outbox' = new_outbox + n -> Candidate -> i
      } else i = n.id implies {
        // My own id came back: I am the leader, send Elect
        inbox' = msg_removed + n.succ -> Elect -> i
        outbox' = new_outbox + n -> Elect -> i
      } else {
        // Sender id is smaller: discard
        inbox' = msg_removed
        outbox' = new_outbox
      }
    }
    // Elect message: forward unless it is for me
    t = Elect implies {
      i != n.id implies {
        inbox' = msg_removed + n.succ -> Elect -> i
        outbox' = new_outbox + n -> Elect -> i
      } else {
        // Elect message for me: consume it (triggers Elected)
        inbox' = msg_removed
        outbox' = new_outbox
      }
    }
  }
}

pred stutter {
  inbox' = inbox
  outbox' = outbox
}

// --- Transition system ---

fact transitions {
  init and always (
    (some n : Node | initiate[n])
    or (some n : Node, t : Type, i : Id | process[n, t, i])
    or stutter
  )
}

// --- Safety ---

assert at_most_one_leader {
  always (lone Elected)
}

// The elected node has the highest id
assert leader_has_max_id {
  always (all n : Elected | no n.id.gt & Node.id)
}

// --- Liveness (with fairness) ---

pred fairness {
  // Weak fairness: if a node can always eventually act, it does
  all n : Node |
    (eventually always (
      (historically no (Candidate -> n.id) & n.outbox)   // can initiate
      or some n.inbox                                      // can process
    ))
    implies
    (always eventually (
      initiate[n]
      or (some t : Type, i : Id | process[n, t, i])
    ))
}

assert eventually_a_leader {
  fairness implies eventually (some Elected)
}

// --- Commands ---

run show {} for 3 Node, 3 Id, 2 Type but 15 steps
run show_election {
  eventually some Elected
} for 3 Node, 3 Id, 2 Type but 15 steps

check at_most_one_leader for 4 Node, 4 Id, 2 Type but 20 steps expect 0
check leader_has_max_id for 4 Node, 4 Id, 2 Type but 20 steps expect 0
check eventually_a_leader for 3 Node, 3 Id, 2 Type but 25 steps

---

8. Analyzer Integration

Detection

Check for the Alloy Analyzer in this order:

1. alloy command on PATH
2. org.alloytools.alloy.dist.jar in the project directory or common locations
3. Any alloy*.jar file in the project directory

Invocation

# If alloy CLI is on PATH:
alloy exec <file.als>

# If alloy CLI is on PATH and using a markdown file:
alloy exec <file.md>

# If using the JAR directly:
java -jar <path-to-alloy.jar> <file.als>

# If using the JAR directly and using a markdown file:
java -jar <path-to-alloy.jar> <file.md>

Interpreting Output

Output	Meaning
"Instance found"	run command found a satisfying instance
"No instance found"	run command: spec may be over-constrained
"Counterexample found"	check command: assertion is violated
"No counterexample found"	check command: assertion holds within scope

If the Analyzer is not available: produce the .als file and inform the user to open it in the Alloy Analyzer GUI or install the CLI tool.

---

9. File Conventions

• File extension: .als
• One module per file
• module declaration should match the filename (e.g., module filesystem in filesystem.als)
• Comments: // (line), -- (line), /* ... */ (block)
• Suggest placing specifications in a models/ or alloy/ directory within the project
• Use clear section comments (// --- Signatures ---, // --- Events ---, etc.) to organize the file
• When writing Alloy in a markdown file (.md), the file must start with a YAML header (frontmatter): three dashes on the first line, followed by a title field in YAML format, followed by three more dashes.

---
title: [ModelTitle]
---