One block

1. Your first block: an RS latch

A latch (or bistable) remembers a bit. Press set, it turns on and stays on; press reset, it turns off and stays off. It is the “hello world” of PLC logic. Here it is in zqel, fully commented (examples/rs_latch.zqel):

FUNCTION_BLOCK RS              // declare a reusable function block named RS
VAR_INPUT                      // its inputs (read at the start of each scan)
    R : BOOL;                  //   R = reset button
    S : BOOL;                  //   S = set button
END_VAR
VAR_OUTPUT                     // its outputs (written at the end of each scan)
    Q : BOOL;                  //   Q = the stored bit
END_VAR
IMPLEMENTATION
    Q:                         // define the output Q with a list of prioritised rules
        OFF WHEN R PRIO 0;     //   if R is pressed, force Q off ... priority 0
        ON  WHEN S PRIO 1;     //   if S is pressed, force Q on  ... priority 1 (higher!)
        HOLD OTHERWISE;        //   otherwise keep Q's previous value
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Design choice, not a law of nature. If R and S are both 1 in the same scan, this block is set-dominant because we gave S the higher priority. A different priority assignment would give a different latch. zqel does not guess which RS behaviour you “meant” — you state it explicitly.

Read the Q: block as a set of competing rules, not as a sequence of steps. Each rule says “under this condition, the output should become this value, and my importance is this number.” The vocabulary:

Keyword	Meaning
ON / OFF	make the output TRUE / FALSE (BOOL outputs only)
SET expr	assign the value of an expression (any type)
HOLD	keep the output's previous value (its memory)
WHEN guard	this rule is active only when guard is true
PRIO n	this rule's priority; bigger number = more important
OTHERWISE	the fallback rule; no condition, no priority

Here is the single most important idea in zqel. Among all the rules whose guard is currently true, the one with the highest PRIO decides the output. The order in which you wrote the rules is irrelevant. Above, S has priority 1 and R has priority 0, so if you press both at once, set wins — this is a “set-dominant” latch. If you wanted reset to win, you would swap the priority numbers, not move the lines around. There is no single “canonical” answer here: IEC 61131-3 itself ships both an SR (set-dominant) and an RS (reset-dominant) standard block. Which one you want is a design decision, and in zqel you make it by choosing the priorities — nothing else.

What the compiler makes of it

Let us compile it and ask for Structured Text:

$ python -m zqel examples/rs_latch.zqel --target st

FUNCTION_BLOCK RS
VAR_INPUT
    R : BOOL;
    S : BOOL;
END_VAR
VAR_OUTPUT
    Q : BOOL;
END_VAR
VAR
    _Q_next : BOOL;
END_VAR
    _Q_next := (S OR (NOT R AND Q));   (* <-- the three rules, collapsed into ONE formula *)
    Q := _Q_next;
END_FUNCTION_BLOCK

Look closely at that one line. Your three prioritised rules — set, reset, hold — were compiled into a single boolean formula:

Q_next  =  S  OR  (NOT R  AND  Q)

In words: Q becomes true if S is pressed (set wins), or else if R is not pressed and Q was already true (hold). This is exactly the classic set-dominant latch equation you would find in a textbook — but you did not write it. You wrote the intent (three rules and their priorities), and Z3 derived the equation, folding the priorities together in the correct order. That derived formula is the meaning of your block, and it is what every backend prints.

Why the extra variable _Q_next? The compiler computes the new value into a temporary first (_Q_next), and only then assigns it to Q. Section 2 explains why this staging matters.

---

2. How a block runs: one scan, all-at-once

A subtle but important point: in a real PLC scan, all of a block's outputs are conceptually updated simultaneously, using the values they had at the start of the scan. If one output's formula reads another output, it must read the old value, not a half-updated new one.

zqel guarantees this, and you can see the mechanism in the generated ST: every new value is computed into a _..._next temporary first, and only after all of them are computed are they committed. The rising-edge detector in the next section shows this clearly. Keep the pattern in mind:

1. compute  _a_next, _b_next, ...   (all from start-of-scan values)
2. commit   a := _a_next;  b := _b_next;  ...

flowchart LR
    S0["state at start of scan<br/>a, b, inputs"]
    C1["compute _a_next<br/>from start-of-scan values"]
    C2["compute _b_next<br/>from start-of-scan values"]
    K{{"commit — all at once"}}
    S1["state at start of the next scan<br/>a, b"]

    S0 --> C1 --> K
    S0 --> C2 --> K
    K --> S1

Both arrows leave the same box. That is the whole point: _b_next cannot see _a_next, no matter which one the generated code happens to assign first.

This is not something you write — it is how zqel renders “update everything at once” into a language (ST) that only has step-by-step assignment.

---

3. Two kinds of memory: registers and derived values

Every output or internal variable is defined in one of two ways, and the difference is exactly when a reference reads its value. This trips up beginners, so read carefully.

