[CatarinaGamboa]

Closes #515

What and why

Since #511 the headline of a state error shows a state of a named set as a value of its set (lockState(d) == locked), but the hints and "Refinement declared here" still used the shorthand (locked, closed(this)). One message used several notations for the same states. Now:

1. Hints name each state of a named set exactly as the headline does, with the receiver: lockState(d) == locked (PM decision). The sentences that said "d is X" or "needs it to be X" now state the condition: when it returns true, undoState(um) == undoable, this call needs undoState(um) == undoable, When doorState(d) == closed and lockState(d) == locked, d can call: .... In that form, a state of an unnamed set in the same class is shown as the headline shows it too, closed(d). Classes with no named set keep the current wording (In state created, f can call: ...).
2. Alternatives in hint state lists are grouped: (a and b) or (c and d). This applies to unnamed sets too, since the problem is the same.
3. "Declared here" stays verbatim (it is source). When the highlighted declaration writes states of named sets in the shorthand, one where line under it says what they mean, for those states only: where closed(this) means doorState(this) == closed, .... It is the same where style the alias notes of refinement errors use.

Display only: the VC, the verdict, which hints are given and the category do not change.

Same rule as the headline. Hints and the gloss both use the rule of StateValues.toSetForm. Its set lookup is now exposed as StateValues.setNameOf (the hints use it), and the gloss runs the error's own display rewrite on each state(arg) call in the declaration. So:

• states of unnamed (stateN) sets keep the shorthand;
• a state name shared by sets with different names keeps the shorthand, so no set is guessed. So does a set name shared by sets of different classes, e.g. a class and its superclass;
• a negation is never turned into a value: hints describe the machine's states as before, and the gloss explains locked(this), never !locked(this), so !locked(this) reads as !(lockState(this) == locked). A declaration in value form (lockState(this) != locked) gets no gloss, since it already uses the headline's notation.

Before / after (CLI, ANSI colours stripped)

ErrorStateHintMultipleSets (sets doorState, lockState)

Before:

State Refinement Error: found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked
26 |         ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets();
27 |         d.lock();
28 |         d.open(); // Expect: State Refinement Error
   |         ^^^^^^^^^
29 |     }
30 | }

Hints:
  - Call d.unlock() before this call to move d from locked to unlocked
  - In state closed and locked, d can call: unlock()

door/ErrorStateHintMultipleSets.java:28

--> Refinement declared here:
12 | 
13 |     @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)")
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14 |     public void open() {}

door/ErrorStateHintMultipleSets.java:13

After:

State Refinement Error: found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked
26 |         ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets();
27 |         d.lock();
28 |         d.open(); // Expect: State Refinement Error
   |         ^^^^^^^^^
29 |     }
30 | }

Hints:
  - Call d.unlock() before this call to move d from lockState(d) == locked to lockState(d) == unlocked
  - When doorState(d) == closed and lockState(d) == locked, d can call: unlock()

door/ErrorStateHintMultipleSets.java:28

--> Refinement declared here:
12 | 
13 |     @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)")
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14 |     public void open() {}
  where closed(this) means doorState(this) == closed, unlocked(this) means lockState(this) == unlocked

door/ErrorStateHintMultipleSets.java:13

The same spec in value form with != (from = "doorState(this) == closed && lockState(this) != locked")

Before:

State Refinement Error: found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) != locked
26 |         ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets();
27 |         d.lock();
28 |         d.open(); // Expect: State Refinement Error
   |         ^^^^^^^^^
29 |     }
30 | }

Hints:
  - Call d.unlock() before this call to move d from locked to unlocked
  - In state closed and locked, d can call: unlock()

doorne/ErrorStateHintMultipleSets.java:28

--> Refinement declared here:
12 | 
13 |     @StateRefinement(from = "doorState(this) == closed && lockState(this) != locked", to = "opened(this)")
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14 |     public void open() {}

doorne/ErrorStateHintMultipleSets.java:13

After (no gloss: the declaration is already in value form; the hints name the machine's states as before, only in the new notation):

State Refinement Error: found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) != locked
26 |         ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets();
27 |         d.lock();
28 |         d.open(); // Expect: State Refinement Error
   |         ^^^^^^^^^
