Suggest the calls that make a failing state transition verify

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

@@ -0,0 +1,25 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open", "closed"})
+public class ErrorStateHintCallSequence {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintCallSequence() {}
+
+    @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 main(String[] args) {
+        ErrorStateHintCallSequence f = new ErrorStateHintCallSequence();
+        f.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,22 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open"})
+public class ErrorStateHintMethodCallReceiver {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintMethodCallReceiver() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    // a call added before the line would act on a different object than the one returned here
+    public static void use() {
+        new ErrorStateHintMethodCallReceiver().read(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"closed", "opened"})
+@StateSet({"unlocked", "locked"})
+public class ErrorStateHintMultipleSets {
+
+    @StateRefinement(to = "closed(this) && unlocked(this)")
+    public ErrorStateHintMultipleSets() {}
+
+    @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)")
+    public void open() {}
+
+    @StateRefinement(from = "opened(this)", to = "closed(this)")
+    public void close() {}
+
+    @StateRefinement(from = "closed(this) && unlocked(this)", to = "locked(this)")
+    public void lock() {}
+
+    @StateRefinement(from = "locked(this)", to = "unlocked(this)")
+    public void unlock() {}
+
+    public static void main(String[] args) {
+        ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets();
+        d.lock();
+        d.open(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open", "closed"})
+public class ErrorStateHintSeveralRefinements {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintSeveralRefinements() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    // allowed in created and in open, but by different refinements, so not when the object can be in either
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    @StateRefinement(from = "open(this)", to = "open(this)")
+    public void ensureOpen() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    public static void use(boolean ready) {
+        ErrorStateHintSeveralRefinements f = new ErrorStateHintSeveralRefinements();
+        if (ready)
+            f.open();
+        f.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,25 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"idle", "ready", "running"})
+public class ErrorStateHintTwoCalls {
+
+    @StateRefinement(to = "idle(this)")
+    public ErrorStateHintTwoCalls() {}
+
+    @StateRefinement(from = "idle(this)", to = "ready(this)")
+    public void prepare() {}
+
+    @StateRefinement(from = "ready(this)", to = "running(this)")
+    public void start() {}
+
+    @StateRefinement(from = "running(this)")
+    public void step() {}
+
+    public static void main(String[] args) {
+        ErrorStateHintTwoCalls r = new ErrorStateHintTwoCalls();
+        r.step(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -2,6 +2,8 @@
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
+import java.util.List;
+
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.processor.VCImplication;
@@ -21,7 +23,7 @@ public class StateRefinementError extends LJError {
     private final SourcePosition declarationPosition;
 
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
-            VCSimplificationResult found, TranslationTable translationTable, String customMessage) {
+            VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints) {
         super("State Refinement Error",
                 String.format("found %s but expected %s",
                         found.getImplication().toPredicate().getExpression().toDisplayString(),
@@ -30,7 +32,8 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
         this.declarationPosition = declarationPosition;
         this.expected = expected;
         this.found = found;
-        if (isTrue(found.getImplication().toPredicate().getExpression()))
+        hints.forEach(this::addHint);
+        if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression()))
             addHint(Hint.general(
                     "No state information is known for this object. Make sure its state is initialized and available at this point."));
     }

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

@@ -12,7 +12,11 @@ public record Hint(Kind kind, String message) {
 
     public enum Kind {
         /** A suggestion that does not come from a specific analysis */
-        GENERAL
+        GENERAL,
+        /** Calls to add before the failing call so the object reaches a state that allows it */
+        CALL_SEQUENCE,
+        /** The calls allowed in the object's current state */
+        AVAILABLE_CALLS
     }
 
     public static Hint general(String message) {

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

@@ -0,0 +1,99 @@
+package liquidjava.diagnostics.hints;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+import liquidjava.diagnostics.hints.Hint.Kind;
+import liquidjava.processor.context.RefinedFunction;
+import liquidjava.processor.context.Variable;
+import liquidjava.processor.state_machine.State;
+import liquidjava.processor.state_machine.StateMachine;
+import liquidjava.utils.Utils;
+import spoon.reflect.reference.CtTypeReference;
+
+/**
+ * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. Each hint only
+ * states what the machine proves, so a suggested sequence of calls always makes the failing call verify.
+ */
+public final class StateHints {
+
+    private static final int MAX_SEQUENCE_LENGTH = 3;
+    private static final int MAX_SEQUENCES = 3;
+    private static final int MAX_LISTED_CALLS = 5;
+
+    private final StateMachine machine;
+    private final String receiver;
+
+    private StateHints(StateMachine machine, String receiver) {
+        this.machine = machine;
+        this.receiver = receiver;
+    }
+
+    /**
+     * @param call
+     *            the method that cannot be called
+     * @param current
+     *            the states the receiver can be in before the call
+     * @param receiver
+     *            the receiver as written in the code
+     */
+    public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver) {
+        if (!machine.models(call) || current.isEmpty() || machine.allows(current, call))
+            return List.of(); // the machine cannot explain why the call failed
+        StateHints hints = new StateHints(machine, receiver);
+        return Stream.concat(hints.howToReach(current, call).stream(), hints.allowedCalls(current).stream()).toList();
+    }
+
+    private List<Hint> howToReach(Set<State> current, RefinedFunction call) {
+        Optional<List<List<RefinedFunction>>> search = machine.shortestPaths(current, call, MAX_SEQUENCES);
+        if (search.isEmpty() || search.get().isEmpty() || search.get().get(0).size() > MAX_SEQUENCE_LENGTH)
+            return List.of();
+        return search.get().stream().map(sequence -> callSequence(current, sequence)).toList();
+    }
+
+    private Hint callSequence(Set<State> current, List<RefinedFunction> sequence) {
+        Set<State> reached = current;
+        for (RefinedFunction method : sequence)
+            reached = machine.after(reached, method);
+        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, names(current), names(reached)));
+    }
+
+    private List<Hint> allowedCalls(Set<State> current) {
+        List<RefinedFunction> allowed = machine.allowedIn(current);
+        if (allowed.isEmpty())
+            return List.of();
+        List<String> signatures = allowed.stream().map(StateHints::signature).toList();
+        String others = machine.complete() ? "" : " (and possibly others)";
+        return List.of(new Hint(Kind.AVAILABLE_CALLS,
+                String.format("In state %s, %s can call: %s%s", names(current), receiver, list(signatures), others)));
+    }
+
+    private String call(RefinedFunction method) {
+        return receiver + "." + signature(method);
+    }
+
+    private static String signature(RefinedFunction method) {
+        return Utils.getSimpleName(method.getName()) + parameters(method);
+    }
+
+    private static String parameters(RefinedFunction function) {
+        return function.getArguments().stream().map(Variable::getType).map(CtTypeReference::getSimpleName)
+                .collect(Collectors.joining(", ", "(", ")"));
+    }
+
+    private static String names(Collection<State> states) {
+        return states.stream().map(State::name).collect(Collectors.joining(" or "));
+    }
+
+    private static String list(List<String> items) {
+        if (items.size() <= MAX_LISTED_CALLS)
+            return String.join(", ", items);
+        return String.join(", ", items.subList(0, MAX_LISTED_CALLS)) + ", ...";
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -8,6 +8,7 @@
 
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.*;
+import liquidjava.diagnostics.hints.Hint;
 import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
@@ -407,7 +408,12 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage) throws LJError {
-        vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage);
+        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of());
+    }
+
+    public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
+            Predicate expected, String customMessage, List<Hint> hints) throws LJError {
+        vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -12,6 +12,7 @@
 import liquidjava.diagnostics.errors.*;
 import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.hints.Hint;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
@@ -436,11 +437,11 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl
     }
 
     protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
-            Predicate found, Predicate expected, String customMessage) throws StateRefinementError {
+            Predicate found, Predicate expected, String customMessage, List<Hint> hints) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
-                customMessage);
+                customMessage, hints);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -4,13 +4,20 @@
 import java.util.*;
 import java.util.stream.Collectors;
 
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.errors.IllegalConstructorTransitionError;
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.SMTUnknownError;
+import liquidjava.diagnostics.hints.Hint;
+import liquidjava.diagnostics.hints.StateHints;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
+import liquidjava.processor.state_machine.State;
+import liquidjava.processor.state_machine.StateMachine;
+import liquidjava.processor.state_machine.StateMachineBuilder;
+import liquidjava.processor.state_machine.StateSolver;
 import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -636,11 +643,51 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom)
                     .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst()
                     .orElse(function.getPlacementInCode().getPosition());
+            List<Hint> hints = stateHints(tc, function, instanceName, prevState, invocation);
             tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState,
-                    expectedStatesDisjunction, message);
+                    expectedStatesDisjunction, message, hints);
         }
     }
 
