Show the verifier's states of a state error on the state machine

client/src/types/fsm.ts

@@ -8,13 +8,16 @@ export type LJStateMachine = {
     errorContext: LJStateMachineErrorContext | null;
 };
 
+// The verifier's states of a rejected call, on the diagram's states
 export type LJStateMachineErrorContext = {
-    calledMethod: string | null;
-    actualStates: string[];
-    receiver?: string | null;
-    expectedStates?: string[];
-    expectedCondition?: string | null;
-    foundCondition?: string | null;
-    definiteFoundState?: string | null;
-    possibleStates?: string[];
+    calledMethod: string;
+    receiver: string;
+    // states the receiver may be in at the call
+    possibleStates: string[];
+    // states from which the call is accepted, empty when they depend on more than the receiver's state
+    acceptedStates: string[];
+    // possible states from which the call is accepted
+    validStates: string[];
+    // possible states from which the call is rejected
+    invalidStates: string[];
 };

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

@@ -17,11 +17,11 @@ function treeNode(errorContext: Partial<LJStateMachineErrorContext> | null = {})
         ],
         errorContext: errorContext && {
             calledMethod: 'getFirstChild',
-            actualStates: ['childrenAllowed'],
             receiver: 'root',
-            expectedStates: ['maybeHasChildren'],
-            definiteFoundState: 'childrenAllowed',
             possibleStates: ['childrenAllowed'],
+            acceptedStates: ['maybeHasChildren'],
+            validStates: [],
+            invalidStates: ['childrenAllowed'],
             ...errorContext,
         },
     };
@@ -47,13 +47,11 @@ function datagramSocket(errorContext: Partial<LJStateMachineErrorContext> = {}):
         ],
         errorContext: {
             calledMethod: 'receive',
-            actualStates: ['bound', 'closed'],
             receiver: 'socket',
-            expectedStates: open,
-            expectedCondition: 'unbound(socket) || bound(socket) || connected(socket)',
-            foundCondition: 'flag ? closed(socket) : bound(socket)',
-            definiteFoundState: null,
             possibleStates: ['bound', 'closed'],
+            acceptedStates: open,
+            validStates: ['bound'],
+            invalidStates: ['closed'],
             ...errorContext,
         },
     };
@@ -84,16 +82,6 @@ describe('state error focus', () => {
         expect(getRelatedStates(getStateErrorFocus(datagramSocket())!)).toEqual(['bound', 'closed', 'unbound', 'connected']);
     });
 