29 |     }
30 | }

Hints:
  - Call d.unlock() before this call to move d from lockState(d) == locked to lockState(d) == unlocked
  - When doorState(d) == closed and lockState(d) == locked, d can call: unlock()

doorne/ErrorStateHintMultipleSets.java:28

--> Refinement declared here:
12 | 
13 |     @StateRefinement(from = "doorState(this) == closed && lockState(this) != locked", to = "opened(this)")
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14 |     public void open() {}

doorne/ErrorStateHintMultipleSets.java:13

state_hint_study_undo_manager_error, sets named phase / undoState / redoState, with if (um.canRedo()) um.redo(); um.undo();

Before:

State Refinement Error: found (#canRedo_result ? redoState(um@27) == redoable : redoState(um@27) == notRedoable) && undoState(um@27) == undoState(#getUndoManager_result) && (#canRedo_result ? undoState(um) == undoable && redoState(um) == notRedoable && phase(um) == phase(#getUndoManager_result) : (#canRedo_result ? redoState(um) == redoable : redoState(um) == notRedoable) && phase(um) == phase(#getUndoManager_result) && undoState(um) == undoState(#getUndoManager_result)) but expected undoState(um) == undoable
26 |         CountingUndoManager um = frame.getUndoManager();
27 |         if (um.canRedo()) um.redo();
28 |         um.undo(); // Expect: State Refinement Error
   |         ^^^^^^^^^^
29 |     }
30 | 

Hints:
  - Guard this call with if (um.canUndo()): when it returns true, um is undoable
  - In state undoable and notRedoable or notUndoable and notRedoable, um can call: canUndo(), canRedo() (and possibly others)

undo/EditCommand.java:28

--> Refinement declared here:
62 | 
63 |     @StateRefinement(from="undoable(this)", to="notUndoable(this) && redoable(this)")
   |                            ^^^^^^^^^^^^^^
64 |     void undo();

undo/UndoManagerRefinementsExpert.java:63

After:

State Refinement Error: found (#canRedo_result ? redoState(um@27) == redoable : redoState(um@27) == notRedoable) && undoState(um@27) == undoState(#getUndoManager_result) && (#canRedo_result ? undoState(um) == undoable && redoState(um) == notRedoable && phase(um) == phase(#getUndoManager_result) : (#canRedo_result ? redoState(um) == redoable : redoState(um) == notRedoable) && phase(um) == phase(#getUndoManager_result) && undoState(um) == undoState(#getUndoManager_result)) but expected undoState(um) == undoable
26 |         CountingUndoManager um = frame.getUndoManager();
27 |         if (um.canRedo()) um.redo();
28 |         um.undo(); // Expect: State Refinement Error
   |         ^^^^^^^^^^
29 |     }
30 | 

Hints:
  - Guard this call with if (um.canUndo()): when it returns true, undoState(um) == undoable
  - When (undoState(um) == undoable and redoState(um) == notRedoable) or (undoState(um) == notUndoable and redoState(um) == notRedoable), um can call: canUndo(), canRedo() (and possibly others)

undo/EditCommand.java:28

--> Refinement declared here:
62 | 
63 |     @StateRefinement(from="undoable(this)", to="notUndoable(this) && redoable(this)")
   |                            ^^^^^^^^^^^^^^
64 |     void undo();
  where undoable(this) means undoState(this) == undoable

undo/UndoManagerRefinementsExpert.java:63

The fixture's two other errors change the same way: this call needs redoState(undoManager) == redoable, when it returns true, redoState(undoManager) == redoable, and where redoable(this) means redoState(this) == redoable.

Decided by the PM

• Hints use the headline's exact form with the receiver (lockState(d) == locked), including grouped alternatives and the guard and "needs" sentences.
• The gloss keeps the spec's own form with (this): where closed(this) means doorState(this) == closed, ....

Still open for the PM

• Grouping. Parentheses appear only when there are several alternatives and an alternative has several states. The issue also suggests naming only the set that matters (e.g. only undoState). That would change which states a hint names, not only how they are written, so it is not in this PR.

