Skip to content

Suggest the calls that make a failing state transition verify - #411

Merged
CatarinaGamboa merged 1 commit into
mainfrom
feat/state-hints-calls
Oct 23, 2026
Merged

Suggest the calls that make a failing state transition verify#411
CatarinaGamboa merged 1 commit into
mainfrom
feat/state-hints-calls

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

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

@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 21, 2026
Merged
3 tasks done
@CatarinaGamboa
CatarinaGamboa added this pull request to stack #415 October 23, 2026 16:59
@CatarinaGamboa
CatarinaGamboa deleted the branch feat/hint-list October 23, 2026 17:43
@CatarinaGamboa @claude
Suggest the calls that make a failing state transition verify
fb438f1 
When a call is made in a state that does not allow it, the verifier
builds the class's state machine from its state sets and state
refinements, proving each transition with the SMT solver, and searches
it for the shortest sequences of calls that lead to a state allowing
the call. The error then suggests those calls and lists the calls
allowed in the current state.

Only transitions that depend on nothing but the state of the object
are modeled, and a call is suggested only when a single state
refinement allows it in every state the object can be in, as in the
verifier, so every suggestion makes the failing call verify.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa
CatarinaGamboa removed this pull request from stack #415 October 23, 2026 18:02
@CatarinaGamboa
CatarinaGamboa changed the base branch from feat/hint-list to main October 23, 2026 18:03
@CatarinaGamboa
CatarinaGamboa merged commit ba44b18 into main Oct 23, 2026
1 check passed
CatarinaGamboa added a commit that referenced this pull request Oct 23, 2026
@CatarinaGamboa @claude
Explain dead ends in failing state transitions (#412)
f657056 
Stacked on #411.

## Description
When no call can fix a failing state transition, the error now says why:
- **Unreachable state:** no sequence of calls reaches a state where the
call is allowed. The hint suggests a constructor that creates the object
in such a state, if one exists.
- **State depending on the path taken:** the object can be in several
states (e.g. after an `if`), and no single sequence of calls works for
all of them.
- **Final state:** no method with a state refinement can be called in
any of the states the object can be in.

These hints claim that something is impossible, so they are only given
when the machine is complete. That means every state-changing method of
the class is modeled, and no superclass or subclass has state
refinements of its own. When nothing is known about the state, these
hints are not given; the next PR handles that case.

`StateMachineBuilder` now also records the states each constructor
creates, when they only depend on the state of `this`.

## Example
```java
f.close();
f.read(); // read() needs open
```
```
 --> No sequence of calls moves f from closed to open. Create a new object instead with new File()
     f is in state closed, where none of its methods with state refinements can be called
```

## Type of change
- [x] New feature

## Checklist
- [x] Added tests:
  - `ErrorStateHintFinalState` and `ErrorStateHintPathDependent`.
- `ErrorStateHintIncomplete` (a transition depends on an argument) and
`ErrorStateHintSubclass` (a subclass adds a transition) get no dead-end
claim.
  - `ErrorStateHintSeveralRefinements` now gets the path-dependent hint.
- [x] `mvn test` passes locally

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 24, 2026
Merged
1 task done
CatarinaGamboa added a commit that referenced this pull request Oct 24, 2026
@CatarinaGamboa @claude
Land the rest of the state hints stack (#412, #413, #414) (#417)
69895fa 
## Description
#412, #413 and #414 were merged into their stacked base branches instead
of `main`: once #411 was merged, their bases were never retargeted.
Their code is only on `feat/state-hints-unknown`.

This PR applies the three reviewed commits on top of `main`, unchanged:
- Explain dead ends in failing state transitions (#412)
- List the calls that reach an allowed state when the state is unknown
(#413)
- Build each class's state machine once per checker (#414)

The hint and state machine files are identical to
`feat/state-hints-unknown`. Rebase-merging keeps the three commits
separate.

## Checklist
- [x] `mvn test` passes locally on top of the current `main` (#408,
#409)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@CatarinaGamboa