[CatarinaGamboa]

Stacked on #410.

Description

When a typestate call fails, the State Refinement Error now says which calls to add before it, and which calls are allowed in the object's current state.

• processor/state_machine/: StateMachineBuilder builds a class's state machine. Its states are the combinations of its @StateSet states, and each transition is proven with the SMT solver on two fresh objects in a separate scope. StateMachine holds the graph and searches it: a breadth-first search over sets of states, so it also works when the object can be in several states. StateSolver wraps the SMT questions.
• diagnostics/hints/StateHints turns the machine into hints: it reads the machine and never calls SMT.
• AuxStateHandler computes the hints right before throwing the error. If computing them fails, the error is reported without hints.

To make sure a hint is never wrong:

• Only transitions that depend on nothing but the state of this are modeled. A method whose refinement mentions parameters, return values or other ghosts is left out, and the machine is marked incomplete.
• A call counts as allowed on a set of states only if a single @StateRefinement allows all of them, as changeState requires.
• Hints are only given when the receiver is a variable, a field or this. For make().read() an added call could act on a different object.
• A superclass or subclass with its own state refinements marks the machine incomplete. When the machine is incomplete, the list of allowed calls ends with "(and possibly others)".

The next PRs add hints for dead ends (unreachable or final state, state depending on the path taken) and for an unknown state, and then cache the machine once per run.

Example

r.step(); // r is idle, step() needs running

State Refinement Error: found idle(r) but expected running(r)
 --> Call r.prepare(), then r.start() before this call to move r from idle to running
     In state idle, r can call: prepare()

Type of change

• New feature

Checklist

• Added tests: ErrorStateHint{CallSequence,TwoCalls,MultipleSets,SeveralRefinements,MethodCallReceiver} and TestStateHints, which checks the exact hints (including that the last two get none)
• mvn test passes locally

🤖 Generated with Claude Code