TLX.Importer.Codegen (TLX v0.5.2)

Copy Markdown

Generates TLX DSL source code from a parsed spec map.

Builds Elixir source strings using Code.format_string!/1 for guaranteed syntactically correct output. Accepts the standard parsed map from TlaParser.parse/1 or PlusCalParser.parse/1.

Summary

Functions

from_broadway(spec_name, source_module, result)

Generate a TLX spec skeleton from a Broadway pipeline.

from_gen_server(spec_name, source_module, result)

Generate a TLX spec skeleton from GenServer callback info.

from_live_view(spec_name, source_module, result)

Generate a TLX spec skeleton from LiveView callback info.

from_reactor(spec_name, source_module, result)

Generate a TLX spec skeleton from a Reactor workflow.

from_state_machine(spec_name, source_module, result)

Generate a TLX spec skeleton from GenStateMachine callback info.

tla_to_elixir(expr)

Translate a TLA+ expression string to Elixir syntax.

to_tlx(parsed)

Convert a parsed spec map into formatted TLX DSL source code.

Functions

from_broadway(spec_name, source_module, result)

Generate a TLX spec skeleton from a Broadway pipeline.

Accepts an extraction result map from TLX.Extractor.Broadway with :producers, :processors, :batchers.

from_gen_server(spec_name, source_module, result)

Generate a TLX spec skeleton from GenServer callback info.

Accepts an extraction result map from TLX.Extractor.GenServer with :fields, :calls, :casts, :infos.

from_live_view(spec_name, source_module, result)

Generate a TLX spec skeleton from LiveView callback info.

Accepts an extraction result map from TLX.Extractor.LiveView with :fields, :events, :infos. Delegates to from_gen_server/3 since both share the multi-field state model.

from_reactor(spec_name, source_module, result)

Generate a TLX spec skeleton from a Reactor workflow.

Accepts an extraction result map from TLX.Extractor.Reactor with :inputs, :steps, :return, :graph.

from_state_machine(spec_name, source_module, result)

Generate a TLX spec skeleton from GenStateMachine callback info.

Accepts either:

  • An extraction result map from TLX.Extractor.GenStatem (with :transitions, :initial, etc.)
  • A legacy list of %{event, from_state} maps (backward compatibility)

Additional parameters:

  • spec_name — string module name
  • source_module — the inspected module name (for comments)

tla_to_elixir(expr)

Translate a TLA+ expression string to Elixir syntax.

to_tlx(parsed)

Convert a parsed spec map into formatted TLX DSL source code.

The map should contain:

  • :module_name — string
  • :variables — list of variable name strings
  • :constants — list of constant name strings
  • :init — list of "var = val" strings (for defaults)
  • :actions — list of %{name, guard, transitions} maps
  • :invariants — list of %{name, expr} maps
  • :processes — (optional) list of %{name, set, actions, variables} maps