@spec accepted_strings(Choreo.FSM.t(), non_neg_integer()) :: [[String.t()]]

Enumerates all accepted input strings up to a maximum length.

This performs a breadth-first expansion of the state space and collects every path that ends in a final state. The result is deduplicated.

Warning: Cyclic FSMs can produce exponentially many paths; keep max_length small.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_final_state(:b)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  ...>   |> Choreo.FSM.add_transition(:b, :b, label: "y")
  iex> Enum.sort(Choreo.FSM.Analysis.accepted_strings(fsm, 2))
  [["x"], ["x", "y"]]

This analysis answers the question: "What inputs are accepted up to length N?"

@spec accepts?(Choreo.FSM.t(), [String.t()]) :: boolean()

Simulates the FSM on a sequence of input symbols.

Returns true if the unique path from the initial state leads to a final state after consuming all inputs.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:idle)
  ...>   |> Choreo.FSM.add_state(:running)
  ...>   |> Choreo.FSM.add_final_state(:done)
  ...>   |> Choreo.FSM.add_transition(:idle, :running, label: "start")
  ...>   |> Choreo.FSM.add_transition(:running, :done, label: "finish")
  iex> Choreo.FSM.Analysis.accepts?(fsm, ["start", "finish"])
  true
  iex> Choreo.FSM.Analysis.accepts?(fsm, ["start"])
  false

This analysis answers the question: "Does this input sequence lead to acceptance?"

@spec alphabet(Choreo.FSM.t()) :: MapSet.t(String.t())

Returns the set of distinct input symbols (the alphabet) of the FSM.

The alphabet is derived from all transition labels. Empty-string labels are excluded.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_state(:c)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  ...>   |> Choreo.FSM.add_transition(:b, :c, label: "y")
  ...>   |> Choreo.FSM.add_transition(:c, :a, label: "x")
  iex> Choreo.FSM.Analysis.alphabet(fsm) |> MapSet.to_list() |> Enum.sort()
  ["x", "y"]

This analysis answers the question: "What are the distinct input symbols?"

@spec complete?(Choreo.FSM.t()) :: boolean()

Checks whether the FSM is complete (total).

A complete FSM has a transition from every state for every symbol in the alphabet. Incomplete FSMs implicitly reject inputs that have no matching transition.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  ...>   |> Choreo.FSM.add_transition(:a, :a, label: "y")
  ...>   |> Choreo.FSM.add_transition(:b, :a, label: "x")
  ...>   |> Choreo.FSM.add_transition(:b, :b, label: "y")
  iex> Choreo.FSM.Analysis.complete?(fsm)
  true

This analysis answers the question: "Does every state handle every input symbol?"

@spec dead_states(Choreo.FSM.t()) :: [Yog.node_id()]

Returns states that have no path to any final state.

A "dead state" (or trap state) is one from which an accepting state can never be reached. If the FSM has no final states, every state is considered dead.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_final_state(:c)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "go")
  ...>   |> Choreo.FSM.add_transition(:a, :c, label: "ok")
  iex> Choreo.FSM.Analysis.dead_states(fsm)
  [:b]

This analysis answers the question: "Which states are traps that can never accept?"

@spec livelock_states(Choreo.FSM.t()) :: [Yog.node_id()]

Returns all reachable states that are part of a cycle of dead states (livelock).

A state is in a livelock when it is reachable from the start, has no path to any final/accepting state, and is part of a cycle (can reach itself).

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:start)
  ...>   |> Choreo.FSM.add_final_state(:ok)
  ...>   |> Choreo.FSM.add_state(:l1)
  ...>   |> Choreo.FSM.add_state(:l2)
  ...>   |> Choreo.FSM.add_transition(:start, :ok, label: "yes")
  ...>   |> Choreo.FSM.add_transition(:start, :l1, label: "fail")
  ...>   |> Choreo.FSM.add_transition(:l1, :l2, label: "loop")
  ...>   |> Choreo.FSM.add_transition(:l2, :l1, label: "back")
  ...>   |> Choreo.FSM.add_state(:dead_end)
  ...>   |> Choreo.FSM.add_transition(:start, :dead_end, label: "trap")
  iex> Enum.sort(Choreo.FSM.Analysis.livelock_states(fsm))
  [:l1, :l2]

This analysis answers the question: "Which states can get trapped in infinite non-accepting loops?"

@spec reachable_states(Choreo.FSM.t()) :: [Yog.node_id()]

Returns all states reachable from any initial state.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_state(:c)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "go")
  iex> Enum.sort(Choreo.FSM.Analysis.reachable_states(fsm))
  [:a, :b]

This analysis answers the question: "Which states can I reach from the start?"

@spec shortest_accepting_path(Choreo.FSM.t()) :: {:ok, [String.t()]} | :error

Finds the shortest sequence of transition labels that leads from an initial state to a final state.

Returns {:ok, [String.t()]} or :error if no accepting path exists.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_final_state(:c)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  ...>   |> Choreo.FSM.add_transition(:b, :c, label: "y")
  iex> Choreo.FSM.Analysis.shortest_accepting_path(fsm)
  {:ok, ["x", "y"]}

This analysis answers the question: "What is the minimum input to reach an accepting state?"

@spec validate(Choreo.FSM.t()) :: [{:error | :warning, String.t()}]

Validates the FSM and returns a list of issues.

Checks for:

* no initial state defined
* no final states defined
* unreachable states
* dead (trap) states
* incomplete alphabet coverage

Returns a list of {severity, message} tuples.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:idle)
  ...>   |> Choreo.FSM.add_final_state(:done)
  ...>   |> Choreo.FSM.add_transition(:idle, :done, label: "go")
  ...>   |> Choreo.FSM.add_transition(:done, :idle, label: "go")
  iex> Choreo.FSM.Analysis.validate(fsm)
  []

This analysis answers the question: "Is the state machine structurally sound?"