From cb2febc7b01e35b38283e52ecd982d28c9ca6334 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 21:46:59 +0000 Subject: [PATCH 1/2] Keep the stepper and View error when a state error cannot be marked 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 --- client/src/webview/script.spec.ts | 17 ++++++++++++++++ client/src/webview/script.ts | 8 +++++++- client/src/webview/views/fsm/fsm.spec.ts | 23 +++++++++++++++++++++ client/src/webview/views/fsm/fsm.ts | 26 ++++++++++++++++++++++-- 4 files changed, 71 insertions(+), 3 deletions(-) diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index bfe2ed1..34d7557 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -309,6 +309,23 @@ describe('webview script', () => { expect(root.querySelectorAll('.diagnostic-state-machine-btn')).toHaveLength(1); }); + it('steps through state errors the verifier could not mark on the diagram', () => { + showDiagnostics([ + stateError('First state error', { ...errorMachine('First', 'close'), errorContext: null }, 4), + stateError('Second state error', { ...errorMachine('Second', 'reset'), errorContext: null }, 9), + ]); + click('[data-tab="fsm"]'); + expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 5 is rejected'); + expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2'); + + click('.state-error-step-btn[data-step="1"]'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Second'); + expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 10 is rejected'); + + click('#state-error-reveal-btn'); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics'); + }); + it('follows the state error at the cursor without overriding a later choice', () => { const first = stateError('First state error', errorMachine('First', 'close'), 4); const second = stateError('Second state error', errorMachine('Second', 'reset'), 9); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 6dcb6f5..672795e 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -430,7 +430,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) ? createMermaidDiagram({ ...displayedStateMachine, errorContext: null }, diagramOrientation, showDiagramConditions) : diagram; renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError, - { index: shownIndex, count: stateErrors.length }); + { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }); renderedStateMachineView = getStateMachineViewKey(); if (displayedStateMachine) renderMermaidDiagram(document, window); break; @@ -441,6 +441,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } } + // the 1-based line of the shown error, null without a position, undefined when no error is shown + function getStateErrorLine(error: StateRefinementError | undefined): number | null | undefined { + if (!error) return undefined; + return error.position ? error.position.lineStart + 1 : null; + } + function getCurrentStateErrors(): StateRefinementError[] { return getStateErrors(diagnostics, currentFile); } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 1bb4c4a..f28de28 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -196,6 +196,29 @@ describe('state machine view', () => { expect(document.querySelector('#diagram-focus-btn')).toBeNull(); }); + it.each([ + ['without the accepted states', { + calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'], + acceptedStates: [], validStates: [], invalidStates: [], + }, 'counter.open() is rejected here'], + ['without an error context', null, 'The call at line 12 is rejected'], + ])('keeps the stepper and View error for a shown error %s', (_, errorContext, text) => { + renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true, { index: 1, count: 2, line: 12 }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe(text); + expect(document.querySelector('.state-error-position')?.textContent).toBe('2 of 2'); + expect(button('state-error-reveal-btn')).not.toBeNull(); + // nothing is marked, so there is nothing to explain or dim + expect(document.querySelector('.diagram-error-legend')).toBeNull(); + expect(document.querySelector('#diagram-focus-btn')).toBeNull(); + }); + + it('says the call is rejected without a line when the shown error has no position', () => { + renderStateMachineView(document.body, machine(), diagram, 'TB', false, true, { index: -1, count: 0, line: null }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe('The call is rejected'); + }); + it('clips the panned diagram below the error summary and legend', () => { renderStateMachineView(document.body, machine({ errorContext: { diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index ffe0836..88d9c8b 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -11,6 +11,8 @@ import { renderMainHeader } from "../sections"; export type StateErrorNavigation = { index: number; count: number; + // the 1-based line of the shown error, if any error is shown + line?: number | null; }; const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 }; @@ -48,7 +50,9 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })} - ${errorFocus ? renderStateErrorSummary(errorFocus, stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) : ''} + ${errorFocus + ? renderStateErrorSummary(getStateErrorSummary(errorFocus), stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) + : isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sm, stateErrors), stateErrors) : ''} ${showConditions && hasConditionExpansions ? /*html*/`
Precondition @@ -67,7 +71,11 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str `; } -function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateErrorNavigation): string { +function isStateErrorShown(stateErrors: StateErrorNavigation): boolean { + return stateErrors.index >= 0 || stateErrors.line !== undefined; +} + +function getStateErrorSummary(focus: StateErrorFocus): string { const call = getRejectedCallText(focus); const receiver = focus.receiver ? `${escapeHtml(focus.receiver)}` : 'the receiver'; const rejected = `${call ? `${escapeHtml(call)}` : 'The call'} is rejected`; @@ -81,6 +89,20 @@ function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateError summary = `${rejected} here`; } if (allowedStates.length > 0) summary += ` \u00B7 allowed in state ${renderStates(allowedStates)}`; + return summary; +} + +// the shown error cannot be marked on the diagram when the verifier could not tell which states allow the call +function getUnmarkedStateErrorSummary(sm: LJStateMachine, stateErrors: StateErrorNavigation): string { + const context = sm.errorContext; + if (context?.calledMethod) { + const call = `${context.receiver ? `${context.receiver}.` : ''}${context.calledMethod}()`; + return `${escapeHtml(call)} is rejected here`; + } + return stateErrors.line ? `The call at line ${stateErrors.line} is rejected` : 'The call is rejected'; +} + +function renderStateErrorSummary(summary: string, stateErrors: StateErrorNavigation): string { return /*html*/`

${summary}

From 523d7c3fb479b8fd2761be8d1a3144992f095a51 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Mon, 26 Oct 2026 11:57:27 +0100 Subject: [PATCH 2/2] Put the State Machine tab next to Verification (#162) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## 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** Tabs: Verification, Context, State Machine **After** Tabs: Verification, State Machine, Context ## 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 --- client/README.md | 2 +- client/package.json | 16 ++++++++-------- client/src/test/walkthrough.test.ts | 2 +- client/src/webview/script.spec.ts | 6 ++++++ client/src/webview/views/sections.ts | 2 +- 5 files changed, 17 insertions(+), 11 deletions(-) diff --git a/client/README.md b/client/README.md index 7b359af..cbbc4df 100644 --- a/client/README.md +++ b/client/README.md @@ -40,7 +40,7 @@ A repository with LiquidJava examples is available at [liquidjava-examples](http ### Getting started in VS Code -The **Get Started with LiquidJava** walkthrough introduces LiquidJava and its interactive tutorial, includes copyable Maven/Gradle annotation dependencies, then explains verification and its status indicator, diagnostics, context, state machines, the Command Palette, and logs. It also links to the [interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/). It opens once on installation, following VS Code’s walkthrough preferences. You can dismiss it at any time and reopen it with **LiquidJava: Show Walkthrough** from the Command Palette or **LiquidJava: Show Commands**. VS Code saves its progress across workspaces. +The **Get Started with LiquidJava** walkthrough introduces LiquidJava and its interactive tutorial, includes copyable Maven/Gradle annotation dependencies, then explains verification and its status indicator, diagnostics, state machines, context, the Command Palette, and logs. It also links to the [interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/). It opens once on installation, following VS Code’s walkthrough preferences. You can dismiss it at any time and reopen it with **LiquidJava: Show Walkthrough** from the Command Palette or **LiquidJava: Show Commands**. VS Code saves its progress across workspaces. ### What are Liquid Types? diff --git a/client/package.json b/client/package.json index 03c22c5..85cd42e 100644 --- a/client/package.json +++ b/client/package.json @@ -227,22 +227,22 @@ ] }, { - "id": "context", - "title": "Inspect context", - "description": "The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.\nLocal variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.\nClick a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.\n[Open LiquidJava view](command:liquidjava.showView)", + "id": "stateMachine", + "title": "Explore state machines", + "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { - "markdown": "media/walkthrough/context.md" + "markdown": "media/walkthrough/state-machine.md" }, "completionEvents": [ "onStepSelected" ] }, { - "id": "stateMachine", - "title": "Explore state machines", - "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)", + "id": "context", + "title": "Inspect context", + "description": "The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.\nLocal variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.\nClick a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { - "markdown": "media/walkthrough/state-machine.md" + "markdown": "media/walkthrough/context.md" }, "completionEvents": [ "onStepSelected" diff --git a/client/src/test/walkthrough.test.ts b/client/src/test/walkthrough.test.ts index 9270f5b..899fe14 100644 --- a/client/src/test/walkthrough.test.ts +++ b/client/src/test/walkthrough.test.ts @@ -25,7 +25,7 @@ suite('LiquidJava walkthrough', () => { assert.ok(walkthrough); assert.equal(walkthrough.title, 'Get Started with LiquidJava'); assert.deepEqual(walkthrough.steps.map((step: { id: string }) => step.id), - ['tutorial', 'annotations', 'verification', 'commands', 'diagnostics', 'context', 'stateMachine', 'logs']); + ['tutorial', 'annotations', 'verification', 'commands', 'diagnostics', 'stateMachine', 'context', 'logs']); assert.equal(walkthrough.steps[0].title, 'Learn LiquidJava'); const commands = await vscode.commands.getCommands(true); assert.ok(commands.includes('liquidjava.showWalkthrough')); diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 34d7557..9b814ef 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -127,6 +127,12 @@ describe('webview script', () => { receive({ type: 'status', status: diagnostics.some(d => d.category === 'error') ? 'failed' : 'passed' }); } + it('puts the State Machine tab next to Verification, which link to each other', () => { + showDiagnostics([]); + + expect(Array.from(root.querySelectorAll('.nav-tab'), tab => tab.getAttribute('data-tab'))).toEqual(['diagnostics', 'fsm', 'context']); + }); + it('posts ready and renders the initial loading view', () => { expect(postMessage.mock.calls).toEqual([[{ type: 'ready' }]]); expect(root.querySelector('h2')?.textContent).toBe('Verification Pending'); diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index de512f5..3dd7b6d 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -141,8 +141,8 @@ export function renderNav(selectedTab: NavTab, stateErrorCount = 0): string { `;