-    it.each([
-        ['the definite found state', { possibleStates: undefined, definiteFoundState: 'closed' }, [], ['closed']],
-        ['the found states', { possibleStates: undefined, definiteFoundState: null }, ['bound'], ['closed']],
-    ])('falls back to %s without possible states', (_, errorContext, validStates, invalidStates) => {
-        const focus = getStateErrorFocus(datagramSocket(errorContext));
-
-        expect(focus?.validStates).toEqual(validStates);
-        expect(focus?.invalidStates).toEqual(invalidStates);
-    });
-
     it('marks valid and invalid states and colours every edge of the called method', () => {
         for (const focusOnError of [true, false]) {
             const diagram = lines(createMermaidDiagram(datagramSocket(), 'TB', false, focusOnError));
@@ -174,25 +162,21 @@ describe('state error focus', () => {
             .toContain(`bound --> bound : ${calledMethod('receive')}<br/>${dimmedMethod('send')}<br/>${dimmedMethod('receiveAll')}`);
     });
 
-    it.each([
-        ['no accepted states', { expectedStates: [], possibleStates: [] }],
-        ['accepted states outside the machine', { expectedStates: ['listening'] }],
-    ])('does not focus with %s', (_, errorContext) => {
-        const sm = datagramSocket(errorContext);
+    it('does not focus without accepted states', () => {
+        const sm = datagramSocket({ acceptedStates: [], validStates: [], invalidStates: [] });
 
         expect(getStateErrorFocus(sm)).toBeNull();
         const diagram = createMermaidDiagram(sm, 'TB', false, true);
         expect(diagram).not.toMatch(/ljStateDimmed|lj-dimmed-transitions|ljStateValid|ljStateInvalid/);
         expect(diagram).toContain('class bound,closed ljStateErrorActual');
     });
 
-    it('ignores possible states outside the machine and falls back when none are given', () => {
-        expect(getStateErrorFocus(datagramSocket({ possibleStates: ['closed', 'listening'] }))?.possibleStates).toEqual(['closed']);
-        expect(getStateErrorFocus(datagramSocket({ possibleStates: [] }))?.possibleStates).toEqual(['bound', 'closed']);
-    });
-
     it('only hints at the accepted states when the state of the receiver is unknown', () => {
-        const sm = datagramSocket({ possibleStates: ['unbound', 'bound', 'connected', 'closed', 'broken'], foundCondition: 'true' });
+        const sm = datagramSocket({
+            possibleStates: ['unbound', 'bound', 'connected', 'closed', 'broken'],
+            validStates: ['unbound', 'bound', 'connected'],
+            invalidStates: ['closed', 'broken'],
+        });
 
         const focus = getStateErrorFocus(sm);
         expect(focus).toMatchObject({ unknownState: true, validStates: [], invalidStates: [] });
@@ -220,9 +204,8 @@ describe('state error focus', () => {
         expect(dimmedTransitions(diagram.join('\n'))).toEqual(['%% lj-dimmed-transitions: edge0 edge2']);
     });
 
-    it('keeps the previous highlighting for an error context without the accepted states', () => {
-        const sm = treeNode();
-        sm.errorContext = { calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'] };
+    it('only highlights the possible states when the accepted states are unknown', () => {
+        const sm = treeNode({ acceptedStates: [], validStates: [], invalidStates: [] });
 
         expect(getStateErrorFocus(sm)).toBeNull();
         const diagram = createMermaidDiagram(sm, 'TB', false, true);

client/src/webview/diagram-focus.ts

@@ -28,23 +28,17 @@ export type StateErrorFocus = {
  */
 export function getStateErrorFocus(sm: LJStateMachine | undefined): StateErrorFocus | null {
     const context = sm?.errorContext;
-    const acceptedStates = sm?.states.filter(state => context?.expectedStates?.includes(state)) ?? [];
-    if (!sm || !context || acceptedStates.length === 0) return null;
+    if (!sm || !context || context.acceptedStates.length === 0) return null;
 
-    const possible = context.possibleStates?.length
-        ? context.possibleStates
-        : context.definiteFoundState ? [context.definiteFoundState] : context.actualStates;
-    const possibleStates = sm.states.filter(state => possible.includes(state));
     // marking every state as valid or invalid would only say that the state is unknown
-    const unknownState = possibleStates.length === sm.states.length;
-    const markedStates = unknownState ? [] : possibleStates;
+    const unknownState = context.possibleStates.length === sm.states.length;
     return {
         calledMethod: context.calledMethod,
-        receiver: context.receiver ?? null,
-        possibleStates,
-        validStates: markedStates.filter(state => acceptedStates.includes(state)),
-        invalidStates: markedStates.filter(state => !acceptedStates.includes(state)),
-        acceptedStates,
+        receiver: context.receiver,
+        possibleStates: context.possibleStates,
+        validStates: unknownState ? [] : context.validStates,
+        invalidStates: unknownState ? [] : context.invalidStates,
+        acceptedStates: context.acceptedStates,
         unknownState,
     };
 }

client/src/webview/diagram.ts

@@ -87,7 +87,7 @@ export function createMermaidDiagram(
     });
 
     if (!errorFocus) {
-        const highlightedStates = sm.states.filter(state => sm.errorContext?.actualStates.includes(state));
+        const highlightedStates = sm.errorContext?.possibleStates ?? [];
         if (highlightedStates.length > 0) {
             lines.push(`    class ${highlightedStates.join(',')} ljStateErrorActual`);
         }

client/src/webview/script.spec.ts

@@ -75,8 +75,8 @@ function errorMachine(className: string, calledMethod: string): LJStateMachine {
         transitions: [...stateMachine.transitions, { from: 'Broken', to: 'Broken', label: 'reopen()' }],
         initialTransitions: [{ to: 'Open' }, { to: 'Broken' }],
         errorContext: {
-            calledMethod, actualStates: ['Closed'], receiver: 'counter', expectedStates: ['Open'],
-            expectedCondition: 'Open(counter)', foundCondition: 'Closed(counter)', definiteFoundState: 'Closed',
+            calledMethod, receiver: 'counter', possibleStates: ['Closed'], acceptedStates: ['Open'],
+            validStates: [], invalidStates: ['Closed'],
         },
     };
 }

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

@@ -1,5 +1,5 @@
 import { afterEach, describe, expect, it, vi } from 'vitest';
-import type { LJStateMachine } from '../../../types/fsm';
+import type { LJStateMachine, LJStateMachineErrorContext } from '../../../types/fsm';
 import { renderStateMachineView } from './fsm';
 
 const diagram = 'stateDiagram-v2\n[*] --> Closed\nClosed --> Open: open';
@@ -13,6 +13,16 @@ function machine(overrides: Partial<LJStateMachine> = {}): LJStateMachine {
     };
 }
 
+// socket.receive(), allowed while the socket is open, as the server reports it for the given possible states
+function socketError(possibleStates: string[]): LJStateMachineErrorContext {
+    const acceptedStates = ['unbound', 'bound', 'connected'];
+    return {
+        calledMethod: 'receive', receiver: 'socket', possibleStates, acceptedStates,
+        validStates: possibleStates.filter(state => acceptedStates.includes(state)),
+        invalidStates: possibleStates.filter(state => !acceptedStates.includes(state)),
+    };
+}
+
 function button(id: string): HTMLButtonElement {
     return document.querySelector<HTMLButtonElement>(`#${id}`)!;
 }
@@ -112,10 +122,7 @@ describe('state machine view', () => {
     it('summarizes where the call is rejected and allowed in one line', () => {
         const errorMachine = machine({
             states: ['unbound', 'bound', 'connected', 'closed'],
-            errorContext: {
-                calledMethod: 'receive', actualStates: ['bound', 'closed'], receiver: 'socket',
-                expectedStates: ['unbound', 'bound', 'connected'], possibleStates: ['bound', 'closed'],
-            },
+            errorContext: socketError(['bound', 'closed']),
         });
         renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true);
 
@@ -132,8 +139,8 @@ describe('state machine view', () => {
         renderStateMachineView(document.body, machine({
             states: ['childrenAllowed', 'maybeHasChildren'],
             errorContext: {
-                calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'], receiver: 'root',
-                expectedStates: ['maybeHasChildren'], definiteFoundState: 'childrenAllowed',
+                calledMethod: 'getFirstChild', receiver: 'root', possibleStates: ['childrenAllowed'],
+                acceptedStates: ['maybeHasChildren'], validStates: [], invalidStates: ['childrenAllowed'],
             },
         }), diagram, 'TB', false, true);
 
@@ -143,21 +150,18 @@ describe('state machine view', () => {
     it.each([
         [
             'the state of the receiver is unknown',
-            { possibleStates: ['unbound', 'bound', 'connected', 'closed'] },
+            ['unbound', 'bound', 'connected', 'closed'],
             'socket.receive() is rejected: the state of socket is unknown here \u00B7 allowed in state unbound or bound or connected',
         ],
         [
             'every possible state accepts the call',
-            { possibleStates: ['bound'] },
+            ['bound'],
             'socket.receive() is rejected here \u00B7 allowed in state bound',
         ],
-    ])('summarizes the error when %s', (_, errorContext, summary) => {
+    ])('summarizes the error when %s', (_, possibleStates, summary) => {
         renderStateMachineView(document.body, machine({
             states: ['unbound', 'bound', 'connected', 'closed'],
-            errorContext: {
-                calledMethod: 'receive', actualStates: [], receiver: 'socket',
-                expectedStates: ['unbound', 'bound', 'connected'], ...errorContext,
-            },
+            errorContext: socketError(possibleStates),
         }), diagram, 'TB', false, true);
 
         expect(document.querySelector('.diagram-error-text')?.textContent).toBe(summary);
@@ -170,10 +174,7 @@ describe('state machine view', () => {
     ])('explains the state marks in a legend with %s', (_, possibleStates, items) => {
         renderStateMachineView(document.body, machine({
             states: ['unbound', 'bound', 'connected', 'closed'],
-            errorContext: {
-                calledMethod: 'receive', actualStates: [], receiver: 'socket',
-                expectedStates: ['unbound', 'bound', 'connected'], possibleStates,
-            },
+            errorContext: socketError(possibleStates),
         }), diagram, 'TB', false, true);
 
         const legend = document.querySelectorAll('.diagram-error-legend-item');
@@ -183,7 +184,10 @@ describe('state machine view', () => {
 
     it.each([
         ['no error', null],
-        ['an error context without the accepted states', { calledMethod: 'open', actualStates: ['Closed'] }],
+        ['an error context without the accepted states', {
+            calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'],
+            acceptedStates: [], validStates: [], invalidStates: [],
+        }],
     ])('omits the error summary with %s', (_, errorContext) => {
         renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true);
 
@@ -194,7 +198,10 @@ describe('state machine view', () => {
 
     it('clips the panned diagram below the error summary and legend', () => {
         renderStateMachineView(document.body, machine({
-            errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] },
+            errorContext: {
+                calledMethod: 'read', receiver: 'counter', possibleStates: ['Closed'],
+                acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'],
+            },
         }), diagram, 'TB', false, true);
 
         const viewport = document.querySelector('.diagram-viewport')!;

server/pom.xml

@@ -101,7 +101,7 @@
 		<maven.compiler.release>20</maven.compiler.release>
 		<!-- versions -->
 		<version.memcompiler>1.3.0</version.memcompiler>
-		<version.spoon>10.4.2</version.spoon>
+		<version.spoon>11.5.0</version.spoon>
 		<version.z3>4.8.17</version.z3>
 		<version.liquidjava>1.0</version.liquidjava>
 		<!-- plugin versions -->
@@ -167,12 +167,12 @@
 		<dependency>
 			<groupId>io.github.liquid-java</groupId>
 			<artifactId>liquidjava-verifier</artifactId>
-			<version>0.0.35</version>
+			<version>0.0.36</version>
 		</dependency>
 		<dependency>
 		  <groupId>io.github.liquid-java</groupId>
 		  <artifactId>liquidjava-fsm</artifactId>
-		  <version>0.1.5</version>
+		  <version>0.2.0</version>
 		</dependency>
 		<dependency>
 			<groupId>tools.aqua</groupId>

server/src/main/java/dtos/errors/StateRefinementErrorDTO.java

@@ -4,9 +4,10 @@
 
 import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
-import liquidjava.fsm.StateMachine;
-import liquidjava.fsm.StateMachineParser;
+import dtos.fsm.StateMachineDTO;
+import liquidjava.diagnostics.errors.StateErrorContext;
 import liquidjava.diagnostics.errors.StateRefinementError;
+import liquidjava.fsm.StateMachineParser;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 
 /**
@@ -18,20 +19,18 @@ public class StateRefinementErrorDTO extends LJErrorDTO {
     public final VCSimplificationResultDTO found;
     public final String customMessage;
     public final SourcePositionDTO declarationPosition;
-    public final StateMachine stateMachine;
+    public final StateMachineDTO stateMachine;
 
     public StateRefinementErrorDTO(StateRefinementError error) {
         super("state-refinement-error", error);
         this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
         this.found = VCSimplificationResultDTO.from(error.getFoundSimplification());
         this.customMessage = error.getCustomMessage();
         this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
+        StateErrorContext context = error.getContext();
         this.stateMachine = declarationPosition == null || declarationPosition.file() == null ? null
-                : StateMachineParser.parseWithErrorContext(
-                        new File(declarationPosition.file()).toURI().toString(),
-                        error.getDeclarationPosition(),
-                        error.getExpected() == null ? null : error.getExpected().getExpression(),
-                        error.getFound());
+                : StateMachineDTO.from(StateMachineParser.parse(new File(declarationPosition.file()).toURI().toString(),
+                        context == null ? null : context.receiverClass()), context);
     }
 
     public static StateRefinementErrorDTO from(StateRefinementError error) {

server/src/main/java/dtos/fsm/StateErrorContextDTO.java

@@ -0,0 +1,51 @@
+package dtos.fsm;
+
+import java.util.List;
+import java.util.stream.Stream;
+
+import liquidjava.diagnostics.errors.StateErrorContext;
+
+/**
+ * DTO for serializing the verifier's states of a rejected call on the diagram of its first 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
+ *
+ * @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
+ * @param possibleStates the states the receiver can be in before the call
+ * @param acceptedStates the states that allow the call, empty if they depend on more than the receiver's state,
+ *                       in which case no state is marked valid or invalid
+ * @param validStates the possible states that allow the call
+ * @param invalidStates the possible states that do not allow the call
+ */
+public record StateErrorContextDTO(
+        String calledMethod,
+        String receiver,
+        List<String> possibleStates,
+        List<String> acceptedStates,
+        List<String> validStates,
+        List<String> invalidStates) {
+
+    public static StateErrorContextDTO from(StateErrorContext context, List<String> states) {
+        if (context == null) return null;
+        String calledMethod = context.method().substring(0, context.method().indexOf('('));
+        List<List<String>> possible = context.possibleStates();
+        List<String> possibleStates = firstSet(possible, states);
+        List<List<String>> 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());
+    }
+
+    /** The states of the diagram that appear in the first state set of {@code combinations} */
+    private static List<String> firstSet(List<List<String>> combinations, List<String> states) {
+        return states.stream().filter(s -> withState(combinations, s).findAny().isPresent()).toList();
+    }
+
+    private static Stream<List<String>> withState(List<List<String>> combinations, String state) {
+        return combinations.stream().filter(c -> c.get(0).equals(state));
+    }
+}