Rewriting TLA+ Fairness Conditions for Symbolic Model Checking

Abstract

Model checking is a formal verification method that uses software to confirm a model of a system fulfills chosen properties. Systems in the TLA+ language are composed of states and transitions. The Apalache model checker for TLA+ is currently unable to reason about whether a system can take a given transition, while TLC can. This is important for verifying properties that assert that a given transition will eventually be taken if it possible. We apply a method from literature for rewriting these properties into a format Apalache accepts on three case studies, with the aim of finding improvements to the method. An equivalent rewrite is found for all cases, though requiring incremental modifications to the literature method. We find that expressions which depend on the updated values of variables after a transition must be distributed across disjunctions. We also note that expressions which depend on the results of prior expressions should be at the same or greater nesting level, and that if the system can pick from a set of new values for a variable, the value chosen must remain constant for the entire rest of the expression, also requiring indenting. From these results, we propose a general method for further research, relying on repeated additional nesting, applied whenever an expression is dependent on a previous expression's variable assignments. We leave its validation for future work.