diff --git a/ChangeLog b/ChangeLog index ff80567e4..24e1b0bfe 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2009-09-21 Guillaume Sadegh + + Rename files related to Safra complementation. + + * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: Rename + as... + * src/tgba/tgbasafracomplement.cc, + src/tgba/tgbasafracomplement.hh: ... these, and adjust class name. + * src/tgba/Makefile.am, src/tgbatest/Makefile.am: Adjust. + * src/tgbatest/complementation.cc: Adjust. + 2009-09-28 Alexandre Duret-Lutz Fix previous patch. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index a63cd0c74..64018a3c8 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -41,7 +41,7 @@ tgba_HEADERS = \ tgbabddcoredata.hh \ tgbabddfactory.hh \ tgbascc.hh \ - tgbacomplement.hh \ + tgbasafracomplement.hh \ tgbaexplicit.hh \ tgbaproduct.hh \ tgbatba.hh \ @@ -63,7 +63,7 @@ libtgba_la_SOURCES = \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ tgbascc.cc \ - tgbacomplement.cc \ + tgbasafracomplement.cc \ tgbaexplicit.cc \ tgbaproduct.cc \ tgbatba.cc \ diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbasafracomplement.cc similarity index 96% rename from src/tgba/tgbacomplement.cc rename to src/tgba/tgbasafracomplement.cc index ce1fadd5d..aa47faf8f 100644 --- a/src/tgba/tgbacomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -34,7 +34,7 @@ #include "ltlast/formula.hh" #include "ltlast/constant.hh" #include "tgbaalgos/dotty.hh" -#include "tgba/tgbacomplement.hh" +#include "tgba/tgbasafracomplement.hh" namespace spot { @@ -848,7 +848,7 @@ namespace spot //////////////////////////////////////// // state_complement - /// States used by spot::tgba_complement. + /// States used by spot::tgba_safra_complement. /// \ingroup tgba_representation class state_complement : public state { @@ -979,21 +979,21 @@ namespace spot return ss.str(); } - /// Successor iterators used by spot::tgba_complement. + /// Successor iterators used by spot::tgba_safra_complement. /// \ingroup tgba_representation - class tgba_complement_succ_iterator: public tgba_succ_iterator + class tgba_safra_complement_succ_iterator: public tgba_succ_iterator { public: typedef std::multimap succ_list_t; - tgba_complement_succ_iterator(const succ_list_t& list, - bdd the_acceptance_cond) + tgba_safra_complement_succ_iterator(const succ_list_t& list, + bdd the_acceptance_cond) : list_(list), the_acceptance_cond_(the_acceptance_cond) { } virtual - ~tgba_complement_succ_iterator() + ~tgba_safra_complement_succ_iterator() { for (succ_list_t::iterator i = list_.begin(); i != list_.end(); ++i) delete i->second; @@ -1012,39 +1012,39 @@ namespace spot }; void - tgba_complement_succ_iterator::first() + tgba_safra_complement_succ_iterator::first() { it_ = list_.begin(); } void - tgba_complement_succ_iterator::next() + tgba_safra_complement_succ_iterator::next() { ++it_; } bool - tgba_complement_succ_iterator::done() const + tgba_safra_complement_succ_iterator::done() const { return it_ == list_.end(); } state_complement* - tgba_complement_succ_iterator::current_state() const + tgba_safra_complement_succ_iterator::current_state() const { assert(!done()); return new state_complement(*(it_->second)); } bdd - tgba_complement_succ_iterator::current_condition() const + tgba_safra_complement_succ_iterator::current_condition() const { assert(!done()); return it_->first; } bdd - tgba_complement_succ_iterator::current_acceptance_conditions() const + tgba_safra_complement_succ_iterator::current_acceptance_conditions() const { assert(!done()); return the_acceptance_cond_; @@ -1101,10 +1101,10 @@ namespace spot // End of the safra construction ////////////////////////////////////////// - // tgba_complement + // tgba_safra_complement ////////////////////////// - tgba_complement::tgba_complement(const tgba* a) + tgba_safra_complement::tgba_safra_complement(const tgba* a) : automaton_(a), safra_(safra_determinisation::create_safra_automaton(a)) { assert(safra_ || "safra construction fails"); @@ -1134,14 +1134,14 @@ namespace spot } - tgba_complement::~tgba_complement() + tgba_safra_complement::~tgba_safra_complement() { get_dict()->unregister_all_my_variables(safra_); delete safra_; } state* - tgba_complement::get_init_state() const + tgba_safra_complement::get_init_state() const { bitset_t empty(safra_->get_nb_acceptance_pairs()); return new state_complement(empty, empty, safra_->get_initial_state(), @@ -1184,7 +1184,7 @@ namespace spot /// @param local_state /// tgba_succ_iterator* - tgba_complement::succ_iter(const state* local_state, + tgba_safra_complement::succ_iter(const state* local_state, const state* /* = 0 */, const tgba* /* = 0 */) const { @@ -1199,7 +1199,7 @@ namespace spot if (tr != safra_->automaton.end()) { bdd condition = bddfalse; - tgba_complement_succ_iterator::succ_list_t succ_list; + tgba_safra_complement_succ_iterator::succ_list_t succ_list; int nb_acceptance_pairs = safra_->get_nb_acceptance_pairs(); bitset_t e(nb_acceptance_pairs); @@ -1266,20 +1266,20 @@ namespace spot #endif } - return new tgba_complement_succ_iterator(succ_list, condition); + return new tgba_safra_complement_succ_iterator(succ_list, condition); } assert("Safra automaton does not find this node"); return 0; } bdd_dict* - tgba_complement::get_dict() const + tgba_safra_complement::get_dict() const { return automaton_->get_dict(); } std::string - tgba_complement::format_state(const state* state) const + tgba_safra_complement::format_state(const state* state) const { const state_complement* s = dynamic_cast(state); @@ -1288,7 +1288,7 @@ namespace spot } bdd - tgba_complement::all_acceptance_conditions() const + tgba_safra_complement::all_acceptance_conditions() const { #if TRANSFORM_TO_TBA return the_acceptance_cond_; @@ -1298,7 +1298,7 @@ namespace spot } bdd - tgba_complement::neg_acceptance_conditions() const + tgba_safra_complement::neg_acceptance_conditions() const { #if TRANSFORM_TO_TBA return !the_acceptance_cond_; @@ -1308,7 +1308,7 @@ namespace spot } bdd - tgba_complement::compute_support_conditions(const state* state) const + tgba_safra_complement::compute_support_conditions(const state* state) const { const state_complement* s = dynamic_cast(state); assert(s); @@ -1328,7 +1328,7 @@ namespace spot } bdd - tgba_complement::compute_support_variables(const state* state) const + tgba_safra_complement::compute_support_variables(const state* state) const { const state_complement* s = dynamic_cast(state); assert(s); @@ -1349,7 +1349,7 @@ namespace spot // display_safra: debug routine. ////////////////////////////// - void display_safra(const tgba_complement* a) + void display_safra(const tgba_safra_complement* a) { test::print_safra_automaton(a->get_safra()); } diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbasafracomplement.hh similarity index 87% rename from src/tgba/tgbacomplement.hh rename to src/tgba/tgbasafracomplement.hh index df494379b..c31a065c6 100644 --- a/src/tgba/tgbacomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -1,5 +1,5 @@ -#ifndef SPOT_TGBA_TGBACOMPLEMENT_HH -# define SPOT_TGBA_TGBACOMPLEMENT_HH +#ifndef SPOT_TGBA_TGBASAFRACOMPLEMENT_HH +# define SPOT_TGBA_TGBASAFRACOMPLEMENT_HH # include # include "tgba/tgba.hh" @@ -30,11 +30,11 @@ namespace spot /// is done on-the-fly when successors are called. /// /// \sa safra_determinisation, tgba_complement::succ_iter. - class tgba_complement : public tgba + class tgba_safra_complement : public tgba { public: - tgba_complement(const tgba* a); - virtual ~tgba_complement(); + tgba_safra_complement(const tgba* a); + virtual ~tgba_safra_complement(); safra_tree_automaton* get_safra() const { @@ -77,7 +77,7 @@ namespace spot /// @param a The \c tgba_complement with an intermediate Safra /// automaton to display /// - void display_safra(const tgba_complement* a); + void display_safra(const tgba_safra_complement* a); } -#endif // SPOT_TGBA_TGBACOMPLEMENT_HH +#endif // SPOT_TGBA_TGBASAFRACOMPLEMENT_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 79e473f04..8d09fb440 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -31,7 +31,7 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ bddprod \ - complement \ + safracomplement \ explicit \ expldot \ explprod \ diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index cdb5dc21f..40c986b9b 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -15,7 +15,7 @@ #include "ltlvisit/clone.hh" #include "tgba/tgbatba.hh" -#include "tgba/tgbacomplement.hh" +#include "tgba/tgbasafracomplement.hh" void usage(const char* prog) { @@ -98,7 +98,8 @@ int main(int argc, char* argv[]) if (spot::format_tgba_parse_errors(std::cerr, file, pel)) return 2; - spot::tgba_complement* complement = new spot::tgba_complement(a); + spot::tgba_safra_complement* complement = + new spot::tgba_safra_complement(a); if (print_automaton) spot::dotty_reachable(std::cout, complement); @@ -132,7 +133,8 @@ int main(int argc, char* argv[]) return 2; } - spot::tgba_complement* complement = new spot::tgba_complement(a); + spot::tgba_safra_complement* complement = + new spot::tgba_safra_complement(a); spot::tgba_statistics a_size = spot::stats_reachable(a); std::cout << "Original: " @@ -189,8 +191,8 @@ int main(int argc, char* argv[]) spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, spot::ltl::clone(f1)); spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); - spot::tgba_complement* nAf = new spot::tgba_complement(Af); - spot::tgba_complement* nAnf = new spot::tgba_complement(Anf); + spot::tgba_safra_complement* nAf = new spot::tgba_safra_complement(Af); + spot::tgba_safra_complement* nAnf = new spot::tgba_safra_complement(Anf); spot::tgba* prod = new spot::tgba_product(nAf, nAnf); spot::emptiness_check* ec = spot::couvreur99(prod); spot::emptiness_check_result* res = ec->check();