From 6884a7f98583b4828079b63d430caf85196b66f8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jun 2003 15:22:42 +0000 Subject: [PATCH] * configure.ac: Output src/tgbaparse/Makefile. * src/Makefile.am (SUBDIRS): Add tgbaparse. (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise, tgba_explicit::add_neg_condition, tgba_explicit::add_neg_promise): New methods. * src/tgba/tgbaexplicit.hh: Declare them. * src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll, src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread. (TESTS): Add tgbaread.cc. (CLEANFILES): Add input. (tgbaread_SOURCES): New variable. --- ChangeLog | 18 +++++- configure.ac | 1 + src/Makefile.am | 5 +- src/ltlenv/environment.hh | 6 +- src/ltltest/readltl.cc | 1 - src/tgba/tgbaexplicit.cc | 28 ++++++-- src/tgba/tgbaexplicit.hh | 5 ++ src/tgbaparse/.cvsignore | 13 ++++ src/tgbaparse/Makefile.am | 31 +++++++++ src/tgbaparse/fmterror.cc | 20 ++++++ src/tgbaparse/parsedecl.hh | 32 ++++++++++ src/tgbaparse/public.hh | 49 ++++++++++++++ src/tgbaparse/tgbaparse.yy | 128 +++++++++++++++++++++++++++++++++++++ src/tgbaparse/tgbascan.ll | 81 +++++++++++++++++++++++ src/tgbatest/.cvsignore | 1 + src/tgbatest/Makefile.am | 9 ++- src/tgbatest/tgbaread.cc | 50 +++++++++++++++ src/tgbatest/tgbaread.test | 31 +++++++++ 18 files changed, 495 insertions(+), 14 deletions(-) create mode 100644 src/tgbaparse/.cvsignore create mode 100644 src/tgbaparse/Makefile.am create mode 100644 src/tgbaparse/fmterror.cc create mode 100644 src/tgbaparse/parsedecl.hh create mode 100644 src/tgbaparse/public.hh create mode 100644 src/tgbaparse/tgbaparse.yy create mode 100644 src/tgbaparse/tgbascan.ll create mode 100644 src/tgbatest/tgbaread.cc create mode 100755 src/tgbatest/tgbaread.test diff --git a/ChangeLog b/ChangeLog index c9da727ea..7fa12f7ca 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,21 @@ 2003-06-05 Alexandre Duret-Lutz + * configure.ac: Output src/tgbaparse/Makefile. + * src/Makefile.am (SUBDIRS): Add tgbaparse. + (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. + * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, + tgba_explicit::get_promise, tgba_explicit::add_neg_condition, + tgba_explicit::add_neg_promise): New methods. + * src/tgba/tgbaexplicit.hh: Declare them. + * src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc, + src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, + src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll, + src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread. + (TESTS): Add tgbaread.cc. + (CLEANFILES): Add input. + (tgbaread_SOURCES): New variable. + * src/ltlparse/ltlparse.yy: Typo in comment. * configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs. @@ -7,7 +23,7 @@ * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc and tgbaexplicit.hh. - * src/tgbatest/Makefile.am, src/tgbatest/defs.in, + * src/tgbatest/Makefile.am, src/tgbatest/defs.in, src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files. 2003-06-04 Alexandre Duret-Lutz diff --git a/configure.ac b/configure.ac index 6d88cfebc..d654f6602 100644 --- a/configure.ac +++ b/configure.ac @@ -33,6 +33,7 @@ AC_CONFIG_FILES([ src/ltlvisit/Makefile src/tgba/Makefile src/tgbaalgos/Makefile + src/tgbaparse/Makefile src/tgbatest/Makefile src/tgbatest/defs src/misc/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 836996887..002395e44 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -2,7 +2,7 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse tgba tgbaalgos . \ +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse tgba tgbaalgos tgbaparse . \ ltltest tgbatest lib_LTLIBRARIES = libspot.la @@ -13,4 +13,5 @@ libspot_la_LIBADD = \ ltlvisit/libltlvisit.la \ ltlast/libltlast.la \ tgba/libtgba.la \ - tgbaalgos/libtgbaalgos.la + tgbaalgos/libtgbaalgos.la \ + tgbaparse/libtgbaparse.la diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 299613d4b..534506a85 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -16,13 +16,13 @@ namespace spot /// \brief Obtain the formula associated to \a prop_str /// /// Usually \a prop_str, is the name of an atomic proposition, - /// a spot::ltl::require simply returns the associated + /// a spot::ltl::require simply returns the associated /// spot::ltl::atomic_prop. /// /// Note this is not a \c const method. Some environment will /// "create" the atomic proposition when asked. /// - /// We return a spot::ltl::formula instead of an + /// We return a spot::ltl::formula instead of an /// spot::ltl::atomic_prop, because this /// will allow nifty tricks (e.g., we could name formulae in an /// environment, and let the parser build a larger tree from @@ -30,7 +30,7 @@ namespace spot /// /// \return 0 iff \a prop_str is not part of the environment, /// or the associated spot::ltl::formula otherwise. - virtual formula* require(const std::string& prop_str) = 0; + virtual formula* require(const std::string& prop_str) = 0; /// Get the name of the environment. virtual const std::string& name() = 0; diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index 9457fe3bd..3a09bdbcc 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -36,7 +36,6 @@ main(int argc, char** argv) spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], pel, env, debug); - spot::ltl::parse_error_list::iterator it; exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 53d50f44a..f2ab0adae 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -122,7 +122,7 @@ namespace spot return t; } - void tgba_explicit::add_condition(transition* t, ltl::formula* f) + int tgba_explicit::get_condition(ltl::formula* f) { assert(dynamic_cast(f)); tgba_bdd_dict::fv_map::iterator i = dict_.var_map.find(f); @@ -137,10 +137,20 @@ namespace spot { v = i->second; } - t->condition &= ithvar(v); + return v; } - void tgba_explicit::add_promise(transition* t, ltl::formula* f) + void tgba_explicit::add_condition(transition* t, ltl::formula* f) + { + t->condition &= ithvar(get_condition(f)); + } + + void tgba_explicit::add_neg_condition(transition* t, ltl::formula* f) + { + t->condition &= ! ithvar(get_condition(f)); + } + + int tgba_explicit::get_promise(ltl::formula* f) { tgba_bdd_dict::fv_map::iterator i = dict_.prom_map.find(f); int v; @@ -154,7 +164,17 @@ namespace spot { v = i->second; } - t->promise &= ithvar(v); + return v; + } + + void tgba_explicit::add_promise(transition* t, ltl::formula* f) + { + t->promise &= ithvar(get_promise(f)); + } + + void tgba_explicit::add_neg_promise(transition* t, ltl::formula* f) + { + t->promise &= ! ithvar(get_promise(f)); } state* diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index f5e7922c3..8583337d1 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -32,7 +32,9 @@ namespace spot create_transition(const std::string& source, const std::string& dest); void add_condition(transition* t, ltl::formula* f); + void add_neg_condition(transition* t, ltl::formula* f); void add_promise(transition* t, ltl::formula* f); + void add_neg_promise(transition* t, ltl::formula* f); // tgba interface virtual ~tgba_explicit(); @@ -44,6 +46,9 @@ namespace spot protected: state* add_state(const std::string& name); + int get_condition(ltl::formula* f); + int get_promise(ltl::formula* f); + typedef std::map ns_map; typedef std::map sn_map; ns_map name_state_map_; diff --git a/src/tgbaparse/.cvsignore b/src/tgbaparse/.cvsignore new file mode 100644 index 000000000..0b2891e85 --- /dev/null +++ b/src/tgbaparse/.cvsignore @@ -0,0 +1,13 @@ +.deps +Makefile +Makefile.in +location.hh +tgbaparse.cc +tgbaparse.hh +tgbaparse.output +tgbascan.cc +position.hh +stack.hh +*.lo +*.la +.libs diff --git a/src/tgbaparse/Makefile.am b/src/tgbaparse/Makefile.am new file mode 100644 index 000000000..196e61887 --- /dev/null +++ b/src/tgbaparse/Makefile.am @@ -0,0 +1,31 @@ +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +noinst_LTLIBRARIES = libtgbaparse.la + +TGBAPARSE_YY = tgbaparse.yy +FROM_TGBAPARSE_YY_MAIN = tgbaparse.cc +FROM_TGBAPARSE_YY_OTHERS = \ + stack.hh \ + position.hh \ + location.hh \ + tgbaparse.hh +FROM_TGBAPARSE_YY = $(FROM_TGBAPARSE_YY_MAIN) $(FROM_TGBAPARSE_YY_OTHERS) + +BUILT_SOURCES = $(FROM_TGBAPARSE_YY) +MAINTAINERCLEANFILES = $(FROM_TGBAPARSE_YY) + +$(FROM_TGBAPARSE_YY_MAIN): $(srcdir)/$(TGBAPARSE_YY) + bison --defines --locations --skeleton=lalr1.cc --report=all \ + $(srcdir)/$(TGBAPARSE_YY) -o $@ +$(FROM_TGBAPARSE_YY_OTHERS): $(TGBAPARSE_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_TGBAPARSE_YY_MAIN) + +EXTRA_DIST = $(TGBAPARSE_YY) + +libtgbaparse_la_SOURCES = \ + fmterror.cc \ + $(FROM_TGBAPARSE_YY) \ + tgbascan.ll \ + parsedecl.hh \ + public.hh diff --git a/src/tgbaparse/fmterror.cc b/src/tgbaparse/fmterror.cc new file mode 100644 index 000000000..c182aed98 --- /dev/null +++ b/src/tgbaparse/fmterror.cc @@ -0,0 +1,20 @@ +#include "public.hh" + +namespace spot +{ + bool + format_tgba_parse_errors(std::ostream& os, + tgba_parse_error_list& error_list) + { + bool printed = false; + spot::tgba_parse_error_list::iterator it; + for (it = error_list.begin(); it != error_list.end(); ++it) + { + if (it->first.begin.filename != "") + os << it->first << ": "; + os << it->second << std::endl; + printed = true; + } + return printed; + } +} diff --git a/src/tgbaparse/parsedecl.hh b/src/tgbaparse/parsedecl.hh new file mode 100644 index 000000000..04799cbc3 --- /dev/null +++ b/src/tgbaparse/parsedecl.hh @@ -0,0 +1,32 @@ +#ifndef SPOT_TGBAPARSE_PARSEDECL_HH +# define SPOT_TGBAPARSE_PARSEDECL_HH + +#include +#include "tgbaparse.hh" +#include "location.hh" + +# define YY_DECL \ + int tgbayylex (yystype *yylval, yy::Location *yylloc) +YY_DECL; + +namespace spot +{ + int tgbayyopen(const std::string& name); + void tgbayyclose(); +} + + +// Gross kludge to compile yy::Parser in another namespace (tgbayy::) +// but still use yy::Location. The reason is that Bison's C++ +// skeleton does not support anything close to %name-prefix at the +// moment. All parser are named yy::Parser which makes it somewhat +// difficult to define multiple parsers. +namespace tgbayy +{ + using namespace yy; +} +#define yy tgbayy + + + +#endif // SPOT_TGBAPARSE_PARSEDECL_HH diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh new file mode 100644 index 000000000..1aca404db --- /dev/null +++ b/src/tgbaparse/public.hh @@ -0,0 +1,49 @@ +#ifndef SPOT_TGBAPARSE_PUBLIC_HH +# define SPOT_TGBAPARSE_PUBLIC_HH + +# include "tgba/tgbaexplicit.hh" +# include "location.hh" +# include "ltlenv/defaultenv.hh" +# include +# include +# include +# include + +namespace spot +{ + /// \brief A parse diagnostic with its location. + typedef std::pair tgba_parse_error; + /// \brief A list of parser diagnostics, as filled by parse. + typedef std::list tgba_parse_error_list; + + /// \brief Build a spot::tgba_explicit from a text file. + /// \param filename The name of the file to parse. + /// \param error_list A list that will be filled with + /// parse errors that occured during parsing. + /// \param env The environment into which parsing should take place. + /// \param debug When true, causes the parser to trace its execution. + /// \return A pointer to the tgba built from \a filename, or + /// 0 if the file could not be opened. + /// + /// Note that the parser usually tries to recover from errors. It can + /// return an non zero value even if it encountered error during the + /// parsing of \a filename. If you want to make sure \a filename + /// was parsed succesfully, check \a error_list for emptiness. + /// + /// \warning This function is not reentrant. + tgba_explicit* tgba_parse(const std::string& filename, + tgba_parse_error_list& error_list, + ltl::environment& env + = ltl::default_environment::instance(), + bool debug = false); + + /// \brief Format diagnostics produced by spot::tgba_parse. + /// \param os Where diagnostics should be output. + /// \param error_list The error list filled by spot::ltl::parse while + /// parsing \a ltl_string. + /// \return \c true iff any diagnostic was output. + bool format_tgba_parse_errors(std::ostream& os, + tgba_parse_error_list& error_list); +} + +#endif // SPOT_TGBAPARSE_PUBLIC_HH diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy new file mode 100644 index 000000000..15af160e7 --- /dev/null +++ b/src/tgbaparse/tgbaparse.yy @@ -0,0 +1,128 @@ +%{ +#include +#include "public.hh" +%} + +%parse-param {spot::tgba_parse_error_list &error_list} +%parse-param {spot::ltl::environment &parse_environment} +%parse-param {spot::tgba_explicit* &result} +%debug +%error-verbose +%union +{ + int token; + std::string* str; + std::list >* list; +} + +%{ +/* tgbaparse.hh and parsedecl.hh include each other recursively. + We mut ensure that YYSTYPE is declared (by the above %union) + before parsedecl.hh uses it. */ +#include "parsedecl.hh" +using namespace spot::ltl; + +/* Ugly hack so that Bison use tgbayylex, not yylex. + (%name-prefix doesn't work for the lalr1.cc skeleton + at the time of writing.) */ +#define yylex tgbayylex + +typedef std::pair pair; +%} + +%token STRING +%token IDENT +%type strident +%type prop_list + + +%% +lines: + | lines line + ; + +line: strident ',' strident ',' prop_list ',' prop_list ';' + { + spot::tgba_explicit::transition* t + = result->create_transition(*$1, *$3); + std::list::iterator i; + for (i = $5->begin(); i != $5->end(); ++i) + if (i->first) + result->add_neg_condition(t, i->second); + else + result->add_condition(t, i->second); + for (i = $7->begin(); i != $7->end(); ++i) + if (i->first) + result->add_neg_promise(t, i->second); + else + result->add_promise(t, i->second); + delete $1; + delete $3; + delete $5; + delete $7; + } + ; + +strident: STRING | IDENT; + +prop_list: + { + $$ = new std::list; + } + | prop_list IDENT + { + $1->push_back(pair(false, parse_environment.require(*$2))); + delete $2; + $$ = $1; + } + | prop_list '!' IDENT + { + $1->push_back(pair(true, parse_environment.require(*$3))); + delete $3; + $$ = $1; + } + ; + +; + +%% + +void +yy::Parser::print_() +{ + if (looka_ == STRING || looka_ == IDENT) + YYCDEBUG << " '" << *value.str << "'"; +} + +void +yy::Parser::error_() +{ + error_list.push_back(spot::tgba_parse_error(location, message)); +} + +namespace spot +{ + tgba_explicit* + tgba_parse(const std::string& name, + tgba_parse_error_list& error_list, + environment& env, + bool debug) + { + if (tgbayyopen(name)) + { + error_list.push_back + (tgba_parse_error(yy::Location(), + std::string("Cannot open file ") + name)); + return 0; + } + tgba_explicit* result = new tgba_explicit; + tgbayy::Parser parser(debug, yy::Location(), error_list, env, result); + parser.parse(); + tgbayyclose(); + return result; + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll new file mode 100644 index 000000000..61b108c45 --- /dev/null +++ b/src/tgbaparse/tgbascan.ll @@ -0,0 +1,81 @@ +%option noyywrap +%option prefix="tgbayy" +%option outfile="lex.yy.c" + +%{ +#include +#include "parsedecl.hh" + +#define YY_USER_ACTION \ + yylloc->columns(yyleng); + +#define YY_USER_INIT \ + do { \ + yylloc->begin.filename = current_file; \ + yylloc->end.filename = current_file; \ + } while (0) + +#define YY_NEVER_INTERACTIVE 1 + +static std::string current_file; + +%} + +eol \n|\r|\n\r|\r\n + +%% + +%{ + yylloc->step (); +%} + +\"[^\"]*\" { + yylval->str = new std::string(yytext + 1, + yyleng - 2); + return STRING; + } + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->str = new std::string(yytext); + return IDENT; + } + + /* discard whitespace */ +{eol} yylloc->lines(yyleng); yylloc->step(); +[ \t]+ yylloc->step(); + +. return *yytext; + +%{ + /* Dummy use of yyunput to shut up a gcc warning. */ + (void) &yyunput; +%} + +%% + +namespace spot +{ + int + tgbayyopen(const std::string &name) + { + if (name == "-") + { + yyin = stdin; + current_file = "standard input"; + } + else + { + yyin = fopen (name.c_str (), "r"); + current_file = name; + if (!yyin) + return 1; + } + return 0; + } + + void + tgbayyclose() + { + fclose(yyin); + } +} \ No newline at end of file diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index be7ec17d9..a64121d54 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -4,3 +4,4 @@ Makefile.in defs explicit .libs +tgbaread diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index b0bf14f38..e4bb9808f 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -4,13 +4,16 @@ LDADD = ../libspot.la check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ - explicit + explicit \ + tgbaread explicit_SOURCES = explicit.cc +tgbaread_SOURCES = tgbaread.cc TESTS = \ - explicit.test + explicit.test \ + tgbaread.test EXTRA_DIST = $(TESTS) -CLEANFILES = stdout expected +CLEANFILES = inpu stdout expected diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc new file mode 100644 index 000000000..5a1ecb0e5 --- /dev/null +++ b/src/tgbatest/tgbaread.cc @@ -0,0 +1,50 @@ +#include +#include "tgbaparse/public.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/dotty.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] filename" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug = false; + int filename_index = 1; + + if (!strcmp(argv[1], "-d")) + { + debug = true; + if (argc < 3) + syntax(argv[0]); + filename_index = 2; + } + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel; + spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], + pel, env, debug); + + exit_code = + spot::format_tgba_parse_errors(std::cerr, pel); + + if (a) + { + spot::dotty_reachable(std::cout, *a); + delete a; + } + else + { + exit_code = 1; + } + return exit_code; +} diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test new file mode 100755 index 000000000..fc175c239 --- /dev/null +++ b/src/tgbatest/tgbaread.test @@ -0,0 +1,31 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input < stdout + +cat >expected < 1 + 2 [label="s2"] + 1 -> 2 [label="\n"] + 3 [label="state 3"] + 2 -> 3 [label="\n"] + 3 -> 1 [label="T\nT"] +} +EOF + +diff stdout expected + +rm input stdout expected