[CatarinaGamboa]

Brings liquidjava-fsm#17 to the extension, for the verifier's named state sets and states written as values of their sets (liquid-java/liquidjava#498, #510, #511; design in liquid-java/liquidjava#502).

Depends on a liquidjava-fsm 0.2.3 release of liquidjava-fsm#17: until it is on Maven Central, server does not build in CI.

What changes

• server/pom.xml: liquidjava-fsm 0.2.2 → 0.2.3, which reads phase(this) == open, open == phase(this) and phase(this) != open in from/to as the states they name, and reports each diagram's stateSetName.
• StateMachineDTO: passes stateSetName to the client (the liquidjava/fsm request returns the fsm records, so it gets it as is).
• State Machine view: a named state set's diagram is titled with its name, also when it is the class's only state set, so it can be matched with the error message (doorState(d) == closed). A state set without a name keeps its states as the title, as now.

Checked, no change needed

The verifier sends the same shapes to the IDE as before (git diff fbc5e9f6 origin/main): StateErrorContext still names states by their names, and hints are unchanged. Only the text of a state error's message, expected and found changes, to doorState(d) == closed for named sets. The client renders those strings as they come, with the generic highlighter, and nothing in the client parses state names out of message text: the diagram marks and the summary line use errorContext. The verification view shows the new form as is (last screenshot).

Screenshots

Headless VS Code with this branch, liquidjava-fsm#17 installed locally as 0.2.3 and the verifier built from liquid-java/liquidjava main, on this spec (d.lock(); d.open(); as the error):

@StateSet(name = "doorState", value = {"closed", "opened"})
@StateSet(name = "lockState", value = {"unlocked", "locked"})
public class Door {
    @StateRefinement(to = "doorState(this) == closed && lockState(this) == unlocked")
    public Door() {}
    @StateRefinement(from = "doorState(this) == closed && lockState(this) == unlocked", to = "doorState(this) == opened")
    public void open() {}
    @StateRefinement(from = "doorState(this) == opened", to = "doorState(this) == closed")
    public void close() {}
    @StateRefinement(from = "doorState(this) == closed && lockState(this) != locked", to = "lockState(this) == locked")
    public void lock() {}
    @StateRefinement(from = "lockState(this) == locked", to = "lockState(this) == unlocked")
    public void unlock() {}
}

Before (main, fsm 0.2.2), the diagrams are wrong: open and lock go from every state with the whole from as a condition, close and unlock are missing, the summary only names lockState, and the titles are the states. After, the diagrams match the spec, the conditions keep the form the spec wrote, and the titles are the set names:

	Before	After
Show all
Focus on error

The verifier's message for the same error (no change here; shown for context):

Not in this PR

• The verifier bump: main of liquid-java/liquidjava is not released yet. When it is, DiagnosticConverterTest needs the new StateRefinementError constructor argument (display, from #511) and the RefinementError one (aliases); the server code itself compiles against it.
• The walkthrough and README examples stay in the shorthand until the extension ships a verifier that accepts named sets.

Tests

• client: vitest run 124 passed (one new test, fails without the change), typecheck and lint clean
• server: mvn test 35 passed, against liquidjava-fsm#17 installed as 0.2.3 in an isolated local Maven repository

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main:

• [P1] Use a published liquidjava-fsm version (server/pom.xml:175): liquidjava-fsm:0.2.3 cannot be resolved from the configured repositories, so the server cannot build or run its tests. Maven Central lists 0.2.2 as the latest release. Publish the version containing stateSetName() before depending on it.

Response

Known and intended: the PR body says it depends on a liquidjava-fsm 0.2.3 release of liquid-java/liquidjava-fsm#17, as #169 did with 0.2.2. The server was tested locally against #17 installed as 0.2.3 in an isolated Maven repository. Nothing else was found; no changes in this round.

[CatarinaGamboa]

Codex review, round 2

codex exec on git diff origin/main...HEAD, told the round 1 outcome: No findings. The loop ends here.

[CatarinaGamboa]

Clean-code review

Audit of this PR's diff against the clean-code-principles checklist (file:line - [principle] issue):

• client/src/webview/views/fsm/fsm.ts:70 - [core-kiss] the single-diagram shortcut now also checks stateSetName; the alternative (always rendering through renderStateSetDiagram) would change the unnamed single-set layout. Kept.
• client/src/webview/views/fsm/fsm.ts:86 - [name-meaningful] title names the one choice (name or states) and escapes once instead of per state. Fine.
• server/src/main/java/dtos/fsm/StateMachineDTO.java:22 - [core-dry] the DTO repeats the fsm record's components, as it already did for the others; it exists to add errorContext. No change.
• server/src/test/java/dtos/fsm/StateMachineDTOTest.java:56 - [lean tests] the name is asserted in the existing DTO test instead of a new one.

No findings to fix; no changes.