[CatarinaGamboa]

Refs #435 (first part: named sets only; carrying a set per branch stays open).

What

@StateSet takes an optional name:

@StateSet(name = "phase", value = {"start", "canEdit", "end"})
@StateSet(name = "undo",  value = {"undoable", "notUndoable"})
@StateSet(name = "redo",  value = {"redoable", "notRedoable"})

A named set's ghost function is called by that name instead of the generated stateN. Messages, hints, simplification steps and the equalities that keep unmentioned sets (AuxStateHandler.getMissingStates) show redo(um) instead of state3(um). Specs can use the name anywhere a ghost works, for example to = "return ? undoable(this) : undo(this) == undo(old(this))". It works in classes, interfaces and @ExternalRefinementsFor specs. Unnamed sets keep stateN with the same numbering, so existing specs behave the same.

Checks, all reported as Error (CustomError, the same kind as "State names must start with lowercase"), on the name:

• not a string literal (e.g. a constant)
• not an identifier starting with a lowercase letter, or old/true/false
• already the name of a state, a @Ghost/@RefinementPredicate ghost or another set of the class (generated stateN included). An alias can't clash, because alias names start with an uppercase letter.

Before / after

Study variant A1_56 (redo guarded, undo not), with the names phase/undo/redo on the spec:

Before:

State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && state2(undoManager@70) == state2(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && state1(undoManager) == state1(#getUndoManager_result) && ... but expected undoable(undoManager)

After:

State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && undo(undoManager@70) == undo(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && phase(undoManager) == phase(#getUndoManager_result) && ... but expected undoable(undoManager)

ErrorStateHintMultipleSets with its sets named doorState and lockState:

- found closed(d@26) && unlocked(d@26) && locked(d) && state1(d) == state1(d@26) but expected closed(d) && unlocked(d)
+ found closed(d@26) && unlocked(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)

New errors:

Error: State set name 'Door' must be an identifier that starts with a lowercase letter
Error: State set name 'locked' is already the name of a state of ErrorStateSetNameOfAState
Error: State set name 'lock' is already the name of a ghost of ErrorStateSetNameOfAGhost
Error: State set name 'door' is already the name of another state set of ErrorStateSetNameOfAnotherSet
Error: State set name must be a string literal

Tests (each fails on main)

• state_hint_study_undo_manager_correct: an external spec with named sets. canUndo() keeps its undo set by name (undo(this) == undo(old(this))) when it returns false. On main the name is unknown, so this fails.
• ErrorStateSetNames: invalid name and clashes with a state, a ghost and another set.
• TestStateHints#foundKeepsANamedStateSetByItsName: exact message with doorState(d).

Full suite passes locally (714 tests). The 6 study exercises and the 19 study variants give byte-identical output to main without names. With names on every multi-set exercise spec, the verdict and line stay the same.

API release needed

name() is new in liquidjava-api. The in-repo api is still 0.0.7, which is already published without name. Reactor builds from the root (CI and the shaded jar) use the in-repo module. A standalone build of the verifier, or any user project (VS Code study projects included), resolves the published 0.0.7, where @StateSet(name = ...) does not compile. Before anyone uses names: ./release.sh api (→ 0.0.8, which also bumps the verifier/example dependency), then a verifier release. Nothing is published in this PR.

Notes

• old works on the receiver, as for every ghost: undo(old(this)). old(undo(this)) (the form in the issue) is not supported for any ghost today.
• A to that only mentions the set function (e.g. undo(this) == ... without any of its states) does not count as mentioning the set, so the keep equality is still added (same as for stateN today).
• vscode-liquidjava (not changed here): server/.../GhostDTO marks states with the regex ^state\d+\(_\) == \d+$. States of a named set would show as "ghost" in autocomplete and the context view. Use ghostState.getParent() != null instead. Set names are not offered in autocomplete, because ContextHistory only carries GhostStates. The state machine view (liquidjava-fsm) reads value of the first @StateSet, so it is unaffected (fsm#8 could use names as titles).

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1 (run locally before the first push)

• [P2] Resolve constant expressions used as state-set names (TypeChecker.java): @StateSet(name = DOOR, ...) with a constant was silently treated as unnamed. Fixed in 5dd2b84: a name that is not a string literal is reported (State set name must be a string literal), like other spec strings that must be literals.

[CatarinaGamboa]

Codex review, round 2

• [P2] Preserve the known-undoable case for canUndo (fixture UndoManagerRefinementsExpert): replacing both canUndo() refinements with the named-set one dropped from="undoable(this)", to="return && undoable(this)". Fixed in 1e30bc3: that refinement is back, and the named one is the second refinement (as before). The client method now uses the false branch.

[CatarinaGamboa]

Codex review, round 3

• [P2] Reject nonliteral components in state-set names (TypeChecker.java): name = PREFIX + "door" went through getStringFromAnnotation, which turns the field reference into null and registered nulldoor. Fixed in 1783aec: the name must be a single string literal, and anything else gets State set name must be a string literal. The shared getStringFromAnnotation is left as it is (out of scope).

[CatarinaGamboa]

Codex review, round 4: no actionable findings (the full Maven suite passes). Review loop done.

[CatarinaGamboa]

Clean-code review (clean-code-principles)

Reviewed the diff only, weighed against the standing rules (smallest PR that tests well, match surrounding style, no tidy-only refactors, lean tests).

Finding	Verdict
TypeChecker.java:210-224 - [solid-srp-function / func-small] the new name parsing and validation (about 13 lines with three name != null && ... guards) sat inside the annotation loop of handleStateSetsFromAnnotation	Fixed in 79a819c. It is now stateSetName(nameValue, position) in the same class, with early returns, and the loop reads as "get name, create set, remember it if named". Error messages, positions and behaviour (including name = "" meaning unnamed) are unchanged.
TypeChecker.java stateSetName - [name-searchable] "[a-z][a-zA-Z0-9_]*", "true", "false" literals	Declined. Each is used once, next to the error message that explains it, and Keys has no boolean-literal constants. A constant would add indirection for a single use.
TypeChecker.java checkStateSetNameIsFree - [core-kiss-readability] the second loop guards on usedBy == null while the first loop does not break	Declined. It is correct as written, and the reader sees that the first matching kind wins. Throwing from inside the loops would duplicate the message.
TypeChecker.java / ExternalRefinementTypeChecker.java createStateGhost(String name, ...) - [core-dry]	OK, an improvement. The PR removed the "state%d" format that was duplicated in both overrides, so the default name now lives in one place.
TestStateHints#foundKeepsANamedStateSetByItsName - repeats replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")	Declined. It matches the existing neighbouring test, and a helper would be a test-only refactor.
Tests - [lean tests] one message test, one error fixture (four name clashes), one correct fixture method	OK. Each clash in ErrorStateSetNames covers a different rule (case, a state, a ghost, another set).

Full suite locally after the fix: 714 tests, 0 failures.