///|
/// One state in an explicitly enumerated finite transition system.
pub(all) struct State {
  id : String
  labels : Array[String]
} derive(Debug)

///|
pub extend State with Debug::{to_repr}

///|
/// A directed transition. `action` is used in counterexample traces.
pub(all) struct Edge {
  from : Int
  to : Int
  action : String
} derive(Debug)

///|
pub extend Edge with Debug::{to_repr}

///|
pub(all) enum ModelError {
  EmptyStates
  InvalidInitial(Int)
  DuplicateState(String)
  InvalidEdge(Int, Int)
} derive(Debug)

///|
pub extend ModelError with Debug::{to_repr}

///|
/// A complete, finite transition system. Dead-end states have an implicit
/// self-loop when interpreting CTL, following the usual total Kripke semantics.
pub struct Model {
  states : Array[State]
  outgoing : Array[Array[Edge]]
  incoming : Array[Array[Int]]
  initial : Int
}

///|
pub fn Model::new(
  states : Array[State],
  edges : Array[Edge],
  initial~ : Int,
) -> Result[Model, ModelError] {
  let count = states.length()
  if count == 0 {
    return Err(EmptyStates)
  }
  if initial < 0 || initial >= count {
    return Err(InvalidInitial(initial))
  }
  let ids : Map[String, Bool] = Map([])
  for state in states {
    if ids.contains(state.id) {
      return Err(DuplicateState(state.id))
    }
    ids[state.id] = true
  }
  let outgoing = Array::makei(count, _ => Array())
  for edge in edges {
    if edge.from < 0 || edge.from >= count || edge.to < 0 || edge.to >= count {
      return Err(InvalidEdge(edge.from, edge.to))
    }
    outgoing[edge.from].push(edge)
  }
  for i in 0..", })
    }
  }
  let incoming = Array::makei(count, _ => Array())
  for i in 0.. State::{
    id: s.id,
    labels: s.labels.copy(),
  })
  Ok({ states: owned_states, outgoing, incoming, initial, })
}

///|
pub fn Model::state_count(self : Model) -> Int {
  self.states.length()
}

///|
pub fn Model::initial(self : Model) -> Int {
  self.initial
}

///|
pub fn Model::state_id(self : Model, index : Int) -> String? {
  self.states.get(index).map(s => s.id)
}

///|
/// Return state IDs that cannot be reached from the initial state, in the
/// model's input order. This helps spot states that cannot affect a verdict.
pub fn Model::unreachable_states(self : Model) -> Array[String] {
  let seen = Array::make(self.states.length(), false)
  let queue = [self.initial]
  seen[self.initial] = true
  let mut head = 0
  while head < queue.length() {
    let current = queue[head]
    head += 1
    for edge in self.outgoing[current] {
      if !seen[edge.to] {
        seen[edge.to] = true
        queue.push(edge.to)
      }
    }
  }
  let missing : Array[String] = []
  for i in 0.. Bool {
  match self.states.get(index) {
    Some(state) => state.labels.contains(label)
    None => false
  }
}

///|
pub fn Model::successors(self : Model, index : Int) -> Array[Edge] {
  match self.outgoing.get(index) {
    Some(edges) => edges.copy()
    _ => []
  }
}