game.cc 35.8 KB
Newer Older
Thibaud Michaud's avatar
Thibaud Michaud committed
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement
Thibaud Michaud's avatar
Thibaud Michaud committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#include "config.h"
Thibaud Michaud's avatar
Thibaud Michaud committed
21

22
#include <spot/twaalgos/game.hh>
23
24
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
25
26
27

namespace spot
{
28
29
  namespace
  {
30
31
32
33
34
35
36
37
38
39
40
41
42
    static const std::vector<bool>*
    ensure_game(const const_twa_graph_ptr& arena, const char* fnname)
    {
      auto owner = arena->get_named_prop<std::vector<bool>>("state-player");
      if (!owner)
        throw std::runtime_error
          (std::string(fnname) + ": automaton should define \"state-player\"");
      if (owner->size() != arena->num_states())
        throw std::runtime_error
          (std::string(fnname) + ": \"state-player\" should have "
           "as many states as the automaton");
      return owner;
    }
Thibaud Michaud's avatar
Thibaud Michaud committed
43

44
45
    static const std::vector<bool>*
    ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname)
Thibaud Michaud's avatar
Thibaud Michaud committed
46
    {
47
48
49
50
51
52
53
54
55
56
      bool max, odd;
      arena->acc().is_parity(max, odd, true);
      if (!(max && odd))
        throw std::runtime_error
          (std::string(fnname) +
           ": arena must have max-odd acceptance condition");
      for (const auto& e : arena->edges())
        if (!e.acc)
          throw std::runtime_error
            (std::string(fnname) + ": arena must be colorized");
57
      return ensure_game(arena, fnname);
Thibaud Michaud's avatar
Thibaud Michaud committed
58
59
    }

60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
    // Internal structs
    // winning regions for env and player
    struct winner_t
    {
      std::vector<bool> has_winner_;
      std::vector<bool> winner_;

      inline bool operator()(unsigned v, bool p)
      {
        // returns true if player p wins v
        // false otherwise
        if (!has_winner_[v])
          return false;

        return winner_[v] == p;
      }

      inline void set(unsigned v, bool p)
      {
        has_winner_[v] = true;
        winner_[v] = p;
      }

      inline void unset(unsigned v)
      {
        has_winner_[v] = false;
      }

      inline bool winner(unsigned v)
      {
        assert(has_winner_.at(v));
        return winner_[v];
      }
    }; // winner_t

    // When using scc decomposition we need to track the
    // changes made to the graph
    struct edge_stash_t
98
    {
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
      edge_stash_t(unsigned num, unsigned dst, acc_cond::mark_t acc) noexcept
        : e_num(num),
          e_dst(dst),
          e_acc(acc)
      {
      }
      const unsigned e_num, e_dst;
      const acc_cond::mark_t e_acc;
    }; // edge_stash_t

    // Internal structs used by parity_game
    // Struct to change recursive calls to stack
    struct work_t
    {
      work_t(unsigned wstep_, unsigned rd_, unsigned min_par_,
             unsigned max_par_) noexcept
        : wstep(wstep_),
          rd(rd_),
          min_par(min_par_),
          max_par(max_par_)
      {
      }
      const unsigned wstep, rd, min_par, max_par;
    }; // work_t

    // Collects information about an scc
    // Used to detect special cases
    struct subgame_info_t
    {
      typedef std::set<unsigned, std::greater<unsigned>> all_parities_t;

      subgame_info_t() noexcept
      {
      }

      subgame_info_t(bool empty, bool one_parity, bool one_player0,
                     bool one_player1, all_parities_t parities) noexcept
        : is_empty(empty),
          is_one_parity(one_parity),
          is_one_player0(one_player0),
          is_one_player1(one_player1),
          all_parities(parities)
      {};
      bool is_empty; // empty subgame
      bool is_one_parity; // only one parity appears in the subgame
      // todo : Not used yet
      bool is_one_player0; // one player subgame for player0 <-> p==false
      bool is_one_player1; // one player subgame for player1 <-> p==true
      all_parities_t all_parities;
    }; // subgame_info_t


