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
            

            

                
            

            

                
///

            

        

            

                10
            

            

                
            

            

                
/// This runs a relaxation fixpoint that re-scans every tau-edge until no length

            

        

            

                11
            

            

                
            

            

                
/// changes, so it is `O(states * transitions)` in the worst case. A single pass

            

        

            

                12
            

            

                
            

            

                
/// suffices when the states are topologically sorted on tau-transitions.

            

        

            

                13
            

            

                
            

            

                
pub fn longest_tau_path<L: LTS>(lts: &L) -> Vec<StateIndex> {

            

        

            

                14
            

            

                
            

            

                
    let mut length = vec![0usize; lts.num_of_states()];

            

        

            

                15
            

            

                
            

            

                
    let mut next = vec![None; lts.num_of_states()];

            

        

            

                16
            

            

                
            

            

                

            

        

            

                17
            

            

                
            

            

                
    loop {

            

        

            

                18
            

            

                
            

            

                
        // For topologically sorted states, a single pass is sufficient, but this generalises to any order.

            

        

            

                19
            

            

                
            

            

                
        let mut changed = false;

            

        

            

                20
            

            

                
            

            

                

            

        

            

                21
            

            

                
            

            

                
        for state in lts.iter_states() {

            

        

            

                22
            

            

                
            

            

                
            for transition in lts

            

        

            

                23
            

            

                
            

            

                
                .outgoing_transitions(state)

            

        

            

                24
            

            

                
            

            

                
                .filter(|transition| lts.is_hidden_label(transition.label))

            

        

            

                25
            

            

                
            

            

                
            {

            

        

            

                26
            

            

                
            

            

                
                let new_length = length[transition.to] + 1;

            

        

            

                27
            

            

                
            

            

                
                if new_length > length[state] {

            

        

            

                28
            

            

                
            

            

                
                    length[state] = new_length;

            

        

            

                29
            

            

                
            

            

                
                    next[state] = Some(transition.to);

            

        

            

                30
            

            

                
            

            

                
                    changed = true;

            

        

            

                31
            

            

                
            

            

                
                }

            

        

            

                32
            

            

                
            

            

                
            }

            

        

            

                33
            

            

                
            

            

                
        }

            

        

            

                34
            

            

                
            

            

                

            

        

            

                35
            

            

                
            

            

                
        if !changed {

            

        

            

                36
            

            

                
            

            

                
            break;

            

        

            

                37
            

            

                
            

            

                
        }

            

        

            

                38
            

            

                
            

            

                
    }

            

        

            

                39
            

            

                
            

            

                

            

        

            

                40
            

            

                
            

            

                
    // Find the state with the longest path

            

        

            

                41
            

            

                
            

            

                
    let (max_state, &max_length) = length

            

        

            

                42
            

            

                
            

            

                
        .iter()

            

        

            

                43
            

            

                
            

            

                
        .enumerate()

            

        

            

                44
            

            

                
            

            

                
        .max_by_key(|(_, len)| **len)

            

        

            

                45
            

            

                
            

            

                
        .unwrap_or((0, &0));

            

        

            

                46
            

            

                
            

            

                

            

        

            

                47
            

            

                
            

            

                
    // Reconstruct the path

            

        

            

                48
            

            

                
            

            

                
    let mut path = Vec::with_capacity(max_length + 1);

            

        

            

                49
            

            

                
            

            

                
    let mut current = StateIndex::new(max_state);

            

        

            

                50
            

            

                
            

            

                
    path.push(current);

            

        

            

                51
            

            

                
            

            

                

            

        

            

                52
            

            

                
            

            

                
    while let Some(next_state) = next[current] {

            

        

            

                53
            

            

                
            

            

                
        path.push(next_state);

            

        

            

                54
            

            

                
            

            

                
        current = next_state;

            

        

            

                55
            

            

                
            

            

                
    }

            

        

            

                56
            

            

                
            

            

                

            

        

            

                57
            

            

                
            

            

                
    path

            

        

            

                58
            

            

                
            

            

                
}