API Reference TLX v#0.5.2

A Spark DSL for writing TLA+/PlusCal specifications.

IR struct for an action DSL entity — holds guard, transitions, branches, and fairness.

IR struct for a branch inside an action — a non-deterministic alternative.

IR struct for a constant DSL entity — holds a constant's name.

Spark DSL extension defining the TLX surface — entities, sections, transformers, and verifiers that compile a defspec block into the internal IR.

Collects all atom literal values used in a spec's variables, transitions, and branches. These need to be declared as TLA+ model value constants.

Generates TLC model configuration (.cfg) files from a compiled TLX.Spec module.

Emits a D2 (Terrastruct) state diagram from a compiled TLX.Spec module.

Emits a GraphViz DOT digraph from a compiled TLX.Spec module.

Emits TLX DSL source code from a compiled spec module.

Shared AST formatting parameterized by symbol tables.

Extracts state machine graph structure from a compiled TLX.Spec module.

Emits a Mermaid stateDiagram-v2 from a compiled TLX.Spec module.

Emits a PlantUML state diagram from a compiled TLX.Spec module.

Emits a PlusCal algorithm (C-syntax) from a compiled TLX.Spec module, wrapped in a valid .tla file.

Emits a PlusCal algorithm (P-syntax / begin-end) from a compiled TLX.Spec module, wrapped in a valid .tla file compatible with pcal.trans.

Emits TLX DSL source with Unicode mathematical symbols.

Emits a TLA+ module from a compiled TLX.Spec module.

Provides the e/1 macro for capturing Elixir expressions as TLA+ AST.

Extracts state machine structure from Ash resources using AshStateMachine.

Extracts pipeline topology from Broadway modules via source AST.

Extracts OTP structure from compiled Erlang BEAM files (ADR-0012 Tier 2).

Extracts GenServer structure from Elixir source code.

Extracts state machine structure from gen_statem/GenStateMachine source code.

Extracts LiveView structure from Elixir source code.

Extracts workflow structure from Reactor modules via Spark introspection.

Function constructor, function set, and Cartesian product for TLA+ expressions.

Generates TLX DSL source code from a parsed spec map.

Parses TLA+ expressions into Elixir AST matching the form produced by TLX.Expr.e/1 at DSL compile time.

Parses PlusCal algorithms (C-syntax and P-syntax) embedded in .tla files into a structured map compatible with TLX.Importer.Codegen.

Parses a subset of TLA+ syntax into a structured map using NimbleParsec, then delegates to TLX.Importer.Codegen for TLX DSL emission.

Introspection functions for compiled TLX specs.

IR struct for a constraint inside the initial block — a custom Init predicate.

IR struct for an invariant — a safety predicate over spec state.

Reusable verification template for GenServer request/response handlers.

Reusable verification template for gen_statem/GenStateMachine state machines.

Reusable verification template for OTP Supervisor restart strategies.

IR struct for a process DSL entity — a concurrent actor with its own variables and actions.

IR struct for a property — a temporal formula over behaviors.

IR struct for a refines DSL entity — links a concrete spec to an abstract one it refines.

IR struct for a single mapping inside refines — binds an abstract variable to a concrete expression.

Sequence operation constructors for use in TLA+ expressions.

Set operation constructors for use in TLA+ expressions.

Random walk state exploration for TLX specs.

Use this module to define a TLA+ specification.

Invokes TLC model checker as a Java subprocess using -tool mode for structured, machine-parseable output.

Temporal operators, quantifiers, and expression helpers for use in property, invariant, and action expressions.

Formats counterexample traces from the simulator or TLC into human-readable output.

Spark transformer that auto-generates a TypeOK invariant from variable usage when the user hasn't declared one.

IR struct for a next :var, expr transition inside an action or branch.

Tuple constructor for use in TLA+ expressions.

IR struct for a variable DSL entity — holds name, default, and type annotation.

Spark verifier that warns when an action has no transitions or branches — catches likely-unintended empty actions.

Spark verifier that rejects next :var, ... transitions targeting an undeclared variable.

IR struct for a with choice — binds a variable ranging over a set for the action body.

Emit a TLA+ spec and run TLC model checker.

Emit a TLA+ or PlusCal specification from a compiled TLX.Spec module.

Generate a TLX spec skeleton from an Ash resource with AshStateMachine.

Generate a TLX spec skeleton from a Broadway pipeline module.

Generate a TLX spec skeleton from a compiled Erlang OTP module.

Generate a TLX spec skeleton from a GenServer module.

Generate a TLX spec skeleton from a Phoenix LiveView module.

Generate a TLX spec skeleton from a Reactor workflow module.

Generate a TLX spec skeleton from a GenStateMachine module.

Import a TLA+ or PlusCal specification file into TLX DSL syntax.

Discover and list all TLX.Spec modules in the project.

Run random walk simulations on a TLX.Spec module.

Watch for file changes and auto-simulate a TLX.Spec module.