[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.

[CatarinaGamboa]

Fixed in 9f90bd5: a guard is now written as a call with the parameters' names, so tryLock(long timeout) gives if (l.tryLock(timeout)). Sequences and "can call" lists still show signatures, e.g. tryLock(long), since they name a method rather than give code to paste. Also rebased on main (#472); the full suite passes locally (681 tests, 0 failures).

[CatarinaGamboa]

[Codex re-review] The type-name issue is fixed, but the guard is still not usable as written in the new withParameter() fixture: it suggests if (l.tryLock(timeout)), while that method has only l in scope and no timeout variable. The name comes from tryLock's declaration, not the caller. Could the hint state that the caller must supply a valid argument (or show a concrete value), rather than present the formal name as an in-scope expression?

[CatarinaGamboa]

Fixed in 0afdf6a. A guard no longer presents the callee's parameter names as expressions: it is written if (l.tryLock(...)), filling in the arguments of tryLock(long timeout), and a guard without parameters stays pasteable as is (if (it.hasNext())). Guards are only suggested when the result decides the state for every argument, so any argument the caller passes works.

The same problem existed in argument conditions and deciding arguments (r.set(int, int) with lo < hi), so those now name the parameters too: r.set(int lo, int hi) with lo < hi, param.setTilingMode(int mode) on line 25 ... with mode == 2.

From a review of the rest of the PR, also fixed: the path search capped the paths to each set of states before preferring ones without argument conditions, so a later unconditioned path could be dropped; it now ranks first, then caps. Plus small cleanups (a dead local, a duplicated returnsValue check). Full suite passes locally (681 tests, 0 failures).

[CatarinaGamboa]

[Codex re-review] The latest update resolves my parameterized guard comment: the hint now asks the caller to supply the arguments and names the formal parameters separately. I also checked the path ranking change; it keeps unconditioned paths before applying the per-state cap. I found no further issue in this update, and CI is green.