GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — Draw only the diagram and look up classes by name by CatarinaGamboa · Pull Request #12 · liquid-java/liquidjava-fsm

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 24, 2026 •
edited
Loading

Uh oh!

There was an error while loading. Please reload this page.

Copy link
Copy Markdown
Contributor

Why

fsm used to build the error overlay by reading the text of the failing call's expected and found predicates again. The verifier now reports its own answer on StateRefinementError#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

  • Removed: parseWithErrorContext, the StateMachineErrorContext record, StateMachine#errorContext, and the text evaluation of found/expected. This is breaking, so it releases as 0.2.0.
  • Added: parse(uri, className) chooses the class by its qualified name, or by the @ExternalRefinementsFor name for specs, instead of taking the first type in the file. The vscode server passes the error's receiverClass, so a file that declares several classes shows the right diagram. parse(uri) is unchanged, and the MCP server only uses that.
  • Bumped: the verifier to 0.0.36 and Spoon to 11.5.0, the version the verifier now uses.

Tests

  • testClassSelectedByName checks the class lookup.
  • testVerifierStatesAreStatesOfTheDiagram runs 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 now closed(this), as in the barista spec. All 24 tests pass on 0.0.36.

🤖 Generated with Claude Code

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

All reactions
CatarinaGamboa and others added 2 commits October 25, 2026 00:48
@CatarinaGamboa @claude
Draw only the diagram and look up classes by name
8573a29
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 <[email protected]>
@CatarinaGamboa @claude
Drop old() from the DatagramSocket fixture's preconditions
ecdac78
Co-Authored-By: Claude Opus 5.5 <[email protected]>
@CatarinaGamboa
CatarinaGamboa marked this pull request as ready for review October 24, 2026 23:52
@CatarinaGamboa
CatarinaGamboa merged commit 7fdc750 into main Oct 24, 2026
2 checks passed

Uh oh!

There was an error while loading. Please reload this page.

This was referenced Oct 25, 2026
Return one machine per @StateSet #8
Closed
Show the verifier's states of a state error on the state machine liquid-java/vscode-liquidjava#160
Merged
CatarinaGamboa added a commit to liquid-java/vscode-liquidjava that referenced this pull request Oct 25, 2026
@CatarinaGamboa @claude
Show the verifier's states of a state error on the state machine (#160)
f1c258a
## 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 <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Uh oh!

There was an error while loading. Please reload this page.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Uh oh!

There was an error while loading. Please reload this page.

1 participant

@CatarinaGamboa
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.
You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.