TLX.Importer.TlaParser (TLX v0.5.2)

Copy Markdown

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

Handles TLA+ output from TLX's own emitter and simple hand-written specs.

Supported TLA+ Subset

  • ---- MODULE Name ---- header and ==== footer
  • EXTENDS clause (comma-separated module list)
  • VARIABLES and CONSTANTS declarations (comma-separated)
  • Operator definitions: Name == body (captures body as a raw string)
  • Multi-line operator bodies (stops at next top-level definition or footer)

Not Supported

  • RECURSIVE operator declarations
  • LAMBDA expressions
  • INSTANCE / WITH (module composition)
  • ASSUME / THEOREM / PROOF
  • LET/IN at the module level (works inside operator bodies as raw text)
  • Nested module definitions
  • Operator parameters: Op(x, y) == ... (parsed as a raw body, not decomposed)

How It Works

The parser extracts structural elements (module name, variables, constants, operator names and bodies) without deeply parsing TLA+ expressions. Operator bodies are captured as raw strings. The build_map/1 function then uses heuristics to identify Init predicates, actions (by looking for primed variables x'), and invariants (operators without primed variables).

For full expression parsing, use TLC directly via mix tlx.check.

Summary

Functions

compute_coverage(parsed)

Compute parse coverage stats from a parsed spec map.

parse(tla_string)

Parse a TLA+ string and return a map of extracted spec components.

parse_tla(binary, opts \\ [])

Parses the given binary as parse_tla.

to_tlx(parsed)

Convert parsed TLA+ into TLX DSL source code.

Functions

compute_coverage(parsed)

Compute parse coverage stats from a parsed spec map.

Returns a map with :attempted (total expressions we tried to parse) and :fallbacks (how many fell back to raw string). Consumers (like mix tlx.import --verbose) render this as a summary table.

parse(tla_string)

Parse a TLA+ string and return a map of extracted spec components.

parse_tla(binary, opts \\ [])

@spec parse_tla(binary(), keyword()) ::
  {:ok, [term()], rest, context, line, byte_offset}
  | {:error, reason, rest, context, line, byte_offset}
when line: {pos_integer(), byte_offset},
     byte_offset: non_neg_integer(),
     rest: binary(),
     reason: String.t(),
     context: map()

Parses the given binary as parse_tla.

Returns {:ok, [token], rest, context, position, byte_offset} or {:error, reason, rest, context, line, byte_offset} where position describes the location of the parse_tla (start position) as {line, offset_to_start_of_line}.

To column where the error occurred can be inferred from byte_offset - offset_to_start_of_line.

Options

  • :byte_offset - the byte offset for the whole binary, defaults to 0
  • :line - the line and the byte offset into that line, defaults to {1, byte_offset}
  • :context - the initial context value. It will be converted to a map

to_tlx(parsed)

Convert parsed TLA+ into TLX DSL source code.

Delegates to TLX.Importer.Codegen.to_tlx/1.