| Yes, I think I was more or less inspired by tlc-bin; but in the end it didn't give me the control that I wanted, so I ended up just putting the Java command into my Makefile. I'm not sure what you're calling "spec" vs "model"; I wrote stuff in PlusCal, which I checked into git; then used `make` to translate that into .tla automatically as needed. The .tla files are .gitignored, so don't choke up your commit history with machine-generated stuff. Here's a snippet of my Makefile: %.tla: %.pcal
cp $< $@
java -cp $(TLATOOLS_JAR) pcal.trans -nocfg $@
rm -f $*.old
.PHONY: all-sources
all: all-sources
SOURCETARGETS += XSA287.tla
TESTTARGETS += XSA287-A.out
XSA287-A.out: XSA287-A.cfg XSA287.tla
java -cp $(TLATOOLS_JAR) -XX:+UseParallelGC tlc2.TLC -config $< -workers 8 XSA287.tla | tee $@
The idea here is that doing "make" would simply compile all the .pcal files into .tla files (thus effectively doing a syntax check); but if you wanted to run any specific test, you would name the output file the test would generate.You can see how I'm working against the way TLA wants to work: It wants to take your PlusCal code at the beginning of the file and rewrite the end of the file, "helpfully" backing up the old file with a ".old" extension; I want to take plain PlusCal code and generate an intermediate file (like an object file) which is not checked in. So I have to copy $FOO.pcal to $FOO.tla, run `pcal.trans` on $FOO.tla, and then delete the useless "$FOO.tla.old" file. I always meant to publish these after XSA-299 went public, but haven't gotten around to it. > Do you mean you'd like to generate a TLA+ spec from your source code? Well obviously the whole project is so large as to be completely prohibitive. The model is written in the C-like variant of PlusCal, and uses a lot of the same variable names and such to help make sure they match the real C functions; and then translated into TLA. 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. |
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!