@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 equivalent?(Choreo.FSM.t(), Choreo.FSM.t()) :: boolean()

Checks if two FSMs accept the exact same language (are equivalent).

Uses a product automaton BFS traversal to check if there is any reachable pair of states where one is accepting (final) and the other is not.

## Examples

  iex> fsm1 =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_final_state(:b)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  iex> fsm2 =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_final_state(:c)
  ...>   |> Choreo.FSM.add_transition(:a, :c, label: "x")
  iex> Choreo.FSM.Analysis.equivalent?(fsm1, fsm2)
  true

@spec generate_test_cases(Choreo.FSM.t(), :state | :transition) :: [[String.t()]]

Generates a set of transition label sequences (test cases) to achieve the specified coverage metric.

Supported strategies:

* `:state` - guarantees every reachable state is visited at least once.
* `:transition` - guarantees every reachable transition is traversed at least once.

## 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.generate_test_cases(fsm, :state) |> Enum.sort()
  [[], ["x"], ["x", "y"]]
  iex> Choreo.FSM.Analysis.generate_test_cases(fsm, :transition) |> Enum.sort()
  [["x"], ["x", "y"]]

@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 minimize(Choreo.FSM.t()) :: Choreo.FSM.t()

Minimizes a DFA using Partition Refinement (Moore's algorithm).

Returns a new minimized FSM.

## 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")
  ...>   |> Choreo.FSM.add_transition(:a, :c, label: "z")
  iex> minimized = Choreo.FSM.Analysis.minimize(fsm)
  iex> minimized.meta.initial_state != nil
  true

@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?"

@spec violates_invariant?(
  Choreo.FSM.t(),
  keyword()
) :: boolean()

Checks whether the FSM graph contains a forbidden state sequence.

This is a static check: it looks for a connected path of transitions matching the sequence given in :forbid_path. It does not simulate a particular execution trace.

Supported options:

* `:forbid_path` - a list of state IDs that must not appear as a
  consecutive path of transitions in the FSM.

## Examples

  iex> fsm =
  ...>   Choreo.FSM.new()
  ...>   |> Choreo.FSM.add_initial_state(:a)
  ...>   |> Choreo.FSM.add_state(:b)
  ...>   |> Choreo.FSM.add_transition(:a, :b, label: "x")
  iex> Choreo.FSM.Analysis.violates_invariant?(fsm, forbid_path: [:a, :b])
  true