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::AsGraph;

7

use merc_lts::LTS;

8

9

use crate::sort_topological;

10

11

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

12

2801

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

13

567488

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

14

2801

15

16

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

17

100

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

18

3934

    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::LabelIndex;

25

    use merc_lts::LabelledTransitionSystem;

26

    use merc_lts::StateIndex;

27

    use merc_lts::random_lts;

28

    use merc_lts::write_aut;

29

    use merc_utilities::random_test;

30

    use test_log::test;

31

32

    use crate::Partition;

33

    use crate::quotient_lts_naive;

34

35

    use super::LTS;

36

    use super::has_tau_loop;

37

    use super::tau_scc_decomposition;

38

39

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

40

1118

    fn reachable_states<F, L>(lts: &L, state_index: StateIndex, filter: &F) -> Vec<usize>

41

1118

    where

42

1118

        F: Fn(StateIndex, LabelIndex, StateIndex) -> bool,

43

1118

        L: LTS,

44

45

1118

        let mut stack = vec![state_index];

46

1118

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

47

48

        // Depth first search to find all reachable states.

49

14995

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

50

26028

            for transition in lts.outgoing_transitions(inner_state_index) {

51

26028

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

52

12759

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

53

12759

                    stack.push(transition.to);

54

13269

55

56

57

58

        // All the states that were visited are reachable.

59

1118

        visited

60

1118

            .into_iter()

61

1118

            .enumerate()

62

43950

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

63

1118

            .collect()

64

1118

65

66

    #[test]

67

    #[cfg_attr(miri, ignore)]

68

    fn test_random_tau_scc_decomposition() {

69

100

        random_test(100, |rng| {

70

100

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

71

72

100

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

73

100

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

74

75

100

            let partitioning = tau_scc_decomposition(&lts);

76

100

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

77

100

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

78

79

100

            files

80

100

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

81

100

                .unwrap();

82

83

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

84

1118

            for state_index in lts.iter_states() {

85

26028

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

86

87

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

88

1118

                let block = partitioning.block_number(state_index);

89

90

1118

                for other_state_index in lts

91

1118

                    .iter_states()

92

43950

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

93

94

62

                    assert!(

95

62

                        reachable.contains(&other_state_index),

96

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

97

);

98

99

100

101

100

            assert!(

102

100

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

103

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

104

);

105

100

});

106

107

108

    #[test]

109

    fn test_cycles() {

110

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

111

5

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

112

113

        let lts = LabelledTransitionSystem::new(

114

            StateIndex::new(0),

115

            None,

116

2

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

117

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

118

);

119

120

        let _ = tau_scc_decomposition(&lts);

121

122