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

5

use bitvec::bitvec;

6

use bitvec::order::Lsb0;

7

use bitvec::vec::BitVec;

8

use log::debug;

9

use log::info;

10

use log::trace;

11

use merc_symbolic::FormatConfig;

12

use oxidd::BooleanFunction;

13

use oxidd::Function;

14

use oxidd::ManagerRef;

15

use oxidd::bdd::BDDFunction;

16

use oxidd::bdd::BDDManagerRef;

17

use oxidd::util::OptBool;

18

use oxidd_core::util::EdgeDropGuard;

19

20

use merc_symbolic::FormatConfigSet;

21

use merc_symbolic::minus;

22

use merc_symbolic::minus_edge;

23

use merc_utilities::MercError;

24

use merc_utilities::Timing;

25

26

use crate::PG;

27

use crate::Player;

28

use crate::Priority;

29

use crate::Projected;

30

use crate::Repeat;

31

use crate::Set;

32

use crate::Solver;

33

use crate::Submap;

34

use crate::VariabilityParityGame;

35

use crate::VariabilityPredecessors;

36

use crate::VertexIndex;

37

use crate::VpgSolver;

38

use crate::combine;

39

use crate::compute_reachable;

40

use crate::project_variability_parity_games_iter;

41

use crate::solve_priority_promotion;

42

use crate::solve_zielonka;

43

use crate::x_and_not_x;

44

45

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

46

300

