Choreo FSM: Comprehensive Walkthrough

Mix.install([
  # For Hex publication/readers:
  # {:choreo, "~> 0.9"},
  # For local development:
  {:choreo, path: Path.expand("~/repos/elixir/choreo")},
  {:kino_vizjs, "~> 0.8.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

fsm =
  FSM.new()
  |> FSM.add_initial_state(:idle)
  |> FSM.add_state(:authenticating)
  |> FSM.add_final_state(:logged_in)
  |> FSM.add_transition(:idle, :authenticating, label: "submit_credentials")
  |> FSM.add_transition(:authenticating, :logged_in, label: "success")

# 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 and demote
fsm = FSM.new() |> FSM.add_state(:a, type: :initial)
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.new()
  |> FSM.add_initial_state(:q0)
  |> FSM.add_final_state(:q0)
  |> FSM.add_transition(:q0, :q0, label: "a")

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.new()
  |> FSM.add_initial_state(:cart_created)
  |> FSM.add_state(:checkout)
  |> FSM.add_state(:payment_pending)
  |> FSM.add_state(:fraud_check)
  |> FSM.add_final_state(:order_shipped)
  |> FSM.add_final_state(:cancelled)
  |> FSM.add_transition(:cart_created, :checkout, label: "proceed")
  |> FSM.add_transition(:checkout, :payment_pending, label: "pay")
  |> FSM.add_transition(:payment_pending, :fraud_check, label: "authorized")
  |> FSM.add_transition(:fraud_check, :order_shipped, label: "passed")
  |> FSM.add_transition(:payment_pending, :cancelled, label: "declined")

Kino.Layout.tabs(
  Mermaid: Kino.Mermaid.new(FSM.to_mermaid(order_flow)),
  "Mermaid (State Diagram)": Kino.Mermaid.new(FSM.to_mermaid(order_flow, syntax: :state_diagram)),
  Graphviz: Kino.VizJS.render(FSM.to_dot(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.new()
  |> FSM.add_initial_state(:q0)
  |> FSM.add_state(:q1)
  |> FSM.add_state(:q2)
  |> FSM.add_transition(:q0, :q1, label: "x")
  |> FSM.add_transition(:q0, :q2, label: "x")
rescue
  e in ArgumentError -> e.message
end

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

We can build a valid DFA safely:

dfa =
  FSM.new()
  |> FSM.add_initial_state(:q0)
  |> FSM.add_state(:q1)
  |> FSM.add_final_state(:q2)
  |> FSM.add_transition(:q0, :q1, label: "a")
  |> FSM.add_transition(:q1, :q2, label: "b")

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.new()
  |> FSM.add_initial_state(:q0)
  |> FSM.add_final_state(:q1)
  |> FSM.add_transition(:q0, :q0, label: "0")
  |> FSM.add_transition(:q0, :q1, label: "1")
  |> FSM.add_transition(:q1, :q1, label: "0")

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.new()
  |> FSM.add_state(:orphan)
  |> FSM.add_state(:trap)
  |> FSM.add_initial_state(:a)
  |> FSM.add_final_state(:c)
  |> FSM.add_transition(:a, :c, label: "x", guard: "ready")
  |> FSM.add_transition(:a, :c, label: "y")

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

Kino.Layout.tabs(
  Mermaid: Kino.Mermaid.new(FSM.to_mermaid(incomplete_fsm)),
  "Mermaid (State Diagram)":
    Kino.Mermaid.new(FSM.to_mermaid(incomplete_fsm, syntax: :state_diagram)),
  Graphviz: Kino.VizJS.render(FSM.to_dot(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