Show states of named sets by their set in state hints and declared-here

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

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// The class and its superclass each have a set named phase: their states keep the shorthand, since phase == ready
+// and phase == busy would read as two values of one set
+@StateSet(name = "phase", value = {"ready", "done"})
+class ErrorStateSetNameInSuperclassBase {
+    @StateRefinement(to = "ready(this)")
+    ErrorStateSetNameInSuperclassBase() {}
+}
+
+@StateSet(name = "phase", value = {"busy", "idle"})
+public class ErrorStateSetNameInSuperclass extends ErrorStateSetNameInSuperclassBase {
+    @StateRefinement(to = "ready(this) && idle(this)")
+    ErrorStateSetNameInSuperclass() {}
+
+    @StateRefinement(from = "idle(this)", to = "busy(this)")
+    void start() {}
+
+    @StateRefinement(from = "ready(this) && busy(this)")
+    void use() {}
+
+    public static void main(String[] args) {
+        ErrorStateSetNameInSuperclass c = new ErrorStateSetNameInSuperclass();
+        c.use(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -75,6 +75,11 @@ public List<String> getMessageNotes() {
         return List.of();
     }
 
+    /** Lines printed under the excerpt of where the refinement is declared that explain it */
+    public List<String> getDeclarationNotes() {
+        return List.of();
+    }
+
     public void setPosition(SourcePosition pos) {
         if (pos == null || pos.getFile() == null)
             return;
@@ -145,8 +150,11 @@ public String toString() {
         if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) {
             sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET);
             String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true);
-            if (declarationSnippet != null)
+            if (declarationSnippet != null) {
                 sb.append(declarationSnippet);
+                for (String note : getDeclarationNotes())
+                    sb.append("  ").append(note).append("\n");
+            }
 
             sb.append("\n").append(declPos.getFile().getPath()).append(":").append(declPos.getLine())
                     .append(Colors.RESET).append("\n");

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

@@ -26,22 +26,27 @@ public class StateRefinementError extends LJError {
     private final VCSimplificationResult found;
     private final SourcePosition declarationPosition;
     private final StateErrorContext context;
+    private final List<String> declarationNotes;
 
     /**
      * @param display
      *            rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are
      *            chosen on them as given
+     * @param declarationNotes
+     *            lines that explain the declaration, printed under its excerpt
      */
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
-            ErrorCategory category, StateErrorContext context, UnaryOperator<Expression> display) {
+            ErrorCategory category, StateErrorContext context, UnaryOperator<Expression> display,
+            List<String> declarationNotes) {
         super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
                 StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable,
                 customMessage);
         this.declarationPosition = declarationPosition;
         this.expected = new Predicate(display.apply(expected.getExpression()));
         this.found = found.map(display);
         this.context = context;
+        this.declarationNotes = declarationNotes;
         hints.forEach(this::addHint);
         setCategory(category);
         if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression()))
@@ -56,6 +61,11 @@ private static boolean appliesGhost(Expression expression) {
                 || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost);
     }
 
+    @Override
+    public List<String> getDeclarationNotes() {
+        return declarationNotes;
+    }
+
     @Override
     public SourcePosition getDeclarationPosition() {
         return declarationPosition;

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

@@ -7,6 +7,7 @@
 import java.util.Set;
 import java.util.TreeSet;
 import java.util.function.Supplier;
+import java.util.function.Function;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
@@ -41,10 +42,21 @@ public final class StateHints {
     private final List<Set<State>> goals;
     /** The state sets the failing call checks, as indexes into {@link State#names()} */
     private final Set<Integer> checkedSets;
+    /** The name of the state set a state is shown as a value of, or empty when it keeps the shorthand */
+    private final Function<String, Optional<String>> setNameOf;
+    /**
+     * Whether states are shown as the error's message shows them, e.g. {@code lockState(d) == locked}: when some state
+     * set of the class is shown by its name
+     */
+    private final boolean asValues;
 
-    private StateHints(StateMachine machine, String receiver, RefinedFunction call) {
+    private StateHints(StateMachine machine, String receiver, RefinedFunction call,
+            Function<String, Optional<String>> setNameOf) {
         this.machine = machine;
         this.receiver = receiver;
+        this.setNameOf = setNameOf;
+        this.asValues = machine.states().stream().flatMap(s -> s.names().stream())
+                .anyMatch(name -> setNameOf.apply(name).isPresent());
         this.goals = machine.statesAllowingByRefinement(call);
         this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream())
                 .collect(Collectors.toCollection(TreeSet::new));
@@ -62,12 +74,15 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call)
      * @param checkedElsewhere
      *            whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose
      *            result says which state it is in
+     * @param setNameOf
+     *            the name of the state set the error's message shows a state as a value of, or empty when it shows the
+     *            shorthand
      */
     public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver,
-            ErrorCategory category, boolean checkedElsewhere) {
+            ErrorCategory category, boolean checkedElsewhere, Function<String, Optional<String>> setNameOf) {
         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, call);
+        StateHints hints = new StateHints(machine, receiver, call, setNameOf);
         if (hints.goals.isEmpty())
             return List.of();
 
@@ -107,7 +122,7 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver)
     private List<Hint> anyState(Set<State> current, RefinedFunction call, boolean checkedElsewhere) {
         String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver
                 : "The state of " + receiver + " is unknown here";
-        String message = known + ", and this call needs it to be " + needed();
+        String message = known + ", and this call needs " + (asValues ? "" : "it to be ") + needed();
         message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse("");
         List<Hint> hints = new ArrayList<>();
         hints.add(new Hint(Kind.NEEDED_STATE, message));
@@ -161,8 +176,8 @@ private List<Hint> guard(Set<State> current, RefinedFunction call) {
         String check = (negated ? "!" : "") + guardCall(guard.method());
         String arguments = guard.method().getArguments().isEmpty() ? ""
                 : ", filling in the arguments of " + declaration(guard.method());
-        String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s is %s", check, arguments,
-                !negated, receiver, needed());
+        String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s", check, arguments,
+                !negated, (asValues ? "" : receiver + " is ") + needed());
         return List.of(new Hint(Kind.GUARD, message));
     }
 
