diff --git a/ChangeLog b/ChangeLog index 415a81431..27fc4a3d5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-11-04 Alexandre Duret-Lutz + * src/tgba/tgba.hh, src/tgba/tgba.cc + (tgba::number_of_acceptance_conditions): New method. + * src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it. + * wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh, tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and tgbaalgos/rundotdec.hh. diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 62663d951..b9cb9009a 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -25,7 +25,8 @@ namespace spot { tgba::tgba() : last_support_conditions_input_(0), - last_support_variables_input_(0) + last_support_variables_input_(0), + num_acc_(-1) { } @@ -75,4 +76,21 @@ namespace spot return ""; } + int + tgba::number_of_acceptance_conditions() const + { + if (num_acc_ < 0) + { + bdd all = all_acceptance_conditions(); + int n = 0; + while (all != bddfalse) + { + ++n; + all -= bdd_satone(all); + } + num_acc_ = n; + } + return num_acc_; + } + } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index f9c613a83..ddb9e78ef 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -173,6 +173,9 @@ namespace spot /// the SCC should be equal to the result of this function. virtual bdd all_acceptance_conditions() const = 0; + /// The number of acceptance conditions. + virtual int number_of_acceptance_conditions() const; + /// \brief Return the conjuction of all negated acceptance /// variables. /// @@ -195,6 +198,7 @@ namespace spot mutable bdd last_support_conditions_output_; mutable const state* last_support_variables_input_; mutable bdd last_support_variables_output_; + mutable int num_acc_; }; } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index a172a6e10..59e45a71b 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -108,18 +108,9 @@ namespace spot lbtt_bfs(const tgba* a, std::ostream& os) : tgba_reachable_iterator_breadth_first(a), os_(os), - acc_count_(0), + acc_count_(a->number_of_acceptance_conditions()), acs_(a->all_acceptance_conditions()) - { - // Count the number of acceptance_conditions. - bdd all = a->all_acceptance_conditions(); - while (all != bddfalse) - { - bdd one = bdd_satone(all); - all -= one; - ++acc_count_; - } } void