I touched on this topic in a blog post I wrote a while back called "
TLA+ is more than a DSL for breadth-first search" but the thesis has developed a bit more as I've been reading
A Science of Concurrent Programs. I think one big reason TLA+ works so well (and is so interesting!) is there is a hierarchy of understanding its model, where going up a step corresponds to being able to use more and more of the language. I propose the steps as being:
- TLA+ specs generate a finite state machine
- TLA+ specs generate a set of behaviors
- TLA+ specs are predicates on the set of all possible behaviors
I think people usually start off at level 1, thinking of TLA+ as generating a simple finite state machine - a concept familiar to programmers. Armed with this understanding you can write meaningful precise specs and safety properties, as well as basic liveness properties conceived as reachability properties of the state graph.
Level 2 is when you stop thinking of TLA+ specs as a breadth-first search of a finite state machine and start thinking of it as generating a set of infinite traces of that machine. This enables you to use & understand more-advanced liveness properties and refinement - or rather, you start thinking of liveness properties as being a type of refinement.
Level 3 is when you start thinking of TLA+ specs as predicates on the space of all possible behaviors - sequences of assignments of all possible values to all possible variables. This is a very abstract way to look at it and is necessary to fully understand the proof rules for the language.
Thoughts? Is this a good paradigm for the learning sequence of the language? Are there other steps, different steps?
Andrew Helwer