liquid-java · rcosta358 · Aug 9, 2026 · Aug 9, 2026
diff --git a/client/src/services/events.ts b/client/src/services/events.ts
@@ -36,6 +36,7 @@ export function registerEvents(context: vscode.ExtensionContext) {
  */
 export async function onActiveFileChange(editor: vscode.TextEditor) {
     extension.file = normalizeFilePath(editor.document.uri.fsPath);
+    extension.stateMachine = undefined;
     extension.webview?.sendMessage({ type: "file", file: extension.file });
     await updateStateMachine(editor.document);
     handleContextUpdate(editor.selection);
@@ -70,4 +71,4 @@ function handleContextUpdate(selection: vscode.Selection) {
     extension.context.allVars = allVars;
     updateErrorAtCursor();
     extension.webview?.sendMessage({ type: "context", context: extension.context, errorAtCursor: extension.errorAtCursor });
-}
+}
diff --git a/client/src/services/state-machine.ts b/client/src/services/state-machine.ts
@@ -1,16 +1,17 @@
 import * as vscode from "vscode";
 import { extension } from "../state";
 import { LJStateMachine } from "../types/fsm";
+import { normalizeFilePath } from "../utils/utils";
 
 /**
  * Requests the state machine for the given document from the language server
  * @param document The text document
  */
 export async function updateStateMachine(document: vscode.TextDocument) {
-    const sm = await extension.client?.sendRequest<LJStateMachine>("liquidjava/fsm", { uri: document.uri.toString() });
+    const file = normalizeFilePath(document.uri.fsPath);
+    const sm = await extension.client?.sendRequest<LJStateMachine | null>("liquidjava/fsm", { uri: document.uri.toString() });
+    if (file !== extension.file) return;
 
-    // dont update diagram if it hasnt changed to a new one
-    if (!sm || JSON.stringify(sm) === JSON.stringify(extension.stateMachine)) return;
     extension.stateMachine = sm;
     extension.webview?.sendMessage({ type: "fsm", sm });
 }
diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts
@@ -36,7 +36,7 @@ export function registerWebview(context: vscode.ExtensionContext) {
                 if (extension.file) extension.webview?.sendMessage({ type: "file", file: extension.file });
                 if (extension.diagnostics) extension.webview?.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics });
                 if (extension.context) extension.webview?.sendMessage({ type: "context", context: extension.context , errorAtCursor: extension.errorAtCursor });
-                if (extension.stateMachine) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine });
+                if (extension.stateMachine !== undefined) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine });
                 if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
                 if (pendingDiagnosticReveal) {
                     extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic: pendingDiagnosticReveal });

