From bb33c5120fdcb778253627df6bf72ff96794ac5e Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 15 Oct 2025 14:24:08 +0200 Subject: [PATCH] translate_aa: fix construction for transition based acc * spot/twaalgos/translate_aa.cc: Here. --- spot/twaalgos/alternation.cc | 19 +++++++- spot/twaalgos/alternation.hh | 1 + spot/twaalgos/translate_aa.cc | 86 +++++++++++++++++++++++++---------- 3 files changed, 81 insertions(+), 25 deletions(-) diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index fb95fd6f3..8de30af15 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -39,6 +39,7 @@ namespace spot } bdd outedge_combiner::operator()(unsigned st, const std::vector& dst_filter, + const std::vector>& edge_filter, bool remove_original_edges) { const auto& dict = aut_->get_dict(); @@ -49,7 +50,23 @@ namespace spot for (auto& e: aut_->out(d1)) { // handle edge filtering - if (!dst_filter.empty()) + if (!edge_filter.empty()) + { + // Trying all univ dests for e, find if there was at least one + // compatible edge that was accepting in the original TFA + auto univ_dests = aut_->univ_dests(e.dst); + if (std::all_of(univ_dests.begin(), univ_dests.end(), + [&](unsigned dst) { + for (const auto& acc_e : edge_filter) + if(std::get<0>(acc_e) == e.src + && std::get<2>(acc_e) == dst + && bdd_implies(e.cond, std::get<1>(acc_e))) + return false; // false because we don't want to skip it + return true; + })) + continue; + } + else if (!dst_filter.empty()) // same for state-based acc { // if any edge destination is an accepting state in the SERE // automaton, handle the edge, otherwise skip it diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index 8d1027e8b..e2e719e1d 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -54,6 +54,7 @@ namespace spot outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u); ~outedge_combiner(); bdd operator()(unsigned st, const std::vector& dst_filter = std::vector(), + const std::vector>& edge_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 163afaf3b..6be7c4f85 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -97,10 +97,11 @@ namespace spot unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut, std::map& old_to_new, - std::vector* acc_states = nullptr, + std::vector* acc_edges = nullptr, bool use_accepting_sink = true) { unsigned ns = sere_aut->num_states(); + bool trans_based = sere_aut->prop_state_acc().is_false(); // TODO: create all new states at once, keeping an initial offset (the // number of states already present in aut_) @@ -111,8 +112,6 @@ namespace spot { unsigned new_st = aut_->new_state(); p.first->second = new_st; - if (acc_states != nullptr && sere_aut->state_is_accepting(st)) - acc_states->push_back(new_st); } return p.first->second; }; @@ -122,10 +121,22 @@ namespace spot unsigned new_st = register_state(st); for (const auto& e : sere_aut->out(st)) { - if (use_accepting_sink && sere_aut->state_is_accepting(e.dst)) - aut_->new_edge(new_st, accepting_sink_, e.cond); - else - aut_->new_edge(new_st, register_state(e.dst), e.cond); + bool edge_is_acc = ((trans_based && e.acc) + || (!trans_based && sere_aut->state_is_accepting(e.dst))); + + if (edge_is_acc) + { + // point to accepting sink instead of original dst if asked + if (use_accepting_sink) + aut_->new_edge(new_st, accepting_sink_, e.cond); + else + { + unsigned new_e = aut_->new_edge(new_st, register_state(e.dst), e.cond); + // remember if old edges were accepting + if (acc_edges != nullptr) + acc_edges->push_back(new_e); + } + } } } @@ -311,25 +322,19 @@ namespace spot twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict); // TODO: this should be a std::vector ! - std::vector acc_states; - std::map old_to_new; - copy_sere_aut_to_res(sere_aut, old_to_new, &acc_states, false); - std::vector acc_edges; + std::map old_to_new; + copy_sere_aut_to_res(sere_aut, old_to_new, &acc_edges, false); + + // mark all edges from NFA in new automaton unsigned ns = sere_aut->num_states(); 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; - for (auto& e : aut_->out(new_st)) - { - e.acc = acc_cond::mark_t{0}; - if (std::find(acc_states.begin(), acc_states.end(), e.dst) - != acc_states.end()) - acc_edges.push_back(aut_->edge_number(e)); - } + e.acc = acc_cond::mark_t{0}; } for (unsigned i : acc_edges) @@ -350,13 +355,26 @@ namespace spot unsigned rhs_init = recurse(f[1]); const auto& dict = aut_->get_dict(); twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict); + bool trans_based = sere_aut->prop_state_acc().is_false(); // DFA recognizes the empty language, so {0} []-> rhs is always true unsigned ns = sere_aut->num_states(); - bool has_accepting_state = false; - for (unsigned st = 0; st < ns && !has_accepting_state; ++st) - has_accepting_state = sere_aut->state_is_accepting(st); - if (!has_accepting_state) + bool accepts = false; + for (unsigned st = 0; st < ns && !accepts; ++st) + { + if (trans_based) + { + for (const auto& e : sere_aut->out(st)) + if (e.acc) + { + accepts = true; + break; + } + } + else + accepts = sere_aut->state_is_accepting(st); + } + if (!accepts) return accepting_sink_; std::map old_to_new; @@ -367,6 +385,8 @@ namespace spot std::vector univ_dest; // TODO: this should be a std::vector ! std::vector acc_states; + // any edge compatible with that should be considered accepting + std::vector> acc_edges; // registers a state in various maps and returns the index of the // anonymous bdd var representing that state @@ -381,7 +401,7 @@ namespace spot old_to_new.emplace(st, new_st); var_to_state.emplace(v, new_st); - if (sere_aut->state_is_accepting(st)) + if (!trans_based && sere_aut->state_is_accepting(st)) acc_states.push_back(new_st); vars &= bdd_ithvar(v); @@ -390,6 +410,15 @@ namespace spot return p.first->second; }; + // FIXME: this code handles dualization, but we cannot dualize if + // this situation arises: + // + // State: 0 + // [a] 1 + // [a] 2 {0} + // + // The quick fix is to simply determinize the NFA before dualizing, + // which removes any existentialism. aut_->copy_ap_of(sere_aut); for (unsigned st = 0; st < ns; ++st) { @@ -400,6 +429,15 @@ namespace spot { int st_bddi = register_state(e.dst); sig |= e.cond & bdd_ithvar(st_bddi); + + // register edge that was accepting in TFA + if (trans_based && e.acc) + { + unsigned new_src = old_to_new[e.src]; + unsigned new_dst = old_to_new[e.dst]; + + acc_edges.push_back({new_src, e.cond, new_dst}); + } } for (bdd cond : minterms_of(bddtrue, aps)) @@ -435,7 +473,7 @@ namespace spot unsigned new_st = it->second; bdd comb = bddtrue; - comb &= oe_(new_st, acc_states, true); + comb &= oe_(new_st, acc_states, acc_edges, true); if (comb != bddtrue) { comb &= oe_(rhs_init);