From 04246acf7d41018696fac64a626ba68c8a94db02 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 23:49:19 +0000 Subject: [PATCH] Label a named state set's diagram with its name The verifier's messages now show a state of a named set as a value of its set, doorState(d) == closed. liquidjava-fsm 0.2.3 reads these specs and reports each diagram's stateSetName, which the server passes on and the State Machine view uses as the diagram's title, also when the class has a single state set, so the diagram can be matched with the message. A state set without a name keeps its states as the title. Co-Authored-By: Claude Opus 5.5 --- client/src/types/fsm.ts | 2 ++ client/src/webview/views/fsm/fsm.spec.ts | 9 +++++++++ client/src/webview/views/fsm/fsm.ts | 8 +++++--- server/src/main/java/dtos/fsm/StateMachineDTO.java | 4 +++- server/src/test/java/dtos/fsm/StateMachineDTOTest.java | 8 +++++--- 5 files changed, 24 insertions(+), 7 deletions(-) diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 7087289..cf94aa5 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -5,6 +5,8 @@ export type LJStateMachine = { className: string; // index of the state set among the class's @StateSet annotations, in declaration order stateSet?: number; + // the name given to the state set, as the verifier's messages use it, e.g. phase(this) == open; null if it has none + stateSetName?: string | null; initialTransitions: { to: string; toCondition?: string | null; constructorSignature?: string | null }[]; // methods that put an object in an unknown state (a field, a parameter or a getter's result) into a state entryTransitions?: { to: string; label: string; toCondition?: string | null }[]; diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 24e186d..8ab4212 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -325,6 +325,15 @@ describe('state machine view', () => { expect(document.querySelectorAll('#diagram-wrapper')).toHaveLength(1); }); + it('labels a named state set with its name, even when it is the only one', () => { + renderStateMachineView(document.body, [{ ...tiling, stateSetName: 'tiling' }, compression], ['tiling diagram', 'compression diagram'], 'TB', false); + expect(Array.from(document.querySelectorAll('.diagram-state-set-title'), node => node.textContent)) + .toEqual(['tiling', 'startCompression \u00B7 compressionExplicit']); + + renderStateMachineView(document.body, [{ ...tiling, stateSetName: 'tiling' }], [diagram], 'TB', false); + expect(document.querySelector('.diagram-state-set-title')?.textContent).toBe('tiling'); + }); + it('keeps a single state set without a state set label', () => { renderStateMachineView(document.body, [tiling], [diagram], 'TB', false); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index bac2ae6..f70086b 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -67,7 +67,7 @@ function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], o ` : ''}
- ${sms.length === 1 + ${sms.length === 1 && !sms[0].stateSetName ? `
${diagrams[0]}
` : sms.map((sm, i) => renderStateSetDiagram(sm, diagrams[i], focusOnError && errorFocuses.length > 0)).join('')}
@@ -79,12 +79,14 @@ function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], o `; } -// the diagram of one state set, labelled with its states, and dimmed when focusing on an error of another state set +// the diagram of one state set, labelled with its name, or its states if it has none, +// 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; + const title = sm.stateSetName ?? sm.states.join(' \u00B7 '); return /*html*/`
-

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

+

${escapeHtml(title)}

${diagram}
`; diff --git a/server/src/main/java/dtos/fsm/StateMachineDTO.java b/server/src/main/java/dtos/fsm/StateMachineDTO.java index 53c42c7..05f7fc8 100644 --- a/server/src/main/java/dtos/fsm/StateMachineDTO.java +++ b/server/src/main/java/dtos/fsm/StateMachineDTO.java @@ -12,12 +12,14 @@ * 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 stateSetName the name given to the state set, or null if it has none * @param entryTransitions the methods that put an object in an unknown state into a state of this state set * @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, + String stateSetName, List states, List transitions, List initialTransitions, @@ -26,7 +28,7 @@ public record StateMachineDTO( public static StateMachineDTO from(StateMachine sm, StateErrorContext context) { if (sm == null) return null; - return new StateMachineDTO(sm.className(), sm.stateSet(), sm.states(), sm.transitions(), + return new StateMachineDTO(sm.className(), sm.stateSet(), sm.stateSetName(), sm.states(), sm.transitions(), sm.initialTransitions(), sm.entryTransitions(), StateErrorContextDTO.from(context, sm.states(), sm.stateSet())); } diff --git a/server/src/test/java/dtos/fsm/StateMachineDTOTest.java b/server/src/test/java/dtos/fsm/StateMachineDTOTest.java index 715eecf..384a05e 100644 --- a/server/src/test/java/dtos/fsm/StateMachineDTOTest.java +++ b/server/src/test/java/dtos/fsm/StateMachineDTOTest.java @@ -53,12 +53,14 @@ void showsTheErrorOnEveryStateSetWhenNoneHasTheCalledMethod() { } @Test - void keepsTheEntryTransitions() { - StateMachine sm = new StateMachine("example.Edit", 0, List.of("start", "endDone"), + void keepsTheStateSetNameAndEntryTransitions() { + StateMachine sm = new StateMachine("example.Edit", 0, "phase", List.of("start", "endDone"), List.of(new StateMachineTransition("start", "endDone", "end")), List.of(new StateMachineInitialTransition("start")), List.of(new StateMachineEntryTransition("endDone", "canUndo", "return"))); - assertEquals(sm.entryTransitions(), StateMachineDTO.from(sm, null).entryTransitions()); + StateMachineDTO dto = StateMachineDTO.from(sm, null); + assertEquals("phase", dto.stateSetName()); + assertEquals(sm.entryTransitions(), dto.entryTransitions()); } @Test