alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Replace reference to RATEXP in the parser, by reference to SERE.

Browse source 
* src/ltlparse/ltlparse.yy: Cleanup the names used in the grammar.
* src/ltlparse/public.hh (parse_ratexp): Rename as...
(parse_sere): ... this.
* src/ltltest/consterm.cc: Adjust call to parse_ratexp().
This commit is contained in:
Alexandre Duret-Lutz 2011-12-05 19:14:03 +01:00
parent 3d183d68c8
commit fa44383efb
3 changed files with 59 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

94
src/ltlparse/ltlparse.yy
View file

@ -80,7 +80,7 @@ using namespace spot::ltl;
/* All tokens. */ /* All tokens. */
%token START_LTL "LTL start marker" %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 PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
%token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace" %token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace"
%token BRACE_BANG_CLOSE "closing brace-bang" %token BRACE_BANG_CLOSE "closing brace-bang"
@ -135,8 +135,8 @@ using namespace spot::ltl;
%nonassoc OP_POST_NEG OP_POST_POS %nonassoc OP_POST_NEG OP_POST_POS
%type <ltl> subformula booleanatom rationalexp %type <ltl> subformula booleanatom sere
%type <ltl> bracedrationalexp parenthesedsubformula %type <ltl> bracedsere parenthesedsubformula
%type <minmax> starargs equalargs sqbracketargs gotoargs %type <minmax> starargs equalargs sqbracketargs gotoargs
%destructor { delete $$; } <str> %destructor { delete $$; } <str>
@ -161,21 +161,21 @@ result: START_LTL subformula END_OF_INPUT
} }
| START_LTL emptyinput | START_LTL emptyinput
{ YYABORT; } { YYABORT; }
| START_RATEXP rationalexp END_OF_INPUT | START_SERE sere END_OF_INPUT
{ result = $2; { result = $2;
YYACCEPT; YYACCEPT;
} }
| START_RATEXP enderror | START_SERE enderror
{ {
result = 0; result = 0;
YYABORT; YYABORT;
} }
| START_RATEXP rationalexp enderror | START_SERE sere enderror
{ {
result = $2; result = $2;
YYACCEPT; YYACCEPT;
} }
| START_RATEXP emptyinput | START_SERE emptyinput
{ YYABORT; } { YYABORT; }
emptyinput: END_OF_INPUT emptyinput: END_OF_INPUT
@ -316,8 +316,8 @@ booleanatom: ATOMIC_PROP
| CONST_FALSE | CONST_FALSE
{ $$ = constant::false_instance(); } { $$ = constant::false_instance(); }
rationalexp: booleanatom sere: booleanatom
| OP_NOT rationalexp | OP_NOT sere
{ {
if ($2->is_boolean()) if ($2->is_boolean())
{ {
@ -334,15 +334,15 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| bracedrationalexp | bracedsere
| PAR_OPEN rationalexp PAR_CLOSE | PAR_OPEN sere PAR_CLOSE
{ $$ = $2; } { $$ = $2; }
| PAR_OPEN error PAR_CLOSE | PAR_OPEN error PAR_CLOSE
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
"treating this parenthetical block as false")); "treating this parenthetical block as false"));
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
| PAR_OPEN rationalexp END_OF_INPUT | PAR_OPEN sere END_OF_INPUT
{ error_list.push_back(parse_error(@1 + @2, { error_list.push_back(parse_error(@1 + @2,
"missing closing parenthesis")); "missing closing parenthesis"));
$$ = $2; $$ = $2;
@ -353,29 +353,29 @@ rationalexp: booleanatom
"treating this parenthetical block as false")); "treating this parenthetical block as false"));
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
| rationalexp OP_AND rationalexp | sere OP_AND sere
{ $$ = multop::instance(multop::And, $1, $3); } { $$ = multop::instance(multop::And, $1, $3); }
| rationalexp OP_AND error | sere OP_AND error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"length-matching and operator"); } "length-matching and operator"); }
| rationalexp OP_SHORT_AND rationalexp | sere OP_SHORT_AND sere
{ $$ = multop::instance(multop::AndNLM, $1, $3); } { $$ = multop::instance(multop::AndNLM, $1, $3); }
| rationalexp OP_SHORT_AND error | sere OP_SHORT_AND error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"non-length-matching and operator"); } "non-length-matching and operator"); }
| rationalexp OP_OR rationalexp | sere OP_OR sere
{ $$ = multop::instance(multop::Or, $1, $3); } { $$ = multop::instance(multop::Or, $1, $3); }
| rationalexp OP_OR error | sere OP_OR error
{ missing_right_binop($$, $1, @2, "or operator"); } { missing_right_binop($$, $1, @2, "or operator"); }
| rationalexp OP_CONCAT rationalexp | sere OP_CONCAT sere
{ $$ = multop::instance(multop::Concat, $1, $3); } { $$ = multop::instance(multop::Concat, $1, $3); }
| rationalexp OP_CONCAT error | sere OP_CONCAT error
{ missing_right_binop($$, $1, @2, "concat operator"); } { missing_right_binop($$, $1, @2, "concat operator"); }
| rationalexp OP_FUSION rationalexp | sere OP_FUSION sere
{ $$ = multop::instance(multop::Fusion, $1, $3); } { $$ = multop::instance(multop::Fusion, $1, $3); }
| rationalexp OP_FUSION error | sere OP_FUSION error
{ missing_right_binop($$, $1, @2, "fusion operator"); } { missing_right_binop($$, $1, @2, "fusion operator"); }
| rationalexp starargs | sere starargs
{ {
if ($2.max < $2.min) if ($2.max < $2.min)
{ {
@ -394,7 +394,7 @@ rationalexp: booleanatom
$$ = bunop::instance(bunop::Star, constant::true_instance(), $$ = bunop::instance(bunop::Star, constant::true_instance(),
$1.min, $1.max); $1.min, $1.max);
} }
| rationalexp equalargs | sere equalargs
{ {
if ($2.max < $2.min) if ($2.max < $2.min)
{ {
@ -416,7 +416,7 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp gotoargs | sere gotoargs
{ {
if ($2.max < $2.min) if ($2.max < $2.min)
{ {
@ -438,7 +438,7 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp OP_XOR rationalexp | sere OP_XOR sere
{ {
if ($1->is_boolean() && $3->is_boolean()) if ($1->is_boolean() && $3->is_boolean())
{ {
@ -465,9 +465,9 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp OP_XOR error | sere OP_XOR error
{ missing_right_binop($$, $1, @2, "xor operator"); } { missing_right_binop($$, $1, @2, "xor operator"); }
| rationalexp OP_IMPLIES rationalexp | sere OP_IMPLIES sere
{ {
if ($1->is_boolean()) if ($1->is_boolean())
{ {
@ -488,9 +488,9 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp OP_IMPLIES error | sere OP_IMPLIES error
{ missing_right_binop($$, $1, @2, "implication operator"); } { missing_right_binop($$, $1, @2, "implication operator"); }
| rationalexp OP_EQUIV rationalexp | sere OP_EQUIV sere
{ {
if ($1->is_boolean() && $3->is_boolean()) if ($1->is_boolean() && $3->is_boolean())
{ {
@ -517,17 +517,17 @@ rationalexp: booleanatom
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp OP_EQUIV error | sere OP_EQUIV error
{ missing_right_binop($$, $1, @2, "equivalent operator"); } { missing_right_binop($$, $1, @2, "equivalent operator"); }
bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE bracedsere: BRACE_OPEN sere BRACE_CLOSE
{ $$ = $2; } { $$ = $2; }
| BRACE_OPEN error BRACE_CLOSE | BRACE_OPEN error BRACE_CLOSE
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
"treating this brace block as false")); "treating this brace block as false"));
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
| BRACE_OPEN rationalexp END_OF_INPUT | BRACE_OPEN sere END_OF_INPUT
{ error_list.push_back(parse_error(@1 + @2, { error_list.push_back(parse_error(@1 + @2,
"missing closing brace")); "missing closing brace"));
$$ = $2; $$ = $2;
@ -617,42 +617,42 @@ subformula: booleanatom
{ $$ = unop::instance(unop::Not, $2); } { $$ = unop::instance(unop::Not, $2); }
| OP_NOT error | OP_NOT error
{ missing_right_op($$, @1, "not operator"); } { missing_right_op($$, @1, "not operator"); }
| bracedrationalexp | bracedsere
{ $$ = unop::instance(unop::Closure, $1); } { $$ = unop::instance(unop::Closure, $1); }
| bracedrationalexp OP_UCONCAT subformula | bracedsere OP_UCONCAT subformula
{ $$ = binop::instance(binop::UConcat, $1, $3); } { $$ = binop::instance(binop::UConcat, $1, $3); }
| bracedrationalexp parenthesedsubformula | bracedsere parenthesedsubformula
{ $$ = binop::instance(binop::UConcat, $1, $2); } { $$ = binop::instance(binop::UConcat, $1, $2); }
| bracedrationalexp OP_UCONCAT error | bracedsere OP_UCONCAT error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"universal overlapping concat operator"); } "universal overlapping concat operator"); }
| bracedrationalexp OP_ECONCAT subformula | bracedsere OP_ECONCAT subformula
{ $$ = binop::instance(binop::EConcat, $1, $3); } { $$ = binop::instance(binop::EConcat, $1, $3); }
| bracedrationalexp OP_ECONCAT error | bracedsere OP_ECONCAT error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"existential overlapping concat operator"); "existential overlapping concat operator");
} }
| bracedrationalexp OP_UCONCAT_NONO subformula | bracedsere OP_UCONCAT_NONO subformula
/* {SERE}[]=>EXP = {SERE;1}[]->EXP */ /* {SERE}[]=>EXP = {SERE;1}[]->EXP */
{ $$ = binop::instance(binop::UConcat, { $$ = binop::instance(binop::UConcat,
multop::instance(multop::Concat, $1, multop::instance(multop::Concat, $1,
constant::true_instance()), $3); constant::true_instance()), $3);
} }
| bracedrationalexp OP_UCONCAT_NONO error | bracedsere OP_UCONCAT_NONO error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"universal non-overlapping concat operator"); "universal non-overlapping concat operator");
} }
| bracedrationalexp OP_ECONCAT_NONO subformula | bracedsere OP_ECONCAT_NONO subformula
/* {SERE}<>=>EXP = {SERE;1}<>->EXP */ /* {SERE}<>=>EXP = {SERE;1}<>->EXP */
{ $$ = binop::instance(binop::EConcat, { $$ = binop::instance(binop::EConcat,
multop::instance(multop::Concat, $1, multop::instance(multop::Concat, $1,
constant::true_instance()), $3); constant::true_instance()), $3);
} }
| bracedrationalexp OP_ECONCAT_NONO error | bracedsere OP_ECONCAT_NONO error
{ missing_right_binop($$, $1, @2, { missing_right_binop($$, $1, @2,
"existential non-overlapping concat operator"); "existential non-overlapping concat operator");
} }
| BRACE_OPEN rationalexp BRACE_BANG_CLOSE | BRACE_OPEN sere BRACE_BANG_CLOSE
/* {SERE}! = {SERE} <>-> 1 */ /* {SERE}! = {SERE} <>-> 1 */
{ $$ = binop::instance(binop::EConcat, $2, { $$ = binop::instance(binop::EConcat, $2,
constant::true_instance()); } constant::true_instance()); }
@ -686,14 +686,14 @@ namespace spot
} }
formula* formula*
parse_ratexp(const std::string& ratexp_string, parse_sere(const std::string& sere_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env, environment& env,
bool debug) bool debug)
{ {
formula* result = 0; formula* result = 0;
flex_set_buffer(ratexp_string.c_str(), flex_set_buffer(sere_string.c_str(),
ltlyy::parser::token::START_RATEXP); ltlyy::parser::token::START_SERE);
ltlyy::parser parser(error_list, env, result); ltlyy::parser parser(error_list, env, result);
parser.set_debug_level(debug); parser.set_debug_level(debug);
parser.parse(); parser.parse();

12
src/ltlparse/public.hh
View file

@ -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). // l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -72,13 +72,13 @@ namespace spot
environment& env = default_environment::instance(), environment& env = default_environment::instance(),
bool debug = false); bool debug = false);
/// \brief Build a formula from a string representing a rational expression. /// \brief Build a formula from a string representing a SERE.
/// \param ratexp_string The string to parse. /// \param sere_string The string to parse.
/// \param error_list A list that will be filled with /// \param error_list A list that will be filled with
/// parse errors that occured during parsing. /// parse errors that occured during parsing.
/// \param env The environment into which parsing should take place. /// \param env The environment into which parsing should take place.
/// \param debug When true, causes the parser to trace its execution. /// \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. /// 0 if the input was unparsable.
/// ///
/// Note that the parser usually tries to recover from errors. It can /// Note that the parser usually tries to recover from errors. It can
@ -87,7 +87,7 @@ namespace spot
/// was parsed succesfully, check \a error_list for emptiness. /// was parsed succesfully, check \a error_list for emptiness.
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
formula* parse_ratexp(const std::string& ratexp_string, formula* parse_sere(const std::string& sere_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env = default_environment::instance(), environment& env = default_environment::instance(),
bool debug = false); bool debug = false);
@ -97,7 +97,7 @@ namespace spot
/// \param os Where diagnostics should be output. /// \param os Where diagnostics should be output.
/// \param input_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 /// \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. /// \return \c true iff any diagnostic was output.
bool format_parse_errors(std::ostream& os, bool format_parse_errors(std::ostream& os,
const std::string& input_string, const std::string& input_string,

6
src/ltltest/consterm.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developement de // Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement
// l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -38,7 +38,7 @@ main(int argc, char **argv)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::parse_error_list p1; 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)) if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2; return 2;