vacuity

ltl analyze vacuity rules.ts

A rule that always passes is not necessarily a rule that is working. Three different problems, reported as three different codes:

Code	Meaning
unsatisfiable	No trace satisfies this rule. It can never pass, so it is broken rather than strict.
never-fires	Nothing the other rules allow can make its antecedent true. It holds vacuously — it is watching for something that cannot happen.
implied	It cannot be broken by anything the other rules allow. It adds nothing.

Each is settled against the rest of the set

Because a rule lives in a rule set. A rule forbidding purgeLogs outright makes any rule about what must precede a purgeLogs vacuous — the second rule is not wrong, it is unreachable, and that is worth knowing before someone trusts it.

This is why vacuity is the analysis to run first. unsatisfiable catches the rule you got backwards; never-fires catches the rule that is shadowed by a stricter one; implied catches the rule that was already covered when someone added it.

What it will not tell you

That a rule is correct. Vacuity is about whether a rule can do anything, not whether what it does is what you meant. For that, witness — the shortest trace that breaks it — is the fastest thing to read, because a rule whose counterexample surprises you is a rule that does not say what you think.