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

12

use merc_io::TimeProgress;

13

use merc_utilities::MercError;

14

use oxidd_dump::Visualizer;

15

16

use crate::SymbolicLtsBdd;

17

use crate::compute_vars_bdd;

18

use crate::minus;

19

use crate::variable_rename_reverse;

20

21

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

22

///

23

/// # Details

24

///

25

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

26

100

pub fn reachability_bdd(

27

100

    manager_ref: &BDDManagerRef,

28

100

    lts: &SymbolicLtsBdd,

29

100

    visualize: bool,

30

100

) -> Result<BDDFunction, MercError> {

31

100

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

32

100

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

33

100

    let mut iteration = 0;

34

35

100

    let progress = TimeProgress::new(

36

1

        |iteration: usize| {

37

1

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

38

1

},

39

1,

40

);

41

42

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

43

100

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

44

100

        .next_state_variables()

45

100

        .iter()

46

100

        .cloned()

47

100

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

48

100

        .collect();

49

50

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

51

100

    let relation_vars_bdd = lts

52

100

        .transition_groups()

53

100

        .iter()

54

500

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

55

500

            let bits = group

56

500

                .write_variables()

57

500

                .iter()

58

6434

                .map(|var| {

59

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

60

6434

                    let index = lts

61

6434

                        .next_state_variables()

62

6434

                        .iter()

63

99330

                        .position(|next_var| next_var == var)

64

6434

                        .unwrap();

65

6434

                    lts.state_variables()[index]

66

6434

})

67

500

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

68

500

            compute_vars_bdd(manager_ref, &bits)?

69

.1

70

500

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

71

500

})

72

100

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

73

74

406

    while todo.satisfiable() {

75

306

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

76

77

        // Apply the transition relations to the todo set.

78

306

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

79

1530

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

80

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

81

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

82

            // would become unconstrained and then after substituting next state

83

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

84

            // spurious states.

85

//

86

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

87

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

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

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

91

1530

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

92

93

            // Substitute next state variables with current state variables.

94

1530

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

95

96

1530

            todo1 = todo1.or(&tmp)?;

97

98

99

306

        if visualize {

100

            // Visualize the current partition.

101

            manager_ref.with_manager_shared(|manager| {

102

                Visualizer::new()

103

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

104

                    .serve()

105

            })?;

106

306

107

108

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

109

306

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

110

306

        states = states.or(&todo)?;

111

306

        progress.print(iteration);

112

306

        iteration += 1;

113

114

115

100

    Ok(states)

116

100

117

118

#[cfg(test)]

119

mod tests {

120

    use oxidd::BooleanFunction;

121

    use oxidd::util::SatCountCache;

122

    use rustc_hash::FxBuildHasher;

123

124

    use merc_ldd::len;

125

    use merc_utilities::Timing;

126

    use merc_utilities::random_test;

127

128

    use crate::SymbolicLtsBdd;

129

    use crate::random_symbolic_lts;

130

    use crate::reachability;

131

    use crate::reachability_bdd;

132

133

    #[test]

134

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

135

1

    fn test_random_reachability() {

136

100

        random_test(100, |rng| {

137

100

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

138

139

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

140

100

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

141

100

            let reachable_states = reachability(&mut storage, &mut lts, &Timing::new()).unwrap();

142

100

            let num_reachable_states = len(&mut storage, &reachable_states);

143

144

100

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

145

100

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

146

147

100

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

148

100

            let num_reachable_states_bdd = reachable_states_bdd

149

100

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

150

100

                as usize;

151

152

100

            assert_eq!(

153

                num_reachable_states, num_reachable_states_bdd,

154

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

155

);

156

100

});

157

1

158