hoa: improve parser and scanner
* src/hoaparse/hoaparse.yy: Improve error reporting in case labeled edges are mixed with unlabeled edges. * src/hoaparse/hoascan.ll: Fix handling of nested comments. * src/tgbatest/hoaparse.test: More coverage.
This commit is contained in:
Alexandre Duret-Lutz
parent
0a21db5c30
commit
e7e21ae58f
3 changed files with 147 additions and 16 deletions
|
|
@ -549,7 +549,7 @@ trans-label: label
|
|||
{
|
||||
if (res.has_state_label)
|
||||
{
|
||||
error(@1, "cannot label this transition because...");
|
||||
error(@1, "cannot label this edge because...");
|
||||
error(res.state_label_loc,
|
||||
"... the state is already labeled.");
|
||||
res.cur_label = res.state_label;
|
||||
|
|
@ -586,11 +586,30 @@ acc-sets:
|
|||
else
|
||||
$$ = $1 | res.h->aut->acc().mark($2);
|
||||
}
|
||||
labeled-edges: | labeled-edges labeled-edge
|
||||
|
||||
/* block of labeled-edges, with occasional (incorrect) unlabeled edge */
|
||||
labeled-edges: | some-labeled-edges
|
||||
some-labeled-edges: labeled-edge
|
||||
| some-labeled-edges labeled-edge
|
||||
| some-labeled-edges incorrectly-unlabeled-edge
|
||||
incorrectly-unlabeled-edge: checked-state-num acc-sig_opt
|
||||
{
|
||||
bdd cond = bddtrue;
|
||||
if (!res.has_state_label)
|
||||
error(@$, "missing label for this edge "
|
||||
"(previous edge is labeled)");
|
||||
else
|
||||
cond = res.state_label;
|
||||
res.h->aut->new_transition(res.cur_state, $1,
|
||||
cond,
|
||||
$2 | res.acc_state);
|
||||
}
|
||||
labeled-edge: trans-label checked-state-num acc-sig_opt
|
||||
{
|
||||
res.h->aut->new_transition(res.cur_state, $2,
|
||||
res.cur_label, $3 | res.acc_state);
|
||||
if (res.cur_label != bddfalse)
|
||||
res.h->aut->new_transition(res.cur_state, $2,
|
||||
res.cur_label,
|
||||
$3 | res.acc_state);
|
||||
}
|
||||
| trans-label state-conj-2 acc-sig_opt
|
||||
{
|
||||
|
|
@ -598,9 +617,12 @@ labeled-edge: trans-label checked-state-num acc-sig_opt
|
|||
YYABORT;
|
||||
}
|
||||
|
||||
/* We never have zero unlabeled edges, these are considered as zero
|
||||
labeled edges. */
|
||||
unlabeled-edges: unlabeled-edge | unlabeled-edges unlabeled-edge
|
||||
/* Block of unlabeled edge, with occasional (incorrect) labeled
|
||||
edge. We never have zero unlabeled edges, these are considered as
|
||||
zero labeled edges. */
|
||||
unlabeled-edges: unlabeled-edge
|
||||
| unlabeled-edges unlabeled-edge
|
||||
| unlabeled-edges incorrectly-labeled-edge
|
||||
unlabeled-edge: checked-state-num acc-sig_opt
|
||||
{
|
||||
bdd cond;
|
||||
|
|
@ -623,14 +645,20 @@ unlabeled-edge: checked-state-num acc-sig_opt
|
|||
cond = *res.cur_guard++;
|
||||
}
|
||||
}
|
||||
res.h->aut->new_transition(res.cur_state, $1,
|
||||
cond, $2 | res.acc_state);
|
||||
if (cond != bddfalse)
|
||||
res.h->aut->new_transition(res.cur_state, $1,
|
||||
cond, $2 | res.acc_state);
|
||||
}
|
||||
| state-conj-2 acc-sig_opt
|
||||
{
|
||||
error(@1, "alternation is not yet supported");
|
||||
YYABORT;
|
||||
}
|
||||
incorrectly-labeled-edge: trans-label unlabeled-edge
|
||||
{
|
||||
error(@1, "ignoring this label, because previous"
|
||||
" edge has no label");
|
||||
}
|
||||
|
||||
%%
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,8 @@
|
|||
#define YY_NEVER_INTERACTIVE 1
|
||||
|
||||
typedef hoayy::parser::token token;
|
||||
static unsigned comment_level = 0;
|
||||
|
||||
%}
|
||||
|
||||
eol \n+|\r+
|
||||
|
|
@ -50,8 +52,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
|
|||
{eol} yylloc->lines(yyleng); yylloc->step();
|
||||
{eol2} yylloc->lines(yyleng / 2); yylloc->step();
|
||||
[ \t\v\f]+ yylloc->step();
|
||||
"/*" BEGIN(in_COMMENT);
|
||||
"//".* continue;
|
||||
"/""*"+ BEGIN(in_COMMENT); comment_level = 1;
|
||||
"\"" BEGIN(in_STRING);
|
||||
|
||||
"HOA:" return token::HOA;
|
||||
|
|
@ -97,10 +98,12 @@ identifier [[:alpha:]_][[:alnum:]_-]*
|
|||
}
|
||||
|
||||
<in_COMMENT>{
|
||||
[^*\n]* continue;
|
||||
"/""*"+ ++comment_level;
|
||||
[^*/\n]* continue;
|
||||
"/"[^*\n]* continue;
|
||||
"*"+[^*/\n]* continue;
|
||||
"\n"+ yylloc->end.column = 1; yylloc->lines(yyleng);
|
||||
"*"+"/" BEGIN(INITIAL);
|
||||
"*"+"/" if (--comment_level == 0) BEGIN(INITIAL);
|
||||
<<EOF>> {
|
||||
error_list.push_back(
|
||||
spot::hoa_parse_error(*yylloc,
|
||||
|
|
@ -155,6 +158,7 @@ namespace spot
|
|||
// ended badly.
|
||||
YY_NEW_FILE;
|
||||
BEGIN(INITIAL);
|
||||
comment_level = 0;
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -300,6 +300,7 @@ EOF
|
|||
|
||||
cat >input<<EOF
|
||||
HOA: v1
|
||||
tool: "test"
|
||||
States: 3
|
||||
Start: 0
|
||||
acc-name: generalized-Buchi 2
|
||||
|
|
@ -320,7 +321,7 @@ cat >input<<EOF
|
|||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:13.7: too many transition for this state, ignoring this one
|
||||
input:14.7: too many transition for this state, ignoring this one
|
||||
EOF
|
||||
|
||||
|
||||
|
|
@ -356,7 +357,7 @@ cat >input <<EOF
|
|||
name: "GFa & GF(b & c)"
|
||||
States: 1
|
||||
Start: 0
|
||||
acc-name: generalized-Buchi 2
|
||||
acc-name: who cares
|
||||
Acceptance: 2 (Inf(0) & Inf(1))
|
||||
AP: 3 "a" "b" "c"
|
||||
Alias: @a 0
|
||||
|
|
@ -417,6 +418,7 @@ State: 0 {0}
|
|||
State: 1
|
||||
[!0] 1
|
||||
[0] 0
|
||||
[f] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
|
|
@ -499,7 +501,7 @@ Acceptance: 1 Inf(0)
|
|||
--BODY--
|
||||
State: 0 {0}
|
||||
[1] 1
|
||||
[!1] 0
|
||||
[!1] 0 /* nested /* comment */ */
|
||||
State: 1
|
||||
[!0] 1
|
||||
[0] 0
|
||||
|
|
@ -524,6 +526,33 @@ State: 1
|
|||
--END--
|
||||
EOF
|
||||
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: [1] 0 {0}
|
||||
[!1] 0
|
||||
1
|
||||
State: 1
|
||||
[!0] 1
|
||||
2
|
||||
State: 2
|
||||
1
|
||||
[t] 2
|
||||
1 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:8.1-4: cannot label this edge because...
|
||||
input:7.8-10: ... the state is already labeled.
|
||||
input:12.6: missing label for this edge (previous edge is labeled)
|
||||
input:15.1-3: ignoring this label, because previous edge has no label
|
||||
EOF
|
||||
|
||||
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
|
|
@ -618,3 +647,73 @@ input:32.1-5: syntax error, unexpected header name, expecting --END-- or State:
|
|||
input:37.1-4: syntax error, unexpected identifier, expecting end of file or HOA:
|
||||
input:39.1-3: syntax error, unexpected identifier, expecting end of file or HOA:
|
||||
EOF
|
||||
|
||||
# A comment can contain --BODY-- or --END--, so we do not want to be
|
||||
# smart about it.
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: Buchi /* unclosed comment
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 1
|
||||
State: 1
|
||||
[t] 0
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 1
|
||||
State: 1
|
||||
[t] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:5.17-25.1: unclosed comment
|
||||
input:5.17-25.1: syntax error, unexpected end of file
|
||||
autfilt: failed to read automaton from input
|
||||
EOF
|
||||
|
||||
# Likewise for strings
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
tool: "unterminated string
|
||||
AP: 0
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 1
|
||||
State: 1
|
||||
[t] 0
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 1
|
||||
State: 1
|
||||
[t] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:4.7-242: unclosed string
|
||||
input:4.7-242: syntax error, unexpected end of file, expecting string
|
||||
autfilt: failed to read automaton from input
|
||||
EOF
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue