diff --git a/NEWS b/NEWS index 445dc756c..541c12c95 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,7 @@ New in spot 0.9.1a: automata. - The Makefile.am of BuDDy, LBTT, and Spot have been adjusted to accomodate Automake 1.12 (while still working with 1.11). + - Better error recovery when parsing broken LTL formulae. New in spot 0.9.1 (2012-05-23): diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index c68d04eb7..7873497c0 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -58,23 +58,36 @@ #include "parsedecl.hh" using namespace spot::ltl; -#define missing_right_op(res, op, str) \ - do \ - { \ - error_list.push_back(parse_error(op, \ - "missing right operand for \"" str "\"")); \ - res = constant::false_instance(); \ - } \ +#define missing_right_op_msg(op, str) \ + error_list.push_back(parse_error(op, \ + "missing right operand for \"" str "\"")); + +#define missing_right_op(res, op, str) \ + do \ + { \ + missing_right_op_msg(op, str); \ + res = constant::false_instance(); \ + } \ while (0); +// right is missing, so complain and use left. #define missing_right_binop(res, left, op, str) \ do \ { \ - left->destroy(); \ - missing_right_op(res, op, str); \ + missing_right_op_msg(op, str); \ + res = left; \ } \ while (0); +// right is missing, so complain and use false. +#define missing_right_binop_hard(res, left, op, str) \ + do \ + { \ + left->destroy(); \ + missing_right_op(res, op, str); \ + } \ + while (0); + } @@ -362,8 +375,8 @@ sere: booleanatom | sere OP_AND sere { $$ = multop::instance(multop::AndRat, $1, $3); } | sere OP_AND error - { missing_right_binop($$, $1, @2, - "length-matching and operator"); } + { missing_right_binop($$, $1, @2, + "length-matching and operator"); } | sere OP_SHORT_AND sere { $$ = multop::instance(multop::AndNLM, $1, $3); } | sere OP_SHORT_AND error @@ -528,6 +541,10 @@ sere: booleanatom bracedsere: BRACE_OPEN sere BRACE_CLOSE { $$ = $2; } + | BRACE_OPEN sere error BRACE_CLOSE + { error_list.push_back(parse_error(@3, "ignoring this")); + $$ = $2; + } | BRACE_OPEN error BRACE_CLOSE { error_list.push_back(parse_error(@$, "treating this brace block as false")); @@ -538,6 +555,11 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE "missing closing brace")); $$ = $2; } + | BRACE_OPEN sere error END_OF_INPUT + { error_list.push_back(parse_error(@3, + "ignoring trailing garbage and missing closing brace")); + $$ = $2; + } | BRACE_OPEN error END_OF_INPUT { error_list.push_back(parse_error(@$, "missing closing brace, " @@ -547,6 +569,10 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE { $$ = $2; } + | PAR_OPEN subformula 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")); @@ -557,6 +583,11 @@ parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE "missing closing parenthesis")); $$ = $2; } + | PAR_OPEN subformula 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, " @@ -630,12 +661,12 @@ subformula: booleanatom | bracedsere parenthesedsubformula { $$ = binop::instance(binop::UConcat, $1, $2); } | bracedsere OP_UCONCAT error - { missing_right_binop($$, $1, @2, + { missing_right_binop_hard($$, $1, @2, "universal overlapping concat operator"); } | bracedsere OP_ECONCAT subformula { $$ = binop::instance(binop::EConcat, $1, $3); } | bracedsere OP_ECONCAT error - { missing_right_binop($$, $1, @2, + { missing_right_binop_hard($$, $1, @2, "existential overlapping concat operator"); } | bracedsere OP_UCONCAT_NONO subformula @@ -645,7 +676,7 @@ subformula: booleanatom constant::true_instance()), $3); } | bracedsere OP_UCONCAT_NONO error - { missing_right_binop($$, $1, @2, + { missing_right_binop_hard($$, $1, @2, "universal non-overlapping concat operator"); } | bracedsere OP_ECONCAT_NONO subformula @@ -655,7 +686,7 @@ subformula: booleanatom constant::true_instance()), $3); } | bracedsere OP_ECONCAT_NONO error - { missing_right_binop($$, $1, @2, + { missing_right_binop_hard($$, $1, @2, "existential non-overlapping concat operator"); } | BRACE_OPEN sere BRACE_BANG_CLOSE diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test index 185453e7b..cc3edd25b 100755 --- a/src/ltltest/parseerr.test +++ b/src/ltltest/parseerr.test @@ -67,23 +67,24 @@ check '/2/3/4/5 a + b /6/7/8/' '' # leading and trailing garbage are skipped run 0 ../equals -E 'a U b c' 'a U b' -run 0 ../equals -E 'a &&& b' '0 && b' # (check multop merging while we are at it) run 0 ../equals -E 'a & b & c & d e' 'a & b & c & d' run 0 ../equals -E 'a & (b | c) & d should work' 'a & (b | c) & d' # Binop recovery -run 0 ../equals -E 'a U' 0 -run 0 ../equals -E 'a U b V c R' 0 +run 0 ../equals -E 'a U' a +run 0 ../equals -E 'a U b V c R' 'a U b V c' +run 0 ../equals -E 'a &&& b' 'a & b' +run 0 ../equals -E 'a &&| b' 'a | b' # Recovery inside parentheses -run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U (0) U e R (0)' +run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U b U e R f' run 0 ../equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)' # Missing parentheses run 0 ../equals -E 'a & (a + b' 'a & (a + b)' -run 0 ../equals -E 'a & (a + b c' 'a & (0)' -run 0 ../equals -E 'a & (+' 'a & (0)' -run 0 ../equals -E 'a & (' 'a & (0)' +run 0 ../equals -E 'a & (a + b c' 'a & (a + b)' +run 0 ../equals -E 'a & (+' 'a & 0' +run 0 ../equals -E 'a & (' 'a & 0' # Invalid ranges run 0 ../equals -E '{a[*8..1];b}' '{a[*1..8];b}'