Precise behavioral models · Formal modeling language
Alloy
Explore structures and counterexamples described by relational constraints.
What it helps you do
Test whether an intended property actually follows from a set of modeled relationships and constraints.
Starting knowledge: Comfort with sets, relations, and logical constraints helps.
- Define entities and relations precisely.
- Separate facts that constrain every instance from assertions you want to check.
- State the analysis scope and inspect any counterexample.
The problem it came from
Daniel Jackson and collaborators developed Alloy in MIT’s Software Design Group. Its language draws on relational logic and related formal-modeling traditions.
The Alloy Analyzer searches for structures satisfying a model and counterexamples to assertions within a configured scope. The current language also supports temporal modeling; this entry uses a small structural example.
Work through an example
sig Participant {}
sig Workshop {}
sig Registration {
participant: one Participant,
workshop: one Workshop
}
assert NoDuplicatePair {
all disj a, b: Registration |
a.participant != b.participant or a.workshop != b.workshop
}
check NoDuplicatePair for 3- Exactly one participant per registration does not imply one registration per participant/workshop pair.
- The assertion is a property to investigate, not an added fact.
- This source example has not been executed by this website; run it in the Analyzer to inspect its result.
Where it helps. Where it stops.
Use it when
- A data or access model has interacting relationships.
- A claim about uniqueness, ownership, or reachability needs a concrete counterexample search.
Potential benefits
- Small generated structures can make a design flaw tangible.
- An assertion separates a desired property from rules that actually imply it.
Limits and common mistakes
- A bounded search without a counterexample is not an unrestricted proof.
- Putting the desired outcome into a fact can make an assertion pass without testing the intended design.
The prompt below asks for this structure. It does not guarantee accuracy, complete coverage, better learning, or conformance to a standard. Treat those outcomes as separate checks.
Practise the judgment
Try a choice, inspect a boundary, then explain a case yourself. Hints and answers are available whenever you need them.
What does “each registration has one participant” fail to establish?
Hint
Distinguish cardinality within a record from uniqueness across records.
Explained answer
Best answer for this case: Uniqueness of the participant/workshop pair across registrations
Two distinct registrations can still refer to the same participant and workshop.
Why not simply add NoDuplicatePair as a fact before checking it?
Hint
Separate assumptions from claims.
Explained answer
Best answer for this case: It would assume the property being investigated
A fact restricts possible models. Assuming the desired conclusion can remove the counterexamples you intended to discover.
Explain what a counterexample with two registrations for one pair would teach you.
Hint
What exactly does the structure demonstrate?
Explained answer & self-review rubric
The existing constraints allow duplicates even though the assertion forbids them. Add or redesign the intended uniqueness constraint, then check whether the implementation enforces it. The counterexample concerns the model, not automatically the deployed database.
- Interpret the violated assertion
- Identify the missing constraint
- Separate model and implementation
Take it into your own work
Manual template
Use this structure yourself, with a colleague, or in your preferred writing tool.
# Relational model
Entities and relations:
Facts / required constraints:
Assertion to investigate:
Scope and time bounds if applicable:
Expected interesting instances:
Analyzer version and actual result:
Counterexample interpretation:
Implementation assumptions:
Review the result
- Is the property tested as an assertion rather than assumed as a fact?
- Is the search scope explicit?
- Does the model include the relationship that can violate the property?
Use this approach with your own AI tool
Help me apply Alloy to the material below.
Reader and existing knowledge: [describe]
Task and desired outcome: [describe]
Use these principles: Define entities and relations precisely.; Separate facts that constrain every instance from assertions you want to check.; State the analysis scope and inspect any counterexample..
Preserve source facts, identifiers, quantities, conditions, exceptions, and uncertainty.
Separate supplied facts from assumptions. Ask for missing information instead of inventing it.
Explain your representation choices and provide a review checklist. Do not claim formal compliance or correctness from formatting alone.
Material: [paste only information you are permitted to share]Go to the source
History and the underlying approach are grounded in these references. Examples, prompts, and practice cases here are original educational adaptations. Edition-specific details should be checked against the referenced publication.
Last editorial review: 2026-10-24. An overview is not certification, and this guide is not a reproduction of a standard.