nb-10 — A procedure with parallel checks

← Course mapChapter 10 / 25 · Advanced

Minimal exampleCommand and resultExercise

Northbridge is fictional. All offices, stations, thresholds and calendars in this course are synthetic and unofficial. No real municipal deployment or legal-validity claims. Verified profile: law 0.1.0, law.core/0.2.

Situation

An operator applies to install a curbside charging station, st1, with a 22 kW nameplate. The permit office cannot approve it on filing alone: two checks must run side by side. The documents desk verifies the application file, while the grid engineer verifies the technical conditions. The station is approved only when both checks have passed. If the documents are in order but the grid engineer has not signed off yet, the case must wait — not jump to approval.

Earlier articles answered “may she have it” with eligibility rules (nb-01: First permit: facts, a rule and a question through nb-03: Exceptions and conflicting rules), and nb-09: From permit to duties and powers tracked who owes what afterwards. This article answers how a case moves. Law DSL expresses that movement as a procedure: the case rests in named states, things that happen to it are recorded as events, and transitions carry it from one state to another.

Two more words complete the picture. A guard is an extra condition a transition demands before it fires. The two checks run as regions — sub-tracks inside one state that advance independently — and a join states how many regions must finish before the case leaves. Here the join demands both.

Prerequisites

You need nb-01: First permit: facts, a rule and a question for facts, strict rules, and law test as the way to check a claim, and nb-02: Why a missing fact is not a refusal for the four truth statuses. Below, NEITHER means “no conclusion either way” — never a refusal.

nb-09: From permit to duties and powers showed duties and powers attaching to parties. Procedures move cases through states instead. The two ideas compose — a revoked permit and a station stuck in review are different questions — but this article needs no position vocabulary.

The new words all appear in the st1 case. The filing of the application is an event: a recorded happening with an identifier and a timestamp. Between steps, the case rests in a state such as Draft or Review. A transition names one legal step: the state it leaves, the state it enters, the event that triggers it, and optional guards — when conditions that must hold for the step to fire. Inside the parallel review state, each check runs in its own region with its own current state, and the join declares how many regions must finish before the case moves on.

Minimal example

All fragments are excerpts from packs/examples/language-demo/procedure/package.law (identifiers as written; package header, imports, type and relation declarations cut where noted; line numbers refer to that file).

Excerpt 1 — the five events (lines 27–45). An event declaration names the happening and the payload it carries; each test later fires events with a unique id and a time.

Arxo Law

event ApplicationFiled {
    station: Station;
}

event ReviewStarted {
    station: Station;
}

event DocsFiled {
    station: Station;
}

event TechApproved {
    station: Station;
}

event ReviewComplete {
    station: Station;
}

Look at the shape of each declaration: a name and a payload. Every event carries the station it concerns, and each test later fires events with a unique id and a time. Filing the application and completing the review are different happenings, and the procedure treats them as such — events record what happened, not what was decided.

Excerpt 2 — the technical guard rule (lines 20–25). tech_ok is an institutional conclusion (computed by the office, not observed), derived from the nameplate: at most 44 kW, a teaching value, not an electrical standard.

Arxo Law

rule TechWithinLimit strict {
    for s: Station;
    for kw: Quantity;
    when nameplate(s, kw) and kw <= 44 kW;
    then tech_ok(s);
}

Look at the when line: the nameplate quantity kw is compared against 44 kW, a teaching value rather than an electrical standard. The transition itself only asks when tech_ok(s); this rule decides when that holds. tech_ok is institutional — computed by the office from the nameplate, not observed.

Excerpt 3 — the parallel state with its two regions (lines 50–69). A region holds its own current state; both regions start in their initial state when review begins. The Docs track needs only its event; the Tech track needs its event plus the guard.

Arxo Law

state Review parallel {
    region Docs {
        state DocsPending initial;
        state DocsOk terminal;
        transition DocsAccept {
            from DocsPending;
            to DocsOk;
            on DocsFiled;
        }
    }
    region Tech {
        state TechPending initial;
        state TechOk terminal;
        transition TechAccept {
            from TechPending;
            to TechOk;
            on TechApproved;
            when tech_ok(s);
        }
    }

Look at the two regions side by side. Each holds its own current state, and both start in their initial state when review begins. The Docs track needs only its event; the Tech track needs its event plus the guard. The tracks are independent: documents can be accepted while technical approval is still pending, and neither track can advance the other.

Excerpt 4 — the join and the three outer transitions (lines 70–88; the procedure header on line 47 and the Draft / Filed declarations on lines 48–49 are cut). join all means every region must reach a terminal state before the case may leave Review.

Arxo Law

    join all;
}
state Approved terminal;
transition File {
    from Draft;
    to Filed;
    on ApplicationFiled;
    when application_complete(s);
}
transition StartReview {
    from Filed;
    to Review;
    on ReviewStarted;
}
transition Decide {
    from Review;
    to Approved;
    on ReviewComplete;
}

