Show the states of named sets as values of their sets in state errors

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

@@ -4,7 +4,8 @@
 import liquidjava.specification.RefinementPredicate;
 import liquidjava.specification.StateSet;
 
-// A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses
+// A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses, and
+// not one of the names given to state sets without a name
 @StateSet(name = "Door", value = {"closed", "opened"}) // Expect: Error
 public class ErrorStateSetNames {}
 
@@ -23,3 +24,6 @@ class ErrorStateSetNameOfAnotherSet {}
 @StateSet(name = "size", value = {"empty", "full"}) // Expect: Error
 @RefinementPredicate("int size(ErrorStateSetNameOfARefinementPredicate b)")
 class ErrorStateSetNameOfARefinementPredicate {}
+
+@StateSet(name = "state2", value = {"closed", "opened"}) // Expect: Error
+class ErrorStateSetNameOfAGeneratedName {}

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

@@ -0,0 +1,21 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// a ghost named like a state of another class is not shown as that state
+@Ghost("boolean ready")
+public class ErrorStateValueGhostName {
+
+    @StateRefinement(from = "ready(this)")
+    void use() {}
+
+    static void test() {
+        ErrorStateValueGhostName sensor = new ErrorStateValueGhostName();
+        sensor.use(); // Expect: State Refinement Error
+    }
+}
+
+@StateSet(name = "phase", value = {"ready", "busy"})
+class ErrorStateValueGhostNameMachine {}

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

@@ -5,6 +5,7 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.function.Predicate;
+import java.util.function.UnaryOperator;
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.context.PlacementInCode;
@@ -18,10 +19,11 @@ record ErrorMessage(String text, DisplayNames names) {
 
     /**
      * Writes the facts of found about the values expected constrains and expected in frame, or only expected when
-     * showsFound rejects those facts; path conditions about other values stay in the derivation
+     * showsFound rejects those facts; path conditions about other values stay in the derivation. The facts are chosen
+     * on expected and found as given, and written as display rewrites them
      */
     static ErrorMessage of(Expression expected, VCSimplificationResult found, TranslationTable translationTable,
-            Predicate<Expression> showsFound, String frame) {
+            Predicate<Expression> showsFound, String frame, UnaryOperator<Expression> display) {
         Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), expected);
         // the names of the message first, then those only the original found has, each with the line of its value
         List<String> message = new ArrayList<>();
@@ -34,9 +36,9 @@ static ErrorMessage of(Expression expected, VCSimplificationResult found, Transl
             PlacementInCode placement = translationTable == null ? null : translationTable.get(name);
             return placement == null ? null : placement.getLine();
         });
-        String expectedText = ExpressionFormatter.format(expected, names);
+        String expectedText = ExpressionFormatter.format(display.apply(expected), names);
         String text = showsFound.test(shown)
-                ? String.format(frame, ExpressionFormatter.format(shown, names), expectedText)
+                ? String.format(frame, ExpressionFormatter.format(display.apply(shown), names), expectedText)
                 : String.format("expected %s but could not prove it", expectedText);
         return new ErrorMessage(text, names);
     }

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

@@ -7,6 +7,7 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.UnaryOperator;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.AliasExpansion;
@@ -51,8 +52,10 @@ public class RefinementError extends LJError {
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
             String customMessage, List<AliasWrapper> aliases) {
-        super("Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
-                shown -> !isTrue(shown), "%s is not a subtype of %s"), position, translationTable, customMessage);
+        super("Refinement Error",
+                ErrorMessage.of(expected.getExpression(), found, translationTable, shown -> !isTrue(shown),
+                        "%s is not a subtype of %s", UnaryOperator.identity()),
+                position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         Expression foundExpression = found.getImplication().toPredicate().getExpression();

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

@@ -3,6 +3,7 @@
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
 import java.util.List;
+import java.util.function.UnaryOperator;
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.categories.ErrorCategory;
@@ -26,15 +27,20 @@ public class StateRefinementError extends LJError {
     private final SourcePosition declarationPosition;
     private final StateErrorContext context;
 
+    /**
+     * @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
+     */
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
-            ErrorCategory category, StateErrorContext context) {
+            ErrorCategory category, StateErrorContext context, UnaryOperator<Expression> display) {
         super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
-                StateRefinementError::appliesGhost, "found %s but expected %s"), position, translationTable,
+                StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable,
                 customMessage);
         this.declarationPosition = declarationPosition;
