Grcov report - reachability

1

use log::info;

2

use log::trace;

3

use oxidd::BooleanFunction;

4

use oxidd::BooleanFunctionQuant;

5

use oxidd::BooleanOperator;

6

use oxidd::ManagerRef;

7

use oxidd::VarNo;

8

use oxidd::bdd::BDDFunction;

9

use oxidd::bdd::BDDManagerRef;

10

use oxidd::util::OutOfMemory;

11

use oxidd::util::SatCountCache;

12

13

use merc_io::TimeProgress;

14

use merc_utilities::MercError;

15

use oxidd_dump::Visualizer;

16

use rustc_hash::FxBuildHasher;

17

18

use crate::SymbolicLtsBdd;

19

use crate::compute_vars_bdd;

20

use crate::minus;

21

use crate::variable_rename_reverse;

22

23

/// Performs reachability analysis on the given symbolic LTS represented using BDDs.

24

///

25

/// # Details

26

///

27

/// When `visualize` has been set to true, intermediate BDDs are visualized using `oxidd-vis`.

28

100

pub fn reachability_bdd(

29

100

    manager_ref: &BDDManagerRef,

30

100

    lts: &SymbolicLtsBdd,

31

100

    visualize: bool,

32

100

) -> Result<usize, MercError> {

33

100

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

34

100

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

35

100

    let mut iteration = 0;

36

37

100

    let progress = TimeProgress::new(

38

5

        |iteration: usize| {

39

5

            info!("Iteration {}", iteration);

40

5

},

41

1,

42

);

43

44

    // Substitution to replace next state variables with current state variables: [s' <- s]

45

100

    let next_state_substitution: Vec<(VarNo, VarNo)> = lts

46

100

        .next_state_variables()

47

100

        .iter()

48

100

        .cloned()

49

100

        .zip(lts.state_variables().iter().cloned())

50

100

        .collect();

51

52

    // Determine the write variables BDDs for all transition groups.

53

100

    let relation_vars_bdd = lts

54

100

        .transition_groups()

55

100

        .iter()

56

500

        .map(|group| -> Result<_, OutOfMemory> {

57

500

            let bits = group

58

500

                .write_variables()

59

500

                .iter()

60

6318

                .map(|var| {

61

                    // Find the index of the current state variable corresponding to this next state variable.

62

6318

                    let index = lts

63

6318

                        .next_state_variables()

64

6318

                        .iter()

65

98217

                        .position(|next_var| next_var == var)

66

6318

                        .unwrap();

67

6318

                    lts.state_variables()[index]

68

6318

})

69

500

                .collect::<Vec<VarNo>>();

70

500

            compute_vars_bdd(manager_ref, &bits)?

71

.1

72

500

                .and(&compute_vars_bdd(manager_ref, lts.action_variables())?.1)

73

500

})

74

100

        .collect::<Result<Vec<BDDFunction>, OutOfMemory>>()?;

75

76

481

    while todo.satisfiable() {

77

381

        trace!("iteration {}", iteration);

78

79

        // Apply the transition relations to the todo set.

80

381

        let mut todo1 = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

81

1905

        for (transition, relation_vars) in lts.transition_groups().iter().zip(relation_vars_bdd.iter()) {

82

            // We explicitly do not quantify over state variables that are not

83

            // written by the transition group. Otherwise, these state variables

84

            // would become unconstrained and then after substituting next state

85

            // variables with current state variables, they would lead to

86

            // spurious states.

87

//

88

            // This can be seen from the following: `exists a. (todo(s) ∧ R(s, s', a))`

89

            // is equal to `todo(s)` if `support(R) = a`, where quantifying over `s` would

90

            // This can be seen from the following: `exists a. (todo(s) ∧ R(s, s', a))`

91

            // is equal to `todo(s)` if `support(R) = a`, where quantifying over `s` would

92

            // result in `T`. And `todo(s)[s' <- s]` is equal to `todo(s)`.

93

1905

            let tmp = todo.apply_exists(BooleanOperator::And, transition.relation(), relation_vars)?;

94

95

            // Substitute next state variables with current state variables.

96

1905

            let tmp = variable_rename_reverse(manager_ref, &tmp, &next_state_substitution)?;

97

98

1905

            todo1 = todo1.or(&tmp)?;

99

100

101

381

        if visualize {

102

            // Visualize the current partition.

103

            manager_ref.with_manager_shared(|manager| {

104

                Visualizer::new()

105

                    .add(&format!("todo1_{iteration}"), manager, [&todo1])

106

                    .serve()

107

            })?;

108

381

109

110

        // Keep todo states that have not been discovered yet, and add them to the set of discovered states.

111

381

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

112

381

        states = states.or(&todo)?;

113

381

        progress.print(iteration);

114

381

        iteration += 1;

115

116

117

100

Ok(

118

100

        states.sat_count::<u64, FxBuildHasher>(lts.state_variables().len() as u32, &mut SatCountCache::default())

119

100

            as usize,

120

100

121

100

122

123

#[cfg(test)]

124

mod tests {

125

    use merc_utilities::random_test;

126

127

    use crate::SymbolicLtsBdd;

128

    use crate::random_symbolic_lts;

129

    use crate::reachability;

130

    use crate::reachability_bdd;

131

132

    #[test]

133

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

134

1

    fn test_random_reachability() {

135

100

        random_test(100, |rng| {

136

100

            let mut storage = merc_ldd::Storage::new();

137

138

            // We don't really check anything here, just ensure that reachability runs without errors.

139

100

            let lts = random_symbolic_lts(rng, &mut storage, 10, 5).unwrap();

140

100

            let num_reachable_states = reachability(&mut storage, &lts).unwrap();

141

142

100

            let manager_ref = oxidd::bdd::new_manager(2028, 2028, 1);

143

100

            let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &lts).unwrap();

144

145

100

            let num_reachable_states_bdd = reachability_bdd(&manager_ref, &lts_bdd, false).unwrap();

146

147

100

            assert_eq!(

148

                num_reachable_states, num_reachable_states_bdd,

149

                "Number of reachable states does not match between BDD and LDD-based reachability."

150

);

151

100

});

152

1

153