apartness.rs 3.58 KB
Newer Older
1
2
3
4
5
6
use crate::{
    automatadefs::{
        mealy::{InputSymbol, Mealy, State},
        traits::{FiniteStateMachine, ObservationTree},
    },
    util::toolbox,
7
};
8
use itertools::Itertools;
Bharat's avatar
Bharat committed
9
use std::collections::VecDeque;
10

11
12
13
14
15
16
17
/// 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,
18
19
    first_state: State,
    second_state: State,
20
) -> Option<Vec<InputSymbol>> {
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
21
    let input_alphabet = toolbox::inputs_iterator(obs_tree.input_size()).collect_vec();
Bharat Garhewal's avatar
Bharat Garhewal committed
22
23
    // We begin with the pair for which we want to compute the relation,
    // the pair is considered to be the "initial state".
24
    let mut work_list = VecDeque::from([(first_state, second_state)]);
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
25
    while let Some((fst, snd)) = work_list.pop_front() {
Bharat Garhewal's avatar
Bharat Garhewal committed
26
        // Immediate return of None is safe, work_list will never be empty here.
27
28
29
30
31
32
33
        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)),
            )
        }) {
34
35
            let (fst_o, fst_d) = fst_o_d;
            let (snd_o, snd_d) = snd_o_d;
36
37
            if fst_o == snd_o {
                work_list.push_back((fst_d, snd_d));
Bharat Garhewal's avatar
Bharat Garhewal committed
38
            } else {
39
                let access_seq = obs_tree.get_transfer_seq(fst, first_state);
Bharat Garhewal's avatar
Bharat Garhewal committed
40
41
                let mut wit = Vec::with_capacity(access_seq.len() + 1);
                wit.extend_from_slice(&access_seq);
42
43
                wit.push(input);
                return Some(wit);
Bharat Garhewal's avatar
Bharat Garhewal committed
44
45
46
            }
        }
    }
47
    None // no witness!
Bharat Garhewal's avatar
Bharat Garhewal committed
48
}
49

Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
50
51
#[inline]
#[must_use]
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
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
}

Bharat's avatar
Bharat committed
75
/// `true` if states are apart.
76
77
78
79
80
81
82
83
84
///
/// 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 {
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
85
    let input_alphabet = toolbox::inputs_iterator(obs_tree.input_size()).collect_vec();
86
87
88
    // 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)]);
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
89
    while let Some((fst, snd)) = work_list.pop_front() {
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
        // 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
}