diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index d5d59a961..03b8d5c2a 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -38,7 +38,7 @@ namespace spot aut_->get_dict()->unregister_all_my_variables(this); } - bdd outedge_combiner::operator()(unsigned st) + bdd outedge_combiner::operator()(unsigned st, const std::vector& dst_filter) { const auto& dict = aut_->get_dict(); bdd res = bddtrue; @@ -47,6 +47,21 @@ namespace spot bdd res2 = bddfalse; for (auto& e: aut_->out(d1)) { + // handle edge filtering + if (!dst_filter.empty()) + { + // if any edge destination is an accepting state in the SERE + // automaton, handle the edge, otherwise skip it + auto univ_dests = aut_->univ_dests(e.dst); + if (std::all_of(univ_dests.begin(), univ_dests.end(), + [&](unsigned dst) + { + return std::find(dst_filter.begin(), dst_filter.end(), dst) + == dst_filter.end(); + })) + continue; + } + bdd out = bddtrue; for (unsigned d: aut_->univ_dests(e.dst)) { @@ -65,7 +80,9 @@ namespace spot } res2 |= e.cond & out; } - res &= res2; + + if (res2 != bddfalse) + res &= res2; } return res; } diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index 9490272a1..4949006f2 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -53,7 +53,7 @@ namespace spot public: outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u); ~outedge_combiner(); - bdd operator()(unsigned st); + bdd operator()(unsigned st, const std::vector& dst_filter = std::vector()); void new_dests(unsigned st, bdd out) const; }; diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index daf9126cb..11b783691 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -274,8 +274,7 @@ namespace spot case op::UConcat: { - // FIXME: combine out edges with rhs ! - //unsigned rhs_init = recurse(f[1]); + unsigned rhs_init = recurse(f[1]); const auto& dict = aut_->get_dict(); twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict); @@ -286,6 +285,7 @@ namespace spot bdd vars = bddtrue; bdd aps = sere_aut->ap_vars(); std::vector univ_dest; + std::vector acc_states; // registers a state in various maps and returns the index of the // anonymous bdd var representing that state @@ -300,6 +300,9 @@ namespace spot old_to_new.emplace(st, new_st); var_to_state.emplace(v, new_st); + if (sere_aut->state_is_accepting(st)) + acc_states.push_back(new_st); + vars &= bdd_ithvar(v); } @@ -345,9 +348,22 @@ namespace spot } } + for (unsigned st = 0; st < ns; ++st) + { + auto it = old_to_new.find(st); + assert(it != old_to_new.end()); + unsigned new_st = it->second; + + bdd comb = bddtrue; + comb &= oe_(new_st, acc_states); + 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(); return it->second; }