Symmetry reduction in TLA+ is a clever trick for cutting down the size of the state space we need to explore during model checking. Think about a distributed system with interchangeable components—servers, nodes, or processes that behave identically. Without symmetry reduction, the model checker wastes time exploring states that are essentially duplicates, differing only in the labels we’ve assigned to these components. Symmetry reduction says, “Hey, if swapping the identities of these components doesn’t change the behavior of the system, let’s treat those states as one.” This massively reduces the computational effort while keeping the results valid.
In this post, I’ll show some simple examples of symmetry using trivial specs where we can actually visualize the state space. The idea is to build a mental model of how symmetry reduction works.
Example 1 - Two counters
In this specification, in each step, one counter increments with the limitation that their max value is 2.
| ------------------------------ MODULE TwoCounters ------------------------------ | |
| EXTENDS Integers | |
| CONSTANTS Counters \* e.g. {c1, c2} | |
| VARIABLES counters | |
| Inc(c) == | |
| /\ counters[c] < 2 | |
| /\ counters' = [counters EXCEPT ![c] = @ + 1] | |
| Init == | |
| counters = [c \in Counters |-> 0] | |
| Next == | |
| \E c \in Counters : | |
| Inc(c) | |
| ============================================================================= |
Without symmetry we 9 unique states.
Fig 1. Two counters, without symmetry.
If we make the counters set symmetrical, we reduce this to 6 unique states. There is only one branch from the initial state because (c1 > 0 @@ c2 > 1) and (c1 > 1 @@ c2 > 0) are equivalent and can be collapsed into one state.
Fig 2. Two counters with symmetry
Example 2 - Two Counters, Two Nodes
In this variant we introduce another set: a set of Nodes. In each step, one node randomly chooses one counter to increment and it increments itself.
| ----------------------------- MODULE CountersNodes ----------------------------- | |
| EXTENDS Integers, FiniteSets, TLC | |
| CONSTANTS Counters, \* e.g. {c1, c2} | |
| Nodes \* e.g. {n1, n2} | |
| VARIABLES counter, | |
| node | |
| Inc(n, c) == | |
| /\ counter[c] < 2 | |
| /\ node' = [node EXCEPT ![n] = @ + 1] | |
| /\ counter' = [counter EXCEPT ![c] = @ + 1] | |
| Init == | |
| /\ counter = [c \in Counters |-> 0] | |
| /\ node = [n \in Nodes |-> 0] | |
| Next == | |
| \E n \in Nodes, c \in Counters : | |
| Inc(n, c) | |
| ============================================================================= |
Without symmetry, we see 27 unique states. If we look at the first branches from the initial state we see:
c1 = 0, c2 = 1 / n1 = 1, n2 = 0
c1 = 1, c2 = 0 / n1 = 1, n2 = 0
c1 = 0, c2 = 1 / n1 = 0, n2 = 1
c1 = 1, c2 = 0 / n1 = 0, n2 = 1
The final states are:
c1 = 2, c2 = 2 / n1 = 4, n2 = 0
c1 = 2, c2 = 2 / n1 = 3, n2 = 1
c1 = 2, c2 = 2 / n1 = 2, n2 = 2
c1 = 2, c2 = 2 / n1 = 1, n2 = 3
c1 = 2, c2 = 2 / n1 = 0, n2 = 4
Fig 3. Nodes and counters, without symmetry. Download link.
Both sets symmetrical
If we make both sets symmetrical, we get 11 unique states (down from 27).
Instead of 4 branches from the initial state, there is only 1! This is because all four initial states are symmetrical as they are composed of only the cross product of both symmetric sets.
Likewise, the final states are reduced to 3 from 5:
c1 = 2, c2 = 2 and n1 = 4, n2 = 0
c1 = 2, c2 = 2 and n1 = 3, n2 = 1
c1 = 2, c2 = 2 and n1 = 2, n2 = 2
This is because (c1 = 2, c2 = 2 / n1 = 4, n2 = 0) is symmetrical with (c1 = 2, c2 = 2 / n1 = 0, n2 = 4), and the same for the 3,1 pair.
Fig 4. Nodes and counters, where both sets are symmetrical. Download link.
Counter symmetry
What if we only made the counters symmetrical? Now we get 18 unique states.
There are two branches from the initial state (compared to 4 without symmetry and 1 with both sets as symmetrical). The same counter is incremented, but different nodes did the incrementing.
c1 = 1, c2 = 0 and n1 = 1, n2 = 0
c1 = 1, c2 = 0 and n1 = 0, n2 = 1
However, there are still 5 final states, like the no symmetry example! This is because the uniqueness of the final states is based on node state and the node set is not symmetrical.
Fig 5. Nodes and counters, where only the counter set is symmetrical. Download link.
Node symmetry
Let’s make the counters non-symmetrical and the nodes symmetrical.
Now we get 16 unique states. We get 2 branches from the initial state again, but this time always from the same node, to two different counters.
c1 = 1, c2 = 0 and n1 = 1, n2 = 0
c1 = 0, c2 = 1 and n1 = 1, n2 = 0
We get the same 3 final states and the double symmetry example, because the final states depend on node state (the counters have always reached the value 2).
c1 = 2, c2 = 2 and n1 = 4, n2 = 0
c1 = 2, c2 = 2 and n1 = 3, n2 = 1
c1 = 2, c2 = 2 and n1 = 2, n2 = 2
Fig 6. Nodes and counters, where only the node set is symmetrical. Download link.
Example 3 - Per node counters
In this example, we take the Node Counters example, but:
Assign each node a single counter. Nodes still non-deterministically try to increment random counters, but they can only do so if the counter is assigned to them.
Each node has an ok variable that records if its last attempt to increment was successful or not.
If a node chooses the right counter, it increments it and sets the ok variable to TRUE and if it chooses the wrong counter, it records ok as FALSE and increments nothing. In the initial state, the ok value of each node is TRUE.
| ----------------------------- MODULE PerNodeCounter ----------------------------- | |
| EXTENDS Integers, FiniteSets, TLC | |
| CONSTANTS Counters, | |
| Nodes | |
| VARIABLES counter, | |
| node, | |
| ok, | |
| mapping | |
| Inc(n, c) == | |
| /\ counter[c] < 2 | |
| /\ mapping[n] = c | |
| /\ node' = [node EXCEPT ![n] = @ + 1] | |
| /\ ok' = [ok EXCEPT ![n] = TRUE] | |
| /\ counter' = [counter EXCEPT ![c] = @ + 1] | |
| /\ UNCHANGED <<mapping>> | |
| Fail(n, c) == | |
| /\ counter[c] < 2 | |
| /\ mapping[n] = c | |
| /\ ok' = [ok EXCEPT ![n] = FALSE] | |
| /\ UNCHANGED <<mapping, node, counter>> | |
| Init == | |
| /\ counter = [c \in Counters |-> 0] | |
| /\ node = [n \in Nodes |-> 0] | |
| /\ ok = [n \in Nodes |-> TRUE] | |
| /\ mapping = CHOOSE m \in [Nodes -> Counters] : | |
| \A c \in Counters : | |
| \E n \in Nodes : c = m[n] | |
| Next == | |
| \E n \in Nodes, c \in Counters : | |
| \/ Inc(n, c) | |
| \/ Fail(n, c) | |
| ============================================================================= |
Without symmetry this gives us 25 unique states. The branches from the initial state are:
c1 = 0, c2 = 0 / n1 = 0, n2 = 0 / n1 = TRUE, n2 = FALSE
c1 = 1, c2 = 0 / n1 = 1, n2 = 0 / n1 = TRUE, n2 = TRUE
c1 = 0, c2 = 0 / n1 = 0, n2 = 0 / n1 = FALSE, n2 = TRUE
c1 = 0, c2 = 1 / n1 = 0, n2 = 1 / n1 = TRUE, n2 = TRUE
There is only a single final state as eventually all nodes choose their own counter 2 times.
Fig 7. Per node counters, without symmetry. Download link.
If we make the counter set symmetrical, it generates exactly the same state space. This is because the counters are tied to the nodes, and change in lock-step, and we didn’t change the symmetry of the nodes.
If we make only the nodes symmetrical, then again, we get exactly the same state space! Again because the two sets are linked and work in lock-step.
We must make both sets symmetrical to see a state space reduction. Now we only get 15 unique states.
There are only two branches from the initial state:
c1 = 0, c2 = 0 / n1 = 0, n2 = 0 / n1 = TRUE, n2 = FALSE
c1 = 1, c2 = 0 / n1 = 1, n2 = 0 / n1 = TRUE, n2 = TRUE
This is because of the following symmetries:
One fail:
c1 = 0, c2 = 0 / n1 = 0, n2 = 0 / n1 = TRUE, n2 = FALSE
c1 = 0, c2 = 0 / n1 = 0, n2 = 0 / n1 = FALSE, n2 = TRUE
One success
c1 = 1, c2 = 0 / n1 = 1, n2 = 0 / n1 = TRUE, n2 = TRUE
c1 = 0, c2 = 1 / n1 = 0, n2 = 1 / n1 = TRUE, n2 = TRUE
Fig 8. Per node counters, with both sets symmetrical. Download link.
How much can symmetry reduce the state space in these examples?
If I run the TwoCounters.tla with 5 nodes and 5 counters with symmetry it reduces the state space from 42, 228 unique states down to 193.
However, it can be computationally expensive for TLC to handle symmetry of large sets, and you may see it take multiple minutes for TLC to start model checking, or in some cases, fail to start at all because the number of permutations of the large sets is too much.
For example, with the final example, with 6 nodes and 6 counters, it takes TLC 5 minutes to get started, then it completes the model checking in around 1 second with 210 unique states found. Without symmetry it takes 20 seconds to find 15,625 unique states. In other words, symmetry can be counterproductive on larger sets. It all depends on the specifics of the specification.
In general, use of symmetry can reduce running time from minutes to seconds, hours to minutes, or simply make it possible at all to model check some configurations.
Be careful, there are gotchas
There are some gotchas with the use of symmetry, so it needs to be used cautiously. The main gotchas for me are:
Symmetry over large sets can be too computationally expensive. The time complexity of finding equivalences in symmetry reduction grows with the factorial of the set size because symmetry involves considering all possible permutations of the elements in the set. This is necessary to identify whether two states are equivalent under some permutation.
Symmetry often doesn’t play well with liveness checking as symmetry can disrupt liveness properties (e.g., "every process eventually gets the token") because it collapses equivalent states, potentially losing critical temporal paths.
Hidden asymmetry. If one member of a symmetrical set is treated differently for some reason, then it can cause invalid state space reductions. In general, it is best for the logic to treat all members equally. If you need special treatment for one member, encode that treatment in the state explicitly (to avoid false equivalence).
I plan to write about both of these points in more detail in the future.
Conclusions
Symmetry is a key tool for reducing the state space. In simple specs, it isn’t too hard to figure out how symmetry collapses the state space. However, as specs get more complex, with more relationships between sets, the impact of symmetry becomes harder to assess and internalize.
Symmetry isn’t magic—it’s a tool with sharp edges. If your components have hidden differences, like priority rules or subtly unique roles, symmetry reduction can merge states that aren’t truly equivalent. Therefore using symmetry requires some discipline: explicitly model any asymmetry, test your assumptions, and double-check that what you’re reducing is genuinely symmetric. When used correctly, symmetry reduction turns an overwhelming problem into something manageable, helping you verify complex systems in minutes, hours or even days, instead of requiring a planet-sized computer that can compute until the heat death of the universe.