Commit 84c9f037 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

neverpase: fix parsing of neverclaim produced by ltl2ba and ltl3ba

These translator may output guards such as (a) || (b), but with the
changes in Spot 1.1.3 it would only work with ((a) || (b)).

Furthermore when ltlcross would fail to parse a neverclaim containing
such a guard, it would fail to parse all later neverclaims, because
the lexer was not properly reset.

* src/neverparse/neverclaimscan.ll: Scan (a) || (b) as a single
token.
(neverclaimyyopen): Reset the lexer.
* src/tgbatest/neverclaimread.test: Add a test for (a) || (b).
* NEWS: Update.
parent 365d0ead
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)
......
......@@ -74,6 +74,10 @@ eol \n|\r|\n\r|\r\n
++parent_level;
yylval->str->append(yytext, yyleng);
}
/* if we match ")&&(" or ")||(", stay in <in_par> 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;
}
......
......@@ -112,6 +112,37 @@ diff stdout expected
rm input stdout expected
# Unparenthesed disjunction
cat >input <<EOF
never { /* p0 || p1 */
accept_init:
if
:: (p1) || (p0) -> goto accept_all
fi;
accept_all:
skip
}
EOF
run 0 ../ltl2tgba -XN input > stdout
cat >expected <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 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 <<EOF
......
Supports Markdown
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