pub fn tau_scc_decomposition(lts: &LabelledTransitionSystem) -> IndexedPartition {

    let partition = scc_decomposition(lts, &|_, label_index, _| lts.is_hidden_label(label_index));

    if cfg!(debug_assertions) {

        let quotient_lts = quotient_lts(lts, &partition, true);

        debug_assert!(!has_tau_loop(&quotient_lts), "The SCC decomposition contains tau-loops");

    partition

}

pub fn scc_decomposition<F>(lts: &LabelledTransitionSystem, filter: &F) -> IndexedPartition

where

    F: Fn(usize, usize, usize) -> bool,

{

    let start = Instant::now();

    trace!("{:?}", lts);

    let mut partition = IndexedPartition::new(lts.num_of_states());

    // The stack for the depth first search.

    let mut stack = Vec::new();

    // Keep track of already visited states.

    let mut state_info: Vec<Option<StateInfo>> = vec![None; lts.num_of_states()];

    let mut smallest_index = 0;

    let mut next_block_number = 0;

    for state_index in lts.iter_states() {

        if state_info[state_index].is_none() {

            trace!("State {state_index}");

            strongly_connect(

                state_index,

                lts,

                filter,

                &mut partition,

                &mut smallest_index,

                &mut next_block_number,

                &mut stack,

                &mut state_info,

            )

        }

    trace!("SCC partition {partition}");

    debug!("Found {} strongly connected components", partition.num_of_blocks());

    debug!("Time scc_decomposition: {:.3}s", start.elapsed().as_secs_f64());

    partition

}

fn strongly_connect<F>(

    state_index: usize,

    lts: &LabelledTransitionSystem,

    filter: &F,

    partition: &mut IndexedPartition,

    smallest_index: &mut usize,

    next_block_number: &mut usize,

    stack: &mut Vec<usize>,

    state_info: &mut Vec<Option<StateInfo>>,

) where

    F: Fn(usize, usize, usize) -> bool,

{

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

    state_info[state_index] = Some(StateInfo {

        index: *smallest_index,

        lowlink: *smallest_index,

        on_stack: true,

    });

    *smallest_index += 1;

    // Start a depth first search from the current state.

    stack.push(state_index);

    for (label_index, to_index) in lts.outgoing_transitions(state_index) {

        if filter(state_index, *label_index, *to_index) {

            if let Some(meta) = &mut state_info[*to_index] {

                if meta.on_stack {

                    // Successor w is in stack S and hence in the current SCC

                    // If w is not on stack, then (v, w) is an edge pointing to an SCC already found and must be ignored

                    // v.lowlink := min(v.lowlink, w.lowlink);

                    let w_index = state_info[*to_index]

                        .as_ref()

                        .expect("The state must be visited in the recursive call")

                        .index;

                    let info = state_info[state_index].as_mut().expect("This state was added before");

                    info.lowlink = info.lowlink.min(w_index);

                }

            } else {

                // Successor w has not yet been visited; recurse on it

                strongly_connect(

                    *to_index,

                    lts,

                    filter,

                    partition,

                    smallest_index,

                    next_block_number,

                    stack,

                    state_info,

                );

                // v.lowlink := min(v.lowlink, w.lowlink);

                let w_lowlink = state_info[*to_index]

                    .as_ref()

                    .expect("The state must be visited in the recursive call")

                    .lowlink;

                let info = state_info[state_index].as_mut().expect("This state was added before");

                info.lowlink = info.lowlink.min(w_lowlink);

            }

        }

    let info = state_info[state_index].as_ref().expect("This state was added before");

    if info.lowlink == info.index {

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

            let info = state_info[index].as_mut().expect("This state was on the stack");

            info.on_stack = false;

            trace!("Added state {index} to block {}", next_block_number);

            partition.set_block(index, *next_block_number);

            if index == state_index || stack.is_empty() {

                *next_block_number += 1;

                break;

            }

    }

}

pub fn has_tau_loop(lts: &LabelledTransitionSystem) -> bool {

    sort_topological(lts, |label_index, _| lts.is_hidden_label(label_index), false).is_err()

}

    fn reachable_states(

        lts: &LabelledTransitionSystem,

        state_index: usize,

        filter: &impl Fn(usize, usize, usize) -> bool,

    ) -> Vec<usize> {

        let mut stack = vec![state_index];

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

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

            for (_, to_index) in lts.outgoing_transitions(inner_state_index) {

                if filter(inner_state_index, 0, *to_index) && !visited[*to_index] {

                    visited[*to_index] = true;

                    stack.push(*to_index);

                }

        visited

            .into_iter()

            .enumerate()

            .filter_map(|(index, visited)| if visited { Some(index) } else { None })

            .collect()

    }

    #[test]

            let reachable = reachable_states(&lts, state_index, &|_, label, _| lts.is_hidden_label(label));

                .filter(|index| state_index != *index && partitioning.block_number(*index) == block)

    #[test]

            || transitions.iter().cloned(),