From c63412ab947ce0e16d2ec637da128048c25f37b4 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Fri, 17 Oct 2025 17:36:40 +0200 Subject: [PATCH] translate_aa: fix sere copy When adapting the code to handle transition-based acceptance, a bug was introduced so that only accepting edges were copied to the result automaton. The self-loop labeled as false edge-case is here as prevention, I am not sure it happens in practice. * spot/twaalgos/translate_aa.cc: Here. --- spot/twaalgos/translate_aa.cc | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index 6be7c4f85..50096a2c3 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -124,19 +124,16 @@ namespace spot 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); - } - } + unsigned new_edge; + // point to accepting sink instead of original dst if asked + if(use_accepting_sink && edge_is_acc) + new_edge = aut_->new_edge(new_st, accepting_sink_, e.cond); + else + new_edge = aut_->new_edge(new_st, register_state(e.dst), e.cond); + + // remember if old edges were accepting + if (acc_edges != nullptr && edge_is_acc) + acc_edges->push_back(new_edge); } } @@ -340,6 +337,9 @@ namespace spot for (unsigned i : acc_edges) { auto& e1 = aut_->edge_storage(i); + // self loop used to mark accepting state, skip it! + if (e1.cond == bddfalse) + continue; for (const auto& e2 : aut_->out(rhs_init)) aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond); }