Skip to content

Commit f1c258a

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Show the verifier's states of a state error on the state machine (#160)
## Why Until now, the state machine view got the receiver's possible and accepted states from liquidjava-fsm, which re-read the error's `expected` and `found` predicates as text. The verifier now computes those states with the SMT solver and reports them on `StateRefinementError#getContext()` (liquid-java/liquidjava#421). fsm 0.2.0 dropped its error context and only draws diagrams (liquid-java/liquidjava-fsm#12). This PR switches the view to the verifier's answer, so the diagram never contradicts the error next to it. ## What **Dependencies:** liquidjava-verifier 0.0.36, liquidjava-fsm 0.2.0 and Spoon 11.5.0, the version the verifier now uses. **Server** - `StateRefinementErrorDTO` builds the diagram with `StateMachineParser.parse(declaration file, context.receiverClass())`, so a file that declares several classes shows the receiver's class. - The new `StateMachineDTO` and `StateErrorContextDTO` keep the shape the webview already reads (`stateMachine.errorContext`). The error context now has `calledMethod`, `receiver`, `possibleStates`, `acceptedStates`, `validStates` and `invalidStates`. - The verifier names each state in every state set. The diagram shows the first set, and a state is marked so that the marks are never wrong: - It is **valid** only if the call is accepted in *every* possible combination with that state. - It is **invalid** only if the call is accepted in *none* of them. - Otherwise it stays unmarked. When the accepted states depend on the arguments, nothing is marked. - With one state set, this gives the same marks as before. **Client** - `getStateErrorFocus` uses the server's lists directly. The fallbacks to `definiteFoundState` and `actualStates` are gone, and so are `expectedCondition` and `foundCondition`, which nothing displayed. **Fixed:** the `setHint` test, which broke when hints became a list (liquid-java/liquidjava#410). Output for the fsm study fixtures (DatagramSocket and tree node), serialized by the server: ```json {"calledMethod":"receive","receiver":"socket","possibleStates":["bound","closed"],"acceptedStates":["unbound","bound","connected"],"validStates":["bound"],"invalidStates":["closed"]} {"calledMethod":"getFirstChild","receiver":"root","possibleStates":["childrenAllowed"],"acceptedStates":["maybeHasChildren"],"validStates":[],"invalidStates":["childrenAllowed"]} ``` These are the same marks the view showed before for these examples. ## Follow-ups - One diagram per `@StateSet` (#115, #116, liquid-java/liquidjava-fsm#8), e.g. ImageWriteParam. - Send the hints as a list (with their kind) and the error category. - Cache the diagram per class instead of parsing the file for each error. ## Tests - Server: `mvn test`, 27 tests pass, including the new `StateErrorContextDTOTest`: one state set, several sets with a partly accepted state, and unknown accepted states. - Client: `vitest`, 71 tests pass, and `tsc` is clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 34d7611 commit f1c258a

12 files changed

Lines changed: 194 additions & 89 deletions

File tree

‎client/src/types/fsm.ts‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,16 @@ export type LJStateMachine = {
88
errorContext: LJStateMachineErrorContext | null;
99
};
1010

11+
// The verifier's states of a rejected call, on the diagram's states
1112
export type LJStateMachineErrorContext = {
12-
calledMethod: string | null;
13-
actualStates: string[];
14-
receiver?: string | null;
15-
expectedStates?: string[];
16-
expectedCondition?: string | null;
17-
foundCondition?: string | null;
18-
definiteFoundState?: string | null;
19-
possibleStates?: string[];
13+
calledMethod: string;
14+
receiver: string;
15+
// states the receiver may be in at the call
16+
possibleStates: string[];
17+
// states from which the call is accepted, empty when they depend on more than the receiver's state
18+
acceptedStates: string[];
19+
// possible states from which the call is accepted
20+
validStates: string[];
21+
// possible states from which the call is rejected
22+
invalidStates: string[];
2023
};

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

