From 953181bbb75011c845f832b95396e2e4070c580f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 9 Sep 2015 01:07:16 +0200
Subject: [PATCH] parseaut: store names from states in the dstar format

* src/parseaut/parseaut.yy: Keep track of named states.
* src/tests/parseaut.test: Test it.
---
 src/parseaut/parseaut.yy | 22 ++++++++++++++++++----
 src/tests/parseaut.test  |  8 ++++----
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy
index c64325cba..e78374013 100644
--- a/src/parseaut/parseaut.yy
+++ b/src/parseaut/parseaut.yy
@@ -1185,9 +1185,7 @@ dstar_sizes:
   }
   | dstar_sizes aps
 
-opt_name: | STRING { delete $1; }
-
-dstar_state_id: "State:" INT opt_name
+dstar_state_id: "State:" INT string_opt
   {
     if (res.cur_guard != res.guards.end())
       error(@1, "not enough transitions for previous state");
@@ -1205,10 +1203,26 @@ dstar_state_id: "State:" INT opt_name
 	  }
 	error(@2, o.str());
       }
+    else
+      {
+	res.info_states[$2].declared = true;
+
+	if ($3)
+	  {
+	    if (!res.state_names)
+	      res.state_names =
+		new std::vector<std::string>(res.states > 0 ?
+					     res.states : 0);
+	    if (res.state_names->size() < $2 + 1)
+	      res.state_names->resize($2 + 1);
+	    (*res.state_names)[$2] = std::move(*$3);
+	    delete $3;
+	  }
+      }
+
     res.cur_guard = res.guards.begin();
     res.dest_map.clear();
     res.cur_state = $2;
-    res.info_states[$2].declared = true;
   }
 
 sign: '+' { $$ = res.plus; }
diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test
index 15cf0beef..914fb8d97 100755
--- a/src/tests/parseaut.test
+++ b/src/tests/parseaut.test
@@ -1040,13 +1040,13 @@ Acc-Sig:
 0
 2
 2
-State: 1
+State: 1 "some name"
 Acc-Sig: -0
 1
 1
 1
 1
-State: 2
+State: 2 "another name"
 Acc-Sig: +0
 2
 2
@@ -1080,9 +1080,9 @@ State: 0
 [0&!1] 0
 [!0&!1] 1
 [1] 2
-State: 1
+State: 1 "some name"
 [t] 1
-State: 2
+State: 2 "another name"
 [t] 2
 --END--
 HOA: v1