Why necessary conditions deserve their own word¶

Every specification clause an engineer writes about an output is an implication. Classical PLC languages offer AND, OR, XOR, NOT — so each implication has to be hand-compiled into a disjunction before it can be written down at all.

That translation looks harmless. This page is about the three things it costs, because each of them was paid in full on one afternoon of modelling, and each is a consequence of the missing distinction rather than of carelessness.

The evidence: twelve clauses, all implications¶

The RIAS 4.1 step-function contract has twelve specification clauses. They were classified after the fact, and the result is the reason this feature exists: all twelve are implications — six necessary, six sufficient — and not one uses OR in its own right.

Every disjunction in that model was translation overhead. Nothing was gained by writing them that way; something was lost three times over.

Cost one: the balance becomes invisible¶

A first version of the model carried five sufficient and four necessary conditions. Bounded synthesis returned a solution that satisfied every clause:

q1n := T0 AND T2 AND q2;
q2n := T0;

Read what that means on the plant floor. Band 2 runs whenever the emergency stop is not pressed, and can never be switched off. The start and stop buttons do not appear in the solution at all.

Nothing was violated. What was missing had never been said: that a plant stands still until it is switched on. That statement is a necessary condition, and a specification weighted towards sufficient conditions is satisfiable by "always on unless forbidden".

In disjunctive form that imbalance cannot be seen. Nine clauses of OR look like nine clauses. The four-role balance the compiler now prints — ON-necessary, OFF-necessary, ON-sufficient, OFF-sufficient — exists so that the missing half is visible before the solver picks the degenerate solution:

balance: Pump: 1 ON-necessary, 0 OFF-necessary, 1 ON-sufficient,
         0 OFF-sufficient, 1 exclusion

Two zeros in that line say: nothing you wrote constrains when the pump is off.

Cost two: conflicts become unreadable¶

These two clauses are contradictory:

T4 OR q1 OR (NOT q2n)
(NOT (T3 AND T0)) OR q2n

They cannot both hold when T3 ∧ T0 ∧ ¬T4 ∧ ¬q1. Nothing about the two disjunctions shows it — you find it by solving, not by reading.

The same two clauses in the typed form:

    RULE q2n ONLY_WHEN (T4 OR q1);
    RULE (T3 AND T0) IMPLIES q2n;

Now the collision is legible: a necessary and a sufficient condition on the same output that cannot both be satisfied. One says the output may only be set under a condition; the other says something else forces it. An engineer sees that without a solver.

Cost three: without the distinction there is no cheap diagnosis¶

Here is the part that turns a readability argument into an engineering one.

A sufficient condition c IMPLIES q and a necessary condition q ONLY_WHEN d conflict exactly when c ∧ ¬d is satisfiable. That is a per-pair check, and it is tiny. Over the twelve clauses of the RIAS contract it runs in about 10 ms and finds both contradictions — including the one that had taken a separate investigation to locate.

That check is only possible because the roles are declared. In disjunctive form there is no pair to check: every clause is just a disjunction, and finding the conflict means asking the solver about the whole specification at once.

The pair analysis is deliberately incomplete — conflicts among three or more clauses escape it. So it is reported as an explanation, never as a verdict; the verdict stays with the global realizability probe. An incomplete check that explains beats a complete one that only says no.

What this is not¶

It is not new expressive power. RULE X ONLY_WHEN Y is exactly NOT X OR Y — the same formula, the same proof obligation, the same generated code. Nothing became provable that was not provable before.

What changed is that the compiler now knows which of the two things you meant, and can therefore count the roles, name a collision, and tell you when half your specification is missing. The information was always in your head; the language just had no place to put it.

docs/adr-necessary-sufficient-clauses.md — the decision, the clause forms and the literal rules
Specify relationally — how to write them
docs/adr-relational-member-composition.md — the same vocabulary applied to instance inputs