Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

[Unreleased]

[0.5.2] - 2026-07-25

Patch release. Fixes a multi-key EXCEPT emission bug on imported ASTs, clears all dependency advisories, and restores the compile pre-push gate under Elixir 1.20.

Fixed (Sprint 69 — green pre-push gates)

• TLX.Emitter.Format.format_ast/2 emitted multi-key EXCEPT incorrectly for imported ASTs. The DSL-form clause {:except_many, f, pairs} matches any 3-tuple, so it shadowed the guarded {:except_many, meta, [f, pairs]} clause below it and received [f, pairs] as its pair list. TLX.Importer.ExprParser produces exactly that shape, so a round-tripped [f EXCEPT ![k1] = v1, ![k2] = v2] never reached the correct branch. Guarded form now comes first, matching TLX.Simulator and the convention used by the neighbouring implies/equiv clauses.
• Removed clauses that Elixir 1.20's type inference proves unreachable: is_boolean/1 cases shadowed by an earlier is_atom/1 clause in TLX.Transformers.TypeOK, TLX.Extractor.GenServer and TLX.Extractor.LiveView (booleans are atoms), and the unused parse_model_values/1 nil clause. Behaviour is unchanged.
• TLX.Extractor.AshStateMachine.get_deprecated_states/1 now calls state_machine_deprecated_states!/1, the accessor ashstate_machine's own transformers use. The DSL option defaults to [], so this returns the same value as the previous `{:ok, }-with-fallbackcase` without the unreachable clause.
• mix compile --warnings-as-errors passes again, restoring the compile pre-push gate.

Changed (Sprint 69 — dependency security)

• Updated dev/test dependencies to clear all mix deps.audit advisories: ash 3.24.3 → 3.30.1, which lifted ecto to 3.14.1 and in turn allowed decimal 2.3.0 → 3.1.1 (GHSA-rhv4-8758-jx7v, unbounded exponent DoS — unreachable at 2.x because ecto ~> 3.13 pinned decimal ~> 2.0). mint 1.7.1 → 1.9.3 clears GHSA-g586-ccqf-7x4r (high) and three further advisories. spark moved 2.6.1 → 2.7.2 as a result; it is TLX's only runtime dependency alongside nimble_parsec, and the full suite passes against it.

[0.5.1] - 2026-07-25

Patch release. Refinement checking did not work through mix tlx.check — a headline v0.4 feature that no caller could reach from the Mix task.

Fixed (Sprint 68 — refinement checking through mix tlx.check)

• mix tlx.check now emits the abstract modules a spec refines, so TLC can resolve the INSTANCE references the emitter generates. Previously only the target spec's .tla was written, and every spec declaring refines failed with Cannot find source file for module <Abstract> before checking anything — surfacing as an unexplained TLC: FAILED (:unknown). Refinement checking did not work through the Mix task at all. Resolution is transitive (an abstract spec that itself refines another pulls that module in too) and cycle-safe. Two refinement targets whose final module segments collide now raise, rather than overwriting each other's file and silently checking against the wrong abstract spec.
• TLC: FAILED (:unknown) now prints TLC's raw output. :unknown means TLC exited non-zero without emitting a violation code TLX recognises — nearly always a parse or semantic error, where TLC's own message is the only actionable detail. It was previously discarded.

Added (Sprint 68)

• mix tlx.check --no-deadlock exposes the :deadlock option TLX.TLC.check/3 already accepted. Specs that intentionally reach an absorbing state (:committed, :failed, :done) previously reported a deadlock violation with no way to suppress it.

[0.5.0] - 2026-04-18

Minor release per the ADR-0002 CHANGELOG-oracle rule. Closes the round-trip track (sprints 54–59) that ADR-0013 scoped, plus seven follow-up sprints polishing the surface.

Highlights:

