Named state sets: optional name on @StateSet

liquidjava-api/src/main/java/liquidjava/specification/StateSet.java

@@ -45,6 +45,20 @@
      */
     String[] value();
 
+    /**
+     * Optional name of the state set, used in messages and usable in predicates as a function that gives the current
+     * state of the set (e.g. {@code redo(this) == old(redo(this))}). It must be a lowercase identifier that is not
+     * already the name of a state, ghost or other state set of the class. Unnamed sets get a generated name.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @StateSet(name = "redo", value = {"redoable", "notRedoable"})
+     * }
+     * </pre>
+     */
+    String name() default "";
+
     /**
      * Container annotation used by {@link Repeatable} to support multiple state sets.
      */

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

@@ -3,8 +3,8 @@
 import liquidjava.specification.StateRefinement;
 import liquidjava.specification.StateSet;
 
-@StateSet({"closed", "opened"})
-@StateSet({"unlocked", "locked"})
+@StateSet(name = "doorState", value = {"closed", "opened"})
+@StateSet(name = "lockState", value = {"unlocked", "locked"})
 public class ErrorStateHintMultipleSets {
 
     @StateRefinement(to = "closed(this) && unlocked(this)")

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

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+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
+@StateSet(name = "Door", value = {"closed", "opened"}) // Expect: Error
+public class ErrorStateSetNames {}
+
+@StateSet(name = "locked", value = {"closed", "opened"}) // Expect: Error
+@StateSet({"unlocked", "locked"})
+class ErrorStateSetNameOfAState {}
+
+@StateSet(name = "lock", value = {"closed", "opened"}) // Expect: Error
+@Ghost("int lock")
+class ErrorStateSetNameOfAGhost {}
+
+@StateSet(name = "door", value = {"closed", "opened"}) // Expect: Error
+@StateSet(name = "door", value = {"unlocked", "locked"})
+class ErrorStateSetNameOfAnotherSet {}

liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java

@@ -26,6 +26,14 @@ public void execute() {
             default -> { }
         }
     }
