Extracting Symbolic Transitions from TLA$$^{}$$ Specifications

In \(\textsc {TLA}^{+}\), a system specification is written as a logical formula that restricts the system behavior. As a logic, \(\textsc {TLA}^{+}\) does not have assignments and other imperative statements that are used by model checkers to compute the successor states of a system state. Model checkers compute successors either explicitly — by evaluating program statements — or symbolically — by translating program statements to an SMT formula and checking its satisfiability. To efficiently enumerate the successors, TLA’s model checker TLC introduces side effects. For instance, an equality \(x' = e\) is interpreted as an assignment of e to the yet unbound variable x.