A native macOS IDE for Alloy 6.2 with built-in SAT solving and temporal logic support
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.
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.
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.
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.
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.
Alloy’s multiplicity keywords translate to cardinality constraints:
one r → exactly one tuple in r → EO encodingsome r → at least one tuple in r → OR of all cellslone r → at most one tuple in r → AMO encodingno r → no tuples in r → AND of negated cells
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.
abstract sig Process {}one sig P1, P2, P3 extends Process {}var sig InCS in Process {} -- processes in critical sectionvar sig Requesting in Process {} -- processes requesting accessfact 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 stepscheck MutualExclusionHolds { always lone InCS} for 3 Process, 10 steps
This model defines a mutual exclusion protocol as a state machine with four actions: 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.
