From 3d5b5be69346eba3f5b2f85cf3de0aaa98c13e11 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Tue, 12 Dec 2017 18:57:39 +0100 Subject: [PATCH] cobuchi: nsa_to_nca() takes is_useful_scc() into account * spot/twaalgos/cobuchi.cc: Add scc_info_options::TRACK_SUCCS in nsa_to_nca(). * spot/twaalgos/sccinfo.cc: Add scc_info_options::TRACK_SUCCS and is_useful_scc() in states_on_acc_cycle_of(). --- spot/twaalgos/cobuchi.cc | 3 ++- spot/twaalgos/sccinfo.cc | 7 ++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 3f1536cdc..2fc3cd3c6 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -219,7 +219,8 @@ namespace spot named_states_(named_states), res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), res_map_(res_->get_named_prop("product-states")), - si_(scc_info(res_, scc_info_options::TRACK_STATES)), + si_(scc_info(res_, scc_info_options::TRACK_STATES + | scc_info_options::TRACK_SUCCS)), nb_states_(res_->num_states()), was_rabin_(was_rabin), orig_num_st_(orig_num_st) diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 0056e8508..567b9f1bd 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -559,7 +559,7 @@ namespace spot std::vector& res, std::vector& old) const { - if (!is_rejecting_scc(scc)) + if (is_useful_scc(scc) && !is_rejecting_scc(scc)) { acc_cond::mark_t all_acc = acc_sets_of(scc); acc_cond::mark_t fin = all_fin & all_acc; @@ -584,7 +584,8 @@ namespace spot for (unsigned i = 0; i < orig_sts->size(); ++i) (*orig_sts)[i] = old[(*orig_sts)[i]]; - scc_info si_tmp(aut, scc_info_options::TRACK_STATES); + scc_info si_tmp(aut, scc_info_options::TRACK_STATES + | scc_info_options::TRACK_SUCCS); unsigned scccount_tmp = si_tmp.scc_count(); for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp) si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf, @@ -608,7 +609,7 @@ namespace spot unsigned nb_pairs = pairs.size(); std::vector res; - if (!is_rejecting_scc(scc)) + if (is_useful_scc(scc) && !is_rejecting_scc(scc)) { std::vector old; unsigned nb_states = aut_->num_states();