From dfe74f31343e7b0ccdf66afc9a7a77dd222f9608 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 Jul 2003 13:19:19 +0000 Subject: [PATCH] Rewrite tgba_succ_iterator_concrete::next for the fourth time (or is it the fifth?). * 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_): New attributes. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize new members. (tgba_succ_iterator_concrete::first): Likewise. (tgba_succ_iterator_concrete::next): Rewrite. * tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle acc_set. --- ChangeLog | 19 ++++ src/tgba/succiterconcrete.cc | 146 +++++++++++++++++++++------- src/tgba/succiterconcrete.hh | 12 ++- src/tgba/tgbabddcoredata.cc | 4 + src/tgba/tgbabddcoredata.hh | 5 +- src/tgba/tgbabddtranslatefactory.cc | 2 + 6 files changed, 147 insertions(+), 41 deletions(-) diff --git a/ChangeLog b/ChangeLog index cb946aea9..facb6d92e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,22 @@ +2003-07-02 Alexandre Duret-Lutz + + Rewrite tgba_succ_iterator_concrete::next for the fourth time + (or is it the fifth?). + + * 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_): New attributes. + * src/tgba/succiterconcrete.cc + (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize + new members. + (tgba_succ_iterator_concrete::first): Likewise. + (tgba_succ_iterator_concrete::next): Rewrite. + * tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute. + * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: + Handle acc_set. + 2003-07-01 Alexandre Duret-Lutz * src/tgba/tgbabddtranslatefactory.cc diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 2e5c9e270..b0fc7ac44 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -8,6 +8,9 @@ namespace spot : data_(d), succ_set_(successors), succ_set_left_(successors), + trans_dest_(bddfalse), + trans_set_(bddfalse), + trans_set_left_(bddfalse), current_(bddfalse) { } @@ -20,7 +23,9 @@ namespace spot tgba_succ_iterator_concrete::first() { succ_set_left_ = succ_set_; - current_ = bddfalse; + trans_dest_ = bddfalse; + trans_set_ = bddfalse; + trans_set_left_ = bddfalse; if (!done()) next(); } @@ -36,44 +41,113 @@ namespace spot // important constraint is that all Next variables must appear in // the satisfaction. // - // For instance if succ_set_ was - // Now[a] * !Now[b] * (c + d) * (Next[a] + Next[b]) - // we'd like to enumerate the following six transitions - // c * Next[a] * Next[b] - // c * Next[a] * !Next[b] - // c * !Next[a] * Next[b] - // d * Next[a] * Next[b] - // d * Next[a] * !Next[b] - // d * !Next[a] * Next[b] - // (We don't really care about the Now variables here.) - // - // Note: on this example it's ok to get something like - // c * Next[a] * Next[b] - // c * Next[a] * !Next[b] - // c * !Next[a] * Next[b] - // d * !c * Next[a] * Next[b] - // d * !c * Next[a] * !Next[b] - // d * !c * !Next[a] * Next[b] - // depending on the BDD order. It doesn't really matter. The important - // point is that we don't want to list all four possible 'c' and 'd' - // combinations. - // FIXME: This is not what we do now: we list all possible combinations - // of atomic propositions. + // The full satisfactions of succ_set_ maybe something + // like this (ignoring Now variables): + // a & b & Next[a] & Next[b] + // !a & b & Next[a] & Next[b] + // a & !b & Next[a] & Next[b] + // 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] + // Is this always correct? No! It depends on the + // accepting conditions associated to each transition. + // We cannot merge transitions which have different + // accepting conditions. + // Let's label transitions with hypothetic accepting sets: + // a & b & Next[a] & Next[b] ; Acc[1] + // !a & b & Next[a] & Next[b] ; Acc[2] + // a & !b & Next[a] & Next[b] ; Acc[2] + // a & b & Next[a] & !Next[b] ; Acc[1] + // Now it's pretty clear only the first two transitions + // may be merged: + // b & Next[a] & Next[b] ; Acc[1] + // a & !b & Next[a] & Next[b] ; Acc[2] + // a & b & Next[a] & !Next[b] ; Acc[1] - // 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 { - succ_set_left_ &= !current_; - if (succ_set_left_ == bddfalse) // No more successors? - return; - current_ = bdd_satoneset(succ_set_left_, - data_.varandnext_set, bddfalse); - // The destination state, computed here, should be - // compatible with the transition relation. Otherwise - // it won't have any successor (a dead node). + // 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_ &= !(trans_set_ & trans_dest_); + 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); + 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_.now_set & data_.next_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_.now_set & data_.next_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_; + } + + // 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_; + + // 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); } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 2e9d2837a..e87bde0c2 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -38,10 +38,14 @@ 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 current_; ///< Current successor, as a conjunction of - /// atomic proposition and Next variables. - bdd current_state_; ///< Current successor, as a - /// conjunction of Now variables. + 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 + /// conjunction of Now variables. }; } diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index eec363fa7..782510619 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -13,6 +13,7 @@ namespace spot var_set(bddtrue), notvar_set(bddtrue), varandnext_set(bddtrue), + acc_set(bddtrue), notacc_set(bddtrue), negacc_set(bddtrue), next_to_now(bdd_newpair()) @@ -30,6 +31,7 @@ namespace spot var_set(copy.var_set), notvar_set(copy.notvar_set), varandnext_set(copy.varandnext_set), + acc_set(copy.acc_set), notacc_set(copy.notacc_set), negacc_set(copy.negacc_set), next_to_now(bdd_copypair(copy.next_to_now)) @@ -50,6 +52,7 @@ namespace spot var_set(left.var_set & right.var_set), notvar_set(left.notvar_set & right.notvar_set), varandnext_set(left.varandnext_set & right.varandnext_set), + acc_set(left.acc_set & right.acc_set), notacc_set(left.notacc_set & right.notacc_set), negacc_set(left.negacc_set & right.negacc_set), next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now)) @@ -102,6 +105,7 @@ namespace spot notnow_set &= acc; notnext_set &= acc; notvar_set &= acc; + acc_set &= acc; negacc_set &= !acc; } } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 8fda345b5..a978c4b40 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -79,9 +79,12 @@ namespace spot /// \brief The (positive) conjunction of all variables which are /// not atomic propositions. bdd notvar_set; - /// \brief The (positive) conjunction of all Next variables + /// \brief The (positive) conjunction of all Next variables /// and atomic propositions. bdd varandnext_set; + /// \brief The (positive) conjunction of all variables which are + /// accepting conditions. + bdd acc_set; /// \brief The (positive) conjunction of all variables which are not /// accepting conditions. bdd notacc_set; diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index 6ae4bd976..0e6a6a410 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -22,7 +22,9 @@ namespace spot data_.notvar_set = bdd_replace(in.notvar_set, rewrite); data_.var_set = bdd_replace(in.var_set, rewrite); data_.varandnext_set = bdd_replace(in.varandnext_set, rewrite); + data_.acc_set = bdd_replace(in.acc_set, rewrite); data_.notacc_set = bdd_replace(in.notacc_set, rewrite); + data_.negacc_set = bdd_replace(in.negacc_set, rewrite); init_ = bdd_replace(from.get_init_bdd(), rewrite);