Grcov report - reachability.rs

1

use std::fmt;

2

3

use log::debug;

4

use log::info;

5

use log::trace;

6

use merc_data::DataExpression;

7

use merc_io::TimeProgress;

8

use merc_ldd::Ldd;

9

use merc_ldd::LddDisplay;

10

use merc_ldd::Storage;

11

use merc_ldd::len;

12

use merc_ldd::minus;

13

use merc_ldd::relational_product;

14

use merc_ldd::union;

15

use merc_utilities::MercError;

16

use merc_utilities::Timing;

17

18

use crate::DependencyGraph;

19

use crate::Relation;

20

21

/// A generic trait representing a symbolic LTS

22

pub trait SymbolicLTS {

23

    /// Returns the LDD representing the set of states.

24

    fn states(&self) -> &Ldd;

25

26

    /// Returns the LDD representing the initial state.

27

    fn initial_state(&self) -> &Ldd;

28

29

    /// Returns an iterator over the summand groups.

30

    fn transition_groups(&self) -> &[impl TransitionGroup];

31

32

    /// Returns a mutable iterator over the summand groups.

33

    fn transition_groups_mut(&mut self) -> &mut [impl TransitionGroup];

34

35

    /// Returns the action labels for the LTS.

36

    fn action_labels(&self) -> &[String];

37

38

    /// Returns the possible values for each process parameter.

39

    fn parameter_values(&self) -> &[Vec<DataExpression>];

40

41

    /// Computes the dependency graph of the LTS.

42

    fn dependency_graph(&self) -> DependencyGraph {

43

        let mut relations = Vec::new();

44

45

        for group in self.transition_groups() {

46

            relations.push(Relation::new(

47

                group.read_indices().iter().map(|i| *i as usize).collect(),

48

                group.write_indices().iter().map(|i| *i as usize).collect(),

49

));

50

51

52

        DependencyGraph::new(relations)

53

54

55

56

pub trait TransitionGroup: fmt::Debug {

57

    /// Returns the transition relation T' -> U' for this summand group.

58

    fn relation(&self) -> &Ldd;

59

60

    /// Returns the read indices for this summand group.

61

    fn read_indices(&self) -> &[u32];

62

63

    /// Returns the write indices for this summand group.

64

    fn write_indices(&self) -> &[u32];

65

66

    /// Returns the action label index for this summand group, if any.

67

    fn action_label_index(&self) -> Option<usize>;

68

69

    /// Returns the meta information for this summand group required to perform the relational product.

70

    fn meta(&self) -> &Ldd;

71

72

    /// Learns the successors of the given set of states.

73

///

74

    /// The `todo` the set of vectors for which successors should be learned.

75

    /// This function should update the [Self::relation] of the transition group

76

    /// to include the new transitions from `todo` to their successors.

77

    fn learn_successors(&mut self, storage: &mut Storage, todo: &Ldd) -> Result<(), MercError>;

78

79

80

/// Performs reachability analysis using the given initial state and transitions from the symbolic LTS.

81

401

pub fn reachability<L: SymbolicLTS>(storage: &mut Storage, lts: &mut L, timing: &Timing) -> Result<Ldd, MercError> {

82

401

    let mut todo = lts.initial_state().clone();

83

401

    let mut states = lts.initial_state().clone(); // The state space.

84

401

    let mut iteration = 0;

85

86

401

    trace!("states = {}", LddDisplay::new(storage, &states));

87

401

    let progress = TimeProgress::new(

88

8

        |(iteration, num_of_states)| {

89

8

            info!("explored {} state(s) after {} iteration(s)", num_of_states, iteration);

90

8

},

91

1,

92

);

93

94

401

    timing.measure("reachability", || {

95

1799

        while todo != *storage.empty_set() {

96

1398

            debug!("Iteration {}: todo size = {}", iteration, len(storage, &todo));

97

98

            // Learn successors for all the transition groups and compute the next todo set.

99

1398

            let mut todo1 = storage.empty_set().clone();

100

8529

            for (i, transition) in lts.transition_groups_mut().iter_mut().enumerate() {

101

8529

                trace!("Learning successors for transition group {}:", i);

102

8529

                timing.measure(&format!("learn_successors_{}", i), || {

103

8529

                    transition.learn_successors(storage, &todo)

104

8529

                })?;

105

106

8529

                let result = relational_product(storage, &todo, transition.relation(), transition.meta());

107

8529

                todo1 = union(storage, &todo1, &result);

108

109

110

1398

            trace!("todo1 = {}", LddDisplay::new(storage, &todo1));

111

112

1398

            todo = minus(storage, &todo1, &states);

113

1398

            states = union(storage, &states, &todo);

114

1398

            if progress.is_due() {

115

8

                progress.print((iteration, len(storage, &states)));

116

1390

117

1398

            iteration += 1;

118

119

120

401

        Ok(states)

121

401

})

122

401