diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 312a4e068..9571c206b 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -261,6 +261,12 @@ aut: aut-1 { res.h->loc = @$; YYACCEPT; } | ENDOFFILE { YYABORT; } | error ENDOFFILE { YYABORT; } + | error aut-1 + { + error(@1, "leading garbage was ignored"); + res.h->loc = @2; + YYACCEPT; + } aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } | never { res.h->type = spot::parsed_aut_type::NeverClaim; } @@ -272,7 +278,7 @@ aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } /**********************************************************************/ hoa: header "--BODY--" body "--END--" -hoa: error "--END--" + | "HOA:" error "--END--" string_opt: { $$ = nullptr; } | STRING { $$ = $1; } @@ -420,10 +426,6 @@ version: IDENTIFIER } format-version: "HOA:" { res.h->loc = @1; } version - | error "HOA:" - { error(@1, "ignoring leading garbage"); - res.h->loc = @2; } - version aps: "AP:" INT { if (res.ignore_more_ap) @@ -1102,7 +1104,11 @@ incorrectly-labeled-edge: trans-label unlabeled-edge /* Rules for LTL2DSTAR's format */ /**********************************************************************/ -dstar: dstar_header "---" dstar_states ENDDSTAR +dstar: dstar_type "v2" "explicit" dstar_header "---" dstar_states ENDDSTAR + | dstar_type error ENDDSTAR + { + error(@$, "failed to parse this as an ltl2dstar automaton"); + } dstar_type: "DRA" { @@ -1117,27 +1123,27 @@ dstar_type: "DRA" res.minus = 1; } -dstar_header: dstar_type "v2" "explicit" dstar_sizes +dstar_header: dstar_sizes { bool err = false; if (res.states < 0) { - error(@4, "missing state count"); + error(@1, "missing state count"); err = true; } if (!res.ignore_more_acc) { - error(@4, "missing acceptance-pair count"); + error(@1, "missing acceptance-pair count"); err = true; } if (res.start.empty()) { - error(@4, "missing start-state number"); + error(@1, "missing start-state number"); err = true; } if (!res.ignore_more_ap) { - error(@4, "missing atomic proposition definition"); + error(@1, "missing atomic proposition definition"); err = true; } if (err) @@ -1155,11 +1161,7 @@ dstar_header: dstar_type "v2" "explicit" dstar_sizes } dstar_sizes: -/* | dstar_sizes error eols - { - error(@2, "unknown header ignored"); - } -*/ + | dstar_sizes error | dstar_sizes "Acceptance-Pairs:" INT { if (res.ignore_more_acc) @@ -1260,6 +1262,7 @@ dstar_transitions: } dstar_states: + | dstar_states error | dstar_states dstar_state_id dstar_state_accsig dstar_transitions { for (auto i: res.dest_map) diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test index 754128cf0..8ee2edc45 100755 --- a/src/tests/parseaut.test +++ b/src/tests/parseaut.test @@ -962,6 +962,48 @@ State: 1 this is complete garbage! --END-- and even more garbage +DRA v2 explicit +Comment: "Safra[NBA=2]" +States: 2 +garbage /* <<--- */ +Acceptance-Pairs: 1 +Start: 0 +AP: 1 "a" +--- +State: 0 +Acc-Sig: +0 +1 +State: 1 +Acc-Sig: +0 +0 +1 +more garbage +DRA v2 explicit +Comment: "Safra[NBA=2]" +States: 2 +Acceptance-Pairs: 1 +Start: 0 +AP: 1 "a" +--- +State: 0 +Acc-Sig: +0 +1 +State: 1 +Acc-Sig: +0 +0 +1 +HOA: v1 +States: 1 +Start: 0 +AP: 0 +Acceptance: 1 Inf(0) +--BODY-- +State: 0 {0} +[t] 0 +--END-- +garbage EOF se='syntax error, unexpected' # this is just to keep lines short @@ -972,10 +1014,14 @@ input:11.2: $se identifier input:11.1-3: ignoring this invalid label input:21.5-7: $se string, expecting integer input:25.1: $se \$undefined -input:25.1-12: ignoring leading garbage input:32.1-5: $se header name, expecting --END-- or State: input:28.1-8: initial state 0 has no definition +input:25.1-12: leading garbage was ignored input:37.1: $se 't' +input:43.1: $se \$undefined +input:56.1: $se \$undefined, expecting State: or end of DSTAR automaton +input:37.1-39.21: leading garbage was ignored +input:81.1: $se \$undefined autfilt: failed to read automaton from input EOF