Idiomatic TLA+
For example multiple assignments in Python:
x = y = z = 'foo'
or formatting strings:
def user_info(user):
return 'Name: {user.name} Age: {user.age}'.format(user=user)
or swap values:
b, a = a, b
or even conditional expression in C. The C language has a ternary expression
(using the two operators ?
and :
) and corresponding C idiom is:
b = a == 4 ? 5 : a - 1;
TLA+ has it’s own idioms and Leslie Lamport described some of them in his great book “Specifying Systems” (Chapter 7. Writing a specification. Some advice.).
The benefits of being familiar with idioms, particularly the larger ones, is that when looking at code you can see several lines of code but because it is familiar as a particular idiom you can mentally represent and think about the code as that single idiom instead of having to necessarily read and comprehend each line individually.
In turn authors of Apalache collect specification idioms that aid them in writing TLA+ specifications. These idioms are quite likely different from the original ideas of Leslie Lamport (the author of TLA+). Apalache documentation describes more TLA+ idioms and I like them a lot.
Let me list all of them here:
- Keep state variables to the minimum
- Update state variables with assignments
- Apply primes only to state variables
- Isolate updates to
VARIABLES
- Isolate non-determinism in actions
- Introduce pure operators
- Introduce a naming convention for operator parameters
- Use Boolean operators in actions, not
IF-THEN-ELSE
CHOOSE
smart, prefer\E
- Do not over-structure
- Do not over-modularize
- Separate normal paths from error paths
- Do you really need those nice recursive operators?
- Do you really need set cardinalities?
- Do you really need integers?