> ## Documentation Index > Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt > Use this file to discover all available pages before exploring further. # MacAlloy > 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](https://alloytools.org/), 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](/formal-methods/alloy-basics) to learn the fundamentals, then return here to run your specifications. ## Platform Overview 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. MacAlloy Architecture Diagram ### 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 ```text theme={null} 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: ```text theme={null} 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: ```text theme={null} 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): ```text theme={null} State₀ → State₁ → State₂ → State₃ → State₄ ↑__________| (loop back) ``` ### Temporal Operators **Future Operators**: * `after` / `X` — in the next state * `always` / `G` — in all future states * `eventually` / `F` — in some future state * `until` / `U` — holds until another property holds * `releases` / `R` — dual of until **Past Operators**: * `before` — in the previous state * `historically` — in all past states * `once` — in some past state * `since` — held since another property held * `triggered` — dual of since ### Temporal Encoding Temporal formulas are unrolled over a bounded number of steps with loop detection: ```alloy theme={null} var sig Active in Process {} fact SomeoneAlwaysActive { always some Active } run {} for 5 Process, 10 steps ``` The `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 ```alloy theme={null} 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 ``` 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. ## Related Resources Use MacAlloy to analyze ACL configurations and detect privilege escalation paths Learn how TLA+ and Alloy specifications work together to verify AD security ## Source Code MacAlloy is open source and available at [github.com/AlchemicalChef/MacAlloy](https://github.com/AlchemicalChef/MacAlloy).