From 691ab0592661de584cf1c0f8caec30bc3eda232d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 21 Nov 2014 10:49:58 +0100
Subject: [PATCH] hoa: catch redefinition of states

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: More test.
---
 src/hoaparse/hoaparse.yy   | 19 +++++++++++++++++--
 src/tgbatest/hoaparse.test | 18 ++++++++++++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index cbac5cf7e..c45340bba 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -47,6 +47,7 @@
     std::vector<int> ap;
     std::vector<bdd> guards;
     std::vector<bdd>::const_iterator cur_guard;
+    std::vector<bool> declared_states; // States that have been declared.
     spot::location states_loc;
     spot::location ap_loc;
     spot::location state_label_loc;
@@ -189,6 +190,7 @@ header-item: "States:" INT
 	       - res.h->aut->num_states();
 	     assert(missing >= 0);
 	     res.h->aut->new_states(missing);
+	     res.declared_states.resize(res.declared_states.size() + missing);
 	   }
            | "Start:" state-conj-2
 	     {
@@ -443,7 +445,11 @@ state-num: INT
 		   }
 		 int missing = ((int) $1) - res.h->aut->num_states() + 1;
 		 if (missing >= 0)
-		   res.h->aut->new_states(missing);
+		   {
+		     res.h->aut->new_states(missing);
+		     res.declared_states.resize(res.declared_states.size()
+						+ missing);
+		   }
 	       }
 	     $$ = $1;
 	   }
@@ -462,6 +468,13 @@ state: state-name labeled-edges
 state-name: "State:" state-label_opt state-num string_opt acc-sig_opt
 	  {
 	    res.cur_state = $3;
+	    if (res.declared_states[$3])
+	      {
+		std::ostringstream o;
+		o << "redeclaration of state " << $3;
+		error(@1 + @3, o.str());
+	      }
+	    res.declared_states[$3] = true;
 	    res.acc_state = $5;
 	  }
 label: '[' label-expr ']'
@@ -614,7 +627,9 @@ namespace spot
     if (!r.h->aut)
       return nullptr;
     if (r.start != -1)
-      r.h->aut->set_init_state(r.start);
+      {
+	r.h->aut->set_init_state(r.start);
+      }
     else
       {
 	// If no initial state has been declared, add one, because
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 11f9e8e38..df3cc96f3 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -85,6 +85,24 @@ input:10.5: state number is larger than state count...
 input:2.1-9: ... declared here.
 EOF
 
+cat >input <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0 {0}
+[0] 0
+State: 0 {0}
+[t] 0
+--END--
+EOF
+
+expecterr input <<EOF
+input:9.1-8: redeclaration of state 0
+EOF
+
 cat >input <<EOF
 HOA: v1
 States: 0