Skip to content

Show state errors in the State Machine view - #159

Merged
CatarinaGamboa merged 3 commits into
mainfrom
feat/155-state-errors-in-view
Oct 26, 2026
Merged

Show state errors in the State Machine view#159
CatarinaGamboa merged 3 commits into
mainfrom
feat/155-state-errors-in-view

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Description

Closes #155.

Makes the State Machine view easy to reach from a state error and keeps the error there. Before, the only way in was a small icon on the error in the Verification tab, and clicking the State Machine tab dropped the error, so getting back meant going through the Verification tab again.

This replaces the earlier version of this PR, which listed the errors beside the diagram. That worked for one error but crowded the view with several, so the view now shows one error at a time.

  • Opens on the first error. The State Machine tab shows the first state error of the current file, focused, as Focus the state machine on the rejected call #158 draws it.
  • Keeps the error. An error chosen with Show in state machine or the arrows stays shown after visiting another tab. Opening another file shows its first error instead.
  • Follows the cursor. When the cursor reaches a state error in the editor, the view shows it. A choice made in the view is kept until the cursor reaches another error, and a new verification does not undo it.
  • Several errors. ‹ 1 of 3 › steps through the state errors of the current file in source order. The stepper only appears with more than one error.
  • Badge. The State Machine tab shows the number of state errors in the current file. This is the number of Show in state machine buttons under Current file in the Verification tab, and the of 3 in the stepper.
  • Back to the error. View error, next to the stepper, returns to that error in the Verification tab. The Show all / Focus on error toggle from Focus the state machine on the rejected call #158 now sits with the legend, since it changes the diagram and not the error.
  • Way in.
    • The type-hierarchy icon on state errors is replaced by a labelled Show in state machine button at the top of the error, below its title.
    • State errors also get a Show in state machine CodeLens in the editor. It reuses liquidjava.showView with an optional 'fsm' tab argument.
  • Re-verification.
    • The shown error is matched again by position. If an edit moved it, it is followed only when its call had exactly one error before and after, so it never jumps to a sibling.
    • Fixed errors disappear.
    • The diagram only re-renders when what it shows changed, so panning is kept.
  • Walkthrough. The text describes the new flow.

Screenshots

A throwaway copy of the UDP chat client with two more state errors: bind on a bound socket and connect after close. Taken after rebasing on #160, with the DatagramSocket spec fix that drops old() from the closed(this) preconditions.

1. Verification tab. Show in state machine at the top of each state error, the badge on the tab, and the CodeLens in the editor (State Refinement Error | Show in state machine, cut off at the editor edge here).

Verification tab with Show in state machine buttons, tab badge and CodeLens

2. Opening the State Machine tab shows the first error. 3. The next error.

First state error, 1 of 3 Second state error, 2 of 3

4. After visiting Context and coming back, the same error is still shown.

State Machine tab after coming back, still 2 of 3

5. View error returns to the bind error in the Verification tab and outlines it.

Verification tab with the bind error outlined

Tests

Rebased on main after #160 (verifier 0.0.36, liquidjava-fsm 0.2.0, Spoon 11.5.0):

  • npm run lint and npm run test:typecheck: clean.
  • npm run test:unit: 89 passed. The new tests are in:
    • state-errors.spec.ts: errors of the current file in source order, re-finding after verification;
    • fsm.spec.ts: stepper, badge, an error from another file, the focus toggle in the legend;
    • script.spec.ts: opening on the first error, the badge counting only the current file, tab memory, stepping, cursor-following, View error, opening from the editor, a new file, no re-render without changes, the button at the top of the error.
  • npm test (VS Code): passing, including the state-errors integration test, which checks the CodeLens and the message it sends to the webview.
  • Server mvn test and the local smoke test: passed.

Follow-ups stacked on this PR: #161 (errors the verifier cannot mark on the diagram) and #162 (tab order).

🤖 Generated with Claude Code

