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..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 @@ -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,39 @@ 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 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, Set.of(k)).equals(statesIn(after, Set.of(k)))) + .collect(Collectors.toCollection(TreeSet::new)); + 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 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()); + } + /** * 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..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 @@ -70,6 +70,25 @@ 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))); + // 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 void setsNamedAreThoseTheDescriptionFixes() { assertEquals(Set.of(1), MACHINE.stateSetsNamed(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED)));