    // A class to solve parity games
    // The current implementation is inspired by
    // by oink however without multicore and adapted to transition based
    // acceptance
    class parity_game
    {
    public:

      bool solve(const twa_graph_ptr &arena)
      {
        // todo check if reordering states according to scc is worth it
        set_up(arena);
        // Start recursive zielonka in a bottom-up fashion on each scc
        subgame_info_t subgame_info;
        for (c_scc_idx_ = 0; c_scc_idx_ < info_->scc_count(); ++c_scc_idx_)
          {
            // Useless SCCs are winning for player 0.
            if (!info_->is_useful_scc(c_scc_idx_))
              {
                for (unsigned v: c_states())
171
172
173
174
175
176
177
178
179
180
181
                  {
                    w_.set(v, false);
                    // The strategy for player 0 is to take the first
                    // available edge.
                    if ((*owner_ptr_)[v] == false)
                      for (const auto &e : arena_->out(v))
                        {
                          s_[v] = arena_->edge_number(e);
                          break;
                        }
                  }
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
                continue;
              }
            // Convert transitions leaving edges to self-loops
            // and check if trivially solvable
            subgame_info = fix_scc();
            // If empty, the scc was trivially solved
            if (!subgame_info.is_empty)
              {
                // Check for special cases
                if (subgame_info.is_one_parity)
                  one_par_subgame_solver(subgame_info, max_abs_par_);
                else
                  {
                    // "Regular" solver
                    max_abs_par_ = *subgame_info.all_parities.begin();
                    w_stack_.emplace_back(0, 0, 0, max_abs_par_);
                    zielonka();
                  }
              }
          }
        // All done -> restore graph, i.e. undo self-looping
        restore();

        assert(std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(),
                           [](bool b)
                           { return b; }));
        assert(std::all_of(s_.cbegin(), s_.cend(),
                           [](unsigned e_idx)
                           { return e_idx > 0; }));

        // Put the solution as named property
        region_t &w = *arena->get_or_set_named_prop<region_t>("state-winner");
        strategy_t &s = *arena->get_or_set_named_prop<strategy_t>("strategy");
        w.swap(w_.winner_);
        s.resize(s_.size());
        std::copy(s_.begin(), s_.end(), s.begin());

        clean_up();
        return w[arena->get_init_state_number()];
      }

    private:

      // Returns the vector of states currently considered
      // i.e. the states of the current scc
      // c_scc_idx_ is set in the 'main' loop
      inline const std::vector<unsigned> &c_states()
      {
        assert(info_);
        return info_->states_of(c_scc_idx_);
      }

      void set_up(const twa_graph_ptr &arena)
      {
236
        owner_ptr_ = ensure_parity_game(arena, "solve_parity_game()");
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
        arena_ = arena;
        unsigned n_states = arena_->num_states();
        // Resize data structures
        subgame_.clear();
        subgame_.resize(n_states, unseen_mark);
        w_.has_winner_.clear();
        w_.has_winner_.resize(n_states, 0);
        w_.winner_.clear();
        w_.winner_.resize(n_states, 0);
        s_.clear();
        s_.resize(n_states, -1);
        // Init
        rd_ = 0;
        max_abs_par_ = arena_->get_acceptance().used_sets().max_set() - 1;
        info_ = std::make_unique<scc_info>(arena_);
        // Every edge leaving an scc needs to be "fixed"
        // at some point.
        // We store: number of edge fixed, original dst, original acc
        change_stash_.clear();
        change_stash_.reserve(info_->scc_count() * 2);
      }

