From 404f66c2477fe59448ce0ef8f40d02afbaac7989 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 17:08:19 +0100 Subject: [PATCH 1/6] Handle Complex State Transitions in DFA --- client/src/types/fsm.ts | 2 +- client/src/webview/diagram.ts | 14 +- client/src/webview/styles.ts | 4 + .../src/main/java/fsm/StateMachineParser.java | 191 ++++++++++++++++-- .../main/java/fsm/StateMachineTransition.java | 7 +- .../java/fsm/StateMachineParserTests.java | 39 ++++ .../fsm/ConditionalPrecondition.java | 14 ++ .../fsm/ConjunctionPrecondition.java | 14 ++ .../fsm/DisjunctionPrecondition.java | 14 ++ .../resources/fsm/PostConditionFiltering.java | 14 ++ 10 files changed, 288 insertions(+), 25 deletions(-) create mode 100644 server/src/test/resources/fsm/ConditionalPrecondition.java create mode 100644 server/src/test/resources/fsm/ConjunctionPrecondition.java create mode 100644 server/src/test/resources/fsm/DisjunctionPrecondition.java create mode 100644 server/src/test/resources/fsm/PostConditionFiltering.java diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index e8f1a96..3c42c22 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -4,5 +4,5 @@ export type LJStateMachine = { className: string; initialStates: string[]; states: string[]; - transitions: { from: string; to: string; label: string }[]; + transitions: { from: string; to: string; label: string; cond?: string | null }[]; }; diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index a3574cd..47a57cd 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -41,9 +41,10 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation // group transitions by from/to states and merge labels const transitionMap = new Map(); sm.transitions.forEach(transition => { + const label = getTransitionLabel(transition.label, transition.cond); const key = `${transition.from}|${transition.to}`; if (!transitionMap.has(key)) transitionMap.set(key, []); - transitionMap.get(key)?.push(transition.label); + transitionMap.get(key)?.push(label); }); // add transitions @@ -56,6 +57,17 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation return lines.join('\n'); } +function getTransitionLabel(label: string, cond?: string | null): string { + if (!cond) { + return escapeMermaidLabel(label); + } + return `${escapeMermaidLabel(label)} (${escapeMermaidLabel(cond)})`; +} + +function escapeMermaidLabel(label: string): string { + return label.replace(/&/g, '&').replace(/"/g, '\\"').replace(//g, '>'); +} + /** * Renders Mermaid diagrams in the document * @param document The document object diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 92b8139..1bb1a69 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -650,6 +650,10 @@ export function getStyles(): string { color: var(--vscode-foreground) !important; background: var(--vscode-editor-background) !important; } + .diagram-container .mermaid .edgeLabel .state-cond { + color: var(--vscode-descriptionForeground) !important; + font-size: 0.85em !important; + } .diagram-container .mermaid svg rect, .diagram-container .mermaid svg circle, .diagram-container .mermaid svg ellipse, diff --git a/server/src/main/java/fsm/StateMachineParser.java b/server/src/main/java/fsm/StateMachineParser.java index 628a0e5..ac02985 100644 --- a/server/src/main/java/fsm/StateMachineParser.java +++ b/server/src/main/java/fsm/StateMachineParser.java @@ -24,6 +24,8 @@ public class StateMachineParser { private static final String STATE_REFINEMENT_ANNOTATION = "StateRefinement"; private static final String EXTERNAL_REFINEMENTS_FOR_ANNOTATION = "ExternalRefinementsFor"; + private record TransitionSource(String from, String cond) {} + /** * Parses a class or interface for the given uri and extracts the state machine information * @param uri the document URI @@ -186,23 +188,150 @@ private static List getTransitions(CtAnnotation ann, } // parse from and to expressions - List fromStates = parseStateExpression(from, states); + List fromSources = from.isEmpty() ? allStateSources(states) : parsePrecondition(from, states); List toStates = parseStateExpression(to, states); - // if no from states, use all states - if (fromStates.isEmpty()) { - fromStates = new ArrayList<>(states); - } - // create transitions for each combination of from and to states - for (String fromState : fromStates) { + for (TransitionSource fromSource : fromSources) { for (String toState : toStates) { - transitions.add(new StateMachineTransition(fromState, toState, method)); + transitions.add(new StateMachineTransition(fromSource.from(), toState, method, fromSource.cond())); } } return transitions; } + private static List allStateSources(List states) { + List sources = new ArrayList<>(); + for (String state : states) { + sources.add(new TransitionSource(state, null)); + } + return sources; + } + + private static List parsePrecondition(String expr, List states) { + Expression ast = RefinementsParser.createAST(expr, ""); + List sources = getPreconditionSources(ast, states); + if (sources.isEmpty()) { + sources = addCondition(allStateSources(states), ast.toString()); + } + return sources; + } + + private static List getPreconditionSources(Expression expr, List states) { + String state = getStateName(expr, states); + if (state != null) { + return List.of(new TransitionSource(state, null)); + } + + if (expr instanceof GroupExpression group) { + return getPreconditionSources(group.getExpression(), states); + } else if (expr instanceof BinaryExpression bin) { + String op = bin.getOperator(); + if (op.equals("&&")) { + return getConjunctionSources(bin, states); + } else if (op.equals("||")) { + return 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(getPreconditionSources(ite.getThen(), states), ite.getCondition().toString())); + sources.addAll(addCondition(getPreconditionSources(ite.getElse(), states), negateCondition(ite.getCondition()))); + return sources; + } + return new ArrayList<>(); + } + + private static List getConjunctionSources(BinaryExpression bin, List states) { + List leftSources = getPreconditionSources(bin.getFirstOperand(), states); + List rightSources = getPreconditionSources(bin.getSecondOperand(), states); + + if (leftSources.isEmpty() && rightSources.isEmpty()) { + return new ArrayList<>(); + } else if (leftSources.isEmpty()) { + return addCondition(rightSources, bin.getFirstOperand().toString()); + } else if (rightSources.isEmpty()) { + return addCondition(leftSources, bin.getSecondOperand().toString()); + } + + List sources = new ArrayList<>(leftSources); + sources.addAll(rightSources); + return sources; + } + + private static List getDisjunctionSources(BinaryExpression bin, List states) { + List sources = new ArrayList<>(); + addDisjunctionBranch(sources, bin.getFirstOperand(), states); + addDisjunctionBranch(sources, bin.getSecondOperand(), states); + return removeRedundantGuardedSources(sources); + } + + private static void addDisjunctionBranch(List sources, Expression expr, List states) { + List parsedSources = getPreconditionSources(expr, states); + if (parsedSources.isEmpty()) { + sources.addAll(addCondition(allStateSources(states), expr.toString())); + } else { + sources.addAll(parsedSources); + } + } + + private static List removeRedundantGuardedSources(List sources) { + List filteredSources = new ArrayList<>(); + for (TransitionSource source : sources) { + if (source.cond() == null || !hasUnguardedSource(sources, source.from())) { + filteredSources.add(source); + } + } + return filteredSources; + } + + private static boolean hasUnguardedSource(List sources, String from) { + for (TransitionSource source : sources) { + if (source.from().equals(from) && source.cond() == null) { + return true; + } + } + return false; + } + + private static List addCondition(List sources, String cond) { + List guardedSources = new ArrayList<>(); + for (TransitionSource source : sources) { + guardedSources.add(new TransitionSource(source.from(), combineConditions(source.cond(), cond))); + } + return guardedSources; + } + + private static String combineConditions(String first, String second) { + if (first == null || first.isEmpty()) { + return second; + } + if (second == null || second.isEmpty()) { + return first; + } + return first + " && " + second; + } + + private static String negateCondition(Expression expr) { + String condition = expr.toString(); + if (expr instanceof Var || expr instanceof FunctionInvocation) { + return "!" + condition; + } + return "!(" + condition + ")"; + } + /** * Parses a state expression and returns the list of states * @param expr the expression @@ -223,35 +352,53 @@ private static List parseStateExpression(String expr, List state */ private static List getStateExpressions(Expression expr, List states) { List stateExpressions = new ArrayList<>(); - if (expr instanceof Var var) { - stateExpressions.add(var.getName()); - } else if (expr instanceof FunctionInvocation func) { - stateExpressions.add(func.getName()); + String state = getStateName(expr, states); + if (state != null) { + stateExpressions.add(state); } else if (expr instanceof GroupExpression group) { stateExpressions.addAll(getStateExpressions(group.getExpression(), states)); } else if (expr instanceof BinaryExpression bin) { - String op = bin.getOperator(); - if (op.equals("||")) { - // combine states from both operands - stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states)); - stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states)); - } + 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); - for (String state : states) { - if (!negatedStates.contains(state)) { - stateExpressions.add(state); + if (!negatedStates.isEmpty()) { + for (String possibleState : states) { + if (!negatedStates.contains(possibleState)) { + stateExpressions.add(possibleState); + } } } } } else if (expr instanceof Ite ite) { // combine states from then and else branches - // TODO: handle conditional transitions stateExpressions.addAll(getStateExpressions(ite.getThen(), states)); stateExpressions.addAll(getStateExpressions(ite.getElse(), states)); } return stateExpressions; } + + 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); + } + return null; + } + + private static String findState(String name, List states) { + if (states.contains(name)) { + return name; + } + String simpleName = Utils.getSimpleName(name); + for (String state : states) { + if (state.equals(simpleName) || Utils.getSimpleName(state).equals(simpleName)) { + return state; + } + } + return null; + } } diff --git a/server/src/main/java/fsm/StateMachineTransition.java b/server/src/main/java/fsm/StateMachineTransition.java index f95ad8a..49cec71 100644 --- a/server/src/main/java/fsm/StateMachineTransition.java +++ b/server/src/main/java/fsm/StateMachineTransition.java @@ -3,4 +3,9 @@ /** * Represents a transition in a state machine */ -public record StateMachineTransition(String from, String to, String label) {} \ No newline at end of file +public record StateMachineTransition(String from, String to, String label, String cond) { + + public StateMachineTransition(String from, String to, String label) { + this(from, to, label, null); + } +} diff --git a/server/src/test/java/fsm/StateMachineParserTests.java b/server/src/test/java/fsm/StateMachineParserTests.java index daad9c4..8eb8653 100644 --- a/server/src/test/java/fsm/StateMachineParserTests.java +++ b/server/src/test/java/fsm/StateMachineParserTests.java @@ -91,6 +91,45 @@ public void testConditionalTransition() { assertStateMachineEquals(expectedSm, sm); } + @Test + public void testConjunctionPrecondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "ConjunctionPrecondition.java"); + StateMachine expectedSm = new StateMachine("ConjunctionPrecondition", List.of("open"), + List.of("open", "closed"), + List.of(new StateMachineTransition("open", "closed", "close", "flag"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testDisjunctionPrecondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "DisjunctionPrecondition.java"); + StateMachine expectedSm = new StateMachine("DisjunctionPrecondition", List.of("ready"), + List.of("ready", "waiting", "done"), + List.of(new StateMachineTransition("waiting", "done", "action", "flag"), + new StateMachineTransition("done", "done", "action", "flag"), + new StateMachineTransition("ready", "done", "action"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testConditionalPrecondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "ConditionalPrecondition.java"); + StateMachine expectedSm = new StateMachine("ConditionalPrecondition", List.of("left"), + List.of("left", "right", "done"), + List.of(new StateMachineTransition("left", "done", "finish", "flag"), + new StateMachineTransition("right", "done", "finish", "!flag"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testPostConditionFiltering() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "PostConditionFiltering.java"); + StateMachine expectedSm = new StateMachine("PostConditionFiltering", List.of("ready"), + List.of("ready", "done"), + List.of(new StateMachineTransition("ready", "done", "finish"))); + assertStateMachineEquals(expectedSm, sm); + } + 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"); diff --git a/server/src/test/resources/fsm/ConditionalPrecondition.java b/server/src/test/resources/fsm/ConditionalPrecondition.java new file mode 100644 index 0000000..9d86921 --- /dev/null +++ b/server/src/test/resources/fsm/ConditionalPrecondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"left", "right", "done"}) +public class ConditionalPrecondition { + + @StateRefinement(to="left(this)") + public ConditionalPrecondition() {} + + @StateRefinement(from="flag ? left(this) : right(this)", to="done(this)") + public void finish(boolean flag) {} +} diff --git a/server/src/test/resources/fsm/ConjunctionPrecondition.java b/server/src/test/resources/fsm/ConjunctionPrecondition.java new file mode 100644 index 0000000..549733c --- /dev/null +++ b/server/src/test/resources/fsm/ConjunctionPrecondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class ConjunctionPrecondition { + + @StateRefinement(to="open(this)") + public ConjunctionPrecondition() {} + + @StateRefinement(from="flag && open(this)", to="closed(this)") + public void close(boolean flag) {} +} diff --git a/server/src/test/resources/fsm/DisjunctionPrecondition.java b/server/src/test/resources/fsm/DisjunctionPrecondition.java new file mode 100644 index 0000000..c2eb62b --- /dev/null +++ b/server/src/test/resources/fsm/DisjunctionPrecondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "waiting", "done"}) +public class DisjunctionPrecondition { + + @StateRefinement(to="ready(this)") + public DisjunctionPrecondition() {} + + @StateRefinement(from="flag || ready(this)", to="done(this)") + public void action(boolean flag) {} +} diff --git a/server/src/test/resources/fsm/PostConditionFiltering.java b/server/src/test/resources/fsm/PostConditionFiltering.java new file mode 100644 index 0000000..4df211c --- /dev/null +++ b/server/src/test/resources/fsm/PostConditionFiltering.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "done"}) +public class PostConditionFiltering { + + @StateRefinement(to="ready(this)") + public PostConditionFiltering() {} + + @StateRefinement(from="ready(this)", to="flag && done(this)") + public void finish(boolean flag) {} +} From 4439cd269026ff2ff6f9b1ca91a707fe911647b1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 17:36:10 +0100 Subject: [PATCH 2/6] Handle Initial State Conditions --- client/src/types/fsm.ts | 2 +- client/src/webview/diagram.ts | 14 +++- client/src/webview/views/fsm/fsm.ts | 6 +- server/src/main/java/fsm/StateMachine.java | 4 +- .../fsm/StateMachineInitialTransition.java | 11 +++ .../src/main/java/fsm/StateMachineParser.java | 64 +++++++++------ .../java/fsm/StateMachineParserTests.java | 81 +++++++++++-------- .../fsm/ConjunctionInitialTransition.java | 14 ++++ 8 files changed, 133 insertions(+), 63 deletions(-) create mode 100644 server/src/main/java/fsm/StateMachineInitialTransition.java create mode 100644 server/src/test/resources/fsm/ConjunctionInitialTransition.java diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 3c42c22..244e664 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -2,7 +2,7 @@ export type LJStateMachine = { className: string; - initialStates: string[]; + initialTransitions: { to: string; cond?: string | null }[]; states: string[]; transitions: { from: string; to: string; label: string; cond?: string | null }[]; }; diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 47a57cd..6981062 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -33,9 +33,10 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation lines.push('stateDiagram-v2'); lines.push(` direction ${orientation}`); - // initial states - sm.initialStates.forEach(state => { - lines.push(` [*] --> ${state}`); + // initial transitions + sm.initialTransitions.forEach(transition => { + const label = getInitialTransitionLabel(transition.cond); + lines.push(` [*] --> ${transition.to}${label ? ` : ${label}` : ''}`); }); // group transitions by from/to states and merge labels @@ -64,6 +65,13 @@ function getTransitionLabel(label: string, cond?: string | null): string { return `${escapeMermaidLabel(label)} (${escapeMermaidLabel(cond)})`; } +function getInitialTransitionLabel(cond?: string | null): string { + if (!cond) { + return ''; + } + return `(${escapeMermaidLabel(cond)})`; +} + function escapeMermaidLabel(label: string): string { return label.replace(/&/g, '&').replace(/"/g, '\\"').replace(//g, '>'); } diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 1a5996c..7139785 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -2,6 +2,8 @@ import type { LJStateMachine } from "../../../types/fsm"; import { renderMainHeader } from "../sections"; export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB"): string { + const initialStateNames = sm ? [...new Set(sm.initialTransitions.map(transition => transition.to))] : []; + return /*html*/`
${renderMainHeader("", 'fsm')} @@ -21,9 +23,9 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram:

