Grcov report - product

1

#![forbid(unsafe_code)]

2

3

use log::trace;

4

5

use merc_collections::IndexedSet;

6

7

use crate::LTS;

8

use crate::LabelledTransitionSystem;

9

use crate::LtsBuilder;

10

use crate::LtsBuilderFast;

11

use crate::StateIndex;

12

use crate::TransitionLabel;

13

14

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

15

///

16

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

17

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

18

/// synchronization.

19

100

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

20

100

    left: &L,

21

100

    right: &R,

22

100

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

23

100

) -> LabelledTransitionSystem<L::Label> {

24

    // Determine the combination of action labels

25

100

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

26

27

300

    for label in left.labels() {

28

300

        all_labels.insert(label.clone());

29

300

30

31

    // Determine the synchronised labels

32

100

    let synchronised_labels = match synchronized_labels {

33

        Some(x) => x,

34

        None => {

35

100

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

36

300

            for label in right.labels() {

37

300

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

38

39

300

                if !inserted {

40

300

                    new_synchronized_labels.push(label.clone());

41

300

42

43

44

            // Tau can never be synchronised.

45

300

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

46

100

            new_synchronized_labels

47

48

};

49

50

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

51

100

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

52

53

100

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

54

100

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

55

100

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

56

57

430

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

58

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

59

330

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

60

330

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

61

62

330

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

63

64

        // Add transitions for the left LTS

65

330

        for left_transition in left.outgoing_transitions(left_state) {

66

287

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

67

                // Find the corresponding right state after this transition

68

202

                for right_transition in right.outgoing_transitions(right_state) {

69

181

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

70

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

71

51

                        let (product_state, inserted) =

72

51

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

73

74

51

                        lts_builder

75

51

                            .add_transition(

76

51

                                StateIndex::new(*product_index),

77

51

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

78

51

                                StateIndex::new(*product_state),

79

80

51

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

81

82

51

                        if inserted {

83

51

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

84

51

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

85

86

130

87

88

            } else {

89

85

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

90

91

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

92

85

                lts_builder

93

85

                    .add_transition(

94

85

                        StateIndex::new(*product_index),

95

85

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

96

85

                        StateIndex::new(*left_index),

97

98

85

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

99

100

85

                if inserted {

101

85

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

102

85

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

103

104

105

106

107

330

        for right_transition in right.outgoing_transitions(right_state) {

108

301

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

109

                // Already handled in the left transitions loop.

110

173

                continue;

111

128

112

113

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

114

128

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

115

128

            lts_builder

116

128

                .add_transition(

117

128

                    StateIndex::new(*product_index),

118

128

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

119

128

                    StateIndex::new(*right_index),

120

121

128

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

122

123

128

            if inserted {

124

                // New state discovered.

125

94

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

126

94

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

127

34

128

129

130

131

100

    if lts_builder.num_of_states() == 0 {

132

41

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

133

41

        lts_builder.require_num_of_states(1);

134

59

135

136

100

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

137

100

138

139

#[cfg(test)]

140

mod tests {

141

    use test_log::test;

142

143

    use merc_io::DumpFiles;

144

    use merc_utilities::random_test;

145

146

    use crate::product_lts;

147

    use crate::random_lts;

148

    use crate::write_aut;

149

150

    #[test]

151

    #[cfg_attr(miri, ignore)]

152

    fn test_random_lts_product() {

153

100

        random_test(100, |rng| {

154

100

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

155

156

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

157

100

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

158

100

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

159

160

100

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

161

100

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

162

100

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

163

164

100

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

165

100

});

166

167