Label a named state set's diagram with its name

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 }[];

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);
 

client/src/webview/views/fsm/fsm.ts

@@ -67,7 +67,7 @@ function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], o
                         ` : ''}
                         <div class="diagram-viewport${focusOnError && errorFocuses.length > 0 ? ' diagram-focused' : ''}">
                             <div id="diagram-wrapper" class="diagram-wrapper">
-                                ${sms.length === 1
+                                ${sms.length === 1 && !sms[0].stateSetName
                                     ? `<pre class="mermaid">${diagrams[0]}</pre>`
                                     : sms.map((sm, i) => renderStateSetDiagram(sm, diagrams[i], focusOnError && errorFocuses.length > 0)).join('')}
                             </div>
@@ -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*/`
         <div class="diagram-state-set${dimmed ? ' diagram-state-set-dimmed' : ''}">
-            <h3 class="diagram-state-set-title">${sm.states.map(state => escapeHtml(state)).join(' \u00B7 ')}</h3>
+            <h3 class="diagram-state-set-title">${escapeHtml(title)}</h3>
             <pre class="mermaid">${diagram}</pre>
         </div>
     `;

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<String> states,
         List<StateMachineTransition> transitions,
         List<StateMachineInitialTransition> 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()));
     }
 

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