Choreo FSM: Comprehensive Walkthrough

Mix.install([
  # For Hex publication/readers:
  {:choreo, "~> 0.14.1"},
  # For local development:
  # {:choreo, path: Path.expand("../..", __DIR__), force: true},
  {:kino_vizjs, "~> 0.9.0"}
])

Introduction

Choreo.FSM is a finite-state machine builder that supports deterministic finite automata (DFAs). You define states, transitions, and analyse reachability, acceptance, and more. Everything renders to DOT or Mermaid.js for visualisation.

API Approaches: Programmatic Pipe API vs Lab DSL

Choreo provides two complementary approaches to modeling finite-state machines:

1. Programmatic Pipe API (Choreo.FSM): The canonical, explicit interface (FSM.new() |> FSM.add_initial_state(...) |> FSM.add_state(...) |> FSM.add_transition(...)). Ideal for automated protocol ingestion, parser generators, and strict programmatic automata validation.
2. Lab DSL (Choreo.Lab.DSL.FSM): An expressive sketch syntax using fsm do ... end, state constructors (initial, state, final), direct transition arrows (~>), and transition modifiers (|> on("event"), |> guard("condition")). Ideal for Livebooks, design reviews, and rapid statechart sketching.

alias Choreo.FSM
alias Choreo.FSM.Analysis
import Choreo.Lab.DSL.FSM

fsm =
  fsm do
    idle = initial("Idle")
    authenticating = state("Authenticating")
    logged_in = final("Logged In")

    idle ~> authenticating |> on("submit_credentials")
    authenticating ~> logged_in |> on("success")
  end

# Render diagrams (Mermaid is preferred as primary tab)
Kino.Layout.tabs([
  "Mermaid (Flowchart)": Choreo.Lab.Siren.new(FSM.to_mermaid(fsm)),
  "Mermaid (State Diagram)": Choreo.Lab.Siren.new(FSM.to_mermaid(fsm, syntax: :state_diagram)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(fsm))
])

State Types

There are three ways to add states. Each stores type information in the FSM's meta field, so analysis and rendering always stay in sync.

You can also remove a special status without deleting the state:

# Promote with the DSL, then demote with the explicit API
fsm =
  fsm do
    initial(:a)
  end

IO.inspect(FSM.initial_state(fsm), label: "Initial state ID")

fsm = FSM.remove_initial_state(fsm, :a)
IO.inspect(FSM.initial_state(fsm), label: "Initial state ID after removal")

A state can be both initial and final

This is useful for modelling "already accepted" start conditions (e.g. an empty string match).

empty_match =
  fsm do
    q0 = initial(:q0)
    final(:q0)

    q0 ~> q0 |> on("a")
  end

Kino.Layout.tabs([
  "Mermaid": Choreo.Lab.Siren.new(FSM.to_mermaid(empty_match)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(empty_match))
])

Building Larger Graphs

order_flow =
  fsm do
    cart_created = initial("Cart Created")
    checkout = state("Checkout")
    payment_pending = state("Payment Pending")
    fraud_check = state("Fraud Check")
    order_shipped = final("Order Shipped")
    cancelled = final("Cancelled")

    cart_created ~> checkout |> on("proceed")
    checkout ~> payment_pending |> on("pay")
    payment_pending ~> fraud_check |> on("authorized")
    fraud_check ~> order_shipped |> on("passed")
    payment_pending ~> cancelled |> on("declined")
  end

Kino.Layout.tabs(
  Siren: Choreo.Lab.Siren.new(FSM.to_mermaid(order_flow)),
  Graphviz: Kino.VizJS.render(FSM.to_dot(order_flow)),
  Sketch: Choreo.Lab.Sketch.new(FSM.to_mermaid(order_flow))
)

Determinism

An FSM is deterministic when two conditions hold:

1. Exactly one initial state.
2. No state has two outgoing transitions with the same label.

Choreo.FSM guarantees determinism at build-time by raising errors if these constraints are violated.

