From 71b08b034a69d410bba18f4f1bb1eb768275ecf0 Mon Sep 17 00:00:00 2001 From: xlauko Date: Thu, 13 Jul 2017 11:19:45 +0200 Subject: [PATCH] tra2tba: Make result state-based if possible * spot/twaalgos/remfin.cc: Create state-based result. --- spot/twaalgos/remfin.cc | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 16e8b9239..ba82d987d 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -84,6 +84,23 @@ namespace spot return scc_mark; } + // Transforms automaton from transition based acceptance to state based + // acceptance. + void make_state_acc(twa_graph_ptr & aut) + { + unsigned nst = aut->num_states(); + for (unsigned s = 0; s < nst; ++s) + { + acc_cond::mark_t acc = 0U; + for (auto& t: aut->out(s)) + acc |= t.acc; + for (auto& t: aut->out(s)) + t.acc = acc; + } + aut->prop_state_acc(true); + } + + // Check whether the SCC contains non-accepting cycles. // // A cycle is accepting (in a Rabin automaton) if there exists an @@ -341,26 +358,11 @@ namespace spot res->prop_universal(deterministic); res->purge_dead_states(); res->merge_edges(); - + if (!aut_pairs.infs()) + make_state_acc(res); return res; } - // Transforms automaton from transition based acceptance to state based - // acceptance. - void make_state_acc(twa_graph_ptr & aut) - { - unsigned nst = aut->num_states(); - for (unsigned s = 0; s < nst; ++s) - { - acc_cond::mark_t acc = 0U; - for (auto& t: aut->out(s)) - acc |= t.acc; - for (auto& t: aut->out(s)) - t.acc = acc; - } - aut->prop_state_acc(true); - } - // If the DNF is // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) -- GitLab