[CatarinaGamboa]

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:

{"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 (Show one state machine diagram per @StateSet #115, Highlight state errors in the relevant @StateSet diagram #116, Return one machine per @StateSet 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