diff --git a/client/src/state.ts b/client/src/state.ts
@@ -25,7 +25,7 @@ export class ExtensionState {
     // application state
     file?: string;
     diagnostics?: LJDiagnostic[];
-    stateMachine?: LJStateMachine;
+    stateMachine?: LJStateMachine | null;
     context?: LJContext;
     currentSelection?: Range;
     errorAtCursor?: RefinementMismatchError;

diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts
@@ -1,4 +1,5 @@
 import type { Range } from './context';
+import type { LJStateMachine } from './fsm';
 import type { VCSimplificationResult } from './vc-implications';
 
 // Type definitions used for LiquidJava diagnostics
@@ -62,6 +63,7 @@ export type RefinementError = BaseDiagnostic & {
     found: VCSimplificationResult;
     customMessage: string;
     counterexample: string;
+    declarationPosition: SourcePosition | null;
 }
 
 export type StateConflictError = BaseDiagnostic & {
@@ -78,6 +80,8 @@ export type StateRefinementError = BaseDiagnostic & {
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;
+    declarationPosition: SourcePosition | null;
+    stateMachine: LJStateMachine | null;
 }
 
 export type ArgumentMismatchError = BaseDiagnostic & {

diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts
@@ -30,7 +30,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     let diagnostics: LJDiagnostic[] | undefined;
     let showAllDiagnostics = false;
     let currentFile: string;
-    let stateMachine: LJStateMachine;
+    let stateMachine: LJStateMachine | undefined;
+    let diagnosticStateMachine: LJStateMachine | undefined;
     let context: LJContext;
     let errorAtCursor: RefinementMismatchError;
     let selectedTab: NavTab = 'diagnostics';
@@ -131,6 +132,24 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             return;
         }
 
+        const diagnosticStateMachineButton = target.closest?.('.diagnostic-state-machine-btn');
+        if (diagnosticStateMachineButton) {
+            e.preventDefault();
+            e.stopPropagation();
+
+            const errorIndex = parseInt(diagnosticStateMachineButton.getAttribute('data-error-index') || '-1', 10);
+            const diagnostic = getDisplayDiagnostics(diagnostics ?? [], showAllDiagnostics, currentFile)
+                .filter(d => d.category === 'error')[errorIndex];
+            if (diagnostic?.type !== 'state-refinement-error' || !diagnostic.stateMachine) return;
+
+            selectedTab = 'fsm';
+            diagnosticStateMachine = diagnostic.stateMachine;
+            showDiagramConditions = false;
+            currentDiagram = '';
+            updateView();
+            return;
+        }
+
         // VC implication simplification step buttons
         const vcImplicationStepButton = target.closest?.('.vc-step-btn');
         if (vcImplicationStepButton) {
@@ -237,6 +256,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             const tab = target.getAttribute('data-tab') as NavTab;
             if (tab && tab !== selectedTab) {
                 vscode.postMessage({ type: 'highlight', range: null });
+                if (tab === 'fsm') diagnosticStateMachine = undefined;
                 selectedTab = tab;
                 updateView();
             }
@@ -309,11 +329,15 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             case 'file':
                 currentFile = msg.file;
                 if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView();
+                diagnosticStateMachine = undefined;
+                stateMachine = undefined;
+                currentDiagram = '';
+                if (selectedTab === 'fsm') updateView();
                 break;
             case 'fsm':
-                stateMachine = msg.sm as LJStateMachine;
+                stateMachine = (msg.sm as LJStateMachine | null) ?? undefined;
                 showDiagramConditions = false;
-                if (selectedTab === 'fsm') updateView();
+                if (selectedTab === 'fsm' && !diagnosticStateMachine) updateView();
                 break;
             case 'context':
                 context = msg.context as LJContext;
@@ -348,10 +372,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
                     : renderLoading();
                 break;
             case 'fsm': {
-                const diagram = createMermaidDiagram(stateMachine, diagramOrientation, showDiagramConditions);
+                const displayedStateMachine = diagnosticStateMachine ?? stateMachine;
+                const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions);
                 currentDiagram = diagram;
-                renderStateMachineView(root, stateMachine, diagram, diagramOrientation, showDiagramConditions);
-                if (stateMachine) renderMermaidDiagram(document, window);
+                renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions);
+                if (displayedStateMachine) renderMermaidDiagram(document, window);
                 break;
             }
             case 'context':

diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
@@ -176,10 +176,16 @@ export function getStyles(): string {
             line-height: 1;
             pointer-events: none;
         }
-        .copy-diagnostic-btn,
-        .diagnostic-context-btn {
+        .diagnostic-actions {
             position: absolute;
             top: 0.5rem;
+            right: 0.5rem;
+            display: flex;
+            gap: 0.25rem;
+        }
+        .copy-diagnostic-btn,
+        .diagnostic-context-btn,
+        .diagnostic-state-machine-btn {
             display: inline-flex;
             align-items: center;
             justify-content: center;
@@ -193,20 +199,16 @@ export function getStyles(): string {
             opacity: 0.65;
             transition: background-color 0.16s ease, border-color 0.16s ease, opacity 0.16s ease, transform 0.16s ease;
         }
-        .copy-diagnostic-btn {
-            right: 0.5rem;
-        }
-        .diagnostic-context-btn {
-            right: 2.5rem;
-        }
         .copy-diagnostic-btn:hover,
-        .diagnostic-context-btn:hover {
+        .diagnostic-context-btn:hover,
+        .diagnostic-state-machine-btn:hover {
             background: var(--vscode-editor-background);
             border-color: var(--vscode-widget-border);
             opacity: 1;
         }
         .copy-diagnostic-btn:disabled,
-        .diagnostic-context-btn:disabled {
+        .diagnostic-context-btn:disabled,
+        .diagnostic-state-machine-btn:disabled {
             opacity: 0.8;
             cursor: default;
         }

diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts
@@ -71,7 +71,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics:
 }
 
 export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string {
-    const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file']);
+    const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'stateMachine']);
     const lines: string[] = [];
 
     Object.entries(diagnostic).forEach(([key, value]) => {

diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
@@ -1,4 +1,4 @@
-import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections";
+import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton } from "../sections";
 import { renderCounterexample } from "./counterexample";
 import { renderVCImplication } from "./vc-implications";
 import type {
@@ -21,8 +21,11 @@ export function renderErrors(errors: LJError[]): string {
             ${errors.map((error, index) => {
                 return /*html*/`
                 <li class="diagnostic-item error-item" ${renderDiagnosticDataAttributes(error)}>
-                    ${renderDiagnosticContextAction(error)}
-                    ${renderCopyDiagnosticButton('error', index)}
+                    <div class="diagnostic-actions">
+                        ${renderDiagnosticStateMachineAction(error, index)}
+                        ${renderDiagnosticContextAction(error)}
+                        ${renderCopyDiagnosticButton('error', index)}
+                    </div>
                     ${renderError(error)}
                 </li>
             `;
@@ -74,3 +77,8 @@ function renderDiagnosticContextAction(error: LJError): string {
     if (error.type !== 'refinement-error' && error.type !== 'state-refinement-error') return "";
     return renderDiagnosticContextButton(error.position);
 }
+
+function renderDiagnosticStateMachineAction(error: LJError, index: number): string {
+    if (error.type !== 'state-refinement-error' || !error.stateMachine) return "";
+    return renderDiagnosticStateMachineButton(index);
+}
diff --git a/client/src/webview/views/diagnostics/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts
@@ -7,7 +7,9 @@ export function renderWarnings(warnings: LJWarning[]): string {
         <ul>
                 ${warnings.map((warning, index) => /*html*/`
                 <li class="diagnostic-item warning-item" ${renderDiagnosticDataAttributes(warning)}>
-                    ${renderCopyDiagnosticButton('warning', index)}
+                    <div class="diagnostic-actions">
+                        ${renderCopyDiagnosticButton('warning', index)}
+                    </div>
                     ${renderWarning(warning)}
                 </li>
             `).join("")}

diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts
@@ -37,8 +37,18 @@ export function renderDiagnosticDataAttributes(diagnostic: LJDiagnostic): string
 }
 
 export const renderLocation = (diagnostic: LJDiagnostic): string => {
-    if (!diagnostic.position || !diagnostic.file) return "";
-    return renderCustomSection("Location", /*html*/`<pre>${renderLocationLink(diagnostic.position)}</pre>`);
+    const positions: SourcePosition[] = [];
+    if (diagnostic.position && diagnostic.file) positions.push(diagnostic.position);
+
+    const declarationPosition = diagnostic.type === 'refinement-error' || diagnostic.type === 'state-refinement-error'
+        ? diagnostic.declarationPosition
+        : null;
+    if (declarationPosition?.file) positions.push(declarationPosition);
+
+    if (positions.length === 0) return "";
+    const title = positions.length === 1 ? "Location" : "Locations";
+    const links = positions.map(renderLocationLink).join("\n");
+    return renderCustomSection(title, /*html*/`<pre>${links}</pre>`);
 };
 
 export function renderVariableHighlightButton(variable: LJVariable): string {
@@ -69,6 +79,14 @@ export function renderDiagnosticContextButton(position?: SourcePosition | null):
     });
 }
 
+export function renderDiagnosticStateMachineButton(errorIndex: number): string {
+    return renderCodiconButton("type-hierarchy", {
+        className: "diagnostic-state-machine-btn",
+        title: "View state machine",
+        attributes: `data-error-index="${errorIndex}"`,
+    });
+}
+
 export function renderDiagnosticRevealButton(position: SourcePosition, content: string): string {
     if (!position.file) return `<code>${content}</code>`
     return /*html*/`

diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java
@@ -1,5 +1,6 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
 import liquidjava.diagnostics.errors.RefinementError;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
@@ -13,13 +14,15 @@ public class RefinementErrorDTO extends LJErrorDTO {
     public final VCSimplificationResultDTO found;
     public final String customMessage;
     public final String counterexample;
+    public final SourcePositionDTO declarationPosition;
 
     public RefinementErrorDTO(RefinementError error) {
         super("refinement-error", error);
         this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
         this.found = VCSimplificationResultDTO.from(error.getFound());
         this.customMessage = error.getCustomMessage();
         this.counterexample = error.getCounterExampleString();
+        this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
     }
 
     public static RefinementErrorDTO from(RefinementError error) {

diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
@@ -1,6 +1,11 @@
 package dtos.errors;
 
+import java.io.File;
+
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
+import fsm.StateMachine;
+import fsm.StateMachineParser;
 import liquidjava.diagnostics.errors.StateRefinementError;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 
@@ -12,12 +17,17 @@ public class StateRefinementErrorDTO extends LJErrorDTO {
     public final String expected;
     public final VCSimplificationResultDTO found;
     public final String customMessage;
+    public final SourcePositionDTO declarationPosition;
+    public final StateMachine stateMachine;
 
     public StateRefinementErrorDTO(StateRefinementError error) {
         super("state-refinement-error", error);
         this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
         this.found = VCSimplificationResultDTO.from(error.getFoundSimplification());
         this.customMessage = error.getCustomMessage();
+        this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
+        this.stateMachine = declarationPosition == null || declarationPosition.file() == null ? null
+                : StateMachineParser.parse(new File(declarationPosition.file()).toURI().toString());
     }
 
     public static StateRefinementErrorDTO from(StateRefinementError error) {