Grcov report - refine.rs

1

use log::info;

2

use merc_io::TimeProgress;

3

use merc_utilities::MercError;

4

use oxidd::BooleanFunction;

5

use oxidd::BooleanFunctionQuant;

6

use oxidd::Manager;

7

use oxidd::ManagerRef;

8

use oxidd::VarNo;

9

use oxidd::bdd::BDDFunction;

10

use oxidd::bdd::BDDManagerRef;

11

use oxidd::util::OutOfMemory;

12

13

use crate::CubeIterAll;

14

use crate::SummandGroupBdd;

15

use crate::SymbolicLtsBdd;

16

use crate::bdd_from_cube;

17

use crate::compute_vars_bdd;

18

use crate::variable_rename;

19

20

/// Strong bisimulation refinement algorithms for symbolic LTSs.

21

pub fn refine_bisimulation(manager_ref: &BDDManagerRef, lts: &SymbolicLtsBdd) -> Result<BDDFunction, MercError> {

22

    // Computes the BDD representing all (next) state variables.

23

    let state_vars = manager_ref.with_manager_shared(|manager| -> Result<_, OutOfMemory> {

24

        let mut bdd: BDDFunction = BDDFunction::t(manager);

25

26

        for var in lts.state_variables().iter().chain(lts.next_state_variables().iter()) {

27

            let var = BDDFunction::var(manager, *var)?;

28

            bdd = bdd.and(&var)?;

29

30

31

        Ok(bdd)

32

    })?;

33

34

    // Computes the vector of action label BDDs.

35

    let action_vars = manager_ref.with_manager_shared(|manager| -> Result<_, OutOfMemory> {

36

        lts.action_variables()

37

            .iter()

38

            .map(|var| BDDFunction::var(manager, *var))

39

            .collect::<Result<Vec<_>, OutOfMemory>>()

40

    })?;

41

42

    // Split the transition group to only have a single action label per group.

43

    let mut split_groups = Vec::new();

44

    for group in lts.transition_groups() {

45

        let action_bdd = group.relation().exists(&state_vars)?;

46

47

        for cube in CubeIterAll::new(&action_bdd) {

48

            // Every cube is a single action.

49

            let cube = cube?;

50

            let label_bdd = bdd_from_cube(manager_ref, &action_vars, &cube)?;

51

52

            split_groups.push(SummandGroupBdd::new(

53

                group.relation().clone().and(&label_bdd)?,

54

                group.read_variables().to_vec(),

55

                group.write_variables().to_vec(),

56

));

57

58

59

60

    // Introduce variables for q, q' after the state and next state variables.

61

    let q_variables = manager_ref

62

        .with_manager_exclusive(|manager| {

63

            manager.add_named_vars((0..lts.state_variables().len()).map(|index| format!("q_{index}")))

64

})

65

        .map_err(|e| e.to_string())?

66

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

67

68

    let q_prime_variables = manager_ref

69

        .with_manager_exclusive(|manager| {

70

            manager.add_named_vars((0..lts.state_variables().len()).map(|index| format!("q_prime_{index}")))

71

})

72

        .map_err(|e| e.to_string())?

73

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

74

75

    // We interleave the p, q, p', and q' variables that all represent states (and next states).

76

    manager_ref.with_manager_exclusive(|manager| {

77

        let order: Vec<_> = lts

78

            .state_variables()

79

            .iter()

80

            .zip(q_variables.iter())

81

            .zip(lts.next_state_variables().iter().zip(q_prime_variables.iter()))

82

            .flat_map(|((s, q), (s_prime, q_prime))| [*s, *q, *s_prime, *q_prime])

83

            .collect();

84

85

        oxidd_reorder::set_var_order(manager, &order)

86

});

87

88

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

89

    let p_prime_bdd = compute_vars_bdd(manager_ref, lts.next_state_variables())?.1;

90

    let q_bdd = compute_vars_bdd(manager_ref, &q_variables)?.1;

91

    let q_prime_bdd = compute_vars_bdd(manager_ref, &q_prime_variables)?.1;

92

93

    // Create renamings from (p -> q), (q -> p'), (p' -> q').

94

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

95

        .state_variables()

96

        .iter()

97

        .cloned()

98

        .zip(q_variables.iter().cloned())

99

        .collect();

100

    let q_to_p_prime: Vec<(VarNo, VarNo)> = q_variables

101

        .iter()

102

        .cloned()

103

        .zip(lts.next_state_variables().iter().cloned())

104

        .collect();

105

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

106

        .next_state_variables()

107

        .iter()

108

        .cloned()

109

        .zip(q_prime_variables.iter().cloned())

110

        .collect();

111

112

    // Represents the b and b' variables (and a renaming from b to b') that must be updated in every iteration.

113

    let mut b_variables: Vec<VarNo> = Vec::new();

114

    let mut b_vars_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::t(manager));

115

116

    let mut b_prime_variables: Vec<VarNo> = Vec::new();

117

    let mut b_prime_vars_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::t(manager));

118

119

    let mut b_to_b_prime: Vec<(VarNo, VarNo)> = Vec::new();

120

121

    // B_0(p, b) = 1 where |b| is 0.

122

    let mut blocks = lts.states().clone();

123

124

    let progress = TimeProgress::new(

125

        |iteration: usize| {

126

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

127

},

128

1,

129

);

130

131

    let mut iteration = 0;

132

    loop {

133

        // Check if B_i is stable w.r.t. all the transition relations.

134

        let mut is_stable = true;

135

        for group in &split_groups {

136

            // Forall b, p, p', q: B_i(p, b) and B_i(q, b) and Ta(p, p') implies exists b', q': Ta(q, q') and B_i(p', b') and B_i(q', b')

137

138

            // Rename B_i(p, b') to B_i(q', b')

139

            let blocks_q = variable_rename(manager_ref, &blocks, &p_to_q)?;

140

            let blocks_p_prime = variable_rename(manager_ref, &blocks_q, &q_to_p_prime)?;

141

            let blocks_p_prime_b_prime = variable_rename(manager_ref, &blocks_p_prime, &b_to_b_prime)?;

142

143

            let condition = blocks.and(&blocks_q)?.and(group.relation())?;

144

145

            let blocks_q_prime = variable_rename(manager_ref, &blocks_p_prime, &p_prime_to_q_prime)?;

146

            let blocks_q_prime_b_prime = variable_rename(manager_ref, &blocks_q_prime, &b_to_b_prime)?;

147

148

            // Rename Ta(p, p') to Ta(q, q')

149

            let relation_q = variable_rename(manager_ref, group.relation(), &p_to_q)?;

150

            let relation_q_q_prime = variable_rename(manager_ref, &relation_q, &p_prime_to_q_prime)?;

151

152

            // Computes exists b', q': Ta(q, q') and B_i(p', b') and B_i(q', b')

153

            let antecant = relation_q_q_prime

154

                .and(&blocks_p_prime_b_prime)?

155

                .and(&blocks_q_prime_b_prime)?

156

                .exists(&q_prime_bdd.and(&b_prime_vars_bdd)?)?;

157

158

            is_stable = is_stable

159

                && condition

160

                    .imp(&antecant)?

161

                    .forall(&b_vars_bdd.and(&p_bdd)?.and(&p_prime_bdd)?.and(&q_bdd)?)?

162

                    .satisfiable();

163

            if !is_stable {

164

                // We are not yet stable, so need to perform additional splitting.

165

                break;

166

167

168

169

        if is_stable {

170

            return Ok(blocks);

171

172

173

        // Introduce new b and b' variables.

174

        let mut b_vars = manager_ref

175

            .with_manager_exclusive(|manager| {

176

                manager.add_named_vars([format!("b_{iteration}"), format!("b_prime_{iteration}")])

177

})

178

            .map_err(|e| e.to_string())?;

179

180

        let b_var = b_vars.next().expect("Two variables are added");

181

        let b_prime_var = b_vars.next().expect("Two variables are added");

182

183

        // Update various structs related to the b variables.

184

        b_variables.push(b_var);

185

        b_prime_variables.push(b_prime_var);

186

187

        b_vars_bdd = manager_ref.with_manager_shared(|manager| b_vars_bdd.and(&BDDFunction::var(manager, b_var)?))?;

188

        b_prime_vars_bdd = manager_ref

189

            .with_manager_shared(|manager| b_prime_vars_bdd.and(&BDDFunction::var(manager, b_prime_var)?))?;

190

191

        b_to_b_prime.push((b_var, b_prime_var));

192

193

        // TODO: implement actual state splitting using the new b variable.

194

        // B_{i+1}(p, b·b1) = B_i(p, b1) ∧ (b ⟺ ∃p': T_a(p, p') ∧ B_i(p', b1))

195

        blocks = manager_ref.with_manager_shared(|manager| -> Result<BDDFunction, OutOfMemory> {

196

            blocks.and(&BDDFunction::var(

197

                manager,

198

                *b_variables.last().expect("At least one b variable is added"),

199

)?)

200

        })?;

201

202

        iteration += 1;

203

        progress.print(iteration);

204

205