GeezerVison

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 <[email protected]>

…#511)

Part of #502 (PR 2, messages). **Depends on #510**, which depends on
#507 and #508. Only the last commit belongs here.

## What

State errors show the states of **named** sets as values of their sets,
whichever form the spec used. `ErrorStateHintMultipleSets` (sets
`doorState` and `lockState`):

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

It is now plain which set fails (only `lockState`), and the frame
equality chains on its own: `doorState(d) == doorState(d@26)` and
`doorState(d@26) == closed`.

`!open(x)` is shown as `door(x) != open`. A state keeps the shorthand
when its set has a generated name (`state2(x) == closed` reads worse
than `closed(x)`), or when sets with different names have a state of
that name. That way the set printed is never a guess.

## How

`StateValues.toSetForm` rewrites expressions for display only.
`StateRefinementError` receives it as `display`:
- **The facts to show are still chosen on the expressions as given.**
`linkedToExpected` and #495's relevance step run first. A shared state
name such as `closed`, which is a variable in the rewritten form, would
otherwise link facts about unrelated objects.
- The message, `getExpected()` and every derivation step
(`VCSimplificationResult.map`) hold the rewritten form, so the **IDE
shows it without a server change**: the server formats those expressions
as they are.

Nothing the verifier decides changes: the VC, the verdict, the hints and
the category are the same. Refinement errors (`RefinementError`) keep
the shorthand for now. They also build alias expansions and
counterexamples from the same expressions, so that would be its own
change.

`Formats.STATE_SET` names the generated `stateN`, which the display
needs to recognise.

## Tests
- `TestStateHints#foundKeepsANamedStateSetByItsName`: the message above.
It fails without the change.

The full suite passes locally.

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

---------

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

…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]>