3 ms·

> And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracki

> And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]). This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether. > What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. Do you mean you'd like to generate a TLA+ spec from your source code? [0] https://github.com/pmer/tla-bin https://github.com/pmer/tla-bin [1] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/ForceMove.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183... [2] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/Version1.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183...

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.
  - 6y ago
hwayne 6y ago
I use a personal wrapper around the command line for most of my work. It's incomplete and has a few holes, but it gets the job done for me. https://github.com/hwayne/tlacli https://github.com/hwayne/tlacli
- agstewart 6y ago
  Thanks for your all your content on TLA+ -- learntla.com was very helpful!

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.
- 6y ago

hwayne 6y ago

I use a personal wrapper around the command line for most of my work. It's incomplete and has a few holes, but it gets the job done for me. https://github.com/hwayne/tlacli https://github.com/hwayne/tlacli

agstewart 6y ago
Thanks for your all your content on TLA+ -- learntla.com was very helpful!