diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index b02b63668..9119cfa3e 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -80,7 +80,7 @@ using namespace spot::ltl; /* All tokens. */ %token START_LTL "LTL start marker" -%token START_RATEXP "RATEXP start marker" +%token START_SERE "SERE start marker" %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis" %token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace" %token BRACE_BANG_CLOSE "closing brace-bang" @@ -135,8 +135,8 @@ using namespace spot::ltl; %nonassoc OP_POST_NEG OP_POST_POS -%type subformula booleanatom rationalexp -%type bracedrationalexp parenthesedsubformula +%type subformula booleanatom sere +%type bracedsere parenthesedsubformula %type starargs equalargs sqbracketargs gotoargs %destructor { delete $$; } @@ -161,21 +161,21 @@ result: START_LTL subformula END_OF_INPUT } | START_LTL emptyinput { YYABORT; } - | START_RATEXP rationalexp END_OF_INPUT + | START_SERE sere END_OF_INPUT { result = $2; YYACCEPT; } - | START_RATEXP enderror + | START_SERE enderror { result = 0; YYABORT; } - | START_RATEXP rationalexp enderror + | START_SERE sere enderror { result = $2; YYACCEPT; } - | START_RATEXP emptyinput + | START_SERE emptyinput { YYABORT; } emptyinput: END_OF_INPUT @@ -316,8 +316,8 @@ booleanatom: ATOMIC_PROP | CONST_FALSE { $$ = constant::false_instance(); } -rationalexp: booleanatom - | OP_NOT rationalexp +sere: booleanatom + | OP_NOT sere { if ($2->is_boolean()) { @@ -334,15 +334,15 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | bracedrationalexp - | PAR_OPEN rationalexp PAR_CLOSE + | bracedsere + | PAR_OPEN sere PAR_CLOSE { $$ = $2; } | PAR_OPEN error PAR_CLOSE { error_list.push_back(parse_error(@$, "treating this parenthetical block as false")); $$ = constant::false_instance(); } - | PAR_OPEN rationalexp END_OF_INPUT + | PAR_OPEN sere END_OF_INPUT { error_list.push_back(parse_error(@1 + @2, "missing closing parenthesis")); $$ = $2; @@ -353,29 +353,29 @@ rationalexp: booleanatom "treating this parenthetical block as false")); $$ = constant::false_instance(); } - | rationalexp OP_AND rationalexp + | sere OP_AND sere { $$ = multop::instance(multop::And, $1, $3); } - | rationalexp OP_AND error + | sere OP_AND error { missing_right_binop($$, $1, @2, "length-matching and operator"); } - | rationalexp OP_SHORT_AND rationalexp + | sere OP_SHORT_AND sere { $$ = multop::instance(multop::AndNLM, $1, $3); } - | rationalexp OP_SHORT_AND error + | sere OP_SHORT_AND error { missing_right_binop($$, $1, @2, "non-length-matching and operator"); } - | rationalexp OP_OR rationalexp + | sere OP_OR sere { $$ = multop::instance(multop::Or, $1, $3); } - | rationalexp OP_OR error + | sere OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } - | rationalexp OP_CONCAT rationalexp + | sere OP_CONCAT sere { $$ = multop::instance(multop::Concat, $1, $3); } - | rationalexp OP_CONCAT error + | sere OP_CONCAT error { missing_right_binop($$, $1, @2, "concat operator"); } - | rationalexp OP_FUSION rationalexp + | sere OP_FUSION sere { $$ = multop::instance(multop::Fusion, $1, $3); } - | rationalexp OP_FUSION error + | sere OP_FUSION error { missing_right_binop($$, $1, @2, "fusion operator"); } - | rationalexp starargs + | sere starargs { if ($2.max < $2.min) { @@ -394,7 +394,7 @@ rationalexp: booleanatom $$ = bunop::instance(bunop::Star, constant::true_instance(), $1.min, $1.max); } - | rationalexp equalargs + | sere equalargs { if ($2.max < $2.min) { @@ -416,7 +416,7 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | rationalexp gotoargs + | sere gotoargs { if ($2.max < $2.min) { @@ -438,7 +438,7 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | rationalexp OP_XOR rationalexp + | sere OP_XOR sere { if ($1->is_boolean() && $3->is_boolean()) { @@ -465,9 +465,9 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | rationalexp OP_XOR error + | sere OP_XOR error { missing_right_binop($$, $1, @2, "xor operator"); } - | rationalexp OP_IMPLIES rationalexp + | sere OP_IMPLIES sere { if ($1->is_boolean()) { @@ -488,9 +488,9 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | rationalexp OP_IMPLIES error + | sere OP_IMPLIES error { missing_right_binop($$, $1, @2, "implication operator"); } - | rationalexp OP_EQUIV rationalexp + | sere OP_EQUIV sere { if ($1->is_boolean() && $3->is_boolean()) { @@ -517,17 +517,17 @@ rationalexp: booleanatom $$ = constant::false_instance(); } } - | rationalexp OP_EQUIV error + | sere OP_EQUIV error { missing_right_binop($$, $1, @2, "equivalent operator"); } -bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE +bracedsere: BRACE_OPEN sere BRACE_CLOSE { $$ = $2; } | BRACE_OPEN error BRACE_CLOSE { error_list.push_back(parse_error(@$, "treating this brace block as false")); $$ = constant::false_instance(); } - | BRACE_OPEN rationalexp END_OF_INPUT + | BRACE_OPEN sere END_OF_INPUT { error_list.push_back(parse_error(@1 + @2, "missing closing brace")); $$ = $2; @@ -617,42 +617,42 @@ subformula: booleanatom { $$ = unop::instance(unop::Not, $2); } | OP_NOT error { missing_right_op($$, @1, "not operator"); } - | bracedrationalexp + | bracedsere { $$ = unop::instance(unop::Closure, $1); } - | bracedrationalexp OP_UCONCAT subformula + | bracedsere OP_UCONCAT subformula { $$ = binop::instance(binop::UConcat, $1, $3); } - | bracedrationalexp parenthesedsubformula + | bracedsere parenthesedsubformula { $$ = binop::instance(binop::UConcat, $1, $2); } - | bracedrationalexp OP_UCONCAT error + | bracedsere OP_UCONCAT error { missing_right_binop($$, $1, @2, "universal overlapping concat operator"); } - | bracedrationalexp OP_ECONCAT subformula + | bracedsere OP_ECONCAT subformula { $$ = binop::instance(binop::EConcat, $1, $3); } - | bracedrationalexp OP_ECONCAT error + | bracedsere OP_ECONCAT error { missing_right_binop($$, $1, @2, "existential overlapping concat operator"); } - | bracedrationalexp OP_UCONCAT_NONO subformula + | bracedsere OP_UCONCAT_NONO subformula /* {SERE}[]=>EXP = {SERE;1}[]->EXP */ { $$ = binop::instance(binop::UConcat, multop::instance(multop::Concat, $1, constant::true_instance()), $3); } - | bracedrationalexp OP_UCONCAT_NONO error + | bracedsere OP_UCONCAT_NONO error { missing_right_binop($$, $1, @2, "universal non-overlapping concat operator"); } - | bracedrationalexp OP_ECONCAT_NONO subformula + | bracedsere OP_ECONCAT_NONO subformula /* {SERE}<>=>EXP = {SERE;1}<>->EXP */ { $$ = binop::instance(binop::EConcat, multop::instance(multop::Concat, $1, constant::true_instance()), $3); } - | bracedrationalexp OP_ECONCAT_NONO error + | bracedsere OP_ECONCAT_NONO error { missing_right_binop($$, $1, @2, "existential non-overlapping concat operator"); } - | BRACE_OPEN rationalexp BRACE_BANG_CLOSE + | BRACE_OPEN sere BRACE_BANG_CLOSE /* {SERE}! = {SERE} <>-> 1 */ { $$ = binop::instance(binop::EConcat, $2, constant::true_instance()); } @@ -686,14 +686,14 @@ namespace spot } formula* - parse_ratexp(const std::string& ratexp_string, + parse_sere(const std::string& sere_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); + flex_set_buffer(sere_string.c_str(), + ltlyy::parser::token::START_SERE); ltlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index e09f47113..89085b1c6 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -72,13 +72,13 @@ namespace spot environment& env = default_environment::instance(), bool debug = false); - /// \brief Build a formula from a string representing a rational expression. - /// \param ratexp_string The string to parse. + /// \brief Build a formula from a string representing a SERE. + /// \param sere_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 + /// \return A pointer to the formula built from \a sere_string, or /// 0 if the input was unparsable. /// /// Note that the parser usually tries to recover from errors. It can @@ -87,17 +87,17 @@ namespace spot /// 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); + formula* parse_sere(const std::string& sere_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 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. + /// or spot::ltl::parse_sere while parsing \a input_string. /// \return \c true iff any diagnostic was output. bool format_parse_errors(std::ostream& os, const std::string& input_string, diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc index ae8f3e3f5..896b6e67d 100644 --- a/src/ltltest/consterm.cc +++ b/src/ltltest/consterm.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developement de -// l'Epita (LRDE). +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -38,7 +38,7 @@ main(int argc, char **argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse_ratexp(argv[1], p1); + spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2;