Add a parse_boolean() function to use in parsers for Automata.

* src/ltlparse/public.hh, src/ltlparse/ltlparse.yy (parse_boolean):
New function.
* src/neverparse/neverclaimparse.yy, src/tgbaparse/tgbaparse.yy:
Use it.

src/ltlparse/ltlparse.yy

@@ -86,12 +86,14 @@ using namespace spot::ltl;
     }							\
   while (0);
 
+  enum parser_type { parser_ltl, parser_bool, parser_sere };
+
   const formula*
   try_recursive_parse(const std::string& str,
 		      const ltlyy::location& location,
 		      spot::ltl::environment& env,
 		      bool debug,
-		      bool sere,
+		      parser_type type,
 		      spot::ltl::parse_error_list& error_list)
     {
       // We want to parse a U (b U c) as two until operators applied
@@ -117,11 +119,19 @@ using namespace spot::ltl;
 	}
 
       spot::ltl::parse_error_list suberror;
-      const spot::ltl::formula* f;
+      const spot::ltl::formula* f = 0;
-      if (sere)
+      switch (type)
-	f = spot::ltl::parse_sere(str, suberror, env, debug, true);
+	{
-      else
+	case parser_sere:
-	f = spot::ltl::parse(str, suberror, env, debug, true);
+	  f = spot::ltl::parse_sere(str, suberror, env, debug, true);
+	  break;
+	case parser_bool:
+	  f = spot::ltl::parse_boolean(str, suberror, env, debug, true);
+	  break;
+	case parser_ltl:
+	  f = spot::ltl::parse(str, suberror, env, debug, true);
+	  break;
+	}
 
       if (suberror.empty())
 	return f;
@@ -149,6 +159,7 @@ using namespace spot::ltl;
 %token START_LTL "LTL start marker"
 %token START_LBT "LBT start marker"
 %token START_SERE "SERE start marker"
+%token START_BOOL "BOOLEAN start marker"
 %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
 %token <str> PAR_BLOCK "(...) block"
 %token <str> BRA_BLOCK "{...} block"
@@ -214,7 +225,7 @@ using namespace spot::ltl;
 
 %nonassoc OP_POST_NEG OP_POST_POS
 
-%type <ltl> subformula booleanatom sere lbtformula
+%type <ltl> subformula booleanatom sere lbtformula boolformula
 %type <ltl> bracedsere parenthesedsubformula
 %type <minmax> starargs equalargs sqbracketargs gotoargs
 
@@ -244,6 +255,22 @@ result:       START_LTL subformula END_OF_INPUT
 	      }
 	    | START_LTL emptyinput
               { YYABORT; }
+            | START_BOOL boolformula END_OF_INPUT
+	      { result = $2;
+		YYACCEPT;
+	      }
+	    | START_BOOL enderror
+	      {
+		result = 0;
+		YYABORT;
+	      }
+	    | START_BOOL boolformula enderror
+	      {
+		result = $2;
+		YYACCEPT;
+	      }
+	    | START_BOOL emptyinput
+              { YYABORT; }
             | START_SERE sere END_OF_INPUT
 	      { result = $2;
 		YYACCEPT;
@@ -439,7 +466,7 @@ sere: booleanatom
 	    | PAR_BLOCK
               {
 		$$ = try_recursive_parse(*$1, @1, parse_environment,
-					 debug_level(), true, error_list);
+					 debug_level(), parser_sere, error_list);
 		delete $1;
 		if (!$$)
 		  YYERROR;
@@ -659,7 +686,8 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE
             | BRA_BLOCK
               {
 		$$ = try_recursive_parse(*$1, @1, parse_environment,
-					 debug_level(), true, error_list);
+					 debug_level(),
+					 parser_sere, error_list);
 		delete $1;
 		if (!$$)
 		  YYERROR;
@@ -668,7 +696,7 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE
 parenthesedsubformula: PAR_BLOCK
               {
 		$$ = try_recursive_parse(*$1, @1, parse_environment,
-					 debug_level(), false, error_list);
+					 debug_level(), parser_ltl, error_list);
 		delete $1;
 		if (!$$)
 		  YYERROR;
@@ -702,6 +730,75 @@ parenthesedsubformula: PAR_BLOCK
 	      }
 
 
