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

4900

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

19

4900

    left: &L,

20

4900

    right: &R,

21

4900

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

22

4900

) -> LabelledTransitionSystem<L::Label> {

23

    // Determine the combination of action labels

24

4900

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

25

26

33100

    for label in left.labels() {

27

33100

        all_labels.insert(label.clone());

28

33100

29

30

    // Determine the synchronised labels

31

4900

    let synchronised_labels = match synchronized_labels {

32

4800

        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

4900

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

51

52

4900

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

53

4900

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

54

4900

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

55

56

44959

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

57

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

58

40059

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

59

40059

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

60

61

40059

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

62

63

        // Add transitions for the left LTS

64

52730

        for left_transition in left.outgoing_transitions(left_state) {

65

52730

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

66

                // Find the corresponding right state after this transition

67

12916

                for right_transition in right.outgoing_transitions(right_state) {

68

12916

                    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

5119

                        let (product_state, inserted) =

71

5119

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

72

73

5119

                        lts_builder.add_transition(

74

5119

                            StateIndex::new(*product_index),

75

5119

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

76

5119

                            StateIndex::new(*product_state),

77

);

78

79

5119

                        if inserted {

80

2334

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

81

2334

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

82

2785

83

7797

84

85

            } else {

86

43635

                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

43635

                lts_builder.add_transition(

90

43635

                    StateIndex::new(*product_index),

91

43635

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

92

43635

                    StateIndex::new(*left_index),

93

);

94

95

43635

                if inserted {

96

26194

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

97

26194

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

98

17441

99

100

101

102

43235

        for right_transition in right.outgoing_transitions(right_state) {

103

40373

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

104

                // Already handled in the left transitions loop.

105

13483

                continue;

106

26890

107

108

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

109

26890

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

110

26890

            lts_builder.add_transition(

111

26890

                StateIndex::new(*product_index),

112

26890

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

113

26890

                StateIndex::new(*right_index),

114

);

115

116

26890

            if inserted {

117

                // New state discovered.

118

6631

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

119

6631

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

120

20259

121

122

123

124

4900

    if lts_builder.num_of_states() == 0 {

125

1015

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

126

1015

        lts_builder.require_num_of_states(1);

127

3885

128

129

4900

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

130

4900

131

132

#[cfg(test)]

133

mod tests {

134

    use test_log::test;

135

136

    use merc_io::DumpFiles;

137

    use merc_utilities::random_test;

138

139

    use crate::product_lts;

140

    use crate::random_lts;

141

    use crate::write_aut;

142

143

    #[test]

144

    #[cfg_attr(miri, ignore)]

145

    fn test_random_lts_product() {

146

100

        random_test(100, |rng| {

147

100

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

148

149

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

150

100

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

151

100

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

152

153

100

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

154

100

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

155

100

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

156

157

100

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

158

100

});

159

160