diff --git a/ChangeLog b/ChangeLog index 492926d8d..d2c635e1e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-01-30 Alexandre Duret-Lutz + + Rename tgba_complement as tgba_kv_complement. + + * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: Rename + as... + * src/tgba/tgbakvcomplement.hh, src/tgba/tgbakvcomplement.cc: + ... these. It makes more sense since we also have + tgba_safra_complement. + * src/tgba/Makefile.am, src/tgbatest/complement.cc, NEWS: Adjust. + 2010-01-30 Alexandre Duret-Lutz Do not recognize "*" as "and". This leaves room for an diff --git a/NEWS b/NEWS index b84a17598..72f6ba00a 100644 --- a/NEWS +++ b/NEWS @@ -24,7 +24,7 @@ New in spot 0.5 (2010-01-31): (in time and memory consumption) for the LTL translation. * Two complementation algorithms for state-based Büchi automata have been implemented: - - tgba_complement is an on-the-fly implementation of the + - tgba_kv_complement is an on-the-fly implementation of the Kupferman-Vardi construction (TCS'05) for generalized acceptance conditions. - tgba_safra_complement is an implementation of Safra's diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 46cb3e7ff..8cbfe6d78 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2009 Laboratoire de Recherche et Développement +## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -43,9 +43,9 @@ tgba_HEADERS = \ tgbabddconcreteproduct.hh \ tgbabddcoredata.hh \ tgbabddfactory.hh \ - tgbacomplement.hh \ tgbaexplicit.hh \ tgbafromfile.hh \ + tgbakvcomplement.hh \ tgbascc.hh \ tgbaproduct.hh \ tgbareduc.hh \ @@ -68,9 +68,9 @@ libtgba_la_SOURCES = \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ - tgbacomplement.cc \ tgbaexplicit.cc \ tgbafromfile.cc \ + tgbakvcomplement.cc \ tgbaproduct.cc \ tgbareduc.cc \ tgbasafracomplement.cc \ diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbakvcomplement.cc similarity index 79% rename from src/tgba/tgbacomplement.cc rename to src/tgba/tgbakvcomplement.cc index 47aeb8e6a..0f0ef4bd1 100644 --- a/src/tgba/tgbacomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,7 +24,7 @@ #include "bdd.h" #include "bddprint.hh" #include "state.hh" -#include "tgbacomplement.hh" +#include "tgbakvcomplement.hh" #include "misc/hash.hh" #include "tgbaalgos/bfssteps.hh" #include "misc/hashfunc.hh" @@ -97,22 +97,22 @@ namespace spot state_shared_ptr_equal> state_set; //////////////////////////////////////// - // state_complement + // state_kv_complement - /// States used by spot::tgba_complement. + /// States used by spot::tgba_kv_complement. /// A state has a map of states associated to ranks, and a set /// of filtered states. /// \ingroup tgba_representation - class state_complement : public state + class state_kv_complement : public state { public: - state_complement(); - state_complement(state_rank_map state_map, state_set state_filter); - virtual ~state_complement() {} + state_kv_complement(); + state_kv_complement(state_rank_map state_map, state_set state_filter); + virtual ~state_kv_complement() {} virtual int compare(const state* other) const; virtual size_t hash() const; - virtual state_complement* clone() const; + virtual state_kv_complement* clone() const; void add(shared_state state, const rank_t& rank); const state_rank_map& get_state_map() const; @@ -123,20 +123,21 @@ namespace spot state_set state_filter_; }; - state_complement::state_complement() + state_kv_complement::state_kv_complement() { } - state_complement::state_complement(state_rank_map state_map, + state_kv_complement::state_kv_complement(state_rank_map state_map, state_set state_filter) : state_map_(state_map), state_filter_(state_filter) { } int - state_complement::compare(const state* o) const + state_kv_complement::compare(const state* o) const { - const state_complement* other = dynamic_cast(o); + const state_kv_complement* other = + dynamic_cast(o); if (other == 0) return 1; @@ -185,7 +186,7 @@ namespace spot } size_t - state_complement::hash() const + state_kv_complement::hash() const { size_t hash = 0; @@ -211,59 +212,59 @@ namespace spot return hash; } - state_complement* - state_complement::clone() const + state_kv_complement* + state_kv_complement::clone() const { - return new state_complement(*this); + return new state_kv_complement(*this); } void - state_complement::add(shared_state state, + state_kv_complement::add(shared_state state, const rank_t& rank) { state_map_[state] = rank; } const state_rank_map& - state_complement::get_state_map() const + state_kv_complement::get_state_map() const { return state_map_; } const state_set& - state_complement::get_filter_set() const + state_kv_complement::get_filter_set() const { return state_filter_; } bool - state_complement::accepting() const + state_kv_complement::accepting() const { return state_filter_.empty(); } - /// Successor iterators used by spot::tgba_complement. + /// Successor iterators used by spot::tgba_kv_complement. /// \ingroup tgba_representation /// /// Since the algorithm works on-the-fly, the key components of the /// algorithm are implemented in this class. /// /// - class tgba_complement_succ_iterator: public tgba_succ_iterator + class tgba_kv_complement_succ_iterator: public tgba_succ_iterator { public: typedef std::list bdd_list_t; - tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton, - bdd the_acceptance_cond, - const acc_list_t& acc_list, - const state_complement* origin); - virtual ~tgba_complement_succ_iterator() {}; + tgba_kv_complement_succ_iterator(const tgba_sgba_proxy* automaton, + bdd the_acceptance_cond, + const acc_list_t& acc_list, + const state_kv_complement* origin); + virtual ~tgba_kv_complement_succ_iterator() {}; virtual void first(); virtual void next(); virtual bool done() const; - virtual state_complement* current_state() const; + virtual state_kv_complement* current_state() const; virtual bdd current_condition() const; virtual bdd current_acceptance_conditions() const; private: @@ -278,8 +279,8 @@ namespace spot const tgba_sgba_proxy* automaton_; bdd the_acceptance_cond_; const acc_list_t& acc_list_; - const state_complement* origin_; - const state_complement* current_state_; + const state_kv_complement* origin_; + const state_kv_complement* current_state_; bdd_list_t condition_list_; bdd_list_t::const_iterator current_condition_; state_rank_map highest_current_ranks_; @@ -287,11 +288,11 @@ namespace spot state_set highest_state_set_; }; - tgba_complement_succ_iterator:: - tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton, - bdd the_acceptance_cond, - const acc_list_t& acc_list, - const state_complement* origin) + tgba_kv_complement_succ_iterator:: + tgba_kv_complement_succ_iterator(const tgba_sgba_proxy* automaton, + bdd the_acceptance_cond, + const acc_list_t& acc_list, + const state_kv_complement* origin) : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), acc_list_(acc_list), origin_(origin) { @@ -300,7 +301,7 @@ namespace spot /// Insert in \a list atomic properties of the formula \a c. void - tgba_complement_succ_iterator::get_atomics(std::set& list, bdd c) + tgba_kv_complement_succ_iterator::get_atomics(std::set& list, bdd c) { bdd current = bdd_satone(c); while (current != bddtrue && current != bddfalse) @@ -317,7 +318,7 @@ namespace spot /// Create the conjunction of all the atomic properties from /// the successors of the current state. void - tgba_complement_succ_iterator::get_conj_list() + tgba_kv_complement_succ_iterator::get_conj_list() { std::set atomics; condition_list_.clear(); @@ -364,18 +365,18 @@ namespace spot /// For each odd rank, its condition associated must not /// be present in its tracked state. bool - tgba_complement_succ_iterator::is_valid_rank() const + tgba_kv_complement_succ_iterator::is_valid_rank() const { for (state_rank_map::const_iterator i = current_ranks_.begin(); i != current_ranks_.end(); ++i) { if (i->second.rank & 1) - { + { if ((automaton_->state_acceptance_conditions(i->first.get()) & i->second.condition.get_bdd()) != bddfalse) return false; - } + } } return true; @@ -388,37 +389,36 @@ namespace spot /// When the rank is odd, its has an acceptance condition associated that /// must not be in its associated state. /// \return false if there is not valid rank as successor. - bool tgba_complement_succ_iterator::next_valid_rank() + bool tgba_kv_complement_succ_iterator::next_valid_rank() { state_rank_map::const_iterator i; - do { - for (i = current_ranks_.begin(); - i != current_ranks_.end(); - ++i) - { - if (i->second.rank != 0) - { - if (i->second.rank & 1) - { - if (i->second.condition.order() == 0) - --i->second.rank; - else - i->second.condition = - acc_list_[i->second.condition.order() - 1]; - } - else - { - --i->second.rank; - i->second.condition = acc_list_[acc_list_.size() - 1]; - } - break; - } - else - { - current_ranks_[i->first] = highest_current_ranks_[i->first]; - } - } - } + do + { + for (i = current_ranks_.begin(); i != current_ranks_.end(); ++i) + { + if (i->second.rank != 0) + { + if (i->second.rank & 1) + { + if (i->second.condition.order() == 0) + --i->second.rank; + else + i->second.condition = + acc_list_[i->second.condition.order() - 1]; + } + else + { + --i->second.rank; + i->second.condition = acc_list_[acc_list_.size() - 1]; + } + break; + } + else + { + current_ranks_[i->first] = highest_current_ranks_[i->first]; + } + } + } while ((i != current_ranks_.end()) && !is_valid_rank()); return i != current_ranks_.end(); @@ -427,7 +427,7 @@ namespace spot /// \brief Create the highest rank of \a origin_ as origin and /// \a condition as successor condition. void - tgba_complement_succ_iterator::successor_highest_rank(bdd condition) + tgba_kv_complement_succ_iterator::successor_highest_rank(bdd condition) { // Highest rank for bdd. state_rank_map sr_map = origin_->get_state_map(); @@ -481,7 +481,7 @@ namespace spot } void - tgba_complement_succ_iterator::first() + tgba_kv_complement_succ_iterator::first() { current_condition_ = condition_list_.begin(); if (done()) @@ -494,7 +494,7 @@ namespace spot } void - tgba_complement_succ_iterator::next() + tgba_kv_complement_succ_iterator::next() { if (done()) return; @@ -512,13 +512,13 @@ namespace spot } bool - tgba_complement_succ_iterator::done() const + tgba_kv_complement_succ_iterator::done() const { return (current_condition_ == condition_list_.end()); } - state_complement* - tgba_complement_succ_iterator::current_state() const + state_kv_complement* + tgba_kv_complement_succ_iterator::current_state() const { if (done()) return 0; @@ -550,11 +550,11 @@ namespace spot } } - return new state_complement(current_ranks_, filter); + return new state_kv_complement(current_ranks_, filter); } bdd - tgba_complement_succ_iterator::current_condition() const + tgba_kv_complement_succ_iterator::current_condition() const { if (done()) return bddfalse; @@ -562,7 +562,7 @@ namespace spot } bdd - tgba_complement_succ_iterator::current_acceptance_conditions() const + tgba_kv_complement_succ_iterator::current_acceptance_conditions() const { if (done()) return bddfalse; @@ -579,7 +579,7 @@ namespace spot /// Retrieve all the atomic acceptance conditions of the automaton. /// They are inserted into \a acc_list_. void - tgba_complement::get_acc_list() + tgba_kv_complement::get_acc_list() { bdd c = automaton_->all_acceptance_conditions(); bdd current = bdd_satone(c); @@ -596,7 +596,7 @@ namespace spot } } - tgba_complement::tgba_complement(const tgba* a) + tgba_kv_complement::tgba_kv_complement(const tgba* a) : automaton_(new tgba_sgba_proxy(a)) { get_dict()->register_all_variables_of(automaton_, this); @@ -610,45 +610,46 @@ namespace spot get_acc_list(); } - tgba_complement::~tgba_complement() + tgba_kv_complement::~tgba_kv_complement() { get_dict()->unregister_all_my_variables(this); delete automaton_; } state* - tgba_complement::get_init_state() const + tgba_kv_complement::get_init_state() const { - state_complement* init = new state_complement(); + state_kv_complement* init = new state_kv_complement(); rank_t r = {2 * nb_states_, bdd_ordered()}; init->add(shared_state(automaton_->get_init_state()), r); return init; } tgba_succ_iterator* - tgba_complement::succ_iter(const state* local_state, + tgba_kv_complement::succ_iter(const state* local_state, const state*, const tgba*) const { - const state_complement* state = - dynamic_cast(local_state); + const state_kv_complement* state = + dynamic_cast(local_state); assert(state); - return new tgba_complement_succ_iterator(automaton_, + return new tgba_kv_complement_succ_iterator(automaton_, the_acceptance_cond_, acc_list_, state); } bdd_dict* - tgba_complement::get_dict() const + tgba_kv_complement::get_dict() const { return automaton_->get_dict(); } std::string - tgba_complement::format_state(const state* state) const + tgba_kv_complement::format_state(const state* state) const { - const state_complement* s = dynamic_cast(state); + const state_kv_complement* s = + dynamic_cast(state); assert(s); std::ostringstream ss; ss << "{ set: {" << std::endl; @@ -674,19 +675,19 @@ namespace spot } bdd - tgba_complement::all_acceptance_conditions() const + tgba_kv_complement::all_acceptance_conditions() const { return the_acceptance_cond_; } bdd - tgba_complement::neg_acceptance_conditions() const + tgba_kv_complement::neg_acceptance_conditions() const { return !the_acceptance_cond_; } bdd - tgba_complement::compute_support_conditions(const state* state) const + tgba_kv_complement::compute_support_conditions(const state* state) const { tgba_succ_iterator* i = succ_iter(state); bdd result = bddtrue; @@ -697,7 +698,7 @@ namespace spot } bdd - tgba_complement::compute_support_variables(const state* state) const + tgba_kv_complement::compute_support_variables(const state* state) const { tgba_succ_iterator* i = succ_iter(state); bdd result = bddtrue; diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbakvcomplement.hh similarity index 86% rename from src/tgba/tgbacomplement.hh rename to src/tgba/tgbakvcomplement.hh index 1bc7597d4..2e548f4a8 100644 --- a/src/tgba/tgbacomplement.hh +++ b/src/tgba/tgbakvcomplement.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -18,8 +18,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBA_TGBACOMPLEMENT_HH -#define SPOT_TGBA_TGBACOMPLEMENT_HH +#ifndef SPOT_TGBA_TGBAKVCOMPLEMENT_HH +#define SPOT_TGBA_TGBAKVCOMPLEMENT_HH #include #include "bdd.h" @@ -77,16 +77,16 @@ namespace spot /// } /// /// The original automaton is used as a States-based Generalized - /// Büchi Automaton. + /// Büchi Automaton. /// /// The construction is done on-the-fly, by the - /// \c tgba_complement_succ_iterator class. - /// \see tgba_complement_succ_iteratora - class tgba_complement : public tgba + /// \c tgba_kv_complement_succ_iterator class. + /// \see tgba_kv_complement_succ_iterator + class tgba_kv_complement : public tgba { public: - tgba_complement(const tgba* a); - virtual ~tgba_complement(); + tgba_kv_complement(const tgba* a); + virtual ~tgba_kv_complement(); // tgba interface virtual state* get_init_state() const; @@ -111,9 +111,9 @@ namespace spot bdd the_acceptance_cond_; unsigned nb_states_; acc_list_t acc_list_; - }; // end class tgba_complement. + }; // end class tgba_kv_complement. } // end namespace spot. -#endif // !SPOT_TGBA_TGBACOMPLEMENT_HH +#endif // !SPOT_TGBA_TGBAKVCOMPLEMENT_HH diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 12b455e2f..b9ee344ff 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -34,14 +34,14 @@ #include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" -#include "tgba/tgbacomplement.hh" +#include "tgba/tgbakvcomplement.hh" void usage(const char* prog) { std::cout << "usage: " << prog << " [options]" << std::endl; std::cout << "with options" << std::endl - << "-S Use safra complementation" - << std::endl + << "-S Use Safra's complementation " + << "instead of Kupferman&Vardi's" << std::endl << "-s buchi_automaton display the safra automaton" << std::endl << "-a buchi_automaton display the complemented automaton" @@ -131,7 +131,7 @@ int main(int argc, char* argv[]) if (safra) complement = new spot::tgba_safra_complement(a); else - complement = new spot::tgba_complement(a); + complement = new spot::tgba_kv_complement(a); if (print_automaton) spot::dotty_reachable(std::cout, complement); @@ -162,7 +162,7 @@ int main(int argc, char* argv[]) if (safra) complement = new spot::tgba_safra_complement(a); else - complement = new spot::tgba_complement(a); + complement = new spot::tgba_kv_complement(a); spot::dotty_reachable(std::cout, complement); f1->destroy(); @@ -219,8 +219,8 @@ int main(int argc, char* argv[]) << safra_complement->number_of_acceptance_conditions() << std::endl; - spot::tgba_complement* complement = - new spot::tgba_complement(a); + spot::tgba_kv_complement* complement = + new spot::tgba_kv_complement(a); b_size = spot::stats_reachable(complement); std::cout << "GBA Complement: " @@ -271,8 +271,8 @@ int main(int argc, char* argv[]) } else { - nAf = new spot::tgba_complement(Af); - nAnf = new spot::tgba_complement(Anf); + nAf = new spot::tgba_kv_complement(Af); + nAnf = new spot::tgba_kv_complement(Anf); } spot::tgba* prod = new spot::tgba_product(nAf, nAnf); spot::emptiness_check* ec = spot::couvreur99(prod);