Declare a normally-closed signal once¶

Fail-safe wiring uses normally-closed contacts: an emergency stop carries 24 V while everything is fine and drops to 0 V when it is pressed or the wire breaks. The electrical signal is the negation of what you mean.

IEC 61131 has no term for this, so models do one of two things — negate at every use, or quietly model the electrical level and let the reader work it out. INVERTED binds the polarity once, where the signal enters.

The declaration¶

FUNCTION_BLOCK Guard
VAR_INPUT Estop : BOOL INVERTED; END_VAR
VAR_OUTPUT Run : BOOL; END_VAR
IMPLEMENTATION
    Run := Estop;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Inside the block, Estop means what its name says: true when the emergency stop is pressed. Run := Estop reads as the logic you intend, and the negation is nowhere in the body.

Where the negation goes¶

Into the generated code, exactly once, at the boundary. The block above emits:

FUNCTION_BLOCK Guard
VAR_INPUT
    Estop : BOOL;
END_VAR
VAR_OUTPUT
    Run : BOOL := FALSE;
END_VAR
    Run := NOT Estop;
END_FUNCTION_BLOCK

Two things are worth noticing. The emitted port is a plain BOOL — the adapter sees the electrical signal it actually has. And the NOT appears once, applied at sampling, not scattered over every use.

INVERTED works the same way on an output: the value is negated on write-back, so the field device receives the level it expects while the body stays in logical terms.

What it does not touch¶

The proof core never sees polarity. An INVERTED port changes the port schema and the emitted code; it does not change the contract, and it does not change the contract hash. A proof about Guard is a proof about its logical meaning, which is the point — the wiring convention is a property of the installation, not of the safety argument.

Where it is rejected¶

INVERTED is a modifier for boolean ports, and the compiler holds that line at the parser:

line 2:23: pol1-bool-only: INVERTED is a BOOL port modifier (got INT)

line 4:14: pol1-ports-only: INVERTED describes the polarity of a PORT;
a local has no external side

The second is the one worth internalising. Polarity is a statement about the boundary between the model and the plant. A local variable has no such boundary — there is no wire to be normally closed — so the modifier would have no meaning to carry.

Code	Meaning
`pol1-bool-only`	the port is not a `BOOL`
`pol1-ports-only`	the declaration is a local, not a port
`pol1-scalar-only`	the port is an aggregate; polarity applies to scalar signals

When to use it¶

Use it whenever the wire carries the negation of the meaning — normally-closed contacts, active-low outputs, fail-safe interlocks. That is the case it exists for, and it is worth declaring even when the body happens to read correctly without it: the declaration is documentation the compiler enforces.

Do not use it to save a NOT in ordinary logic. INVERTED says something about the installation, and a reader is entitled to believe it.

docs/adr-signal-polarity.md — the decision and where the boundary map is applied