Skip to content

How to specify an output relationally

Audience: engineer who knows what the plant must never do, and wants the compiler to hold them to it.\ Prerequisites: RULE, INVARIANT and priorities from the Introduction by Example.\ Language Reference: §8.6a Typed relational clauses.

Most specification clauses are implications. Written as raw disjunctions they all look alike, and one crucial distinction disappears: whether a condition permits an output or forces it. The typed clauses keep that distinction — and the compiler can then tell you things it could not see before.

The four forms

RULE <literal>   ONLY_WHEN <condition> ;   (* necessary:  literal → condition *)
RULE <condition> IMPLIES   <literal>   ;   (* sufficient: condition → literal *)
RULE <output>    IFF       <condition> ;   (* definition: both directions     *)
RULE <source>    EXCLUDES  <source>    ;   (* exclusion:  NOT (a AND b)       *)

<literal> is one declared BOOL output, bare (Release) or negated (NOT Release). The condition may not mention that output.

1. Say what an output requires — ONLY_WHEN

A two-hand press must never release with one hand:

    RULE Release ONLY_WHEN (Left AND Right);

Read it as: Release may only be true when both buttons are pressed. It does not say the press releases whenever both are held — that would be the sufficient direction, and mixing the two up is exactly the mistake this syntax prevents.

2. Say what forces an output — IMPLIES

The forbidding direction is the same clause with the sides swapped and the output negated:

    RULE (Left AND NOT Right) IMPLIES NOT Release;

3. Say that an output is a condition — IFF

When an output is nothing but an abbreviation, say so:

FUNCTION_BLOCK Actuator
VAR_INPUT Release : BOOL; Enabled : BOOL; END_VAR
VAR_OUTPUT Press : BOOL; END_VAR
IMPLEMENTATION
    RULE Press IFF (Release AND Enabled);
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Press needs no separate definition: the compiler materialises it from the clause and records the provenance as defined, not searched. If any other clause contradicts the definition, the compile fails closed (ns1-iff-conflict) — nothing is materialised on a contradiction.

4. Say that two outputs are mutually exclusive — EXCLUDES

FUNCTION_BLOCK Drive
VAR_INPUT Fwd : BOOL; Rev : BOOL; END_VAR
VAR_OUTPUT MotorFwd : BOOL; MotorRev : BOOL; END_VAR
IMPLEMENTATION
    MotorFwd := Fwd AND NOT Rev;
    MotorRev := Rev AND NOT Fwd;
    RULE MotorFwd EXCLUDES MotorRev;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

EXCLUDES normalises to NOT (a AND b) and is symmetric. It is the readable form of a motor interlock — and unlike a comment, it is proved.

The whole example

FUNCTION_BLOCK TwoHandPress
VAR_INPUT
    Left  : BOOL;
    Right : BOOL;
END_VAR
VAR_OUTPUT
    Release : BOOL;
END_VAR
IMPLEMENTATION
    Release := Left AND Right;

    RULE Release ONLY_WHEN (Left AND Right);
    RULE (Left AND NOT Right) IMPLIES NOT Release;
    RULE (Right AND NOT Left) IMPLIES NOT Release;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Reading the balance

Compiling prints one INFO line per output:

Release: 1 ON-necessary, 0 OFF-necessary, 0 ON-sufficient, 2 OFF-sufficient

The four columns are the four roles: what must hold for the output to be on (ON-necessary), what must hold for it to be off, what forces it on, what forces it off. The line is information, not a verdict — but read it, because an output with no necessary conditions is exactly the shape that lets a synthesiser answer "always on unless forbidden" and still satisfy every clause.

defined (IFF) appears instead for an output defined by a biconditional, and legacy RULE clauses that touch an output are counted as unclassified — a half-migrated block cannot present a balance that looks complete and is not.

When clauses collide

Two clauses that cannot both hold produce an explanation:

warning: [ns1-pair-conflict] clauses at lines 12 and 14 drive 'Release' to
both values when both antecedents hold (c AND d is satisfiable)

The verdict still comes from the ordinary proof over the whole clause set — the pair analysis only explains which two clauses collide and why, which a single unsatisfiable-core message rarely does. It is deliberately incomplete: conflicts among three or more clauses escape it.

Timers on the condition side — not yet

A clause such as

RULE HELD(Trip, T#30s) IMPLIES NOT Enable;

reads naturally, but the compiler refuses it today:

[sema-error] HELD/ELAPSED may not appear inside an INVARIANT (not yet
supported); use them only in rule guards / definitions

The reason is structural: a RULE is checked as an invariant over the transition, and a statement about how long something has held needs k-induction, which the proof core does not do yet. HELD/ELAPSED therefore live where they already work — in rule guards and definitions:

FUNCTION_BLOCK Watchdog
VAR_INPUT Trip : BOOL; END_VAR
VAR_OUTPUT Enable : BOOL; TooLong : BOOL; END_VAR
IMPLEMENTATION
    TooLong := HELD(Trip, T#30s);
    Enable  := NOT TooLong AND NOT Trip;

    RULE TooLong IMPLIES NOT Enable;     (* the mirrored signal is ordinary BOOL *)
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The mirror pattern keeps the timing in a definition, where it is supported, and lets the relational clause speak about an ordinary boolean. Direct temporal antecedents are tracked as future work (ADR NS-1.9 and the temporal track).

A register name means the previous value in a clause

Writing Enable as a register instead — Enable: OFF WHEN TooLong PRIO 20; HOLD OTHERWISE; — makes the same clause fail, with a counterexample where Enable is still on while TooLong has just become true. That is not a bug: inside a clause a register name denotes the value entering the scan, while a definition (:=) denotes the value leaving it. A clause about what an output must be after this scan therefore belongs on a defined output — or must name the previous value explicitly with PRE.