pub fn strong_bisim_sigref(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition {

    let mut timepre = timing.start("preprocess");

    let incoming = IncomingTransitions::new(lts);

    timepre.finish();

    let mut time = timing.start("reduction");

    let partition = signature_refinement::<_, _, false>(lts, &incoming, |state_index, partition, _, builder| {

        strong_bisim_signature(state_index, lts, partition, builder);

    }, |_, _| { None });

    debug_assert_eq!(

        strong_bisim_sigref_naive(lts, timing),

    time.finish();

    partition.into()

}

pub fn strong_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition {

    let mut time = timing.start("reduction");

    let partition = signature_refinement_naive(lts, |state_index, partition, _, builder| {

        strong_bisim_signature(state_index, lts, partition, builder);

    });

    time.finish();

    partition

}

pub fn branching_bisim_sigref(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition {

    let mut timepre = timing.start("preprocess");

    let (preprocessed_lts, preprocess_partition) = preprocess_branching(lts);

    let incoming = IncomingTransitions::new(&preprocessed_lts);

    timepre.finish();

    let mut time = timing.start("reduction");

    let mut expected_builder = SignatureBuilder::default();

    let mut visited = FxHashSet::default();

    let mut stack = Vec::new();

    let partition =

        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);

            // Compute the expected signature, only used in debugging.

            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 *label == lts.num_of_labels() && key_to_signature[*key].is_subset_of(signature, (*label, *key)) {

                        return Some(*key);

                    }

                    if *label != lts.num_of_labels() {

                        return None;

                    }

                None

        });

    debug_assert_eq!(

        signature_refinement_naive(&preprocessed_lts, |state_index, partition, _, builder| {

            branching_bisim_signature(

                state_index,

                &preprocessed_lts,

                partition,

                builder,

                &mut visited,

                &mut stack,

            );

        }),

    time.finish();

    // Combine the SCC partition with the branching bisimulation partition.

    let combined_partition = combine_partition(preprocess_partition, &partition);

    trace!("Final partition {combined_partition}");

    combined_partition

}

pub fn branching_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition {

    let mut timepre = timing.start("preprocess");

    let (preprocessed_lts, preprocess_partition) = preprocess_branching(lts);

    timepre.finish();

    let mut time = timing.start("reduction");

    let mut expected_builder = SignatureBuilder::default();

    let mut visited = FxHashSet::default();

    let mut stack = Vec::new();

    let partition = signature_refinement_naive(

        &preprocessed_lts,

        |state_index, partition, state_to_signature, builder| {

            branching_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder);

            // Compute the expected signature, only used in debugging.

            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(),

        },

    );

    time.finish();

    // Combine the SCC partition with the branching bisimulation partition.

    let combined_partition = combine_partition(preprocess_partition, &partition);

    trace!("Final partition {combined_partition}");

    combined_partition

}

fn signature_refinement<F, G, const BRANCHING: bool>(lts: &LabelledTransitionSystem, incoming: &IncomingTransitions, 

    mut signature: F,

    mut renumber: G) -> BlockPartition

where

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

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

{

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

    let mut arena = Bump::new();

    let mut builder = SignatureBuilder::default();

    let mut split_builder = BlockPartitionBuilder::default();

    // Put all the states in the initial partition { S }.

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

    // Assigns the signature to each state.

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

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

    state_to_key.resize_with(lts.num_of_states(), usize::default);

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

    // Refine partitions until stable.

    let mut iteration = 0usize;

    let mut num_of_blocks;

    let mut states = Vec::new();

    // Used to keep track of dirty blocks.

    let mut worklist = vec![0];

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

        id.clear();

        // Removes the existing signatures.

        key_to_signature.clear();

        arena.reset();

        num_of_blocks = partition.num_of_blocks();

        let block = partition.block(block_index);

        debug_assert!(

            block.has_marked(),

        if BRANCHING {

            partition.mark_backward_closure(block_index, incoming);

        }

        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((_, index)) = id.get_key_value(&Signature::new(&builder)) {

                    state_to_key[state_index] = *index;

                    *index

                    let slice = arena.alloc_slice_copy(&builder);

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

                        key

                        let result = key_to_signature.len();

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

                        result

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

                    // (branching)  Keep track of the signature for every block in the next partition.

                    state_to_key[state_index] = number;

                    number

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

                index

            })

            if block_index != new_block_index {

                states.clear();

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

                for &state_index in &states {

                    for &(label_index, incoming_state) in incoming.incoming_transitions(state_index) {

                        if BRANCHING {

                            if !lts.is_hidden_label(label_index)

                                || partition.block_number(incoming_state) != partition.block_number(state_index)

                                let other_block = partition.block_number(incoming_state);

                                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(incoming_state);

                            }

                            let other_block = partition.block_number(incoming_state);

                            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(incoming_state);

            }

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

        iteration += 1;

        if num_of_blocks != partition.num_of_blocks() {

            debug!("Iteration {iteration}, found {} blocks", partition.num_of_blocks());

        }

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

    partition

}

fn signature_refinement_naive<F>(lts: &LabelledTransitionSystem, mut signature: F) -> IndexedPartition

where

    F: FnMut(usize, &IndexedPartition, &Vec<Signature>, &mut SignatureBuilder),

{

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

    let mut arena = Bump::new();

    let mut builder = SignatureBuilder::default();

    // Put all the states in the initial partition { S }.

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

    // Assigns the signature to each state.

    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);

    // Refine partitions until stable.

    let mut old_count = 1;

    let mut iteration = 0;

    while old_count != id.len() {

        old_count = id.len();

        debug!("Iteration {iteration}, found {old_count} blocks");

        swap(&mut partition, &mut next_partition);

        // Clear the current partition to start the next blocks.

        id.clear();

        // Remove the current signatures.

        arena.reset();

        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 = id.len();

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

                state_to_signature[state_index] = Signature::new(signature.as_slice());

                new_id = *index;

            } else {

                let slice = arena.alloc_slice_copy(&builder);

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

                // (branching) Keep track of the signature for every block in the next partition.

                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>(lts: &LabelledTransitionSystem, partition: &P, mut compute_signature: F) -> bool

where

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

    P: Partition,

{

    // Check that the partition is indeed stable and as such is a quotient of strong bisimulation

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

    // Avoids reallocations when computing the signature.

    let mut builder = SignatureBuilder::default();

    for state_index in lts.iter_states() {

        let block = partition.block_number(state_index);

        // Compute the flat signature, which has Hash and is more compact.

        compute_signature(state_index, partition, &mut builder);

        let signature: Vec<(usize, usize)> = 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| signature.as_ref().unwrap())

        .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

}

    #[test]

    fn is_refinement(

        lts: &LabelledTransitionSystem,

        strong_partition: &impl Partition,

        branching_partition: &impl Partition,

    ) {

        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),

                }

    }

    #[test]

    #[test]