1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2021 Laboratoire de Recherche et Développement 3 // 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 #include <spot/twaalgos/sccinfo.hh> 22 #include <stack> 23 #include <algorithm> 24 #include <queue> 25 #include <spot/twa/bddprint.hh> 26 #include <spot/twaalgos/bfssteps.hh> 27 #include <spot/twaalgos/mask.hh> 28 #include <spot/twaalgos/genem.hh> 29 #include <spot/misc/escape.hh> 30 31 namespace spot 32 { report_need_track_states()33 void scc_info::report_need_track_states() 34 { 35 throw std::runtime_error 36 ("scc_info was not run with option TRACK_STATES"); 37 } 38 report_need_track_succs()39 void scc_info::report_need_track_succs() 40 { 41 throw std::runtime_error 42 ("scc_info was not run with option TRACK_SUCCS"); 43 } 44 report_incompatible_stop_on_acc()45 void scc_info::report_incompatible_stop_on_acc() 46 { 47 throw std::runtime_error 48 ("scc_info was run with option STOP_ON_ACC"); 49 } 50 51 // this one is not yet needed in the hh file report_need_stop_on_acc()52 static void report_need_stop_on_acc() 53 { 54 throw std::runtime_error 55 ("scc_info was not run with option STOP_ON_ACC"); 56 } 57 58 namespace 59 { 60 struct scc 61 { 62 public: sccspot::__anon293b3a100111::scc63 scc(int index, acc_cond::mark_t in_acc): 64 in_acc(in_acc), index(index) 65 { 66 } 67 68 acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition 69 acc_cond::mark_t acc = {}; // union of all acceptance marks in the SCC 70 // intersection of all marks in the SCC 71 acc_cond::mark_t common = acc_cond::mark_t::all(); 72 int index; // Index of the SCC 73 bool trivial = true; // Whether the SCC has no cycle 74 bool accepting = false; // Necessarily accepting 75 }; 76 } 77 scc_info(const scc_and_mark_filter & filt,scc_info_options options)78 scc_info::scc_info(const scc_and_mark_filter& filt, scc_info_options options) 79 : scc_info(filt.get_aut(), filt.start_state(), 80 filt.get_filter(), 81 const_cast<scc_and_mark_filter*>(&filt), options) 82 { 83 } 84 scc_info(const_twa_graph_ptr aut,unsigned initial_state,edge_filter filter,void * filter_data,scc_info_options options)85 scc_info::scc_info(const_twa_graph_ptr aut, 86 unsigned initial_state, 87 edge_filter filter, 88 void* filter_data, 89 scc_info_options options) 90 : aut_(aut), initial_state_(initial_state), 91 filter_(filter), filter_data_(filter_data), 92 options_(options) 93 { 94 unsigned n = aut->num_states(); 95 96 if (initial_state != -1U && n <= initial_state) 97 throw std::runtime_error 98 ("scc_info: supplied initial state does not exist"); 99 100 sccof_.resize(n, -1U); 101 102 if (!!(options & scc_info_options::TRACK_STATES_IF_FIN_USED) 103 && aut->acc().uses_fin_acceptance()) 104 options_ = options = options | scc_info_options::TRACK_STATES; 105 106 std::vector<unsigned> live; 107 live.reserve(n); 108 std::deque<scc> root_; // Stack of SCC roots. 109 std::vector<int> h_(n, 0); 110 // Map of visited states. Values > 0 designate maximal SCC. 111 // Values < 0 number states that are part of incomplete SCCs being 112 // completed. 0 denotes non-visited states. 113 114 int num_ = 0; // Number of visited nodes, negated. 115 116 struct stack_item { 117 unsigned src; 118 unsigned out_edge; 119 unsigned univ_pos; 120 }; 121 // DFS stack. Holds (STATE, TRANS, UNIV_POS) pairs where TRANS is 122 // the current outgoing transition of STATE, and UNIV_POS is used 123 // when the transition is universal to iterate over all possible 124 // destinations. 125 std::stack<stack_item> todo_; 126 auto& gr = aut->get_graph(); 127 128 std::deque<unsigned> init_states; 129 std::vector<bool> init_seen(n, false); 130 auto push_init = [&](unsigned s) 131 { 132 if (h_[s] != 0 || init_seen[s]) 133 return; 134 init_seen[s] = true; 135 init_states.push_back(s); 136 }; 137 138 bool track_states = !!(options & scc_info_options::TRACK_STATES); 139 bool track_succs = !!(options & scc_info_options::TRACK_SUCCS); 140 auto backtrack = [&](unsigned curr) 141 { 142 if (root_.back().index == h_[curr]) 143 { 144 unsigned num = node_.size(); 145 acc_cond::mark_t acc = root_.back().acc; 146 acc_cond::mark_t common = root_.back().common; 147 bool triv = root_.back().trivial; 148 node_.emplace_back(acc, common, triv); 149 150 auto& succ = node_.back().succ_; 151 unsigned np1 = num + 1; 152 auto s = live.rbegin(); 153 do 154 { 155 sccof_[*s] = num; 156 h_[*s] = np1; 157 158 // Gather all successor SCCs 159 if (track_succs) 160 for (auto& t: aut->out(*s)) 161 if (SPOT_LIKELY(t.cond != bddfalse)) 162 for (unsigned d: aut->univ_dests(t)) 163 { 164 unsigned n = sccof_[d]; 165 if (n == num || n == -1U) 166 continue; 167 // If edges are cut, we are not able to 168 // maintain proper successor information. 169 if (filter_) 170 switch (filter_(t, d, filter_data_)) 171 { 172 case edge_filter_choice::keep: 173 break; 174 case edge_filter_choice::ignore: 175 case edge_filter_choice::cut: 176 continue; 177 } 178 succ.emplace_back(n); 179 } 180 } 181 while (*s++ != curr); 182 183 if (track_states) 184 { 185 auto& nbs = node_.back().states_; 186 nbs.insert(nbs.end(), s.base(), live.end()); 187 } 188 189 node_.back().one_state_ = curr; 190 live.erase(s.base(), live.end()); 191 192 if (track_succs) 193 { 194 std::sort(succ.begin(), succ.end()); 195 succ.erase(std::unique(succ.begin(), succ.end()), succ.end()); 196 } 197 198 bool accept = !triv && root_.back().accepting; 199 node_.back().accepting_ = accept; 200 if (accept) 201 one_acc_scc_ = num; 202 bool reject = triv || 203 aut->acc().maybe_accepting(acc, common).is_false(); 204 node_.back().rejecting_ = reject; 205 root_.pop_back(); 206 } 207 }; 208 209 // Setup depth-first search from the initial state. But we may 210 // have a conjunction of initial state in alternating automata. 211 if (initial_state_ == -1U) 212 initial_state_ = aut->get_init_state_number(); 213 for (unsigned init: aut->univ_dests(initial_state_)) 214 push_init(init); 215 216 while (!init_states.empty()) 217 { 218 unsigned init = init_states.front(); 219 init_states.pop_front(); 220 int spi = h_[init]; 221 if (spi > 0) 222 continue; 223 assert(spi == 0); 224 h_[init] = --num_; 225 root_.emplace_back(num_, acc_cond::mark_t({})); 226 todo_.emplace(stack_item{init, gr.state_storage(init).succ, 0}); 227 live.emplace_back(init); 228 229 while (!todo_.empty()) 230 { 231 // We are looking at the next successor in SUCC. 232 unsigned tr_succ = todo_.top().out_edge; 233 234 // If there is no more successor, backtrack. 235 if (!tr_succ) 236 { 237 // We have explored all successors of state CURR. 238 unsigned curr = todo_.top().src; 239 240 // Backtrack TODO_. 241 todo_.pop(); 242 243 // When backtracking the root of an SCC, we must also 244 // remove that SCC from the ARC/ROOT stacks. We must 245 // discard from H all reachable states from this SCC. 246 assert(!root_.empty()); 247 backtrack(curr); 248 continue; 249 } 250 251 // We have a successor to look at. 252 // Fetch the values we are interested in... 253 auto& e = gr.edge_storage(tr_succ); 254 255 // Skip false edges. 256 if (SPOT_UNLIKELY(e.cond == bddfalse)) 257 { 258 todo_.top().out_edge = e.next_succ; 259 continue; 260 } 261 262 unsigned dest = e.dst; 263 if ((int) dest < 0) 264 { 265 // Iterate over all destinations of a universal edge. 266 if (todo_.top().univ_pos == 0) 267 todo_.top().univ_pos = ~dest + 1; 268 const auto& v = gr.dests_vector(); 269 dest = v[todo_.top().univ_pos]; 270 // Last universal destination? 271 if (~e.dst + v[~e.dst] == todo_.top().univ_pos) 272 { 273 todo_.top().out_edge = e.next_succ; 274 todo_.top().univ_pos = 0; 275 } 276 else 277 { 278 ++todo_.top().univ_pos; 279 } 280 } 281 else 282 { 283 todo_.top().out_edge = e.next_succ; 284 } 285 286 // Do we really want to look at this 287 if (filter_) 288 switch (filter_(e, dest, filter_data_)) 289 { 290 case edge_filter_choice::keep: 291 break; 292 case edge_filter_choice::ignore: 293 continue; 294 case edge_filter_choice::cut: 295 push_init(e.dst); 296 continue; 297 } 298 299 acc_cond::mark_t acc = e.acc; 300 301 // Are we going to a new state? 302 int spi = h_[dest]; 303 if (spi == 0) 304 { 305 // Yes. Number it, stack it, and register its successors 306 // for later processing. 307 h_[dest] = --num_; 308 root_.emplace_back(num_, acc); 309 todo_.emplace(stack_item{dest, gr.state_storage(dest).succ, 0}); 310 live.emplace_back(dest); 311 continue; 312 } 313 314 // We already know the state. 315 316 // Have we reached a maximal SCC? 317 if (spi > 0) 318 continue; 319 320 // Now this is the most interesting case. We have reached a 321 // state S1 which is already part of a non-dead SCC. Any such 322 // non-dead SCC has necessarily been crossed by our path to 323 // this state: there is a state S2 in our path which belongs 324 // to this SCC too. We are going to merge all states between 325 // this S1 and S2 into this SCC.. 326 // 327 // This merge is easy to do because the order of the SCC in 328 // ROOT is descending: we just have to merge all SCCs from the 329 // top of ROOT that have an index lesser than the one of 330 // the SCC of S2 (called the "threshold"). 331 int threshold = spi; 332 bool is_accepting = false; 333 // If this is a self-loop, check its acceptance alone. 334 if (dest == e.src) 335 is_accepting = aut->acc().accepting(acc); 336 337 acc_cond::mark_t common = acc; 338 assert(!root_.empty()); 339 while (threshold > root_.back().index) 340 { 341 acc |= root_.back().acc; 342 acc_cond::mark_t in_acc = root_.back().in_acc; 343 acc |= in_acc; 344 common &= root_.back().common; 345 common &= in_acc; 346 is_accepting |= root_.back().accepting; 347 root_.pop_back(); 348 assert(!root_.empty()); 349 } 350 351 // Note that we do not always have 352 // threshold == root_.back().index 353 // after this loop, the SCC whose index is threshold might have 354 // been merged with a higher SCC. 355 356 root_.back().acc |= acc; 357 root_.back().common &= common; 358 root_.back().accepting |= is_accepting 359 || aut->acc().accepting(root_.back().acc); 360 // This SCC is no longer trivial. 361 root_.back().trivial = false; 362 363 if (root_.back().accepting 364 && !!(options & scc_info_options::STOP_ON_ACC)) 365 { 366 while (!todo_.empty()) 367 { 368 unsigned curr = todo_.top().src; 369 todo_.pop(); 370 backtrack(curr); 371 } 372 return; 373 } 374 } 375 } 376 if (track_succs && !(options & scc_info_options::STOP_ON_ACC)) 377 determine_usefulness(); 378 } 379 determine_usefulness()380 void scc_info::determine_usefulness() 381 { 382 // An SCC is useful if it is not rejecting or it has a successor 383 // SCC that is useful. 384 unsigned scccount = scc_count(); 385 for (unsigned i = 0; i < scccount; ++i) 386 { 387 if (!node_[i].is_rejecting()) 388 { 389 node_[i].useful_ = true; 390 continue; 391 } 392 node_[i].useful_ = false; 393 for (unsigned j: node_[i].succ()) 394 if (node_[j].is_useful()) 395 { 396 node_[i].useful_ = true; 397 break; 398 } 399 } 400 } 401 marks_of(unsigned scc) const402 std::set<acc_cond::mark_t> scc_info::marks_of(unsigned scc) const 403 { 404 std::set<acc_cond::mark_t> res; 405 for (auto& t: inner_edges_of(scc)) 406 res.insert(t.acc); 407 return res; 408 } 409 marks() const410 std::vector<std::set<acc_cond::mark_t>> scc_info::marks() const 411 { 412 unsigned n = aut_->num_states(); 413 std::vector<std::set<acc_cond::mark_t>> result(scc_count()); 414 415 for (unsigned src = 0; src < n; ++src) 416 { 417 unsigned src_scc = scc_of(src); 418 if (src_scc == -1U || is_rejecting_scc(src_scc)) 419 continue; 420 auto& s = result[src_scc]; 421 for (auto& t: aut_->out(src)) 422 { 423 if (scc_of(t.dst) != src_scc || SPOT_UNLIKELY(t.cond == bddfalse)) 424 continue; 425 s.insert(t.acc); 426 } 427 } 428 return result; 429 } 430 weak_sccs() const431 std::vector<bool> scc_info::weak_sccs() const 432 { 433 unsigned n = scc_count(); 434 std::vector<bool> result(scc_count()); 435 auto acc = marks(); 436 for (unsigned s = 0; s < n; ++s) 437 result[s] = is_rejecting_scc(s) || acc[s].size() == 1; 438 return result; 439 } 440 scc_ap_support(unsigned scc) const441 bdd scc_info::scc_ap_support(unsigned scc) const 442 { 443 bdd support = bddtrue; 444 for (auto& t: edges_of(scc)) 445 support &= bdd_support(t.cond); 446 return support; 447 } 448 check_scc_emptiness(unsigned n) const449 bool scc_info::check_scc_emptiness(unsigned n) const 450 { 451 if (SPOT_UNLIKELY(!aut_->is_existential())) 452 throw std::runtime_error("scc_info::check_scc_emptiness() " 453 "does not support alternating automata"); 454 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) 455 report_need_track_states(); 456 return generic_emptiness_check_for_scc(*this, n); 457 } 458 determine_unknown_acceptance()459 void scc_info::determine_unknown_acceptance() 460 { 461 unsigned s = scc_count(); 462 bool changed = false; 463 // iterate over SCCs in topological order 464 do 465 { 466 --s; 467 if (!is_rejecting_scc(s) && !is_accepting_scc(s)) 468 { 469 if (SPOT_UNLIKELY(!aut_->is_existential())) 470 throw std::runtime_error( 471 "scc_info::determine_unknown_acceptance() " 472 "does not support alternating automata"); 473 auto& node = node_[s]; 474 if (check_scc_emptiness(s)) 475 { 476 node.rejecting_ = true; 477 } 478 else 479 { 480 node.accepting_ = true; 481 if (one_acc_scc_ < 0) 482 one_acc_scc_ = s; 483 } 484 changed = true; 485 } 486 } 487 while (s); 488 if (changed && !!(options_ & scc_info_options::TRACK_SUCCS)) 489 determine_usefulness(); 490 } 491 492 // A reimplementation of spot::bfs_steps for explicit automata. 493 // bool filter(const twa_graph::edge_storage_t&) returns true if the 494 // transition has to be filtered out. 495 // bool match(const twa_graph::edge_storage_t&) returns true if the BFS 496 // has to stop after this transition. 497 // Returns the destination of the matched transition, or -1 if no match has 498 // been found. 499 template <typename edge_filter_type, 500 typename step_matcher_type> explicit_bfs_steps(const const_twa_graph_ptr aut,unsigned start,twa_run::steps & steps,edge_filter_type filter,step_matcher_type match)501 static int explicit_bfs_steps(const const_twa_graph_ptr aut, unsigned start, 502 twa_run::steps& steps, 503 edge_filter_type filter, 504 step_matcher_type match) 505 { 506 auto& gr = aut->get_graph(); 507 // The backlink of each state is the index of the edge that 508 // discovered it in the BFS, so BACKLINKS effectively describes a 509 // tree rooted at START. 510 std::vector<unsigned> backlinks(aut->num_states(), 0); 511 std::deque<unsigned> bfs_queue; 512 bfs_queue.emplace_back(start); 513 while (!bfs_queue.empty()) 514 { 515 unsigned src = bfs_queue.front(); 516 bfs_queue.pop_front(); 517 for (auto& t: aut->out(src)) 518 { 519 if (SPOT_UNLIKELY(t.cond == bddfalse) || filter(t)) 520 continue; 521 522 if (match(t)) 523 { 524 // Build the path from START to T.DST by following the 525 // backlinks, starting at the end. 526 twa_run::steps path; 527 path.emplace_front(aut->state_from_number(t.src), 528 t.cond, t.acc); 529 unsigned src = t.src; 530 while (src != start) 531 { 532 unsigned bl_num = backlinks[src]; 533 assert(bl_num); 534 auto& bl_edge = gr.edge_storage(bl_num); 535 src = bl_edge.src; 536 path.emplace_front(aut->state_from_number(src), 537 bl_edge.cond, bl_edge.acc); 538 } 539 steps.splice(steps.end(), path); 540 return t.dst; 541 } 542 543 if (!backlinks[t.dst]) 544 { 545 backlinks[t.dst] = aut->edge_number(t); 546 bfs_queue.push_back(t.dst); 547 } 548 } 549 } 550 return -1; 551 } 552 get_accepting_run(unsigned scc,twa_run_ptr r) const553 void scc_info::get_accepting_run(unsigned scc, twa_run_ptr r) const 554 { 555 const scc_info::scc_node& node = node_[scc]; 556 if (!node.is_accepting()) 557 throw std::runtime_error("scc_info::get_accepting_cycle needs to be " 558 "called on an accepting scc"); 559 if (SPOT_UNLIKELY(!(options_ & scc_info_options::STOP_ON_ACC))) 560 report_need_stop_on_acc(); 561 562 unsigned init = aut_->get_init_state_number(); 563 564 // The accepting cycle should honor any edge filter we have. 565 auto filter = [this](const twa_graph::edge_storage_t& t) 566 { 567 if (!filter_) 568 return false; 569 // Filter out ignored and cut transitions. 570 return filter_(t, t.dst, filter_data_) 571 != edge_filter_choice::keep; 572 }; 573 574 // The SCC exploration has a small optimization that can flag SCCs 575 // as accepting if they contain accepting self-loops, even if the 576 // SCC itself has some Fin acceptance to check. So we have to 577 // deal with this situation before we look for the more complex 578 // case of satisfying the condition with a larger cycle. We do 579 // this first, because it's good to return a small cycle if we 580 // can. 581 const acc_cond& acccond = aut_->acc(); 582 unsigned num_states = aut_->num_states(); 583 for (unsigned s = 0; s < num_states; ++s) 584 { 585 // We scan the entire state to find those in the SCC, because 586 // we cannot rely on TRACK_STATES being on. 587 if (scc_of(s) != scc) 588 continue; 589 for (auto& e: aut_->out(s)) 590 if (e.src == e.dst && SPOT_LIKELY(e.cond != bddfalse) 591 && !filter(e) && acccond.accepting(e.acc)) 592 { 593 // We have found an accepting self-loop. That's the cycle 594 // part of our accepting run. 595 r->cycle.clear(); 596 r->cycle.emplace_front(aut_->state_from_number(e.src), 597 e.cond, e.acc); 598 // Add the prefix. 599 r->prefix.clear(); 600 if (e.src != init) 601 explicit_bfs_steps(aut_, init, r->prefix, 602 [](const twa_graph::edge_storage_t&) 603 { 604 return false; // Do not filter. 605 }, 606 [&](const twa_graph::edge_storage_t& t) 607 { 608 return t.dst == e.src; 609 }); 610 return; 611 } 612 } 613 614 // Prefix search 615 616 r->prefix.clear(); 617 int substart; 618 if (scc_of(init) == scc) 619 { 620 // The initial state is in the target SCC: no prefix needed. 621 substart = init; 622 } 623 else 624 { 625 substart = explicit_bfs_steps(aut_, init, r->prefix, 626 [](const twa_graph::edge_storage_t&) 627 { 628 return false; // Do not filter. 629 }, 630 [&](const twa_graph::edge_storage_t& t) 631 { 632 // Match any state in the SCC. 633 return scc_of(t.dst) == scc; 634 }); 635 } 636 637 const unsigned start = (unsigned)substart; 638 639 // Cycle search 640 acc_cond actual_cond = acccond.restrict_to(node.acc_marks()) 641 .force_inf(node.acc_marks()); 642 assert(!actual_cond.uses_fin_acceptance()); 643 assert(!actual_cond.is_f()); 644 acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks()); 645 r->cycle.clear(); 646 647 do 648 { 649 substart = explicit_bfs_steps(aut_, substart, r->cycle, 650 [&](const twa_graph::edge_storage_t& t) 651 { 652 // Stay in the specified SCC. 653 return scc_of(t.dst) != scc || filter(t); 654 }, 655 [&](const twa_graph::edge_storage_t& t) 656 { 657 if (!acc_to_see) // We have seen all the marks, go back to start. 658 return t.dst == start; 659 if (t.acc & acc_to_see) 660 { 661 acc_to_see -= t.acc; 662 return true; 663 } 664 return false; 665 }); 666 assert(0 <= substart); 667 } 668 while (acc_to_see || (unsigned)substart != start); 669 } 670 671 std::ostream& dump_scc_info_dot(std::ostream & out,const_twa_graph_ptr aut,scc_info * sccinfo)672 dump_scc_info_dot(std::ostream& out, 673 const_twa_graph_ptr aut, scc_info* sccinfo) 674 { 675 scc_info* m = sccinfo ? sccinfo : new scc_info(aut); 676 677 out << "digraph G {\n i [label=\"\", style=invis, height=0]\n"; 678 int start = m->scc_of(aut->get_init_state_number()); 679 out << " i -> " << start << std::endl; 680 681 std::vector<bool> seen(m->scc_count()); 682 seen[start] = true; 683 684 std::queue<int> q; 685 q.push(start); 686 while (!q.empty()) 687 { 688 int state = q.front(); 689 q.pop(); 690 691 out << " " << state << " [shape=box," 692 << (aut->acc().accepting(m->acc_sets_of(state)) ? 693 "style=bold," : "") 694 << "label=\"" << state; 695 { 696 size_t n = m->states_of(state).size(); 697 out << " (" << n << " state"; 698 if (n > 1) 699 out << 's'; 700 out << ')'; 701 } 702 out << "\"]\n"; 703 704 for (unsigned dest: m->succ(state)) 705 { 706 out << " " << state << " -> " << dest << '\n'; 707 if (seen[dest]) 708 continue; 709 seen[dest] = true; 710 q.push(dest); 711 } 712 } 713 714 out << "}\n"; 715 if (!sccinfo) 716 delete m; 717 return out; 718 } 719 720 std::vector<twa_graph_ptr> split_on_sets(unsigned scc,acc_cond::mark_t sets,bool preserve_names) const721 scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets, 722 bool preserve_names) const 723 { 724 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) 725 report_need_track_states(); 726 std::vector<twa_graph_ptr> res; 727 728 std::vector<bool> seen(aut_->num_states(), false); 729 std::vector<bool> cur(aut_->num_states(), false); 730 731 for (unsigned init: states_of(scc)) 732 { 733 if (seen[init]) 734 continue; 735 cur.assign(aut_->num_states(), false); 736 737 auto copy = make_twa_graph(aut_->get_dict()); 738 copy->copy_ap_of(aut_); 739 copy->copy_acceptance_of(aut_); 740 copy->prop_state_acc(aut_->prop_state_acc()); 741 transform_accessible(aut_, copy, [&](unsigned src, 742 bdd& cond, 743 acc_cond::mark_t& m, 744 unsigned dst) 745 { 746 cur[src] = seen[src] = true; 747 if (filter_) 748 { 749 twa_graph::edge_storage_t e; 750 e.cond = cond; 751 e.acc = m; 752 e.src = src; 753 e.dst = dst; 754 if (filter_(e, dst, filter_data_) 755 != edge_filter_choice::keep) 756 { 757 cond = bddfalse; 758 return; 759 } 760 } 761 if (scc_of(dst) != scc 762 || (m & sets) 763 || (seen[dst] && !cur[dst])) 764 { 765 cond = bddfalse; 766 return; 767 } 768 }, 769 init); 770 if (copy->num_edges()) 771 { 772 if (preserve_names) 773 copy->copy_state_names_from(aut_); 774 res.push_back(copy); 775 } 776 } 777 return res; 778 } 779 780 void states_on_acc_cycle_of_rec(unsigned scc,acc_cond::mark_t all_fin,acc_cond::mark_t all_inf,unsigned nb_pairs,std::vector<acc_cond::rs_pair> & pairs,std::vector<unsigned> & res,std::vector<unsigned> & old) const781 scc_info::states_on_acc_cycle_of_rec(unsigned scc, 782 acc_cond::mark_t all_fin, 783 acc_cond::mark_t all_inf, 784 unsigned nb_pairs, 785 std::vector<acc_cond::rs_pair>& pairs, 786 std::vector<unsigned>& res, 787 std::vector<unsigned>& old) const 788 { 789 if (is_useful_scc(scc) && !is_rejecting_scc(scc)) 790 { 791 acc_cond::mark_t all_acc = acc_sets_of(scc); 792 acc_cond::mark_t fin = all_fin & all_acc; 793 acc_cond::mark_t inf = all_inf & all_acc; 794 795 // Get all Fin acceptance set that appears in the SCC and does not have 796 // their corresponding Inf appearing in the SCC. 797 acc_cond::mark_t m = {}; 798 if (fin) 799 for (unsigned p = 0; p < nb_pairs; ++p) 800 if (fin & pairs[p].fin && !(inf & pairs[p].inf)) 801 m |= pairs[p].fin; 802 803 if (m) 804 for (const twa_graph_ptr& aut : split_on_sets(scc, m)) 805 { 806 auto orig_sts = aut->get_named_prop 807 <std::vector<unsigned>>("original-states"); 808 809 // Update mapping of state numbers between the current automaton 810 // and the starting one. 811 for (unsigned i = 0; i < orig_sts->size(); ++i) 812 (*orig_sts)[i] = old[(*orig_sts)[i]]; 813 814 scc_info si_tmp(aut, scc_info_options::TRACK_STATES 815 | scc_info_options::TRACK_SUCCS); 816 unsigned scccount_tmp = si_tmp.scc_count(); 817 for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp) 818 si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf, 819 nb_pairs, pairs, res, 820 *orig_sts); 821 } 822 823 else // Accepting cycle found. 824 for (unsigned s : states_of(scc)) 825 res.push_back(old[s]); 826 } 827 } 828 829 std::vector<unsigned> states_on_acc_cycle_of(unsigned scc) const830 scc_info::states_on_acc_cycle_of(unsigned scc) const 831 { 832 std::vector<acc_cond::rs_pair> pairs; 833 if (!aut_->acc().is_streett_like(pairs)) 834 throw std::runtime_error("states_on_acc_cycle_of only works with " 835 "Streett-like acceptance condition"); 836 unsigned nb_pairs = pairs.size(); 837 838 std::vector<unsigned> res; 839 if (is_useful_scc(scc) && !is_rejecting_scc(scc)) 840 { 841 std::vector<unsigned> old; 842 unsigned nb_states = aut_->num_states(); 843 for (unsigned i = 0; i < nb_states; ++i) 844 old.push_back(i); 845 846 acc_cond::mark_t all_fin = {}; 847 acc_cond::mark_t all_inf = {}; 848 std::tie(all_inf, all_fin) = aut_->get_acceptance().used_inf_fin_sets(); 849 850 states_on_acc_cycle_of_rec(scc, all_fin, all_inf, nb_pairs, pairs, res, 851 old); 852 } 853 854 return res; 855 } 856 857 scc_info::edge_filter_choice filter_mark_(const twa_graph::edge_storage_t & e,unsigned,void * data)858 scc_and_mark_filter::filter_mark_ 859 (const twa_graph::edge_storage_t& e, unsigned, void* data) 860 { 861 auto& d = *reinterpret_cast<scc_and_mark_filter*>(data); 862 if (d.cut_sets_ & e.acc) 863 return scc_info::edge_filter_choice::cut; 864 return scc_info::edge_filter_choice::keep; 865 } 866 867 scc_info::edge_filter_choice filter_scc_and_mark_(const twa_graph::edge_storage_t & e,unsigned dst,void * data)868 scc_and_mark_filter::filter_scc_and_mark_ 869 (const twa_graph::edge_storage_t& e, unsigned dst, void* data) 870 { 871 auto& d = *reinterpret_cast<scc_and_mark_filter*>(data); 872 if (d.lower_si_->scc_of(dst) != d.lower_scc_) 873 return scc_info::edge_filter_choice::ignore; 874 if (d.cut_sets_ & e.acc) 875 return scc_info::edge_filter_choice::cut; 876 return scc_info::edge_filter_choice::keep; 877 } 878 879 scc_info::edge_filter_choice filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t & e,unsigned,void * data)880 scc_and_mark_filter::filter_scc_and_mark_and_edges_ 881 (const twa_graph::edge_storage_t& e, unsigned, void* data) 882 { 883 auto& d = *reinterpret_cast<scc_and_mark_filter*>(data); 884 auto* si = d.lower_si_; 885 if (si->scc_of(e.dst) != si->scc_of(e.src)) 886 return edge_filter_choice::ignore; 887 if (auto f = si->get_filter()) 888 if (auto choice = f(e, e.dst, si->get_filter_data()); 889 choice != edge_filter_choice::keep) 890 return choice; 891 if (!(*d.keep_).get(d.aut_->edge_number(e)) || (d.cut_sets_ & e.acc)) 892 return edge_filter_choice::cut; 893 return edge_filter_choice::keep; 894 } 895 } 896