[gwd]

> This is from memory, but the TLA+ toolkit distinguishes between your "specification of your algorithm" and a (bounded) "model of your specification".

That's right, I'm remembering now. So yeah, the "models" are the ".cfg" files (which as you can see from the Makefile snippet are actually specified with the "-config" argument.

The .pcal files are actually just "normal" TLA files with the generated content replaced with

    \* BEGIN TRANSLATION
    \* END TRANSLATION

pcal.trans doesn't check to see that there's something there, since it's just going to throw it away. So I call them .pcal, but they're "really" non-generated TLA + pcal.

> It's amusing that you want some TLA CLI tools that work kind of how the LaTex toolkit works, another of Leslie Lamport's contributions...

I've got a number of tools I've written for my own personal use over the years, and TLA+ has "one person spent a few decades being both sole author and user" fingerprints all over it. :-)

> Please do!

Tomorrow I'll look through things and if it's suitable I'll post my git repo somewhere.