[CatarinaGamboa]

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 Add a Relevant to Expected step to state errors #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

[CatarinaGamboa]

Codex review, round 1 (codex exec review, this PR's commit only)

[P2] Distinguish generated set names from explicit names (StateValues.java). When a user explicitly names a state set state1 or state2, that name is accepted by stateSetName, but this pattern treats it as generated and leaves open(x) in state error messages.

Fixed, by keeping those names for sets without a name. An explicit name = "state2" is now an error: State set name 'state2' is kept for state sets without a name. Such a name could already clash with a generated one, for example an unnamed second set. With it reserved, the spelling tells exactly which sets were named, and there is no flag to carry. The pattern lives once, as Formats.STATE_SET_NAMES, next to STATE_SET, and both the check and the display use it.

Test: one line in ErrorStateSetNames.

Rebased on #510 after its round 4 fix.

Clean-code review (clean-code-principles)

• solid-srp / core-separation-of-concerns: deciding what to show stays in ErrorMessage, on the expressions as given. Rewriting for display is one function, StateValues.toSetForm, applied last. The error stores the displayed form, so the CLI and the IDE cannot disagree.
• solid-ocp: ErrorMessage.of takes the rewrite as a parameter. RefinementError passes identity(), and moving it to the new form later is a one-line change there.
• core-dry: VCSimplificationResult.map rewrites every derivation step through one method. Formats.STATE_SET and STATE_SET_NAMES replace the inline "state%d".
• name-meaningful: toSetForm, setValue, display.
• Tests: the existing message test now asserts the new form, plus one fixture line for the reserved names.

[CatarinaGamboa]

Codex review, round 2

[P2] Resolve the state's owning set before rewriting it. When two loaded classes have a state with the same name in differently named sets, both match by simple name, so even A.open(x) is left in the shorthand.

Declined: this is the intended fallback. An invocation's qualifier is the class where the spec was written, not the class that owns the set. A spec in A about a Door parameter writes A.open(d), and the solver resolves it through d's type. Picking a set by qualifier could therefore print the wrong set name. The display only rewrites when the set name is certain, and otherwise keeps the shorthand, which is still correct. That was in the PR description from the start ("so that the set printed is never a guess"). No code change.

[CatarinaGamboa]

Codex review, round 3

[P2] A ghost can be displayed as a state of an unrelated set. A boolean @Ghost("boolean ready") on Sensor was shown as phase(#new_Sensor) == ready == false, because an unrelated class has a set phase with a state ready.

Fixed. The display matched by name only. It now keeps the shorthand when a ghost that is not a state (a @Ghost, or a @RefinementPredicate) has that name, since the name alone does not tell which one it is. toSetForm takes the context's ghosts for that.

Regression: ErrorStateValueGhostName and TestStateHints#ghostNamedLikeAStateOfAnotherClassKeepsItsForm, which expects found ready(sensor) == false but expected ready(sensor). The full suite passes locally.

[CatarinaGamboa]

Codex review, round 4

[P2] Reserve only names the verifier can generate. state\d+ also matches state0 and state01, which are never generated, so name = "state0" was rejected.

Fixed: the reserved names are now state[1-9][0-9]*, exactly what Formats.STATE_SET produces. The full suite passes locally.

With this, the review loop for this PR is done: four rounds, three real fixes (reserved names, ghosts named like states, this one) and one intended fallback declined.