Look at Decide: it reads like a single step, but from Review plus join all makes it a rendezvous. join all means every region must reach a terminal state before the case may leave Review, so the ReviewComplete event operates only once DocsOk and TechOk both hold.

Command and result

Run the procedure suite:

Terminal

law test packs/examples/language-demo/procedure

Observed result (engine law 0.1.0):

Output

law test demo.northbridge.procedure: мир demo.northbridge.procedure, demo.northbridge.calculations, demo.northbridge.permits, demo.northbridge.vocabulary
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / filing with a complete set
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / without the set the case stands still
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / re-entry holds the state
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / both regions ready — decision taken
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / join waits for both regions
  ok   [demo.northbridge.procedure] tests/procedure.lawtest / technical conditions above the threshold block the region
итого: 6 проверено, 6 прошли, 0 не прошли, 0 не исполнены; код 0

All six tests pass: each answer matched its expectation. That says the machine moves the case as declared — it is not a ruling that st1’s station deserves approval. The first line names the world under test: the procedure package together with the calculations, permits and vocabulary packages it is evaluated with. The summary line is in Russian and says that 6 tests were checked, 6 passed, none failed and none were left unexecuted, with exit code 0.

The package also passes the static check:

Terminal

law engine check packs/examples/language-demo/procedure/package.law

Output

check OK: packs/examples/language-demo/procedure/package.law

check OK means the package file is well-formed; the suite run above is what exercises its behavior.

What the decisive tests assert (evaluate truth(current_state(...)) in every case):

Test	Setup	Expects
filing with a complete set	application_complete plus a File attempt	Filed TRUE_ONLY
without the set the case stands still	File attempt, completeness absent	Draft TRUE_ONLY
re-entry holds the state	two File attempts	Filed TRUE_ONLY
both regions ready — decision taken	22 kW plate, all five events attempted in order	Approved TRUE_ONLY
join waits for both regions	same but no TechAccept attempt	Approved NEITHER
technical conditions above the threshold block the region	120 kW plate, all events attempted	Approved NEITHER

Two test helpers appear in every setup. procedure_instance declares st1 a case of this procedure, and attempted_transition records that a named transition was tried with a named event. A step fires only when the case is in the from state, the event is on record, and every guard holds — three ingredients, all at once.

Why this construct

The task is to move one case through filing, two parallel checks, and a single approval — refusing to decide early while refusing to lose the case’s place on repeated filings. Each sub-question has its own construct and its own observable proof. Events answer “what happened”, with the id and time payloads in the tests. Transitions answer “which steps are legal from here”: Draft ignores a review start, and only File moves it. Guards answer “what else must hold”: completeness for filing, tech_ok for the Tech track. Regions answer “what advances independently”: the documents track needs no grid engineer. The join answers “when is the whole review done”: join all means both tracks terminal.

Plain eligibility rules in the style of nb-01: First permit: facts, a rule and a question through nb-03: Exceptions and conflicting rules can label a station “approvable”, but they cannot say the documents passed while the grid check is still pending — states keep that middle. Positions from nb-09: From permit to duties and powers track standing relations with windows, not step-by-step movement. Use rules for “does it qualify”, positions for “who owes what”, procedures for “where is the case and what may happen next”.

The proof is the six tests above: guarded filing fires, unguarded filing blocks, re-entry holds, both-tracks approval goes through, the join waits, and the threshold blocks — all under law test. What the tests do not prove is that 44 kW is the right engineering limit. The suite proves the machine enforces the declared threshold; the threshold itself is a teaching value (see Limits). All acts are fictional data, not legal advice.

Changed condition

Take both regions ready — decision taken and change one fact: the nameplate goes from 22 kW to 120 kW. Everything else is identical — same completeness, same five attempted transitions, same timestamps.

With 22 kW, TechWithinLimit derives tech_ok(st1), so TechAccept reaches TechOk. Both regions are terminal, and Decide on ReviewComplete yields current_state(st1, Approved) TRUE_ONLY. With 120 kW, 120 kW <= 44 kW is false, so tech_ok(st1) never holds: the TechAccept attempt misfires, the Tech region stays TechPending, and the same Decide attempt yields Approved NEITHER.

The failure is local. The Docs region still reaches DocsOk; only the guarded track blocks, and through it the join. One number, two outcomes.

The same one-change logic governs entry. The two filing tests differ only in whether application_complete(st1) is asserted. The engine never files an incomplete case out of helpfulness.

