diff --git a/ChangeLog b/ChangeLog index 3d1c5b1ce..898df995c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2009-10-04 Damien Lefortier + + Add a class to represent Transition-based Alternating Automata (TAA). + + * misc/Makefile.am, misc/bbop.cc, misc/bddop.hh: Factorize some + code on BDDs to compute all_acceptance_conditions from + neg_acceptance_condition. + * src/tgba/Makefile.am, src/tgbatest/Makefile.am: Adjust. + * src/tgba/taa.cc, src/tgba/taa.hh: The TAA class. + * src/tgba/tgbaexplicit.hh: Use the factorized code in bddop.hh. + * src/tgbatest/taa.cc, src/tgbatest/taa.test: Some test cases. + 2009-10-07 Alexandre Duret-Lutz * AUTHORS: Add Damien Lefortier, Guillaume Sadegh, and Félix diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 41771fd0d..573bf3d02 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -28,6 +28,7 @@ misc_HEADERS = \ bareword.hh \ bddalloc.hh \ bddlt.hh \ + bddop.hh \ escape.hh \ freelist.hh \ hash.hh \ @@ -45,6 +46,7 @@ noinst_LTLIBRARIES = libmisc.la libmisc_la_SOURCES = \ bareword.cc \ bddalloc.cc \ + bddop.cc \ escape.cc \ freelist.cc \ memusage.cc \ diff --git a/src/misc/bddop.cc b/src/misc/bddop.cc new file mode 100644 index 000000000..325e33003 --- /dev/null +++ b/src/misc/bddop.cc @@ -0,0 +1,51 @@ +// 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 "bddop.hh" + +namespace spot +{ + bdd + compute_all_acceptance_conditions(bdd neg_acceptance_conditions) + { + bdd all = bddfalse; + + // Build all_acceptance_conditions_ from neg_acceptance_conditions_ + // I.e., transform !A & !B & !C into + // A & !B & !C + // + !A & B & !C + // + !A & !B & C + bdd cur = neg_acceptance_conditions; + while (cur != bddtrue) + { + assert(cur != bddfalse); + + bdd v = bdd_ithvar(bdd_var(cur)); + all |= v & bdd_exist(neg_acceptance_conditions, v); + + assert(bdd_high(cur) != bddtrue); + cur = bdd_low(cur); + } + + return all; + } +} diff --git a/src/misc/bddop.hh b/src/misc/bddop.hh new file mode 100644 index 000000000..c374ae294 --- /dev/null +++ b/src/misc/bddop.hh @@ -0,0 +1,34 @@ +// 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_MISC_BDDOP_HH_ +# define SPOT_MISC_BDDOP_HH_ + +#include "bdd.h" + +namespace spot +{ + /// \brief Compute all acceptance conditions from all neg acceptance + /// conditions. + bdd compute_all_acceptance_conditions(bdd neg_acceptance_conditions); +} + +#endif /* !SPOT_MISC_BDDOP_HH_ */ diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 9e3567e26..aee3b13dd 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -34,6 +34,7 @@ tgba_HEADERS = \ statebdd.hh \ succiter.hh \ succiterconcrete.hh \ + taa.hh \ tgba.hh \ tgbabddconcrete.hh \ tgbabddconcretefactory.hh \ @@ -59,6 +60,7 @@ libtgba_la_SOURCES = \ futurecondcol.cc \ succiterconcrete.cc \ statebdd.cc \ + taa.cc \ tgba.cc \ tgbabddconcrete.cc \ tgbabddconcretefactory.cc \ diff --git a/src/tgba/taa.cc b/src/tgba/taa.cc new file mode 100644 index 000000000..103027319 --- /dev/null +++ b/src/tgba/taa.cc @@ -0,0 +1,412 @@ +// 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 +#include "ltlvisit/destroy.hh" +#include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" +#include "taa.hh" + +namespace spot +{ + /*----. + | taa | + `----*/ + + taa::taa(bdd_dict* dict) + : name_state_map_(), state_name_map_(), dict_(dict), + all_acceptance_conditions_(bddfalse), + all_acceptance_conditions_computed_(false), + neg_acceptance_conditions_(bddtrue), + init_(0), state_set_vec_() + { + } + + taa::~taa() + { + ns_map::iterator i; + for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + { + taa::state::iterator i2; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + delete *i2; + delete i->second; + } + ss_vec::iterator j; + for (j = state_set_vec_.begin(); j != state_set_vec_.end(); ++j) + delete *j; + dict_->unregister_all_my_variables(this); + } + + void + taa::set_init_state(const std::string& s) + { + init_ = add_state(s); + } + + taa::transition* + taa::create_transition(const std::string& s, + const std::vector& d) + { + state* src = add_state(s); + state_set* dst = add_state_set(d); + transition* t = new transition; + t->dst = dst; + t->condition = bddtrue; + t->acceptance_conditions = bddfalse; + src->push_back(t); + return t; + } + + taa::transition* + taa::create_transition(const std::string& s, const std::string& d) + { + std::vector vec; + vec.push_back(d); + return create_transition(s, vec); + } + + void + taa::add_condition(transition* t, const ltl::formula* f) + { + t->condition &= formula_to_bdd(f, dict_, this); + ltl::destroy(f); + } + + void + taa::add_acceptance_condition(transition* t, const ltl::formula* f) + { + if (dict_->acc_map.find(f) == dict_->acc_map.end()) + { + int v = dict_->register_acceptance_variable(f, this); + bdd neg = bdd_nithvar(v); + neg_acceptance_conditions_ &= neg; + + // Append neg to all acceptance conditions. + ns_map::iterator i; + for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + { + taa::state::iterator i2; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + (*i2)->acceptance_conditions &= neg; + } + + all_acceptance_conditions_computed_ = false; + } + + bdd_dict::fv_map::iterator i = dict_->acc_map.find(f); + assert(i != dict_->acc_map.end()); + ltl::destroy(f); + bdd v = bdd_ithvar(i->second); + t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v); + } + + state* + taa::get_init_state() const + { + taa::state_set* s = new taa::state_set; + s->insert(init_); + return new spot::state_set(s); + } + + tgba_succ_iterator* + taa::succ_iter(const spot::state* state, + const spot::state* global_state, + const tgba* global_automaton) const + { + const spot::state_set* s = dynamic_cast(state); + assert(s); + (void) global_state; + (void) global_automaton; + return new taa_succ_iterator(s->get_state(), + all_acceptance_conditions()); + } + + bdd_dict* + taa::get_dict() const + { + return dict_; + } + + std::string + taa::format_state(const spot::state* s) const + { + 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->size() == 0) + 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; + } + } + + bdd + taa::all_acceptance_conditions() const + { + if (!all_acceptance_conditions_computed_) + { + all_acceptance_conditions_ = + compute_all_acceptance_conditions(neg_acceptance_conditions_); + all_acceptance_conditions_computed_ = true; + } + return all_acceptance_conditions_; + } + + bdd + taa::neg_acceptance_conditions() const + { + return neg_acceptance_conditions_; + } + + bdd + taa::compute_support_conditions(const spot::state* s) const + { + const spot::state_set* se = dynamic_cast(s); + assert(se); + const state_set* ss = se->get_state(); + + bdd res = bddtrue; + taa::state_set::const_iterator i; + taa::state::const_iterator j; + for (i = ss->begin(); i != ss->end(); ++i) + for (j = (*i)->begin(); j != (*i)->end(); ++j) + res |= (*j)->condition; + return res; + } + + bdd + taa::compute_support_variables(const spot::state* s) const + { + const spot::state_set* se = dynamic_cast(s); + assert(se); + const state_set* ss = se->get_state(); + + bdd res = bddtrue; + taa::state_set::const_iterator i; + taa::state::const_iterator j; + for (i = ss->begin(); i != ss->end(); ++i) + for (j = (*i)->begin(); j != (*i)->end(); ++j) + res &= bdd_support((*j)->condition); + return res; + } + + taa::state* + taa::add_state(const std::string& name) + { + ns_map::iterator i = name_state_map_.find(name); + if (i == name_state_map_.end()) + { + 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; + } + + taa::state_set* + taa::add_state_set(const std::vector& names) + { + state_set* ss = new state_set; + for (unsigned i = 0; i < names.size(); ++i) + ss->insert(add_state(names[i])); + state_set_vec_.push_back(ss); + return ss; + } + + /*----------. + | state_set | + `----------*/ + + const taa::state_set* + state_set::get_state() const + { + return s_; + } + + int + state_set::compare(const spot::state* other) const + { + const state_set* o = dynamic_cast(other); + assert(o); + + const taa::state_set* s1 = get_state(); + const taa::state_set* s2 = o->get_state(); + + if (*s1 == *s2) + return 0; + + taa::state_set::const_iterator it1 = s1->begin(); + taa::state_set::const_iterator it2 = s2->begin(); + while (it2 != s2->end() && it1 != s1->end()) + { + int i = *it1++ - *it2++; + if (i != 0) + return i; + } + return s1->size() - s2->size(); + } + + size_t + state_set::hash() const + { + size_t res = wang32_hash(0); + taa::state_set::const_iterator it = s_->begin(); + while (it != s_->end()) + { + res += reinterpret_cast(*it++) - static_cast(0); + res ^= wang32_hash(res); + } + return res; + } + + state_set* + state_set::clone() const + { + taa::state_set* s = new taa::state_set(*s_); + return new spot::state_set(s); + } + + /*--------------. + | taa_succ_iter | + `--------------*/ + + taa_succ_iterator::taa_succ_iterator(const taa::state_set* s, bdd all_acc) + : bounds_(), its_(), all_acceptance_conditions_(all_acc), + empty_(s->empty()) + { + 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()); + } + } + + void + taa_succ_iterator::first() + { + if (!done() && current_condition() == bddfalse) + next(); + } + + 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); + } + + 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_.size() == 0 ? true : false; + } + + 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); + } + + 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; + } + + 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_); + } +} diff --git a/src/tgba/taa.hh b/src/tgba/taa.hh new file mode 100644 index 000000000..7319476c8 --- /dev/null +++ b/src/tgba/taa.hh @@ -0,0 +1,175 @@ +// 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_TGBA_TAA_HH_ +# define SPOT_TGBA_TAA_HH_ + +#include +#include +#include "misc/hash.hh" +#include "ltlast/formula.hh" +#include "bdddict.hh" +#include "tgba.hh" + +namespace spot +{ + /// \brief A Transition-based Alternating Automaton (TAA). + class taa : public tgba + { + public: + taa(bdd_dict* dict); + + struct transition; + typedef std::list state; + typedef std::set state_set; + + /// Explicit transitions. + struct transition + { + bdd condition; + bdd acceptance_conditions; + const state_set* dst; + }; + + void set_init_state(const std::string& state); + + transition* + create_transition(const std::string& src, + const std::vector& dst); + transition* + create_transition(const std::string& src, const std::string& dst); + + void add_condition(transition* t, const ltl::formula* f); + void add_acceptance_condition(transition* t, const ltl::formula* f); + + /// TGBA interface. + virtual ~taa(); + virtual spot::state* get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const spot::state* local_state, + const spot::state* global_state = 0, + const tgba* global_automaton = 0) const; + virtual bdd_dict* get_dict() const; + + /// \brief Format the state as a string for printing. + /// + /// If state is a spot::state_set of only one element, then the + /// string corresponding to state->get_state() is returned. + /// + /// Otherwise a string composed of each string corresponding to + /// each state->get_state() in the spot::state_set is returned, + /// e.g. like {string_1,...,string_n}. + virtual std::string format_state(const spot::state* state) const; + + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + protected: + virtual bdd compute_support_conditions(const spot::state* state) const; + virtual bdd compute_support_variables(const spot::state* state) const; + + typedef Sgi::hash_map< + const std::string, taa::state*, string_hash + > ns_map; + + typedef Sgi::hash_map< + const taa::state*, std::string, ptr_hash + > sn_map; + + typedef std::vector ss_vec; + + ns_map name_state_map_; + sn_map state_name_map_; + bdd_dict* dict_; + mutable bdd all_acceptance_conditions_; + mutable bool all_acceptance_conditions_computed_; + bdd neg_acceptance_conditions_; + taa::state* init_; + ss_vec state_set_vec_; + + private: + // Disallow copy. + taa(const taa& other); + taa& operator=(const taa& other); + + /// \brief Return the taa::state for \a name, creating it if it + /// does not exist. The first state added is the initial state + /// which can be overridden with set_init_state. + taa::state* add_state(const std::string& name); + + /// \brief Return the taa::state_set for \a names. + taa::state_set* add_state_set(const std::vector& names); + }; + + /// Set of states deriving from spot::state. + class state_set : public spot::state + { + public: + /// The taa::state_set has been allocated with \c new. It is the + /// responsability of the state_set to \c delete it when no longer + /// needed (cf. dtor). + state_set(const taa::state_set* s) + : s_(s) + { + } + + virtual int compare(const spot::state*) const; + virtual size_t hash() const; + virtual state_set* clone() const; + + virtual ~state_set() + { + delete s_; + } + + const taa::state_set* get_state() const; + private: + const taa::state_set* s_; + }; + + class taa_succ_iterator : public tgba_succ_iterator + { + public: + taa_succ_iterator(const taa::state_set* s, bdd all_acc); + + virtual ~taa_succ_iterator() + { + } + + virtual void first(); + virtual void next(); + virtual bool done() const; + + virtual state_set* current_state() const; + virtual bdd current_condition() const; + virtual bdd current_acceptance_conditions() const; + + private: + typedef taa::state::const_iterator iterator; + + std::vector > bounds_; + std::vector its_; + bdd all_acceptance_conditions_; + mutable bool empty_; + }; +} + +#endif /* !SPOT_TGBA_TAAEXPLICIT_HH_ */ diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 0880cacdd..ffbfc687b 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -24,6 +24,7 @@ #include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" #include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" #include namespace spot @@ -383,25 +384,8 @@ namespace spot { if (!all_acceptance_conditions_computed_) { - bdd all = bddfalse; - - // Build all_acceptance_conditions_ from neg_acceptance_conditions_ - // I.e., transform !A & !B & !C into - // A & !B & !C - // + !A & B & !C - // + !A & !B & C - bdd cur = neg_acceptance_conditions_; - while (cur != bddtrue) - { - assert(cur != bddfalse); - - bdd v = bdd_ithvar(bdd_var(cur)); - all |= v & bdd_exist(neg_acceptance_conditions_, v); - - assert(bdd_high(cur) != bddtrue); - cur = bdd_low(cur); - } - all_acceptance_conditions_ = all; + all_acceptance_conditions_ = + compute_all_acceptance_conditions(neg_acceptance_conditions_); all_acceptance_conditions_computed_ = true; } return all_acceptance_conditions_; diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 79e473f04..9f3ad5cb2 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -41,6 +41,7 @@ check_PROGRAMS = \ readsave \ reductgba \ reduccmp \ + taa \ tgbaread \ tripprod @@ -62,6 +63,7 @@ readsave_SOURCES = readsave.cc reductgba_SOURCES = reductgba.cc reduccmp_SOURCES = reductgba.cc reduccmp_CXXFLAGS = -DREDUCCMP +taa_SOURCES = taa.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc @@ -70,6 +72,7 @@ tripprod_SOURCES = tripprod.cc TESTS = \ eltl2tgba.test \ explicit.test \ + taa.test \ tgbaread.test \ readsave.test \ ltl2tgba.test \ diff --git a/src/tgbatest/taa.cc b/src/tgbatest/taa.cc new file mode 100644 index 000000000..f4d0699b6 --- /dev/null +++ b/src/tgbatest/taa.cc @@ -0,0 +1,80 @@ +// 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 +#include "misc/hash.hh" +#include "ltlenv/defaultenv.hh" +#include "ltlast/allnodes.hh" +#include "tgba/taa.hh" + +typedef Sgi::hash_set< + const spot::state*, spot::state_ptr_hash, spot::state_ptr_equal + > mset; + +void +dfs(spot::taa* a, const spot::state* s, mset& m) +{ + if (m.find(s) != m.end()) + return; + m.insert(s); + + spot::tgba_succ_iterator* i = a->succ_iter(s); + assert(i); + for (i->first(); !i->done(); i->next()) + { + std::cout << a->format_state(i->current_state()) << std::endl; + dfs(a, i->current_state(), m); + } + delete i; +} + +int +main() +{ + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::ltl::default_environment& e = + spot::ltl::default_environment::instance(); + spot::taa* a = new spot::taa(dict); + + typedef spot::taa::transition trans; + typedef spot::taa::state state; + typedef spot::taa::state_set state_set; + + std::string ss1_values[] = { "state 2", "state 3" }; + std::vector ss1_vector(ss1_values, ss1_values + 2); + trans* t1 = a->create_transition("state 1", ss1_vector); + trans* t2 = a->create_transition("state 2", "state 3"); + trans* t3 = a->create_transition("state 2", "state 4"); + + a->add_condition(t1, e.require("a")); + a->add_condition(t2, e.require("b")); + a->add_condition(t3, e.require("c")); + + mset m; + spot::state* init = a->get_init_state(); + dfs(a, init, m); + + delete init; + delete a; + delete dict; +} diff --git a/src/tgbatest/taa.test b/src/tgbatest/taa.test new file mode 100755 index 000000000..d7e39d256 --- /dev/null +++ b/src/tgbatest/taa.test @@ -0,0 +1,6 @@ +#!/bin/sh + +. ./defs || exit -1 +set -e + +run 0 ../taa || exit 1