Composing TLA+ Specifications with State Machines
Skip to Content
New: Logic for Programmers is now content-complete and in the hands of the copy editor! Get the current beta for 20% off here.
Hillel Wayne
Posted on<br>Jun 17, 2024
Last year a client asked me to solve a problem: they wanted to be able to compose two large TLA+ specs as part of a larger system. Normally you’re not supposed to do this and instead write one large spec with both systems hardcoded in, but these specs were enormous and had many internal invariants of their own. They needed a way to develop the two specs independently and then integrate them with minimal overhead.
This is what I came up with. Warning: this is a complex solution is aimed at advanced TLA+ users. For a much (much) gentler introduction, check out my website learntla.
The example
Let’s start by giving a motivating system:<br>a Worker sends an authentication request to a Server . If the password matches the server’s internal password, the server responds “valid”, otherwise it responds “invalid”. If the worker receives “invalid” as a response, it goes into an error state. The worker can retry from that state and submit a new authentication request.
The worker and server have shared state via the request/response. As an additional complication, we’ll add internal state to the server, in the form of a request log that is hidden from the worker.
We can use this example to show the problems of composition and my solution (though I’ll say the example is a little too simple to make it worthwhile).
The problem with composition
What we want is for the composition to be as simple and painless as possible. If our specs are WorkerSpec and ServerSpec, the easiest composition would just be
CombinedSpec == WorkerSpec /\ ServerSpec
I talk about the problems we have in-depth here, but the gist is that if ServerSpec and WorkerSpec are “normal” specs, they’ll place contradictory constraints on the shared variables.
For example, WorkerSpec will likely read the server response, but not modify it. So to run WorkerSpec independently of the composition, we have to say the response never changes, which is equivalent to saying we can’t change it, which makes it impossible for ServerSpec to send a response!
The normal way around this is to break apart both WorkerSpec and ServerSpec into collections of actions, and then carefully stitch them together in non-contradictory ways. Which is about as complex as it sounds: composing two specs can be as much work as writing them in the first place.
This is why I’m trying to find a better way.
The big idea
What we need to do is write specs intended to represent part of the world and then incorporate them into a “whole world” main spec. To do this, we’ll use one of TLA+’s most powerful features: we can use x' to both assign the next value to x and constrain what the next value can be. Say we have
VARIABLE x, y
Foo ==<br>/\ x' \in {0, 1}<br>/\ y' \in {0, 1}
Bar == x' y'
Next == Foo /\ Bar
When TLC<br>evaluates Next, it reads x' and y' in Foo as assignments. There are four possible assignments, so the model checker evaluates them all.
Then, since x' and y' are already chosen, TLC reads the statement in Bar as a constraint. Three of the possible assignments break that constraint, so TLC eliminates those possibilities, leaving us with a unique next state.
This means that a Spec Q can take two specs, X and Y, and constrain them against each other. X can have an action Inc that increments x_log, and then Q says that Inc can only happen if y_flag is true. Similarly, Q can make one assignment trigger another:
Inc ==<br>/\ x_log' = x_log + 1
Sync ==<br>IF ~y_flag /\ y_flag'<br>THEN Inc<br>ELSE TRUE
Next == (X!Next \/ Y!Next) /\ Sync
Now, changing y_flag to true forces an increment in x_log. Q is using one spec to drive side-effects in the system.
This is just a state machine! Constraints on transitions are just guard clauses and assignments on transitions are just effects. These can be enforced on other specifications that the state machine doesn’t know about.
Here’s how to make this idea work in practice:
Write an abstract state machine for all of the high-level state transitions of the core component
Write the other components as “open” specs that don’t fully describe their next states.
Refine the core component into the main spec, with a Sync action that adds guards and side-effects to the state transitions.
The Solution
We’ll model this with three separate specs: workerSM.tla, server.tla, and system.tla.
The state machine
Since the whole system is based around the worker’s state machine, let’s start with workerSM.tla. This won’t represent what happens when the worker transitions states, just what the transitions are.
(source)
------------------- MODULE workerSM...