diff --git a/README.md b/README.md index 8f0c632..a2e0c83 100644 --- a/README.md +++ b/README.md @@ -46,6 +46,32 @@ A state machine only has the transitions that mention its states. States of othe 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. +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: + +```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(); +``` + +```json +"entryTransitions": [ + { + "to": "endDone", + "label": "canUndo", + "toCondition": "return" + } +] +``` + ### JSON Output ```json @@ -77,7 +103,8 @@ conditions, and in a `to` they are left out, since they change at the same time. "to": "open", "toCondition": null } - ] + ], + "entryTransitions": [] } ``` diff --git a/src/main/java/liquidjava/fsm/StateMachine.java b/src/main/java/liquidjava/fsm/StateMachine.java index 2b7ce94..1d25cbb 100644 --- a/src/main/java/liquidjava/fsm/StateMachine.java +++ b/src/main/java/liquidjava/fsm/StateMachine.java @@ -12,8 +12,14 @@ public record StateMachine( int stateSet, List states, List transitions, - List initialTransitions + List initialTransitions, + List entryTransitions ) { + public StateMachine(String className, int stateSet, List states, List transitions, + List initialTransitions) { + this(className, stateSet, states, transitions, initialTransitions, List.of()); + } + public StateMachine(String className, List states, List transitions, List initialTransitions) { this(className, 0, states, transitions, initialTransitions); diff --git a/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java b/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java new file mode 100644 index 0000000..83b3218 --- /dev/null +++ b/src/main/java/liquidjava/fsm/StateMachineEntryTransition.java @@ -0,0 +1,12 @@ +package liquidjava.fsm; + +/** + * 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 + */ +public record StateMachineEntryTransition(String to, String label, String toCondition) { + + public StateMachineEntryTransition(String to, String label) { + this(to, label, null); + } +} diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 4248651..1325903 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -123,11 +123,12 @@ private static StateMachine parseStateSet(CtType ctType, String qualifiedName } initialTransitions = new ArrayList<>(initialTransitions); initialTransitions.addAll(factoryTransitions); - List transitions = getTransitions(ctType, simpleClassName, states, otherStates); - if (transitions.isEmpty()) + List entryTransitions = new ArrayList<>(); + List transitions = getTransitions(ctType, simpleClassName, states, otherStates, entryTransitions); + if (transitions.isEmpty() && entryTransitions.isEmpty()) return null; // no transitions found - return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions); + return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions, entryTransitions); } /** @@ -277,18 +278,23 @@ private static String getParameterTypes(CtExecutable element) { * @param className the class name * @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(CtType ctType, String className, List states, - List otherStates) { + List otherStates, List entryTransitions) { List transitions = new ArrayList<>(); for (CtMethod method : ctType.getMethods()) { // for interfaces we skip constructor methods (methods with same name as class) if (ctType.isInterface() && method.getSimpleName().equals(className)) continue; + // the verifier uses the first StateRefinement whose from matches, so the states that an earlier from + // always matches are not reached by the later ones + List coveredStates = new ArrayList<>(); for (CtAnnotation annotation : method.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) { - transitions.addAll(getTransitions(annotation, method.getSimpleName(), states, otherStates)); + transitions.addAll(getTransitions(annotation, method.getSimpleName(), states, otherStates, + coveredStates, entryTransitions)); } } } @@ -297,14 +303,18 @@ private static List getTransitions(CtType ctType, Str /** * 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 * @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 otherStates, List coveredStates, List entryTransitions) { List transitions = new ArrayList<>(); String from = ann.getValueAsString("from"); String to = ann.getValueAsString("to"); @@ -315,11 +325,25 @@ private static List getTransitions(CtAnnotation ann, return transitions; // parse from and to expressions, the states of the other state sets in from are kept as conditions - List fromSources = from.isEmpty() ? allStateSources(states) : parsePrecondition(from, states); + List fromSources; + if (from.isEmpty()) { + fromSources = allStateSources(states).stream() + .filter(source -> !coveredStates.contains(source.from())).toList(); + } else { + fromSources = parsePrecondition(from, states); + fromSources.stream().filter(source -> source.cond() == null).map(TransitionSource::from) + .forEach(coveredStates::add); + } List toSources = fromMentionsStates && !toMentionsStates ? 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 8380a9d..2072f0a 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -79,6 +79,36 @@ public void testToOnlyTransition() { assertStateMachineEquals(expectedSm, sm); } + @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"), + List.of(new StateMachineTransition("start", "canEdit", "addEdit"), + new StateMachineTransition("canEdit", "canEdit", "addEdit"), + new StateMachineTransition("start", "start", "canUndo", null, "!return"), + new StateMachineTransition("canEdit", "canEdit", "canUndo"), + new StateMachineTransition("endDone", "endDone", "canUndo"), + new StateMachineTransition("endUndone", "endUndone", "canUndo", null, "!return"), + new StateMachineTransition("endDone", "endDone", "reset"), + new StateMachineTransition("start", "start", "reset"), + new StateMachineTransition("canEdit", "start", "reset"), + new StateMachineTransition("endUndone", "start", "reset"), + 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()); + } + @Test public void testMultipleInitialStates() { // overloading constructors with different initial states diff --git a/src/test/resources/fsm/EntryTransition.java b/src/test/resources/fsm/EntryTransition.java new file mode 100644 index 0000000..40cdbf9 --- /dev/null +++ b/src/test/resources/fsm/EntryTransition.java @@ -0,0 +1,30 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"start", "canEdit", "endDone", "endUndone"}) +public class EntryTransition { + + @StateRefinement(to="start(this)") + public EntryTransition() {} + + @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 + @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") + public boolean canUndo() { return false; } + + // the last alternative still goes from the states that the others do not cover + @StateRefinement(from="endDone(this)") + @StateRefinement(to="start(this)") + public void reset() {} +}