From c9271959dfdb50b96e75f20e17e5b4c2fa46b086 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 23:24:34 +0000 Subject: [PATCH 1/2] Read named state sets and states written as values of their sets The verifier now accepts @StateSet(name = "phase", value = {...}) and a state written as a value of its set, phase(this) == open, which it reads as open(this), and phase(this) != open as !open(this). The parser took such a from for a condition on every state, so the diagram lost its transitions. A comparison of a one-argument function with a state, in either order, is now that state, and != negates it, wherever the shorthand is read: from, to, constructors and factories. Conditions keep the form the spec wrote. Each state machine carries stateSetName, the name given to its state set, or null when it has none, so a client can label the diagram with the name the verifier's messages use. Co-Authored-By: Claude Opus 5.5 --- README.md | 4 + .../java/liquidjava/fsm/StateMachine.java | 7 ++ .../liquidjava/fsm/StateMachineParser.java | 105 ++++++++++++------ .../fsm/StateMachineParserTests.java | 18 +++ src/test/resources/fsm/StateValues.java | 23 ++++ 5 files changed, 124 insertions(+), 33 deletions(-) create mode 100644 src/test/resources/fsm/StateValues.java diff --git a/README.md b/README.md index 3e97b2f..36702aa 100644 --- a/README.md +++ b/README.md @@ -53,6 +53,9 @@ A class with several `@StateSet` annotations has one state machine per state set 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. +`stateSetName` is the name given to the state set, `@StateSet(name = "phase", value = {...})`, or null if it has none. +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 @@ -86,6 +89,7 @@ boolean canUndo(); { "className": "example.File", "stateSet": 0, + "stateSetName": null, "states": [ "open", "closed" diff --git a/src/main/java/liquidjava/fsm/StateMachine.java b/src/main/java/liquidjava/fsm/StateMachine.java index 1d25cbb..80ce020 100644 --- a/src/main/java/liquidjava/fsm/StateMachine.java +++ b/src/main/java/liquidjava/fsm/StateMachine.java @@ -6,15 +6,22 @@ * 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 + * @param stateSetName the name given to the state set, or null if it has none */ public record StateMachine( String className, int stateSet, + String stateSetName, List states, List transitions, List initialTransitions, List entryTransitions ) { + public StateMachine(String className, int stateSet, List states, List transitions, + List initialTransitions, List entryTransitions) { + this(className, stateSet, null, states, transitions, initialTransitions, entryTransitions); + } + public StateMachine(String className, int stateSet, List states, List transitions, List initialTransitions) { this(className, stateSet, states, transitions, initialTransitions, List.of()); diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 06c333b..eb75815 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -19,6 +19,7 @@ import liquidjava.utils.Utils; import spoon.Launcher; import spoon.reflect.CtModel; +import spoon.reflect.code.CtLiteral; import spoon.reflect.declaration.CtAnnotation; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtExecutable; @@ -35,6 +36,9 @@ public class StateMachineParser { private record TransitionSource(String from, String cond) {} + // name is null when the state set has none + private record StateSet(String name, List states) {} + /** * Parses a class or interface for the given uri and extracts the state machine information * @param uri the document URI @@ -96,7 +100,7 @@ public static List parseAll(List uris, String className) { // extract class name, state sets and methods, with those inherited from the specs of the supertypes List> supertypes = getSupertypes(model, ctType); List> specs = getSpecs(model, ctType, supertypes); - List> stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList(); + List stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList(); List> methods = getMethods(specs, supertypes); String qualifiedName = getClassName(ctType); List stateMachines = new ArrayList<>(); @@ -104,7 +108,7 @@ public static List parseAll(List uris, String className) { List otherStates = new ArrayList<>(); for (int j = 0; j < stateSets.size(); j++) { if (j != i) - otherStates.addAll(stateSets.get(j)); + otherStates.addAll(stateSets.get(j).states()); } StateMachine sm = parseStateSet(ctType, methods, qualifiedName, i, stateSets.get(i), otherStates); if (sm != null) @@ -138,12 +142,13 @@ private static CtModel buildModel(List uris) throws URISyntaxException { * @param methods the methods of the class, with those it inherits * @param qualifiedName the class name * @param stateSet the index of the state set - * @param states the states of the state set + * @param set 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, List> methods, String qualifiedName, - int stateSet, List states, List otherStates) { + int stateSet, StateSet set, List otherStates) { + List states = set.states(); if (states.isEmpty()) return null; // no states found String simpleClassName = Utils.getSimpleName(qualifiedName); @@ -162,7 +167,8 @@ private static StateMachine parseStateSet(CtType ctType, List> me if (transitions.isEmpty() && entryTransitions.isEmpty()) return null; // no transitions found - return new StateMachine(qualifiedName, stateSet, states, transitions, initialTransitions, entryTransitions); + return new StateMachine(qualifiedName, stateSet, set.name(), states, transitions, initialTransitions, + entryTransitions); } /** @@ -358,17 +364,23 @@ private static String getClassName(CtType ctType) { * @param ctType the CtType (class or interface) * @return list of state sets, in declaration order */ - private static List> getStateSets(CtType ctType) { - List> stateSets = new ArrayList<>(); + 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"); - stateSets.add(List.of(stateArray)); + stateSets.add(new StateSet(getStateSetName(annotation), List.of(stateArray))); } } return stateSets; } + // an empty name is no name, as in the verifier + private static String getStateSetName(CtAnnotation annotation) { + return annotation.getValues().get("name") instanceof CtLiteral literal + && literal.getValue() instanceof String name && !name.isEmpty() ? name : null; + } + /** * Gets the elements that represent constructors (actual constructors for classes, methods named after the class for interfaces) * @param ctType the CtType (class or interface) @@ -600,6 +612,20 @@ private static List getTransitionSources(Expression expr, List return List.of(new TransitionSource(state, null)); } + Expression negated = getNegated(expr); + if (negated != null) { + List negatedStates = getStateExpressions(negated, states); + if (!negatedStates.isEmpty()) { + List sources = new ArrayList<>(); + for (String possibleState : states) { + if (!negatedStates.contains(possibleState)) { + sources.add(new TransitionSource(possibleState, null)); + } + } + return sources; + } + } + if (expr instanceof BinaryExpression bin) { String op = bin.getOperator(); if (op.equals("&&")) { @@ -607,19 +633,6 @@ private static List getTransitionSources(Expression expr, List } else if (op.equals("||")) { return stateOnlyDisjunctions ? getStateSources(bin, states) : getDisjunctionSources(bin, states); } - } else if (expr instanceof UnaryExpression unary) { - if (unary.getOp().equals("!")) { - List negatedStates = getStateExpressions(unary.getExpression(), states); - if (!negatedStates.isEmpty()) { - List sources = new ArrayList<>(); - for (String possibleState : states) { - if (!negatedStates.contains(possibleState)) { - sources.add(new TransitionSource(possibleState, null)); - } - } - return sources; - } - } } else if (expr instanceof Ite ite) { List sources = new ArrayList<>(); sources.addAll(addCondition(getTransitionSources(ite.getThen(), states, stateOnlyDisjunctions), ite.getCondition().toString())); @@ -740,23 +753,22 @@ private static List getStateSources(Expression expr, List getStateExpressions(Expression expr, List states) { List stateExpressions = new ArrayList<>(); String state = getStateName(expr, states); + Expression negated = getNegated(expr); if (state != null) { stateExpressions.add(state); - } else if (expr instanceof BinaryExpression bin) { - stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states)); - stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states)); - } else if (expr instanceof UnaryExpression unary) { - if (unary.getOp().equals("!")) { - // all except those in the expression - List negatedStates = getStateExpressions(unary.getExpression(), states); - if (!negatedStates.isEmpty()) { - for (String possibleState : states) { - if (!negatedStates.contains(possibleState)) { - stateExpressions.add(possibleState); - } + } else if (negated != null) { + // all except those in the expression + List negatedStates = getStateExpressions(negated, states); + if (!negatedStates.isEmpty()) { + for (String possibleState : states) { + if (!negatedStates.contains(possibleState)) { + stateExpressions.add(possibleState); } } } + } else if (expr instanceof BinaryExpression bin) { + stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states)); + stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states)); } else if (expr instanceof Ite ite) { // combine states from then and else branches stateExpressions.addAll(getStateExpressions(ite.getThen(), states)); @@ -765,11 +777,38 @@ private static List getStateExpressions(Expression expr, List st return stateExpressions; } + /** + * Gets the state an expression is in: open(this), or open written as a value of its state set, as in + * phase(this) == open or open == phase(this), which the verifier reads as open(this) + */ private static String getStateName(Expression expr, List states) { if (expr instanceof Var var) { return findState(var.getName(), states); } else if (expr instanceof FunctionInvocation func) { return findState(func.getName(), states); + } else if (expr instanceof BinaryExpression bin && bin.getOperator().equals("==")) { + String state = getStateValue(bin.getFirstOperand(), bin.getSecondOperand(), states); + return state != null ? state : getStateValue(bin.getSecondOperand(), bin.getFirstOperand(), states); + } + return null; + } + + private static String getStateValue(Expression stateSet, Expression value, List states) { + return stateSet instanceof FunctionInvocation func && func.getArgs().size() == 1 && value instanceof Var var + ? findState(var.getName(), states) + : null; + } + + /** + * Gets what a negation negates: e in !e, or a == b in a != b, so that phase(this) != open is read as !open(this) + * as in the verifier + * @return the negated expression, or null if expr is not a negation + */ + private static Expression getNegated(Expression expr) { + if (expr instanceof UnaryExpression unary && unary.getOp().equals("!")) { + return unary.getExpression(); + } else if (expr instanceof BinaryExpression bin && bin.getOperator().equals("!=")) { + return new BinaryExpression(bin.getFirstOperand(), "==", bin.getSecondOperand()); } return null; } diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index 3876961..b9721a4 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -8,6 +8,7 @@ import java.nio.file.Path; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; import org.junit.jupiter.api.Test; @@ -342,6 +343,23 @@ public void testStateMachinePerStateSet() { assertEquals(List.of(), StateMachineParser.parseAll(uri("TwoStateClasses.java"), "fsm.Missing")); } + @Test + public void testStatesWrittenAsValuesOfTheirStateSets() { + List sms = StateMachineParser.parseAll(uri("StateValues.java")); + assertEquals(Arrays.asList("phase", null), sms.stream().map(StateMachine::stateSetName).toList()); + assertStateMachineEquals(stateMachine("StateValues", 0, List.of("open", "closed", "broken"), + List.of(new StateMachineTransition("open", "broken", "breakDown", "state2(this) == unlocked", null), + new StateMachineTransition("closed", "broken", "breakDown", "state2(this) == unlocked", null), + new StateMachineTransition("open", "closed", "close"), + new StateMachineTransition("closed", "open", "openLocked")), + List.of(new StateMachineInitialTransition("open"))), sms.get(0)); + assertStateMachineEquals(stateMachine("StateValues", 1, List.of("unlocked", "locked"), + List.of(new StateMachineTransition("unlocked", "unlocked", "breakDown", "phase(this) != broken", null), + new StateMachineTransition("unlocked", "locked", "openLocked", "phase(this) == closed", null), + new StateMachineTransition("locked", "locked", "openLocked", "phase(this) == closed", null)), + List.of(new StateMachineInitialTransition("unlocked"))), sms.get(1)); + } + private static final StateMachine FRAME = new StateMachine("java.awt.Frame", 0, List.of("displayable", "notDisplayable"), List.of(new StateMachineTransition("notDisplayable", "notDisplayable", "setUndecorated"), diff --git a/src/test/resources/fsm/StateValues.java b/src/test/resources/fsm/StateValues.java new file mode 100644 index 0000000..fa5f7df --- /dev/null +++ b/src/test/resources/fsm/StateValues.java @@ -0,0 +1,23 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// states written as values of their state sets, in either order, with == and !=, mixed with the shorthand +@StateSet(name = "phase", value = {"open", "closed", "broken"}) +@StateSet({"unlocked", "locked"}) +public class StateValues { + + @StateRefinement(to = "phase(this) == open && unlocked(this)") + public StateValues() {} + + @StateRefinement(from = "open == this.phase()", to = "closed(this)") + public void close() {} + + // the unnamed state set is named state2 + @StateRefinement(from = "phase() != broken && state2(this) == unlocked", to = "phase(this) == broken") + public void breakDown() {} + + @StateRefinement(from = "phase(this) == closed", to = "phase(this) == open && state2(this) == locked") + public void openLocked() {} +} From b5a1061172a55b67328481388c6dd730b488952c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 23:31:59 +0000 Subject: [PATCH 2/2] Negate only a state compared with != as a value of its set open(this) != false is not phase(this) != open: it means open(this), so its complement drew the transition from the other states. Only a comparison that is itself a state value is read as its negation. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/fsm/StateMachineParser.java | 45 +++++++++---------- 1 file changed, 20 insertions(+), 25 deletions(-) diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index eb75815..21691df 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -612,18 +612,15 @@ private static List getTransitionSources(Expression expr, List return List.of(new TransitionSource(state, null)); } - Expression negated = getNegated(expr); - if (negated != null) { - List negatedStates = getStateExpressions(negated, states); - if (!negatedStates.isEmpty()) { - List sources = new ArrayList<>(); - for (String possibleState : states) { - if (!negatedStates.contains(possibleState)) { - sources.add(new TransitionSource(possibleState, null)); - } + List negatedStates = getNegatedStates(expr, states); + if (!negatedStates.isEmpty()) { + List sources = new ArrayList<>(); + for (String possibleState : states) { + if (!negatedStates.contains(possibleState)) { + sources.add(new TransitionSource(possibleState, null)); } - return sources; } + return sources; } if (expr instanceof BinaryExpression bin) { @@ -753,17 +750,14 @@ private static List getStateSources(Expression expr, List getStateExpressions(Expression expr, List states) { List stateExpressions = new ArrayList<>(); String state = getStateName(expr, states); - Expression negated = getNegated(expr); + List negatedStates = getNegatedStates(expr, states); if (state != null) { stateExpressions.add(state); - } else if (negated != null) { + } else if (!negatedStates.isEmpty()) { // all except those in the expression - List negatedStates = getStateExpressions(negated, states); - if (!negatedStates.isEmpty()) { - for (String possibleState : states) { - if (!negatedStates.contains(possibleState)) { - stateExpressions.add(possibleState); - } + for (String possibleState : states) { + if (!negatedStates.contains(possibleState)) { + stateExpressions.add(possibleState); } } } else if (expr instanceof BinaryExpression bin) { @@ -800,17 +794,18 @@ private static String getStateValue(Expression stateSet, Expression value, List< } /** - * Gets what a negation negates: e in !e, or a == b in a != b, so that phase(this) != open is read as !open(this) - * as in the verifier - * @return the negated expression, or null if expr is not a negation + * Gets the states a negation excludes: those in e for !e, or open for phase(this) != open, which the verifier + * reads as !open(this) + * @return the excluded states, or none if expr is not the negation of a state */ - private static Expression getNegated(Expression expr) { + private static List getNegatedStates(Expression expr, List states) { if (expr instanceof UnaryExpression unary && unary.getOp().equals("!")) { - return unary.getExpression(); + return getStateExpressions(unary.getExpression(), states); } else if (expr instanceof BinaryExpression bin && bin.getOperator().equals("!=")) { - return new BinaryExpression(bin.getFirstOperand(), "==", bin.getSecondOperand()); + String state = getStateName(new BinaryExpression(bin.getFirstOperand(), "==", bin.getSecondOperand()), states); + return state == null ? List.of() : List.of(state); } - return null; + return List.of(); } private static String findState(String name, List states) {