From 443e6fbf4790afd06b54e74ee369c1d37ce7384c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 21:41:47 +0000 Subject: [PATCH 1/2] Send one state machine per state set from the language server A class with several @StateSet annotations, such as ImageWriteParam, now has one diagram per state set. liquidjava/fsm returns the list from liquidjava-fsm's parseAll, and a state refinement error carries stateMachines instead of stateMachine. The verifier names each state by its name in every state set, so the error context of each diagram uses that state set's names. A state is marked invalid only if no accepted state has it, so that a call like write(), which needs a state in each state set, does not blame the state set that is already right. The error is only put on the diagrams of the state sets whose transitions have the called method. Co-Authored-By: Claude Opus 5.5 --- server/pom.xml | 2 +- server/src/main/java/LJLanguageServer.java | 5 +- .../dtos/errors/StateRefinementErrorDTO.java | 8 ++- .../java/dtos/fsm/StateErrorContextDTO.java | 34 +++++++---- .../main/java/dtos/fsm/StateMachineDTO.java | 26 +++++++- .../dtos/fsm/StateErrorContextDTOTest.java | 34 ++++++++++- .../java/dtos/fsm/StateMachineDTOTest.java | 60 +++++++++++++++++++ .../java/utils/DiagnosticConverterTest.java | 2 +- 8 files changed, 145 insertions(+), 26 deletions(-) create mode 100644 server/src/test/java/dtos/fsm/StateMachineDTOTest.java diff --git a/server/pom.xml b/server/pom.xml index 102d8ba..735309d 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-fsm - 0.2.0 + 0.2.1 tools.aqua diff --git a/server/src/main/java/LJLanguageServer.java b/server/src/main/java/LJLanguageServer.java index 0c3876f..fe2b668 100644 --- a/server/src/main/java/LJLanguageServer.java +++ b/server/src/main/java/LJLanguageServer.java @@ -1,3 +1,4 @@ +import java.util.List; import java.util.concurrent.CompletableFuture; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -93,8 +94,8 @@ public void setTrace(Object params) { } @JsonRequest("liquidjava/fsm") - public CompletableFuture fsm(Uri uri) { - return CompletableFuture.supplyAsync(() -> StateMachineParser.parse(uri.uri()), stateMachineExecutor); + public CompletableFuture> fsm(Uri uri) { + return CompletableFuture.supplyAsync(() -> StateMachineParser.parseAll(uri.uri()), stateMachineExecutor); } @JsonNotification("liquidjava/verify") diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index 4862ccc..0940d97 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -1,6 +1,7 @@ package dtos.errors; import java.io.File; +import java.util.List; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.VCSimplificationResultDTO; @@ -19,7 +20,7 @@ public class StateRefinementErrorDTO extends LJErrorDTO { public final VCSimplificationResultDTO found; public final String customMessage; public final SourcePositionDTO declarationPosition; - public final StateMachineDTO stateMachine; + public final List stateMachines; public StateRefinementErrorDTO(StateRefinementError error) { super("state-refinement-error", error); @@ -28,8 +29,9 @@ public StateRefinementErrorDTO(StateRefinementError error) { this.customMessage = error.getCustomMessage(); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); StateErrorContext context = error.getContext(); - this.stateMachine = declarationPosition == null || declarationPosition.file() == null ? null - : StateMachineDTO.from(StateMachineParser.parse(new File(declarationPosition.file()).toURI().toString(), + this.stateMachines = declarationPosition == null || declarationPosition.file() == null ? List.of() + : StateMachineDTO.from(StateMachineParser.parseAll( + new File(declarationPosition.file()).toURI().toString(), context == null ? null : context.receiverClass()), context); } diff --git a/server/src/main/java/dtos/fsm/StateErrorContextDTO.java b/server/src/main/java/dtos/fsm/StateErrorContextDTO.java index ef51e3f..af6c1e8 100644 --- a/server/src/main/java/dtos/fsm/StateErrorContextDTO.java +++ b/server/src/main/java/dtos/fsm/StateErrorContextDTO.java @@ -6,9 +6,10 @@ import liquidjava.diagnostics.errors.StateErrorContext; /** - * DTO for serializing the verifier's states of a rejected call on the diagram of its first state set + * DTO for serializing the verifier's states of a rejected call on the diagram of one state set * The verifier names each state by its name in every state set, so a state of the diagram is valid only if the call - * is accepted in every possible combination with it, and invalid only if it is accepted in none + * is accepted in every possible combination with it, and invalid only if no accepted state has it, so that a state is + * not blamed for a call rejected because of another state set * * @param calledMethod the name of the called method, as in the diagram's transitions * @param receiver the receiver of the call as written in the code @@ -26,26 +27,33 @@ public record StateErrorContextDTO( List validStates, List invalidStates) { - public static StateErrorContextDTO from(StateErrorContext context, List states) { + public static StateErrorContextDTO from(StateErrorContext context, List states, int stateSet) { if (context == null) return null; - String calledMethod = context.method().substring(0, context.method().indexOf('(')); + String calledMethod = calledMethod(context); List> possible = context.possibleStates(); - List possibleStates = firstSet(possible, states); + List possibleStates = inStateSet(possible, states, stateSet); List> accepted = context.acceptedStates(); if (accepted == null) // nothing can be marked without knowing which states allow the call return new StateErrorContextDTO(calledMethod, context.receiver(), possibleStates, List.of(), List.of(), List.of()); - return new StateErrorContextDTO(calledMethod, context.receiver(), possibleStates, firstSet(accepted, states), - possibleStates.stream().filter(s -> withState(possible, s).allMatch(accepted::contains)).toList(), - possibleStates.stream().filter(s -> withState(possible, s).noneMatch(accepted::contains)).toList()); + List acceptedStates = inStateSet(accepted, states, stateSet); + return new StateErrorContextDTO(calledMethod, context.receiver(), possibleStates, acceptedStates, + possibleStates.stream() + .filter(s -> withState(possible, s, stateSet).allMatch(accepted::contains)).toList(), + possibleStates.stream().filter(s -> !acceptedStates.contains(s)).toList()); } - /** The states of the diagram that appear in the first state set of {@code combinations} */ - private static List firstSet(List> combinations, List states) { - return states.stream().filter(s -> withState(combinations, s).findAny().isPresent()).toList(); + /** The name of the called method, as in the diagram's transitions */ + public static String calledMethod(StateErrorContext context) { + return context.method().substring(0, context.method().indexOf('(')); } - private static Stream> withState(List> combinations, String state) { - return combinations.stream().filter(c -> c.get(0).equals(state)); + /** The states of the diagram that appear in the given state set of {@code combinations} */ + private static List inStateSet(List> combinations, List states, int stateSet) { + return states.stream().filter(s -> withState(combinations, s, stateSet).findAny().isPresent()).toList(); + } + + private static Stream> withState(List> combinations, String state, int stateSet) { + return combinations.stream().filter(c -> stateSet < c.size() && c.get(stateSet).equals(state)); } } diff --git a/server/src/main/java/dtos/fsm/StateMachineDTO.java b/server/src/main/java/dtos/fsm/StateMachineDTO.java index 74a3200..67a2121 100644 --- a/server/src/main/java/dtos/fsm/StateMachineDTO.java +++ b/server/src/main/java/dtos/fsm/StateMachineDTO.java @@ -8,10 +8,14 @@ import liquidjava.fsm.StateMachineTransition; /** - * DTO for serializing a state machine diagram, with the state error shown on it + * DTO for serializing the state machine diagram of one state set, with the state error shown on it + * + * @param stateSet the index of the state set among the class's StateSet annotations + * @param errorContext the state error on this diagram, or null if the call does not involve this state set */ public record StateMachineDTO( String className, + int stateSet, List states, List transitions, List initialTransitions, @@ -19,7 +23,23 @@ public record StateMachineDTO( public static StateMachineDTO from(StateMachine sm, StateErrorContext context) { if (sm == null) return null; - return new StateMachineDTO(sm.className(), sm.states(), sm.transitions(), sm.initialTransitions(), - StateErrorContextDTO.from(context, sm.states())); + return new StateMachineDTO(sm.className(), sm.stateSet(), sm.states(), sm.transitions(), + sm.initialTransitions(), StateErrorContextDTO.from(context, sm.states(), sm.stateSet())); + } + + /** + * The diagrams of every state set of a class, with the state error only on those of the state sets the called + * method changes or requires, or on all of them if the called method is in none + */ + public static List from(List sms, StateErrorContext context) { + String calledMethod = context == null ? null : StateErrorContextDTO.calledMethod(context); + boolean anyHasMethod = calledMethod != null && sms.stream().anyMatch(sm -> hasMethod(sm, calledMethod)); + return sms.stream() + .map(sm -> from(sm, !anyHasMethod || hasMethod(sm, calledMethod) ? context : null)) + .toList(); + } + + private static boolean hasMethod(StateMachine sm, String method) { + return sm.transitions().stream().anyMatch(t -> t.label().equals(method)); } } diff --git a/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java b/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java index dc0661b..01a1e1e 100644 --- a/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java +++ b/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java @@ -15,7 +15,7 @@ void marksThePossibleStatesThatAllowTheCall() { StateErrorContext context = new StateErrorContext("f", "example.File", "read(int)", List.of(List.of("closed"), List.of("open")), List.of(List.of("open")), true); assertEquals(new StateErrorContextDTO("read", "f", List.of("open", "closed"), List.of("open"), - List.of("open"), List.of("closed")), StateErrorContextDTO.from(context, List.of("open", "closed"))); + List.of("open"), List.of("closed")), StateErrorContextDTO.from(context, List.of("open", "closed"), 0)); } @Test @@ -23,17 +23,45 @@ void leavesAStateUnmarkedWhenTheCallIsAllowedInOnlySomeOfItsCombinations() { StateErrorContext context = new StateErrorContext("d", "example.Door", "open()", List.of(List.of("closed", "locked"), List.of("closed", "unlocked"), List.of("opened", "locked")), List.of(List.of("closed", "unlocked")), true); - StateErrorContextDTO dto = StateErrorContextDTO.from(context, List.of("closed", "opened")); + StateErrorContextDTO dto = StateErrorContextDTO.from(context, List.of("closed", "opened"), 0); assertEquals(List.of("closed", "opened"), dto.possibleStates()); assertEquals(List.of(), dto.validStates()); assertEquals(List.of("opened"), dto.invalidStates()); } + @Test + void marksTheStatesOfTheGivenStateSet() { + // setCompressionType is only allowed in compressionExplicit, whatever the tiling state + StateErrorContext context = new StateErrorContext("p", "javax.imageio.ImageWriteParam", + "setCompressionType(String)", List.of(List.of("tilingExplicit", "startCompression")), + List.of(List.of("startTiling", "compressionExplicit"), List.of("tilingExplicit", "compressionExplicit")), + true); + assertEquals(new StateErrorContextDTO("setCompressionType", "p", List.of("startCompression"), + List.of("compressionExplicit"), List.of(), List.of("startCompression")), + StateErrorContextDTO.from(context, List.of("startCompression", "compressionExplicit"), 1)); + } + + @Test + void doesNotBlameAStateForACallRejectedBecauseOfAnotherStateSet() { + // write needs tilingSet and compressionSet, the receiver only has the compression state right + StateErrorContext context = new StateErrorContext("p", "example.Params", "write()", + List.of(List.of("tilingExplicit", "compressionSet")), List.of(List.of("tilingSet", "compressionSet")), + true); + StateErrorContextDTO tiling = StateErrorContextDTO.from(context, List.of("tilingExplicit", "tilingSet"), 0); + assertEquals(List.of("tilingExplicit"), tiling.invalidStates()); + StateErrorContextDTO compression = StateErrorContextDTO.from(context, + List.of("compressionExplicit", "compressionSet"), 1); + assertEquals(List.of("compressionSet"), compression.possibleStates()); + assertEquals(List.of("compressionSet"), compression.acceptedStates()); + assertEquals(List.of(), compression.validStates()); + assertEquals(List.of(), compression.invalidStates()); + } + @Test void acceptedStatesThatDependOnTheArgumentsMarkNothing() { StateErrorContext context = new StateErrorContext("f", "example.File", "reopen(int)", List.of(List.of("open")), null, false); - StateErrorContextDTO dto = StateErrorContextDTO.from(context, List.of("open", "closed")); + StateErrorContextDTO dto = StateErrorContextDTO.from(context, List.of("open", "closed"), 0); assertEquals(List.of(), dto.acceptedStates()); assertEquals(List.of(), dto.validStates()); assertEquals(List.of(), dto.invalidStates()); diff --git a/server/src/test/java/dtos/fsm/StateMachineDTOTest.java b/server/src/test/java/dtos/fsm/StateMachineDTOTest.java new file mode 100644 index 0000000..3999204 --- /dev/null +++ b/server/src/test/java/dtos/fsm/StateMachineDTOTest.java @@ -0,0 +1,60 @@ +package dtos.fsm; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.diagnostics.errors.StateErrorContext; +import liquidjava.fsm.StateMachine; +import liquidjava.fsm.StateMachineInitialTransition; +import liquidjava.fsm.StateMachineTransition; + +class StateMachineDTOTest { + + private static final StateMachine TILING = new StateMachine("example.Params", 0, + List.of("startTiling", "tilingSet"), + List.of(new StateMachineTransition("startTiling", "tilingSet", "setTiling"), + new StateMachineTransition("tilingSet", "tilingSet", "write", "compressionSet(this)", null)), + List.of(new StateMachineInitialTransition("startTiling"))); + private static final StateMachine COMPRESSION = new StateMachine("example.Params", 1, + List.of("startCompression", "compressionSet"), + List.of(new StateMachineTransition("startCompression", "compressionSet", "setCompressionType"), + new StateMachineTransition("compressionSet", "compressionSet", "write", "tilingSet(this)", null)), + List.of(new StateMachineInitialTransition("startCompression"))); + + private static StateErrorContext call(String method) { + return new StateErrorContext("p", "example.Params", method, List.of(List.of("startTiling", "startCompression")), + List.of(List.of("tilingSet", "compressionSet")), true); + } + + @Test + void showsTheErrorOnlyOnTheStateSetsOfTheCalledMethod() { + List dtos = StateMachineDTO.from(List.of(TILING, COMPRESSION), call("setTiling(int)")); + assertEquals(List.of(0, 1), dtos.stream().map(StateMachineDTO::stateSet).toList()); + assertEquals(List.of("startTiling"), dtos.get(0).errorContext().invalidStates()); + assertNull(dtos.get(1).errorContext()); + } + + @Test + void showsTheErrorOnEveryStateSetTheCalledMethodRequires() { + List dtos = StateMachineDTO.from(List.of(TILING, COMPRESSION), call("write()")); + assertEquals(List.of("startTiling"), dtos.get(0).errorContext().invalidStates()); + assertEquals(List.of("startCompression"), dtos.get(1).errorContext().invalidStates()); + } + + @Test + void showsTheErrorOnEveryStateSetWhenNoneHasTheCalledMethod() { + List dtos = StateMachineDTO.from(List.of(TILING, COMPRESSION), call("close()")); + assertNotNull(dtos.get(0).errorContext()); + assertNotNull(dtos.get(1).errorContext()); + } + + @Test + void hasNoErrorWithoutAContext() { + List dtos = StateMachineDTO.from(List.of(TILING, COMPRESSION), null); + assertNull(dtos.get(0).errorContext()); + assertNull(dtos.get(1).errorContext()); + } +} diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index f7c0d2e..1732d88 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -177,7 +177,7 @@ void preservesStateRefinementDetailsWithoutDeclarationFile() { assertEquals("true", dto.found.implication().predicate()); assertEquals("expected closed", dto.customMessage); assertNull(dto.declarationPosition); - assertNull(dto.stateMachine); + assertEquals(List.of(), dto.stateMachines); } @Test From 902f4e8e96b03a586a6dd834ab82410583418136 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 21:59:34 +0000 Subject: [PATCH 2/2] 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 --- client/media/walkthrough/state-machine.md | 4 +- client/src/services/codelens.ts | 2 +- client/src/services/events.ts | 2 +- client/src/services/state-machine.ts | 8 +- client/src/services/webview.ts | 2 +- client/src/state.ts | 2 +- client/src/test/state-errors.test.ts | 10 +- client/src/types/diagnostics.ts | 3 +- client/src/types/fsm.ts | 6 +- client/src/webview/diagram-focus.spec.ts | 18 ++- client/src/webview/diagram-focus.ts | 26 +++- client/src/webview/script.spec.ts | 34 ++++- client/src/webview/script.ts | 30 ++-- client/src/webview/state-errors.spec.ts | 4 +- client/src/webview/state-errors.ts | 2 +- client/src/webview/styles.ts | 16 +++ .../webview/views/diagnostics/diagnostics.ts | 2 +- .../src/webview/views/diagnostics/errors.ts | 2 +- client/src/webview/views/fsm/fsm.spec.ts | 134 ++++++++++++++---- client/src/webview/views/fsm/fsm.ts | 90 +++++++----- 20 files changed, 289 insertions(+), 108 deletions(-) diff --git a/client/media/walkthrough/state-machine.md b/client/media/walkthrough/state-machine.md index 94bcdb9..d4d58fe 100644 --- a/client/media/walkthrough/state-machine.md +++ b/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. diff --git a/client/src/services/codelens.ts b/client/src/services/codelens.ts index ca850c5..d42b56e 100644 --- a/client/src/services/codelens.ts +++ b/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", diff --git a/client/src/services/events.ts b/client/src/services/events.ts index 4dcfeb3..6de5b62 100644 --- a/client/src/services/events.ts +++ b/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); diff --git a/client/src/services/state-machine.ts b/client/src/services/state-machine.ts index 6532025..6024841 100644 --- a/client/src/services/state-machine.ts +++ b/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("liquidjava/fsm", { uri: document.uri.toString() }); + const sms = await extension.client?.sendRequest("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 }); } diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index 1267214..e4aab45 100644 --- a/client/src/services/webview.ts +++ b/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 }); diff --git a/client/src/state.ts b/client/src/state.ts index f31dcdc..0dbab1c 100644 --- a/client/src/state.ts +++ b/client/src/state.ts @@ -27,7 +27,7 @@ export class ExtensionState { diagnostics?: LJDiagnostic[]; readonly diagnosticsEmitter = new vscode.EventEmitter(); readonly failureEmitter = new vscode.EventEmitter(); - stateMachine?: LJStateMachine | null; + stateMachines?: LJStateMachine[] | null; context?: LJContext; currentSelection?: Range; errorAtCursor?: RefinementMismatchError; diff --git a/client/src/test/state-errors.test.ts b/client/src/test/state-errors.test.ts index 0ceec2d..09da9e9 100644 --- a/client/src/test/state-errors.test.ts +++ b/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)); diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 2c03de4..36ab1c4 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -99,7 +99,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 & { diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 9b03565..9e70bb4 100644 --- a/client/src/types/fsm.ts +++ b/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 diff --git a/client/src/webview/diagram-focus.spec.ts b/client/src/webview/diagram-focus.spec.ts index 7fd41a1..8145072 100644 --- a/client/src/webview/diagram-focus.spec.ts +++ b/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([]); + }); +}); diff --git a/client/src/webview/diagram-focus.ts b/client/src/webview/diagram-focus.ts index b0c1a5f..624ce45 100644 --- a/client/src/webview/diagram-focus.ts +++ b/client/src/webview/diagram-focus.ts @@ -54,10 +54,28 @@ export function getRelatedStates(focus: StateErrorFocus): string[] { /** * Gets the text shown for the rejected call, e.g. root.getFirstChild() - * @param focus + * @param call the called method and receiver of the state error * @returns the call text, or null when the called method is unknown */ -export function getRejectedCallText(focus: StateErrorFocus): string | null { - if (!focus.calledMethod) return null; - return `${focus.receiver ? `${focus.receiver}.` : ''}${focus.calledMethod}()`; +export function getRejectedCallText(call: Pick): string | null { + if (!call.calledMethod) return null; + return `${call.receiver ? `${call.receiver}.` : ''}${call.calledMethod}()`; +} + +/** + * Orders the state machines of a class so that those of the state sets with the state error come first + * @param sms the state machines, one per state set, in declaration order + * @returns the state machines with the state error, then the others, each in declaration order + */ +export function orderStateMachines(sms: LJStateMachine[]): LJStateMachine[] { + return [...sms.filter(sm => sm.errorContext), ...sms.filter(sm => !sm.errorContext)]; +} + +/** + * Gets the state error to focus on in each state machine that has one + * @param sms the state machines, one per state set + * @returns the state error focus of each state set with the error + */ +export function getStateErrorFocuses(sms: LJStateMachine[]): StateErrorFocus[] { + return sms.map(getStateErrorFocus).filter((focus): focus is StateErrorFocus => !!focus); } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index c7c1219..45c428e 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -63,7 +63,7 @@ function stateError(title: string, sm: LJStateMachine, line = position.lineStart title, message: `${title} message`, hints: [], file, position: errorPosition, category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)', found: { implication: null as never, origin: null, simplification: 'Closed(counter)' }, - customMessage: '', declarationPosition: null, stateMachine: sm, + customMessage: '', declarationPosition: null, stateMachines: [sm], }; } @@ -142,7 +142,7 @@ describe('webview script', () => { it('switches between diagnostics, context, and state machine tabs', async () => { showDiagnostics([diagnostic(currentFile, 'Current error')]); receive({ type: 'context', context: context() }); - receive({ type: 'fsm', sm: stateMachine }); + receive({ type: 'fsm', sms: [stateMachine] }); postMessage.mockClear(); click('[data-tab="context"]'); @@ -194,7 +194,7 @@ describe('webview script', () => { // the tab keeps the error after visiting another tab click('[data-tab="diagnostics"]'); - receive({ type: 'fsm', sm: stateMachine }); + receive({ type: 'fsm', sms: [stateMachine] }); click('[data-tab="fsm"]'); expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all'); expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed'); @@ -216,11 +216,35 @@ describe('webview script', () => { await vi.waitFor(() => expect(transform()).toBe('matrix(1, 0, 0, 1, 0, 0)')); }); + it('shows the diagram of the state set with the error first and copies every diagram', async () => { + const writeText = vi.fn().mockResolvedValue(undefined); + vi.stubGlobal('navigator', { clipboard: { writeText } }); + const other: LJStateMachine = { + ...stateMachine, className: 'Counter', stateSet: 0, states: ['Idle', 'Busy'], + transitions: [{ from: 'Idle', to: 'Busy', label: 'start()' }], + }; + const withError = { ...errorMachine('Counter', 'close'), stateSet: 1 }; + showDiagnostics([{ ...stateError('State refinement error', withError), stateMachines: [other, withError] } as LJDiagnostic]); + click('.diagnostic-state-machine-btn'); + + await vi.waitFor(() => expect(runMermaid).toHaveBeenCalledTimes(1)); + expect(runMermaid.mock.calls[0][0].nodes).toHaveLength(2); + expect(Array.from(root.querySelectorAll('.diagram-state-set-title'), node => node.textContent)) + .toEqual(['Open \u00B7 Closed \u00B7 Broken', 'Idle \u00B7 Busy']); + expect(root.querySelector('.diagram-state-set:last-child')?.classList.contains('diagram-state-set-dimmed')).toBe(true); + + click('#copy-diagram-btn'); + const copied: string = writeText.mock.calls[0][0]; + expect(copied.match(/stateDiagram-v2/g)).toHaveLength(2); + expect(copied).toContain('Idle --> Busy'); + expect(copied).not.toMatch(/ljState|lj-dimmed|lj-state-error-method/); + }); + it('copies the Mermaid source without the error overlay', async () => { const writeText = vi.fn().mockResolvedValue(undefined); vi.stubGlobal('navigator', { clipboard: { writeText } }); showDiagnostics([]); - receive({ type: 'fsm', sm: { ...errorMachine('Counter', 'close'), errorContext: null } }); + receive({ type: 'fsm', sms: [{ ...errorMachine('Counter', 'close'), errorContext: null }] }); click('[data-tab="fsm"]'); click('#copy-diagram-btn'); const plain = writeText.mock.calls[0][0]; @@ -296,7 +320,7 @@ describe('webview script', () => { stateError('Second state error', errorMachine('Second', 'reset'), 9), stateError('First state error', errorMachine('First', 'close'), 4), ]); - receive({ type: 'fsm', sm: stateMachine }); + receive({ type: 'fsm', sms: [stateMachine] }); click('[data-tab="fsm"]'); expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index cc44922..843dd1a 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -2,6 +2,7 @@ import { handleVCImplicationStepClick } from "./views/diagnostics/vc-implication import { renderLoading } from "./views/loading"; import { renderStopped } from "./views/stopped"; import { renderStateMachineView } from "./views/fsm/fsm"; +import { orderStateMachines } from "./diagram-focus"; import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram"; import type { LJDiagnostic, RefinementMismatchError, StateRefinementError } from "../types/diagnostics"; import type { Range } from "../types/context"; @@ -31,7 +32,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let diagnostics: LJDiagnostic[] | undefined; let showAllDiagnostics = false; let currentFile: string; - let stateMachine: LJStateMachine | undefined; + let stateMachines: LJStateMachine[] = []; // the last state error shown, kept while switching tabs let selectedStateError: StateRefinementError | undefined; let cursorStateErrorKey: string | undefined; @@ -152,7 +153,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) 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; + if (diagnostic?.type !== 'state-refinement-error' || diagnostic.stateMachines.length === 0) return; showStateError(diagnostic); return; } @@ -381,11 +382,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) // the view shows the first error of the new file instead if (selectedStateError && selectedStateError.file.toLowerCase() !== currentFile?.toLowerCase()) selectedStateError = undefined; if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView(); - stateMachine = undefined; + stateMachines = []; if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); break; case 'fsm': - stateMachine = (msg.sm as LJStateMachine | null) ?? undefined; + stateMachines = (msg.sms as LJStateMachine[] | null) ?? []; if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); break; case 'context': @@ -429,17 +430,18 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) break; case 'fsm': { const { error: shownError, index: shownIndex } = getShownStateError(stateErrors); - const displayedStateMachine = shownError?.stateMachine ?? stateMachine; + const displayedStateMachines = orderStateMachines(shownError?.stateMachines ?? stateMachines); const focusOnError = focusDiagramOnError && !!shownError; - const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions, focusOnError); - // copy the diagram without the error overlay - currentDiagram = displayedStateMachine?.errorContext - ? createMermaidDiagram({ ...displayedStateMachine, errorContext: null }, diagramOrientation, showDiagramConditions) - : diagram; - renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError, + const diagrams = displayedStateMachines.map(sm => + createMermaidDiagram(sm, diagramOrientation, showDiagramConditions, focusOnError)); + // copy the diagrams without the error overlay + currentDiagram = displayedStateMachines + .map(sm => createMermaidDiagram({ ...sm, errorContext: null }, diagramOrientation, showDiagramConditions)) + .join('\n\n'); + renderStateMachineView(root, displayedStateMachines, diagrams, diagramOrientation, showDiagramConditions, focusOnError, { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }); renderedStateMachineView = getStateMachineViewKey(); - if (displayedStateMachine) renderMermaidDiagram(document, window); + if (displayedStateMachines.length > 0) renderMermaidDiagram(document, window); break; } case 'context': @@ -485,7 +487,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) // shows the state error at the cursor once the cursor reaches it, without overriding later choices in the view function followCursorStateError(error: LJDiagnostic | undefined) { - const stateError = error?.type === 'state-refinement-error' && error.stateMachine ? error : undefined; + const stateError = error?.type === 'state-refinement-error' && error.stateMachines.length > 0 ? error : undefined; const key = stateError ? getStateErrorKey(stateError) : undefined; if (key === cursorStateErrorKey) return; cursorStateErrorKey = key; @@ -509,7 +511,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) function getStateMachineViewKey(): string { const stateErrors = getCurrentStateErrors(); const { error: shownError } = getShownStateError(stateErrors); - return JSON.stringify([shownError?.stateMachine ?? stateMachine ?? null, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]); + return JSON.stringify([shownError?.stateMachines ?? stateMachines, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]); } function revealDiagnostic(target: DiagnosticRevealTarget) { diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index b93de4a..93ee165 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -26,7 +26,7 @@ function stateError(line: number, overrides: Partial = {}) found: { implication: null as never, origin: null, simplification: null }, customMessage: '', declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }, - stateMachine: machine(), + stateMachines: [machine()], ...overrides, }; } @@ -34,7 +34,7 @@ function stateError(line: number, overrides: Partial = {}) describe('state errors', () => { it('keeps only the state errors that carry a state machine', () => { const withMachine = stateError(10); - const withoutMachine = stateError(14, { stateMachine: null }); + const withoutMachine = stateError(14, { stateMachines: [] }); const refinementError = { ...stateError(16), type: 'custom-error' } as unknown as LJDiagnostic; expect(getAllStateErrors([withMachine, withoutMachine, refinementError])).toEqual([withMachine]); diff --git a/client/src/webview/state-errors.ts b/client/src/webview/state-errors.ts index 52a96a8..50c47db 100644 --- a/client/src/webview/state-errors.ts +++ b/client/src/webview/state-errors.ts @@ -24,7 +24,7 @@ export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentF */ export function getAllStateErrors(diagnostics: LJDiagnostic[] | undefined): StateRefinementError[] { return (diagnostics ?? []).filter((diagnostic): diagnostic is StateRefinementError => - diagnostic.type === 'state-refinement-error' && !!diagnostic.stateMachine); + diagnostic.type === 'state-refinement-error' && diagnostic.stateMachines.length > 0); } export function getStateErrorKey(error: StateRefinementError): string { diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index be36de7..cca45c0 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -966,6 +966,22 @@ export function getStyles(): string { max-width: 100%; height: auto; } + /* the diagrams of a class with several state sets, one below the other */ + .diagram-state-set + .diagram-state-set { + margin-top: 1.5rem; + padding-top: 1rem; + border-top: 1px solid var(--vscode-panel-border); + } + .diagram-state-set-title { + margin: 0 0 0.5rem; + font-size: 0.85rem; + font-weight: 600; + text-align: center; + color: var(--vscode-descriptionForeground); + } + .diagram-state-set-dimmed { + opacity: 0.25; + } .diagram-header { position: absolute; top: 1rem; diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index d6efabb..aa15bf5 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -90,7 +90,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: } export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string { - const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'stateMachine']); + const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'stateMachines']); 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 index d79c611..0e58ed4 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -87,6 +87,6 @@ function renderDiagnosticContextAction(error: LJError): string { } function renderDiagnosticStateMachineAction(error: LJError, index: number): string { - if (error.type !== 'state-refinement-error' || !error.stateMachine) return ""; + if (error.type !== 'state-refinement-error' || error.stateMachines.length === 0) return ""; return renderDiagnosticStateMachineButton(index); } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index f28de28..aaab5c9 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -34,7 +34,7 @@ afterEach(() => { describe('state machine view', () => { it('selects State Machine and shows an empty state when no machine is available', () => { - renderStateMachineView(document.body, undefined, '', 'TB', false); + renderStateMachineView(document.body, [], [], 'TB', false); expect(document.querySelector('.nav-tab.selected')?.textContent).toBe('State Machine'); expect(document.body.textContent).toContain('No state machine available for the current file'); @@ -43,7 +43,7 @@ describe('state machine view', () => { }); it('renders the class, Mermaid source, and labeled diagram controls', () => { - renderStateMachineView(document.body, machine(), diagram, 'TB', false); + renderStateMachineView(document.body, [machine()], [diagram], 'TB', false); expect(document.querySelector('.diagram-title')?.textContent).toBe('Connection'); expect(document.querySelector('.mermaid')?.textContent).toBe(diagram); @@ -59,7 +59,7 @@ describe('state machine view', () => { it('escapes class titles while retaining their text', () => { const className = ' & Connection'; - renderStateMachineView(document.body, machine({ className }), diagram, 'TB', false); + renderStateMachineView(document.body, [machine({ className })], [diagram], 'TB', false); const title = document.querySelector('.diagram-title')!; expect(title.textContent).toBe(className); @@ -69,16 +69,16 @@ describe('state machine view', () => { it.each([ ['TB', 'arrow-down'], ['LR', 'arrow-right'], ] as const)('shows the %s orientation icon', (orientation, icon) => { - renderStateMachineView(document.body, machine(), diagram, orientation, false); + renderStateMachineView(document.body, [machine()], [diagram], orientation, false); expect(button('diagram-orientation-btn').querySelector(`.codicon-${icon}`)).not.toBeNull(); }); it('disables condition expansion when transitions have no additional conditions', () => { - renderStateMachineView(document.body, machine({ + renderStateMachineView(document.body, [machine({ initialTransitions: [{ to: 'Closed', toCondition: null }], transitions: [{ from: 'Closed', to: 'Open', label: 'open', fromCondition: '', toCondition: null }], - }), diagram, 'TB', false); + })], [diagram], 'TB', false); const toggle = button('diagram-conditions-btn'); expect(toggle.disabled).toBe(true); @@ -92,16 +92,16 @@ describe('state machine view', () => { ['method precondition', machine({ transitions: [{ from: 'Closed', to: 'Open', label: 'open', fromCondition: 'size > 0' }] })], ['method postcondition', machine({ transitions: [{ from: 'Closed', to: 'Open', label: 'open', toCondition: 'size == 1' }] })], ] as const)('enables condition expansion for an %s', (_, stateMachine) => { - renderStateMachineView(document.body, stateMachine, diagram, 'TB', false); + renderStateMachineView(document.body, [stateMachine], [diagram], 'TB', false); expect(button('diagram-conditions-btn').disabled).toBe(false); expect(button('diagram-conditions-btn').getAttribute('aria-label')).toBe('Expand Conditions'); }); it.each([false, true])('renders condition controls and legend with showConditions=%s', showConditions => { - renderStateMachineView(document.body, machine({ + renderStateMachineView(document.body, [machine({ initialTransitions: [{ to: 'Closed', toCondition: 'size == 0' }], - }), diagram, 'TB', showConditions); + })], [diagram], 'TB', showConditions); const toggle = button('diagram-conditions-btn'); const label = showConditions ? 'Collapse Conditions' : 'Expand Conditions'; @@ -124,25 +124,25 @@ describe('state machine view', () => { states: ['unbound', 'bound', 'connected', 'closed'], errorContext: socketError(['bound', 'closed']), }); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true); const summary = document.querySelector('.diagram-error-text')!; expect(summary.textContent).toBe('socket.receive() is rejected when socket is in state closed \u00B7 allowed in state bound'); expect(Array.from(summary.querySelectorAll('code'), node => node.textContent)).toEqual(['socket.receive()', 'socket', 'closed', 'bound']); expect(button('diagram-focus-btn').textContent?.trim()).toBe('Show all'); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, false); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, false); expect(button('diagram-focus-btn').textContent?.trim()).toBe('Focus on error'); }); it('omits the allowed part of the summary when no possible state accepts the call', () => { - renderStateMachineView(document.body, machine({ + renderStateMachineView(document.body, [machine({ states: ['childrenAllowed', 'maybeHasChildren'], errorContext: { calledMethod: 'getFirstChild', receiver: 'root', possibleStates: ['childrenAllowed'], acceptedStates: ['maybeHasChildren'], validStates: [], invalidStates: ['childrenAllowed'], }, - }), diagram, 'TB', false, true); + })], [diagram], 'TB', false, true); expect(document.querySelector('.diagram-error-text')?.textContent).toBe('root.getFirstChild() is rejected when root is in state childrenAllowed'); }); @@ -159,10 +159,10 @@ describe('state machine view', () => { 'socket.receive() is rejected here \u00B7 allowed in state bound', ], ])('summarizes the error when %s', (_, possibleStates, summary) => { - renderStateMachineView(document.body, machine({ + renderStateMachineView(document.body, [machine({ states: ['unbound', 'bound', 'connected', 'closed'], errorContext: socketError(possibleStates), - }), diagram, 'TB', false, true); + })], [diagram], 'TB', false, true); expect(document.querySelector('.diagram-error-text')?.textContent).toBe(summary); }); @@ -172,10 +172,10 @@ describe('state machine view', () => { ['only an invalid and other accepted states', ['closed'], ['\u2715 Call rejected', 'Allowed, but not reachable here']], ['an unknown receiver state', ['unbound', 'bound', 'connected', 'closed'], ['Allowed, but not reachable here']], ])('explains the state marks in a legend with %s', (_, possibleStates, items) => { - renderStateMachineView(document.body, machine({ + renderStateMachineView(document.body, [machine({ states: ['unbound', 'bound', 'connected', 'closed'], errorContext: socketError(possibleStates), - }), diagram, 'TB', false, true); + })], [diagram], 'TB', false, true); const legend = document.querySelectorAll('.diagram-error-legend-item'); expect(Array.from(legend, item => item.textContent)).toEqual(items); @@ -189,7 +189,7 @@ describe('state machine view', () => { acceptedStates: [], validStates: [], invalidStates: [], }], ])('omits the error summary with %s', (_, errorContext) => { - renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true); + renderStateMachineView(document.body, [machine({ errorContext })], [diagram], 'TB', false, true); expect(document.querySelector('.diagram-error-summary')).toBeNull(); expect(document.querySelector('.diagram-error-legend')).toBeNull(); @@ -203,7 +203,7 @@ describe('state machine view', () => { }, '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 }); + 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'); @@ -214,18 +214,18 @@ describe('state machine view', () => { }); 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 }); + 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({ + renderStateMachineView(document.body, [machine({ errorContext: { calledMethod: 'read', receiver: 'counter', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'], }, - }), diagram, 'TB', false, true); + })], [diagram], 'TB', false, true); const viewport = document.querySelector('.diagram-viewport')!; expect(viewport.querySelector('#diagram-wrapper .mermaid')).not.toBeNull(); @@ -235,11 +235,11 @@ describe('state machine view', () => { }); it('preserves the previous diagram container height when rerendering', () => { - renderStateMachineView(document.body, machine(), diagram, 'TB', false); + renderStateMachineView(document.body, [machine()], [diagram], 'TB', false); const previousContainer = document.querySelector('.diagram-container')!; vi.spyOn(previousContainer, 'offsetHeight', 'get').mockReturnValue(240); - renderStateMachineView(document.body, machine({ className: 'UpdatedConnection' }), diagram, 'LR', false); + renderStateMachineView(document.body, [machine({ className: 'UpdatedConnection' })], [diagram], 'LR', false); const container = document.querySelector('.diagram-container')!; expect(container).not.toBe(previousContainer); @@ -254,17 +254,17 @@ describe('state machine view', () => { const stepButtons = () => Array.from(document.querySelectorAll('.state-error-step-btn'), node => [node.getAttribute('aria-label'), node.disabled]); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 }); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true, { index: 0, count: 3 }); expect(document.querySelector('.state-error-position')?.textContent).toBe('1 of 3'); expect(stepButtons()).toEqual([['Previous state error', true], ['Next state error', false]]); expect(button('state-error-reveal-btn').textContent).toBe('View error'); expect(document.querySelector('.nav-tab.selected .nav-badge')?.textContent).toBe('3'); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 2, count: 3 }); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true, { index: 2, count: 3 }); expect(document.querySelector('.state-error-position')?.textContent).toBe('3 of 3'); expect(stepButtons()).toEqual([['Previous state error', false], ['Next state error', true]]); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 1 }); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true, { index: 0, count: 1 }); expect(document.querySelector('.state-error-stepper')).toBeNull(); expect(button('state-error-reveal-btn')).not.toBeNull(); }); @@ -273,7 +273,7 @@ describe('state machine view', () => { const errorMachine = machine({ errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, }); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: -1, count: 2 }); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true, { index: -1, count: 2 }); expect(document.querySelector('.state-error-stepper')).toBeNull(); expect(button('state-error-reveal-btn')).not.toBeNull(); @@ -284,16 +284,90 @@ describe('state machine view', () => { const errorMachine = machine({ errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, }); - renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 }); + renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true, { index: 0, count: 3 }); expect(button('diagram-focus-btn').closest('.diagram-error-legend')).not.toBeNull(); expect(document.querySelector('.diagram-error-actions #diagram-focus-btn')).toBeNull(); }); it('shows no state error badge or summary when the file has no state errors', () => { - renderStateMachineView(document.body, machine(), diagram, 'TB', false, false, { index: -1, count: 0 }); + renderStateMachineView(document.body, [machine()], [diagram], 'TB', false, false, { index: -1, count: 0 }); expect(document.querySelector('.nav-badge')).toBeNull(); expect(document.querySelector('.diagram-error-summary')).toBeNull(); }); + + describe('several state sets', () => { + // ImageWriteParam: setCompressionType() needs compressionExplicit, whatever the tiling state + const tiling = machine({ + className: 'ImageWriteParam', stateSet: 0, states: ['startTiling', 'tilingSet'], + transitions: [{ from: 'startTiling', to: 'tilingSet', label: 'setTiling' }], + }); + const compression = machine({ + className: 'ImageWriteParam', stateSet: 1, states: ['startCompression', 'compressionExplicit'], + transitions: [{ from: 'startCompression', to: 'compressionExplicit', label: 'setCompressionMode' }], + }); + const compressionError: LJStateMachineErrorContext = { + calledMethod: 'setCompressionType', receiver: 'param', possibleStates: ['startCompression'], + acceptedStates: ['compressionExplicit'], validStates: [], invalidStates: ['startCompression'], + }; + + it('renders one labelled diagram per state set under the class title', () => { + renderStateMachineView(document.body, [tiling, compression], ['tiling diagram', 'compression diagram'], 'TB', false); + + expect(document.querySelectorAll('.diagram-title')).toHaveLength(1); + expect(document.querySelector('.diagram-title')?.textContent).toBe('ImageWriteParam'); + expect(Array.from(document.querySelectorAll('.diagram-state-set-title'), node => node.textContent)) + .toEqual(['startTiling \u00B7 tilingSet', 'startCompression \u00B7 compressionExplicit']); + expect(Array.from(document.querySelectorAll('.diagram-state-set .mermaid'), node => node.textContent)) + .toEqual(['tiling diagram', 'compression diagram']); + expect(document.querySelectorAll('#diagram-wrapper')).toHaveLength(1); + }); + + it('keeps a single state set without a state set label', () => { + renderStateMachineView(document.body, [tiling], [diagram], 'TB', false); + + expect(document.querySelector('.diagram-state-set')).toBeNull(); + expect(document.querySelector('.mermaid')?.textContent).toBe(diagram); + }); + + it('dims the diagrams of the state sets the error does not involve when focusing on it', () => { + const sms = [{ ...compression, errorContext: compressionError }, tiling]; + renderStateMachineView(document.body, sms, ['compression diagram', 'tiling diagram'], 'TB', false, true); + + expect(Array.from(document.querySelectorAll('.diagram-state-set'), node => node.classList.contains('diagram-state-set-dimmed'))) + .toEqual([false, true]); + expect(document.querySelector('.diagram-error-text')?.textContent) + .toBe('param.setCompressionType() is rejected when param is in state startCompression'); + + renderStateMachineView(document.body, sms, ['compression diagram', 'tiling diagram'], 'TB', false, false); + expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull(); + }); + + it('summarizes a call that needs a state of each state set', () => { + // write() needs tilingSet and compressionExplicit, the receiver is in startTiling and compressionExplicit + const write = { calledMethod: 'write', receiver: 'param' }; + const sms = [ + { ...tiling, errorContext: { ...write, possibleStates: ['startTiling'], acceptedStates: ['tilingSet'], validStates: [], invalidStates: ['startTiling'] } }, + { ...compression, errorContext: { ...write, possibleStates: ['compressionExplicit'], acceptedStates: ['compressionExplicit'], validStates: ['compressionExplicit'], invalidStates: [] } }, + ]; + renderStateMachineView(document.body, sms, ['tiling diagram', 'compression diagram'], 'TB', false, true); + + expect(document.querySelector('.diagram-error-text')?.textContent) + .toBe('param.write() is rejected when param is in state startTiling \u00B7 allowed in state compressionExplicit'); + expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull(); + expect(Array.from(document.querySelectorAll('.diagram-error-legend-item'), node => node.textContent)) + .toEqual(['\u2715 Call rejected', '\u2713 Call allowed', 'Allowed, but not reachable here']); + }); + + it('names the call of the state set with the error when it cannot be marked', () => { + const unmarked = { ...compressionError, acceptedStates: [], invalidStates: [] }; + renderStateMachineView(document.body, [{ ...compression, errorContext: unmarked }, tiling], + ['compression diagram', 'tiling diagram'], 'TB', false, true, { index: 0, count: 1, line: 7 }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe('param.setCompressionType() is rejected here'); + // nothing is marked, so nothing is dimmed + expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull(); + }); + }); }); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 88d9c8b..992bdcd 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,5 +1,5 @@ import type { LJStateMachine } from "../../../types/fsm"; -import { INVALID_STATE_ICON, VALID_STATE_ICON, getRejectedCallText, getStateErrorFocus, type StateErrorFocus } from "../../diagram-focus"; +import { INVALID_STATE_ICON, VALID_STATE_ICON, getRejectedCallText, getStateErrorFocuses, type StateErrorFocus } from "../../diagram-focus"; import { renderCodiconButton } from "../../icons"; import { escapeHtml } from "../../utils"; import { renderMainHeader } from "../sections"; @@ -17,18 +17,23 @@ export type StateErrorNavigation = { const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 }; -export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION) { +/** + * 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) { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; const diagramHeight = previousDiagramContainer?.offsetHeight; - root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, focusOnError, stateErrors, diagramHeight); + root.innerHTML = renderStateMachineViewHtml(sms, diagrams, orientation, showConditions, focusOnError, stateErrors, diagramHeight); } -function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string { - const errorFocus = getStateErrorFocus(sm); - const hasConditionExpansions = sm - ? sm.initialTransitions.some(transition => !!transition.toCondition) - || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition) - : false; +function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string { + const className = sms[0]?.className; + const errorFocuses = getStateErrorFocuses(sms); + const hasConditionExpansions = sms.some(sm => + sm.initialTransitions.some(transition => !!transition.toCondition) + || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition)); const conditionToggleLabel = !hasConditionExpansions ? 'No additional conditions to expand' : showConditions ? 'Collapse Conditions' : 'Expand Conditions'; @@ -36,11 +41,11 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
${renderMainHeader("", 'fsm', stateErrors.count)} - ${sm ? /*html*/` + ${className !== undefined ? /*html*/`
-

${escapeHtml(sm.className)}

+

${escapeHtml(className)}

${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} @@ -50,9 +55,9 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
- ${errorFocus - ? renderStateErrorSummary(getStateErrorSummary(errorFocus), stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) - : isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sm, stateErrors), stateErrors) : ''} + ${errorFocuses.length > 0 + ? renderStateErrorSummary(getStateErrorSummary(errorFocuses), stateErrors) + renderStateErrorLegend(errorFocuses, focusOnError) + : isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sms, stateErrors), stateErrors) : ''} ${showConditions && hasConditionExpansions ? /*html*/`
Precondition @@ -61,7 +66,9 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ` : ''}
- 
${diagram}
+ ${sms.length === 1 + ? `
${diagrams[0]}
` + : sms.map((sm, i) => renderStateSetDiagram(sm, diagrams[i], focusOnError && errorFocuses.length > 0)).join('')}
@@ -71,34 +78,53 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str `; } +// the diagram of one state set, labelled with its states, and dimmed when focusing on an error of another state set +function renderStateSetDiagram(sm: LJStateMachine, diagram: string, dimUnrelated: boolean): string { + const dimmed = dimUnrelated && !sm.errorContext; + return /*html*/` +
+

${sm.states.map(state => escapeHtml(state)).join(' \u00B7 ')}

+ 
${diagram}
+
+ `; +} + function isStateErrorShown(stateErrors: StateErrorNavigation): boolean { return stateErrors.index >= 0 || stateErrors.line !== undefined; } -function getStateErrorSummary(focus: StateErrorFocus): string { +// summarises the error of every state set it involves, which is rejected when the receiver is in any invalid state +function getStateErrorSummary(focuses: StateErrorFocus[]): string { + const focus = focuses[0]; const call = getRejectedCallText(focus); const receiver = focus.receiver ? `${escapeHtml(focus.receiver)}` : 'the receiver'; const rejected = `${call ? `${escapeHtml(call)}` : 'The call'} is rejected`; - const allowedStates = focus.unknownState ? focus.acceptedStates : focus.validStates; + const invalidStates = focuses.flatMap(focus => focus.invalidStates); + const allowedStates = focuses + .map(focus => focus.unknownState ? focus.acceptedStates : focus.validStates) + .filter(states => states.length > 0); let summary: string; - if (focus.unknownState) { + if (invalidStates.length > 0) { + summary = `${rejected} when ${receiver} is in state ${renderStates(invalidStates)}`; + } else if (focuses.every(focus => focus.unknownState)) { summary = `${rejected}: the state of ${receiver} is unknown here`; - } else if (focus.invalidStates.length > 0) { - summary = `${rejected} when ${receiver} is in state ${renderStates(focus.invalidStates)}`; } else { summary = `${rejected} here`; } - if (allowedStates.length > 0) summary += ` \u00B7 allowed in state ${renderStates(allowedStates)}`; + // the call needs an allowed state of each state set + if (allowedStates.length > 0) { + summary += ` \u00B7 allowed in state ${allowedStates + .map(states => allowedStates.length > 1 && states.length > 1 ? `(${renderStates(states)})` : renderStates(states)) + .join(' and ')}`; + } 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`; - } +// the shown error cannot be marked on the diagrams when the verifier could not tell which states allow the call +function getUnmarkedStateErrorSummary(sms: LJStateMachine[], stateErrors: StateErrorNavigation): string { + const context = sms.find(sm => sm.errorContext)?.errorContext; + const call = context ? getRejectedCallText(context) : null; + if (call) return `${escapeHtml(call)} is rejected here`; return stateErrors.line ? `The call at line ${stateErrors.line} is rejected` : 'The call is rejected'; } @@ -125,11 +151,11 @@ function renderStateErrorStepper({ index, count }: StateErrorNavigation): string } // explains the state marks with the same outlines, fills, and icons as the diagram, next to the toggle that dims the rest -function renderStateErrorLegend(focus: StateErrorFocus, focusOnError: boolean): string { +function renderStateErrorLegend(focuses: StateErrorFocus[], focusOnError: boolean): string { const items = [ - focus.invalidStates.length > 0 ? renderLegendItem('invalid', `${INVALID_STATE_ICON} Call rejected`) : '', - focus.validStates.length > 0 ? renderLegendItem('valid', `${VALID_STATE_ICON} Call allowed`) : '', - focus.acceptedStates.some(state => !focus.validStates.includes(state)) + focuses.some(focus => focus.invalidStates.length > 0) ? renderLegendItem('invalid', `${INVALID_STATE_ICON} Call rejected`) : '', + focuses.some(focus => focus.validStates.length > 0) ? renderLegendItem('valid', `${VALID_STATE_ICON} Call allowed`) : '', + focuses.some(focus => focus.acceptedStates.some(state => !focus.validStates.includes(state))) ? renderLegendItem('accepted', 'Allowed, but not reachable here') : '', ].filter(Boolean);