States: ${sm.states.join(', ')}

-

Initial state${sm.initialStates.length > 1 ? 's' : ''}: ${sm.initialStates.join(', ')}

+

Initial state${initialStateNames.length > 1 ? 's' : ''}: ${initialStateNames.join(', ')}

Number of states: ${sm.states.length}

-

Number of transitions: ${sm.transitions.length + 1}

+

Number of transitions: ${sm.transitions.length + sm.initialTransitions.length}

` : 'No state machine available for the current file'} diff --git a/server/src/main/java/fsm/StateMachine.java b/server/src/main/java/fsm/StateMachine.java index c26d07c..f2cee34 100644 --- a/server/src/main/java/fsm/StateMachine.java +++ b/server/src/main/java/fsm/StateMachine.java @@ -7,7 +7,7 @@ */ public record StateMachine( String className, - List initialStates, List states, - List transitions + List transitions, + List initialTransitions ) { } diff --git a/server/src/main/java/fsm/StateMachineInitialTransition.java b/server/src/main/java/fsm/StateMachineInitialTransition.java new file mode 100644 index 0000000..e61294a --- /dev/null +++ b/server/src/main/java/fsm/StateMachineInitialTransition.java @@ -0,0 +1,11 @@ +package fsm; + +/** + * Represents an initial transition in a state machine + */ +public record StateMachineInitialTransition(String to, String cond) { + + public StateMachineInitialTransition(String to) { + this(to, null); + } +} diff --git a/server/src/main/java/fsm/StateMachineParser.java b/server/src/main/java/fsm/StateMachineParser.java index ac02985..ec63080 100644 --- a/server/src/main/java/fsm/StateMachineParser.java +++ b/server/src/main/java/fsm/StateMachineParser.java @@ -3,9 +3,7 @@ import java.net.URI; import java.util.ArrayList; import java.util.Collection; -import java.util.HashSet; import java.util.List; -import java.util.Set; import liquidjava.rj_language.ast.*; import liquidjava.rj_language.parsing.RefinementsParser; @@ -52,13 +50,16 @@ public static StateMachine parse(String uri) { return null; // no states found String className = getClassName(ctType); - // get initial states and transitions - List initialStates = getInitialStates(ctType, className, states); + // get initial transitions and method transitions + List initialTransitions = getInitialTransitions(ctType, className, states); + if (initialTransitions.isEmpty()) { + initialTransitions = List.of(new StateMachineInitialTransition(states.get(0))); + } List transitions = getTransitions(ctType, className, states); if (transitions.isEmpty()) return null; // no transitions found - return new StateMachine(className, initialStates, states, transitions); + return new StateMachine(className, states, transitions, initialTransitions); } catch (Exception e) { e.printStackTrace(); @@ -125,25 +126,24 @@ private static Collection getConstructorElements(CtType } /** - * Gets the initial states from a class or interface + * Gets the initial transitions from a class or interface * If not explicitly defined, uses the first state in the state set * @param ctType the CtType (class or interface) * @param className the class name * @param states the list of states - * @return initial states + * @return initial transitions */ - private static List getInitialStates(CtType ctType, String className, List states) { - Set initialStates = new HashSet<>(); + private static List getInitialTransitions(CtType ctType, String className, List states) { + List initialTransitions = new ArrayList<>(); for (CtElement element : getConstructorElements(ctType, className)) { for (CtAnnotation annotation : element.getAnnotations()) { if (annotation.getAnnotationType().getSimpleName().equals(STATE_REFINEMENT_ANNOTATION)) { String to = annotation.getValueAsString("to"); - List parsedStates = parseStateExpression(to, states); - initialStates.addAll(parsedStates); + initialTransitions.addAll(parseInitialTransitions(to, states)); } } } - return initialStates.isEmpty() ? List.of(states.get(0)) : initialStates.stream().toList(); + return initialTransitions; } /** @@ -210,27 +210,27 @@ private static List allStateSources(List states) { private static List parsePrecondition(String expr, List states) { Expression ast = RefinementsParser.createAST(expr, ""); - List sources = getPreconditionSources(ast, states); + List sources = getTransitionSources(ast, states, false); if (sources.isEmpty()) { sources = addCondition(allStateSources(states), ast.toString()); } return sources; } - private static List getPreconditionSources(Expression expr, List states) { + private static List getTransitionSources(Expression expr, List states, boolean stateOnlyDisjunctions) { String state = getStateName(expr, states); if (state != null) { return List.of(new TransitionSource(state, null)); } if (expr instanceof GroupExpression group) { - return getPreconditionSources(group.getExpression(), states); + return getTransitionSources(group.getExpression(), states, stateOnlyDisjunctions); } else if (expr instanceof BinaryExpression bin) { String op = bin.getOperator(); if (op.equals("&&")) { - return getConjunctionSources(bin, states); + return getConjunctionSources(bin, states, stateOnlyDisjunctions); } else if (op.equals("||")) { - return getDisjunctionSources(bin, states); + return stateOnlyDisjunctions ? getStateSources(bin, states) : getDisjunctionSources(bin, states); } } else if (expr instanceof UnaryExpression unary) { if (unary.getOp().equals("!")) { @@ -247,16 +247,16 @@ private static List getPreconditionSources(Expression expr, Li } } else if (expr instanceof Ite ite) { List sources = new ArrayList<>(); - sources.addAll(addCondition(getPreconditionSources(ite.getThen(), states), ite.getCondition().toString())); - sources.addAll(addCondition(getPreconditionSources(ite.getElse(), states), negateCondition(ite.getCondition()))); + sources.addAll(addCondition(getTransitionSources(ite.getThen(), states, stateOnlyDisjunctions), ite.getCondition().toString())); + sources.addAll(addCondition(getTransitionSources(ite.getElse(), states, stateOnlyDisjunctions), negateCondition(ite.getCondition()))); return sources; } return new ArrayList<>(); } - private static List getConjunctionSources(BinaryExpression bin, List states) { - List leftSources = getPreconditionSources(bin.getFirstOperand(), states); - List rightSources = getPreconditionSources(bin.getSecondOperand(), states); + private static List getConjunctionSources(BinaryExpression bin, List states, boolean stateOnlyDisjunctions) { + List leftSources = getTransitionSources(bin.getFirstOperand(), states, stateOnlyDisjunctions); + List rightSources = getTransitionSources(bin.getSecondOperand(), states, stateOnlyDisjunctions); if (leftSources.isEmpty() && rightSources.isEmpty()) { return new ArrayList<>(); @@ -279,7 +279,7 @@ private static List getDisjunctionSources(BinaryExpression bin } private static void addDisjunctionBranch(List sources, Expression expr, List states) { - List parsedSources = getPreconditionSources(expr, states); + List parsedSources = getTransitionSources(expr, states, false); if (parsedSources.isEmpty()) { sources.addAll(addCondition(allStateSources(states), expr.toString())); } else { @@ -332,6 +332,24 @@ private static String negateCondition(Expression expr) { return "!(" + condition + ")"; } + private static List parseInitialTransitions(String expr, List states) { + if (expr == null || expr.isEmpty()) return new ArrayList<>(); + Expression ast = RefinementsParser.createAST(expr, ""); + List initialTransitions = new ArrayList<>(); + for (TransitionSource source : getTransitionSources(ast, states, true)) { + initialTransitions.add(new StateMachineInitialTransition(source.from(), source.cond())); + } + return initialTransitions; + } + + private static List getStateSources(Expression expr, List states) { + List sources = new ArrayList<>(); + for (String state : getStateExpressions(expr, states)) { + sources.add(new TransitionSource(state, null)); + } + return sources; + } + /** * Parses a state expression and returns the list of states * @param expr the expression diff --git a/server/src/test/java/fsm/StateMachineParserTests.java b/server/src/test/java/fsm/StateMachineParserTests.java index 8eb8653..20b1a59 100644 --- a/server/src/test/java/fsm/StateMachineParserTests.java +++ b/server/src/test/java/fsm/StateMachineParserTests.java @@ -15,9 +15,10 @@ public class StateMachineParserTests { @Test public void testSimpleStateMachine() { StateMachine sm = StateMachineParser.parse(BASE_URI + "Simple.java"); - StateMachine expectedSm = new StateMachine("Simple", List.of("open"), List.of("open", "closed"), + StateMachine expectedSm = new StateMachine("Simple", List.of("open", "closed"), List.of(new StateMachineTransition("open", "closed", "close"), - new StateMachineTransition("open", "open", "read"))); + new StateMachineTransition("open", "open", "read")), + List.of(new StateMachineInitialTransition("open"))); assertStateMachineEquals(expectedSm, sm); } @@ -25,8 +26,9 @@ public void testSimpleStateMachine() { public void testOrTransition() { // state1 || state2 => separate transitions from both state1 and state2 StateMachine sm = StateMachineParser.parse(BASE_URI + "OrTransition.java"); - StateMachine expectedSm = new StateMachine("OrTransition", List.of("a"), List.of("a", "b", "c"), List - .of(new StateMachineTransition("a", "c", "action"), new StateMachineTransition("b", "c", "action"))); + StateMachine expectedSm = new StateMachine("OrTransition", List.of("a", "b", "c"), List + .of(new StateMachineTransition("a", "c", "action"), new StateMachineTransition("b", "c", "action")), + List.of(new StateMachineInitialTransition("a"))); assertStateMachineEquals(expectedSm, sm); } @@ -34,9 +36,10 @@ public void testOrTransition() { public void testNegationTransition() { // !state => all states except state StateMachine sm = StateMachineParser.parse(BASE_URI + "NegationTransition.java"); - StateMachine expectedSm = new StateMachine("NegationTransition", List.of("open"), - List.of("open", "closed", "locked"), List.of(new StateMachineTransition("open", "locked", "lock"), - new StateMachineTransition("closed", "locked", "lock"))); + StateMachine expectedSm = new StateMachine("NegationTransition", List.of("open", "closed", "locked"), + List.of(new StateMachineTransition("open", "locked", "lock"), + new StateMachineTransition("closed", "locked", "lock")), + List.of(new StateMachineInitialTransition("open"))); assertStateMachineEquals(expectedSm, sm); } @@ -44,10 +47,11 @@ public void testNegationTransition() { public void testSelfLoop() { // from=state, to=state or from=state => self-loop StateMachine sm = StateMachineParser.parse(BASE_URI + "SelfLoop.java"); - StateMachine expectedSm = new StateMachine("SelfLoop", List.of("idle"), List.of("idle", "running"), + StateMachine expectedSm = new StateMachine("SelfLoop", List.of("idle", "running"), List.of(new StateMachineTransition("idle", "idle", "noop"), new StateMachineTransition("idle", "running", "start"), - new StateMachineTransition("running", "running", "tick"))); + new StateMachineTransition("running", "running", "tick")), + List.of(new StateMachineInitialTransition("idle"))); assertStateMachineEquals(expectedSm, sm); } @@ -55,9 +59,10 @@ public void testSelfLoop() { public void testToOnlyTransition() { // no from => all states contain a transition to state StateMachine sm = StateMachineParser.parse(BASE_URI + "ToOnlyTransition.java"); - StateMachine expectedSm = new StateMachine("ToOnlyTransition", List.of("a"), List.of("a", "b", "c"), + StateMachine expectedSm = new StateMachine("ToOnlyTransition", List.of("a", "b", "c"), List.of(new StateMachineTransition("a", "c", "action"), new StateMachineTransition("b", "c", "action"), - new StateMachineTransition("c", "c", "action"))); + new StateMachineTransition("c", "c", "action")), + List.of(new StateMachineInitialTransition("a"))); assertStateMachineEquals(expectedSm, sm); } @@ -65,9 +70,10 @@ public void testToOnlyTransition() { public void testMultipleInitialStates() { // overloading constructors with different initial states StateMachine sm = StateMachineParser.parse(BASE_URI + "MultipleInitialStates.java"); - StateMachine expectedSm = new StateMachine("MultipleInitialStates", List.of("initialized", "uninitialized"), - List.of("initialized", "uninitialized", "error"), - List.of(new StateMachineTransition("uninitialized", "initialized", "init"))); + StateMachine expectedSm = new StateMachine("MultipleInitialStates", List.of("initialized", "uninitialized", "error"), + List.of(new StateMachineTransition("uninitialized", "initialized", "init")), + List.of(new StateMachineInitialTransition("uninitialized"), + new StateMachineInitialTransition("initialized"))); assertStateMachineEquals(expectedSm, sm); } @@ -75,9 +81,9 @@ public void testMultipleInitialStates() { public void testExternalRefinementsInterface() { // class name from @ExternalStateRefinements StateMachine sm = StateMachineParser.parse(BASE_URI + "ExternalRefinements.java"); - StateMachine expectedSm = new StateMachine("Connection", List.of("disconnected"), - List.of("connected", "disconnected"), - List.of(new StateMachineTransition("disconnected", "connected", "connect"))); + StateMachine expectedSm = new StateMachine("Connection", List.of("connected", "disconnected"), + List.of(new StateMachineTransition("disconnected", "connected", "connect")), + List.of(new StateMachineInitialTransition("disconnected"))); assertStateMachineEquals(expectedSm, sm); } @@ -85,55 +91,66 @@ public void testExternalRefinementsInterface() { public void testConditionalTransition() { // transitions for both branches of condition StateMachine sm = StateMachineParser.parse(BASE_URI + "ConditionalTransition.java"); - StateMachine expectedSm = new StateMachine("ConditionalTransition", List.of("off", "on"), List.of("on", "off"), + StateMachine expectedSm = new StateMachine("ConditionalTransition", List.of("on", "off"), List.of(new StateMachineTransition("on", "off", "turnOff"), - new StateMachineTransition("off", "on", "turnOn"))); + new StateMachineTransition("off", "on", "turnOn")), + List.of(new StateMachineInitialTransition("on", "flag"), + new StateMachineInitialTransition("off", "!flag"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testConjunctionInitialTransition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "ConjunctionInitialTransition.java"); + StateMachine expectedSm = new StateMachine("ConjunctionInitialTransition", List.of("on", "off"), + List.of(new StateMachineTransition("on", "off", "turnOff")), + List.of(new StateMachineInitialTransition("on", "flag"))); assertStateMachineEquals(expectedSm, sm); } @Test public void testConjunctionPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "ConjunctionPrecondition.java"); - StateMachine expectedSm = new StateMachine("ConjunctionPrecondition", List.of("open"), - List.of("open", "closed"), - List.of(new StateMachineTransition("open", "closed", "close", "flag"))); + StateMachine expectedSm = new StateMachine("ConjunctionPrecondition", List.of("open", "closed"), + List.of(new StateMachineTransition("open", "closed", "close", "flag")), + List.of(new StateMachineInitialTransition("open"))); assertStateMachineEquals(expectedSm, sm); } @Test public void testDisjunctionPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "DisjunctionPrecondition.java"); - StateMachine expectedSm = new StateMachine("DisjunctionPrecondition", List.of("ready"), - List.of("ready", "waiting", "done"), + StateMachine expectedSm = new StateMachine("DisjunctionPrecondition", List.of("ready", "waiting", "done"), List.of(new StateMachineTransition("waiting", "done", "action", "flag"), new StateMachineTransition("done", "done", "action", "flag"), - new StateMachineTransition("ready", "done", "action"))); + new StateMachineTransition("ready", "done", "action")), + List.of(new StateMachineInitialTransition("ready"))); assertStateMachineEquals(expectedSm, sm); } @Test public void testConditionalPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "ConditionalPrecondition.java"); - StateMachine expectedSm = new StateMachine("ConditionalPrecondition", List.of("left"), - List.of("left", "right", "done"), + StateMachine expectedSm = new StateMachine("ConditionalPrecondition", List.of("left", "right", "done"), List.of(new StateMachineTransition("left", "done", "finish", "flag"), - new StateMachineTransition("right", "done", "finish", "!flag"))); + new StateMachineTransition("right", "done", "finish", "!flag")), + List.of(new StateMachineInitialTransition("left"))); assertStateMachineEquals(expectedSm, sm); } @Test public void testPostConditionFiltering() { StateMachine sm = StateMachineParser.parse(BASE_URI + "PostConditionFiltering.java"); - StateMachine expectedSm = new StateMachine("PostConditionFiltering", List.of("ready"), - List.of("ready", "done"), - List.of(new StateMachineTransition("ready", "done", "finish"))); + StateMachine expectedSm = new StateMachine("PostConditionFiltering", List.of("ready", "done"), + List.of(new StateMachineTransition("ready", "done", "finish")), + List.of(new StateMachineInitialTransition("ready"))); assertStateMachineEquals(expectedSm, sm); } 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.initialStates(), actual.initialStates(), "Initial states should match"); + assertEquals(expected.initialTransitions(), actual.initialTransitions(), "Initial transitions should match"); assertEquals(expected.states(), actual.states(), "States should match"); assertEquals(expected.transitions(), actual.transitions(), "State transitions should match"); } diff --git a/server/src/test/resources/fsm/ConjunctionInitialTransition.java b/server/src/test/resources/fsm/ConjunctionInitialTransition.java new file mode 100644 index 0000000..e54a32e --- /dev/null +++ b/server/src/test/resources/fsm/ConjunctionInitialTransition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"on", "off"}) +public class ConjunctionInitialTransition { + + @StateRefinement(to="flag && on(this)") + public ConjunctionInitialTransition(boolean flag) {} + + @StateRefinement(from="on(this)", to="off(this)") + public void turnOff() {} +} From 1604a4d6c0a21d127e0df939f9b63268fde61e78 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 18:06:05 +0100 Subject: [PATCH 3/6] Handle Post-Conditions --- client/src/types/fsm.ts | 4 +- client/src/webview/diagram.ts | 23 +++++---- client/src/webview/styles.ts | 4 +- .../fsm/StateMachineInitialTransition.java | 2 +- .../src/main/java/fsm/StateMachineParser.java | 40 +++++++--------- .../main/java/fsm/StateMachineTransition.java | 4 +- .../java/fsm/StateMachineParserTests.java | 47 +++++++++++++++++-- .../resources/fsm/CombinedPostCondition.java | 14 ++++++ .../fsm/ConditionalPostCondition.java | 14 ++++++ .../fsm/DisjunctionPostCondition.java | 14 ++++++ .../test/resources/fsm/GuardedSelfLoop.java | 14 ++++++ 11 files changed, 138 insertions(+), 42 deletions(-) create mode 100644 server/src/test/resources/fsm/CombinedPostCondition.java create mode 100644 server/src/test/resources/fsm/ConditionalPostCondition.java create mode 100644 server/src/test/resources/fsm/DisjunctionPostCondition.java create mode 100644 server/src/test/resources/fsm/GuardedSelfLoop.java diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 244e664..1385fe6 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -2,7 +2,7 @@ export type LJStateMachine = { className: string; - initialTransitions: { to: string; cond?: string | null }[]; + initialTransitions: { to: string; postCond?: string | null }[]; states: string[]; - transitions: { from: string; to: string; label: string; cond?: string | null }[]; + transitions: { from: string; to: string; label: string; preCond?: string | null; postCond?: string | null }[]; }; diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 6981062..2ef929a 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -35,14 +35,14 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation // initial transitions sm.initialTransitions.forEach(transition => { - const label = getInitialTransitionLabel(transition.cond); + const label = getInitialTransitionLabel(transition.postCond); lines.push(` [*] --> ${transition.to}${label ? ` : ${label}` : ''}`); }); // group transitions by from/to states and merge labels const transitionMap = new Map(); sm.transitions.forEach(transition => { - const label = getTransitionLabel(transition.label, transition.cond); + const label = getTransitionLabel(transition.label, transition.preCond, transition.postCond); const key = `${transition.from}|${transition.to}`; if (!transitionMap.has(key)) transitionMap.set(key, []); transitionMap.get(key)?.push(label); @@ -58,18 +58,23 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation return lines.join('\n'); } -function getTransitionLabel(label: string, cond?: string | null): string { - if (!cond) { - return escapeMermaidLabel(label); - } - return `${escapeMermaidLabel(label)} (${escapeMermaidLabel(cond)})`; +function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null): string { + return [ + getConditionLabel(preCond), + escapeMermaidLabel(label), + getConditionLabel(postCond) + ].filter(Boolean).join('
'); +} + +function getInitialTransitionLabel(postCond?: string | null): string { + return getConditionLabel(postCond); } -function getInitialTransitionLabel(cond?: string | null): string { +function getConditionLabel(cond?: string | null): string { if (!cond) { return ''; } - return `(${escapeMermaidLabel(cond)})`; + return `${escapeMermaidLabel(cond)}`; } function escapeMermaidLabel(label: string): string { diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 1bb1a69..e27719e 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -652,7 +652,9 @@ export function getStyles(): string { } .diagram-container .mermaid .edgeLabel .state-cond { color: var(--vscode-descriptionForeground) !important; - font-size: 0.85em !important; + display: inline-block !important; + font-size: 0.82em !important; + line-height: 1.2 !important; } .diagram-container .mermaid svg rect, .diagram-container .mermaid svg circle, diff --git a/server/src/main/java/fsm/StateMachineInitialTransition.java b/server/src/main/java/fsm/StateMachineInitialTransition.java index e61294a..23a9b9c 100644 --- a/server/src/main/java/fsm/StateMachineInitialTransition.java +++ b/server/src/main/java/fsm/StateMachineInitialTransition.java @@ -3,7 +3,7 @@ /** * Represents an initial transition in a state machine */ -public record StateMachineInitialTransition(String to, String cond) { +public record StateMachineInitialTransition(String to, String postCond) { public StateMachineInitialTransition(String to) { this(to, null); diff --git a/server/src/main/java/fsm/StateMachineParser.java b/server/src/main/java/fsm/StateMachineParser.java index ec63080..a8c6a9e 100644 --- a/server/src/main/java/fsm/StateMachineParser.java +++ b/server/src/main/java/fsm/StateMachineParser.java @@ -182,19 +182,16 @@ private static List getTransitions(CtAnnotation ann, String from = ann.getValueAsString("from"); String to = ann.getValueAsString("to"); - // if has from but not to, to is the same as from (self-loop) - if (!from.isEmpty() && to.isEmpty()) { - to = from; - } - // parse from and to expressions List fromSources = from.isEmpty() ? allStateSources(states) : parsePrecondition(from, states); - List toStates = parseStateExpression(to, states); + List toSources = !from.isEmpty() && to.isEmpty() + ? parseStateSources(from, states) + : parsePostcondition(to, states); // create transitions for each combination of from and to states for (TransitionSource fromSource : fromSources) { - for (String toState : toStates) { - transitions.add(new StateMachineTransition(fromSource.from(), toState, method, fromSource.cond())); + for (TransitionSource toSource : toSources) { + transitions.add(new StateMachineTransition(fromSource.from(), toSource.from(), method, fromSource.cond(), toSource.cond())); } } return transitions; @@ -217,6 +214,12 @@ private static List parsePrecondition(String expr, List parsePostcondition(String expr, List states) { + if (expr == null || expr.isEmpty()) return new ArrayList<>(); + Expression ast = RefinementsParser.createAST(expr, ""); + return getTransitionSources(ast, states, true); + } + private static List getTransitionSources(Expression expr, List states, boolean stateOnlyDisjunctions) { String state = getStateName(expr, states); if (state != null) { @@ -334,14 +337,19 @@ private static String negateCondition(Expression expr) { private static List parseInitialTransitions(String expr, List states) { if (expr == null || expr.isEmpty()) return new ArrayList<>(); - Expression ast = RefinementsParser.createAST(expr, ""); List initialTransitions = new ArrayList<>(); - for (TransitionSource source : getTransitionSources(ast, states, true)) { + for (TransitionSource source : parsePostcondition(expr, states)) { initialTransitions.add(new StateMachineInitialTransition(source.from(), source.cond())); } return initialTransitions; } + private static List parseStateSources(String expr, List states) { + if (expr == null || expr.isEmpty()) return new ArrayList<>(); + Expression ast = RefinementsParser.createAST(expr, ""); + return getStateSources(ast, states); + } + private static List getStateSources(Expression expr, List states) { List sources = new ArrayList<>(); for (String state : getStateExpressions(expr, states)) { @@ -350,18 +358,6 @@ private static List getStateSources(Expression expr, List parseStateExpression(String expr, List states) { - if (expr == null || expr.isEmpty()) return new ArrayList<>(); - Expression ast = RefinementsParser.createAST(expr, ""); - return getStateExpressions(ast, states); - } - /** * Gets state names from an expression AST recursively * @param expr the expression diff --git a/server/src/main/java/fsm/StateMachineTransition.java b/server/src/main/java/fsm/StateMachineTransition.java index 49cec71..33f0f58 100644 --- a/server/src/main/java/fsm/StateMachineTransition.java +++ b/server/src/main/java/fsm/StateMachineTransition.java @@ -3,9 +3,9 @@ /** * Represents a transition in a state machine */ -public record StateMachineTransition(String from, String to, String label, String cond) { +public record StateMachineTransition(String from, String to, String label, String preCond, String postCond) { public StateMachineTransition(String from, String to, String label) { - this(from, to, label, null); + this(from, to, label, null, null); } } diff --git a/server/src/test/java/fsm/StateMachineParserTests.java b/server/src/test/java/fsm/StateMachineParserTests.java index 20b1a59..08e97e2 100644 --- a/server/src/test/java/fsm/StateMachineParserTests.java +++ b/server/src/test/java/fsm/StateMachineParserTests.java @@ -112,7 +112,7 @@ public void testConjunctionInitialTransition() { public void testConjunctionPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "ConjunctionPrecondition.java"); StateMachine expectedSm = new StateMachine("ConjunctionPrecondition", List.of("open", "closed"), - List.of(new StateMachineTransition("open", "closed", "close", "flag")), + List.of(new StateMachineTransition("open", "closed", "close", "flag", null)), List.of(new StateMachineInitialTransition("open"))); assertStateMachineEquals(expectedSm, sm); } @@ -121,8 +121,8 @@ public void testConjunctionPrecondition() { public void testDisjunctionPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "DisjunctionPrecondition.java"); StateMachine expectedSm = new StateMachine("DisjunctionPrecondition", List.of("ready", "waiting", "done"), - List.of(new StateMachineTransition("waiting", "done", "action", "flag"), - new StateMachineTransition("done", "done", "action", "flag"), + List.of(new StateMachineTransition("waiting", "done", "action", "flag", null), + new StateMachineTransition("done", "done", "action", "flag", null), new StateMachineTransition("ready", "done", "action")), List.of(new StateMachineInitialTransition("ready"))); assertStateMachineEquals(expectedSm, sm); @@ -132,8 +132,8 @@ public void testDisjunctionPrecondition() { public void testConditionalPrecondition() { StateMachine sm = StateMachineParser.parse(BASE_URI + "ConditionalPrecondition.java"); StateMachine expectedSm = new StateMachine("ConditionalPrecondition", List.of("left", "right", "done"), - List.of(new StateMachineTransition("left", "done", "finish", "flag"), - new StateMachineTransition("right", "done", "finish", "!flag")), + List.of(new StateMachineTransition("left", "done", "finish", "flag", null), + new StateMachineTransition("right", "done", "finish", "!flag", null)), List.of(new StateMachineInitialTransition("left"))); assertStateMachineEquals(expectedSm, sm); } @@ -142,11 +142,48 @@ public void testConditionalPrecondition() { public void testPostConditionFiltering() { StateMachine sm = StateMachineParser.parse(BASE_URI + "PostConditionFiltering.java"); StateMachine expectedSm = new StateMachine("PostConditionFiltering", List.of("ready", "done"), + List.of(new StateMachineTransition("ready", "done", "finish", null, "flag")), + List.of(new StateMachineInitialTransition("ready"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testCombinedPostCondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "CombinedPostCondition.java"); + StateMachine expectedSm = new StateMachine("CombinedPostCondition", List.of("ready", "done"), + List.of(new StateMachineTransition("ready", "done", "finish", "x", "flag")), + List.of(new StateMachineInitialTransition("ready"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testConditionalPostCondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "ConditionalPostCondition.java"); + StateMachine expectedSm = new StateMachine("ConditionalPostCondition", List.of("ready", "done", "error"), + List.of(new StateMachineTransition("ready", "done", "finish", null, "flag"), + new StateMachineTransition("ready", "error", "finish", null, "!flag")), + List.of(new StateMachineInitialTransition("ready"))); + assertStateMachineEquals(expectedSm, sm); + } + + @Test + public void testDisjunctionPostCondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "DisjunctionPostCondition.java"); + StateMachine expectedSm = new StateMachine("DisjunctionPostCondition", List.of("ready", "done"), List.of(new StateMachineTransition("ready", "done", "finish")), List.of(new StateMachineInitialTransition("ready"))); assertStateMachineEquals(expectedSm, sm); } + @Test + public void testGuardedSelfLoopDoesNotDuplicateCondition() { + StateMachine sm = StateMachineParser.parse(BASE_URI + "GuardedSelfLoop.java"); + StateMachine expectedSm = new StateMachine("GuardedSelfLoop", List.of("ready", "done"), + List.of(new StateMachineTransition("ready", "ready", "poll", "flag", null)), + List.of(new StateMachineInitialTransition("ready"))); + assertStateMachineEquals(expectedSm, sm); + } + 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"); diff --git a/server/src/test/resources/fsm/CombinedPostCondition.java b/server/src/test/resources/fsm/CombinedPostCondition.java new file mode 100644 index 0000000..83f0099 --- /dev/null +++ b/server/src/test/resources/fsm/CombinedPostCondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "done"}) +public class CombinedPostCondition { + + @StateRefinement(to="ready(this)") + public CombinedPostCondition() {} + + @StateRefinement(from="x && ready(this)", to="done(this) && flag") + public void finish(boolean x, boolean flag) {} +} diff --git a/server/src/test/resources/fsm/ConditionalPostCondition.java b/server/src/test/resources/fsm/ConditionalPostCondition.java new file mode 100644 index 0000000..9225cc3 --- /dev/null +++ b/server/src/test/resources/fsm/ConditionalPostCondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "done", "error"}) +public class ConditionalPostCondition { + + @StateRefinement(to="ready(this)") + public ConditionalPostCondition() {} + + @StateRefinement(from="ready(this)", to="flag ? done(this) : error(this)") + public void finish(boolean flag) {} +} diff --git a/server/src/test/resources/fsm/DisjunctionPostCondition.java b/server/src/test/resources/fsm/DisjunctionPostCondition.java new file mode 100644 index 0000000..8bd23f1 --- /dev/null +++ b/server/src/test/resources/fsm/DisjunctionPostCondition.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "done"}) +public class DisjunctionPostCondition { + + @StateRefinement(to="ready(this)") + public DisjunctionPostCondition() {} + + @StateRefinement(from="ready(this)", to="done(this) || flag") + public void finish(boolean flag) {} +} diff --git a/server/src/test/resources/fsm/GuardedSelfLoop.java b/server/src/test/resources/fsm/GuardedSelfLoop.java new file mode 100644 index 0000000..685bc7e --- /dev/null +++ b/server/src/test/resources/fsm/GuardedSelfLoop.java @@ -0,0 +1,14 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"ready", "done"}) +public class GuardedSelfLoop { + + @StateRefinement(to="ready(this)") + public GuardedSelfLoop() {} + + @StateRefinement(from="flag && ready(this)") + public void poll(boolean flag) {} +} From 99291efffd11753fefaeabf6d1f6a2647ca690e6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 18:16:16 +0100 Subject: [PATCH 4/6] Expand & Collapse Conditions in Diagram --- client/src/webview/diagram.ts | 16 ++++++++++------ client/src/webview/script.ts | 15 +++++++++++++-- client/src/webview/styles.ts | 5 ++++- client/src/webview/views/fsm/fsm.ts | 9 ++++++++- 4 files changed, 35 insertions(+), 10 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 2ef929a..16afe85 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -21,7 +21,7 @@ let startY = 0; * @param sm * @returns Mermaid diagram string */ -export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation: "LR" | "TB"): string { +export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation: "LR" | "TB", showConditions = false): string { if (!sm) return ''; const lines: string[] = []; @@ -35,14 +35,14 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation // initial transitions sm.initialTransitions.forEach(transition => { - const label = getInitialTransitionLabel(transition.postCond); + const label = getInitialTransitionLabel(transition.postCond, showConditions); lines.push(` [*] --> ${transition.to}${label ? ` : ${label}` : ''}`); }); // group transitions by from/to states and merge labels const transitionMap = new Map(); sm.transitions.forEach(transition => { - const label = getTransitionLabel(transition.label, transition.preCond, transition.postCond); + const label = getTransitionLabel(transition.label, transition.preCond, transition.postCond, showConditions); const key = `${transition.from}|${transition.to}`; if (!transitionMap.has(key)) transitionMap.set(key, []); transitionMap.get(key)?.push(label); @@ -58,7 +58,11 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation return lines.join('\n'); } -function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null): string { +function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null, showConditions = false): string { + if (!showConditions) { + return escapeMermaidLabel(label); + } + return [ getConditionLabel(preCond), escapeMermaidLabel(label), @@ -66,8 +70,8 @@ function getTransitionLabel(label: string, preCond?: string | null, postCond?: s ].filter(Boolean).join('
'); } -function getInitialTransitionLabel(postCond?: string | null): string { - return getConditionLabel(postCond); +function getInitialTransitionLabel(postCond?: string | null, showConditions = false): string { + return showConditions ? getConditionLabel(postCond) : ''; } function getConditionLabel(cond?: string | null): string { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index f2fcb37..ea0c6e6 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -34,6 +34,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let errorAtCursor: RefinementMismatchError; let selectedTab: NavTab = 'diagnostics'; let diagramOrientation: "LR" | "TB" = "TB"; + let showDiagramConditions = false; let currentDiagram: string = ''; let revealTimeout: ReturnType | undefined; const contextSectionState: ContextSectionState = { @@ -147,6 +148,15 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) return; } + // toggle diagram conditions + if (target.id === 'diagram-conditions-btn') { + e.stopPropagation(); + if ((target as HTMLButtonElement).disabled) return; + showDiagramConditions = !showDiagramConditions; + updateView(); + return; + } + // zoom in if (target.id === 'zoom-in-btn') { e.stopPropagation(); @@ -260,6 +270,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) break; case 'fsm': stateMachine = msg.sm as LJStateMachine; + showDiagramConditions = false; if (selectedTab === 'fsm') updateView(); break; case 'context': @@ -282,9 +293,9 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) root.innerHTML = renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, expandedErrors); break; case 'fsm': { - const diagram = createMermaidDiagram(stateMachine, diagramOrientation); + const diagram = createMermaidDiagram(stateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; - root.innerHTML = renderStateMachineView(stateMachine, diagram, diagramOrientation); + root.innerHTML = renderStateMachineView(stateMachine, diagram, diagramOrientation, showDiagramConditions); if (stateMachine) renderMermaidDiagram(document, window); break; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e27719e..479db10 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -619,9 +619,12 @@ export function getStyles(): string { background: none; opacity: 1; } + .diagram-control-btn.active { + opacity: 1; + } .diagram-control-btn:disabled { cursor: default; - opacity: 0.8; + opacity: 0.35; } .mermaid .statediagramTitleText { font-size: 30px!important; diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 7139785..bf10010 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,8 +1,14 @@ import type { LJStateMachine } from "../../../types/fsm"; import { renderMainHeader } from "../sections"; -export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB"): string { +export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean): string { const initialStateNames = sm ? [...new Set(sm.initialTransitions.map(transition => transition.to))] : []; + const hasConditionExpansions = sm + ? sm.initialTransitions.some(transition => !!transition.postCond) + || sm.transitions.some(transition => !!transition.preCond || !!transition.postCond) + : false; + const conditionToggleLabel = showConditions ? 'Collapse Conditions' : 'Expand Conditions'; + const conditionToggleIcon = showConditions ? '⊟' : '⊞'; return /*html*/`
@@ -15,6 +21,7 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: +
From 0c1adb93ed05035a2b2b054dbda03efe304c5994 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:08:04 +0100 Subject: [PATCH 5/6] Add Colors --- client/src/webview/diagram.ts | 10 +++++----- client/src/webview/styles.ts | 8 ++++++++ 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 16afe85..3cbf58f 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -64,21 +64,21 @@ function getTransitionLabel(label: string, preCond?: string | null, postCond?: s } return [ - getConditionLabel(preCond), + getConditionLabel('pre', preCond), escapeMermaidLabel(label), - getConditionLabel(postCond) + getConditionLabel('post', postCond) ].filter(Boolean).join('
'); } function getInitialTransitionLabel(postCond?: string | null, showConditions = false): string { - return showConditions ? getConditionLabel(postCond) : ''; + return showConditions ? getConditionLabel('post', postCond) : ''; } -function getConditionLabel(cond?: string | null): string { +function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string { if (!cond) { return ''; } - return `${escapeMermaidLabel(cond)}`; + return `${kind}: ${escapeMermaidLabel(cond)}`; } function escapeMermaidLabel(label: string): string { diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 479db10..2873aac 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -38,6 +38,8 @@ export function getStyles(): string { --lj-token-boolean: var(--vscode-debugTokenExpression-boolean, var(--vscode-symbolIcon-booleanForeground, var(--vscode-editor-foreground))); --lj-token-identifier: var(--vscode-debugTokenExpression-name, var(--vscode-editor-foreground)); --lj-token-punctuation: var(--vscode-editor-foreground); + --lj-state-cond-pre: var(--lj-token-function); + --lj-state-cond-post: var(--lj-token-type); } body.vscode-light { --lj-token-keyword: #0000FF; @@ -659,6 +661,12 @@ export function getStyles(): string { font-size: 0.82em !important; line-height: 1.2 !important; } + .diagram-container .mermaid .edgeLabel .state-cond-pre { + color: var(--lj-state-cond-pre) !important; + } + .diagram-container .mermaid .edgeLabel .state-cond-post { + color: var(--lj-state-cond-post) !important; + } .diagram-container .mermaid svg rect, .diagram-container .mermaid svg circle, .diagram-container .mermaid svg ellipse, From 247d03ce24137d48dff1938db799a6f6e679a0d9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:52:35 +0100 Subject: [PATCH 6/6] Remove Prefix from Labels --- client/src/webview/diagram.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 3cbf58f..19c6a7e 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -78,7 +78,7 @@ function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string { if (!cond) { return ''; } - return `${kind}: ${escapeMermaidLabel(cond)}`; + return `${escapeMermaidLabel(cond)}`; } function escapeMermaidLabel(label: string): string {