Choreo FSM: Comprehensive Walkthrough

Mix.install([
  # For Hex publication/readers:
  # {:choreo, "~> 0.12.0"},
  # 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.

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)": Kino.Mermaid.new(FSM.to_mermaid(fsm)),
  "Mermaid (State Diagram)": Kino.Mermaid.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": Kino.Mermaid.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": Kino.Mermaid.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": Kino.Mermaid.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": Kino.Mermaid.new(FSM.to_mermaid(order_flow, theme: :dark)),
  "Graphviz": Kino.VizJS.render(FSM.to_dot(order_flow, theme: :dark))
])

Summary