Lines changed: 15 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,11 @@ function treeNode(errorContext: Partial<LJStateMachineErrorContext> | null = {})
1717
],
1818
errorContext: errorContext && {
1919
calledMethod: 'getFirstChild',
20-
actualStates: ['childrenAllowed'],
2120
receiver: 'root',
22-
expectedStates: ['maybeHasChildren'],
23-
definiteFoundState: 'childrenAllowed',
2421
possibleStates: ['childrenAllowed'],
22+
acceptedStates: ['maybeHasChildren'],
23+
validStates: [],
24+
invalidStates: ['childrenAllowed'],
2525
...errorContext,
2626
},
2727
};
@@ -47,13 +47,11 @@ function datagramSocket(errorContext: Partial<LJStateMachineErrorContext> = {}):
4747
],
4848
errorContext: {
4949
calledMethod: 'receive',
50-
actualStates: ['bound', 'closed'],
5150
receiver: 'socket',
52-
expectedStates: open,
53-
expectedCondition: 'unbound(socket) || bound(socket) || connected(socket)',
54-
foundCondition: 'flag ? closed(socket) : bound(socket)',
55-
definiteFoundState: null,
5651
possibleStates: ['bound', 'closed'],
52+
acceptedStates: open,
53+
validStates: ['bound'],
54+
invalidStates: ['closed'],
5755
...errorContext,
5856
},
5957
};
@@ -84,16 +82,6 @@ describe('state error focus', () => {
8482
expect(getRelatedStates(getStateErrorFocus(datagramSocket())!)).toEqual(['bound', 'closed', 'unbound', 'connected']);
8583
});
8684