      // Checks if an scc is empty and reports the occurring parities
      // or special cases
      inline subgame_info_t
      inspect_scc(unsigned max_par)
      {
        subgame_info_t info;
        info.is_empty = true;
        info.is_one_player0 = true;
        info.is_one_player1 = true;
        for (unsigned v : c_states())
          {
            if (subgame_[v] != unseen_mark)
              continue;

            bool multi_edge = false;
            for (const auto &e : arena_->out(v))
              if (subgame_[e.dst] == unseen_mark)
276
                {
277
278
279
                  info.is_empty = false;
                  unsigned this_par = e.acc.max_set() - 1;
                  if (this_par <= max_par)
280
                    {
281
282
                      info.all_parities.insert(this_par);
                      multi_edge = true;
283
                    }
284
                }
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
            if (multi_edge)
              {
                // This state has multiple edges, so it is not
                // a one player subgame for !owner
                if ((*owner_ptr_)[v])
                  info.is_one_player1 = false;
                else
                  info.is_one_player0 = false;
              }
          } // v
        assert(info.all_parities.size() || info.is_empty);
        info.is_one_parity = info.all_parities.size() == 1;
        // Done
        return info;
      }

      // Checks if an scc can be trivially solved,
      // that is, all vertices of the scc belong to the
      // attractor of a transition leaving the scc
      inline subgame_info_t
      fix_scc()
      {
        auto scc_acc = info_->acc_sets_of(c_scc_idx_);
        // We will override all parities of edges leaving the scc
        bool added[] = {false, false};
        unsigned par_pair[2];
        unsigned scc_new_par = std::max(scc_acc.max_set(), 1u);
        if (scc_new_par&1)
          {
            par_pair[1] = scc_new_par;
            par_pair[0] = scc_new_par+1;
          }
        else
          {
            par_pair[1] = scc_new_par+1;
            par_pair[0] = scc_new_par;
          }
        acc_cond::mark_t even_mark({par_pair[0]});
        acc_cond::mark_t odd_mark({par_pair[1]});

        // Only necessary to pass tests
        max_abs_par_ = std::max(par_pair[0], par_pair[1]);

        for (unsigned v : c_states())
          {
            assert(subgame_[v] == unseen_mark);
            for (auto &e : arena_->out(v))
              {
                // The outgoing edges are taken finitely often
                // -> disregard parity
335
                if (info_->scc_of(e.dst) != c_scc_idx_)
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
                  {
                    // Edge leaving the scc
                    change_stash_.emplace_back(arena_->edge_number(e),
                                               e.dst, e.acc);
                    if (w_.winner(e.dst))
                      {
                        // Winning region of player -> odd
                        e.acc = odd_mark;
                        added[1] = true;
                      }
                    else
                      {
                        // Winning region of env -> even
                        e.acc = even_mark;
                        added[0] = true;
                      }
                    // Replace with self-loop
                    e.dst = e.src;
                  }
              } // e
          } // v

        // Compute the attractors of the self-loops/transitions leaving scc
        // These can be directly added to the winning states
        // Note: attractors can not intersect therefore the order in which
        // they are computed does not matter
        unsigned dummy_rd;

        for (bool p : {false, true})
          if (added[p])
            attr(dummy_rd, p, par_pair[p], true, par_pair[p]);

        if (added[0] || added[1])
          // Fix "negative" strategy
          for (unsigned v : c_states())
            if (subgame_[v] != unseen_mark)
              s_[v] = std::abs(s_[v]);

        return inspect_scc(unseen_mark);
      } // fix_scc

