Grcov report - product

1

#![forbid(unsafe_code)]

2

3

use std::collections::HashSet;

4

5

use log::trace;

6

7

use merc_collections::IndexedSet;

8

9

use crate::LTS;

10

use crate::LabelledTransitionSystem;

11

use crate::LtsBuilder;

12

use crate::LtsBuilderFast;

13

use crate::StateIndex;

14

use crate::TransitionLabel;

15

16

/// Computes the synchronous product LTS of two given LTSs.

17

///

18

///  If `synchronized_labels` is `None`, then all common labels (except tau) are

19

/// considered synchronized. Otherwise, the provided labels are used for

20

/// synchronization.

21

100

pub fn product_lts<L: LTS, R: LTS<Label = L::Label>>(

22

100

    left: &L,

23

100

    right: &R,

24

100

    synchronized_labels: Option<Vec<L::Label>>,

25

100

) -> LabelledTransitionSystem<L::Label> {

26

    // Determine the combination of action labels

27

100

    let mut all_labels: IndexedSet<L::Label> = IndexedSet::new();

28

29

300

    for label in left.labels() {

30

300

        all_labels.insert(label.clone());

31

300

32

33

    // Determine the synchronised labels

34

100

    let synchronised_labels = match synchronized_labels {

35

        Some(x) => x,

36

        None => {

37

100

            let mut new_synchronized_labels: Vec<L::Label> = Vec::new();

38

300

            for label in right.labels() {

39

300

                let (_index, inserted) = all_labels.insert(label.clone());

40

41

300

                if !inserted {

42

300

                    new_synchronized_labels.push(label.clone());

43

300

44

45

46

            // Tau can never be synchronised.

47

300

            new_synchronized_labels.retain(|l| !l.is_tau_label());

48

100

            new_synchronized_labels

49

50

};

51

52

    // Membership is queried once per transition, so use a set for O(1) lookups.

53

100

    let synchronised_set: HashSet<&L::Label> = synchronised_labels.iter().collect();

54

55

    // For the product we do not know the number of states and transitions in advance.

56

100

    let mut lts_builder = LtsBuilderFast::new(all_labels.to_vec(), Vec::new());

57

58

100

    let mut discovered_states: IndexedSet<(StateIndex, StateIndex)> = IndexedSet::new();

59

100

    let mut working = vec![(left.initial_state_index(), right.initial_state_index())];

60

100

    let (_, _) = discovered_states.insert((left.initial_state_index(), right.initial_state_index()));

61

62

454

    while let Some((left_state, right_state)) = working.pop() {

63

        // Find the (left, right) in the set of states.

64

354

        let (product_index, inserted) = discovered_states.insert((left_state, right_state));

65

354

        debug_assert!(!inserted, "The product state must have already been added");

66

67

354

        trace!("Considering ({left_state}, {right_state})");

68

69

        // Add transitions for the left LTS

70

354

        for left_transition in left.outgoing_transitions(left_state) {

71

319

            if synchronised_set.contains(&left.labels()[*left_transition.label]) {

72

                // Find the corresponding right state after this transition

73

206

                for right_transition in right.outgoing_transitions(right_state) {

74

184

                    if left.labels()[*left_transition.label] == right.labels()[*right_transition.label] {

75

                        // Labels match so introduce (left, right) -[a]-> (left', right') iff left -[a]-> left' and right -[a]-> right', and a is a synchronous action.

76

77

                        let (product_state, inserted) =

77

                            discovered_states.insert((left_transition.to, right_transition.to));

78

79

77

                        lts_builder

80

77

                            .add_transition(

81

77

                                StateIndex::new(*product_index),

82

77

                                &left.labels()[*left_transition.label],

83

77

                                StateIndex::new(*product_state),

84

85

77

                            .expect("Adding transitions does not fail");

86

87

77

                        if inserted {

88

77

                            trace!("Adding ({}, {})", left_transition.to, right_transition.to);

89

77

                            working.push((left_transition.to, right_transition.to));

90

91

107

92

93

            } else {

94

113

                let (left_index, inserted) = discovered_states.insert((left_transition.to, right_state));

95

96

                // (left, right) -[a]-> (left', right) iff left -[a]-> left' and a is not a synchronous action.

97

113

                lts_builder

98

113

                    .add_transition(

99

113

                        StateIndex::new(*product_index),

100

113

                        &left.labels()[*left_transition.label],

101

113

                        StateIndex::new(*left_index),

102

103

113

                    .expect("Adding transitions does not fail");

104

105

113

                if inserted {

106

113

                    trace!("Adding ({}, {})", left_transition.to, right_state);

107

113

                    working.push((left_transition.to, right_state));

108

109

110

111

112

354

        for right_transition in right.outgoing_transitions(right_state) {

113

315

            if synchronised_set.contains(&right.labels()[*right_transition.label]) {

114

                // Already handled in the left transitions loop.

115

223

                continue;

116

92

117

118

            // (left, right) -[a]-> (left, right') iff right -[a]-> right' and a is not a synchronous action.

119

92

            let (right_index, inserted) = discovered_states.insert((left_state, right_transition.to));

120

92

            lts_builder

121

92

                .add_transition(

122

92

                    StateIndex::new(*product_index),

123

92

                    &right.labels()[*right_transition.label],

124

92

                    StateIndex::new(*right_index),

125

126

92

                .expect("Adding transitions does not fail");

127

128

92

            if inserted {

129

                // New state discovered.

130

64

                trace!("Adding ({}, {})", left_state, right_transition.to);

131

64

                working.push((left_state, right_transition.to));

132

28

133

134

135

136

100

    if lts_builder.num_of_states() == 0 {

137

45

        // The product has no states, but an LTS requires at least one state (the initial state).

138

45

        lts_builder.require_num_of_states(1);

139

55

140

141

100

    lts_builder.finish(StateIndex::new(0), true)

142

100

143

144

#[cfg(test)]

145

mod tests {

146

    use test_log::test;

147

148

    use merc_io::DumpFiles;

149

    use merc_utilities::random_test;

150

151

    use crate::product_lts;

152

    use crate::random_lts;

153

    use crate::write_aut;

154

155

    #[test]

156

    #[cfg_attr(miri, ignore)]

157

1

    fn test_random_lts_product() {

158

100

        random_test(100, |rng| {

159

100

            let files = DumpFiles::new("test_random_lts_product");

160

161

            // This test only checks the assertions of an LTS internally.

162

100

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

163

100

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

164

165

100

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

166

100

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

167

100

            let product = product_lts(&left, &right, None);

168

169

100

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

170

100

});

171

1

172