Read named state sets and states written as values of their sets

README.md

@@ -53,6 +53,9 @@ A class with several `@StateSet` annotations has one state machine per state set
 A state machine only has the transitions that mention its states. States of other state sets in a `from` are kept as
 conditions, and in a `to` they are left out, since they change at the same time.
 `parse` returns the state machine of the first state set.
+`stateSetName` is the name given to the state set, `@StateSet(name = "phase", value = {...})`, or null if it has none.
+As in the verifier, a state can also be written as a value of its state set, `phase(this) == open` or
+`phase(this) != open`, in either order and mixed with the shorthand `open(this)`.
 
 The verifier uses the first `@StateRefinement` of a method whose `from` matches the current state. A `@StateRefinement`
 without `from` therefore only goes from the states that the earlier ones do not cover. When it sits beside
@@ -86,6 +89,7 @@ boolean canUndo();
 {
   "className": "example.File",
   "stateSet": 0,
+  "stateSetName": null,
   "states": [
     "open",
     "closed"

src/main/java/liquidjava/fsm/StateMachine.java

@@ -6,15 +6,22 @@
  * Represents the state machine of one state set of a class
  *
  * @param stateSet the index of the state set among the class's StateSet annotations, in declaration order
+ * @param stateSetName the name given to the state set, or null if it has none
  */
 public record StateMachine(
     String className,
     int stateSet,
+    String stateSetName,
     List<String> states,
     List<StateMachineTransition> transitions,
     List<StateMachineInitialTransition> initialTransitions,
     List<StateMachineEntryTransition> entryTransitions
 ) {
+    public StateMachine(String className, int stateSet, List<String> states, List<StateMachineTransition> transitions,
+            List<StateMachineInitialTransition> initialTransitions, List<StateMachineEntryTransition> entryTransitions) {
+        this(className, stateSet, null, states, transitions, initialTransitions, entryTransitions);
+    }
+
     public StateMachine(String className, int stateSet, List<String> states, List<StateMachineTransition> transitions,
             List<StateMachineInitialTransition> initialTransitions) {
         this(className, stateSet, states, transitions, initialTransitions, List.of());

src/main/java/liquidjava/fsm/StateMachineParser.java

@@ -19,6 +19,7 @@
 import liquidjava.utils.Utils;
 import spoon.Launcher;
 import spoon.reflect.CtModel;
+import spoon.reflect.code.CtLiteral;
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtExecutable;
@@ -35,6 +36,9 @@ public class StateMachineParser {
 
     private record TransitionSource(String from, String cond) {}
 
+    // name is null when the state set has none
+    private record StateSet(String name, List<String> states) {}
+
     /**
      * Parses a class or interface for the given uri and extracts the state machine information
      * @param uri the document URI
@@ -96,15 +100,15 @@ public static List<StateMachine> parseAll(List<String> uris, String className) {
             // extract class name, state sets and methods, with those inherited from the specs of the supertypes
             List<CtTypeReference<?>> supertypes = getSupertypes(model, ctType);
             List<CtType<?>> specs = getSpecs(model, ctType, supertypes);
-            List<List<String>> stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList();
+            List<StateSet> stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList();
             List<CtMethod<?>> methods = getMethods(specs, supertypes);
             String qualifiedName = getClassName(ctType);
             List<StateMachine> stateMachines = new ArrayList<>();
             for (int i = 0; i < stateSets.size(); i++) {
                 List<String> otherStates = new ArrayList<>();
                 for (int j = 0; j < stateSets.size(); j++) {
                     if (j != i)
-                        otherStates.addAll(stateSets.get(j));
+                        otherStates.addAll(stateSets.get(j).states());
                 }
                 StateMachine sm = parseStateSet(ctType, methods, qualifiedName, i, stateSets.get(i), otherStates);
                 if (sm != null)
@@ -138,12 +142,13 @@ private static CtModel buildModel(List<String> uris) throws URISyntaxException {
      * @param methods the methods of the class, with those it inherits
      * @param qualifiedName the class name
      * @param stateSet the index of the state set
-     * @param states the states of the state set
+     * @param set the state set
      * @param otherStates the states of the other state sets
      * @return StateMachine or null if the state set has no transitions
      */
     private static StateMachine parseStateSet(CtType<?> ctType, List<CtMethod<?>> methods, String qualifiedName,
-            int stateSet, List<String> states, List<String> otherStates) {
+            int stateSet, StateSet set, List<String> otherStates) {
+        List<String> states = set.states();
         if (states.isEmpty())
             return null; // no states found
         String simpleClassName = Utils.getSimpleName(qualifiedName);
@@ -162,7 +167,8 @@ private static StateMachine parseStateSet(CtType<?> ctType, List<CtMethod<?>> me
         if (transitions.isEmpty() && entryTransitions.isEmpty())
             return null; // no transitions found
 
-        return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions, entryTransitions);
+        return new StateMachine(qualifiedName, stateSet, set.name(), states, transitions, initialTransitions,
+                entryTransitions);
     }
 
     /**
@@ -358,17 +364,23 @@ private static String getClassName(CtType<?> ctType) {
      * @param ctType the CtType (class or interface)
      * @return list of state sets, in declaration order
      */
-    private static List<List<String>> getStateSets(CtType<?> ctType) {
-        List<List<String>> stateSets = new ArrayList<>();
+    private static List<StateSet> getStateSets(CtType<?> ctType) {
+        List<StateSet> stateSets = new ArrayList<>();
         for (CtAnnotation<?> annotation : ctType.getAnnotations()) {
             if (annotation.getAnnotationType().getSimpleName().equals(STATE_SET_ANNOTATION)) {
                 String[] stateArray = (String[]) annotation.getValueAsObject("value");
-                stateSets.add(List.of(stateArray));
+                stateSets.add(new StateSet(getStateSetName(annotation), List.of(stateArray)));
             }
         }
         return stateSets;
     }
 
+    // an empty name is no name, as in the verifier
+    private static String getStateSetName(CtAnnotation<?> annotation) {
+        return annotation.getValues().get("name") instanceof CtLiteral<?> literal
+                && literal.getValue() instanceof String name && !name.isEmpty() ? name : null;
+    }
+
     /**
      * Gets the elements that represent constructors (actual constructors for classes, methods named after the class for interfaces)
      * @param ctType the CtType (class or interface)
@@ -600,26 +612,24 @@ private static List<TransitionSource> getTransitionSources(Expression expr, List
             return List.of(new TransitionSource(state, null));
         }
 
+        List<String> negatedStates = getNegatedStates(expr, states);
+        if (!negatedStates.isEmpty()) {
+            List<TransitionSource> sources = new ArrayList<>();
+            for (String possibleState : states) {
+                if (!negatedStates.contains(possibleState)) {
+                    sources.add(new TransitionSource(possibleState, null));
+                }
+            }
+            return sources;
+        }
+
         if (expr instanceof BinaryExpression bin) {
             String op = bin.getOperator();
             if (op.equals("&&")) {
                 return getConjunctionSources(bin, states, stateOnlyDisjunctions);
             } else if (op.equals("||")) {
                 return stateOnlyDisjunctions ? getStateSources(bin, states) : getDisjunctionSources(bin, states);
             }
-        } else if (expr instanceof UnaryExpression unary) {
-            if (unary.getOp().equals("!")) {
-                List<String> negatedStates = getStateExpressions(unary.getExpression(), states);
-                if (!negatedStates.isEmpty()) {
-                    List<TransitionSource> sources = new ArrayList<>();
-                    for (String possibleState : states) {
-                        if (!negatedStates.contains(possibleState)) {
-                            sources.add(new TransitionSource(possibleState, null));
-                        }
-                    }
-                    return sources;
-                }
-            }
         } else if (expr instanceof Ite ite) {
             List<TransitionSource> sources = new ArrayList<>();
             sources.addAll(addCondition(getTransitionSources(ite.getThen(), states, stateOnlyDisjunctions), ite.getCondition().toString()));
@@ -740,23 +750,19 @@ private static List<TransitionSource> getStateSources(Expression expr, List<Stri
     private static List<String> getStateExpressions(Expression expr, List<String> states) {
         List<String> stateExpressions = new ArrayList<>();
         String state = getStateName(expr, states);
+        List<String> negatedStates = getNegatedStates(expr, states);
         if (state != null) {
             stateExpressions.add(state);
+        } else if (!negatedStates.isEmpty()) {
+            // all except those in the expression
+            for (String possibleState : states) {
+                if (!negatedStates.contains(possibleState)) {
+                    stateExpressions.add(possibleState);
+                }
+            }
         } else if (expr instanceof BinaryExpression bin) {
             stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states));
             stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states));
-        } else if (expr instanceof UnaryExpression unary) {
-            if (unary.getOp().equals("!")) {
-                // all except those in the expression
-                List<String> negatedStates = getStateExpressions(unary.getExpression(), states);
-                if (!negatedStates.isEmpty()) {
-                    for (String possibleState : states) {
-                        if (!negatedStates.contains(possibleState)) {
-                            stateExpressions.add(possibleState);
-                        }
-                    }
-                }
-            }
         } else if (expr instanceof Ite ite) {
             // combine states from then and else branches
             stateExpressions.addAll(getStateExpressions(ite.getThen(), states));
@@ -765,15 +771,43 @@ private static List<String> getStateExpressions(Expression expr, List<String> st
         return stateExpressions;
     }
 
+    /**
+     * Gets the state an expression is in: open(this), or open written as a value of its state set, as in
+     * phase(this) == open or open == phase(this), which the verifier reads as open(this)
+     */
     private static String getStateName(Expression expr, List<String> states) {
         if (expr instanceof Var var) {
             return findState(var.getName(), states);
         } else if (expr instanceof FunctionInvocation func) {
             return findState(func.getName(), states);
+        } else if (expr instanceof BinaryExpression bin && bin.getOperator().equals("==")) {
+            String state = getStateValue(bin.getFirstOperand(), bin.getSecondOperand(), states);
+            return state != null ? state : getStateValue(bin.getSecondOperand(), bin.getFirstOperand(), states);
         }
         return null;
     }
 
+    private static String getStateValue(Expression stateSet, Expression value, List<String> states) {
+        return stateSet instanceof FunctionInvocation func && func.getArgs().size() == 1 && value instanceof Var var
+                ? findState(var.getName(), states)
+                : null;
+    }
+
+    /**
+     * Gets the states a negation excludes: those in e for !e, or open for phase(this) != open, which the verifier
+     * reads as !open(this)
+     * @return the excluded states, or none if expr is not the negation of a state
+     */
+    private static List<String> getNegatedStates(Expression expr, List<String> states) {
+        if (expr instanceof UnaryExpression unary && unary.getOp().equals("!")) {
+            return getStateExpressions(unary.getExpression(), states);
+        } else if (expr instanceof BinaryExpression bin && bin.getOperator().equals("!=")) {
+            String state = getStateName(new BinaryExpression(bin.getFirstOperand(), "==", bin.getSecondOperand()), states);
+            return state == null ? List.of() : List.of(state);
+        }
+        return List.of();
+    }
+
     private static String findState(String name, List<String> states) {
         if (states.contains(name)) {
             return name;

src/test/java/liquidjava/fsm/StateMachineParserTests.java

@@ -8,6 +8,7 @@
 
 import java.nio.file.Path;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.List;
 
 import org.junit.jupiter.api.Test;
@@ -342,6 +343,23 @@ public void testStateMachinePerStateSet() {
         assertEquals(List.of(), StateMachineParser.parseAll(uri("TwoStateClasses.java"), "fsm.Missing"));
     }
 
+    @Test
+    public void testStatesWrittenAsValuesOfTheirStateSets() {
+        List<StateMachine> sms = StateMachineParser.parseAll(uri("StateValues.java"));
+        assertEquals(Arrays.asList("phase", null), sms.stream().map(StateMachine::stateSetName).toList());
+        assertStateMachineEquals(stateMachine("StateValues", 0, List.of("open", "closed", "broken"),
+                List.of(new StateMachineTransition("open", "broken", "breakDown", "state2(this) == unlocked", null),
+                        new StateMachineTransition("closed", "broken", "breakDown", "state2(this) == unlocked", null),
+                        new StateMachineTransition("open", "closed", "close"),
+                        new StateMachineTransition("closed", "open", "openLocked")),
+                List.of(new StateMachineInitialTransition("open"))), sms.get(0));
+        assertStateMachineEquals(stateMachine("StateValues", 1, List.of("unlocked", "locked"),
+                List.of(new StateMachineTransition("unlocked", "unlocked", "breakDown", "phase(this) != broken", null),
+                        new StateMachineTransition("unlocked", "locked", "openLocked", "phase(this) == closed", null),
+                        new StateMachineTransition("locked", "locked", "openLocked", "phase(this) == closed", null)),
+                List.of(new StateMachineInitialTransition("unlocked"))), sms.get(1));
+    }
+
     private static final StateMachine FRAME = new StateMachine("java.awt.Frame", 0,
             List.of("displayable", "notDisplayable"),
             List.of(new StateMachineTransition("notDisplayable", "notDisplayable", "setUndecorated"),

src/test/resources/fsm/StateValues.java

@@ -0,0 +1,23 @@
+package fsm;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// states written as values of their state sets, in either order, with == and !=, mixed with the shorthand
+@StateSet(name = "phase", value = {"open", "closed", "broken"})
+@StateSet({"unlocked", "locked"})
+public class StateValues {
+
+    @StateRefinement(to = "phase(this) == open && unlocked(this)")
+    public StateValues() {}
+
+    @StateRefinement(from = "open == this.phase()", to = "closed(this)")
+    public void close() {}
+
+    // the unnamed state set is named state2
+    @StateRefinement(from = "phase() != broken && state2(this) == unlocked", to = "phase(this) == broken")
+    public void breakDown() {}
+
+    @StateRefinement(from = "phase(this) == closed", to = "phase(this) == open && state2(this) == locked")
+    public void openLocked() {}
+}