1
use merc_lts::LTS;
2
use merc_lts::StateIndex;
3

            
4
/// Computes the length of the longest path consisting solely of tau (hidden) transitions in the given LTS.
5
///
6
/// # Details
7
///
8
/// Assumes that the LTS does not contain any tau-cycles.
9
pub fn longest_tau_path<L: LTS>(lts: &L) -> Vec<StateIndex> {
10
    let mut length = vec![0usize; lts.num_of_states()];
11
    let mut next = vec![None; lts.num_of_states()];
12

            
13
    loop {
14
        // For topologically sorted states, a single pass is sufficient, but this generalises to any order.
15
        let mut changed = false;
16

            
17
        for state in lts.iter_states() {
18
            for transition in lts
19
                .outgoing_transitions(state)
20
                .filter(|transition| lts.is_hidden_label(transition.label))
21
            {
22
                let new_length = length[transition.to] + 1;
23
                if new_length > length[state] {
24
                    length[state] = new_length;
25
                    next[state] = Some(transition.to);
26
                    changed = true;
27
                }
28
            }
29
        }
30

            
31
        if !changed {
32
            break;
33
        }
34
    }
35

            
36
    // Find the state with the longest path
37
    let (max_state, &max_length) = length
38
        .iter()
39
        .enumerate()
40
        .max_by_key(|(_, len)| **len)
41
        .unwrap_or((0, &0));
42

            
43
    // Reconstruct the path
44
    let mut path = Vec::with_capacity(max_length + 1);
45
    let mut current = StateIndex::new(max_state);
46
    path.push(current);
47

            
48
    while let Some(next_state) = next[current] {
49
        path.push(next_state);
50
        current = next_state;
51
    }
52

            
53
    path
54
}