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 wan...
