diff --git a/ChangeLog b/ChangeLog index 0aa3fe0b3..ae4aa8519 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2004-06-02 Alexandre Duret-Lutz + * iface/gspn/common.cc, iface/gspn/common.hh: Remove the + class gspn_environment, and move it to ... + * src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file + as class declarative_environment. + * src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh. + (libltlenv_la_SOURCES): Add declenv.cc. + * iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc, + iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc, + iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references + to declarative_environment. + * HACKING, src/sanity/style.test: NULL is not portable, prohibit it. * iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, diff --git a/iface/gspn/common.cc b/iface/gspn/common.cc index 32f803887..ae025b201 100644 --- a/iface/gspn/common.cc +++ b/iface/gspn/common.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. // @@ -32,50 +32,4 @@ namespace spot return os; } - // gspn_environment - ////////////////////////////////////////////////////////////////////// - - gspn_environment::gspn_environment() - { - } - - gspn_environment::~gspn_environment() - { - for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i) - ltl::destroy(i->second); - } - - bool - gspn_environment::declare(const std::string& prop_str) - { - if (props_.find(prop_str) != props_.end()) - return false; - props_[prop_str] = ltl::atomic_prop::instance(prop_str, *this); - return true; - } - - ltl::formula* - gspn_environment::require(const std::string& prop_str) - { - prop_map::iterator i = props_.find(prop_str); - if (i == props_.end()) - return 0; - // It's an atomic_prop, so we do not have to use the clone() visitor. - return i->second->ref(); - } - - /// Get the name of the environment. - const std::string& - gspn_environment::name() - { - static std::string name("gspn environment"); - return name; - } - - const gspn_environment::prop_map& - gspn_environment::get_prop_map() const - { - return props_; - } - } diff --git a/iface/gspn/common.hh b/iface/gspn/common.hh index 5d90ae5a5..4acd216e2 100644 --- a/iface/gspn/common.hh +++ b/iface/gspn/common.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. // @@ -24,9 +24,6 @@ # include # include -# include "ltlast/atomic_prop.hh" -# include "ltlenv/environment.hh" - // Do not include gspnlib.h here, or it will polute the user's // namespace with internal C symbols. @@ -61,31 +58,6 @@ namespace spot }; std::ostream& operator<<(std::ostream& os, const gspn_exeption& e); - - class gspn_environment : public ltl::environment - { - public: - gspn_environment(); - ~gspn_environment(); - - /// Declare an atomic proposition. Return false iff the - /// proposition was already declared. - bool declare(const std::string& prop_str); - - virtual ltl::formula* require(const std::string& prop_str); - - /// Get the name of the environment. - virtual const std::string& name(); - - typedef std::map prop_map; - - /// Get the map of atomic proposition known to this environment. - const prop_map& get_prop_map() const; - - private: - prop_map props_; - }; - } #endif // SPOT_IFACE_GSPN_COMMON_HH diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc index 0d1836808..208d08e9f 100644 --- a/iface/gspn/dottygspn.cc +++ b/iface/gspn/dottygspn.cc @@ -26,7 +26,7 @@ int main(int argc, char **argv) try { - spot::gspn_environment env; + spot::ltl::declarative_environment env; if (argc <= 2) { diff --git a/iface/gspn/dottyssp.cc b/iface/gspn/dottyssp.cc index f9f7063cf..1d33619a0 100644 --- a/iface/gspn/dottyssp.cc +++ b/iface/gspn/dottyssp.cc @@ -28,7 +28,7 @@ int main(int argc, char **argv) try { - spot::gspn_environment env; + spot::ltl::declarative_environment env; if (argc <= 3) { diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 26e0d2ed0..c9bc35a94 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -92,16 +92,16 @@ namespace spot bdd alive_prop; bdd dead_prop; - tgba_gspn_private_(bdd_dict* dict, gspn_environment& env, + tgba_gspn_private_(bdd_dict* dict, ltl::declarative_environment& env, const std::string& dead) : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) { - const gspn_environment::prop_map& p = env.get_prop_map(); + const ltl::declarative_environment::prop_map& p = env.get_prop_map(); try { - for (gspn_environment::prop_map::const_iterator i = p.begin(); - i != p.end(); ++i) + for (ltl::declarative_environment::prop_map::const_iterator i + = p.begin(); i != p.end(); ++i) { // Skip the DEAD proposition, GreatSPN knows nothing // about it. @@ -319,7 +319,7 @@ namespace spot class tgba_gspn: public tgba { public: - tgba_gspn(bdd_dict* dict, gspn_environment& env, + tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, const std::string& dead); tgba_gspn(const tgba_gspn& other); tgba_gspn& operator=(const tgba_gspn& other); @@ -341,7 +341,7 @@ namespace spot }; - tgba_gspn::tgba_gspn(bdd_dict* dict, gspn_environment& env, + tgba_gspn::tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, const std::string& dead) { data_ = new tgba_gspn_private_(dict, env, dead); @@ -462,7 +462,8 @@ namespace spot ////////////////////////////////////////////////////////////////////// gspn_interface::gspn_interface(int argc, char **argv, - bdd_dict* dict, gspn_environment& env, + bdd_dict* dict, + ltl::declarative_environment& env, const std::string& dead) : dict_(dict), env_(env), dead_(dead) { diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index 4c48e2039..cdc912b47 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -28,6 +28,7 @@ # include # include "tgba/tgba.hh" # include "common.hh" +# include "ltlenv/declenv.hh" namespace spot { @@ -36,13 +37,13 @@ namespace spot { public: gspn_interface(int argc, char **argv, - bdd_dict* dict, gspn_environment& env, + bdd_dict* dict, ltl::declarative_environment& env, const std::string& dead = "true"); ~gspn_interface(); tgba* automaton() const; private: bdd_dict* dict_; - gspn_environment& env_; + ltl::declarative_environment& env_; const std::string dead_; }; } diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 75a6cb0dd..536f8bc48 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -90,7 +90,7 @@ main(int argc, char **argv) bool proj = true; std::string dead = "true"; - spot::gspn_environment env; + spot::ltl::declarative_environment env; while (formula_index < argc && *argv[formula_index] == '-') { diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index c4f42d0d4..9b75f5d95 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -122,19 +122,20 @@ namespace spot size_t prop_count; const tgba* operand; - tgba_gspn_ssp_private_(bdd_dict* dict, const gspn_environment& env, - const tgba* operand) + tgba_gspn_ssp_private_(bdd_dict* dict, + const ltl::declarative_environment& env, + const tgba* operand) : refs(1), dict(dict), all_props(0), operand(operand) { - const gspn_environment::prop_map& p = env.get_prop_map(); + const ltl::declarative_environment::prop_map& p = env.get_prop_map(); try { AtomicProp max_prop = 0; - for (gspn_environment::prop_map::const_iterator i = p.begin(); - i != p.end(); ++i) + for (ltl::declarative_environment::prop_map::const_iterator i + = p.begin(); i != p.end(); ++i) { int var = dict->register_proposition(i->second, this); AtomicProp index; @@ -280,8 +281,8 @@ namespace spot class tgba_gspn_ssp: public tgba { public: - tgba_gspn_ssp(bdd_dict* dict, const gspn_environment& env, - const tgba* operand); + tgba_gspn_ssp(bdd_dict* dict, const ltl::declarative_environment& env, + const tgba* operand); tgba_gspn_ssp(const tgba_gspn_ssp& other); tgba_gspn_ssp& operator=(const tgba_gspn_ssp& other); virtual ~tgba_gspn_ssp(); @@ -302,8 +303,9 @@ namespace spot tgba_gspn_ssp_private_* data_; }; - tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict, const gspn_environment& env, - const tgba* operand) + tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict, + const ltl::declarative_environment& env, + const tgba* operand) { data_ = new tgba_gspn_ssp_private_(dict, env, operand); } @@ -534,7 +536,8 @@ namespace spot gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv, bdd_dict* dict, - const gspn_environment& env, + const + ltl::declarative_environment& env, bool inclusion) : dict_(dict), env_(env) { diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index 8fab892f1..5e4996bf8 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -30,6 +30,7 @@ # include "common.hh" # include "tgbaalgos/gtec/gtec.hh" # include "tgbaalgos/gtec/ce.hh" +# include "ltlenv/declenv.hh" namespace spot { @@ -38,13 +39,13 @@ namespace spot { public: gspn_ssp_interface(int argc, char **argv, - bdd_dict* dict, const gspn_environment& env, + bdd_dict* dict, const ltl::declarative_environment& env, bool inclusion = false); ~gspn_ssp_interface(); tgba* automaton(const tgba* operand) const; private: bdd_dict* dict_; - const gspn_environment& env_; + const ltl::declarative_environment& env_; }; emptiness_check* emptiness_check_ssp_semi(const tgba* ssp_automata); diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am index e7a3a3dfb..c3dbf107f 100644 --- a/src/ltlenv/Makefile.am +++ b/src/ltlenv/Makefile.am @@ -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. ## @@ -25,9 +25,11 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) ltlenvdir = $(pkgincludedir)/ltlenv ltlenv_HEADERS = \ + declenv.hh \ defaultenv.hh \ environment.hh noinst_LTLIBRARIES = libltlenv.la libltlenv_la_SOURCES = \ - defaultenv.cc \ No newline at end of file + declenv.cc \ + defaultenv.cc diff --git a/src/ltlenv/declenv.cc b/src/ltlenv/declenv.cc new file mode 100644 index 000000000..9f3a5a55f --- /dev/null +++ b/src/ltlenv/declenv.cc @@ -0,0 +1,71 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "declenv.hh" + +namespace spot +{ + namespace ltl + { + + declarative_environment::declarative_environment() + { + } + + declarative_environment::~declarative_environment() + { + for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i) + ltl::destroy(i->second); + } + + bool + declarative_environment::declare(const std::string& prop_str) + { + if (props_.find(prop_str) != props_.end()) + return false; + props_[prop_str] = ltl::atomic_prop::instance(prop_str, *this); + return true; + } + + ltl::formula* + declarative_environment::require(const std::string& prop_str) + { + prop_map::iterator i = props_.find(prop_str); + if (i == props_.end()) + return 0; + // It's an atomic_prop, so we do not have to use the clone() visitor. + return i->second->ref(); + } + + const std::string& + declarative_environment::name() + { + static std::string name("declarative environment"); + return name; + } + + const declarative_environment::prop_map& + declarative_environment::get_prop_map() const + { + return props_; + } + } +} diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh new file mode 100644 index 000000000..58971348a --- /dev/null +++ b/src/ltlenv/declenv.hh @@ -0,0 +1,66 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_LTLENV_DECLENV_HH +# define SPOT_LTLENV_DECLENV_HH + +# include "environment.hh" +# include +# include +# include "ltlvisit/destroy.hh" +# include "ltlast/atomic_prop.hh" + +namespace spot +{ + namespace ltl + { + + /// \brief A declarative environment. + /// + /// This environment recognizes all atomic propositions + /// that have been previously declared. It will reject other. + class declarative_environment : public environment + { + public: + declarative_environment(); + ~declarative_environment(); + + /// Declare an atomic proposition. Return false iff the + /// proposition was already declared. + bool declare(const std::string& prop_str); + + virtual ltl::formula* require(const std::string& prop_str); + + /// Get the name of the environment. + virtual const std::string& name(); + + typedef std::map prop_map; + + /// Get the map of atomic proposition known to this environment. + const prop_map& get_prop_map() const; + + private: + prop_map props_; + }; + } +} + +#endif // SPOT_LTLENV_DECLENV_HH