From 336b998a79e191dfa8e64dd4625b5e1d98987fc2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 26 Oct 2026 19:11:51 +0000 Subject: [PATCH 1/2] Name state errors as a compiler would on the state machine The summary said the call is rejected when the receiver is in a state and allowed in another, and the legend marked states as call rejected, call allowed, or allowed but not reachable. Say invalid method call, then the expected and actual states, as the Verification tab and compilers do, and mark the actual states as expected or not and the other expected states. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/script.spec.ts | 4 +- client/src/webview/views/fsm/fsm.spec.ts | 38 ++++++++--------- client/src/webview/views/fsm/fsm.ts | 53 +++++++++++------------- 3 files changed, 45 insertions(+), 50 deletions(-) diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index dbd0e44..1a35885 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -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'); diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index aaab5c9..1145453 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -119,7 +119,7 @@ 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']), @@ -127,15 +127,15 @@ describe('state machine view', () => { 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 unbound or bound or connected \u00B7 actual 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: { @@ -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 maybeHasChildren \u00B7 actual 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 unbound or bound or connected \u00B7 actual 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 unbound or bound or connected \u00B7 actual bound', ], ])('summarizes the error when %s', (_, possibleStates, summary) => { renderStateMachineView(document.body, [machine({ @@ -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'], @@ -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 }); @@ -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', () => { @@ -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 compressionExplicit \u00B7 actual startCompression'); renderStateMachineView(document.body, sms, ['compression diagram', 'tiling diagram'], 'TB', false, false); expect(document.querySelector('.diagram-state-set-dimmed')).toBeNull(); @@ -354,10 +354,10 @@ 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 tilingSet and compressionExplicit \u00B7 actual 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', () => { @@ -365,7 +365,7 @@ describe('state machine view', () => { 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(); }); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 289da27..4533588 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -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 ? `${escapeHtml(focus.receiver)}` : 'the receiver'; - const rejected = `${call ? `${escapeHtml(call)}` : '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 ${expected} \u00B7 actual ${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 `${escapeHtml(call)} 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 ${escapeHtml(call)}` : 'Invalid method call'; } function renderStateErrorSummary(summary: string, stateErrors: StateErrorNavigation): string { @@ -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*/` @@ -173,6 +161,13 @@ function renderLegendItem(kind: string, label: string): string { return `${label}`; } +// 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 => `${escapeHtml(state)}`).join(' or '); } From d3be0f80394e56c6e2f27b8ced54c16c5c39e5de Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 26 Oct 2026 20:29:07 +0000 Subject: [PATCH 2/2] Keep the word state in the state error summary Co-Authored-By: Claude Opus 5.5 --- client/src/webview/views/fsm/fsm.spec.ts | 12 ++++++------ client/src/webview/views/fsm/fsm.ts | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 1145453..455acae 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -127,7 +127,7 @@ describe('state machine view', () => { renderStateMachineView(document.body, [errorMachine], [diagram], 'TB', false, true); const summary = document.querySelector('.diagram-error-text')!; - expect(summary.textContent).toBe('Invalid method call socket.receive() \u00B7 expected unbound or bound or connected \u00B7 actual bound or closed'); + 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'); @@ -144,19 +144,19 @@ describe('state machine view', () => { }, })], [diagram], 'TB', false, true); - expect(document.querySelector('.diagram-error-text')?.textContent).toBe('Invalid method call root.getFirstChild() \u00B7 expected maybeHasChildren \u00B7 actual 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'], - 'Invalid method call socket.receive() \u00B7 expected unbound or bound or connected \u00B7 actual unknown', + 'Invalid method call socket.receive() \u00B7 expected state unbound or bound or connected \u00B7 actual state unknown', ], [ 'every actual is expected', ['bound'], - 'Invalid method call socket.receive() \u00B7 expected unbound or bound or connected \u00B7 actual 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({ @@ -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('Invalid method call param.setCompressionType() \u00B7 expected compressionExplicit \u00B7 actual 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(); @@ -354,7 +354,7 @@ describe('state machine view', () => { renderStateMachineView(document.body, sms, ['tiling diagram', 'compression diagram'], 'TB', false, true); expect(document.querySelector('.diagram-error-text')?.textContent) - .toBe('Invalid method call param.write() \u00B7 expected tilingSet and compressionExplicit \u00B7 actual startTiling and 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 Actual state, not expected', '\u2713 Actual state, expected', 'Expected state']); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 4533588..5e08ae7 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -101,7 +101,7 @@ function getStateErrorSummary(focuses: StateErrorFocus[]): string { const actual = focuses.every(focus => focus.unknownState) ? 'unknown' : renderStateSets(focuses.filter(focus => !focus.unknownState).map(focus => focus.possibleStates)); - return `${renderInvalidCall(call)} \u00B7 expected ${expected} \u00B7 actual ${actual}`; + 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