1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2012-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/postproc.hh> 22 #include <spot/twaalgos/minimize.hh> 23 #include <spot/twaalgos/simulation.hh> 24 #include <spot/twaalgos/sccfilter.hh> 25 #include <spot/twaalgos/degen.hh> 26 #include <spot/twaalgos/stripacc.hh> 27 #include <cstdlib> 28 #include <spot/misc/optionmap.hh> 29 #include <spot/twaalgos/powerset.hh> 30 #include <spot/twaalgos/isdet.hh> 31 #include <spot/twaalgos/dtbasat.hh> 32 #include <spot/twaalgos/dtwasat.hh> 33 #include <spot/twaalgos/complete.hh> 34 #include <spot/twaalgos/totgba.hh> 35 #include <spot/twaalgos/sbacc.hh> 36 #include <spot/twaalgos/sepsets.hh> 37 #include <spot/twaalgos/determinize.hh> 38 #include <spot/twaalgos/alternation.hh> 39 #include <spot/twaalgos/parity.hh> 40 #include <spot/twaalgos/cobuchi.hh> 41 #include <spot/twaalgos/cleanacc.hh> 42 #include <spot/twaalgos/toparity.hh> 43 44 namespace spot 45 { 46 namespace 47 { 48 static twa_graph_ptr ensure_ba(twa_graph_ptr & a)49 ensure_ba(twa_graph_ptr& a) 50 { 51 if (a->acc().is_t()) 52 { 53 auto m = a->set_buchi(); 54 for (auto& t: a->edges()) 55 t.acc = m; 56 } 57 return a; 58 } 59 } 60 postprocessor(const option_map * opt)61 postprocessor::postprocessor(const option_map* opt) 62 { 63 if (opt) 64 { 65 degen_order_ = opt->get("degen-order", 0); 66 degen_reset_ = opt->get("degen-reset", 1); 67 degen_cache_ = opt->get("degen-lcache", 1); 68 degen_lskip_ = opt->get("degen-lskip", 1); 69 degen_lowinit_ = opt->get("degen-lowinit", 0); 70 degen_remscc_ = opt->get("degen-remscc", 1); 71 det_scc_ = opt->get("det-scc", 1); 72 det_simul_ = opt->get("det-simul", -1); 73 det_stutter_ = opt->get("det-stutter", 1); 74 det_max_states_ = opt->get("det-max-states", -1); 75 det_max_edges_ = opt->get("det-max-edges", -1); 76 simul_ = opt->get("simul", -1); 77 simul_method_ = opt->get("simul-method", -1); 78 dpa_simul_ = opt->get("dpa-simul", -1); 79 dba_simul_ = opt->get("dba-simul", -1); 80 scc_filter_ = opt->get("scc-filter", -1); 81 ba_simul_ = opt->get("ba-simul", -1); 82 tba_determinisation_ = opt->get("tba-det", 0); 83 sat_minimize_ = opt->get("sat-minimize", 0); 84 sat_incr_steps_ = opt->get("sat-incr-steps", -2); // -2 or any num < -1 85 sat_langmap_ = opt->get("sat-langmap", 0); 86 sat_acc_ = opt->get("sat-acc", 0); 87 sat_states_ = opt->get("sat-states", 0); 88 state_based_ = opt->get("state-based", 0); 89 wdba_minimize_ = opt->get("wdba-minimize", -1); 90 gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); 91 simul_max_ = opt->get("simul-max", 4096); 92 wdba_det_max_ = opt->get("wdba-det-max", 4096); 93 simul_trans_pruning_ = opt->get("simul-trans-pruning", 512); 94 95 if (sat_acc_ && sat_minimize_ == 0) 96 sat_minimize_ = 1; // Dicho. 97 if (sat_states_ && sat_minimize_ == 0) 98 sat_minimize_ = 1; 99 if (sat_minimize_) 100 { 101 tba_determinisation_ = 1; 102 if (sat_acc_ <= 0) 103 sat_acc_ = -1; 104 if (sat_states_ <= 0) 105 sat_states_ = -1; 106 } 107 108 // Set default param value if not provided and used. 109 if (sat_minimize_ == 2 && sat_incr_steps_ < 0) // Assume algorithm. 110 sat_incr_steps_ = 6; 111 else if (sat_minimize_ == 3 && sat_incr_steps_ < -1) // Incr algorithm. 112 sat_incr_steps_ = 2; 113 } 114 } 115 116 twa_graph_ptr do_simul(const twa_graph_ptr & a,int opt) const117 postprocessor::do_simul(const twa_graph_ptr& a, int opt) const 118 { 119 if (opt == 0) 120 return a; 121 if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states()) 122 return a; 123 124 static unsigned sim = [&]() 125 { 126 if (simul_method_ != -1) 127 return simul_method_; 128 129 char* s = getenv("SPOT_SIMULATION_REDUCTION"); 130 return s ? *s - '0' : 0; 131 }(); 132 133 if (sim == 2) 134 opt += 3; 135 136 // FIXME: simulation-based reduction now have work-arounds for 137 // non-separated sets, so we can probably try them. 138 if (!has_separate_sets(a)) 139 return a; 140 switch (opt) 141 { 142 case 1: 143 return simulation(a, simul_trans_pruning_); 144 case 2: 145 return cosimulation(a, simul_trans_pruning_); 146 case 3: 147 return iterated_simulations(a, simul_trans_pruning_); 148 case 4: 149 return reduce_direct_sim(a); 150 case 5: 151 return reduce_direct_cosim(a); 152 case 6: 153 return reduce_iterated(a); 154 default: 155 return iterated_simulations(a, simul_trans_pruning_); 156 } 157 } 158 159 twa_graph_ptr do_sba_simul(const twa_graph_ptr & a,int opt) const160 postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt) const 161 { 162 if (ba_simul_ <= 0) 163 return a; 164 if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states()) 165 return a; 166 switch (opt) 167 { 168 case 0: 169 return a; 170 case 1: 171 return simulation_sba(a, simul_trans_pruning_); 172 case 2: 173 return cosimulation_sba(a, simul_trans_pruning_); 174 case 3: 175 default: 176 return iterated_simulations_sba(a, simul_trans_pruning_); 177 } 178 } 179 180 twa_graph_ptr choose_degen(const twa_graph_ptr & a) const181 postprocessor::choose_degen(const twa_graph_ptr& a) const 182 { 183 if (state_based_) 184 return do_degen(a); 185 else 186 return do_degen_tba(a); 187 } 188 189 twa_graph_ptr do_degen(const twa_graph_ptr & a) const190 postprocessor::do_degen(const twa_graph_ptr& a) const 191 { 192 auto d = degeneralize(a, 193 degen_reset_, degen_order_, 194 degen_cache_, degen_lskip_, 195 degen_lowinit_, degen_remscc_); 196 return do_sba_simul(d, ba_simul_); 197 } 198 199 twa_graph_ptr do_degen_tba(const twa_graph_ptr & a) const200 postprocessor::do_degen_tba(const twa_graph_ptr& a) const 201 { 202 return degeneralize_tba(a, 203 degen_reset_, degen_order_, 204 degen_cache_, degen_lskip_, 205 degen_lowinit_, degen_remscc_); 206 } 207 208 twa_graph_ptr do_scc_filter(const twa_graph_ptr & a,bool arg) const209 postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const 210 { 211 if (scc_filter_ == 0) 212 return a; 213 if (state_based_ && a->prop_state_acc().is_true()) 214 return scc_filter_states(a, arg); 215 else 216 return scc_filter(a, arg); 217 } 218 219 twa_graph_ptr do_scc_filter(const twa_graph_ptr & a) const220 postprocessor::do_scc_filter(const twa_graph_ptr& a) const 221 { 222 return do_scc_filter(a, scc_filter_ > 1); 223 } 224 225 #define PREF_ (pref_ & (Small | Deterministic)) 226 #define COMP_ (pref_ & Complete) 227 #define SBACC_ (pref_ & SBAcc) 228 #define COLORED_ (pref_ & Colored) 229 230 231 twa_graph_ptr finalize(twa_graph_ptr tmp) const232 postprocessor::finalize(twa_graph_ptr tmp) const 233 { 234 if (PREF_ != Any && level_ != Low) 235 tmp->remove_unused_ap(); 236 if (COMP_) 237 tmp = complete(tmp); 238 bool want_parity = type_ & Parity; 239 if (want_parity && tmp->acc().is_generalized_buchi()) 240 tmp = choose_degen(tmp); 241 assert(!!SBACC_ == state_based_); 242 if (state_based_) 243 tmp = sbacc(tmp); 244 if (type_ == Buchi) 245 tmp = ensure_ba(tmp); 246 if (want_parity) 247 { 248 reduce_parity_here(tmp, COLORED_); 249 parity_kind kind = parity_kind_any; 250 parity_style style = parity_style_any; 251 if ((type_ & ParityMin) == ParityMin) 252 kind = parity_kind_min; 253 else if ((type_ & ParityMax) == ParityMax) 254 kind = parity_kind_max; 255 if ((type_ & ParityOdd) == ParityOdd) 256 style = parity_style_odd; 257 else if ((type_ & ParityEven) == ParityEven) 258 style = parity_style_even; 259 change_parity_here(tmp, kind, style); 260 } 261 return tmp; 262 } 263 264 twa_graph_ptr run(twa_graph_ptr a,formula f)265 postprocessor::run(twa_graph_ptr a, formula f) 266 { 267 if (simul_ < 0) 268 simul_ = (level_ == Low) ? 1 : 3; 269 if (ba_simul_ < 0) 270 ba_simul_ = (level_ == High) ? simul_ : 0; 271 int detaut_simul_default = (level_ != Low && simul_ > 0) ? 1 : 0; 272 if (dpa_simul_ < 0) 273 dpa_simul_ = detaut_simul_default; 274 if (dba_simul_ < 0) 275 dba_simul_ = detaut_simul_default; 276 if (det_simul_ < 0) 277 det_simul_ = simul_ > 0; 278 if (scc_filter_ < 0) 279 scc_filter_ = 1; 280 if (type_ == BA) 281 { 282 pref_ |= SBAcc; 283 type_ = Buchi; 284 } 285 if (SBACC_) 286 state_based_ = true; 287 else if (state_based_) 288 pref_ |= SBAcc; 289 290 bool via_gba = 291 (type_ == Buchi) || (type_ == GeneralizedBuchi) || (type_ == Monitor); 292 bool want_parity = type_ & Parity; 293 if (COLORED_ && !want_parity) 294 throw std::runtime_error("postprocessor: the Colored setting only works " 295 "for parity acceptance"); 296 297 298 299 // Attempt to simplify the acceptance condition, unless this is a 300 // parity automaton and we want parity acceptance in the output. 301 auto simplify_acc = [&](twa_graph_ptr in) 302 { 303 if (PREF_ == Any && level_ == Low) 304 return in; 305 bool isparity = in->acc().is_parity(); 306 if (isparity && in->is_existential() 307 && (type_ == Generic || want_parity)) 308 { 309 auto res = reduce_parity(in); 310 if (want_parity || gen_reduce_parity_) 311 return res; 312 // In case type_ == Generic and gen_reduce_parity_ == 0, 313 // we only return the result of reduce_parity() if it can 314 // lower the number of colors. Otherwise, 315 // simplify_acceptance() will not do better and we return 316 // the input unchanged. The reason for not always using 317 // the output of reduce_parity() is that is may hide 318 // symmetries between automata, as in issue #402. 319 return (res->num_sets() < in->num_sets()) ? res : in; 320 } 321 if (want_parity && isparity) 322 return cleanup_parity(in); 323 if (level_ == High) 324 return simplify_acceptance(in); 325 else 326 return cleanup_acceptance(in); 327 }; 328 a = simplify_acc(a); 329 330 if (!a->is_existential() && 331 // We will probably have to revisit this condition later. 332 // Currently, the intent is that postprocessor should never 333 // return an alternating automaton, unless it is called with 334 // its laxest settings. 335 !(type_ == Generic && PREF_ == Any && level_ == Low)) 336 a = remove_alternation(a); 337 338 if ((via_gba || (want_parity && !a->acc().is_parity())) 339 && !a->acc().is_generalized_buchi()) 340 { 341 // If we do want a parity automaton, we can use to_parity(). 342 // However (1) degeneralization is better if the input is 343 // GBA, and (2) if we want a deterministic parity automaton and the 344 // input is not deterministic, that is useless here. We need 345 // to determinize it first, and our deterministization 346 // function only deal with TGBA as input. 347 if (want_parity && (PREF_ != Deterministic || is_deterministic(a))) 348 { 349 a = to_parity(a); 350 } 351 else 352 { 353 a = to_generalized_buchi(a); 354 if (PREF_ == Any && level_ == Low) 355 a = do_scc_filter(a, true); 356 } 357 } 358 359 if (PREF_ == Any && level_ == Low 360 && (type_ == Generic 361 || type_ == GeneralizedBuchi 362 || (type_ == Buchi && a->acc().is_buchi()) 363 || (type_ == Monitor && a->num_sets() == 0) 364 || (want_parity && a->acc().is_parity()) 365 || (type_ == CoBuchi && a->acc().is_co_buchi()))) 366 return finalize(a); 367 368 int original_acc = a->num_sets(); 369 370 // Remove useless SCCs. 371 if (type_ == Monitor) 372 // Do not bother about acceptance conditions, they will be 373 // ignored. 374 a = scc_filter_states(a); 375 else 376 a = do_scc_filter(a, (PREF_ == Any)); 377 378 if (type_ == Monitor) 379 { 380 if (PREF_ == Deterministic) 381 a = minimize_monitor(a); 382 else 383 strip_acceptance_here(a); 384 385 if (PREF_ != Any) 386 { 387 if (PREF_ != Deterministic) 388 a = do_simul(a, simul_); 389 390 // For Small,High we return the smallest between the output of 391 // the simulation, and that of the deterministic minimization. 392 // Prefer the deterministic automaton in case of equality. 393 if (PREF_ == Small && level_ == High && simul_) 394 { 395 auto m = minimize_monitor(a); 396 if (m->num_states() <= a->num_states()) 397 a = m; 398 } 399 } 400 return finalize(a); 401 } 402 403 if (PREF_ == Any) 404 { 405 if (type_ == Buchi) 406 a = choose_degen(a); 407 else if (type_ == CoBuchi) 408 a = to_nca(a); 409 return finalize(a); 410 } 411 412 bool dba_is_wdba = false; 413 bool dba_is_minimal = false; 414 twa_graph_ptr dba = nullptr; 415 twa_graph_ptr sim = nullptr; 416 417 output_aborter aborter_ 418 (det_max_states_ >= 0 ? static_cast<unsigned>(det_max_states_) : -1U, 419 det_max_edges_ >= 0 ? static_cast<unsigned>(det_max_edges_) : -1U); 420 output_aborter* aborter = 421 (det_max_states_ >= 0 || det_max_edges_ >= 0) ? &aborter_ : nullptr; 422 423 int wdba_minimize = wdba_minimize_; 424 if (wdba_minimize == -1) 425 { 426 if (level_ == High) 427 wdba_minimize = 1; 428 else if (level_ == Medium || PREF_ == Deterministic) 429 wdba_minimize = 2; 430 else 431 wdba_minimize = 0; 432 } 433 if (wdba_minimize == 2) 434 wdba_minimize = minimize_obligation_garanteed_to_work(a, f); 435 if (wdba_minimize) 436 { 437 bool reject_bigger = (PREF_ == Small) && (level_ <= Medium); 438 output_aborter* ab = aborter; 439 output_aborter wdba_aborter(wdba_det_max_ > 0 ? 440 (static_cast<unsigned>(wdba_det_max_) 441 + a->num_states()) : -1U); 442 if (!ab && PREF_ != Deterministic) 443 ab = &wdba_aborter; 444 dba = minimize_obligation(a, f, nullptr, reject_bigger, ab); 445 446 if (dba 447 && dba->prop_inherently_weak().is_true() 448 && dba->prop_universal().is_true()) 449 { 450 // The WDBA is a BA, so no degeneralization is required. 451 // We just need to add an acceptance set if there is none. 452 dba_is_minimal = dba_is_wdba = true; 453 if (type_ == Buchi) 454 ensure_ba(dba); 455 } 456 else 457 { 458 // Minimization failed. 459 dba = nullptr; 460 } 461 } 462 463 // Run a simulation when wdba failed (or was not run), or 464 // at hard levels if we want a small output. 465 if (!dba || (level_ == High && PREF_ == Small)) 466 { 467 if ((state_based_ && a->prop_state_acc().is_true()) 468 && !tba_determinisation_ 469 && (type_ != Buchi || a->acc().is_buchi())) 470 { 471 sim = do_sba_simul(a, ba_simul_); 472 } 473 else 474 { 475 sim = do_simul(a, simul_); 476 // Degeneralize the result of the simulation if needed. 477 // No need to do that if tba_determinisation_ will be used. 478 if (type_ == Buchi && !tba_determinisation_) 479 sim = choose_degen(sim); 480 else if (want_parity && !sim->acc().is_parity()) 481 sim = do_degen_tba(sim); 482 else if (state_based_ && !tba_determinisation_) 483 sim = sbacc(sim); 484 } 485 } 486 487 // If WDBA failed, but the simulation returned a deterministic 488 // automaton, use it as dba. 489 assert(dba || sim); 490 if (!dba && is_deterministic(sim)) 491 { 492 std::swap(sim, dba); 493 // We postponed degeneralization above in case we would need 494 // to perform TBA-determinisation, but now it is clear 495 // that we won't perform it. So do degeneralize. 496 if (tba_determinisation_) 497 { 498 if (type_ == Buchi) 499 dba = choose_degen(dba); 500 else if (state_based_) 501 dba = sbacc(dba); 502 assert(is_deterministic(dba)); 503 } 504 } 505 506 // If we don't have a DBA, attempt tba-determinization if requested. 507 if (tba_determinisation_ && !dba) 508 { 509 twa_graph_ptr tmpd = nullptr; 510 if (PREF_ == Deterministic 511 && f 512 && f.is_syntactic_recurrence() 513 && sim->num_sets() > 1) 514 tmpd = degeneralize_tba(sim); 515 516 auto in = tmpd ? tmpd : sim; 517 518 // These thresholds are arbitrary. 519 // 520 // For producing Small automata, we assume that a 521 // deterministic automaton that is twice the size of the 522 // original will never get reduced to a smaller one. We also 523 // do not want more than 2^13 cycles in an SCC. 524 // 525 // For Deterministic automata, we accept automata that 526 // are 8 times bigger, with no more that 2^15 cycle per SCC. 527 // The cycle threshold is the most important limit here. You 528 // may up it if you want to try producing larger automata. 529 auto tmp = 530 tba_determinize_check(in, 531 (PREF_ == Small) ? 2 : 8, 532 1 << ((PREF_ == Small) ? 13 : 15), 533 f); 534 if (tmp && tmp != in) 535 { 536 // There is no point in running the reverse simulation on 537 // a deterministic automaton, since all prefixes are 538 // unique. 539 dba = do_simul(tmp, dba_simul_); 540 } 541 if (dba && PREF_ == Deterministic) 542 { 543 // disregard the result of the simulation. 544 sim = nullptr; 545 } 546 else 547 { 548 // degeneralize sim, because we did not do it earlier 549 if (type_ == Buchi) 550 sim = choose_degen(sim); 551 } 552 } 553 554 if ((PREF_ == Deterministic && (type_ == Generic || want_parity)) && !dba) 555 { 556 bool det_simul = det_simul_; 557 auto tba = to_generalized_buchi(sim); 558 if (simul_max_ > 0 559 && static_cast<unsigned>(simul_max_) < tba->num_states()) 560 det_simul = false; 561 dba = tgba_determinize(tba, 562 false, det_scc_, det_simul, det_stutter_, 563 aborter, simul_trans_pruning_); 564 // Setting det-max-states or det-max-edges may cause tgba_determinize 565 // to fail. 566 567 if (dba) 568 { 569 dba = do_simul(simplify_acc(dba), dpa_simul_); 570 sim = nullptr; 571 } 572 } 573 574 // Now dba contains either the result of WDBA-minimization (in 575 // that case dba_is_wdba=true), or some deterministic automaton 576 // that is either the result of the simulation or of the 577 // TBA-determinization (dba_is_wdba=false in both cases), or a 578 // parity automaton coming from tgba_determinize(). If the dba is 579 // a WDBA, we do not have to run SAT-minimization. A negative 580 // value in sat_minimize_ can force its use for debugging. 581 if (sat_minimize_ && dba && (!dba_is_wdba || sat_minimize_ < 0)) 582 { 583 if (type_ == Generic) 584 throw std::runtime_error 585 ("postproc() not yet updated to mix sat-minimize and Generic"); 586 unsigned target_acc; 587 if (type_ == Buchi) 588 target_acc = 1; 589 else if (sat_acc_ != -1) 590 target_acc = sat_acc_; 591 else 592 // Take the number of acceptance sets from the input 593 // automaton, not from dba, because dba often has been 594 // degeneralized by tba_determinize_check(). Make sure it 595 // is at least 1. 596 target_acc = original_acc > 0 ? original_acc : 1; 597 598 const_twa_graph_ptr in = nullptr; 599 if (target_acc == 1) 600 { 601 // If we are seeking a minimal DBA with unknown number of 602 // states, then we should start from the degeneralized, 603 // because the input TBA might be smaller. 604 if (state_based_) 605 in = degeneralize(dba); 606 else 607 in = degeneralize_tba(dba); 608 } 609 else 610 { 611 in = dba; 612 } 613 614 twa_graph_ptr res = complete(in); 615 if (target_acc == 1) 616 { 617 if (sat_states_ != -1) 618 res = dtba_sat_synthetize(res, sat_states_, state_based_); 619 else if (sat_minimize_ == 1) 620 res = dtba_sat_minimize_dichotomy 621 (res, state_based_, sat_langmap_); 622 else if (sat_minimize_ == 2) 623 res = dtba_sat_minimize_assume(res, state_based_, -1, 624 sat_incr_steps_); 625 else if (sat_minimize_ == 3) 626 res = dtba_sat_minimize_incr(res, state_based_, -1, 627 sat_incr_steps_); 628 else // if (sat_minimize == 4 || sat_minimize == -1) 629 res = dtba_sat_minimize(res, state_based_); 630 } 631 else 632 { 633 if (sat_states_ != -1) 634 res = dtwa_sat_synthetize 635 (res, target_acc, 636 acc_cond::acc_code::generalized_buchi(target_acc), 637 sat_states_, state_based_); 638 else if (sat_minimize_ == 1) 639 res = dtwa_sat_minimize_dichotomy 640 (res, target_acc, 641 acc_cond::acc_code::generalized_buchi(target_acc), 642 state_based_, sat_langmap_); 643 else if (sat_minimize_ == 2) 644 res = dtwa_sat_minimize_assume 645 (res, target_acc, 646 acc_cond::acc_code::generalized_buchi(target_acc), 647 state_based_, -1, false, sat_incr_steps_); 648 else if (sat_minimize_ == 3) 649 res = dtwa_sat_minimize_incr 650 (res, target_acc, 651 acc_cond::acc_code::generalized_buchi(target_acc), 652 state_based_, -1, false, sat_incr_steps_); 653 else // if (sat_minimize_ == 4 || sat_minimize_ == -1) 654 res = dtwa_sat_minimize 655 (res, target_acc, 656 acc_cond::acc_code::generalized_buchi(target_acc), 657 state_based_); 658 } 659 660 if (res) 661 { 662 dba = do_scc_filter(res, true); 663 dba_is_minimal = true; 664 } 665 } 666 667 // Degeneralize the dba resulting from tba-determinization or 668 // sat-minimization (which is a TBA) if requested and needed. 669 if (dba && !dba_is_wdba && type_ == Buchi && state_based_ 670 && !(dba_is_minimal && dba->num_sets() == 1)) 671 dba = degeneralize(dba); 672 673 if (dba && sim) 674 { 675 if (dba->num_states() > sim->num_states()) 676 dba = nullptr; 677 else 678 sim = nullptr; 679 } 680 681 if (level_ == High && scc_filter_ != 0) 682 { 683 if (dba) 684 { 685 // Do that even for WDBA, to remove marks from transitions 686 // leaving trivial SCCs. 687 dba = do_scc_filter(dba, true); 688 assert(!sim); 689 } 690 else if (sim) 691 { 692 sim = do_scc_filter(sim, true); 693 assert(!dba); 694 } 695 } 696 697 sim = dba ? dba : sim; 698 699 if (type_ == CoBuchi) 700 { 701 unsigned ns = sim->num_states(); 702 if (PREF_ == Deterministic) 703 sim = to_dca(sim); 704 else 705 sim = to_nca(sim); 706 707 // if the input of to_dca/to_nca was weak, the number of 708 // states has not changed, and running simulation is useless. 709 if (level_ != Low && ns < sim->num_states()) 710 sim = do_simul(sim, simul_); 711 } 712 713 return finalize(sim); 714 } 715 } 716