diff --git a/ChangeLog b/ChangeLog index 7bdee08a2..4c5c13af0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2010-03-05 Alexandre Duret-Lutz + + Better selection of the acceptance of the initial state in SBA. + + * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set + cycle_start_ to start in the accepting layer of the degeneralized + automaton if the initial state has an accepting self-loop. + Otherwise, starts at the level of the first acceptance condition + as previously. + (tgba_sba_proxy::get_init_state): Use cycle_start_. + * src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so + that we can use it in tgba_sba_proxy::tgba_sba_proxy. + (tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state): + Declare. + * src/tgbatest/ltl2tgba.test: More tests. + 2010-03-05 Alexandre Duret-Lutz Generalize the previous patch to accepting states in SBA. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index ecc5b118d..c4fd6467a 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -375,7 +375,49 @@ namespace spot : tgba_tba_proxy(a) { if (a->number_of_acceptance_conditions() > 0) - acc_cycle_.push_back(bddtrue); + { + cycle_start_ = acc_cycle_.insert(acc_cycle_.end(), bddtrue); + + bdd all = a->all_acceptance_conditions(); + + state* init = a->get_init_state(); + tgba_succ_iterator* it = a->succ_iter(init); + for (it->first(); !it->done(); it->next()) + { + // Look only for transitions that are accepting. + if (all != it->current_acceptance_conditions()) + continue; + // Look only for self-loops. + state* dest = it->current_state(); + if (dest->compare(init) == 0) + { + // The initial state has an accepting self-loop. + // In that case it is better to start the accepting + // cycle on a "acceptance" state. This will avoid + // duplication of the initial state. + // The cycle_start_ points to the right starting + // point already, so just return. + delete dest; + delete it; + return; + } + delete dest; + } + delete it; + } + + // If we arrive here either because the number of acceptance + // condition is 0, or because the initial state has no accepting + // self-loop, start the acceptance cycle on the first condition + // (that is a non-accepting state if the number of conditions is + // not 0). + cycle_start_ = acc_cycle_.begin(); + } + + state* + tgba_sba_proxy::get_init_state() const + { + return new state_tba_proxy(a_->get_init_state(), cycle_start_); } bool diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 4dfbb4a0f..eb45384dc 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 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), // Université Pierre et Marie Curie. @@ -79,8 +81,8 @@ namespace spot virtual bdd compute_support_variables(const state* state) const; cycle_list acc_cycle_; - private: const tgba* a_; + private: bdd the_acceptance_cond_; // Disallow copy. tgba_tba_proxy(const tgba_tba_proxy&); @@ -115,6 +117,10 @@ namespace spot /// considered accepting. This is useful in algorithms working on /// degeneralized automata with state acceptance conditions. bool state_is_accepting(const state* state) const; + + virtual state* get_init_state() const; + protected: + cycle_list::iterator cycle_start_; }; } diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 3be074a71..390d5bb2b 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -59,3 +59,19 @@ for opt in '' -D -DS; do grep 'transitions: 6$' stdout grep 'states: 3$' stdout done + +# Make sure '!(Ga U b)' has 3 states and 6 transitions, +# before and after degeneralization. +for opt in '' -D -DS; do + ../ltl2tgba -k -f -R3 $opt '!(Ga U b)' > stdout + grep 'transitions: 6$' stdout + grep 'states: 3$' stdout +done + +# Make sure 'Ga U b' has 4 states and 6 transitions, +# before and after degeneralization. +for opt in '' -D -DS; do + ../ltl2tgba -k -f -R3 $opt 'Ga U b' > stdout + grep 'transitions: 6$' stdout + grep 'states: 4$' stdout +done