diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 3c9181a6b..4ae1eb40c 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -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"); + } %% diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll index cb751b183..7df03ae9c 100644 --- a/src/hoaparse/hoascan.ll +++ b/src/hoaparse/hoascan.ll @@ -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:]_-]* } { - [^*\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); <> { 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; } diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index b28d18362..a7258ac4d 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -300,6 +300,7 @@ EOF cat >input<input<input <input <input <input <input <