From a26dd5af1d4b6ab6feda64095edb5056c19f2190 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 9 Sep 2015 00:44:39 +0200
Subject: [PATCH] parseaut: better recovery from dstar errors

* src/parseaut/parseaut.yy: Do not call YYABORT on errors
in headers.
* src/tests/parseaut.test: Test this.
---
 src/parseaut/parseaut.yy | 46 +++++++++++-------------
 src/tests/parseaut.test  | 75 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 95 insertions(+), 26 deletions(-)

diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy
index 9571c206b..c64325cba 100644
--- a/src/parseaut/parseaut.yy
+++ b/src/parseaut/parseaut.yy
@@ -1125,39 +1125,25 @@ dstar_type: "DRA"
 
 dstar_header: dstar_sizes
   {
-    bool err = false;
     if (res.states < 0)
-      {
-	error(@1, "missing state count");
-	err = true;
-      }
+      error(@1, "missing state count");
     if (!res.ignore_more_acc)
-      {
-	error(@1, "missing acceptance-pair count");
-	err = true;
-      }
+      error(@1, "missing acceptance-pair count");
     if (res.start.empty())
-      {
-	error(@1, "missing start-state number");
-	err = true;
-      }
+      error(@1, "missing start-state number");
     if (!res.ignore_more_ap)
+      error(@1, "missing atomic propositions definition");
+
+    if (res.states > 0)
       {
-	error(@1, "missing atomic proposition definition");
-	err = true;
+	res.h->aut->new_states(res.states);;
+	res.info_states.resize(res.states);
       }
-    if (err)
-      {
-	res.h->aut = nullptr;
-	YYABORT;
-      }
-    res.h->aut->new_states(res.states);;
-    res.info_states.resize(res.states);
-    fill_guards(res);
-    res.cur_guard = res.guards.end();
     res.h->aut->prop_state_based_acc();
     res.h->aut->prop_deterministic();
     // res.h->aut->prop_complete();
+    fill_guards(res);
+    res.cur_guard = res.guards.end();
   }
 
 dstar_sizes:
@@ -1182,7 +1168,16 @@ dstar_sizes:
   }
   | dstar_sizes "States:" INT
   {
-    res.states = $3;
+    if (res.states < 0)
+      {
+	res.states = $3;
+      }
+    else
+      {
+	error(@$, "redeclaration of state count");
+	if ((unsigned) res.states < $3)
+	  res.states = $3;
+      }
   }
   | dstar_sizes "Start:" INT
   {
@@ -1642,7 +1637,6 @@ lbtt-transitions:
 
 static void fill_guards(result_& r)
 {
-  spot::bdd_dict_ptr d = r.h->aut->get_dict();
   unsigned nap = r.ap.size();
 
   int* vars = new int[nap];
diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test
index 8ee2edc45..15cf0beef 100755
--- a/src/tests/parseaut.test
+++ b/src/tests/parseaut.test
@@ -1025,6 +1025,81 @@ input:81.1: $se \$undefined
 autfilt: failed to read automaton from input
 EOF
 
+# More error recovery in DSTAR automata
+cat >input <<EOF
+DRA v2 explicit
+Comment: "Safra[NBA=2]"
+States: 3
+States: 3
+Start: 0
+AP: 2 "a" "b"
+---
+State: 0
+Acc-Sig:
+1
+0
+2
+2
+State: 1
+Acc-Sig: -0
+1
+1
+1
+1
+State: 2
+Acc-Sig: +0
+2
+2
+2
+2
+never { /* true */
+accept_init:
+	if
+	:: (1) -> goto accept_init
+	fi;
+}
+EOF
+
+../../bin/autfilt input -H >output 2>&1 && exit 1
+cat output
+cat >expected <<EOF
+input:1.16-4.9: redeclaration of state count
+input:1.16-6.13: missing acceptance-pair count
+input:15.11: no acceptance pairs have been declared
+input:21.11: no acceptance pairs have been declared
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0&!1] 0
+[!0&!1] 1
+[1] 2
+State: 1
+[t] 1
+State: 2
+[t] 2
+--END--
+HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic
+--BODY--
+State: 0 {0}
+[t] 0
+--END--
+EOF
+diff output expected
+
 # A comment can contain --BODY-- or --END--, so we do not want to be
 # smart about it.
 cat >input <<EOF