pub fn solve_variability_zielonka(

47

300

    manager_ref: &BDDManagerRef,

48

300

    game: &VariabilityParityGame,

49

300

    variant: VpgSolver,

50

300

    alternative_solving: bool,

51

300

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

52

300

    debug_assert!(

53

300

        game.is_vpg_total(manager_ref)?,

54

        "Zielonka solver requires a total parity game"

55

);

56

57

300

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

58

59

    // Determine the initial set of vertices V

60

300

    let V = Submap::new(

61

300

        manager_ref,

62

300

        if alternative_solving {

63

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

64

        } else {

65

300

            game.configuration().clone()

66

},

67

300

        game.num_of_vertices(),

68

);

69

70

300

    let full_V = V.clone();

71

300

    let (W0, W1) = match variant {

72

200

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

73

100

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

74

        VpgSolver::Product => {

75

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

76

77

};

78

79

300

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

80

300

    if cfg!(debug_assertions) {

81

300

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

82

83

84

300

    let (W0, W1) = if alternative_solving {

85

        // Intersect the results with the game's configuration

86

        let config = game.configuration();

87

88

            W0.and_function(manager_ref, config)?,

89

            W1.and_function(manager_ref, config)?,

90

91

    } else {

92

300

        (W0, W1)

93

};

94

95

300

    Ok([W0, W1])

96

300

97

98

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

99

100

pub fn solve_variability_product_zielonka<'a>(

100

    vpg: &'a VariabilityParityGame,

101

100

    solver: Solver,

102

100

    timing: &'a Timing,

103

100

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

104

332

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

105

332

        match result {

106

332

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

107

332

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

108

109

332

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

110

111

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

112

332

                let (pg_solution, _) = match solver {

113

332

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

114

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

115

};

116

332

                let mut new_solution = [

117

332

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

118

332

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

119

332

];

120

7304

                for v in game.iter_vertices() {

121

7304

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

122

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

123

946

                        if pg_solution[0][proj_v] {

124

480

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

125

480

126

946

                        if pg_solution[1][proj_v] {

127

466

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

128

480

129

6358

130

131

132

332

                Ok((bits, bdd, new_solution))

133

134

            Err(result) => Err(result),

135

136

332

})

137

100

138

139

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

140

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

141

100

pub fn verify_variability_product_zielonka_solution(

142

100

    vpg: &VariabilityParityGame,

143

100

    solution: &[Submap; 2],

144

100

    timing: &Timing,

145

100

) -> Result<(), MercError> {

146

100

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

147

332

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

148

332

        match res {

149

332

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

150

7304

                for v in vpg.iter_vertices() {

151

7304

                    if pg_solution[0][*v] {

152

                        // Won by Even

153

480

                        assert!(

154

480

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

155

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

156

                            FormatConfig(&bits)

157

);

158

6824

159

160

7304

                    if pg_solution[1][*v] {

161

                        // Won by Odd

162

466

                        assert!(

163

466

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

164

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

165

                            FormatConfig(&bits)

166

);

167

6838

168

169

170

332

                Ok(())

171

172

            Err(res) => Err(res),

173

174

332

    })?;

175

176

100

    Ok(())

177

100

178

179

struct VariabilityZielonkaSolver<'a> {

180

    game: &'a VariabilityParityGame,

181

182

    manager_ref: &'a BDDManagerRef,

183

184

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

185

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

186

    alternative_solving: bool,

187

188

    /// Reused temporary queue for attractor computation.

189

    temp_queue: Vec<VertexIndex>,

190

191

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

192

    temp_vertices: BitVec<usize, Lsb0>,

193

194

    /// Stores the predecessors of the game.

195

    predecessors: VariabilityPredecessors,

196

197

    /// Temporary storage for vertices per priority.

198

    priority_vertices: Vec<Vec<VertexIndex>>,

199

200

    /// The BDD function representing the universe configuration.

201

    true_bdd: BDDFunction,

202

203

    /// The BDD function representing the empty configuration.

204

    false_bdd: BDDFunction,

205

206

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

207

    recursive_calls: usize,

208

209

210

impl<'a> VariabilityZielonkaSolver<'a> {

211

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

212

300

    pub(crate) fn new(

213

300

        manager_ref: &'a BDDManagerRef,

214

300

        game: &'a VariabilityParityGame,

215

300

        alternative_solving: bool,

216

300

    ) -> Self {

217

        // Keep track of the vertices for each priority

218

300

        let mut priority_vertices = Vec::new();

219

220

6600

        for v in game.iter_vertices() {

221

6600

            let prio = game.priority(v);

222

223

7498

            while prio >= priority_vertices.len() {

224

898

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

225

898

226

227

6600

            priority_vertices[prio].push(v);

228

229

230

300

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

231

300

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

232

233

300

        Self {

234

300

            game,

235

300

            manager_ref,

236

300

            temp_queue: Vec::new(),

237

300

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

238

300

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

239

300

            priority_vertices,

240

300

            recursive_calls: 0,

241

300

            alternative_solving,

242

300

            true_bdd,

243

300

            false_bdd,

244

300

245

300

246

247

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

248

2032

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

249

2032

        self.recursive_calls += 1;

250

251

        // For debugging mostly

252

2032

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

253

254

        #[cfg(debug_assertions)]

255

2032

        let gamma_copy = gamma.clone();

256

257

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

258

2032

        if gamma.is_all_empty_set() {

259

746

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

260

1286

261

262

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

263

1286

        let highest_prio = self.get_highest_prio(&gamma);

264

265

        // 6. x := m mod 2

266

1286

        let x = Player::from_priority(highest_prio);

267

1286

        let not_x = x.opponent();

268

269

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

270

1286

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

271

272

1286

        self.manager_ref

273

1286

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

274

9694

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

275

9694

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

276

9694

277

278

1286

                Ok(())

279

1286

            })?;

280

281

1286

        debug!(

282

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

283

            gamma.number_of_non_empty(),

284

            highest_prio,

285

            self.get_lowest_prio(&gamma),

286

x,

287

            mu.number_of_non_empty()

288

);

289

290

1286

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

291

1286

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

292

1286

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

293

1286

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

294

295

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

296

1286

        debug!(

297

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

298

            alpha.number_of_non_empty()

299

);

300

1286

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

301

302

1286

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

303

1286

        if omega1_not_x.is_all_empty_set() {

304

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

305

740

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

306

            // 20. return (omega_0, omega_1)

307

740

            Ok(combine(omega1_x, omega1_not_x, x))

308

        } else {

309

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

310

546

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

311

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

312

546

            debug!(

313

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

314

                beta.number_of_non_empty()

315

);

316

546

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

317

318

546

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

319

320

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

321

546

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

322

546

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

323

324

            // 20. return (omega_0, omega_1)

325

            #[cfg(debug_assertions)]

326

546

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

327

546

            Ok(combine(omega2_x, omega2_not_x, x))

328

329

2032

330

331

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

332

1009

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

333

1009

        self.recursive_calls += 1;

334

1009

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

335

        #[cfg(debug_assertions)]

336

1009

        let gamma_copy = gamma.clone();

337

338

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

339

1009

        if gamma.is_all_empty_set() {

340

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

341

371

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

342

638

343

344

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

345

638

        let highest_prio = self.get_highest_prio(&gamma);

346

347

        // 6. x := m mod 2

348

638

        let x = Player::from_priority(highest_prio);

349

638

        let not_x = x.opponent();

350

351

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

352

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

353

638

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

354

355

638

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

356

357

638

        self.manager_ref

358

638

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

359

4808

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

360

4808

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

361

4808

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

362

363

364

638

                Ok(())

365

638

            })?;

366

367

638

        debug!(

368

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

369

            gamma.number_of_non_empty(),

370

            highest_prio,

371

            self.get_lowest_prio(&gamma),

372

x,

373

            mu.number_of_non_empty()

374

);

375

376

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

377

638

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

378

638

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

379

638

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

380

638

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

381

382

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

383

638

        debug!(

384

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

385

            alpha.number_of_non_empty()

386

);

387

638

        let (omega1_0, omega1_1) =

388

638

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

389

390

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

391

638

        let C_restricted = minus(

392

638

            &if !self.alternative_solving {

393

638

                self.true_bdd.clone()

394

            } else {

395

                self.game.configuration().clone()

396

},

397

638

&C,

398

)?;

399

400

638

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

401

638

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

402

403

        // 10.

404

638

        if omega1_not_x_restricted.is_all_empty_set() {

405

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

406

367

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

407

            #[cfg(debug_assertions)]

408

367

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

409

410

            // 22. return (omega_0, omega_1)

411

367

            Ok(combine(omega1_x, omega1_not_x, x))

412

        } else {

413

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

414

271

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

415

5962

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

416

5962

                C1 = C1.or(func)?;

417

418

271

            C1 = C1.and(&C)?;

419

420

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

421

271

            let C1_restricted = minus(

422

271

                &if self.alternative_solving {

423

                    self.true_bdd.clone()

424

                } else {

425

271

                    self.game.configuration().clone()

426

},

427

271

                &C1,

428

)?;

429

430

271

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

431

271

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

432

271

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

433

271

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

434

435

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

436

271

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

437

438

271

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

439

271

            let (omega2_0, omega2_1) =

440

271

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

441

442

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

443

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

444

271

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

445

271

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

446

271

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

447

448

271

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

449

271

            let omega2_x_result = omega2_x.or(

450

271

                self.manager_ref,

451

271

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

452

)?;

453

271

            let omega2_not_x_result = omega2_not_x

454

271

                .or(self.manager_ref, &omega1_not_x_restricted)?

455

271

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

456

457

271

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

458

271

            Ok(combine(omega2_x_result, omega2_not_x_result, x))

459

460

1009

461

462

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

463

///

464

    /// # Details

465

///

466

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

467

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

468

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

469

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

470

///

471

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

472

2741

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

473

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

474

2741

        debug_assert!(

475

2741

            self.temp_queue.is_empty(),

476

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

477

);

478

479

2741

        self.manager_ref.with_manager_shared(|manager| {

480

17691

            for v in A.iter_vertices(manager) {

481

17691

                self.temp_queue.push(v);

482

17691

483

17691

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

484

17691

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

485

17691

486

2741

});

487

488

        // 4. While Q not empty do

489

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

490

2741

        self.manager_ref

491

2741

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

492

                // Used for satisfiability checks

493

2741

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

494

495

25879

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

496

23138

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

497

498

                    // For every v \in Ew do

499

48215

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

500

48215

                        let mut a = EdgeDropGuard::new(

501

48215

                            manager,

502

48215

                            BDDFunction::and_edge(

503

48215

                                manager,

504

48215

                                &EdgeDropGuard::new(

505

48215

                                    manager,

506

48215

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

507

),

508

48215

                                edge_guard.as_edge(manager),

509

)?,

510

);

511

512

48215

                        if *a != *f_edge {

513

                            // 7. if v in V_\alpha

514

29931

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

515

6104

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

516

6104

                                // This assignment has already been computed above.

517

6104

                            } else {

518

                                // 10. a := gamma(v)

519

23827

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

520

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

521

52610

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

522

52610

                                    let tmp = EdgeDropGuard::new(

523

52610

                                        manager,

524

52610

                                        BDDFunction::and_edge(

525

52610

                                            manager,

526

52610

                                            &EdgeDropGuard::new(

527

52610

                                                manager,

528

52610

                                                BDDFunction::and_edge(

529

52610

                                                    manager,

530

52610

                                                    gamma[v].as_edge(manager),

531

52610

                                                    edge_w1.label().as_edge(manager),

532

)?,

533

),

534

52610

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

535

)?,

536

);

537

538

52610

                                    if *tmp != *f_edge {

539

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

540

44031

                                        let tmp = EdgeDropGuard::new(

541

44031

                                            manager,

542

44031

                                            BDDFunction::and_edge(

543

44031

                                                manager,

544

44031

                                                edge_w1.label().as_edge(manager),

545

44031

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

546

)?,

547

);

548

549

44031

                                        a = EdgeDropGuard::new(

550

44031

                                            manager,

551

44031

                                            BDDFunction::and_edge(

552

44031

                                                manager,

553

44031

&a,

554

44031

                                                &EdgeDropGuard::new(

555

44031

                                                    manager,

556

44031

                                                    BDDFunction::or_edge(

557

44031

                                                        manager,

558

44031

                                                        &EdgeDropGuard::new(

559

44031

                                                            manager,

560

44031

                                                            minus_edge(

561

44031

                                                                manager,

562

44031

                                                                if self.alternative_solving {

563

                                                                    self.true_bdd.as_edge(manager)

564

                                                                } else {

565

44031

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

566

},

567

44031

                                                                &tmp,

568

)?,

569

),

570

44031

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

571

)?,

572

),

573

)?,

574

);

575

8579

576

577

578

579

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

580

29931

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

581

582

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

583

5795

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

584

5795

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

585

586

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

587

5795

                                if !self.temp_vertices[*v] {

588

5447

                                    self.temp_queue.push(v);

589

5447

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

590

5447

591

24136

592

18284

593

594

595

596

2741

                Ok(())

597

2741

            })?;

598

599

2741

        debug_assert!(

600

2741

            !self.temp_vertices.any(),

601

            "temp_vertices should be empty after attractor computation"

602

);

603

604

2741

        Ok(A)

605

2741

606

607

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

608

1924

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

609

1924

        let mut highest = usize::MIN;

610

1924

        self.manager_ref.with_manager_shared(|manager| {

611

24151

            for v in V.iter_vertices(manager) {

612

24151

                highest = highest.max(*self.game.priority(v));

613

24151

614

1924

});

615

1924

        Priority::new(highest)

616

1924

617

618

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

619

///

620

    /// Only used for debug logging, so it is kept out of the hot path.

621

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

622

        let mut lowest = usize::MAX;

623

        self.manager_ref.with_manager_shared(|manager| {

624

            for v in V.iter_vertices(manager) {

625

                lowest = lowest.min(*self.game.priority(v));

626

627

});

628

        Priority::new(lowest)

629

630

631

    /// 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.

632

1213

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

633

1213

        self.manager_ref

634

1213

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

635

18722

                for v in V.iter_vertices(manager) {

636

18722

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

637

638

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

639

18722

                    assert!(

640

18722

                        tmp == V[v],

641

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

642

);

643

644

18722

                    assert!(

645

18722

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

646

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

647

);

648

649

650

1213

                Ok(())

651

1213

            })?;

652

653

1213

        Ok(())

654

1213

655

656

657

#[cfg(test)]

658

mod tests {

659

    use merc_io::DumpFiles;

660

    use merc_macros::merc_test;

661

    use merc_utilities::Timing;

662

663

    use merc_utilities::random_test;

664

665

    use crate::VpgSolver;

666

667

    use crate::random_variability_parity_game;

668

669

    use crate::solve_variability_zielonka;

670

671

    use crate::verify_variability_product_zielonka_solution;

672

    use crate::write_vpg;

673

674

    #[merc_test]

675

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

676

    fn test_random_variability_parity_game_solve() {

677

100

        random_test(100, |rng| {

678

100

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

679

680

100

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

681

100

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

682

683

100

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

684

685

100

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

686

100

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

687

100

})

688

689

690

    #[merc_test]

691

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

692

    fn test_random_variability_parity_game_solve_optimised_left() {

693

100

        random_test(100, |rng| {

694

100

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

695

696

100

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

697

100

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

698

699

100

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

700

701

100

            let solution =

702

100

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

703

100

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

704

705

100

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

706

100

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

707

100

})

708

709