diff --git a/NEWS b/NEWS index 8545115b7..1c4e87574 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,11 @@ New in spot 2.2.1.dev (Not yet released) being a terminal automaton is that reaching an accepting transition guarantees that any suffix will be accepted. + * The HOA parser incorrectly read "Acceptance: 1 Bar(0)" as a valid + way to specify "Acceptance: 1 Fin(0)" because it assumed that + everything that was not Inf was Fin. These errors are now + diagnosed. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 12a7ec517..3d83cbd19 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -867,11 +867,21 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' { res.pos_acc_sets |= res.aut_or_ks->acc().mark($3); if (*$1 == "Inf") - $$ = new spot::acc_cond::acc_code - (res.aut_or_ks->acc().inf({$3})); - else - $$ = new spot::acc_cond::acc_code - (res.aut_or_ks->acc().fin({$3})); + { + $$ = new spot::acc_cond::acc_code + (res.aut_or_ks->acc().inf({$3})); + } + else if (*$1 == "Fin") + { + $$ = new spot::acc_cond::acc_code + (res.aut_or_ks->acc().fin({$3})); + } + else + { + error(@1, std::string("unknown acceptance '") + *$1 + + "', expected Fin or Inf"); + $$ = new spot::acc_cond::acc_code; + } } else { diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 665f8cc70..a4c8769d0 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -152,11 +152,23 @@ AP: 2 "a" "b" Acceptance: 0 t --BODY-- --END-- +HOA: v1 +name: "1" +States: 1 +Start: 0 +AP: 0 +acc-name: Buchi +Acceptance: 1 Foo(0) +--BODY-- +State: 0 {0} +[t] 0 +--END-- EOF expecterr input <input <