Alloy Specification Language
Table of Contents
1. Introduction
Alloy is a formal specification language for software modeling, based on first-order relational logic with transitive closure.
1.1. Key Characteristics
- Declarative relational modeling
- Bounded model checking (SAT-based)
- Automatic counterexample generation
- Small scope hypothesis
3. Core Concepts
3.1. Signatures and Relations
Ran this exact model through the Alloy Analyzer API directly (the local alloy.jar, AlloyTools 5.1.0, via CompUtil.parseEverything_fromFile + TranslateAlloyToKodkod.execute_command, SAT4J solver). It parses, typechecks, and ~run {} for 5~ returns a satisfiable instance -- the signature/relation/fact syntax is correct and =fact acyclic= is not over-constrained to UNSAT.
sig Node {
edges: set Node
}
sig Graph {
nodes: set Node
}
fact acyclic {
no n: Node | n in n.^edges
}
4. Bounded Model Checking
Decompiled the bundled alloy.jar (AlloyTools 5.1.0, same distribution as this machine's ~/bin/alloy) and read A4Options.java directly: ~public SatSolver solver = SatSolver.SAT4J;~ -- SAT4J (pure Java) is the default solver, not MiniSat. MiniSat is bundled only as an optional native JNI solver (MiniSatJNI, libminisat.so), alongside Glucose, Lingeling, and CryptoMiniSat. Relabeled the diagram node to name the actual default.
6. Example: Redirect Termination
Ran the model directly (local alloy.jar, AlloyTools 5.1.0, via CompUtil/TranslateAlloyToKodkod, SAT4J solver). ~check AllRedirectsTerminate for 10~ returns satisfiable=true: a counterexample exists, =RedirectMap{URL$0->URL$1, URL$1->URL$0}=, a two-URL redirect loop. Nothing in the model constrains =redirect= to be acyclic, so the assertion is false as written, not proven. Reworded the section intro and added the actual check result below.
Checking whether a web redirect chain always terminates.
6.1. Model
sig URL {}
sig RedirectMap {
redirect: URL -> lone URL
}
pred terminates[m: RedirectMap] {
no u: URL | u in u.^(m.redirect)
}
assert AllRedirectsTerminate {
all m: RedirectMap | terminates[m]
}
check AllRedirectsTerminate for 10
Running this check in the Alloy Analyzer finds a counterexample at scope 10:
two URLs redirecting to each other. The model never restricts redirect to
be acyclic, so an instance with a loop is valid, and the assertion fails. A
model that actually proves termination needs an added fact ruling out
cycles:
fact acyclicRedirects {
all m: RedirectMap | no u: URL | u in u.^(m.redirect)
}
Verified: adding this fact to the model makes the check return UNSAT (no counterexample) at the same scope.
7. Resources
- Alloy Analyzer
- Alloy Tutorial
- Software Abstractions (Jackson, 2012)
- TLA+ Traffic Lights and Communication Protocol — the same small-model approach in TLA+, checked with TLC