TLX Roadmap

Vision

Enable Elixir developers to write formally verifiable TLA+/PlusCal specifications using a Spark DSL, bridging the gap between Elixir's actor model and TLA+'s formal verification.

Phases

Phase 1: Foundation (complete)

Target: v0.1.x Focus: Core DSL, internal IR, TLA+ emitter

• [x] Spark DSL for variables, constants, init, actions (guard + next)
• [x] Internal IR structs (%TLX.Spec{}, %TLX.Action{}, etc.)
• [x] TLA+ emitter (generate valid .tla files from IR)
• [x] Invariant declarations
• [x] First example spec: simple state machine
• [x] Foundational ADRs (0001, 0002, 0003)

Phase 2: PlusCal and Concurrency (complete)

Target: v0.2.x Focus: Process support, PlusCal emission, temporal properties

• [x] Process declarations (concurrent actors)
• [x] PlusCal emitter (labels, await, either/or, with)
• [x] Temporal properties (always, eventually)
• [x] Fairness annotations (weak/strong)
• [x] Quantifiers (exists, forall)
• [x] Non-deterministic choice
• [x] TLC integration (invoke TLC as subprocess, parse results)

Phase 3: Simulation and Tooling (complete)

Target: v0.3.x Focus: Elixir simulator, Mix tasks, developer experience

• [x] Elixir simulator (random walk state exploration)
• [x] mix tlx.check task (emit + run TLC)
• [x] mix tlx.simulate task (Elixir random exploration)
• [x] Counterexample trace formatting
• [x] Spark introspection and documentation generation

Phase 4: Production Readiness (complete)

Target: v1.0.0 Focus: Hardening, documentation, public release

• [x] Comprehensive test suite
• [x] Diátaxis documentation (tutorials, how-to, reference, explanation)
• [x] Hex.pm publication (package metadata ready, publish when public)
• [x] Real-world example specs (mutex, producer-consumer)

Phase 5: Semantic Intelligence (proposed)

Target: v0.2.x Focus: Compile-time analysis, smarter diagnostics

• [x] Auto-generated TypeOK invariants from variable usage
• [x] Empty action / zero-transition warnings
• [x] Better error messages with source locations and suggestions
• [x] Simulator constant injection

Phase 6: Expressiveness (complete)

Target: v0.2.x Focus: Close the gap with full TLA+/PlusCal

• [x] IF/THEN/ELSE in expressions (ite/3)
• [x] Set operations (union, intersect, subset, cardinality, set_of, in_set)
• [x] Non-deterministic set pick (pick :var, :set)
• [x] Custom Init expressions (initial section with constraint)
• [x] LET/IN local definitions (let_in/3)

Phase 7: Tooling (complete)

Target: v0.3.x Focus: Developer workflow

• [x] mix tlx.watch — auto-simulate on save
• [x] mix tlx.list — discover spec modules
• [x] Extract shared AST formatting into TLX.Emitter.Format (symbol-table-parameterized)
• [x] CI integration (GitHub Actions workflow)
• [x] Mix task naming: Mix.Tasks.Tlx.* (Mix convention)

Phase 8: Forge Integration (complete)

Target: v0.3.x Focus: Bridge to the original motivation

• [x] GenStateMachine → TLX skeleton generator
• [x] TLA+ → TLX importer
• [x] Forge example specs — 6 abstract (from ADRs) + 6 concrete (from code), all TLC-verified
• [x] Refinement checking — concrete specs refine abstract specs via INSTANCE/WITH

Phase 9: Robustness (complete)

Target: v0.2.x Focus: Replace fragile string-based approaches with proper tools

Sprint 15 — TLC tool mode and PlusCal emitter compat:

• [x] TLC -tool mode output parsing (replaces regex stdout scraping; JSON unavailable in TLC 2.19)
• [x] PlusCal C-syntax emitter fixed for pcal.trans acceptance
• [x] PlusCal P-syntax emitter (begin/end style)
• [x] Integration tested: PlusCal → pcal.trans → TLC

Sprint 16 — Proper parsers and AST-based code gen:

• [x] NimbleParsec TLA+ parser (replaces regex importer)
• [x] PlusCal parser for importing PlusCal specs (C-syntax and P-syntax)
• [x] AST-based code generation via Code.format_string!/1 for mix tlx.import and mix tlx.gen.from_state_machine
• [x] Round-trip fidelity tests: emit → parse → codegen preserves structure

Phase 11: Refinement and Verification (complete)

Target: v0.2.8 Focus: Spec-vs-spec comparison, emitter robustness

• [x] refines DSL block with mapping entities
• [x] TLA+ INSTANCE/WITH emission for refinement checking
• [x] Auto-declare atom model values as CONSTANTS (TLA+ and .cfg)
• [x] Fix branched action TLA+ emission (UNCHANGED inside disjunctions)
• [x] Handle 3-tuple AST forms for ite/let_in/set ops inside e()
• [x] Auto-include abstract spec atoms in INSTANCE identity mappings
• [x] formal-spec skill — workflow from ADR to refinement-checked specs

Phase 10: Documentation (complete)

