Embedding Rules

alloy:model(name) is a fragment belonging to the logical model name. Fragments with the same model name are combined in document order into a single logical model.

Only the first fragment may contain a module declaration.

When a model block contains a check statement for an assertion, the reference is implicit — no separate directive is needed. The check result is automatically displayed as a status badge in the HTML report.

Formal Properties

specdown's own document model provides a worked example. Every executable unit belongs to exactly one heading scope, and no two heading scopes can share an executable unit.

module docmodel

sig Heading {}

sig Block {
  scope: one Heading
}

sig TableRow {
  scope: one Heading
}

The one multiplicity on scope already guarantees single ownership, so the following assertions are provably true by construction. In a real project you would model properties that are not obvious from the signature alone — this example is deliberately simple to introduce the syntax.

assert blockBelongsToOneScope {
  all b: Block | one b.scope
}

check blockBelongsToOneScope for 5

assert rowBelongsToOneScope {
  all r: TableRow | one r.scope
}

check rowBelongsToOneScope for 5

Scoped Checks with but Clauses

Alloy's check command supports type-specific scope overrides via but clauses — for example, check foo for 5 but 6 Int sets the default scope to 5 but widens the integer bitwidth to 6 bits.

This is essential when a model uses integer values outside the default 4-bit range (-8 to 7).

module scoring

sig Player {
  score: one Int
}

fact validScores {
  all p: Player | p.score >= 0 and p.score <= 21
}

assert scoreBound {
  all p: Player | p.score >= 0 implies p.score <= 21
}

check scoreBound for 3 but 6 Int

Without but 6 Int, Alloy's default 4-bit integers only cover -8 to 7, which cannot represent values like 10 or 21. The wider bitwidth lets the solver explore the full range declared in the fact.

Combination Rules

Fragments with the same model name are merged into a single virtual .als file. Source mapping comments are inserted into the generated model.

A module declaration in a subsequent fragment is a compile-time error.

Model Reference

An explicit alloy:ref directive links a section to a check result defined in a different section. This is useful for cross-section references.

> alloy:ref(access#privateIsolation, scope=5)

The directive displays as a badge in the HTML report and links to a counterexample artifact on failure.

A dry-run must recognize alloy:ref directives as alloy checks.

State Machine Models

Alloy is especially useful for modeling state machines where exhaustive path coverage by example is impractical.

This example models a traffic light with valid transitions only. Alloy proves that an invalid transition (Green → Red) cannot happen.

module traffic

abstract sig Color {}
one sig Red, Yellow, Green extends Color {}

sig Light {
  color: one Color
}

pred validTransition[from, to: Color] {
  from = Red implies to = Green
  from = Green implies to = Yellow
  from = Yellow implies to = Red
}

assert noGreenToRed {
  all from, to: Color |
    validTransition[from, to] implies not (from = Green and to = Red)
}

check noGreenToRed for 5

Counterexample Artifacts

When an Alloy check fails, specdown writes a counterexample artifact to .artifacts/specdown/counterexamples/. The AlloyCheckResult in the JSON report includes a counterexamplePath field pointing to this file.

On failure, the message field includes a counterexample summary extracted from the Alloy solver output.

The JSON report includes a counterexamplePath for the failing check.

The counterexample artifact file exists on disk.