      inline bool
      attr(unsigned &rd, bool p, unsigned max_par,
           bool acc_par, unsigned min_win_par)
      {
        // Computes the attractor of the winning set of player p within a
        // subgame given as rd.
        // If acc_par is true, max_par transitions are also accepting and
        // the subgame count will be increased
        // The attracted vertices are directly added to the set

        // Increase rd meaning we create a new subgame
        if (acc_par)
          rd = ++rd_;
        // todo replace with a variant of topo sort ?
        // As proposed in Oink! / PGSolver
        // Needs the transposed graph however

        assert((!acc_par) || (acc_par && (max_par&1) == p));
        assert(!acc_par || (0 < min_win_par));
        assert((min_win_par <= max_par) && (max_par <= max_abs_par_));

        bool grown = false;
        // We could also directly mark states as owned,
        // instead of adding them to to_add first,
        // possibly reducing the number of iterations.
        // However by making the algorithm complete a loop
        // before adding it is like a backward bfs and (generally) reduces
        // the size of the strategy
        static std::vector<unsigned> to_add;

        assert(to_add.empty());

        do
          {
            if (!to_add.empty())
              {
                grown = true;
                for (unsigned v : to_add)
                  {
                    // v is winning
                    w_.set(v, p);
                    // Mark if demanded
                    if (acc_par)
                      {
                        assert(subgame_[v] == unseen_mark);
                        subgame_[v] = rd;
                      }
                  }
              }
            to_add.clear();

            for (unsigned v : c_states())
              {
                if ((subgame_[v] < rd) || (w_(v, p)))
                  // Not in subgame or winning
                  continue;

                bool is_owned = (*owner_ptr_)[v] == p;
                bool wins = !is_owned;
                // Loop over out-going

                // Optim: If given the choice,
                // we seek to go to the "oldest" subgame
                // That is the subgame with the lowest rd value
                unsigned min_subgame_idx = -1u;
                for (const auto &e: arena_->out(v))
                  {
                    unsigned this_par = e.acc.max_set() - 1;
                    if ((subgame_[e.dst] >= rd) && (this_par <= max_par))
                      {
                        // Check if winning
                        if (w_(e.dst, p)
                            || (acc_par && (min_win_par <= this_par)))
                          {
                            assert(!acc_par || (this_par < min_win_par) ||
                                   (acc_par && (min_win_par <= this_par) &&
                                    ((this_par&1) == p)));
                            if (is_owned)
                              {
                                wins = true;
                                if (acc_par)
                                  {
                                    s_[v] = arena_->edge_number(e);
                                    if (min_win_par <= this_par)
                                      // max par edge
                                      // change sign -> mark as needs
                                      // to be possibly fixed
                                      s_[v] = -s_[v];
                                    break;
                                  }
                                else
                                  {
                                    //snapping
                                    if (subgame_[e.dst] < min_subgame_idx)
                                      {
                                        s_[v] = arena_->edge_number(e);
                                        min_subgame_idx = subgame_[e.dst];
                                        if (!p)
                                          // No optim for env
                                          break;
                                      }
                                  }
                              }// owned
                          }
                        else
                          {
                            if (!is_owned)
                              {
                                wins = false;
                                break;
                              }
                          } // winning
                      } // subgame
                  }// for edges
                if (wins)
                  to_add.push_back(v);
              } // for v
          } while (!to_add.empty());
        // done

        assert(to_add.empty());
        return grown;
      }