+    /**
+     * Hints on how to fix a call to {@code function} made in a state that does not allow it. They are best effort: if
+     * they cannot be computed, the error is reported without them
+     */
+    private static List<Hint> stateHints(TypeChecker tc, RefinedFunction function, String instanceName, Predicate state,
+            CtElement invocation) {
+        Optional<String> receiver = receiverOf(invocation);
+        if (receiver.isEmpty() || !StateMachineBuilder.canModel(function))
+            return List.of();
+        try {
+            StateSolver solver = new StateSolver(tc, invocation.getPosition());
+            Optional<StateMachine> machine = StateMachineBuilder.build(tc, solver, function.getTargetClass(),
+                    invocation);
+            if (machine.isEmpty())
+                return List.of();
+            Set<State> current = solver.possibleStates(machine.get().states(), state, instanceName);
+            return StateHints.forCall(machine.get(), function, current, receiver.get());
+        } catch (RuntimeException e) {
+            // a failure to compute hints must not replace the error being reported
+            DebugLog.warn("Could not compute state hints: " + e.getMessage());
+            return List.of();
+        }
+    }
+
+    /**
+     * The receiver of {@code invocation} as written in the code, if it names an object that calls can be added to: a
+     * variable, a field or {@code this}
+     */
+    private static Optional<String> receiverOf(CtElement invocation) {
+        if (!(invocation instanceof CtInvocation<?> call))
+            return Optional.empty();
+        CtExpression<?> target = call.getTarget();
+        if (target == null || target.isImplicit())
+            return Optional.of(Keys.THIS);
+        if (target instanceof CtVariableRead<?> || target instanceof CtThisAccess<?>)
+            return Optional.of(target.toString());
+        return Optional.empty();
+    }
+
     private static Predicate checkOldMentions(Predicate transitionedState, String instanceName,
             String newInstanceName) {
         return transitionedState.changeOldMentions(instanceName, newInstanceName);