diff --git a/ChangeLog b/ChangeLog index 03668e7fe..be3cca895 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2009-07-30 Felix Abecassis + + Add TGBA union implementation. + + * src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh: New files. + Union of two TGBAs. + * src/tgba/Makefile.am: Adjust. + 2009-07-09 Guillaume Sadegh * m4/intel.m4: Fix to support the cache. @@ -5,7 +13,7 @@ 2009-07-08 Guillaume Sadegh * src/tgba/tgbacomplement.cc: Stay on 80 columns. - + 2009-07-08 Félix Abecassis Add 2 benchmarks directories. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index dd825e136..a63cd0c74 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -46,7 +46,8 @@ tgba_HEADERS = \ tgbaproduct.hh \ tgbatba.hh \ tgbareduc.hh \ - tgbafromfile.hh + tgbafromfile.hh \ + tgbaunion.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -67,4 +68,5 @@ libtgba_la_SOURCES = \ tgbaproduct.cc \ tgbatba.cc \ tgbareduc.cc \ - tgbafromfile.cc + tgbafromfile.cc \ + tgbaunion.cc diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc new file mode 100644 index 000000000..8e55d4302 --- /dev/null +++ b/src/tgba/tgbaunion.cc @@ -0,0 +1,403 @@ +// 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 "tgbaunion.hh" +#include +#include +#include "misc/hashfunc.hh" + +namespace spot +{ + + //////////////////////////////////////////////////////////// + // state_union + + state_union::state_union(const state_union& o) + : state(), + left_(o.left()->clone()), + right_(o.right()->clone()) + { + } + + state_union::~state_union() + { + delete left_; + delete right_; + } + + int + state_union::compare(const state* other) const + { + const state_union* o = dynamic_cast(other); + assert(o); + // Initial state + if (!o->left() && !o->right()) + return left_ || right_; + // States from different automata. + if (left_ && !o->left()) + return -1; + // States from different automata. + if (right_ && !o->right()) + return 1; + // States from left automata. + if (left_) + return left_->compare(o->left()); + // States from right automata. + if (right_) + return right_->compare(o->right()); + // 0 should never be returned. + return 0; + } + + size_t + state_union::hash() const + { + // We assume that size_t is 32-bit wide. + if (left_) + return wang32_hash(left_->hash()); + if (right_) + return wang32_hash(right_->hash()); + return 0; + } + + state_union* + state_union::clone() const + { + return new state_union(*this); + } + + //////////////////////////////////////////////////////////// + // tgba_succ_iterator_union + + tgba_succ_iterator_union::tgba_succ_iterator_union + (tgba_succ_iterator* left, tgba_succ_iterator* right, + bdd left_missing, bdd right_missing, bdd left_neg, bdd right_neg) + : left_(left), right_(right), + left_missing_(left_missing), + right_missing_(right_missing), + left_neg_(left_neg), right_neg_(right_neg) + { + } + + tgba_succ_iterator_union::~tgba_succ_iterator_union() + { + delete left_; + delete right_; + } + + void + tgba_succ_iterator_union::next() + { + // Is it the initial state ? + if (left_ && right_) + { + // Yes, first iterate on the successors of the initial state of the + // left automaton. + if (!left_->done()) + { + left_->next(); + if (!left_->done()) + current_cond_ = left_->current_condition(); + else + current_cond_ = right_->current_condition(); + } + // Now iterate with the successors of the initial state of the right + // automaton. + else + { + right_->next(); + if (!right_->done()) + current_cond_ = right_->current_condition(); + } + } + else + { + // No, iterate either on the left or the right automaton. + if (left_) + { + left_->next(); + if (!left_->done()) + current_cond_ = left_->current_condition(); + } + else + { + right_->next(); + if (!right_->done()) + current_cond_ = right_->current_condition(); + } + } + } + + void + tgba_succ_iterator_union::first() + { + if (right_) + { + right_->first(); + current_cond_ = right_->current_condition(); + } + if (left_) + { + left_->first(); + current_cond_ = left_->current_condition(); + } + } + + bool + tgba_succ_iterator_union::done() const + { + if (right_) + return right_->done(); + else + return left_->done(); + } + + state_union* + tgba_succ_iterator_union::current_state() const + { + if (left_ && !left_->done()) + return new state_union(left_->current_state(), 0); + else + return new state_union(0, right_->current_state()); + } + + bdd + tgba_succ_iterator_union::current_condition() const + { + return current_cond_; + } + + bdd tgba_succ_iterator_union::current_acceptance_conditions() const + { + if (left_ && right_) + { + if (left_->done()) + return right_->current_acceptance_conditions(); + else + return left_->current_acceptance_conditions(); + } + // If we are either on the left or the right automaton, we need to modify + // the acceptance conditions of the transition. + if (left_) + { + bdd cur = (left_->current_acceptance_conditions() & left_neg_) + | left_missing_; + return cur; + } + else + { + bdd cur = (right_->current_acceptance_conditions() & right_neg_) + | right_missing_; + return cur; + } + } + + //////////////////////////////////////////////////////////// + // tgba_union + + tgba_union::tgba_union(const tgba* left, const tgba* right) + : dict_(left->get_dict()), left_(left), right_(right) + { + assert(dict_ == right->get_dict()); + + // Conjunction of negated acceptance conditions, e.g. !a & !b & !c + bdd lna = left_->neg_acceptance_conditions(); + bdd rna = right_->neg_acceptance_conditions(); + + left_acc_complement_ = lna; + right_acc_complement_ = rna; + + // Disjunctive Normal Form for all acceptance conditions + // e.g. (a & !b & !c) | (b & !a & !c) | (c & !a & !b) + bdd lac = left_->all_acceptance_conditions(); + bdd rac = right_->all_acceptance_conditions(); + + // Remove all occurences in rna of the variables in the set lna. + // The result is a set with the missing variables in the left automaton, + // i.e. the variables that are in the right automaton but not in the left + // one. + bdd lmac = bdd_exist(rna, lna); + left_var_missing_ = lmac; + // Remove all occurences in lna of the variables in the set rna. + // The result is a set with the missing variables in the right automaton, + // i.e. the variables that are in the left automaton but not in the right + // one. + bdd rmac = bdd_exist(lna, rna); + right_var_missing_ = rmac; + + // The new Disjunctive Normal Form for our union. + all_acceptance_conditions_ = ((lac & lmac) | (rac & rmac)); + // Simply the conjunction of left and right negated acceptance conditions. + neg_acceptance_conditions_ = lna & rna; + + // "-" is a NAND between the two sets. + // The result is the list of acceptance conditions to add to each + // transition. + // For example if a transition on the left automaton has (a & !b) + // and the right automaton has a new acceptance condition c, the resulting + // acceptance condition will be (a & !b & !c) | (c & !a & !b) + left_acc_missing_ = all_acceptance_conditions_ - (lac & lmac); + right_acc_missing_ = all_acceptance_conditions_ - (rac & rmac); + + dict_->register_all_variables_of(&left_, this); + dict_->register_all_variables_of(&right_, this); + } + + tgba_union::~tgba_union() + { + dict_->unregister_all_my_variables(this); + } + + state* + tgba_union::get_init_state() const + { + return new state_union(0, 0); + } + + tgba_succ_iterator_union* + tgba_union::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const + { + (void) global_state; + (void) global_automaton; + const state_union* s = dynamic_cast(local_state); + assert(s); + tgba_succ_iterator_union* res = 0; + // Is it the initial state ? + if (!s->left() && !s->right()) + { + // Yes, create an iterator with both initial states. + state* left_init = left_->get_init_state(); + state* right_init = right_->get_init_state(); + tgba_succ_iterator* li = left_->succ_iter(left_init); + tgba_succ_iterator* ri = right_->succ_iter(right_init); + res = new tgba_succ_iterator_union(li, ri, left_acc_missing_, + right_acc_missing_, + left_var_missing_, + right_var_missing_); + delete left_init; + delete right_init; + } + else + { + // No, create an iterator based on the corresponding state + // in the left or in the right automaton. + if (s->left()) + { + tgba_succ_iterator* li = left_->succ_iter(s->left()); + res = new tgba_succ_iterator_union(li, 0, left_acc_missing_, + right_acc_missing_, + left_var_missing_, + right_var_missing_); + } + else + { + tgba_succ_iterator* ri = right_->succ_iter(s->right()); + res = new tgba_succ_iterator_union(0, ri, left_acc_missing_, + right_acc_missing_, + left_var_missing_, + right_var_missing_); + } + } + return res; + } + + bdd + tgba_union::compute_support_conditions(const state* in) const + { + const state_union* s = dynamic_cast(in); + assert(s); + if (!s->left() && !s->right()) + return (left_->support_conditions(left_->get_init_state()) + & right_->support_conditions(right_->get_init_state())); + if (s->left()) + return left_->support_conditions(s->left()); + else + return right_->support_conditions(s->right()); + } + + bdd + tgba_union::compute_support_variables(const state* in) const + { + const state_union* s = dynamic_cast(in); + assert(s); + if (!s->left() && !s->right()) + return (left_->support_variables(left_->get_init_state()) + & right_->support_variables(right_->get_init_state())); + if (s->left()) + return left_->support_variables(s->left()); + else + return right_->support_variables(s->right()); + } + + bdd_dict* + tgba_union::get_dict() const + { + return dict_; + } + + std::string + tgba_union::format_state(const state* target_state) const + { + const state_union* s = dynamic_cast(target_state); + assert(s); + if (!s->left() && !s->right()) + { + return "initial"; + } + else + { + if (s->left()) + return (left_->format_state(s->left())); + else + return (right_->format_state(s->right())); + } + } + + state* + tgba_union::project_state(const state* s, const tgba* t) const + { + const state_union* s2 = dynamic_cast(s); + assert(s2); + // We can't project the initial state of our union. + if (!s2->left() && !s2->right()) + return 0; + if (t == this) + return s2->clone(); + if (s2->left()) + return left_->project_state(s2->left(), t); + else + return right_->project_state(s2->right(), t); + } + + bdd + tgba_union::all_acceptance_conditions() const + { + return all_acceptance_conditions_; + } + + bdd + tgba_union::neg_acceptance_conditions() const + { + return neg_acceptance_conditions_; + } +} diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh new file mode 100644 index 000000000..59b7ce43e --- /dev/null +++ b/src/tgba/tgbaunion.hh @@ -0,0 +1,165 @@ +// 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_TGBAUNION_HH +# define SPOT_TGBA_TGBAUNION_HH + +#include "tgba.hh" +#include "statebdd.hh" + +namespace spot +{ + /// \brief A state for spot::tgba_union. + /// \ingroup tgba_on_the_fly_algorithms + /// + /// This state is in fact a pair. + /// If the first member equals 0 and the second is different from 0, + /// the state belongs to the left automaton. + /// If the first member is different from 0 and the second is 0, + /// the state belongs to the right automaton. + /// If both members are 0, the state is the initial state. + class state_union : public state + { + public: + /// \brief Constructor + /// \param left The state from the left automaton. + /// \param right The state from the right automaton. + /// These states are acquired by spot::state_union, and will + /// be deleted on destruction. + state_union(state* left, state* right) + : left_(left), + right_(right) + { + } + + /// Copy constructor + state_union(const state_union& o); + + virtual ~state_union(); + + state* + left() const + { + return left_; + } + + state* + right() const + { + return right_; + } + + virtual int compare(const state* other) const; + virtual size_t hash() const; + virtual state_union* clone() const; + + private: + state* left_; ///< Does the state belongs + /// to the left automaton ? + state* right_; ///< Does the state belongs + /// to the right automaton ? + }; + + /// \brief Iterate over the successors of an union computed on the fly. + class tgba_succ_iterator_union: public tgba_succ_iterator + { + public: + tgba_succ_iterator_union(tgba_succ_iterator* left, + tgba_succ_iterator* right, + bdd left_missing, + bdd right_missing, bdd left_var, bdd right_var); + + virtual ~tgba_succ_iterator_union(); + + // iteration + void first(); + void next(); + bool done() const; + + // inspection + state_union* current_state() const; + bdd current_condition() const; + bdd current_acceptance_conditions() const; + + protected: + tgba_succ_iterator* left_; + tgba_succ_iterator* right_; + bdd current_cond_; + bdd left_missing_; + bdd right_missing_; + bdd left_neg_; + bdd right_neg_; + friend class tgba_union; + }; + + /// \brief A lazy union. (States are computed on the fly.) + class tgba_union: public tgba + { + public: + /// \brief Constructor. + /// \param left The left automata in the union. + /// \param right The right automata in the union. + tgba_union(const tgba* left, const tgba* right); + + virtual ~tgba_union(); + + virtual state* get_init_state() const; + + virtual tgba_succ_iterator_union* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; + + virtual bdd_dict* get_dict() const; + + virtual std::string format_state(const state* state) const; + + virtual state* project_state(const state* s, const tgba* t) const; + + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + protected: + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + + private: + bdd_dict* dict_; + const tgba* left_; + const tgba* right_; + bdd left_acc_missing_; + bdd right_acc_missing_; + bdd left_acc_complement_; + bdd right_acc_complement_; + bdd left_var_missing_; + bdd right_var_missing_; + bdd all_acceptance_conditions_; + bdd neg_acceptance_conditions_; + bddPair* right_common_acc_; + // Disallow copy. + tgba_union(const tgba_union&); + tgba_union& operator=(const tgba_union&); + }; + + +} + +#endif // SPOT_TGBA_TGBAUNION_HH