From 7f6f718ab06265f49d0ffd234d06583633341f3e Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 21:39:28 +0000 Subject: [PATCH] Parse one state machine per state set A class with several @StateSet annotations, such as ImageWriteParam with its tiling and compression states, was drawn with the first state set only, and the other state set's predicates showed up as conditions on its arrows. parseAll returns one StateMachine per state set, in declaration order, with the index of the state set in stateSet. That is the order the verifier uses in StateErrorContext. Each state machine only keeps the transitions that mention its states. States of other state sets stay as conditions in a from, and are left out of a to, since they change at the same time. parse keeps returning the first state machine. Co-Authored-By: Claude Opus 5.5 --- README.md | 9 + .../java/liquidjava/fsm/StateMachine.java | 12 +- .../liquidjava/fsm/StateMachineParser.java | 172 +++++++++++++----- .../fsm/StateMachineParserTests.java | 62 ++++++- src/test/resources/fsm/TwoStateSets.java | 40 ++++ .../fsm/errors/image/ImageParams.java | 40 ++++ .../fsm/errors/image/ImageParamsClient.java | 17 ++ 7 files changed, 301 insertions(+), 51 deletions(-) create mode 100644 src/test/resources/fsm/TwoStateSets.java create mode 100644 src/test/resources/fsm/errors/image/ImageParams.java create mode 100644 src/test/resources/fsm/errors/image/ImageParamsClient.java 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 + } +}