# TLX v0.5.2 - Table of Contents

A Spark DSL for writing and verifying TLA+/PlusCal specifications, with TLC model checking, refinement, and an AI-assisted formal specification workflow

## Pages

- [TLX](readme.md)
- [Changelog](changelog.md)
- [FAQ](faq.md)

- DSL Reference
  - [TLX](dsl-tlx.md)

- Tutorials
  - [Tutorial: Extract and Verify a GenServer](extract-and-verify.md)
  - [Getting Started with TLX](getting-started.md)
  - [Tutorial: Visualize a Spec](visualize-a-spec.md)

- How-To Guides
  - [How to Audit Spec Coverage](audit-spec-coverage.md)
  - [How to Extract Specs from Framework Modules](extract-from-frameworks.md)
  - [How to Extract Specs from OTP Modules](extract-from-otp.md)
  - [How to Find Race Conditions with TLX](find-race-conditions.md)
  - [How to Generate Diagrams](generate-diagrams.md)
  - [How to Model Your GenServer as a TLX Spec](model-a-genserver.md)
  - [How to Run TLC Model Checking](run-tlc.md)
  - [How to Use OTP Patterns](use-otp-patterns.md)
  - [How to Verify Your Code Matches Your Design](verify-with-refinement.md)

- Explanations
  - [Extraction Architecture](extraction-architecture.md)
  - [Formal Specs vs Property-Based Testing](formal-spec-vs-testing.md)
  - [How TLX Works](internals.md)
  - [OTP Patterns vs defspec](patterns-vs-defspec.md)
  - [TLX vs Writing TLA+ Directly](tlx-vs-raw-tla.md)
  - [Why Formal Verification Matters for Elixir](why-formal-verification.md)

- Reference
  - [DSL Reference](dsl.md)
  - [Expression Reference](expressions.md)
  - [Extractors Reference](extractors.md)
  - [Mix Tasks Reference](mix-tasks.md)
  - [OTP Patterns Reference](otp-patterns.md)
  - [Quality Configuration](quality-configuration.md)
  - [TLA+ to TLX Mapping Reference](tlaplus-mapping.md)
  - [TLA+ Constructs Not Supported by TLX](tlaplus-unsupported.md)

