diff --git a/ChangeLog b/ChangeLog index fb57ab877..ee19e7a32 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,11 +1,27 @@ +2003-07-03 Alexandre Duret-Lutz + + * src/tgba/succiter.hh (tgba_succ_iterator::current_condition): + State that this is a boolean function. + * src/tgba/succiterconcrete.hh + (tgba_succ_iterator_concrete::trans_dest_, + tgba_succ_iterator_concrete::trans_set_, + tgba_succ_iterator_concrete::trans_set_left_, + tgba_succ_iterator_concrete::neg_trans_set_): Remove. + * src/tgba/succiterconcrete.cc + (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete, + tgba_succ_iterator_concrete::first): Adjust to removed members. + (tgba_succ_iterator_concrete::next): Simplify, transitions + are no labelled by boolean functions, not only conjunctions. + Suggested by Denis Poitrenaud. + 2003-07-02 Alexandre Duret-Lutz - * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New - function. - * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): + * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New + function. + * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): Likewise. - * src/tgba/tgbabddtranslatefactory.cc - (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use + * src/tgba/tgbabddtranslatefactory.cc + (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_core_data::translate. * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 4c278c7ad..7c619f778 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -66,6 +66,8 @@ namespace spot /// with different conditions, leading to the same state. virtual state* current_state() = 0; /// \brief Get the condition on the transition leading to this successor. + /// + /// This is a boolean function of atomic propositions. virtual bdd current_condition() = 0; /// \brief Get the accepting conditions on the transition leading /// to this successor. diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 395fcda01..6f09debc8 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -8,9 +8,6 @@ namespace spot : data_(d), succ_set_(successors), succ_set_left_(successors), - trans_dest_(bddfalse), - trans_set_(bddfalse), - trans_set_left_(bddfalse), current_(bddfalse) { } @@ -23,9 +20,7 @@ namespace spot tgba_succ_iterator_concrete::first() { succ_set_left_ = succ_set_; - trans_dest_ = bddfalse; - trans_set_ = bddfalse; - trans_set_left_ = bddfalse; + current_ = bddfalse; if (!done()) next(); } @@ -49,10 +44,10 @@ namespace spot // a & b & Next[a] & !Next[b] // This denotes four transitions, three of which going to // the same node. Obviously (a&b | !a&b | a&!b) - // == (a | b), so it's tempting to replace these three - // transitions by the following two: - // a & Next[a] & Next[b] - // b & Next[a] & Next[b] + // == (a | b), so it's tempting to replace these four + // transitions by + // (a + b) & Next[a] & Next[b] + // a & b & Next[a] & !Next[b] // Is this always correct? No! It depends on the // accepting conditions associated to each transition. // We cannot merge transitions which have different @@ -70,86 +65,55 @@ namespace spot do { - // We performs a two-level iteration on transitions. - // - // succ_set_ and succ_set_left_ hold the information about the - // outer loop: the set of all transitiong going off this - // state. - // - // From this (outer) set, we compute subsets of transitions - // going to the same state and sharing the same accepting - // conditions. These are held by the trans_set_ and - // trans_set_left_ variables. - // - // We iterate of trans_set_ until all its transitions - // have been seen (trans_set_left_ is then empty). Then - // we remove trans_set_ from succ_set_left_ and compute another - // subset of succ_set_left_ to iterate over. - // FIXME: Iterating on the successors this way (calling // bdd_satone{,set} 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. - if (trans_set_left_ == bddfalse) + succ_set_left_ &= !current_; + if (succ_set_left_ == bddfalse) // No more successors? + return; + + // Pick one transition, and extract its destination. + bdd trans = bdd_satoneset(succ_set_left_, data_.next_set, + bddfalse); + bdd dest = bdd_exist(trans, data_.notnext_set); + + // Gather all transitions going to this destination... + current_ = succ_set_left_ & dest; + // ... and compute their accepting sets. + bdd as = data_.accepting_conditions & current_; + + // AS is false when no satisfaction of the current transition + // belongs to an accepting set: current_ can be used as-is. + if (as != bddfalse) { - succ_set_left_ &= !(trans_set_ & trans_dest_); - if (succ_set_left_ == bddfalse) // No more successors? - return; + // Otherwise, we have accepting sets, and we should + // restrict current_ to a subset sharing the same + // accepting conditions. + // same accepting set. - // Pick one transition, and extract its destination. - bdd trans = bdd_satoneset(succ_set_left_, data_.next_set, - bddfalse); - trans_dest_ = bdd_exist(trans, data_.notnext_set); - - // Gather all transitions going to this destination... - bdd st = succ_set_left_ & trans_dest_; - // ... and compute their accepting sets. - bdd as = data_.accepting_conditions & st; - - if (as == bddfalse) - { - // AS is false when no transition from ST belongs to - // an accepting set. Iterate over ST directly. - trans_set_ = bdd_exist(st, data_.nownext_set); - } - else - { - // Otherwise, we have accepting sets, and we should - // only work over a set of transitions sharing the - // same accepting set. - - as = bdd_exist(as, data_.nownext_set); - // as = (a | (!a)&b) & (Acc[a] | Acc[b]) + (!a & Acc[b]) - bdd cube = bdd_satone(as); - // cube = (!ab & Acc[a]) - bdd prop = bdd_exist(cube, data_.acc_set); - // prop = (!a)&b - bdd acc = bdd_forall(bdd_restrict(as, prop), data_.var_set); - // acc = (Acc[a] | Acc[b]) - trans_set_ = bdd_restrict(as, acc); - // trans_set = (a | (!a)&b) - } - trans_set_left_ = trans_set_; - neg_trans_set_ = !trans_set_; + as = bdd_exist(as, data_.nownext_set); + // as = (a | (!a)&b) & (Acc[a] | Acc[b]) + (!a & Acc[b]) + bdd cube = bdd_satone(as); + // cube = (!ab & Acc[a]) + bdd prop = bdd_exist(cube, data_.acc_set); + // prop = (!a)&b + bdd acc = bdd_forall(bdd_restrict(as, prop), data_.var_set); + // acc = (Acc[a] | Acc[b]) + bdd all = as & acc; + // all = (a | (!a)&b) & (Acc[a] | Acc[b]) + current_ = bdd_exist(all, data_.acc_set) & dest; + // current_ = (a | (!a)&b) & (Next...) } - // Pick and remove one satisfaction from trans_set_left_. - bdd cube = bdd_satone(trans_set_left_); - trans_set_left_ &= !cube; - // Let this cube grow as much as possible. - // (e.g., cube "(!a)&b" taken from "a | (!a)&b" can - // be simplified to "b"). - cube = bdd_simplify(cube, cube | neg_trans_set_); - // Complete with the destination. - current_ = cube & trans_dest_; - + assert(current_ != bddfalse); // The destination state, computed here, should be compatible // with the transition relation. Otherwise it won't have any // successor (a dead node) and we can skip it. We need to // compute current_state_ anyway, so this test costs us nothing. - current_state_ = bdd_replace(bdd_exist(current_, data_.notnext_set), - data_.next_to_now); + assert(dest == bdd_exist(current_, data_.notnext_set)); + current_state_ = bdd_replace(dest, data_.next_to_now); } while ((current_state_ & data_.relation) == bddfalse); } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index e87bde0c2..8b18389d0 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -38,10 +38,6 @@ namespace spot const tgba_bdd_core_data& data_; ///< Core data of the automaton. bdd succ_set_; ///< The set of successors. bdd succ_set_left_; ///< Unexplored successors (including current_). - bdd trans_dest_; ///< Destination state of currently explored subset - bdd trans_set_; ///< Set of successors with the same destination. - bdd neg_trans_set_; ///< Negation of trans_set_. - bdd trans_set_left_;///< Part of trans_set_ not yet explored. bdd current_; ///< \brief Current successor, as a conjunction of /// atomic proposition and Next variables. bdd current_state_; ///< \brief Current successor, as a