Re: [tlaplus] TLX — TLA+ specifications in Elixir syntax, with TLC integration

Hello, Andrew.

Is the input DSL itself a subset of valid Elixir code? Thanks,

Yes. But… 🙂

Elixir compiles to the BEAM virtual machine, and provides a macro system to generate or transform code at compile-time [1].

Elixir libraries usually take advantage of this to provide high-level, declarative, and often pipeline-oriented, DSL. [2] [3]

In TLX, I'm using the Spark[4] library to provide a specification DSL, based on TLA+ constructs like defspec, variables/constants, actions, awaits/guards, next, branches, invariants, refines, etc.

Under the hood, the spec is transformed to an IR (based on Elixir structs) that is used by TLX Emitters to output TLA+, PlusCal, DOT, mermaid, D2,... or by tools like the TLX Simulator. TLX Extractors and Importers can also generate IR from TLA+ specs or State Machines from Elixir code.

HTH,

Georges

---

[1] see the meta-programming section in the Elixir docs: https://hexdocs.pm/elixir/main/quote-and-unquote.html

[2] Plug, a specification for composing web applications with functions: https://hexdocs.pm/plug/readme.html#hello-world-websockets

[3] Ash, a declarative application framework: https://hexdocs.pm/ash/what-is-ash.html

[4] "Spark is a framework for creating declarative domain-specific languages in Elixir. It transforms simple struct definitions into rich, extensible DSLs that come with autocomplete, documentation generation, and sophisticated tooling built right in." (https://github.com/ash-project/spark?tab=readme-ov-file)

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/351DFFB1-ADFB-4DAA-B37C-9784B71E5B65%40gmail.com.