Target: v0.2.9 Focus: Diátaxis documentation and reference

• [x] How-to guides (model GenServer, find race conditions, run TLC, verify with refinement)
• [x] Explanation pages (why formal verification, TLX vs raw TLA+, formal specs vs testing)
• [x] Getting-started tutorial rewrite (traffic light example)
• [x] Reference docs (DSL, mix tasks, expressions)
• [x] CONTRIBUTING.md with tone guidelines
• [x] FAQ.md

Phase 12: Expressiveness II (complete)

Target: v0.2.11 Focus: Functions, maps, records, sequences

• [x] Function application (at/2) and update (except/3)
• [x] CHOOSE, set comprehension (filter/3), CASE (case_of/1)
• [x] if syntax inside e(), let_in block style
• [x] DOMAIN, range sets, implication/equivalence
• [x] Sequence operations (len, append, head, tail, sub_seq)
• [x] Configurable EXTENDS (extends [:Sequences])
• [x] Record construction (record/1), multi-key EXCEPT (except_many/2)
• [x] Symbols emitter (TLX DSL with math notation)

Phase 13: Quality and Supply Chain (complete)

Target: v0.3.1 Focus: Toolchain validation, supply chain security, emitter fixes

• [x] SANY and pcal.trans toolchain validation (87 integration tests)
• [x] AllConstructs comprehensive spec covering every DSL construct
• [x] Emitter fixes: map defaults, atom collection, multi-action PlusCal
• [x] SPDX copyright and license headers on all source files
• [x] SECURITY.md, GitHub Actions CI, Dependabot
• [x] ADRs 4-10 documenting architectural decisions
• [x] mix tlx.list and mix tlx.watch
• [x] Published on Hex.pm

Sprint History

Proposed Sprints

Sprint 44: State/Transition Coverage

Goal: Answer "do my tests exercise all the states and transitions my spec defines?"

TLC gives exhaustive spec coverage (proof). This feature gives test coverage against the spec — which states/transitions the ExUnit suite actually exercises at runtime.

Architecture:

Spec (TLX)              Implementation            Tests (ExUnit)
    │                        │                         │
    ▼                        ▼                         ▼
Graph.extract/2 ──→  State/Transition Map    Instrumentation hooks
    │                                              │
    └──────────────── Compare ─────────────────────┘
                         │
                    Coverage Report

Instrumentation approaches by module type:

Deliverables:

1. TLX.Coverage — test helper module

   • start_tracking(module, spec) — begins state/transition recording
   • stop_tracking(module) — returns %{visited_states, visited_transitions}
   • report(module, spec) — compares against spec, prints coverage table

2. mix tlx.coverage — mix task that runs tests with tracking enabled

   • Reads spec → implementation mapping from # Source: headers
   • Instruments implementations during test run
   • Reports per-spec coverage after tests complete

3. ExUnit integration:

   defmodule MyApp.ReconcilerTest do
     use ExUnit.Case
     use TLX.Coverage, spec: ReconcilerSpec, module: MyApp.Reconciler
   
     # Tests run normally — coverage tracked automatically
     test "check returns in_sync" do
       # ...
     end
   end
   # After: prints state/transition coverage report

Output format:

State Coverage: MyApp.Reconciler (spec: ReconcilerSpec)
─────────────────────────────────────────────────────
States:
  :idle        ✓ (12 visits)
  :in_sync     ✓ (8 visits)
  :drifted     ✓ (4 visits)
  :error       ✗ NOT TESTED

Transitions:
  idle → in_sync (check/success)     ✓ (6 visits)
  idle → drifted (check/failure)     ✓ (4 visits)
  drifted → in_sync (apply/success)  ✓ (3 visits)
  drifted → drifted (apply/failure)  ✗ NOT TESTED
─────────────────────────────────────────────────────
States: 3/4 (75%)   Transitions: 3/4 (75%)

Challenges:

• GenServer state is opaque — need to map struct fields to spec variables
• LiveView assigns change frequently — need to filter spec-relevant fields only
• Transition detection requires comparing consecutive states, not just snapshots
• gen_statem state_functions mode: state is the function name, not in :sys.get_state
• Performance: :sys.trace adds overhead; only enable during test runs

Prerequisites: None — uses existing specs and the shared Graph extraction module. Independent of extractors.

Sprints 54–59: Round-Trip Track (ADR-0013) — shipped

Driver: ADR-0013 — importer round-trips TLX-emitted output losslessly; hand-written TLA+ stays best-effort.

All six sprints landed. Importer now parses 63 TLA+ constructs to structured Elixir AST (foundation, sets, quantifiers, records, EXCEPT, arithmetic, tuples, Cartesian, functions, sequences, SelectSeq LAMBDA, CASE, temporal operators). TLX.Importer.Codegen emits real e(...) calls instead of raw-string comments. CI gate at test/integration/emitter_coverage_test.exs asserts every emitted construct has a matching parser rule.

See per-sprint plans and retrospectives in docs/sprints/sprint-0054-*.md through sprint-0059-*.md for scope, design decisions, surprises, and handoffs.