diff --git a/NEWS b/NEWS index b6e826959..feddc4544 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,11 @@ New in spot 1.1.3a (not released) - * Nothing yet. + * Bug fixes: + - The parser for neverclaim, updated in 1.1.3, would fail to + parse guards of the form (a) || (b) output by ltl2ba or + ltl3ba, and would only understand ((a) || (b)). + - When used from ltlcross, the same parser would fail to + parser further neverclaims after the first failure. New in spot 1.1.3 (2013-07-09) diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 77656137d..79609034e 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -74,6 +74,10 @@ eol \n|\r|\n\r|\r\n ++parent_level; yylval->str->append(yytext, yyleng); } + /* if we match ")&&(" or ")||(", stay in mode */ + ")"[ \t]*("&&"|"||")[ \t]*"(" { + yylval->str->append(yytext, yyleng); + } ")" { yylval->str->append(yytext, yyleng); if (!--parent_level) @@ -128,6 +132,10 @@ namespace spot if (!yyin) return 1; } + // Reset the lexer in case a previous parse + // ended badly. + BEGIN(0); + YY_NEW_FILE; return 0; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 5407fce59..3d3b033d6 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -112,6 +112,37 @@ diff stdout expected rm input stdout expected +# Unparenthesed disjunction +cat >input < goto accept_all + fi; +accept_all: + skip +} +EOF +run 0 ../ltl2tgba -XN input > stdout + +cat >expected < 1 + 1 [label="accept_init", peripheries=2] + 1 -> 2 [label="p1 | p0\n{Acc[1]}"] + 2 [label="accept_all", peripheries=2] + 2 -> 2 [label="1\n{Acc[1]}"] +} +EOF + +# Sort out some possible inversions in the output. +# (The order is not guaranteed by SPOT.) +sed -e 's/p0 | p1/p1 | p0/g' stdout > tmp_ && mv tmp_ stdout +diff stdout expected + +rm input stdout expected + # Test broken guards in input cat >input <