Draw a StateRefinement without from only from the states it leaves uncovered

README.md

@@ -57,31 +57,19 @@ conditions, and in a `to` they are left out, since they change at the same time.
 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
-`@StateRefinement`s with `from`, it is also an entry transition in `entryTransitions`: how an object whose state is
-unknown (a field, a parameter or the result of a getter) enters the protocol, drawn as an arrow from the initial pseudo
-state. For example, `canUndo` below moves an object in an unknown state to `endDone` when it returns `true`, but keeps
-the state it was in otherwise:
+The verifier uses the first `@StateRefinement` of a method whose `from` matches the current state, and reads a
+`@StateRefinement` without `from` as `from = true`: the method can be called in any state and moves to `to`. It therefore
+goes from the states that the earlier ones do not cover, and never from the initial pseudo state, which only
+constructors and factory methods leave. For example, `canRedo` below goes from `notRedoable` to `redoable` when it
+returns `true` and stays in `notRedoable` otherwise, while in `redoable` the first alternative decides:
 
 ```java
-@StateRefinement(from="start(this)", to="!return && start(this)")
-@StateRefinement(from="canEdit(this)")
-@StateRefinement(from="endDone(this)")
-@StateRefinement(from="endUndone(this)", to="!return && endUndone(this)")
-@StateRefinement(to="return ? endDone(this) : true")
-boolean canUndo();
+@StateRefinement(from = "redo(this) == redoable", to = "redo(this) == redoable && return")
+@StateRefinement(to = "return ? redo(this) == redoable : redo(this) == notRedoable")
+boolean canRedo();
 ```
 
-```json
-"entryTransitions": [
-  {
-    "to": "endDone",
-    "label": "canUndo",
-    "toCondition": "return"
-  }
-]
-```
+`entryTransitions` is always empty and only kept so that clients still compile.
 
 ### JSON Output
 

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

@@ -7,6 +7,7 @@
  *
  * @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