• A register is defined by rules (like Q: above). It is stored: it has memory that survives across scans. Inside a register's rules, a reference to another register means that register's value at the start of the scan — its “pre-value”, the old value. This is what you need for edge detection: to detect a change, you must compare against the previous value.

• A derived value is defined with the := operator (name := expression;). It is combinational: it is recomputed every scan and not stored. Inside a derived definition, a reference to a register means its freshly computed new value — no one-scan delay.

Beginners usually need one compact picture:

Where you read a register	What you get
inside a rule block (Q: / M: / ...)	the old value from the start of the scan
inside a derived definition (x := ...)	the new value just computed for this scan

If you remember only one sentence from this section, remember this: rules read old state; := reads freshly computed state.

flowchart LR
    OLD["registers<br/><b>old</b> values<br/>(start of scan)"]
    RULES["rule blocks<br/><code>Q: SET … WHEN …</code>"]
    NEW["registers<br/><b>new</b> values"]
    DER["derived definitions<br/><code>x := …</code>"]

    OLD -->|"a rule reads here"| RULES
    RULES --> NEW
    NEW -->|"a := reads here"| DER

    style OLD fill:#fff3cd,stroke:#856404,color:#000
    style NEW fill:#d4edda,stroke:#155724,color:#000

The two reads sit on opposite sides of the same box. That is why pulling a subexpression out of a rule into a := definition is not a refactoring: it moves the read across the boundary, and the program changes.

A rising-edge detector (R_TRIG, examples/iec/r_trig.zqel) outputs a one-scan pulse each time its input goes from 0 to 1. It must remember the previous input:

FUNCTION_BLOCK R_TRIG
VAR_INPUT
    CLK : BOOL;                    // the signal we watch for a rising edge
END_VAR
VAR_OUTPUT
    Q : BOOL;                      // Q = 1 for exactly one scan on a 0->1 edge
END_VAR
VAR
    M : BOOL;                      // hidden internal memory: the PREVIOUS CLK
END_VAR
IMPLEMENTATION
    Q:                             // Q is a REGISTER, so M below is read as its PRE-value
        SET CLK AND NOT M OTHERWISE;   // edge = CLK is high now AND was low last scan
    M:
        SET CLK OTHERWISE;         // remember this scan's CLK for the next scan
END_IMPLEMENTATION
END_FUNCTION_BLOCK

