GeezerVison is showing github.com — State Machine view: show a multi-set state error in the set that is wrong by CatarinaGamboa · Pull Request #182 · liquid-java/vscode-liquidjava
Conversation
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
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
In the State Machine view, when the call is rejected because of the state of another state set:
- the call is red only in the diagram of the state set in a wrong state; in the others it is drawn as usual and its unmet condition is red, also with conditions collapsed
- the diagram of the state set in a wrong state comes first, so focus mode fits it
- a transition that keeps its state is drawn as a round loop instead of a curl as small as its arrowhead
- a condition on other state sets is written as their states after the method, e.g. open [lockState: unlocked], with != on a two-state set as its other state
- the summary line names the state sets (expected doorState closed, lockState unlocked · actual lockState locked) and leaves out those in which every state allows the call; unnamed state sets keep the current wording
Co-Authored-By: Claude Opus 5.5 <[email protected]>
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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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).
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
… the method
A transition label reads [condition before] method [condition after] on one line,
with each condition written as the spec writes it. The unmet clauses of a condition
are marked, also next to clauses that are not about a state.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
|
Codex review, round 6 (after the change to conditions as in the spec, [pre] method [post])
- [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.
- [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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
|
Codex review, round 7
- [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.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Assignees
No one assigned
Milestone
No milestone
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
|
