How TLX Works

This page explains TLX's internal architecture for contributors. See the C4 model for the visual architecture and ADRs for the decisions behind it.

The Pipeline

A TLX specification goes through three stages:

Elixir source → Spark DSL (compile-time) → Internal IR → Output
                                                          ├── TLA+ emitter → .tla file → TLC (mix tlx.check)
                                                          ├── PlusCal emitters → .tla file (C/P syntax)
                                                          ├── Config emitter → .cfg file
                                                          ├── Elixir emitter → round-trip source
                                                          └── Simulator → Elixir state exploration

Stage 1: DSL → IR. When a user writes defspec MySpec do ... end, Spark compiles the DSL entities into Elixir structs at compile time. Spark handles validation (schema types), transformation (auto-TypeOK), and verification (undeclared variables, empty actions). The result is a set of entities stored in the module's Spark config, accessible via Spark.Dsl.Extension.get_entities/2.

Stage 2: IR → Output. Emitters and the simulator read entities from the compiled module and produce output. They never modify the IR — it's read-only after compilation.

The Spark DSL Extension

TLX.Dsl (lib/tlx/dsl.ex) defines the DSL grammar as Spark entities and sections. Key concepts:

• Entities are the building blocks: variable, constant, action, invariant, property, process, refines, etc. Each entity has a target struct (e.g., TLX.Variable, TLX.Action) and a schema defining its options.
• Sections group entities: variables, constants, actions, invariants, properties, processes, refinements, initial.
• Top-level sections (top_level?: true) allow entities to be written directly in the defspec body without wrapping do blocks.
• Imports bring expression helpers (TLX.Expr, TLX.Temporal, TLX.Sets, TLX.Sequences) into scope inside DSL blocks, so e(), forall(), union(), etc. are available.

Spark provides:

• Transformers — run after compilation. TLX.Transformers.TypeOK auto-generates a type_ok invariant from variable defaults.
• Verifiers — check for errors. TLX.Verifiers.TransitionTargets catches undeclared variable references. TLX.Verifiers.EmptyAction warns about actions with no transitions.
• Introspection — Spark.Dsl.Extension.get_entities(module, [:actions]) returns all action entities for a module.

The Internal Representation

Each DSL entity compiles to a plain Elixir struct:

Expressions are stored as {:expr, quoted_ast} tuples — the e() macro captures Elixir AST and wraps it for passthrough through Spark's schema validation. See ADR-0005.

Functions like forall/3, ite/3, union/2 used outside e() produce 4-tuple forms (e.g., {:ite, cond, then, else}). Inside e(), they're captured as 3-tuple AST call nodes (e.g., {:ite, meta, [cond, then, else]}). The Format module handles both forms.

The Emitters

All emitters follow the same pattern:

1. Read entities from the compiled module via Spark.Dsl.Extension.get_entities/2
2. Format expressions using TLX.Emitter.Format with a symbol table
3. Assemble output strings

Format Module

TLX.Emitter.Format (lib/tlx/emitter/format.ex) is the shared AST formatter. It's parameterized by symbol tables — maps that control output syntax. See ADR-0006.

Four symbol tables: tla_symbols, pluscal_symbols, unicode_symbols, elixir_symbols. Each emitter picks one:

@symbols Format.tla_symbols()
defp format_ast(ast), do: Format.format_ast(ast, @symbols)

Key functions:

• format_ast(ast, symbols) — format an Elixir AST node (operators, quantifiers, function calls, literals)
• format_expr(expr, symbols) — unwrap {:expr, ast} and format; also handles :member, :and_members, and direct-call forms
• format_value(val, symbols) — format default values (integers, atoms, booleans, lists, maps, MapSets)

Atoms Collector

TLX.Emitter.Atoms (lib/tlx/emitter/atoms.ex) traverses all entities to find atom literals used as values. These are declared as TLA+ CONSTANTS and model values in the .cfg file. See ADR-0007.

TLA+ Emitter

TLX.Emitter.TLA generates the standard TLA+ output: MODULE header, EXTENDS, CONSTANTS, VARIABLES, Init, each action as a TLA+ operator, Next (disjunction of all actions), Spec (with fairness), invariants, and ==== footer. It handles UNCHANGED clauses, branched actions (nested disjunctions), and refinement (INSTANCE/WITH).

PlusCal Emitters

TLX.Emitter.PlusCalC and TLX.Emitter.PlusCalP generate PlusCal C-syntax (braces) and P-syntax (begin/end) respectively. Single-process specs with multiple actions are wrapped in while(TRUE) { either/or }. See ADR-0009.

