nb-10 solutions — A procedure with parallel checks

← Back to lessonChapter 10 / 25 · Advanced · Worked solution

How to verify

Checkable against law test packs/examples/language-demo/procedure (6 checked, 6 passed). Identifiers and code as written.

1. A review start attempted while in Draft

Answer: the case stays Draft — current_state(st1, Draft) is TRUE_ONLY and any Filed or Review query is NEITHER.

StartReview declares from Filed, and a transition fires only from its from state. An attempt while the case rests in Draft finds no matching step, so it is absorbed with no effect — the same absorption the without the set test shows for a guardless-blocked File. State first, event second: the procedure checks where the case is before it cares what happened.

2. The 44 kW boundary

Answer: 44 kW derives tech_ok (the rule uses <=); 45 kW does not — so 44 kW approves like the 22 kW test, 45 kW blocks like the 120 kW test.

TechWithinLimit fires when kw <= 44 kW. A 44 kW plate satisfies the comparison, TechAccept reaches TechOk, both regions are terminal, and Decide yields Approved TRUE_ONLY. A 45 kW plate fails the comparison exactly as 120 kW does: tech_ok never holds, the Tech region stays TechPending, the join is unsatisfied, and Approved is NEITHER. Boundary included on one side only — <= against the declared 44 kW teaching value.

3. Which region finished, and the one missing attempt

Answer: Docs reached DocsOk; Tech stayed TechPending. Attempting TechAccept with the TechApproved event flips Approved to TRUE_ONLY.

The join-waits test attempts DocsAccept (with DocsFiled) but never attempts TechAccept. With the 22 kW plate the guard would hold, so the single missing ingredient is the attempt itself: add the tech assertion from the ready test — attempted_transition(st1, TechAccept, TechApproved { … }) at 13:00 — and both regions are terminal when Decide fires on ReviewComplete, giving Approved TRUE_ONLY. This is the article’s changed condition in reverse: same setup, one attempt added, join satisfied.

4. Why double filing stays Filed

Answer: the second File finds the case already past its from state, so it misfires; only StartReview on ReviewStarted moves the case on to Review.

The first attempt carries Draft → Filed and fires. The second attempt names the same transition, whose from is Draft — but the case now rests in Filed, so the step does not apply and the case holds. Re-entry is absorbed, never re-executed. Progress needs a different transition: StartReview (from Filed, on ReviewStarted), which the ready test attempts at 11:00 to enter the parallel state.

5. The three ingredients of Decide, and which the threshold breaks

Answer: (a) the case rests in Review with both regions terminal, (b) the ReviewComplete event is on record, (c) the join sees DocsOk and TechOk. The over-threshold test keeps (a)-in-part and (b) but breaks (c) via the Tech guard.

Standing: filing and review entry succeeded (22-vs-120 differs only in the plate), so the case is in Review. Event: Decide with ReviewComplete at 14:00 is attempted in both tests. Regions: Docs reaches DocsOk in both — but with 120 kW tech_ok never holds, so TechAccept misfires, Tech stays TechPending, and join all refuses the exit. Add nothing but a passing plate and the twin test both regions ready — decision taken goes TRUE_ONLY.

How to verify

Terminal

law test packs/examples/language-demo/procedure

Expected: итого: 6 проверено, 6 прошли, 0 не прошли, 0 не исполнены. The deciding tests are filing with a complete set, without the set the case stands still, re-entry holds the state, both regions ready — decision taken, join waits for both regions, and technical conditions above the threshold block the region.