apartness.rs

use crate::{
    automatadefs::{
        mealy::{InputSymbol, Mealy, State},
        traits::{FiniteStateMachine, ObservationTree},
    },
    util::toolbox,
};
use itertools::Itertools;
use std::collections::VecDeque;

/// Provides a witness between the two states, if one exists.
///
/// If witness is not needed, use [`states_are_apart`].
#[inline]
#[must_use]
pub fn compute_witness<Tree: ObservationTree>(
    obs_tree: &Tree,
    first_state: State,
    second_state: State,
) -> Option<Vec<InputSymbol>> {
    let input_alphabet = toolbox::inputs_iterator(obs_tree.input_size()).collect_vec();
    // We begin with the pair for which we want to compute the relation,
    // the pair is considered to be the "initial state".
    let mut work_list = VecDeque::from([(first_state, second_state)]);
    while let Some((fst, snd)) = work_list.pop_front() {
        // Immediate return of None is safe, work_list will never be empty here.
        for (input, (fst_o_d, snd_o_d)) in input_alphabet.iter().filter_map(|&input| {
            Some(input).zip(
                obs_tree
                    .get_out_succ(fst, input)
                    .zip(obs_tree.get_out_succ(snd, input)),
            )
        }) {
            let (fst_o, fst_d) = fst_o_d;
            let (snd_o, snd_d) = snd_o_d;
            if fst_o == snd_o {
                work_list.push_back((fst_d, snd_d));
            } else {
                let access_seq = obs_tree.get_transfer_seq(fst, first_state);
                let mut wit = Vec::with_capacity(access_seq.len() + 1);
                wit.extend_from_slice(&access_seq);
                wit.push(input);
                return Some(wit);
            }
        }
    }
    None // no witness!
}

#[inline]
#[must_use]
pub fn tree_and_hyp_states_apart<Tree: ObservationTree>(
    obs_tree: &Tree,
    tree_state: State,
    hyp_state: State,
    fsm: &Mealy,
) -> bool {
    let input_size = fsm.input_alphabet().len();
    let mut work_list = VecDeque::from([(tree_state, hyp_state)]);
    while let Some((ts, hs)) = work_list.pop_front() {
        for i in toolbox::inputs_iterator(input_size) {
            let tree_hyp_next_pair = obs_tree.get_out_succ(ts, i).zip(Some(fsm.step_from(hs, i)));
            if let Some(((out_t, dest_t), (dest_h, out_h))) = tree_hyp_next_pair {
                if out_h == out_t {
                    work_list.push_back((dest_t, dest_h));
                } else {
                    return true;
                }
            }
        }
    }
    false
}

/// `true` if states are apart.
///
/// If a witness is needed, use [`compute_witness`].
#[inline]
#[must_use]
pub fn states_are_apart<Tree: ObservationTree>(
    obs_tree: &Tree,
    first_state: State,
    second_state: State,
) -> bool {
    let input_alphabet = toolbox::inputs_iterator(obs_tree.input_size()).collect_vec();
    // We begin with the pair for which we want to compute the relation,
    // the pair is considered to be the "initial state".
    let mut work_list = VecDeque::from([(first_state, second_state)]);
    while let Some((fst, snd)) = work_list.pop_front() {
        // Immediate return of None is safe, work_list will never be empty here.
        for (fst_o_d, snd_o_d) in input_alphabet.iter().filter_map(|&input| {
            obs_tree
                .get_out_succ(fst, input)
                .zip(obs_tree.get_out_succ(snd, input))
        }) {
            let (fst_o, fst_d) = fst_o_d;
            let (snd_o, snd_d) = snd_o_d;
            if fst_o == snd_o {
                work_list.push_back((fst_d, snd_d));
            } else {
                return true;
            }
        }
    }
    false
}