Typical mistake

A natural misreading of Decide is “the review finished, so approve”. Suppose only the Docs track is done and ReviewComplete fires. The case is still not approved: Approved stays NEITHER, exactly as join waits for both regions shows. The event occurred, but the transition did not fire — from Review under join all demands both regions terminal, not merely “some progress”.

When a case is not approved, check three things in order: the case’s state, the recorded event, and every guard plus every joined region. Here the missing TechAccept attempt fails the third check, so Decide is a no-op and the case rests where it was. An event proposes; the procedure disposes.

Limits

A transition needs all three ingredients at once: the right state, the recorded event, and true guards. Remove any one and the case stands still — it never errors, never guesses, never skips ahead. without the set keeps Draft; join waits keeps the case inside Review.

Re-entry is absorbed. Filing twice does not file twice: re-entry holds the state stays Filed. Idempotent attempts make retries safe, but a duplicate event is therefore no evidence of progress.

The threshold is didactic. 44 kW is a teaching value chosen to make the guard visible — 22 passes, 120 fails — not an electrical standard and not advice for any real connection.

State is read through current_state. Truth queries see where the case is; the “why” is the conjunction of attempts, guards and region states the tests assemble.

Verified profile: engine law 0.1.0, semantics law.core/0.2. Events with id/time payloads, attempted_transition, current_state, parallel regions and join all are facts about this profile’s implementation, never claims about the language in general. One more boundary, from the suite README: stage (allocation rounds, covered in nb-12: Allocation in rounds) and procedure never share one world.

Exercise

Without running the engine, predict, then check with law test:

1. In without the set the case stands still, a ReviewStarted event is never attempted — but suppose it were, with the case still in Draft. Which state would current_state(st1, …) report, and why does the from of StartReview decide it?
2. The guard rule uses kw <= 44 kW. Predict tech_ok(st1) for a 44 kW plate and for a 45 kW plate, and say which test outcome each would produce if every event were attempted.
3. In join waits for both regions, which region reached its terminal state and which did not — and what single additional attempt would flip Approved from NEITHER to TRUE_ONLY?
4. In re-entry holds the state, why do two File attempts leave the case Filed instead of moving it further — which transition could move it on, and on which event?
5. Name the three ingredients Decide needs in the ready test (case state, event, regions), and say which ingredient the over-threshold test breaks while keeping the other two intact.

Write down each prediction first; run the suite; explain any miss in one sentence. Checkable solution: full solution: predictions and checkable answers.

Sources

• Source: packs/examples/language-demo/procedure/package.law (events, TechWithinLimit, StationApproval with regions Docs/Tech and join all)
• Tests: packs/examples/language-demo/procedure/tests/procedure.lawtest (the six procedure tests)
• Suite tour: packs/examples/language-demo/README.md
• Language reference: docs/language/09-advanced-cheat-sheet.law.md (procedures and advanced constructs), docs/language/06-testing-a-package.law.md (the law test reference)
• Prerequisite: nb-09: From permit to duties and powers; next: nb-11: Appeal: reading, judgment and precedent

Three levels:

1. Northbridge use (this article): station filing under a completeness guard, parallel document and technical tracks with a 44 kW nameplate guard, one approval joined on both — verified by the six tests above.
2. Domain template: whenever one case needs several independent checks before a single decision, model each check as a region with its own terminal state, guard the technical tracks with derived institutional facts, join with join all, and read the case’s place only through current_state. Keep re-entry idempotent so retries never advance a case by accident.
3. Confirmed external formalization: bid opening in public procurement (Kazakhstan, art. 6(1)(2)) — package kz.corpus.procurement, corpus/laws/kz/laws/procurement/procurement.law:927-933, construct transition with from/to/on/when.

How procedures relate to appeals (next article)

The appeals package hears a contested refusal instead of moving a case: readings are selected, judgments are rendered, precedents are followed or distinguished. It is verified by law test packs/examples/language-demo/appeals (7 checked, 7 passed, 0 failed), including judgment rendered (TRUE_ONLY once the hearing officer’s judgment is on record) and precedent distinguished (FALSE_ONLY where the defendant’s facts differ). Procedures advance the undisputed case step by step; appeals resolve what is contested about it.

Sources and scope of verification

The external example is the OpenBids transition, with the domain-event carrier BidsOpeningHeld and the guard announced(lot). The move needs the right state plus the recorded event plus a true guard — this article’s “all three at once”, with the carrier as a domain event. Evidence: docs/research/constructs/18-procedure/corpus-forms.en.md, section 1 (rated exemplary there). The recorded verification confirms the construct’s presence at the cited lines only, by direct source read; it makes no claim about deployment, runtime behavior, or legal correctness.