-        this.expected = expected;
-        this.found = found;
+        this.expected = new Predicate(display.apply(expected.getExpression()));
+        this.found = found.map(display);
         this.context = context;
         hints.forEach(this::addHint);
         setCategory(category);

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

@@ -213,7 +213,8 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError {
                 SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue);
                 String name = stateSetName(nameValue, namePosition);
                 CtNewArray<String> states = (CtNewArray<String>) ann.getAllValues().get("value");
-                GhostFunction g = createStateSet(states, name != null ? name : String.format("state%d", set), element);
+                GhostFunction g = createStateSet(states, name != null ? name : String.format(Formats.STATE_SET, set),
+                        element);
                 stateSets.put(g, name != null ? namePosition : Utils.getAnnotationValuePosition(states));
                 checkStatesAreNotInAnotherSet(g, states, setOfState);
             }
@@ -262,6 +263,9 @@ private static String stateSetName(CtExpression<?> nameValue, SourcePosition pos
         if (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") || name.equals("false"))
             throw new CustomError(String.format(
                     "State set name '%s' must be an identifier that starts with a lowercase letter", name), position);
+        if (name.matches(Formats.STATE_SET_NAMES))
+            throw new CustomError(String.format("State set name '%s' is kept for state sets without a name", name),
+                    position);
         return name;
     }
 

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

@@ -17,6 +17,7 @@
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.StateValues;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.Var;
@@ -463,7 +464,8 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition
         VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified,
                 new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf));
         throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints,
-                category, context);
+                category, context,
+                e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()));
     }
 
     /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */

liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java

