[CatarinaGamboa]

Part of #454 (part (a): what the hint suggests when any state is possible, and how hints name states). Part (b), suggesting a check such as canRedo(), needs return-value queries modelled as guards. That is a separate change.

Problem

When the receiver's state is unknown, the hint has two problems:

1. It suggests transitions whose own precondition is just as unknown. In the issue, redo() needs redoable, and the hint suggests undo(), which needs undoable. Following it only moves the error to undo().
2. It names states in every combination with state sets the call does not check: "undoable and redoable or notUndoable and redoable", and six combinations with the study's three-set spec. Hints for partly known states do the same ("No sequence of calls moves this from <6 combinations> to <6 combinations>").

Before (the issue's JabRef exercise in VS Code):

Cause

StateHints.reachingCalls listed every transition from a state that does not allow the call into one that does (StateMachine.transitionsEnabling), whatever its from. All hints printed a set of states by joining each state's names in every state set.

Fix

• States are named briefly, everywhere. StateMachine.describe (new StateCover) names a set of states as the fewest groups that each fix the state in some state sets and allow any state in the others: a smallest cover by maximal sub-products of the state sets. It works on the machine's solver-built states, with no string matching. Every state hint uses it, for the current, needed and reached states. For example:

  • redoable(this) with three state sets reads redoable;
  • closed(this) && unlocked(this) reads closed and unlocked;
  • open(this) || loud(this) across two sets reads open or loud;
  • two refinements from = "undoable(this)" and from = "redoable(this)" read undoable or redoable;
  • a receiver known only to be notRedoable reads notRedoable.

  The receiver's current state is named in every state set the call checks, plus any set its states agree on. So a join that differs in a checked set still lists each state (closed and unlocked or opened and unlocked), and one that differs only in an unchecked set does not (closed). A single fully known state reads as before (closed and locked). When every state allows the call, each by its own refinement, the needed state is named per refinement (a or b, not every state).

• Only calls that work from any state. When any state is possible, the hint reuses the call sequence search of the known-state case, starting from every state. A call is suggested only if it is allowed in every state. That covers transitions with no from and sequences that start with one (reset(), then open()). Same limits as before: at most 3 sequences of at most 3 calls.

• The needed state is always named. The NEEDED_STATE hint (renamed from REACHING_CALLS, which nothing in vscode-liquidjava or liquidjava-mcp uses) always names the state the call needs, plus the constructors that create an object in it. That includes a call that every state allows, each by a different refinement (a toggle). Constructors are not suggested when the receiver is this. The same applies to the existing "Create a new object instead" hint.

• Only constructors that can be called. StateMachineBuilder leaves out the constructors of abstract classes and interfaces (abstractType, as in Give state hints when the state set or methods come from the receiver's supertypes #464), enums, and private constructors, so no hint suggests new for them.

• A failed check is not "unknown". In if (!it.hasNext()) it.next();, the receiver's own refinement says nothing, but the error's found ((#fresh == true --> hasMore(it)) && !#fresh) mentions its state through the check's result. StateErrorCategories.checkedElsewhere looks at what the error shows as found (TypeChecker.shownFound, the same premise chain the error prints). It only computes that when every state is possible and the receiver's own refinement mentions none. It counts a state only if it is applied to the receiver's instance, or to an object the solver proves equal to it (Scanner same = it; if (!it.hasNext()) same.next();). A check on another object (if (other.hasNext()) it.next();, or the "checked the wrong object" if (it.hasNext()) other.next();) leaves the state unknown. When it does count, the category is none instead of UNKNOWN, and the hint reads "What is known here does not decide the state of it, and this call needs it to be hasMore". Joins of every state across several state sets (if (p) d.open(); if (q) d.lock(); d.enter();) are not checks. They keep main's category (none) and main's "No sequence of calls moves d from … Create a new object instead" hint.

• What changes outside the unknown case:

  • The only category change is UNKNOWN to none for a failed check on the receiver itself (iterator_observer_error, state_test_method_error).
  • Known-state hints change in two ways. States are named more briefly, as above. The constructor suggestions also go away for this receivers and for abstract classes, interfaces, enums and private constructors (in "Create a new object instead with …").
  • StateMachineBuilder now leaves those constructors out of the machine. canModel and the methods it admits are unchanged.

Extension point for part (b). StateHints.anyState builds the hints for "any state is possible": the needed state, then the call sequences from any state. It already tells the two causes apart: nothing known, or a check that did not decide the state. A guard hint goes between the two hints, once the machine records queries whose return value decides a state set. For example: "Check undoManager.canRedo() before this call", or for a failed check, "Call it.next() only when it.hasNext() returns true".

Clean-code pass (878738a, no change in any hint: all 84 state fixtures and 30 reviewer reproducers print the same hints before and after):

• StateCover searches for the smallest cover exactly, with no greedy fallback, and keeps each group's states with it.
• StateHints takes the needed states from one source, and names the checked state sets (checkedSets) and the check flag (checkedElsewhere) apart.
• StateErrorCategories shares its "every state possible, none mentioned" test.
• StateMachine.statesAllowing is derived from statesAllowingByRefinement.
• AuxStateHandler only looks for a check when no argument decided the state.

Hint output, before (main) and after

Issue reproducer (external UndoManager spec, two state sets, receiver from a method return):

before: The state of undoManager is unknown here. To get it to undoable and redoable or notUndoable and redoable, use: undoManager.undo() (from undoable and notRedoable)
after:  The state of undoManager is unknown here, and this call needs it to be redoable

Three state sets (parameter receiver):

before: The state of history is unknown here. To get it to start and undoable and redoable or start and notUndoable and redoable or canEdit and undoable and redoable or canEdit and notUndoable and redoable or end and undoable and redoable or end and notUndoable and redoable, use: history.undo() (from start and undoable and notRedoable or canEdit and undoable and notRedoable or end and undoable and notRedoable)
after:  The state of history is unknown here, and this call needs it to be redoable

Disjunction across state sets (from = "open(this) || loud(this)") and one refinement per set (undoOrRedo()):

before: No state information is known for this object. Make sure its state is initialized and available at this point.
after:  The state of s is unknown here, and this call needs it to be open or loud
after:  The state of history is unknown here, and this call needs it to be undoable or redoable

A failed check (if (!it.hasNext()) it.next();):

before: (no hint)
after:  What is known here does not decide the state of it, and this call needs it to be hasMore

A call allowed in any state (reset() has no from; open() needs created):

before: The state of f is unknown here. To get it to open, use: f.open() (from created)
after:  The state of f is unknown here, and this call needs it to be open
        Call f.reset(), then f.open() before this call to move f from any state to open

Partly known state (this known to be notRedoable, three state sets):

before: No sequence of calls moves this from start and undoable and notRedoable or start and notUndoable and notRedoable or canEdit and undoable and notRedoable or canEdit and notUndoable and notRedoable or end and undoable and notRedoable or end and notUndoable and notRedoable to start and undoable and redoable or ... (6 combinations)
        In state start and undoable and notRedoable or ... (6 combinations), this can call: check()
after:  No sequence of calls moves this from notRedoable to redoable
        In state notRedoable, this can call: check()

Toggle (a class whose flip() goes from up to down and back):

before: The state of t is unknown here. To get it to up or down, use: new ErrorStateHintUnknownToggle()
after:  The state of t is unknown here, and this call needs it to be up or down. Objects created with new ErrorStateHintUnknownToggle() start in such a state

Known state, unchanged (after open(); close();):

Call f.reset(), then f.open() before this call to move f from closed to open
In state closed, f can call: reset()

Every other state fixture. I ran each Error* state fixture and test-suite directory on main and on this branch and compared the hints. Apart from the cases above, the only changes are:

• every "unknown" hint now has the new wording;
• iterator_observer_error and resultset_forward_error (line 67) now get the needed-state hint. On main they got the generic "No state information is known…" hint, or no hint after a failed hasNext();
• state_test_method_error (if (edit.canUndo()) {} else edit.undo();) now reads "What is known here does not decide the state of edit…" instead of "unknown", and no longer suggests edit.redo();
• ErrorLoopPostState no longer suggests new ErrorLoopPostState() for this;
• ErrorPathDependentOtherStateSet now reads "from closed to opened" instead of two combinations each.

Merging with #464. Both PRs touch StateMachineBuilder and StateHints, and the conflicts are mechanical:

• keep one abstractType: both PRs add an identical one;
• move Give state hints when the state set or methods come from the receiver's supertypes #464's .distinct() on the constructor lists into StateHints.newObjects, which replaces both lists here;
• merge this PR's typeName (in privateConstructor) with Give state hints when the state set or methods come from the receiver's supertypes #464's parameterTypes, which do the same thing.

Tests

Each test pins one behaviour. To keep CI fast, the fixtures are grouped so that one verifier run checks several errors. Every new test fails without its fix: on the PR's base, or on the commit before the fix it pins.

Test (TestStateHints)	Fixture	Pins
unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet	classes/state_hint_undo_manager_error	the issue reproducer: needs redoable, undo() not suggested
unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState	ErrorStateHintUnknownState (existing, expectation changed)	a call that needs another unknown state is not suggested
unknownStateSuggestsCallsAllowedInAnyState	ErrorStateHintUnknownAnyState	reset(), then open() is suggested; open() alone is not
statesAreNamedOnlyInTheStateSetsThatMatter	ErrorStateHintNaming (3 errors)	open or loud across sets; a toggle on {a, b} × {x, y, z} reads a or b; a partly known state reads notRedoable
failedCheckOfTheReceiverIsNotAnUnknownState	classes/state_hint_checked_error (3 errors)	a failed hasNext() on the receiver, or on a variable holding it, "does not decide", with no category; a check of another scanner leaves it unknown (UNKNOWN)
joinsAreNotTakenForAnUnknownState	ErrorStateHintJoins (2 errors)	a join of every state of two sets keeps main's "No sequence of calls" hint, with no category; a join in one checked set lists both states
onlyConstructorsThatCanBeCalledAreSuggested	ErrorStateHintConstructors (4 errors)	a concrete class's constructor is suggested; none for this, an abstract class or a private constructor

StateMachineTest has 10 unit tests for describe and stateSetsNamed. They run in milliseconds and cover the state naming: one set, cross-set and three-set disjunctions, every state, forced sets, and declaration order.

Removed as overlapping: separate fixtures for three state sets, a one-set disjunction, one refinement per set, a two-set goal, a field receiver, several and long sequences, the one-set toggle, a known state, and the external abstract and interface specs. Each is covered by one of the tests above, by an existing test or by the unit tests. The interface spec never reached the guard, since an interface cannot declare a constructor refinement.

Test time (mvn test for the verifier, two interleaved runs of each on the same machine, surefire time summed over test cases):

	tests	surefire	wall	TestExamples	TestStateHints
base (0053074)	547	81.9 s	89.1 s	64.8 s	2.2 s
PR before trimming (b9683e9)	613	98.6 s (+16.7)	106.0 s (+16.9)	72.2 s	9.7 s
PR now	569	88.2 s (+6.3)	95.2 s (+6.1)	67.3 s	5.3 s

mvn test for the verifier: 569 tests, 0 failures, 0 errors.

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] The new needed-state hint can recommend an impossible constructor. Reproducer on this PR head: @StateSet({"fresh", "ready"}) abstract class AbstractHint has a constructor with to = "ready(this)" and use() with from = "ready(this)"; fail(AbstractHint value) { value.use(); }. The verifier reports the state error, then says Objects created with new AbstractHint() start in such a state. new AbstractHint() cannot compile. newObjects uses every constructor returned by the machine without checking whether its class is instantiable. #464 contains an abstractType guard that removes this suggestion on its branch; please ensure that guard lands with this PR (or add it here), and test an unknown receiver of an abstract type. Focused TestStateHints and StateMachineTest passed, but this case is currently untested.

[CatarinaGamboa]

[Claude] Fixed in d7ce256: StateMachineBuilder now leaves out the constructors of abstract classes and interfaces (abstractType, the same helper and placement as #464), enums, and private constructors. So no hint suggests new for them, neither "Objects created with…" nor "Create a new object instead with…". Tests: your reproducer (ErrorStateHintUnknownAbstract), an external spec for the abstract java.io.InputStream, an interface spec (RunnableFuture), a private constructor, and a concrete class where the suggestion stays. Interfaces cannot declare a constructor refinement (the verifier warns), so the interface branch is defensive.

[CatarinaGamboa]

[Codex re-review] The abstract-class case is fixed, and the private-constructor case is now covered. One accessibility gap remains: package-private and protected constructors are also not callable from every site, but privateConstructor filters only private constructors and enums. For example, a public testSuite.lib.PackageCtor with a package-private constructor that creates ready, used from testSuite.Use with an unknown PackageCtor value and a call requiring ready, can still suggest new PackageCtor() even though testSuite.Use cannot invoke it. Please account for caller package/subclass access or omit constructors whose accessibility cannot be established. The PR CI is green.

[CatarinaGamboa]

[Claude] Fixed in efa18bf:

• A. A failed check counts only when the state is applied to the receiver instance or to an object the solver proves equal to it (Scanner same = it). if (other.hasNext()) it.next(); and if (it.hasNext()) other.next(); are UNKNOWN again.
• B. A join of every state across two sets keeps main's category (none) and its "No sequence of calls moves d from … Create a new object instead" hint. Current states are named in every set the call checks, so closed and unlocked or opened and unlocked stays explicit.
• C. A goal of every state is named per refinement (a or b).
• D. MAX_EXACT is now 13. A brute force over all products of at most 16 states confirms it.
• E. shownFound is computed lazily.

New fixtures cover each case. The 84 existing state fixtures are unchanged from d7ce256. 600 tests, 0 failures. The PR body has the corrected claims and the merge notes for #464.

[CatarinaGamboa]

[Codex review] Package-private constructors can still be suggested from unrelated packages. Example: testSuite.Use gets new PackageCtor() although the public testSuite.lib.PackageCtor constructor is package-private. Please filter constructors by caller accessibility.

[CatarinaGamboa]

[Claude] 878738a: clean-code pass and trimmed tests.

• Code: StateCover is exact-only, with no greedy fallback, and each group keeps its states. Needed states come from one source in StateHints. Clearer names (checkedSets, checkedElsewhere, join). A shared "nothing mentioned" test in StateErrorCategories. statesAllowing is derived from statesAllowingByRefinement. No check lookup when an argument decided the state. Hint output is identical on all 84 state fixtures and 30 reproducers.
• Tests: 27 new hint tests and 23 fixtures are now 6 tests over 6 fixtures (one existing fixture changed), each pinning one behaviour. Every test fails without its fix. There are 569 tests in total, all passing.
• Time vs base (0053074): +16.7 s of surefire time before (+20%), +6.3 s now (+8%), averaged over two interleaved runs.