GeezerVison

Copy link

Copy Markdown

Collaborator

CatarinaGamboa force-pushed the feat/502-state-messages branch from f240944 to 51a2e6b Compare November 9, 2026 18:33

CatarinaGamboa force-pushed the feat/502-state-messages branch 2 times, most recently from 47bbf25 to 9f0664b Compare November 9, 2026 21:00

CatarinaGamboa force-pushed the feat/502-state-messages branch from 9f0664b to f764dc0 Compare November 9, 2026 21:44

1 check passed

…512)

Part of #502 (PR 3, docs). **Depends on #511** (and so on #510, #508 and
#507). Only the last commit belongs here.

The README's typestate example now names its set and writes states as
values of it:

```java
@stateset(name="connection", value={"unconnected", "bound", "connected", "closed"})
...
@StateRefinement(from="connection(this) == unconnected", to="connection(this) == bound")
public void bind(SocketAddress add);
...
@StateRefinement(from="connection(this) != closed", to="connection(this) == closed")
public void close();
```

A short paragraph says that the shorthand `bound(this)` is still
accepted, that a `to` keeps the sets it does not mention, and what the
error looks like. That error was checked by running the README example
on #511:

```
State Refinement Error: found connection(socket) == bound but expected connection(socket) == connected
```

The study exercises live in the study repository and are not changed
here.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

…re (#517)

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 (#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](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>