diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index eef15b2c4..c9bd4ddb4 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -36,7 +36,8 @@ namespace spot aut_->get_dict()->unregister_all_my_variables(this); } - bdd outedge_combiner::operator()(unsigned st, const std::vector& dst_filter) + bdd outedge_combiner::operator()(unsigned st, const std::vector& dst_filter, + bool remove_original_edges) { const auto& dict = aut_->get_dict(); bdd res = bddtrue; @@ -77,6 +78,9 @@ namespace spot out &= bdd_ithvar(p.first->second); } res2 |= e.cond & out; + + if (remove_original_edges) + e.cond = bddfalse; } if (res2 != bddfalse) diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index 7f0f22bff..0017f27bb 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -54,7 +54,8 @@ namespace spot public: outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u); ~outedge_combiner(); - bdd operator()(unsigned st, const std::vector& dst_filter = std::vector()); + bdd operator()(unsigned st, const std::vector& dst_filter = std::vector(), + bool remove_original_edges = false); void new_dests(unsigned st, bdd out) const; }; diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index 11b783691..bd1a1d3de 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -355,15 +355,18 @@ namespace spot unsigned new_st = it->second; bdd comb = bddtrue; - comb &= oe_(new_st, acc_states); - comb &= oe_(rhs_init); - oe_.new_dests(new_st, comb); + comb &= oe_(new_st, acc_states, true); + if (comb != bddtrue) + { + comb &= oe_(rhs_init); + oe_.new_dests(new_st, comb); + } } auto it = old_to_new.find(sere_aut->get_init_state_number()); assert(it != old_to_new.end()); - //aut_->merge_edges(); + aut_->merge_edges(); return it->second; }