      // We need to check if transitions that are accepted due
      // to their parity remain in the winning region of p
      inline bool
      fix_strat_acc(unsigned rd, bool p, unsigned min_win_par, unsigned max_par)
      {
        for (unsigned v : c_states())
          {
            // Only current attractor and owned
            // and winning vertices are concerned
            if ((subgame_[v] != rd) || !w_(v, p)
                || ((*owner_ptr_)[v] != p) || (s_[v] > 0))
              continue;

            // owned winning vertex of attractor
            // Get the strategy edge
            s_[v] = -s_[v];
            const auto &e_s = arena_->edge_storage(s_[v]);
            // Optimization only for player
            if (!p && w_(e_s.dst, p))
              // If current strat is admissible -> nothing to do
              // for env
              continue;

            // This is an accepting edge that is no longer admissible
            // or we seek a more desirable edge (for player)
            assert(min_win_par <= e_s.acc.max_set() - 1);
            assert(e_s.acc.max_set() - 1 <= max_par);

            // Strategy heuristic : go to the oldest subgame
            unsigned min_subgame_idx = -1u;

            s_[v] = -1;
            for (const auto &e_fix : arena_->out(v))
              {
                if (subgame_[e_fix.dst] >= rd)
                  {
                    unsigned this_par = e_fix.acc.max_set() - 1;
                    // This edge must have less than max_par,
                    // otherwise it would have already been attracted
                    assert((this_par <= max_par)
                           || ((this_par&1) != (max_par&1)));
                    // if it is accepting and leads to the winning region
                    // -> valid fix
                    if ((min_win_par <= this_par)
                        && (this_par <= max_par)
                        && w_(e_fix.dst, p)
                        && (subgame_[e_fix.dst] < min_subgame_idx))
                      {
                        // Max par edge to older subgame found
                        s_[v] = arena_->edge_number(e_fix);
                        min_subgame_idx = subgame_[e_fix.dst];
                      }
                  }
              }
            if (s_[v] == -1)
              // NO fix found
              // This state is NOT won by p due to any accepting edges
              return true; // true -> grown
          }
        // Nothing to fix or all fixed
        return false; // false -> not grown == all good
      }
563

564
565
566
567
568
569
570
571
572
573
      inline void zielonka()
      {
        while (!w_stack_.empty())
          {
            auto this_work = w_stack_.back();
            w_stack_.pop_back();

            switch (this_work.wstep)
              {
              case (0):
574
                {
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
                  assert(this_work.rd == 0);
                  assert(this_work.min_par == 0);

                  unsigned rd;
                  assert(this_work.max_par <= max_abs_par_);

                  // Check if empty and get parities
                  subgame_info_t subgame_info =
                    inspect_scc(this_work.max_par);

                  if (subgame_info.is_empty)
                    // Nothing to do
                    break;
                  if (subgame_info.is_one_parity)
                    {
                      // Can be trivially solved
                      one_par_subgame_solver(subgame_info, this_work.max_par);
                      break;
                    }

                  // Compute the winning parity boundaries
                  // -> Priority compression
                  // Optional, improves performance
                  // Highest actually occurring
                  unsigned max_par = *subgame_info.all_parities.begin();
                  unsigned min_win_par = max_par;
                  while ((min_win_par > 2) &&
                         (!subgame_info.all_parities.count(min_win_par-1)))
                    min_win_par -= 2;
                  assert(max_par > 0);
                  assert(!subgame_info.all_parities.empty());
                  assert(min_win_par > 0);

                  // Get the player
                  bool p = min_win_par&1;
                  assert((max_par&1) == (min_win_par&1));
                  // Attraction to highest par
                  // This increases rd_ and passes it to rd
                  attr(rd, p, max_par, true, min_win_par);
                  // All those attracted get subgame_[v] <- rd

                  // Continuation
                  w_stack_.emplace_back(1, rd, min_win_par, max_par);
                  // Recursion
                  w_stack_.emplace_back(0, 0, 0, min_win_par-1);
                  // Others attracted will have higher counts in subgame
                  break;
622
                }
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
              case (1):
                {
                  unsigned rd = this_work.rd;
                  unsigned min_win_par = this_work.min_par;
                  unsigned max_par = this_work.max_par;
                  assert((min_win_par&1) == (max_par&1));
                  bool p = min_win_par&1;
                  // Check if the attractor of w_[!p] is equal to w_[!p]
                  // if so, player wins if there remain accepting transitions
                  // for max_par (see fix_strat_acc)
                  // This does not increase but reuse rd
                  bool grown = attr(rd, !p, max_par, false, min_win_par);
                  // todo investigate: A is an attractor, so the only way that
                  // attr(w[!p]) != w[!p] is if the max par "exit" edges lead
                  // to a trap for player/ exit the winning region of the
                  // player so we can do a fast check instead of the
                  // generic attr computation which only needs to be done
                  // if the fast check is positive

                  // Check if strategy needs to be fixed / is fixable
                  if (!grown)
                    // this only concerns parity accepting edges
                    grown = fix_strat_acc(rd, p, min_win_par, max_par);
                  // If !grown we are done, and the partitions are valid

                  if (grown)
                    {
                      // Reset current game without !p attractor
                      for (unsigned v : c_states())
                        if (!w_(v, !p) && (subgame_[v] >= rd))
                          {
                            // delete ownership
                            w_.unset(v);
                            // Mark as unseen
                            subgame_[v] = unseen_mark;
                            // Unset strat for testing
                            s_[v] = -1;
                          }
                      w_stack_.emplace_back(0, 0, 0, max_par);
                      // No need to do anything else
                      // the attractor of !p of this level is not changed
                    }
                  break;
                }
              default:
                throw std::runtime_error("No valid workstep");
              } // switch
          } // while
      } // zielonka

