diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index 1fd6e03df..d4128ed4f 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -71,34 +71,43 @@ namespace spot aut_->new_edge(init_state, dst, e.cond, acc); } - unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut) + unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut, + std::map& old_to_new, + std::vector* acc_states = nullptr, + bool use_accepting_sink = true) { + unsigned ns = sere_aut->num_states(); + + // TODO: create all new states at once, keeping an initial offset (the + // number of states already present in aut_) aut_->copy_ap_of(sere_aut); - std::map old_to_new; auto register_state = [&](unsigned st) -> unsigned { auto p = old_to_new.emplace(st, 0); if (p.second) { 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; }; - unsigned ns = sere_aut->num_states(); for (unsigned st = 0; st < ns; ++st) { unsigned new_st = register_state(st); for (const auto& e : sere_aut->out(st)) { - if (sere_aut->state_is_accepting(e.dst)) + 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); } } - return register_state(sere_aut->get_init_state_number()); + auto it = old_to_new.find(sere_aut->get_init_state_number()); + assert(it != old_to_new.end()); + return it->second; } @@ -272,6 +281,47 @@ namespace spot return init_state; } + case op::EConcat: + { + 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); + + // 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; + 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)); + } + } + + for (unsigned i : acc_edges) + { + auto& e1 = aut_->edge_storage(i); + for (const auto& e2 : aut_->out(rhs_init)) + aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond); + } + + auto it = old_to_new.find(sere_aut->get_init_state_number()); + assert(it != old_to_new.end()); + + return it->second; + } + case op::UConcat: { unsigned rhs_init = recurse(f[1]); @@ -375,7 +425,8 @@ namespace spot { twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], aut_->get_dict()); - return copy_sere_aut_to_res(sere_aut); + std::map old_to_new; + return copy_sere_aut_to_res(sere_aut, old_to_new); } case op::NegClosure: @@ -384,7 +435,6 @@ namespace spot case op::Xor: case op::Implies: case op::Equiv: - case op::EConcat: case op::EConcatMarked: case op::OrRat: case op::AndRat: @@ -419,7 +469,10 @@ namespace spot aut->set_init_state(init_state); if (purge_dead_states) - aut->purge_dead_states(); + { + aut->purge_dead_states(); + aut->merge_edges(); + } return aut; }