87-
it.each([
88-
['the definite found state', { possibleStates: undefined, definiteFoundState: 'closed' }, [], ['closed']],
89-
['the found states', { possibleStates: undefined, definiteFoundState: null }, ['bound'], ['closed']],
90-
])('falls back to %s without possible states', (_, errorContext, validStates, invalidStates) => {
91-
const focus = getStateErrorFocus(datagramSocket(errorContext));
92-
93-
expect(focus?.validStates).toEqual(validStates);
94-
expect(focus?.invalidStates).toEqual(invalidStates);
95-
});
96-
9785
it('marks valid and invalid states and colours every edge of the called method', () => {
9886
for (const focusOnError of [true, false]) {
9987
const diagram = lines(createMermaidDiagram(datagramSocket(), 'TB', false, focusOnError));
@@ -174,25 +162,21 @@ describe('state error focus', () => {
174162
.toContain(`bound --> bound : ${calledMethod('receive')}<br/>${dimmedMethod('send')}<br/>${dimmedMethod('receiveAll')}`);
175163
});
176164

177-
it.each([
178-
['no accepted states', { expectedStates: [], possibleStates: [] }],
179-
['accepted states outside the machine', { expectedStates: ['listening'] }],
180-
])('does not focus with %s', (_, errorContext) => {
181-
const sm = datagramSocket(errorContext);
165+
it('does not focus without accepted states', () => {
166+
const sm = datagramSocket({ acceptedStates: [], validStates: [], invalidStates: [] });
182167

183168
expect(getStateErrorFocus(sm)).toBeNull();
184169
const diagram = createMermaidDiagram(sm, 'TB', false, true);
185170
expect(diagram).not.toMatch(/ljStateDimmed|lj-dimmed-transitions|ljStateValid|ljStateInvalid/);
186171
expect(diagram).toContain('class bound,closed ljStateErrorActual');
187172
});
188173

189-
it('ignores possible states outside the machine and falls back when none are given', () => {
190-
expect(getStateErrorFocus(datagramSocket({ possibleStates: ['closed', 'listening'] }))?.possibleStates).toEqual(['closed']);
191-
expect(getStateErrorFocus(datagramSocket({ possibleStates: [] }))?.possibleStates).toEqual(['bound', 'closed']);
192-
});
193-
194174
it('only hints at the accepted states when the state of the receiver is unknown', () => {
195-
const sm = datagramSocket({ possibleStates: ['unbound', 'bound', 'connected', 'closed', 'broken'], foundCondition: 'true' });
175+
const sm = datagramSocket({
176+
possibleStates: ['unbound', 'bound', 'connected', 'closed', 'broken'],
177+
validStates: ['unbound', 'bound', 'connected'],
178+
invalidStates: ['closed', 'broken'],
179+
});
196180

197181
const focus = getStateErrorFocus(sm);
198182
expect(focus).toMatchObject({ unknownState: true, validStates: [], invalidStates: [] });
@@ -220,9 +204,8 @@ describe('state error focus', () => {
220204
expect(dimmedTransitions(diagram.join('\n'))).toEqual(['%% lj-dimmed-transitions: edge0 edge2']);
221205
});
222206

223-
it('keeps the previous highlighting for an error context without the accepted states', () => {
224-
const sm = treeNode();
225-
sm.errorContext = { calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'] };
207+
it('only highlights the possible states when the accepted states are unknown', () => {
208+
const sm = treeNode({ acceptedStates: [], validStates: [], invalidStates: [] });
226209

227210
expect(getStateErrorFocus(sm)).toBeNull();
228211
const diagram = createMermaidDiagram(sm, 'TB', false, true);

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

Lines changed: 7 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -28,23 +28,17 @@ export type StateErrorFocus = {
2828
*/
2929
export function getStateErrorFocus(sm: LJStateMachine | undefined): StateErrorFocus | null {
3030
const context = sm?.errorContext;
31-
const acceptedStates = sm?.states.filter(state => context?.expectedStates?.includes(state)) ?? [];
32-
if (!sm || !context || acceptedStates.length === 0) return null;
31+
if (!sm || !context || context.acceptedStates.length === 0) return null;
3332

34-
const possible = context.possibleStates?.length
35-
? context.possibleStates
36-
: context.definiteFoundState ? [context.definiteFoundState] : context.actualStates;
37-
const possibleStates = sm.states.filter(state => possible.includes(state));
3833
// marking every state as valid or invalid would only say that the state is unknown
39-
const unknownState = possibleStates.length === sm.states.length;
40-
const markedStates = unknownState ? [] : possibleStates;
34+
const unknownState = context.possibleStates.length === sm.states.length;
4135
return {
4236
calledMethod: context.calledMethod,
43-
receiver: context.receiver ?? null,
44-
possibleStates,
45-
validStates: markedStates.filter(state => acceptedStates.includes(state)),
46-
invalidStates: markedStates.filter(state => !acceptedStates.includes(state)),
47-
acceptedStates,
37+
receiver: context.receiver,
38+
possibleStates: context.possibleStates,
39+
validStates: unknownState ? [] : context.validStates,
40+
invalidStates: unknownState ? [] : context.invalidStates,
41+
acceptedStates: context.acceptedStates,
4842
unknownState,
4943
};
5044
}

‎client/src/webview/diagram.ts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ export function createMermaidDiagram(
8787
});
8888

8989
if (!errorFocus) {
90-
const highlightedStates = sm.states.filter(state => sm.errorContext?.actualStates.includes(state));
90+
const highlightedStates = sm.errorContext?.possibleStates ?? [];
9191
if (highlightedStates.length > 0) {
9292
lines.push(` class ${highlightedStates.join(',')} ljStateErrorActual`);
9393
}

‎client/src/webview/script.spec.ts‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,8 +75,8 @@ function errorMachine(className: string, calledMethod: string): LJStateMachine {
7575
transitions: [...stateMachine.transitions, { from: 'Broken', to: 'Broken', label: 'reopen()' }],
7676
initialTransitions: [{ to: 'Open' }, { to: 'Broken' }],
7777
errorContext: {
78-
calledMethod, actualStates: ['Closed'], receiver: 'counter', expectedStates: ['Open'],
79-
expectedCondition: 'Open(counter)', foundCondition: 'Closed(counter)', definiteFoundState: 'Closed',
78+
calledMethod, receiver: 'counter', possibleStates: ['Closed'], acceptedStates: ['Open'],
79+
validStates: [], invalidStates: ['Closed'],
8080
},
8181
};
8282
}

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

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import { afterEach, describe, expect, it, vi } from 'vitest';
2-
import type { LJStateMachine } from '../../../types/fsm';
2+
import type { LJStateMachine, LJStateMachineErrorContext } from '../../../types/fsm';
33
import { renderStateMachineView } from './fsm';
44

55
const diagram = 'stateDiagram-v2\n[*] --> Closed\nClosed --> Open: open';
@@ -13,6 +13,16 @@ function machine(overrides: Partial<LJStateMachine> = {}): LJStateMachine {
1313
};
1414
}
1515

16+
// socket.receive(), allowed while the socket is open, as the server reports it for the given possible states
17+
function socketError(possibleStates: string[]): LJStateMachineErrorContext {
18+
const acceptedStates = ['unbound', 'bound', 'connected'];
19+
return {
20+
calledMethod: 'receive', receiver: 'socket', possibleStates, acceptedStates,
21+
validStates: possibleStates.filter(state => acceptedStates.includes(state)),
22+
invalidStates: possibleStates.filter(state => !acceptedStates.includes(state)),
23+
};
24+
}
25+
1626
function button(id: string): HTMLButtonElement {
1727
return document.querySelector<HTMLButtonElement>(`#${id}`)!;
1828
}
@@ -112,10 +122,7 @@ describe('state machine view', () => {
112122
it('summarizes where the call is rejected and allowed in one line', () => {
113123
const errorMachine = machine({
114124
states: ['unbound', 'bound', 'connected', 'closed'],
115-
errorContext: {
116-
calledMethod: 'receive', actualStates: ['bound', 'closed'], receiver: 'socket',
117-
expectedStates: ['unbound', 'bound', 'connected'], possibleStates: ['bound', 'closed'],
118-
},
125+
errorContext: socketError(['bound', 'closed']),
119126
});
120127
renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true);
121128

@@ -132,8 +139,8 @@ describe('state machine view', () => {
132139
renderStateMachineView(document.body, machine({
133140
states: ['childrenAllowed', 'maybeHasChildren'],
134141
errorContext: {
135-
calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'], receiver: 'root',
136-
expectedStates: ['maybeHasChildren'], definiteFoundState: 'childrenAllowed',
142+
calledMethod: 'getFirstChild', receiver: 'root', possibleStates: ['childrenAllowed'],
143+
acceptedStates: ['maybeHasChildren'], validStates: [], invalidStates: ['childrenAllowed'],
137144
},
138145
}), diagram, 'TB', false, true);
139146

@@ -143,21 +150,18 @@ describe('state machine view', () => {
143150
it.each([
144151
[
145152
'the state of the receiver is unknown',
146-
{ possibleStates: ['unbound', 'bound', 'connected', 'closed'] },
153+
['unbound', 'bound', 'connected', 'closed'],
147154
'socket.receive() is rejected: the state of socket is unknown here \u00B7 allowed in state unbound or bound or connected',
148155
],
149156
[
150157
'every possible state accepts the call',
151-
{ possibleStates: ['bound'] },
158+
['bound'],
152159
'socket.receive() is rejected here \u00B7 allowed in state bound',
153160
],
154-
])('summarizes the error when %s', (_, errorContext, summary) => {
161+
])('summarizes the error when %s', (_, possibleStates, summary) => {
155162
renderStateMachineView(document.body, machine({
156163
states: ['unbound', 'bound', 'connected', 'closed'],
157-
errorContext: {
158-
calledMethod: 'receive', actualStates: [], receiver: 'socket',
159-
expectedStates: ['unbound', 'bound', 'connected'], ...errorContext,
160-
},
164+
errorContext: socketError(possibleStates),
161165
}), diagram, 'TB', false, true);
162166

163167
expect(document.querySelector('.diagram-error-text')?.textContent).toBe(summary);
@@ -170,10 +174,7 @@ describe('state machine view', () => {
170174
])('explains the state marks in a legend with %s', (_, possibleStates, items) => {
171175
renderStateMachineView(document.body, machine({
172176
states: ['unbound', 'bound', 'connected', 'closed'],
173-
errorContext: {
174-
calledMethod: 'receive', actualStates: [], receiver: 'socket',
175-
expectedStates: ['unbound', 'bound', 'connected'], possibleStates,
176-
},
177+
errorContext: socketError(possibleStates),
177178
}), diagram, 'TB', false, true);
178179

179180
const legend = document.querySelectorAll('.diagram-error-legend-item');
@@ -183,7 +184,10 @@ describe('state machine view', () => {
183184

184185
it.each([
185186
['no error', null],
186-
['an error context without the accepted states', { calledMethod: 'open', actualStates: ['Closed'] }],
187+
['an error context without the accepted states', {
188+
calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'],
189+
acceptedStates: [], validStates: [], invalidStates: [],
190+
}],
187191
])('omits the error summary with %s', (_, errorContext) => {
188192
renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true);
189193

@@ -194,7 +198,10 @@ describe('state machine view', () => {
194198

195199
it('clips the panned diagram below the error summary and legend', () => {
196200
renderStateMachineView(document.body, machine({
197-
errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] },
201+
errorContext: {
202+
calledMethod: 'read', receiver: 'counter', possibleStates: ['Closed'],
203+
acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'],
204+
},
198205
}), diagram, 'TB', false, true);
199206

200207
const viewport = document.querySelector('.diagram-viewport')!;

‎server/pom.xml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@
101101
<maven.compiler.release>20</maven.compiler.release>
102102
<!-- versions -->
103103
<version.memcompiler>1.3.0</version.memcompiler>
104-
<version.spoon>10.4.2</version.spoon>
104+
<version.spoon>11.5.0</version.spoon>
105105
<version.z3>4.8.17</version.z3>
106106
<version.liquidjava>1.0</version.liquidjava>
107107
<!-- plugin versions -->
@@ -167,12 +167,12 @@
167167
<dependency>
168168
<groupId>io.github.liquid-java</groupId>
169169
<artifactId>liquidjava-verifier</artifactId>
170-
<version>0.0.35</version>
170+
<version>0.0.36</version>
171171
</dependency>
172172
<dependency>
173173
<groupId>io.github.liquid-java</groupId>
174174
<artifactId>liquidjava-fsm</artifactId>
175-
<version>0.1.5</version>
175+
<version>0.2.0</version>
176176
</dependency>
177177
<dependency>
178178
<groupId>tools.aqua</groupId>

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

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,10 @@
44

55
import dtos.diagnostics.SourcePositionDTO;
66
import dtos.diagnostics.VCSimplificationResultDTO;
7-
import liquidjava.fsm.StateMachine;
8-
import liquidjava.fsm.StateMachineParser;
7+
import dtos.fsm.StateMachineDTO;
8+
import liquidjava.diagnostics.errors.StateErrorContext;
99
import liquidjava.diagnostics.errors.StateRefinementError;
10+
import liquidjava.fsm.StateMachineParser;
1011
import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
1112

1213
/**
@@ -18,20 +19,18 @@ public class StateRefinementErrorDTO extends LJErrorDTO {
1819
public final VCSimplificationResultDTO found;
1920
public final String customMessage;
2021
public final SourcePositionDTO declarationPosition;
21-
public final StateMachine stateMachine;
22+
public final StateMachineDTO stateMachine;
2223

2324
public StateRefinementErrorDTO(StateRefinementError error) {
2425
super("state-refinement-error", error);
2526
this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
2627
this.found = VCSimplificationResultDTO.from(error.getFoundSimplification());
2728
this.customMessage = error.getCustomMessage();
2829
this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
30+
StateErrorContext context = error.getContext();
2931
this.stateMachine = declarationPosition == null || declarationPosition.file() == null ? null
30-
: StateMachineParser.parseWithErrorContext(
31-
new File(declarationPosition.file()).toURI().toString(),
32-
error.getDeclarationPosition(),
33-
error.getExpected() == null ? null : error.getExpected().getExpression(),
34-
error.getFound());
32+
: StateMachineDTO.from(StateMachineParser.parse(new File(declarationPosition.file()).toURI().toString(),
33+
context == null ? null : context.receiverClass()), context);
3534
}
3635

3736
public static StateRefinementErrorDTO from(StateRefinementError error) {

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

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
package dtos.fsm;
2+
3+
import java.util.List;
4+
import java.util.stream.Stream;
5+
6+
import liquidjava.diagnostics.errors.StateErrorContext;
7+
8+
/**
9+
* DTO for serializing the verifier's states of a rejected call on the diagram of its first state set
10+
* The verifier names each state by its name in every state set, so a state of the diagram is valid only if the call
11+
* is accepted in every possible combination with it, and invalid only if it is accepted in none
12+
*
13+
* @param calledMethod the name of the called method, as in the diagram's transitions
14+
* @param receiver the receiver of the call as written in the code
15+
* @param possibleStates the states the receiver can be in before the call
16+
* @param acceptedStates the states that allow the call, empty if they depend on more than the receiver's state,
17+
* in which case no state is marked valid or invalid
18+
* @param validStates the possible states that allow the call
19+
* @param invalidStates the possible states that do not allow the call
20+
*/
21+
public record StateErrorContextDTO(
22+
String calledMethod,
23+
String receiver,
24+
List<String> possibleStates,
25+
List<String> acceptedStates,
26+
List<String> validStates,
27+
List<String> invalidStates) {
28+
29+
public static StateErrorContextDTO from(StateErrorContext context, List<String> states) {
30+
if (context == null) return null;
31+
String calledMethod = context.method().substring(0, context.method().indexOf('('));
32+
List<List<String>> possible = context.possibleStates();
33+
List<String> possibleStates = firstSet(possible, states);
34+
List<List<String>> accepted = context.acceptedStates();
35+
if (accepted == null) // nothing can be marked without knowing which states allow the call
36+
return new StateErrorContextDTO(calledMethod, context.receiver(), possibleStates, List.of(), List.of(),
37+
List.of());
38+
return new StateErrorContextDTO(calledMethod, context.receiver(), possibleStates, firstSet(accepted, states),
39+
possibleStates.stream().filter(s -> withState(possible, s).allMatch(accepted::contains)).toList(),
40+
possibleStates.stream().filter(s -> withState(possible, s).noneMatch(accepted::contains)).toList());
41+
}
42+
43+
/** The states of the diagram that appear in the first state set of {@code combinations} */
44+
private static List<String> firstSet(List<List<String>> combinations, List<String> states) {
45+
return states.stream().filter(s -> withState(combinations, s).findAny().isPresent()).toList();
46+
}
47+
48+
private static Stream<List<String>> withState(List<List<String>> combinations, String state) {
49+
return combinations.stream().filter(c -> c.get(0).equals(state));
50+
}
51+
}

0 commit comments

Comments
 (0)