- ADRs
  - [1. Record Architecture Decisions](0001-record-architecture-decisions.md)
  - [2. Adopt Development Best Practices](0002-adopt-development-best-practices.md)
  - [3. Use Elixir with Spark DSL Framework](0003-adopt-elixir-spark-stack.md)
  - [4. Emit TLA+, Don't Reimplement TLC](0004-emit-tla-not-reimplement-tlc.md)
  - [5. Use {:expr, quoted} Wrapper for AST Passthrough](0005-expr-wrapper-for-ast-passthrough.md)
  - [6. Shared Format Module with Symbol Tables](0006-shared-format-module-with-symbol-tables.md)
  - [7. Auto-Declare Atom Values as TLA+ Model Value CONSTANTS](0007-auto-declare-atom-model-values.md)
  - [8. Mix Task Naming: Mix.Tasks.Tlx, Not Mix.Tasks.TLX](0008-mix-task-naming-convention.md)
  - [9. PlusCal Multi-Action Wrapping with while/either](0009-pluscal-multi-action-wrapping.md)
  - [10. Distribute Agent Skills via usage_rules](0010-agent-skills-via-usage-rules.md)
  - [11. OTP Patterns as Reusable Verification Templates](0011-otp-patterns-as-verification-templates.md)
  - [12. OTP Extraction Strategy](0012-otp-extraction-strategy.md)
  - [13. Importer Scope: Lossless for TLX-Emitted Output, Best-Effort for Hand-Written](0013-importer-scope-lossless-for-tlx-output.md)
  - [14. Layered Strictness: Permissive DSL, Validating Emitter, Prescriptive Linter](0014-layered-strictness-permissive-dsl-validating-emitter-prescriptive-linter.md)
  - [15. Credo Plugin: Opt-In Linter for TLA+ Formality](0015-credo-plugin-opt-in-linter-for-tla-formality.md)

- Roadmap
  - [TLX Roadmap](roadmap.md)

## Modules

- [TLX](TLX.md): A Spark DSL for writing TLA+/PlusCal specifications.
- [TLX.Action](TLX.Action.md): IR struct for an `action` DSL entity — holds guard, transitions, branches, and fairness.
- [TLX.Branch](TLX.Branch.md): IR struct for a `branch` inside an action — a non-deterministic alternative.
- [TLX.Constant](TLX.Constant.md): IR struct for a `constant` DSL entity — holds a constant's name.
- [TLX.Dsl](TLX.Dsl.md): Spark DSL extension defining the TLX surface — entities, sections, transformers, and verifiers that compile a `defspec` block into the internal IR.
- [TLX.Emitter.Atoms](TLX.Emitter.Atoms.md): Collects all atom literal values used in a spec's variables, transitions,
and branches. These need to be declared as TLA+ model value constants.

- [TLX.Emitter.Config](TLX.Emitter.Config.md): Generates TLC model configuration (`.cfg`) files from a compiled `TLX.Spec` module.

- [TLX.Emitter.D2](TLX.Emitter.D2.md): Emits a D2 (Terrastruct) state diagram from a compiled `TLX.Spec` module.
- [TLX.Emitter.Dot](TLX.Emitter.Dot.md): Emits a GraphViz DOT digraph from a compiled `TLX.Spec` module.
- [TLX.Emitter.Elixir](TLX.Emitter.Elixir.md): Emits TLX DSL source code from a compiled spec module.
- [TLX.Emitter.Format](TLX.Emitter.Format.md): Shared AST formatting parameterized by symbol tables.
- [TLX.Emitter.Graph](TLX.Emitter.Graph.md): Extracts state machine graph structure from a compiled `TLX.Spec` module.
- [TLX.Emitter.Mermaid](TLX.Emitter.Mermaid.md): Emits a Mermaid `stateDiagram-v2` from a compiled `TLX.Spec` module.
- [TLX.Emitter.PlantUML](TLX.Emitter.PlantUML.md): Emits a PlantUML state diagram from a compiled `TLX.Spec` module.
- [TLX.Emitter.PlusCalC](TLX.Emitter.PlusCalC.md): Emits a PlusCal algorithm (C-syntax) from a compiled `TLX.Spec` module,
wrapped in a valid `.tla` file.

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

- [TLX.Emitter.Symbols](TLX.Emitter.Symbols.md): Emits TLX DSL source with Unicode mathematical symbols.
- [TLX.Emitter.TLA](TLX.Emitter.TLA.md): Emits a TLA+ module from a compiled `TLX.Spec` module.

- [TLX.Expr](TLX.Expr.md): Provides the `e/1` macro for capturing Elixir expressions as TLA+ AST.
- [TLX.Extractor.AshStateMachine](TLX.Extractor.AshStateMachine.md): Extracts state machine structure from Ash resources using AshStateMachine.
- [TLX.Extractor.Broadway](TLX.Extractor.Broadway.md): Extracts pipeline topology from Broadway modules via source AST.
- [TLX.Extractor.Erlang](TLX.Extractor.Erlang.md): Extracts OTP structure from compiled Erlang BEAM files (ADR-0012 Tier 2).
- [TLX.Extractor.GenServer](TLX.Extractor.GenServer.md): Extracts GenServer structure from Elixir source code.
- [TLX.Extractor.GenStatem](TLX.Extractor.GenStatem.md): Extracts state machine structure from gen_statem/GenStateMachine source code.
- [TLX.Extractor.LiveView](TLX.Extractor.LiveView.md): Extracts LiveView structure from Elixir source code.
- [TLX.Extractor.Reactor](TLX.Extractor.Reactor.md): Extracts workflow structure from Reactor modules via Spark introspection.
- [TLX.Functions](TLX.Functions.md): Function constructor, function set, and Cartesian product for TLA+
expressions.
- [TLX.Importer.Codegen](TLX.Importer.Codegen.md): Generates TLX DSL source code from a parsed spec map.
- [TLX.Importer.ExprParser](TLX.Importer.ExprParser.md): Parses TLA+ expressions into Elixir AST matching the form produced by
`TLX.Expr.e/1` at DSL compile time.
- [TLX.Importer.PlusCalParser](TLX.Importer.PlusCalParser.md): Parses PlusCal algorithms (C-syntax and P-syntax) embedded in `.tla` files
into a structured map compatible with `TLX.Importer.Codegen`.

- [TLX.Importer.TlaParser](TLX.Importer.TlaParser.md): Parses a subset of TLA+ syntax into a structured map using NimbleParsec,
then delegates to `TLX.Importer.Codegen` for TLX DSL emission.
- [TLX.Info](TLX.Info.md): Introspection functions for compiled TLX specs.

- [TLX.InitConstraint](TLX.InitConstraint.md): IR struct for a `constraint` inside the `initial` block — a custom Init predicate.
- [TLX.Invariant](TLX.Invariant.md): IR struct for an `invariant` — a safety predicate over spec state.
- [TLX.Patterns.OTP.GenServer](TLX.Patterns.OTP.GenServer.md): Reusable verification template for GenServer request/response handlers.
- [TLX.Patterns.OTP.StateMachine](TLX.Patterns.OTP.StateMachine.md): Reusable verification template for gen_statem/GenStateMachine state machines.
- [TLX.Patterns.OTP.Supervisor](TLX.Patterns.OTP.Supervisor.md): Reusable verification template for OTP Supervisor restart strategies.
- [TLX.Process](TLX.Process.md): IR struct for a `process` DSL entity — a concurrent actor with its own variables and actions.
- [TLX.Property](TLX.Property.md): IR struct for a `property` — a temporal formula over behaviors.
- [TLX.Refinement](TLX.Refinement.md): IR struct for a `refines` DSL entity — links a concrete spec to an abstract one it refines.
- [TLX.RefinementMapping](TLX.RefinementMapping.md): IR struct for a single `mapping` inside `refines` — binds an abstract variable to a concrete expression.
- [TLX.Sequences](TLX.Sequences.md): Sequence operation constructors for use in TLA+ expressions.
- [TLX.Sets](TLX.Sets.md): Set operation constructors for use in TLA+ expressions.
- [TLX.Simulator](TLX.Simulator.md): Random walk state exploration for TLX specs.
- [TLX.Spec](TLX.Spec.md): Use this module to define a TLA+ specification.
- [TLX.TLC](TLX.TLC.md): Invokes TLC model checker as a Java subprocess using `-tool` mode
for structured, machine-parseable output.

- [TLX.Temporal](TLX.Temporal.md): Temporal operators, quantifiers, and expression helpers for use in
property, invariant, and action expressions.
- [TLX.Trace](TLX.Trace.md): Formats counterexample traces from the simulator or TLC
into human-readable output.

- [TLX.Transformers.TypeOK](TLX.Transformers.TypeOK.md): Spark transformer that auto-generates a `TypeOK` invariant from variable usage when the user hasn't declared one.
- [TLX.Transition](TLX.Transition.md): IR struct for a `next :var, expr` transition inside an action or branch.
- [TLX.Tuples](TLX.Tuples.md): Tuple constructor for use in TLA+ expressions.
- [TLX.Variable](TLX.Variable.md): IR struct for a `variable` DSL entity — holds name, default, and type annotation.
- [TLX.Verifiers.EmptyAction](TLX.Verifiers.EmptyAction.md): Spark verifier that warns when an action has no transitions or branches — catches likely-unintended empty actions.
- [TLX.Verifiers.TransitionTargets](TLX.Verifiers.TransitionTargets.md): Spark verifier that rejects `next :var, ...` transitions targeting an undeclared variable.
- [TLX.WithChoice](TLX.WithChoice.md): IR struct for a `with` choice — binds a variable ranging over a set for the action body.

## Mix Tasks

- [mix tlx.check](Mix.Tasks.Tlx.Check.md): Emit a TLA+ spec and run TLC model checker.
- [mix tlx.emit](Mix.Tasks.Tlx.Emit.md): Emit a TLA+ or PlusCal specification from a compiled TLX.Spec module.
- [mix tlx.gen.from_ash_state_machine](Mix.Tasks.Tlx.Gen.FromAshStateMachine.md): Generate a TLX spec skeleton from an Ash resource with AshStateMachine.
- [mix tlx.gen.from_broadway](Mix.Tasks.Tlx.Gen.FromBroadway.md): Generate a TLX spec skeleton from a Broadway pipeline module.
- [mix tlx.gen.from_erlang](Mix.Tasks.Tlx.Gen.FromErlang.md): Generate a TLX spec skeleton from a compiled Erlang OTP module.
- [mix tlx.gen.from_gen_server](Mix.Tasks.Tlx.Gen.FromGenServer.md): Generate a TLX spec skeleton from a GenServer module.
- [mix tlx.gen.from_live_view](Mix.Tasks.Tlx.Gen.FromLiveView.md): Generate a TLX spec skeleton from a Phoenix LiveView module.
- [mix tlx.gen.from_reactor](Mix.Tasks.Tlx.Gen.FromReactor.md): Generate a TLX spec skeleton from a Reactor workflow module.
- [mix tlx.gen.from_state_machine](Mix.Tasks.Tlx.Gen.FromStateMachine.md): Generate a TLX spec skeleton from a GenStateMachine module.
- [mix tlx.import](Mix.Tasks.Tlx.Import.md): Import a TLA+ or PlusCal specification file into TLX DSL syntax.
- [mix tlx.list](Mix.Tasks.Tlx.List.md): Discover and list all TLX.Spec modules in the project.
- [mix tlx.simulate](Mix.Tasks.Tlx.Simulate.md): Run random walk simulations on a TLX.Spec module.
- [mix tlx.watch](Mix.Tasks.Tlx.Watch.md): Watch for file changes and auto-simulate a TLX.Spec module.

