pub fn new(slice: &[(usize, usize)]) -> Signature {

        Signature(slice)

    }

    pub fn as_slice(&self) -> &[(usize, usize)] {

        unsafe { &*self.0 }

    }

    pub fn is_subset_of(&self, other: &[(usize, usize)], exclude: (usize, usize)) -> bool {

        let mut self_iter = self.as_slice().iter();

        let mut other_iter = other.iter().filter(|&&x| x != exclude);

        let mut self_item: Option<&(usize, usize)> = self_iter.next();

        let mut other_item = other_iter.next();

        while let Some(&o) = other_item {

            match self_item {

                Some(&s) if s == o => {

                    // Match found, move both iterators forward

                    self_item = self_iter.next();

                    other_item = other_iter.next();

                }

                Some(&s) if s < o => {

                    // Move only self iterator forward

                    self_item = self_iter.next();

                }

                    return false;

        true

    }

    fn default() -> Self {

        Signature(&[])

    }

    fn eq(&self, other: &Self) -> bool {

        self.as_slice() == other.as_slice()

    }

    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {

        unsafe { (*self.0).hash(state) }

    }

pub fn strong_bisim_signature(

    state_index: StateIndex,

    lts: &LabelledTransitionSystem,

    partition: &impl Partition,

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    for (label, to) in lts.outgoing_transitions(state_index) {

        builder.push((*label, partition.block_number(*to)));

    }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature(

    state_index: StateIndex,

    lts: &LabelledTransitionSystem,

    partition: &impl Partition,

    builder: &mut SignatureBuilder,

    visited: &mut FxHashSet<usize>,

    stack: &mut Vec<usize>,

) {

    // Clear the builders and the list of visited states.

    builder.clear();

    visited.clear();

    // A stack used for depth first search of tau paths.

    debug_assert!(stack.is_empty(), "The stack should be empty");

    stack.push(state_index);

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

        visited.insert(inner_state_index);

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

            if lts.is_hidden_label(*label_index) {

                if partition.block_number(state_index) == partition.block_number(*to_index) {

                    if !visited.contains(to_index) {

                        visited.insert(*to_index);

                        stack.push(*to_index);

                    }

                } else {

                    //  pi(s) != pi(t)

                    builder.push((*label_index, partition.block_number(*to_index)));

                }

            } else {

                // (a != tau) This is a visible action only reachable from tau paths with equal signatures.

                builder.push((*label_index, partition.block_number(*to_index)));

            }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature_sorted(

    state_index: StateIndex,

    lts: &LabelledTransitionSystem,

    partition: &impl Partition,

    state_to_signature: &[Signature],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    for &(label_index, to) in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(to);

        if partition.block_number(state_index) == to_block {

            if lts.is_hidden_label(label_index) {

                // Inert tau transition, take signature from the outgoing tau-transition.

                builder.extend(state_to_signature[to].as_slice());

            } else {

                builder.push((label_index, to_block));

            }

        } else {

            // Visible action, add to the signature.

            builder.push((label_index, to_block));

        }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature_inductive(

    state_index: StateIndex,

    lts: &LabelledTransitionSystem,

    partition: &BlockPartition,

    state_to_key: &[usize],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    let num_act: usize = lts.num_of_labels(); //this label index does not occur.

    for &(label_index, to) in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(to);

        if partition.block_number(state_index) == to_block {

            if lts.is_hidden_label(label_index) && partition.is_element_marked(to) {

                // Inert tau transition, take signature from the outgoing tau-transition.

                builder.push((num_act, state_to_key[to]));

            } else {

                builder.push((label_index, to_block));

            }

        } else {

            // Visible action, add to the signature.

            builder.push((label_index, to_block));

        }

    builder.sort_unstable();

    builder.dedup();

}

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

    let scc_partition = tau_scc_decomposition(lts);

    let tau_loop_free_lts = quotient_lts(lts, &scc_partition, true);

    // Sort the states according to the topological order of the tau transitions.

    let topological_permutation = sort_topological(

        &tau_loop_free_lts,

        |label_index, _| tau_loop_free_lts.is_hidden_label(label_index),

        true,

    )

    .expect("After quotienting, the LTS should not contain cycles");

    (

        reorder_states(&tau_loop_free_lts, |i| topological_permutation[i]),

        reorder_partition(scc_partition, |i| topological_permutation[i]),

    )

}