Authors: Shon Feder, Igor Konnov + (who likes to contribute?)
This document is under construction. If you like to contribute, open a pull request.
In this document, we collect specification idioms that aid us in writing TLA+ specifications that are:
- understood by distributed system engineers,
- understood by verification engineers, and
- understood by automatic analysis tools such as the Apalache model checker.
If you believe, that the above points are contradictory when put together, it is to some extent true. TLA+ is an extremely general specification language. As a result, it is easy to write a short specification that leaves a human reader puzzled . It is even easier to write a (syntactically correct) specification that turns any program trying to reason about TLA+ to dust.
Nevertheless, we find TLA+ quite useful when writing concise specifications of distributed protocols at Informal Systems. Other specification languages -- especially, those designed for software verification -- would require us to introduce unnecessary book-keeping details that would both obfuscate the protocols and make their verification harder. However, we do not always need "all the power of mathematics", so we find it useful to introduce additional structure in TLA+ specifications.
Below, we summarize the idioms that help us in maintaining that structure. As a bonus, these idioms usually aid the Apalache model checker in analyzing the specifications. Our idioms are quite likely different from the original ideas of Leslie Lamport (the author of TLA+). So it is useful to read Lamport's Specifying Systems. Importantly, these are idioms, not rules set in stone. If you believe that one of those idioms does not work for you in your specific setting, don't follow it.
If this is the first page where you encounter the word "TLA+", we do not recommend that you continue to read the material. It is better to start with The TLA+ Video Course by Leslie Lamport. Once you have understood the basics and tried the language, it makes sense to ask the question: "How do I write a specification that other people understand?". We believe that many TLA+ users reinvent rules that are similar to our idioms. By providing you with a bit of guidance, we hope to reduce your discomfort when learning more advanced TLA+.
Idiom 0: Keep state variables to the minimum 🔋
Idiom 1: Update state variables with assignments 📅
Idiom 2: Apply primes only to state variables 📌
Idiom 3: Isolate updates to VARIABLES 👻
Idiom 4: Isolate non-determinism in actions 🔮
Idiom 5: Introduce pure operators 🙈
Idiom 6: Introduce a naming convention for operator parameters 🛂
Idiom 7: Use Boolean operators in actions, not IF-THEN-ELSE 🙅
Idiom 8: CHOOSE smart, prefer \E 💂♂️
Idiom 9: Do not over-structure 🔬
Idiom 10: Do not over-modularize 🦆
Idiom 11: Separate normal paths from error paths. ⚡
Idiom 12: Do you really need those nice recursive operators? 🌀
Idiom 13: Do you really need set cardinalities? 🍕
Idiom 14: Do you really need integers? 🔢