Name only the state sets a suggested call sequence changes

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -74,7 +74,7 @@ public static List<Hint> 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<Hint> sequences = hints.howToReach(current, call, hints.namesHere(current),
+        List<Hint> 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<Hint> anyState(Set<State> current, RefinedFunction call, boolean ch
         List<Hint> 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<Hint> howToReach(Set<State> current, RefinedFunction call, String from,
+    private List<Hint> howToReach(Set<State> current, RefinedFunction call, boolean fromAnyState,
             Supplier<List<Hint>> unreachable) {
         Optional<List<List<CallVariant>>> search = machine.shortestPaths(current, call, MAX_SEQUENCES);
         if (search.isEmpty())
@@ -134,7 +134,7 @@ private List<Hint> howToReach(Set<State> 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<State> current, List<CallVariant> sequence, String from) {
+    /** The states before and after {@code sequence} are named only in the state sets it changes */
+    private Hint callSequence(Set<State> current, List<CallVariant> sequence, boolean fromAnyState) {
         Set<State> reached = current;
         for (CallVariant step : sequence)
             reached = machine.after(reached, step);
+        Set<Integer> 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<State> current, RefinedFunction call, boolean pathDependent) {

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<List<String>> describe(Collection<State> subset, Set<Integer> 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<List<String>> describeOnly(Collection<State> subset, Set<Integer> shown) {
+        List<State> 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<Integer> stateSetsChanged(Collection<State> before, Collection<State> after) {
+        Set<Integer> every = IntStream.range(0, states.get(0).names().size()).boxed()
+                .collect(Collectors.toCollection(TreeSet::new));
+        Set<Integer> changed = every.stream()
+                .filter(k -> !statesIn(before, Set.of(k)).equals(statesIn(after, Set.of(k))))
+                .collect(Collectors.toCollection(TreeSet::new));
+        Set<Integer> 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<List<String>> statesIn(Collection<State> subset, Set<Integer> 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

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()"));
     }
 

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<State> before = List.of(state("a", "x", "old"), state("b", "y", "old"));
+        List<State> 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)));