Commit 106a14f8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent a010ebc8
......@@ -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)
{
......
......@@ -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 <ltl> subformula booleanatom sere
%type <ltl> subformula booleanatom sere lbtformula
%type <ltl> bracedsere parenthesedsubformula
%type <minmax> 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,
......
......@@ -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 */
<lbt>p[0-9]+ {
yylval->str = new std::string(yytext, yyleng);
return token::ATOMIC_PROP;
}
/* Atomic propositions can also be enclosed in double quotes. */
<lbt>\"[^\"]*\" {
yylval->str = new std::string(yytext + 1,
yyleng - 2);
return token::ATOMIC_PROP;
}
<*>. return *yytext;
<<EOF>> return token::END_OF_INPUT;
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment