From 7ce27ef994066c7c5b73ef0fb45ed2f711672501 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Thu, 22 Oct 2009 14:37:30 +0200 Subject: [PATCH] Improve ltl_to_taa. * src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not on-the-fly anymore allowing some redundant transitions to be removed. Also a new function to output a TAA. * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the refined rules from Tauriainen. * src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in ltl_to_taa. * src/tgbatest/spotlbtt.test: More tests. --- ChangeLog | 15 ++- src/tgba/taa.cc | 213 +++++++++++++++++++++++-------------- src/tgba/taa.hh | 19 ++-- src/tgbaalgos/ltl2taa.cc | 139 ++++++++++++++++++------ src/tgbaalgos/ltl2taa.hh | 4 +- src/tgbatest/ltl2tgba.cc | 5 +- src/tgbatest/spotlbtt.test | 18 +++- 7 files changed, 289 insertions(+), 124 deletions(-) diff --git a/ChangeLog b/ChangeLog index bec88f39f..80bdf8c72 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2009-10-22 Damien Lefortier + + Improve ltl_to_taa. + + * src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not + on-the-fly anymore allowing some redundant transitions to be + removed. Also a new function to output a TAA. + * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the + refined rules from Tauriainen. + * src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in + ltl_to_taa. + * src/tgbatest/spotlbtt.test: More tests. + 2009-10-17 Damien Lefortier Fix make check in sanity. @@ -23,7 +36,7 @@ * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: The algortihm. * src/tgbaalgos/Makefile.am: Adjust. - * src/tgbatest/ltl2tgba: New option: -taa, which uses this new + * src/tgbatest/ltl2tgba.cc: New option: -taa, which uses this new translation algorithm. * src/tgbatest/spotlbtt.test: Add ltl2tgba -taa. diff --git a/src/tgba/taa.cc b/src/tgba/taa.cc index a6febf380..880c1113d 100644 --- a/src/tgba/taa.cc +++ b/src/tgba/taa.cc @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include #include #include "ltlvisit/destroy.hh" @@ -120,6 +121,23 @@ namespace spot t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v); } + void + taa::output(std::ostream& os) const + { + ns_map::const_iterator i; + for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + { + taa::state::const_iterator i2; + os << "State: " << i->first << std::endl; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + { + os << " " << format_state_set((*i2)->dst) + << ", C:" << (*i2)->condition + << ", A:" << (*i2)->acceptance_conditions << std::endl; + } + } + } + state* taa::get_init_state() const { @@ -153,30 +171,7 @@ namespace spot const spot::state_set* se = dynamic_cast(s); assert(se); const state_set* ss = se->get_state(); - - state_set::const_iterator i1 = ss->begin(); - sn_map::const_iterator i2; - if (ss->empty()) - return std::string("{}"); - if (ss->size() == 1) - { - i2 = state_name_map_.find(*i1); - assert(i2 != state_name_map_.end()); - return i2->second; - } - else - { - std::string res("{"); - while (i1 != ss->end()) - { - i2 = state_name_map_.find(*i1++); - assert(i2 != state_name_map_.end()); - res += i2->second; - res += ","; - } - res[res.size() - 1] = '}'; - return res; - } + return format_state_set(ss); } bdd @@ -259,6 +254,34 @@ namespace spot return ss; } + std::string + taa::format_state_set(const taa::state_set* ss) const + { + state_set::const_iterator i1 = ss->begin(); + sn_map::const_iterator i2; + if (ss->empty()) + return std::string("{}"); + if (ss->size() == 1) + { + i2 = state_name_map_.find(*i1); + assert(i2 != state_name_map_.end()); + return "{" + i2->second + "}"; + } + else + { + std::string res("{"); + while (i1 != ss->end()) + { + i2 = state_name_map_.find(*i1++); + assert(i2 != state_name_map_.end()); + res += i2->second; + res += ","; + } + res[res.size() - 1] = '}'; + return res; + } + } + /*----------. | state_set | `----------*/ @@ -317,96 +340,130 @@ namespace spot `--------------*/ taa_succ_iterator::taa_succ_iterator(const taa::state_set* s, bdd all_acc) - : bounds_(), its_(), all_acceptance_conditions_(all_acc), - empty_(s->empty()) + : all_acceptance_conditions_(all_acc), seen_() { + if (s->empty()) + { + taa::transition* t = new taa::transition; + t->condition = bddtrue; + t->acceptance_conditions = bddfalse; + t->dst = new taa::state_set; + succ_.push_back(t); + return; + } + + std::vector pos; + std::vector > bounds; for (taa::state_set::const_iterator i = s->begin(); i != s->end(); ++i) { - bounds_.push_back(std::make_pair((*i)->begin(), (*i)->end())); - its_.push_back((*i)->begin()); + pos.push_back((*i)->begin()); + bounds.push_back(std::make_pair((*i)->begin(), (*i)->end())); } + + while (pos[0] != bounds[0].second) + { + taa::transition* t = new taa::transition; + t->condition = bddtrue; + t->acceptance_conditions = bddfalse; + taa::state_set* ss = new taa::state_set; + for (unsigned i = 0; i < pos.size(); ++i) + { + 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. + ss->insert(*j); + + // Fill the new transition. + t->dst = ss; + t->condition &= (*pos[i])->condition; + t->acceptance_conditions |= (*pos[i])->acceptance_conditions; + } + // Look for another transition to merge with. + seen_map::iterator i; + for (i = seen_.find(*ss); i != seen_.end(); ++i) + { + 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) + { + seen_.insert(std::make_pair(*ss, t)); + succ_.push_back(t); + } + else + { + delete t->dst; + delete t; + } + + 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)) + { + ++pos[i]; + break; + } + else + pos[i] = bounds[i].first; + } + } + } + + taa_succ_iterator::~taa_succ_iterator() + { + for (unsigned i = 0; i < succ_.size(); ++i) + delete succ_[i]; } void taa_succ_iterator::first() { - if (!done() && current_condition() == bddfalse) - next(); + i_ = succ_.begin(); } void taa_succ_iterator::next() { - if (empty_) - empty_ = false; - - do - { - for (unsigned i = 0; i < its_.size(); ++i) - { - if (std::distance(its_[i], bounds_[i].second) > 1) - { - ++its_[i]; - break; - } - else - { - if (i + 1 == its_.size()) - its_[0] = bounds_[0].second; // We are done. - else - its_[i] = bounds_[i].first; - } - } - } - while (!done() && current_condition() == bddfalse); + ++i_; } bool taa_succ_iterator::done() const { - if (empty_) - return false; - - for (unsigned i = 0; i < its_.size(); ++i) - if (its_[i] == bounds_[i].second) - return true; - return its_.empty() ? true : false; + return i_ == succ_.end(); } spot::state_set* taa_succ_iterator::current_state() const { assert(!done()); - taa::state_set::const_iterator i; - taa::state_set* res = new taa::state_set; - for (unsigned p = 0; p < its_.size(); ++p) - for (i = (*its_[p])->dst->begin(); i != (*its_[p])->dst->end(); ++i) - if ((*i)->size() > 0) // Remove well states. - res->insert(*i); - - return new spot::state_set(res); + return new spot::state_set((*i_)->dst); } bdd taa_succ_iterator::current_condition() const { assert(!done()); - bdd res = bddtrue; - for (unsigned i = 0; i < its_.size(); ++i) - res &= (*its_[i])->condition; - return res; + return (*i_)->condition; } bdd taa_succ_iterator::current_acceptance_conditions() const { - if (empty_) - return all_acceptance_conditions_; - assert(!done()); - bdd res = bddfalse; - for (unsigned i = 0; i < its_.size(); ++i) - res |= (*its_[i])->acceptance_conditions; - return all_acceptance_conditions_ - (res & all_acceptance_conditions_); + return all_acceptance_conditions_ - + ((*i_)->acceptance_conditions & all_acceptance_conditions_); } } diff --git a/src/tgba/taa.hh b/src/tgba/taa.hh index 70a66fdec..6c6671ee9 100644 --- a/src/tgba/taa.hh +++ b/src/tgba/taa.hh @@ -23,6 +23,7 @@ # define SPOT_TGBA_TAA_HH #include +#include #include #include "misc/hash.hh" #include "ltlast/formula.hh" @@ -60,6 +61,9 @@ namespace spot void add_condition(transition* t, const ltl::formula* f); void add_acceptance_condition(transition* t, const ltl::formula* f); + /// \brief Output a TAA. + void output(std::ostream& os) const; + /// TGBA interface. virtual ~taa(); virtual spot::state* get_init_state() const; @@ -117,6 +121,9 @@ namespace spot /// \brief Return the taa::state_set for \a names. taa::state_set* add_state_set(const std::vector& names); + + /// \brief Format a taa::state_set as a string for printing. + std::string format_state_set(const taa::state_set* ss) const; }; /// Set of states deriving from spot::state. @@ -149,10 +156,7 @@ namespace spot { public: taa_succ_iterator(const taa::state_set* s, bdd all_acc); - - virtual ~taa_succ_iterator() - { - } + virtual ~taa_succ_iterator(); virtual void first(); virtual void next(); @@ -164,11 +168,12 @@ namespace spot private: typedef taa::state::const_iterator iterator; + typedef std::multimap seen_map; - std::vector > bounds_; - std::vector its_; + std::vector::const_iterator i_; + std::vector succ_; bdd all_acceptance_conditions_; - mutable bool empty_; + seen_map seen_; }; } diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 68e628e49..fa11749d6 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -28,6 +28,7 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/clone.hh" +#include "ltlvisit/contain.hh" #include "ltl2taa.hh" namespace spot @@ -40,8 +41,10 @@ namespace spot class ltl2taa_visitor : public const_visitor { public: - ltl2taa_visitor(taa* res, bool negated = false) - : res_(res), negated_(negated), init_(), succ_(), to_free_() + ltl2taa_visitor(taa* res, language_containment_checker* lcc, + bool refined = false, bool negated = false) + : res_(res), refined_(refined), negated_(negated), + lcc_(lcc), init_(), succ_(), to_free_() { } @@ -74,8 +77,8 @@ namespace spot dst.push_back(std::string("well")); taa::transition* t = res_->create_transition(init_, dst); res_->add_condition(t, clone(f)); - - succ_.push_back(std::make_pair(dst, f)); + succ_state ss = { dst, f, constant::true_instance() }; + succ_.push_back(ss); } void @@ -86,10 +89,13 @@ namespace spot switch (node->val()) { case constant::True: + { dst.push_back(std::string("well")); res_->create_transition(init_, dst); - succ_.push_back(std::make_pair(dst, node)); + succ_state ss = { dst, node, constant::true_instance() }; + succ_.push_back(ss); return; + } case constant::False: return; } @@ -108,12 +114,16 @@ namespace spot switch (node->op()) { case unop::X: + { if (v.succ_.empty()) // Handle X(0) return; dst.push_back(v.init_); res_->create_transition(init_, dst); - succ_.push_back(std::make_pair(dst, constant::true_instance())); + succ_state ss = + { dst, constant::true_instance(), constant::true_instance() }; + succ_.push_back(ss); return; + } case unop::F: case unop::G: assert(0); // TBD @@ -139,44 +149,65 @@ namespace spot std::vector::iterator i1; std::vector::iterator i2; taa::transition* t = 0; + bool contained = false; switch (node->op()) { case binop::U: // Strong + if (refined_) + contained = lcc_->contained(node->second(), node->first()); for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) { - i1->first.push_back(init_); // Add the initial state - t = res_->create_transition(init_, i1->first); - res_->add_condition(t, clone(i1->second)); + // Refined rule + if (refined_ && contained) + i1->Q.erase + (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end()); + + i1->Q.push_back(init_); // Add the initial state + i1->acc = node; + t = res_->create_transition(init_, i1->Q); + res_->add_condition(t, clone(i1->condition)); res_->add_acceptance_condition(t, clone(node)); succ_.push_back(*i1); } for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) { - t = res_->create_transition(init_, i2->first); - res_->add_condition(t, clone(i2->second)); + t = res_->create_transition(init_, i2->Q); + res_->add_condition(t, clone(i2->condition)); succ_.push_back(*i2); } return; case binop::R: // Weak + if (refined_) + contained = lcc_->contained(node->first(), node->second()); for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) { for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) { std::vector u; // Union - std::copy(i1->first.begin(), i1->first.end(), ii(u, u.begin())); - std::copy(i2->first.begin(), i2->first.end(), ii(u, u.begin())); - const formula* f = multop::instance - (multop::And, clone(i1->second), clone(i2->second)); + std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.begin())); + formula* f = clone(i1->condition); // Refined rule + if (!refined_ || !contained) + { + std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.begin())); + f = multop::instance(multop::And, f, clone(i2->condition)); + } to_free_.push_back(f); t = res_->create_transition(init_, u); res_->add_condition(t, clone(f)); - succ_.push_back(std::make_pair(u, f)); + succ_state ss = { u, f, constant::true_instance() }; + succ_.push_back(ss); } - i2->first.push_back(init_); // Add the initial state - t = res_->create_transition(init_, i2->first); - res_->add_condition(t, clone(i2->second)); + if (refined_) // Refined rule + i2->Q.erase + (remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end()); + + i2->Q.push_back(init_); // Add the initial state + t = res_->create_transition(init_, i2->Q); + res_->add_condition(t, clone(i2->condition)); + if (refined_ && i2->acc != constant::true_instance()) + res_->add_acceptance_condition(t, clone(i2->acc)); succ_.push_back(*i2); } return; @@ -211,8 +242,35 @@ namespace spot std::vector p = all_n_tuples(vs); for (unsigned n = 0; n < p.size() && ok; ++n) { - t = res_->create_transition(init_, p[n].first); - res_->add_condition(t, clone(p[n].second)); + if (refined_) + { + std::vector v; // All sub initial states. + sort(p[n].Q.begin(), p[n].Q.end()); + for (unsigned m = 0; m < node->size(); ++m) + { + if (!binary_search(p[n].Q.begin(), p[n].Q.end(), vs[m].init_)) + break; + v.push_back(vs[m].init_); + } + + if (v.size() == node->size()) + { + std::vector Q; + sort(v.begin(), v.end()); + for (unsigned m = 0; m < p[n].Q.size(); ++m) + if (!binary_search(v.begin(), v.end(), p[n].Q[m])) + Q.push_back(p[n].Q[m]); + Q.push_back(init_); + t = res_->create_transition(init_, Q); + res_->add_condition(t, clone(p[n].condition)); + if (p[n].acc != constant::true_instance()) + res_->add_acceptance_condition(t, clone(p[n].acc)); + succ_.push_back(p[n]); + return; + } + } + t = res_->create_transition(init_, p[n].Q); + res_->add_condition(t, clone(p[n].condition)); succ_.push_back(p[n]); } return; @@ -221,8 +279,8 @@ namespace spot for (unsigned n = 0; n < node->size(); ++n) for (i = vs[n].succ_.begin(); i != vs[n].succ_.end(); ++i) { - t = res_->create_transition(init_, i->first); - res_->add_condition(t, clone(i->second)); + t = res_->create_transition(init_, i->Q); + res_->add_condition(t, clone(i->condition)); succ_.push_back(*i); } return; @@ -241,7 +299,7 @@ namespace spot ltl2taa_visitor recurse(const formula* f) { - ltl2taa_visitor v(res_, negated_); + ltl2taa_visitor v(res_, lcc_, refined_, negated_); f->accept(v); for (unsigned i = 0; i < v.to_free_.size(); ++i) to_free_.push_back(v.to_free_[i]); @@ -250,15 +308,20 @@ namespace spot private: taa* res_; + bool refined_; bool negated_; + language_containment_checker* lcc_; typedef std::insert_iterator< std::vector > ii; - typedef std::pair< - std::vector, const formula* - > succ_state; + struct succ_state + { + std::vector Q; // States + const formula* condition; + const formula* acc; + }; std::string init_; std::vector succ_; @@ -279,16 +342,20 @@ namespace spot { std::vector u; // Union formula* f = constant::true_instance(); + formula* a = constant::true_instance(); for (unsigned i = 0; i < vs.size(); ++i) { if (vs[i].succ_.empty()) continue; const succ_state& ss(vs[i].succ_[pos[i] - 1]); - std::copy(ss.first.begin(), ss.first.end(), ii(u, u.begin())); - f = multop::instance(multop::And, clone(ss.second), f); + std::copy(ss.Q.begin(), ss.Q.end(), ii(u, u.begin())); + f = multop::instance(multop::And, clone(ss.condition), f); + a = multop::instance(multop::And, clone(ss.acc), a); } to_free_.push_back(f); - product.push_back(std::make_pair(u, f)); + to_free_.push_back(a); + succ_state ss = { u, f, a }; + product.push_back(ss); for (int i = vs.size() - 1; i >= 0; --i) { @@ -309,7 +376,7 @@ namespace spot } // anonymous taa* - ltl_to_taa(const ltl::formula* f, bdd_dict* dict) + ltl_to_taa(const ltl::formula* f, bdd_dict* dict, bool refined_rules) { // TODO: s/unabbreviate_ltl/unabbreviate_logic/ const ltl::formula* f1 = ltl::unabbreviate_ltl(f); @@ -318,10 +385,16 @@ namespace spot std::cerr << ltl::to_string(f2) << std::endl; - taa* res = new spot::taa(dict); - ltl2taa_visitor v(res); + spot::taa* res = new spot::taa(dict); + language_containment_checker* lcc = + new language_containment_checker(dict, false, false, false, false); + ltl2taa_visitor v(res, lcc, refined_rules); f2->accept(v); ltl::destroy(f2); + delete lcc; + + // TODO: temporary. + res->output(std::cerr); return v.result(); } diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index 6f6928375..3b81a60bf 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -47,8 +47,10 @@ namespace spot /// /// \param f The formula to translate into an automaton. /// \param dict The spot::bdd_dict the constructed automata should use. + /// \param refined_rules If this parameter is set, refined rules are used. /// \return A spot::taa that recognizes the language of \a f. - taa* ltl_to_taa(const ltl::formula* f, bdd_dict* dict); + taa* ltl_to_taa(const ltl::formula* f, bdd_dict* dict, + bool refined_rules = false); } #endif // SPOT_TGBAALGOS_LTL2TAA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a5a95abed..82da391a5 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -232,7 +232,8 @@ main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-c")) { containment = true; - fm_opt = true; + if (!taa_opt) + fm_opt = true; } else if (!strcmp(argv[formula_index], "-d")) { @@ -592,7 +593,7 @@ main(int argc, char** argv) fm_red, containment); else if (taa_opt) - to_free = a = spot::ltl_to_taa(f, dict); + to_free = a = spot::ltl_to_taa(f, dict, containment); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 286566b51..491499b45 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -140,8 +140,6 @@ Algorithm Enabled = no } - - Algorithm { Name = "Spot (Couvreur -- FM), post reduction with direct simulation" @@ -270,6 +268,22 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Tauriainen -- TAA) pre reduction" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -taa -t -r7'" + Enabled = yes +} + +Algorithm +{ + Name = "Spot (Tauriainen -- TAA) pre reduction + refined rules" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -taa -t -r7 -c'" + Enabled = yes +} + GlobalOptions { Rounds = 100