Repository navigation
Name only the state sets a suggested call sequence changes - #484
Merged
Merged
Conversation
A hint such as "Call s.mark() before this call to move s from open and unmarked to open and marked" named every state set, including the ones the calls leave as they are. It now names only the sets whose states differ before and after the calls: "move s from unmarked to marked". Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
Codex review, round 1
|
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
Round 1: fixed / declined
|
Collaborator
Author
Codex review, round 2No actionable findings. The targeted |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #482.
What
With more than one
@StateSet, the call-sequence hint named every state set, including the ones the suggested calls leave as they are. It now names only the sets whose states differ before and after the calls. Only the displayed hint changes; no solver query changes.Reproducer from the issue:
Existing fixture
ErrorStateHintMultipleSets:How
StateMachine.stateSetsChanged(before, after): the sets whose states differ. If the sets it would leave out, taken together, differ too (how states of different sets are combined changed), every set is named, as before.StateMachine.describeOnly(subset, sets): namessubsetonly in the given sets, reusingStateCover(the naming from Suggest result checks and argument conditions in state hints #474/Ask the solver only about the state sets a refinement names #475) on the states that agree withsubsetin those sets.StateHints.callSequencenames both sides with these.from any stateis unchanged.Not changed, on purpose
In state open and unmarked, s can call: mark()still names the full state: which calls are allowed depends on every set, so droppingopenwould make the hint less accurate.found open(s) && unmarked(s) but expected marked(s) && open(s)) is left as it is. These are the verifier's real predicates (the simplified premise chain and thefromdisjunction, with arguments, ghosts and aliases). The IDE reads them too. Dropping or reordering conjuncts that hold on both sides would need a semantic check on arbitrary predicates. Doing that only for display is riskier than this PR should be. It could be a follow-up if the study needs it.Tests
TestStateHints.callSequenceNamesOnlyTheStateSetsItChanges(the renamed multi-set test; fails on main).StateMachineTest:statesAreNamedOnlyInTheSetsShown,setsChangedAreThoseWhoseStatesDiffer(including the cases where how the sets are combined changes).mvn test: 692 tests, 0 failures. No other expectation changed. The dcm4che hint (from startCompression to compressionExplicit) already named a single set.🤖 Generated with Claude Code