Skip to content

Name state errors as a compiler would on the state machine #168

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 2 commits into from
Oct 27, 2026
Merged

Name state errors as a compiler would on the state machine #168

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
336b998
Name state errors as a compiler would on the state machine
CatarinaGamboa Oct 26, 2026
d3be0f8
Keep the word state in the state error summary
CatarinaGamboa Oct 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions client/src/webview/script.spec.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -370,12 +370,12 @@ describe('webview script', () => {
stateError('Second state error', { ...errorMachine('Second', 'reset'), errorContext: null }, 9),
]);
click('[data-tab="fsm"]');
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 5 is rejected');
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call at line 5');
expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2');

click('.state-error-step-btn[data-step="1"]');
expect(root.querySelector('.diagram-title')?.textContent).toBe('Second');
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 10 is rejected');
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call at line 10');

click('#state-error-reveal-btn');
expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics');
Expand Down
38 changes: 19 additions & 19 deletions client/src/webview/views/fsm/fsm.spec.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,23 +119,23 @@ describe('state machine view', () => {
}
});

it('summarizes where the call is rejected and allowed in one line', () => {
it('summarizes the invalid call with the expected and actual states in one line', () => {
const errorMachine = machine({
states: ['unbound', 'bound', 'connected', 'closed'],
errorContext: socketError(['bound', 'closed']),
});
renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true);

const summary = document.querySelector('.diagram-error-text')!;
expect(summary.textContent).toBe('socket.receive() is rejected when socket is in state closed \u00B7 allowed in state bound');
expect(Array.from(summary.querySelectorAll('code'), node => node.textContent)).toEqual(['socket.receive()', 'socket', 'closed', 'bound']);
expect(summary.textContent).toBe('Invalid method call socket.receive() \u00B7 expected state unbound or bound or connected \u00B7 actual state bound or closed');
expect(Array.from(summary.querySelectorAll('code'), node => node.textContent)).toEqual(['socket.receive()', 'unbound', 'bound', 'connected', 'bound', 'closed']);
expect(button('diagram-focus-btn').textContent?.trim()).toBe('Show all');

renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, false);
expect(button('diagram-focus-btn').textContent?.trim()).toBe('Focus on error');
});

