Grcov report - variability

1

//! To keep with the theory, we use capitalized variable names for sets of vertices.

2

//! Authors: Maurice Laveaux, Sjef van Loo, Erik de Vink and Tim A.C. Willemse

3

#![allow(nonstandard_style)]

4

#![allow(unused)]

5

6

use std::fmt;

7

use std::ops::Index;

8

9

use bitvec::bitvec;

10

use bitvec::order::Lsb0;

11

use bitvec::vec::BitVec;

12

use log::debug;

13

use log::info;

14

use log::trace;

15

use merc_symbolic::FormatConfig;

16

use oxidd::BooleanFunction;

17

use oxidd::Edge;

18

use oxidd::Function;

19

use oxidd::Manager;

20

use oxidd::ManagerRef;

21

use oxidd::bdd::BDDFunction;

22

use oxidd::bdd::BDDManagerRef;

23

use oxidd::util::AllocResult;

24

use oxidd::util::OptBool;

25

use oxidd_core::util::EdgeDropGuard;

26

27

use merc_symbolic::FormatConfigSet;

28

use merc_symbolic::minus;

29

use merc_symbolic::minus_edge;

30

use merc_utilities::MercError;

31

use merc_utilities::Timing;

32

33

use crate::PG;

34

use crate::Player;

35

use crate::Priority;

36

use crate::Projected;

37

use crate::Repeat;

38

use crate::Set;

39

use crate::Solver;

40

use crate::Submap;

41

use crate::VariabilityParityGame;

42

use crate::VariabilityPredecessors;

43

use crate::VertexIndex;

44

use crate::VpgSolver;

45

use crate::combine;

46

use crate::compute_reachable;

47

use crate::project_variability_parity_games_iter;

48

use crate::solve_priority_promotion;

49

use crate::solve_zielonka;

50

use crate::x_and_not_x;

51

52

/// Solves the given variability parity game using the specified Zielonka algorithm variant.

53

300

