Grcov report - translate.rs

1

use log::debug;

2

use log::info;

3

use log::trace;

4

use oxidd::BooleanFunction;

5

use oxidd::ManagerRef;

6

use oxidd::bdd::BDDFunction;

7

use oxidd::bdd::BDDManagerRef;

8

9

use merc_collections::IndexedSet;

10

use merc_io::TimeProgress;

11

use merc_lts::LTS;

12

use merc_lts::StateIndex;

13

use merc_syntax::ActFrm;

14

use merc_syntax::ActFrmBinaryOp;

15

use merc_syntax::Action;

16

use merc_syntax::FixedPointOperator;

17

use merc_syntax::ModalityOperator;

18

use merc_syntax::MultiAction;

19

use merc_syntax::RegFrm;

20

use merc_syntax::StateFrm;

21

use merc_syntax::StateFrmOp;

22

use merc_utilities::MercError;

23

24

use crate::FeatureTransitionSystem;

25

use crate::ModalEquationSystem;

26

use crate::Player;

27

use crate::Priority;

28

use crate::VariabilityParityGame;

29

use crate::VertexIndex;

30

use crate::compute_reachable;

31

use crate::make_vpg_total;

32

33

/// Translates a feature transition system into a variability parity game.

34

1

pub fn translate(

35

1

    manager_ref: &BDDManagerRef,

36

1

    fts: &FeatureTransitionSystem,

37

1

    configuration: BDDFunction,

38

1

    formula: &StateFrm,

39

1

) -> Result<VariabilityParityGame, MercError> {

40

    // Parses all labels into MultiAction once

41

1

    let parsed_labels: Result<Vec<MultiAction>, MercError> =

42

5

        fts.labels().iter().map(|label| MultiAction::parse(label)).collect();

43

44

    // Simplify the labels by stripping BDD information

45

1

    let simplified_labels: Vec<MultiAction> = parsed_labels?

46

1

        .iter()

47

1

        .map(strip_feature_configuration_from_multi_action)

48

1

        .collect();

49

50

1

    let equation_system = ModalEquationSystem::new(formula);

51

1

    debug!("{}", equation_system);

52

1

    let mut algorithm = Translation::new(

53

1

        fts,

54

1

        &simplified_labels,

55

1

        &equation_system,

56

1

        manager_ref.with_manager_shared(|manager| BDDFunction::t(manager)),

57

);

58

59

1

    algorithm.translate(fts.initial_state_index(), 0)?;

60

61

    // Convert the feature diagram (with names) to a VPG

62

1

    let variables: Vec<BDDFunction> = fts.features().values().cloned().collect();

63

64

1

    let result = VariabilityParityGame::from_edges(

65

1

        manager_ref,

66

1

        VertexIndex::new(0),

67

1

        algorithm.vertices.iter().map(|(p, _)| p).cloned().collect(),

68

1

        algorithm.vertices.into_iter().map(|(_, pr)| pr).collect(),

69

1

        configuration,

70

1

        variables,

71

2

        || algorithm.edges.iter().cloned(),

72

);

73

74

    // Check that all vertices are reachable from the initial vertex. After

75

    // totality it could be that the true or false nodes are not reachable.

76

1

    if cfg!(debug_assertions) {

77

1

        let (_, reachable_vertices) = compute_reachable(&result);

78

1

        debug_assert!(

79

23

            reachable_vertices.iter().all(|v| v.is_some()),

80

            "Not all vertices are reachable from the initial vertex"

81

);

82

83

84

    // Ensure that the result is a total VPG.

85

1

    let total_result = if !result.is_total(manager_ref)? {

86

1

        make_vpg_total(manager_ref, &result)?

87

    } else {

88

        result

89

};

90

91

1

    Ok(total_result)

92

1

93

94

/// Is used to distinguish between StateFrm and Equation vertices in the vertex map.

95

#[derive(Clone, Debug, PartialEq, Eq, Hash)]

96

enum Formula<'a> {

97

    StateFrm(&'a StateFrm),

98

    Equation(usize),

99

100

101

/// Local struct to keep track of the translation state

102

///

103

/// Implements the translation from (s, Ψ) pairs to VPG vertices and edges.

104

/// However, to avoid the complication of merging sub-results we immediately

105

/// store the vertices and edges into mutable vectors. Furthermore, to avoid

106

/// stack overflows we use a breadth-first search approach with a queue. This

107

/// means that during queuing we immediately assign a fresh index to each (s, Ψ)

108

/// pair (if it does not yet exist) and then queue it to assign its actual

109

/// values later on.

110

struct Translation<'a> {

111

    vertex_map: IndexedSet<(StateIndex, Formula<'a>)>,

112

    vertices: Vec<(Player, Priority)>,

113

    edges: Vec<(VertexIndex, BDDFunction, VertexIndex)>,

114

115

    // Used for the breadth first search.

116

    queue: Vec<(StateIndex, Formula<'a>, VertexIndex)>,

117

118

    /// The parsed labels of the FTS.

119

    parsed_labels: &'a Vec<MultiAction>,

120

121

    /// The feature transition system being translated.

122

    fts: &'a FeatureTransitionSystem,

123

124

    /// A reference to the modal equation system being translated.

125

    equation_system: &'a ModalEquationSystem,

126

127

    /// The BDD representing the "true" feature configuration.

128

    true_bdd: BDDFunction,

129

130

    /// Use to print progress information.

131

    progress: TimeProgress<usize>,

132

133

134

impl<'a> Translation<'a> {

135

    /// Creates a new translation instance.

136

1

    fn new(

137

1

        fts: &'a FeatureTransitionSystem,

138

1

        parsed_labels: &'a Vec<MultiAction>,

139

1

        equation_system: &'a ModalEquationSystem,

140

1

        true_bdd: BDDFunction,

141

1

    ) -> Self {

142

1

        let progress: TimeProgress<usize> = TimeProgress::new(

143

            |num_of_vertices: usize| {

144

                info!("Translated {} vertices...", num_of_vertices);

145

},

146

1,

147

);

148

149

1

        Self {

150

1

            vertex_map: IndexedSet::new(),

151

1

            vertices: Vec::new(),

152

1

            edges: Vec::new(),

153

1

            queue: Vec::new(),

154

1

            fts,

155

1

            parsed_labels,

156

1

            equation_system,

157

1

            true_bdd,

158

1

            progress,

159

1

160

1

161

162

    /// Perform the actual translation.

163

1

    fn translate(&mut self, initial_state: StateIndex, initial_equation_index: usize) -> Result<(), MercError> {

164

        // We store (state, formula, N) into the queue, where N is the vertex number assigned to this pair. This means

165

        // that during the traversal we can assume this N to exist.

166

1

        self.queue = vec![(

167

1

            initial_state,

168

1

            Formula::Equation(initial_equation_index),

169

1

            VertexIndex::new(0),

170

1

)];

171

1

        self.vertices.push((Player::Odd, Priority::new(0))); // Placeholder for the initial vertex

172

173

25

        while let Some((s, formula, vertex_index)) = self.queue.pop() {

174

24

            debug!("Translating vertex {}: (s={}, formula={:?})", vertex_index, s, formula);

175

24

            self.progress.print(self.vertices.len());

176

24

            match formula {

177

19

                Formula::StateFrm(f) => {

178

19

                    self.translate_vertex(s, f, vertex_index);

179

19

180

5

                Formula::Equation(i) => {

181

5

                    self.translate_equation(s, i, vertex_index);

182

5

183

184

185

186

1

        Ok(())

187

1

188

189

    /// Translate a single vertex (s, Ψ) into the variability parity game vertex and its outgoing edges.

190

///

191

    /// The `fts` and `parsed_labels` are used to find the outgoing transitions matching the modalities in the formula.

192

///

193

    /// These are stored in the provided `vertices` and `edges` vectors.

194

    /// The `vertex_map` is used to keep track of already translated vertices.

195

///

196

    /// This function is recursively called for subformulas.

197

19

    pub fn translate_vertex(&mut self, s: StateIndex, formula: &'a StateFrm, vertex_index: VertexIndex) {

198

19

        match formula {

199

            StateFrm::True => {

200

                // (s, true) → odd, 0

201

                self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

202

203

            StateFrm::False => {

204

                // (s, false) → even, 0

205

                self.vertices[vertex_index] = (Player::Even, Priority::new(0));

206

207

6

            StateFrm::Binary { op, lhs, rhs } => {

208

6

                match op {

209

6

                    StateFrmOp::Conjunction => {

210

6

                        // (s, Ψ_1 ∧ Ψ_2) →_P odd, (s, Ψ_1) and (s, Ψ_2), 0

211

6

                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

212

6

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

213

6

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

214

6

215

6

                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_1));

216

6

                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_2));

217

6

218

                    StateFrmOp::Disjunction => {

219

                        // (s, Ψ_1 ∨ Ψ_2) →_P even, (s, Ψ_1) and (s, Ψ_2), 0

220

                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

221

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

222

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

223

224

                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_1));

225

                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_2));

226

227

                    _ => {

228

                        unimplemented!("Cannot translate binary operator in {}", formula);

229

230

231

232

4

            StateFrm::Id(identifier, _args) => {

233

4

                let (i, _equation) = self

234

4

                    .equation_system

235

4

                    .find_equation_by_identifier(identifier)

236

4

                    .expect("Variable must correspond to an equation");

237

4

238

4

                self.vertices[vertex_index] = (Player::Odd, Priority::new(0)); // The priority and owner do not matter here

239

4

                let equation_vertex = self.queue_vertex(s, Formula::Equation(i));

240

4

                self.edges.push((vertex_index, self.true_bdd.clone(), equation_vertex));

241

4

242

            StateFrm::Modality {

243

9

                operator,

244

9

                formula,

245

9

                expr,

246

            } => {

247

9

                match operator {

248

                    ModalityOperator::Box => {

249

                        // (s, [a] Ψ) → odd, (s', Ψ) for all s' with s -a-> s', 0

250

9

                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

251

252

12

                        for transition in self.fts.outgoing_transitions(s) {

253

12

                            let action = &self.parsed_labels[*transition.label];

254

255

12

                            trace!("Matching action {} against formula {}", action, formula);

256

257

12

                            if match_regular_formula(formula, action) {

258

4

                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

259

4

260

4

                                self.edges.push((

261

4

                                    vertex_index,

262

4

                                    self.fts.feature_label(transition.label).clone(),

263

4

                                    s_prime_psi,

264

4

));

265

8

266

267

268

                    ModalityOperator::Diamond => {

269

                        // (s, <a> Ψ) → even, (s', Ψ) for all s' with s -a-> s', 0

270

                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

271

272

                        for transition in self.fts.outgoing_transitions(s) {

273

                            let action = &self.parsed_labels[*transition.label];

274

275

                            if match_regular_formula(formula, action) {

276

                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

277

278

                                self.edges.push((

279

                                    vertex_index,

280

                                    self.fts.feature_label(transition.label).clone(),

281

                                    s_prime_psi,

282

));

283

284

285

286

287

288

            _ => {

289

                unimplemented!("Cannot translate formula {}", formula);

290

291

292

19

293

294

    /// Applies the translation to the given (s, equation) vertex.

295

5

    fn translate_equation(&mut self, s: StateIndex, equation_index: usize, vertex_index: VertexIndex) {

296

5

        let equation = self.equation_system.equation(equation_index);

297

5

        match equation.operator() {

298

3

            FixedPointOperator::Least => {

299

3

                // (s, μ X. Ψ) →_P odd, (s, Ψ[x := μ X. Ψ]), 2 * floor(AD(Ψ)/2) + 1. In Rust division is already floor.

300

3

                self.vertices[vertex_index] = (

301

3

                    Player::Odd,

302

3

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2) + 1),

303

3

);

304

3

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

305

3

                self.edges.push((vertex_index, self.true_bdd.clone(), s_psi));

306

3

307

2

            FixedPointOperator::Greatest => {

308

2

                // (s, ν X. Ψ) →_P even, (s, Ψ[x := ν X. Ψ]), 2 * (AD(Ψ)/2). In Rust division is already floor.

309

2

                self.vertices[vertex_index] = (

310

2

                    Player::Even,

311

2

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2)),

312

2

);

313

2

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

314

2

                self.edges.push((vertex_index, self.true_bdd.clone(), s_psi));

315

2

316

317

5

318

319

    /// Queues a new pair to be translated, returning its vertex index.

320

25

    fn queue_vertex(&mut self, s: StateIndex, formula: Formula<'a>) -> VertexIndex {

321

25

        let (index, inserted) = self.vertex_map.insert((s, formula.clone()));

322

25

        let vertex_index = VertexIndex::new(*index);

323

324

25

        if inserted {

325

23

            // New vertex, assign placeholder values

326

23

            self.vertices.resize(*vertex_index + 1, (Player::Odd, Priority::new(0)));

327

23

            self.queue.push((s, formula, vertex_index));

328

23

329

330

25

        vertex_index

331

25

332

333

334

/// Removes the BDD information from the multi-action, i.e., only keeps the action labels.

335

5

fn strip_feature_configuration_from_multi_action(multi_action: &MultiAction) -> MultiAction {

336

    MultiAction {

337

5

        actions: multi_action

338

5

            .actions

339

5

            .iter()

340

5

            .map(|action| Action {

341

4

                id: action.id.clone(),

342

4

                args: Vec::new(),

343

4

})

344

5

            .collect(),

345

346

5

347

348

/// Returns true iff the given action matches the regular formula.

349

12

fn match_regular_formula(formula: &RegFrm, action: &MultiAction) -> bool {

350

12

    match formula {

351

12

        RegFrm::Action(action_formula) => match_action_formula(action_formula, action),

352

        RegFrm::Choice { lhs, rhs } => match_regular_formula(lhs, action) || match_regular_formula(rhs, action),

353

        _ => {

354

            unimplemented!("Cannot translate regular formula {}", formula);

355

356

357

12

358

359

/// Returns true iff the given action matches the action formula.

360

12

fn match_action_formula(formula: &ActFrm, action: &MultiAction) -> bool {

361

12

    match formula {

362

        ActFrm::True => true,

363

        ActFrm::False => false,

364

12

        ActFrm::MultAct(expected_action) => expected_action == action,

365

        ActFrm::Binary { op, lhs, rhs } => match op {

366

            ActFrmBinaryOp::Union => match_action_formula(lhs, action) || match_action_formula(rhs, action),

367

            ActFrmBinaryOp::Intersect => match_action_formula(lhs, action) && match_action_formula(rhs, action),

368

            _ => {

369

                unimplemented!("Cannot translate binary operator {}", formula);

370

371

},

372

        ActFrm::Negation(expr) => !match_action_formula(expr, action),

373

        _ => {

374

            unimplemented!("Cannot translate action formula {}", formula);

375

376

377

12

378

379

#[cfg(test)]

380

mod tests {

381

    use merc_macros::merc_test;

382

    use merc_syntax::UntypedStateFrmSpec;

383

384

    use crate::FeatureDiagram;

385

    use crate::read_fts;

386

387

    use super::*;

388

389

    #[merc_test]

390

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

391

    fn test_running_example() {

392

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

393

394

        let fd = FeatureDiagram::from_reader(

395

            &manager_ref,

396

            include_bytes!("../../../examples/vpg/running_example_fts.fd") as &[u8],

397

398

        .unwrap();

399

        let fts = read_fts(

400

            &manager_ref,

401

            include_bytes!("../../../examples/vpg/running_example_fts.aut") as &[u8],

402

            fd.features().clone(),

403

404

        .unwrap();

405

406

        let formula = UntypedStateFrmSpec::parse(include_str!("../../../examples/vpg/running_example.mcf")).unwrap();

407

408

        let _vpg = translate(&manager_ref, &fts, fd.configuration().clone(), &formula.formula).unwrap();

409

410