Config Emitter

TLX.Emitter.Config generates .cfg files for TLC: SPECIFICATION, CONSTANTS (model values), INVARIANT, and PROPERTY directives.

Diagram Emitters

Four emitters generate state machine diagrams from specs:

• TLX.Emitter.Graph — shared module that extracts states, edges, and initial state from a compiled spec into a %Graph{} struct
• TLX.Emitter.Dot — GraphViz DOT digraph
• TLX.Emitter.Mermaid — Mermaid stateDiagram-v2 (renders in GitHub/GitLab markdown)
• TLX.Emitter.PlantUML — PlantUML @startuml/@enduml (enterprise tools, Confluence)
• TLX.Emitter.D2 — D2/Terrastruct (modern declarative diagrams)

All four diagram emitters consume TLX.Emitter.Graph.extract/2 for graph data, then render in their respective syntax.

Extractors

Extractors auto-generate spec skeletons from existing code (see Extraction Architecture and ADR-0012):

OTP Patterns

Reusable macros in TLX.Patterns.OTP.* generate complete specs from declarative options (see OTP Patterns Reference and ADR-0011):

• TLX.Patterns.OTP.StateMachine — single state variable, event-driven transitions
• TLX.Patterns.OTP.GenServer — multiple fields, partial state updates, guards
• TLX.Patterns.OTP.Supervisor — restart strategies, bounded restarts, escalation

The Simulator

TLX.Simulator (lib/tlx/simulator.ex) performs random walk state exploration without TLC or Java. It:

1. Builds the initial state from variable defaults
2. At each step, finds all enabled actions (guards evaluate to true)
3. Picks one at random and applies its transitions
4. Checks all invariants after each transition
5. Reports violations with a counterexample trace

The simulator evaluates expressions by walking the AST and interpreting operators directly in Elixir. It uses the same {:expr, ast} representation as the emitters.

Limitations: the simulator cannot check temporal properties (always/eventually), only safety invariants. It's not exhaustive — it samples random paths. For exhaustive verification, use TLC via mix tlx.check.

The Importers

TLX imports go through a three-module pipeline: structural parsing, expression parsing, codegen.

TLX.Importer.TlaParser handles the module structure — header, EXTENDS, VARIABLES, CONSTANTS, operator definitions — via NimbleParsec. It also pre-strips TLA+ comments (\* line, (* *) block, nestable) so downstream classifiers don't false-positive on temporal tokens inside comments.

TLX.Importer.ExprParser parses each operator body into Elixir AST matching what TLX.Expr.e/1 produces at DSL compile time. Covers 63 TLA+ constructs: literals, arithmetic, comparison, logical, implication, IF/THEN/ELSE, sets (literal, comprehension, union/intersect/difference, SUBSET/UNION, Cardinality, range), quantifiers (bounded and unbounded), functions (application, DOMAIN, EXCEPT, records, constructor, function set), sequences, LAMBDA (SelectSeq-scoped), CASE, and temporal operators. TlaParser attaches the resulting ASTs to actions (guard_ast, transition ast), invariants (ast), and properties (ast). Operators containing temporal tokens are classified as properties; others as invariants.

TLX.Importer.Codegen generates TLX DSL source from the parsed map. Uses Code.format_string!/1 for syntactic correctness. Pre-processes the parsed map to restore :atom form for identifiers matching declared CONSTANTS. Property bodies emit in canonical shape (outer temporal/binder peeled, e(...) around the innermost predicate).

Per ADR-0013, the importer guarantees lossless round-trip for TLX-emitted output — every AST attachment point is non-nil for emitter output. Hand-written TLA+ is best-effort tier-2: the expression parser falls back to raw-string capture on failure, logs a Logger.warning, and the codegen comment path keeps the text intact. TlaParser.parse/1 returns a :coverage map with attempted/fallback counts; mix tlx.import --verbose prints the summary.

A CI gate at test/integration/emitter_coverage_test.exs asserts parser coverage for every construct the emitter produces — adding a new emitter rule without a parser counterpart fails the build.

Key Files

What to Read Next

• TLX vs writing TLA+ directly — what the DSL adds
• ADR-0004: Emit TLA+, don't reimplement TLC — the fundamental boundary
• ADR-0005: {:expr, quoted} wrapper — how expressions flow through the pipeline
• ADR-0006: Shared Format module — how emitters share formatting
• ADR-0013: Importer scope — lossless round-trip for TLX-emitted output, best-effort for hand-written