Grcov report - reachability

1

use log::info;

2

use oxidd::BooleanFunction;

3

use oxidd::BooleanFunctionQuant;

4

use oxidd::BooleanOperator;

5

use oxidd::FunctionSubst;

6

use oxidd::ManagerRef;

7

use oxidd::Subst;

8

use oxidd::VarNo;

9

use oxidd::bdd::BDDFunction;

10

use oxidd::bdd::BDDManagerRef;

11

use oxidd::util::OutOfMemory;

12

use oxidd::util::SatCountCache;

13

14

use merc_io::TimeProgress;

15

use merc_utilities::MercError;

16

use oxidd_dump::Visualizer;

17

use rustc_hash::FxBuildHasher;

18

19

use crate::SymbolicLtsBdd;

20

use crate::compute_vars_bdd;

21

use crate::minus;

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

30

        |iteration: usize| {

39

30

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

40

30

},

41

1,

42

);

43

44

45

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

46

//

47

    // Definition of subtitution:

48

    // > f[x <- g] = (!g ∧ f[x <- false]) ∨ (g ∧ f[x <- true])

49

100

    let state_variables = compute_vars_bdd(manager_ref, lts.state_variables())?.0;

50

100

    let next_state_substitution = Subst::new(lts.next_state_variables(), state_variables);

51

52

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

53

500

    let relation_vars_bdd = lts.transition_groups().iter().map(|group| -> Result<_, OutOfMemory> {

54

7011

        let bits = group.write_variables().iter().map(|var| {

55

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

56

107244

            let index = lts.next_state_variables().iter().position(|next_var| next_var == var).unwrap();

57

7011

            lts.state_variables()[index]

58

7011

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

59

60

500

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

61

500

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

62

63

431

    while todo.satisfiable() {

64

        // Apply the transition relations to the todo set.

65

331

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

66

1655

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

67

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

68

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

69

            // would become unconstrained and then after substituting next state

70

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

71

            // spurious states.

72

//

73

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

74

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

75

            // result in `T`.

76

1655

            todo1 = todo1.or(&todo.apply_exists(

77

1655

                BooleanOperator::And,

78

1655

                transition.relation(),

79

1655

                relation_vars,

80

            )?)?;

81

82

83

        // Substitute next state variables with current state variables.

84

331

        todo1 = todo1.substitute(&next_state_substitution)?;

85

86

331

        if visualize {

87

            // Visualize the current partition.

88

            manager_ref.with_manager_shared(|manager| {

89

                Visualizer::new()

90

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

91

                    .serve()

92

            })?;

93

331

94

95

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

96

331

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

97

331

        states = states.or(&todo)?;

98

331

        progress.print(iteration);

99

331

        iteration += 1;

100

101

102

100

Ok(

103

100

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

104

100

            as usize,

105

100

106

100

107

108

#[cfg(test)]

109

mod tests {

110

    use merc_utilities::random_test;

111

112

    use crate::SymbolicLtsBdd;

113

    use crate::random_symbolic_lts;

114

    use crate::reachability;

115

    use crate::reachability_bdd;

116

117

    #[test]

118

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

119

1

    fn test_random_reachability() {

120

100

        random_test(100, |rng| {

121

100

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

122

123

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

124

100

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

125

100

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

126

127

100

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

128

100

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

129

130

100

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

131

132

100

            assert_eq!(

133

                num_reachable_states, num_reachable_states_bdd,

134

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

135

);

136

100

});

137

1

138