• Importer round-trips TLA+ to structured AST for 63 constructs (every emit-side construct from sprints 45–52 plus the foundation).
• CI gate prevents future emitter/parser drift.
• Property classifier is AST-informed, not string-heuristic.
• Atom round-trip fidelity: re-imported specs preserve :atom form.
• Canonical codegen shape for properties (temporal + binder peel).
• TLA+ comment stripping.
• Observability: Logger.warning on fallback + mix tlx.import --verbose.
• Zero mix docs warnings (16 modules documented + 3 prose fixes).

Fixed (Sprint 53 — zero mix docs warnings)

• mix docs now runs warning-free. Added one-line moduledocs to 12 IR struct modules (TLX.Variable, Constant, Action, Transition, Branch, Invariant, Property, Process, Refinement, RefinementMapping, InitConstraint, WithChoice) and to 4 DSL internals (TLX.Dsl, Transformers.TypeOK, Verifiers.EmptyAction, Verifiers.TransitionTargets). Rewrote 3 prose references (CHANGELOG + roadmap) that pointed to private or non-existent functions. Scope grew from the original plan's 3 structs once mix docs revealed the full 52-warning picture.

Added (Sprint 64 — quantifier short forms)

• TLX.Importer.ExprParser accepts unbounded forms: \E x : P, \A x : P, CHOOSE x : P. AST uses nil in the set position. Emitter gains matching clauses for the nil-set shape. TLX doesn't emit these shapes; import path for hand-written TLA+ (ADR-0013 tier-2).

Changed (Sprint 66 — atom round-trip fidelity)

• TLX.Importer.Codegen.to_tlx/1 now preprocesses the parsed map, walking every AST attachment and replacing bare-identifier nodes whose names match declared CONSTANTS with atom literals. Round-tripping a spec with state == :done no longer drops the : prefix.

Changed (Sprint 67 — binder canonical shape)

• Properties with forall/exists/choose at the AST root now emit in canonical peeled form: forall(:x, <recurse set>, <recurse body>) instead of e(forall(:x, set, body)). Mirrors Sprint 63's temporal peel. Unbounded form falls back to e(...) wrapping since there's no DSL 2-arg binder.

Changed (Sprint 63 — property codegen canonical shape)

• TLX.Importer.Codegen now emits property bodies in canonical form: outer temporal constructors (always, eventually, leads_to, until, weak_until) appear as direct calls, with e(...) wrapping the innermost predicate. Previously wrapped the whole body in one outer e(...). Round-trip output now matches hand-written idiom (always(eventually(e(state == :done)))). Part B of the plan (full emit→parse→emit byte-equivalence test) deferred; canonical-shape regression guard in the Sprint 59 matrix is sufficient.

Added (Sprint 61 — fallback logging and import observability)

• Logger.warning when the expression parser falls back to raw-string capture — snippet truncated to 80 chars + parse reason. Tier-2 fallbacks are now visible in the logs.
• :coverage map in TlaParser.parse/1 output — attempted vs fallback counts per category (invariants, properties, guards, transitions) plus a total. Additive field; existing consumers unaffected.
• mix tlx.import --verbose (alias -v) — prints parse-coverage summary after import. Zero noise for TLX-emitted input (which round-trips losslessly per ADR-0013).

Added (Sprint 62 — TLA+ comment stripping)

• TlaParser.parse/1 now strips \* line comments and (* ... *) block comments (nestable) before parsing. Replaces comment content with spaces so parser error messages preserve line/column accuracy. Fixes the pre-existing false-positive in the Sprint 58 property classifier where [] inside a comment would misclassify an invariant as a property.

Fixed (Sprint 60)

