From 9d232af82f6254a8264ba327aff3ec0d1d349622 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Aug 2011 10:39:00 +0200 Subject: [PATCH] Refine yesterday's change to the degeneralization. This avoids a small regression on the size of degeneralized automata of our usual list of literature formulae. * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::union_acceptance_conditions_of_original_state): New method. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting states, ignore only the last expected acceptance condition if its common to all outgoing transitions AND if it is not used by any outgoing transitions of the destination. --- ChangeLog | 15 ++++++++ src/tgba/tgbatba.cc | 86 ++++++++++++++++++++++++++++++++++++++++----- src/tgba/tgbatba.hh | 13 ++++++- 3 files changed, 105 insertions(+), 9 deletions(-) diff --git a/ChangeLog b/ChangeLog index 532ee587b..f56bc652d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2011-08-26 Alexandre Duret-Lutz + + Refine yesterday's change to the degeneralization. + + This avoids a small regression on the size of degeneralized + automata of our usual list of literature formulae. + + * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc + (tgba_tba_proxy::union_acceptance_conditions_of_original_state): + New method. + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting + states, ignore only the last expected acceptance condition if its + common to all outgoing transitions AND if it is not used by any + outgoing transitions of the destination. + 2011-08-25 Alexandre Duret-Lutz Make sure the degeneralization is idempotent (up to renaming of diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 50ed88dc3..37248aa6a 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -173,17 +173,59 @@ namespace spot // states are accepting. if (*expected == bddtrue) { - // When degeneralizing to SBA, remove the acceptance - // conditions that are common to all outgoing - // transitions of this state. Since they are common, - // we need not fear removing them: we will see them - // eventually if we make a cycle. This helps to make - // the degeneralization idempotent. - acc -= aut->common_acceptance_conditions_of_original_state(rs); + // When degeneralizing to SBA, ignore the last + // expected acceptance set (the value of *prev below) + // if it is common to all other outgoing transitions (of the + // current state) AND if it is not used by any outgoing + // transition of the destination state. + // + // 1) It's correct to do that, because this acceptance + // set is common to other outgoing transitions. + // Therefore if we make a cycle to this state we + // will eventually see that acceptance set thanks + // to the "pulling" of the common acceptance sets + // of the destination state (cf. "odest"). + // + // 2) It's also desirable because it makes the + // degeneralization idempotent (up to a renaming of + // states). Consider the following automaton where + // 1 is initial and => marks accepting transitions: + // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, + // with 1 as accepting state. However if you try + // degeralize it without ignoring *prev, we'll get + // two copies of states 2, depending on whether we + // reach it using 1=>2 or from 2->2. If this + // example was not clear, uncomment this following + // "if" block, and play with the "degenid.test" + // test case. + // + // 3) Ignoring all common acceptance sets would also + // be correct, but it would make the + // degeneralization produce larger automata in some + // cases. The current condition to ignore only one + // acceptance set if is this not used by the next + // state is a heuristic that is compatible with + // point 2) above while not causing more states to + // be generated in our benchmark of 188 formulae + // from the literature. + if (expected != cycle.begin()) + { + iterator prev = expected; + --prev; + bdd common = aut-> + common_acceptance_conditions_of_original_state(rs); + if ((common & *prev) == *prev) + { + bdd u = aut-> + union_acceptance_conditions_of_original_state(odest); + if ((u & *prev) != *prev) + acc -= *prev; + } + } // Use the acceptance sets common to all outgoing // transition of the destination state. In case of a // self-loop, we will be adding back the acceptance - // sets we removed. This is what we want. + // set we removed. This is what we want. acc |= otheracc; } else @@ -371,6 +413,14 @@ namespace spot ++i; s->destroy(); } + i = accmapu_.begin(); + while (i != accmapu_.end()) + { + // Advance the iterator before deleting the key. + const state* s = i->first; + ++i; + s->destroy(); + } } state* @@ -417,6 +467,26 @@ namespace spot return common; } + bdd + tgba_tba_proxy::union_acceptance_conditions_of_original_state(const state* s) + const + { + // Lookup cache + accmap_t::const_iterator i = accmapu_.find(s); + if (i != accmapu_.end()) + return i->second; + + bdd common = bddfalse; + tgba_succ_iterator* it = a_->succ_iter(s); + for (it->first(); !it->done(); it->next()) + common |= it->current_acceptance_conditions(); + delete it; + + // Populate cache + accmapu_[s->clone()] = common; + return common; + } + bdd_dict* tgba_tba_proxy::get_dict() const { diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index b85ebd29f..46eb06f01 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // l'Epita. // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -87,6 +87,16 @@ namespace spot bdd common_acceptance_conditions_of_original_state(const state* ostate) const; + /// \brief Return the union of acceptance conditions of all outgoing + /// transitions of state \a ostate in the original automaton. + /// + /// This internal function is only meant to be used to implement + /// the iterator returned by succ_iter. + /// + /// The result of this function is computed the first time, and + /// then cached. + bdd union_acceptance_conditions_of_original_state(const state* s) const; + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; @@ -98,6 +108,7 @@ namespace spot typedef Sgi::hash_map accmap_t; mutable accmap_t accmap_; + mutable accmap_t accmapu_; // Disallow copy. tgba_tba_proxy(const tgba_tba_proxy&);