+ * @param entryTransitions always empty, see {@link StateMachineEntryTransition}
  */
 public record StateMachine(
     String className,
@@ -15,7 +16,7 @@ public record StateMachine(
     List<String> states,
     List<StateMachineTransition> transitions,
     List<StateMachineInitialTransition> initialTransitions,
-    List<StateMachineEntryTransition> entryTransitions
+    @Deprecated List<StateMachineEntryTransition> entryTransitions
 ) {
     public StateMachine(String className, int stateSet, List<String> states, List<StateMachineTransition> transitions,
             List<StateMachineInitialTransition> initialTransitions, List<StateMachineEntryTransition> entryTransitions) {

src/main/java/liquidjava/fsm/StateMachineEntryTransition.java

@@ -2,8 +2,10 @@
 
 /**
  * Represents an entry transition in a state machine, a method that puts an object in an unknown state into a state
- * These come from a StateRefinement without from beside StateRefinements with from in the same method
+ * @deprecated no longer produced: a StateRefinement without from goes from the states the others do not cover, and only
+ * constructors and factory methods enter the state machine; kept so that clients still compile
  */
+@Deprecated
 public record StateMachineEntryTransition(String to, String label, String toCondition) {
 
     public StateMachineEntryTransition(String to, String label) {

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

@@ -162,13 +162,11 @@ private static StateMachine parseStateSet(CtType<?> ctType, List<CtMethod<?>> me
         }
         initialTransitions = new ArrayList<>(initialTransitions);
         initialTransitions.addAll(factoryTransitions);
-        List<StateMachineEntryTransition> entryTransitions = new ArrayList<>();
-        List<StateMachineTransition> transitions = getTransitions(methods, states, otherStates, entryTransitions);
-        if (transitions.isEmpty() && entryTransitions.isEmpty())
+        List<StateMachineTransition> transitions = getTransitions(methods, states, otherStates);
+        if (transitions.isEmpty())
             return null; // no transitions found
 
-        return new StateMachine(qualifiedName, stateSet, set.name(), states, transitions, initialTransitions,
-                entryTransitions);
+        return new StateMachine(qualifiedName, stateSet, set.name(), states, transitions, initialTransitions, List.of());
     }
 
     /**
@@ -481,11 +479,10 @@ private static String getParameterTypes(CtExecutable<?> element) {
      * @param methods the methods, without the constructors of interfaces
      * @param states the list of states
      * @param otherStates the states of the other state sets
-     * @param entryTransitions the list where the entry transitions are added
      * @return list of StateMachineTransition
      */
     private static List<StateMachineTransition> getTransitions(List<CtMethod<?>> methods, List<String> states,
-            List<String> otherStates, List<StateMachineEntryTransition> entryTransitions) {
+            List<String> otherStates) {
         List<StateMachineTransition> transitions = new ArrayList<>();
         for (CtMethod<?> method : methods) {
             // the verifier uses the first StateRefinement whose from matches, so the states that an earlier from
@@ -494,7 +491,7 @@ private static List<StateMachineTransition> getTransitions(List<CtMethod<?>> met
             for (CtAnnotation<?> annotation : method.getAnnotations()) {
                 if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) {
                     transitions.addAll(getTransitions(annotation, method.getSimpleName(), states, otherStates,
-                            coveredStates, entryTransitions));
+                            coveredStates));
                 }
             }
         }
@@ -504,17 +501,16 @@ private static List<StateMachineTransition> getTransitions(List<CtMethod<?>> met
     /**
      * Gets transitions from the given annotation
      * A StateRefinement without from goes from every state that an earlier StateRefinement of the method does not
-     * cover, and when some are covered it is also an entry transition for objects in an unknown state
+     * cover, as the verifier reads it with from = true; only constructors and factory methods enter the state machine
      * @param ann the CtAnnotation
      * @param method the method name
      * @param states the list of states
      * @param otherStates the states of the other state sets
      * @param coveredStates the states covered by the earlier StateRefinements of the method, updated with this one
-     * @param entryTransitions the list where the entry transitions are added
      * @return list of StateMachineTransition
      */
     private static List<StateMachineTransition> getTransitions(CtAnnotation<?> ann, String method, List<String> states,
-            List<String> otherStates, List<String> coveredStates, List<StateMachineEntryTransition> entryTransitions) {
+            List<String> otherStates, List<String> coveredStates) {
         List<StateMachineTransition> transitions = new ArrayList<>();
         String from = ann.getValueAsString("from");
         String to = ann.getValueAsString("to");
@@ -538,12 +534,6 @@ private static List<StateMachineTransition> getTransitions(CtAnnotation<?> ann,
                 ? parseStateSources(from, states)
                 : parsePostcondition(to, states, otherStates);
 
-        if (from.isEmpty() && !coveredStates.isEmpty()) {
-            for (TransitionSource toSource : toSources) {
-                entryTransitions.add(new StateMachineEntryTransition(toSource.from(), method, toSource.cond()));
-            }
-        }
-
         // create transitions for each combination of from and to states
         for (TransitionSource fromSource : fromSources) {
             for (TransitionSource toSource : toSources) {

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

@@ -81,10 +81,10 @@ public void testToOnlyTransition() {
     }
 
     @Test
-    public void testEntryTransition() {
-        // no from beside alternatives with from => entry transition, and edges only from the states they do not cover
-        StateMachine sm = StateMachineParser.parse(uri("EntryTransition.java"));
-        StateMachine expectedSm = stateMachine("EntryTransition", List.of("start", "canEdit", "endDone", "endUndone"),
+    public void testNoFromBesideFromIsNotEntryTransition() {
+        // no from beside alternatives with from => edges only from the states they do not cover, not from the start
+        StateMachine sm = StateMachineParser.parse(uri("NoFromBesideFrom.java"));
+        StateMachine expectedSm = stateMachine("NoFromBesideFrom", List.of("start", "canEdit", "endDone", "endUndone"),
                 List.of(new StateMachineTransition("start", "canEdit", "addEdit"),
                         new StateMachineTransition("canEdit", "canEdit", "addEdit"),
                         new StateMachineTransition("start", "start", "canUndo", null, "!return"),
@@ -98,15 +98,6 @@ public void testEntryTransition() {
                         new StateMachineTransition("endDone", "endUndone", "undo")),
                 List.of(new StateMachineInitialTransition("start")));
         assertStateMachineEquals(expectedSm, sm);
-        assertEquals(List.of(new StateMachineEntryTransition("endDone", "canUndo", "return"),
-                        new StateMachineEntryTransition("start", "reset")),
-                sm.entryTransitions());
-    }
-
-    @Test
-    public void testToOnlyTransitionHasNoEntryTransition() {
-        // no from without alternatives goes from every state, also in a known state
-        StateMachine sm = StateMachineParser.parse(uri("ToOnlyTransition.java"));
         assertEquals(List.of(), sm.entryTransitions());
     }
 

src/test/resources/fsm/EntryTransition.java → src/test/resources/fsm/NoFromBesideFrom.java

@@ -4,18 +4,18 @@
 import liquidjava.specification.StateSet;
 
 @StateSet({"start", "canEdit", "endDone", "endUndone"})
-public class EntryTransition {
+public class NoFromBesideFrom {
 
     @StateRefinement(to="start(this)")
-    public EntryTransition() {}
+    public NoFromBesideFrom() {}
 
     @StateRefinement(from="start(this) || canEdit(this)", to="canEdit(this)")
     public void addEdit() {}
 
     @StateRefinement(from="endDone(this)", to="endUndone(this)")
     public void undo() {}
 
-    // the from alternatives decide in a known state, the last one only for an object in an unknown state
+    // the from alternatives cover every state, so the last one adds no transition
     @StateRefinement(from="start(this)", to="!return && start(this)")
     @StateRefinement(from="canEdit(this)")
     @StateRefinement(from="endDone(this)")