diff --git a/spot/tl/sonf.cc b/spot/tl/sonf.cc index 0b70ab5e3..29b613eaa 100644 --- a/spot/tl/sonf.cc +++ b/spot/tl/sonf.cc @@ -131,7 +131,7 @@ namespace spot { // recurse into rhs first (_ []-> rhs) formula rhs = - extractor(f[1], extracted, extractor, false, false); + f[1].map(extractor, extracted, extractor, false, false); f = formula::binop(kind, f[0], rhs); formula ap = formula::ap(new_ap_name()); diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 8de30af15..fb95fd6f3 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -39,7 +39,6 @@ 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(); @@ -50,23 +49,7 @@ namespace spot for (auto& e: aut_->out(d1)) { // handle edge filtering - 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 (!dst_filter.empty()) { // 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 e2e719e1d..8d1027e8b 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -54,7 +54,6 @@ 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 6be7c4f85..095f92c5a 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -26,7 +26,6 @@ #include #include #include -#include #include #include @@ -35,24 +34,6 @@ namespace spot { namespace { - twa_graph_ptr sere_aa_translate(formula f, const bdd_dict_ptr& dict) - { - // old bdd method - if (sere_aa_translation_options() == 0) - return sere_to_tgba(f, dict, true); - - // derivation - if (sere_aa_translation_options() == 1) - return derive_finite_automaton_with_first(f, dict); - - // linear form - if (sere_aa_translation_options() == 2) - return expand_finite_automaton(f, dict, exp_opts::expand_opt::None); - - // linear form - trans-based - return expand_finite_automaton2(f, dict, exp_opts::expand_opt::None); - } - struct ltl_to_aa_builder { ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink) @@ -97,11 +78,10 @@ namespace spot unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut, std::map& old_to_new, - std::vector* acc_edges = nullptr, + std::vector* acc_states = 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_) @@ -112,6 +92,8 @@ 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; }; @@ -121,22 +103,10 @@ namespace spot unsigned new_st = register_state(st); for (const auto& e : sere_aut->out(st)) { - 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); - } - } + 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); } } @@ -319,22 +289,43 @@ 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); + twa_graph_ptr sere_aut; + if (sere_aa_translation_options() == 0) + { + // old bdd method + sere_aut = sere_to_tgba(f[0], dict, true); + } + else if (sere_aa_translation_options() == 1) + { + // derivation + sere_aut = derive_finite_automaton_with_first(f[0], dict); + } + else + { + // linear form + sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None); + } // TODO: this should be a std::vector ! - std::vector acc_edges; + std::vector acc_states; std::map old_to_new; - copy_sere_aut_to_res(sere_aut, old_to_new, &acc_edges, false); + copy_sere_aut_to_res(sere_aut, old_to_new, &acc_states, false); - // mark all edges from NFA in new automaton + std::vector acc_edges; 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}; + { + 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)); + } } for (unsigned i : acc_edges) @@ -354,27 +345,29 @@ 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(); + twa_graph_ptr sere_aut; + if (sere_aa_translation_options() == 0) + { + // old bdd method + sere_aut = sere_to_tgba(f[0], dict, true); + } + else if (sere_aa_translation_options() == 1) + { + // derivation + sere_aut = derive_finite_automaton_with_first(f[0], dict); + } + else + { + // linear form + sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None); + } // DFA recognizes the empty language, so {0} []-> rhs is always true unsigned ns = sere_aut->num_states(); - 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) + 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) return accepting_sink_; std::map old_to_new; @@ -385,8 +378,6 @@ 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 @@ -401,7 +392,7 @@ namespace spot old_to_new.emplace(st, new_st); var_to_state.emplace(v, new_st); - if (!trans_based && sere_aut->state_is_accepting(st)) + if (sere_aut->state_is_accepting(st)) acc_states.push_back(new_st); vars &= bdd_ithvar(v); @@ -410,15 +401,6 @@ 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) { @@ -429,15 +411,6 @@ 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)) @@ -473,7 +446,7 @@ namespace spot unsigned new_st = it->second; bdd comb = bddtrue; - comb &= oe_(new_st, acc_states, acc_edges, true); + comb &= oe_(new_st, acc_states, true); if (comb != bddtrue) { comb &= oe_(rhs_init); @@ -556,16 +529,14 @@ namespace spot pref = 0; else if (!strcasecmp(version, "derive")) pref = 1; - else if (!strcasecmp(version, "lf")) + else if (!strcasecmp(version, "expansion")) pref = 2; - else if (!strcasecmp(version, "lft")) - pref = 3; else { const char* err = ("sere_aa_translation_options(): argument" - " should be one of {bdd,derive,lf,lft}"); + " should be one of {bdd,derive,expansion}"); if (env) - err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,lf,lft}"; + err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}"; throw std::runtime_error(err); } }