Choreo.FSM (Choreo v0.14.0)

Copy Markdown View Source

Finite-state machine builder on top of Yog.

Choreo.FSM lets you define states, transitions, and render classic state-machine diagrams. It supports normal states, initial states, and final (accepting) states.

When to use

Use Choreo.FSM when modelling stateful behaviour — protocol handlers, UI flows, game states, or embedded-system controllers. It verifies determinism, finds dead states, and checks whether any input sequence leads to acceptance.

Further reading

Quick Start

fsm =
  Choreo.FSM.new()
  |> Choreo.FSM.add_initial_state(:idle, label: "Idle")
  |> Choreo.FSM.add_state(:running, label: "Running")
  |> Choreo.FSM.add_final_state(:done, label: "Done")
  |> Choreo.FSM.add_transition(:idle, :running, label: "start")
  |> Choreo.FSM.add_transition(:running, :done, label: "finish")
  |> Choreo.FSM.add_transition(:running, :idle, label: "pause")

dot = Choreo.FSM.to_dot(fsm)
mermaid = Choreo.FSM.to_mermaid(fsm)

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; running [label="Running", fillcolor="#e2e8f0"]; idle [label="Idle", fontcolor="white", fillcolor="#10b981"]; done [label="Done", penwidth="2.0", fillcolor="#e2e8f0", shape="doublecircle"]; running -> idle [label="pause"]; running -> done [label="finish"]; idle -> running [label="start"]; __start_idle [shape=point, width=0.15, height=0.15, style=filled, fillcolor=black]; __start_idle -> idle; }

Themes

Use any built-in theme (:default, :dark, :minimal, :warm, :forest, :ocean) or a custom Choreo.Theme struct:

dot = Choreo.FSM.to_dot(fsm, theme: :dark)
mermaid = Choreo.FSM.to_mermaid(fsm, theme: :dark)

Summary

Functions

Adds a final (accepting) state to the FSM.

Adds an initial state to the FSM.

Adds a state to the FSM.

Adds a transition (directed edge) between two states.

Returns the complement FSM: final states become normal, and normal states become final.

Returns all final state IDs.

Returns the initial state ID, or nil if none is defined.

Creates a new empty FSM.

Prunes unreachable and dead states, returning a smaller equivalent FSM.

Removes a state from the set of final states.

Removes a state from the set of initial states.

Fully removes a state and all transitions involving it from the FSM.

Returns all state IDs in the FSM.

Renders the FSM to DOT format.

Renders the FSM to Mermaid.js syntax.

Converts the multigraph to a simple graph.

Returns all transitions as {from, to, label} tuples.

Types

t()

@type t() :: %Choreo.FSM{
  edge_meta: %{optional(Yog.Multi.Graph.edge_id()) => map()},
  graph: Yog.Multi.Graph.t(),
  meta: %{
    initial_state: Yog.node_id() | nil,
    final_states: MapSet.t(Yog.node_id()),
    strict: boolean()
  }
}

Functions

add_final_state(fsm, id, opts \\ [])

@spec add_final_state(t(), Yog.node_id(), keyword()) :: t()

Adds a final (accepting) state to the FSM.

Final states are rendered as double circles.

Options

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_final_state(:done)
iex> :done in Choreo.FSM.final_states(fsm)
true

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; done [label="done", penwidth="2.0", fillcolor="#e2e8f0", shape="doublecircle"]; }

add_initial_state(fsm, id, opts \\ [])

@spec add_initial_state(t(), Yog.node_id(), keyword()) :: t()

Adds an initial state to the FSM.

Initial states are rendered with a filled entry-point dot and an incoming arrow in DOT output.

Options

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_initial_state(:idle)
iex> Choreo.FSM.initial_state(fsm) == :idle
true

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; idle [label="idle", fontcolor="white", fillcolor="#10b981"]; __start_idle [shape=point, width=0.15, height=0.15, style=filled, fillcolor=black]; __start_idle -> idle; }

add_state(fsm, id, opts \\ [])

@spec add_state(t(), Yog.node_id(), keyword()) :: t()

Adds a state to the FSM.

Options

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_state(:idle, label: "Idle")
iex> fsm.graph.nodes[:idle].label
"Idle"

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; idle [label="Idle", fillcolor="#e2e8f0"]; }

