diff --git a/ChangeLog b/ChangeLog index 6abb10caf..624a9ce25 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,24 @@ +2004-02-02 Alexandre Duret-Lutz + + Hide the tgba_gspn and tgba_gspn_eesrg classes. Offer the + corresponding automaton via the automaton() method of the + gspn_interface and gspn_eesrg_interface classes. + + * iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take dict and + env arguments. + (gspn_interface::automaton): New method. + (tgba_gspn): Move all the declaration ... + * iface/gspn/gspn.cc (tgba_gspn): ... here. + (gspn_interface::automaton): Implement it. + * iface/gspn/eesrg.hh (gspn_eesrg_interface::gspn_eesrg_interface): + Take dict and env arguments. + (gspn_eesrg_interface::automaton): New method. + (tgba_gspn_eesrg): Move all the declaration ... + * iface/gspn/gspn.cc (tgba_gspn_eesrg): ... here. + (gspn_eesrg_interface::automaton): Implement it. + * iface/gspn/dottygspn.cc, iface/gspn/dottyeesrg.cc, + iface/gspn/ltlgspn.cc: Adjust. + 2004-01-30 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc: Fix output of F0, F1, G0, G1, X0, and X1. diff --git a/iface/gspn/dottyeesrg.cc b/iface/gspn/dottyeesrg.cc index cd628688f..887604f61 100644 --- a/iface/gspn/dottyeesrg.cc +++ b/iface/gspn/dottyeesrg.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -40,8 +40,8 @@ main(int argc, char **argv) while (argc > 3) env.declare(argv[--argc]); - spot::gspn_eesrg_interface gspn(2, argv); spot::bdd_dict* dict = new spot::bdd_dict(); + spot::gspn_eesrg_interface gspn(2, argv, dict, env); spot::tgba_parse_error_list pel1; spot::tgba_explicit* control = spot::tgba_parse(argv[--argc], pel1, @@ -49,12 +49,10 @@ main(int argc, char **argv) if (spot::format_tgba_parse_errors(std::cerr, pel1)) return 2; - { - spot::tgba_gspn_eesrg a(dict, env, control); - - spot::dotty_reachable(std::cout, &a); - } + spot::tgba* a = gspn.automaton(control); + spot::dotty_reachable(std::cout, a); + delete a; delete control; delete dict; } diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc index 4f44e5ed8..0d1836808 100644 --- a/iface/gspn/dottygspn.cc +++ b/iface/gspn/dottygspn.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -40,16 +40,13 @@ main(int argc, char **argv) --argc; } - spot::gspn_interface gspn(2, argv); - spot::bdd_dict* dict = new spot::bdd_dict(); + spot::gspn_interface gspn(2, argv, dict, env); + spot::tgba* a = gspn.automaton(); - { - spot::tgba_gspn a(dict, env); - - spot::dotty_reachable(std::cout, &a); - } + spot::dotty_reachable(std::cout, a); + delete a; delete dict; } catch (spot::gspn_exeption e) diff --git a/iface/gspn/eesrg.cc b/iface/gspn/eesrg.cc index edd0ad4cf..b953b1038 100644 --- a/iface/gspn/eesrg.cc +++ b/iface/gspn/eesrg.cc @@ -30,21 +30,6 @@ namespace spot { - gspn_eesrg_interface::gspn_eesrg_interface(int argc, char **argv) - { - int res = initialize(argc, argv); - if (res) - throw gspn_exeption("initialize()", res); - } - - gspn_eesrg_interface::~gspn_eesrg_interface() - { - int res = finalize(); - if (res) - throw gspn_exeption("finalize()", res); - } - - // state_gspn_eesrg ////////////////////////////////////////////////////////////////////// @@ -345,6 +330,30 @@ namespace spot // tgba_gspn_eesrg ////////////////////////////////////////////////////////////////////// + class tgba_gspn_eesrg: public tgba + { + public: + tgba_gspn_eesrg(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(); + virtual state* get_init_state() const; + virtual tgba_succ_iterator* + 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 spot::state* state) const; + virtual bdd compute_support_variables(const spot::state* state) const; + private: + tgba_gspn_eesrg_private_* data_; + }; tgba_gspn_eesrg::tgba_gspn_eesrg(bdd_dict* dict, const gspn_environment& env, const tgba* operand) @@ -469,4 +478,30 @@ namespace spot return data_->operand->neg_acceptance_conditions(); } + // gspn_eesrg_interface + ////////////////////////////////////////////////////////////////////// + + gspn_eesrg_interface::gspn_eesrg_interface(int argc, char **argv, + bdd_dict* dict, + const gspn_environment& env) + : dict_(dict), env_(env) + { + int res = initialize(argc, argv); + if (res) + throw gspn_exeption("initialize()", res); + } + + gspn_eesrg_interface::~gspn_eesrg_interface() + { + int res = finalize(); + if (res) + throw gspn_exeption("finalize()", res); + } + + tgba* + gspn_eesrg_interface::automaton(const tgba* operand) const + { + return new tgba_gspn_eesrg(dict_, env_, operand); + } + } diff --git a/iface/gspn/eesrg.hh b/iface/gspn/eesrg.hh index 05bcaf6b2..a63355d06 100644 --- a/iface/gspn/eesrg.hh +++ b/iface/gspn/eesrg.hh @@ -35,39 +35,13 @@ namespace spot class gspn_eesrg_interface { public: - gspn_eesrg_interface(int argc, char **argv); + gspn_eesrg_interface(int argc, char **argv, + bdd_dict* dict, const gspn_environment& env); ~gspn_eesrg_interface(); - // FIXME: I think we should have - // tgba* get_automata(); - }; - - - /// Data private to tgba_gspn. - struct tgba_gspn_eesrg_private_; - - class tgba_gspn_eesrg: public tgba - { - public: - tgba_gspn_eesrg(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(); - virtual state* get_init_state() const; - virtual tgba_succ_iterator* - 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 spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; + tgba* automaton(const tgba* operand) const; private: - tgba_gspn_eesrg_private_* data_; + bdd_dict* dict_; + const gspn_environment& env_; }; } diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 9262f525e..772c37003 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -27,21 +27,6 @@ namespace spot { - gspn_interface::gspn_interface(int argc, char **argv) - { - int res = initialize(argc, argv); - if (res) - throw gspn_exeption("initialize()", res); - } - - gspn_interface::~gspn_interface() - { - int res = finalize(); - if (res) - throw gspn_exeption("finalize()", res); - } - - // state_gspn ////////////////////////////////////////////////////////////////////// @@ -276,6 +261,35 @@ namespace spot ////////////////////////////////////////////////////////////////////// + + + /// Data private to tgba_gspn. + struct tgba_gspn_private_; + + class tgba_gspn: public tgba + { + public: + tgba_gspn(bdd_dict* dict, const gspn_environment& env); + tgba_gspn(const tgba_gspn& other); + tgba_gspn& operator=(const tgba_gspn& other); + virtual ~tgba_gspn(); + virtual state* get_init_state() const; + virtual tgba_succ_iterator* + 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 bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + protected: + virtual bdd compute_support_conditions(const spot::state* state) const; + virtual bdd compute_support_variables(const spot::state* state) const; + private: + tgba_gspn_private_* data_; + }; + + tgba_gspn::tgba_gspn(bdd_dict* dict, const gspn_environment& env) { data_ = new tgba_gspn_private_(dict, env); @@ -392,6 +406,31 @@ namespace spot return bddtrue; } + // gspn_interface + ////////////////////////////////////////////////////////////////////// + + gspn_interface::gspn_interface(int argc, char **argv, + bdd_dict* dict, const gspn_environment& env) + : dict_(dict), env_(env) + { + int res = initialize(argc, argv); + if (res) + throw gspn_exeption("initialize()", res); + } + + gspn_interface::~gspn_interface() + { + int res = finalize(); + if (res) + throw gspn_exeption("finalize()", res); + } + + tgba* + gspn_interface::automaton() const + { + return new tgba_gspn(dict_, env_); + } + } diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index a9cc3508e..5bd1927e2 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -35,39 +35,14 @@ namespace spot class gspn_interface { public: - gspn_interface(int argc, char **argv); + gspn_interface(int argc, char **argv, + bdd_dict* dict, const gspn_environment& env); ~gspn_interface(); - // FIXME: I think we should have - // tgba* get_automata(); - }; - - - /// Data private to tgba_gspn. - struct tgba_gspn_private_; - - class tgba_gspn: public tgba - { - public: - tgba_gspn(bdd_dict* dict, const gspn_environment& env); - tgba_gspn(const tgba_gspn& other); - tgba_gspn& operator=(const tgba_gspn& other); - virtual ~tgba_gspn(); - virtual state* get_init_state() const; - virtual tgba_succ_iterator* - 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 bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - protected: - virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; + tgba* automaton() const; private: - tgba_gspn_private_* data_; + bdd_dict* dict_; + const gspn_environment& env_; }; - } #endif // SPOT_IFACE_GSPN_GSPN_HH diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 1bdfdc8de..345f19f79 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -132,7 +132,7 @@ main(int argc, char **argv) spot::bdd_dict* dict = new spot::bdd_dict(); #if EESRG - spot::gspn_eesrg_interface gspn(2, argv); + spot::gspn_eesrg_interface gspn(2, argv, dict, env); spot::tgba_parse_error_list pel1; spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], @@ -140,7 +140,7 @@ main(int argc, char **argv) if (spot::format_tgba_parse_errors(std::cerr, pel1)) return 2; #else - spot::gspn_interface gspn(2, argv); + spot::gspn_interface gspn(2, argv, dict, env); #endif spot::tgba* a_f = 0; @@ -156,11 +156,11 @@ main(int argc, char **argv) spot::ltl::destroy(f); #ifndef EESRG - spot::tgba* model = new spot::tgba_gspn(dict, env); + spot::tgba* model = gspn.automaton(); spot::tgba_product* prod = new spot::tgba_product(model, a_f); #else spot::tgba_product* ca = new spot::tgba_product(control, a_f); - spot::tgba* model = new spot::tgba_gspn_eesrg(dict, env, ca); + spot::tgba* model = gspn.automaton(ca); spot::tgba* prod = model; #endif