Enable parsing stand-alone rational expressions with the LTL parser.

* src/ltlparse/ltlparse.yy (parse_ratexp): New function.
(START_LTL, START_RATEXP): Add these new tokens.
(result): Parse and LTL formula or a rational expression depending
on the start symbol.
* src/ltlparse/public.hh (parse_ratexp): New function.
* src/ltlparse/parsedecl.hh (flex_set_buffer): Add a new argument
to set the starting rule.
* src/ltlparse/ltlscan.ll (flex_set_buffer): Adjust.
(start_token): New global variable.  Return this as first token if
it is set.

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,26 +126,49 @@ using namespace spot::ltl;
 %printer { debug_stream() << *$$; } <str>
 
 %%
-result:       subformula END_OF_INPUT
+result:       START_LTL subformula END_OF_INPUT
-	      { result = $1;
+	      { result = $2;
 		YYACCEPT;
 	      }
-	    | error END_OF_INPUT
+	    | START_LTL enderror
-	      { error_list.push_back(parse_error(@1,
+	      {
-				      "could not parse anything sensible"));
 		result = 0;
 		YYABORT;
 	      }
-	    | subformula error END_OF_INPUT
+	    | START_LTL subformula enderror
-	      { error_list.push_back(parse_error(@2,
+	      {
+		result = $2;
+		YYACCEPT;
+	      }
+	    | 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"));
-		result = $1;
-		YYACCEPT;
-	      }
-	    | END_OF_INPUT
-              { error_list.push_back(parse_error(@$, "empty input"));
-		result = 0;
-		YYABORT;
 	      }
 
 /* The reason we use `constant::false_instance()' for error recovery
@@ -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;
+    }
+
   }
 }
 

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();
 %}
 

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

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 input_string The string that were parsed.
-    /// \param error_list The error list filled by spot::ltl::parse while
+    /// \param error_list The error list filled by spot::ltl::parse
-    ///        parsing \a ltl_string.
+    ///        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);
 
     /// @}