Show one state machine diagram per state set

The State Machine view stacks the diagram of each state set of a class,
such as the tiling and compression states of ImageWriteParam, under the
class name, each labelled with its states. A class with one state set
looks as before.

A state error is drawn on the diagrams of the state sets it involves,
which come first, and focusing on it dims the other diagrams. The
summary lists the rejected states of every state set and the allowed
states each one needs. Copy Mermaid Source copies every diagram.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

client/media/walkthrough/state-machine.md

@@ -1,4 +1,4 @@
-The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`.
+The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`. A class with several `@StateSet` annotations has one diagram per state set, one below the other.
 Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.
 Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.
-From 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.
+From a state error, choose **Show in state machine** to see the related states and call, on the diagrams of the state sets the call involves. 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.

client/src/services/codelens.ts

@@ -40,7 +40,7 @@ function createDiagnosticCodeLenses(diagnostic: LJDiagnostic, file: string): vsc
         command: "liquidjava.showView",
         arguments: [targetDiagnostic]
     })];
-    if (diagnostic.type === 'state-refinement-error' && diagnostic.stateMachine) {
+    if (diagnostic.type === 'state-refinement-error' && diagnostic.stateMachines.length > 0) {
         codeLenses.push(new vscode.CodeLens(range, {
             title: "Show in state machine",
             command: "liquidjava.showView",

client/src/services/events.ts

@@ -36,7 +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.stateMachines = undefined;
     extension.webview?.sendMessage({ type: "file", file: extension.file });
     await updateStateMachine(editor.document);
     handleContextUpdate(editor.selection);

client/src/services/state-machine.ts

@@ -4,14 +4,14 @@ import { LJStateMachine } from "../types/fsm";
 import { normalizeFilePath } from "../utils/utils";
 
 /**
- * Requests the state machine for the given document from the language server
+ * Requests the state machines for the given document from the language server, one per state set
  * @param document The text document
  */
 export async function updateStateMachine(document: vscode.TextDocument) {
     const file = normalizeFilePath(document.uri.fsPath);
-    const sm = await extension.client?.sendRequest<LJStateMachine | null>("liquidjava/fsm", { uri: document.uri.toString() });
+    const sms = await extension.client?.sendRequest<LJStateMachine[] | null>("liquidjava/fsm", { uri: document.uri.toString() });
     if (file !== extension.file) return;
 
-    extension.stateMachine = sm;
-    extension.webview?.sendMessage({ type: "fsm", sm });
+    extension.stateMachines = sms;
+    extension.webview?.sendMessage({ type: "fsm", sms });
 }

client/src/services/webview.ts

@@ -39,7 +39,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 !== undefined) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine });
+                if (extension.stateMachines !== undefined) extension.webview?.sendMessage({ type: "fsm", sms: extension.stateMachines });
                 if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
                 if (pendingDiagnosticReveal) {
                     extension.webview?.sendMessage({ type: "revealDiagnostic", ...pendingDiagnosticReveal });

client/src/state.ts

@@ -27,7 +27,7 @@ export class ExtensionState {
     diagnostics?: LJDiagnostic[];
     readonly diagnosticsEmitter = new vscode.EventEmitter<LJDiagnostic[]>();
     readonly failureEmitter = new vscode.EventEmitter<void>();
-    stateMachine?: LJStateMachine | null;
+    stateMachines?: LJStateMachine[] | null;
     context?: LJContext;
     currentSelection?: Range;
     errorAtCursor?: RefinementMismatchError;

client/src/test/state-errors.test.ts

@@ -47,8 +47,8 @@ suite('Bundled LiquidJava state machine errors', () => {
             await ready;
 
             const machine = nextWebviewMessage('the refinements file state machine', event =>
-                event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm
-                    ? event.message.sm as LJStateMachine : undefined);
+                event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sms?.length
+                    ? (event.message.sms as LJStateMachine[])[0] : undefined);
             const stateError = nextWebviewMessage('the state error diagnostics', event =>
                 event.direction === 'toWebview' && event.message.type === 'diagnostics'
                     ? (event.message.diagnostics as LJDiagnostic[]).find(isStateError) : undefined);
@@ -58,9 +58,9 @@ suite('Bundled LiquidJava state machine errors', () => {
 
             const [sm, error] = await Promise.all([machine, stateError]);
             assert.equal(sm.className, 'javax.swing.tree.DefaultMutableTreeNode');
-            assert.ok(error.stateMachine, 'the state error must carry its state machine');
-            assert.equal(error.stateMachine.className, sm.className, 'errors are matched to the machine by class');
-            assert.ok(error.stateMachine.errorContext, 'the state error must carry its error context');
+            assert.equal(error.stateMachines.length, 1, 'the state error must carry the state machine of each state set');
+            assert.equal(error.stateMachines[0].className, sm.className, 'errors are matched to the machine by class');
+            assert.ok(error.stateMachines[0].errorContext, 'the state error must carry its error context');
             assert.ok(error.position && sameFile(error.position.file ?? error.file, callerUri));
             assert.ok(error.declarationPosition?.file && sameFile(error.declarationPosition.file, refinementsUri));
 

client/src/types/diagnostics.ts

@@ -90,7 +90,8 @@ export type StateRefinementError = BaseDiagnostic & {
     found: VCSimplificationResult;
     customMessage: string;
     declarationPosition: SourcePosition | null;
-    stateMachine: LJStateMachine | null;
+    // one state machine per state set of the receiver's class
+    stateMachines: LJStateMachine[];
 }
 
 export type ArgumentMismatchError = BaseDiagnostic & {

client/src/types/fsm.ts

@@ -1,11 +1,15 @@
 // Type definitions used for representing finite state machines
 
+// The state machine of one state set of a class
 export type LJStateMachine = {
     className: string;
+    // index of the state set among the class's @StateSet annotations, in declaration order
+    stateSet?: number;
     initialTransitions: { to: string; toCondition?: string | null; constructorSignature?: string | null }[];
     states: string[];
     transitions: { from: string; to: string; label: string; fromCondition?: string | null; toCondition?: string | null }[];
-    errorContext: LJStateMachineErrorContext | null;
+    // the state error on this state set, null if the call does not involve it
+    errorContext?: LJStateMachineErrorContext | null;
 };
 
 // The verifier's states of a rejected call, on the diagram's states

client/src/webview/diagram-focus.spec.ts

@@ -1,7 +1,7 @@
 import { afterEach, describe, expect, it, vi } from 'vitest';
 import type { LJStateMachine, LJStateMachineErrorContext } from '../types/fsm';
 import { createMermaidDiagram, renderMermaidDiagram } from './diagram';
-import { getRelatedStates, getStateErrorFocus } from './diagram-focus';
+import { getRelatedStates, getStateErrorFocus, getStateErrorFocuses, orderStateMachines } from './diagram-focus';
 
 // DefaultMutableTreeNode from the state error focus issue:
 // root.add(...); root.removeAllChildren(); root.getFirstChild(); // state error
@@ -250,3 +250,19 @@ describe('rendered state error focus', () => {
         expect(dimmed('g.label.lj-dimmed')).toEqual(['edge0', 'edge1', 'edge12']);
     });
 });
+
+describe('state errors on several state sets', () => {
+    const tiling: LJStateMachine = { ...treeNode(null), className: 'ImageWriteParam', stateSet: 0 };
+    const compression: LJStateMachine = { ...treeNode(), className: 'ImageWriteParam', stateSet: 1 };
+    const other: LJStateMachine = { ...treeNode(null), className: 'ImageWriteParam', stateSet: 2 };
+
+    it('puts the state sets with the error first, keeping the declaration order otherwise', () => {
+        expect(orderStateMachines([tiling, compression, other])).toEqual([compression, tiling, other]);
+        expect(orderStateMachines([tiling, other])).toEqual([tiling, other]);
+    });
+
+    it('focuses on the error of each state set that has it', () => {
+        expect(getStateErrorFocuses([tiling, compression, other])).toEqual([getStateErrorFocus(compression)]);
+        expect(getStateErrorFocuses([tiling, other])).toEqual([]);
+    });
+});