From 0479c75f67416c9b290d10adaf657b109ee92087 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 12:22:56 +0000 Subject: [PATCH] Show the verifier's hints in the State Machine view The State Machine view showed where a call is rejected but not how to fix it, while the verifier's hints were only in the Verification tab. A collapsed "Ways to fix" section under the legend now lists the hints of the shown error, as in the Verification tab. Nothing is read from the diagram, which ignores the transitions' conditions and the code. Its open state is kept per error, apart from the Verification tab's hints. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/diagram.ts | 4 +- client/src/webview/script.spec.ts | 17 +++++++++ client/src/webview/script.ts | 3 +- client/src/webview/styles.ts | 15 ++++++++ client/src/webview/views/fsm/fsm.spec.ts | 37 +++++++++++++++++++ client/src/webview/views/fsm/fsm.ts | 35 ++++++++++++++++-- client/src/webview/views/sections.ts | 47 ++++++++++++++++-------- 7 files changed, 136 insertions(+), 22 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index e3c61cd..c7ec593 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -549,8 +549,8 @@ export function registerPanListeners(document: any) { const onMouseDown = (e: any) => { const target = e.target as any; if (target.tagName === 'A' || target.tagName === 'BUTTON') return; - // keep the error summary text selectable, and the collapsed labels clickable - if (target.closest?.('.diagram-error-summary, .lj-collapsed-methods, .lj-methods-popover')) return; + // keep the error summary and the ways to fix it selectable, and the collapsed labels clickable + if (target.closest?.('.diagram-error-summary, .diagram-fixes, .lj-collapsed-methods, .lj-methods-popover')) return; e.preventDefault(); isPanning = true; diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 1757650..73457db 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -530,6 +530,23 @@ describe('webview script', () => { expect(hint().open).toBe(false); }); + it('shows the hints of the shown state error as ways to fix it, open after switching tabs once opened', () => { + const error = { ...stateError('State refinement error', errorMachine('Counter', 'close')), hints: [{ kind: 'general' as const, message: 'Call open() first' }] }; + showDiagnostics([error]); + click('.diagnostic-state-machine-btn'); + const ways = () => root.querySelector('.diagram-fixes')!; + expect(ways().open).toBe(false); + expect(ways().querySelector('.hint-message')?.textContent).toBe('Call open() first'); + + ways().open = true; + ways().dispatchEvent(new Event('toggle')); + click('[data-tab="diagnostics"]'); + // the hint of the Verification tab keeps its own state + expect(root.querySelector('.error-item .hint-section')!.open).toBe(false); + click('[data-tab="fsm"]'); + expect(ways().open).toBe(true); + }); + it('opens on the first state error of a newly opened file', () => { showDiagnostics([ stateError('Main error', errorMachine('Main', 'close'), 4), diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index bce2a0d..fbd5cd3 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -441,7 +441,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) .map(sm => createMermaidDiagram({ ...sm, errorContext: null }, diagramOrientation, showDiagramConditions, false, displayedStateMachines)) .join('\n\n'); renderStateMachineView(root, displayedStateMachines, diagrams, diagramOrientation, showDiagramConditions, focusOnError, - { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }, badges); + { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }, badges, + shownError ? { hints: shownError.hints, key: getStateErrorKey(shownError) } : undefined); renderedStateMachineView = getStateMachineViewKey(); if (displayedStateMachines.length > 0) renderMermaidDiagram(document, window); break; diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 39c39d7..ac83a49 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -1308,5 +1308,20 @@ export function getStyles(): string { border: 1px dashed; border-color: var(--lj-state-accepted); } + .diagram-fixes { + margin-bottom: 0.75rem; + font-size: 0.85rem; + cursor: default; + user-select: text; + } + .diagram-fixes[open] .hint-summary { + margin-bottom: 0.25rem; + } + .diagram-fixes-source { + margin: 0.5rem 0 0.25rem; + font-size: 0.8rem; + font-weight: 600; + color: var(--vscode-descriptionForeground); + } `; } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 1d4110c..756986c 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -136,6 +136,43 @@ describe('state machine view', () => { expect(button('diagram-focus-btn').textContent?.trim()).toBe('Focus on error'); }); + describe('ways to fix', () => { + const socket = () => machine({ + className: 'DatagramSocket', states: ['unbound', 'bound', 'connected', 'closed'], + initialTransitions: [{ to: 'bound', constructorSignature: 'new DatagramSocket()' }], + transitions: [{ from: 'closed', to: 'unbound', label: 'reset' }], errorContext: socketError(['bound', 'closed']), + }); + const pathDependent = { kind: 'path-dependent-state' as const, message: 'socket can be in bound or closed here, depending on the path taken' }; + + it('lists the verifier hints, collapsed', () => { + renderStateMachineView(document.body, [socket()], [diagram], 'TB', false, true, undefined, undefined, { hints: [pathDependent], key: 'error' }); + + const section = document.querySelector('details.diagram-fixes')!; + expect(section.open).toBe(false); + expect(section.getAttribute('data-hint-key')).toBe('fsm|error'); + expect(section.querySelector('.diagram-fixes-source')?.textContent).toBe('From the verifier'); + expect(section.querySelector('.hint-note')?.textContent).toBe(pathDependent.message); + // nothing is read from the diagram, which ignores the conditions and the code + expect(section.textContent).not.toContain('socket.reset()'); + }); + + it('shows the verifier hints of an error that cannot be marked on the diagram', () => { + const sm = socket(); + sm.errorContext = { ...sm.errorContext!, acceptedStates: [], validStates: [], invalidStates: [] }; + renderStateMachineView(document.body, [sm], [diagram], 'TB', false, true, { index: 0, count: 1, line: 4 }, undefined, { hints: [pathDependent], key: 'error' }); + + expect(document.querySelector('.diagram-fixes .hint-note')?.textContent).toBe(pathDependent.message); + }); + + it('has no section without hints', () => { + renderStateMachineView(document.body, [socket()], [diagram], 'TB', false, true, undefined, undefined, { hints: [], key: 'error' }); + expect(document.querySelector('.diagram-fixes')).toBeNull(); + + renderStateMachineView(document.body, [socket()], [diagram], 'TB', false, true); + expect(document.querySelector('.diagram-fixes')).toBeNull(); + }); + }); + it('names the expected and actual states when no actual is expected', () => { renderStateMachineView(document.body, [machine({ states: ['childrenAllowed', 'maybeHasChildren'], diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 1f06454..65f50bf 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,8 +1,9 @@ +import type { LJHint } from "../../../types/diagnostics"; import type { LJStateMachine } from "../../../types/fsm"; import { INVALID_STATE_ICON, VALID_STATE_ICON, getRejectedCallText, getStateErrorFocus, getStateErrorFocuses, type StateErrorFocus } from "../../diagram-focus"; import { renderCodiconButton } from "../../icons"; import { escapeHtml } from "../../utils"; -import { renderMainHeader, type NavBadges } from "../sections"; +import { getShownHints, renderHintKey, renderHintList, renderMainHeader, type NavBadges } from "../sections"; /** * The position of the shown state error among the state errors of the current file @@ -17,18 +18,26 @@ export type StateErrorNavigation = { const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 }; +/** + * The verifier's hints of the shown state error, and the key that keeps their section open across renders + */ +export type StateErrorHints = { + hints: LJHint[]; + key: string; +}; + /** * Renders the State Machine view with the diagram of each state set of a class, stacked * @param sms the state machines, one per state set * @param diagrams the Mermaid diagram of each state machine */ -export function renderStateMachineView(root: HTMLElement, sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION, badges: NavBadges = { errors: 0, stateErrors: stateErrors.count }) { +export function renderStateMachineView(root: HTMLElement, sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION, badges: NavBadges = { errors: 0, stateErrors: stateErrors.count }, hints?: StateErrorHints) { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; const diagramHeight = previousDiagramContainer?.offsetHeight; - root.innerHTML = renderStateMachineViewHtml(sms, diagrams, orientation, showConditions, focusOnError, stateErrors, badges, diagramHeight); + root.innerHTML = renderStateMachineViewHtml(sms, diagrams, orientation, showConditions, focusOnError, stateErrors, badges, hints, diagramHeight); } -function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, badges: NavBadges, diagramHeight?: number): string { +function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, badges: NavBadges, hints: StateErrorHints | undefined, diagramHeight?: number): string { const className = sms[0]?.className; const errorFocuses = getStateErrorFocuses(sms); const hasConditionExpansions = sms.some(sm => @@ -59,6 +68,7 @@ function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], o ${errorFocuses.length > 0 ? renderStateErrorSummary(getStateErrorSummary(sms), stateErrors) + renderStateErrorLegend(errorFocuses, focusOnError) : isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sms, stateErrors), stateErrors) : ''} + ${renderWaysToFix(hints)} ${showConditions && hasConditionExpansions ? /*html*/`
Precondition @@ -168,6 +178,23 @@ function renderStateErrorStepper({ index, count }: StateErrorNavigation): string `; } +/** + * Renders the verifier's hints for the shown state error, collapsed like the hints in the Verification tab + */ +function renderWaysToFix(hints: StateErrorHints | undefined): string { + const verifierHints = getShownHints(hints?.hints); + if (verifierHints.length === 0) return ''; + return /*html*/` +
+ Ways to fix +
+

From the verifier

+
${renderHintList(verifierHints)}
+
+
+ `; +} + // explains the state marks with the same outlines, fills, and icons as the diagram, next to the toggle that collapses the rest function renderStateErrorLegend(focuses: StateErrorFocus[], focusOnError: boolean): string { const items = [ diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 6941ca7..d295dea 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -36,28 +36,45 @@ export function setHintOpen(key: string, open: boolean) { * @param key Identifies the diagnostic, so opened hints stay open after a new verification */ export function renderHints(hints: LJHint[] | undefined, key?: string): string { - const shown = (hints ?? []).filter(hint => hint.message.trim()); + const shown = getShownHints(hints); if (shown.length === 0) return ''; - const options = shown.filter(hint => hint.kind === 'call-sequence'); - const listsOptions = options.length > 1; - const notes = listsOptions ? shown.filter(hint => hint.kind !== 'call-sequence') : shown; - const open = key !== undefined && openHints.has(key); return /*html*/` -
+
${shown.length === 1 ? 'Hint' : 'Hints'} -
- ${listsOptions ? /*html*/` -
-

Any one of these:

-
    ${options.map(hint => `
  • ${renderHintMessage(hint)}
    • `).join('')}
-
- ` : ''} - ${notes.map(hint => `
${renderHintMessage(hint)}
`).join('')} -
+
${renderHintList(shown)}
`; } +export function getShownHints(hints: LJHint[] | undefined): LJHint[] { + return (hints ?? []).filter(hint => hint.message.trim()); +} + +// the attributes that keep a hint section open across renders +export function renderHintKey(key: string | undefined): string { + if (key === undefined) return ''; + return ` data-hint-key="${escapeHtml(key)}"${openHints.has(key) ? ' open' : ''}`; +} + +/** + * Renders hints with the calls to add as options, when there are several, followed by the other hints + * @param hints the hints with a message + */ +export function renderHintList(hints: LJHint[]): string { + const options = hints.filter(hint => hint.kind === 'call-sequence'); + const listsOptions = options.length > 1; + const notes = listsOptions ? hints.filter(hint => hint.kind !== 'call-sequence') : hints; + return /*html*/` + ${listsOptions ? /*html*/` +
+

Any one of these:

+
    ${options.map(hint => `
  • ${renderHintMessage(hint)}
    • `).join('')}
+
+ ` : ''} + ${notes.map(hint => `
${renderHintMessage(hint)}
`).join('')} + `; +} + function renderHintMessage(hint: LJHint): string { return `${escapeHtml(hint.message.trim())}`; }