Skip to content

Keep the stepper and View error when a state error cannot be marked, and put State Machine next to Verification - #161

Merged
CatarinaGamboa merged 2 commits into
mainfrom
feat/state-error-without-context
Oct 26, 2026
Merged

Keep the stepper and View error when a state error cannot be marked, and put State Machine next to Verification#161
CatarinaGamboa merged 2 commits into
mainfrom
feat/state-error-without-context

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

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.

State Machine tab without an error summary

After: the summary and View error are shown.

State Machine tab with The call at line 49 is rejected and View error

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

Verification tab with the error outlined

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

This was referenced Oct 25, 2026
Merged
Merged
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Show state errors in the State Machine view (#159)
0730892 
## 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 #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 #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).

<img width="900" alt="Verification tab with Show in state machine
buttons, tab badge and CodeLens"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/159/1-verification.png?v=3"
/>

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

<img width="560" alt="First state error, 1 of 3"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/159/2-first.png?v=3"
/> <img width="560" alt="Second state error, 2 of 3"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/159/3-next.png?v=3"
/>

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

<img width="560" alt="State Machine tab after coming back, still 2 of 3"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/159/4-back.png?v=3"
/>

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

<img width="560" alt="Verification tab with the bind error outlined"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/159/5-view-error.png?v=3"
/>

## 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](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)
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 and others added 2 commits October 26, 2026 10:59
@CatarinaGamboa @claude
Keep the stepper and View error when a state error cannot be marked
cb2febc 
When the verifier cannot tell which states allow the call, the diagram has
no marks and the error summary was not shown, so the state errors could not
be stepped through or opened in the Verification tab.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@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
CatarinaGamboa force-pushed the feat/state-error-without-context branch from 67a862b to 523d7c3 Compare October 26, 2026 10:59
@CatarinaGamboa
CatarinaGamboa changed the base branch from feat/155-state-errors-in-view to main October 26, 2026 10:59
@CatarinaGamboa CatarinaGamboa changed the title Keep the stepper and View error when a state error cannot be marked Keep the stepper and View error when a state error cannot be marked, and put State Machine next to Verification Oct 26, 2026
@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 26, 2026
Merged
@CatarinaGamboa
CatarinaGamboa merged commit 7b6a3bd into main Oct 26, 2026
3 of 6 checks passed
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Put the error actions on the title line and collapse hints (#164)
d4dd7bb 
## Description
Stacked on #161; merge that first.

- **Actions on the title line.** **Show in state machine** now sits on
the line of the error title, before the View related context and copy
icons. When the side bar is too narrow, the actions wrap below the
title, aligned right. Warnings get the same title line for their copy
icon.
- **Hints start closed.** A hint is a `Hint` section the user can open.
A hint the user opens stays open after a new verification, so editing
the code does not close it. Hints are matched across verifications by
the diagnostic's position, the same key the state errors already use,
now shared as `getDiagnosticKey`.

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

**Before**

<img width="560" alt="Error card with Show in state machine below the
title and the hint open"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/error-card/before.png"
/>

**After**, with the hint closed and then opened.

<img width="560" alt="Error card with Show in state machine on the title
line and a closed hint"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/error-card/after-closed.png"
/> <img width="560" alt="Error card with the hint opened"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/error-card/after-open.png"
/>

**A narrow side bar**: the actions wrap below the title.

<img width="360" alt="Narrow side bar with the actions below the title"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/error-card/after-narrow.png"
/>

## Tests
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 95 passed. In `script.spec.ts`, the state machine
button test now checks that it is the first action on the title line,
and a new test checks that hints start closed and stay open or closed
after a new verification.
- `npm test` (VS Code): 9 + 1 passing. 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
Retake #163 screenshots after rebasing on #161
1f51742
This was referenced Oct 26, 2026
Merged
Merged
CatarinaGamboa added a commit that referenced this pull request Oct 26, 2026
@CatarinaGamboa @claude
Put the error actions on the title line, collapse hints, and show hin…
a4cbd80 
…ts as separate options (#165)

## Description
Replaces #164, which was merged into the #161 branch after #161 had been
merged into main, so it never reached main. The first commit is #164
unchanged; the second separates the hints.

**Error title line (from #164).** **Show in state machine** sits on the
line of the error title, before the View related context and copy icons.
When the side bar is too narrow, the actions wrap below the title,
aligned right. Warnings get the same title line for their copy icon.

**Hints start closed (from #164).** The hints are a `Hint` / `Hints`
section the user can open. Hints the user opens stay open after a new
verification, so editing does not close them.

**Separate hints.** The verifier reports a list of hints, each with a
kind, but the server joined them into one string, so several suggested
call sequences read as if all of them had to be applied.
- **Server:** `hints` is now a list of `{ kind, message }`, from
`LJDiagnostic#getHints()`, replacing the joined `hint` string. The kind
is the verifier's `Hint.Kind` in kebab case, e.g. `call-sequence`.
- **View:** two or more `call-sequence` hints are listed as bullets
under **Any one of these:**. Every other hint, such as the calls
available in the current state, is its own paragraph, separated by a
line. A single call sequence is shown as a plain hint.

## Screenshots
`E_OSS_A1_17_InterruptManager` from the C-stars proposal in
building-examples-liquidjava, where the verifier suggests three call
sequences and lists the available calls.

**Before:** the action below the title, and the three call sequences and
the available calls run together.

<img width="560" alt="Error card before: Show in state machine below the
title"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/before-card.png"
/> <img width="560" alt="Hints before: all suggestions run together"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/before-hints.png"
/>

**After:** the actions on the title line, the hints closed and then
opened.

<img width="560" alt="Error card with the actions on the title line and
the hints closed"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-closed.png"
/> <img width="560" alt="Hints opened: Any one of these with three
bullets, then the available calls"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-open.png"
/>

**A narrow side bar:** the actions wrap below the title.

<img width="360" alt="Narrow side bar with the actions below the title"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-narrow.png"
/>

## Tests
- Server `mvn test`: 28 passing. New `DiagnosticConverterTest` test:
each hint keeps its kind and message, in order.
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 97 passed. New tests in `script.spec.ts`:
  - hints start closed and stay open or closed after a new verification;
- several call sequences are listed as options apart from the other
hints;
  - a single call sequence is a plain hint;
  - the state machine button is the first action on the title line.
- `npm test` (VS Code): 9 + 1 passing. Local smoke test: passed.

After the full run I only changed the CSS of the option list (bullets
and spacing). Unit tests and lint were re-run after it.

🤖 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
Show one state machine diagram per state set (#163)
083e4db 
Closes #115. Uses liquidjava-fsm 0.2.1 (liquid-java/liquidjava-fsm#13).

## Why
A class with several `@StateSet`s, like `ImageWriteParam` with its
tiling and compression states, was drawn as one diagram of the first
state set. Every compression method ended up on the tiling diagram, and
a compression error was marked on a tiling state:
`setCompressionQuality()` in `startCompression` showed `startTiling` as
rejected.

## What
- **Server:** `liquidjava/fsm` and `StateRefinementErrorDTO` now return
one `StateMachineDTO` per state set (`stateMachines`, with a `stateSet`
index), using `StateMachineParser.parseAll` from fsm 0.2.1.
- The error context goes only on the diagrams whose transitions include
the called method, and each one uses its own state set's part of the
verifier's states.
- A state is marked rejected only if no accepted state includes it, so a
call that is rejected because of another state set doesn't blame this
one. With one state set this gives the same marks as before.
- **View:** the diagrams are stacked, each titled with its states. The
diagram with the error comes first, and **Focus on error** dims the
others. The summary combines the state sets the call involves. **Copy
Mermaid Source** copies every diagram.
- A class with one state set looks exactly as before.
- The walkthrough mentions the per-state-set diagrams.

Arrows between state sets are left for later. A method that needs a
state of the other state set keeps it as a condition, e.g.
`[compressionSet(this)]`.

## Screenshots
Expert `ImageWriteParam` spec, in headless VS Code.

**Tiling error:** the tiling diagram comes first.

![Tiling
error](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/163/tiling-error.png?v=2)

**Focus on error:** the compression diagram below it is dimmed.

![Compression diagram
dimmed](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/163/compression-dimmed.png?v=2)

**Compression error, before and after:** before, it was drawn on the
tiling diagram with `startTiling` marked rejected. Now it is on the
compression diagram.

| Before | After |
|---|---|
|
![Before](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/163/before-compression-error.png)
|
![After](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/163/compression-error.png?v=2)
|

**Show all:**

![Show
all](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/163/show-all.png?v=2)

## Tests
- Server: `StateMachineDTOTest` (new) and `StateErrorContextDTOTest`
cover per-state-set marking and not blaming another state set. 34 tests
pass.
- Client: new specs for stacking, dimming, ordering and copying several
diagrams, and for an error that cannot be marked (#161) on a class with
several state sets. 105 unit tests pass, typecheck and lint are clean.
- Integration (`vscode-test`): all 10 tests pass.

Rebased on main after #165. The screenshots are from the build after
#161.

🤖 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.

1 participant

@CatarinaGamboa