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
---
[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)