diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts
index e8f1a96..1385fe6 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; postCond?: string | null }[];
     states: string[];
-    transitions: { from: string; to: string; label: string }[];
+    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 a3574cd..19c6a7e 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[] = [];
@@ -33,17 +33,19 @@ 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.postCond, showConditions);
+        lines.push(`    [*] --> ${transition.to}${label ? ` : ${label}` : ''}`);
     });
     
     // group transitions by from/to states and merge labels
     const transitionMap = new Map<string, string[]>();
     sm.transitions.forEach(transition => {
+        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(transition.label);
+        transitionMap.get(key)?.push(label);
     });
 
     // add transitions
@@ -56,6 +58,33 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation
     return lines.join('\n');
 }
 
+function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null, showConditions = false): string {
+    if (!showConditions) {
+        return escapeMermaidLabel(label);
+    }
+
+    return [
+        getConditionLabel('pre', preCond),
+        escapeMermaidLabel(label),
+        getConditionLabel('post', postCond)
+    ].filter(Boolean).join('<br/>');
+}
+
+function getInitialTransitionLabel(postCond?: string | null, showConditions = false): string {
+    return showConditions ? getConditionLabel('post', postCond) : '';
+}
+
+function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string {
+    if (!cond) {
+        return '';
+    }
+    return `<span class="state-cond state-cond-${kind}">${escapeMermaidLabel(cond)}</span>`;
+}
+
+function escapeMermaidLabel(label: string): string {
+    return label.replace(/&/g, '&amp;').replace(/"/g, '\\"').replace(/</g, '&lt;').replace(/>/g, '&gt;');
+}
+
 /**
  * Renders Mermaid diagrams in the document
  * @param document The document object
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<typeof setTimeout> | 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 92b8139..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;
@@ -619,9 +621,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;
@@ -650,6 +655,18 @@ 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;
+            display: inline-block !important;
+            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,
diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts
index 1a5996c..bf10010 100644
--- a/client/src/webview/views/fsm/fsm.ts
+++ b/client/src/webview/views/fsm/fsm.ts
@@ -1,7 +1,15 @@
 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*/`
         <div>
             ${renderMainHeader("", 'fsm')}
@@ -13,6 +21,7 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram:
                             <button id="zoom-out-btn" class="diagram-control-btn" title="Zoom Out">-</button>
                             <button id="zoom-reset-btn" class="diagram-control-btn" title="Reset Zoom">⟲</button>
                             <button id="diagram-orientation-btn" class="diagram-control-btn" title="Rotate Diagram">${orientation === "TB" ? "↓" : "→"}</button>
+                            <button id="diagram-conditions-btn" class="diagram-control-btn${showConditions ? ' active' : ''}" title="${conditionToggleLabel}" aria-label="${conditionToggleLabel}" aria-pressed="${showConditions ? 'true' : 'false'}" ${hasConditionExpansions ? '' : 'disabled'}>${conditionToggleIcon}</button>
                             <button id="copy-diagram-btn" class="diagram-control-btn" title="Copy Mermaid Source">⎘</button>
                         </div>
                         <div id="diagram-wrapper" class="diagram-wrapper">
@@ -21,9 +30,9 @@ export function renderStateMachineView(sm: LJStateMachine | undefined, diagram:
                     </div>
                     <div>
                         <p><strong>States:</strong> ${sm.states.join(', ')}</p>
-                        <p><strong>Initial state${sm.initialStates.length > 1 ? 's' : ''}:</strong> ${sm.initialStates.join(', ')}</p>
+                        <p><strong>Initial state${initialStateNames.length > 1 ? 's' : ''}:</strong> ${initialStateNames.join(', ')}</p>
                         <p><strong>Number of states:</strong> ${sm.states.length}</p>
-                        <p><strong>Number of transitions:</strong> ${sm.transitions.length + 1}</p>
+                        <p><strong>Number of transitions:</strong> ${sm.transitions.length + sm.initialTransitions.length}</p>
                     </div>
                 </div>`
             : '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<String> initialStates,
     List<String> states,
-    List<StateMachineTransition> transitions
+    List<StateMachineTransition> transitions,
+    List<StateMachineInitialTransition> 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..23a9b9c
--- /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 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 628a0e5..a8c6a9e 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;
@@ -24,6 +22,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
@@ -50,13 +50,16 @@ public static StateMachine parse(String uri) {
                 return null; // no states found
             String className = getClassName(ctType);
 
-            // get initial states and transitions
-            List<String> initialStates = getInitialStates(ctType, className, states);
+            // get initial transitions and method transitions
+            List<StateMachineInitialTransition> initialTransitions = getInitialTransitions(ctType, className, states);
+            if (initialTransitions.isEmpty()) {
+                initialTransitions = List.of(new StateMachineInitialTransition(states.get(0)));
+            }
             List<StateMachineTransition> 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();
@@ -123,25 +126,24 @@ private static Collection<? extends CtElement> 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<String> getInitialStates(CtType<?> ctType, String className, List<String> states) {
-        Set<String> initialStates = new HashSet<>();
+    private static List<StateMachineInitialTransition> getInitialTransitions(CtType<?> ctType, String className, List<String> states) {
+        List<StateMachineInitialTransition> 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<String> 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;
     }
 
     /**
@@ -180,39 +182,180 @@ private static List<StateMachineTransition> 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<TransitionSource> fromSources = from.isEmpty() ? allStateSources(states) : parsePrecondition(from, states);
+        List<TransitionSource> 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 (TransitionSource toSource : toSources) {
+                transitions.add(new StateMachineTransition(fromSource.from(), toSource.from(), method, fromSource.cond(), toSource.cond()));
+            }
         }
+        return transitions;
+    }
 
-        // parse from and to expressions
-        List<String> fromStates = parseStateExpression(from, states);
-        List<String> toStates = parseStateExpression(to, states);
+    private static List<TransitionSource> allStateSources(List<String> states) {
+        List<TransitionSource> sources = new ArrayList<>();
+        for (String state : states) {
+            sources.add(new TransitionSource(state, null));
+        }
+        return sources;
+    }
 
-        // if no from states, use all states
-        if (fromStates.isEmpty()) {
-            fromStates = new ArrayList<>(states);
+    private static List<TransitionSource> parsePrecondition(String expr, List<String> states) {
+        Expression ast = RefinementsParser.createAST(expr, "");
+        List<TransitionSource> sources = getTransitionSources(ast, states, false);
+        if (sources.isEmpty()) {
+            sources = addCondition(allStateSources(states), ast.toString());
         }
+        return sources;
+    }
 
-        // create transitions for each combination of from and to states
-        for (String fromState : fromStates) {
-            for (String toState : toStates) {
-                transitions.add(new StateMachineTransition(fromState, toState, method));
+    private static List<TransitionSource> parsePostcondition(String expr, List<String> states) {
+        if (expr == null || expr.isEmpty()) return new ArrayList<>();
+        Expression ast = RefinementsParser.createAST(expr, "");
+        return getTransitionSources(ast, states, true);
+    }
+
+    private static List<TransitionSource> getTransitionSources(Expression expr, List<String> states, boolean stateOnlyDisjunctions) {
+        String state = getStateName(expr, states);
+        if (state != null) {
+            return List.of(new TransitionSource(state, null));
+        }
+
+        if (expr instanceof GroupExpression group) {
+            return getTransitionSources(group.getExpression(), states, stateOnlyDisjunctions);
+        } else if (expr instanceof BinaryExpression bin) {
+            String op = bin.getOperator();
+            if (op.equals("&&")) {
+                return getConjunctionSources(bin, states, stateOnlyDisjunctions);
+            } else if (op.equals("||")) {
+                return stateOnlyDisjunctions ? getStateSources(bin, states) : getDisjunctionSources(bin, states);
             }
+        } else if (expr instanceof UnaryExpression unary) {
+            if (unary.getOp().equals("!")) {
+                List<String> negatedStates = getStateExpressions(unary.getExpression(), states);
+                if (!negatedStates.isEmpty()) {
+                    List<TransitionSource> 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<TransitionSource> sources = new ArrayList<>();
+            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 transitions;
+        return new ArrayList<>();
     }
 
-    /**
-     * Parses a state expression and returns the list of states
-     * @param expr the expression
-     * @param states the list of possible states
-     * @return list of states
-     */
-    private static List<String> parseStateExpression(String expr, List<String> states) {
+    private static List<TransitionSource> getConjunctionSources(BinaryExpression bin, List<String> states, boolean stateOnlyDisjunctions) {
+        List<TransitionSource> leftSources = getTransitionSources(bin.getFirstOperand(), states, stateOnlyDisjunctions);
+        List<TransitionSource> rightSources = getTransitionSources(bin.getSecondOperand(), states, stateOnlyDisjunctions);
+
+        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<TransitionSource> sources = new ArrayList<>(leftSources);
+        sources.addAll(rightSources);
+        return sources;
+    }
+
+    private static List<TransitionSource> getDisjunctionSources(BinaryExpression bin, List<String> states) {
+        List<TransitionSource> sources = new ArrayList<>();
+        addDisjunctionBranch(sources, bin.getFirstOperand(), states);
+        addDisjunctionBranch(sources, bin.getSecondOperand(), states);
+        return removeRedundantGuardedSources(sources);
+    }
+
+    private static void addDisjunctionBranch(List<TransitionSource> sources, Expression expr, List<String> states) {
+        List<TransitionSource> parsedSources = getTransitionSources(expr, states, false);
+        if (parsedSources.isEmpty()) {
+            sources.addAll(addCondition(allStateSources(states), expr.toString()));
+        } else {
+            sources.addAll(parsedSources);
+        }
+    }
+
+    private static List<TransitionSource> removeRedundantGuardedSources(List<TransitionSource> sources) {
+        List<TransitionSource> 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<TransitionSource> sources, String from) {
+        for (TransitionSource source : sources) {
+            if (source.from().equals(from) && source.cond() == null) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    private static List<TransitionSource> addCondition(List<TransitionSource> sources, String cond) {
+        List<TransitionSource> 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 + ")";
+    }
+
+    private static List<StateMachineInitialTransition> parseInitialTransitions(String expr, List<String> states) {
+        if (expr == null || expr.isEmpty()) return new ArrayList<>();
+        List<StateMachineInitialTransition> initialTransitions = new ArrayList<>();
+        for (TransitionSource source : parsePostcondition(expr, states)) {
+            initialTransitions.add(new StateMachineInitialTransition(source.from(), source.cond()));
+        }
+        return initialTransitions;
+    }
+
+    private static List<TransitionSource> parseStateSources(String expr, List<String> states) {
         if (expr == null || expr.isEmpty()) return new ArrayList<>();
         Expression ast = RefinementsParser.createAST(expr, "");
-        return getStateExpressions(ast, states);
+        return getStateSources(ast, states);
+    }
+
+    private static List<TransitionSource> getStateSources(Expression expr, List<String> states) {
+        List<TransitionSource> sources = new ArrayList<>();
+        for (String state : getStateExpressions(expr, states)) {
+            sources.add(new TransitionSource(state, null));
+        }
+        return sources;
     }
 
     /**
@@ -223,35 +366,53 @@ private static List<String> parseStateExpression(String expr, List<String> state
      */
     private static List<String> getStateExpressions(Expression expr, List<String> states) {
         List<String> 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<String> 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<String> 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<String> 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..33f0f58 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 preCond, String postCond) {
+
+    public StateMachineTransition(String from, String to, String label) {
+        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 daad9c4..08e97e2 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,16 +91,103 @@ 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", "closed"),
+                List.of(new StateMachineTransition("open", "closed", "close", "flag", null)),
+                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", "waiting", "done"),
+                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);
+    }
+
+    @Test
+    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", null),
+                        new StateMachineTransition("right", "done", "finish", "!flag", null)),
+                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", "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");
-        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/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/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/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() {}
+}
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/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/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/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) {}
+}
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) {}
+}