Composition and Modular Verification of TLA+ specs

TLA+ is compositional in the abstract sense... In the astral plane, a program execution is an infinite sequence of states, each state giving a value to every variable in an imagined universal state space. A spec is a predicate (yes/no test) on executions, which denotes a set of allowed executions. In this setup, the steps that change variables in other specs look like stuttering to yours. And that enables us to denote composition as a beautiful purely logical conjunction, Spec1 /\ Spec2.The problem is, this is too pure. When you try to model check a conjunction of two specs, your astral travel gets grounded. Since TLC only accepts specs in the normal form Init /\ [][Next]_vars, you need to manually expand the conjunction of two boxed formulas as: [][N1]_v1 /\ [][N2]_v2 = []((N1 \/ UNCHANGED v1) /\ (N2 \/ UNCHANGED v2))Expanding this gives us joint steps for N1/\N2, solo steps for each side, and both side stutter steps (which can be omitted vacuously). However, shared read/write…