VAR ... END_VAR declares hidden internal state — M here — that is not part of the public interface. The generated ST makes the pre-value and the all-at-once update visible:

    _Q_next := (CLK AND NOT M);    (* uses M = the OLD previous-CLK *)
    _M_next := CLK;                (* next scan's "previous CLK" *)
    Q := _Q_next;                  (* only now do we commit the new values ... *)
    M := _M_next;                  (* ... so _Q_next above saw the OLD M, not CLK *)

If both assignments happened immediately in order, M would be overwritten before Q read it and the edge detection would break. The _next staging is precisely what prevents that. This is the reading-time rule made concrete.

Rule of thumb. Need the previous value (edges, latches, counters comparing to a limit)? Use a register (rules). Need a value computed fresh this scan from other results (a plain combinational output)? Use :=.

---

4. Priorities in depth, and the errors that keep them honest

Because priority is written down explicitly, the compiler can check two things a human reviewer usually misses.

(a) No silent tie-breaks. If two rules with the same priority could be active at the same time but demand different results, that is not a coin toss — it is an ambiguous-priority error, reported with a counterexample. You must give them different priorities or make their conditions mutually exclusive. (Two rules with equal priority that agree — e.g. several OFF rules — are fine.)

(b) No dead code. A rule that is always beaten by a higher-priority rule can never affect the output. zqel reports it as an unreachable-rule warning so you can delete it or fix its condition.

A bounded up-counter (examples/counter.zqel) uses a realistic three-level priority stack:

FUNCTION_BLOCK Counter
VAR_INPUT
    Reset : BOOL;                  // reset to zero
    Count : BOOL;                  // count-up pulse
END_VAR
VAR_OUTPUT
    Value : INT;                   // the current count
END_VAR
IMPLEMENTATION
    Value:
        SET 0         WHEN Reset       PRIO 30;   // reset beats everything
        HOLD          WHEN Value >= 10 PRIO 20;   // at the limit: freeze (saturate)
        SET Value + 1 WHEN Count       PRIO 10;   // otherwise, if counting, add one
        HOLD OTHERWISE;                           // idle: keep the value

    INVARIANT                       // a property we DEMAND the compiler prove:
        Value >= 0;                 //   the count is never negative
    INVARIANT
        Value <= 10;                //   and never exceeds 10
END_IMPLEMENTATION
END_FUNCTION_BLOCK

INT is a 16-bit signed integer with the same wrap-around behaviour as real PLC hardware (add 1 to 32767 and you get −32768). zqel models this faithfully, so its proofs are about what the hardware actually does, not an idealised infinite integer. We will come back to the two INVARIANT lines in the next section.

The generated ST folds the four-rule priority stack into nested SEL calls (SEL(cond, a, b) is the IEC selector: it returns b if cond is true, else a — a two-way multiplexer):

    (* proven invariant: (Value >= 0) *)
    (* proven invariant: (Value <= 10) *)
    _Value_next := SEL(Reset, SEL(((10 <= Value) OR NOT Count), (1 + Value), Value), 0);
    Value := _Value_next;

Unfold it from the outside in and you recover your priorities exactly: if Reset, result is 0; else if (Value >= 10 or not counting) keep Value; else Value + 1. The two comment lines are the compiler telling you which properties it proved before emitting this code.

---

---

4b. Saying when, not what: relational clauses

Everything so far computed a value: ON WHEN …, :=, a priority ladder. Some requirements do not arrive in that shape. "The pump may only run while the valve is open" is not a formula for the pump — it is a condition on the pump, and turning it into a formula is work you do in your head and the next reader has to undo.

RULE lets you write the condition itself. Three forms carry most of it:

Form	Reads as
RULE X ONLY_WHEN Y	X may hold only while Y — a permission
RULE X IMPLIES Y	X forces Y — a trigger
RULE X EXCLUDES Y	X and Y never hold together

A first attempt, and why it fails

An interlock, written the way one says it out loud:

FUNCTION_BLOCK Interlock
VAR_INPUT Demand : BOOL; ValveOpen : BOOL; Fault : BOOL; END_VAR
VAR_OUTPUT Pump : BOOL; END_VAR
IMPLEMENTATION
    RULE Pump ONLY_WHEN ValveOpen;
    RULE Pump EXCLUDES Fault;
    RULE Demand IMPLIES Pump;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The compiler refuses, and the refusal is the interesting part:

warning: [ns1-pair-conflict] sufficient clause (line 7) and necessary clause
(line 5) on 'Pump' collide: the antecedent Demand can hold while the necessary
condition ValveOpen fails
verification failed:
  [synthesis-contract-unrealizable] no output satisfies all RULEs for the input
  assignment [Demand=True, Fault=False, ValveOpen=False]; colliding clauses:
  RULE #1, RULE #3

Demand on, valve shut — no fault needed. One rule says the pump must run, one says it may not, and nothing satisfies both. The requirements were contradictory before any code existed, and the counterexample is the situation your plant would have found for you.

Read the two lines as the different things they are. The warning explains which two clauses collide and why, naming your own signals. The verdict underneath comes from the proof over the whole clause set, and it would fail with or without the explanation — which matters, because a collision that needs three clauses to appear escapes the pair analysis entirely.

The fix is to say what you meant — demand triggers the pump when it is allowed to:

FUNCTION_BLOCK Interlock
VAR_INPUT Demand : BOOL; ValveOpen : BOOL; Fault : BOOL; END_VAR
VAR_OUTPUT Pump : BOOL; END_VAR
IMPLEMENTATION
    RULE Pump ONLY_WHEN ValveOpen;
    RULE Pump EXCLUDES Fault;
    RULE Demand AND ValveOpen AND NOT Fault IMPLIES Pump;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Compilation succeeded: Interlock
  3 output properties verified
  balance: Pump: 1 ON-necessary, 0 OFF-necessary, 1 ON-sufficient,
           0 OFF-sufficient, 1 exclusion

Clauses constrain; they need not determine

Look at what came out:

    (* proven invariant: NOT (Pump AND Fault) *)
    (* proven invariant: (NOT ((Demand AND ValveOpen) AND NOT Fault) OR Pump) *)
    Pump := (ValveOpen AND NOT Fault);

Demand is not in the generated code. That is not a bug — read the rules again and you will see they never say the pump must be off without demand. Pump := ValveOpen AND NOT Fault satisfies all three, and so would Pump := Demand AND ValveOpen AND NOT Fault. Several implementations fit; the compiler picked one and proved it fits.

The balance: line is the compiler telling you exactly this. It counts the roles your clauses fill — here one ON-necessary, one ON-sufficient, and zero OFF-necessary and OFF-sufficient. Nothing you wrote constrains when the pump is off.

When you do want it pinned down, say so with IFF:

FUNCTION_BLOCK InterlockExact
VAR_INPUT Demand : BOOL; ValveOpen : BOOL; Fault : BOOL; END_VAR
VAR_OUTPUT Pump : BOOL; END_VAR
IMPLEMENTATION
    RULE Pump IFF Demand AND ValveOpen AND NOT Fault;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Compilation succeeded: InterlockExact
  1 output property verified
  balance: Pump: defined (IFF)

    Pump := (Demand AND ValveOpen AND NOT Fault);

Now Demand is there, because now you said it belongs there.

Which to reach for

Use clauses when the requirement is a condition — interlocks, permissions, mutual exclusions — especially when several of them come from different documents and different people. Each stays readable on its own, and the compiler folds them together and tells you when they disagree.

Use := or a priority ladder when you genuinely have a value to compute. Neither is more advanced than the other; they answer different questions.