[CatarinaGamboa]

Closes #173.

Uses liquidjava-fsm 0.2.3 (which includes liquidjava-fsm#16) and verifier 0.0.37, both on main since #179. Rebased onto main on 2026-11-10: the server/pom.xml bump is gone; server tests pass (39 with #178 merged in too).

Why

A state error can be on a method declared in a subclass's spec (Frame.setUndecorated) while the state set is declared in a superclass's spec (Window). In that case the State Machine view could not explain the error:

• With verifier 0.0.36 (no state context), it showed Window's diagram without setUndecorated and marked no states (the issue's screenshot).
• With verifier main (Give state hints when the state set or methods come from the receiver's supertypes liquidjava#464), the context names java.awt.Frame. The parser then found Frame's spec, which has no @StateSet, so the error had no diagram at all.

What

• liquidjava-fsm#16. The parser merges the specs of a class's supertypes, following the rule from liquidjava#464: state sets of the class and then of its supertypes, nearest first; for each method, the class's own refinement, otherwise that of the nearest type that declares it. The details are in that PR.
• StateRefinementErrorDTO. It parses the diagrams for the context's receiverClass. It reads the declaration's file plus the files of the state sets and state refinements the verifier registered (ContextHistory), so specs split across files are found, including a supertype spec with methods but no state set. Without a context it behaves as before (first class of the declaration's file).
• Known limit. A project class that extends an unannotated project class in a file the verifier registered nothing for stops the walk there, so that class's diagram leaves out the states further up. The parser only sees the spec files.

No verifier change is needed. liquidjava#464 already sends the context with the receiver's states for this case. The view needs a verifier release with #464 (after 0.0.36). With 0.0.36 nothing changes for this case: that verifier sends no context, so the view still shows the first class of the declaration's file (Window in the issue's file).

Screenshots

Both columns use verifier main @ 9e4b5e64.

	Before (main)	After
Issue reproducer (host.pack(); host.setUndecorated(true);)
Study exercise A1_09 (LITIENGINE GameWindow)

In A1_09 the actual state shows as "unknown" because the verifier finds both displayable and notDisplayable possible (it depends on the path). notDisplayable is marked as the expected state, and setUndecorated is the failing call.

I did not take a split-files screenshot. With FrameRefinements.java read before WindowRefinements.java, the verifier stops with liquid-java/liquidjava#461 before it reaches the state error. StateRefinementErrorDTOTest covers that layout.

Tests

• server mvn test: 39 passed, 0 failures (liquidjava-fsm 0.2.3 built locally from Update README #16, verifier 0.0.36). New StateRefinementErrorDTOTest:
  • Specs in two files: the diagram is java.awt.Frame, with setUndecorated, dispose and pack on Window's states; displayable is marked invalid and notDisplayable accepted.
  • Without a context: the first class of the declaration's file, as before.
  • A JFrame spec over a method-only Frame spec and Window's state set: all their methods are drawn.
  • The verifier run on that fixture: the files of all three specs are selected.
• client npm run test:unit: 123 passed. npm run test:typecheck: clean. npm test (VS Code): 9 + 1 passing.

Overlap with #172

None. #172 changes only the client webview. This PR changes only the server and its fsm dependency.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

Run over both diffs (this PR and liquid-java/liquidjava-fsm#16). Codex's findings, verbatim:

I found two issues in the server’s file selection. I could not run tests, as requested.

1. Method-only ancestor specs are omitted — vscode-liquidjava/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java:37 and :63. The DTO supplies the declaration file plus files found through GhostState. An ancestor spec with method refinements but no @StateSet contributes no ghost file, so its transitions never reach the parser. For example, a three-file hierarchy with the failing method in Frame, a method-only Dialog spec, and the state set in Window will omit Dialog’s methods. Fix: gather the relevant ancestor spec files from registered refinements as well as state sets. Add a three-file test with a method-only middle ancestor.

2. One unrelated file can erase the diagram — StateRefinementErrorDTO.java:63 and liquidjava-fsm/src/main/java/liquidjava/fsm/StateMachineParser.java:123. stateSetFiles() passes every registered ghost file to one Spoon build, including files unrelated to the target hierarchy. If any path cannot be read or parsed, the parser’s catch at line 113 returns an empty list for the entire diagram. It also makes each error parse all registered state-set files. Fix: select files for the target class and its ancestors before building the model, and handle a bad ancillary file without discarding the usable specs. Test with an unrelated unavailable file.

[CatarinaGamboa]

Round 1 replies

1. Method-only ancestor specs are omitted. Fixed in 1ce5b5b. I reproduced it: the spec files came only from ghost states, so a Frame spec without @StateSet between JFrame and Window was never read. specFiles() now also includes the files of the verifier's state-refined methods.
   • StateRefinementErrorDTOTest.showsTheMethodsOfASuperclassSpecWithoutStateSet: three files, the methods are setDefaultCloseOperation, setUndecorated, dispose, pack.
   • readsTheSpecsOfTheStateSetsAndOfTheMethodsWithoutStateSet: runs the verifier on that fixture and checks that all three spec files are selected.
   • The parser side is tested in liquidjava-fsm#16 (testMethodsInheritedFromASpecWithoutStateSet, 0ae018e).
2. One unrelated file can erase the diagram. Partly fixed in liquidjava-fsm 0ae018e.
   • Missing file: reproduced. A path that no longer exists made Spoon throw, and the diagram was empty. The parser now skips files that do not exist (testMissingFileDoesNotDiscardTheOthers).
   • File that does not parse: not reproduced. Spoon builds the model without classpath and still returned the diagram.
   • Picking only the hierarchy's files (declined): the server cannot resolve the receiver's supertypes before parsing. The parser does that, and it only keeps the types in the hierarchy. The files are the specs the verifier just read, usually a few, and they are parsed only when there is a state error.

Server mvn test: 39 passed. fsm mvn test: 32 passed. Client unit: 123 passed. VS Code: 9 + 1 passing. The UI is unchanged for the screenshots' fixtures.

[CatarinaGamboa]

Codex review, round 2

Run over both diffs (this PR and liquid-java/liquidjava-fsm#16). Codex's findings, verbatim:

I found two correctness gaps and one language server performance risk. I did not run commands or tests, as requested.

• liquidjava-fsm StateMachineParser.java:174–179, 245–250 — only one spec is read per target class. getType returns the first type whose @ExternalRefinementsFor names the class. If two files specify the same class—one declaring its @StateSet, the other refining a method—the second is ignored even though the new API accepts both files. Collect all matching specs for each target class and add a test that splits one class’s state set and method refinements across files.

• vscode-liquidjava StateRefinementErrorDTO.java:35–42, 58–62; liquidjava-fsm StateMachineParser.java:126–132 — an unrelated spec can suppress the error’s diagram. specFiles() passes every registered spec file to one Spoon model build. If an unrelated file cannot be parsed, parseAll catches the failure and returns no diagrams, including for a valid declaration file. Limit parsing to the target hierarchy, or isolate file failures so a usable spec still produces a diagram. Test with a valid Frame/Window pair plus an invalid unrelated spec.

• vscode-liquidjava StateRefinementErrorDTO.java:35–42 — every error rebuilds the same full model. A verification with many state errors parses all registered spec files once per DTO. Cache the parsed diagrams or model for the verification, and reuse them across errors.

The new test at StateRefinementErrorDTOTest.java:63–68 also changes the global CommandLineLauncher.cmdArgs.lspMode without restoring it; use try/finally to keep tests independent.

[CatarinaGamboa]

Round 2 replies

1. Only one spec is read per target class. Declined. This is how the parser already behaved for a single file. Merging several specs of one class would also need de-duplication. The study exercise A1_09 has the same Window and Frame specs in two files, so merging them would draw each state set twice and shift the stateSet indexes the verifier's states use. Keeping the first spec of each class shows the right diagram for that case. Splitting one class's state set and methods across two files can be its own issue if we need it.
2. An unrelated spec can suppress the diagram. Declined, same as round 1. A missing file is now skipped (liquidjava-fsm 0ae018e). A file that does not parse still gives the diagram: I checked with class Broken { void m( { } next to the Frame/Window specs.
3. Every error rebuilds the same model. Declined. Measured with the A1_09 specs (two files): a warm parseAll takes 130 to 225 ms, and parsing only the declaration's file takes 143 ms. The cost grows with the number of spec files, not with the project. A per-verification cache would add state to the DTOs for no visible gain.
4. lspMode not restored in the test. Fixed in a0b32aa with try/finally.

Server mvn test: 39 passed. Main code unchanged in this round.

[CatarinaGamboa]

Codex review, round 3

Run over both diffs (this PR and liquid-java/liquidjava-fsm#16). Codex's findings, verbatim:

I found three correctness gaps in the supplied changes. I reviewed the provided code only; I did not run commands.

• vscode-liquidjava — StateRefinementErrorDTO.java:55–57: split specs still produce no diagram without context. The null-context branch parses only the declaration file. For an error declared in B_FrameRefinements.java, that file has no @StateSet, so the result is empty even when the Window spec is in specFiles. This contradicts the PR’s stated behavior with verifier 0.0.36. Fix: select the declaration’s class, then parse it with the collected spec files in both branches. Add a test using FRAME, WINDOW, and a null context; the current null-context test starts from WINDOW and misses this case.

• liquidjava-fsm — StateMachineParser.java:174–179, 245–252: only the first spec for a class is used. getType returns one matching type. If two input files both use @ExternalRefinementsFor("java.awt.Frame"), a state set or method in the second spec is lost. Fix: collect all matching specs for each class and merge their state sets and methods in a defined order. Test a state set and method split between two specs for the same target class.

• liquidjava-fsm — StateMachineParser.java:122–132, 189–209: a missing intermediate source type cuts off inheritance. The model contains only the supplied spec files. For project classes Child extends Middle extends Parent, if Middle has no spec and its source file is not supplied, the hierarchy walk cannot reach Parent’s state set. The verifier can see that relationship in its project model, so diagram state-set indexes may diverge from the error context. Fix: supply the relevant source hierarchy to Spoon, or derive the hierarchy from verifier-provided type information. Test an unannotated intermediate class in a separate file.

[CatarinaGamboa]

Round 3 replies

1. Split specs without a context. The finding is right, and the PR description was wrong about it, so I corrected the description. I did not change the code. With verifier 0.0.36 there is no context, so the server cannot tell which class the error is about, and it keeps the old behavior (first class of the declaration's file). Guessing the class from the declaration's position would be a separate heuristic. Verifier main sends the context, which covers this case. The study needs a verifier release with liquidjava#464 anyway, to mark the states.
2. Only the first spec of a class. Declined, see round 2: merging duplicate specs (A1_09 has two copies of the Window/Frame specs) would duplicate the state sets.
3. Missing unannotated intermediate source class. Declined, and now listed in the PR description as a known limit. The class's own state sets come first, as in the verifier, so a cut superclass chain usually only leaves out sets at the end, and the diagram is partial rather than wrong. There is one exception: if the class also implements an interface with its own state set, that set moves up in the order and its index no longer matches the verifier's. Fixing it would mean giving the parser the whole project's sources on each error.

No code change in this round.

[CatarinaGamboa]

Codex review, round 4

Run over both diffs (this PR and liquid-java/liquidjava-fsm#16). Codex's findings, verbatim:

I found two correctness gaps and one test gap across the PRs. I could not run tests, as requested.

• liquidjava-fsm/src/main/java/liquidjava/fsm/StateMachineParser.java:174-178,245-250 — Only one spec is read per target class. getType returns the first type whose @ExternalRefinementsFor names the target. If two spec files refine the same class, the second file’s state sets and methods disappear from the diagram, while the verifier can register both. Collect all matching specs for each target, merge their refinements, and deduplicate state sets using the verifier’s rule.

• liquidjava-fsm/src/main/java/liquidjava/fsm/StateMachineParser.java:192-209 and vscode-liquidjava/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java:55-59,65-71 — An unannotated project class breaks inheritance. The server passes registered spec files only. When an intermediate project superclass has no spec and cannot be resolved from those files, the parser stops before reaching a higher superclass’s state set. This is the stated known limit, but it leaves ordinary project hierarchies with an incomplete diagram. Supply the verifier’s resolved hierarchy, or make the relevant project source types available to the parser.

• vscode-liquidjava/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java:64-73 — The file-selection test does not test the DTO’s actual path. It checks that specFiles() contains three files, then the other tests pass file lists directly. Add an integration assertion that constructs a StateRefinementErrorDTO from a verifier error and checks its diagram; include two spec files targeting the same class to cover the first finding.

[CatarinaGamboa]

Round 4 replies

1. Only one spec per target class. Declined, as in rounds 2 and 3.
2. Unannotated intermediate project class. Declined, as in round 3. It is listed as a known limit.
3. No test from a real verifier error to the DTO's diagram. Declined for now. The server builds against verifier 0.0.36, which sends no context for this case, so that test could only check the old behavior. I ran the full path locally against verifier main @ 9e4b5e64. A scratch test verified the issue's fixture and built StateRefinementErrorDTO from the real error. It gave java.awt.Frame with setUndecorated, dispose and pack, and the verifier's states marked. The screenshots show the same in VS Code. That test should be added with the verifier bump that includes liquidjava#464.

Codex's remaining findings repeat ones already declined, so the review loop stops here. No code change in this round.