| > I'm not sure what you're calling "spec" vs "model" This is from memory, but the TLA+ toolkit distinguishes between your "specification of your algorithm" and a (bounded) "model of your specification". So, you might have some spec for a sorting function that works for arrays of natural numbers of arbitrary length. And your model would limit it to arrays of length 5, and "define" the natural numbers to be `range(0,10)` -- ie. you are checking a finite "model". I think this is consistent with the language used in the wiki article (the OP). > You can see how I'm working against the way TLA wants to work I'd much prefer your suggested workflow. I don't recall that you can write plain old 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 always meant to publish these after XSA-299 went public, but haven't gotten around to it. Please do! > It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly. That seems like a really tractable problem to me, if the C files were written with this in mind. I've actually been thinking about this since giving an internal talk on my TLA+ project last week! |
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
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.