diff --git a/ChangeLog b/ChangeLog index e21ac3f57..5495b22d2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-05-28 Alexandre Duret-Lutz + + * src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant. + * src/tgba/tgbabddtranslateproxy.cc, + src/tgba/tgbabddtranslateproxy.hh: New files. + * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. + 2003-05-27 Alexandre Duret-Lutz * src/tgba/bddprint.cc, src/tgba/bddprint.hh, @@ -8,8 +15,8 @@ src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc: Add Doxygen comments. - * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, - src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, + * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, + src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add Doxygen comments. @@ -18,7 +25,7 @@ * src/tgba/state.hh: Add Doxygen comments. (state::compare): Take a state*, not a state&. (state_ptr_less_than): New functor. - * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a + * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a state&. * src/tgba/statebdd.cc (state_bdd::compare): Likewise. * src/tgba/succiter.hh: Add Doxygen comments. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index b7d44e091..1e17d6d4d 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -31,4 +31,6 @@ libtgba_la_SOURCES = \ tgbabdddict.hh \ tgbabddfactory.hh \ tgbabddtranslatefactory.cc \ - tgbabddtranslatefactory.hh + tgbabddtranslatefactory.hh \ + tgbabddtranslateproxy.cc \ + tgbabddtranslateproxy.hh diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index 2f508c374..2a4e970e0 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.hh @@ -16,12 +16,19 @@ namespace spot } /// Return the BDD part of the state. - bdd + bdd as_bdd() const { return state_; } - + + /// Return the BDD part of the state. + bdd& + as_bdd() + { + return state_; + } + virtual int compare(const state* other) const; protected: diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 2e4b13f86..acdc1089a 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -12,7 +12,7 @@ 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 diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 18013f446..e68883f4e 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -77,7 +77,7 @@ namespace spot /// This formating is the responsability of the automata /// who owns the state. virtual std::string format_state(const state* state) const = 0; - }; + }; } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 1ea06c8e2..cf20b02af 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -15,7 +15,7 @@ namespace spot /// \li "Next" variables, that encode the destination state /// \li atomic propositions, which are things to verify before going on /// to the next state - /// \li promises: \c a \c U \c b, or \c F \cb, both imply that \c b + /// \li promises: \c a \c U \c b, or \c F \c b, both imply that \c b /// should be verified eventually. We encode this with \c Prom[b], /// and check that promises are fullfilled in the emptyness check. bdd relation; diff --git a/src/tgba/tgbabddtranslateproxy.cc b/src/tgba/tgbabddtranslateproxy.cc new file mode 100644 index 000000000..44e7f2546 --- /dev/null +++ b/src/tgba/tgbabddtranslateproxy.cc @@ -0,0 +1,137 @@ +#include "tgbabddtranslateproxy.hh" +#include "bddprint.hh" + +namespace spot +{ + + // tgba_bdd_translate_proxy_succ_iterator + // -------------------------------------- + + tgba_bdd_translate_proxy_succ_iterator:: + tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it, + bddPair* rewrite) + : iter_(it), rewrite_(rewrite) + { + } + + void + tgba_bdd_translate_proxy_succ_iterator::first() + { + iter_->first(); + } + + void + tgba_bdd_translate_proxy_succ_iterator::next() + { + iter_->next(); + } + + bool + tgba_bdd_translate_proxy_succ_iterator::done() + { + return iter_->done(); + } + + state_bdd* + tgba_bdd_translate_proxy_succ_iterator::current_state() + { + state_bdd* s = iter_->current_state(); + s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_); + return s; + } + + bdd + tgba_bdd_translate_proxy_succ_iterator::current_condition() + { + return bdd_replace(iter_->current_condition(), rewrite_); + } + + bdd + tgba_bdd_translate_proxy_succ_iterator::current_promise() + { + return bdd_replace(iter_->current_promise(), rewrite_); + } + + + // tgba_bdd_translate_proxy + // ------------------------ + + tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from, + const tgba_bdd_dict& to) + : from_(from), to_(to) + { + const tgba_bdd_dict& f = from.get_dict(); + rewrite_to_ = bdd_newpair(); + rewrite_from_ = bdd_newpair(); + + tgba_bdd_dict::fv_map::const_iterator i_from; + tgba_bdd_dict::fv_map::const_iterator i_to; + + for (i_from = f.now_map.begin(); i_from != f.now_map.end(); ++i_from) + { + i_to = to_.now_map.find(i_from->first); + assert(i_to != to_.now_map.end()); + bdd_setpair(rewrite_to_, i_from->second, i_to->second); + bdd_setpair(rewrite_to_, i_from->second + 1, i_to->second + 1); + bdd_setpair(rewrite_from_, i_to->second, i_from->second); + bdd_setpair(rewrite_from_, i_to->second + 1, i_from->second + 1); + } + for (i_from = f.var_map.begin(); i_from != f.var_map.end(); ++i_from) + { + i_to = to_.var_map.find(i_from->first); + assert(i_to != to_.var_map.end()); + bdd_setpair(rewrite_to_, i_from->second, i_to->second); + bdd_setpair(rewrite_from_, i_to->second, i_from->second); + } + for (i_from = f.prom_map.begin(); i_from != f.prom_map.end(); ++i_from) + { + i_to = to_.prom_map.find(i_from->first); + assert(i_to != to_.prom_map.end()); + bdd_setpair(rewrite_to_, i_from->second, i_to->second); + bdd_setpair(rewrite_from_, i_to->second, i_from->second); + } + } + + tgba_bdd_translate_proxy::~tgba_bdd_translate_proxy() + { + bdd_freepair(rewrite_from_); + bdd_freepair(rewrite_to_); + } + + state_bdd* + tgba_bdd_translate_proxy::get_init_state() const + { + state_bdd* s = dynamic_cast(from_.get_init_state()); + assert(s); + s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_to_); + return s; + } + + tgba_bdd_translate_proxy_succ_iterator* + tgba_bdd_translate_proxy::succ_iter(const state* state) const + { + const state_bdd* s = dynamic_cast(state); + assert(s); + state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_)); + tgba_succ_iterator_concrete* it = + dynamic_cast(from_.succ_iter(&s2)); + assert(it); + return new tgba_bdd_translate_proxy_succ_iterator(it, rewrite_to_); + } + + const tgba_bdd_dict& + tgba_bdd_translate_proxy::get_dict() const + { + return to_; + } + + std::string + tgba_bdd_translate_proxy::format_state(const state* state) const + { + const state_bdd* s = dynamic_cast(state); + assert(s); + return bdd_format_set(to_, s->as_bdd()); + } + + +} diff --git a/src/tgba/tgbabddtranslateproxy.hh b/src/tgba/tgbabddtranslateproxy.hh new file mode 100644 index 000000000..526a390a3 --- /dev/null +++ b/src/tgba/tgbabddtranslateproxy.hh @@ -0,0 +1,64 @@ +#ifndef SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH +# define SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH + +#include "tgba.hh" +#include "succiterconcrete.hh" + +namespace spot +{ + /// \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 + { + public: + tgba_bdd_translate_proxy_succ_iterator + (tgba_succ_iterator_concrete* it, bddPair* rewrite); + + // iteration + void first(); + void next(); + bool done(); + + // inspection + state_bdd* current_state(); + bdd current_condition(); + bdd current_promise(); + protected: + tgba_succ_iterator_concrete* iter_; + bddPair* rewrite_; + }; + + + /// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables + /// on the fly. + class tgba_bdd_translate_proxy: public tgba + { + public: + /// \brief Construcor. + /// \param from The spot::tgba to masquerade. + /// \param to The new dictionary to use. + 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* + 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; + + 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