diff --git a/ChangeLog b/ChangeLog index 9bd0c2b40..ad1d99836 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,7 +1,21 @@ 2003-06-16 Alexandre Duret-Lutz + * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... + * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these. + (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ... + (tgba_product, tgba_product_succ_iterator): ... these, and adjust + all uses. + * src/tgba/tgbabddtranslateproxy.cc, + src/tgba/tgbabddtranslateproxy.hh: Rename as ... + * src/tgba/tgbatranslateproxy.cc, + src/tgba/tgbatranslateproxy.hh: ... these. + (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator): + Rename as ... + (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these, + and adjust all uses. + Make sure we can multiply two tgba_explicit. - + * tgba/state.hh (state::translate, state::clone, state::as_bdd): New virtual methods. * tgba/stataebdd.cc (state::translate, state::clone): New methods. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index e6d5dc387..531a75437 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -30,11 +30,11 @@ libtgba_la_SOURCES = \ tgbabdddict.cc \ tgbabdddict.hh \ tgbabddfactory.hh \ - tgbabddprod.cc \ - tgbabddprod.hh \ tgbabddtranslatefactory.cc \ tgbabddtranslatefactory.hh \ - tgbabddtranslateproxy.cc \ - tgbabddtranslateproxy.hh \ tgbaexplicit.cc \ - tgbaexplicit.hh + tgbaexplicit.hh \ + tgbaproduct.cc \ + tgbaproduct.hh \ + tgbatranslateproxy.cc \ + tgbatranslateproxy.hh diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 202534216..2ddbe2cc2 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -26,7 +26,7 @@ namespace spot /// /// If this state uses any BDD variable. This function /// should rewrite the variables according to \a rewrite. - /// This used by spot::tgbabddtranslateproxy. + /// This used by spot::tgba_translate_proxy. virtual void translate(bddPair* rewrite) { // This does nothing by default and is diff --git a/src/tgba/tgbabddprod.cc b/src/tgba/tgbaproduct.cc similarity index 74% rename from src/tgba/tgbabddprod.cc rename to src/tgba/tgbaproduct.cc index 4dd346e37..802f2f05d 100644 --- a/src/tgba/tgbabddprod.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,5 +1,5 @@ -#include "tgbabddprod.hh" -#include "tgbabddtranslateproxy.hh" +#include "tgbaproduct.hh" +#include "tgbatranslateproxy.hh" #include "dictunion.hh" #include @@ -33,15 +33,15 @@ namespace spot } //////////////////////////////////////////////////////////// - // tgba_bdd_product_succ_iterator + // tgba_product_succ_iterator - tgba_bdd_product_succ_iterator::tgba_bdd_product_succ_iterator + tgba_product_succ_iterator::tgba_product_succ_iterator (tgba_succ_iterator* left, tgba_succ_iterator* right) : left_(left), right_(right) { } - tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator() + tgba_product_succ_iterator::~tgba_product_succ_iterator() { delete left_; if (right_) @@ -49,7 +49,7 @@ namespace spot } void - tgba_bdd_product_succ_iterator::step_() + tgba_product_succ_iterator::step_() { left_->next(); if (left_->done()) @@ -60,7 +60,7 @@ namespace spot } void - tgba_bdd_product_succ_iterator::next_non_false_() + tgba_product_succ_iterator::next_non_false_() { while (!done()) { @@ -78,7 +78,7 @@ namespace spot } void - tgba_bdd_product_succ_iterator::first() + tgba_product_succ_iterator::first() { if (!right_) return; @@ -98,41 +98,41 @@ namespace spot } void - tgba_bdd_product_succ_iterator::next() + tgba_product_succ_iterator::next() { step_(); next_non_false_(); } bool - tgba_bdd_product_succ_iterator::done() + tgba_product_succ_iterator::done() { return !right_ || right_->done(); } state_bdd_product* - tgba_bdd_product_succ_iterator::current_state() + tgba_product_succ_iterator::current_state() { return new state_bdd_product(left_->current_state(), right_->current_state()); } bdd - tgba_bdd_product_succ_iterator::current_condition() + tgba_product_succ_iterator::current_condition() { return current_cond_; } - bdd tgba_bdd_product_succ_iterator::current_promise() + bdd tgba_product_succ_iterator::current_promise() { return left_->current_promise() & right_->current_promise(); } //////////////////////////////////////////////////////////// - // tgba_bdd_product + // tgba_product - tgba_bdd_product::tgba_bdd_product(const tgba& left, const tgba& right) + tgba_product::tgba_product(const tgba& left, const tgba& right) : dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict())) { // Translate the left automaton if needed. @@ -143,7 +143,7 @@ namespace spot } else { - left_ = new tgba_bdd_translate_proxy(left, dict_); + left_ = new tgba_translate_proxy(left, dict_); left_should_be_freed_ = true; } @@ -155,12 +155,12 @@ namespace spot } else { - right_ = new tgba_bdd_translate_proxy(right, dict_); + right_ = new tgba_translate_proxy(right, dict_); right_should_be_freed_ = true; } } - tgba_bdd_product::~tgba_bdd_product() + tgba_product::~tgba_product() { if (left_should_be_freed_) delete left_; @@ -169,31 +169,31 @@ namespace spot } state* - tgba_bdd_product::get_init_state() const + tgba_product::get_init_state() const { return new state_bdd_product(left_->get_init_state(), right_->get_init_state()); } - tgba_bdd_product_succ_iterator* - tgba_bdd_product::succ_iter(const state* state) const + tgba_product_succ_iterator* + tgba_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); + return new tgba_product_succ_iterator(li, ri); } const tgba_bdd_dict& - tgba_bdd_product::get_dict() const + tgba_product::get_dict() const { return dict_; } std::string - tgba_bdd_product::format_state(const state* state) const + tgba_product::format_state(const state* state) const { const state_bdd_product* s = dynamic_cast(state); assert(s); diff --git a/src/tgba/tgbabddprod.hh b/src/tgba/tgbaproduct.hh similarity index 80% rename from src/tgba/tgbabddprod.hh rename to src/tgba/tgbaproduct.hh index 7e1e84a21..b712bf686 100644 --- a/src/tgba/tgbabddprod.hh +++ b/src/tgba/tgbaproduct.hh @@ -1,5 +1,5 @@ -#ifndef SPOT_TGBA_TGBABDDPROD_HH -# define SPOT_TGBA_TGBABDDPROD_HH +#ifndef SPOT_TGBA_TGBAPRODUCT_HH +# define SPOT_TGBA_TGBAPRODUCT_HH #include "tgba.hh" #include "statebdd.hh" @@ -7,7 +7,7 @@ namespace spot { - /// \brief A state for spot::tgba_bdd_product. + /// \brief A state for spot::tgba_product. /// /// This state is in fact a pair of state: the state from the left /// automaton and that of the right. @@ -50,13 +50,13 @@ namespace spot /// \brief Iterate over the successors of a product computed on the fly. - class tgba_bdd_product_succ_iterator: public tgba_succ_iterator + class tgba_product_succ_iterator: public tgba_succ_iterator { public: - tgba_bdd_product_succ_iterator(tgba_succ_iterator* left, - tgba_succ_iterator* right); + tgba_product_succ_iterator(tgba_succ_iterator* left, + tgba_succ_iterator* right); - virtual ~tgba_bdd_product_succ_iterator(); + virtual ~tgba_product_succ_iterator(); // iteration void first(); @@ -82,20 +82,20 @@ namespace spot }; /// \brief A lazy product. (States are computed on the fly.) - class tgba_bdd_product : public tgba + class tgba_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); + tgba_product(const tgba& left, const tgba& right); - virtual ~tgba_bdd_product(); + virtual ~tgba_product(); virtual state* get_init_state() const; - virtual tgba_bdd_product_succ_iterator* + virtual tgba_product_succ_iterator* succ_iter(const state* state) const; virtual const tgba_bdd_dict& get_dict() const; @@ -112,4 +112,4 @@ namespace spot } -#endif // SPOT_TGBA_TGBABDDPROD_HH +#endif // SPOT_TGBA_TGBAPRODUCT_HH diff --git a/src/tgba/tgbabddtranslateproxy.cc b/src/tgba/tgbatranslateproxy.cc similarity index 65% rename from src/tgba/tgbabddtranslateproxy.cc rename to src/tgba/tgbatranslateproxy.cc index d1a51bf3b..7d0e42a96 100644 --- a/src/tgba/tgbabddtranslateproxy.cc +++ b/src/tgba/tgbatranslateproxy.cc @@ -1,46 +1,45 @@ -#include "tgbabddtranslateproxy.hh" +#include "tgbatranslateproxy.hh" #include "bddprint.hh" #include namespace spot { - // tgba_bdd_translate_proxy_succ_iterator + // tgba_translate_proxy_succ_iterator // -------------------------------------- - tgba_bdd_translate_proxy_succ_iterator:: - tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator* it, - bddPair* rewrite) + tgba_translate_proxy_succ_iterator:: + tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it, + bddPair* rewrite) : iter_(it), rewrite_(rewrite) { } - tgba_bdd_translate_proxy_succ_iterator:: - ~tgba_bdd_translate_proxy_succ_iterator() + tgba_translate_proxy_succ_iterator::~tgba_translate_proxy_succ_iterator() { delete iter_; } void - tgba_bdd_translate_proxy_succ_iterator::first() + tgba_translate_proxy_succ_iterator::first() { iter_->first(); } void - tgba_bdd_translate_proxy_succ_iterator::next() + tgba_translate_proxy_succ_iterator::next() { iter_->next(); } bool - tgba_bdd_translate_proxy_succ_iterator::done() + tgba_translate_proxy_succ_iterator::done() { return iter_->done(); } state* - tgba_bdd_translate_proxy_succ_iterator::current_state() + tgba_translate_proxy_succ_iterator::current_state() { state* s = iter_->current_state(); s->translate(rewrite_); @@ -48,23 +47,23 @@ namespace spot } bdd - tgba_bdd_translate_proxy_succ_iterator::current_condition() + tgba_translate_proxy_succ_iterator::current_condition() { return bdd_replace(iter_->current_condition(), rewrite_); } bdd - tgba_bdd_translate_proxy_succ_iterator::current_promise() + tgba_translate_proxy_succ_iterator::current_promise() { return bdd_replace(iter_->current_promise(), rewrite_); } - // tgba_bdd_translate_proxy + // tgba_translate_proxy // ------------------------ - tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from, - const tgba_bdd_dict& to) + tgba_translate_proxy::tgba_translate_proxy(const tgba& from, + const tgba_bdd_dict& to) : from_(from), to_(to) { const tgba_bdd_dict& f = from.get_dict(); @@ -99,40 +98,40 @@ namespace spot } } - tgba_bdd_translate_proxy::~tgba_bdd_translate_proxy() + tgba_translate_proxy::~tgba_translate_proxy() { bdd_freepair(rewrite_from_); bdd_freepair(rewrite_to_); } state* - tgba_bdd_translate_proxy::get_init_state() const + tgba_translate_proxy::get_init_state() const { state* s = from_.get_init_state(); s->translate(rewrite_to_); return s; } - tgba_bdd_translate_proxy_succ_iterator* - tgba_bdd_translate_proxy::succ_iter(const state* s) const + tgba_translate_proxy_succ_iterator* + tgba_translate_proxy::succ_iter(const state* s) const { state* s2 = s->clone(); s2->translate(rewrite_from_); - tgba_bdd_translate_proxy_succ_iterator *res = - new tgba_bdd_translate_proxy_succ_iterator(from_.succ_iter(s2), + tgba_translate_proxy_succ_iterator *res = + new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2), rewrite_to_); delete s2; return res; } const tgba_bdd_dict& - tgba_bdd_translate_proxy::get_dict() const + tgba_translate_proxy::get_dict() const { return to_; } std::string - tgba_bdd_translate_proxy::format_state(const state* s) const + tgba_translate_proxy::format_state(const state* s) const { state* s2 = s->clone(); s2->translate(rewrite_from_); diff --git a/src/tgba/tgbabddtranslateproxy.hh b/src/tgba/tgbatranslateproxy.hh similarity index 65% rename from src/tgba/tgbabddtranslateproxy.hh rename to src/tgba/tgbatranslateproxy.hh index ffb2488fa..14a54878a 100644 --- a/src/tgba/tgbabddtranslateproxy.hh +++ b/src/tgba/tgbatranslateproxy.hh @@ -1,5 +1,5 @@ -#ifndef SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH -# define SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH +#ifndef SPOT_TGBA_TGBATRANSLATEPROXY_HH +# define SPOT_TGBA_TGBATRANSLATEPROXY_HH #include "tgba.hh" @@ -7,12 +7,12 @@ 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 + class tgba_translate_proxy_succ_iterator: public tgba_succ_iterator { public: - tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator* it, - bddPair* rewrite); - virtual ~tgba_bdd_translate_proxy_succ_iterator(); + tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it, + bddPair* rewrite); + virtual ~tgba_translate_proxy_succ_iterator(); // iteration void first(); @@ -31,20 +31,20 @@ namespace spot /// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables /// on the fly. - class tgba_bdd_translate_proxy: public tgba + class tgba_translate_proxy: public tgba { public: /// \brief Constructor. /// \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); + tgba_translate_proxy(const tgba& from, + const tgba_bdd_dict& to); - virtual ~tgba_bdd_translate_proxy(); + virtual ~tgba_translate_proxy(); virtual state* get_init_state() const; - virtual tgba_bdd_translate_proxy_succ_iterator* + virtual tgba_translate_proxy_succ_iterator* succ_iter(const state* state) const; virtual const tgba_bdd_dict& get_dict() const; @@ -60,4 +60,4 @@ namespace spot } -#endif // SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH +#endif // SPOT_TGBA_TGBATRANSLATEPROXY_HH diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 4e20a0d6a..48f02286c 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -2,7 +2,7 @@ #include #include "tgba/ltl2tgba.hh" #include "tgba/tgbaexplicit.hh" -#include "tgba/tgbabddprod.hh" +#include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" #include "ltlast/allnodes.hh" @@ -33,7 +33,7 @@ main(int argc, char** argv) return 2; { - spot::tgba_bdd_product p(*a1, *a2); + spot::tgba_product p(*a1, *a2); spot::tgba_save_reachable(std::cout, p); } diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index c68075215..78915ad79 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -4,7 +4,7 @@ #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgba/ltl2tgba.hh" -#include "tgba/tgbabddprod.hh" +#include "tgba/tgbaproduct.hh" #include "tgba/tgbabddconcreteproduct.hh" #include "tgbaalgos/dotty.hh" @@ -46,7 +46,7 @@ main(int argc, char** argv) #ifdef BDD_CONCRETE_PRODUCT spot::tgba_bdd_concrete p = spot::product(a1, a2); #else - spot::tgba_bdd_product p(a1, a2); + spot::tgba_product p(a1, a2); #endif spot::dotty_reachable(std::cout, p);