diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 939dad973..a2ba35c4d 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -74,6 +74,8 @@ using namespace spot::ltl; /* All tokens. */ +%token START_LTL "LTL start marker" +%token START_RATEXP "RATEXP start marker" %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis" %token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace" %token OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator" @@ -124,27 +126,50 @@ using namespace spot::ltl; %printer { debug_stream() << *$$; } %% -result: subformula END_OF_INPUT - { result = $1; +result: START_LTL subformula END_OF_INPUT + { result = $2; YYACCEPT; } - | error END_OF_INPUT - { error_list.push_back(parse_error(@1, - "could not parse anything sensible")); + | START_LTL enderror + { result = 0; YYABORT; } - | subformula error END_OF_INPUT - { error_list.push_back(parse_error(@2, - "ignoring trailing garbage")); - result = $1; + | START_LTL subformula enderror + { + result = $2; YYACCEPT; } - | END_OF_INPUT - { error_list.push_back(parse_error(@$, "empty input")); + | START_LTL emptyinput + { YYABORT; } + | START_RATEXP rationalexp END_OF_INPUT + { result = $2; + YYACCEPT; + } + | START_RATEXP enderror + { result = 0; YYABORT; } + | START_RATEXP rationalexp enderror + { + result = $2; + YYACCEPT; + } + | START_RATEXP emptyinput + { YYABORT; } + +emptyinput: END_OF_INPUT + { + error_list.push_back(parse_error(@$, "empty input")); + result = 0; + } + +enderror: error END_OF_INPUT + { + error_list.push_back(parse_error(@1, + "ignoring trailing garbage")); + } /* The reason we use `constant::false_instance()' for error recovery is that it isn't reference counted. (Hence it can't leak references.) */ @@ -361,12 +386,29 @@ namespace spot bool debug) { formula* result = 0; - flex_set_buffer(ltl_string.c_str()); + flex_set_buffer(ltl_string.c_str(), + ltlyy::parser::token::START_LTL); ltlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); return result; } + + formula* + parse_ratexp(const std::string& ratexp_string, + parse_error_list& error_list, + environment& env, + bool debug) + { + formula* result = 0; + flex_set_buffer(ratexp_string.c_str(), + ltlyy::parser::token::START_RATEXP); + ltlyy::parser parser(error_list, env, result); + parser.set_debug_level(debug); + parser.parse(); + return result; + } + } } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 863d77dd9..b5a8b3d77 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -43,14 +43,16 @@ static const char* to_parse = 0; static size_t to_parse_size = 0; +static int start_token = 0; typedef ltlyy::parser::token token; void -flex_set_buffer(const char* buf) +flex_set_buffer(const char* buf, int start_tok) { to_parse = buf; to_parse_size = strlen(to_parse); + start_token = start_tok; } %} @@ -60,6 +62,12 @@ flex_set_buffer(const char* buf) %% %{ + if (start_token) + { + int t = start_token; + start_token = 0; + return t; + } yylloc->step(); %} diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh index 7d802296a..8c5edbfd8 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/ltlparse/parsedecl.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE) // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -29,6 +31,6 @@ int ltlyylex (ltlyy::parser::semantic_type *yylval, ltlyy::location *yylloc) YY_DECL; -void flex_set_buffer(const char *buf); +void flex_set_buffer(const char *buf, int start_tok); #endif // SPOT_LTLPARSE_PARSEDECL_HH diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 843036da7..e09f47113 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -72,14 +72,35 @@ namespace spot environment& env = default_environment::instance(), bool debug = false); - /// \brief Format diagnostics produced by spot::ltl::parse. + /// \brief Build a formula from a string representing a rational expression. + /// \param ratexp_string The string 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 formula built from \a ratexp_string, or + /// 0 if the input was unparsable. + /// + /// 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 ltl_string. If you want to make sure \a ltl_string + /// was parsed succesfully, check \a error_list for emptiness. + /// + /// \warning This function is not reentrant. + formula* parse_ratexp(const std::string& ratexp_string, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); + + /// \brief Format diagnostics produced by spot::ltl::parse + /// or spot::ltl::ratexp /// \param os Where diagnostics should be output. - /// \param ltl_string The string that were parsed. - /// \param error_list The error list filled by spot::ltl::parse while - /// parsing \a ltl_string. + /// \param input_string The string that were parsed. + /// \param error_list The error list filled by spot::ltl::parse + /// or spot::ltl::parse_ratexp while parsing \a input_string. /// \return \c true iff any diagnostic was output. bool format_parse_errors(std::ostream& os, - const std::string& ltl_string, + const std::string& input_string, parse_error_list& error_list); /// @}