Idiomatic TLA+

Authors: Shon Feder, Igor Konnov + (who likes to contribute?)

This document is under construction. If you like to contribute, open a pull request.

Introduction

In this document, we collect specification idioms that aid us in writing TLA+ specifications that are:

  1. understood by distributed system engineers,
  2. understood by verification engineers, and
  3. 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+.

The idioms

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? ๐Ÿ”ข