Named state sets: optional name on @StateSet by CatarinaGamboa · Pull Request #498 · liquid-java/liquidjava

CatarinaGamboa · 2026-11-06T13:30:28Z

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 (rebased on #495, which leaves out the unrelated unlocked(d@26)):

- found closed(d@26) && locked(d) && state1(d) == state1(d@26) but expected closed(d) && unlocked(d)
+ found closed(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 · 2026-11-06T13:30:35Z

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 · 2026-11-06T13:36:16Z

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 · 2026-11-06T13:44:07Z

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 · 2026-11-06T13:47:39Z

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

CatarinaGamboa · 2026-11-06T15:48:16Z

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.

A named state set's ghost function takes that name instead of the generated stateN, so messages, hints and the equalities that keep unmentioned sets print e.g. redo(um), and specs can use it like any ghost (redo(old(this))). Unnamed sets keep stateN. A name must be a lowercase identifier that is not already a state, ghost or other state set of the class. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…lock set Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Fixes #452 **Cause.** `MethodsFirstChecker` and `ExternalRefinementTypeChecker` registered a type's `@StateSet`s and `@Ghost`s while visiting that type. A spec read before the declaring type was visited could not see them. For external specs that is #452: an interface in a spec file cannot use states declared by an interface later in the same file. **Fix.** A new first pass, `GhostsFirstChecker`, registers the ghosts and state sets of every type, in the package and all its sub-packages, before any spec is read. It runs after `FieldGhostsGeneration`, which turns fields into ghosts, and before the existing passes. It also registers `@RefinementPredicate` ghosts, which are only allowed on types, so the name checks for state sets from #498 still see them. External specs keep their naming under the refined class through a new `ExternalRefinementTypeChecker.registerGhosts`. The "could not find class" warning is still reported once, by the existing visit. This is also step 0b of #502: with every set known when a spec is parsed, `phase(this) == open` can be resolved where it is written. **Before / after** (the reproducer from #452, `state_set_declared_later_correct`): ``` Not Found Error: Ghost 'java.awt.Frame.notDisplayable' could not be found ``` now passes verification. **Tests.** - `state_set_declared_later_correct`: the #452 reproducer, which fails on main. - `ErrorStateSetNames`: a set named like a `@RefinementPredicate` ghost is still reported. It fails if `@RefinementPredicate` is registered after the sets. The full suite passes locally. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Part of #502 (PR 1, the language). **Depends on #507 and #508.** Until they are merged, this diff also shows their commits; only the last commit belongs here. ## What A spec can write a state as a value of its set: ```java @stateset(name = "door", value = {"closed", "opened"}) @stateset(name = "lock", value = {"unlocked", "locked"}) ... @StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened") void open(); ``` `set(e) == state` means `state(e)`, and `set(e) != state` means `!state(e)`, in either order. The old shorthand stays valid, and the two can be mixed. ## How `StateValues.toShorthand` rewrites the new form into the shorthand **once, where the spec is parsed and in that spec's scope**. Everything after that is unchanged, and that includes every part that reads states syntactically: the frame equalities, the state machine, the hints, `DecidingArgument`, `StateErrorCategories` and #495's relevance pass. The parse sites are: - `@Refinement`, via `getRefinementFromAnnotation`; - method from/to, via `createStatePredicate`; - constructor `to`, via `setConstructorStates`; - alias bodies, at registration, where only the alias's parameters are variables. Every set is already registered when specs are parsed (#508), so there is no late resolution, and a caller's variable can never capture a state name. **Scope rules** (from the #502 design reviews): - A variable in scope keeps its meaning. That covers parameters, context variables, and `_`, `this` and `return`, which are always variables. Specs that are valid today mean the same. - A name that is a state of *another* set of the class is an error: `State 'locked' is not a state of 'door' (its states are closed, opened)`. - Only the sets that apply to the argument's type are considered, that is, sets declared on its class or a supertype. The type comes from `this`, `_`, a parameter, a context variable, `old(x)`, or an alias's declared parameter type. When the type is known, any applicable set may have the state, as with the shorthand. When it is unknown, every set of that name must have it, and otherwise the name stays an unknown variable. The rewritten state is named exactly as the shorthand written in the same place (`a.Sub.door(this) == open` becomes `a.Sub.open(this)`), so it is resolved the same way. **Two new checks on `@StateSet`** (⚠️ breaking for specs that have this ambiguity today: they are now rejected even if the ambiguous state is never used), because `open(this)` must say which set it means: - Two sets of one class may not share a state name: `State 'open' is in two state sets of X: state1 and state2`. That was accepted before, and the shorthand picked one set silently. - The #498 name check now covers generated names, so a state called `state1` next to the unnamed set `state1` is reported. ## Tests (each fails without the change) - `CorrectStateValues`, written only in the new form: two named sets, a constructor `to`, from/to, `!=`, a branch that keeps a set via `old`, a parameter named like a state, an alias used next to a local variable named like its state, and states named `_` and `return`. - `ErrorStateValues`: the wrong-set error, a state name shared by two sets, and a state named like a generated set. - `TestStateHints#queryWrittenWithItsStateSetIsOfferedAsAGuard`: a query written in the new form is still offered as a guard, so the state machine reads it. The full suite passes locally. Found while testing: #509, an existing false error for a boolean query in an ordinary class, with either form. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Brings [liquidjava-fsm#17](liquid-java/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): ```java @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 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/178/before-all.png" width="380"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/178/after-all.png" width="380"> | | Focus on error | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/178/before-focus.png" width="380"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/178/after-focus.png" width="380"> | The verifier's message for the same error (no change here; shown for context): <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/178/verification.png" width="380"> ## 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](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa mentioned this pull request Nov 6, 2026

States of a named @StateSet are shown as plain ghosts (GhostDTO matches stateN by regex) liquid-java/vscode-liquidjava#177

Open

CatarinaGamboa mentioned this pull request Nov 6, 2026

Found: rewrite facts through ghost equalities g(x) == g(x@k) so they are stated about x #501

Open

CatarinaGamboa and others added 7 commits November 9, 2026 17:09

Report a state set name that is not a string literal

3f8c132

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Keep canUndo()'s known-undoable refinement in the named-sets fixture

68d2fcd

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Accept only a plain string literal as a state set name

93a3759

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Read a state set's name in its own method

3704886

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Name both state sets in ErrorStateHintMultipleSets

6272851

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Expect the Found of ErrorStateHintMultipleSets without the unrelated …

1d67db4

…lock set Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa force-pushed the feat/435-named-state-sets branch from c9a5ba1 to 1d67db4 Compare November 9, 2026 17:12

CatarinaGamboa merged commit 2c4f484 into main Nov 9, 2026
1 check passed

This was referenced Nov 9, 2026

Read named state sets and states written as values of their sets liquid-java/liquidjava-fsm#17

Merged

Label a named state set's diagram with its name liquid-java/vscode-liquidjava#178

Merged

Warn when a state set is named like a method of its class #514

Closed

Navigation Menu

Repository navigation

Named state sets: optional name on @StateSet - #498

Named state sets: optional name on @StateSet#498
CatarinaGamboa merged 7 commits into
mainfrom
feat/435-named-state-sets

CatarinaGamboa commented Nov 6, 2026 •

edited

Loading

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

CatarinaGamboa commented Nov 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

Before / after

Tests (each fails on main)

API release needed

Notes

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Uh oh!

CatarinaGamboa commented Nov 6, 2026

Clean-code review (clean-code-principles)

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CatarinaGamboa commented Nov 6, 2026 •

edited

Loading