# Let's see what happens if we attempt to add duplicate outgoing transition labels:
try do
  fsm do
    q0 = initial(:q0)
    q1 = state(:q1)
    q2 = state(:q2)

    q0 ~> q1 |> on("x")
    q0 ~> q2 |> on("x")
  end
rescue
  e in ArgumentError -> e.message
end

# Or if we attempt to define a second initial state:
try do
  fsm do
    initial(:q0)
    initial(:q1)
  end
rescue
  e in ArgumentError -> e.message
end

We can build a valid DFA safely:

dfa =
  fsm do
    q0 = initial(:q0)
    q1 = state(:q1)
    q2 = final(:q2)

    q0 ~> q1 |> on("a")
    q1 ~> q2 |> on("b")
  end

Analysis

Reachability & Dead States

IO.inspect(Analysis.reachable_states(order_flow), label: "Reachable")
IO.inspect(Analysis.dead_states(order_flow), label: "Dead (trap) states")

Acceptance

IO.inspect(Analysis.accepts?(order_flow, ["proceed", "pay", "authorized", "passed"]), label: "Accepts happy path")
IO.inspect(Analysis.accepts?(order_flow, ["proceed", "pay", "declined"]), label: "Accepts cancelled path")
IO.inspect(Analysis.accepts?(order_flow, ["proceed"]), label: "Rejects incomplete path")

Path Finding & accepted_strings/2

For branching FSMs, Analysis.accepted_strings/2 computes all valid paths up to a specified length:

branching_fsm =
  fsm do
    q0 = initial(:q0)
    q1 = final(:q1)

    q0 ~> q0 |> on("0")
    q0 ~> q1 |> on("1")
    q1 ~> q1 |> on("0")
  end

IO.inspect(Analysis.shortest_accepting_path(order_flow), label: "Shortest accepting path (order_flow)")
IO.inspect(Analysis.accepted_strings(branching_fsm, 3), label: "Accepted strings up to length 3 (branching)")

Alphabet & Completeness

IO.inspect(Analysis.alphabet(order_flow), label: "Alphabet")
IO.inspect(Analysis.complete?(order_flow), label: "Complete?")

Validation

validate/1 returns a list of structural warnings/errors found in the FSM (such as unreachable states, trap/dead states, or incompleteness).

Note that state_diagram syntax does not show orphan states.

incomplete_fsm =
  fsm do
    state(:orphan)
    state(:trap)
    a = initial(:a)
    c = final(:c)

    a ~> c |> on("x") |> guard("ready")
    a ~> c |> on("y")
  end

Analysis.validate(incomplete_fsm)
|> Enum.each(fn {severity, msg} ->
  IO.puts("[#{severity}] #{msg}")
end)

Kino.Layout.tabs(
  Siren: Choreo.Lab.Siren.new(FSM.to_mermaid(incomplete_fsm)),
  Graphviz: Kino.VizJS.render(FSM.to_dot(incomplete_fsm)),
  Sketch: Choreo.Lab.Sketch.new(FSM.to_mermaid(incomplete_fsm))
)

Transforms

Complement

Swap final and non-final states.

comp = FSM.complement(dfa)

IO.inspect(FSM.final_states(comp), label: "Final states in complement")

Kino.Layout.tabs([
  "Mermaid": Choreo.Lab.Siren.new(FSM.to_mermaid(comp)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(comp))
])

Prune

Remove unreachable states and dead (trap) states, producing a smaller equivalent FSM.

pruned = FSM.prune(incomplete_fsm)

IO.inspect(FSM.states(pruned), label: "States after pruning")

Kino.Layout.tabs([
  "Mermaid": Choreo.Lab.Siren.new(FSM.to_mermaid(pruned)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(pruned))
])

Theming

Render with the built-in :dark theme or a custom Choreo.Theme.

Kino.Layout.tabs([
  "Mermaid": Choreo.Lab.Siren.new(FSM.to_mermaid(order_flow, theme: :dark)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(order_flow, theme: :dark))
])

Cheat Sheet

Lab DSL Syntax (Choreo.Lab.DSL.FSM)

Programmatic Pipe API & Analysis (Choreo.FSM)

Summary