Repository navigation
Draw only the diagram and look up classes by name - #12
Merged
Merged
Conversation
The verifier now reports the receiver's possible and accepted states on StateRefinementError#getContext, so the error context fsm re-derived from the predicates' text is removed, along with parseWithErrorContext. parse(uri, className) picks a class in a file that declares several. A test checks that the verifier's states are states of the diagram. Bumps the verifier to 0.0.36 and Spoon to 11.5.0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa
marked this pull request as ready for review
October 24, 2026 23:52
This was referenced Oct 25, 2026
CatarinaGamboa
added a commit
to liquid-java/vscode-liquidjava
that referenced
this pull request
Oct 25, 2026
## 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
fsm used to build the error overlay by reading the text of the failing call's
expectedandfoundpredicates again. The verifier now reports its own answer onStateRefinementError#getContext()(liquidjava#421): the receiver, its class, the called method, and the possible and accepted states. That answer comes from the SMT solver, so the text reading could only disagree with it. fsm now only does what needs no verification: drawing the class's state machine.What
parseWithErrorContext, theStateMachineErrorContextrecord,StateMachine#errorContext, and the text evaluation of found/expected. This is breaking, so it releases as 0.2.0.parse(uri, className)chooses the class by its qualified name, or by the@ExternalRefinementsForname for specs, instead of taking the first type in the file. The vscode server passes the error'sreceiverClass, so a file that declares several classes shows the right diagram.parse(uri)is unchanged, and the MCP server only uses that.Tests
testClassSelectedByNamechecks the class lookup.testVerifierStatesAreStatesOfTheDiagramruns the verifier on the door, tree and udp clients. For every state error it checks that the verifier's possible and accepted states, in the first state set, are states of fsm's diagram. This is the contract between the two repos.The DatagramSocket fixture had preconditions with
old(this)(closed(this) && connected(old(this))), which the verifier cannot build a machine for (liquidjava#422).old()should not appear in a precondition, so they are nowclosed(this), as in the barista spec. All 24 tests pass on 0.0.36.🤖 Generated with Claude Code