      // Undo change to the graph made along the way
      inline void restore()
      {
        // "Unfix" the edges leaving the sccs
        // This is called once the game has been solved
        for (auto &e_stash : change_stash_)
          {
            auto &e = arena_->edge_storage(e_stash.e_num);
            e.dst = e_stash.e_dst;
            e.acc = e_stash.e_acc;
          }
        // Done
      }
686

687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
      // Empty all internal variables
      inline void clean_up()
      {
        info_ = nullptr;
        subgame_.clear();
        w_.has_winner_.clear();
        w_.winner_.clear();
        s_.clear();
        rd_ = 0;
        max_abs_par_ = 0;
        change_stash_.clear();
      }

      // Dedicated solver for special cases
      inline void one_par_subgame_solver(const subgame_info_t &info,
                                         unsigned max_par)
      {
        assert(info.all_parities.size() == 1);
        // The entire subgame is won by the player of the only parity
        // Any edge will do
        // todo optim for smaller circuit
        // This subgame gets its own counter
        ++rd_;
        unsigned rd = rd_;
        unsigned one_par = *info.all_parities.begin();
        bool winner = one_par & 1;
        assert(one_par <= max_par);

        for (unsigned v : c_states())
          {
            if (subgame_[v] != unseen_mark)
              continue;
            // State of the subgame
            subgame_[v] = rd;
            w_.set(v, winner);
            // Get the strategy
            assert(s_[v] == -1);
            for (const auto &e : arena_->out(v))
              {
                unsigned this_par = e.acc.max_set() - 1;
                if ((subgame_[e.dst] >= rd) && (this_par <= max_par))
                  {
                    assert(this_par == one_par);
                    // Ok for strat
                    s_[v] = arena_->edge_number(e);
                    break;
                  }
              }
            assert((0 < s_[v]) && (s_[v] < unseen_mark));
          }
        // Done
      }

      const unsigned unseen_mark = std::numeric_limits<unsigned>::max();

      twa_graph_ptr arena_;
      const std::vector<bool> *owner_ptr_;
      unsigned rd_;
      winner_t w_;
      // Subgame array similar to the one from oink!
      std::vector<unsigned> subgame_;
      // strategies for env and player; For synthesis only player is needed
      // We need a signed value here in order to "fix" the strategy
      // during construction
      std::vector<long long> s_;

      // Informations about sccs andthe current scc
      std::unique_ptr<scc_info> info_;
      unsigned max_abs_par_; // Max parity occurring in the current scc
      // Info on the current scc
      unsigned c_scc_idx_;
      // Fixes made to the sccs that have to be undone
      // before returning
      std::vector<edge_stash_t> change_stash_;
      // Change recursive calls to stack
      std::vector<work_t> w_stack_;
    };
764

765
766
  } // anonymous

767
768
769
770
771
772
  bool solve_parity_game(const twa_graph_ptr& arena)
  {
    parity_game pg;
    return pg.solve(arena);
  }

773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
  void pg_print(std::ostream& os, const const_twa_graph_ptr& arena)
  {
    auto owner = ensure_parity_game(arena, "pg_print");

    unsigned ns = arena->num_states();
    unsigned init = arena->get_init_state_number();
    os << "parity " << ns - 1 << ";\n";
    std::vector<bool> seen(ns, false);
    std::vector<unsigned> todo({init});
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        if (seen[src])
          continue;
        seen[src] = true;
        os << src << ' ';
        os << arena->out(src).begin()->acc.max_set() - 1 << ' ';
        os << (*owner)[src] << ' ';
        bool first = true;
        for (auto& e: arena->out(src))
          {
            if (!first)
              os << ',';
            first = false;
            os << e.dst;
            if (!seen[e.dst])
              todo.push_back(e.dst);
          }
        if (src == init)
          os << " \"INIT\"";
        os << ";\n";
      }
  }

