Guarantee machine closure with this one weird trick

[Hillel Wayne]

I'm doing some contract work on a very complex spec with multiple levels of refinement and a bunch of spec compositions. I've been coming up with lots of useful tricks and one of them is about handling fairness constraints. Take the constraint

WF_vars(A)

If A is not a subaction of Next, then this acts as a state constraint on the whole spec, effectively filtering out any behaviors that ever have ENABLED <<A>>_vars.  This isn't "machine closed", as defined on page 112 of Specifying Systems. This can be really annoying but is mostly avoidable... for single-file specs. But when you're conjoining multiple modules with shared state it's really easy to accidentally violate this. And it's not always obvious when it happens, since the only symptom is a smaller state space.

Anyway, here's how to guarantee that your specs are always machine closed:

WF_vars(Next /\ A)

That's it! Since Next /\ A is tautologically a subaction of Next you'll never have an accidental constraint. You are more likely to have liveness errors where your fairness conditions don't seem to be "working", but that's a whole lot easier to debug in practice.

H