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 10 and 11 drive 'Release' to
both values: their antecedents demand and fault can hold at the same time

A necessary clause colliding with a sufficient one reads slightly differently, because what fails is a different thing:

warning: [ns1-pair-conflict] sufficient clause (line 10) and necessary clause
(line 11) on 'Release' collide: the antecedent pressed can hold while the
necessary condition (NOT locked) fails

Both name the conditions from your block. Until 2026-09-04 they ended in a fixed (c AND d is satisfiable) no matter what the signals were called, so an explanation meant to point at two clauses named variables that were not in the program.

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:

verification failed:
  [synthesis-contract-unrealizable] no output satisfies all RULEs for the input
  assignment [demand=True, fault=True]; colliding clauses: RULE #1, RULE #2

It is deliberately incomplete: conflicts among three or more clauses escape it, and the verdict fires anyway. A missing warning is therefore not a promise that the clauses agree.

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: the timers' own
laws are not yet part of the step relation (ADR TMR-1). Mirror the condition
into a register and state the claim over that (ADR TX-1.2), or use them in
rule guards / definitions.

The reason is not the depth of the induction. This page used to say the statement "needs k-induction, which the proof core does not do yet"; ADR TX-2.2 withdraws that. A RULE is checked as an invariant over the transition, and HELD is already a state bit — one step would be enough. What is missing is that the timers' own laws (reset, run, clock, threshold) are not yet in the step relation, so the encoding would be unsound in one direction and incomplete in the other. Until that lands, HELD/ELAPSED 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.