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

9

        |iteration: usize| {

37

9

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

38

9

},

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

6879

                .map(|var| {

59

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

60

6879

                    let index = lts

61

6879

                        .next_state_variables()

62

6879

                        .iter()

63

106341

                        .position(|next_var| next_var == var)

64

6879

                        .expect("write variable not found in next-state variables");

65

6879

                    lts.state_variables()[index]

66

6879

})

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

439

    while todo.satisfiable() {

75

339

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

76

77

        // Apply the transition relations to the todo set.

78

339

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

79

1695

        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

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

89

1695

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

90

91

            // Substitute next state variables with current state variables.

92

1695

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

93

94

1695

            todo1 = todo1.or(&tmp)?;

95

96

97

339

        if visualize {

98

            // Visualize the current partition.

99

            manager_ref.with_manager_shared(|manager| {

100

                Visualizer::new()

101

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

102

                    .serve()

103

            })?;

104

339

105

106

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

107

339

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

108

339

        states = states.or(&todo)?;

109

339

        progress.print(iteration);

110

339

        iteration += 1;

111

112

113

100

    Ok(states)

114

100

115

116

#[cfg(test)]

117

mod tests {

118

    use oxidd::BooleanFunction;

119

    use oxidd::util::SatCountCache;

120

    use rustc_hash::FxBuildHasher;

121

122

    use merc_utilities::Timing;

123

    use merc_utilities::random_test;

124

125

    use crate::SymbolicLtsBdd;

126

    use crate::random_symbolic_lts;

127

    use crate::reachability;

128

    use crate::reachability_bdd;

129

130

    #[test]

131

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

132

1

    fn test_random_reachability() {

133

100

        random_test(100, |rng| {

134

100

            let manager = oxidd::ldd::new_manager(2048, 1024, 1);

135

136

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

137

100

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

138

100

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

139

100

            let num_reachable_states = reachable_states.len();

140

141

100

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

142

100

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

143

144

100

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

145

100

            let num_reachable_states_bdd = reachable_states_bdd

146

100

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

147

100

                as usize;

148

149

100

            assert_eq!(

150

                num_reachable_states, num_reachable_states_bdd,

151

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

152

);

153

100

});

154

1

155