+
+    // When canUndo() returns false its spec keeps the undo set by name, so the manager is still notUndoable
+    static void undoAfterAsking(javax.swing.undo.UndoableEdit edit) {
+        UndoManager undoManager = new UndoManager();
+        if (!undoManager.canUndo())
+            undoManager.addEdit(edit);
+        undoManager.undo();
+    }
 }
 
 enum StandardActions {

liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java

@@ -16,9 +16,9 @@
 // JDK 21: after end() the manager is one CompoundEdit, and undo/redo alternate over all edits at
 // once (AbstractUndoableEdit.hasBeenDone), so end() makes it undoable and not redoable.
 @ExternalRefinementsFor("javax.swing.undo.UndoManager")
-@StateSet({"start", "canEdit", "end"})
-@StateSet({"undoable", "notUndoable"})
-@StateSet({"redoable", "notRedoable"})
+@StateSet(name="phase", value={"start", "canEdit", "end"})
+@StateSet(name="undo", value={"undoable", "notUndoable"})
+@StateSet(name="redo", value={"redoable", "notRedoable"})
 public interface UndoManagerRefinementsExpert {
 
     @StateRefinement(to="start(this) && notUndoable(this) && notRedoable(this)")
@@ -81,8 +81,9 @@ public interface UndoManagerRefinementsExpert {
     // Queries: they never change the manager, they tell the verifier which state it is in. When it is
     // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose
     // state is unknown) the answer decides.
+    // When canUndo() returns false it keeps the undo set by name.
     @StateRefinement(from="undoable(this)", to="return && undoable(this)")
-    @StateRefinement(to="return ? undoable(this) : notUndoable(this)")
+    @StateRefinement(to="return ? undoable(this) : undo(this) == undo(old(this))")
     boolean canUndo();
 
     @StateRefinement(from="redoable(this)", to="return && redoable(this)")

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

@@ -119,12 +119,11 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition
     }
 
     @Override
-    protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
+    protected Optional<GhostFunction> createStateGhost(String name, CtElement element) {
         String klass = Utils.getSimpleName(prefix);
         if (klass != null) {
             CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
             List<String> params = List.of(klass);
-            String name = String.format("state%d", order);
             GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix);
             return Optional.of(gh);
         }

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

@@ -3,6 +3,7 @@
 import java.lang.annotation.Annotation;
 import java.util.Collections;
 import java.util.HashMap;
+import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
@@ -200,20 +201,60 @@ public Optional<String> getMessageFromAnnotation(CtElement element) {
     @SuppressWarnings("unchecked")
     public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
         int set = 0;
+        Map<GhostFunction, SourcePosition> namedSets = new LinkedHashMap<>();
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
             String an = ann.getAnnotationType().getQualifiedName();
             if (an.contentEquals("liquidjava.specification.StateSet")) {
                 set++;
-                createStateSet((CtNewArray<String>) ann.getAllValues().get("value"), set, element);
+                CtExpression<?> nameValue = ann.getValues().get("name");
+                SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue);
+                String name = stateSetName(nameValue, namePosition);
+                GhostFunction g = createStateSet((CtNewArray<String>) ann.getAllValues().get("value"),
+                        name != null ? name : String.format("state%d", set), element);
+                if (name != null)
+                    namedSets.put(g, namePosition);
             }
             if (an.contentEquals("liquidjava.specification.Ghost")) {
                 CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
                 createStateGhost(s.getValue(), element, Utils.getAnnotationValuePosition(s));
             }
         }
-    }
-
-    private void createStateSet(CtNewArray<String> e, int set, CtElement element) throws LJError {
+        // checked once every set and ghost of the class exists, so the order of the annotations does not matter
+        for (Map.Entry<GhostFunction, SourcePosition> named : namedSets.entrySet())
+            checkStateSetNameIsFree(named.getKey(), named.getValue());
+    }
+
+    /** The name given to a state set, or null when it has none */
+    private static String stateSetName(CtExpression<?> nameValue, SourcePosition position) throws LJError {
+        if (nameValue == null)
+            return null;
+        if (!(nameValue instanceof CtLiteral<?> literal && literal.getValue()instanceof String name))
+            throw new CustomError("State set name must be a string literal", position);
+        if (name.isEmpty())
+            return null;
+        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);
+        return name;
+    }
+
+    /** Reports a named state set whose name is also the name of a state, ghost or other state set of its class */
+    private void checkStateSetNameIsFree(GhostFunction set, SourcePosition position) throws LJError {
+        String name = set.getName();
+        String usedBy = null;
+        for (GhostState gs : context.getGhostState(set.getParentClassName()))
+            if (gs.getPrefix().equals(set.getPrefix()) && gs.getName().equals(name))
+                usedBy = gs.getParent() != null ? "a state" : "a ghost";
+        for (GhostFunction g : context.getGhosts())
+            if (usedBy == null && g != set && g.getPrefix().equals(set.getPrefix()) && g.getName().equals(name))
+                usedBy = context.getGhostStates().stream().anyMatch(gs -> gs.getParent() == g) ? "another state set"
+                        : "a ghost";
+        if (usedBy != null)
+            throw new CustomError(String.format("State set name '%s' is already the name of %s of %s", name, usedBy,
+                    set.getParentClassName()), position);
+    }
+
+    private GhostFunction createStateSet(CtNewArray<String> e, String name, CtElement element) throws LJError {
 
         // if any of the states starts with uppercase, throw error (reserved for alias)
         for (CtExpression<?> ce : e.getElements()) {
@@ -227,7 +268,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
             }
         }
 
-        Optional<GhostFunction> og = createStateGhost(set, element);
+        Optional<GhostFunction> og = createStateGhost(name, element);
         if (og.isEmpty()) {
             throw new RuntimeException("Error in creation of GhostFunction");
         }
@@ -252,6 +293,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
             }
             order++;
         }
+        return g;
     }
 
     protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
@@ -294,13 +336,12 @@ protected String getSimpleClassName(CtElement element) {
         return getEnclosingType(element).map(CtType::getSimpleName).orElse(null);
     }
 
-    protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
+    protected Optional<GhostFunction> createStateGhost(String name, CtElement element) {
         Optional<CtType<?>> enclosingType = getEnclosingType(element);
         if (enclosingType.isPresent()) {
             CtType<?> type = enclosingType.get();
             CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
             List<String> params = Collections.singletonList(type.getSimpleName());
-            String name = String.format("state%d", order);
             GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName());
             return Optional.of(gh);
         }

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

@@ -339,6 +339,14 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() {
                 error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
     }
 
+    @Test
+    void foundKeepsANamedStateSetByItsName() {
+        StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0);
+        assertEquals(
+                "found closed(d@26) && unlocked(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)",
+                error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+    }
+
     @Test
     void classWithoutStateSetKeepsTheGeneralHint() {
         assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(