[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Guarantee machine closure with this one weird trick

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


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.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bbcd87f7-045b-fa8f-2d0a-176932e84237%40gmail.com.