diff --git a/ChangeLog b/ChangeLog index 81cdf4c41..9bd0c2b40 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,42 @@ +2003-06-16 Alexandre Duret-Lutz + + 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. + * tgba/stataebdd.hh (state::translate, state::clone): New methods. + * tgba/tgbabddprod.cc (state_bdd_product::clone, + tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): + New methods. + (tgba_bdd_product_succ_iterator::first): Reset right_ + if any of left_ or right_ is already done (i.e., is empty). + (tgba_bdd_product_succ_iterator::done): Return true + if right_ is NULL. + (tgba_bdd_product_succ_iterator::current_state, + tgba_bdd_product::get_init_state): Work directory with `state's. + * tgba/tgbabddprod.hh (state_bdd_product::clone, + tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): + New methods. + * tgba/tgbabddtranslateproxy.cc + (tgba_bdd_translate_proxy_succ_iterator:: + tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator. + (tgba_bdd_translate_proxy_succ_iterator:: + ~tgba_bdd_translate_proxy_succ_iterator): New method. + (tgba_bdd_translate_proxy_succ_iterator::current_state, + tgba_bdd_translate_proxy::get_init_state, + tgba_bdd_translate_proxy::succ_iter): Work on `state's and + `tgba_succ_iterator's directlry. + (tgba_bdd_translate_proxy::format_state): Delegate formating + to the proxied automata. + * tgba/tgbaexplicit.cc (state_explicit::clone): New method. + * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, + tgba_explicit::get_promise): Call ltl::destroy on existing formulae. + * tgbatest/Makefile.am (check_PROGRAMS): Add explprod. + (explprod_SOURCES): New variable. + (TESTS): Add explprod.test. + (CLEANFILES): Add input1 and input2. + 2003-06-12 Alexandre Duret-Lutz * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 608e6fb0c..202534216 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -22,6 +22,28 @@ namespace spot /// \sa spot::state_ptr_less_than virtual int compare(const state* other) const = 0; + /// \brief Translate a state. + /// + /// If this state uses any BDD variable. This function + /// should rewrite the variables according to \a rewrite. + /// This used by spot::tgbabddtranslateproxy. + virtual void translate(bddPair* rewrite) + { + // This does nothing by default and is + // overridden in spot::state_bdd. + (void) rewrite; + } + + /// Duplicate a state. + virtual state* clone() const = 0; + + /// Return the BDD part of the state. + virtual bdd + as_bdd() const + { + return bddtrue; + } + virtual ~state() { } diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc index 028eabb58..d6b623790 100644 --- a/src/tgba/statebdd.cc +++ b/src/tgba/statebdd.cc @@ -1,9 +1,10 @@ #include "statebdd.hh" -#include "bddprint.hh" +#include #include namespace spot { + int state_bdd::compare(const state* other) const { @@ -14,4 +15,18 @@ namespace spot assert(o); return o->as_bdd().id() - state_.id(); } + + void + state_bdd::translate(bddPair* rewrite) + { + state_ = bdd_replace(state_, rewrite); + } + + /// Duplicate a state. + state_bdd* + state_bdd::clone() const + { + return new state_bdd(*this); + } + } diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index 2a4e970e0..2927bd44c 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.hh @@ -16,20 +16,15 @@ namespace spot } /// Return the BDD part of the state. - bdd + virtual 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; + virtual void translate(bddPair* rewrite); + virtual state_bdd* clone() const; protected: bdd state_; ///< BDD representation of the state. diff --git a/src/tgba/tgbabddprod.cc b/src/tgba/tgbabddprod.cc index 73b74961d..4dd346e37 100644 --- a/src/tgba/tgbabddprod.cc +++ b/src/tgba/tgbabddprod.cc @@ -26,6 +26,12 @@ namespace spot return right_->compare(o->right()); } + state_bdd_product* + state_bdd_product::clone() const + { + return new state_bdd_product(*this); + } + //////////////////////////////////////////////////////////// // tgba_bdd_product_succ_iterator @@ -35,6 +41,13 @@ namespace spot { } + tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator() + { + delete left_; + if (right_) + delete right_; + } + void tgba_bdd_product_succ_iterator::step_() { @@ -67,8 +80,20 @@ namespace spot void tgba_bdd_product_succ_iterator::first() { + if (!right_) + return; + left_->first(); right_->first(); + // If one of the two successor set is empty initially, we reset + // right_, so that done() can detect this situation easily. (We + // choose to reset right_ because this variable is already used by + // done().) + if (left_->done() || right_->done()) + { + delete right_; + right_ = 0; + } next_non_false_(); } @@ -82,18 +107,15 @@ namespace spot bool tgba_bdd_product_succ_iterator::done() { - return right_->done(); + return !right_ || right_->done(); } - state_bdd* + state_bdd_product* 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); + return new state_bdd_product(left_->current_state(), + right_->current_state()); } bdd @@ -149,11 +171,8 @@ namespace spot 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); + return new state_bdd_product(left_->get_init_state(), + right_->get_init_state()); } tgba_bdd_product_succ_iterator* diff --git a/src/tgba/tgbabddprod.hh b/src/tgba/tgbabddprod.hh index 3bd034f82..7e1e84a21 100644 --- a/src/tgba/tgbabddprod.hh +++ b/src/tgba/tgbabddprod.hh @@ -7,7 +7,7 @@ namespace spot { - /// \brief A state for spot::tgba_bdd_product. + /// \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. @@ -19,32 +19,33 @@ namespace spot /// \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), + state_bdd_product(state* left, state* right) + : state_bdd(left->as_bdd() & right->as_bdd()), + left_(left), right_(right) { } - + virtual ~state_bdd_product(); - state_bdd* + state* left() const { return left_; } - state_bdd* + state* right() const { return right_; } virtual int compare(const state* other) const; + virtual state_bdd_product* clone() const; private: - state_bdd* left_; ///< State from the left automaton. - state_bdd* right_; ///< State from the right automaton. + state* left_; ///< State from the left automaton. + state* right_; ///< State from the right automaton. }; @@ -52,16 +53,18 @@ namespace spot class tgba_bdd_product_succ_iterator: public tgba_succ_iterator { public: - tgba_bdd_product_succ_iterator(tgba_succ_iterator* left, + tgba_bdd_product_succ_iterator(tgba_succ_iterator* left, tgba_succ_iterator* right); - + + virtual ~tgba_bdd_product_succ_iterator(); + // iteration void first(); void next(); bool done(); // inspection - state_bdd* current_state(); + state_bdd_product* current_state(); bdd current_condition(); bdd current_promise(); @@ -77,7 +80,7 @@ namespace spot tgba_succ_iterator* right_; bdd current_cond_; }; - + /// \brief A lazy product. (States are computed on the fly.) class tgba_bdd_product : public tgba { @@ -87,12 +90,12 @@ namespace spot /// \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* + virtual tgba_bdd_product_succ_iterator* succ_iter(const state* state) const; virtual const tgba_bdd_dict& get_dict() const; diff --git a/src/tgba/tgbabddtranslateproxy.cc b/src/tgba/tgbabddtranslateproxy.cc index 51d34764c..d1a51bf3b 100644 --- a/src/tgba/tgbabddtranslateproxy.cc +++ b/src/tgba/tgbabddtranslateproxy.cc @@ -9,12 +9,18 @@ namespace spot // -------------------------------------- tgba_bdd_translate_proxy_succ_iterator:: - tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it, + tgba_bdd_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() + { + delete iter_; + } + void tgba_bdd_translate_proxy_succ_iterator::first() { @@ -33,11 +39,11 @@ namespace spot return iter_->done(); } - state_bdd* + state* tgba_bdd_translate_proxy_succ_iterator::current_state() { - state_bdd* s = iter_->current_state(); - s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_); + state* s = iter_->current_state(); + s->translate(rewrite_); return s; } @@ -99,25 +105,24 @@ namespace spot bdd_freepair(rewrite_to_); } - state_bdd* + state* 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_); + 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* state) const + tgba_bdd_translate_proxy::succ_iter(const state* s) 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_); + 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), + rewrite_to_); + delete s2; + return res; } const tgba_bdd_dict& @@ -127,12 +132,13 @@ namespace spot } std::string - tgba_bdd_translate_proxy::format_state(const state* state) const + tgba_bdd_translate_proxy::format_state(const state* s) const { - const state_bdd* s = dynamic_cast(state); - assert(s); - return bdd_format_set(to_, s->as_bdd()); + state* s2 = s->clone(); + s2->translate(rewrite_from_); + std::string res = from_.format_state(s2); + delete s2; + return res; } - } diff --git a/src/tgba/tgbabddtranslateproxy.hh b/src/tgba/tgbabddtranslateproxy.hh index 5901995cb..ffb2488fa 100644 --- a/src/tgba/tgbabddtranslateproxy.hh +++ b/src/tgba/tgbabddtranslateproxy.hh @@ -2,7 +2,6 @@ # define SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH #include "tgba.hh" -#include "succiterconcrete.hh" namespace spot { @@ -11,8 +10,9 @@ namespace spot 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); + tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator* it, + bddPair* rewrite); + virtual ~tgba_bdd_translate_proxy_succ_iterator(); // iteration void first(); @@ -20,11 +20,11 @@ namespace spot bool done(); // inspection - state_bdd* current_state(); + state* current_state(); bdd current_condition(); bdd current_promise(); protected: - tgba_succ_iterator_concrete* iter_; + tgba_succ_iterator* iter_; bddPair* rewrite_; }; @@ -42,7 +42,7 @@ namespace spot virtual ~tgba_bdd_translate_proxy(); - virtual state_bdd* get_init_state() const; + virtual state* get_init_state() const; virtual tgba_bdd_translate_proxy_succ_iterator* succ_iter(const state* state) const; diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index f2ab0adae..4feab5c41 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,5 @@ #include "ltlast/atomic_prop.hh" +#include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" #include @@ -14,37 +15,37 @@ namespace spot { } - void + void tgba_explicit_succ_iterator::first() { i_ = s_->begin(); } - void + void tgba_explicit_succ_iterator::next() { ++i_; } - bool + bool tgba_explicit_succ_iterator::done() { return i_ == s_->end(); } - state_explicit* + state_explicit* tgba_explicit_succ_iterator::current_state() { return new state_explicit((*i_)->dest); } - bdd + bdd tgba_explicit_succ_iterator::current_condition() { return (*i_)->condition; } - bdd + bdd tgba_explicit_succ_iterator::current_promise() { return (*i_)->promise; @@ -54,7 +55,7 @@ namespace spot //////////////////////////////////////// // state_explicit - const tgba_explicit::state* + const tgba_explicit::state* state_explicit::get_state() const { return state_; @@ -68,6 +69,12 @@ namespace spot return o->get_state() - get_state(); } + state_explicit* + state_explicit::clone() const + { + return new state_explicit(*this); + } + //////////////////////////////////////// // tgba_explicit @@ -88,7 +95,7 @@ namespace spot delete i->second; } } - + tgba_explicit::state* tgba_explicit::add_state(const std::string& name) { @@ -109,7 +116,7 @@ namespace spot } tgba_explicit::transition* - tgba_explicit::create_transition(const std::string& source, + tgba_explicit::create_transition(const std::string& source, const std::string& dest) { tgba_explicit::state* s = add_state(source); @@ -135,6 +142,7 @@ namespace spot } else { + ltl::destroy(f); v = i->second; } return v; @@ -162,6 +170,7 @@ namespace spot } else { + ltl::destroy(f); v = i->second; } return v; @@ -177,27 +186,27 @@ namespace spot t->promise &= ! ithvar(get_promise(f)); } - state* + state* tgba_explicit::get_init_state() const { return new state_explicit(init_); } - tgba_succ_iterator* + tgba_succ_iterator* tgba_explicit::succ_iter(const spot::state* state) const { const state_explicit* s = dynamic_cast(state); assert(s); return new tgba_explicit_succ_iterator(s->get_state()); } - - const tgba_bdd_dict& + + const tgba_bdd_dict& tgba_explicit::get_dict() const { return dict_; } - std::string + std::string tgba_explicit::format_state(const spot::state* s) const { const state_explicit* se = dynamic_cast(s); diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 8583337d1..2b34dcebd 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -68,6 +68,8 @@ namespace spot virtual int compare(const spot::state* other) const; + virtual state_explicit* clone() const; + virtual ~state_explicit() { } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 5dbcb2cb4..afe587dba 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -24,7 +24,7 @@ namespace spot node = m.size() + 1; m[st] = node; - os << " " << node << " [label=\"" + os << " " << node << " [label=\"" << g.format_state(st) << "\"]" << std::endl; return true; } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 28140d1b0..49929a83c 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -9,11 +9,13 @@ check_PROGRAMS = \ tgbaread \ ltl2tgba \ ltlprod \ - bddprod + bddprod \ + explprod bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT explicit_SOURCES = explicit.cc +explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc readsave_SOURCES = readsave.cc @@ -25,8 +27,9 @@ TESTS = \ readsave.test \ ltl2tgba.test \ ltlprod.test \ - bddprod.test + bddprod.test \ + explprod.test EXTRA_DIST = $(TESTS) -CLEANFILES = input stdout expected +CLEANFILES = input input1 input2 stdout expected diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index dd980a845..679eb8b4f 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -6,10 +6,10 @@ int main() { - spot::ltl::default_environment& e = + spot::ltl::default_environment& e = spot::ltl::default_environment::instance(); spot::tgba_explicit a; - + typedef spot::tgba_explicit::transition trans; trans* t1 = a.create_transition("state 0", "state 1"); diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc new file mode 100644 index 000000000..4e20a0d6a --- /dev/null +++ b/src/tgbatest/explprod.cc @@ -0,0 +1,48 @@ +#include +#include +#include "tgba/ltl2tgba.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbabddprod.hh" +#include "tgbaparse/public.hh" +#include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " file1 file2" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 3) + syntax(argv[0]); + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel1; + spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env); + if (spot::format_tgba_parse_errors(std::cerr, pel1)) + return 2; + spot::tgba_parse_error_list pel2; + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + if (spot::format_tgba_parse_errors(std::cerr, pel1)) + return 2; + + { + spot::tgba_bdd_product p(*a1, *a2); + spot::tgba_save_reachable(std::cout, p); + } + + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::atomic_prop::instance_count() != 0); + delete a1; + delete a2; + assert(spot::ltl::atomic_prop::instance_count() == 0); + return exit_code; +} diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test new file mode 100755 index 000000000..8a091429b --- /dev/null +++ b/src/tgbatest/explprod.test @@ -0,0 +1,29 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input1 <input2 <expected < stdout + +cat stdout +diff stdout expected +rm input1 input2 stdout expected diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index ed094c60d..0077eb61d 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -33,7 +33,7 @@ main(int argc, char** argv) spot::tgba_parse_error_list pel; spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], pel, env, debug); - + exit_code = spot::format_tgba_parse_errors(std::cerr, pel);