Repository navigation
Put the State Machine tab next to Verification - #162
Merged
Merged
Conversation
The Verification and State Machine tabs link to each other with Show in state machine and View error, so they now sit side by side, with Context last. The walkthrough steps follow the same order. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa
added a commit
that referenced
this pull request
Oct 26, 2026
## 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
merged commit Oct 26, 2026
5b65c2c
into
feat/155-state-errors-in-view
3 checks passed
CatarinaGamboa
added a commit
that referenced
this pull request
Oct 26, 2026
## 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
…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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
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_AccessKeyGeneratorfrom the C-stars proposal in building-examples-liquidjava.Before
After
Tests
npm run lintandnpm run test:typecheck: clean.npm run test:unit: 90 passed. New test inscript.spec.tsfor the tab order.npm test(VS Code): passed; the walkthrough test now expects the new step order.mvn testand the local smoke test: passed.🤖 Generated with Claude Code