diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 285961554..622272c86 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -42,7 +42,6 @@ tgba_HEADERS = \ tgbaproduct.hh \ tgbasgba.hh \ tgbasafracomplement.hh \ - tgbaunion.hh \ wdbacomp.hh noinst_LTLIBRARIES = libtgba.la @@ -61,5 +60,4 @@ libtgba_la_SOURCES = \ tgbasafracomplement.cc \ tgbascc.cc \ tgbasgba.cc \ - tgbaunion.cc \ wdbacomp.cc diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc deleted file mode 100644 index 8567ee76d..000000000 --- a/src/tgba/tgbaunion.cc +++ /dev/null @@ -1,426 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 3 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 this program. If not, see . - -#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() - { - left_->destroy(); - right_->destroy(); - } - - int - state_union::compare(const state* other) const - { - const state_union* o = down_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) - { - } - - void - tgba_succ_iterator_union::recycle(const tgba* l, tgba_succ_iterator* left, - const tgba* r, tgba_succ_iterator* right) - { - l->release_iter(left_); - left_ = left; - r->release_iter(right_); - right_ = right; - } - - tgba_succ_iterator_union::~tgba_succ_iterator_union() - { - delete left_; - delete right_; - } - - bool - 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()) - { - if (left_->next()) - { - current_cond_ = left_->current_condition(); - return true; - } - else if (!right_->done()) - { - current_cond_ = right_->current_condition(); - return true; - } - else - { - return false; - } - } - // Now iterate with the successors of the initial state of the right - // automaton. - else - { - if (right_->next()) - { - current_cond_ = right_->current_condition(); - return true; - } - else - { - return false; - } - } - } - else - { - // No, iterate either on the left or the right automaton. - if (left_) - { - if (left_->next()) - { - current_cond_ = left_->current_condition(); - return true; - } - else - { - return false; - } - } - else - { - if (right_->next()) - { - current_cond_ = right_->current_condition(); - return true; - } - else - { - return false; - } - } - } - } - - bool - tgba_succ_iterator_union::first() - { - bool r = false; - if (right_) - { - r = right_->first(); - if (r) - current_cond_ = right_->current_condition(); - } - bool l = false; - if (left_) - { - l = left_->first(); - if (l) - current_cond_ = left_->current_condition(); - } - return r || l; - } - - 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* st) const - { - const state_union* s = down_cast(st); - assert(s); - // Is it the initial state ? - tgba_succ_iterator* li; - tgba_succ_iterator* ri; - 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(); - li = left_->succ_iter(left_init); - ri = right_->succ_iter(right_init); - left_init->destroy(); - right_init->destroy(); - } - // No, create an iterator based on the corresponding state - // in the left or in the right automaton. - else if (s->left()) - { - li = left_->succ_iter(s->left()); - ri = nullptr; - } - else - { - li = nullptr; - ri = right_->succ_iter(s->right()); - } - - if (iter_cache_) - { - tgba_succ_iterator_union* res = - down_cast(iter_cache_); - res->recycle(left_, li, right_, ri); - iter_cache_ = nullptr; - return res; - } - return new tgba_succ_iterator_union(li, ri, - left_acc_missing_, - right_acc_missing_, - left_var_missing_, - right_var_missing_); - } - - bdd - tgba_union::compute_support_conditions(const state* in) const - { - const state_union* s = down_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_dict_ptr - tgba_union::get_dict() const - { - return dict_; - } - - std::string - tgba_union::format_state(const state* target_state) const - { - const state_union* s = down_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 = down_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 deleted file mode 100644 index 6c67c1b32..000000000 --- a/src/tgba/tgbaunion.hh +++ /dev/null @@ -1,161 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBA_TGBAUNION_HH -# define SPOT_TGBA_TGBAUNION_HH - -#include "tgba.hh" - -namespace spot -{ - /// \ingroup tgba_on_the_fly_algorithms - /// \brief A state for spot::tgba_union. - /// - /// 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 SPOT_API 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 destroyed 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 SPOT_API 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); - - void recycle(const tgba* l, tgba_succ_iterator* left, - const tgba* r, tgba_succ_iterator* right); - - virtual ~tgba_succ_iterator_union(); - - // iteration - bool first(); - bool 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 SPOT_API 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* state) const; - - virtual bdd_dict_ptr 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; - - private: - bdd_dict_ptr 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_; - // Disallow copy. - tgba_union(const tgba_union&) SPOT_DELETED; - tgba_union& operator=(const tgba_union&) SPOT_DELETED; - }; - - -} - -#endif // SPOT_TGBA_TGBAUNION_HH