From 133bcf9442da9d079bd7f5e7f878017a9c7e8d15 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Apr 2004 12:05:20 +0000 Subject: [PATCH] Rename EESRG as SSP. * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/dottyeesrg.cc: Rename as ... * iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc: ... these. Adjust all classes and function names. * iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes filenames and function names. * m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS. --- ChangeLog | 9 + iface/gspn/Makefile.am | 28 +-- iface/gspn/{dottyeesrg.cc => dottyssp.cc} | 4 +- iface/gspn/ltlgspn.cc | 28 +-- iface/gspn/{eesrg.cc => ssp.cc} | 236 +++++++++++----------- iface/gspn/{eesrg.hh => ssp.hh} | 20 +- m4/gspnlib.m4 | 10 +- 7 files changed, 172 insertions(+), 163 deletions(-) rename iface/gspn/{dottyeesrg.cc => dottyssp.cc} (95%) rename iface/gspn/{eesrg.cc => ssp.cc} (73%) rename iface/gspn/{eesrg.hh => ssp.hh} (73%) diff --git a/ChangeLog b/ChangeLog index 55a1325d7..eb3cf7780 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,15 @@ 2004-04-15 Soheib Baarir Alexandre Duret-Lutz + Rename EESRG as SSP. + * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, + iface/gspn/dottyeesrg.cc: Rename as ... + * iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc: + ... these. Adjust all classes and function names. + * iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes + filenames and function names. + * m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS. + * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): Rewrite. (numbered_state_heap_hash_map::index): New functions. diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index c05a7c888..35d76dce6 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -28,7 +28,7 @@ gspn_HEADERS = \ common.hh \ gspn.hh -lib_LTLIBRARIES = libspotgspn.la libspotgspneesrg.la +lib_LTLIBRARIES = libspotgspn.la libspotgspnssp.la libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la libspotgspn_la_SOURCES = \ common.cc \ @@ -40,17 +40,17 @@ check_PROGRAMS = \ ltlgspn-rg \ ltlgspn-srg -if WITH_GSPN_EESRG -gspn_HEADERS += eesrg.hh +if WITH_GSPN_SSP +gspn_HEADERS += ssp.hh check_PROGRAMS += \ - dottygspn-eesrg \ - ltlgspn-eesrg + dottygspn-ssp \ + ltlgspn-ssp -libspotgspneesrg_la_LIBADD = $(top_builddir)/src/libspot.la -libspotgspneesrg_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS) -libspotgspneesrg_la_SOURCES = \ +libspotgspnssp_la_LIBADD = $(top_builddir)/src/libspot.la +libspotgspnssp_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS) +libspotgspnssp_la_SOURCES = \ common.cc \ - eesrg.cc + ssp.cc endif @@ -60,8 +60,8 @@ dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) dottygspn_srg_SOURCES = dottygspn.cc dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -dottygspn_eesrg_SOURCES = dottyeesrg.cc -dottygspn_eesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS) +dottygspn_ssp_SOURCES = dottyssp.cc +dottygspn_ssp_LDADD = libspotgspnssp.la $(LIBGSPNSSP_LDFLAGS) ltlgspn_rg_SOURCES = ltlgspn.cc ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) @@ -69,9 +69,9 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) ltlgspn_srg_SOURCES = ltlgspn.cc ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -ltlgspn_eesrg_SOURCES = ltlgspn.cc -ltlgspn_eesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS) -ltlgspn_eesrg_CPPFLAGS = -DEESRG=1 $(AM_CPPFLAGS) +ltlgspn_ssp_SOURCES = ltlgspn.cc +ltlgspn_ssp_LDADD = libspotgspnssp.la $(LIBGSPNSSP_LDFLAGS) +ltlgspn_ssp_CPPFLAGS = -DSSP=1 $(AM_CPPFLAGS) EXTRA_DIST = \ examples/DCSwave/DCSWave.def \ diff --git a/iface/gspn/dottyeesrg.cc b/iface/gspn/dottyssp.cc similarity index 95% rename from iface/gspn/dottyeesrg.cc rename to iface/gspn/dottyssp.cc index 887604f61..f9f7063cf 100644 --- a/iface/gspn/dottyeesrg.cc +++ b/iface/gspn/dottyssp.cc @@ -19,7 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "eesrg.hh" +#include "ssp.hh" #include "tgbaalgos/dotty.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaparse/public.hh" @@ -41,7 +41,7 @@ main(int argc, char **argv) env.declare(argv[--argc]); spot::bdd_dict* dict = new spot::bdd_dict(); - spot::gspn_eesrg_interface gspn(2, argv, dict, env); + spot::gspn_ssp_interface gspn(2, argv, dict, env); spot::tgba_parse_error_list pel1; spot::tgba_explicit* control = spot::tgba_parse(argv[--argc], pel1, diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 05c7040b9..860c19a3b 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -19,11 +19,11 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef EESRG +#ifndef SSP #include "gspn.hh" #define MIN_ARG 3 #else -#include "eesrg.hh" +#include "ssp.hh" #define MIN_ARG 4 #include "tgba/tgbaexplicit.hh" #include "tgbaparse/public.hh" @@ -43,7 +43,7 @@ void syntax(char* prog) { std::cerr << "Usage: "<< prog -#ifndef EESRG +#ifndef SSP << " [OPTIONS...] model formula props..." << std::endl #else << " [OPTIONS...] model formula automata props..." << std::endl @@ -54,7 +54,7 @@ syntax(char* prog) << std::endl << " -e use Couvreur's emptiness-check (default)" << std::endl << " -e2 use Couvreur's emptiness-check's shy variant" << std::endl -#ifdef EESRG +#ifdef SSP << " -e3 use semi-d. incl. Couvreur's emptiness-check" << std::endl << " -e4 use semi-d. incl. Couvreur's emptiness-check's shy variant" @@ -153,8 +153,8 @@ main(int argc, char **argv) argv[1] = argv[formula_index]; spot::bdd_dict* dict = new spot::bdd_dict(); -#if EESRG - spot::gspn_eesrg_interface gspn(2, argv, dict, env); +#if SSP + spot::gspn_ssp_interface gspn(2, argv, dict, env); spot::tgba_parse_error_list pel1; spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], @@ -177,7 +177,7 @@ main(int argc, char **argv) } spot::ltl::destroy(f); -#ifndef EESRG +#ifndef SSP spot::tgba* model = gspn.automaton(); spot::tgba_product* prod = new spot::tgba_product(model, a_f); #else @@ -204,15 +204,15 @@ main(int argc, char **argv) case Couvreur2: ec = new spot::emptiness_check_shy(prod); break; -#ifdef EESRG +#ifdef SSP case Couvreur3: - ec = spot::emptiness_check_eesrg_semi(prod); + ec = spot::emptiness_check_ssp_semi(prod); break; case Couvreur4: - ec = spot::emptiness_check_eesrg_shy_semi(prod); + ec = spot::emptiness_check_ssp_shy_semi(prod); break; case Couvreur5: - ec = spot::emptiness_check_eesrg_shy(prod); + ec = spot::emptiness_check_ssp_shy(prod); break; #endif default: @@ -227,10 +227,10 @@ main(int argc, char **argv) if (compute_counter_example) { spot::counter_example* ce; -#ifndef EESRG +#ifndef SSP ce = new spot::counter_example(ecs); #else - ce = spot::counter_example_eesrg(ecs); + ce = spot::counter_example_ssp(ecs); #endif ce->print_result(std::cout, proj ? model : 0); ce->print_stats(std::cout); @@ -273,7 +273,7 @@ main(int argc, char **argv) delete d; } } -#ifndef EESRG +#ifndef SSP delete prod; delete model; #else diff --git a/iface/gspn/eesrg.cc b/iface/gspn/ssp.cc similarity index 73% rename from iface/gspn/eesrg.cc rename to iface/gspn/ssp.cc index 6e3952e82..9d76888fe 100644 --- a/iface/gspn/eesrg.cc +++ b/iface/gspn/ssp.cc @@ -23,7 +23,7 @@ #include #include #include -#include "eesrg.hh" +#include "ssp.hh" #include "misc/bddlt.hh" #include #include "tgbaalgos/gtec/explscc.hh" @@ -48,19 +48,19 @@ namespace spot } } - // state_gspn_eesrg + // state_gspn_ssp ////////////////////////////////////////////////////////////////////// - class state_gspn_eesrg: public state + class state_gspn_ssp: public state { public: - state_gspn_eesrg(State left, const state* right) + state_gspn_ssp(State left, const state* right) : left_(left), right_(right) { } virtual - ~state_gspn_eesrg() + ~state_gspn_ssp() { delete right_; } @@ -68,7 +68,7 @@ namespace spot virtual int compare(const state* other) const { - const state_gspn_eesrg* o = dynamic_cast(other); + const state_gspn_ssp* o = dynamic_cast(other); assert(o); int res = (reinterpret_cast(o->left()) - reinterpret_cast(left())); @@ -84,9 +84,9 @@ namespace spot - static_cast(0)) << 10 + right_->hash(); } - virtual state_gspn_eesrg* clone() const + virtual state_gspn_ssp* clone() const { - return new state_gspn_eesrg(left(), right()->clone()); + return new state_gspn_ssp(left(), right()->clone()); } State @@ -104,12 +104,12 @@ namespace spot private: State left_; const state* right_; - }; // state_gspn_eesrg + }; // state_gspn_ssp - // tgba_gspn_eesrg_private_ + // tgba_gspn_ssp_private_ ////////////////////////////////////////////////////////////////////// - struct tgba_gspn_eesrg_private_ + struct tgba_gspn_ssp_private_ { int refs; // reference count @@ -122,7 +122,7 @@ namespace spot size_t prop_count; const tgba* operand; - tgba_gspn_eesrg_private_(bdd_dict* dict, const gspn_environment& env, + tgba_gspn_ssp_private_(bdd_dict* dict, const gspn_environment& env, const tgba* operand) : refs(1), dict(dict), all_props(0), operand(operand) @@ -158,7 +158,7 @@ namespace spot } } - tgba_gspn_eesrg_private_::~tgba_gspn_eesrg_private_() + tgba_gspn_ssp_private_::~tgba_gspn_ssp_private_() { dict->unregister_all_my_variables(this); if (all_props) @@ -167,13 +167,13 @@ namespace spot }; - // tgba_succ_iterator_gspn_eesrg + // tgba_succ_iterator_gspn_ssp ////////////////////////////////////////////////////////////////////// - class tgba_succ_iterator_gspn_eesrg: public tgba_succ_iterator + class tgba_succ_iterator_gspn_ssp: public tgba_succ_iterator { public: - tgba_succ_iterator_gspn_eesrg(Succ_* succ_tgba, + tgba_succ_iterator_gspn_ssp(Succ_* succ_tgba, size_t size_tgba, bdd* bdd_arry, state** state_arry, @@ -192,7 +192,7 @@ namespace spot } virtual - ~tgba_succ_iterator_gspn_eesrg() + ~tgba_succ_iterator_gspn_ssp() { for(size_t i = 0; i < size_states_; i++) @@ -237,7 +237,7 @@ namespace spot current_state() const { return - new state_gspn_eesrg(successors_[current_succ_].succ_, + new state_gspn_ssp(successors_[current_succ_].succ_, (state_array_[successors_[current_succ_] .arc->curr_state])->clone()); } @@ -271,20 +271,20 @@ namespace spot size_t size_states_; Props_* props_; int size_prop_; - }; // tgba_succ_iterator_gspn_eesrg + }; // tgba_succ_iterator_gspn_ssp - // tgba_gspn_eesrg + // tgba_gspn_ssp ////////////////////////////////////////////////////////////////////// - class tgba_gspn_eesrg: public tgba + class tgba_gspn_ssp: public tgba { public: - tgba_gspn_eesrg(bdd_dict* dict, const gspn_environment& env, + tgba_gspn_ssp(bdd_dict* dict, const gspn_environment& env, const tgba* operand); - tgba_gspn_eesrg(const tgba_gspn_eesrg& other); - tgba_gspn_eesrg& operator=(const tgba_gspn_eesrg& other); - virtual ~tgba_gspn_eesrg(); + tgba_gspn_ssp(const tgba_gspn_ssp& other); + tgba_gspn_ssp& operator=(const tgba_gspn_ssp& other); + virtual ~tgba_gspn_ssp(); virtual state* get_init_state() const; virtual tgba_succ_iterator* succ_iter(const state* local_state, @@ -299,52 +299,52 @@ namespace spot virtual bdd compute_support_conditions(const spot::state* state) const; virtual bdd compute_support_variables(const spot::state* state) const; private: - tgba_gspn_eesrg_private_* data_; + tgba_gspn_ssp_private_* data_; }; - tgba_gspn_eesrg::tgba_gspn_eesrg(bdd_dict* dict, const gspn_environment& env, + tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict, const gspn_environment& env, const tgba* operand) { - data_ = new tgba_gspn_eesrg_private_(dict, env, operand); + data_ = new tgba_gspn_ssp_private_(dict, env, operand); } - tgba_gspn_eesrg::tgba_gspn_eesrg(const tgba_gspn_eesrg& other) + tgba_gspn_ssp::tgba_gspn_ssp(const tgba_gspn_ssp& other) : tgba() { data_ = other.data_; ++data_->refs; } - tgba_gspn_eesrg::~tgba_gspn_eesrg() + tgba_gspn_ssp::~tgba_gspn_ssp() { if (--data_->refs == 0) delete data_; } - tgba_gspn_eesrg& - tgba_gspn_eesrg::operator=(const tgba_gspn_eesrg& other) + tgba_gspn_ssp& + tgba_gspn_ssp::operator=(const tgba_gspn_ssp& other) { if (&other == this) return *this; - this->~tgba_gspn_eesrg(); - new (this) tgba_gspn_eesrg(other); + this->~tgba_gspn_ssp(); + new (this) tgba_gspn_ssp(other); return *this; } - state* tgba_gspn_eesrg::get_init_state() const + state* tgba_gspn_ssp::get_init_state() const { - // Use 0 as initial state for the EESRG side. State 0 does not + // Use 0 as initial state for the SSP side. State 0 does not // exists, but when passed to succ() it will produce the list // of initial states. - return new state_gspn_eesrg(0, data_->operand->get_init_state()); + return new state_gspn_ssp(0, data_->operand->get_init_state()); } tgba_succ_iterator* - tgba_gspn_eesrg::succ_iter(const state* state_, + tgba_gspn_ssp::succ_iter(const state* state_, const state* global_state, const tgba* global_automaton) const { - const state_gspn_eesrg* s = dynamic_cast(state_); + const state_gspn_ssp* s = dynamic_cast(state_); assert(s); (void) global_state; (void) global_automaton; @@ -422,7 +422,7 @@ namespace spot res = 1; } - tgba_gspn_eesrg_private_::prop_map::iterator k + tgba_gspn_ssp_private_::prop_map::iterator k = data_->prop_dict.find(var); if (k != data_->prop_dict.end()) @@ -450,36 +450,36 @@ namespace spot } delete i; - return new tgba_succ_iterator_gspn_eesrg(succ_tgba_, size_tgba_, + return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_, bdd_array, state_array, size_states, props_, nb_arc_props); } bdd - tgba_gspn_eesrg::compute_support_conditions(const spot::state* state) const + tgba_gspn_ssp::compute_support_conditions(const spot::state* state) const { (void) state; return bddtrue; } bdd - tgba_gspn_eesrg::compute_support_variables(const spot::state* state) const + tgba_gspn_ssp::compute_support_variables(const spot::state* state) const { (void) state; return bddtrue; } bdd_dict* - tgba_gspn_eesrg::get_dict() const + tgba_gspn_ssp::get_dict() const { return data_->dict; } std::string - tgba_gspn_eesrg::format_state(const state* state) const + tgba_gspn_ssp::format_state(const state* state) const { - const state_gspn_eesrg* s = dynamic_cast(state); + const state_gspn_ssp* s = dynamic_cast(state); assert(s); char* str; State gs = s->left(); @@ -504,9 +504,9 @@ namespace spot } state* - tgba_gspn_eesrg::project_state(const state* s, const tgba* t) const + tgba_gspn_ssp::project_state(const state* s, const tgba* t) const { - const state_gspn_eesrg* s2 = dynamic_cast(s); + const state_gspn_ssp* s2 = dynamic_cast(s); assert(s2); if (t == this) return s2->clone(); @@ -514,7 +514,7 @@ namespace spot } bdd - tgba_gspn_eesrg::all_acceptance_conditions() const + tgba_gspn_ssp::all_acceptance_conditions() const { // There is no acceptance conditions in GSPN systems, they all // come from the operand automaton. @@ -522,17 +522,17 @@ namespace spot } bdd - tgba_gspn_eesrg::neg_acceptance_conditions() const + tgba_gspn_ssp::neg_acceptance_conditions() const { // There is no acceptance conditions in GSPN systems, they all // come from the operand automaton. return data_->operand->neg_acceptance_conditions(); } - // gspn_eesrg_interface + // gspn_ssp_interface ////////////////////////////////////////////////////////////////////// - gspn_eesrg_interface::gspn_eesrg_interface(int argc, char **argv, + gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv, bdd_dict* dict, const gspn_environment& env) : dict_(dict), env_(env) @@ -542,7 +542,7 @@ namespace spot throw gspn_exeption("initialize()", res); } - gspn_eesrg_interface::~gspn_eesrg_interface() + gspn_ssp_interface::~gspn_ssp_interface() { int res = finalize(); if (res) @@ -550,19 +550,19 @@ namespace spot } tgba* - gspn_eesrg_interface::automaton(const tgba* operand) const + gspn_ssp_interface::automaton(const tgba* operand) const { - return new tgba_gspn_eesrg(dict_, env_, operand); + return new tgba_gspn_ssp(dict_, env_, operand); } ////////////////////////////////////////////////////////////////////// - class connected_component_eesrg: public explicit_connected_component + class connected_component_ssp: public explicit_connected_component { public: virtual - ~connected_component_eesrg() + ~connected_component_ssp() { } @@ -573,8 +573,8 @@ namespace spot for (i = states.begin(); i !=states.end(); i++) { - const state_gspn_eesrg* old_state = (const state_gspn_eesrg*)(*i); - const state_gspn_eesrg* new_state = (const state_gspn_eesrg*)(s); + const state_gspn_ssp* old_state = (const state_gspn_ssp*)(*i); + const state_gspn_ssp* new_state = (const state_gspn_ssp*)(s); if ((old_state->right())->compare(new_state->right()) == 0 && old_state->left() @@ -601,31 +601,31 @@ namespace spot set_type states; }; - class connected_component_eesrg_factory : + class connected_component_ssp_factory : public explicit_connected_component_factory { public: - virtual connected_component_eesrg* + virtual connected_component_ssp* build() const { - return new connected_component_eesrg(); + return new connected_component_ssp(); } /// Get the unique instance of this class. - static const connected_component_eesrg_factory* + static const connected_component_ssp_factory* instance() { - static connected_component_eesrg_factory f; + static connected_component_ssp_factory f; return &f; } protected: virtual - ~connected_component_eesrg_factory() + ~connected_component_ssp_factory() { } /// Construction is forbiden. - connected_component_eesrg_factory() + connected_component_ssp_factory() { } }; @@ -633,11 +633,11 @@ namespace spot ////////////////////////////////////////////////////////////////////// - class numbered_state_heap_eesrg_semi : public numbered_state_heap + class numbered_state_heap_ssp_semi : public numbered_state_heap { public: virtual - ~numbered_state_heap_eesrg_semi() + ~numbered_state_heap_ssp_semi() { // Free keys in H. hash_type::iterator i = h.begin(); @@ -658,10 +658,10 @@ namespace spot hash_type::const_iterator i; for (i = h.begin(); i != h.end(); ++i) { - const state_gspn_eesrg* old_state = - dynamic_cast(i->first); - const state_gspn_eesrg* new_state = - dynamic_cast(s); + const state_gspn_ssp* old_state = + dynamic_cast(i->first); + const state_gspn_ssp* new_state = + dynamic_cast(s); assert(old_state); assert(new_state); @@ -701,10 +701,10 @@ namespace spot hash_type::iterator i; for (i = h.begin(); i != h.end(); ++i) { - const state_gspn_eesrg* old_state = - dynamic_cast(i->first); - const state_gspn_eesrg* new_state = - dynamic_cast(s); + const state_gspn_ssp* old_state = + dynamic_cast(i->first); + const state_gspn_ssp* new_state = + dynamic_cast(s); assert(old_state); assert(new_state); @@ -797,22 +797,22 @@ namespace spot state_ptr_hash, state_ptr_equal> hash_type; hash_type h; ///< Map of visited states. - friend class numbered_state_heap_eesrg_const_iterator; - friend class emptiness_check_shy_eesrg; + friend class numbered_state_heap_ssp_const_iterator; + friend class emptiness_check_shy_ssp; }; - class numbered_state_heap_eesrg_const_iterator : + class numbered_state_heap_ssp_const_iterator : public numbered_state_heap_const_iterator { public: - numbered_state_heap_eesrg_const_iterator - (const numbered_state_heap_eesrg_semi::hash_type& h) + numbered_state_heap_ssp_const_iterator + (const numbered_state_heap_ssp_semi::hash_type& h) : numbered_state_heap_const_iterator(), h(h) { } - ~numbered_state_heap_eesrg_const_iterator() + ~numbered_state_heap_ssp_const_iterator() { } @@ -847,57 +847,57 @@ namespace spot } private: - numbered_state_heap_eesrg_semi::hash_type::const_iterator i; - const numbered_state_heap_eesrg_semi::hash_type& h; + numbered_state_heap_ssp_semi::hash_type::const_iterator i; + const numbered_state_heap_ssp_semi::hash_type& h; }; numbered_state_heap_const_iterator* - numbered_state_heap_eesrg_semi::iterator() const + numbered_state_heap_ssp_semi::iterator() const { - return new numbered_state_heap_eesrg_const_iterator(h); + return new numbered_state_heap_ssp_const_iterator(h); } - /// \brief Factory for numbered_state_heap_eesrg_semi + /// \brief Factory for numbered_state_heap_ssp_semi /// /// This class is a singleton. Retrieve the instance using instance(). - class numbered_state_heap_eesrg_factory_semi: + class numbered_state_heap_ssp_factory_semi: public numbered_state_heap_factory { public: - virtual numbered_state_heap_eesrg_semi* + virtual numbered_state_heap_ssp_semi* build() const { - return new numbered_state_heap_eesrg_semi(); + return new numbered_state_heap_ssp_semi(); } /// Get the unique instance of this class. - static const numbered_state_heap_eesrg_factory_semi* + static const numbered_state_heap_ssp_factory_semi* instance() { - static numbered_state_heap_eesrg_factory_semi f; + static numbered_state_heap_ssp_factory_semi f; return &f; } protected: virtual - ~numbered_state_heap_eesrg_factory_semi() + ~numbered_state_heap_ssp_factory_semi() { } - numbered_state_heap_eesrg_factory_semi() + numbered_state_heap_ssp_factory_semi() { } }; - class emptiness_check_shy_eesrg : public emptiness_check_shy + class emptiness_check_shy_ssp : public emptiness_check_shy { public: - emptiness_check_shy_eesrg(const tgba* a) + emptiness_check_shy_ssp(const tgba* a) : emptiness_check_shy(a, - numbered_state_heap_eesrg_factory_semi::instance()) + numbered_state_heap_ssp_factory_semi::instance()) { } @@ -905,16 +905,16 @@ namespace spot virtual int* find_state(const state* s) { - typedef numbered_state_heap_eesrg_semi::hash_type hash_type; - hash_type& h = dynamic_cast(ecs_->h)->h; + typedef numbered_state_heap_ssp_semi::hash_type hash_type; + hash_type& h = dynamic_cast(ecs_->h)->h; hash_type::iterator i; for (i = h.begin(); i != h.end(); ++i) { - const state_gspn_eesrg* old_state = - dynamic_cast(i->first); - const state_gspn_eesrg* new_state = - dynamic_cast(s); + const state_gspn_ssp* old_state = + dynamic_cast(i->first); + const state_gspn_ssp* new_state = + dynamic_cast(s); assert(old_state); assert(new_state); @@ -943,8 +943,8 @@ namespace spot for (size_t i = 0; i < size_tgba_; i++) { - state_gspn_eesrg* s = - new state_gspn_eesrg + state_gspn_ssp* s = + new state_gspn_ssp (succ_tgba_[i], old_state->right()->clone()); queue.push_back(successor(queue.begin()->acc, s)); @@ -966,35 +966,35 @@ namespace spot emptiness_check* - emptiness_check_eesrg_semi(const tgba* eesrg_automata) + emptiness_check_ssp_semi(const tgba* ssp_automata) { - assert(dynamic_cast(eesrg_automata)); + assert(dynamic_cast(ssp_automata)); return - new emptiness_check(eesrg_automata, - numbered_state_heap_eesrg_factory_semi::instance()); + new emptiness_check(ssp_automata, + numbered_state_heap_ssp_factory_semi::instance()); } emptiness_check* - emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata) + emptiness_check_ssp_shy_semi(const tgba* ssp_automata) { - assert(dynamic_cast(eesrg_automata)); + assert(dynamic_cast(ssp_automata)); return new emptiness_check_shy - (eesrg_automata, - numbered_state_heap_eesrg_factory_semi::instance()); + (ssp_automata, + numbered_state_heap_ssp_factory_semi::instance()); } emptiness_check* - emptiness_check_eesrg_shy(const tgba* eesrg_automata) + emptiness_check_ssp_shy(const tgba* ssp_automata) { - assert(dynamic_cast(eesrg_automata)); - return new emptiness_check_shy_eesrg(eesrg_automata); + assert(dynamic_cast(ssp_automata)); + return new emptiness_check_shy_ssp(ssp_automata); } counter_example* - counter_example_eesrg(const emptiness_check_status* status) + counter_example_ssp(const emptiness_check_status* status) { return new counter_example(status, - connected_component_eesrg_factory::instance()); + connected_component_ssp_factory::instance()); } } diff --git a/iface/gspn/eesrg.hh b/iface/gspn/ssp.hh similarity index 73% rename from iface/gspn/eesrg.hh rename to iface/gspn/ssp.hh index 0c4228cc5..d525d771a 100644 --- a/iface/gspn/eesrg.hh +++ b/iface/gspn/ssp.hh @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_IFACE_GSPN_EESRG_HH -# define SPOT_IFACE_GSPN_EESRG_HH +#ifndef SPOT_IFACE_GSPN_SSP_HH +# define SPOT_IFACE_GSPN_SSP_HH // Do not include gspnlib.h here, or it will polute the user's // namespace with internal C symbols. @@ -34,23 +34,23 @@ namespace spot { - class gspn_eesrg_interface + class gspn_ssp_interface { public: - gspn_eesrg_interface(int argc, char **argv, + gspn_ssp_interface(int argc, char **argv, bdd_dict* dict, const gspn_environment& env); - ~gspn_eesrg_interface(); + ~gspn_ssp_interface(); tgba* automaton(const tgba* operand) const; private: bdd_dict* dict_; const gspn_environment& env_; }; - emptiness_check* emptiness_check_eesrg_semi(const tgba* eesrg_automata); - emptiness_check* emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata); - emptiness_check* emptiness_check_eesrg_shy(const tgba* eesrg_automata); + emptiness_check* emptiness_check_ssp_semi(const tgba* ssp_automata); + emptiness_check* emptiness_check_ssp_shy_semi(const tgba* ssp_automata); + emptiness_check* emptiness_check_ssp_shy(const tgba* ssp_automata); - counter_example* counter_example_eesrg(const emptiness_check_status* status); + counter_example* counter_example_ssp(const emptiness_check_status* status); } -#endif // SPOT_IFACE_GSPN_EESRG_GSPN_EESRG_HH +#endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH diff --git a/m4/gspnlib.m4 b/m4/gspnlib.m4 index 07b63b8f2..3c1283ea0 100644 --- a/m4/gspnlib.m4 +++ b/m4/gspnlib.m4 @@ -29,16 +29,16 @@ AC_DEFUN([AX_CHECK_GSPNLIB], [ LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" # Soheib Baarir is working on this library, and it is not part # of the GreatSPN repository yet. Use it only if it is here. - AC_CHECK_LIB([gspnESRG], [initialize], [have_eesrg=yes], - [have_eesrg=no], [-lm -lfl]) - LIBGSPNESRG_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnESRG -lm -lfl" + AC_CHECK_LIB([gspnSSP], [initialize], [have_ssp=yes], + [have_ssp=no], [-lm -lfl]) + LIBGSPNSSP_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnSSP -lm -lfl" LDFLAGS="$ax_tmp_LDFLAGS" LIBS="$ax_tmp_LIBS" fi AM_CONDITIONAL([WITH_GSPN], [test "x${with_gspn-no}" != xno]) - AM_CONDITIONAL([WITH_GSPN_EESRG], [test "x${have_eesrg-no}" != xno]) + AM_CONDITIONAL([WITH_GSPN_SSP], [test "x${have_ssp-no}" != xno]) AC_SUBST([LIBGSPN_CPPFLAGS]) AC_SUBST([LIBGSPNRG_LDFLAGS]) AC_SUBST([LIBGSPNSRG_LDFLAGS]) - AC_SUBST([LIBGSPNESRG_LDFLAGS]) + AC_SUBST([LIBGSPNSSP_LDFLAGS]) ])