* configure.ac: Output src/ltlenv/Makefile.

* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
* src/ltlparse/public.hh (parse): Take an environment as third
argument.
* src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the
atomic proposition via the environment.
* src/ltltest/readltl.cc (main): Adjust the call to parse().
* src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.

ChangeLog

@@ -1,5 +1,15 @@
 2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* configure.ac: Output src/ltlenv/Makefile.
+	* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
+	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
+	* src/ltlparse/public.hh (parse): Take an environment as third
+	argument.
+	* src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the
+	atomic proposition via the environment.
+	* src/ltltest/readltl.cc (main): Adjust the call to parse().
+	* src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.
+
 	* src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files.
 	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
 	* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit

configure.ac

@@ -18,6 +18,7 @@ AC_CHECK_PROG([DOT], [dot], [dot])
 AC_CONFIG_FILES([
   Makefile
   src/Makefile
+  src/ltlenv/Makefile
   src/ltlast/Makefile
   src/ltlparse/Makefile
   src/ltltest/Makefile

src/Makefile.am

@@ -1,4 +1,4 @@
 AUTOMAKE_OPTIONS = subdir-objects
 
 # List directories in the order they must be built.
-SUBDIRS = misc ltlast ltlvisit ltlparse ltltest 
+SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse ltltest 

src/ltlenv/.cvsignore

@@ -0,0 +1,4 @@
+.deps
+Makefile
+Makefile.in
+libltlenv.a

src/ltlenv/Makefile.am

@@ -0,0 +1,8 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+lib_LIBRARIES = libltlenv.a
+libltlenv_a_SOURCES = \
+  defaultenv.cc \
+  defaultenv.hh \
+  environment.hh

src/ltlenv/defaultenv.cc

@@ -0,0 +1,33 @@
+#include "defaultenv.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    atomic_prop*
+    default_environment::require(const std::string& s)
+    {
+      return new atomic_prop(s);
+    }
+
+    const std::string&
+    default_environment::name()
+    {
+      static std::string name("default environment");
+      return name;
+    }
+
+    default_environment::default_environment()
+    {
+    }
+
+    default_environment& 
+    default_environment::instance()
+    {
+      static default_environment* singleton = new default_environment();
+      return *singleton;
+    }
+
+  }
+}

src/ltlenv/defaultenv.hh

@@ -0,0 +1,26 @@
+#ifndef SPOT_LTLENV_DEFAULT_ENVIRONMENT_HH
+# define SPOT_LTLENV_DEFAULT_ENVIRONMENT_HH
+
+# include "environment.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    class default_environment : public environment
+    {
+    public:
+      virtual atomic_prop* require(const std::string& prop_str);
+      virtual const std::string& name();
+
+      /* This class is a singleton.  */
+      static default_environment& instance();
+    protected:
+      default_environment();
+    };
+
+  }
+}
+
+#endif // SPOT_LTLENV_DEFAULT_ENVIRONMENT_HH

src/ltlenv/environment.hh

@@ -0,0 +1,29 @@
+#ifndef SPOT_LTLENV_ENVIRONMENT_HH
+# define SPOT_LTLENV_ENVIRONMENT_HH
+
+# include "ltlast/atomic_prop.hh"
+# include <string>
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    class environment
+    {
+    public:
+      // Check whether the environment contains the atomic proposition
+      // described by prop_str.
+      // Note this is NOT a const method.  Some environment will
+      // "create" the atomic proposition when asked.
+      virtual atomic_prop* require(const std::string& prop_str) = 0; 
+
+      virtual const std::string& name() = 0;
+      // FIXME: More functions will be needed later, but
+      // it's enough for now.
+    };
+
+  }
+}
+
+#endif // SPOT_LTLENV_ENVIRONMENT_HH

src/ltlparse/ltlparse.yy

@@ -31,6 +31,7 @@ namespace spot
   namespace ltl
   {
     extern parse_error_list* error_list;
+    extern environment* parse_environment;
   }
 }
 %}
@@ -93,7 +94,22 @@ many_errors: error
 	    | many_errors error
 
 subformula: ATOMIC_PROP
-	      { $$ = new atomic_prop(*$1); delete $1; }
+	      { 
+		$$ = parse_environment->require(*$1); 
+		if (! $$)
+		  {
+		    std::string s = "unknown atomic proposition `";
+		    s += *$1;
+		    s += "' in environment `";
+		    s += parse_environment->name();
+		    s += "'";
+		    error_list->push_back(parse_error(@1, s));
+		    delete $1; 
+		    YYERROR;
+		  }
+		else
+		  delete $1; 
+	      }
 	    | CONST_TRUE
               { $$ = new constant(constant::True); }
 	    | CONST_FALSE
@@ -162,14 +178,17 @@ namespace spot
   namespace ltl
   {
     parse_error_list* error_list;
+    environment* parse_environment;
 
     formula*
     parse(const std::string& ltl_string, 
 	  parse_error_list& error_list,
+	  environment& env,
 	  bool debug)
     {
       result = 0;
       ltl::error_list = &error_list;
+      parse_environment = &env;
       flex_set_buffer(ltl_string.c_str());
       yy::Parser parser(debug, yy::Location());
       parser.parse();  

src/ltlparse/public.hh

@@ -1,9 +1,10 @@
 #ifndef SPOT_LTLPARSE_PUBLIC_HH
 # define SPOT_LTLPARSE_PUBLIC_HH
 
-# include <string>
 # include "ltlast/formula.hh"
 # include "location.hh"
+# include "ltlenv/defaultenv.hh"
+# include <string>
 # include <list>
 # include <utility>
 # include <iostream>
@@ -17,8 +18,9 @@ namespace spot
 
     // Beware: this function is *not* reentrant.
     formula* parse(const std::string& ltl_string, 
-		    parse_error_list& error_list,
-		    bool debug = false);
+		   parse_error_list& error_list,
+		   environment& env = default_environment::instance(),
+		   bool debug = false);
 
     // Return true iff any diagnostic was output to os.
     bool format_parse_errors(std::ostream& os,

src/ltltest/Makefile.am

@@ -1,7 +1,8 @@
 AM_CPPFLAGS = -I$(srcdir)/..
 LDADD = ../ltlparse/libltlparse.a \
         ../ltlvisit/libltlvisit.a \
-        ../ltlast/libltlast.a 
+        ../ltlast/libltlast.a \
+	../ltlenv/libltlenv.a 
 
 check_SCRIPTS = defs
 

src/ltltest/readltl.cc

@@ -29,9 +29,10 @@ main(int argc, char **argv)
       formula_index = 2;
     }    
   
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::parse_error_list pel;
   spot::ltl::formula *f = spot::ltl::parse(argv[formula_index], 
-					    pel, debug);
+					   pel, env, debug);
 
   spot::ltl::parse_error_list::iterator it;
   exit_code =