diff --git a/README.md b/README.md index 44c6c8a..8f0c632 100644 --- a/README.md +++ b/README.md @@ -36,13 +36,22 @@ import liquidjava.fsm.StateMachineParser; StateMachine stateMachine = StateMachineParser.parse(path.toUri().toString()); // in a file with several classes, or for a verifier error's StateErrorContext#receiverClass StateMachine named = StateMachineParser.parse(path.toUri().toString(), "example.File"); +// one state machine per @StateSet, in declaration order +List stateMachines = StateMachineParser.parseAll(path.toUri().toString()); ``` +A class with several `@StateSet` annotations has one state machine per state set, since each changes independently. +`stateSet` is the index of the state set, the same order the verifier uses in `StateErrorContext`. +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. + ### JSON Output ```json { "className": "example.File", + "stateSet": 0, "states": [ "open", "closed" diff --git a/src/main/java/liquidjava/fsm/StateMachine.java b/src/main/java/liquidjava/fsm/StateMachine.java index 055344e..2b7ce94 100644 --- a/src/main/java/liquidjava/fsm/StateMachine.java +++ b/src/main/java/liquidjava/fsm/StateMachine.java @@ -3,11 +3,19 @@ import java.util.List; /** - * Represents a state machine + * 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 */ public record StateMachine( String className, + int stateSet, List states, List transitions, List initialTransitions -) {} +) { + public StateMachine(String className, List states, List transitions, + List initialTransitions) { + this(className, 0, states, transitions, initialTransitions); + } +} diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index a9a77ad..4248651 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -39,9 +39,30 @@ public static StateMachine parse(String uri) { * Parses the class or interface with the given name in the given uri, for files that declare several * @param uri the document URI * @param className the qualified class name, or the name given by ExternalRefinementsFor - * @return StateMachine or null if none found + * @return StateMachine of the first state set with transitions, or null if none found */ public static StateMachine parse(String uri, String className) { + List stateMachines = parseAll(uri, className); + return stateMachines.isEmpty() ? null : stateMachines.get(0); + } + + /** + * Parses a class or interface for the given uri and extracts one state machine per state set + * @param uri the document URI + * @return the state machines of the state sets with transitions, in declaration order + */ + public static List parseAll(String uri) { + return parseAll(uri, null); + } + + /** + * Parses the class or interface with the given name in the given uri and extracts one state machine per state set + * Each state set changes independently, so a state machine only has the transitions that mention its states + * @param uri the document URI + * @param className the qualified class name, or the name given by ExternalRefinementsFor + * @return the state machines of the state sets with transitions, in declaration order + */ + public static List parseAll(String uri, String className) { try { String filePath = Paths.get(new URI(uri)).toString(); Launcher launcher = new Launcher(); @@ -54,36 +75,61 @@ public static StateMachine parse(String uri, String className) { // get class or interface CtType ctType = getType(model, className); if (ctType == null) - return null; // no class or interface found + return List.of(); // no class or interface found - // extract class name and states - List states = getStates(ctType); - if (states == null || states.isEmpty()) - return null; // no states found + // extract class name and state sets + List> stateSets = getStateSets(ctType); String qualifiedName = getClassName(ctType); - String simpleClassName = Utils.getSimpleName(qualifiedName); - - // get initial transitions and method transitions - List factoryTransitions = getFactoryTransitions(ctType, simpleClassName, states); - List initialTransitions = getInitialTransitions(ctType, simpleClassName, states); - // interfaces only have an implicit initial state when there are no factory methods - if (initialTransitions.isEmpty() && (ctType instanceof CtClass || factoryTransitions.isEmpty())) { - initialTransitions = getDefaultInitialTransitions(ctType, simpleClassName, states.get(0)); + List stateMachines = new ArrayList<>(); + for (int i = 0; i < stateSets.size(); i++) { + List otherStates = new ArrayList<>(); + for (int j = 0; j < stateSets.size(); j++) { + if (j != i) + otherStates.addAll(stateSets.get(j)); + } + StateMachine sm = parseStateSet(ctType, qualifiedName, i, stateSets.get(i), otherStates); + if (sm != null) + stateMachines.add(sm); } - initialTransitions = new ArrayList<>(initialTransitions); - initialTransitions.addAll(factoryTransitions); - List transitions = getTransitions(ctType, simpleClassName, states); - if (transitions.isEmpty()) - return null; // no transitions found - - return new StateMachine(qualifiedName, states, transitions, initialTransitions); + return stateMachines; } catch (Exception e) { e.printStackTrace(); - return null; + return List.of(); } } + /** + * Extracts the state machine of one state set + * @param ctType the CtType (class or interface) + * @param qualifiedName the class name + * @param stateSet the index of the state set + * @param states the states of 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, String qualifiedName, int stateSet, + List states, List otherStates) { + if (states.isEmpty()) + return null; // no states found + String simpleClassName = Utils.getSimpleName(qualifiedName); + + // get initial transitions and method transitions + List factoryTransitions = getFactoryTransitions(ctType, simpleClassName, states, otherStates); + List initialTransitions = getInitialTransitions(ctType, simpleClassName, states, otherStates); + // interfaces only have an implicit initial state when there are no factory methods + if (initialTransitions.isEmpty() && (ctType instanceof CtClass || factoryTransitions.isEmpty())) { + initialTransitions = getDefaultInitialTransitions(ctType, simpleClassName, states.get(0)); + } + initialTransitions = new ArrayList<>(initialTransitions); + initialTransitions.addAll(factoryTransitions); + List transitions = getTransitions(ctType, simpleClassName, states, otherStates); + if (transitions.isEmpty()) + return null; // no transitions found + + return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions); + } + /** * Finds the class or interface in the model with the given name, or the first one if the name is null * @param model the CtModel @@ -115,18 +161,19 @@ private static String getClassName(CtType ctType) { } /** - * Gets the possible states from a class or interface + * Gets the state sets from a class or interface * @param ctType the CtType (class or interface) - * @return list of states + * @return list of state sets, in declaration order */ - private static List getStates(CtType ctType) { + private static List> getStateSets(CtType ctType) { + List> stateSets = new ArrayList<>(); for (CtAnnotation annotation : ctType.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(STATE_SET_ANNOTATION)) { String[] stateArray = (String[]) annotation.getValueAsObject("value"); - return List.of(stateArray); + stateSets.add(List.of(stateArray)); } } - return null; + return stateSets; } /** @@ -149,9 +196,11 @@ private static Collection> getConstructorElements(CtTy * @param ctType the CtType (class or interface) * @param className the class name * @param states the list of states + * @param otherStates the states of the other state sets * @return initial transitions */ - private static List getInitialTransitions(CtType ctType, String className, List states) { + private static List getInitialTransitions(CtType ctType, String className, + List states, List otherStates) { List initialTransitions = new ArrayList<>(); for (CtExecutable element : getConstructorElements(ctType, className)) { String signature = getConstructorSignature(element, className); @@ -159,7 +208,7 @@ private static List getInitialTransitions(CtType< for (CtAnnotation annotation : element.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) { String to = annotation.getValueAsString("to"); - List transitions = parseInitialTransitions(to, states, signature); + List transitions = parseInitialTransitions(to, states, otherStates, signature); initialTransitions.addAll(transitions); hasExplicitInitialState |= !transitions.isEmpty(); } @@ -194,9 +243,11 @@ private static String getConstructorSignature(CtExecutable element, String cl * @param ctType the CtType (class or interface) * @param className the class name * @param states the list of states + * @param otherStates the states of the other state sets * @return initial transitions */ - private static List getFactoryTransitions(CtType ctType, String className, List states) { + private static List getFactoryTransitions(CtType ctType, String className, + List states, List otherStates) { List initialTransitions = new ArrayList<>(); for (CtMethod method : ctType.getMethods()) { if (ctType.isClass() && !method.isStatic()) @@ -207,7 +258,7 @@ private static List getFactoryTransitions(CtType< for (CtAnnotation annotation : method.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(REFINEMENT_ANNOTATION)) { String refinement = annotation.getValueAsString("value"); - initialTransitions.addAll(parseInitialTransitions(refinement, states, signature)); + initialTransitions.addAll(parseInitialTransitions(refinement, states, otherStates, signature)); } } } @@ -225,9 +276,11 @@ private static String getParameterTypes(CtExecutable element) { * @param ctType the CtType (class or interface) * @param className the class name * @param states the list of states + * @param otherStates the states of the other state sets * @return list of StateMachineTransition */ - private static List getTransitions(CtType ctType, String className, List states) { + private static List getTransitions(CtType ctType, String className, List states, + List otherStates) { List transitions = new ArrayList<>(); for (CtMethod method : ctType.getMethods()) { // for interfaces we skip constructor methods (methods with same name as class) @@ -235,7 +288,7 @@ private static List getTransitions(CtType ctType, Str continue; for (CtAnnotation annotation : method.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) { - transitions.addAll(getTransitions(annotation, method.getSimpleName(), states)); + transitions.addAll(getTransitions(annotation, method.getSimpleName(), states, otherStates)); } } } @@ -247,18 +300,25 @@ private static List getTransitions(CtType ctType, Str * @param ann the CtAnnotation * @param method the method name * @param states the list of states + * @param otherStates the states of the other state sets * @return list of StateMachineTransition */ - private static List getTransitions(CtAnnotation ann, String method, List states) { + private static List getTransitions(CtAnnotation ann, String method, List states, + List otherStates) { List transitions = new ArrayList<>(); String from = ann.getValueAsString("from"); String to = ann.getValueAsString("to"); + boolean fromMentionsStates = mentionsStates(from, states); + boolean toMentionsStates = mentionsStates(to, states); + // the states of this state set do not change + if (!fromMentionsStates && !toMentionsStates) + return transitions; - // parse from and to expressions + // 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 toSources = !from.isEmpty() && to.isEmpty() + List toSources = fromMentionsStates && !toMentionsStates ? parseStateSources(from, states) - : parsePostcondition(to, states); + : parsePostcondition(to, states, otherStates); // create transitions for each combination of from and to states for (TransitionSource fromSource : fromSources) { @@ -286,12 +346,42 @@ private static List parsePrecondition(String expr, List parsePostcondition(String expr, List states) { + private static List parsePostcondition(String expr, List states, List otherStates) { if (expr == null || expr.isEmpty()) return new ArrayList<>(); - Expression ast = RefinementsParser.createAST(expr, ""); + Expression ast = withoutStates(RefinementsParser.createAST(expr, ""), otherStates); + if (ast == null) return new ArrayList<>(); return getTransitionSources(ast, states, true); } + /** + * Removes the conjuncts that set a state of another state set, which change at the same time and are not conditions + * @param expr the postcondition + * @param otherStates the states of the other state sets + * @return the postcondition without them, or null if nothing is left + */ + private static Expression withoutStates(Expression expr, List otherStates) { + if (getStateName(expr, otherStates) != null) { + return null; + } + if (expr instanceof BinaryExpression bin && bin.getOperator().equals("&&")) { + Expression left = withoutStates(bin.getFirstOperand(), otherStates); + Expression right = withoutStates(bin.getSecondOperand(), otherStates); + if (left == null) return right; + if (right == null) return left; + return new BinaryExpression(left, "&&", right); + } else if (expr instanceof Ite ite) { + Expression then = withoutStates(ite.getThen(), otherStates); + Expression otherwise = withoutStates(ite.getElse(), otherStates); + return new Ite(ite.getCondition(), then == null ? ite.getThen() : then, otherwise == null ? ite.getElse() : otherwise); + } + return expr; + } + + private static boolean mentionsStates(String expr, List states) { + if (expr == null || expr.isEmpty()) return false; + return !getStateExpressions(RefinementsParser.createAST(expr, ""), states).isEmpty(); + } + private static List getTransitionSources(Expression expr, List states, boolean stateOnlyDisjunctions) { String state = getStateName(expr, states); if (state != null) { @@ -406,10 +496,10 @@ private static String negateCondition(Expression expr) { } private static List parseInitialTransitions(String expr, List states, - String constructorSignature) { + List otherStates, String constructorSignature) { if (expr == null || expr.isEmpty()) return new ArrayList<>(); List initialTransitions = new ArrayList<>(); - for (TransitionSource source : parsePostcondition(expr, states)) { + for (TransitionSource source : parsePostcondition(expr, states, otherStates)) { initialTransitions.add(new StateMachineInitialTransition(source.from(), source.cond(), constructorSignature)); } return initialTransitions; diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index c346dd1..8380a9d 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -274,23 +274,63 @@ public void testClassSelectedByName() { assertNull(StateMachineParser.parse(uri("TwoStateClasses.java"), "fsm.Missing")); } + @Test + public void testStateMachinePerStateSet() { + // each state set only has the transitions that mention its states, the other state sets stay as conditions + List sms = StateMachineParser.parseAll(uri("TwoStateSets.java")); + assertEquals(2, sms.size()); + assertStateMachineEquals(stateMachine("TwoStateSets", 0, List.of("startTiling", "tilingExplicit", "tilingSet"), + List.of(new StateMachineTransition("startTiling", "startTiling", "resetTiling", "compressionSet(this)", null), + new StateMachineTransition("tilingExplicit", "startTiling", "resetTiling", "compressionSet(this)", null), + new StateMachineTransition("tilingSet", "startTiling", "resetTiling", "compressionSet(this)", null), + new StateMachineTransition("tilingExplicit", "tilingSet", "setTiling"), + new StateMachineTransition("startTiling", "tilingExplicit", "setTilingMode", null, "mode == 2"), + new StateMachineTransition("startTiling", "startTiling", "setTilingMode", null, "!(mode == 2)"), + new StateMachineTransition("tilingExplicit", "tilingExplicit", "setTilingMode", null, "mode == 2"), + new StateMachineTransition("tilingExplicit", "startTiling", "setTilingMode", null, "!(mode == 2)"), + new StateMachineTransition("tilingSet", "tilingExplicit", "setTilingMode", null, "mode == 2"), + new StateMachineTransition("tilingSet", "startTiling", "setTilingMode", null, "!(mode == 2)"), + new StateMachineTransition("tilingSet", "tilingSet", "write", "compressionSet(this)", null)), + List.of(new StateMachineInitialTransition("startTiling"), + new StateMachineInitialTransition("tilingExplicit"))), sms.get(0)); + // the second constructor does not set a compression state, so it starts in the first one + assertStateMachineEquals(stateMachine("TwoStateSets", 1, + List.of("startCompression", "compressionExplicit", "compressionSet"), + List.of(new StateMachineTransition("compressionSet", "compressionSet", "resetTiling"), + new StateMachineTransition("startCompression", "compressionExplicit", "setCompressionMode", null, "mode == 2"), + new StateMachineTransition("startCompression", "startCompression", "setCompressionMode", null, "!(mode == 2)"), + new StateMachineTransition("compressionExplicit", "compressionExplicit", "setCompressionMode", null, "mode == 2"), + new StateMachineTransition("compressionExplicit", "startCompression", "setCompressionMode", null, "!(mode == 2)"), + new StateMachineTransition("compressionSet", "compressionExplicit", "setCompressionMode", null, "mode == 2"), + new StateMachineTransition("compressionSet", "startCompression", "setCompressionMode", null, "!(mode == 2)"), + new StateMachineTransition("compressionExplicit", "compressionSet", "setCompressionType"), + new StateMachineTransition("compressionSet", "compressionSet", "write", "tilingSet(this)", null)), + List.of(new StateMachineInitialTransition("startCompression"), + new StateMachineInitialTransition("startCompression"))), sms.get(1)); + // parse keeps returning the first state set + assertEquals(sms.get(0), StateMachineParser.parse(uri("TwoStateSets.java"))); + assertEquals(List.of(), StateMachineParser.parseAll(uri("TwoStateClasses.java"), "fsm.Missing")); + } + @Test public void testVerifierStatesAreStatesOfTheDiagram() { - for (String directory : List.of("errors/door", "errors/tree", "errors/udp")) { + for (String directory : List.of("errors/door", "errors/tree", "errors/udp", "errors/image")) { List errors = stateErrors(directory); assertFalse(errors.isEmpty(), "Expected state refinement errors in " + directory); for (StateRefinementError error : errors) { StateErrorContext context = error.getContext(); assertNotNull(context, "Expected the verifier's states for " + error.getMessage()); - StateMachine sm = StateMachineParser.parse(error.getDeclarationPosition().getFile().toURI().toString(), - context.receiverClass()); - assertNotNull(sm, "Expected a diagram of " + context.receiverClass()); + List sms = StateMachineParser.parseAll( + error.getDeclarationPosition().getFile().toURI().toString(), context.receiverClass()); + assertFalse(sms.isEmpty(), "Expected a diagram of " + context.receiverClass()); List> verifierStates = new ArrayList<>(context.possibleStates()); if (context.acceptedStates() != null) verifierStates.addAll(context.acceptedStates()); - // the diagram shows the first state set - for (List state : verifierStates) - assertTrue(sm.states().contains(state.get(0)), state.get(0) + " is not in " + sm.states()); + // the verifier names a state in each state set in the same order as the diagrams + for (StateMachine sm : sms) + for (List state : verifierStates) + assertTrue(sm.states().contains(state.get(sm.stateSet())), + state.get(sm.stateSet()) + " is not in " + sm.states()); } } } @@ -298,6 +338,7 @@ public void testVerifierStatesAreStatesOfTheDiagram() { private static void assertStateMachineEquals(StateMachine expected, StateMachine actual) { assertNotNull(actual, "State machine should not be null"); assertEquals(expected.className(), actual.className(), "Class names should match"); + assertEquals(expected.stateSet(), actual.stateSet(), "State sets should match"); assertEquals(expected.initialTransitions(), actual.initialTransitions().stream() .map(transition -> new StateMachineInitialTransition(transition.to(), transition.toCondition())) .toList(), "Initial transitions should match"); @@ -307,8 +348,13 @@ private static void assertStateMachineEquals(StateMachine expected, StateMachine private static StateMachine stateMachine(String className, List states, List transitions, List initialTransitions) { + return stateMachine(className, 0, states, transitions, initialTransitions); + } + + private static StateMachine stateMachine(String className, int stateSet, List states, + List transitions, List initialTransitions) { String qualifiedName = className.contains(".") ? className : "fsm." + className; - return new StateMachine(qualifiedName, states, transitions, initialTransitions); + return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions); } private static List stateErrors(String directory) { diff --git a/src/test/resources/fsm/TwoStateSets.java b/src/test/resources/fsm/TwoStateSets.java new file mode 100644 index 0000000..674c3b8 --- /dev/null +++ b/src/test/resources/fsm/TwoStateSets.java @@ -0,0 +1,40 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"startTiling", "tilingExplicit", "tilingSet"}) +@StateSet({"startCompression", "compressionExplicit", "compressionSet"}) +public class TwoStateSets { + + // sets the state of both state sets + @StateRefinement(to="startTiling(this) && startCompression(this)") + public TwoStateSets() {} + + // only sets the tiling state, the compression state starts in the first state + @StateRefinement(to="tilingExplicit(this)") + public TwoStateSets(int mode) {} + + @StateRefinement(to="mode == 2 ? tilingExplicit(this) : startTiling(this)") + public void setTilingMode(int mode) {} + + @StateRefinement(from="tilingExplicit(this)", to="tilingSet(this)") + public void setTiling(int width) {} + + @StateRefinement(to="mode == 2 ? compressionExplicit(this) : startCompression(this)") + public void setCompressionMode(int mode) {} + + @StateRefinement(from="compressionExplicit(this)", to="compressionSet(this)") + public void setCompressionType(String type) {} + + // requires a state of each state set + @StateRefinement(from="tilingSet(this) && compressionSet(this)") + public void write() {} + + // requires a compression state and changes the tiling state + @StateRefinement(from="compressionSet(this)", to="startTiling(this)") + public void resetTiling() {} + + // does not refer to any state + public void setProgressiveMode(int mode) {} +} diff --git a/src/test/resources/fsm/errors/image/ImageParams.java b/src/test/resources/fsm/errors/image/ImageParams.java new file mode 100644 index 0000000..aa785ce --- /dev/null +++ b/src/test/resources/fsm/errors/image/ImageParams.java @@ -0,0 +1,40 @@ +package fsm.errors.image; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"startTiling", "tilingExplicit", "tilingSet"}) +@StateSet({"startCompression", "compressionExplicit", "compressionSet"}) +public class ImageParams { + + // sets the state of both state sets + @StateRefinement(to="startTiling(this) && startCompression(this)") + public ImageParams() {} + + // only sets the tiling state, the compression state starts in the first state + @StateRefinement(to="tilingExplicit(this)") + public ImageParams(int mode) {} + + @StateRefinement(to="mode == 2 ? tilingExplicit(this) : startTiling(this)") + public void setTilingMode(int mode) {} + + @StateRefinement(from="tilingExplicit(this)", to="tilingSet(this)") + public void setTiling(int width) {} + + @StateRefinement(to="mode == 2 ? compressionExplicit(this) : startCompression(this)") + public void setCompressionMode(int mode) {} + + @StateRefinement(from="compressionExplicit(this)", to="compressionSet(this)") + public void setCompressionType(String type) {} + + // requires a state of each state set + @StateRefinement(from="tilingSet(this) && compressionSet(this)") + public void write() {} + + // requires a compression state and changes the tiling state + @StateRefinement(from="compressionSet(this)", to="startTiling(this)") + public void resetTiling() {} + + // does not refer to any state + public void setProgressiveMode(int mode) {} +} diff --git a/src/test/resources/fsm/errors/image/ImageParamsClient.java b/src/test/resources/fsm/errors/image/ImageParamsClient.java new file mode 100644 index 0000000..02967b1 --- /dev/null +++ b/src/test/resources/fsm/errors/image/ImageParamsClient.java @@ -0,0 +1,17 @@ +package fsm.errors.image; + +public class ImageParamsClient { + + public static void typeWithoutExplicitMode() { + ImageParams params = new ImageParams(); + params.setTilingMode(2); + params.setCompressionType("JPEG"); // state error: found startCompression, expected compressionExplicit + } + + public static void writeWithoutTiling() { + ImageParams params = new ImageParams(2); + params.setCompressionMode(2); + params.setCompressionType("JPEG"); + params.write(); // state error: found tilingExplicit, expected tilingSet and compressionSet + } +}