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

10

use crate::StateIndex;

11

use crate::TransitionLabel;

12

13

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

14

///

15

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

16

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

17

/// synchronization.

18

3500

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

19

3500

    left: &L,

20

3500

    right: &R,

21

3500

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

22

3500

) -> LabelledTransitionSystem<L::Label> {

23

    // Determine the combination of action labels

24

3500

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

25

26

15700

    for label in left.labels() {

27

15700

        all_labels.insert(label.clone());

28

15700

29

30

    // Determine the synchronised labels

31

3500

    let synchronised_labels = match synchronized_labels {

32

3400

        Some(x) => x,

33

        None => {

34

100

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

35

300

            for label in right.labels() {

36

300

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

37

38

300

                if !inserted {

39

300

                    new_synchronized_labels.push(label.clone());

40

300

41

42

43

            // Tau can never be synchronised.

44

300

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

45

100

            new_synchronized_labels

46

47

};

48

49

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

50

3500

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

51

52

3500

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

53

3500

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

54

3500

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

55

56

55542

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

57

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

58

52042

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

59

52042

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

60

61

52042

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

62

63

        // Add transitions for the left LTS

64

183010

        for left_transition in left.outgoing_transitions(left_state) {

65

183010

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

66

                // Find the corresponding right state after this transition

67

113562

                for right_transition in right.outgoing_transitions(right_state) {

68

113512

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

69

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

70

29149

                        let (product_state, inserted) =

71

29149

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

72

73

29149

                        lts_builder.add_transition(

74

29149

                            StateIndex::new(*product_index),

75

29149

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

76

29149

                            StateIndex::new(*product_state),

77

);

78

79

29149

                        if inserted {

80

4883

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

81

4883

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

82

24266

83

84363

84

85

            } else {

86

145575

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

87

88

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

89

145575

                lts_builder.add_transition(

90

145575

                    StateIndex::new(*product_index),

91

145575

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

92

145575

                    StateIndex::new(*left_index),

93

);

94

95

145575

                if inserted {

96

33005

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

97

33005

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

98

112570

99

100

101

102

124117

        for right_transition in right.outgoing_transitions(right_state) {

103

123518

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

104

                // Already handled in the left transitions loop.

105

40363

                continue;

106

83155

107

108

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

109

83155

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

110

83155

            lts_builder.add_transition(

111

83155

                StateIndex::new(*product_index),

112

83155

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

113

83155

                StateIndex::new(*right_index),

114

);

115

116

83155

            if inserted {

117

                // New state discovered.

118

10654

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

119

10654

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

120

72501

121

122

123

124

3500

    if lts_builder.num_of_states() == 0 {

125

524

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

126

524

        lts_builder.require_num_of_states(1);

127

2976

128

129

3500

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

130

3500

131

132

#[cfg(test)]

133

mod tests {

134

    use crate::random_lts;

135

    use crate::write_aut;

136

137

    use super::*;

138

139

    use merc_io::DumpFiles;

140

    use test_log::test;

141

142

    use merc_utilities::random_test;

143

144

    #[test]

145

    #[cfg_attr(miri, ignore)]

146

    fn test_random_lts_product() {

147

100

        random_test(100, |rng| {

148

100

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

149

150

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

151

100

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

152

100

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

153

154

100

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

155

100

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

156

100

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

157

158

100

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

159

100

});

160

161