diff --git a/ChangeLog b/ChangeLog index 46ef404e0..ef8a6e689 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2003-04-17 Alexandre DURET-LUTZ + * 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 diff --git a/configure.ac b/configure.ac index 9ba463d70..bb973ad9c 100644 --- a/configure.ac +++ b/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 diff --git a/src/Makefile.am b/src/Makefile.am index 9a56ba1a5..ca2c21a03 100644 --- a/src/Makefile.am +++ b/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 diff --git a/src/ltlenv/.cvsignore b/src/ltlenv/.cvsignore new file mode 100644 index 000000000..4908c148a --- /dev/null +++ b/src/ltlenv/.cvsignore @@ -0,0 +1,4 @@ +.deps +Makefile +Makefile.in +libltlenv.a diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am new file mode 100644 index 000000000..6d97fa371 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/ltlenv/defaultenv.cc b/src/ltlenv/defaultenv.cc new file mode 100644 index 000000000..03bd64520 --- /dev/null +++ b/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; + } + + } +} diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh new file mode 100644 index 000000000..d8266feb0 --- /dev/null +++ b/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 diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh new file mode 100644 index 000000000..3e70fea2d --- /dev/null +++ b/src/ltlenv/environment.hh @@ -0,0 +1,29 @@ +#ifndef SPOT_LTLENV_ENVIRONMENT_HH +# define SPOT_LTLENV_ENVIRONMENT_HH + +# include "ltlast/atomic_prop.hh" +# include + +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 diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 16e76a566..83550f346 100644 --- a/src/ltlparse/ltlparse.yy +++ b/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(); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 1a13553cc..ebb8be038 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -1,9 +1,10 @@ #ifndef SPOT_LTLPARSE_PUBLIC_HH # define SPOT_LTLPARSE_PUBLIC_HH -# include # include "ltlast/formula.hh" # include "location.hh" +# include "ltlenv/defaultenv.hh" +# include # include # include # include @@ -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, diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 5095a4d56..f056d381f 100644 --- a/src/ltltest/Makefile.am +++ b/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 diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index 4e7486bc3..04c0db8fe 100644 --- a/src/ltltest/readltl.cc +++ b/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 =