Choreo FSM: Comprehensive Walkthrough

Mix.install([
  {:choreo, github: "code-shoily/choreo", branch: "main"},
  {:kino_vizjs, "~> 0.8"}
])

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 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")

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(:a in FSM.initial_states(fsm), label: "Is :a initial?")

fsm = FSM.remove_initial_state(fsm, :a)
IO.inspect(:a in FSM.initial_states(fsm), label: "Is :a initial 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.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.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 ensures validation tools help track structural determinism.

# Deterministic — single start, unique labels per state
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.deterministic?(dfa)

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

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

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 issues found in the FSM.

bad_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")
  |> FSM.add_transition(:a, :c, label: "y")

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

bad_fsm
|> Choreo.FSM.Render.DOT.to_dot()
|> Kino.VizJS.render()

Transforms

Complement

Swap final and non-final states.

comp = FSM.complement(dfa)

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

Prune

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

pruned = FSM.prune(bad_fsm)

IO.inspect(FSM.states(pruned), label: "States after pruning")
Kino.VizJS.render(FSM.to_dot(pruned))

Theming

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

dot_dark = FSM.to_dot(order_flow, theme: :presentation)
Kino.VizJS.render(dot_dark)

Summary