From 01b389e40f88584def1b89c563a2844d0e363c65 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 19:32:25 +0000 Subject: [PATCH 1/2] Name only the state sets a suggested call sequence changes 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 --- .../diagnostics/hints/StateHints.java | 19 +++++++----- .../processor/state_machine/StateMachine.java | 30 +++++++++++++++++++ .../liquidjava/api/tests/TestStateHints.java | 5 ++-- .../state_machine/StateMachineTest.java | 15 ++++++++++ 4 files changed, 58 insertions(+), 11 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index aeb931ae..62629559 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -74,7 +74,7 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set if (category == ErrorCategory.UNKNOWN || checkedElsewhere) return hints.anyState(current, call, checkedElsewhere); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; - List sequences = hints.howToReach(current, call, hints.namesHere(current), + List sequences = hints.howToReach(current, call, false, () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); // in a known state, a check is suggested only when no sequence of calls reaches a state that allows the call boolean reachable = sequences.stream().anyMatch(h -> h.kind() == Kind.CALL_SEQUENCE); @@ -112,19 +112,19 @@ private List anyState(Set current, RefinedFunction call, boolean ch List hints = new ArrayList<>(); hints.add(new Hint(Kind.NEEDED_STATE, message)); hints.addAll(guard(current, call)); - hints.addAll(howToReach(current, call, "any state", List::of)); + hints.addAll(howToReach(current, call, true, List::of)); return hints; } /** * The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} * - * @param from - * how to name {@code current} + * @param fromAnyState + * whether to name {@code current} as any state * @param unreachable * the hints to give if no sequence exists */ - private List howToReach(Set current, RefinedFunction call, String from, + private List howToReach(Set current, RefinedFunction call, boolean fromAnyState, Supplier> unreachable) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) @@ -134,7 +134,7 @@ private List howToReach(Set current, RefinedFunction call, String f return unreachable.get(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return sequences.stream().map(sequence -> callSequence(current, sequence, from)).toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence, fromAnyState)).toList(); } /** @@ -193,13 +193,16 @@ private boolean namesCheckedState(RefinedFunction method) { return refinements.anyMatch(p -> StateMachine.mayName(p, checked)); } - private Hint callSequence(Set current, List sequence, String from) { + /** The states before and after {@code sequence} are named only in the state sets it changes */ + private Hint callSequence(Set current, List sequence, boolean fromAnyState) { Set reached = current; for (CallVariant step : sequence) reached = machine.after(reached, step); + Set changed = machine.stateSetsChanged(current, reached); + String from = fromAnyState ? "any state" : join(machine.describeOnly(current, changed)); String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, - receiver, from, names(reached))); + receiver, from, join(machine.describeOnly(reached, changed)))); } private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index db045cfc..0cae9063 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -11,6 +11,7 @@ import java.util.Map; import java.util.Optional; import java.util.Set; +import java.util.TreeSet; import java.util.stream.Collectors; import java.util.stream.IntStream; @@ -243,6 +244,35 @@ public List> describe(Collection subset, Set named) return StateCover.of(states, Set.copyOf(subset), named); } + /** + * {@code subset} named only by its states in the sets {@code shown}, whatever they are in the other sets, e.g. + * {@code [[unmarked]]} for the state {@code open and unmarked} if only the second set is shown + */ + public List> describeOnly(Collection subset, Set shown) { + List agreeing = states.stream() + .filter(s -> subset.stream().anyMatch( + member -> shown.stream().allMatch(k -> s.names().get(k).equals(member.names().get(k))))) + .toList(); + return describe(agreeing, shown); + } + + /** + * The state sets, as indexes into {@link State#names()}, whose states in {@code after} differ from those in + * {@code before}; every set if no set differs on its own, since then only their combination changed + */ + public Set stateSetsChanged(Collection before, Collection after) { + Set every = IntStream.range(0, states.get(0).names().size()).boxed() + .collect(Collectors.toCollection(TreeSet::new)); + Set changed = every.stream().filter(k -> !statesIn(before, k).equals(statesIn(after, k))) + .collect(Collectors.toCollection(TreeSet::new)); + return changed.isEmpty() ? every : changed; + } + + /** The states of the set {@code k} that {@code subset} has */ + private static Set statesIn(Collection subset, int k) { + return subset.stream().map(s -> s.names().get(k)).collect(Collectors.toSet()); + } + /** * The state sets that {@code subset} depends on, as indexes into {@link State#names()}: those its * {@link #describe(Collection) description} names diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index ec009a44..42f7d494 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -37,10 +37,9 @@ void missingCallsAreSuggestedInOrder() { } @Test - void statesOfMultipleStateSetsAreCombined() { + void callSequenceNamesOnlyTheStateSetsItChanges() { assertHints("ErrorStateHintMultipleSets.java", - new Hint(Kind.CALL_SEQUENCE, - "Call d.unlock() before this call to move d from closed and locked to closed and unlocked"), + new Hint(Kind.CALL_SEQUENCE, "Call d.unlock() before this call to move d from locked to unlocked"), new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()")); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 7c5ebf7e..147c80cb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -70,6 +70,21 @@ void statesAreNamedInEverySetAsked() { MACHINE.describe(Set.copyOf(MACHINE.states()), Set.of(0))); } + @Test + void statesAreNamedOnlyInTheSetsShown() { + assertEquals(List.of(List.of("locked")), MACHINE.describeOnly(Set.of(OPEN_LOCKED), Set.of(1))); + assertEquals(List.of(List.of("locked"), List.of("unlocked")), + MACHINE.describeOnly(Set.of(OPEN_LOCKED, CLOSED_UNLOCKED), Set.of(1))); + } + + @Test + void setsChangedAreThoseWhoseStatesDiffer() { + assertEquals(Set.of(1), MACHINE.stateSetsChanged(Set.of(OPEN_LOCKED), Set.of(OPEN_UNLOCKED))); + // each set has the same states on both sides, only how they are combined changed + assertEquals(Set.of(0, 1), + MACHINE.stateSetsChanged(Set.of(OPEN_LOCKED, CLOSED_UNLOCKED), Set.of(OPEN_UNLOCKED, CLOSED_LOCKED))); + } + @Test void setsNamedAreThoseTheDescriptionFixes() { assertEquals(Set.of(1), MACHINE.stateSetsNamed(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); From df4e0befb8b9f650f6531e781070166acccbf201 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 19:39:07 +0000 Subject: [PATCH 2/2] Name every state set when the unchanged sets are recombined Co-Authored-By: Claude Opus 5.5 --- .../processor/state_machine/StateMachine.java | 16 ++++++++++------ .../state_machine/StateMachineTest.java | 4 ++++ 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 0cae9063..1b3a9d78 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -258,19 +258,23 @@ public List> describeOnly(Collection subset, Set sh /** * The state sets, as indexes into {@link State#names()}, whose states in {@code after} differ from those in - * {@code before}; every set if no set differs on its own, since then only their combination changed + * {@code before}. Every set if the other sets, taken together, differ too: then how the states of different sets + * are combined changed, which naming the changed sets alone would hide. */ public Set stateSetsChanged(Collection before, Collection after) { Set every = IntStream.range(0, states.get(0).names().size()).boxed() .collect(Collectors.toCollection(TreeSet::new)); - Set changed = every.stream().filter(k -> !statesIn(before, k).equals(statesIn(after, k))) + Set changed = every.stream() + .filter(k -> !statesIn(before, Set.of(k)).equals(statesIn(after, Set.of(k)))) .collect(Collectors.toCollection(TreeSet::new)); - return changed.isEmpty() ? every : changed; + Set kept = every.stream().filter(k -> !changed.contains(k)).collect(Collectors.toSet()); + return !changed.isEmpty() && statesIn(before, kept).equals(statesIn(after, kept)) ? changed : every; } - /** The states of the set {@code k} that {@code subset} has */ - private static Set statesIn(Collection subset, int k) { - return subset.stream().map(s -> s.names().get(k)).collect(Collectors.toSet()); + /** The states of the sets {@code sets} that {@code subset} has, combined as in its states */ + private static Set> statesIn(Collection subset, Set sets) { + return subset.stream().map(s -> sets.stream().sorted().map(s.names()::get).toList()) + .collect(Collectors.toSet()); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 147c80cb..a5cadb03 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -83,6 +83,10 @@ void setsChangedAreThoseWhoseStatesDiffer() { // each set has the same states on both sides, only how they are combined changed assertEquals(Set.of(0, 1), MACHINE.stateSetsChanged(Set.of(OPEN_LOCKED, CLOSED_UNLOCKED), Set.of(OPEN_UNLOCKED, CLOSED_LOCKED))); + // the third set changed, and so did how the first two are combined + List before = List.of(state("a", "x", "old"), state("b", "y", "old")); + List after = List.of(state("a", "y", "new"), state("b", "x", "new")); + assertEquals(Set.of(0, 1, 2), machine(before).stateSetsChanged(before, after)); } @Test