Re: [tlaplus] Are there any guides on writing our own PlusCal translators?

I've been thinking a lot about custom tooling workflows in the context of TLA+ recently. As a result, I made a survey of all PlusCal variants that have been written about. The general conclusion is that their codebases are forks of the toolbox itself. Off the top of my head: Distributed PlusCal, Choreographic PlusCal, Erla+ is a custom codegen tool but does this also. A rarer alternative is to use a completely home-grown stack, such as PGo. I know I missed some more prototypes, but hopefully that illustrates what I'm saying.

That doesn't mean people didn't use the feature, but it does mean that all examples I know of people successfully extending PlusCal didn't.

Of course, this isn't really an answer to your actual question. I'd also be interested if anyone chimed in with usage examples of this feature I just learned about.

Best,

-Finn

On Tue, Jul 15, 2025 at 1:35 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:

I noticed in this option in the pluscal manual:

-spec name This option is used to have the translation performed by ex-
ecuting a TLA+ specification instead of by the translator itself. It
causes the translator to write to the file AST .tla in the current direc-
tory a TLA+ module that defines ast to equal a TLA+ representation
of the algorithm’s abstract syntax tree (AST) and fairness to equal
the fairness option. (The current directory is the one from which the
translator is run.) The translator then copies the files name.tla and
name.cfg from its own internal directory to the current directory, runs
TLC on name.tla, and uses TLC’s output to produce the translation.

So it seems like there is at least some functionality for writing custom extensions to PlusCal. Has anybody written more about this / are there any demonstrative examples online?

(The paragraph after immediately warns about limitations of this (no formatting, doesn't handle bulleted lists of conjuncts), so I'm mostly asking out of curiosity.)

H

--
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/7124c16e-6f35-4632-8946-5934766f0fe9%40gmail.com.