Grcov report - scc_decomposition.rs

1

#![forbid(unsafe_code)]

2

3

use merc_collections::IndexedPartition;

4

5

use merc_collections::scc_decomposition;

6

use merc_lts::LTS;

7

use merc_lts::AsGraph;

8

9

use crate::sort_topological;

10

11

/// Computes the strongly connected tau component partitioning of the given LTS.

12

1101

pub fn tau_scc_decomposition(lts: &impl LTS) -> IndexedPartition {

13

19675

    scc_decomposition(&AsGraph(lts), |_, label_index, _| lts.is_hidden_label(label_index))

14

1101

15

16

/// Returns true iff the labelled transition system has tau-loops.

17

100

pub fn has_tau_loop(lts: &impl LTS) -> bool {

18

3116

    sort_topological(lts, |label_index, _| lts.is_hidden_label(label_index), false).is_err()

19

100

20

21

#[cfg(test)]

22

mod tests {

23

    use merc_io::DumpFiles;

24

    use merc_lts::random_lts;

25

    use merc_lts::write_aut;

26

    use merc_lts::LabelIndex;

27

    use merc_lts::LabelledTransitionSystem;

28

    use merc_lts::StateIndex;

29

    use merc_utilities::random_test;

30

    use test_log::test;

31

32

    use crate::quotient_lts_naive;

33

    use crate::Partition;

34

35

    use super::*;

36

37

    /// Returns the reachable states from the given state index.

38

920

    fn reachable_states(

39

920

        lts: &impl LTS,

40

920

        state_index: StateIndex,

41

920

        filter: &impl Fn(StateIndex, LabelIndex, StateIndex) -> bool,

42

920

    ) -> Vec<usize> {

43

920

        let mut stack = vec![state_index];

44

920

        let mut visited = vec![false; lts.num_of_states()];

45

46

        // Depth first search to find all reachable states.

47

12952

        while let Some(inner_state_index) = stack.pop() {

48

25787

            for transition in lts.outgoing_transitions(inner_state_index) {

49

25787

                if filter(inner_state_index, LabelIndex::new(0), transition.to) && !visited[transition.to.value()] {

50

11112

                    visited[transition.to.value()] = true;

51

11112

                    stack.push(transition.to);

52

14675

53

54

55

56

        // All the states that were visited are reachable.

57

920

        visited

58

920

            .into_iter()

59

920

            .enumerate()

60

31020

            .filter_map(|(index, visited)| if visited { Some(index) } else { None })

61

920

            .collect()

62

920

63

64

    #[test]

65

    #[cfg_attr(miri, ignore)]

66

    fn test_random_tau_scc_decomposition() {

67

100

        random_test(100, |rng| {

68

100

            let mut files = DumpFiles::new("test_random_tau_scc_decomposition");

69

70

100

            let lts = random_lts(rng, 10, 3, 3);

71

100

            files.dump("input.aut", |f| write_aut(f, &lts)).unwrap();

72

73

100

            let partitioning = tau_scc_decomposition(&lts);

74

100

            let reduction = quotient_lts_naive(&lts, &partitioning, true);

75

100

            assert!(!has_tau_loop(&reduction), "The SCC decomposition contains tau-loops");

76

77

100

            files

78

100

                .dump("tau_scc_decomposition.aut", |f| write_aut(f, &reduction))

79

100

                .unwrap();

80

81

            // Check that states in a strongly connected component are reachable from each other.

82

920

            for state_index in lts.iter_states() {

83

25787

                let reachable = reachable_states(&lts, state_index, &|_, label, _| lts.is_hidden_label(label));

84

85

                // All other states in the same block should be reachable.

86

920

                let block = partitioning.block_number(state_index);

87

88

920

                for other_state_index in lts

89

920

                    .iter_states()

90

31020

                    .filter(|index| state_index != *index && partitioning.block_number(*index) == block)

91

92

132

                    assert!(

93

132

                        reachable.contains(&other_state_index),

94

                        "State {state_index} and {other_state_index} should be connected"

95

);

96

97

98

99

100

            assert!(

100

                reduction.num_of_states() == tau_scc_decomposition(&reduction).num_of_blocks(),

101

                "Applying SCC decomposition again should yield the same number of SCC after second application"

102

);

103

100

});

104

105

106

    #[test]

107

    fn test_cycles() {

108

        let transitions = [(0, 0, 2), (0, 0, 4), (1, 0, 0), (2, 0, 1), (2, 0, 0)]

109

5

            .map(|(from, label, to)| (StateIndex::new(from), LabelIndex::new(label), StateIndex::new(to)));

110

111

        let lts = LabelledTransitionSystem::new(

112

            StateIndex::new(0),

113

            None,

114

2

            || transitions.iter().cloned(),

115

            vec!["tau".to_string(), "a".to_string()],

116

);

117

118

        let _ = tau_scc_decomposition(&lts);

119

120