@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 24, 2026
Merged
CatarinaGamboa added a commit that referenced this pull request Oct 24, 2026
@CatarinaGamboa @claude
Focus the state machine on the rejected call (#158)
34d7611 
## Description
Closes #117.

When the State Machine view is opened from a state refinement error, it
marks the rejected call on the full diagram. There are two sets of
states:
- **P**, the states the receiver can be in, from Found;
- **A**, the states the call accepts, from Expected.

The view marks:
- **Invalid, P \ A**: red outline and **✕**. The call fails from here.
- **Valid, P ∩ A**: green outline and **✓**. The call is fine from here.
- **Accepted but not possible here, A \ P**: a thin dashed yellow
outline and no text. It hints at where the object could be brought.
- **The failed method**: every arrow labelled with it gets a red label,
including inside merged labels. The rejected call is never drawn as a
new transition.

Red and green have a faint fill and yellow is outline only, so a large
machine stays calm.

The full diagram is always shown. Focus mode dims what does not help
with the error:
- states outside P ∪ A;
- constructors;
- every method name that is neither the failed method nor a transition
that moves the receiver out of a state in P to a different state. This
applies to each name inside merged labels: in `getOption / receive /
send / …` only `receive` stays bright.

An arrow's path is dimmed only when all of its names are. "Show all" and
"Focus on error" switch the dimming off and on and keep pan and zoom.
The label text is identical in both modes, so the layout does not move.

A one-line legend shows only the marks that are present: "✕ Call
rejected", "✓ Call allowed" and "Allowed, but not reachable here". In
light themes the dashed outline uses a darker warning colour.

One summary line sits above the diagram, e.g. "`socket.receive()` is
rejected when `socket` is in state `closed` · allowed in state `bound`".

**Edge cases**
- When the receiver's state is unknown (every state is possible), only A
is marked, and the summary says the state is unknown.
- With no known receiver or accepted states, or with an older server,
the view behaves as on `main`.

**Data**
- P is `possibleStates` (liquid-java/liquidjava-fsm#11). With an older
server, it falls back to `definiteFoundState` and then `actualStates`.
- A is `expectedStates`.
- **Dependency:** bumps `liquidjava-fsm` to 0.1.5.
- The call is matched by its exact method name from the error context,
not by label text.
- "Copy Mermaid Source" copies the plain diagram.

## Screenshots
These are real verifier output in headless VS Code.

**UDP chat client.** The study example `E_OSS_A1_22_UdpChatClient`:
`receive` after an `if` that may close the socket. In focus mode the
following stay bright:
- `receive`;
- `close` and `connect` out of `bound`;
- the accessors out of `closed`.

The accessors stay bright because the DatagramSocket spec writes `from =
"closed(this) && connected(old(this))"`, which is drawn as an arrow from
`closed` to `connected`. That `old(...)` in a `from` is a spec error,
not an extension issue.

<img width="720" alt="DatagramSocket focus: only receive, close and
connect stay bright"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-focus-methods.png"
/>

<details><summary>Whole UDP machine: focus in dark and light, and Show
all</summary>

<img width="560" alt="UDP focus, dark"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-dark.png"
/> <img width="560" alt="UDP focus, light"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-light.png"
/>

<img width="560" alt="UDP Show all"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-show-all.png"
/>
</details>

**DefaultMutableTreeNode** (the issue's example). `getFirstChild()`
after `removeAllChildren()`:
- `childrenAllowed` is invalid;
- `maybeHasChildren` is accepted;
- `add`, the way there, stays bright;
- `removeAllChildren` is dimmed.

<img width="560" alt="Tree focus, dark"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/tree-dark.png"
/> <img width="560" alt="Tree focus, light"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/tree-light.png"
/>

<details><summary>Dimmed unrelated state (simplified demo machine, not a
real class)</summary>

<img width="560" alt="Dimmed unrelated state"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/dimming-demo.png"
/>
</details>

## Tests
Run against liquidjava-fsm 0.1.5 and verifier 0.0.35 from Maven Central:
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 75 passed in 7 files.
- `npm test` (VS Code): 8 + 1 passing.
- Server `mvn test`: 24 passing.
- Local smoke test: passed.

The new tests cover:
- the split into Valid, Invalid and accepted states;
- the fallbacks and the unknown-state case;
- empty or unknown states;
- exact method matching (`receive` does not match `receiveAll`);
- red labels inside merged labels;
- dimming of rendered paths and labels, per-name dimming inside merged
labels, and the rule for which methods count as useful;
- the legend;
- dimmed constructors;
- diagram clipping below the summary when panned;
- the toggle keeping zoom;
- plain Mermaid copy;
- the computed outline styles.

Independently reviewed twice; all findings were fixed.

## Known limits
- Large machines such as DatagramSocket have long stacked self-loop
labels. This already happens on `main`.
- #159 touches the same webview files; whichever PR merges second will
be rebased.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa
CatarinaGamboa force-pushed the feat/155-state-errors-in-view branch from 9150883 to 31edcee Compare October 24, 2026 22:46
CatarinaGamboa added a commit that referenced this pull request Oct 24, 2026
@CatarinaGamboa
Screenshots for the reworked #159
7c18c19
CatarinaGamboa and others added 3 commits October 25, 2026 21:23
@CatarinaGamboa @claude
Keep the state error in the State Machine view and link it to the editor
79accc2 
The tab keeps the last state error shown and follows the error at the cursor,
steps through several errors, counts them on the tab, and links back to the
error in the Verification tab. State errors get a labelled Show in state
machine button and CodeLens.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa @claude
Open the State Machine view on the first state error of the file
f3e6eba 
Count only the state errors of the current file, keep the focus toggle with
the legend apart from View error, and move Show in state machine to the top
of the error.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa @claude
Use the verifier's error context in the state error test fixtures
9fc9be9 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa
CatarinaGamboa force-pushed the feat/155-state-errors-in-view branch from 9a42f7a to 9fc9be9 Compare October 25, 2026 21:27
This was referenced Oct 25, 2026
Merged
Merged
@CatarinaGamboa
CatarinaGamboa merged commit 0730892 into main Oct 26, 2026
3 checks passed
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Put the State Machine tab next to Verification (#162)
5b65c2c 
## Description
Stacked on #159; merge that first. Independent of #161.

The tabs are now **Verification · State Machine · Context**.
Verification and State Machine link to each other through **Show in
state machine** and **View error**, so they now sit side by side.
Context shows the variables at the cursor for any file and works fine at
the end.

The walkthrough steps and the README sentence that lists them follow the
same order.

## Screenshots
`E_OSS_A1_19_AccessKeyGenerator` from the C-stars proposal in
building-examples-liquidjava.

**Before**

<img width="560" alt="Tabs: Verification, Context, State Machine"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/tab-order/before.png"
/>

**After**

<img width="560" alt="Tabs: Verification, State Machine, Context"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/tab-order/after.png"
/>

## Tests
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 90 passed. New test in `script.spec.ts` for the
tab order.
- `npm test` (VS Code): passed; the walkthrough test now expects the new
step order.
- Server `mvn test` and the local smoke test: passed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Put the State Machine tab next to Verification (#162)
523d7c3 
## Description
Stacked on #159; merge that first. Independent of #161.

The tabs are now **Verification · State Machine · Context**.
Verification and State Machine link to each other through **Show in
state machine** and **View error**, so they now sit side by side.
Context shows the variables at the cursor for any file and works fine at
the end.

The walkthrough steps and the README sentence that lists them follow the
same order.

## Screenshots
`E_OSS_A1_19_AccessKeyGenerator` from the C-stars proposal in
building-examples-liquidjava.

**Before**

<img width="560" alt="Tabs: Verification, Context, State Machine"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/tab-order/before.png"
/>

**After**

<img width="560" alt="Tabs: Verification, State Machine, Context"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/tab-order/after.png"
/>

## Tests
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 90 passed. New test in `script.spec.ts` for the
tab order.
- `npm test` (VS Code): passed; the walkthrough test now expects the new
step order.
- Server `mvn test` and the local smoke test: passed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Keep the stepper and View error when a state error cannot be marked, …
7b6a3bd 
…and put State Machine next to Verification (#161)

## Description
Based on main after #159. It also carries the tab order from #162, which
was merged into the #159 branch after #159 had been merged into main, so
it never reached main.

**Tab order.** The tabs are now **Verification · State Machine ·
Context**, since Verification and State Machine link to each other
through **Show in state machine** and **View error**. The walkthrough
steps and the README follow the same order. Screenshots and tests are in
#162.

**Errors without marks:**

When the verifier cannot tell which states allow a call, the diagram has
no marks and the error summary was not shown. With it went the `‹ 1 of 3
›` stepper and **View error**: the tab showed a badge but no way to step
through the errors or go back to them.

This happens in two cases:
- the allowed states depend on the call's arguments, so the verifier
reports no accepted states;
- the verifier finds no state machine for the call. In the C-stars
exercise `E_OSS_A1_09_PlayfieldWindow`, `setUndecorated` is a
`java.awt.Frame` method, but the `@StateSet` is declared on
`java.awt.Window`, so the error has no state context.

The summary row is now shown for every shown state error. Without marks,
it says `counter.open() is rejected here` when the verifier names the
call, or `The call at line 49 is rejected` otherwise. The legend and the
Show all toggle stay hidden, since nothing is marked or dimmed.

## Screenshots
`E_OSS_A1_09_PlayfieldWindow` from the C-stars proposal in
building-examples-liquidjava.

**Before** (#159): the badge says 1 state error, but nothing in the tab
shows it.

<img width="560" alt="State Machine tab without an error summary"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/state-error-without-context/before.png"
/>

**After:** the summary and View error are shown.

<img width="560" alt="State Machine tab with The call at line 49 is
rejected and View error"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/state-error-without-context/after.png"
/>

**View error** goes back to the error in the Verification tab.

<img width="560" alt="Verification tab with the error outlined"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/state-error-without-context/view-error.png"
/>

## Tests
Run on this branch, rebased on main (verifier 0.0.36, liquidjava-fsm
0.2.0):
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 94 passed. New tests:
- `fsm.spec.ts`: stepper, View error and text without accepted states,
without an error context, and without a position;
- `script.spec.ts`: stepping through errors without an error context and
going back to one, and the tab order.
- `npm test` (VS Code): 9 + 1 passing, including the walkthrough test
with the new step order.
- Server `mvn test`: 27 passing. Local smoke test: passed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Show state machine errors in the State Machine view

1 participant

@CatarinaGamboa