parseaut: diagnose invalid acceptance terms

* spot/parseaut/parseaut.yy: Add a diagnostic.
* tests/core/parseaut.test: Test it.
* NEWS: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-01 15:51:55 +01:00
parent f3b95a8a11
commit 3d726fccb2
3 changed files with 32 additions and 5 deletions

5
NEWS
View file

@ -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:

View file

@ -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
{

View file

@ -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 <<EOF
input:4.1-3: ignoring this redeclaration of APs...
input:2.1-5: ... previously declared here.
input:14.15-17: unknown acceptance 'Foo', expected Fin or Inf
EOF
cat >input <<EOF