808
  void alternate_players(spot::twa_graph_ptr& arena,
809
810
811
812
                         bool first_player, bool complete0)
  {
    auto um = arena->acc().unsat_mark();
    if (!um.first)
813
      throw std::runtime_error
814
        ("alternate_players(): game winning condition is a tautology");
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844

    unsigned sink_env = 0;
    unsigned sink_con = 0;

    std::vector<bool> seen(arena->num_states(), false);
    unsigned init = arena->get_init_state_number();
    std::vector<unsigned> todo({init});
    auto owner = new std::vector<bool>(arena->num_states(), false);
    (*owner)[init] = first_player;
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        seen[src] = true;
        bdd missing = bddtrue;
        for (const auto& e: arena->out(src))
          {
            bool osrc = (*owner)[src];
            if (complete0 && !osrc)
              missing -= e.cond;

            if (!seen[e.dst])
              {
                (*owner)[e.dst] = !osrc;
                todo.push_back(e.dst);
              }
            else if ((*owner)[e.dst] == osrc)
              {
                delete owner;
                throw
845
                  std::runtime_error("alternate_players(): odd cycle detected");
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
              }
          }
        if (complete0 && !(*owner)[src] && missing != bddfalse)
          {
            if (sink_env == 0)
              {
                sink_env = arena->new_state();
                sink_con = arena->new_state();
                owner->push_back(true);
                owner->push_back(false);
                arena->new_edge(sink_con, sink_env, bddtrue, um.second);
                arena->new_edge(sink_env, sink_con, bddtrue, um.second);
              }
            arena->new_edge(src, sink_con, missing, um.second);
          }
      }

    arena->set_named_prop("state-player", owner);
  }
865
866

  twa_graph_ptr
867
868
869
  highlight_strategy(twa_graph_ptr& aut,
                     int player0_color,
                     int player1_color)
870
  {
871
    auto owner = ensure_game(aut, "highlight_strategy()");
872
873
    region_t* w = aut->get_named_prop<region_t>("state-winner");
    strategy_t* s = aut->get_named_prop<strategy_t>("strategy");
874
875
876
877
878
879
880
    if (!w)
      throw std::runtime_error
        ("highlight_strategy(): "
         "winning region unavailable, solve the game first");
    if (!s)
      throw std::runtime_error
        ("highlight_strategy(): strategy unavailable, solve the game first");
881

882
    unsigned ns = aut->num_states();
883
    auto* hl_edges = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
884
      ("highlight-edges");
885
886
887
888
889
    auto* hl_states = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-states");

    if (unsigned sz = std::min(w->size(), s->size()); sz < ns)
      ns = sz;
890

891
    for (unsigned n = 0; n < ns; ++n)
892
      {
893
894
895
896
897
898
        int color = (*w)[n] ? player1_color : player0_color;
        if (color == -1)
          continue;
        (*hl_states)[n] = color;
        if ((*w)[n] == (*owner)[n])
          (*hl_edges)[(*s)[n]] = color;
899
900
901
902
903
      }

    return aut;
  }

904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
  void set_state_players(twa_graph_ptr arena, std::vector<bool> owners)
  {
    std::vector<bool>* owners_ptr = new std::vector<bool>(owners);
    set_state_players(arena, owners_ptr);
  }

  void set_state_players(twa_graph_ptr arena, std::vector<bool>* owners)
  {
    if (owners->size() != arena->num_states())
      throw std::runtime_error
        ("set_state_players(): There must be as many owners as states");

    arena->set_named_prop<std::vector<bool>>("state-player", owners);
  }

  void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner)
  {
    if (state >= arena->num_states())
      throw std::runtime_error("set_state_player(): invalid state number");

    std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
      ("state-player");
    if (!owners)
      {
        owners = new std::vector<bool>(arena->num_states(), false);
        arena->set_named_prop<std::vector<bool>>("state-player", owners);
      }

    (*owners)[state] = owner;
  }

  const std::vector<bool>& get_state_players(const_twa_graph_ptr arena)
  {
937
    std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
938
      ("state-player");
939
    if (!owners)
940
941
942
      throw std::runtime_error
        ("get_state_players(): state-player property not defined, not a game");

943
    return *owners;
944
945
946
947
948
949
950
  }

  unsigned get_state_player(const_twa_graph_ptr arena, unsigned state)
  {
    if (state >= arena->num_states())
      throw std::runtime_error("get_state_player(): invalid state number");

951
    std::vector<bool>* owners = arena->get_named_prop<std::vector<bool>>
952
      ("state-player");
953
    if (!owners)
954
955
956
      throw std::runtime_error
        ("get_state_player(): state-player property not defined, not a game");

957
958
959
    return (*owners)[state] ? 1 : 0;
  }

