From 106a14f8dbcff3823eeb882267fe018e2c6e7387 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Sep 2012 17:43:13 +0200 Subject: [PATCH] Implement a parser for LBT's prefix syntax for LTL. * src/ltlparse/public.hh (parse_lbt): New function. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Implement it. * src/bin/ltlfilt.cc: Use it. --- src/bin/ltlfilt.cc | 11 +++++- src/ltlparse/ltlparse.yy | 85 +++++++++++++++++++++++++++++++++++++++- src/ltlparse/ltlscan.ll | 16 ++++++++ src/ltlparse/public.hh | 24 ++++++++++++ 4 files changed, 134 insertions(+), 2 deletions(-) diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index ac8ec8387..902a3b6ca 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -86,6 +86,7 @@ Exit status:\n\ #define OPT_IMPLIED_BY 23 #define OPT_IMPLY 24 #define OPT_EQUIVALENT_TO 25 +#define OPT_LBT 26 static const argp_option options[] = { @@ -94,6 +95,7 @@ static const argp_option options[] = { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, { "file", 'F', "FILENAME", 0, "process each line of FILENAME as a formula", 0 }, + { "lbt-input", OPT_LBT, 0, 0, "read all formulas using LBT's prefix syntax", 0 }, { 0, 0, 0, 0, "Error handling:", 2 }, { "skip-errors", OPT_SKIP_ERRORS, 0, 0, "output erroneous lines as-is without processing", 0 }, @@ -178,6 +180,7 @@ static bool one_match = false; enum error_style_t { drop_errors, skip_errors }; static error_style_t error_style = drop_errors; +static bool lbt = false; static bool quiet = false; static bool nnf = false; static bool negate = false; @@ -275,6 +278,8 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_GUARANTEE: guarantee = obligation = true; break; + case OPT_LBT: + lbt = true; case OPT_LTL: ltl = true; break; @@ -367,7 +372,11 @@ namespace const char* filename = 0, int linenum = 0) { spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = spot::ltl::parse(input, pel); + const spot::ltl::formula* f; + if (lbt) + f = spot::ltl::parse_lbt(input, pel); + else + f = spot::ltl::parse(input, pel); if (!f || pel.size() > 0) { diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 751b1a96e..a5136552f 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -94,6 +94,7 @@ using namespace spot::ltl; /* All tokens. */ %token START_LTL "LTL start marker" +%token START_LBT "LBT 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" @@ -157,7 +158,7 @@ using namespace spot::ltl; %nonassoc OP_POST_NEG OP_POST_POS -%type subformula booleanatom sere +%type subformula booleanatom sere lbtformula %type bracedsere parenthesedsubformula %type starargs equalargs sqbracketargs gotoargs @@ -203,6 +204,22 @@ result: START_LTL subformula END_OF_INPUT } | START_SERE emptyinput { YYABORT; } + | START_LBT lbtformula END_OF_INPUT + { result = $2; + YYACCEPT; + } + | START_LBT enderror + { + result = 0; + YYABORT; + } + | START_LBT lbtformula enderror + { + result = $2; + YYACCEPT; + } + | START_LBT emptyinput + { YYABORT; } emptyinput: END_OF_INPUT { @@ -708,6 +725,57 @@ subformula: booleanatom constant::true_instance()); } ; +lbtformula: ATOMIC_PROP + { + $$ = parse_environment.require(*$1); + if (! $$) + { + std::string s = "unknown atomic proposition `"; + s += *$1; + s += "' in environment `"; + s += parse_environment.name(); + s += "'"; + error_list.push_back(parse_error(@1, s)); + delete $1; + YYERROR; + } + else + delete $1; + } + | '!' lbtformula + { $$ = unop::instance(unop::Not, $2); } + | '&' lbtformula lbtformula + { $$ = multop::instance(multop::And, $2, $3); } + | '|' lbtformula lbtformula + { $$ = multop::instance(multop::Or, $2, $3); } + | '^' lbtformula lbtformula + { $$ = binop::instance(binop::Xor, $2, $3); } + | 'i' lbtformula lbtformula + { $$ = binop::instance(binop::Implies, $2, $3); } + | 'e' lbtformula lbtformula + { $$ = binop::instance(binop::Equiv, $2, $3); } + | 'X' lbtformula + { $$ = unop::instance(unop::X, $2); } + | 'F' lbtformula + { $$ = unop::instance(unop::F, $2); } + | 'G' lbtformula + { $$ = unop::instance(unop::G, $2); } + | 'U' lbtformula lbtformula + { $$ = binop::instance(binop::U, $2, $3); } + | 'V' lbtformula lbtformula + { $$ = binop::instance(binop::R, $2, $3); } + | 'R' lbtformula lbtformula + { $$ = binop::instance(binop::R, $2, $3); } + | 'W' lbtformula lbtformula + { $$ = binop::instance(binop::W, $2, $3); } + | 'M' lbtformula lbtformula + { $$ = binop::instance(binop::M, $2, $3); } + | 't' + { $$ = constant::true_instance(); } + | 'f' + { $$ = constant::false_instance(); } + ; + %% void @@ -735,6 +803,21 @@ namespace spot return result; } + const formula* + parse_lbt(const std::string& ltl_string, + parse_error_list& error_list, + environment& env, + bool debug) + { + const formula* result = 0; + flex_set_buffer(ltl_string.c_str(), + ltlyy::parser::token::START_LBT); + ltlyy::parser parser(error_list, env, result); + parser.set_debug_level(debug); + parser.parse(); + return result; + } + const formula* parse_sere(const std::string& sere_string, parse_error_list& error_list, diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index da47f7212..84f1b211c 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -60,6 +60,7 @@ flex_set_buffer(const char* buf, int start_tok) %s not_prop %x sqbracket +%x lbt BOX "[]"|"□"|"⬜"|"◻" DIAMOND "<>"|"◇"|"⋄"|"♢" @@ -79,6 +80,8 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" { int t = start_token; start_token = 0; + if (t == token::START_LBT) + BEGIN(lbt); return t; } yylloc->step(); @@ -205,6 +208,19 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" return token::ATOMIC_PROP; } + /* in LBT's format, atomic proposition look like p0 or p3141592 */ +p[0-9]+ { + yylval->str = new std::string(yytext, yyleng); + return token::ATOMIC_PROP; + } + /* Atomic propositions can also be enclosed in double quotes. */ +\"[^\"]*\" { + yylval->str = new std::string(yytext + 1, + yyleng - 2); + return token::ATOMIC_PROP; + } + + <*>. return *yytext; <> return token::END_OF_INPUT; diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index d6f315e9d..bf75480e8 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -72,6 +72,30 @@ namespace spot environment& env = default_environment::instance(), bool debug = 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 + /// 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 ltl_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. + /// + /// The LBT syntax, also used by the lbtt and scheck tools, is + /// extended to support W, and M operators (as done in lbtt), and + /// double-quoted atomic propositions that do not start with 'p'. + /// + /// \warning This function is not reentrant. + const formula* parse_lbt(const std::string& ltl_string, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); + /// \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