From 2b5519d5c9bce819d418bc5a9eb4618d2feeb30d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 26 Oct 2026 20:28:43 +0000 Subject: [PATCH] Draw a StateRefinement without from as an entry transition The verifier uses the first StateRefinement of a method whose from matches, so one without from only goes from the states that the earlier ones do not cover. Beside StateRefinements with from it is also how an object in an unknown state enters the protocol, now in entryTransitions. Closes #14 Co-Authored-By: Claude Opus 5.5 --- README.md | 29 +++++++++++++- .../java/liquidjava/fsm/StateMachine.java | 8 +++- .../fsm/StateMachineEntryTransition.java | 12 ++++++ .../liquidjava/fsm/StateMachineParser.java | 38 +++++++++++++++---- .../fsm/StateMachineParserTests.java | 30 +++++++++++++++ src/test/resources/fsm/EntryTransition.java | 30 +++++++++++++++ 6 files changed, 138 insertions(+), 9 deletions(-) create mode 100644 src/main/java/liquidjava/fsm/StateMachineEntryTransition.java create mode 100644 src/test/resources/fsm/EntryTransition.java 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() {} +}