MacAlloy is a native macOS IDE for Alloy 6.2, providing a complete formal verification environment without external dependencies. It implements Alloy 6.2 language support with a custom CDCL SAT solver, enabling lightweight formal analysis directly on macOS.
New to Alloy? Start with Alloy Basics to learn the fundamentals, then return here to run your specifications. | Component | Implementation |
|---|
| Parser | Recursive descent parser for Alloy 6.2 syntax |
| Type Checker | Full semantic analysis with symbol table |
| Translator | Kodkod-style relational-to-boolean encoding |
| SAT Solver | Native CDCL solver with VSIDS heuristic |
| Visualizer | Force-directed graph layout for instances |
MacAlloy runs entirely on-device with no network dependencies, making it suitable for air-gapped environments and offline formal verification workflows.
Architecture
MacAlloy follows a classic compiler pipeline architecture, transforming Alloy specifications through successive stages until reaching a SAT problem that can be solved for satisfying instances.
Compilation Pipeline
Lexer: Tokenizes Alloy source into a stream of tokens with full Alloy 6.2 syntax support including temporal operators.
Parser: Recursive descent parser produces an abstract syntax tree (AST) representing the model structure—signatures, fields, facts, predicates, functions, and commands.
Semantic Analyzer: Performs type checking, resolves references, builds the symbol table, and validates that the model is well-formed before translation.
Translator: Converts the high-level relational model into a propositional formula using Kodkod-style encoding techniques.
SAT Solver: Solves the generated CNF formula to find satisfying assignments (model instances) or prove unsatisfiability.
Instance Extractor: Decodes SAT assignments back into Alloy instances with concrete atoms and relations.
SAT Solver Implementation
MacAlloy includes a production-grade CDCL (Conflict-Driven Clause Learning) SAT solver implementing modern solving techniques:
Core Algorithms
Two-Watched Literals: Efficient unit propagation using the two-watched-literal scheme. Each clause maintains two watched literals; only when a watched literal becomes false does the solver examine the clause.
VSIDS Decision Heuristic: Variable State Independent Decaying Sum tracks variable activity based on participation in conflicts. Variables involved in recent conflicts receive activity bumps, with periodic decay to favor recently active variables.
First-UIP Conflict Analysis: When a conflict occurs, the solver analyzes the implication graph to find the First Unique Implication Point—the most recent decision level variable that alone implies the conflict. This generates a learned clause that prevents the same conflict pattern.
Non-Chronological Backtracking: Rather than backtracking one level at a time, the solver jumps directly to the decision level indicated by the learned clause, pruning large portions of the search space.
Luby Restart Sequence: Periodic restarts using the Luby sequence prevent the solver from getting stuck in unproductive regions of the search space while preserving learned clauses.
Solver Characteristics
Propagation: Two-watched literals with lazy update
Decisions: VSIDS with activity decay (0.95)
Learning: First-UIP with clause minimization
Restarts: Luby sequence (base: 100 conflicts)
Deletion: Activity-based clause deletion
Relational Encoding
MacAlloy uses Kodkod-style bounded model finding to translate Alloy’s relational logic into propositional SAT:
Boolean Matrix Representation
Relations are encoded as boolean matrices where each cell represents whether a tuple belongs to the relation:
For relation r: A → B with |A| = 3, |B| = 2
b0 b1
a0 [ x00 x01 ]
a1 [ x10 x11 ]
a2 [ x20 x21 ]
Each xij is a boolean variable: true iff (ai, bj) ∈ r
Relational Operations
The translator implements the full relational algebra:
| Operation | Encoding |
|---|
Union (+) | Disjunction of corresponding matrix cells |
Intersection (&) | Conjunction of corresponding matrix cells |
Difference (-) | Conjunction with negation |
Join (.) | Existential quantification over shared column |
Product (→) | Cartesian product of matrices |
Transpose (~) | Matrix transposition |
Transitive Closure (^) | Iterative squaring up to scope bound |
Reflexive-Transitive Closure (*) | Closure plus identity relation |
Multiplicity Constraints
Alloy’s multiplicity keywords translate to cardinality constraints:
one r → exactly one tuple in r → EO encoding
some r → at least one tuple in r → OR of all cells
lone r → at most one tuple in r → AMO encoding
no r → no tuples in r → AND of negated cells
Temporal Logic Support
MacAlloy implements Alloy 6’s temporal extension with full LTL (Linear Temporal Logic) support:
Trace Semantics
Temporal models are verified over traces—infinite sequences of states represented as lassos (finite prefix + repeating suffix):
State₀ → State₁ → State₂ → State₃ → State₄
↑__________|
(loop back)
Temporal Operators
Future Operators:
after / X — in the next statealways / G — in all future stateseventually / F — in some future stateuntil / U — holds until another property holdsreleases / R — dual of until
Past Operators:
before — in the previous statehistorically — in all past statesonce — in some past statesince — held since another property heldtriggered — dual of since
Temporal Encoding
Temporal formulas are unrolled over a bounded number of steps with loop detection:
var sig Active in Process {}
fact SomeoneAlwaysActive {
always some Active
}
run {} for 5 Process, 10 steps
steps bound controls trace length. The solver searches for a lasso-shaped trace satisfying all temporal constraints.
Instance Visualization
MacAlloy provides interactive visualization of satisfying instances:
Force-Directed Layout
Instances are rendered as graphs using force-directed placement:
- Atoms appear as labeled nodes
- Relations appear as directed edges between nodes
- Signatures determine node styling and grouping
Trace Visualization
For temporal models, the trace viewer provides:
- Step-by-step state navigation
- Playback controls for animation
- Visual diff highlighting between states
- Loop point indication
IDE Features
Editor
- Syntax highlighting for Alloy 6.2 with customizable themes
- Real-time error underlining as you type
- Severity-based error indicators:
- Red squiggles for errors
- Orange squiggles for warnings
- Blue squiggles for hints
- Line numbers and code folding
- Auto-indentation
Code Intelligence
MacAlloy provides advanced code navigation and refactoring capabilities:
- Document Outline: Sidebar displaying all signatures, predicates, functions, and assertions for quick navigation
- Go-to-Definition: Command+Click on any symbol to jump to its declaration
- Hover Information: View type information and documentation by hovering over symbols
- Find All References: Locate every usage of a symbol across your specification
- Symbol Renaming: Rename symbols with automatic updates to all references
Diagnostics
- Parse errors with source location
- Type errors with expected vs actual types
- Semantic warnings (unused declarations, shadowing)
- Click-to-navigate from error to source
Analysis
- Run commands to find satisfying instances
- Check commands to search for counterexamples
- Instance enumeration with “Next” button
- Scope configuration per signature
File Management
- Recent files quick access menu
- Drag-and-drop support for
.als files
- Unsaved changes detection with confirmation prompts
- Native macOS file dialogs
Keyboard Shortcuts
| Shortcut | Action |
|---|
| ⌘+Click | Go to definition |
| ⌘+Shift+F | Find all references |
| ⌘+R | Rename symbol |
| ⌘+N | New file |
| ⌘+O | Open file |
| ⌘+S | Save file |
Requirements
| Platform | Minimum Version |
|---|
| macOS | 14.0 (Sonoma) |
| Xcode (for building) | 15.0 |
Comparison with Alloy Analyzer
| Aspect | Alloy Analyzer | MacAlloy |
|---|
| Platform | Java (cross-platform) | Native macOS |
| SAT Backend | External solvers (SAT4J, MiniSat, etc.) | Built-in CDCL solver |
| Dependencies | JVM required | None (self-contained) |
| Alloy Version | 6.2 | 6.2 |
| Temporal Logic | Full LTL | Full LTL |
| Visualization | Swing-based | SwiftUI with force-directed layout |
| Offline Use | Requires JVM installation | Fully self-contained |
MacAlloy is particularly well-suited for education and workshops where installing Java and configuring external SAT solvers presents friction. The self-contained nature simplifies deployment.
Example: Modeling a Mutex Protocol
abstract sig Process {}
one sig P1, P2, P3 extends Process {}
var sig InCS in Process {} -- processes in critical section
var sig Requesting in Process {} -- processes requesting access
fact Init {
no InCS -- initially no one in critical section
no Requesting -- initially no one requesting
}
pred Request[p: Process] {
p not in Requesting
p not in InCS
Requesting' = Requesting + p
InCS' = InCS
}
pred Enter[p: Process] {
p in Requesting
no InCS
InCS' = InCS + p
Requesting' = Requesting - p
}
pred Exit[p: Process] {
p in InCS
InCS' = InCS - p
Requesting' = Requesting
}
pred stutter {
InCS' = InCS
Requesting' = Requesting
}
fact Transitions {
always (
(some p: Process | Request[p]) or
(some p: Process | Enter[p]) or
(some p: Process | Exit[p]) or
stutter
)
}
run { eventually some InCS } for 3 Process, 8 steps
check MutualExclusionHolds {
always lone InCS
} for 3 Process, 10 steps
Request (ask for access), Enter (acquire the critical section), Exit (release), and stutter (no change). The run command finds example traces, while check verifies that the safety property (at most one process in the critical section) holds for all reachable states. If the property can be violated, MacAlloy displays a counterexample trace.
Source Code
MacAlloy is open source and available at github.com/AlchemicalChef/MacAlloy.