GeezerVison is showing github.com — Name only the state sets a suggested call sequence changes by CatarinaGamboa · Pull Request #484 · liquid-java/liquidjava
Conversation
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:
before: Call s.mark() before this call to move s from open and unmarked to open and marked
after: Call s.mark() before this call to move s from unmarked to marked
Existing fixture ErrorStateHintMultipleSets:
before: Call d.unlock() before this call to move d from closed and locked to closed and unlocked
after: Call d.unlock() before this call to move d from locked to unlocked
How
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 dropping open would make the hint less accurate.- Found/expected (
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 the from disjunction, 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
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
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 <[email protected]>
Codex review, round 1
- [P2] Include state sets whose combinations change (StateMachine.java:266-268): when a sequence changes how states from different sets are paired while also changing a third set, the per-set comparison misses the pairing change. For example,
{(a,x,old), (b,y,old)} becoming {(a,y,new), (b,x,new)} returns only the third set, so the hint says only old moved to new. The fallback to every set handles this only when no individual set changes.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
Round 1: fixed / declined
- Fixed, combinations changing alongside a set:
stateSetsChanged now also compares the sets it would leave out, taken together (as combined tuples). If they differ, every set is named. Codex's example is added to StateMachineTest.setsChangedAreThoseWhoseStatesDiffer. Full suite: 692 tests, 0 failures.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
Codex review, round 2
No actionable findings. The targeted StateMachineTest and TestStateHints suites pass.
|
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Assignees
No one assigned
Milestone
No milestone
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.
|