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

    scc_decomposition(lts, &|_, label_index, _| lts.is_hidden_label(label_index))

}

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

where

    F: Fn(StateIndex, LabelIndex, StateIndex) -> bool,

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

    let mut stack = Vec::new();

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

    let mut smallest_index = 0;

    let mut next_block_number = BlockIndex::new(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!(

    partition

}

fn strongly_connect<F>(

    state_index: StateIndex,

    lts: &impl LTS,

    filter: &F,

    partition: &mut IndexedPartition,

    smallest_index: &mut usize,

    next_block_number: &mut BlockIndex,

    stack: &mut Vec<StateIndex>,

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

) where

    F: Fn(StateIndex, LabelIndex, StateIndex) -> bool,

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

    state_info[state_index] = Some(StateInfo {

        index: *smallest_index,

        lowlink: *smallest_index,

        on_stack: true,

    });

    *smallest_index += 1;

    stack.push(state_index);

    for transition in lts.outgoing_transitions(state_index) {

        if filter(state_index, transition.label, transition.to) {

            if let Some(meta) = &mut state_info[transition.to] {

                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[transition.to]

                        .as_ref()

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

                        .index;

                    let info = state_info[state_index.value()]

                        .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(

                    transition.to,

                    lts,

                    filter,

                    partition,

                    smallest_index,

                    next_block_number,

                    stack,

                    state_info,

                );

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

                let w_lowlink = state_info[transition.to.value()]

                    .as_ref()

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

                    .lowlink;

                let info = state_info[state_index.value()]

                    .as_mut()

                    .expect("This state was added before");

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

            }

        }

    let info = state_info[state_index.value()]

        .as_ref()

        .expect("This state was added before");

    if info.lowlink == info.index {

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

            let info = state_info[index.value()].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 = BlockIndex::new(next_block_number.value() + 1);

                break;

            }

    }

}

pub fn has_tau_loop<L>(lts: &L) -> bool

where

    L: LTS,

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

}

    fn reachable_states(

        lts: &impl LTS,

        state_index: StateIndex,

        filter: &impl Fn(StateIndex, LabelIndex, StateIndex) -> 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 transition in lts.outgoing_transitions(inner_state_index) {

                if filter(inner_state_index, LabelIndex::new(0), transition.to) && !visited[transition.to.value()] {

                    visited[transition.to.value()] = true;

                    stack.push(transition.to);

                }

        visited

            .into_iter()

            .enumerate()

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

            .collect()

    }

        random_test(100, |rng| {

            let mut files = DumpFiles::new("test_random_tau_scc_decomposition");

            let lts = random_lts(rng, 10, 3, 3);

            files.dump("input.aut", |f| write_aut(f, &lts)).unwrap();

            let partitioning = tau_scc_decomposition(&lts);

            let reduction = quotient_lts_naive(&lts, &partitioning, true);

            assert!(!has_tau_loop(&reduction), "The SCC decomposition contains tau-loops");

            files.dump("tau_scc_decomposition.aut", |f| write_aut(f, &reduction)).unwrap();

            for state_index in lts.iter_states() {

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

                let block = partitioning.block_number(state_index);

                for other_state_index in lts

                    .iter_states()

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

                    assert!(

                        reachable.contains(&other_state_index),

            assert!(

                reduction.num_of_states() == tau_scc_decomposition(&reduction).num_of_blocks(),

        });

            .map(|(from, label, to)| (StateIndex::new(from), LabelIndex::new(label), StateIndex::new(to)));

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