[CatarinaGamboa]

Closes #180. Based on main (#178 and #174 are merged there); not stacked on #172 (see below).

What changes, per proposal

When a call needs the states of several state sets (Door: d.lock(); d.open();, open needs doorState(this) == closed && lockState(this) == unlocked):

• Failure marked where it is. Which set is wrong comes from the server's errorContext per diagram, not from message text: a set whose invalidStates is not empty is in a wrong state; a set whose possible states are all accepted, with another set in a wrong state, is "right". In a right set, a transition of the call from the actual state whose condition names the wrong set is drawn as usual (white, normal arrow) and only the clause the actual state does not meet is red, also when conditions are collapsed. In the wrong set the call is red as before. Every other transition of the call stays red as now: when it has no condition on the wrong set, when the condition is not only states, when no set is wrong on its own (the verifier can only reject the combination), or when the state is unknown.
• Wrong set first. orderStateMachines puts the sets in a wrong state first, then the other sets of the error, then the rest. Focus mode fits the first diagram as before, so the ✕ state is now on screen (A1_38: mark first, the case from the IDE review).
• Self-loops. A transition that keeps its state is drawn as a round loop (same ends, same side, as far out as before so it stays inside the laid-out SVG, slightly thicker) instead of ELK's flat curl the size of its arrowhead. It is redrawn after Mermaid renders, from a %% lj-self-loops: comment like the existing dimmed-transitions one.
• Conditions as in the spec, before and after the method. A label reads [condition before] method [condition after] on one line, e.g. [lockState(this) == unlocked] open. Each condition is the spec text, so it reads like the Expected box and the spec, and a condition with other clauses stays readable: in [lockState(this) == unlocked && size(this) > 0] open only the clause the actual state does not meet is red. Edge labels no longer wrap at Mermaid's 200px width, so a condition stays on the line of its method.
• Set names in the summary. "expected doorState closed, lockState unlocked · actual lockState locked": expected in declaration order; actual lists only the sets in a wrong state (all known ones if none is). A set in which every state allows the call is left out of both sides, for named and unnamed sets (the A1_56 "(undoable or notUndoable) and redoable" case). Unnamed sets keep the current wording.

Single-set classes are unchanged except for the round self-loops and the summary naming a named set (expected phase open · actual phase closed).

Ways to fix and #172