it('omits the allowed part of the summary when no possible state accepts the call', () => {
it('names the expected and actual states when no actual is expected', () => {
renderStateMachineView(document.body, [machine({
states: ['childrenAllowed', 'maybeHasChildren'],
errorContext: {
Expand All @@ -144,19 +144,19 @@ describe('state machine view', () => {
},
})], [diagram], 'TB', false, true);

expect(document.querySelector('.diagram-error-text')?.textContent).toBe('root.getFirstChild() is rejected when root is in state childrenAllowed');
expect(document.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call root.getFirstChild() \u00B7 expected state maybeHasChildren \u00B7 actual state childrenAllowed');
});

it.each([
[
'the state of the receiver is unknown',
['unbound', 'bound', 'connected', 'closed'],
'socket.receive() is rejected: the state of socket is unknown here \u00B7 allowed in state unbound or bound or connected',
'Invalid method call socket.receive() \u00B7 expected state unbound or bound or connected \u00B7 actual state unknown',
],
[
'every possible state accepts the call',
'every actual is expected',
['bound'],
'socket.receive() is rejected here \u00B7 allowed in state bound',
'Invalid method call socket.receive() \u00B7 expected state unbound or bound or connected \u00B7 actual state bound',
],
])('summarizes the error when %s', (_, possibleStates, summary) => {
renderStateMachineView(document.body, [machine({
Expand All @@ -168,9 +168,9 @@ describe('state machine view', () => {
});

it.each([
['invalid, valid, and other accepted states', ['bound', 'closed'], ['\u2715 Call rejected', '\u2713 Call allowed', 'Allowed, but not reachable here']],
['only an invalid and other accepted states', ['closed'], ['\u2715 Call rejected', 'Allowed, but not reachable here']],
['an unknown receiver state', ['unbound', 'bound', 'connected', 'closed'], ['Allowed, but not reachable here']],
['invalid, valid, and other accepted states', ['bound', 'closed'], ['\u2715 Actual state, not expected', '\u2713 Actual state, expected', 'Expected state']],
['only an invalid and other accepted states', ['closed'], ['\u2715 Actual state, not expected', 'Expected state']],
['an unknown receiver state', ['unbound', 'bound', 'connected', 'closed'], ['Expected state']],
])('explains the state marks in a legend with %s', (_, possibleStates, items) => {
renderStateMachineView(document.body, [machine({
states: ['unbound', 'bound', 'connected', 'closed'],
Expand Down Expand Up @@ -200,8 +200,8 @@ describe('state machine view', () => {
['without the accepted states', {
calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'],
acceptedStates: [], validStates: [], invalidStates: [],
}, 'counter.open() is rejected here'],
['without an error context', null, 'The call at line 12 is rejected'],
}, 'Invalid method call counter.open()'],
['without an error context', null, 'Invalid method call at line 12'],
])('keeps the stepper and View error for a shown error %s', (_, errorContext, text) => {
renderStateMachineView(document.body, [machine({ errorContext })], [diagram], 'TB', false, true, { index: 1, count: 2, line: 12 });

Expand All @@ -213,10 +213,10 @@ describe('state machine view', () => {
expect(document.querySelector('#diagram-focus-btn')).toBeNull();
});

it('says the call is rejected without a line when the shown error has no position', () => {
it('names the invalid call without a line when the shown error has no position', () => {
renderStateMachineView(document.body, [machine()], [diagram], 'TB', false, true, { index: -1, count: 0, line: null });

expect(document.querySelector('.diagram-error-text')?.textContent).toBe('The call is rejected');
expect(document.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call');
});

it('clips the panned diagram below the error summary and legend', () => {
Expand Down Expand Up @@ -338,7 +338,7 @@ describe('state machine view', () => {
expect(Array.from(document.querySelectorAll('.diagram-state-set'), node => node.classList.contains('diagram-state-set-dimmed')))
.toEqual([false, true]);
expect(document.querySelector('.diagram-error-text')?.textContent)
.toBe('param.setCompressionType() is rejected when param is in state startCompression');
.toBe('Invalid method call param.setCompressionType() \u00B7 expected state compressionExplicit \u00B7 actual state startCompression');

renderStateMachineView(document.body, sms, ['compression diagram', 'tiling diagram'], 'TB', false, false);
expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull();
Expand All @@ -354,18 +354,18 @@ describe('state machine view', () => {
renderStateMachineView(document.body, sms, ['tiling diagram', 'compression diagram'], 'TB', false, true);

expect(document.querySelector('.diagram-error-text')?.textContent)
.toBe('param.write() is rejected when param is in state startTiling \u00B7 allowed in state compressionExplicit');
.toBe('Invalid method call param.write() \u00B7 expected state tilingSet and compressionExplicit \u00B7 actual state startTiling and compressionExplicit');
expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull();
expect(Array.from(document.querySelectorAll('.diagram-error-legend-item'), node => node.textContent))
.toEqual(['\u2715 Call rejected', '\u2713 Call allowed', 'Allowed, but not reachable here']);
.toEqual(['\u2715 Actual state, not expected', '\u2713 Actual state, expected', 'Expected state']);
});

it('names the call of the state set with the error when it cannot be marked', () => {
const unmarked = { ...compressionError, acceptedStates: [], invalidStates: [] };
renderStateMachineView(document.body, [{ ...compression, errorContext: unmarked }, tiling],
['compression diagram', 'tiling diagram'], 'TB', false, true, { index: 0, count: 1, line: 7 });

expect(document.querySelector('.diagram-error-text')?.textContent).toBe('param.setCompressionType() is rejected here');
expect(document.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call param.setCompressionType()');
// nothing is marked, so nothing is dimmed
expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull();
});
Expand Down
53 changes: 24 additions & 29 deletions client/src/webview/views/fsm/fsm.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,39 +93,27 @@ function isStateErrorShown(stateErrors: StateErrorNavigation): boolean {
return stateErrors.index >= 0 || stateErrors.line !== undefined;
}

// summarises the error of every state set it involves, which is rejected when the receiver is in any invalid state
// summarises the error of every state set it involves as a compiler would: the invalid call, then the expected and actual states
function getStateErrorSummary(focuses: StateErrorFocus[]): string {
const focus = focuses[0];
const call = getRejectedCallText(focus);
const receiver = focus.receiver ? `<code>${escapeHtml(focus.receiver)}</code>` : 'the receiver';
const rejected = `${call ? `<code>${escapeHtml(call)}</code>` : 'The call'} is rejected`;
const invalidStates = focuses.flatMap(focus => focus.invalidStates);
const allowedStates = focuses
.map(focus => focus.unknownState ? focus.acceptedStates : focus.validStates)
.filter(states => states.length > 0);
let summary: string;
if (invalidStates.length > 0) {
summary = `${rejected} when ${receiver} is in state ${renderStates(invalidStates)}`;
} else if (focuses.every(focus => focus.unknownState)) {
summary = `${rejected}: the state of ${receiver} is unknown here`;
} else {
summary = `${rejected} here`;
}
// the call needs an allowed state of each state set
if (allowedStates.length > 0) {
summary += ` \u00B7 allowed in state ${allowedStates
.map(states => allowedStates.length > 1 && states.length > 1 ? `(${renderStates(states)})` : renderStates(states))
.join(' and ')}`;
}
return summary;
const call = getRejectedCallText(focuses[0]);
// the call needs an expected state of each state set
const expected = renderStateSets(focuses.map(focus => focus.acceptedStates));
const actual = focuses.every(focus => focus.unknownState)
? 'unknown'
: renderStateSets(focuses.filter(focus => !focus.unknownState).map(focus => focus.possibleStates));
return `${renderInvalidCall(call)} \u00B7 expected state ${expected} \u00B7 actual state ${actual}`;
}

// the shown error cannot be marked on the diagrams when the verifier could not tell which states allow the call
function getUnmarkedStateErrorSummary(sms: LJStateMachine[], stateErrors: StateErrorNavigation): string {
const context = sms.find(sm => sm.errorContext)?.errorContext;
const call = context ? getRejectedCallText(context) : null;
if (call) return `<code>${escapeHtml(call)}</code> is rejected here`;
return stateErrors.line ? `The call at line ${stateErrors.line} is rejected` : 'The call is rejected';
if (call || !stateErrors.line) return renderInvalidCall(call);
return `Invalid method call at line ${stateErrors.line}`;
}

function renderInvalidCall(call: string | null): string {
return call ? `Invalid method call <code>${escapeHtml(call)}</code>` : 'Invalid method call';
}

function renderStateErrorSummary(summary: string, stateErrors: StateErrorNavigation): string {
Expand Down Expand Up @@ -153,10 +141,10 @@ function renderStateErrorStepper({ index, count }: StateErrorNavigation): string
// explains the state marks with the same outlines, fills, and icons as the diagram, next to the toggle that dims the rest
function renderStateErrorLegend(focuses: StateErrorFocus[], focusOnError: boolean): string {
const items = [
focuses.some(focus => focus.invalidStates.length > 0) ? renderLegendItem('invalid', `${INVALID_STATE_ICON} Call rejected`) : '',
focuses.some(focus => focus.validStates.length > 0) ? renderLegendItem('valid', `${VALID_STATE_ICON} Call allowed`) : '',
focuses.some(focus => focus.invalidStates.length > 0) ? renderLegendItem('invalid', `${INVALID_STATE_ICON} Actual state, not expected`) : '',
focuses.some(focus => focus.validStates.length > 0) ? renderLegendItem('valid', `${VALID_STATE_ICON} Actual state, expected`) : '',
focuses.some(focus => focus.acceptedStates.some(state => !focus.validStates.includes(state)))
? renderLegendItem('accepted', 'Allowed, but not reachable here')
? renderLegendItem('accepted', 'Expected state')
: '',
].filter(Boolean);
return /*html*/`
Expand All @@ -173,6 +161,13 @@ function renderLegendItem(kind: string, label: string): string {
return `<span class="diagram-error-legend-item"><span class="diagram-error-legend-swatch diagram-error-legend-${kind}" aria-hidden="true"></span>${label}</span>`;
}

// the states of each state set, the call needs one state of each
function renderStateSets(stateSets: string[][]): string {
return stateSets
.map(states => stateSets.length > 1 && states.length > 1 ? `(${renderStates(states)})` : renderStates(states))
.join(' and ');
}

function renderStates(states: string[]): string {
return states.map(state => `<code>${escapeHtml(state)}</code>`).join(' or ');
}
Loading