pub fn solve_variability_zielonka(

54

300

    manager_ref: &BDDManagerRef,

55

300

    game: &VariabilityParityGame,

56

300

    variant: VpgSolver,

57

300

    alternative_solving: bool,

58

300

) -> Result<[Submap; 2], MercError> {

59

300

    debug_assert!(

60

300

        game.is_total(manager_ref)?,

61

        "Zielonka solver requires a total parity game"

62

);

63

64

300

    let mut zielonka = VariabilityZielonkaSolver::new(manager_ref, game, alternative_solving);

65

66

    // Determine the initial set of vertices V

67

300

    let V = Submap::new(

68

300

        manager_ref,

69

300

        if alternative_solving {

70

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

71

        } else {

72

300

            game.configuration().clone()

73

},

74

300

        game.num_of_vertices(),

75

);

76

77

300

    let full_V = V.clone();

78

300

    let (W0, W1) = match variant {

79

200

        VpgSolver::Family => zielonka.solve_recursive(V, 0)?,

80

100

        VpgSolver::FamilyOptimisedLeft => zielonka.zielonka_family_optimised(V, 0)?,

81

        VpgSolver::Product => {

82

            panic!("Product-based Zielonka is implemented in solve_product_zielonka");

83

84

};

85

86

300

    debug!("recursive calls" = zielonka.recursive_calls; "Performed {} recursive calls", zielonka.recursive_calls);

87

300

    if cfg!(debug_assertions) {

88

300

        zielonka.check_partition(&W0, &W1, &full_V)?;

89

90

91

300

    let (W0, W1) = if alternative_solving {

92

        // Intersect the results with the game's configuration

93

        let config = game.configuration();

94

95

            W0.and_function(manager_ref, config)?,

96

            W1.and_function(manager_ref, config)?,

97

98

    } else {

99

300

        (W0, W1)

100

};

101

102

300

    Ok([W0, W1])

103

300

104

105

/// Solves the given variability parity game using the product-based Zielonka algorithm.

106

100

pub fn solve_variability_product_zielonka<'a>(

107

100

    vpg: &'a VariabilityParityGame,

108

100

    solver: Solver,

109

100

    timing: &'a Timing,

110

100

) -> impl Iterator<Item = Result<(Vec<OptBool>, BDDFunction, [Set; 2]), MercError>> + 'a {

111

330

    project_variability_parity_games_iter(vpg, timing).map(move |result| {

112

330

        match result {

113

330

            Ok((Projected { bits, bdd, game }, timing)) => {

114

330

                let (reachable_pg, projection) = timing.measure("reachable", || compute_reachable(&game));

115

116

330

                debug!("Solving projection on {}...", FormatConfig(&bits));

117

118

                // We cannot yet construct a strategy for the VPG solver.

119

330

                let (pg_solution, _) = match solver {

120

330

                    Solver::Zielonka => solve_zielonka(&reachable_pg, false),

121

                    Solver::PriorityPromotion => solve_priority_promotion(&reachable_pg, false),

122

};

123

330

                let mut new_solution = [

124

330

                    bitvec![usize, Lsb0; 0; vpg.num_of_vertices()],

125

330

                    bitvec![usize, Lsb0; 0; vpg.num_of_vertices()],

126

330

];

127

7260

                for v in game.iter_vertices() {

128

7260

                    if let Some(proj_v) = projection[*v] {

129

                        // Vertex is reachable in the projection, set its solution

130

953

                        if pg_solution[0][proj_v] {

131

480

                            new_solution[0].set(*v, true);

132

480

133

953

                        if pg_solution[1][proj_v] {

134

473

                            new_solution[1].set(*v, true);

135

480

136

6307

137

138

139

330

                Ok((bits, bdd, new_solution))

140

141

            Err(result) => Err(result),

142

143

330

})

144

100

145

146

/// Verifies that the solution obtained from the variability product-based Zielonka solver

147

/// is consistent with the solution of the variability parity game.

148

100

pub fn verify_variability_product_zielonka_solution(

149

100

    vpg: &VariabilityParityGame,

150

100

    solution: &[Submap; 2],

151

100

    timing: &Timing,

152

100

) -> Result<(), MercError> {

153

100

    info!("Verifying variability product-based Zielonka solution...");

154

330

    solve_variability_product_zielonka(vpg, Solver::Zielonka, timing).try_for_each(|res| {

155

330

        match res {

156

330

            Ok((bits, cube, pg_solution)) => {

157

7260

                for v in vpg.iter_vertices() {

158

7260

                    if pg_solution[0][*v] {

159

                        // Won by Even

160

480

                        assert!(

161

480

                            solution[0][v].and(&cube)?.satisfiable(),

162

                            "Projection {}, vertex {v} is won by even in the product, but not in the vpg",

163

                            FormatConfig(&bits)

164

);

165

6780

166

167

7260

                    if pg_solution[1][*v] {

168

                        // Won by Odd

169

473

                        assert!(

170

473

                            solution[1][v].and(&cube)?.satisfiable(),

171

                            "Projection {}, vertex {v} is won by odd in the product, but not in the vpg",

172

                            FormatConfig(&bits)

173

);

174

6787

175

176

177

330

                Ok(())

178

179

            Err(res) => Err(res),

180

181

330

    })?;

182

183

100

    Ok(())

184

100

185

186

struct VariabilityZielonkaSolver<'a> {

187

    game: &'a VariabilityParityGame,

188

189

    manager_ref: &'a BDDManagerRef,

190

191

    /// Instead of solving the game only for the valid configurations, solve for

192

    /// all configurations and then restrict the result at the end.

193

    alternative_solving: bool,

194

195

    /// Reused temporary queue for attractor computation.

196

    temp_queue: Vec<VertexIndex>,

197

198

    /// Keep track of the vertices in the temp_queue above in the attractor computation.

199

    temp_vertices: BitVec<usize, Lsb0>,

200

201

    /// Stores the predecessors of the game.

202

    predecessors: VariabilityPredecessors,

203

204

    /// Temporary storage for vertices per priority.

205

    priority_vertices: Vec<Vec<VertexIndex>>,

206

207

    /// The BDD function representing the universe configuration.

208

    true_bdd: BDDFunction,

209

210

    /// The BDD function representing the empty configuration.

211

    false_bdd: BDDFunction,

212

213

    /// Keeps track of the total number of recursive calls.

214

    recursive_calls: usize,

215

216

217

impl<'a> VariabilityZielonkaSolver<'a> {

218

    /// Creates a new VariabilityZielonkaSolver for the given game.

219

300

    pub fn new(manager_ref: &'a BDDManagerRef, game: &'a VariabilityParityGame, alternative_solving: bool) -> Self {

220

        // Keep track of the vertices for each priority

221

300

        let mut priority_vertices = Vec::new();

222

223

6600

        for v in game.iter_vertices() {

224

6600

            let prio = game.priority(v);

225

226

7498

            while prio >= priority_vertices.len() {

227

898

                priority_vertices.push(Vec::new());

228

898

229

230

6600

            priority_vertices[prio].push(v);

231

232

233

300

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

234

300

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

235

236

300

        Self {

237

300

            game,

238

300

            manager_ref,

239

300

            temp_queue: Vec::new(),

240

300

            temp_vertices: BitVec::repeat(false, game.num_of_vertices()),

241

300

            predecessors: VariabilityPredecessors::new(manager_ref, game),

242

300

            priority_vertices,

243

300

            recursive_calls: 0,

244

300

            alternative_solving,

245

300

            true_bdd,

246

300

            false_bdd,

247

300

248

300

249

250

    /// Solves the variability parity game for the given set of vertices V.

251

2054

    fn solve_recursive(&mut self, gamma: Submap, depth: usize) -> Result<(Submap, Submap), MercError> {

252

2054

        self.recursive_calls += 1;

253

254

        // For debugging mostly

255

2054

        let indent = Repeat::new(" ", depth);

256

2054

        let gamma_copy = gamma.clone();

257

258

        // 1. if \gamma == \epsilon then

259

2054

        if gamma.is_empty() {

260

752

            return Ok((gamma.clone(), gamma));

261

1302

262

263

        // 5. m := max { p(v) | v in V && \gamma(v) \neq \emptyset }

264

1302

        let (highest_prio, lowest_prio) = self.get_highest_lowest_prio(&gamma);

265

266

        // 6. x := m mod 2

267

1302

        let x = Player::from_priority(&highest_prio);

268

1302

        let not_x = x.opponent();

269

270

        // 7. \mu := lambda v in V. bigcup { \gamma(v) | p(v) = m }

271

1302

        let mut mu = Submap::new(self.manager_ref, self.false_bdd.clone(), self.game.num_of_vertices());

272

273

1302

        self.manager_ref

274

1302

            .with_manager_shared(|manager| -> Result<(), MercError> {

275

9829

                for v in &self.priority_vertices[*highest_prio] {

276

9829

                    mu.set(manager, *v, gamma[*v].clone());

277

9829

278

279

1302

                Ok(())

280

1302

            })?;

281

282

1302

        debug!(

283

            "|gamma| = {}, m = {}, l = {}, x = {}, |mu| = {}",

284

            gamma.number_of_non_empty(),

285

            highest_prio,

286

            lowest_prio,

287

x,

288

            mu.number_of_non_empty()

289

);

290

291

1302

        trace!("{indent}Vertices in gamma: {:?}", gamma);

292

1302

        trace!("{indent}Vertices in mu: {:?}", mu);

293

1302

        let alpha = self.attractor(x, &gamma, mu)?;

294

1302

        trace!("{indent}Vertices in alpha: {:?}", alpha);

295

296

        // 9. (omega'_0, omega'_1) := solve(\gamma \ \alpha)

297

1302

        debug!(

298

            "{indent}zielonka_family(gamma \\ alpha), |alpha| = {}",

299

            alpha.number_of_non_empty()

300

);

301

1302

        let (omega1_0, omega1_1) = self.solve_recursive(gamma.clone().minus(self.manager_ref, &alpha)?, depth + 1)?;

302

303

1302

        let (mut omega1_x, mut omega1_not_x) = x_and_not_x(omega1_0, omega1_1, x);

304

1302

        if omega1_not_x.is_empty() {

305

            // 11. omega_x := omega'_x \cup alpha

306

750

            omega1_x = omega1_x.or(self.manager_ref, &alpha)?;

307

            // 20. return (omega_0, omega_1)

308

750

            Ok(combine(omega1_x, omega1_not_x, x))

309

        } else {

310

            // 14. \beta := attr_notalpha(\omega'_notx)

311

552

            let beta = self.attractor(not_x, &gamma, omega1_not_x)?;

312

            // 15. (omega''_0, omega''_1) := solve(gamma \ beta)

313

552

            debug!(

314

                "{indent}solve_rec(gamma \\ beta), |beta| = {}",

315

                beta.number_of_non_empty()

316

);

317

552

            trace!("{indent}Vertices in beta: {:?}", beta);

318

319

552

            let (mut omega2_0, mut omega2_1) =

320

552

                self.solve_recursive(gamma.minus(self.manager_ref, &beta)?, depth + 1)?;

321

322

            // 17. omega''_notx := omega''_notx \cup \beta

323

552

            let (omega2_x, mut omega2_not_x) = x_and_not_x(omega2_0, omega2_1, x);

324

552

            omega2_not_x = omega2_not_x.or(self.manager_ref, &beta)?;

325

326

            // 20. return (omega_0, omega_1)

327

552

            if cfg!(debug_assertions) {

328

552

                self.check_partition(&omega2_x, &omega2_not_x, &gamma_copy)?;

329

330

552

            Ok(combine(omega2_x, omega2_not_x, x))

331

332

2054

333

334

    /// Left-optimised Zielonka solver that has improved theoretical complexity, but might be slower in practice.

335

1045

    fn zielonka_family_optimised(&mut self, gamma: Submap, depth: usize) -> Result<(Submap, Submap), MercError> {

336

1045

        self.recursive_calls += 1;

337

1045

        let indent = Repeat::new(" ", depth);

338

1045

        let gamma_copy = gamma.clone();

339

340

        // 1. if \gamma == \epsilon then

341

1045

        if gamma.is_empty() {

342

            // 2. return (\epsilon, \epsilon)

343

381

            return Ok((gamma.clone(), gamma));

344

664

345

346

        // 5. m := max { p(v) | v in V && \gamma(v) \neq \emptyset }

347

664

        let (highest_prio, lowest_prio) = self.get_highest_lowest_prio(&gamma);

348

349

        // 6. x := m mod 2

350

664

        let x = Player::from_priority(&highest_prio);

351

664

        let not_x = x.opponent();

352

353

        // 7. C := { c in \bigC | exists v in V : p(v) = m && c in \gamma(v) }

354

        // 8. \mu := lambda v in V. bigcup { \gamma(v) | p(v) = m }

355

664

        let mut mu = Submap::new(self.manager_ref, self.false_bdd.clone(), self.game.num_of_vertices());

356

357

664

        let mut C = self.false_bdd.clone();

358

359

664

        self.manager_ref

360

664

            .with_manager_shared(|manager| -> Result<(), MercError> {

361

5024

                for v in &self.priority_vertices[*highest_prio] {

362

5024

                    mu.set(manager, *v, gamma[*v].clone());

363

5024

                    C = C.or(&gamma[*v])?;

364

365

366

664

                Ok(())

367

664

            })?;

368

369

664

        debug!(

370

            "{indent}|gamma| = {}, m = {}, l = {}, x = {}, |mu| = {}",

371

            gamma.number_of_non_empty(),

372

            highest_prio,

373

            lowest_prio,

374

x,

375

            mu.number_of_non_empty()

376

);

377

378

        // 9. alpha := attr_x(\mu).

379

664

        trace!("{indent}gamma: {:?}", gamma);

380

664

        trace!("{indent}C: {}", FormatConfigSet(&C));

381

664

        let alpha = self.attractor(x, &gamma, mu)?;

382

664

        trace!("{indent}alpha: {:?}", alpha);

383

384

        // 10. (omega'_0, omega'_1) := solve(gamma \ alpha)

385

664

        debug!(

386

            "{indent}zielonka_family_opt(gamma \\ alpha) |alpha| = {}",

387

            alpha.number_of_non_empty()

388

);

389

664

        let (omega1_0, omega1_1) =

390

664

            self.zielonka_family_optimised(gamma.clone().minus(self.manager_ref, &alpha)?, depth + 1)?;

391

392

        // omega_prime[not_x] restricted to (gamma \ C)

393

664

        let C_restricted = minus(

394

664

            &if !self.alternative_solving {

395

664

                self.true_bdd.clone()

396

            } else {

397

                self.game.configuration().clone()

398

},

399

664

&C,

400

)?;

401

402

664

        let (mut omega1_x, omega1_not_x) = x_and_not_x(omega1_0, omega1_1, x);

403

664

        let omega1_not_x_restricted = omega1_not_x.clone().minus_function(self.manager_ref, &C_restricted)?;

404

405

        // 10.

406

664

        if omega1_not_x_restricted.is_empty() {

407

            // 11. omega'_x := omega'_x \cup A

408

383

            omega1_x = omega1_x.or(self.manager_ref, &alpha)?;

409

383

            if cfg!(debug_assertions) {

410

383

                self.check_partition(&omega1_x, &omega1_not_x, &gamma_copy)?;

411

412

413

            // 22. return (omega_0, omega_1)

414

383

            Ok(combine(omega1_x, omega1_not_x, x))

415

        } else {

416

            // C' := { c in C | exists v: c in omega'_not_x(v) }

417

281

            let mut C1 = self.false_bdd.clone();

418

6182

            for (_v, func) in omega1_not_x.iter() {

419

6182

                C1 = C1.or(func)?;

420

421

281

            C1 = C1.and(&C)?;

422

423

            // beta := attr_not_x(omega'_not_x | C')

424

281

            let C1_restricted = minus(

425

281

                &if self.alternative_solving {

426

                    self.true_bdd.clone()

427

                } else {

428

281

                    self.game.configuration().clone()

429

},

430

281

                &C1,

431

)?;

432

433

281

            let omega1_not_x_restricted1 = omega1_not_x.clone().minus_function(self.manager_ref, &C1_restricted)?;

434

281

            trace!("{indent}omega'_notx_restricted: {:?}", omega1_not_x_restricted1);

435

281

            let alpha1 = self.attractor(not_x, &gamma, omega1_not_x_restricted1)?;

436

281

            trace!("{indent}alpha': {:?}", alpha1);

437

438

            // Solve on (gamma | C') \ alpha'

439

281

            let gamma_restricted = gamma.minus_function(self.manager_ref, &C1_restricted)?;

440

441

281

            debug!("{indent}zielonka_family_opt((gamma | C') \\ alpha')");

442

281

            let (omega2_0, omega2_1) =

443

281

                self.zielonka_family_optimised(gamma_restricted.minus(self.manager_ref, &alpha1)?, depth + 1)?;

444

445

            // 18. omega'_x := omega'_x\C' cup alpha\C' cup omega''_x

446

            // 19. omega_not_x := omega'_not_x\C' cup omega''_x cup beta

447

281

            let (omega2_x, omega2_not_x) = x_and_not_x(omega2_0, omega2_1, x);

448

281

            let omega1_x_restricted = omega1_x.minus_function(self.manager_ref, &C1)?;

449

281

            let omega1_not_x_restricted = omega1_not_x.minus_function(self.manager_ref, &C1)?;

450

451

281

            let alpha_restricted = alpha.minus_function(self.manager_ref, &C1)?;

452

281

            let omega2_x_result = omega2_x.or(

453

281

                self.manager_ref,

454

281

                &omega1_x_restricted.or(self.manager_ref, &alpha_restricted)?,

455

)?;

456

281

            let omega2_not_x_result = omega2_not_x

457

281

                .or(self.manager_ref, &omega1_not_x_restricted)?

458

281

                .or(self.manager_ref, &alpha1)?;

459

460

281

            debug!("{indent}return (omega''_0, omega''_1)");

461

281

            Ok(combine(omega2_x_result, omega2_not_x_result, x))

462

463

1045

464

465

    /// Computes the attractor for `player` to the set `A` within the set of vertices `gamma`.

466

///

467

    /// # Details

468

///

469

    /// The definition of the attractor is as follows:

470

    ///     Attrx,γ (β) = intersection { α ⊆ γ | ∀v ∈ V, c ∈ C: (c ∈ β(v) ⇒ c ∈ α(v)) ∧

471

    ///          (v ∈ Vx ∧ (∃w ∈ V : v c −→ γ w ∧ c ∈ α(w)) ⇒ c ∈ α(v)) ∧

472

    ///          (v ∈ V¯x ∧ (∀w ∈ V : v c −→ γ w ⇒ c ∈ α(w)) ⇒ c ∈ α(v)) }

473

///

474

    /// The relation to the implementation is not entirely straightforward. The player `x` is called alpha here, and A is the beta set.

475

2799

    fn attractor(&mut self, alpha: Player, gamma: &Submap, mut A: Submap) -> Result<Submap, MercError> {

476

        // 2. Queue Q := {v \in V | A(v) != \emptyset }

477

2799

        debug_assert!(

478

2799

            self.temp_queue.is_empty(),

479

            "temp_queue should be empty at the start of attractor computation"

480

);

481

482

2799

        self.manager_ref.with_manager_shared(|manager| {

483

18017

            for v in A.iter_vertices(manager) {

484

18017

                self.temp_queue.push(v);

485

18017

486

18017

                // temp_vertices keeps track of which vertices are in the queue.

487

18017

                self.temp_vertices.set(*v, true);

488

18017

489

2799

});

490

491

        // 4. While Q not empty do

492

        // 5. w := Q.pop()

493

2799

        self.manager_ref

494

2799

            .with_manager_shared(|manager| -> Result<(), MercError> {

495

                // Used for satisfiability checks

496

2799

                let f_edge = EdgeDropGuard::new(manager, BDDFunction::f_edge(manager));

497

498

26626

                while let Some(w) = self.temp_queue.pop() {

499

23827

                    self.temp_vertices.set(*w, false);

500

501

                    // For every v \in Ew do

502

49420

                    for (v, edge_guard) in self.predecessors.predecessors(w) {

503

49420

                        let mut a = EdgeDropGuard::new(

504

49420

                            manager,

505

49420

                            BDDFunction::and_edge(

506

49420

                                manager,

507

49420

                                &EdgeDropGuard::new(

508

49420

                                    manager,

509

49420

                                    BDDFunction::and_edge(manager, gamma[v].as_edge(manager), A[w].as_edge(manager))?,

510

),

511

49420

                                edge_guard.as_edge(manager),

512

)?,

513

);

514

515

49420

                        if *a != *f_edge {

516

                            // 7. if v in V_\alpha

517

30553

                            if self.game.owner(v) == alpha {

518

6399

                                // 8. a := gamma(v) \intersect \theta(v, w) \intersect A(w)

519

6399

                                // This assignment has already been computed above.

520

6399

                            } else {

521

                                // 10. a := gamma(v)

522

24154

                                a = EdgeDropGuard::new(manager, gamma[v].clone().into_edge(manager));

523

                                // 11. for w' \in vE such that gamma(v) && theta(v, w') && \gamma(w') != \emptyset do

524

53702

                                for edge_w1 in self.game.outgoing_edges(v) {

525

53702

                                    let tmp = EdgeDropGuard::new(

526

53702

                                        manager,

527

53702

                                        BDDFunction::and_edge(

528

53702

                                            manager,

529

53702

                                            &EdgeDropGuard::new(

530

53702

                                                manager,

531

53702

                                                BDDFunction::and_edge(

532

53702

                                                    manager,

533

53702

                                                    gamma[v].as_edge(manager),

534

53702

                                                    edge_w1.label().as_edge(manager),

535

)?,

536

),

537

53702

                                            gamma[edge_w1.to()].as_edge(manager),

538

)?,

539

);

540

541

53702

                                    if *tmp != *f_edge {

542

                                        // 12. a := a && ((C \ (theta(v, w') && \gamma(w'))) \cup A(w'))

543

44787

                                        let tmp = EdgeDropGuard::new(

544

44787

                                            manager,

545

44787

                                            BDDFunction::and_edge(

546

44787

                                                manager,

547

44787

                                                edge_w1.label().as_edge(manager),

548

44787

                                                gamma[edge_w1.to()].as_edge(manager),

549

)?,

550

);

551

552

44787

                                        a = EdgeDropGuard::new(

553

44787

                                            manager,

554

44787

                                            BDDFunction::and_edge(

555

44787

                                                manager,

556

44787

&a,

557

44787

                                                &EdgeDropGuard::new(

558

44787

                                                    manager,

559

44787

                                                    BDDFunction::or_edge(

560

44787

                                                        manager,

561

44787

                                                        &EdgeDropGuard::new(

562

44787

                                                            manager,

563

44787

                                                            minus_edge(

564

44787

                                                                manager,

565

44787

                                                                if self.alternative_solving {

566

                                                                    self.true_bdd.as_edge(manager)

567

                                                                } else {

568

44787

                                                                    self.game.configuration().as_edge(manager)

569

},

570

44787

                                                                &tmp,

571

)?,

572

),

573

44787

                                                        A[edge_w1.to()].as_edge(manager),

574

)?,

575

),

576

)?,

577

);

578

8915

579

580

581

582

                            // 15. a \ A(v) != \emptyset

583

30553

                            if *EdgeDropGuard::new(manager, minus_edge(manager, &a, A[v].as_edge(manager))?) != *f_edge

584

585

                                // 16. A(v) := A(v) \cup a

586

6170

                                let was_empty = *A[v].as_edge(manager) == *f_edge;

587

6170

                                let update = BDDFunction::or_edge(manager, A[v].as_edge(manager), &a)?;

588

6170

                                let is_empty = update == *f_edge;

589

590

6170

                                A.set(manager, v, BDDFunction::from_edge(manager, update));

591

592

                                // 17. if v not in Q then Q.push(v)

593

6170

                                if !self.temp_vertices[*v] {

594

5810

                                    self.temp_queue.push(v);

595

5810

                                    self.temp_vertices.set(*v, true);

596

5810

597

24383

598

18867

599

600

601

602

2799

                Ok(())

603

2799

            })?;

604

605

2799

        debug_assert!(

606

2799

            !self.temp_vertices.any(),

607

            "temp_vertices should be empty after attractor computation"

608

);

609

610

2799

        Ok(A)

611

2799

612

613

    /// Returns the highest and lowest priority in the given set of vertices V.

614

1966

    fn get_highest_lowest_prio(&self, V: &Submap) -> (Priority, Priority) {

615

1966

        let mut highest = usize::MIN;

616

1966

        let mut lowest = usize::MAX;

617

618

1966

        self.manager_ref.with_manager_shared(|manager| {

619

24498

            for v in V.iter_vertices(manager) {

620

24498

                let prio = self.game.priority(v);

621

24498

                highest = highest.max(*prio);

622

24498

                lowest = lowest.min(*prio);

623

24498

624

1966

});

625

626

1966

        (Priority::new(highest), Priority::new(lowest))

627

1966

628

629

    /// Checks that the sets W0 and W1 form a  partition w.r.t the submap V, i.e., their union is V and their intersection is empty.

630

1235

    fn check_partition(&self, W0: &Submap, W1: &Submap, V: &Submap) -> Result<(), MercError> {

631

1235

        self.manager_ref

632

1235

            .with_manager_shared(|manager| -> Result<(), MercError> {

633

18938

                for v in V.iter_vertices(manager) {

634

18938

                    let tmp = W0[v].or(&W1[v])?;

635

636

                    // The union of both solutions should be the entire set of vertices.

637

18938

                    assert!(

638

18938

                        tmp == V[v],

639

                        "The union of both solutions should be the entire set of vertices, but vertex {v} is missing."

640

);

641

642

18938

                    assert!(

643

18938

                        !W0[v].and(&W1[v])?.satisfiable(),

644

                        "The intersection of both solutions should be empty, but vertex {v} has non-empty intersection."

645

);

646

647

648

1235

                Ok(())

649

1235

            })?;

650

651

1235

        Ok(())

652

1235

653

654

655

#[cfg(test)]

656

mod tests {

657

    use merc_io::DumpFiles;

658

    use merc_macros::merc_test;

659

    use merc_utilities::Timing;

660

    use oxidd::BooleanFunction;

661

    use oxidd::Manager;

662

    use oxidd::ManagerRef;

663

    use oxidd::bdd::BDDFunction;

664

    use oxidd::util::AllocResult;

665

666

    use merc_utilities::random_test;

667

668

    use crate::PG;

669

    use crate::Submap;

670

    use crate::VertexIndex;

671

    use crate::VpgSolver;

672

    use crate::project_variability_parity_games_iter;

673

    use crate::random_variability_parity_game;

674

    use crate::solve_variability_product_zielonka;

675

    use crate::solve_variability_zielonka;

676

    use crate::solve_zielonka;

677

    use crate::verify_variability_product_zielonka_solution;

678

    use crate::write_vpg;

679

680

    #[merc_test]

681

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

682

    fn test_random_variability_parity_game_solve() {

683

100

        random_test(100, |rng| {

684

100

            let mut files = DumpFiles::new("test_random_variability_parity_game_solve");

685

686

100

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

687

100

            let vpg = random_variability_parity_game(&manager_ref, rng, true, 20, 3, 3, 3).unwrap();

688

689

100

            files.dump("input.vpg", |w| write_vpg(w, &vpg)).unwrap();

690

691

100

            let solution = solve_variability_zielonka(&manager_ref, &vpg, VpgSolver::Family, false).unwrap();

692

100

            verify_variability_product_zielonka_solution(&vpg, &solution, &Timing::new()).unwrap();

693

100

})

694

695

696

    #[merc_test]

697

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

698

    fn test_random_variability_parity_game_solve_optimised_left() {

699

100

        random_test(100, |rng| {

700

100

            let mut files = DumpFiles::new("test_random_variability_parity_game_solve_optimised_left");

701

702

100

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

703

100

            let vpg = random_variability_parity_game(&manager_ref, rng, true, 20, 3, 3, 3).unwrap();

704

705

100

            files.dump("input.vpg", |w| write_vpg(w, &vpg)).unwrap();

706

707

100

            let solution =

708

100

                solve_variability_zielonka(&manager_ref, &vpg, VpgSolver::FamilyOptimisedLeft, false).unwrap();

709

100

            let solution_expected = solve_variability_zielonka(&manager_ref, &vpg, VpgSolver::Family, false).unwrap();

710

711

100

            debug_assert_eq!(solution[0], solution_expected[0]);

712

100

            debug_assert_eq!(solution[1], solution_expected[1]);

713

100

})

714

715