+boolformula: booleanatom
+            | PAR_BLOCK
+              {
+		$$ = try_recursive_parse(*$1, @1, parse_environment,
+					 debug_level(), parser_bool, error_list);
+		delete $1;
+		if (!$$)
+		  YYERROR;
+	      }
+            | PAR_OPEN boolformula PAR_CLOSE
+	      { $$ = $2; }
+	    | PAR_OPEN boolformula error PAR_CLOSE
+	      { error_list.push_back(parse_error(@3, "ignoring this"));
+		$$ = $2;
+	      }
+	    | PAR_OPEN error PAR_CLOSE
+	      { error_list.push_back(parse_error(@$,
+		 "treating this parenthetical block as false"));
+		$$ = constant::false_instance();
+	      }
+	    | PAR_OPEN boolformula END_OF_INPUT
+	      { error_list.push_back(parse_error(@1 + @2,
+				      "missing closing parenthesis"));
+		$$ = $2;
+	      }
+	    | PAR_OPEN boolformula error END_OF_INPUT
+	      { error_list.push_back(parse_error(@3,
+                "ignoring trailing garbage and missing closing parenthesis"));
+		$$ = $2;
+	      }
+	    | PAR_OPEN error END_OF_INPUT
+	      { error_list.push_back(parse_error(@$,
+                    "missing closing parenthesis, "
+		    "treating this parenthetical block as false"));
+		$$ = constant::false_instance();
+	      }
+	    | boolformula OP_AND boolformula
+	      { $$ = multop::instance(multop::And, $1, $3); }
+	    | boolformula OP_AND error
+              { missing_right_binop($$, $1, @2, "and operator"); }
+	    | boolformula OP_SHORT_AND boolformula
+	      { $$ = multop::instance(multop::And, $1, $3); }
+	    | boolformula OP_SHORT_AND error
+              { missing_right_binop($$, $1, @2, "and operator"); }
+	    | boolformula OP_STAR boolformula
+	      { $$ = multop::instance(multop::And, $1, $3); }
+	    | boolformula OP_STAR error
+              { missing_right_binop($$, $1, @2, "and operator"); }
+	    | boolformula OP_OR boolformula
+	      { $$ = multop::instance(multop::Or, $1, $3); }
+	    | boolformula OP_OR error
+              { missing_right_binop($$, $1, @2, "or operator"); }
+	    | boolformula OP_XOR boolformula
+	      { $$ = binop::instance(binop::Xor, $1, $3); }
+	    | boolformula OP_XOR error
+	      { missing_right_binop($$, $1, @2, "xor operator"); }
+	    | boolformula OP_IMPLIES boolformula
+	      { $$ = binop::instance(binop::Implies, $1, $3); }
+	    | boolformula OP_IMPLIES error
+	      { missing_right_binop($$, $1, @2, "implication operator"); }
+	    | boolformula OP_EQUIV boolformula
+	      { $$ = binop::instance(binop::Equiv, $1, $3); }
+	    | boolformula OP_EQUIV error
+	      { missing_right_binop($$, $1, @2, "equivalent operator"); }
+	    | OP_NOT boolformula
+	      { $$ = unop::instance(unop::Not, $2); }
+	    | OP_NOT error
+	      { missing_right_op($$, @1, "not operator"); }
+
 subformula: booleanatom
             | parenthesedsubformula
 	    | subformula OP_AND subformula
@@ -806,7 +903,7 @@ subformula: booleanatom
             | BRA_BANG_BLOCK
               {
 		$$ = try_recursive_parse(*$1, @1, parse_environment,
-					 debug_level(), true, error_list);
+					 debug_level(), parser_sere, error_list);
 		delete $1;
 		if (!$$)
 		  YYERROR;
@@ -894,6 +991,23 @@ namespace spot
       return result;
     }
 
+    const formula*
+    parse_boolean(const std::string& ltl_string,
+		  parse_error_list& error_list,
+		  environment& env,
+		  bool debug, bool lenient)
+    {
+      const formula* result = 0;
+      flex_set_buffer(ltl_string.c_str(),
+		      ltlyy::parser::token::START_BOOL,
+		      lenient);
+      ltlyy::parser parser(error_list, env, result);
+      parser.set_debug_level(debug);
+      parser.parse();
+      flex_unset_buffer();
+      return result;
+    }
+
     const formula*
     parse_lbt(const std::string& ltl_string,
 	  parse_error_list& error_list,

src/ltlparse/public.hh

@@ -63,7 +63,7 @@ namespace spot
     ///        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
+    /// return a 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.
     ///
@@ -74,6 +74,31 @@ namespace spot
 			 bool debug = false,
 			 bool lenient = false);
 
+    /// \brief Build a Boolean formula from a string.
+    /// \param ltl_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.
+    /// \param lenient When true, parenthesized blocks that cannot be
+    ///                parsed as subformulas will be considered as
+    ///                atomic propositions.
+    /// \return A pointer to the formula built from \a ltl_string, or
+    ///        0 if the input was unparsable.
+    ///
+    /// Note that the parser usually tries to recover from errors.  It can
+    /// return a 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.
+    const formula* parse_boolean(const std::string& ltl_string,
+				 parse_error_list& error_list,
+				 environment& env =
+				 default_environment::instance(),
+				 bool debug = false,
+				 bool lenient = false);
+
     /// \brief Build a formula from an LTL string in LBT's format.
     /// \param ltl_string The string to parse.
     /// \param error_list A list that will be filled with

src/neverparse/neverclaimparse.yy

@@ -201,9 +201,9 @@ transition:
       else
 	{
 	  spot::ltl::parse_error_list pel;
-	  const spot::ltl::formula* f = spot::ltl::parse(*$3, pel,
+	  const spot::ltl::formula* f =
-							 parse_environment,
+	    spot::ltl::parse_boolean(*$3, pel, parse_environment,
-							 false, true);
+				     debug_level(), true);
 	  delete $3;
 	  for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
 	  i != pel.end(); ++i)

src/tgbaparse/tgbaparse.yy

@@ -113,7 +113,8 @@ line: strident ',' strident ',' condition ',' acc_list ';'
 	       {
 		 parse_error_list pel;
 		 const formula* f =
-		   spot::ltl::parse(*$5, pel, parse_environment);
+		   spot::ltl::parse_boolean(*$5, pel, parse_environment,
+					    debug_level());
 		 for (parse_error_list::iterator i = pel.begin();
 		      i != pel.end(); ++i)
 		   {