add_transition(fsm, from, to, opts \\ [])

@spec add_transition(t(), Yog.node_id(), Yog.node_id(), keyword()) :: t()

Adds a transition (directed edge) between two states.

Multiple transitions are allowed per (from, to) pair (parallel edges), as long as they have unique labels from the source state.

Guards are rendered as part of the transition label and therefore participate in analysis as transition symbols. Choreo stores guard text for rendering and inspection; it does not evaluate guard expressions.

Options

Examples

iex> fsm =
...>   Choreo.FSM.new()
...>   |> Choreo.FSM.add_state(:a)
...>   |> Choreo.FSM.add_state(:b)
...>   |> Choreo.FSM.add_transition(:a, :b, label: "go")
iex> Yog.Multi.edges_between(fsm.graph, :a, :b) != []
true

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; b [label="b", fillcolor="#e2e8f0"]; a [label="a", fillcolor="#e2e8f0"]; a -> b [label="go"]; }

complement(fsm)

@spec complement(t()) :: t()

Returns the complement FSM: final states become normal, and normal states become final.

Initial states keep their :initial type. Note that if the initial state was not previously final, it becomes both initial and final in the complement FSM (which is mathematically correct to accept the empty string).

This operation assumes a complete DFA for strict language-complement semantics. If the FSM is incomplete, missing transitions still reject during simulation; complement/1 does not add an implicit sink state.

Examples

iex> fsm =
...>   Choreo.FSM.new()
...>   |> Choreo.FSM.add_initial_state(:a)
...>   |> Choreo.FSM.add_final_state(:b)
iex> comp = Choreo.FSM.complement(fsm)
iex> :a in Choreo.FSM.final_states(comp)
true
iex> :b in Choreo.FSM.final_states(comp)
false

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; b [label="b", fillcolor="#e2e8f0"]; a [label="a", penwidth="2.0", fontcolor="white", fillcolor="#10b981", shape="doublecircle"]; __start_a [shape=point, width=0.15, height=0.15, style=filled, fillcolor=black]; __start_a -> a; }

final_states(fsm)

@spec final_states(t()) :: [Yog.node_id()]

Returns all final state IDs.

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_final_state(:done)
iex> :done in Choreo.FSM.final_states(fsm)
true

initial_state(fsm)

@spec initial_state(t()) :: Yog.node_id() | nil

Returns the initial state ID, or nil if none is defined.

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_initial_state(:idle)
iex> Choreo.FSM.initial_state(fsm)
:idle

new(opts \\ [])

@spec new(keyword()) :: t()

Creates a new empty FSM.

Options

  • :directed — whether the underlying graph is directed (default: true)
  • :strict — if true, raises on transition definitions with non-existent states (default: false)

Examples

iex> fsm = Choreo.FSM.new()
iex> fsm.graph.kind == :directed
true

prune(fsm)

@spec prune(t()) :: t()

Prunes unreachable and dead states, returning a smaller equivalent FSM.

  • Unreachable states — no path from any initial state
  • Dead states — no path to any final state

Examples

iex> fsm =
...>   Choreo.FSM.new()
...>   |> Choreo.FSM.add_initial_state(:a)
...>   |> Choreo.FSM.add_state(:b)
...>   |> Choreo.FSM.add_state(:trap)
...>   |> Choreo.FSM.add_final_state(:c)
...>   |> Choreo.FSM.add_transition(:a, :c, label: "go")
iex> pruned = Choreo.FSM.prune(fsm)
iex> :a in Choreo.FSM.states(pruned)
true
iex> :b in Choreo.FSM.states(pruned)
false
iex> :trap in Choreo.FSM.states(pruned)
false

Diagram

digraph G { graph [rankdir=LR, splines=spline, nodesep=0.5, ranksep=1.0]; node [shape=circle, style=filled, fillcolor="#e2e8f0", fontname="Helvetica", fontsize=12, fontcolor="#1e293b"]; edge [arrowhead=normal, color="#475569", style=solid, fontname="Helvetica", fontsize=10, penwidth=1.0]; c [label="c", penwidth="2.0", fillcolor="#e2e8f0", shape="doublecircle"]; a [label="a", fontcolor="white", fillcolor="#10b981"]; a -> c [label="go"]; __start_a [shape=point, width=0.15, height=0.15, style=filled, fillcolor=black]; __start_a -> a; }

