List the calls that reach an allowed state when the state is unknown

liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownState.java

@@ -0,0 +1,24 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open", "closed"})
+public class ErrorStateHintUnknownState {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintUnknownState() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+
+    public static void use(ErrorStateHintUnknownState f) {
+        f.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -22,7 +22,9 @@ public enum Kind {
         /** The object's state depends on the path taken, and no sequence of calls works for all of them */
         PATH_DEPENDENT_STATE,
         /** The object is in a state where no call with a state refinement is allowed */
-        FINAL_STATE
+        FINAL_STATE,
+        /** The object's state is unknown, so these are the calls that lead to a state that allows the failing call */
+        REACHING_CALLS
     }
 
     public static Hint general(String message) {

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

@@ -1,7 +1,10 @@
 package liquidjava.diagnostics.hints;
 
+import java.util.ArrayList;
 import java.util.Collection;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
@@ -12,6 +15,7 @@
 import liquidjava.processor.context.Variable;
 import liquidjava.processor.state_machine.State;
 import liquidjava.processor.state_machine.StateMachine;
+import liquidjava.processor.state_machine.Transition;
 import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -49,17 +53,34 @@ public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set
             return List.of();
 
         StateHints hints = new StateHints(machine, receiver);
+        if (hints.isUnknown(current))
+            return hints.reachingCalls(call, goal);
         return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream())
                 .toList();
     }
 
+    /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */
+    private List<Hint> reachingCalls(RefinedFunction call, Set<State> goal) {
+        Map<RefinedFunction, List<State>> sources = new LinkedHashMap<>();
+        for (Transition t : machine.transitionsEnabling(call))
+            sources.computeIfAbsent(t.method(), m -> new ArrayList<>()).add(t.from());
+        Stream<String> constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor);
+        Stream<String> calls = sources.entrySet().stream()
+                .map(e -> call(e.getKey()) + " (from " + names(e.getValue()) + ")");
+        List<String> ways = Stream.concat(constructors, calls).toList();
+        if (ways.isEmpty())
+            return List.of();
+        return List.of(new Hint(Kind.REACHING_CALLS, String.format(
+                "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways))));
+    }
+
     private List<Hint> howToReach(Set<State> current, RefinedFunction call, Set<State> goal) {
         Optional<List<List<RefinedFunction>>> search = machine.shortestPaths(current, call, MAX_SEQUENCES);
         if (search.isEmpty())
             return List.of();
         List<List<RefinedFunction>> sequences = search.get();
         if (sequences.isEmpty())
-            return machine.complete() && !isUnknown(current) ? List.of(unreachable(current, call, goal)) : List.of();
+            return machine.complete() ? List.of(unreachable(current, call, goal)) : List.of();
         if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH)
             return List.of();
         return sequences.stream().map(sequence -> callSequence(current, sequence)).toList();

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java

@@ -107,6 +107,11 @@ public Optional<List<List<RefinedFunction>>> shortestPaths(Set<State> current, R
         return Optional.of(List.of());
     }
 
+    /** The transitions from a state where {@code call} is not allowed to states where it is */
+    public List<Transition> transitionsEnabling(RefinedFunction call) {
+        return transitions.stream().filter(t -> !allows(Set.of(t.from()), call) && allows(t.to(), call)).toList();
+    }
+
     /** The constructors that create the object in a state where {@code call} is allowed */
     public List<RefinedFunction> constructorsEnabling(RefinedFunction call) {
         return constructors.entrySet().stream().filter(e -> allows(e.getValue(), call)).map(Map.Entry::getKey).toList();

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java

@@ -77,6 +77,12 @@ void receiverThatIsNotAVariableGetsNoHints() {
         assertHints("ErrorStateHintMethodCallReceiver.java");
     }
 
+    @Test
+    void unknownStateListsTheCallsThatLeadToTheExpectedState() {
+        assertHints("ErrorStateHintUnknownState.java", new Hint(Kind.REACHING_CALLS,
+                "The state of f is unknown here. To get it to open, use: f.open() (from created)"));
+    }
+
     @Test
     void classWithoutStateSetKeepsTheGeneralHint() {
         assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(