From 11ecdf2b86cd9f8cdb1aa6f300e36dd84a7f8614 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Sat, 7 Nov 2009 15:50:45 +0100 Subject: [PATCH] * src/tgba/taa.cc, src/tgba/taa.hh: Speed up the cartesian product in taa_succ_iterator and allow multiple initial states in taa. * src/tgba/ltl2taa.cc: Remove temporary printing. --- ChangeLog | 6 +++ src/tgba/taa.cc | 92 ++++++++++++++++++++++++---------------- src/tgba/taa.hh | 23 +++++++++- src/tgbaalgos/ltl2taa.cc | 9 +--- 4 files changed, 84 insertions(+), 46 deletions(-) diff --git a/ChangeLog b/ChangeLog index 452509826..461d844bc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2009-11-07 Damien Lefortier + + * src/tgba/taa.cc, src/tgba/taa.hh: Speed up the cartesian product + in taa_succ_iterator and allow multiple initial states in taa. + * src/tgba/ltl2taa.cc: Remove temporary printing. + 2009-11-05 Alexandre Duret-Lutz Fix ltlcounter.test for VPATH builds and n > 2. diff --git a/src/tgba/taa.cc b/src/tgba/taa.cc index 880c1113d..b24adb153 100644 --- a/src/tgba/taa.cc +++ b/src/tgba/taa.cc @@ -21,6 +21,7 @@ #include #include +#include #include #include "ltlvisit/destroy.hh" #include "tgba/formula2bdd.hh" @@ -61,7 +62,15 @@ namespace spot void taa::set_init_state(const std::string& s) { - init_ = add_state(s); + std::vector v; + v.push_back(s); + set_init_state(v); + } + + void + taa::set_init_state(const std::vector& s) + { + init_ = add_state_set(s); } taa::transition* @@ -141,9 +150,7 @@ namespace spot state* taa::get_init_state() const { - taa::state_set* s = new taa::state_set; - s->insert(init_); - return new spot::state_set(s); + return new spot::state_set(init_); } tgba_succ_iterator* @@ -233,12 +240,6 @@ namespace spot taa::state* s = new taa::state; name_state_map_[name] = s; state_name_map_[s] = name; - - // The first state we add is the inititial state. - // It can also be overridden with set_init_state(). - if (!init_) - init_ = s; - return s; } return i->second; @@ -352,13 +353,18 @@ namespace spot return; } - std::vector pos; - std::vector > bounds; + bounds_t bounds; for (taa::state_set::const_iterator i = s->begin(); i != s->end(); ++i) - { - pos.push_back((*i)->begin()); bounds.push_back(std::make_pair((*i)->begin(), (*i)->end())); - } + + /// Sorting might make the cartesian product faster by not + /// exploring all possibilities. + std::sort(bounds.begin(), bounds.end(), distance_sort()); + + std::vector pos; + pos.reserve(bounds.size()); + for (bounds_t::const_iterator i = bounds.begin(); i != bounds.end(); ++i) + pos.push_back(i->first); while (pos[0] != bounds[0].second) { @@ -366,39 +372,50 @@ namespace spot t->condition = bddtrue; t->acceptance_conditions = bddfalse; taa::state_set* ss = new taa::state_set; - for (unsigned i = 0; i < pos.size(); ++i) + + unsigned p; + for (p = 0; p < pos.size() && t->condition != bddfalse; ++p) { taa::state_set::const_iterator j; - for (j = (*pos[i])->dst->begin(); j != (*pos[i])->dst->end(); ++j) - if ((*j)->size() > 0) // Remove well states. + for (j = (*pos[p])->dst->begin(); j != (*pos[p])->dst->end(); ++j) + if ((*j)->size() > 0) // Remove sink states. ss->insert(*j); // Fill the new transition. t->dst = ss; - t->condition &= (*pos[i])->condition; - t->acceptance_conditions |= (*pos[i])->acceptance_conditions; + t->condition &= (*pos[p])->condition; + t->acceptance_conditions |= (*pos[p])->acceptance_conditions; } - // Look for another transition to merge with. + // If p != pos.size() we have found a contradiction + assert(p > 0); + + // If no contradiction, then look for another transition to + // merge with the new one. seen_map::iterator i; - for (i = seen_.find(*ss); i != seen_.end(); ++i) + if (t->condition != bddfalse) { - if (*i->second->dst == *t->dst - && i->second->condition == t->condition) + for (i = seen_.find(ss); i != seen_.end(); ++i) { - i->second->acceptance_conditions &= t->acceptance_conditions; - break; - } - if (*i->second->dst == *t->dst - && i->second->acceptance_conditions == t->acceptance_conditions) - { - i->second->condition |= t->condition; - break; + if (*i->second->dst == *t->dst + && i->second->condition == t->condition) + { + i->second->acceptance_conditions &= t->acceptance_conditions; + break; + } + if (*i->second->dst == *t->dst + && i->second->acceptance_conditions == t->acceptance_conditions) + { + i->second->condition |= t->condition; + break; + } } } - // Mark this transition as seen and keep it, or delete it. - if (i == seen_.end() && t->condition != bddfalse) + // Mark the new transition as seen and keep it if we have not + // found any contraction and no other transition to merge with, + // or delete it otherwise. + if (t->condition != bddfalse && i == seen_.end()) { - seen_.insert(std::make_pair(*ss, t)); + seen_.insert(std::make_pair(ss, t)); succ_.push_back(t); } else @@ -409,8 +426,9 @@ namespace spot for (int i = pos.size() - 1; i >= 0; --i) { - if (std::distance(pos[i], bounds[i].second) > 1 || - (i == 0 && std::distance(pos[i], bounds[i].second) == 1)) + if ((i < int(p)) + && (std::distance(pos[i], bounds[i].second) > 1 + || (i == 0 && std::distance(pos[i], bounds[i].second) == 1))) { ++pos[i]; break; diff --git a/src/tgba/taa.hh b/src/tgba/taa.hh index 6c6671ee9..a217492d7 100644 --- a/src/tgba/taa.hh +++ b/src/tgba/taa.hh @@ -51,6 +51,7 @@ namespace spot }; void set_init_state(const std::string& state); + void set_init_state(const std::vector& state); transition* create_transition(const std::string& src, @@ -106,7 +107,7 @@ namespace spot mutable bdd all_acceptance_conditions_; mutable bool all_acceptance_conditions_computed_; bdd neg_acceptance_conditions_; - taa::state* init_; + taa::state_set* init_; ss_vec state_set_vec_; private: @@ -167,8 +168,26 @@ namespace spot virtual bdd current_acceptance_conditions() const; private: + /// Those typedefs are used to generate all possible successors in + /// the constructor using a cartesian product. typedef taa::state::const_iterator iterator; - typedef std::multimap seen_map; + typedef std::pair iterator_pair; + typedef std::vector bounds_t; + typedef Sgi::hash_multimap< + const taa::state_set*, taa::transition*, ptr_hash + > seen_map; + + struct distance_sort : + public std::binary_function + { + bool + operator()(const iterator_pair& lhs, const iterator_pair& rhs) const + { + return std::distance(lhs.first, lhs.second) < + std::distance(rhs.first, rhs.second); + } + }; std::vector::const_iterator i_; std::vector succ_; diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index fa11749d6..65951a69f 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -74,7 +74,7 @@ namespace spot init_ = to_string(f); std::vector dst; - dst.push_back(std::string("well")); + dst.push_back(std::string("sink")); taa::transition* t = res_->create_transition(init_, dst); res_->add_condition(t, clone(f)); succ_state ss = { dst, f, constant::true_instance() }; @@ -90,7 +90,7 @@ namespace spot { case constant::True: { - dst.push_back(std::string("well")); + dst.push_back(std::string("sink")); res_->create_transition(init_, dst); succ_state ss = { dst, node, constant::true_instance() }; succ_.push_back(ss); @@ -383,8 +383,6 @@ namespace spot const ltl::formula* f2 = ltl::negative_normal_form(f1); ltl::destroy(f1); - std::cerr << ltl::to_string(f2) << std::endl; - spot::taa* res = new spot::taa(dict); language_containment_checker* lcc = new language_containment_checker(dict, false, false, false, false); @@ -393,9 +391,6 @@ namespace spot ltl::destroy(f2); delete lcc; - // TODO: temporary. - res->output(std::cerr); - return v.result(); } }