3 ms·

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 int

by gwd 6y ago

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.

agstewart 6y ago
> 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!
- gwd 6y ago
  > 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.
- gwd 6y ago
  Not sure if you'll see this, but finally got around to posting my repo: https://gitlab.com/xen-project/people/gdunlap/tla https://gitlab.com/xen-project/people/gdunlap/tla

by gwd 6y ago

agstewart 6y ago

> 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!

gwd 6y ago
> 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.
gwd 6y ago
Not sure if you'll see this, but finally got around to posting my repo: https://gitlab.com/xen-project/people/gdunlap/tla https://gitlab.com/xen-project/people/gdunlap/tla