pub fn new(slice: &'a [(LabelIndex, BlockIndex)]) -> Signature<'a> {

        Signature(slice)

    }

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

        self.0

    }

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

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

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

        let mut self_item = 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: Hasher>(&self, state: &mut H) {

        self.as_slice().hash(state)

    }

pub fn is_tau_hat<L: LTS>(label: LabelIndex, lts: &L) -> bool {

    label == lts.num_of_labels()

}

fn tau_hat<L: LTS>(lts: &L) -> LabelIndex {

    LabelIndex::new(lts.num_of_labels())

}

pub fn strong_bisim_signature<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    for transition in lts.outgoing_transitions(state_index) {

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

    }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    builder: &mut SignatureBuilder,

    visited: &mut FxHashSet<StateIndex>,

    stack: &mut Vec<StateIndex>,

) {

    builder.clear();

    visited.clear();

    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 transition in lts.outgoing_transitions(inner_state_index) {

            if lts.is_hidden_label(transition.label) {

                if partition.block_number(state_index) == partition.block_number(transition.to) {

                    if !visited.contains(&transition.to) {

                        visited.insert(transition.to);

                        stack.push(transition.to);

                    }

                } else {

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

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

                }

            } else {

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

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

            }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature_sorted<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    state_to_signature: &[Signature],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    for transition in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(transition.to);

        if partition.block_number(state_index) == to_block {

            if lts.is_hidden_label(transition.label) {

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

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

            } else {

                builder.push((transition.label, to_block));

            }

        } else {

            // Visible action, add to the signature.

            builder.push((transition.label, to_block));

        }

    builder.sort_unstable();

    builder.dedup();

}

pub fn branching_bisim_signature_inductive<L: LTS>(

    state_index: StateIndex,

    lts: &L,

    partition: &BlockPartition,

    state_to_key: &[BlockIndex],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    for transition in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(transition.to);

        if partition.block_number(state_index) == to_block {

            if lts.is_hidden_label(transition.label) && partition.is_element_marked(transition.to) {

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

                builder.push((tau_hat(lts), state_to_key[transition.to]));

            } else {

                builder.push((transition.label, to_block));

            }

        } else {

            // Visible action, add to the signature.

            builder.push((transition.label, to_block));

        }

    builder.sort_unstable();

    builder.dedup();

}

pub fn weak_bisim_presignature_sorted<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    state_to_taus: &[Signature],

    state_to_key: &[Option<usize>],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

    for transition in lts.outgoing_transitions(state_index) {

        if lts.is_hidden_label(transition.label) {

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

            builder.push((tau_hat(lts), BlockIndex::new(state_to_key[transition.to].unwrap())));

        } else {

            for (label_after, color) in state_to_taus[transition.to].as_slice() {

                if lts.is_hidden_label(*label_after) {

                    builder.push((transition.label, *color));

                }

    builder.sort_unstable();

    builder.dedup();

}

pub fn weak_bisim_signature_sorted_full<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    state_to_taus: &[Signature],

    state_to_signature: &[Option<usize>],

    key_to_signature: &[Signature],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

    for transition in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(transition.to);

        if lts.is_hidden_label(transition.label) {

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

            builder.extend(key_to_signature[state_to_signature[transition.to].unwrap()].as_slice());

        } else {

            builder.push((transition.label, to_block));

            for (label_after, color) in state_to_taus[transition.to].as_slice() {

                if lts.is_hidden_label(*label_after) {

                    builder.push((transition.label, *color));

                }

    builder.sort_unstable();

    builder.dedup();

}

pub fn weak_bisim_signature_sorted<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    state_to_signature: &[Signature],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

    for transition in lts.outgoing_transitions(state_index) {

        let to_block = partition.block_number(transition.to);

        if lts.is_hidden_label(transition.label) {

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

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

        } else {

            builder.push((transition.label, to_block));

            for (label_after, color) in state_to_signature[transition.to].as_slice() {

                if lts.is_hidden_label(*label_after) {

                    builder.push((transition.label, *color));

                }

    builder.sort_unstable();

    builder.dedup();

}

pub fn weak_bisim_signature_sorted_taus<L: LTS, P: Partition>(

    state_index: StateIndex,

    lts: &L,

    partition: &P,

    state_to_taus: &[Signature],

    builder: &mut SignatureBuilder,

) {

    builder.clear();

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

    for transition in lts.outgoing_transitions(state_index) {

        if lts.is_hidden_label(transition.label) {

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

            builder.extend(state_to_taus[transition.to].as_slice());

        }

    builder.sort_unstable();

    builder.dedup();

}

pub fn tau_cycle_elimination_and_reorder<L: LTS>(

    lts: L,

    state: StateIndex,

    eliminate_tau_selfloops: bool,

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

    let scc_partition = tau_scc_decomposition_iterative(&lts);

    let tau_loop_free_lts = quotient_lts_naive(&lts, &scc_partition, eliminate_tau_selfloops, eliminate_tau_selfloops);

    let mapped_state = StateIndex::new(*scc_partition.block_number(state));

    drop(lts);

    drop(scc_partition);

    let topological_permutation = sort_topological(

        &tau_loop_free_lts,

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

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

        LabelledTransitionSystem::new_from_permutation(tau_loop_free_lts, |i| topological_permutation[i]),

        topological_permutation[mapped_state],

}