diff --git a/ChangeLog b/ChangeLog index 898df995c..8a1741cab 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2009-10-16 Damien Lefortier + + Add a new algorithm (from Tauriainen) to translate LTL formulae to + TGBA which uses TAA as an intermediate representation. This is a + basic version, optimizations and enhancements will come later. + + * 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 + translation algorithm. + * src/tgbatest/spotlbtt.test: Add ltl2tgba -taa. + 2009-10-04 Damien Lefortier Add a class to represent Transition-based Alternating Automata (TAA). diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 56436b273..a5efe5e36 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -38,6 +38,7 @@ tgbaalgos_HEADERS = \ emptiness_stats.hh \ gv04.hh \ lbtt.hh \ + ltl2taa.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ @@ -69,6 +70,7 @@ libtgbaalgos_la_SOURCES = \ emptiness.cc \ gv04.cc \ lbtt.cc \ + ltl2taa.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc new file mode 100644 index 000000000..b5004bb07 --- /dev/null +++ b/src/tgbaalgos/ltl2taa.cc @@ -0,0 +1,328 @@ +// Copyright (C) 2009 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/lunabbrev.hh" +#include "ltlvisit/tunabbrev.hh" +#include "ltlvisit/nenoform.hh" +#include "ltlvisit/destroy.hh" +#include "ltlvisit/tostring.hh" +#include "ltlvisit/clone.hh" +#include "ltl2taa.hh" + +namespace spot +{ + namespace + { + using namespace ltl; + + /// \brief Recursively translate a formula into a TAA. + class ltl2taa_visitor : public const_visitor + { + public: + ltl2taa_visitor(taa* res, bool negated = false) + : res_(res), negated_(negated), init_(), succ_(), to_free_() + { + } + + virtual + ~ltl2taa_visitor() + { + } + + taa* + result() + { + for (unsigned i = 0; i < to_free_.size(); ++i) + destroy(to_free_[i]); + res_->set_init_state(init_); + return res_; + } + + void + visit(const atomic_prop* node) + { + const formula* f = node; // Handle negation + if (negated_) + { + f = unop::instance(unop::Not, clone(node)); + to_free_.push_back(f); + } + init_ = to_string(f); + std::vector dst; + + 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)); + } + + void + visit(const constant* node) + { + init_ = to_string(node); + std::vector dst; + 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)); + return; + case constant::False: + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const unop* node) + { + negated_ = node->op() == unop::Not; + ltl2taa_visitor v = recurse(node->child()); + + init_ = to_string(node); + std::vector dst; + switch (node->op()) + { + case unop::X: + if (v.succ_.size() == 0) // Handle X(0) + return; + dst.push_back(v.init_); + res_->create_transition(init_, dst); + succ_.push_back(std::make_pair(dst, constant::true_instance())); + return; + case unop::F: + case unop::G: + assert(0); // TBD + return; + case unop::Not: + // Done in recurse + succ_ = v.succ_; + return; + case unop::Finish: + assert(!"unsupported operator"); + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const binop* node) + { + ltl2taa_visitor v1 = recurse(node->first()); + ltl2taa_visitor v2 = recurse(node->second()); + + init_ = to_string(node); + std::vector::iterator i1; + std::vector::iterator i2; + taa::transition* t = 0; + switch (node->op()) + { + case binop::U: // Strong + 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)); + 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)); + succ_.push_back(*i2); + } + return; + case binop::R: // Weak + 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)); + 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)); + } + + i2->first.push_back(init_); // Add the initial state + t = res_->create_transition(init_, i2->first); + res_->add_condition(t, clone(i2->second)); + succ_.push_back(*i2); + } + return; + case binop::Xor: + case binop::Implies: + case binop::Equiv: + assert(0); // TBD + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const multop* node) + { + bool ok = true; + std::vector vs; + for (unsigned n = 0; n < node->size(); ++n) + { + vs.push_back(recurse(node->nth(n))); + if (vs[n].succ_.size() == 0) // Handle 0 + ok = false; + } + + init_ = to_string(node); + std::vector::iterator i; + taa::transition* t = 0; + switch (node->op()) + { + case multop::And: + { + 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)); + succ_.push_back(p[n]); + } + return; + } + case multop::Or: + 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)); + succ_.push_back(*i); + } + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const automatop* node) + { + (void) node; + assert(!"unsupported operator"); + } + + ltl2taa_visitor + recurse(const formula* f) + { + ltl2taa_visitor v(res_, negated_); + f->accept(v); + for (unsigned i = 0; i < v.to_free_.size(); ++i) + to_free_.push_back(v.to_free_[i]); + return v; + } + + private: + taa* res_; + bool negated_; + + typedef std::insert_iterator< + std::vector + > ii; + + typedef std::pair< + std::vector, const formula* + > succ_state; + + std::string init_; + std::vector succ_; + + std::vector to_free_; + + public: + std::vector + all_n_tuples(const std::vector& vs) + { + std::vector product; + + std::vector pos; + for (unsigned i = 0; i < vs.size(); ++i) + pos.push_back(vs[i].succ_.size()); + + while (pos[0] != 0) + { + std::vector u; // Union + formula* f = constant::true_instance(); + for (unsigned i = 0; i < vs.size(); ++i) + { + if (vs[i].succ_.size() == 0) + 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); + } + to_free_.push_back(f); + product.push_back(std::make_pair(u, f)); + + for (int i = vs.size() - 1; i >= 0; --i) + { + if (vs[i].succ_.size() == 0) + continue; + if (pos[i] > 1 || (i == 0 && pos[0] == 1)) + { + --pos[i]; + break; + } + else + pos[i] = vs[i].succ_.size(); + } + } + return product; + } + }; + } // anonymous + + taa* + ltl_to_taa(const ltl::formula* f, bdd_dict* dict) + { + // TODO: s/unabbreviate_ltl/unabbreviate_logic/ + const ltl::formula* f1 = ltl::unabbreviate_ltl(f); + const ltl::formula* f2 = ltl::negative_normal_form(f1); + ltl::destroy(f1); + + std::cerr << ltl::to_string(f2) << std::endl; + + taa* res = new spot::taa(dict); + ltl2taa_visitor v(res); + f2->accept(v); + ltl::destroy(f2); + + return v.result(); + } +} diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh new file mode 100644 index 000000000..e6d41b441 --- /dev/null +++ b/src/tgbaalgos/ltl2taa.hh @@ -0,0 +1,54 @@ +// Copyright (C) 2009 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TAAALGOS_LTL2TAA_HH_ +# define SPOT_TAAALGOS_LTL2TAA_HH_ + +#include "ltlast/formula.hh" +#include "tgba/taa.hh" + +namespace spot +{ + /// \brief Build a spot::taa* from an LTL formula. + /// + /// This is based on the following. + /// \verbatim + /// @techreport{HUT-TCS-A104, + /// address = {Espoo, Finland}, + /// author = {Heikki Tauriainen}, + /// month = {September}, + /// note = {Doctoral dissertation}, + /// number = {A104}, + /// pages = {xii+229}, + /// title = {Automata and Linear Temporal Logic: Translations + /// with Transition-Based Acceptance}, + /// type = {Research Report}, + /// year = {2006} + /// } + /// \endverbatim + /// + /// \param f The formula to translate into an automaton. + /// \param dict The spot::bdd_dict the constructed automata should use. + /// \return A spot::taa that recognizes the language of \a f. + taa* ltl_to_taa(const ltl::formula* f, bdd_dict* dict); +} + +#endif /* !SPOT_TAAALGOS_LTL2TAA_HH_ */ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 58515ff5e..a5a95abed 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -33,6 +33,7 @@ #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/ltl2taa.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/dotty.hh" @@ -79,6 +80,7 @@ syntax(char* prog) << " -E[ALGO] emptiness-check, expect no accepting run" << std::endl << " -f use Couvreur's FM algorithm for translation" + << " -taa use Tauriainen's TAA-based algorithm for translation" << std::endl << " -fr1 use -r1 (see below) at each step of FM" << std::endl << " -fr2 use -r2 (see below) at each step of FM" << std::endl @@ -172,6 +174,7 @@ main(int argc, char** argv) bool paper_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled; + bool taa_opt = false; bool fm_opt = false; int fm_red = spot::ltl::Reduce_None; bool fm_exprop_opt = false; @@ -279,6 +282,10 @@ main(int argc, char** argv) expect_counter_example = false; output = -1; } + else if (!strcmp(argv[formula_index], "-taa")) + { + taa_opt = true; + } else if (!strcmp(argv[formula_index], "-f")) { fm_opt = true; @@ -584,7 +591,10 @@ main(int argc, char** argv) fair_loop_approx, unobservables, fm_red, containment); else - to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); + if (taa_opt) + to_free = a = spot::ltl_to_taa(f, dict); + else + to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); } spot::tgba_tba_proxy* degeneralized = 0; diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 7629932e8..286566b51 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -73,7 +73,7 @@ Algorithm Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc" Path = "${LBTT_TRANSLATE}" Parameters = "--spot '../eltl2tgba -L'" - Enabled = yes + Enabled = no } Algorithm @@ -262,6 +262,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Tauriainen -- TAA)" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -taa -t'" + Enabled = yes +} + GlobalOptions { Rounds = 100