pub fn reachability<L: LTS>(lts: &L, state: StateIndex) -> Vec<bool> {

    let mut reachable = vec![false; lts.num_of_states()];

    reachable[state] = true;

    let mut stack = vec![state];

    while let Some(state) = stack.pop() {

        debug_assert!(reachable[state], "State {} must already be marked as reachable", state);

        trace!("Visiting {}", state);

        for transition in lts.outgoing_transitions(state) {

            if !reachable[transition.to] {

                trace!("Transition -[{}]-> {}", transition.label, transition.to);

                reachable[transition.to] = true;

                stack.push(transition.to);

            }

    trace!("Finished reachability");

    reachable

}

pub fn num_reachable_states<L: LTS>(lts: &L, state: StateIndex) -> usize {

    reachability(lts, state).iter().filter(|&&r| r).count()

}