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

///

22

/// Returns the block relation `B(p, b)` together with the block-encoding

23

/// variables `b` (in allocation order). The block variables are required to

24

/// interpret the relation, e.g. to feed it into [`crate::quotient_symbolic`].

25

pub fn refine_bisimulation(

26

    manager_ref: &BDDManagerRef,

27

    lts: &SymbolicLtsBdd,

28

) -> Result<(BDDFunction, Vec<VarNo>), MercError> {

29

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

30

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

31

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

32

33

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

34

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

35

            bdd = bdd.and(&var)?;

36

37

38

        Ok(bdd)

39

    })?;

40

41

    // Computes the vector of action label BDDs.

42

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

43

        lts.action_variables()

44

            .iter()

45

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

46

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

47

    })?;

48

49

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

50

    let mut split_groups = Vec::new();

51

    for group in lts.transition_groups() {

52

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

53

54

        for cube in CubeIterAll::with_variables(&action_bdd, lts.action_variables()) {

55

            // Every cube is a single action.

56

            let cube = cube?;

57

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

58

59

            split_groups.push(SummandGroupBdd::new(

60

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

61

                group.read_variables().to_vec(),

62

                group.write_variables().to_vec(),

63

));

64

65

66

67

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

68

    let q_variables = manager_ref

69

        .with_manager_exclusive(|manager| {

70

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

71

})

72

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

73

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

74

75

    let q_prime_variables = manager_ref

76

        .with_manager_exclusive(|manager| {

77

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

78

})

79

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

80

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

81

82

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

83

    manager_ref.with_manager_exclusive(|manager| {

84

        let order: Vec<_> = lts

85

            .state_variables()

86

            .iter()

87

            .zip(q_variables.iter())

88

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

89

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

90

            .collect();

91

92

        oxidd_reorder::set_var_order(manager, &order)

93

});

94

95

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

96

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

97

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

98

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

99

    let action_vars_bdd = compute_vars_bdd(manager_ref, lts.action_variables())?.1;

100

101

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

102

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

103

        .state_variables()

104

        .iter()

105

        .cloned()

106

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

107

        .collect();

108

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

109

        .iter()

110

        .cloned()

111

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

112

        .collect();

113

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

114

        .next_state_variables()

115

        .iter()

116

        .cloned()

117

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

118

        .collect();

119

120

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

121

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

122

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

123

124

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

125

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

126

127

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

128

129

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

130

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

131

132

    let progress = TimeProgress::new(

133

        |iteration: usize| {

134

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

135

},

136

1,

137

);

138

139

    let mut iteration = 0;

140

    loop {

141

        // Check if B_i is stable w.r.t. all the transition relations. When an unstable group is

142

        // found, save it along with the precomputed B_i(p', b2) for use in the splitting step.

143

        let mut unstable_group: Option<&SummandGroupBdd> = None;

144

        let mut unstable_blocks_p_prime_b_prime: Option<BDDFunction> = None;

145

146

        for group in &split_groups {

147

            // 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')

148

149

            // Rename B_i(p, b) to B_i(p', b2) via the chain p -> q -> p' then b -> b'

150

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

151

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

152

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

153

154

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

155

156

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

157

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

158

159

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

160

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

161

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

162

163

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

164

            let antecant = relation_q_q_prime

165

                .and(&blocks_p_prime_b_prime)?

166

                .and(&blocks_q_prime_b_prime)?

167

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

168

169

            let group_stable = condition

170

                .imp(&antecant)?

171

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

172

                .satisfiable();

173

174

            if !group_stable {

175

                unstable_group = Some(group);

176

                unstable_blocks_p_prime_b_prime = Some(blocks_p_prime_b_prime);

177

                break;

178

179

180

181

        let Some(group) = unstable_group else {

182

            return Ok((blocks, b_variables));

183

};

184

        let blocks_p_prime_b_prime = unstable_blocks_p_prime_b_prime.unwrap();

185

186

        // Introduce new b and b' variables.

187

        let mut b_vars = manager_ref

188

            .with_manager_exclusive(|manager| {

189

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

190

})

191

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

192

193

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

194

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

195

196

        // Update various structs related to the b variables.

197

        b_variables.push(b_var);

198

        b_prime_variables.push(b_prime_var);

199

200

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

201

        b_prime_vars_bdd = manager_ref

202

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

203

204

        b_to_b_prime.push((b_var, b_prime_var));

205

206

        // Implement state splitting: B_{i+1}(p, b, b1, b2) = B_i(p, b1) ∧ (b ⟺ ∃p', a: T_a(p, p') ∧ B_i(p', b2))

207

//

208

        // blocks_p_prime_b_prime already holds B_i(p', b2). Quantify out p' and the fixed action

209

        // label variables to obtain a predicate over (p, b2) that says "p can do a to reach

210

        // the block encoded by b2".

211

        let to_quantify = p_prime_bdd.and(&action_vars_bdd)?;

212

        let reachable = group.relation().and(&blocks_p_prime_b_prime)?.exists(&to_quantify)?;

213

214

        let b_new_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::var(manager, b_var))?;

215

        blocks = blocks.and(&b_new_bdd.equiv(&reachable)?)?;

216

217

        iteration += 1;

218

        progress.print(iteration);

219

220

221

222

// #[cfg(test)]

223

// mod tests {

224

//     use merc_lts::LTS;

225

//     use merc_lts::LtsBuilderMem;

226

//     use merc_reduction::Equivalence;

227

//     use merc_reduction::compare_lts;

228

//     use merc_reduction::reduce_lts;

229

//     use merc_utilities::Timing;

230

231

//     use merc_utilities::random_test;

232

233

//     use crate::SymbolicLtsBdd;

234

//     use crate::bdd::refine_bisimulation;

235

//     use crate::convert_symbolic_lts;

236

//     use crate::convert_symbolic_lts_bdd;

237

//     use crate::quotient_symbolic;

238

//     use crate::random_symbolic_lts;

239

240

//     #[test]

241

//     #[ignore = "refine_bisimulation aborts in oxidd_reorder::set_var_order; see function docs"]

242

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

243

//     fn test_random_refine_bisimulation() {

244

//         random_test(100, |rng| {

245

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

246

247

//             let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap();

248

249

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

250

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

251

252

//             let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new());

253

//             let explicit_lts = convert_symbolic_lts(&ldd_manager, &mut builder, &lts).unwrap();

254

//             let explicit_lts_reduced =

255

//                 reduce_lts(explicit_lts.clone(), Equivalence::StrongBisim, false, &Timing::new());

256

257

//             // refine_bisimulation returns B(p, b) together with the block variables b,

258

//             // which is exactly the (partition, block_vars) pair quotient_symbolic expects.

259

//             let (partition, block_vars) = refine_bisimulation(&manager_ref, &lts_bdd).unwrap();

260

261

//             let quotient_lts = quotient_symbolic(&manager_ref, &lts_bdd, &partition, &block_vars).unwrap();

262

263

//             let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new());

264

//             let symbolic_lts_reduced = convert_symbolic_lts_bdd(&manager_ref, &mut builder, &quotient_lts).unwrap();

265

266

//             assert_eq!(

267

//                 explicit_lts_reduced.num_of_states(),

268

//                 symbolic_lts_reduced.num_of_states()

269

//             );

270

//             assert_eq!(

271

//                 explicit_lts_reduced.num_of_transitions(),

272

//                 symbolic_lts_reduced.num_of_transitions()

273

//             );

274

275

//             assert!(

276

//                 compare_lts(

277

//                     Equivalence::StrongBisim,

278

//                     explicit_lts_reduced,

279

//                     symbolic_lts_reduced,

280

//                     false,

281

//                     &Timing::new()

282

//                 ),

283

//                 "The refine_bisimulation quotient should be bisimilar to the explicit reduction"

284

//             );

285

//         });

286

//     }

287

// }