[CatarinaGamboa]

Description

Adds the Argument picks the state category (codebook C3.1) and a hint for it. These errors had no useful hint before: a transition that depends on an argument isn't part of the state machine, so the existing hints can't explain it.

• Each object instance now records the last call that changed its state (StateChange). Method calls and constructors record their own call, and state-preserving calls keep the previous record. A join of branches records nothing, which ends the search below.
• DecidingArgument follows that chain back to the last call that changed a state set the failing call checks. If that call's transition depends on its arguments or result, the SMT solver looks for values that would have allowed the failing call: the state before the call, the call's to with its parameters left free, and the failing call's from. The model gives the values for the hint.
• When such values exist, the category comes before the other state categories. The error then gets only the deciding hint. If none exist, the error keeps its other category (for example ErrorArgumentCannotPickTheState).

Example

State Refinement Error: found empty(buffer) but expected filled(buffer)

Hints:
  - buffer.reset(boolean) on line 20 decides the state of buffer: with keep == true, this call would be allowed

Category: Argument picks the state (C3.1).

Measured against the codebook

Same runs as #418:

• Corpus: 94 of 99 right (91 before), 1 wrong, 4 with no category.
• Exercises: 42 of 52 right (34 before), 6 wrong, 4 with no category.

The category now finds 12 of the 15 C3.1 cases. The ones it misses:

• a guard in from that changes no state;
• an earlier value that is the real cause;
• a returned value at a join.

Type of change

• New feature

Checklist

• Added tests:
  • ErrorArgumentPicksTheState, ErrorConstructorArgumentPicksTheState and ErrorArgumentPicksTheStateEarlier (the decider is found past a call on another state set);
  • ErrorArgumentCannotPickTheState (no value helps, so no category change);
  • cases in TestErrorCategories and TestStateHints.
• mvn test passes locally

🤖 Generated with Claude Code