# nb-10 — A procedure with parallel checks
*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](/tutorials/northbridge/nb-01-first-permit/) through
[nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/)), and
[nb-09: From permit to duties and powers](/tutorials/northbridge/nb-09-duties-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](/tutorials/northbridge/nb-01-first-permit/) 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](/tutorials/northbridge/nb-02-missing-fact/) for
the four truth statuses. Below, `NEITHER` means "no conclusion either
way" — never a refusal.
[nb-09: From permit to duties and powers](/tutorials/northbridge/nb-09-duties-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`.
```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.
```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.
```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`.
```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:
```sh
law test packs/examples/language-demo/procedure
```
Observed result (engine `law 0.1.0`):
```text
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:
```sh
law engine check packs/examples/language-demo/procedure/package.law
```
```text
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](/tutorials/northbridge/nb-01-first-permit/) through
[nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/) 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](/tutorials/northbridge/nb-09-duties-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](/tutorials/northbridge/nb-12-allocation-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](/tutorials/northbridge/solutions/nb-10-solutions/).
## 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](/tutorials/northbridge/nb-09-duties-powers/);
next: [nb-11: Appeal: reading, judgment and precedent](/tutorials/northbridge/nb-11-appeal/)
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.