960
  bool solve_safety_game(twa_graph_ptr game)
961
  {
962
963
964
965
    if (!game->acc().is_t())
      throw std::runtime_error
        ("solve_safety_game(): arena should have true acceptance");

966
967
    auto owners = get_state_players(game);

968
969
    unsigned ns = game->num_states();
    auto winners = new region_t(ns, true);
970
    game->set_named_prop("state-winner", winners);
971
    auto strategy = new strategy_t(ns, 0);
972
973
    game->set_named_prop("strategy", strategy);

974
975
976
977
978
979
980
981
982
983
984
985
986
    // transposed is a reversed copy of game to compute predecessors
    // more easily.  It also keep track of the original edge iindex.
    struct edge_data {
      unsigned edgeidx;
    };
    digraph<void, edge_data> transposed;
    // Reverse the automaton, compute the out degree of
    // each state, and save dead-states in queue.
    transposed.new_states(ns);
    std::vector<unsigned> out_degree;
    out_degree.reserve(ns);
    std::vector<unsigned> queue;
    for (unsigned s = 0; s < ns; ++s)
987
      {
988
989
990
991
992
993
994
995
996
997
998
999
        unsigned deg = 0;
        for (auto& e: game->out(s))
          {
            transposed.new_edge(e.dst, e.src, game->edge_number(e));
            ++deg;
          }
        out_degree.push_back(deg);
        if (deg == 0)
          {
            (*winners)[s] = false;
            queue.push_back(s);
          }
1000
      }
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
    // queue is initially filled with dead-states, which are winning
    // for player 0.  Any predecessor owned by player 0 is therefore
    // winning as well (check 1), and any predecessor owned by player
    // 1 that has all its successors winning for player 0 (check 2) is
    // also winning.  Use queue to propagate everything.
    // For the second check, we decrease out_degree by each edge leading
    // to a state winning for player 0, so if out_degree reaches 0,
    // we have ensured that all outgoing transitions are winning for 0.
    //
    // We use queue as a stack, to propagate bad states in DFS.
    // However it would be ok to replace the vector by a std::deque
    // to implement a BFS and build shorter strategies for player 0.
    // Right no we are assuming that strategies for player 0 have
    // limited uses, so we just avoid the overhead of std::deque in
    // favor of the simpler std::vector.
    while (!queue.empty())
1017
      {
1018
1019
1020
        unsigned s = queue.back();
        queue.pop_back();
        for (auto& e: transposed.out(s))
1021
          {
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
            unsigned pred = e.dst;
            if (!(*winners)[pred])
              continue;
            // check 1 || check 2
            bool check1 = owners[pred] == false;
            if (check1 || --out_degree[pred] == 0)
              {
                (*winners)[pred] = false;
                queue.push_back(pred);
                if (check1)
                  (*strategy)[pred] = e.edgeidx;
              }
          }
      }
    // Let's fill in the strategy for Player 1.
    for (unsigned s = 0; s < ns; ++s)
      if (owners[s] && (*winners)[s])
        for (auto& e: game->out(s))
          if ((*winners)[e.dst])
            {
              (*strategy)[s] = game->edge_number(e);
              break;
            }
1045
1046

    return (*winners)[game->get_init_state_number()];
1047
  }
Thibaud Michaud's avatar
Thibaud Michaud committed
1048
}