diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 5de0d232e..441232d4c 100644 --- a/src/ltlparse/ltlparse.yy +++ b/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; - if (sere) - f = spot::ltl::parse_sere(str, suberror, env, debug, true); - else - f = spot::ltl::parse(str, suberror, env, debug, true); + const spot::ltl::formula* f = 0; + switch (type) + { + case parser_sere: + 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 PAR_BLOCK "(...) block" %token BRA_BLOCK "{...} block" @@ -214,7 +225,7 @@ using namespace spot::ltl; %nonassoc OP_POST_NEG OP_POST_POS -%type subformula booleanatom sere lbtformula +%type subformula booleanatom sere lbtformula boolformula %type bracedsere parenthesedsubformula %type 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, diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 9e1cebaaa..e4f6019e7 100644 --- a/src/ltlparse/public.hh +++ b/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 diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 646362dec..73d4337c0 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/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, - parse_environment, - false, true); + const spot::ltl::formula* f = + spot::ltl::parse_boolean(*$3, pel, parse_environment, + debug_level(), true); delete $3; for(spot::ltl::parse_error_list::const_iterator i = pel.begin(); i != pel.end(); ++i) diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 13da43fcd..8978b5397 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/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) {