From 9fd33667c06c439ca90de166890e7ed7cc3ab765 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Tue, 9 Aug 2022 12:24:37 +0200 Subject: [PATCH] ltl2aa: fix R & M operators handling --- spot/twaalgos/translate_aa.cc | 28 +++------------------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index c68b30268..490ffd7a7 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -189,31 +189,9 @@ namespace spot for (auto& e : aut_->out(rhs_init)) add_self_loop(e, init_state, acc); - std::vector dsts; - for (const auto& lhs_e : aut_->out(lhs_init)) - { - const auto& lhs_dsts = aut_->univ_dests(lhs_e); - std::copy(lhs_dsts.begin(), lhs_dsts.end(), - std::back_inserter(dsts)); - size_t lhs_dest_num = dsts.size(); - - for (const auto& rhs_e : aut_->out(rhs_init)) - { - const auto& rhs_dsts = aut_->univ_dests(rhs_e); - std::copy(rhs_dsts.begin(), rhs_dsts.end(), - std::back_inserter(dsts)); - - bdd cond = lhs_e.cond & rhs_e.cond; - - unsigned dst = uniq_.new_univ_dests(dsts.begin(), - dsts.end()); - aut_->new_edge(init_state, dst, cond, {}); - - // reset to only lhs' current edge destinations - dsts.resize(lhs_dest_num); - } - dsts.clear(); - } + bdd comb = oe_(lhs_init); + comb &= oe_(rhs_init); + oe_.new_dests(init_state, comb); return init_state; }