Skip to content

Parse one state machine per state set #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 1 commit into from
Oct 26, 2026
Merged

Parse one state machine per state set #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<StateMachine> 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"
Expand Down
12 changes: 10 additions & 2 deletions src/main/java/liquidjava/fsm/StateMachine.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<String> states,
List<StateMachineTransition> transitions,
List<StateMachineInitialTransition> initialTransitions
) {}
) {
public StateMachine(String className, List<String> states, List<StateMachineTransition> transitions,
List<StateMachineInitialTransition> initialTransitions) {
this(className, 0, states, transitions, initialTransitions);
}
}
172 changes: 131 additions & 41 deletions src/main/java/liquidjava/fsm/StateMachineParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<StateMachine> 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<StateMachine> 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<StateMachine> parseAll(String uri, String className) {
try {
String filePath = Paths.get(new URI(uri)).toString();
Launcher launcher = new Launcher();
Expand All @@ -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<String> states = getStates(ctType);
if (states == null || states.isEmpty())
return null; // no states found
// extract class name and state sets
List<List<String>> stateSets = getStateSets(ctType);
String qualifiedName = getClassName(ctType);
String simpleClassName = Utils.getSimpleName(qualifiedName);

// get initial transitions and method transitions
List<StateMachineInitialTransition> factoryTransitions = getFactoryTransitions(ctType, simpleClassName, states);
List<StateMachineInitialTransition> 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<StateMachine> stateMachines = new ArrayList<>();
for (int i = 0; i < stateSets.size(); i++) {
List<String> 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<StateMachineTransition> 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<String> states, List<String> otherStates) {
if (states.isEmpty())
return null; // no states found
String simpleClassName = Utils.getSimpleName(qualifiedName);

// get initial transitions and method transitions
List<StateMachineInitialTransition> factoryTransitions = getFactoryTransitions(ctType, simpleClassName, states, otherStates);
List<StateMachineInitialTransition> 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<StateMachineTransition> 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
Expand Down Expand Up @@ -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<String> getStates(CtType<?> ctType) {
private static List<List<String>> getStateSets(CtType<?> ctType) {
List<List<String>> 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;
}

/**
Expand All @@ -149,17 +196,19 @@ private static Collection<? extends CtExecutable<?>> 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<StateMachineInitialTransition> getInitialTransitions(CtType<?> ctType, String className, List<String> states) {
private static List<StateMachineInitialTransition> getInitialTransitions(CtType<?> ctType, String className,
List<String> states, List<String> otherStates) {
List<StateMachineInitialTransition> initialTransitions = new ArrayList<>();
for (CtExecutable<?> element : getConstructorElements(ctType, className)) {
String signature = getConstructorSignature(element, className);
boolean hasExplicitInitialState = false;
for (CtAnnotation<?> annotation : element.getAnnotations()) {
if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) {
String to = annotation.getValueAsString("to");
List<StateMachineInitialTransition> transitions = parseInitialTransitions(to, states, signature);
List<StateMachineInitialTransition> transitions = parseInitialTransitions(to, states, otherStates, signature);
initialTransitions.addAll(transitions);
hasExplicitInitialState |= !transitions.isEmpty();
}
Expand Down Expand Up @@ -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<StateMachineInitialTransition> getFactoryTransitions(CtType<?> ctType, String className, List<String> states) {
private static List<StateMachineInitialTransition> getFactoryTransitions(CtType<?> ctType, String className,
List<String> states, List<String> otherStates) {
List<StateMachineInitialTransition> initialTransitions = new ArrayList<>();
for (CtMethod<?> method : ctType.getMethods()) {
if (ctType.isClass() && !method.isStatic())
Expand All @@ -207,7 +258,7 @@ private static List<StateMachineInitialTransition> 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));
}
}
}
Expand All @@ -225,17 +276,19 @@ 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<StateMachineTransition> getTransitions(CtType<?> ctType, String className, List<String> states) {
private static List<StateMachineTransition> getTransitions(CtType<?> ctType, String className, List<String> states,
List<String> otherStates) {
List<StateMachineTransition> 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;
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));
}
}
}
Expand All @@ -247,18 +300,25 @@ private static List<StateMachineTransition> 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<StateMachineTransition> getTransitions(CtAnnotation<?> ann, String method, List<String> states) {
private static List<StateMachineTransition> getTransitions(CtAnnotation<?> ann, String method, List<String> states,
List<String> otherStates) {
List<StateMachineTransition> 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<TransitionSource> fromSources = from.isEmpty() ? allStateSources(states) : parsePrecondition(from, states);
List<TransitionSource> toSources = !from.isEmpty() && to.isEmpty()
List<TransitionSource> 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) {
Expand Down Expand Up @@ -286,12 +346,42 @@ private static List<TransitionSource> parsePrecondition(String expr, List<String
return sources;
}

private static List<TransitionSource> parsePostcondition(String expr, List<String> states) {
private static List<TransitionSource> parsePostcondition(String expr, List<String> states, List<String> 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<String> 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<String> states) {
if (expr == null || expr.isEmpty()) return false;
return !getStateExpressions(RefinementsParser.createAST(expr, ""), states).isEmpty();
}

private static List<TransitionSource> getTransitionSources(Expression expr, List<String> states, boolean stateOnlyDisjunctions) {
String state = getStateName(expr, states);
if (state != null) {
Expand Down Expand Up @@ -406,10 +496,10 @@ private static String negateCondition(Expression expr) {
}

private static List<StateMachineInitialTransition> parseInitialTransitions(String expr, List<String> states,
String constructorSignature) {
List<String> otherStates, String constructorSignature) {
if (expr == null || expr.isEmpty()) return new ArrayList<>();
List<StateMachineInitialTransition> 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;
Expand Down
Loading
Loading