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_collections::scc_decomposition_iterative;

7

use merc_lts::AsGraph;

8

use merc_lts::LTS;

9

10

use crate::sort_topological;

11

12

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

13

402

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

14

311935

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

15

402

16

17

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

18

5203

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

19

1670126

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

20

5203

21

22

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

23

100

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

24

199904

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

25

100

26

27

#[cfg(test)]

28

mod tests {

29

    use merc_io::DumpFiles;

30

    use merc_lts::LabelIndex;

31

    use merc_lts::LabelledTransitionSystem;

32

    use merc_lts::StateIndex;

33

    use merc_lts::TransitionLabel;

34

    use merc_lts::random_lts;

35

    use merc_lts::reachability;

36

    use merc_lts::write_aut;

37

    use merc_utilities::random_test;

38

    use test_log::test;

39

40

    use crate::Partition;

41

    use crate::quotient_lts_naive;

42

43

    use super::LTS;

44

    use super::has_tau_loop;

45

    use super::tau_scc_decomposition;

46

    use super::tau_scc_decomposition_iterative;

47

48

    /// Returns all states reachable from `state_index` via transitions accepted by `filter`.

49

100000

    fn reachable_states<L: LTS>(

50

100000

        lts: &L,

51

100000

        state_index: StateIndex,

52

100000

        filter: impl Fn(LabelIndex) -> bool,

53

100000

    ) -> Vec<StateIndex> {

54

100000

        let mut result = Vec::new();

55

149941

        reachability(lts, state_index, filter, |s| result.push(s));

56

100000

        result

57

100000

58

59

    #[test]

60

    #[cfg_attr(miri, ignore)]

61

    fn test_random_tau_scc_decomposition() {

62

100

        random_test(100, |rng| {

63

100

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

64

65

100

            let lts = random_lts::<String, _>(rng, 1000, 3);

66

100

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

67

68

100

            let partitioning = tau_scc_decomposition(&lts);

69

100

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

70

100

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

71

72

100

            files

73

100

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

74

100

                .unwrap();

75

76

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

77

100000

            for state_index in lts.iter_states() {

78

150219

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

79

80

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

81

100000

                let block = partitioning.block_number(state_index);

82

83

100000

                for other_state_index in lts

84

100000

                    .iter_states()

85

100000000

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

86

87

38

                    assert!(

88

38

                        reachable.contains(&other_state_index),

89

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

90

);

91

92

93

94

100

            assert!(

95

100

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

96

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

97

);

98

100

});

99

100

101

    #[test]

102

    #[cfg_attr(miri, ignore)]

103

    fn test_random_tau_scc_decomposition_compare_iterative() {

104

100

        random_test(100, |rng| {

105

100

            let lts = random_lts::<String, _>(rng, 1000, 3);

106

107

100

            let partition_recursive = tau_scc_decomposition(&lts);

108

100

            let partition_iterative = tau_scc_decomposition_iterative(&lts);

109

110

100

            assert_eq!(

111

100

                partition_recursive.num_of_blocks(),

112

100

                partition_iterative.num_of_blocks(),

113

                "Both algorithms should find the same number of SCCs"

114

);

115

116

            // Both partitions must agree on which pairs of states belong to the same SCC.

117

100000

            for s in lts.iter_states() {

118

100000000

                for t in lts.iter_states() {

119

100000000

                    let same_recursive = partition_recursive.block_number(s) == partition_recursive.block_number(t);

120

100000000

                    let same_iterative = partition_iterative.block_number(s) == partition_iterative.block_number(t);

121

100000000

                    assert_eq!(

122

                        same_recursive, same_iterative,

123

                        "States {s} and {t} should be in the same SCC in both algorithms"

124

);

125

126

127

100

});

128

129

130

    #[test]

131

    fn test_cycles() {

132

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

133

5

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

134

135

        let lts = LabelledTransitionSystem::new(

136

            StateIndex::new(0),

137

            None,

138

2

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

139

            vec![String::tau_label(), "a".to_string()],

140

);

141

142

        let _ = tau_scc_decomposition(&lts);

143

144