From 74e20a6ec4bf882587f77f9cc893fd0943a40abf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 10 Aug 2014 15:18:17 +0200 Subject: [PATCH] complete: get rid of tgba_explicit_number * src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh (tgba_complete_here): New method for tgba_digraph. (tgba_complete): Rewrite using dupexp and the above. --- src/tgbaalgos/complete.cc | 163 +++++++++++++++++--------------------- src/tgbaalgos/complete.hh | 20 +++-- 2 files changed, 89 insertions(+), 94 deletions(-) diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index b24b57465..b4bb4bda4 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -18,111 +18,96 @@ // along with this program. If not, see . #include "complete.hh" -#include "reachiter.hh" #include "ltlast/constant.hh" +#include "dupexp.hh" namespace spot { - - namespace + unsigned tgba_complete_here(tgba_digraph* aut) { - class tgbacomplete_iter: - public tgba_reachable_iterator_depth_first_stack - { - bdd_dict* dict_; - tgba_explicit_number* out_; - bdd addacc_; - - typedef state_explicit_number::transition trans; - public: - tgbacomplete_iter(const tgba* a) - : tgba_reachable_iterator_depth_first_stack(a), - dict_(a->get_dict()), - out_(new tgba_explicit_number(dict_)), - addacc_(bddfalse) + unsigned n = aut->num_states(); + unsigned sink = -1U; + bdd allacc = aut->all_acceptance_conditions(); + if (allacc == bddfalse) { - dict_->register_all_variables_of(a, out_); - - if (a->number_of_acceptance_conditions() == 0) + // We cannot safely complete an automaton if it has no + // acceptance set as the added sink would become accepting. + // In this case, add an acceptance set to all transitions. + const ltl::formula* t = ltl::constant::true_instance(); + int v = aut->get_dict()->register_acceptance_variable(t, aut); + allacc = bdd_ithvar(v); + aut->set_acceptance_conditions(allacc); + for (auto& t: aut->transitions()) + t.acc = allacc; + } + else + { + // If some acceptance sets were used, loop over the states and + // seek a state that has only self loops, and that is not + // accepting. This will be our sink state. + for (unsigned i = 0; i < n; ++i) { - const ltl::formula* t = ltl::constant::true_instance(); - int accvar = - dict_->register_acceptance_variable(t, out_); - addacc_ = bdd_ithvar(accvar); - out_->set_acceptance_conditions(addacc_); - } - else - { - out_->set_acceptance_conditions(a->all_acceptance_conditions()); + bool selfloop = true; + bdd accsum = bddfalse; + for (auto& t: aut->out(i)) + { + if (t.dst != i) // Not a self-loop + { + selfloop = false; + break; + } + accsum |= t.acc; + } + if (selfloop && accsum != allacc) // We have found a sink! + { + sink = i; + break; + } } } - - tgba_explicit_number* - result() + // If we haven't found any sink, simply add one. + if (sink == -1U) { - return out_; + sink = aut->new_state(); + ++n; } - void - end() + // Now complete all states (including the sink). + for (unsigned i = 0; i < n; ++i) { - out_->merge_transitions(); - // create a sink state if needed. - if (out_->has_state(0)) - { - trans* t = out_->create_transition(0, 0); - t->condition = bddtrue; - } - } - - void process_state(const state*, int n, - tgba_succ_iterator* i) - { - // add a transition to a sink state if the state is not complete. - bdd all = bddtrue; + bdd missingcond = bddtrue; bdd acc = bddfalse; - if (i->first()) + for (auto& t: aut->out(i)) { - // In case the automaton use state-based acceptance, propagate - // the acceptance of the first transition to the one we add. - acc = i->current_acceptance_conditions(); - - do - all -= i->current_condition(); - while (i->next()); - } - if (all != bddfalse) - { - trans* t = out_->create_transition(n, 0); - t->condition = all; - t->acceptance_conditions = acc | addacc_; + missingcond -= t.cond; + // FIXME: This is ugly. + // + // In case the automaton uses state-based acceptance, we + // need to put the new transition in the same set as all + // the other. + // + // In case the automaton uses transition-based acceptance, + // it does not matter what acceptance set we put the new + // transition into. + // + // So in both cases, we put the transition in the same + // acceptance sets as the last outgoing transition of the + // state. + acc = t.acc; } + // In case the automaton use state-based acceptance, propagate + // the acceptance of the first transition to the one we add. + if (missingcond != bddfalse) + aut->new_transition(i, sink, missingcond, acc); } - - void - process_link(const state*, int in, - const state*, int out, - const tgba_succ_iterator* si) - { - assert(in > 0); - assert(out > 0); - trans* t1 = out_->create_transition(in, out); - - t1->condition = si->current_condition(); - t1->acceptance_conditions = - si->current_acceptance_conditions() | addacc_; - } - - }; - - } // anonymous - - tgba_explicit_number* tgba_complete(const tgba* aut) - { - tgbacomplete_iter ci(aut); - ci.run(); - return ci.result(); + return sink; } + + tgba_digraph* tgba_complete(const tgba* aut) + { + tgba_digraph* res = tgba_dupexp_dfs(aut); + tgba_complete_here(res); + return res; + } + } - - diff --git a/src/tgbaalgos/complete.hh b/src/tgbaalgos/complete.hh index 35a173980..9a0216f09 100644 --- a/src/tgbaalgos/complete.hh +++ b/src/tgbaalgos/complete.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -20,13 +20,23 @@ #ifndef SPOT_TGBAALGOS_COMPLETE_HH # define SPOT_TGBAALGOS_COMPLETE_HH -#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbagraph.hh" namespace spot { - /// Complete a TGBA - SPOT_API tgba_explicit_number* - tgba_complete(const tgba* aut); + /// \brief Complete a tgba_digraph in place. + /// + /// If the tgba has no acceptance set, one will be added. The + /// returned value is the number of the sink state (it can be a new + /// state added for completion, or an existing non-accepting state + /// that has been reused as sink state because it had not outgoing + /// transitions apart from self-loops.) + SPOT_API unsigned tgba_complete_here(tgba_digraph* aut); + + /// \brief Clone a tgba and complete it. + /// + /// If the tgba has no acceptance set, one will be added. + SPOT_API tgba_digraph* tgba_complete(const tgba* aut); } #endif // SPOT_TGBAALGOS_COMPLETE_HH