diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 1e17d6d4d..c87fdbf2d 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -30,6 +30,8 @@ libtgba_la_SOURCES = \ tgbabdddict.cc \ tgbabdddict.hh \ tgbabddfactory.hh \ + tgbabddprod.cc \ + tgbabddprod.hh \ tgbabddtranslatefactory.cc \ tgbabddtranslatefactory.hh \ tgbabddtranslateproxy.cc \ diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 68972794b..f41727323 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -46,7 +46,7 @@ namespace spot { bdd_freepair(next_to_now); } - + void tgba_bdd_core_data::declare_now_next(bdd now, bdd next) { @@ -57,14 +57,14 @@ namespace spot notvar_set &= both; notprom_set &= both; } - + void tgba_bdd_core_data::declare_atomic_prop(bdd var) { notnow_set &= var; notprom_set &= var; } - + void tgba_bdd_core_data::declare_promise(bdd prom) { diff --git a/src/tgba/tgbabdddict.cc b/src/tgba/tgbabdddict.cc index b9e2db10c..32213b799 100644 --- a/src/tgba/tgbabdddict.cc +++ b/src/tgba/tgbabdddict.cc @@ -29,4 +29,30 @@ namespace spot } return os; } + + bool + tgba_bdd_dict::contains(const tgba_bdd_dict& other) const + { + fv_map::const_iterator i; + for (i = other.var_map.begin(); i != other.var_map.end(); ++i) + { + fv_map::const_iterator i2 = var_map.find(i->first); + if (i2 == var_map.end() || i->second != i2->second) + return false; + } + for (i = other.now_map.begin(); i != other.now_map.end(); ++i) + { + fv_map::const_iterator i2 = now_map.find(i->first); + if (i2 == now_map.end() || i->second != i2->second) + return false; + } + for (i = other.prom_map.begin(); i != other.prom_map.end(); ++i) + { + fv_map::const_iterator i2 = prom_map.find(i->first); + if (i2 == prom_map.end() || i->second != i2->second) + return false; + } + return true; + } + } diff --git a/src/tgba/tgbabdddict.hh b/src/tgba/tgbabdddict.hh index 20a4d4d56..9b4d6e199 100644 --- a/src/tgba/tgbabdddict.hh +++ b/src/tgba/tgbabdddict.hh @@ -26,6 +26,9 @@ namespace spot /// \brief Dump all variables for debugging. /// \param os The output stream. std::ostream& dump(std::ostream& os) const; + + /// Whether this dictionary contains \a other. + bool contains(const tgba_bdd_dict& other) const; }; } diff --git a/src/tgba/tgbabddprod.cc b/src/tgba/tgbabddprod.cc new file mode 100644 index 000000000..316420e91 --- /dev/null +++ b/src/tgba/tgbabddprod.cc @@ -0,0 +1,186 @@ +#include "tgbabddprod.hh" +#include "tgbabddtranslateproxy.hh" +#include "dictunion.hh" + +namespace spot +{ + + //////////////////////////////////////////////////////////// + // state_bdd_product + + state_bdd_product::~state_bdd_product() + { + delete left_; + delete right_; + } + + int + state_bdd_product::compare(const state* other) const + { + const state_bdd_product* o = dynamic_cast(other); + assert(o); + int res = left_->compare(o->left()); + if (res != 0) + return res; + return right_->compare(o->right()); + } + + //////////////////////////////////////////////////////////// + // tgba_bdd_product_succ_iterator + + tgba_bdd_product_succ_iterator::tgba_bdd_product_succ_iterator + (tgba_succ_iterator* left, tgba_succ_iterator* right) + : left_(left), right_(right) + { + } + + void + tgba_bdd_product_succ_iterator::step_() + { + left_->next(); + if (left_->done()) + { + left_->first(); + right_->next(); + } + } + + void + tgba_bdd_product_succ_iterator::next_non_false_() + { + while (!done()) + { + bdd l = left_->current_condition(); + bdd r = right_->current_condition(); + bdd current_cond = l & r; + + if (current_cond != bddfalse) + { + current_cond_ = current_cond; + return; + } + step_(); + } + } + + void + tgba_bdd_product_succ_iterator::first() + { + left_->first(); + right_->first(); + next_non_false_(); + } + + void + tgba_bdd_product_succ_iterator::next() + { + step_(); + next_non_false_(); + } + + bool + tgba_bdd_product_succ_iterator::done() + { + return right_->done(); + } + + + state_bdd* + tgba_bdd_product_succ_iterator::current_state() + { + state_bdd* ls = dynamic_cast(left_->current_state()); + state_bdd* rs = dynamic_cast(right_->current_state()); + assert(ls); + assert(rs); + return new state_bdd_product(ls, rs); + } + + bdd + tgba_bdd_product_succ_iterator::current_condition() + { + return current_cond_; + } + + bdd tgba_bdd_product_succ_iterator::current_promise() + { + return left_->current_promise() & right_->current_promise(); + } + + //////////////////////////////////////////////////////////// + // tgba_bdd_product + + tgba_bdd_product::tgba_bdd_product(const tgba& left, const tgba& right) + : dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict())) + { + // Translate the left automaton if needed. + if (dict_.contains(left.get_dict())) + { + left_ = &left; + left_should_be_freed_ = false; + } + else + { + left_ = new tgba_bdd_translate_proxy(left, dict_); + left_should_be_freed_ = true; + } + + // Translate the right automaton if needed. + if (dict_.contains(right.get_dict())) + { + right_ = &right; + right_should_be_freed_ = false; + } + else + { + right_ = new tgba_bdd_translate_proxy(right, dict_); + right_should_be_freed_ = true; + } + } + + tgba_bdd_product::~tgba_bdd_product() + { + if (left_should_be_freed_) + delete left_; + if (right_should_be_freed_) + delete right_; + } + + state* + tgba_bdd_product::get_init_state() const + { + state_bdd* ls = dynamic_cast(left_->get_init_state()); + state_bdd* rs = dynamic_cast(right_->get_init_state()); + assert(ls); + assert(rs); + return new state_bdd_product(ls, rs); + } + + tgba_bdd_product_succ_iterator* + tgba_bdd_product::succ_iter(const state* state) const + { + const state_bdd_product* s = dynamic_cast(state); + assert(s); + + tgba_succ_iterator* li = left_->succ_iter(s->left()); + tgba_succ_iterator* ri = right_->succ_iter(s->right()); + return new tgba_bdd_product_succ_iterator(li, ri); + } + + const tgba_bdd_dict& + tgba_bdd_product::get_dict() const + { + return dict_; + } + + std::string + tgba_bdd_product::format_state(const state* state) const + { + const state_bdd_product* s = dynamic_cast(state); + assert(s); + return (left_->format_state(s->left()) + + " * " + + right_->format_state(s->right())); + } + + +} diff --git a/src/tgba/tgbabddprod.hh b/src/tgba/tgbabddprod.hh new file mode 100644 index 000000000..3bd034f82 --- /dev/null +++ b/src/tgba/tgbabddprod.hh @@ -0,0 +1,112 @@ +#ifndef SPOT_TGBA_TGBABDDPROD_HH +# define SPOT_TGBA_TGBABDDPROD_HH + +#include "tgba.hh" +#include "statebdd.hh" + +namespace spot +{ + + /// \brief A state for spot::tgba_bdd_product. + /// + /// This state is in fact a pair of state: the state from the left + /// automaton and that of the right. + class state_bdd_product : public state_bdd + { + public: + /// \brief Constructor + /// \param left The state from the left automaton. + /// \param right The state from the right automaton. + /// These state are acquired by spot::state_bdd_product, and will + /// be deleted on destruction. + state_bdd_product(state_bdd* left, state_bdd* right) + : state_bdd(left->as_bdd() & right->as_bdd()), + left_(left), + right_(right) + { + } + + virtual ~state_bdd_product(); + + state_bdd* + left() const + { + return left_; + } + + state_bdd* + right() const + { + return right_; + } + + virtual int compare(const state* other) const; + + private: + state_bdd* left_; ///< State from the left automaton. + state_bdd* right_; ///< State from the right automaton. + }; + + + /// \brief Iterate over the successors of a product computed on the fly. + class tgba_bdd_product_succ_iterator: public tgba_succ_iterator + { + public: + tgba_bdd_product_succ_iterator(tgba_succ_iterator* left, + tgba_succ_iterator* right); + + // iteration + void first(); + void next(); + bool done(); + + // inspection + state_bdd* current_state(); + bdd current_condition(); + bdd current_promise(); + + private: + //@{ + /// Internal routines to advance to the next successor. + void step_(); + void next_non_false_(); + //@} + + protected: + tgba_succ_iterator* left_; + tgba_succ_iterator* right_; + bdd current_cond_; + }; + + /// \brief A lazy product. (States are computed on the fly.) + class tgba_bdd_product : public tgba + { + public: + /// \brief Constructor. + /// \param left The left automata in the product. + /// \param right The right automata in the product. + /// Do not be fooled by these arguments: a product \emph is commutative. + tgba_bdd_product(const tgba& left, const tgba& right); + + virtual ~tgba_bdd_product(); + + virtual state* get_init_state() const; + + virtual tgba_bdd_product_succ_iterator* + succ_iter(const state* state) const; + + virtual const tgba_bdd_dict& get_dict() const; + + virtual std::string format_state(const state* state) const; + + private: + const tgba* left_; + bool left_should_be_freed_; + const tgba* right_; + bool right_should_be_freed_; + tgba_bdd_dict dict_; + }; + +} + +#endif // SPOT_TGBA_TGBABDDPROD_HH diff --git a/src/tgba/tgbabddtranslateproxy.hh b/src/tgba/tgbabddtranslateproxy.hh index 526a390a3..5901995cb 100644 --- a/src/tgba/tgbabddtranslateproxy.hh +++ b/src/tgba/tgbabddtranslateproxy.hh @@ -6,7 +6,7 @@ namespace spot { - /// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber + /// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber /// BDD variables on the fly. class tgba_bdd_translate_proxy_succ_iterator: public tgba_succ_iterator { @@ -34,31 +34,30 @@ namespace spot class tgba_bdd_translate_proxy: public tgba { public: - /// \brief Construcor. + /// \brief Constructor. /// \param from The spot::tgba to masquerade. /// \param to The new dictionary to use. - tgba_bdd_translate_proxy(const tgba& from, + tgba_bdd_translate_proxy(const tgba& from, const tgba_bdd_dict& to); virtual ~tgba_bdd_translate_proxy(); virtual state_bdd* get_init_state() const; - virtual tgba_bdd_translate_proxy_succ_iterator* + virtual tgba_bdd_translate_proxy_succ_iterator* succ_iter(const state* state) const; virtual const tgba_bdd_dict& get_dict() const; - virtual std::string - tgba_bdd_translate_proxy::format_state(const state* state) const; - + virtual std::string format_state(const state* state) const; + private: const tgba& from_; ///< The spot::tgba to masquerade. tgba_bdd_dict to_; ///< The new dictionar to use. bddPair* rewrite_to_; ///< The rewriting pair for from->to. bddPair* rewrite_from_; ///< The rewriting pair for to->from. }; - + } #endif // SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH