## TLA⁺ is more than a DSL for breadth-first search

Although it isn’t usually taught that way, a lot of TLA⁺ newcomers develop the understanding that TLA⁺ is just a fancy domain-specific language (DSL) for breadth-first search. If you want to model all possible executions of a concurrent system - so the thinking goes - all you have to do is define:
The set of variables modeling your system The values of those variables in the initial state(s) Possible actions changing those variables to generate successor states Safety invariants you want to be true in every state The model checker will then use breadth-first search (BFS) to churn through all possible states (& thus execution orders) of your system, validating your invariants.
[Read More]