• Nested e(...) inside quantifier/binder constructors — e(forall(:v, set, e(inner))) now emits correctly. Previously the inner e() left a {:e, meta, [arg]} macro-call AST that the emitter rendered as literal tuple text. Fixed with a format_ast clause unwrapping the {:e, ...} shape. (Pre-existing bug surfaced by Sprint 59's round-trip matrix.)

Added (Sprint 59 — round-trip matrix and CI gate)

• TLX.RoundTrip test helper — asserts that every AST attachment point (action guard, transition RHS, invariant body, property body) receives a non-nil AST for TLX-emitted input. Raises with ADR-0013 violation messages when tier-2 fallback triggers.
• test/integration/round_trip_matrix_test.exs — four fixture specs (arithmetic, sets, quantifier, temporal) each asserted lossless via TLX.RoundTrip.assert_lossless/1.
• test/integration/emitter_coverage_test.exs — 63 canonical TLA+ expressions (every construct shipped in Sprints 54–58), each with expected AST root-node atom. Adding a new emitter rule without a parser rule breaks this test.

Added (Sprint 58 — CASE and temporal operators)

• TLX.Importer.ExprParser adds CASE p1 -> e1 [] ... [] OTHER -> d parsing (with [] as clause separator scoped inside CASE) and the full temporal-operator set: []P (always), <>P (eventually) at the unary tier (tight binding per TLA+ precedence), and ~>, \U, \W at a new top-level temporal_binary tier (loose binding).
• TLX.Importer.TlaParser gains extract_properties/1: operators whose bodies contain temporal operators are classified as properties; non-temporal operators remain invariants. Replaces the string-level body contains "[]" filter that previously dropped properties entirely.
• TLX.Importer.Codegen emits property :name, e(<ast>) for temporal-bearing operators, wrapping in e(...) so the DSL captures the AST without compile-time evaluation of bare identifiers.

Added (Sprint 57 — sequences and LAMBDA)

• TLX.Importer.ExprParser extended: Len, Head, Tail, Seq, Append, SubSeq (function calls), \o (binary infix), and SelectSeq(s, LAMBDA x: pred) (with LAMBDA scoped to the SelectSeq context per ADR-0013). Standalone LAMBDA is rejected.
• Builtin call dispatch reorganized into 1-/2-/3-arg buckets plus a dedicated SelectSeq combinator — new sequence ops slot into existing infrastructure without grammar rewrites.

Added (Sprint 56 — arithmetic extensions, tuples, Cartesian, functions)

• TLX.Importer.ExprParser extended: integer division x \div y, modulo x % y, exponentiation x ^ y (right-associative, higher precedence than */\div/%), unary negation -x, tuple literal <<a, b, c>> (including empty and single-element), Cartesian product A \X B (left-associative binary, matching emitter shape), function constructor [x \in S |-> expr], function set [D -> R]. Bracket-primary dispatch order: fn_of → record → fn_set → EXCEPT (fn_of tries first since both start with ident, but fn_of requires \in after while record requires |->).

Added (Sprint 55 — sets, quantifiers, records, EXCEPT)

• TLX.Importer.ExprParser grows the grammar: set literal {a, b, c} and comprehensions ({x \in S : P} filter, {expr : x \in S} set_map), binary set ops (\union, \intersect, \ difference, \subseteq, \in), unary set ops (SUBSET, UNION), integer range a..b, quantifiers (\E, \A, CHOOSE), function application (f[x] postfix, chained), DOMAIN f, EXCEPT (single- and multi-key), records ([a |-> 1, b |-> 2]), and Cardinality(...).
• Round-trip tests: real TLX spec with in_set(flags, power_set(nodes)) and cardinality(flags) >= 0 invariants re-emits as structured e(...) calls instead of raw-string comments.

Added (Sprint 54 — expression parser foundation)

• TLX.Importer.ExprParser — NimbleParsec-based TLA+ expression parser producing Elixir AST matching the form TLX.Expr.e/1 builds at DSL compile time. Foundation subset: integer/boolean literals, identifiers, parenthesization, equality/comparison/arithmetic/logical operators, implication (=>), equivalence (<=>), and IF ... THEN ... ELSE.
• TLX.Importer.TlaParser now attaches structured ASTs to actions (:guard_ast), transitions (:ast), and invariants (:ast) when bodies parse successfully. Raw-string fields preserved for tier-2 best-effort fallback per ADR-0013.
• TLX.Importer.Codegen emits structured e(<Macro.to_string(ast)>) calls when an AST is available, falling back to the string-replacement tla_to_elixir/1 path otherwise. Round-trip through mix tlx.import now produces real Elixir expressions, not comment-wrapped raw TLA+.
• Tests: 35 ExprParser unit tests (literals, operators, precedence, parens, IF/THEN/ELSE, error cases, Macro.to_string round-trip) + 4 Sprint-54-specific round-trip assertions on Counter spec.

[0.4.6] - 2026-04-18

Eight sprints of expressiveness and simulator work: every sprint-retro follow-up from 45–47 is closed, every basic TLA+ primitive gap identified by codebase audit is shipped.

Added

• case/do syntax inside e() — native Elixir case expressions transform at macro expansion into {:case_of, clauses} IR, emitting TLA+ CASE ... [] OTHER -> .... Supports literal atom/integer/string patterns and _ wildcard (mapped to :otherwise sentinel).
• :otherwise sentinel in case_of/1 clauses — emits TLA+ OTHER branch and is treated as always-truthy in the simulator.
• Tests: case/do emission across TLA+, PlusCal-C, PlusCal-P; simulator evaluation with literal patterns + wildcard.
• until(p, q) and weak_until(p, q) temporal operators — emit TLA+ (p) \U (q) (strong: q must eventually hold) and (p) \W (q) (weak: p may hold forever). Round-trip via Elixir emitter and Unicode U/W symbols via Symbols emitter.
• Set ops: difference(a, b) (a \ b), set_map(:var, :set, expr) ({expr : var \in set}), power_set(s) (SUBSET s), distributed_union(s) (UNION s).
• Sequence ops: concat(s, t) (s \o t), seq_set(s) (Seq(s) type constraint).
• New TLX.Tuples module with tuple([a, b, c]) → <<a, b, c>>. Imported into all DSL sections alongside Sets/Sequences/Temporal/Expr.
• Simulator support for all new ops (both AST-capture and direct-call forms) — except seq_set (infinite type constraint, not materializable).

Fixed

• Simulator: ops written inside e(...) in guards or invariants now evaluate correctly. Previously e(cardinality(set)), e(in_set(x, s)), e(len(q)), and 20+ other set/sequence/function ops raised FunctionClauseError because only the direct-call IR form was handled. Added AST-capture clauses delegating to the existing direct-call logic.
• Simulator case_of eval no longer drops matched clauses whose body evaluates to false or nil. Previously used Enum.find_value/2, which treats any falsy callback return as "no match found" and falls through to later clauses. Switched to Enum.reduce_while/3.

Added (arithmetic)

• Integer division: e(div(x, y)) → x \div y
• Modulo: e(rem(x, y)) → x % y
• Exponentiation: e(x ** y) → x^y
• Unary negation: e(-x) → -x

All four are AST-form only (inside e()) and use operators from the TLA+ Integers module (always extended). Simulator evaluates them via Kernel.div/2, Kernel.rem/2, and a tail-recursive integer_pow/2 (avoids :math.pow/2's float result).

Added (functions and Cartesian product)

• Function constructor: fn_of(:x, set, expr) → [x \in set |-> expr]. Simulator materializes as an Elixir map.
• Function set (type): fn_set(domain, range) → [domain -> range]. Emission-only — [S -> T] can be exponentially large; TLC handles it at model-check time.
• Cartesian product: cross(a, b) → (a \X b). Simulator builds a MapSet of 2-element lists.
• New TLX.Functions module wired into all DSL section imports alongside TLX.Sets, TLX.Sequences, TLX.Tuples, TLX.Temporal, TLX.Expr.

Added (sequence filtering)

• select_seq(:var, seq, pred) — sequence filter emitting TLA+ SelectSeq(s, LAMBDA var: pred). First TLX construct to emit LAMBDA. Signature mirrors filter/3, choose/3, set_map/3 (variable-first). Simulator filters using the bound variable, same semantics as filter.

[0.4.5] - 2026-04-14

Fixed

• mix tlx.check now emits TLA+ directly instead of PlusCal-C → pcal.trans. Eliminates false deadlocks from PlusCal's pc variable and removes one Java invocation.

Removed

• Dead code: translate_pluscal/2 and find_tla2tools/0 from Mix.Tasks.Tlx.Check (TLC.check/3 has its own jar detection).

[0.4.4] - 2026-04-14

Fixed

• PlusCal emitters: type_ok and member invariants now use quoted strings for atoms, matching action variable values. Previously invariants used bare constants while actions used strings, causing SANY/TLC failures.
• Simulator: ite/3, case_of/1, let_in/3 used outside e() now evaluate correctly. Previously compile_expr treated them as literals instead of routing to eval_ast.
• Simulator: {:expr, ast} nodes inside ite/case_of/let_in children now unwrapped during evaluation.

Added

• Property-based atom consistency tests: for every atom in a spec, verify each emitter uses its expected format consistently (quoted for PlusCal, bare for TLA+). Catches representation mismatches across emitters.
• Regression tests for simulator ite/3, case_of/1, let_in/3 outside e().

Changed

• Forge example specs moved to the Forge project (~/Projects/Forge/specs/).

[0.4.3] - 2026-04-14

Added

• Reference: TLA+↔TLX comprehensive mapping (docs/reference/tlaplus-mapping.md)
• Reference: TLA+ unsupported constructs with workarounds (docs/reference/tlaplus-unsupported.md)
• 3 OTP pattern examples: StateMachine, GenServer, Supervisor (examples/patterns/)
• Multi-format diagram examples: DOT, Mermaid, PlantUML, D2 (examples/diagrams/)
• examples/README.md — index of all specs, patterns, and diagrams
• Roadmap: Sprints 44–47 (state coverage, case/do in e(), until/weak_until, set/sequence/tuple gaps)

[0.4.2] - 2026-04-14

Changed

• Extract shared TLX.Emitter.Graph module from diagram emitters — DOT, Mermaid, PlantUML, D2 now consume struct directly instead of regex-parsing DOT text output
• C4 architecture model updated for v0.4.0 features (extractors, patterns, skills, Graph module)

Added

• CONTRIBUTING.md: call for contributors (BEAM languages, TLA+, Ash/Reactor/Broadway reviewers)
• usage-rules.md updated for v0.4.0 (patterns, extractors, skills)

[0.4.1] - 2026-04-13

Added

• Diátaxis documentation for v0.4.0 features:
  • Tutorials: extract-and-verify, visualize-a-spec
  • How-tos: extract-from-otp, extract-from-frameworks, use-otp-patterns, generate-diagrams, audit-spec-coverage
  • Explanations: extraction-architecture, patterns-vs-defspec
  • References: mix-tasks (updated with 8 new tasks + PlantUML/D2), otp-patterns, extractors
• CHANGELOG v0.4.0 entry
• Updated README, getting-started, internals for v0.4.0
• model-a-genserver.md: note about extractor shortcut

[0.4.0] - 2026-04-01

Added

• OTP verification patterns: StateMachine, GenServer, Supervisor — reusable macros generating complete specs from declarative options
• 7 extractors for auto-generating spec skeletons from existing code:
  • Elixir source AST: gen_statem, GenServer, LiveView
  • BEAM abstract_code: Erlang gen_server, gen_fsm
  • Runtime introspection: Ash.StateMachine, Reactor
  • Source AST: Broadway pipelines
• 3 diagram emitters: Mermaid (GitHub markdown), PlantUML (enterprise), D2 (Terrastruct)
• 4 agent skills: formal-spec (with enrichment workflow), spec-audit, visualize, spec-drift
• 8 new mix tasks: gen.from_gen_server, gen.from_live_view, gen.from_erlang, gen.from_ash_state_machine, gen.from_reactor, gen.from_broadway, emit formats plantuml and d2
• ADR-0011 (OTP patterns as verification templates)
• ADR-0012 (OTP extraction strategy — tiered fallback)
• Diátaxis documentation: 2 tutorials, 5 how-tos, 2 explanations, 3 references for v0.4.0 features
• Dev dependencies: ash, ash_state_machine, broadway (dev/test only)

[0.3.3] - 2026-04-01

Added

• GraphViz DOT emitter (--format dot) — state machine diagrams from specs
• DOT files for all examples (mutex, raft_leader, two_phase_commit)

[0.3.2] - 2026-04-01

Added

• ADRs 4-10: architectural decisions (emit not reimplement, expr wrapper, Format module, auto atoms, Mix task naming, PlusCal wrapping, usage_rules)
• Internals documentation for contributors (docs/explanation/internals.md)
• C4 model updated with importers, emitter components, formal-spec skill, Hex.pm
• Sprint 23/24 plans and retrospectives

Fixed

• Moduledoc examples updated to flat DSL syntax (removed obsolete section wrappers)
• Sprint index README updated (was stuck at Sprint 12)
• TlaParser supported TLA+ subset documented
• README status updated: published on Hex

[0.3.1] - 2026-03-31

Added

• mix tlx.list — discover and list all TLX.Spec modules with entity counts
• mix tlx.watch — file watcher with auto-recompile and re-simulate on changes
• SANY and pcal.trans toolchain validation (87 integration tests)
• AllConstructs comprehensive spec covering every DSL construct
• SECURITY.md with vulnerability disclosure policy
• GitHub Actions CI workflow with Dependabot
• CONTRIBUTING.md background and collaboration invite
• All docs as ex_doc extras grouped by Diátaxis category (52 HTML pages)

Fixed

• Map defaults (%{}) now emit valid TLA+ ([x \in {} |-> 0])
• Atoms inside e(if ...) now collected by TLX.Emitter.Atoms
• Multi-action PlusCal specs wrap in while(TRUE) { either/or } for pcal.trans
• Mix task modules renamed to Mix.Tasks.Tlx.* (Mix discovery convention)
• Empty list default documented: use variable :q do default [] end

[0.3.0] - 2026-03-31

Added

• SPDX copyright and license headers on all source files (REUSE-compliant)

[0.2.11] - 2026-03-31

Added

• Record construction: record(a: 1, b: 2) → [a |-> 1, b |-> 2]
• Multi-key EXCEPT: except_many(f, [{k1, v1}, ...]) → [f EXCEPT ![k1] = v1, ...]
• Symbols emitter (--format symbols) — TLX DSL with math notation (□ ◇ ∧ ∨ ¬ ∀ ∃ ∈)
• FAQ.md — pronunciation, Java requirements, Unicode symbols

Changed

• Replaced Unicode emitter (TLA+ structure) with Symbols emitter (TLX DSL structure)
• PlusCal emitter renamed to PlusCalC; added PlusCalP for P-syntax
• Module naming standardized: TLX (all caps) throughout

[0.2.10] - 2026-03-31

Added

• Sequence operations: len/1, append/2, head/1, tail/1, sub_seq/3 (requires extends [:Sequences])
• DOMAIN: domain(f) → DOMAIN f
• Range sets: range(a, b) → a..b
• Implication: implies(p, q) → p => q
• Equivalence: equiv(p, q) → p <=> q
• Configurable EXTENDS: extends [:Sequences] DSL option

[0.2.9] - 2026-03-31

Added

• Function application: at(f, x) → f[x], except(f, x, v) → [f EXCEPT ![x] = v]
• CHOOSE: choose(:var, :set, expr) → CHOOSE var \in set : expr
• Set comprehension: filter(:var, :set, expr) → {var \in set : expr}
• CASE: case_of([{cond, val}, ...]) → CASE cond -> val [] ...
• if syntax inside e() — e(if cond, do: x, else: y) emits IF cond THEN x ELSE y
• let_in block style — let_in :var, binding do body end
• Diátaxis documentation: 4 how-to guides, 3 explanation pages, getting-started rewrite
• Reference documentation: DSL, mix tasks, expressions
• CONTRIBUTING.md with documentation tone guidelines

[0.2.8] - 2026-03-31

Added

• Refinement checking: refines AbstractSpec do mapping :var, e(expr) end
• TLA+ INSTANCE/WITH emission for spec-vs-spec comparison
• Auto-declare atom model values as CONSTANTS (TLA+ and .cfg)
• formal-spec agent skill — workflow from ADR to refinement-checked specs
• usage-rules.md — package-level AI guidance for consumers

Fixed

• Branched action TLA+ emission: UNCHANGED inside disjunctions
• Handle 3-tuple AST forms for ite/let_in/set ops inside e()
• Abstract spec atoms auto-included in INSTANCE identity mappings

[0.2.7] - 2026-03-31

Added

• IF/THEN/ELSE: ite(cond, then, else) → IF cond THEN then ELSE else
• Set operations: union/2, intersect/2, subset/2, cardinality/1, set_of/1, in_set/1
• Non-deterministic set pick: pick :var, :set do ... end
• Custom Init: initial do constraint(...) end
• LET/IN: let_in(:var, binding, body) → LET var == binding IN body

[0.2.6] - 2026-03-30

Added

• NimbleParsec TLA+ parser (replaces regex importer)
• PlusCal parser for C-syntax and P-syntax
• AST-based code generation via Code.format_string!/1
• Round-trip fidelity tests: emit → parse → codegen preserves structure

[0.2.5] - 2026-03-30

Added

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

[0.2.4] - 2026-03-30

Added

• TLC integration tests against real tla2tools.jar subprocess
• Tests tagged @integration, excluded from default mix test

Fixed

• TLC exit code handling — any non-zero now parses output for violations
• Trace extraction regex updated for real TLC 2.19 output format

[0.2.3] - 2026-03-30

Added

• TLA+ importer (mix tlx.import) — parse .tla files into Tlx DSL source
• GenStateMachine skeleton generator (mix tlx.gen.from_state_machine)
• Tlx.Importer.TlaParser — extracts variables, constants, Init, actions, invariants

[0.2.2] - 2026-03-30

Added

• Two-Phase Commit example (examples/two_phase_commit.ex)
• Raft leader election example (examples/raft_leader.ex)
• Simulator found and helped fix two Raft bugs: vote clearing on step-down and stale-term quorum checks

[0.2.1] - 2026-03-30

Added

• Auto-generated TypeOK invariant for enum-like variables
• Empty action compile-time warning (actions with no transitions)
• "Did you mean?" suggestions for undeclared variable errors (Levenshtein)
• Source location in verifier error messages
• Simulator constant injection: simulate(Spec, constants: %{max: 3})

[0.2.0] - 2026-03-30

Added

• e() macro — replaces verbose {:expr, quote(do: ...)} syntax
• await as alias for guard — reads naturally for PlusCal users
• defspec macro — shorthand for defmodule + use Tlx.Spec
• Flat top-level sections — no variables do ... end wrappers needed
• Bare literals — next :x, 0 without e() wrapping
• Batch next — next flag1: true, turn: 2 keyword list form
• transitions macro as alias for batch next
• Auto-imported Tlx.Temporal operators in invariants and properties sections
• Positional default on variable — variable :x, 0
• Positional expr on invariant and property — invariant :bounded, e(x >= 0)
• Unicode math pretty-printer (mix tlx.emit MySpec -f unicode) — ≜ ∧ ∨ ¬ □ ◇ ∀ ∃
• Elixir DSL round-trip emitter (mix tlx.emit MySpec -f elixir)
• Generated .tla files for examples

Changed

• Breaking: DSL sections are now top-level (no wrapping do blocks)
• Breaking: {:expr, quote(do: ...)} replaced by e() macro
• Breaking: invariant and property take expr as positional arg, not expr: keyword

[0.1.7] - 2026-03-30

Added

• Producer-consumer bounded buffer example (examples/producer_consumer.ex)
• Getting-started tutorial (docs/tutorials/getting-started.md)
• Hex.pm package metadata and LICENSES directory (REUSE compliance)
• Edge case tests (empty specs, invariant-only specs, single-state traces)
• Phase 4 substantially complete

[0.1.6] - 2026-03-30

Added

• Trace formatter (Tlx.Trace) — numbered states with variable diffs, compact/verbose modes
• Spark formatter config (spark_locals_without_parens) for DSL calls
• Spark cheat sheet generation (documentation/dsls/DSL-Tlx.md)
• ExDoc includes DSL reference as extra
• Phase 3 complete

[0.1.5] - 2026-03-30

Added

• Elixir simulator (Tlx.Simulator) — random walk state exploration with invariant checking
• mix tlx.simulate task — run simulations from CLI with configurable steps/runs/seed
• Peterson's mutual exclusion example (examples/mutex.ex)
• Simulator found and helped fix a real bug in the initial mutex spec

Fixed

• Atom formatting consistency: TLA+ emitter uses bare model values, PlusCal uses quoted strings
• Boolean literals emit as TRUE/FALSE in both emitters

[0.1.4] - 2026-03-30

Added

• Temporal properties: always, eventually, leads_to via Tlx.Temporal
• Fairness annotations: :weak (WF) and :strong (SF) on actions and processes
• Quantifiers: forall and exists emit \A / \E in TLA+
• Spec formula generation: Init /\ [][Next]_vars /\ Fairness
• vars tuple emission for all state variables
• PROPERTY declarations in .cfg output
• Phase 2 complete

[0.1.3] - 2026-03-30

Added

• Process declarations: process :name do set(:const); action ... end
• Multi-process PlusCal emission with process (Name \in Set) blocks
• TLC integration (Tlx.TLC) — invoke TLC, parse output, extract counterexample traces
• Config file generation (Tlx.Emitter.Config) — SPECIFICATION, CONSTANTS, INVARIANTS
• mix tlx.check task — emit, translate, run TLC, report pass/fail
• Verifier checks process action transitions for undeclared variables

[0.1.2] - 2026-03-30

Added

• PlusCal emitter (Tlx.Emitter.PlusCal) — C-syntax with labels, await, either/or
• Non-deterministic choice: branch entity for either/or within actions
• mix tlx.emit task — emit TLA+ or PlusCal from CLI
• Multi-variable UNCHANGED handling verified and tested
• Verifier now checks branch transitions for undeclared variables

[0.1.1] - 2026-03-29

Added

• Spark DSL extension: variables, constants, actions (guard + next), invariants
• Internal IR structs (Tlx.Variable, Tlx.Constant, Tlx.Action, Tlx.Transition, Tlx.Invariant)
• TLA+ emitter (Tlx.Emitter.TLA) — generates valid .tla files from compiled specs
• Compile-time verifier: undeclared variable references in next produce errors
• Info module (Tlx.Info) for Spark introspection
• Foundational ADRs (0001, 0002, 0003)
• C4 architecture model (Structurizr DSL)
• Quality gates (lefthook, gitleaks, credo, dialyxir)
• Roadmap and Sprint 1 plan
• usage_rules for Spark AI documentation

[0.1.0] - 2026-03-29

Added

• Initial project structure
• Elixir/Spark project scaffold
• Diátaxis documentation framework