All-at-once, and the interlock that isn't one

Registers in a zqel block update simultaneously: every rule reads the values the state had when the scan began. That is one sentence in the tutorial, and it sounds like a formality about evaluation order.

It is not. This page follows one real safety requirement through it, because the consequence is a class of defect that a sequential language will not show you — and that a proof will.

The requirement

RIAS exercise 4.2, a press with two-hand interlocking (examples/rias/4.2-zweihandpresse.md):

A3: A release cannot be granted, or is withdrawn, if one of the hand buttons has been held for more than 30 s.

A4: The press drive is activated only when a release is present and the foot switch T3 is pressed.

Read as an engineer would: the lockout wins over the drive. One register grants the release, another detects the lockout, and the drive follows the release. Three things, each obvious.

The model that looks right

    Lockout:
        ON WHEN HELD(T1, T#30s) OR HELD(T2, T#30s);
        OFF OTHERWISE;

    Release:
        OFF WHEN NOT (T1 AND T2)                     PRIO 30;
        OFF WHEN HELD(T1, T#30s) OR HELD(T2, T#30s)  PRIO 20;
        ON  WHEN T1 AND T2 AND NOT HELD(T1, T#100ms)
                           AND NOT HELD(T2, T#100ms) PRIO 10;
        HOLD OTHERWISE;

    PA:
        ON WHEN Release AND T3;      (* <- the defect *)
        OFF OTHERWISE;

Every line reads correctly. Release is withdrawn under lockout, and PA follows Release. Ask the compiler to prove that a lockout excludes the drive:

    INVARIANT (NOT PA) OR (NOT Lockout);

It refuses:

verification failed:
  [invariant-step] invariant can be violated after one cycle:
  (NOT PA OR NOT Lockout)
      counterexample: Lockout=1, PA=0->1, Release=1->0

What the counterexample says

Read the arrows. In this scan Release goes from 1 to 0 — the lockout has just engaged and withdraws it. In the same scan PA goes from 0 to 1.

Both registers read the state as it was at the start of the scan, where Release was still 1. So the drive starts in the very scan the interlock engages. For exactly one cycle, the press runs with the lockout active.

That is not an edge case invented by a solver. It is the scan in which the operator has held a button for thirty seconds — the situation the requirement was written for.

Why a sequential language hides this

In Ladder or SFC the same three pieces are usually written as networks evaluated top to bottom:

Network 1:   T1 held 30s  OR  T2 held 30s   ──( Lockout )
Network 2:   T1 AND T2 AND NOT Lockout      ──( Release )     (* latching *)
Network 3:   Release AND T3                 ──( PA )

Here it appears fine, and it may even be fine — because network 3 runs after network 2 and sees the fresh value. The correctness rests entirely on the order of the networks.

Nothing in the program records that dependence. Move network 3 above network 2 — during a refactor, when splitting a POU, when a colleague reorders for readability — and the defect appears, silently, with no diagnostic anywhere. The behaviour changed; the code still looks like a correct interlock.

That is the trade a sequential language makes: it lets you write in reading order, and it pays by making correctness depend on a property nobody states and no tool checks.

What zqel does instead

Simultaneous update removes the order, so it removes the hidden dependence — but it does not remove the problem. It surfaces it: a register that reads another register reads the previous scan's value, always and visibly, and the proof then either goes through or hands you the counterexample above.

The fix is to name the condition rather than the register:

    PA:
        ON WHEN T1 AND T2 AND T3
                AND NOT (HELD(T1, T#30s) OR HELD(T2, T#30s))
                AND (Release OR (NOT HELD(T1, T#100ms)
                                 AND NOT HELD(T2, T#100ms)));
        OFF OTHERWISE;

Now the lockout condition is evaluated in the same instant for both, and the four safety properties verify:

Compilation succeeded: TwoHandPress
  4 output properties verified

The complete model is examples/rias/TwoHandPress.zqel.

The rule of thumb

A register may not guard an output that is updated beside it.

If output B must respect a condition that register A tracks, B's guard names the condition, not A. A then exists so the contract can speak about it — which is exactly its role in the timer pattern too: the mirror register is there for the INVARIANT to reference, never for another output to read.

Where you genuinely want the previous scan's value, say so with PRE. That is a deliberate one-step dependency, and it reads as one.

What this costs, honestly

Writing the condition twice is redundancy, and redundancy can drift. The compiler does not check that Release's guard and PA's guard agree about the lockout — it checks that the properties you stated hold.

So the safeguard is not the duplication; it is the INVARIANT. State the requirement as a property and the prover holds both guards to it. Leave the property out and you have two copies of a condition and no one watching them. That is the part worth taking from this page: the duplication is a consequence, the proof is the point.