[CatarinaGamboa]

Closes #482.

What

With more than one @StateSet, the call-sequence hint named every state set, including the ones the suggested calls leave as they are. It now names only the sets whose states differ before and after the calls. Only the displayed hint changes; no solver query changes.

Reproducer from the issue:

before: Call s.mark() before this call to move s from open and unmarked to open and marked
after:  Call s.mark() before this call to move s from unmarked to marked

Existing fixture ErrorStateHintMultipleSets:

before: Call d.unlock() before this call to move d from closed and locked to closed and unlocked
after:  Call d.unlock() before this call to move d from locked to unlocked

How

• StateMachine.stateSetsChanged(before, after): the sets whose states differ. If the sets it would leave out, taken together, differ too (how states of different sets are combined changed), every set is named, as before.
• StateMachine.describeOnly(subset, sets): names subset only in the given sets, reusing StateCover (the naming from Suggest result checks and argument conditions in state hints #474/Ask the solver only about the state sets a refinement names #475) on the states that agree with subset in those sets.
• StateHints.callSequence names both sides with these. from any state is unchanged.

Not changed, on purpose

• In state open and unmarked, s can call: mark() still names the full state: which calls are allowed depends on every set, so dropping open would make the hint less accurate.
• Found/expected (found open(s) && unmarked(s) but expected marked(s) && open(s)) is left as it is. These are the verifier's real predicates (the simplified premise chain and the from disjunction, with arguments, ghosts and aliases). The IDE reads them too. Dropping or reordering conjuncts that hold on both sides would need a semantic check on arbitrary predicates. Doing that only for display is riskier than this PR should be. It could be a follow-up if the study needs it.

Tests

• TestStateHints.callSequenceNamesOnlyTheStateSetsItChanges (the renamed multi-set test; fails on main).
• StateMachineTest: statesAreNamedOnlyInTheSetsShown, setsChangedAreThoseWhoseStatesDiffer (including the cases where how the sets are combined changes).
• mvn test: 692 tests, 0 failures. No other expectation changed. The dcm4che hint (from startCompression to compressionExplicit) already named a single set.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

• [P2] Include state sets whose combinations change (StateMachine.java:266-268): when a sequence changes how states from different sets are paired while also changing a third set, the per-set comparison misses the pairing change. For example, {(a,x,old), (b,y,old)} becoming {(a,y,new), (b,x,new)} returns only the third set, so the hint says only old moved to new. The fallback to every set handles this only when no individual set changes.

[CatarinaGamboa]

Round 1: fixed / declined

• Fixed, combinations changing alongside a set: stateSetsChanged now also compares the sets it would leave out, taken together (as combined tuples). If they differ, every set is named. Codex's example is added to StateMachineTest.setsChangedAreThoseWhoseStatesDiffer. Full suite: 692 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2

No actionable findings. The targeted StateMachineTest and TestStateHints suites pass.