1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017-2018, 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/cobuchi.hh> 22 23 #include <spot/misc/bddlt.hh> 24 #include <spot/misc/bitvect.hh> 25 #include <spot/misc/hash.hh> 26 #include <spot/twa/acc.hh> 27 #include <spot/twa/bddprint.hh> 28 #include <spot/twa/twagraph.hh> 29 #include <spot/twaalgos/powerset.hh> 30 #include <spot/twaalgos/product.hh> 31 #include <spot/twaalgos/sccinfo.hh> 32 #include <spot/twaalgos/totgba.hh> 33 #include <spot/twaalgos/isdet.hh> 34 #include <spot/twaalgos/strength.hh> 35 #include <spot/twaalgos/sbacc.hh> // For issue #317 36 #include <stack> 37 #include <unordered_map> 38 39 #define TRACE 0 40 #if TRACE 41 #define trace std::cerr 42 #else 43 #define trace while (0) std::cout 44 #endif 45 46 namespace spot 47 { 48 namespace 49 { 50 typedef std::pair<unsigned, unsigned> pair_state_nca; 51 52 // Helper function that returns the called 'augmented subset construction' 53 // of the given automaton, i.e. the product of the automaton with its 54 // powerset construction. 55 // 56 // 'aut_power' is the automaton that will be used for the powerset 57 // construction and 'aut_prod' is the one that will be used for the 58 // product. They may be confusing in the sense that why the same automaton 59 // is not used for the product and the powerset construction. Actually, 60 // when dealing with an automaton A with Rabin acceptance, it is firstly 61 // converted into an automaton B with Streett-like acceptance. The powerset 62 // construction of B happens to be isomorphic with the powerset construction 63 // of A. Therefore, you would like to use A (which is smaller than B) for 64 // the powerset construction and B for the product. 65 static 66 twa_graph_ptr aug_subset_cons(const const_twa_graph_ptr & aut_prod,const const_twa_graph_ptr & aut_power,bool named_states,struct power_map & pmap)67 aug_subset_cons(const const_twa_graph_ptr& aut_prod, 68 const const_twa_graph_ptr& aut_power, 69 bool named_states, 70 struct power_map& pmap) 71 { 72 twa_graph_ptr res = nullptr; 73 74 if (is_deterministic(aut_prod)) 75 { 76 res = make_twa_graph(aut_prod, twa::prop_set::all()); 77 auto v = new product_states; 78 res->set_named_prop("product-states", v); 79 for (unsigned s = 0; s < aut_power->num_states(); ++s) 80 v->emplace_back(s, s); 81 for (unsigned s = 0; s < aut_power->num_states(); ++s) 82 pmap.map_.push_back({s}); 83 } 84 else 85 { 86 res = product(aut_prod, tgba_powerset(aut_power, pmap)); 87 } 88 89 if (named_states) 90 { 91 const product_states* res_map = res->get_named_prop 92 <product_states>("product-states"); 93 94 auto v = new std::vector<std::string>; 95 res->set_named_prop("state-names", v); 96 97 auto get_st_name = 98 [&](const pair_state_nca& x) 99 { 100 std::stringstream os; 101 os << x.first << ",{"; 102 bool not_first = false; 103 for (auto& a : pmap.states_of(x.second)) 104 { 105 if (not_first) 106 os << ','; 107 else 108 not_first = true; 109 os << a; 110 } 111 os << '}'; 112 return os.str(); 113 }; 114 115 unsigned num_states = res->num_states(); 116 for (unsigned i = 0; i < num_states; ++i) 117 v->emplace_back(get_st_name((*res_map)[i])); 118 } 119 return res; 120 } 121 122 class nsa_to_nca_converter final 123 { 124 protected: 125 struct power_map pmap_; // Sets of sts (powerset cons.). 126 127 const_twa_graph_ptr aut_; // The given automaton. 128 bool state_based_; // Is it state based? 129 std::vector<acc_cond::rs_pair> pairs_; // All pairs of the acc. cond. 130 unsigned nb_pairs_; // Nb pair in the acc. cond. 131 bool named_states_; // Name states for display? 132 twa_graph_ptr res_; // The augmented subset const. 133 product_states* res_map_; // States of the aug. sub. cons. 134 scc_info si_; // SCC information. 135 unsigned nb_states_; // Number of states. 136 unsigned was_dnf_; // Was it DNF before Streett? 137 std::vector<unsigned>* orig_states_; // Match old Rabin st. from new. 138 std::vector<unsigned>* orig_clauses_; // Associated Rabin clauses. 139 unsigned orig_num_st_; // Rabin original nb states. 140 141 // Keep information of states that are wanted to be seen infinitely 142 // often (cf Header). save_inf_nca_st(unsigned s,vect_nca_info * nca_info)143 void save_inf_nca_st(unsigned s, vect_nca_info* nca_info) 144 { 145 const pair_state_nca& st = (*res_map_)[s]; 146 auto bv = make_bitvect(orig_num_st_); 147 for (unsigned state : pmap_.states_of(st.second)) 148 bv->set(state); 149 unsigned clause = 0; 150 unsigned state = st.first; 151 if (was_dnf_) 152 { 153 clause = (*orig_clauses_)[state]; 154 assert((int)clause >= 0); 155 state = (*orig_states_)[state]; 156 assert((int)state >= 0); 157 } 158 nca_info->push_back(new nca_st_info(clause, state, bv)); 159 } 160 161 // Helper function that marks states that we want to see finitely often 162 // and save some information about states that we want to see infinitely 163 // often (cf Header). set_marks_using(std::vector<bool> & nca_is_inf_state,vect_nca_info * nca_info)164 void set_marks_using(std::vector<bool>& nca_is_inf_state, 165 vect_nca_info* nca_info) 166 { 167 for (unsigned s = 0; s < nb_states_; ++s) 168 { 169 unsigned src_scc = si_.scc_of(s); 170 if (nca_is_inf_state[s]) 171 { 172 for (auto& e : res_->out(s)) 173 e.acc = {}; 174 175 if (nca_info) 176 save_inf_nca_st(s, nca_info); 177 } 178 else 179 { 180 for (auto& e : res_->out(s)) 181 { 182 if (si_.scc_of(e.dst) == src_scc || state_based_) 183 e.acc = acc_cond::mark_t({0}); 184 else 185 e.acc = {}; 186 } 187 } 188 } 189 } 190 191 public: 192 nsa_to_nca_converter(const const_twa_graph_ptr ref_prod,const const_twa_graph_ptr ref_power,std::vector<acc_cond::rs_pair> & pairs,bool named_states=false,bool was_dnf=false,unsigned orig_num_st=0)193 nsa_to_nca_converter(const const_twa_graph_ptr ref_prod, 194 const const_twa_graph_ptr ref_power, 195 std::vector<acc_cond::rs_pair>& pairs, 196 bool named_states = false, 197 bool was_dnf = false, 198 unsigned orig_num_st = 0) 199 : aut_(ref_prod), 200 state_based_(aut_->prop_state_acc().is_true()), 201 pairs_(pairs), 202 nb_pairs_(pairs.size()), 203 named_states_(named_states), 204 res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), 205 res_map_(res_->get_named_prop<product_states>("product-states")), 206 si_(res_, (scc_info_options::TRACK_STATES 207 | scc_info_options::TRACK_SUCCS)), 208 nb_states_(res_->num_states()), 209 was_dnf_(was_dnf), 210 orig_num_st_(orig_num_st ? orig_num_st : ref_prod->num_states()) 211 { 212 if (was_dnf) 213 { 214 orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>> 215 ("original-states"); 216 orig_clauses_ = ref_prod->get_named_prop<std::vector<unsigned>> 217 ("original-clauses"); 218 } 219 } 220 ~nsa_to_nca_converter()221 ~nsa_to_nca_converter() 222 {} 223 run(vect_nca_info * nca_info)224 twa_graph_ptr run(vect_nca_info* nca_info) 225 { 226 std::vector<bool> nca_is_inf_state; // Accepting or rejecting sts. 227 nca_is_inf_state.resize(nb_states_, false); 228 229 // Iterate over all SCCs and check for accepting states. A state 's' 230 // is accepting if there is a cycle containing 's' that visits 231 // finitely often all acceptance sets marked as Fin or infinitely 232 // often acceptance sets marked by Inf. 233 unsigned nb_scc = si_.scc_count(); 234 for (unsigned scc = 0; scc < nb_scc; ++scc) 235 for (unsigned st : si_.states_on_acc_cycle_of(scc)) 236 nca_is_inf_state[st] = true; 237 238 set_marks_using(nca_is_inf_state, nca_info); 239 240 res_->prop_state_acc(state_based_); 241 res_->set_co_buchi(); 242 res_->merge_edges(); 243 return res_; 244 } 245 }; 246 } 247 248 249 twa_graph_ptr nsa_to_nca(const_twa_graph_ptr ref,bool named_states,vect_nca_info * nca_info)250 nsa_to_nca(const_twa_graph_ptr ref, 251 bool named_states, 252 vect_nca_info* nca_info) 253 { 254 if (ref->acc().is_parity()) 255 ref = to_generalized_streett(ref); 256 257 std::vector<acc_cond::rs_pair> pairs; 258 if (!ref->acc().is_streett_like(pairs)) 259 throw std::runtime_error("nsa_to_nca() only works with Streett-like or " 260 "Parity acceptance condition"); 261 262 // FIXME: At the moment this algorithm does not support 263 // transition-based acceptance. See issue #317. Once that is 264 // fixed we may remove the next line. 265 ref = sbacc(std::const_pointer_cast<twa_graph>(ref)); 266 267 nsa_to_nca_converter nca_converter(ref, ref, pairs, named_states, false); 268 return nca_converter.run(nca_info); 269 } 270 271 272 twa_graph_ptr dnf_to_nca(const_twa_graph_ptr ref,bool named_states,vect_nca_info * nca_info)273 dnf_to_nca(const_twa_graph_ptr ref, bool named_states, 274 vect_nca_info* nca_info) 275 { 276 const acc_cond::acc_code& code = ref->get_acceptance(); 277 if (!code.is_dnf()) 278 throw std::runtime_error("dnf_to_nca() only works with DNF acceptance " 279 "condition"); 280 281 // FIXME: At the moment this algorithm does not support 282 // transition-based acceptance. See issue #317. Once that is 283 // fixed we may remove the next line. 284 ref = sbacc(std::const_pointer_cast<twa_graph>(ref)); 285 286 auto streett_aut = spot::dnf_to_streett(ref, true); 287 288 std::vector<acc_cond::rs_pair> pairs; 289 if (!streett_aut->acc().is_streett_like(pairs)) 290 throw std::runtime_error("dnf_to_nca() could not convert the original " 291 "automaton into an intermediate Streett-like automaton"); 292 293 nsa_to_nca_converter nca_converter(streett_aut, 294 ref, 295 pairs, 296 named_states, 297 true, 298 ref->num_states()); 299 return nca_converter.run(nca_info); 300 } 301 302 namespace 303 { 304 twa_graph_ptr weak_to_cobuchi(const const_twa_graph_ptr & aut)305 weak_to_cobuchi(const const_twa_graph_ptr& aut) 306 { 307 trival iw = aut->prop_inherently_weak(); 308 if (iw.is_false()) 309 return nullptr; 310 scc_info si(aut); 311 if (iw.is_maybe() && !is_weak_automaton(aut, &si)) 312 return nullptr; 313 auto res = make_twa_graph(aut->get_dict()); 314 res->copy_ap_of(aut); 315 res->prop_copy(aut, twa::prop_set::all()); 316 res->new_states(aut->num_states()); 317 si.determine_unknown_acceptance(); 318 unsigned ns = si.scc_count(); 319 for (unsigned s = 0; s < ns; ++s) 320 { 321 acc_cond::mark_t m = {}; 322 if (si.is_rejecting_scc(s)) 323 m = acc_cond::mark_t{0}; 324 else 325 assert(si.is_accepting_scc(s)); 326 327 for (auto& e: si.edges_of(s)) 328 res->new_edge(e.src, e.dst, e.cond, m); 329 } 330 res->set_co_buchi(); 331 res->set_init_state(aut->get_init_state_number()); 332 res->prop_weak(true); 333 res->prop_state_acc(true); 334 return res; 335 } 336 } 337 338 twa_graph_ptr to_nca(const_twa_graph_ptr aut,bool named_states)339 to_nca(const_twa_graph_ptr aut, bool named_states) 340 { 341 if (aut->acc().is_co_buchi()) 342 return make_twa_graph(aut, twa::prop_set::all()); 343 344 if (auto weak = weak_to_cobuchi(aut)) 345 return weak; 346 347 const acc_cond::acc_code& code = aut->get_acceptance(); 348 349 std::vector<acc_cond::rs_pair> pairs; 350 if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) 351 return nsa_to_nca(aut, named_states); 352 else if (code.is_dnf()) 353 return dnf_to_nca(aut, named_states); 354 355 auto tmp = make_twa_graph(aut, twa::prop_set::all()); 356 tmp->set_acceptance(aut->acc().num_sets(), 357 aut->get_acceptance().to_dnf()); 358 return to_nca(tmp, named_states); 359 } 360 361 namespace 362 { 363 struct mp_hash 364 { 365 size_t operator ()spot::__anonf458a0080411::mp_hash366 operator()(std::pair<unsigned, const bitvect_array*> bv) const noexcept 367 { 368 size_t res = 0; 369 size_t size = bv.second->size(); 370 for (unsigned i = 0; i < size; ++i) 371 res = wang32_hash(res ^ wang32_hash(bv.second->at(i).hash())); 372 res = wang32_hash(res ^ bv.first); 373 return res; 374 } 375 }; 376 377 struct mp_equal 378 { operator ()spot::__anonf458a0080411::mp_equal379 bool operator()(std::pair<unsigned, const bitvect_array*> bvl, 380 std::pair<unsigned, const bitvect_array*> bvr) const 381 { 382 if (bvl.first != bvr.first) 383 return false; 384 size_t size = bvl.second->size(); 385 for (unsigned i = 0; i < size; ++i) 386 if (bvl.second->at(i) != bvr.second->at(i)) 387 return false; 388 return true; 389 } 390 }; 391 392 typedef std::unordered_map 393 <std::pair<unsigned, const bitvect_array*>, unsigned, mp_hash, mp_equal> 394 dca_st_mapping; 395 class dca_breakpoint_cons final 396 { 397 protected: 398 const_twa_graph_ptr aut_; // The given automaton. 399 vect_nca_info* nca_info_; // Info (cf Header). 400 unsigned nb_copy_; // != 0 if was Rabin. 401 bdd ap_; // All AP. 402 std::vector<bdd> num2bdd_; // Get bdd from AP num. 403 std::map<bdd, unsigned, bdd_less_than> bdd2num_; // Get AP num from bdd. 404 405 // Each state is characterized by a bitvect_array of 2 bitvects: 406 // bv1 -> the set of original states that it represents 407 // bv2 -> a set of marked states (~) 408 // To do so, we keep a correspondance between a state number and its 409 // bitvect representation. 410 dca_st_mapping bv_to_num_; 411 std::vector<std::pair<unsigned, bitvect_array*>> num_2_bv_; 412 413 // Next states to process. 414 std::stack<std::pair<std::pair<unsigned, bitvect_array*>, unsigned>> 415 todo_; 416 // All allocated bitvect that must be freed at the end. 417 std::vector<const bitvect_array*> toclean_; 418 419 public: dca_breakpoint_cons(const const_twa_graph_ptr aut,vect_nca_info * nca_info,unsigned nb_copy)420 dca_breakpoint_cons(const const_twa_graph_ptr aut, 421 vect_nca_info* nca_info, 422 unsigned nb_copy) 423 : aut_(aut), 424 nca_info_(nca_info), 425 nb_copy_(nb_copy), 426 ap_(aut->ap_vars()) 427 { 428 // Get all bdds. 429 unsigned i = 0; 430 for (bdd one: minterms_of(bddtrue, ap_)) 431 { 432 num2bdd_.push_back(one); 433 bdd2num_[one] = i++; 434 } 435 } 436 ~dca_breakpoint_cons()437 ~dca_breakpoint_cons() 438 { 439 for (auto p : *nca_info_) 440 delete p; 441 } 442 run(bool named_states)443 twa_graph_ptr run(bool named_states) 444 { 445 unsigned ns = aut_->num_states(); 446 unsigned nc = num2bdd_.size(); 447 448 // Fill bv_aut_trans_ which is a bitvect of all possible transitions 449 // of each state for each letter. 450 auto bv_aut_trans_ = std::unique_ptr<bitvect_array>( 451 make_bitvect_array(ns, ns * nc)); 452 for (unsigned src = 0; src < ns; ++src) 453 { 454 size_t base = src * nc; 455 for (auto& t: aut_->out(src)) 456 for (bdd one: minterms_of(t.cond, ap_)) 457 bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst); 458 } 459 trace << "All_states:\n" << *bv_aut_trans_ << '\n'; 460 461 twa_graph_ptr res = make_twa_graph(aut_->get_dict()); 462 res->copy_ap_of(aut_); 463 res->set_co_buchi(); 464 465 // Rename states of resulting automata (for display purposes). 466 std::vector<std::string>* state_name = nullptr; 467 if (named_states) 468 { 469 state_name = new std::vector<std::string>(); 470 res->set_named_prop("state-names", state_name); 471 } 472 473 // Function used to add a new state. A new state number is associated 474 // to the state if has never been added before, otherwise the old 475 // state number is returned. 476 auto new_state = [&](std::pair<unsigned, bitvect_array*> bv_st) 477 -> unsigned 478 { 479 auto p = bv_to_num_.emplace(bv_st, 0); 480 if (!p.second) 481 return p.first->second; 482 483 p.first->second = res->new_state(); 484 todo_.emplace(bv_st, p.first->second); 485 assert(num_2_bv_.size() == p.first->second); 486 num_2_bv_.push_back(bv_st); 487 488 // For display purposes only. 489 if (named_states) 490 { 491 assert(p.first->second == state_name->size()); 492 std::ostringstream os; 493 bool not_first = false; 494 os << '{'; 495 for (unsigned s = 0; s < ns; ++s) 496 { 497 if (bv_st.second->at(1).get(s)) 498 { 499 if (not_first) 500 os << ','; 501 else 502 not_first = true; 503 os << '~'; 504 } 505 if (bv_st.second->at(0).get(s)) 506 os << s; 507 } 508 os << '|' << bv_st.first << '}'; 509 state_name->emplace_back(os.str()); 510 } 511 return p.first->second; 512 }; 513 514 // Set init state 515 auto bv_init = make_bitvect_array(ns, 2); 516 toclean_.push_back(bv_init); 517 bv_init->at(0).set(aut_->get_init_state_number()); 518 res->set_init_state(new_state(std::make_pair(0, bv_init))); 519 520 // Processing loop 521 while (!todo_.empty()) 522 { 523 auto top = todo_.top(); 524 todo_.pop(); 525 526 // Bitvect array of all possible moves for each letter. 527 auto bv_trans = make_bitvect_array(ns, nc); 528 for (unsigned s = 0; s < ns; ++s) 529 if (top.first.second->at(0).get(s)) 530 for (unsigned l = 0; l < nc; ++l) 531 bv_trans->at(l) |= bv_aut_trans_->at(s * nc + l); 532 toclean_.push_back(bv_trans); 533 534 // Bitvect array of all possible moves for each state marked 535 // for each letter. If no state is marked (breakpoint const.), 536 // nothing is set. 537 bool marked = !top.first.second->at(1).is_fully_clear(); 538 auto bv_trans_mark = make_bitvect_array(ns, nc); 539 if (marked) 540 for (unsigned s = 0; s < ns; ++s) 541 if (top.first.second->at(1).get(s)) 542 for (unsigned l = 0; l < nc; ++l) 543 bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l); 544 toclean_.push_back(bv_trans_mark); 545 546 trace << "src:" << top.second; 547 if (named_states) 548 trace << ' ' << (*state_name)[top.second]; 549 trace << '\n'; 550 551 for (unsigned l = 0; l < nc; ++l) 552 { 553 trace << "l: " 554 << bdd_format_formula(aut_->get_dict(), num2bdd_[l]) 555 << '\n'; 556 557 auto bv_res = make_bitvect_array(ns, 2); 558 toclean_.push_back(bv_res); 559 bv_res->at(0) |= bv_trans->at(l); 560 // If this state has not any outgoing edges. 561 if (bv_res->at(0).is_fully_clear()) 562 continue; 563 564 // Set states that must be marked. 565 for (const auto& p : *nca_info_) 566 { 567 if (p->clause_num != top.first.first) 568 continue; 569 570 if (*p->all_dst == bv_res->at(0)) 571 if ((marked && bv_trans_mark->at(l).get(p->state_num)) 572 || (!marked && bv_res->at(0).get(p->state_num))) 573 bv_res->at(1).set(p->state_num); 574 } 575 576 unsigned i = bv_res->at(1).is_fully_clear() ? 577 (top.first.first + 1) % (nb_copy_ + 1) 578 : top.first.first; 579 580 trace << "dest\n" << *bv_res << "i: " << i << '\n'; 581 res->new_edge(top.second, 582 new_state(std::make_pair(i, bv_res)), 583 num2bdd_[l]); 584 } 585 trace << '\n'; 586 } 587 588 // Set rejecting states. 589 scc_info si(res); 590 bool state_based = (bool)aut_->prop_state_acc(); 591 unsigned res_size = res->num_states(); 592 for (unsigned s = 0; s < res_size; ++s) 593 { 594 unsigned s_scc = si.scc_of(s); 595 if (num_2_bv_[s].second->at(1).is_fully_clear()) 596 for (auto& edge : res->out(s)) 597 if (state_based || si.scc_of(edge.dst) == s_scc) 598 edge.acc = acc_cond::mark_t({0}); 599 } 600 601 // Delete all bitvect arrays allocated by this method (run). 602 for (auto v: toclean_) 603 delete v; 604 605 res->merge_edges(); 606 return res; 607 } 608 }; 609 } 610 611 612 twa_graph_ptr nsa_to_dca(const_twa_graph_ptr aut,bool named_states)613 nsa_to_dca(const_twa_graph_ptr aut, bool named_states) 614 { 615 trace << "NSA_to_dca\n"; 616 std::vector<acc_cond::rs_pair> pairs; 617 if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity()) 618 throw std::runtime_error("nsa_to_dca() only works with Streett-like or " 619 "Parity acceptance condition"); 620 621 // FIXME: At the moment this algorithm does not support 622 // transition-based acceptance. See issue #317. Once that is 623 // fixed we may remove the next line. 624 aut = sbacc(std::const_pointer_cast<twa_graph>(aut)); 625 626 // Get states that must be visited infinitely often in NCA. 627 vect_nca_info nca_info; 628 nsa_to_nca(aut, named_states, &nca_info); 629 630 #if TRACE 631 trace << "PRINTING INFO\n"; 632 for (unsigned i = 0; i < nca_info.size(); ++i) 633 trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num 634 << ',' << *nca_info[i]->all_dst << ">\n"; 635 #endif 636 637 dca_breakpoint_cons dca(aut, &nca_info, 0); 638 return dca.run(named_states); 639 } 640 641 642 twa_graph_ptr dnf_to_dca(const_twa_graph_ptr aut,bool named_states)643 dnf_to_dca(const_twa_graph_ptr aut, bool named_states) 644 { 645 trace << "DNF_to_dca\n"; 646 const acc_cond::acc_code& code = aut->get_acceptance(); 647 if (!code.is_dnf()) 648 throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like " 649 "included) acceptance condition"); 650 651 // FIXME: At the moment this algorithm does not support 652 // transition-based acceptance. See issue #317. Once that is 653 // fixed we may remove the next line. 654 aut = sbacc(std::const_pointer_cast<twa_graph>(aut)); 655 656 // Get states that must be visited infinitely often in NCA. 657 vect_nca_info nca_info; 658 dnf_to_nca(aut, false, &nca_info); 659 660 #if TRACE 661 trace << "PRINTING INFO\n"; 662 for (unsigned i = 0; i < nca_info.size(); ++i) 663 trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num 664 << ',' << *nca_info[i]->all_dst << ">\n"; 665 #endif 666 667 unsigned nb_copy = 0; 668 for (const auto& p : nca_info) 669 if (nb_copy < p->clause_num) 670 nb_copy = p->clause_num; 671 672 dca_breakpoint_cons dca(aut, &nca_info, nb_copy); 673 return dca.run(named_states); 674 } 675 676 677 twa_graph_ptr to_dca(const_twa_graph_ptr aut,bool named_states)678 to_dca(const_twa_graph_ptr aut, bool named_states) 679 { 680 if (is_deterministic(aut)) 681 { 682 if (aut->acc().is_co_buchi()) 683 return make_twa_graph(aut, twa::prop_set::all()); 684 if (auto weak = weak_to_cobuchi(aut)) 685 return weak; 686 } 687 688 const acc_cond::acc_code& code = aut->get_acceptance(); 689 690 std::vector<acc_cond::rs_pair> pairs; 691 if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) 692 return nsa_to_dca(aut, named_states); 693 else if (code.is_dnf()) 694 return dnf_to_dca(aut, named_states); 695 696 auto tmp = make_twa_graph(aut, twa::prop_set::all()); 697 tmp->set_acceptance(aut->acc().num_sets(), 698 aut->get_acceptance().to_dnf()); 699 return to_nca(tmp, named_states); 700 } 701 } 702