diff --git a/README.md b/README.md index 36702aa..074dde4 100644 --- a/README.md +++ b/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 diff --git a/src/main/java/liquidjava/fsm/StateMachine.java b/src/main/java/liquidjava/fsm/StateMachine.java index 80ce020..e8fb5a4 100644 --- a/src/main/java/liquidjava/fsm/StateMachine.java +++ b/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 states, List transitions, List initialTransitions, - List entryTransitions + @Deprecated List entryTransitions ) { public StateMachine(String className, int stateSet, List states, List transitions, List initialTransitions, List entryTransitions) { diff --git a/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java b/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java index 83b3218..0cea1fa 100644 --- a/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java +++ b/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) { diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 21691df..712d2f4 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -162,13 +162,11 @@ private static StateMachine parseStateSet(CtType ctType, List> me } initialTransitions = new ArrayList<>(initialTransitions); initialTransitions.addAll(factoryTransitions); - List entryTransitions = new ArrayList<>(); - List transitions = getTransitions(methods, states, otherStates, entryTransitions); - if (transitions.isEmpty() && entryTransitions.isEmpty()) + List 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 getTransitions(List> methods, List states, - List otherStates, List entryTransitions) { + List otherStates) { List 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 getTransitions(List> 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 getTransitions(List> 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 getTransitions(CtAnnotation ann, String method, List states, - List otherStates, List coveredStates, List entryTransitions) { + List otherStates, List coveredStates) { List transitions = new ArrayList<>(); String from = ann.getValueAsString("from"); String to = ann.getValueAsString("to"); @@ -538,12 +534,6 @@ private static List 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) { diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index b9721a4..f374bf9 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/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()); } diff --git a/src/test/resources/fsm/EntryTransition.java b/src/test/resources/fsm/NoFromBesideFrom.java similarity index 84% rename from src/test/resources/fsm/EntryTransition.java rename to src/test/resources/fsm/NoFromBesideFrom.java index 40cdbf9..915a121 100644 --- a/src/test/resources/fsm/EntryTransition.java +++ b/src/test/resources/fsm/NoFromBesideFrom.java @@ -4,10 +4,10 @@ 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() {} @@ -15,7 +15,7 @@ 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)")