Grcov report - product

1

use log::trace;

2

3

use merc_collections::IndexedSet;

4

5

use crate::LTS;

6

use crate::LabelledTransitionSystem;

7

use crate::LtsBuilderFast;

8

use crate::StateIndex;

9

use crate::TransitionLabel;

10

11

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

12

///

13

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

14

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

15

/// synchronization.

16

3100

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

17

3100

    left: &L,

18

3100

    right: &R,

19

3100

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

20

3100

) -> LabelledTransitionSystem<L::Label> {

21

    // Determine the combination of action labels

22

3100

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

23

24

15900

    for label in left.labels() {

25

15900

        all_labels.insert(label.clone());

26

15900

27

28

    // Determine the synchronised labels

29

3100

    let synchronised_labels = match synchronized_labels {

30

3000

        Some(x) => x,

31

        None => {

32

100

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

33

300

            for label in right.labels() {

34

300

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

35

36

300

                if !inserted {

37

300

                    new_synchronized_labels.push(label.clone());

38

300

39

40

41

            // Tau can never be synchronised.

42

300

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

43

100

            new_synchronized_labels

44

45

};

46

47

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

48

3100

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

49

50

3100

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

51

3100

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

52

3100

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

53

54

63275

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

55

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

56

60175

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

57

60175

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

58

59

60175

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

60

61

        // Add transitions for the left LTS

62

219294

        for left_transition in left.outgoing_transitions(left_state) {

63

219294

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

64

                // Find the corresponding right state after this transition

65

98866

                for right_transition in right.outgoing_transitions(right_state) {

66

98866

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

67

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

68

20104

                        let (product_state, inserted) =

69

20104

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

70

71

20104

                        lts_builder.add_transition(

72

20104

                            StateIndex::new(*product_index),

73

20104

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

74

20104

                            StateIndex::new(*product_state),

75

);

76

77

20104

                        if inserted {

78

4192

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

79

4192

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

80

15912

81

78762

82

83

            } else {

84

189530

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

85

86

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

87

189530

                lts_builder.add_transition(

88

189530

                    StateIndex::new(*product_index),

89

189530

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

90

189530

                    StateIndex::new(*left_index),

91

);

92

93

189530

                if inserted {

94

38706

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

95

38706

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

96

150824

97

98

99

100

146906

        for right_transition in right.outgoing_transitions(right_state) {

101

146530

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

102

                // Already handled in the left transitions loop.

103

37291

                continue;

104

109239

105

106

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

107

109239

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

108

109239

            lts_builder.add_transition(

109

109239

                StateIndex::new(*product_index),

110

109239

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

111

109239

                StateIndex::new(*right_index),

112

);

113

114

109239

            if inserted {

115

                // New state discovered.

116

14177

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

117

14177

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

118

95062

119

120

121

122

3100

    if lts_builder.num_of_states() == 0 {

123

452

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

124

452

        lts_builder.require_num_of_states(1);

125

2648

126

127

3100

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

128

3100

129

130

#[cfg(test)]

131

mod tests {

132

    use crate::{random_lts, write_aut};

133

134

    use super::*;

135

136

    use merc_io::DumpFiles;

137

    use test_log::test;

138

139

    use merc_utilities::random_test;

140

141

    #[test]

142

    #[cfg_attr(miri, ignore)]

143

    fn test_random_lts_product() {

144

100

        random_test(100, |rng| {

145

100

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

146

147

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

148

100

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

149

100

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

150

151

100

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

152

100

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

153

100

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

154

155

100

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

156

100

});

157

158