From 5a1e38d90f216f48bb917c4e4248c0553131da3a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 9 Dec 2014 16:00:10 +0100
Subject: [PATCH] hoa: store the automaton name as a property

* src/hoaparse/hoaparse.yy: Store the automaton name.
* src/tgbaalgos/hoa.cc: Output it if it exists.
* src/tgbatest/hoaparse.test: Adjust tests.
---
 src/hoaparse/hoaparse.yy   | 4 +++-
 src/tgbaalgos/hoa.cc       | 5 ++++-
 src/tgbatest/hoaparse.test | 3 +++
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 3746223b3..09c14f2e2 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -359,7 +359,9 @@ header-item: "States:" INT
 	     }
            | "name:" STRING
              {
-	       delete $2;
+	       res.h->aut->set_named_prop("automaton-name", $2, [](void* name) {
+		   delete static_cast<std::string*>(name);
+		 });
 	     }
            | "properties:" properties
            | HEADERNAME header-spec
diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc
index 9af87195b..b8a9e6772 100644
--- a/src/tgbaalgos/hoa.cc
+++ b/src/tgbaalgos/hoa.cc
@@ -250,7 +250,10 @@ namespace spot
 
     const char nl = newline ? '\n' : ' ';
     os << "HOA: v1" << nl;
-    if (f)
+    auto* n = aut->get_named_prop("automaton-name");
+    if (n)
+      escape_str(os << "name: \"", *static_cast<std::string*>(n)) << '"' << nl;
+    else if (f)
       escape_str(os << "name: \"", to_string(f)) << '"' << nl;
     os << "States: " << num_states << nl
        << "Start: 0" << nl
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 958227236..9ba078ab0 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -384,6 +384,7 @@ EOF
 
 expectok input <<EOF
 HOA: v1
+name: "GFa & GF(b & c)"
 States: 1
 Start: 0
 AP: 3 "a" "b" "c"
@@ -431,6 +432,7 @@ AP: 1 "a"
 [!0--ABORT--
 HOA: v1
 States: 2
+name: "survivor"
 Start: 0
 Acceptance: 2 (Inf(0) & Inf(!0)) & Inf(!1)
 AP: 1 "a"
@@ -460,6 +462,7 @@ diff stderr input.exp
 
 cat >expected <<EOF
 HOA: v1
+name: "survivor"
 States: 2
 Start: 0
 AP: 1 "a"