remove_final_state(fsm, id)

@spec remove_final_state(t(), Yog.node_id()) :: t()

Removes a state from the set of final states.

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_final_state(:done) |> Choreo.FSM.remove_final_state(:done)
iex> :done in Choreo.FSM.final_states(fsm)
false

remove_initial_state(fsm, id)

@spec remove_initial_state(t(), Yog.node_id()) :: t()

Removes a state from the set of initial states.

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_initial_state(:idle) |> Choreo.FSM.remove_initial_state(:idle)
iex> Choreo.FSM.initial_state(fsm)
nil

remove_state(fsm, id)

@spec remove_state(t(), Yog.node_id()) :: t()

Fully removes a state and all transitions involving it from the FSM.

If the state was the initial state, the initial state is cleared. If the state was a final state, it is removed from the final states set. If the state does not exist, the FSM is returned unchanged.

Examples

iex> fsm =
...>   Choreo.FSM.new()
...>   |> Choreo.FSM.add_state(:a)
...>   |> Choreo.FSM.add_state(:b)
...>   |> Choreo.FSM.remove_state(:a)
iex> :a in Choreo.FSM.states(fsm)
false
iex> :b in Choreo.FSM.states(fsm)
true

states(fsm)

@spec states(t()) :: [Yog.node_id()]

Returns all state IDs in the FSM.

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_state(:a) |> Choreo.FSM.add_state(:b)
iex> Enum.sort(Choreo.FSM.states(fsm))
[:a, :b]

theme(name \\ :default, overrides \\ [])

@spec theme(atom(), keyword()) :: Choreo.Theme.t()

Returns a theme for Choreo.FSM.

Examples

iex> theme = Choreo.FSM.theme(:default, graph_rankdir: :tb)
iex> theme.graph_rankdir
:tb

to_dot(fsm, opts \\ [])

@spec to_dot(t(), keyword()) :: String.t()

Renders the FSM to DOT format.

Options

  • :theme:default, :dark, :minimal, :warm, :forest, :ocean, or a Choreo.Theme struct
  • :highlighted_nodes — list of state IDs to highlight
  • :highlighted_edges — list of edge IDs or {from, to} tuples to highlight
  • Any other option accepted by Yog.Multi.DOT.to_dot/2, such as :rankdir

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_state(:a)
iex> dot = Choreo.FSM.to_dot(fsm)
iex> String.contains?(dot, "digraph")
true
iex> String.contains?(dot, "a")
true

to_mermaid(fsm, opts \\ [])

@spec to_mermaid(t(), keyword()) :: String.t()

Renders the FSM to Mermaid.js syntax.

The default output is flowchart syntax. Pass syntax: :state_diagram to render native Mermaid stateDiagram-v2 syntax.

Options

  • :syntax:flowchart (default) or :state_diagram
  • :theme:default, :dark, :minimal, :warm, :forest, :ocean, or a Choreo.Theme struct (for :flowchart syntax)
  • :direction:lr (default), :td, :rl, :bt (for :flowchart syntax)
  • :highlighted_nodes — list of state IDs to highlight (for :flowchart syntax)
  • :highlighted_edges — list of edge IDs or {from, to} tuples to highlight (for :flowchart syntax)

Examples

iex> fsm = Choreo.FSM.new() |> Choreo.FSM.add_state(:a)
iex> mermaid = Choreo.FSM.to_mermaid(fsm)
iex> String.contains?(mermaid, "graph LR")
true
iex> String.contains?(mermaid, "a")
true

to_simple_graph(fsm, opts \\ [])

@spec to_simple_graph(t(), keyword()) :: Yog.Graph.t()

Converts the multigraph to a simple graph.

transitions(fsm)

@spec transitions(t()) :: [{Yog.node_id(), Yog.node_id(), String.t()}]

Returns all transitions as {from, to, label} tuples.

Examples

iex> fsm =
...>   Choreo.FSM.new()
...>   |> Choreo.FSM.add_state(:a)
...>   |> Choreo.FSM.add_state(:b)
...>   |> Choreo.FSM.add_transition(:a, :b, label: "go")
iex> Choreo.FSM.transitions(fsm)
[{:a, :b, "go"}]