From 6d0546c3174160829aae7366023d25966f88a422 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Jun 2003 15:15:30 +0000 Subject: [PATCH] * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... (succ_set_left_): ... this. (current_base_, current_base_left_): New variables. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first): Reset current_. (tgba_succ_iterator_concrete::next): Rewrite. (tgba_succ_iterator_concrete::current_state): Simplify. (tgba_succ_iterator_concrete::current_accepting_conditions): Remove atomic proposition with universal quantification. * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state): Complete the initial state. (tgba_bdd_concrete::succ_iter): Do not remove Now variable from the BDD passed to the iterator. * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update notnow_set and var_set. --- ChangeLog | 18 ++++ src/tgba/ltl2tgba.cc | 20 ++++- src/tgba/succiterconcrete.cc | 124 ++++++++++++++++++++++++---- src/tgba/succiterconcrete.hh | 27 ++++-- src/tgba/tgbabddconcrete.cc | 35 +++++++- src/tgba/tgbabddcoredata.cc | 12 ++- src/tgba/tgbabddcoredata.hh | 10 ++- src/tgba/tgbabddtranslatefactory.cc | 2 + 8 files changed, 216 insertions(+), 32 deletions(-) diff --git a/ChangeLog b/ChangeLog index e3b27eb93..cf4a95a4d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,23 @@ 2003-06-25 Alexandre Duret-Lutz + * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... + (succ_set_left_): ... this. + (current_base_, current_base_left_): New variables. + * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first): + Reset current_. + (tgba_succ_iterator_concrete::next): Rewrite. + (tgba_succ_iterator_concrete::current_state): Simplify. + (tgba_succ_iterator_concrete::current_accepting_conditions): Remove + atomic proposition with universal quantification. + * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula. + * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state): + Complete the initial state. + (tgba_bdd_concrete::succ_iter): Do not remove Now variable + from the BDD passed to the iterator. + * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables. + * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust + to update notnow_set and var_set. + * src/tgbatest/ltl2tgba.cc: Support -v. 2003-06-24 Alexandre Duret-Lutz diff --git a/src/tgba/ltl2tgba.cc b/src/tgba/ltl2tgba.cc index be45e7ade..c873035c3 100644 --- a/src/tgba/ltl2tgba.cc +++ b/src/tgba/ltl2tgba.cc @@ -1,5 +1,8 @@ #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" +#include "ltlvisit/lunabbrev.hh" +#include "ltlvisit/nenoform.hh" +#include "ltlvisit/destroy.hh" #include "tgbabddconcretefactory.hh" #include @@ -211,12 +214,23 @@ namespace spot tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f) { + // Normalize the formula. We want all the negation on + // the atomic proposition. We also suppress logic + // abbreviation such as <=>, =>, or XOR, since they + // would involve negations at the BDD level. + const ltl::formula* f1 = ltl::unabbreviate_logic(f); + const ltl::formula* f2 = ltl::negative_normal_form(f1); + ltl::destroy(f1); + + // Traverse the formula and draft the automaton in a factory. tgba_bdd_concrete_factory fact; ltl_trad_visitor v(fact); - f->accept(v); + f2->accept(v); + ltl::destroy(f2); fact.finish(); - tgba_bdd_concrete g(fact); - g.set_init_state(v.result()); + + // Finally setup the resulting automaton. + tgba_bdd_concrete g(fact, v.result()); return g; } } diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 3eed1813e..5ad11c290 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -5,8 +5,12 @@ namespace spot { tgba_succ_iterator_concrete::tgba_succ_iterator_concrete (const tgba_bdd_core_data& d, bdd successors) - : data_(d), succ_set_(successors), next_succ_set_(successors), - current_(bddfalse) + : data_(d), + succ_set_(successors), + succ_set_left_(successors), + current_(bddfalse), + current_base_(bddfalse), + current_base_left_(bddfalse) { } @@ -17,7 +21,8 @@ namespace spot void tgba_succ_iterator_concrete::first() { - next_succ_set_ = succ_set_; + succ_set_left_ = succ_set_; + current_ = bddfalse; if (!done()) next(); } @@ -26,28 +31,117 @@ namespace spot tgba_succ_iterator_concrete::next() { assert(!done()); + // succ_set_ is the set of successors we have to explore. it + // contains Now/Next variable and atomic propositions. Each + // satisfaction of succ_set_ represents a transition, and we want + // to compute as little transitions as possible. However one + // 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.) + // + // 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] + // 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. - // FIXME: Iterating on the successors this way (calling bdd_satone - // and NANDing out the result from the set) requires several descent - // of the BDD. Maybe it would be faster to compute all satisfying - // formula in one operation. - next_succ_set_ &= !current_; - current_ = bdd_satone(next_succ_set_); + // 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_; + } + 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); } bool tgba_succ_iterator_concrete::done() { - return next_succ_set_ == bddfalse; + return succ_set_left_ == bddfalse; } state_bdd* tgba_succ_iterator_concrete::current_state() { assert(!done()); - - return new state_bdd(bdd_replace(bdd_exist(current_, data_.notnext_set), - data_.next_to_now)); + return new state_bdd(current_state_); } bdd @@ -61,7 +155,9 @@ namespace spot tgba_succ_iterator_concrete::current_accepting_conditions() { assert(!done()); - return bdd_exist(bdd_restrict(data_.accepting_conditions, current_), + return bdd_exist(bdd_forall(bdd_restrict(data_.accepting_conditions, + current_), + data_.var_set), data_.notacc_set); } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index cbb5de91d..abe3b68c7 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -13,12 +13,14 @@ namespace spot public: /// \brief Build a spot::tgba_succ_iterator_concrete. /// - /// \param successors The set of successors with ingoing conditions - /// and promises, represented as a BDD. The job of this iterator - /// will be to enumerate the satisfactions of that BDD and split - /// them into destination state, conditions, and promises. - /// \param d The core data of the automata. These contains - /// sets of variables useful to split a BDD. + /// \param successors The set of successors with ingoing + /// 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. + /// 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); virtual ~tgba_succ_iterator_concrete(); @@ -33,10 +35,17 @@ namespace spot bdd current_accepting_conditions(); private: - const tgba_bdd_core_data& data_; ///< Core data of the automata. + const tgba_bdd_core_data& data_; ///< Core data of the automaton. bdd succ_set_; ///< The set of successors. - bdd next_succ_set_; ///< Unexplored successors (including current_). - bdd current_; ///< Current successor. + 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 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/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 0de57bc1c..0b68839c5 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -10,8 +10,9 @@ namespace spot } tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) - : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init) + : data_(fact.get_core_data()), dict_(fact.get_dict()) { + set_init_state(init); } tgba_bdd_concrete::~tgba_bdd_concrete() @@ -21,6 +22,36 @@ namespace spot void tgba_bdd_concrete::set_init_state(bdd s) { + // Usually, the ltl2tgba translator will return an + // initial state which does not include all true Now variables, + // even though the truth of some Now variables is garanteed. + // + // For instance, when building the automata for the formula GFa, + // the translator will define the following two equivalences + // Now[Fa] <=> a | (Prom[a] & Next[Fa]) + // Now[GFa] <=> Now[Fa] & Next[GFa] + // and return Now[GFa] as initial state. + // + // Starting for state Now[GFa], we could then build + // the following automaton: + // In state Now[GFa]: + // if `a', go to state Now[GFa] & Now[Fa] + // if `!a', go to state Now[GFa] & Now[Fa] with Prom[a] + // In state Now[GFa] & Now[Fa]: + // if `a', go to state Now[GFa] & Now[Fa] + // if `!a', go to state Now[GFa] & Now[Fa] with Prom[a] + // + // As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share + // the same actions. This is no surprise, because + // Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences + // defined by the translator. + // + // This happens because we haven't completed the initial + // state with the value of other Now variables. We can + // complete this state with the other equivalant Now variables + // here, but we can't do anything about the remaining unknown + // variables. + s &= bdd_relprod(s, data_.relation, data_.notnow_set); init_ = s; } @@ -41,7 +72,7 @@ namespace spot { const state_bdd* s = dynamic_cast(state); assert(s); - bdd succ_set = bdd_exist(data_.relation & s->as_bdd(), data_.now_set); + bdd succ_set = data_.relation & s->as_bdd(); return new tgba_succ_iterator_concrete(data_, succ_set); } diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 931a2ae1d..f56ba3a8f 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -4,7 +4,8 @@ namespace spot { tgba_bdd_core_data::tgba_bdd_core_data() : relation(bddtrue), accepting_conditions(bddfalse), - now_set(bddtrue), negnow_set(bddtrue), notnext_set(bddtrue), + now_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()) { @@ -13,7 +14,8 @@ namespace spot 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), - notnext_set(copy.notnext_set), notvar_set(copy.notvar_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)) { @@ -27,7 +29,9 @@ namespace spot | right.accepting_conditions), now_set(left.now_set & right.now_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), + var_set(left.var_set & right.var_set), notvar_set(left.notvar_set & right.notvar_set), notacc_set(left.notacc_set & right.notacc_set), negacc_set(left.negacc_set & right.negacc_set), @@ -57,6 +61,7 @@ namespace spot now_set &= now; negnow_set &= !now; notnext_set &= now; + notnow_set &= next; bdd both = now & next; notvar_set &= both; notacc_set &= both; @@ -65,13 +70,16 @@ namespace spot void tgba_bdd_core_data::declare_atomic_prop(bdd var) { + notnow_set &= var; notnext_set &= var; notacc_set &= var; + var_set &= var; } void tgba_bdd_core_data::declare_accepting_condition(bdd acc) { + notnow_set &= acc; notnext_set &= acc; notvar_set &= acc; negacc_set &= !acc; diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 11579905f..433b9f756 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -31,9 +31,9 @@ namespace spot /// in which a transition is. Actually we never return Acc[x] /// alone, but Acc[x] and all other accepting variables negated. /// - /// So if there is three accepting set \c a, \c b, and \c c, and + /// So if there is three accepting set \c a, \c b, and \c c, and /// a transition is in set \c a, we'll return \c Acc[a]&!Acc[b]&!Acc[c]. - /// If the transition is in both \c a and \c b, we'll return + /// If the transition is in both \c a and \c b, we'll return /// \c (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c (!Acc[a]\&Acc[b]\&!Acc[c]). /// /// Accepting conditions are attributed to transitions and are @@ -65,9 +65,15 @@ namespace spot /// The conjunction of all Now variables, in their negated form. bdd negnow_set; /// \brief The (positive) conjunction of all variables which are + /// not Now variables. + bdd notnow_set; + /// \brief The (positive) conjunction of all variables which are /// not Next variables. bdd notnext_set; /// \brief The (positive) conjunction of all variables which are + /// atomic propositions. + bdd var_set; + /// \brief The (positive) conjunction of all variables which are /// not atomic propositions. bdd notvar_set; /// The (positive) conjunction of all variables which are not diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index c1e4ab12e..d77d17718 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -16,8 +16,10 @@ namespace spot data_.accepting_conditions = bdd_replace(in.accepting_conditions, rewrite); data_.now_set = bdd_replace(in.now_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); data_.notvar_set = bdd_replace(in.notvar_set, rewrite); + data_.var_set = bdd_replace(in.var_set, rewrite); data_.notacc_set = bdd_replace(in.notacc_set, rewrite); init_ = bdd_replace(from.get_init_bdd(), rewrite);