pub fn weak_bisimulation<L: LTS>(

    lts: L,

    state: StateIndex,

    preprocess: bool,

    divergence_preserving: bool,

    timing: &Timing,

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

    if preprocess {

        weak_bisimulation_preprocessed(lts, state, divergence_preserving, timing)

}

pub fn weak_bisimulation_parallel<L: LTS>(

    lts: L,

    state: StateIndex,

    preprocess: bool,

    divergence_preserving: bool,

    timing: &Timing,

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

    if preprocess {

        weak_bisimulation_parallel_preprocessed(lts, state, divergence_preserving, timing)

}

fn weak_bisimulation_preprocessed<L: LTS>(

    lts: L,

    state: StateIndex,

    divergence_preserving: bool,

    timing: &Timing,

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || {

        tau_cycle_elimination_and_reorder(lts, state, !divergence_preserving)

    });

    timing.measure("reduction", || {

        let blocks = if divergence_preserving {

            let divergence_preserving_lts = DivergencePreservingLts::new(&tau_loop_free_lts);

            weak_bisimulation_impl(&divergence_preserving_lts)

            weak_bisimulation_impl(&tau_loop_free_lts)

        (tau_loop_free_lts, mapped_state, blocks)

    })

}

fn weak_bisimulation_parallel_preprocessed<L: LTS>(

    lts: L,

    state: StateIndex,

    divergence_preserving: bool,

    timing: &Timing,

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || {

        tau_cycle_elimination_and_reorder(lts, state, !divergence_preserving)

    });

    timing.measure("reduction", || {

        let blocks = if divergence_preserving {

            let divergence_preserving_lts = DivergencePreservingLts::new(&tau_loop_free_lts);

            weak_bisimulation_parallel_impl(&divergence_preserving_lts)

            weak_bisimulation_parallel_impl(&tau_loop_free_lts)

        (tau_loop_free_lts, mapped_state, blocks)

    })

}

fn weak_bisimulation_impl<L: LTS>(lts: &L) -> MarkedBlockPartition {

    let mut blocks = MarkedBlockPartition::new(lts.num_of_states());

    let mut act_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

    let mut tau_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

    let incoming = IncomingTransitions::new(lts);

    let progress = TimeProgress::new(

        |num_of_blocks: usize| {

            info!("Found {} blocks...", num_of_blocks);

        },

        let mut stable = true;

        for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            progress.print(blocks.num_of_blocks());

            if *blocks.block(block_index).annotation() {

                continue;

            }

            trace!("Stabilising block {:?}", block_index);

            stable = false;

            blocks.mark_block_stable(block_index);

            for label in lts.labels().iter().enumerate().map(|(i, _)| LabelIndex::new(i)) {

                compute_weak_act(

                    &mut act_mark,

                    &mut tau_mark,

                    lts,

                    &blocks,

                    &incoming,

                    block_index,

                    label,

                for block_prime in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

                    stabilise(block_prime, &mut act_mark, &mut blocks);

                }

        if stable {

            trace!("Partition is stable!");

            break;

        }

    blocks

}

fn weak_bisimulation_parallel_impl<L: LTS>(lts: &L) -> MarkedBlockPartition {

    let progress = TimeProgress::new(

    let mut blocks = MarkedBlockPartition::new(lts.num_of_states());

    let mut marked = Vec::from_iter(iter::repeat_n(

        bitvec![u64, Lsb0; 0; lts.labels().len()],

        lts.num_of_states(),

    let incoming = IncomingTransitions::new(lts);

        let mut stable = true;

        for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            progress.print(blocks.num_of_blocks());

            if *blocks.block(block_index).annotation() {

                continue;

            }

            trace!("Stabilising block {:?}", block_index);

            stable = false;

            blocks.mark_block_stable(block_index);

            for act_mark in &mut marked {

                act_mark.fill(false);

            }

            compute_weak_acts(&mut marked, lts, &incoming, &blocks, block_index);

            while let Some(label) = find_act(lts, &blocks, &mut marked) {

                for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

                    stabilise_act(block_index, label, &mut marked, &mut blocks);

                }

        if stable {

            trace!("Partition is stable!");

            break;

        }

    blocks

}

fn compute_weak_act<L: LTS>(

    act_mark: &mut BitArray,

    tau_mark: &mut BitArray,

    lts: &L,

    blocks: &MarkedBlockPartition,

    incoming: &IncomingTransitions,

    block: BlockIndex,

    label: LabelIndex,

) {

    for s in lts.iter_states() {

        act_mark.set(

            *s,

            lts.is_hidden_label(label) && blocks.iter_block(block).any(|state| state == *s),

        for transition in lts.outgoing_transitions(s) {

            if transition.label == label {

                if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {

                    act_mark.set(*s, true);

                }

            }

    for t in lts.iter_states() {

        if lts.is_hidden_label(label) {

            tau_mark.set(*t, act_mark[*t]);

        }

        if act_mark[*t] {

            for transition in incoming.incoming_silent_transitions(t) {

                act_mark.set(*transition.from, true);

            }

        }

}

fn compute_weak_acts<L: LTS>(

    marked: &mut [BitArray],

    lts: &L,

    incoming: &IncomingTransitions<'_>,

    blocks: &MarkedBlockPartition,

    block: BlockIndex,

) {

    if cfg!(debug_assertions) {

        let mut tau_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

        for s in lts.iter_states() {

            tau_mark.set(*s, marked[*s][0]);

        }

        let act_mark = (0..lts.labels().len())

            .map(|label| {

                let mut act_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

                for s in lts.iter_states() {

                    act_mark.set(*s, marked[*s][label]);

                }

                compute_weak_act(

                    &mut act_mark,

                    &mut tau_mark,

                    lts,

                    blocks,

                    incoming,

                    block,

                    LabelIndex::new(label),

                act_mark

            })

            .collect::<Vec<_>>();

        compute_weak_acts_inner(marked, lts, incoming, blocks, block);

        for label in 1..lts.labels().len() {

            debug_assert!(

                act_mark[label].iter().zip(marked.iter()).all(|(a, m)| a == m[label]),

}

fn compute_weak_acts_inner<L: LTS>(

    marked: &mut [BitArray],

    lts: &L,

    incoming: &IncomingTransitions<'_>,

    blocks: &MarkedBlockPartition,

    block: BlockIndex,

) {

    debug_assert!(

        marked.iter().all(|m| m.not_any()),

    let tau_index = LabelIndex::new(0);

    debug_assert!(

        lts.is_hidden_label(tau_index),

    for t in blocks.iter_block(block) {

        marked[t].set(*tau_index, true);

    }

    for t in lts.iter_states() {

        if marked[*t][*tau_index] {

            for transition in incoming.incoming_silent_transitions(t) {

                // s.marked[tau] := True if t.marked[tau]

                marked[transition.from].set(*tau_index, true);

            }

        }

    for t in lts.iter_states() {

        for transition in lts.outgoing_transitions(t) {

            if marked[*transition.to][*tau_index] {

                marked[*t].set(*transition.label, true);

            }

        for transition in incoming.incoming_silent_transitions(t) {

            let [marked_s, marked_t] = marked

                .get_disjoint_mut([*transition.from, *t])

                .expect("The indices are disjoint");

            for (i, number) in marked_s.as_raw_mut_slice().iter_mut().enumerate() {

                *number |= marked_t.as_raw_slice()[i];

            }

}

fn find_act<L: LTS>(_lts: &L, blocks: &MarkedBlockPartition, marked: &mut [BitArray]) -> Option<LabelIndex> {

    for block in (0..blocks.num_of_blocks()).map(BlockIndex::new) {

        let s = blocks.iter_block(block).next().expect("Block is non-empty");

        for t in blocks.iter_block(block) {

            if marked[s] != marked[t] {

                for (label, marked_s) in marked[s].iter().enumerate() {

                    if marked_s != marked[t][label] {

                        return Some(LabelIndex::new(label));

                    }

            }

    None

}

fn stabilise(block: BlockIndex, act_mark: &mut BitArray, blocks: &mut MarkedBlockPartition) {

    blocks.split_block(block, |state| act_mark[*state]);

}

fn stabilise_act(block: BlockIndex, act: LabelIndex, marked: &mut [BitArray], blocks: &mut MarkedBlockPartition) {

    blocks.split_block(block, |state| marked[*state][*act]);

}

    fn test_weak_bisimulation() {

        random_test(100, |rng| {

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

            let lts = random_lts::<String, _>(rng, 1000, 3);

            let mut timing = Timing::new();

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

            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &mut timing);

            let expected = reduce_lts(lts, Equivalence::WeakBisimSigref, false, &mut timing);

            assert_eq!(result.num_of_states(), expected.num_of_states());

            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

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

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

            assert!(compare_lts(

                Equivalence::StrongBisim,

                result,

                expected,

                &mut timing

        })

    }

    fn test_weak_bisimulation_parallel() {

        random_test(100, |rng| {

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

            let lts = random_lts::<String, _>(rng, 100, 3);

            let mut timing = Timing::new();

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

            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &mut timing);

            let expected = reduce_lts(lts, Equivalence::WeakBisimParallel, false, &mut timing);

            assert_eq!(result.num_of_states(), expected.num_of_states());

            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

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

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

            assert!(compare_lts(

                Equivalence::StrongBisim,

                result,

                expected,

                &mut timing

        })

    }