From 6b266c5c35281f17ed71ff3a44050e6e557700fa Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 01:29:06 +0100 Subject: [PATCH] Show the verifier's states of a state error on the state machine Bumps the verifier to 0.0.36, liquidjava-fsm to 0.2.0 and Spoon to 11.5.0. fsm now only draws the diagram, picked by the error's receiver class, and the possible, accepted, valid and invalid states come from the verifier's StateErrorContext instead of fsm's reading of the predicates' text. A state of the diagram is marked only when every possible combination with it agrees, so the marks stay true for classes with several state sets. Co-Authored-By: Claude Opus 5.5 --- client/src/types/fsm.ts | 19 ++++--- client/src/webview/diagram-focus.spec.ts | 47 ++++++----------- client/src/webview/diagram-focus.ts | 20 +++----- client/src/webview/diagram.ts | 2 +- client/src/webview/script.spec.ts | 4 +- client/src/webview/views/fsm/fsm.spec.ts | 47 +++++++++-------- server/pom.xml | 6 +-- .../dtos/errors/StateRefinementErrorDTO.java | 15 +++--- .../java/dtos/fsm/StateErrorContextDTO.java | 51 +++++++++++++++++++ .../main/java/dtos/fsm/StateMachineDTO.java | 25 +++++++++ .../dtos/fsm/StateErrorContextDTOTest.java | 41 +++++++++++++++ .../java/utils/DiagnosticConverterTest.java | 6 ++- 12 files changed, 194 insertions(+), 89 deletions(-) create mode 100644 server/src/main/java/dtos/fsm/StateErrorContextDTO.java create mode 100644 server/src/main/java/dtos/fsm/StateMachineDTO.java create mode 100644 server/src/test/java/dtos/fsm/StateErrorContextDTOTest.java 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);