TLA+ Formal Modeling and Programmers: Avoiding the Imperative “Brainwash”

4 points

5 years ago

I use the term brainwash as satire. Of course, the programmer imperative sensibility is quite important if you want to ship product, which is the bottom line.

But I've found the imperative mentality in my own work on TLA+ modeling initially confusing. I offer the following write-up to help clarify several important points (focusing on TLA+ Pluscal) in a technical note with example models, Python code. It's the first in a series on modeling a distributed key-value store I'm working on:

https://github.com/rodgarrison/tla_note1

Beyond basics I also give a recipe to use TLA+ at the command line for those of us who prefer it over IDEs. TLA's toolbox IDE is nice; still I prefer command line development when possible.

In the paper:

- program behavior versus model states

- deadlock

- termination

- coverage (label) checks

- setting up TLA+ on the command line

Hope it helps. As I note in the abstract I got some help of my own from the TLA Google Group.

2 comments