[CatarinaGamboa]

Fixes #454, fixes #455, fixes #473.

What changes

The state machine behind the state hints used to drop every method whose state refinements mention a parameter or the result. That meant canRedo() could never be suggested before redo(), and setCompressionMode(int) with mode == 2 could never be suggested before setCompressionType. Those methods are now kept as call variants:

Variant	Meaning	Used for
any arguments	parameters and result left free	call sequences, "can call" lists
arguments meeting a condition	a condition the refinement itself tests (mode == 2, lo < hi, its negation limit <= 0)	call sequences: "... with mode == 2"
result checked (_ / !_)	boolean methods whose to mentions the result	the new guard hint

Boolean methods without a state refinement whose return refinement relates the result to the state, such as @Refinement("_ == true --> hasMore(this)") boolean hasNext(), are kept as guards too.

What a variant does is worked out by the solver only when a hint needs it, and then cached. Building the machine costs the same as on main.

When a hint is given

• Guard. Suggested only when the verifier allows the check in every state the receiver can be in. Like the verifier, that means the first refinement whose from holds in all of them. The result must be able to have the value checked, and the failing call must then be allowed in every state that is left. It is shown when the state is unknown or was checked without being decided. In a known state, it is shown only if no call sequence exists or the state depends on the path taken. If several checks would do, none is shown, because the refinements can't tell them apart (e.g. a coarse UndoManager spec where canUndo, canRedo and canUndoOrRedo all imply the same state).
• Argument condition. Suggested only when every argument meeting it leads to a state that allows the call. A sequence that needs no condition is preferred.
• Earlier argument value (State hint "with mode == N" uses one example value without checking it always works #473). The "decides the state … with mode == 2" hint used one example value from the solver. The value is now checked to work whatever else holds, otherwise no value is claimed.
• Methods kept as variants still leave the machine incomplete, exactly as before. So no new "no sequence of calls" or "final state" claims can appear, and "(and possibly others)" stays.

Hints

A1_56 (study spec, three state sets):

- The state of undoManager is unknown here, and this call needs it to be redoable
- Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable

After guarding redo(), the undo() call gets "Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable", and with both guards the program verifies.

A1_01:

- Call wParam.setCompressionMode(int) with mode == 2 before this call to move wParam from startCompression to compressionExplicit
- In state startCompression, wParam can call: setCompressionMode(int) (and possibly others)

Negated guard: "Guard this call with if (!c.isClosed()): when it returns false, c is open".

#454 can close fully. Part (a) (name only the needed state, don't suggest undo()) was done in #458, and part (b) (suggest canRedo()) is done here.

Tests

• New fixtures:
  • ErrorStateHintGuards (11 cases: negated guard, guard with a parameter, known state, and 8 cases that must get no guard, including several checks proving the same thing)
  • ErrorStateHintArgumentConditions (7 cases, including the State hint "with mode == N" uses one example value without checking it always works #473 example)
  • CorrectStateHintGuards (the hints applied: it verifies)
  • state_hint_compression_mode_error (A1_01)
  • state_hint_study_undo_manager_error / _correct (A1_56 with the study's spec, unchanged)
• TestStateHints asserts every hint text. StateMachineTest covers how refinements are chosen for a set of states.
• Full suite: 681 tests, 0 failures.
• I compared hints on every example in the repo, main against this branch (381 test paths). No error changed and no hint was lost. 9 existing examples gained hints, all of them guards, argument conditions or "can call" lines that the refinements justify.

Performance

For the study's 12-state UndoManager (state_hint_study_undo_manager_error):

	main	this PR
machine build	963 solver calls, ~4.3–4.9 s	963 solver calls, ~4.3 s
first error, including the build	975 calls, ~4.5–5.0 s	1407 calls, ~6.6 s
second error (machine cached)	12 calls, ~0.1 s	12 calls, ~0.1 s

The extra cost is the guard check in an unknown state, paid once per class per run. To keep it down, the possible states are narrowed one state set at a time, and a check of the result reuses the states found for any result.

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] The parameterized guard hint is not a usable Java edit: the new test expects if (l.tryLock(long)), but long is a type, not an argument expression. For GuardLock.tryLock(long timeout), please render a placeholder/value such as tryLock(timeout) (or describe the needed argument in prose) so the suggested if can be applied.