@@ -206,6 +221,11 @@ private Hint callSequence(Set<State> current, List<CallVariant> sequence, boolea
     }
 
     private Hint unreachable(Set<State> current, RefinedFunction call, boolean pathDependent) {
+        if (pathDependent && asValues)
+            return new Hint(Kind.PATH_DEPENDENT_STATE, String.format(
+                    "Depending on the path taken, %s here, and no sequence of calls moves %s from all of them to %s. "
+                            + "Make %s reach this line in the same state on every path",
+                    namesHere(current), receiver, needed(), receiver));
         if (pathDependent)
             return new Hint(Kind.PATH_DEPENDENT_STATE, String.format(
                     "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. "
@@ -222,13 +242,15 @@ private List<Hint> allowedCalls(Set<State> current) {
         if (!allowed.isEmpty()) {
             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",
-                    namesHere(current), receiver, list(signatures), others)));
+            return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("%s %s, %s can call: %s%s",
+                    asValues ? "When" : "In state", namesHere(current), receiver, list(signatures), others)));
         }
         boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty());
         if (machine.complete() && noCallsInAnyState)
-            return List.of(new Hint(Kind.FINAL_STATE,
-                    String.format("%s is in state %s, where none of its methods with state refinements can be called",
+            return List.of(new Hint(Kind.FINAL_STATE, asValues
+                    ? String.format("When %s, none of the methods of %s with state refinements can be called",
+                            namesHere(current), receiver)
+                    : String.format("%s is in state %s, where none of its methods with state refinements can be called",
                             receiver, namesHere(current))));
         return List.of();
     }
@@ -311,11 +333,26 @@ private String needed() {
         Set<State> goal = machine.ordered(goals.stream().flatMap(Set::stream).toList());
         if (goal.size() < machine.states().size())
             return names(goal);
-        return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or "));
+        return join(goals.stream().flatMap(g -> machine.describe(g).stream()).distinct().toList());
     }
 
-    private static String join(List<List<String>> groups) {
-        return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or "));
+    /** The groups joined by {@code or}, each in parentheses if it has several states and there are other groups */
+    private String join(List<List<String>> groups) {
+        return groups.stream().map(group -> {
+            String states = group.stream().map(this::stateName).collect(Collectors.joining(" and "));
+            return groups.size() > 1 && group.size() > 1 ? "(" + states + ")" : states;
+        }).collect(Collectors.joining(" or "));
+    }
+
+    /**
+     * A state as the error's message shows it, e.g. {@code lockState(d) == locked}, or {@code closed(d)} for a state
+     * that keeps the shorthand, or only its name if no state set of the class is shown by its name
+     */
+    private String stateName(String state) {
+        if (!asValues)
+            return state;
+        return setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state)
+                .orElse(state + "(" + receiver + ")");
     }
 
     private static String list(List<String> items) {

liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java

@@ -7,6 +7,8 @@ public class ObjectState {
 
     Predicate from;
     Predicate to;
+    /** {@code from} as written, before states written as values of their sets are read as the shorthand */
+    Predicate writtenFrom;
     SourcePosition fromPosition;
     SourcePosition toPosition;
     String message;
@@ -33,6 +35,14 @@ public void setTo(Predicate to) {
         this.to = to;
     }
 
+    public Predicate getWrittenFrom() {
+        return writtenFrom;
+    }
+
+    public void setWrittenFrom(Predicate writtenFrom) {
+        this.writtenFrom = writtenFrom;
+    }
+
     public SourcePosition getFromPosition() {
         return fromPosition;
     }
@@ -77,6 +87,7 @@ public ObjectState clone() {
         Predicate clonedFrom = from == null ? null : from.clone();
         Predicate clonedTo = to == null ? null : to.clone();
         ObjectState clone = new ObjectState(clonedFrom, clonedTo, message);
+        clone.setWrittenFrom(writtenFrom);
         clone.setFromPosition(fromPosition);
         clone.setToPosition(toPosition);
         return clone;

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

@@ -588,14 +588,15 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage) throws LJError {
-        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null);
+        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null,
+                List.of());
     }
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
-            StateErrorContext context) throws LJError {
+            StateErrorContext context, List<String> declarationNotes) throws LJError {
         vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints,
-                category, context);
+                category, context, declarationNotes);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

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

@@ -457,15 +457,16 @@ protected Predicate shownFound(Predicate found, Predicate expected) {
 
     protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
             Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
-            StateErrorContext context) throws StateRefinementError {
+            StateErrorContext context, List<String> declarationNotes) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected));
         VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified,
                 new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf));
         throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints,
                 category, context,
-                e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()));
+                e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()),
+                declarationNotes);
     }
 
     /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */