MacAlloy is a native Apple platform IDE for Alloy 6.2, providing a complete formal verification environment without external dependencies. It implements the full Alloy language specification with a custom CDCL SAT solver, enabling lightweight formal analysis directly on macOS and iPad.
Unlike the Java-based Alloy Analyzer, MacAlloy is built entirely in Swift using a from-scratch implementation of the Alloy toolchain:
| 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.
Source Code → Lexer → Parser → Semantic Analyzer → Translator → SAT Solver → Instance Extractor
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
- Real-time error underlining as you type
- Line numbers and code folding
- Auto-indentation
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
Requirements
| Platform | Minimum Version |
|---|
| macOS | 14.0 (Sonoma) |
| iPadOS | 17.0 |
| Xcode (for building) | 15.0 |
Comparison with Alloy Analyzer
| Aspect | Alloy Analyzer | MacAlloy |
|---|
| Platform | Java (cross-platform) | Native Apple (macOS, iPad) |
| 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 {
var waiting: lone 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 MutualExclusion {
always lone InCS
}
fact Progress {
always (some Requesting implies eventually some InCS)
}
fact Fairness {
all p: Process | always (p in Requesting implies eventually p in 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
}
run { eventually some InCS } for 3 Process, 8 steps
Source Code
MacAlloy is open source and available at github.com/AlchemicalChef/MacAlloy.