Newer
Older
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, State},
traits::{FiniteStateMachine, ObservationTree},
},
util::toolbox,
/// 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)]);
// 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));
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);
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
}
///
/// 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)]);
// 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
}