1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017-2018, 2020-2021 Laboratoire de Recherche et 3 // Développement de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #include "config.h" 21 22 #include <utility> 23 24 #include <spot/misc/timer.hh> 25 #include <spot/twaalgos/game.hh> 26 #include <spot/misc/bddlt.hh> 27 #include <spot/twaalgos/sccinfo.hh> 28 29 namespace spot 30 { 31 namespace 32 { 33 static const std::vector<bool>* ensure_game(const const_twa_graph_ptr & arena,const char * fnname)34 ensure_game(const const_twa_graph_ptr& arena, const char* fnname) 35 { 36 auto owner = arena->get_named_prop<std::vector<bool>>("state-player"); 37 if (!owner) 38 throw std::runtime_error 39 (std::string(fnname) + ": automaton should define \"state-player\""); 40 if (owner->size() != arena->num_states()) 41 throw std::runtime_error 42 (std::string(fnname) + ": \"state-player\" should have " 43 "as many states as the automaton"); 44 return owner; 45 } 46 47 static const std::vector<bool>* ensure_parity_game(const const_twa_graph_ptr & arena,const char * fnname)48 ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname) 49 { 50 bool max, odd; 51 arena->acc().is_parity(max, odd, true); 52 if (!(max && odd)) 53 throw std::runtime_error 54 (std::string(fnname) + 55 ": arena must have max-odd acceptance condition"); 56 for (const auto& e : arena->edges()) 57 if (!e.acc) 58 throw std::runtime_error 59 (std::string(fnname) + ": arena must be colorized"); 60 return ensure_game(arena, fnname); 61 } 62 63 // Internal structs 64 // winning regions for env and player 65 struct winner_t 66 { 67 std::vector<bool> has_winner_; 68 std::vector<bool> winner_; 69 operator ()spot::__anonc177216f0111::winner_t70 inline bool operator()(unsigned v, bool p) 71 { 72 // returns true if player p wins v 73 // false otherwise 74 if (!has_winner_[v]) 75 return false; 76 77 return winner_[v] == p; 78 } 79 setspot::__anonc177216f0111::winner_t80 inline void set(unsigned v, bool p) 81 { 82 has_winner_[v] = true; 83 winner_[v] = p; 84 } 85 unsetspot::__anonc177216f0111::winner_t86 inline void unset(unsigned v) 87 { 88 has_winner_[v] = false; 89 } 90 winnerspot::__anonc177216f0111::winner_t91 inline bool winner(unsigned v) 92 { 93 assert(has_winner_.at(v)); 94 return winner_[v]; 95 } 96 }; // winner_t 97 98 // When using scc decomposition we need to track the 99 // changes made to the graph 100 struct edge_stash_t 101 { edge_stash_tspot::__anonc177216f0111::edge_stash_t102 edge_stash_t(unsigned num, unsigned dst, acc_cond::mark_t acc) noexcept 103 : e_num(num), 104 e_dst(dst), 105 e_acc(acc) 106 { 107 } 108 const unsigned e_num, e_dst; 109 const acc_cond::mark_t e_acc; 110 }; // edge_stash_t 111 112 // Internal structs used by parity_game 113 // Struct to change recursive calls to stack 114 struct work_t 115 { work_tspot::__anonc177216f0111::work_t116 work_t(unsigned wstep_, unsigned rd_, unsigned min_par_, 117 unsigned max_par_) noexcept 118 : wstep(wstep_), 119 rd(rd_), 120 min_par(min_par_), 121 max_par(max_par_) 122 { 123 } 124 const unsigned wstep, rd, min_par, max_par; 125 }; // work_t 126 127 // Collects information about an scc 128 // Used to detect special cases 129 struct subgame_info_t 130 { 131 typedef std::set<unsigned, std::greater<unsigned>> all_parities_t; 132 subgame_info_tspot::__anonc177216f0111::subgame_info_t133 subgame_info_t() noexcept 134 { 135 } 136 subgame_info_tspot::__anonc177216f0111::subgame_info_t137 subgame_info_t(bool empty, bool one_parity, bool one_player0, 138 bool one_player1, all_parities_t parities) noexcept 139 : is_empty(empty), 140 is_one_parity(one_parity), 141 is_one_player0(one_player0), 142 is_one_player1(one_player1), 143 all_parities(parities) 144 {}; 145 bool is_empty; // empty subgame 146 bool is_one_parity; // only one parity appears in the subgame 147 // todo : Not used yet 148 bool is_one_player0; // one player subgame for player0 <-> p==false 149 bool is_one_player1; // one player subgame for player1 <-> p==true 150 all_parities_t all_parities; 151 }; // subgame_info_t 152 153 154 // A class to solve parity games 155 // The current implementation is inspired by 156 // by oink however without multicore and adapted to transition based 157 // acceptance 158 class parity_game 159 { 160 public: 161 solve(const twa_graph_ptr & arena)162 bool solve(const twa_graph_ptr &arena) 163 { 164 // todo check if reordering states according to scc is worth it 165 set_up(arena); 166 // Start recursive zielonka in a bottom-up fashion on each scc 167 subgame_info_t subgame_info; 168 for (c_scc_idx_ = 0; c_scc_idx_ < info_->scc_count(); ++c_scc_idx_) 169 { 170 // Useless SCCs are winning for player 0. 171 if (!info_->is_useful_scc(c_scc_idx_)) 172 { 173 for (unsigned v: c_states()) 174 { 175 w_.set(v, false); 176 // The strategy for player 0 is to take the first 177 // available edge. 178 if ((*owner_ptr_)[v] == false) 179 for (const auto &e : arena_->out(v)) 180 { 181 s_[v] = arena_->edge_number(e); 182 break; 183 } 184 } 185 continue; 186 } 187 // Convert transitions leaving edges to self-loops 188 // and check if trivially solvable 189 subgame_info = fix_scc(); 190 // If empty, the scc was trivially solved 191 if (!subgame_info.is_empty) 192 { 193 // Check for special cases 194 if (subgame_info.is_one_parity) 195 one_par_subgame_solver(subgame_info, max_abs_par_); 196 else 197 { 198 // "Regular" solver 199 max_abs_par_ = *subgame_info.all_parities.begin(); 200 w_stack_.emplace_back(0, 0, 0, max_abs_par_); 201 zielonka(); 202 } 203 } 204 } 205 // All done -> restore graph, i.e. undo self-looping 206 restore(); 207 208 assert(std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(), 209 [](bool b) 210 { return b; })); 211 assert(std::all_of(s_.cbegin(), s_.cend(), 212 [](unsigned e_idx) 213 { return e_idx > 0; })); 214 215 // Put the solution as named property 216 region_t &w = *arena->get_or_set_named_prop<region_t>("state-winner"); 217 strategy_t &s = *arena->get_or_set_named_prop<strategy_t>("strategy"); 218 w.swap(w_.winner_); 219 s.resize(s_.size()); 220 std::copy(s_.begin(), s_.end(), s.begin()); 221 222 clean_up(); 223 return w[arena->get_init_state_number()]; 224 } 225 226 private: 227 228 // Returns the vector of states currently considered 229 // i.e. the states of the current scc 230 // c_scc_idx_ is set in the 'main' loop c_states()231 inline const std::vector<unsigned> &c_states() 232 { 233 assert(info_); 234 return info_->states_of(c_scc_idx_); 235 } 236 set_up(const twa_graph_ptr & arena)237 void set_up(const twa_graph_ptr &arena) 238 { 239 owner_ptr_ = ensure_parity_game(arena, "solve_parity_game()"); 240 arena_ = arena; 241 unsigned n_states = arena_->num_states(); 242 // Resize data structures 243 subgame_.clear(); 244 subgame_.resize(n_states, unseen_mark); 245 w_.has_winner_.clear(); 246 w_.has_winner_.resize(n_states, 0); 247 w_.winner_.clear(); 248 w_.winner_.resize(n_states, 0); 249 s_.clear(); 250 s_.resize(n_states, -1); 251 // Init 252 rd_ = 0; 253 max_abs_par_ = arena_->get_acceptance().used_sets().max_set() - 1; 254 info_ = std::make_unique<scc_info>(arena_); 255 // Every edge leaving an scc needs to be "fixed" 256 // at some point. 257 // We store: number of edge fixed, original dst, original acc 258 change_stash_.clear(); 259 change_stash_.reserve(info_->scc_count() * 2); 260 } 261 262 // Checks if an scc is empty and reports the occurring parities 263 // or special cases 264 inline subgame_info_t inspect_scc(unsigned max_par)265 inspect_scc(unsigned max_par) 266 { 267 subgame_info_t info; 268 info.is_empty = true; 269 info.is_one_player0 = true; 270 info.is_one_player1 = true; 271 for (unsigned v : c_states()) 272 { 273 if (subgame_[v] != unseen_mark) 274 continue; 275 276 bool multi_edge = false; 277 for (const auto &e : arena_->out(v)) 278 if (subgame_[e.dst] == unseen_mark) 279 { 280 info.is_empty = false; 281 unsigned this_par = e.acc.max_set() - 1; 282 if (this_par <= max_par) 283 { 284 info.all_parities.insert(this_par); 285 multi_edge = true; 286 } 287 } 288 if (multi_edge) 289 { 290 // This state has multiple edges, so it is not 291 // a one player subgame for !owner 292 if ((*owner_ptr_)[v]) 293 info.is_one_player1 = false; 294 else 295 info.is_one_player0 = false; 296 } 297 } // v 298 assert(info.all_parities.size() || info.is_empty); 299 info.is_one_parity = info.all_parities.size() == 1; 300 // Done 301 return info; 302 } 303 304 // Checks if an scc can be trivially solved, 305 // that is, all vertices of the scc belong to the 306 // attractor of a transition leaving the scc 307 inline subgame_info_t fix_scc()308 fix_scc() 309 { 310 auto scc_acc = info_->acc_sets_of(c_scc_idx_); 311 // We will override all parities of edges leaving the scc 312 bool added[] = {false, false}; 313 unsigned par_pair[2]; 314 unsigned scc_new_par = std::max(scc_acc.max_set(), 1u); 315 if (scc_new_par&1) 316 { 317 par_pair[1] = scc_new_par; 318 par_pair[0] = scc_new_par+1; 319 } 320 else 321 { 322 par_pair[1] = scc_new_par+1; 323 par_pair[0] = scc_new_par; 324 } 325 acc_cond::mark_t even_mark({par_pair[0]}); 326 acc_cond::mark_t odd_mark({par_pair[1]}); 327 328 // Only necessary to pass tests 329 max_abs_par_ = std::max(par_pair[0], par_pair[1]); 330 331 for (unsigned v : c_states()) 332 { 333 assert(subgame_[v] == unseen_mark); 334 for (auto &e : arena_->out(v)) 335 { 336 // The outgoing edges are taken finitely often 337 // -> disregard parity 338 if (info_->scc_of(e.dst) != c_scc_idx_) 339 { 340 // Edge leaving the scc 341 change_stash_.emplace_back(arena_->edge_number(e), 342 e.dst, e.acc); 343 if (w_.winner(e.dst)) 344 { 345 // Winning region of player -> odd 346 e.acc = odd_mark; 347 added[1] = true; 348 } 349 else 350 { 351 // Winning region of env -> even 352 e.acc = even_mark; 353 added[0] = true; 354 } 355 // Replace with self-loop 356 e.dst = e.src; 357 } 358 } // e 359 } // v 360 361 // Compute the attractors of the self-loops/transitions leaving scc 362 // These can be directly added to the winning states 363 // Note: attractors can not intersect therefore the order in which 364 // they are computed does not matter 365 unsigned dummy_rd; 366 367 for (bool p : {false, true}) 368 if (added[p]) 369 attr(dummy_rd, p, par_pair[p], true, par_pair[p]); 370 371 if (added[0] || added[1]) 372 // Fix "negative" strategy 373 for (unsigned v : c_states()) 374 if (subgame_[v] != unseen_mark) 375 s_[v] = std::abs(s_[v]); 376 377 return inspect_scc(unseen_mark); 378 } // fix_scc 379 380 inline bool attr(unsigned & rd,bool p,unsigned max_par,bool acc_par,unsigned min_win_par)381 attr(unsigned &rd, bool p, unsigned max_par, 382 bool acc_par, unsigned min_win_par) 383 { 384 // Computes the attractor of the winning set of player p within a 385 // subgame given as rd. 386 // If acc_par is true, max_par transitions are also accepting and 387 // the subgame count will be increased 388 // The attracted vertices are directly added to the set 389 390 // Increase rd meaning we create a new subgame 391 if (acc_par) 392 rd = ++rd_; 393 // todo replace with a variant of topo sort ? 394 // As proposed in Oink! / PGSolver 395 // Needs the transposed graph however 396 397 assert((!acc_par) || (acc_par && (max_par&1) == p)); 398 assert(!acc_par || (0 < min_win_par)); 399 assert((min_win_par <= max_par) && (max_par <= max_abs_par_)); 400 401 bool grown = false; 402 // We could also directly mark states as owned, 403 // instead of adding them to to_add first, 404 // possibly reducing the number of iterations. 405 // However by making the algorithm complete a loop 406 // before adding it is like a backward bfs and (generally) reduces 407 // the size of the strategy 408 static std::vector<unsigned> to_add; 409 410 assert(to_add.empty()); 411 412 do 413 { 414 if (!to_add.empty()) 415 { 416 grown = true; 417 for (unsigned v : to_add) 418 { 419 // v is winning 420 w_.set(v, p); 421 // Mark if demanded 422 if (acc_par) 423 { 424 assert(subgame_[v] == unseen_mark); 425 subgame_[v] = rd; 426 } 427 } 428 } 429 to_add.clear(); 430 431 for (unsigned v : c_states()) 432 { 433 if ((subgame_[v] < rd) || (w_(v, p))) 434 // Not in subgame or winning 435 continue; 436 437 bool is_owned = (*owner_ptr_)[v] == p; 438 bool wins = !is_owned; 439 // Loop over out-going 440 441 // Optim: If given the choice, 442 // we seek to go to the "oldest" subgame 443 // That is the subgame with the lowest rd value 444 unsigned min_subgame_idx = -1u; 445 for (const auto &e: arena_->out(v)) 446 { 447 unsigned this_par = e.acc.max_set() - 1; 448 if ((subgame_[e.dst] >= rd) && (this_par <= max_par)) 449 { 450 // Check if winning 451 if (w_(e.dst, p) 452 || (acc_par && (min_win_par <= this_par))) 453 { 454 assert(!acc_par || (this_par < min_win_par) || 455 (acc_par && (min_win_par <= this_par) && 456 ((this_par&1) == p))); 457 if (is_owned) 458 { 459 wins = true; 460 if (acc_par) 461 { 462 s_[v] = arena_->edge_number(e); 463 if (min_win_par <= this_par) 464 // max par edge 465 // change sign -> mark as needs 466 // to be possibly fixed 467 s_[v] = -s_[v]; 468 break; 469 } 470 else 471 { 472 //snapping 473 if (subgame_[e.dst] < min_subgame_idx) 474 { 475 s_[v] = arena_->edge_number(e); 476 min_subgame_idx = subgame_[e.dst]; 477 if (!p) 478 // No optim for env 479 break; 480 } 481 } 482 }// owned 483 } 484 else 485 { 486 if (!is_owned) 487 { 488 wins = false; 489 break; 490 } 491 } // winning 492 } // subgame 493 }// for edges 494 if (wins) 495 to_add.push_back(v); 496 } // for v 497 } while (!to_add.empty()); 498 // done 499 500 assert(to_add.empty()); 501 return grown; 502 } 503 504 // We need to check if transitions that are accepted due 505 // to their parity remain in the winning region of p 506 inline bool fix_strat_acc(unsigned rd,bool p,unsigned min_win_par,unsigned max_par)507 fix_strat_acc(unsigned rd, bool p, unsigned min_win_par, unsigned max_par) 508 { 509 for (unsigned v : c_states()) 510 { 511 // Only current attractor and owned 512 // and winning vertices are concerned 513 if ((subgame_[v] != rd) || !w_(v, p) 514 || ((*owner_ptr_)[v] != p) || (s_[v] > 0)) 515 continue; 516 517 // owned winning vertex of attractor 518 // Get the strategy edge 519 s_[v] = -s_[v]; 520 const auto &e_s = arena_->edge_storage(s_[v]); 521 // Optimization only for player 522 if (!p && w_(e_s.dst, p)) 523 // If current strat is admissible -> nothing to do 524 // for env 525 continue; 526 527 // This is an accepting edge that is no longer admissible 528 // or we seek a more desirable edge (for player) 529 assert(min_win_par <= e_s.acc.max_set() - 1); 530 assert(e_s.acc.max_set() - 1 <= max_par); 531 532 // Strategy heuristic : go to the oldest subgame 533 unsigned min_subgame_idx = -1u; 534 535 s_[v] = -1; 536 for (const auto &e_fix : arena_->out(v)) 537 { 538 if (subgame_[e_fix.dst] >= rd) 539 { 540 unsigned this_par = e_fix.acc.max_set() - 1; 541 // This edge must have less than max_par, 542 // otherwise it would have already been attracted 543 assert((this_par <= max_par) 544 || ((this_par&1) != (max_par&1))); 545 // if it is accepting and leads to the winning region 546 // -> valid fix 547 if ((min_win_par <= this_par) 548 && (this_par <= max_par) 549 && w_(e_fix.dst, p) 550 && (subgame_[e_fix.dst] < min_subgame_idx)) 551 { 552 // Max par edge to older subgame found 553 s_[v] = arena_->edge_number(e_fix); 554 min_subgame_idx = subgame_[e_fix.dst]; 555 } 556 } 557 } 558 if (s_[v] == -1) 559 // NO fix found 560 // This state is NOT won by p due to any accepting edges 561 return true; // true -> grown 562 } 563 // Nothing to fix or all fixed 564 return false; // false -> not grown == all good 565 } 566 zielonka()567 inline void zielonka() 568 { 569 while (!w_stack_.empty()) 570 { 571 auto this_work = w_stack_.back(); 572 w_stack_.pop_back(); 573 574 switch (this_work.wstep) 575 { 576 case (0): 577 { 578 assert(this_work.rd == 0); 579 assert(this_work.min_par == 0); 580 581 unsigned rd; 582 assert(this_work.max_par <= max_abs_par_); 583 584 // Check if empty and get parities 585 subgame_info_t subgame_info = 586 inspect_scc(this_work.max_par); 587 588 if (subgame_info.is_empty) 589 // Nothing to do 590 break; 591 if (subgame_info.is_one_parity) 592 { 593 // Can be trivially solved 594 one_par_subgame_solver(subgame_info, this_work.max_par); 595 break; 596 } 597 598 // Compute the winning parity boundaries 599 // -> Priority compression 600 // Optional, improves performance 601 // Highest actually occurring 602 unsigned max_par = *subgame_info.all_parities.begin(); 603 unsigned min_win_par = max_par; 604 while ((min_win_par > 2) && 605 (!subgame_info.all_parities.count(min_win_par-1))) 606 min_win_par -= 2; 607 assert(max_par > 0); 608 assert(!subgame_info.all_parities.empty()); 609 assert(min_win_par > 0); 610 611 // Get the player 612 bool p = min_win_par&1; 613 assert((max_par&1) == (min_win_par&1)); 614 // Attraction to highest par 615 // This increases rd_ and passes it to rd 616 attr(rd, p, max_par, true, min_win_par); 617 // All those attracted get subgame_[v] <- rd 618 619 // Continuation 620 w_stack_.emplace_back(1, rd, min_win_par, max_par); 621 // Recursion 622 w_stack_.emplace_back(0, 0, 0, min_win_par-1); 623 // Others attracted will have higher counts in subgame 624 break; 625 } 626 case (1): 627 { 628 unsigned rd = this_work.rd; 629 unsigned min_win_par = this_work.min_par; 630 unsigned max_par = this_work.max_par; 631 assert((min_win_par&1) == (max_par&1)); 632 bool p = min_win_par&1; 633 // Check if the attractor of w_[!p] is equal to w_[!p] 634 // if so, player wins if there remain accepting transitions 635 // for max_par (see fix_strat_acc) 636 // This does not increase but reuse rd 637 bool grown = attr(rd, !p, max_par, false, min_win_par); 638 // todo investigate: A is an attractor, so the only way that 639 // attr(w[!p]) != w[!p] is if the max par "exit" edges lead 640 // to a trap for player/ exit the winning region of the 641 // player so we can do a fast check instead of the 642 // generic attr computation which only needs to be done 643 // if the fast check is positive 644 645 // Check if strategy needs to be fixed / is fixable 646 if (!grown) 647 // this only concerns parity accepting edges 648 grown = fix_strat_acc(rd, p, min_win_par, max_par); 649 // If !grown we are done, and the partitions are valid 650 651 if (grown) 652 { 653 // Reset current game without !p attractor 654 for (unsigned v : c_states()) 655 if (!w_(v, !p) && (subgame_[v] >= rd)) 656 { 657 // delete ownership 658 w_.unset(v); 659 // Mark as unseen 660 subgame_[v] = unseen_mark; 661 // Unset strat for testing 662 s_[v] = -1; 663 } 664 w_stack_.emplace_back(0, 0, 0, max_par); 665 // No need to do anything else 666 // the attractor of !p of this level is not changed 667 } 668 break; 669 } 670 default: 671 throw std::runtime_error("No valid workstep"); 672 } // switch 673 } // while 674 } // zielonka 675 676 // Undo change to the graph made along the way restore()677 inline void restore() 678 { 679 // "Unfix" the edges leaving the sccs 680 // This is called once the game has been solved 681 for (auto &e_stash : change_stash_) 682 { 683 auto &e = arena_->edge_storage(e_stash.e_num); 684 e.dst = e_stash.e_dst; 685 e.acc = e_stash.e_acc; 686 } 687 // Done 688 } 689 690 // Empty all internal variables clean_up()691 inline void clean_up() 692 { 693 info_ = nullptr; 694 subgame_.clear(); 695 w_.has_winner_.clear(); 696 w_.winner_.clear(); 697 s_.clear(); 698 rd_ = 0; 699 max_abs_par_ = 0; 700 change_stash_.clear(); 701 } 702 703 // Dedicated solver for special cases one_par_subgame_solver(const subgame_info_t & info,unsigned max_par)704 inline void one_par_subgame_solver(const subgame_info_t &info, 705 unsigned max_par) 706 { 707 assert(info.all_parities.size() == 1); 708 // The entire subgame is won by the player of the only parity 709 // Any edge will do 710 // todo optim for smaller circuit 711 // This subgame gets its own counter 712 ++rd_; 713 unsigned rd = rd_; 714 unsigned one_par = *info.all_parities.begin(); 715 bool winner = one_par & 1; 716 assert(one_par <= max_par); 717 718 for (unsigned v : c_states()) 719 { 720 if (subgame_[v] != unseen_mark) 721 continue; 722 // State of the subgame 723 subgame_[v] = rd; 724 w_.set(v, winner); 725 // Get the strategy 726 assert(s_[v] == -1); 727 for (const auto &e : arena_->out(v)) 728 { 729 unsigned this_par = e.acc.max_set() - 1; 730 if ((subgame_[e.dst] >= rd) && (this_par <= max_par)) 731 { 732 assert(this_par == one_par); 733 // Ok for strat 734 s_[v] = arena_->edge_number(e); 735 break; 736 } 737 } 738 assert((0 < s_[v]) && (s_[v] < unseen_mark)); 739 } 740 // Done 741 } 742 743 const unsigned unseen_mark = std::numeric_limits<unsigned>::max(); 744 745 twa_graph_ptr arena_; 746 const std::vector<bool> *owner_ptr_; 747 unsigned rd_; 748 winner_t w_; 749 // Subgame array similar to the one from oink! 750 std::vector<unsigned> subgame_; 751 // strategies for env and player; For synthesis only player is needed 752 // We need a signed value here in order to "fix" the strategy 753 // during construction 754 std::vector<long long> s_; 755 756 // Informations about sccs andthe current scc 757 std::unique_ptr<scc_info> info_; 758 unsigned max_abs_par_; // Max parity occurring in the current scc 759 // Info on the current scc 760 unsigned c_scc_idx_; 761 // Fixes made to the sccs that have to be undone 762 // before returning 763 std::vector<edge_stash_t> change_stash_; 764 // Change recursive calls to stack 765 std::vector<work_t> w_stack_; 766 }; 767 768 } // anonymous 769 770 solve_parity_game(const twa_graph_ptr & arena)771 bool solve_parity_game(const twa_graph_ptr& arena) 772 { 773 parity_game pg; 774 return pg.solve(arena); 775 } 776 solve_game(const twa_graph_ptr & arena)777 bool solve_game(const twa_graph_ptr& arena) 778 { 779 bool dummy1, dummy2; 780 auto& acc = arena->acc(); 781 if (acc.is_t()) 782 return solve_safety_game(arena); 783 if (!arena->acc().is_parity(dummy1, dummy2, true)) 784 throw std::runtime_error 785 ("solve_game(): unsupported acceptance condition."); 786 return solve_parity_game(arena); 787 } 788 pg_print(std::ostream & os,const const_twa_graph_ptr & arena)789 void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) 790 { 791 auto owner = ensure_parity_game(arena, "pg_print"); 792 793 unsigned ns = arena->num_states(); 794 unsigned init = arena->get_init_state_number(); 795 os << "parity " << ns - 1 << ";\n"; 796 std::vector<bool> seen(ns, false); 797 std::vector<unsigned> todo({init}); 798 while (!todo.empty()) 799 { 800 unsigned src = todo.back(); 801 todo.pop_back(); 802 if (seen[src]) 803 continue; 804 seen[src] = true; 805 os << src << ' '; 806 os << arena->out(src).begin()->acc.max_set() - 1 << ' '; 807 os << (*owner)[src] << ' '; 808 bool first = true; 809 for (auto& e: arena->out(src)) 810 { 811 if (!first) 812 os << ','; 813 first = false; 814 os << e.dst; 815 if (!seen[e.dst]) 816 todo.push_back(e.dst); 817 } 818 if (src == init) 819 os << " \"INIT\""; 820 os << ";\n"; 821 } 822 } 823 alternate_players(spot::twa_graph_ptr & arena,bool first_player,bool complete0)824 void alternate_players(spot::twa_graph_ptr& arena, 825 bool first_player, bool complete0) 826 { 827 auto um = arena->acc().unsat_mark(); 828 if (!um.first && complete0) 829 throw std::runtime_error 830 ("alternate_players(): Cannot complete monitor."); 831 832 unsigned sink_env = 0; 833 unsigned sink_con = 0; 834 835 std::vector<bool> seen(arena->num_states(), false); 836 unsigned init = arena->get_init_state_number(); 837 std::vector<unsigned> todo({init}); 838 auto owner = new std::vector<bool>(arena->num_states(), false); 839 (*owner)[init] = first_player; 840 while (!todo.empty()) 841 { 842 unsigned src = todo.back(); 843 todo.pop_back(); 844 seen[src] = true; 845 bdd missing = bddtrue; 846 for (const auto& e: arena->out(src)) 847 { 848 bool osrc = (*owner)[src]; 849 if (complete0 && !osrc) 850 missing -= e.cond; 851 852 if (!seen[e.dst]) 853 { 854 (*owner)[e.dst] = !osrc; 855 todo.push_back(e.dst); 856 } 857 else if ((*owner)[e.dst] == osrc) 858 { 859 delete owner; 860 throw std::runtime_error 861 ("alternate_players(): Odd cycle detected."); 862 } 863 } 864 if (complete0 && !(*owner)[src] && missing != bddfalse) 865 { 866 if (sink_env == 0) 867 { 868 sink_env = arena->new_state(); 869 sink_con = arena->new_state(); 870 owner->push_back(true); 871 owner->push_back(false); 872 arena->new_edge(sink_con, sink_env, bddtrue, um.second); 873 arena->new_edge(sink_env, sink_con, bddtrue, um.second); 874 } 875 arena->new_edge(src, sink_con, missing, um.second); 876 } 877 } 878 879 arena->set_named_prop("state-player", owner); 880 } 881 882 twa_graph_ptr highlight_strategy(twa_graph_ptr & aut,int player0_color,int player1_color)883 highlight_strategy(twa_graph_ptr& aut, 884 int player0_color, 885 int player1_color) 886 { 887 auto owner = ensure_game(aut, "highlight_strategy()"); 888 region_t* w = aut->get_named_prop<region_t>("state-winner"); 889 strategy_t* s = aut->get_named_prop<strategy_t>("strategy"); 890 if (!w) 891 throw std::runtime_error 892 ("highlight_strategy(): " 893 "winning region unavailable, solve the game first"); 894 if (!s) 895 throw std::runtime_error 896 ("highlight_strategy(): strategy unavailable, solve the game first"); 897 898 unsigned ns = aut->num_states(); 899 auto* hl_edges = aut->get_or_set_named_prop<std::map<unsigned, unsigned>> 900 ("highlight-edges"); 901 auto* hl_states = aut->get_or_set_named_prop<std::map<unsigned, unsigned>> 902 ("highlight-states"); 903 904 if (unsigned sz = std::min(w->size(), s->size()); sz < ns) 905 ns = sz; 906 907 for (unsigned n = 0; n < ns; ++n) 908 { 909 int color = (*w)[n] ? player1_color : player0_color; 910 if (color == -1) 911 continue; 912 (*hl_states)[n] = color; 913 if ((*w)[n] == (*owner)[n]) 914 (*hl_edges)[(*s)[n]] = color; 915 } 916 917 return aut; 918 } 919 set_state_players(twa_graph_ptr arena,const region_t & owners)920 void set_state_players(twa_graph_ptr arena, const region_t& owners) 921 { 922 set_state_players(arena, region_t(owners)); 923 } 924 set_state_players(twa_graph_ptr arena,region_t && owners)925 void set_state_players(twa_graph_ptr arena, region_t&& owners) 926 { 927 if (owners.size() != arena->num_states()) 928 throw std::runtime_error 929 ("set_state_players(): There must be as many owners as states"); 930 931 arena->set_named_prop<region_t>("state-player", 932 new region_t(std::forward<region_t>(owners))); 933 } 934 set_state_player(twa_graph_ptr arena,unsigned state,bool owner)935 void set_state_player(twa_graph_ptr arena, unsigned state, bool owner) 936 { 937 if (state >= arena->num_states()) 938 throw std::runtime_error("set_state_player(): invalid state number"); 939 940 region_t *owners = arena->get_named_prop<region_t>("state-player"); 941 if (!owners) 942 throw std::runtime_error("set_state_player(): Can only set the state of " 943 "an individual " 944 "state if \"state-player\" already exists."); 945 if (owners->size() != arena->num_states()) 946 throw std::runtime_error("set_state_player(): The \"state-player\" " 947 "vector has a different " 948 "size comparerd to the automaton! " 949 "Called new_state in between?"); 950 951 (*owners)[state] = owner; 952 } 953 get_state_players(const_twa_graph_ptr arena)954 const region_t& get_state_players(const_twa_graph_ptr arena) 955 { 956 region_t *owners = arena->get_named_prop<region_t> 957 ("state-player"); 958 if (!owners) 959 throw std::runtime_error 960 ("get_state_players(): state-player property not defined, not a game?"); 961 962 return *owners; 963 } 964 get_state_player(const_twa_graph_ptr arena,unsigned state)965 bool get_state_player(const_twa_graph_ptr arena, unsigned state) 966 { 967 if (state >= arena->num_states()) 968 throw std::runtime_error("get_state_player(): invalid state number"); 969 970 region_t* owners = arena->get_named_prop<region_t>("state-player"); 971 if (!owners) 972 throw std::runtime_error 973 ("get_state_player(): state-player property not defined, not a game?"); 974 975 return (*owners)[state]; 976 } 977 978 get_strategy(const_twa_graph_ptr arena)979 const strategy_t& get_strategy(const_twa_graph_ptr arena) 980 { 981 auto strat_ptr = arena->get_named_prop<strategy_t>("strategy"); 982 if (!strat_ptr) 983 throw std::runtime_error("get_strategy(): Named prop " 984 "\"strategy\" not set." 985 "Arena not solved?"); 986 return *strat_ptr; 987 } 988 set_strategy(twa_graph_ptr arena,const strategy_t & strat)989 void set_strategy(twa_graph_ptr arena, const strategy_t& strat) 990 { 991 set_strategy(arena, strategy_t(strat)); 992 } set_strategy(twa_graph_ptr arena,strategy_t && strat)993 void set_strategy(twa_graph_ptr arena, strategy_t&& strat) 994 { 995 if (arena->num_states() != strat.size()) 996 throw std::runtime_error("set_strategy(): strategies need to have " 997 "the same size as the automaton."); 998 arena->set_named_prop<strategy_t>("strategy", 999 new strategy_t(std::forward<strategy_t>(strat))); 1000 } 1001 set_synthesis_outputs(const twa_graph_ptr & arena,const bdd & outs)1002 void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs) 1003 { 1004 arena->set_named_prop<bdd>("synthesis-outputs", new bdd(outs)); 1005 } 1006 get_synthesis_outputs(const const_twa_graph_ptr & arena)1007 bdd get_synthesis_outputs(const const_twa_graph_ptr& arena) 1008 { 1009 if (auto outptr = arena->get_named_prop<bdd>("synthesis-outputs")) 1010 return *outptr; 1011 else 1012 throw std::runtime_error 1013 ("get_synthesis_outputs(): synthesis-outputs not defined"); 1014 } 1015 1016 std::vector<std::string> get_synthesis_output_aps(const const_twa_graph_ptr & arena)1017 get_synthesis_output_aps(const const_twa_graph_ptr& arena) 1018 { 1019 std::vector<std::string> out_names; 1020 1021 bdd outs = get_synthesis_outputs(arena); 1022 1023 auto dict = arena->get_dict(); 1024 1025 auto to_bdd = [&](const auto& x) 1026 { 1027 return bdd_ithvar(dict->has_registered_proposition(x, arena.get())); 1028 }; 1029 1030 for (const auto& ap : arena->ap()) 1031 if (bdd_implies(outs, to_bdd(ap))) 1032 out_names.push_back(ap.ap_name()); 1033 1034 return out_names; 1035 } 1036 1037 set_state_winners(twa_graph_ptr arena,const region_t & winners)1038 void set_state_winners(twa_graph_ptr arena, const region_t& winners) 1039 { 1040 set_state_winners(arena, region_t(winners)); 1041 } 1042 set_state_winners(twa_graph_ptr arena,region_t && winners)1043 void set_state_winners(twa_graph_ptr arena, region_t&& winners) 1044 { 1045 if (winners.size() != arena->num_states()) 1046 throw std::runtime_error 1047 ("set_state_winners(): There must be as many winners as states"); 1048 1049 arena->set_named_prop<region_t>("state-winner", 1050 new region_t(std::forward<region_t>(winners))); 1051 } 1052 set_state_winner(twa_graph_ptr arena,unsigned state,bool winner)1053 void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner) 1054 { 1055 if (state >= arena->num_states()) 1056 throw std::runtime_error("set_state_winner(): invalid state number"); 1057 1058 region_t *winners = arena->get_named_prop<region_t>("state-winner"); 1059 if (!winners) 1060 throw std::runtime_error("set_state_winner(): Can only set the state of " 1061 "an individual " 1062 "state if \"state-winner\" already exists."); 1063 if (winners->size() != arena->num_states()) 1064 throw std::runtime_error("set_state_winner(): The \"state-winnerr\" " 1065 "vector has a different " 1066 "size compared to the automaton! " 1067 "Called new_state in between?"); 1068 1069 (*winners)[state] = winner; 1070 } 1071 get_state_winners(const_twa_graph_ptr arena)1072 const region_t& get_state_winners(const_twa_graph_ptr arena) 1073 { 1074 region_t *winners = arena->get_named_prop<region_t>("state-winner"); 1075 if (!winners) 1076 throw std::runtime_error 1077 ("get_state_winners(): state-winner property not defined, not a game?"); 1078 1079 return *winners; 1080 } 1081 get_state_winner(const_twa_graph_ptr arena,unsigned state)1082 bool get_state_winner(const_twa_graph_ptr arena, unsigned state) 1083 { 1084 if (state >= arena->num_states()) 1085 throw std::runtime_error("get_state_winner(): invalid state number"); 1086 1087 region_t* winners = arena->get_named_prop<region_t>("state-winner"); 1088 if (!winners) 1089 throw std::runtime_error 1090 ("get_state_winner(): state-winner property not defined, not a game?"); 1091 1092 return (*winners)[state]; 1093 } 1094 1095 solve_safety_game(const twa_graph_ptr & game)1096 bool solve_safety_game(const twa_graph_ptr& game) 1097 { 1098 if (!game->acc().is_t()) 1099 throw std::runtime_error 1100 ("solve_safety_game(): arena should have true acceptance"); 1101 1102 auto owners = get_state_players(game); 1103 1104 unsigned ns = game->num_states(); 1105 auto winners = new region_t(ns, true); 1106 game->set_named_prop("state-winner", winners); 1107 auto strategy = new strategy_t(ns, 0); 1108 game->set_named_prop("strategy", strategy); 1109 1110 // transposed is a reversed copy of game to compute predecessors 1111 // more easily. It also keep track of the original edge iindex. 1112 struct edge_data { 1113 unsigned edgeidx; 1114 }; 1115 digraph<void, edge_data> transposed; 1116 // Reverse the automaton, compute the out degree of 1117 // each state, and save dead-states in queue. 1118 transposed.new_states(ns); 1119 std::vector<unsigned> out_degree; 1120 out_degree.reserve(ns); 1121 std::vector<unsigned> queue; 1122 for (unsigned s = 0; s < ns; ++s) 1123 { 1124 unsigned deg = 0; 1125 for (auto& e: game->out(s)) 1126 { 1127 transposed.new_edge(e.dst, e.src, game->edge_number(e)); 1128 ++deg; 1129 } 1130 out_degree.push_back(deg); 1131 if (deg == 0) 1132 { 1133 (*winners)[s] = false; 1134 queue.push_back(s); 1135 } 1136 } 1137 // queue is initially filled with dead-states, which are winning 1138 // for player 0. Any predecessor owned by player 0 is therefore 1139 // winning as well (check 1), and any predecessor owned by player 1140 // 1 that has all its successors winning for player 0 (check 2) is 1141 // also winning. Use queue to propagate everything. 1142 // For the second check, we decrease out_degree by each edge leading 1143 // to a state winning for player 0, so if out_degree reaches 0, 1144 // we have ensured that all outgoing transitions are winning for 0. 1145 // 1146 // We use queue as a stack, to propagate bad states in DFS. 1147 // However it would be ok to replace the vector by a std::deque 1148 // to implement a BFS and build shorter strategies for player 0. 1149 // Right no we are assuming that strategies for player 0 have 1150 // limited uses, so we just avoid the overhead of std::deque in 1151 // favor of the simpler std::vector. 1152 while (!queue.empty()) 1153 { 1154 unsigned s = queue.back(); 1155 queue.pop_back(); 1156 for (auto& e: transposed.out(s)) 1157 { 1158 unsigned pred = e.dst; 1159 if (!(*winners)[pred]) 1160 continue; 1161 // check 1 || check 2 1162 bool check1 = owners[pred] == false; 1163 if (check1 || --out_degree[pred] == 0) 1164 { 1165 (*winners)[pred] = false; 1166 queue.push_back(pred); 1167 if (check1) 1168 (*strategy)[pred] = e.edgeidx; 1169 } 1170 } 1171 } 1172 // Let's fill in the strategy for Player 1. 1173 for (unsigned s = 0; s < ns; ++s) 1174 if (owners[s] && (*winners)[s]) 1175 for (auto& e: game->out(s)) 1176 if ((*winners)[e.dst]) 1177 { 1178 (*strategy)[s] = game->edge_number(e); 1179 break; 1180 } 1181 1182 return (*winners)[game->get_init_state_number()]; 1183 } 1184 } 1185