Grcov report - zielonka.rs

1

#![allow(nonstandard_style)]

2

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

3

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

4

//!

5

//! Implements the standard Zielonka recursive solver for any parity game

6

//! implementing the [`crate::PG`] trait.

7

8

use core::fmt;

9

use std::ops::BitAnd;

10

11

use bitvec::bitvec;

12

use bitvec::order::Lsb0;

13

use bitvec::vec::BitVec;

14

use itertools::Itertools;

15

use log::debug;

16

use log::trace;

17

18

use crate::PG;

19

use crate::Player;

20

use crate::Pred;

21

use crate::Predecessors;

22

use crate::Priority;

23

use crate::Repeat;

24

use crate::Strat;

25

use crate::Strategy;

26

use crate::VertexIndex;

27

28

/// The type for a set of vertices.

29

pub type Set = BitVec<usize, Lsb0>;

30

31

/// Solves the given parity game using the Zielonka algorithm.

32

///

33

/// If `compute_strategy` is true, also computes the winning strategy for both

34

/// players. Otherwise, returns `None` strategies.

35

2992

pub fn solve_zielonka<G: PG>(game: &G, compute_strategy: bool) -> ([Set; 2], Option<[Strategy; 2]>) {

36

2992

    if compute_strategy {

37

100

        let (solution, strategy) = solve_zielonka_impl::<G, Strategy>(game);

38

100

        (solution, Some(strategy))

39

    } else {

40

2892

        let (solution, _) = solve_zielonka_impl::<G, ()>(game);

41

2892

        (solution, None)

42

43

2992

44

45

/// Solves the given parity game using the Zielonka algorithm, computing a

46

/// strategy representation of type `S`.

47

2992

fn solve_zielonka_impl<G: PG, S: Strat>(game: &G) -> ([Set; 2], [S; 2]) {

48

2992

    debug_assert!(game.is_total(), "Zielonka solver requires a total parity game");

49

50

    // Initial set of vertices V = all vertices

51

2992

    let mut V = bitvec![usize, Lsb0; 0; game.num_of_vertices()];

52

2992

    V.set_elements(usize::MAX);

53

2992

    let full_V = V.clone(); // Used for debugging.

54

55

2992

    let mut zielonka = ZielonkaSolver::<_, S>::new(game);

56

57

2992

    let (W0, S0, W1, S1) = zielonka.zielonka_rec(V, 0);

58

59

    // Check that the result is a valid partition

60

2992

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

61

2992

    if cfg!(debug_assertions) {

62

2992

        check_partition(&W0, &W1, &full_V);

63

2992

64

65

2992

    ([W0, W1], [S0, S1])

66

2992

67

68

struct ZielonkaSolver<'a, G: PG, S: Strat> {

69

    game: &'a G,

70

71

    /// Reused temporary queue for attractor computation.

72

    temp_queue: Vec<VertexIndex>,

73

74

    /// Reused per-vertex counter, used during attractor computation to count the

75

    /// number of successors of an opponent vertex that are still within the

76

    /// subgame but not yet in the attractor set.

77

    attractor_counters: Vec<usize>,

78

79

    /// Stores the predecessors of the game.

80

    predecessors: Predecessors<'a>,

81

82

    /// Temporary storage for vertices per priority.

83

    priority_vertices: Vec<Vec<VertexIndex>>,

84

85

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

86

    recursive_calls: usize,

87

88

    /// The `S` is not actually stored in the struct, but we need to keep track of the type for the recursive calls.

89

    _strategy: std::marker::PhantomData<S>,

90

91

92

impl<G: PG, S: Strat> ZielonkaSolver<'_, G, S> {

93

    /// Creates a new Zielonka solver for the given parity game.

94

2992

    fn new<'a>(game: &'a G) -> ZielonkaSolver<'a, G, S> {

95

        // Keep track of the vertices for each priority

96

2992

        let mut priority_vertices = Vec::new();

97

98

82014

        for v in game.iter_vertices() {

99

82014

            let prio = game.priority(v);

100

101

88646

            while prio >= priority_vertices.len() {

102

6632

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

103

6632

104

105

82014

            priority_vertices[prio].push(v);

106

107

108

2992

        ZielonkaSolver {

109

2992

            game,

110

2992

            predecessors: Predecessors::new(game),

111

2992

            priority_vertices,

112

2992

            temp_queue: Vec::new(),

113

2992

            attractor_counters: vec![0; game.num_of_vertices()],

114

2992

            recursive_calls: 0,

115

2992

            _strategy: std::marker::PhantomData,

116

2992

117

2992

118

119

    /// Recursively solves the parity game for the given set of vertices V.

120

///

121

    /// # Details

122

///

123

    /// The strategy computation is taken from the following paper:

124

///

125

    /// >  Oliver Friedmann. Recursive algorithm for parity games requires exponential time. RAIRO Theor. Informatics Appl. 45(4): 449-457 (2011) [DOI](https://doi.org/10.1051/ita/2011124).

126

15669

    fn zielonka_rec(&mut self, V: Set, depth: usize) -> (Set, S, Set, S) {

127

15669

        self.recursive_calls += 1;

128

        #[cfg(debug_assertions)]

129

15669

        let full_V = V.clone(); // Used for debugging

130

15669

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

131

132

15669

        if !V.any() {

133

6270

            return (V.clone(), S::new(), V.clone(), S::new());

134

9399

135

136

9399

        let highest_prio = self.get_highest_prio(&V);

137

9399

        let alpha = Player::from_priority(highest_prio);

138

9399

        let not_alpha = alpha.opponent();

139

140

        // Collect the set U of vertices with the highest priority in V

141

9399

        let mut U = bitvec![usize, Lsb0; 0; self.game.num_of_vertices()];

142

140609

        for &v in self.priority_vertices[highest_prio].iter() {

143

140609

            if V[*v] {

144

82237

                U.set(*v, true);

145

82237

146

147

148

9399

        debug!(

149

            "{}|V| = {}, highest prio = {}, lowest prio = {}, player = {}, |U| = {}",

150

            indent,

151

            V.count_ones(),

152

            highest_prio,

153

            self.get_lowest_prio(&V),

154

            alpha,

155

            U.count_ones()

156

);

157

9399

        trace!("{}Vertices in U: {}", indent, DisplaySet(&U));

158

159

9399

        let U_clone = U.clone();

160

161

9399

        let (A, A_strategy) = self.attractor(alpha, &V, U);

162

163

9399

        trace!("{}Vertices in A: {}", indent, DisplaySet(&A));

164

9399

        debug!("{}zielonka(V \\ A) |A| = {}", indent, A.count_ones());

165

9399

        let (W1_0, S1_0, W1_1, S1_1) = self.zielonka_rec(V.clone().bitand(!A.clone()), depth + 1);

166

167

9399

        let (mut W1_alpha, mut S1_alpha, W1_not_alpha, S1_not_alpha) =

168

9399

            x_and_not_x_strategy(W1_0, S1_0, W1_1, S1_1, alpha);

169

170

9399

        if !W1_not_alpha.any() {

171

6121

            W1_alpha |= A;

172

            // Combine the strategy from the attractor with the recursive strategy.

173

6121

            S1_alpha = S1_alpha

174

6121

                .union(A_strategy)

175

6121

                .extend_arbitrary(self.game, &U_clone, &V, alpha);

176

6121

            combine_with_strategy(W1_alpha, S1_alpha, W1_not_alpha, S::new(), alpha)

177

        } else {

178

3278

            let (B, B_strategy) = self.attractor(not_alpha, &V, W1_not_alpha);

179

180

3278

            trace!("{}Vertices in B: {}", indent, DisplaySet(&B));

181

3278

            debug!("{}zielonka(V \\ B)", indent);

182

3278

            let (W2_0, S2_0, W2_1, S2_1) = self.zielonka_rec(V.bitand(!B.clone()), depth + 1);

183

184

3278

            let (W2_alpha, S2_alpha, mut W2_not_alpha, mut S2_not_alpha) =

185

3278

                x_and_not_x_strategy(W2_0, S2_0, W2_1, S2_1, alpha);

186

187

3278

            W2_not_alpha |= B;

188

            // Combine the strategy from the attractor with the recursive strategy

189

3278

            S2_not_alpha = S2_not_alpha.union(B_strategy).union(S1_not_alpha);

190

191

            #[cfg(debug_assertions)]

192

3278

            check_partition(&W2_alpha, &W2_not_alpha, &full_V);

193

3278

            combine_with_strategy(W2_alpha, S2_alpha, W2_not_alpha, S2_not_alpha, alpha)

194

195

15669

196

197

    /// Computes the attractor for `alpha` to the set `U` within the vertices `V`.

198

///

199

    /// # Details

200

///

201

    /// Instead of rescanning the outgoing edges of an opponent vertex every time

202

    /// one of its successors is added to the attractor, a per-vertex counter of

203

    /// the successors still outside the attractor is maintained. The opponent

204

    /// vertex is attracted once that counter reaches zero, giving an overall

205

    /// linear-time attractor.

206

12677

    fn attractor(&mut self, alpha: Player, V: &Set, mut A: Set) -> (Set, S) {

207

        // 1. strategy := empty

208

12677

        let mut strategy = S::new();

209

210

        // Initialise the counter of every opponent vertex in V.

211

326818

        for v in V.iter_ones().map(VertexIndex::new) {

212

326818

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

213

210168

                self.attractor_counters[*v] = self.game.outgoing_edges(v).filter(|edge| V[*edge.to()]).count();

214

154189

215

216

217

        // 2. Q = {v \in A}

218

12677

        self.temp_queue.clear();

219

129097

        for v in A.iter_ones() {

220

129097

            self.temp_queue.push(VertexIndex::new(v));

221

129097

222

223

        // 4. While Q is not empty do

224

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

225

213491

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

226

            // For every u \in Ew do

227

270749

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

228

270749

                if !V[*v] || A[*v] {

229

179315

                    continue;

230

91434

231

232

91434

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

233

                    // v \in V_\alpha can move to w \in A, so it is attracted.

234

39388

                    true

235

                } else {

236

                    // One more successor of v (namely w) entered the attractor;

237

                    // v is attracted once all of its successors within V did.

238

52046

                    self.attractor_counters[*v] -= 1;

239

52046

                    self.attractor_counters[*v] == 0

240

};

241

242

91434

                if attracted {

243

71717

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

244

39388

                        strategy.set(v, w);

245

40540

246

247

71717

                    A.set(*v, true);

248

71717

                    self.temp_queue.push(v);

249

19717

250

251

252

253

12677

        (A, strategy)

254

12677

255

256

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

257

9399

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

258

9399

        let mut highest = usize::MIN;

259

208018

        for v in V.iter_ones() {

260

208018

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

261

208018

262

9399

        Priority::new(highest)

263

9399

264

265

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

266

///

267

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

268

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

269

        let mut lowest = usize::MAX;

270

        for v in V.iter_ones() {

271

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

272

273

        Priority::new(lowest)

274

275

276

277

/// Checks that the given solutions are a valid partition of the vertices in V

278

6470

pub fn check_partition(W0: &Set, W1: &Set, V: &Set) {

279

6470

    let intersection = W0.clone() & W1;

280

6470

    if intersection.any() {

281

        panic!(

282

            "The winning sets are not disjoint. Vertices in both sets: {}",

283

            intersection

284

);

285

6470

286

287

6470

    let both = W0.clone() | W1;

288

6470

    if both != *V {

289

        let missing = V.clone() & !both;

290

        panic!(

291

            "The winning sets do not cover all vertices. Missing vertices: {}",

292

            missing

293

);

294

6470

295

6470

296

297

/// Returns the given pair ordered by player, left is alpha and right is not_alpha.

298

2741

pub fn x_and_not_x<U>(omega_0: U, omega_1: U, player: Player) -> (U, U) {

299

2741

    match player {

300

1382

        Player::Even => (omega_0, omega_1),

301

1359

        Player::Odd => (omega_1, omega_0),

302

303

2741

304

305

/// Combines a pair of submaps ordered by player into a pair even, odd.

306

1924

pub fn combine<U>(omega_x: U, omega_not_x: U, player: Player) -> (U, U) {

307

1924

    match player {

308

1105

        Player::Even => (omega_x, omega_not_x),

309

819

        Player::Odd => (omega_not_x, omega_x),

310

311

1924

312

313

/// Returns the given pair ordered by player, left is alpha and right is not_alpha.

314

12677

pub fn x_and_not_x_strategy<U, V>(

315

12677

    omega_0: U,

316

12677

    strategy_0: V,

317

12677

    omega_1: U,

318

12677

    strategy_1: V,

319

12677

    player: Player,

320

12677

) -> (U, V, U, V) {

321

12677

    match player {

322

4387

        Player::Even => (omega_0, strategy_0, omega_1, strategy_1),

323

8290

        Player::Odd => (omega_1, strategy_1, omega_0, strategy_0),

324

325

12677

326

327

/// Combines a pair of submaps ordered by player into a pair even, odd.

328

9399

pub fn combine_with_strategy<U, V>(

329

9399

    omega_x: U,

330

9399

    strategy_x: V,

331

9399

    omega_not_x: U,

332

9399

    strategy_not_x: V,

333

9399

    player: Player,

334

9399

) -> (U, V, U, V) {

335

9399

    match player {

336

3718

        Player::Even => (omega_x, strategy_x, omega_not_x, strategy_not_x),

337

5681

        Player::Odd => (omega_not_x, strategy_not_x, omega_x, strategy_x),

338

339

9399

340

341

/// Helper struct to display a set of vertices.

342

struct DisplaySet<'a>(&'a Set);

343

344

impl fmt::Display for DisplaySet<'_> {

345

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

346

        write!(f, "{{{}}}", self.0.iter_ones().format(", "))

347

348

349

350

#[cfg(test)]

351

mod tests {

352

    use merc_io::DumpFiles;

353

    use merc_utilities::random_test;

354

355

    use crate::random_parity_game;

356

    use crate::verify_solution;

357

    use crate::write_pg;

358

359

    #[test]

360

    #[cfg_attr(miri, ignore)] // Miri is too slow for this test.

361

1

    fn test_random_zielonka_solver() {

362

100

        random_test(100, |rng| {

363

100

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

364

100

            let game = random_parity_game(rng, true, 100, 5, 3);

365

366

100

            files.dump("input.pg", |writer| write_pg(writer, &game)).unwrap();

367

368

100

            let (solution, strategy) = super::solve_zielonka(&game, true);

369

370

100

            verify_solution(&game, &solution, &strategy.unwrap());

371

100

});

372

1

373