@@ -16,6 +16,8 @@
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.utils.Utils;
+import liquidjava.utils.constants.Formats;
 
 /**
  * Reads a state written as a value of its state set, {@code phase(e) == open}, as the state shorthand {@code open(e)},
@@ -91,6 +93,49 @@ private Optional<FunctionInvocation> stateOf(Expression set, Expression name) th
         return Optional.empty();
     }
 
+    /**
+     * {@code expression} with each state of a named set, {@code open(e)}, written as a value of its set,
+     * {@code phase(e) == open}, and {@code !open(e)} as {@code phase(e) != open}, for display. A state keeps the
+     * shorthand when its set has a generated name, such as {@code state1}, when sets with different names have a state
+     * of that name, or when a ghost that is not a state has that name: the name alone does not tell which it is
+     *
+     * @param ghosts
+     *            the ghosts that are not states, and the state set functions
+     */
+    public static Expression toSetForm(Expression expression, List<GhostState> states, List<GhostFunction> ghosts) {
+        return rewriteToSetForm(expression.clone(), states, ghosts);
+    }
+
+    private static Expression rewriteToSetForm(Expression e, List<GhostState> states, List<GhostFunction> ghosts) {
+        if (e instanceof UnaryExpression u && u.getOp().equals("!")) {
+            Optional<BinaryExpression> value = setValue(u.getExpression(), "!=", states, ghosts);
+            if (value.isPresent())
+                return value.get();
+        }
+        Optional<BinaryExpression> value = setValue(e, "==", states, ghosts);
+        if (value.isPresent())
+            return value.get();
+        for (int i = 0; i < e.getChildren().size(); i++)
+            e.setChild(i, rewriteToSetForm(e.getChildren().get(i), states, ghosts));
+        return e;
+    }
+
+    /** {@code set(e) op state} when {@code e} is the state {@code state(e)} of a set with one, given name */
+    private static Optional<BinaryExpression> setValue(Expression e, String op, List<GhostState> states,
+            List<GhostFunction> ghosts) {
+        if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1)
+                || ghosts.stream().anyMatch(g -> g.matches(invocation.getName()))
+                || states.stream().anyMatch(s -> s.getParent() == null && s.matches(invocation.getName())))
+            return Optional.empty();
+        List<String> setNames = states.stream().filter(s -> s.getParent() != null && s.matches(invocation.getName()))
+                .map(s -> s.getParent().getName()).distinct().toList();
+        if (setNames.size() != 1 || setNames.get(0).matches(Formats.STATE_SET_NAMES))
+            return Optional.empty();
+        FunctionInvocation set = new FunctionInvocation(qualifiedLike(invocation.getName(), setNames.get(0)),
+                List.of(invocation.getArgs().get(0).clone()));
+        return Optional.of(new BinaryExpression(set, op, new Var(Utils.getSimpleName(invocation.getName()))));
+    }
+
     /** The states of {@code set}, or only those named {@code name} when it is not null */
     private List<GhostState> statesOf(GhostFunction set, String name) {
         return states.stream().filter(s -> s.getParent() == set && (name == null || s.getName().equals(name))).toList();

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java

@@ -2,8 +2,11 @@
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.function.UnaryOperator;
 
 import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 
 /**
  * Result of simplifying VC implication chain
@@ -65,6 +68,15 @@ public List<String> getBinders() {
         return binderNames;
     }
 
+    /** This result with each refinement of its chain, and of the chains it was simplified from, rewritten by f */
+    public VCSimplificationResult map(UnaryOperator<Expression> f) {
+        VCImplication chain = implication.clone();
+        for (VCImplication row = chain; row != null; row = row.getNext())
+            if (row.getRefinement() != null)
+                row.setRefinement(new Predicate(f.apply(row.getRefinement().getExpression())));
+        return new VCSimplificationResult(chain, origin == null ? null : origin.map(f), simplification);
+    }
+
     @Override
     public String toString() {
         if (origin == null)

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java

@@ -5,4 +5,8 @@ public final class Formats {
     public static final String THIS = "this#%s";
     public static final String RET = "#ret_%d";
     public static final String ENUM = "%s.%s";
+    /** The name of a state set declared without one, numbered from 1 in the order of the declarations */
+    public static final String STATE_SET = "state%d";
+    /** The names {@link #STATE_SET} gives, which a state set cannot be given explicitly */
+    public static final String STATE_SET_NAMES = "state[1-9][0-9]*";
 }

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

@@ -343,7 +343,7 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() {
     void foundKeepsANamedStateSetByItsName() {
         StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0);
         assertEquals(
-                "found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)",
+                "found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked",
                 error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
     }
 
@@ -354,6 +354,13 @@ void queryWrittenWithItsStateSetIsOfferedAsAGuard() {
                 new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked"));
     }
 
+    @Test
+    void ghostNamedLikeAStateOfAnotherClassKeepsItsForm() {
+        StateRefinementError error = errors("ErrorStateValueGhostName.java", 1).get(0);
+        assertEquals("found ready(sensor) == false but expected ready(sensor)",
+                error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+    }
+
     @Test
     void classWithoutStateSetKeepsTheGeneralHint() {
         assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(

liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java

@@ -7,6 +7,7 @@
 
 import java.util.Arrays;
 import java.util.List;
+import java.util.function.UnaryOperator;
 
 import org.junit.jupiter.api.Test;
 
@@ -143,7 +144,7 @@ void stateMessageKeepsAStateReachingExpectedThroughAnAlias() {
                 new Predicate(RefinementsParser.createAST("full(box)", "")),
                 new VCSimplificationResult(
                         vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")),
-                new TranslationTable(), null, List.of(), null, null);
+                new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity());
         assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage());
     }