* 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.

ChangeLog

@@ -1,5 +1,16 @@
 2004-06-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* 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,

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_;
-  }
-
 }

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 <string>
 # include <iostream>
-# 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<const std::string, ltl::atomic_prop*> 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

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)
 	{

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)
 	{

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();
+	  for (ltl::declarative_environment::prop_map::const_iterator i
-	       i != p.end(); ++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)
   {

iface/gspn/gspn.hh

@@ -28,6 +28,7 @@
 # include <string>
 # 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_;
   };
 }

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] == '-')
 	{

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,
+    tgba_gspn_ssp_private_(bdd_dict* dict,
-			     const tgba* operand)
+			   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();
+	  for (ltl::declarative_environment::prop_map::const_iterator i
-	       i != p.end(); ++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,
+    tgba_gspn_ssp(bdd_dict* dict, const ltl::declarative_environment& env,
-		    const tgba* operand);
+		  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,
+  tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict,
-				   const tgba* operand)
+			       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)
   {

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);

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
+  declenv.cc \
+  defaultenv.cc

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_;
+    }
+  }
+}

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 <string>
+# include <map>
+# 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<const std::string, ltl::atomic_prop*> 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