diff --git a/ChangeLog b/ChangeLog index a480292c8..a295a7927 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-06-25 Alexandre Duret-Lutz + * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): + Rewrite using bdd_satoneset. This time it's for real. (I hope.) + * src/tgba/succiterconcrete.hh (current_base_, + current_base_left_): Delete. + * tgba/tgbabddcoredata.hh (next_set): New variable. + * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust + to update next_set. + * src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbaproduct.hh: Fix Doxygen comments. diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 5ad11c290..2304e0599 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -8,9 +8,7 @@ namespace spot : data_(d), succ_set_(successors), succ_set_left_(successors), - current_(bddfalse), - current_base_(bddfalse), - current_base_left_(bddfalse) + current_(bddfalse) { } @@ -49,41 +47,6 @@ namespace spot // d * !Next[a] * Next[b] // (We don't really care about the Now variables here.) // - // Calling bdd_fullsatone on succ_set_ would compute many more - // transitions (twice as much on this example), since all - // atomic propositions would have to appear. - // - // Basically, we want to use bdd_satone for atomic propositions - // and bdd_fullsatone for Next variable. We achieve this as - // follows - // (1) compute a (non-full) satisfaction of succ_set_ - // e.g. Now[a] * !Now[b] * c * Next[a] - // (2) retain only the atomic propositions (here: c), and call it - // our current base - // (3) compute a full satisfaction for succ_set_ & current_base_ - // Now[a] * !Now[b] * c * d * Next[a] * Next[b] - // (4) retain only the Next variables - // Next[a] * Next[b] - // (5) and finally append them to the current base - // c * Next[a] * Next[b] - // This is the first successor. - // - // This algorithm would compute only one successor. In order to - // iterate over the other ones, we have a couple of variables that - // remember what has been explored so far and what is yet to - // explore. - // - // The next time we compute a successor, we start at (3) and - // compute the *next* full satisfaction matching current_base_. The - // current_base_left_ serves this purpose: holding all the - // current_base_ satisfactions that haven't yet been explored. - // - // Once we've explored all satisfactions of current_base_, we - // start over at (1) and compute the *next* (non-full) - // satisfaction of succ_set_. To that effect, the variable - // next_succ_set hold all these satisfactions that must still be - // explored. - // // Note: on this example we would not exactly get the six transitions // mentionned, but maybe something like // c * Next[a] * Next[b] @@ -92,43 +55,27 @@ namespace spot // d * !c * Next[a] * Next[b] // d * !c * Next[a] * !Next[b] // d * !c * !Next[a] * Next[b] - // depending on the BDD order. + // depending on the BDD order. It doesn't really matter. The important + // point is that we don't list all four possible 'c' and 'd' combinations. - // FIXME: It would help to have this half-full half-partial - // satisfaction operation available as one BDD function. // FIXME: Iterating on the successors this way (calling // bdd_satone/bdd_fullsetone and NANDing out the result from a // set) requires several descent of the BDD. Maybe it would be // faster to compute all satisfying formula in one operation. do { - if (current_ == bddfalse) - { - succ_set_left_ &= !current_base_; - if (succ_set_left_ == bddfalse) // No more successors? - return; - // (1) (2) - current_base_ = bdd_exist(bdd_satone(succ_set_left_), - data_.notvar_set); - current_base_left_ = current_base_; - } - // (3) (4) (5) - current_ = - current_base_ & bdd_exist(bdd_fullsatone(succ_set_left_ - & current_base_left_), - data_.notnext_set); - current_base_left_ &= !current_; + succ_set_left_ &= !current_; + if (succ_set_left_ == bddfalse) // No more successors? + return; + current_ = bdd_satoneset(succ_set_left_, data_.next_set, bddfalse); + + // The destination state, computed here, should be + // compatible with the transition relation. Otherwise + // it won't have any successor (a dead node). + current_state_ = bdd_replace(bdd_exist(current_, data_.notnext_set), + data_.next_to_now); } - while (// No more successors with the current_base_? Compute - // the next base. - current_ == bddfalse - // The destination state, computed here, should be - // compatible with the transition relation. Otherwise - // it won't have any successor and useless. - || ((current_state_ = bdd_replace(bdd_exist(current_, - data_.notnext_set), - data_.next_to_now)) - & data_.relation) == bddfalse); + while ((current_state_ & data_.relation) == bddfalse); } bool diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index abe3b68c7..9d0058281 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -17,8 +17,8 @@ namespace spot /// conditions and accepting conditions, represented as a BDD. /// The job of this iterator will be to enumerate the /// satisfactions of that BDD and split them into destination - /// states and conditions, and compute accepting conditions. - /// \param d The core data of the automata. + /// states and conditions, and compute accepting conditions. + /// \param d The core data of the automata. /// These contains sets of variables useful to split a BDD, and /// compute accepting conditions. tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors); @@ -42,10 +42,6 @@ namespace spot /// atomic proposition and Next variables. bdd current_state_; ///< Current successor, as a /// conjunction of Now variables. - bdd current_base_; ///< Current successor base. - bdd current_base_left_; ///< Used to lists all possible full satisfaction - /// current_base_ which haven't been explored. - }; } diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index f56ba3a8f..4df8a2ea2 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -3,20 +3,33 @@ namespace spot { tgba_bdd_core_data::tgba_bdd_core_data() - : relation(bddtrue), accepting_conditions(bddfalse), - now_set(bddtrue), negnow_set(bddtrue), - notnow_set(bddtrue), notnext_set(bddtrue), var_set(bddtrue), - notvar_set(bddtrue), notacc_set(bddtrue), negacc_set(bddtrue), + : relation(bddtrue), + accepting_conditions(bddfalse), + now_set(bddtrue), + next_set(bddtrue), + negnow_set(bddtrue), + notnow_set(bddtrue), + notnext_set(bddtrue), + var_set(bddtrue), + notvar_set(bddtrue), + notacc_set(bddtrue), + negacc_set(bddtrue), next_to_now(bdd_newpair()) { } tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy) - : relation(copy.relation), accepting_conditions(copy.accepting_conditions), - now_set(copy.now_set), negnow_set(copy.negnow_set), - notnow_set(copy.notnow_set), notnext_set(copy.notnext_set), - var_set(copy.var_set), notvar_set(copy.notvar_set), - notacc_set(copy.notacc_set), negacc_set(copy.negacc_set), + : relation(copy.relation), + accepting_conditions(copy.accepting_conditions), + now_set(copy.now_set), + next_set(copy.next_set), + negnow_set(copy.negnow_set), + notnow_set(copy.notnow_set), + notnext_set(copy.notnext_set), + var_set(copy.var_set), + notvar_set(copy.notvar_set), + notacc_set(copy.notacc_set), + negacc_set(copy.negacc_set), next_to_now(bdd_copypair(copy.next_to_now)) { } @@ -28,6 +41,7 @@ namespace spot accepting_conditions(left.accepting_conditions | right.accepting_conditions), now_set(left.now_set & right.now_set), + next_set(left.next_set & right.next_set), negnow_set(left.negnow_set & right.negnow_set), notnow_set(left.notnow_set & right.notnow_set), notnext_set(left.notnext_set & right.notnext_set), @@ -59,6 +73,7 @@ namespace spot tgba_bdd_core_data::declare_now_next(bdd now, bdd next) { now_set &= now; + next_set &= next; negnow_set &= !now; notnext_set &= now; notnow_set &= next; diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 433b9f756..98e1ec085 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -62,6 +62,8 @@ namespace spot /// The conjunction of all Now variables, in their positive form. bdd now_set; + /// The conjunction of all Next variables, in their positive form. + bdd next_set; /// The conjunction of all Now variables, in their negated form. bdd negnow_set; /// \brief The (positive) conjunction of all variables which are diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index d77d17718..44ba04216 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -15,6 +15,7 @@ namespace spot data_.relation = bdd_replace(in.relation, rewrite); data_.accepting_conditions = bdd_replace(in.accepting_conditions, rewrite); data_.now_set = bdd_replace(in.now_set, rewrite); + data_.next_set = bdd_replace(in.next_set, rewrite); data_.negnow_set = bdd_replace(in.negnow_set, rewrite); data_.notnow_set = bdd_replace(in.notnow_set, rewrite); data_.notnext_set = bdd_replace(in.notnext_set, rewrite);