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::Submap;

40

use crate::VariabilityParityGame;

41

use crate::VariabilityPredecessors;

42

use crate::VertexIndex;

43

use crate::combine;

44

use crate::compute_reachable;

45

use crate::project_variability_parity_games_iter;

46

use crate::solve_zielonka;

47

use crate::x_and_not_x;

48

49

/// Variant of the Zielonka algorithm to use.

50

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

51

#[cfg_attr(feature = "clap", derive(clap::ValueEnum))]

52

pub enum ZielonkaVariant {

53

    /// Product-based Zielonka variant.

54

    Product,

55

    /// Standard family-based Zielonka algorithm.

56

    Family,

57

    /// Left-optimised family-based Zielonka variant.

58

    FamilyOptimisedLeft,

59

60

61

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

62

300

pub fn solve_variability_zielonka(

63

300

    manager_ref: &BDDManagerRef,

64

300

    game: &VariabilityParityGame,

65

300

    variant: ZielonkaVariant,

66

300

    alternative_solving: bool,

67

300

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

68

300

    debug_assert!(

69

300

        game.is_total(manager_ref)?,

70

        "Zielonka solver requires a total parity game"

71

);

72

73

300

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

74

75

    // Determine the initial set of vertices V

76

300

    let V = Submap::new(

77

300

        manager_ref,

78

300

        if alternative_solving {

79

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

80

        } else {

81

300

            game.configuration().clone()

82

},

83

300

        game.num_of_vertices(),

84

);

85

86

300

    let full_V = V.clone();

87

300

    let (W0, W1) = match variant {

88

200

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

89

100

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

90

        ZielonkaVariant::Product => {

91

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

92

93

};

94

95

300

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

96

300

    if cfg!(debug_assertions) {

97

300

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

98

99

100

300

    let (W0, W1) = if alternative_solving {

101

        // Intersect the results with the game's configuration

102

        let config = game.configuration();

103

104

            W0.and_function(manager_ref, config)?,

105

            W1.and_function(manager_ref, config)?,

106

107

    } else {

108

300

        (W0, W1)

109

};

110

111

300

    Ok([W0, W1])

112

300

113

114

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

115

100

pub fn solve_variability_product_zielonka<'a>(

116

100

    vpg: &'a VariabilityParityGame,

117

100

    timing: &'a Timing,

118

100

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

119

318

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

120

318

        match result {

121

318

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

122

318

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

123

124

318

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

125

126

318

                let (pg_solution, _) = solve_zielonka(&reachable_pg, false);

127

318

                let mut new_solution = [

128

318

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

129

318

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

130

318

];

131

6996

                for v in game.iter_vertices() {

132

6996

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

133

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

134

902

                        if pg_solution[0][proj_v] {

135

402

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

136

500

137

902

                        if pg_solution[1][proj_v] {

138

500

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

139

500

140

6094

141

142

143

318

                Ok((bits, bdd, new_solution))

144

145

            Err(result) => Err(result),

146

147

318

})

148

100

149

150

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

151

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

152

100

pub fn verify_variability_product_zielonka_solution(

153

100

    vpg: &VariabilityParityGame,

154

100

    solution: &[Submap; 2],

155

100

    timing: &Timing,

156

100

) -> Result<(), MercError> {

157

100

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

158

318

    solve_variability_product_zielonka(vpg, timing).try_for_each(|res| {

159

318

        match res {

160

318

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

161

6996

                for v in vpg.iter_vertices() {

162

6996

                    if pg_solution[0][*v] {

163

                        // Won by Even

164

402

                        assert!(

165

402

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

166

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

167

                            FormatConfig(&bits)

168

);

169

6594

170

171

6996

                    if pg_solution[1][*v] {

172

                        // Won by Odd

173

500

                        assert!(

174

500

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

175

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

176

                            FormatConfig(&bits)

177

);

178

6496

179

180

181

318

                Ok(())

182

183

            Err(res) => Err(res),

184

185

318

    })?;

186

187

100

    Ok(())

188

100

189

190

struct VariabilityZielonkaSolver<'a> {

191

    game: &'a VariabilityParityGame,

192

193

    manager_ref: &'a BDDManagerRef,

194

195

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

196

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

197

    alternative_solving: bool,

198

199

    /// Reused temporary queue for attractor computation.

200

    temp_queue: Vec<VertexIndex>,

201

202

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

203

    temp_vertices: BitVec<usize, Lsb0>,

204

205

    /// Stores the predecessors of the game.

206

    predecessors: VariabilityPredecessors,

207

208

    /// Temporary storage for vertices per priority.

209

    priority_vertices: Vec<Vec<VertexIndex>>,

210

211

    /// The BDD function representing the universe configuration.

212

    true_bdd: BDDFunction,

213

214

    /// The BDD function representing the empty configuration.

215

    false_bdd: BDDFunction,

216

217

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

218

    recursive_calls: usize,

219

220

221

impl<'a> VariabilityZielonkaSolver<'a> {

222

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

223

300

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

224

        // Keep track of the vertices for each priority

225

300

        let mut priority_vertices = Vec::new();

226

227

6600

        for v in game.iter_vertices() {

228

6600

            let prio = game.priority(v);

229

230

7500

            while prio >= priority_vertices.len() {

231

900

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

232

900

233

234

6600

            priority_vertices[prio].push(v);

235

236

237

300

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

238

300

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

239

240

300

        Self {

241

300

            game,

242

300

            manager_ref,

243

300

            temp_queue: Vec::new(),

244

300

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

245

300

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

246

300

            priority_vertices,

247

300

            recursive_calls: 0,

248

300

            alternative_solving,

249

300

            true_bdd,

250

300

            false_bdd,

251

300

252

300

253

254

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

255

1894

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

256

1894

        self.recursive_calls += 1;

257

258

        // For debugging mostly

259

1894

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

260

1894

        let gamma_copy = gamma.clone();

261

262

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

263

1894

        if gamma.is_empty() {

264

706

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

265

1188

266

267

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

268

1188

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

269

270

        // 6. x := m mod 2

271

1188

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

272

1188

        let not_x = x.opponent();

273

274

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

275

1188

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

276

277

1188

        self.manager_ref

278

1188

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

279

8956

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

280

8956

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

281

8956

282

283

1188

                Ok(())

284

1188

            })?;

285

286

1188

        debug!(

287

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

288

            gamma.number_of_non_empty(),

289

            highest_prio,

290

            lowest_prio,

291

x,

292

            mu.number_of_non_empty()

293

);

294

295

1188

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

296

1188

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

297

1188

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

298

1188

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

299

300

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

301

1188

        debug!(

302

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

303

            alpha.number_of_non_empty()

304

);

305

1188

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

306

307

1188

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

308

1188

        if omega1_not_x.is_empty() {

309

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

310

682

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

311

            // 20. return (omega_0, omega_1)

312

682

            Ok(combine(omega1_x, omega1_not_x, x))

313

        } else {

314

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

315

506

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

316

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

317

506

            debug!(

318

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

319

                beta.number_of_non_empty()

320

);

321

506

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

322

323

506

            let (mut omega2_0, mut omega2_1) =

324

506

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

325

326

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

327

506

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

328

506

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

329

330

            // 20. return (omega_0, omega_1)

331

506

            if cfg!(debug_assertions) {

332

506

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

333

334

506

            Ok(combine(omega2_x, omega2_not_x, x))

335

336

1894

337

338

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

339

879

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

340

879

        self.recursive_calls += 1;

341

879

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

342

879

        let gamma_copy = gamma.clone();

343

344

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

345

879

        if gamma.is_empty() {

346

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

347

333

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

348

546

349

350

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

351

546

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

352

353

        // 6. x := m mod 2

354

546

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

355

546

        let not_x = x.opponent();

356

357

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

358

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

359

546

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

360

361

546

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

362

363

546

        self.manager_ref

364

546

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

365

4101

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

366

4101

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

367

4101

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

368

369

370

546

                Ok(())

371

546

            })?;

372

373

546

        debug!(

374

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

375

            gamma.number_of_non_empty(),

376

            highest_prio,

377

            lowest_prio,

378

x,

379

            mu.number_of_non_empty()

380

);

381

382

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

383

546

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

384

546

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

385

546

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

386

546

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

387

388

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

389

546

        debug!(

390

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

391

            alpha.number_of_non_empty()

392

);

393

546

        let (omega1_0, omega1_1) =

394

546

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

395

396

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

397

546

        let C_restricted = minus(

398

546

            &if !self.alternative_solving {

399

546

                self.true_bdd.clone()

400

            } else {

401

                self.game.configuration().clone()

402

},

403

546

&C,

404

)?;

405

406

546

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

407

546

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

408

409

        // 10.

410

546

        if omega1_not_x_restricted.is_empty() {

411

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

412

313

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

413

313

            if cfg!(debug_assertions) {

414

313

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

415

416

417

            // 22. return (omega_0, omega_1)

418

313

            Ok(combine(omega1_x, omega1_not_x, x))

419

        } else {

420

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

421

233

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

422

5126

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

423

5126

                C1 = C1.or(func)?;

424

425

233

            C1 = C1.and(&C)?;

426

427

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

428

233

            let C1_restricted = minus(

429

233

                &if self.alternative_solving {

430

                    self.true_bdd.clone()

431

                } else {

432

233

                    self.game.configuration().clone()

433

},

434

233

                &C1,

435

)?;

436

437

233

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

438

233

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

439

233

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

440

233

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

441

442

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

443

233

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

444

445

233

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

446

233

            let (omega2_0, omega2_1) =

447

233

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

448

449

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

450

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

451

233

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

452

233

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

453

233

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

454

455

233

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

456

233

            let omega2_x_result = omega2_x.or(

457

233

                self.manager_ref,

458

233

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

459

)?;

460

233

            let omega2_not_x_result = omega2_not_x

461

233

                .or(self.manager_ref, &omega1_not_x_restricted)?

462

233

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

463

464

233

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

465

233

            Ok(combine(omega2_x_result, omega2_not_x_result, x))

466

467

879

468

469

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

470

///

471

    /// # Details

472

///

473

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

474

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

475

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

476

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

477

///

478

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

479

2473

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

480

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

481

2473

        debug_assert!(

482

2473

            self.temp_queue.is_empty(),

483

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

484

);

485

486

2473

        self.manager_ref.with_manager_shared(|manager| {

487

16120

            for v in A.iter_vertices(manager) {

488

16120

                self.temp_queue.push(v);

489

16120

490

16120

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

491

16120

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

492

16120

493

2473

});

494

495

        // 4. While Q not empty do

496

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

497

2473

        self.manager_ref

498

2473

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

499

                // Used for satisfiability checks

500

2473

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

501

502

23473

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

503

21000

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

504

505

                    // For every v \in Ew do

506

43462

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

507

43462

                        let mut a = EdgeDropGuard::new(

508

43462

                            manager,

509

43462

                            BDDFunction::and_edge(

510

43462

                                manager,

511

43462

                                &EdgeDropGuard::new(

512

43462

                                    manager,

513

43462

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

514

),

515

43462

                                edge_guard.as_edge(manager),

516

)?,

517

);

518

519

43462

                        if *a != *f_edge {

520

                            // 7. if v in V_\alpha

521

27668

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

522

5635

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

523

5635

                                // This assignment has already been computed above.

524

5635

                            } else {

525

                                // 10. a := gamma(v)

526

22033

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

527

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

528

49287

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

529

49287

                                    let tmp = EdgeDropGuard::new(

530

49287

                                        manager,

531

49287

                                        BDDFunction::and_edge(

532

49287

                                            manager,

533

49287

                                            &EdgeDropGuard::new(

534

49287

                                                manager,

535

49287

                                                BDDFunction::and_edge(

536

49287

                                                    manager,

537

49287

                                                    gamma[v].as_edge(manager),

538

49287

                                                    edge_w1.label().as_edge(manager),

539

)?,

540

),

541

49287

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

542

)?,

543

);

544

545

49287

                                    if *tmp != *f_edge {

546

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

547

41231

                                        let tmp = EdgeDropGuard::new(

548

41231

                                            manager,

549

41231

                                            BDDFunction::and_edge(

550

41231

                                                manager,

551

41231

                                                edge_w1.label().as_edge(manager),

552

41231

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

553

)?,

554

);

555

556

41231

                                        a = EdgeDropGuard::new(

557

41231

                                            manager,

558

41231

                                            BDDFunction::and_edge(

559

41231

                                                manager,

560

41231

&a,

561

41231

                                                &EdgeDropGuard::new(

562

41231

                                                    manager,

563

41231

                                                    BDDFunction::or_edge(

564

41231

                                                        manager,

565

41231

                                                        &EdgeDropGuard::new(

566

41231

                                                            manager,

567

41231

                                                            minus_edge(

568

41231

                                                                manager,

569

41231

                                                                if self.alternative_solving {

570

                                                                    self.true_bdd.as_edge(manager)

571

                                                                } else {

572

41231

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

573

},

574

41231

                                                                &tmp,

575

)?,

576

),

577

41231

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

578

)?,

579

),

580

)?,

581

);

582

8056

583

584

585

586

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

587

27668

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

588

589

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

590

5284

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

591

5284

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

592

5284

                                let is_empty = update == *f_edge;

593

594

5284

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

595

596

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

597

5284

                                if !self.temp_vertices[*v] {

598

4880

                                    self.temp_queue.push(v);

599

4880

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

600

4880

601

22384

602

15794

603

604

605

606

2473

                Ok(())

607

2473

            })?;

608

609

2473

        debug_assert!(

610

2473

            !self.temp_vertices.any(),

611

            "temp_vertices should be empty after attractor computation"

612

);

613

614

2473

        Ok(A)

615

2473

616

617

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

618

1734

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

619

1734

        let mut highest = usize::MIN;

620

1734

        let mut lowest = usize::MAX;

621

622

1734

        self.manager_ref.with_manager_shared(|manager| {

623

21881

            for v in V.iter_vertices(manager) {

624

21881

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

625

21881

                highest = highest.max(*prio);

626

21881

                lowest = lowest.min(*prio);

627

21881

628

1734

});

629

630

1734

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

631

1734

632

633

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

634

1119

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

635

1119

        self.manager_ref

636

1119

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

637

16939

                for v in V.iter_vertices(manager) {

638

16939

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

639

640

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

641

16939

                    assert!(

642

16939

                        tmp == V[v],

643

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

644

);

645

646

16939

                    assert!(

647

16939

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

648

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

649

);

650

651

652

1119

                Ok(())

653

1119

            })?;

654

655

1119

        Ok(())

656

1119

657

658

659

#[cfg(test)]

660

mod tests {

661

    use merc_io::DumpFiles;

662

    use merc_macros::merc_test;

663

    use merc_utilities::Timing;

664

    use oxidd::BooleanFunction;

665

    use oxidd::Manager;

666

    use oxidd::ManagerRef;

667

    use oxidd::bdd::BDDFunction;

668

    use oxidd::util::AllocResult;

669

670

    use merc_utilities::random_test;

671

672

    use crate::PG;

673

    use crate::Submap;

674

    use crate::VertexIndex;

675

    use crate::ZielonkaVariant;

676

    use crate::project_variability_parity_games_iter;

677

    use crate::random_variability_parity_game;

678

    use crate::solve_variability_product_zielonka;

679

    use crate::solve_variability_zielonka;

680

    use crate::solve_zielonka;

681

    use crate::verify_variability_product_zielonka_solution;

682

    use crate::write_vpg;

683

684

    #[merc_test]

685

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

686

    fn test_random_variability_parity_game_solve() {

687

100

        random_test(100, |rng| {

688

100

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

689

690

100

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

691

100

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

692

693

100

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

694

695

100

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

696

100

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

697

100

})

698

699

700

    #[merc_test]

701

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

702

    fn test_random_variability_parity_game_solve_optimised_left() {

703

100

        random_test(100, |rng| {

704

100

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

705

706

100

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

707

100

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

708

709

100

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

710

711

100

            let solution =

712

100

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

713

100

            let solution_expected =

714

100

                solve_variability_zielonka(&manager_ref, &vpg, ZielonkaVariant::Family, false).unwrap();

715

716

100

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

717

100

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

718

100

})

719

720