diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 2ed670a..9b03565 100644 --- a/client/src/types/fsm.ts +++ b/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[]; }; diff --git a/client/src/webview/diagram-focus.spec.ts b/client/src/webview/diagram-focus.spec.ts index 3998949..7fd41a1 100644 --- a/client/src/webview/diagram-focus.spec.ts +++ b/client/src/webview/diagram-focus.spec.ts @@ -17,11 +17,11 @@ function treeNode(errorContext: Partial | 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 = {}): ], 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,11 +162,8 @@ describe('state error focus', () => { .toContain(`bound --> bound : ${calledMethod('receive')}
${dimmedMethod('send')}
${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); @@ -186,13 +171,12 @@ describe('state error focus', () => { 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); diff --git a/client/src/webview/diagram-focus.ts b/client/src/webview/diagram-focus.ts index b2fb317..b0c1a5f 100644 --- a/client/src/webview/diagram-focus.ts +++ b/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, }; } diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index fd8c50b..2e93993 100644 --- a/client/src/webview/diagram.ts +++ b/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`); } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index d643e31..bed56cc 100644 --- a/client/src/webview/script.spec.ts +++ b/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'], }, }; } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index ad639c8..f17d6e5 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/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 { }; } +// 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(`#${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')!; diff --git a/server/pom.xml b/server/pom.xml index 7cd2cb9..102d8ba 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -101,7 +101,7 @@ 20 1.3.0 - 10.4.2 + 11.5.0 4.8.17 1.0 @@ -167,12 +167,12 @@ io.github.liquid-java liquidjava-verifier - 0.0.35 + 0.0.36 io.github.liquid-java liquidjava-fsm - 0.1.5 + 0.2.0 tools.aqua diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index a65fa27..4862ccc 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/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,7 +19,7 @@ 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); @@ -26,12 +27,10 @@ public StateRefinementErrorDTO(StateRefinementError error) { 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) { diff --git a/server/src/main/java/dtos/fsm/StateErrorContextDTO.java b/server/src/main/java/dtos/fsm/StateErrorContextDTO.java new file mode 100644 index 0000000..ef51e3f --- /dev/null +++ b/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 possibleStates, + List acceptedStates, + List validStates, + List invalidStates) { + + public static StateErrorContextDTO from(StateErrorContext context, List states) { + if (context == null) return null; + String calledMethod = context.method().substring(0, context.method().indexOf('(')); + List> possible = context.possibleStates(); + List possibleStates = firstSet(possible, states); + 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()); + } + + /** 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(); + } + + private static Stream> withState(List> combinations, String state) { + return combinations.stream().filter(c -> c.get(0).equals(state)); + } +} diff --git a/server/src/main/java/dtos/fsm/StateMachineDTO.java b/server/src/main/java/dtos/fsm/StateMachineDTO.java new file mode 100644 index 0000000..74a3200 --- /dev/null +++ b/server/src/main/java/dtos/fsm/StateMachineDTO.java @@ -0,0 +1,25 @@ +package dtos.fsm; + +import java.util.List; + +import liquidjava.diagnostics.errors.StateErrorContext; +import liquidjava.fsm.StateMachine; +import liquidjava.fsm.StateMachineInitialTransition; +import liquidjava.fsm.StateMachineTransition; + +/** + * DTO for serializing a state machine diagram, with the state error shown on it + */ +public record StateMachineDTO( + String className, + List states, + List transitions, + List initialTransitions, + StateErrorContextDTO errorContext) { + + 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())); + } +} diff --git a/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java b/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java new file mode 100644 index 0000000..dc0661b --- /dev/null +++ b/server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java @@ -0,0 +1,41 @@ +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; + +class StateErrorContextDTOTest { + + @Test + 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"))); + } + + @Test + 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")); + assertEquals(List.of("closed", "opened"), dto.possibleStates()); + assertEquals(List.of(), dto.validStates()); + assertEquals(List.of("opened"), dto.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")); + assertEquals(List.of(), dto.acceptedStates()); + assertEquals(List.of(), dto.validStates()); + assertEquals(List.of(), dto.invalidStates()); + } +} diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index b276efb..6de0095 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -16,6 +16,7 @@ import dtos.warnings.*; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.hints.Hint; import liquidjava.diagnostics.warnings.*; import liquidjava.processor.VCImplication; import liquidjava.processor.context.PlacementInCode; @@ -48,7 +49,7 @@ void createSourcePosition() throws Exception { @Test void preservesCommonDiagnosticFields() throws Exception { CustomError error = new CustomError("verification failed", position); - error.setHint("check the refinement"); + error.addHint(Hint.general("check the refinement")); LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(error); assertEquals("error", dto.category); assertEquals("custom-error", dto.type); @@ -154,7 +155,8 @@ void preservesRefinementDetailsAndSimplificationHistory() { void preservesStateRefinementDetailsWithoutDeclarationFile() { StateRefinementErrorDTO dto = (StateRefinementErrorDTO) DiagnosticConverter.convertToDTO( new StateRefinementError(position, null, new Predicate(new LiteralBoolean(false)), - new VCSimplificationResult(new VCImplication(new Predicate())), null, "expected closed")); + new VCSimplificationResult(new VCImplication(new Predicate())), null, "expected closed", + List.of(), null, null)); assertEquals("error", dto.category); assertEquals("state-refinement-error", dto.type); assertEquals("false", dto.expected);