pub fn strong_bisim_sigref<L: LTS>(lts: L, timing: &Timing) -> (L, BlockPartition) {

    let incoming = timing.measure("preprocess", || IncomingTransitions::new(&lts));

    let partition = timing.measure("reduction", || {

        signature_refinement::<_, _, _, false>(

            &lts,

            &incoming,

            |state_index, partition, _, builder| {

                strong_bisim_signature(state_index, &lts, partition, builder);

            },

    });

    (lts, partition)

}

pub fn strong_bisim_sigref_naive<L: LTS>(lts: L, timing: &Timing) -> (L, IndexedPartition) {

    let partition = timing.measure("reduction", || {

        signature_refinement_naive::<_, _, false>(&lts, |state_index, partition, _, builder| {

            strong_bisim_signature(state_index, &lts, partition, builder);

        })

    });

    (lts, partition)

}

pub fn branching_bisim_sigref<L: LTS>(lts: L, state: StateIndex, timing: &Timing) -> (LabelledTransitionSystem<L::Label>, StateIndex, BlockPartition) {

    let (preprocessed_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

    let incoming = timing.measure("preprocess", || IncomingTransitions::new(&preprocessed_lts));

    if log_enabled!(log::Level::Debug) {

    }

    let mut expected_builder = SignatureBuilder::default();

    let mut visited = FxHashSet::default();

    let mut stack = Vec::new();

    let partition = timing.measure("reduction", || {

        signature_refinement::<_, _, _, true>(

            &preprocessed_lts,

            &incoming,

            |state_index, partition, state_to_key, builder| {

                branching_bisim_signature_inductive(state_index, &preprocessed_lts, partition, state_to_key, builder);

                if cfg!(debug_assertions) {

                    branching_bisim_signature(

                        state_index,

                        &preprocessed_lts,

                        partition,

                        &mut expected_builder,

                        &mut visited,

                        &mut stack,

                    let expected_result = builder.clone();

                    let signature = Signature::new(builder);

                    debug_assert_eq!(

                        signature.as_slice(),

            },

            |signature, key_to_signature| {

                for (label, key) in signature.iter().rev() {

                    if is_tau_hat(*label, &preprocessed_lts)

                        && key_to_signature[*key].is_subset_of(signature, (*label, *key))

                        return Some(*key);

                    }

                    if !is_tau_hat(*label, &preprocessed_lts) {

                        return None;

                    }

                None

            },

    });

    (preprocessed_lts, mapped_state, partition)

}

pub fn branching_bisim_sigref_naive<L: LTS>(

    lts: L,

    state: StateIndex,

    timing: &Timing,

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

    let (preprocessed_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

    timing.measure("reduction", || {

        let mut expected_builder = SignatureBuilder::default();

        let mut visited = FxHashSet::default();

        let mut stack = Vec::new();

        let partition = signature_refinement_naive::<_, _, false>(

            &preprocessed_lts,

            |state_index, partition, state_to_signature, builder| {

                branching_bisim_signature_sorted(

                    state_index,

                    &preprocessed_lts,

                    partition,

                    state_to_signature,

                    builder,

                if cfg!(debug_assertions) {

                    branching_bisim_signature(

                        state_index,

                        &preprocessed_lts,

                        partition,

                        &mut expected_builder,

                        &mut visited,

                        &mut stack,

                    let expected_result = builder.clone();

                    let signature = Signature::new(builder);

                    debug_assert_eq!(

                        signature.as_slice(),

            },

        (preprocessed_lts, mapped_state, partition)

    })

}

pub fn weak_bisim_sigref_inductive_naive<L: LTS>(

    lts: L,

    state: StateIndex,

    preprocess: bool,

    timing: &Timing,

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

    if preprocess {

        weak_bisim_sigref_inductive_naive_impl(lts, state, timing)

}

pub fn weak_bisim_sigref_inductive_naive_impl<L: LTS>(

    lts: L,

    state: StateIndex,

    timing: &Timing,

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

    let (preprocessed_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

    let partition = timing.measure("reduction", || signature_refinement_weak(&preprocessed_lts));

    (preprocessed_lts, mapped_state, partition)

}

pub fn weak_bisim_sigref_naive<L: LTS>(

    lts: L,

    state: StateIndex,

    preprocess: bool,

    timing: &Timing,

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

    if preprocess {

        weak_bisim_sigref_naive_impl(lts, state, timing)

}

fn weak_bisim_sigref_naive_impl<L: LTS>(

    lts: L,

    state: StateIndex,

    timing: &Timing,

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

    let (preprocessed_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

    let partition = timing.measure("reduction", || {

        signature_refinement_naive::<_, _, true>(

            &preprocessed_lts,

            |state_index, partition, state_to_signature, builder| {

                weak_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder)

            },

    });

    (preprocessed_lts, mapped_state, partition)

}

fn signature_refinement<F, G, L, const BRANCHING: bool>(

    lts: &L,

    incoming: &IncomingTransitions,

    mut signature: F,

    mut renumber: G,

) -> BlockPartition

where

    F: FnMut(StateIndex, &BlockPartition, &[BlockIndex], &mut SignatureBuilder),

    G: FnMut(&[(LabelIndex, BlockIndex)], &Vec<Signature>) -> Option<BlockIndex>,

    L: LTS,

    let mut arena = Bump::new();

    let mut builder = SignatureBuilder::default();

    let mut split_builder = BlockPartitionBuilder::default();

    let mut id: FxHashMap<Signature<'_>, BlockIndex> = FxHashMap::default();

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

    let mut state_to_key: Vec<BlockIndex> = Vec::new();

    state_to_key.resize_with(lts.num_of_states(), || BlockIndex::new(0));

    let mut key_to_signature: Vec<Signature> = Vec::new();

    let mut iteration = 0usize;

    let mut states = Vec::new();

    let mut worklist = vec![BlockIndex::new(0)];

    let progress = TimeProgress::new(

        |(iteration, blocks)| {

            info!("Iteration {iteration}, found {blocks} blocks...");

        },

    while let Some(block_index) = worklist.pop() {

        id.clear();

        key_to_signature.clear();

        let id: &mut FxHashMap<Signature<'_>, BlockIndex> = unsafe { std::mem::transmute(&mut id) };

        let key_to_signature: &'_ mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut key_to_signature) };

        arena.reset();

        let block = partition.block(block_index);

        debug_assert!(

            block.has_marked(),

        if BRANCHING {

            partition.mark_backward_closure(block_index, incoming);

        }

        let num_blocks = partition.num_of_blocks();

        let empty_slice: &[(LabelIndex, BlockIndex)] = &[];

        for new_block_index in

            partition.partition_marked_with(block_index, &mut split_builder, |state_index, partition| {

                signature(state_index, partition, &state_to_key, &mut builder);

                let index = if let Some(key) = renumber(&builder, key_to_signature) {

                    key

                } else if let Some((_, index)) = id.get_key_value(&Signature::new(&builder)) {

                    *index

                    let slice = if builder.is_empty() {

                        empty_slice

                        arena.alloc_slice_copy(&builder)

                    let number = BlockIndex::new(key_to_signature.len());

                    id.insert(Signature::new(slice), number);

                    key_to_signature.push(Signature::new(slice));

                    number

                state_to_key[state_index] = index;

                trace!("State {state_index} signature {builder:?} index {index}");

                index

            })

            if block_index != new_block_index {

                states.clear();

                states.extend(partition.iter_block(new_block_index));

                for &state_index in &states {

                    for transition in incoming.incoming_transitions(state_index) {

                        if BRANCHING {

                            if !lts.is_hidden_label(transition.label)

                                || partition.block_number(transition.from) < num_blocks

                                let other_block = partition.block_number(transition.from);

                                if !partition.block(other_block).has_marked() {

                                    // If block was not already marked then add it to the worklist.

                                    worklist.push(other_block);

                                }

                                partition.mark_element(transition.from);

                            }

                            let other_block = partition.block_number(transition.from);

                            if !partition.block(other_block).has_marked() {

                                // If block was not already marked then add it to the worklist.

                                worklist.push(other_block);

                            }

                            partition.mark_element(transition.from);

            }

        trace!("Iteration {iteration} partition {partition}");

        iteration += 1;

        progress.print((iteration, partition.num_of_blocks()));

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

    partition

}

fn signature_refinement_weak<L: LTS>(lts: &L) -> IndexedPartition

where {

    let mut arena = Bump::new();

    let mut builder = SignatureBuilder::default();

    let mut id: FxHashMap<Signature<'_>, BlockIndex> = FxHashMap::default();

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

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

    let mut state_to_signature: Vec<Option<usize>> = Vec::new();

    let mut key_to_signature: Vec<Signature> = Vec::new();

    let mut state_to_taus: Vec<Signature> = Vec::new();

    state_to_signature.resize_with(lts.num_of_states(), || None);

    state_to_taus.resize_with(lts.num_of_states(), Signature::default);

    let mut old_count = 1;

    let mut iteration = 0;

    let progress = TimeProgress::new(

    let empty_slice: &[(LabelIndex, BlockIndex)] = &[];

    while old_count != id.len() {

        old_count = id.len();

        progress.print((iteration, old_count));

        swap(&mut partition, &mut next_partition);

        id.clear();

        arena.reset();

        state_to_signature.clear();

        key_to_signature.clear();

        state_to_signature.resize_with(lts.num_of_states(), || None);

        let state_to_signature: &'_ mut Vec<Option<usize>> = unsafe { std::mem::transmute(&mut state_to_signature) };

        let id: &'_ mut FxHashMap<Signature<'_>, BlockIndex> = unsafe { std::mem::transmute(&mut id) };

        let key_to_signature: &'_ mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut key_to_signature) };

        let state_to_taus: &'_ mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut state_to_taus) };

        state_to_taus.resize_with(lts.num_of_states(), Signature::default);

        for state in lts.iter_states() {

            weak_bisim_signature_sorted_taus(state, lts, &partition, state_to_taus, &mut builder);

            let slice = if builder.is_empty() {

                arena.alloc_slice_copy(&builder)

            state_to_taus[state] = Signature::new(slice);

        for state_index in lts.iter_states() {

            weak_bisim_presignature_sorted(

                state_index,

                lts,

                &partition,

                state_to_taus,

                state_to_signature,

                &mut builder,

            let mut inductive_key = None;

            for keyvalue in builder.as_slice() {

                if is_tau_hat(keyvalue.0, lts) {

                    let tau_sig = &key_to_signature[keyvalue.1.value()];

                    let presig = Signature::new(&builder);

                    if tau_sig.is_subset_of(presig.as_slice(), *keyvalue) {

                        inductive_key = Some(*keyvalue.1);

                        break;

                    }

                }

            if let Some(inductive_key) = inductive_key {

                trace!(

                state_to_signature[state_index] = Some(inductive_key);

                next_partition.set_block(*state_index, BlockIndex::new(inductive_key));

                weak_bisim_signature_sorted_full(

                    state_index,

                    lts,

                    &partition,

                    state_to_taus,

                    state_to_signature,

                    key_to_signature,

                    &mut builder,

                trace!("State {state_index} final signature {:?}", builder.as_slice());

                let mut new_id = BlockIndex::new(key_to_signature.len());

                if let Some((_signature, index)) = id.get_key_value(&Signature::new(&builder)) {

                    // SAFETY: We know that the signature lives as long as the arena

                    state_to_signature[state_index] = Some(index.value());

                    new_id = *index;

                } else {

                    let slice = if builder.is_empty() {

                        arena.alloc_slice_copy(&builder)

                    id.insert(Signature::new(slice), new_id);

                    key_to_signature.push(Signature::new(slice));

                    state_to_signature[state_index] = Some(new_id.value());

                next_partition.set_block(*state_index, new_id);

        iteration += 1;

        debug_assert!(

            iteration <= lts.num_of_states().max(2),

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

    partition

}

fn signature_refinement_naive<F, L: LTS, const WEAK: bool>(lts: &L, mut signature: F) -> IndexedPartition

where

    F: FnMut(StateIndex, &IndexedPartition, &Vec<Signature<'_>>, &mut SignatureBuilder),

    let mut arena = Bump::new();

    let mut builder = SignatureBuilder::default();

    let mut id: FxHashMap<Signature<'_>, BlockIndex> = FxHashMap::default();

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

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

    let mut state_to_signature: Vec<Signature<'_>> = Vec::new();

    state_to_signature.resize_with(lts.num_of_states(), Signature::default);

    let mut old_count = 1;

    let mut iteration = 0;

    let progress = TimeProgress::new(

    let empty_slice: &[(LabelIndex, BlockIndex)] = &[];

    while old_count != id.len() {

        trace!("Iteration {} ({} blocks)", iteration, id.len());

        old_count = id.len();

        progress.print((iteration, old_count));

        swap(&mut partition, &mut next_partition);

        id.clear();

        state_to_signature.clear();

        state_to_signature.resize_with(lts.num_of_states(), Signature::default);

        let id: &'_ mut FxHashMap<Signature<'_>, BlockIndex> = unsafe { std::mem::transmute(&mut id) };

        let state_to_signature: &mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut state_to_signature) };

        arena.reset();

        if WEAK {

            for state_index in lts.iter_states() {

                weak_bisim_signature_sorted_taus(state_index, lts, &partition, state_to_signature, &mut builder);

                trace!("State {state_index} weak signature {:?}", builder);

                let slice = if builder.is_empty() {

                    arena.alloc_slice_copy(&builder)

                state_to_signature[state_index] = Signature::new(slice);

        }

        for state_index in lts.iter_states() {

            signature(state_index, &partition, state_to_signature, &mut builder);

            trace!("State {state_index} signature {builder:?}");

            let mut new_id = BlockIndex::new(id.len());

            if let Some((signature, index)) = id.get_key_value(&Signature::new(&builder)) {

                // SAFETY: We know that the signature lives as long as the arena

                state_to_signature[state_index] = unsafe {

                    std::mem::transmute::<Signature<'_>, Signature<'_>>(Signature::new(signature.as_slice()))

                };

                new_id = *index;

            } else {

                let slice = if builder.is_empty() {

                    empty_slice

                    arena.alloc_slice_copy(&builder)

                id.insert(Signature::new(slice), new_id);

                state_to_signature[state_index] = Signature::new(slice);

            next_partition.set_block(*state_index, new_id);

        iteration += 1;

        debug_assert!(

            iteration <= lts.num_of_states().max(2),

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

    debug_assert!(

        is_valid_refinement(lts, &partition, |state_index, partition, builder| signature(

            state_index,

            partition,

            &state_to_signature,

            builder

    partition

}

pub fn is_valid_refinement<F, P, L>(lts: &L, partition: &P, mut compute_signature: F) -> bool

where

    F: FnMut(StateIndex, &P, &mut SignatureBuilder),

    P: Partition,

    L: LTS,

    let mut block_to_signature: Vec<Option<SignatureBuilder>> = vec![None; partition.num_of_blocks()];

    let mut builder = SignatureBuilder::default();

    for state_index in lts.iter_states() {

        let block = partition.block_number(state_index);

        compute_signature(state_index, partition, &mut builder);

        let signature: Vec<(LabelIndex, BlockIndex)> = builder.clone();

        if let Some(block_signature) = &block_to_signature[block] {

            if signature != *block_signature {

            }

        } else {

            block_to_signature[block] = Some(signature);

        };

    let mut signature_to_block: FxHashMap<Signature, usize> = FxHashMap::default();

    for (block_index, signature) in block_to_signature

        .iter()

        .map(|signature: &Option<SignatureBuilder>| signature.as_ref().expect("Signature should be defined"))

        .enumerate()

        if let Some(other_block_index) = signature_to_block.get(&Signature::new(signature)) {

        } else {

            signature_to_block.insert(Signature::new(signature), block_index);

        }

    true

}

    fn equal_partitions<P: Partition, Q: Partition>(left: &P, right: &Q) -> bool {

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

            let mut other_block_index = None;

            for state_index in (0..left.len())

                .map(StateIndex::new)

                .filter(|&state_index| left.block_number(state_index) == block_index)

                match other_block_index {

                    None => other_block_index = Some(right.block_number(state_index)),

                    Some(other_block_index) => {

                        if right.block_number(state_index) != other_block_index {

                        }

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

            let mut other_block_index = None;

            for state_index in (0..left.len())

                .map(StateIndex::new)

                .filter(|&state_index| right.block_number(state_index) == block_index)

                match other_block_index {

                    None => other_block_index = Some(left.block_number(state_index)),

                    Some(other_block_index) => {

                        if left.block_number(state_index) != other_block_index {

                        }

        true

    }

    fn is_refinement<L: LTS, P: Partition, Q: Partition>(lts: &L, strong_partition: &P, branching_partition: &Q) {

        for state_index in lts.iter_states() {

            for other_state_index in lts.iter_states() {

                if strong_partition.block_number(state_index) == strong_partition.block_number(other_state_index) {

                    assert_eq!(

                        branching_partition.block_number(state_index),

                        branching_partition.block_number(other_state_index),

                }

    }

        random_test(100, |rng| {

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

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

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

            let mut timing = Timing::new();

            let (result_lts, result_partition) = strong_bisim_sigref(lts.clone(), &mut timing);

            let (expected_lts, expected_partition) = strong_bisim_sigref_naive(lts, &mut timing);

            files

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

                .unwrap();

            files

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

                .unwrap();

            assert!(equal_partitions(&result_partition, &expected_partition));

        });

        random_test(100, |rng| {

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

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

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

            let mut timing = Timing::new();

            let (result_lts, _, result_partition) = branching_bisim_sigref(lts.clone(), StateIndex::new(0), &mut timing);

            let (expected_lts, _, expected_partition) = branching_bisim_sigref_naive(lts, StateIndex::new(0), &mut timing);

            files

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

                .unwrap();

            files

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

                .unwrap();

            assert!(equal_partitions(&result_partition, &expected_partition));

        });

        random_test(100, |rng| {

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

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

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

            let mut timing = Timing::new();

            let (result_lts, _, result_partition) = weak_bisim_sigref_naive(lts.clone(), StateIndex::new(0), false, &mut timing);

            let (expected_lts, _, expected_partition) = weak_bisim_sigref_inductive_naive(lts, StateIndex::new(0), false, &mut timing);

            files

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

                .unwrap();

            files

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

                .unwrap();

            assert!(equal_partitions(&result_partition, &expected_partition));

        });

        random_test(100, |rng| {

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

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

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

            let mut timing = Timing::new();

            let (preprocessed_lts, _, branching_partition) = branching_bisim_sigref_naive(lts, StateIndex::new(0), &mut timing);

            files

                .dump("preprocessed.aut", |writer| write_aut(writer, &preprocessed_lts))

                .unwrap();

            let strong_partition = strong_bisim_sigref_naive(preprocessed_lts.clone(), &mut timing).1;

            is_refinement(&preprocessed_lts, &strong_partition, &branching_partition);

        });

        random_test(100, |rng| {

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

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

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

            let mut timing = Timing::new();

            let (preprocessed_lts, _, weak_partition) = weak_bisim_sigref_naive(lts, StateIndex::new(0), false, &mut timing);

            files

                .dump("preprocessed.aut", |writer| write_aut(writer, &preprocessed_lts))

                .unwrap();

            let (_, _, branching_partition) = branching_bisim_sigref_naive(preprocessed_lts.clone(), StateIndex::new(0), &mut timing);

            is_refinement(&preprocessed_lts, &branching_partition, &weak_partition);

        });