parsetl: improve coverage
* spot/parsetl/parsetl.yy: Adjust one diagnostic. * spot/parsetl/scantl.ll: Fix recovering of missing closing brace in lenient mode. * tests/python/ltlparse.py: Add tests. * NEWS: Mention the lenient mode bug.
This commit is contained in:
parent
6b339a3712
commit
bf31ff12ad
4 changed files with 145 additions and 9 deletions
5
NEWS
5
NEWS
|
|
@ -1,6 +1,9 @@
|
||||||
New in spot 2.3.2.dev (not yet released)
|
New in spot 2.3.2.dev (not yet released)
|
||||||
|
|
||||||
Nothing yet.
|
Bug fixes:
|
||||||
|
|
||||||
|
- In "lenient" mode the parser would fail to recover from
|
||||||
|
a missing closing brace.
|
||||||
|
|
||||||
New in spot 2.3.2 (2017-03-15)
|
New in spot 2.3.2 (2017-03-15)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -393,7 +393,7 @@ fstarargs: OP_BFSTAR
|
||||||
equalargs: OP_EQUAL_OPEN sqbracketargs
|
equalargs: OP_EQUAL_OPEN sqbracketargs
|
||||||
{ $$ = $2; }
|
{ $$ = $2; }
|
||||||
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
|
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
|
||||||
{ error_list.emplace_back(@$, "treating this equal block as [*]");
|
{ error_list.emplace_back(@$, "treating this equal block as [=]");
|
||||||
$$.min = 0U; $$.max = fnode::unbounded(); }
|
$$.min = 0U; $$.max = fnode::unbounded(); }
|
||||||
| OP_EQUAL_OPEN error_opt END_OF_INPUT
|
| OP_EQUAL_OPEN error_opt END_OF_INPUT
|
||||||
{ error_list.
|
{ error_list.
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
/* -*- coding: utf-8 -*-
|
/* -*- coding: utf-8 -*-
|
||||||
** Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, Laboratoire de
|
** Copyright (C) 2010-2015, 2017, Laboratoire de Recherche et
|
||||||
** Recherche et Développement de l'Epita (LRDE).
|
** Développement de l'Epita (LRDE).
|
||||||
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
** et Marie Curie.
|
** et Marie Curie.
|
||||||
|
|
@ -142,7 +142,7 @@ eol2 (\n\r)+|(\r\n)+
|
||||||
if (!missing_parent)
|
if (!missing_parent)
|
||||||
error_list.push_back(
|
error_list.push_back(
|
||||||
spot::one_parse_error(*yylloc,
|
spot::one_parse_error(*yylloc,
|
||||||
"missing closing parenthese"));
|
"missing closing parenthesis"));
|
||||||
missing_parent = true;
|
missing_parent = true;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -192,7 +192,7 @@ eol2 (\n\r)+|(\r\n)+
|
||||||
}
|
}
|
||||||
[^{}]+ yylval->str->append(yytext, yyleng);
|
[^{}]+ yylval->str->append(yytext, yyleng);
|
||||||
<<EOF>> {
|
<<EOF>> {
|
||||||
unput(')');
|
unput('}');
|
||||||
if (!missing_parent)
|
if (!missing_parent)
|
||||||
error_list.push_back(
|
error_list.push_back(
|
||||||
spot::one_parse_error(*yylloc,
|
spot::one_parse_error(*yylloc,
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- mode: python; coding: utf-8 -*-
|
||||||
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
|
# Copyright (C) 2009-2012, 2014-2017 Laboratoire de Recherche et
|
||||||
# Développement de l'Epita (LRDE).
|
# Développement de l'Epita (LRDE).
|
||||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
|
|
@ -33,12 +33,145 @@ for str1 in l:
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
str2 = str(pf.f)
|
str2 = str(pf.f)
|
||||||
del pf
|
del pf
|
||||||
sys.stdout.write(str2 + "\n")
|
|
||||||
# Try to reparse the stringified formula
|
# Try to reparse the stringified formula
|
||||||
pf = spot.parse_infix_psl(str2, e)
|
pf = spot.parse_infix_psl(str2, e)
|
||||||
if pf.format_errors(spot.get_cout()):
|
if pf.format_errors(spot.get_cout()):
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
sys.stdout.write(str(pf.f) + "\n")
|
|
||||||
del pf
|
del pf
|
||||||
|
|
||||||
|
for str1 in ['a * b', 'a xor b', 'a <-> b']:
|
||||||
|
pf = spot.parse_infix_boolean(str1, e, False)
|
||||||
|
if pf.format_errors(spot.get_cout()):
|
||||||
|
sys.exit(1)
|
||||||
|
str2 = str(pf.f)
|
||||||
|
del pf
|
||||||
|
# Try to reparse the stringified formula
|
||||||
|
pf = spot.parse_infix_boolean(str2, e)
|
||||||
|
if pf.format_errors(spot.get_cout()):
|
||||||
|
sys.exit(1)
|
||||||
|
del pf
|
||||||
|
|
||||||
|
f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]')
|
||||||
|
assert not f6.errors
|
||||||
|
del f6
|
||||||
|
|
||||||
|
f6 = spot.parse_infix_sere('-')
|
||||||
|
assert f6.errors
|
||||||
|
del f6
|
||||||
|
|
||||||
|
for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
|
||||||
|
('{foo[->', 'missing closing bracket for goto operator'),
|
||||||
|
('{foo[->3..1]}', "reversed range"),
|
||||||
|
('{foo[*bug]}', "treating this star block as [*]"),
|
||||||
|
('{foo[*bug', "missing closing bracket for star"),
|
||||||
|
('{foo[*3..1]}', "reversed range"),
|
||||||
|
('{[*3..1]}', "reversed range"),
|
||||||
|
('{foo[:*bug]}', "treating this fusion-star block as [:*]"),
|
||||||
|
('{foo[:*3..1]}', "reversed range"),
|
||||||
|
('{foo[:*bug', "missing closing bracket for fusion-star"),
|
||||||
|
('{foo[=bug]}', "treating this equal block as [=]"),
|
||||||
|
('{foo[=bug', "missing closing bracket for equal operator"),
|
||||||
|
('{foo[=3..1]}', "reversed range"),
|
||||||
|
('{()}', "treating this brace block as false"),
|
||||||
|
('{(a b)}', "treating this parenthetical block as false"),
|
||||||
|
('{(a*}', "missing closing parenthesis"),
|
||||||
|
('{(a*&)}', "missing right operand for "
|
||||||
|
+ "\"non-length-matching and operator\""),
|
||||||
|
('{(a*&&)}', "missing right operand for "
|
||||||
|
+ "\"length-matching and operator\""),
|
||||||
|
('{(a*|)}', "missing right operand for \"or operator\""),
|
||||||
|
('{a*;}', "missing right operand for \"concat operator\""),
|
||||||
|
('{a*::b}', "missing right operand for \"fusion operator\""),
|
||||||
|
('{a* xor }', "missing right operand for \"xor operator\""),
|
||||||
|
('{a* -> }', "missing right operand for "
|
||||||
|
+ "\"implication operator\""),
|
||||||
|
('{a <-> <-> b }',
|
||||||
|
"missing right operand for \"equivalent operator\""),
|
||||||
|
('{a;b b}', "ignoring this"),
|
||||||
|
('{*', "missing closing brace"),
|
||||||
|
('{(a', "missing closing parenthesis"),
|
||||||
|
('{* a', "ignoring trailing garbage and missing closing brace"),
|
||||||
|
('F(a b)', "ignoring this"),
|
||||||
|
('F(-)', "treating this parenthetical block as false"),
|
||||||
|
('F(', "missing closing parenthesis"),
|
||||||
|
('F(a b', "ignoring trailing garbage and "
|
||||||
|
+ "missing closing parenthesis"),
|
||||||
|
('F(-', "missing closing parenthesis"),
|
||||||
|
('F(-', "parenthetical block as false"),
|
||||||
|
('a&', "missing right operand for \"and operator\""),
|
||||||
|
('a*', "missing right operand for \"and operator\""),
|
||||||
|
('a|', "missing right operand for \"or operator\""),
|
||||||
|
('a^', "missing right operand for \"xor operator\""),
|
||||||
|
('a->', "missing right operand for \"implication operator\""),
|
||||||
|
('a<->', "missing right operand for \"equivalent operator\""),
|
||||||
|
('!', "missing right operand for \"not operator\""),
|
||||||
|
('a W', "missing right operand for \"weak until operator\""),
|
||||||
|
('a U', "missing right operand for \"until operator\""),
|
||||||
|
('a R', "missing right operand for \"release operator\""),
|
||||||
|
('a M', "missing right operand for "
|
||||||
|
+ "\"strong release operator\""),
|
||||||
|
('{a}[]->', "missing right operand for "
|
||||||
|
+ "\"universal overlapping concat operator\""),
|
||||||
|
('{a}[]=>', "missing right operand for "
|
||||||
|
+ "\"universal non-overlapping concat operator\""),
|
||||||
|
('{a}<>->', "missing right operand for "
|
||||||
|
+ "\"existential overlapping concat operator\""),
|
||||||
|
('{a}<>=>', "missing right operand for "
|
||||||
|
+ "\"existential non-overlapping concat operator\""),
|
||||||
|
('(X)', "missing right operand for \"next operator\""),
|
||||||
|
('("X)', "unclosed string"),
|
||||||
|
('("X)', "missing closing parenthesis"),
|
||||||
|
('{"X', "unclosed string"),
|
||||||
|
('{"X}', "missing closing brace"),
|
||||||
|
]:
|
||||||
|
f7 = spot.parse_infix_psl(x)
|
||||||
|
assert f7.errors
|
||||||
|
ostr = spot.ostringstream()
|
||||||
|
f7.format_errors(ostr)
|
||||||
|
err = ostr.str()
|
||||||
|
print(err)
|
||||||
|
assert msg in err
|
||||||
|
del f7
|
||||||
|
|
||||||
|
for (x, msg) in [('a&', "missing right operand for \"and operator\""),
|
||||||
|
('a*', "missing right operand for \"and operator\""),
|
||||||
|
('a|', "missing right operand for \"or operator\""),
|
||||||
|
('a^', "missing right operand for \"xor operator\""),
|
||||||
|
('a->', "missing right operand for \"implication operator\""),
|
||||||
|
('a<->', "missing right operand for \"equivalent operator\""),
|
||||||
|
('(-', "parenthetical block as false"),
|
||||||
|
('(-', "missing closing parenthesis"),
|
||||||
|
('(-)', "treating this parenthetical block as false"),
|
||||||
|
('(a', "missing closing parenthesis"),
|
||||||
|
('(a b)', "ignoring this"),
|
||||||
|
('(a b', "ignoring trailing garbage and "
|
||||||
|
+ "missing closing parenthesis"),
|
||||||
|
('!', "missing right operand for \"not operator\""),
|
||||||
|
]:
|
||||||
|
f8 = spot.parse_infix_boolean(x)
|
||||||
|
assert f8.errors
|
||||||
|
ostr = spot.ostringstream()
|
||||||
|
f8.format_errors(ostr)
|
||||||
|
err = ostr.str()
|
||||||
|
print(err)
|
||||||
|
assert msg in err
|
||||||
|
del f8
|
||||||
|
|
||||||
|
for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
|
||||||
|
('a<->', "missing right operand for \"equivalent operator\""),
|
||||||
|
('(aa', "missing closing parenthesis"),
|
||||||
|
('("aa', "missing closing parenthesis"),
|
||||||
|
('"(aa', "unclosed string"),
|
||||||
|
('{aa', "missing closing brace"),
|
||||||
|
]:
|
||||||
|
f9 = spot.parse_infix_psl(x, spot.default_environment.instance(),
|
||||||
|
False, True)
|
||||||
|
assert f9.errors
|
||||||
|
ostr = spot.ostringstream()
|
||||||
|
f9.format_errors(ostr)
|
||||||
|
err = ostr.str()
|
||||||
|
print(err)
|
||||||
|
assert msg in err
|
||||||
|
del f9
|
||||||
|
|
||||||
assert spot.fnode_instances_check()
|
assert spot.fnode_instances_check()
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue