From 404f66c2477fe59448ce0ef8f40d02afbaac7989 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 17:08:19 +0100 Subject: [PATCH 01/22] 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 02/22] 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 03/22] 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 04/22] 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 05/22] 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 a2a5f9e900d10f603e475738e54aafe70715a471 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:23:49 +0100 Subject: [PATCH 06/22] Add New Icons to Webview --- client/.vscodeignore | 6 ++++ client/package-lock.json | 12 ++++++++ client/package.json | 1 + client/src/webview/html.ts | 4 ++- client/src/webview/icons.ts | 4 +++ client/src/webview/script.ts | 21 ++++++++------ client/src/webview/styles.ts | 29 ++++++++++++++----- .../views/diagnostics/derivation-nodes.ts | 3 +- .../webview/views/diagnostics/diagnostics.ts | 3 +- client/src/webview/views/fsm/fsm.ts | 14 ++++----- client/src/webview/views/sections.ts | 3 +- 11 files changed, 73 insertions(+), 27 deletions(-) create mode 100644 client/src/webview/icons.ts diff --git a/client/.vscodeignore b/client/.vscodeignore index c04789a..0f5bd73 100644 --- a/client/.vscodeignore +++ b/client/.vscodeignore @@ -11,6 +11,12 @@ vsc-extension-quickstart.md # Build artifacts out/** node_modules/** +!node_modules/ +!node_modules/@vscode/ +!node_modules/@vscode/codicons/ +!node_modules/@vscode/codicons/dist/ +!node_modules/@vscode/codicons/dist/codicon.css +!node_modules/@vscode/codicons/dist/codicon.ttf *.vsix # Test files diff --git a/client/package-lock.json b/client/package-lock.json index c40ab3c..bfd164f 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -9,6 +9,7 @@ "version": "0.0.78", "license": "MIT", "dependencies": { + "@vscode/codicons": "^0.0.45", "ftp": "^0.3.10", "get-port": "^5.1.1", "jsonc-parser": "^0.4.2", @@ -3212,9 +3213,20 @@ "engines": { "node": ">=0.10.0" } + }, + "node_modules/@vscode/codicons": { + "version": "0.0.45", + "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.45.tgz", + "integrity": "sha512-1KAZ7XCMagp5Gdrlr4bbbcAqgcIL623iO1wW6rfcSVGAVUQvR0WP7bQx1SbJ11gmV3fdQTSEFIJQ/5C+HuVasw==", + "license": "CC-BY-4.0" } }, "dependencies": { + "@vscode/codicons": { + "version": "0.0.45", + "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.45.tgz", + "integrity": "sha512-1KAZ7XCMagp5Gdrlr4bbbcAqgcIL623iO1wW6rfcSVGAVUQvR0WP7bQx1SbJ11gmV3fdQTSEFIJQ/5C+HuVasw==" + }, "@babel/code-frame": { "version": "7.12.11", "resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.12.11.tgz", diff --git a/client/package.json b/client/package.json index 3febc8e..da7ebae 100644 --- a/client/package.json +++ b/client/package.json @@ -178,6 +178,7 @@ "webpack-cli": "^5.1.4" }, "dependencies": { + "@vscode/codicons": "^0.0.45", "ftp": "^0.3.10", "get-port": "^5.1.1", "jsonc-parser": "^0.4.2", diff --git a/client/src/webview/html.ts b/client/src/webview/html.ts index c878007..f444fb1 100644 --- a/client/src/webview/html.ts +++ b/client/src/webview/html.ts @@ -13,6 +13,7 @@ export function getHtml(webview: vscode.Webview, extensionUri: vscode.Uri): stri const nonce = Date.now().toString(); const cspSource = webview.cspSource; const scriptUri = webview.asWebviewUri(vscode.Uri.joinPath(extensionUri, "media", "webview.js")); + const codiconsUri = webview.asWebviewUri(vscode.Uri.joinPath(extensionUri, "node_modules", "@vscode", "codicons", "dist", "codicon.css")); return /*html*/ ` @@ -21,8 +22,9 @@ export function getHtml(webview: vscode.Webview, extensionUri: vscode.Uri): stri + diff --git a/client/src/webview/icons.ts b/client/src/webview/icons.ts new file mode 100644 index 0000000..bd82bed --- /dev/null +++ b/client/src/webview/icons.ts @@ -0,0 +1,4 @@ +export function renderCodicon(name: string, className = ""): string { + const classes = ["codicon", `codicon-${name}`, className].filter(Boolean).join(" "); + return ``; +} diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index ea0c6e6..da67c94 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -74,7 +74,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const icon = contextToggleButton.querySelector('.context-toggle-icon'); if (icon) { - icon.textContent = nextExpanded ? '▾' : '▸'; + icon.classList.toggle('codicon-chevron-down', nextExpanded); + icon.classList.toggle('codicon-chevron-right', !nextExpanded); } return; @@ -140,7 +141,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } // toggle diagram orientation - if (target.id === 'diagram-orientation-btn') { + if (target.closest?.('#diagram-orientation-btn')) { e.stopPropagation(); diagramOrientation = diagramOrientation === "TB" ? "LR" : "TB"; resetZoom(document); @@ -149,40 +150,42 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } // toggle diagram conditions - if (target.id === 'diagram-conditions-btn') { + const diagramConditionsButton = target.closest?.('#diagram-conditions-btn'); + if (diagramConditionsButton) { e.stopPropagation(); - if ((target as HTMLButtonElement).disabled) return; + if ((diagramConditionsButton as HTMLButtonElement).disabled) return; showDiagramConditions = !showDiagramConditions; updateView(); return; } // zoom in - if (target.id === 'zoom-in-btn') { + if (target.closest?.('#zoom-in-btn')) { e.stopPropagation(); zoomIn(document); return; } // zoom out - if (target.id === 'zoom-out-btn') { + if (target.closest?.('#zoom-out-btn')) { e.stopPropagation(); zoomOut(document); return; } // reset zoom - if (target.id === 'zoom-reset-btn') { + if (target.closest?.('#zoom-reset-btn')) { e.stopPropagation(); resetZoom(document); return; } // copy diagram source - if (target.id === 'copy-diagram-btn') { + const copyDiagramButton = target.closest?.('#copy-diagram-btn'); + if (copyDiagramButton) { e.stopPropagation(); if (!currentDiagram) return - copyDiagramToClipboard(target, currentDiagram); + copyDiagramToClipboard(copyDiagramButton, currentDiagram); return; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 2873aac..b57d4db 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -164,6 +164,16 @@ export function getStyles(): string { border-radius: 4px; position: relative; } + .codicon { + display: inline-flex; + align-items: center; + justify-content: center; + width: 1em; + height: 1em; + font-size: 1rem; + line-height: 1; + pointer-events: none; + } .copy-diagnostic-btn { position: absolute; top: 0.5rem; @@ -179,7 +189,6 @@ export function getStyles(): string { border: 1px solid transparent; border-radius: 4px; opacity: 0.65; - font-size: 1.25rem; transition: background-color 0.16s ease, border-color 0.16s ease, opacity 0.16s ease, transform 0.16s ease; } .copy-diagnostic-btn:hover { @@ -328,14 +337,18 @@ export function getStyles(): string { } .reset-btn { margin: 0; - padding: 0.4rem 0.8rem; + display: inline-flex; + align-items: center; + justify-content: center; + width: 1.75rem; + height: 1.75rem; + padding: 0; background-color: transparent; color: var(--vscode-button-foreground); border: none; border-radius: 4px; cursor: pointer; font-family: var(--vscode-font-family); - font-size: larger; flex-shrink: 0; opacity: 0.7; } @@ -529,7 +542,6 @@ export function getStyles(): string { width: 1rem; text-align: center; flex-shrink: 0; - font-size: larger; } .context-section-content.collapsed { display: none; @@ -609,12 +621,15 @@ export function getStyles(): string { z-index: 10; } .diagram-control-btn { - font-size: clamp(0.75rem, 5vw, 1.5rem); - padding: clamp(0.25rem, 1vw, 0.5rem); + display: inline-flex; + align-items: center; + justify-content: center; + width: 1.75rem; + height: 1.75rem; + padding: 0; color: var(--vscode-foreground); background: none; border: none; - font-family: 'Courier New', Courier, monospace; opacity: 0.7; } .diagram-control-btn:hover { diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts index ca8e8a3..8a75964 100644 --- a/client/src/webview/views/diagnostics/derivation-nodes.ts +++ b/client/src/webview/views/diagnostics/derivation-nodes.ts @@ -1,6 +1,7 @@ import type { LJError, RefinementMismatchError } from "../../../types/diagnostics"; import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; // Handles rendering and interaction of derivation nodes in refinement errors @@ -138,7 +139,7 @@ export function renderDerivationNode( ${renderJsonTree(error, node, errorId, "root", expansions)} ${expansions.size === 0 ? ' (click to expand)' : ''}
- + `; } diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index 8895cdf..ca87b90 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -1,4 +1,5 @@ import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics"; +import { renderCodicon } from "../../icons"; import { renderErrors } from "./errors"; import { renderMainHeader } from "../sections"; import { renderWarnings } from "./warnings"; @@ -51,7 +52,7 @@ export function getDisplayDiagnostics(diagnostics: LJDiagnostic[], showAll: bool } export function renderCopyDiagnosticButton(indexType: 'error' | 'warning', index: number): string { - return /*html*/``; + return /*html*/``; } export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: LJDiagnostic[]) { diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index bf10010..81b1258 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,4 +1,5 @@ import type { LJStateMachine } from "../../../types/fsm"; +import { renderCodicon } from "../../icons"; import { renderMainHeader } from "../sections"; export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean): string { @@ -8,7 +9,6 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: || sm.transitions.some(transition => !!transition.preCond || !!transition.postCond) : false; const conditionToggleLabel = showConditions ? 'Collapse Conditions' : 'Expand Conditions'; - const conditionToggleIcon = showConditions ? '⊟' : '⊞'; return /*html*/`
@@ -17,12 +17,12 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram:
- - - - - - + + + + + + 
${diagram}
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 0ce66fe..9f46036 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -2,6 +2,7 @@ import type { LJDiagnostic, PlacementInCode, SourcePosition, TranslationTable } import { escapeHtml } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; +import { renderCodicon } from "../icons"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -21,7 +22,7 @@ export const renderExpressionSection = (title: string, expression: string): stri export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` `; From 4900e7928e7de9c7a17bdf59a989cb6a5e9d73c1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:30:04 +0100 Subject: [PATCH 07/22] Add Pop Animation to Buttons --- client/src/webview/diagram.ts | 2 -- client/src/webview/icons.ts | 19 +++++++++++++++++++ client/src/webview/script.ts | 6 ++++++ client/src/webview/styles.ts | 12 ++++++------ .../webview/views/diagnostics/diagnostics.ts | 10 ++++++---- client/src/webview/views/fsm/fsm.ts | 14 +++++++------- 6 files changed, 44 insertions(+), 19 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 3cbf58f..2027288 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -245,7 +245,6 @@ export async function copyDiagramToClipboard(target: any, diagram: string) { try { target.disabled = true; await navigator.clipboard.writeText(diagram); - target.classList.add('copied'); target.setAttribute('title', 'Copied!'); } catch (e) { target.setAttribute('title', 'Copy failed'); @@ -253,7 +252,6 @@ export async function copyDiagramToClipboard(target: any, diagram: string) { // reset button after timeout setTimeout(() => { target.setAttribute('title', title); - target.classList.remove('copied'); target.disabled = false; }, COPY_TIMEOUT_MS); } diff --git a/client/src/webview/icons.ts b/client/src/webview/icons.ts index bd82bed..367047b 100644 --- a/client/src/webview/icons.ts +++ b/client/src/webview/icons.ts @@ -2,3 +2,22 @@ export function renderCodicon(name: string, className = ""): string { const classes = ["codicon", `codicon-${name}`, className].filter(Boolean).join(" "); return ``; } + +type CodiconButtonOptions = { + id?: string; + className?: string; + title: string; + ariaLabel?: string; + attributes?: string; + disabled?: boolean; +}; + +export function renderCodiconButton(iconName: string, options: CodiconButtonOptions): string { + const classes = ["icon-button", options.className].filter(Boolean).join(" "); + const id = options.id ? ` id="${options.id}"` : ""; + const ariaLabel = ` aria-label="${options.ariaLabel ?? options.title}"`; + const attributes = options.attributes ? ` ${options.attributes}` : ""; + const disabled = options.disabled ? " disabled" : ""; + + return `${renderCodicon(iconName)}`; +} diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index da67c94..6774c7c 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -51,6 +51,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) root.addEventListener('click', (e: MouseEvent) => { const target = e.target instanceof Element ? e.target : null; if (!target) return; + const iconButton = target.closest?.('.icon-button'); + if (iconButton && !(iconButton as HTMLButtonElement).disabled) { + iconButton.classList.remove('icon-button-pop'); + void (iconButton as HTMLElement).offsetWidth; + iconButton.classList.add('icon-button-pop'); + } // context section toggle const contextToggleButton = target.closest?.('.context-toggle-btn'); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index b57d4db..40460c6 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -200,15 +200,15 @@ export function getStyles(): string { opacity: 0.8; cursor: default; } - .copied { - animation: copy-diagnostic-pop 0.42s ease-out; + .icon-button-pop { + animation: icon-button-pop 0.28s ease-out; } - @keyframes copy-diagnostic-pop { + @keyframes icon-button-pop { 0% { - transform: scale(0.8); + transform: scale(0.96); } - 45% { - transform: scale(1.18); + 55% { + transform: scale(1.05); } 100% { transform: scale(1); diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index ca87b90..8af8634 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -1,5 +1,5 @@ import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics"; -import { renderCodicon } from "../../icons"; +import { renderCodiconButton } from "../../icons"; import { renderErrors } from "./errors"; import { renderMainHeader } from "../sections"; import { renderWarnings } from "./warnings"; @@ -52,7 +52,11 @@ export function getDisplayDiagnostics(diagnostics: LJDiagnostic[], showAll: bool } export function renderCopyDiagnosticButton(indexType: 'error' | 'warning', index: number): string { - return /*html*/``; + return renderCodiconButton("copy", { + className: "copy-diagnostic-btn", + title: "Copy diagnostic", + attributes: `data-${indexType}-index="${index}"`, + }); } export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: LJDiagnostic[]) { @@ -70,7 +74,6 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: try { button.disabled = true; await navigator.clipboard.writeText(diagnosticText); - button.classList.add('copied'); button.setAttribute('title', 'Copied!'); } catch (e) { button.setAttribute('title', 'Copy failed'); @@ -78,7 +81,6 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: setTimeout(() => { button.innerHTML = originalContent; button.setAttribute('title', originalTitle); - button.classList.remove('copied'); button.disabled = false; }, COPY_BUTTON_RESET_MS); } diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 81b1258..f5106b3 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,5 +1,5 @@ import type { LJStateMachine } from "../../../types/fsm"; -import { renderCodicon } from "../../icons"; +import { renderCodiconButton } from "../../icons"; import { renderMainHeader } from "../sections"; export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean): string { @@ -17,12 +17,12 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram:
- - - - - - + ${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} + ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} + ${renderCodiconButton("refresh", { id: "zoom-reset-btn", className: "diagram-control-btn", title: "Reset Zoom" })} + ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Rotate Diagram" })} + ${renderCodiconButton(showConditions ? "collapse-all" : "expand-all", { id: "diagram-conditions-btn", className: `diagram-control-btn${showConditions ? ' active' : ''}`, title: conditionToggleLabel, attributes: `aria-pressed="${showConditions ? 'true' : 'false'}"`, disabled: !hasConditionExpansions })} + ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })} 
${diagram}
From 1abe19be3de5545a3bb9feb11ee79529bf0339ef Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:31:30 +0100 Subject: [PATCH 08/22] Refactor Copy to Clipboard Logic --- client/src/webview/clipboard.ts | 22 +++++++++++++++++++ client/src/webview/diagram.ts | 17 ++------------ .../webview/views/diagnostics/diagnostics.ts | 20 ++--------------- 3 files changed, 26 insertions(+), 33 deletions(-) create mode 100644 client/src/webview/clipboard.ts diff --git a/client/src/webview/clipboard.ts b/client/src/webview/clipboard.ts new file mode 100644 index 0000000..8a40025 --- /dev/null +++ b/client/src/webview/clipboard.ts @@ -0,0 +1,22 @@ +const COPY_BUTTON_RESET_MS = 2000; + +export async function copyToClipboard(button: HTMLButtonElement, text: string) { + const originalTitle = button.getAttribute('title'); + + try { + button.disabled = true; + await navigator.clipboard.writeText(text); + button.setAttribute('title', 'Copied!'); + } catch (e) { + button.setAttribute('title', 'Copy failed'); + } finally { + setTimeout(() => { + if (originalTitle !== null) { + button.setAttribute('title', originalTitle); + } else { + button.removeAttribute('title'); + } + button.disabled = false; + }, COPY_BUTTON_RESET_MS); + } +} diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 2027288..b2a27d1 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -1,4 +1,5 @@ import type { LJStateMachine } from "../types/fsm"; +import { copyToClipboard } from "./clipboard"; // constants const MIN_ZOOM = 0.2; @@ -6,7 +7,6 @@ const MAX_ZOOM = 5; const ZOOM_BUTTON_FACTOR = 1.5; const SCROLL_ZOOM_IN_FACTOR = 1.05; const SCROLL_ZOOM_OUT_FACTOR = 0.95; -const COPY_TIMEOUT_MS = 2000; // state variables let zoomLevel = 1; @@ -241,18 +241,5 @@ export function registerPanListeners(document: any) { } export async function copyDiagramToClipboard(target: any, diagram: string) { - const title = target.getAttribute('title'); - try { - target.disabled = true; - await navigator.clipboard.writeText(diagram); - target.setAttribute('title', 'Copied!'); - } catch (e) { - target.setAttribute('title', 'Copy failed'); - } finally { - // reset button after timeout - setTimeout(() => { - target.setAttribute('title', title); - target.disabled = false; - }, COPY_TIMEOUT_MS); - } + await copyToClipboard(target, diagram); } diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index 8af8634..f0b4232 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -1,11 +1,10 @@ import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics"; +import { copyToClipboard } from "../../clipboard"; import { renderCodiconButton } from "../../icons"; import { renderErrors } from "./errors"; import { renderMainHeader } from "../sections"; import { renderWarnings } from "./warnings"; -const COPY_BUTTON_RESET_MS = 2000; - export function renderDiagnosticsView( diagnostics: LJDiagnostic[], showAll: boolean, @@ -68,22 +67,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: if (!diagnostic) return; const diagnosticText = formatDiagnosticForClipboard(diagnostic); - const originalTitle = button.getAttribute('title'); - const originalContent = button.innerHTML; - - try { - button.disabled = true; - await navigator.clipboard.writeText(diagnosticText); - button.setAttribute('title', 'Copied!'); - } catch (e) { - button.setAttribute('title', 'Copy failed'); - } finally { - setTimeout(() => { - button.innerHTML = originalContent; - button.setAttribute('title', originalTitle); - button.disabled = false; - }, COPY_BUTTON_RESET_MS); - } + await copyToClipboard(button, diagnosticText); } export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string { From 6902d25005baea836fe0d7c09c0a4abb46784b97 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:34:45 +0100 Subject: [PATCH 09/22] Update Chevron Icons --- client/src/webview/script.ts | 4 ++-- client/src/webview/views/sections.ts | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 6774c7c..5155713 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -80,8 +80,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const icon = contextToggleButton.querySelector('.context-toggle-icon'); if (icon) { - icon.classList.toggle('codicon-chevron-down', nextExpanded); - icon.classList.toggle('codicon-chevron-right', !nextExpanded); + icon.classList.toggle('codicon-triangle-down', nextExpanded); + icon.classList.toggle('codicon-triangle-right', !nextExpanded); } return; diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 9f46036..3b13934 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -22,7 +22,7 @@ export const renderExpressionSection = (title: string, expression: string): stri export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` `; From 247d03ce24137d48dff1938db799a6f6e679a0d9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:52:35 +0100 Subject: [PATCH 10/22] 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 { From 5fe7418ed93e95260e9043bac2f3a1924158c29c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 19 May 2026 23:53:08 +0100 Subject: [PATCH 11/22] 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 b2a27d1..ebb4351 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 { From 04289e821164099fcbd84d5e45b2e6b24bebc33e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 11:59:46 +0100 Subject: [PATCH 12/22] Fix Diagram Rendering --- client/src/webview/diagram.ts | 2 ++ client/src/webview/script.ts | 2 +- client/src/webview/views/fsm/fsm.ts | 10 ++++++++-- 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index ebb4351..9154c17 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -101,6 +101,8 @@ export async function renderMermaidDiagram(document: any, window: any) { await mermaid.run({ nodes: mermaidElements }); applyTransform(document); registerPanListeners(document); + const diagramContainer = document.querySelector('.diagram-container') as HTMLElement | null; + if (diagramContainer) diagramContainer.style.minHeight = ''; } catch (e) { console.error('Failed to render Mermaid diagram:', e); } diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 5155713..80aeee2 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -304,7 +304,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) case 'fsm': { const diagram = createMermaidDiagram(stateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; - root.innerHTML = renderStateMachineView(stateMachine, diagram, diagramOrientation, showDiagramConditions); + renderStateMachineView(root, stateMachine, diagram, diagramOrientation, showDiagramConditions); if (stateMachine) renderMermaidDiagram(document, window); break; } diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index f5106b3..a920dc3 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -2,7 +2,13 @@ import type { LJStateMachine } from "../../../types/fsm"; import { renderCodiconButton } from "../../icons"; import { renderMainHeader } from "../sections"; -export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean): string { +export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean) { + const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; + const diagramHeight = previousDiagramContainer?.offsetHeight; + root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight); +} + +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number): string { const initialStateNames = sm ? [...new Set(sm.initialTransitions.map(transition => transition.to))] : []; const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.postCond) @@ -15,7 +21,7 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: ${renderMainHeader("", 'fsm')} ${sm ? /*html*/`
-
+
${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} From 5ef7e280237ccd4b41fe889b670a14f5e38bb5da Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 13:54:41 +0100 Subject: [PATCH 13/22] Minor Change --- client/src/webview/script.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 80aeee2..71a9728 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -279,7 +279,6 @@ 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': From 7f4546a9e3dc4613eb5f1c5c78ba0bebaa16a3d3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 13:58:00 +0100 Subject: [PATCH 14/22] Minor Change --- client/src/webview/styles.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 40460c6..12c15bb 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -673,7 +673,7 @@ export function getStyles(): string { .diagram-container .mermaid .edgeLabel .state-cond { color: var(--vscode-descriptionForeground) !important; display: inline-block !important; - font-size: 0.82em !important; + font-size: 0.76em !important; line-height: 1.2 !important; } .diagram-container .mermaid .edgeLabel .state-cond-pre { From 942a8562de5345cba6f99b9890100b80c3464938 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:01:11 +0100 Subject: [PATCH 15/22] Minor Fix --- client/src/webview/diagram.ts | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 9154c17..5683c02 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -51,7 +51,7 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation // add transitions transitionMap.forEach((labels, key) => { const [from, to] = key.split('|'); - const mergedLabel = labels.join(', '); + const mergedLabel = labels.join('
'); lines.push(` ${from} --> ${to} : ${mergedLabel}`); }); @@ -59,10 +59,7 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation } function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null, showConditions = false): string { - if (!showConditions) { - return escapeMermaidLabel(label); - } - + if (!showConditions) return escapeMermaidLabel(label); return [ getConditionLabel('pre', preCond), escapeMermaidLabel(label), @@ -75,9 +72,8 @@ function getInitialTransitionLabel(postCond?: string | null, showConditions = fa } function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string { - if (!cond) { - return ''; - } + if (!cond) return ''; + return `${escapeMermaidLabel(cond)}`; } From 10614b6bff1aa7f46fbe10ffd59cecacf8d3228f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:02:55 +0100 Subject: [PATCH 16/22] Minor Fix --- client/src/webview/styles.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 12c15bb..3fb8362 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -614,8 +614,8 @@ export function getStyles(): string { } .diagram-controls { position: absolute; - top: 0.5rem; - right: 0.5rem; + top: 1rem; + right: 1rem; display: flex; gap: 0.5rem; z-index: 10; From c47b4c604e53d9f215660da7ec32c2e354fc36f2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:08:52 +0100 Subject: [PATCH 17/22] Add Legend --- client/src/webview/styles.ts | 17 +++++++++++++++++ client/src/webview/views/fsm/fsm.ts | 6 ++++++ 2 files changed, 23 insertions(+) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 3fb8362..1016641 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -620,6 +620,23 @@ export function getStyles(): string { gap: 0.5rem; z-index: 10; } + .diagram-condition-legend { + position: absolute; + bottom: 1rem; + right: 1rem; + display: flex; + flex-direction: column; + gap: 0.25rem; + font-size: 0.8rem; + z-index: 10; + pointer-events: none; + } + .diagram-condition-legend-pre { + color: var(--lj-state-cond-pre); + } + .diagram-condition-legend-post { + color: var(--lj-state-cond-post); + } .diagram-control-btn { display: inline-flex; align-items: center; diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index a920dc3..522fb2f 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -30,6 +30,12 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton(showConditions ? "collapse-all" : "expand-all", { id: "diagram-conditions-btn", className: `diagram-control-btn${showConditions ? ' active' : ''}`, title: conditionToggleLabel, attributes: `aria-pressed="${showConditions ? 'true' : 'false'}"`, disabled: !hasConditionExpansions })} ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
+ ${showConditions && hasConditionExpansions ? /*html*/` +
+ Precondition + Postcondition +
+ ` : ''} 
${diagram}
From 5f94154c55159a459adcdf77f4aa12999f81a9e4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:18:21 +0100 Subject: [PATCH 18/22] Update Icon --- client/src/webview/views/fsm/fsm.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 522fb2f..88c4e6a 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -25,8 +25,8 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} - ${renderCodiconButton("refresh", { id: "zoom-reset-btn", className: "diagram-control-btn", title: "Reset Zoom" })} - ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Rotate Diagram" })} + ${renderCodiconButton("screen-normal", { id: "zoom-reset-btn", className: "diagram-control-btn", title: "Reset Zoom" })} + ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Diagram Orientation" })} ${renderCodiconButton(showConditions ? "collapse-all" : "expand-all", { id: "diagram-conditions-btn", className: `diagram-control-btn${showConditions ? ' active' : ''}`, title: conditionToggleLabel, attributes: `aria-pressed="${showConditions ? 'true' : 'false'}"`, disabled: !hasConditionExpansions })} ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
From e11e5233442a9cb5b895d5c67eed8dd1e397b5bd Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:20:23 +0100 Subject: [PATCH 19/22] Minor Change --- client/src/webview/views/fsm/fsm.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 88c4e6a..3080baa 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -26,7 +26,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} ${renderCodiconButton("screen-normal", { id: "zoom-reset-btn", className: "diagram-control-btn", title: "Reset Zoom" })} - ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Diagram Orientation" })} + ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Toggle Orientation" })} ${renderCodiconButton(showConditions ? "collapse-all" : "expand-all", { id: "diagram-conditions-btn", className: `diagram-control-btn${showConditions ? ' active' : ''}`, title: conditionToggleLabel, attributes: `aria-pressed="${showConditions ? 'true' : 'false'}"`, disabled: !hasConditionExpansions })} ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
From 5c07ed50d64711ad4788ab846c5734b67284204b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:31:06 +0100 Subject: [PATCH 20/22] Minor Change --- client/src/webview/styles.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 1016641..4460777 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -630,6 +630,7 @@ export function getStyles(): string { font-size: 0.8rem; z-index: 10; pointer-events: none; + font-weight: 500; } .diagram-condition-legend-pre { color: var(--lj-state-cond-pre); From 60dc711868b36a5dc1fae146560ac037c4b088db Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 14:55:37 +0100 Subject: [PATCH 21/22] Minor Fix --- client/src/webview/styles.ts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 4460777..c3aa58b 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -11,6 +11,7 @@ export function getStyles(): string { height: 100%; margin: 0; box-sizing: border-box; + scrollbar-gutter: stable both-edges; } #root { width: 100%; @@ -27,7 +28,8 @@ export function getStyles(): string { height: 100%; padding: 1rem; font-family: var(--vscode-font-family); - overflow: auto; + overflow-x: hidden; + overflow-y: auto; --lj-token-keyword: var(--vscode-symbolIcon-keywordForeground, var(--vscode-editor-foreground)); --lj-token-control: var(--vscode-debugTokenExpression-name, var(--vscode-symbolIcon-keywordForeground, var(--vscode-editor-foreground))); --lj-token-function: var(--vscode-symbolIcon-functionForeground, var(--vscode-editor-foreground)); From 2a52f26674812f8c3f5dff288951e2929fb4b465 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 20 May 2026 15:16:54 +0100 Subject: [PATCH 22/22] Update Color --- client/src/webview/styles.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index c3aa58b..215c0bd 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -40,7 +40,7 @@ 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-pre: var(--lj-token-identifier); --lj-state-cond-post: var(--lj-token-type); } body.vscode-light {