Not in this PR. Highlighting unlock on the diagram needs to know which calls a hint suggests, and HintDTO only has kind and message; getting the calls from the message text, or from paths in the diagram (judged unsound in #171), are both out. #172 lists the verifier's hints in a "Ways to fix" section and does not draw them; drawing a hint is #156, which needs a structured hint from the verifier first. So this PR does not depend on #172 and does not touch the hints; the two only meet in fsm.ts/script.ts call sites and should rebase cleanly in either order.

Screenshots

Headless VS Code, this branch's server (verifier 0.0.37, fsm 0.2.3). Focus mode is what opens from the error.

Door (the spec from #178, d.lock(); d.open();):

	Before (main)	After
Focus on error
Show all

Study exercise A1_38 (BufferedInputStream, sets stream and mark; buffered.reset() without mark(); proposal-D-task-types with liquidjava-api 0.0.8):

	Before (main)	After
Focus on error
Show all

The right set, scrolled down in focus mode (call drawn as usual, unmet condition red). These two and the A1_38 shots are from before the change to conditions as in the spec, which they still show as [lockState: unlocked]; the Door shots above are current:

Door doorState	A1_38 stream

Not in this PR

• Marking states that are current and fine (closed in doorState, open in stream), as agreed.
• Highlighting the ways to fix on the diagram (above).

Reviews

• Codex: 5 rounds (comments below); rounds 1-4 found one or two issues each, all fixed; round 5 found nothing.
• Clean-code audit: comment below; one fix, the rest declined with reasons.

Tests

• client: npm run test:unit 128 passed (5 new, each fails without the change: order, call/condition marks with != and collapsed conditions, round loop, named summary without the any-state set; one existing expectation gains the self-loop comment), npm run test:typecheck and npm run lint clean.
• server: no change; mvn -B test 39 passed.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main

The new cross-state-set highlighting can either hide the rejected call entirely or attribute it to an unrelated condition.

Review comment:

- [P2] Keep the failed-call marker unless an unmet guard is identified — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:124-127
  When another state set rejects the call, this removes the failed-call marker from every matching transition in the current diagram. If that transition has no `fromCondition`—as in the existing multi-set `write()` fixture—there is no unmet condition to mark, so the diagram no longer identifies the rejected call. If the condition is an unrelated predicate, the fallback instead colours that predicate as unmet without evidence. Only replace the method marker after identifying a guard on the rejecting state set.
The new cross-state-set highlighting can either hide the rejected call entirely or attribute it to an unrelated condition.

Review comment:

- [P2] Keep the failed-call marker unless an unmet guard is identified — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:124-127
  When another state set rejects the call, this removes the failed-call marker from every matching transition in the current diagram. If that transition has no `fromCondition`—as in the existing multi-set `write()` fixture—there is no unmet condition to mark, so the diagram no longer identifies the rejected call. If the condition is an unrelated predicate, the fallback instead colours that predicate as unmet without evidence. Only replace the method marker after identifying a guard on the rejecting state set.

Fixed in a00337d: the call keeps its red mark unless its condition is parsed as states and names the state set in a wrong state; a raw or unrelated condition is no longer coloured. Regression assertion added to the Door test.

[CatarinaGamboa]

Codex review, round 2

codex exec review --base origin/main

The new condition highlighting can identify a satisfied guard as the cause of an error, and enlarged self-loops can render outside the SVG bounds.

Full review comments:

- [P2] Mark only guards that the actual state violates — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:236-239
  When a condition has multiple clauses on the same state set, this marks every clause as unmet merely because that state set rejects the call. For example, with actual `lockState` = `locked`, `[lockState(this) != jammed && lockState(this) == unlocked]` marks both clauses, although `locked` satisfies the first. Compare each clause's allowed states with the receiver's possible states before marking it unmet.

- [P2] Expand SVG bounds when enlarging self-loops — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:333-336
  For a self-loop near the edge of a tightly laid-out diagram, the replacement Bézier can extend beyond Mermaid's original SVG viewBox. Because the path is enlarged only after Mermaid computes those bounds, the round loop can be clipped. Update the SVG bounds or reserve enough layout space for the rewritten path.
The new condition highlighting can identify a satisfied guard as the cause of an error, and enlarged self-loops can render outside the SVG bounds.

Full review comments:

- [P2] Mark only guards that the actual state violates — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:236-239
  When a condition has multiple clauses on the same state set, this marks every clause as unmet merely because that state set rejects the call. For example, with actual `lockState` = `locked`, `[lockState(this) != jammed && lockState(this) == unlocked]` marks both clauses, although `locked` satisfies the first. Compare each clause's allowed states with the receiver's possible states before marking it unmet.

- [P2] Expand SVG bounds when enlarging self-loops — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:333-336
  For a self-loop near the edge of a tightly laid-out diagram, the replacement Bézier can extend beyond Mermaid's original SVG viewBox. Because the path is enlarged only after Mermaid computes those bounds, the round loop can be clipped. Update the SVG bounds or reserve enough layout space for the rewritten path.

Fixed in b532387: (1) a clause is marked only if some possible state of the rejecting set does not meet it (Door test now covers lockState(this) != jammed && lockState(this) == unlocked); (2) instead of enlarging the SVG bounds, the round loop now reaches exactly as far out as ELK's curl did (control points at 4/3 of the curl's depth), so it stays inside the laid-out bounds.

[CatarinaGamboa]

Codex review, round 3

codex exec review --base origin/main

The new method-wide suppression can leave a failed-call transition without any visible error marker when only another transition has an unmet guard.

Review comment:

- [P2] Keep the failed-call marker on transitions without an unmet guard — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:126-126
  When the called method has multiple transitions and only one has an unmet cross-state-set condition, `hasUnmetCall` suppresses the failed-call marker on every transition with that method name. An alternative transition without that guard is then shown with neither a marked method nor a marked condition, hiding the error on that path. Apply the suppression per transition rather than per method.
The new method-wide suppression can leave a failed-call transition without any visible error marker when only another transition has an unmet guard.

Review comment:

- [P2] Keep the failed-call marker on transitions without an unmet guard — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/diagram.ts:126-126
  When the called method has multiple transitions and only one has an unmet cross-state-set condition, `hasUnmetCall` suppresses the failed-call marker on every transition with that method name. An alternative transition without that guard is then shown with neither a marked method nor a marked condition, hiding the error on that path. Apply the suppression per transition rather than per method.

Fixed in 5a5ec09: the decision is per transition — a transition of the call keeps its red mark unless it has its own unmet condition.

[CatarinaGamboa]

Codex review, round 4

codex exec review --base origin/main

The new summary filtering can make expected and actual states ambiguous for unnamed state sets.

Review comment:

- [P2] Keep unnamed state sets aligned in the error summary — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/views/fsm/fsm.ts:118-119
  When an error involves unnamed state sets and one of them allows the call in every state, `expectedErrors` omits that set but `knownErrors` still includes it in the actual-state list. For example, the summary can report one expected state against two actual states, with no names to show which states correspond. Keep the same state sets on both sides of the unnamed summary, or retain the unconstraining set there.
The new summary filtering can make expected and actual states ambiguous for unnamed state sets.

Review comment:

- [P2] Keep unnamed state sets aligned in the error summary — /tmp/claude-1000/-home-cvgamboa-git/65c26c82-6025-4502-8514-5187a6544fc7/scratchpad/wt180/client/src/webview/views/fsm/fsm.ts:118-119
  When an error involves unnamed state sets and one of them allows the call in every state, `expectedErrors` omits that set but `knownErrors` still includes it in the actual-state list. For example, the summary can report one expected state against two actual states, with no names to show which states correspond. Keep the same state sets on both sides of the unnamed summary, or retain the unconstraining set there.

Fixed in 1d4d893: a state set that allows the call in every state is now left out of both the expected and the actual side (named and unnamed), so the two sides stay aligned.

[CatarinaGamboa]

Codex review, round 5

codex exec review --base origin/main

I found no actionable regression in the diff. Type-checking and all 128 unit tests passed.
I found no actionable regression in the diff. Type-checking and all 128 unit tests passed.

Nothing to fix; loop ends here.

[CatarinaGamboa]

Clean-code review (clean-code-principles), own diff

• client/src/webview/diagram-focus.ts:81 - [core-encapsulation] hasWrongState was exported but only used inside the module. Fixed in 18a984a.
• client/src/webview/diagram.ts:48 - [func-few-arguments] createMermaidDiagram gains a fifth positional parameter (stateSets). Declined: it follows the existing positional style with defaults, and an options object would change every call site and test for no behaviour change.
• client/src/webview/diagram.ts:212 - [func-few-arguments] hasUnmetCondition takes four arguments. Declined: each is a distinct input of the decision; bundling them into an object would only move the names.
• client/src/webview/diagram.ts:216,234 - [core-dry] a called transition's condition is parsed twice (once to decide whether it is unmet, once to label it). Declined (KISS): parsing is a few regexes on one short string per transition; caching would couple the two functions.
• client/src/webview/diagram.ts:200-205 - [name-meaningful] getTransitionLabel now receives FromConditionLabel with isGuard instead of sniffing the HTML; the first draft compared a string prefix, replaced before pushing.
• client/src/webview/state-conditions.ts - [solid-srp] parsing the spec's state conditions lives in its own module, separate from rendering in diagram.ts; no change needed.

Nothing else relevant: no duplicated logic with existing helpers (getConditionLabel, escapeMermaidLabel, getListedTransitions are reused), no dead code, constants named (SELF_LOOPS_COMMENT).

[CatarinaGamboa]

Codex review, round 6 (after the change to conditions as in the spec, [pre] method [post])

1. [P2] A || anywhere made the whole condition unreadable as states, so lockState(this) == unlocked && (size(this) > 0 || ready(this)) lost its unmet mark. Fixed in the next commit: conditions split on the top-level &&, and only a part holding an || is left unread. The test covers this case.
2. [P2] The summary leaves out a set whose states are all accepted, but with correlated acceptance (only (A0,B0) and (A1,B1)) set A still decides which B is valid. Not changed: this is the agreed rule from the earlier rounds (the A1_56 case). The server sends only per-set projections, so the client can't tell a correlated combination from an independent one. No study spec has a disjunction across sets.

[CatarinaGamboa]

Codex review, round 7

1. [P2] Same issue as round 6 item 2, with a worse example: when no set is in a wrong state and a combination rejects the call, the summary could read expected C c · actual C c. Fixed: a set in which every state allows the call is left out only when another set is in a wrong state. Otherwise every set is named. The test covers both.