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

ltlparse: allow comments

* src/ltlparse/ltlscan.ll: Skip comments.
* src/ltltest/ltlfilt.test: Test this.
* NEWS: Mention it.
parent 9cee6e6f
......@@ -63,6 +63,8 @@ New in spot 1.99a (not yet released)
either by Divine (as patched by the LTSmin people) or by
Spins (the LTSmin compiler for Promela).
- LTL formulas can include /* comments */.
- Spot is now compiling in C++11 mode. The set of features we use
requires GCC >= 4.6 or Clang >= 3.1. These minimum versions
are old enough that it should not be an issue to most people.
......
......@@ -40,6 +40,8 @@ static int start_token = 0;
static int parent_level = 0;
static bool missing_parent = false;
static bool lenient_mode = false;
static int orig_cond = 0;
static unsigned comment_level = 0;
typedef ltlyy::parser::token token;
......@@ -50,6 +52,7 @@ typedef ltlyy::parser::token token;
%x in_bra
%x sqbracket
%x lbt
%x in_COMMENT
BOX "[]"|"□"|"⬜"|"◻"
DIAMOND "<>"|"◇"|"⋄"|"♢"
......@@ -61,6 +64,8 @@ CIRCLE "()"|"○"|"◯"
NOT "!"|"~"|"¬"
BOXARROW {BOX}{ARROWL}|"|"{ARROWL}|"↦"
BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
eol \n+|\r+
eol2 (\n\r)+|(\r\n)+
%%
......@@ -74,6 +79,30 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
yylloc->step();
%}
<*>"/""*"+ {
if (YY_START != in_COMMENT)
{
orig_cond = YY_START;
BEGIN(in_COMMENT);
comment_level = 0;
}
++comment_level;
}
<in_COMMENT>{
[^*/\n\r]* continue;
"/"[^*\n\r]* continue;
"*"+[^*/\n\r]* continue;
{eol} yylloc->lines(yyleng); yylloc->end.column = 1;
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond);
<<EOF>> {
BEGIN(orig_cond);
error_list.push_back(
spot::ltl::one_parse_error(*yylloc,
"unclosed comment"));
return 0;
}
}
"(" {
if (!lenient_mode)
......@@ -308,7 +337,6 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
return token::ATOMIC_PROP;
}
<*>. return *yytext;
<<EOF>> return token::END_OF_INPUT;
......
......@@ -34,14 +34,14 @@ checkopt()
# The empty lines in the file are meant, we want to make sure that
# they are ignored.
cat >formulas <<EOF
GFa | FGb
F(GFa | Gb)
GFa | FGb /* comment to ignore */
F(GFa | /* tricky /* comment */)*/ Gb)
F(b W GFa)
GFa | Gb
b W GFa
!{a;b*;c}!
!{a:b*:c}
!{a:b[*/*ignore me*/]:c/*ignore this comment*/}
a U Fb
G(a & Xb)
Xa
......
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