IDE

Hints reach vscode-liquidjava as plain message text, so the new notation shows there with no change. The extension does not show the declaration excerpt, only a location link, so the gloss needs a server and client change: liquid-java/vscode-liquidjava#181 (label study).

Tests

The existing exact-message tests in TestStateHints are updated, and one test is added. Each one fails on main:

• callSequenceNamesOnlyTheStateSetsItChanges: the hints for doorState/lockState (named sets), in the headline form.
• queryWrittenWithItsStateSetIsOfferedAsAGuard: needed state and guard for set lock (named set, value-form spec).
• joinsAreNotTakenForAnUnknownState: grouping, with unnamed sets, which keep the shorthand.
• foundKeepsANamedStateSetByItsName: also checks the where line under the declaration.
• New: setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand (fixture ErrorStateSetNameInSuperclass), from Codex round 1. When a class and its superclass each have a set named phase, the headline (Show the states of named sets as values of their sets in state errors #511's rule) and the hints printed phase(c) == ready && phase(c) == busy, which reads as two values of one set. StateValues.setNameOf, shared by both, now keeps the shorthand in that case.

The other hint tests use unnamed sets and pass unchanged, so the shorthand is kept there. The full suite passes locally (728 tests).

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

Audit of this PR's new code only (clean-code-principles); the PM's small-PR rules take precedence.

• StateRefinementError.java ON_A_NAME: [name-meaningful] the name does not say it matches a call. Fixed: renamed to CALL_ON_A_NAME (in the next push).
• StateHints.forCall: [func-few-arguments] now 7 parameters. Declined: bundling them needs a new parameter class, which the small-PR rule rules out; the new one is a single function.
• AuxStateHandler.stateHints: [core-dry] the set == state text repeats the shape toSetForm builds as an expression. Declined: the set lookup itself is shared (StateValues.setNameOf, which toSetForm now uses too); only the 3-character join is repeated, and building an expression to print it would be more code.
• LJDiagnostic.getDeclarationText: [core-dry] reads the declaration's file again after getSnippet has read it. Declined: it runs only when an error is printed, and sharing the read would mean reshaping getSnippet.
• StateRefinementError.getDeclarationNotes: [core-kiss] finds states with a regex over source text instead of the parsed predicate. Declined: the note explains the text as written in the excerpt, and the parsed from has this substituted and can be a disjunction of several refinements. Each match goes through the same display rewrite as the headline, so a call that is not a state of a named set gets no note.
• StateHints.join: [func-single-purpose] names and groups at once. Kept: it is one short expression, and the grouping only makes sense together with the joining.

No SOLID or layering issues: the hint wording stays in StateHints, the set lookup in StateValues, and printing in LJDiagnostic.

[CatarinaGamboa]

Codex review, round 1

1. Inherited sets with the same set name give a false hint. If a class and its superclass each declare a set named phase (ready/done and busy/idle), a failed use() with from = "ready(this) && busy(this)" gets the hint In state phase == idle and phase == ready, which reads as an impossible value of one set. A shared state name across inherited sets gives an ambiguous ready and ready.
2. Test gap: multiline declarations. getDeclarationText reads only the first line of the declaration, so a text-block from whose states are on later lines gets no gloss. The only gloss assertion uses a single-line string.

[CatarinaGamboa]

Reply to Codex review, round 1

1. Fixed (9a1d86c). Confirmed with the CLI: on this branch both the hints and the headline (the Show the states of named sets as values of their sets in state errors #511 rule) printed phase(c) == ready && phase(c) == busy. StateValues.setNameOf, which the headline and the hints share, now keeps the shorthand when sets of different classes have that set name. Now: found ready(c) && idle(c) but expected ready(c) && busy(c), with hints move c from idle to busy and In state idle and ready. The new test TestStateHints#setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand (fixture ErrorStateSetNameInSuperclass) fails without the fix. A state name shared by inherited sets already kept the shorthand, both in the headline and in the hints, since Show the states of named sets as values of their sets in state errors #511 (several set names give no set).
2. Declined. The excerpt itself shows only the first line of the declaration, and the gloss is meant to explain only the states shown in it (as the issue asks). A gloss for states on lines that are not shown would explain text the reader cannot see.

Full suite passes locally (728 tests).

[CatarinaGamboa]

Codex review, round 2

1. Off by one in getDeclarationText. Codex says the Spoon end column is inclusive and substring's end is exclusive, so the last ) would be dropped. Then from = "closed(this) && unlocked(this)" would explain only closed(this), and from = "closed(this)" would get no note.
2. Test gaps. Negation (from = "!ready(this)") and disjunction (from = "ready(this) || busy(this)") in a named set are not tested for message, note and hints together, and the superclass shared-name test does not check the declaration note.

[CatarinaGamboa]

Reply to Codex review, round 2

No code changes this round.

1. Declined, not a bug. Spoon columns are 1-based with an inclusive end. Converting to 0-based gives substring(column - 1, endColumn), whose exclusive end is exactly the inclusive 1-based end, as getSnippet already does for the ^ markers. The CLI output in the PR body shows both closed(this) and unlocked(this) explained. TestStateHints#foundKeepsANamedStateSetByItsName checks that line and passes.
2. Declined (lean tests). The hints do not depend on how the spec is written: they name the machine's states, so a negated or disjunctive from takes the same path the updated tests cover. The negated form in the gloss is shown in the PR body (no note for value form; !locked(this) gets the note for locked(this)). Grouping of alternatives is covered by joinsAreNotTakenForAnUnknownState. The superclass case goes through the same setNameOf check for the note as for the hints, which the new test covers. The PM asked for only the tests that fail without the fix.

[CatarinaGamboa]

Codex review, round 3

No findings. Codex rebuilt the verifier, ran TestStateHints and ran the CLI on fresh copies of the named-set and superclass cases. It found no correctness bug, no message that misstates what was checked, and no test gap that would fail without the fix. The review loop ends here.

[CatarinaGamboa]

Codex review, round 4

On the new diff (hints in the headline's form with the receiver, as the PM decided; commit e2ce936). No findings. Codex rebuilt the verifier and ran the CLI on fresh inputs: named sets, named and unnamed sets mixed in one class, and a field receiver this.door. Headline, hints and declaration note agreed in each case. The earlier declines were given to it and not repeated. The full suite passes locally (728 tests).

[CatarinaGamboa]

Codex review, round 5

On the AST-based declared-here note (commit 361d463). No correctness bug found. One test gap: the gloss assertion (ready(this)-style states) would also pass with the old regex. Codex suggests a test with from = "ready(old(this))", which the regex could not match. The CLI now prints where ready(old(this)) means phase(old(this)) == ready for it.

Declined: the regex is deleted, so a test that only fails against deleted code protects nothing going forward. old(this) in a from is also not a spec anyone writes. The existing assertion still checks the note end to end, as the PM asked. The full suite passes locally (728 tests).

[CatarinaGamboa]

Re: "why do we need CALL_ON_A_NAME if we have an AST already?"

You're right, it's gone (commit 361d463).

Why the regex existed. The note has to explain what the source wrote: closed(this) gets a note, doorState(this) == closed does not. By the time the error is built, the only AST at hand is the from after StateValues.toShorthand, which reads doorState(this) == closed as closed(this). That AST can't tell the two apart, so I scanned the text of the declaration instead. That was fragile: it depended on the printed line and on display leaving non-states unchanged.

What replaced it.

• AuxStateHandler.getStates already parses the from string with the RJ parser before toShorthand runs. That parsed predicate is now kept on ObjectState as writtenFrom (and copied by clone).
• Where the error is built, AuxStateHandler walks the FunctionInvocation nodes of the declaration's writtenFrom. It explains those that are a state of a named set, using StateValues.setNameOf/toSetForm, the same lookup the headline uses: where closed(this) means doorState(this) == closed, ....
• The notes go to StateRefinementError as a list. LJDiagnostic only prints them and no longer reads or scans source text.

The output is unchanged for the PR's examples. A value-form from, ghost functions and aliases get no note. The full suite passes.