From 0d59e55f4d62e0f387144fab952e233618ffb767 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 25 Nov 2014 11:37:29 +0100
Subject: [PATCH] hoa: fix handling of escaped characters in atomic
 propositions

* src/hoaparse/hoascan.ll: Remove superfluous line.
* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* src/tgbatest/hoaparse.test: Test it.
---
 src/hoaparse/hoascan.ll    | 1 -
 src/tgbaalgos/hoaf.cc      | 7 ++++++-
 src/tgbatest/hoaparse.test | 4 ++--
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll
index 7df03ae9c..a87734f46 100644
--- a/src/hoaparse/hoascan.ll
+++ b/src/hoaparse/hoascan.ll
@@ -118,7 +118,6 @@ identifier  [[:alpha:]_][[:alnum:]_-]*
 			   yylval->str = new std::string(s);
 			   return token::STRING;
  			}
-  \\\"			s += '"';
   \\.			s += yytext[1];
   [^\\\"]+		s.append(yytext, yyleng);
   <<EOF>>		{
diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc
index 7f11f2260..33bc5f28d 100644
--- a/src/tgbaalgos/hoaf.cc
+++ b/src/tgbaalgos/hoaf.cc
@@ -31,6 +31,7 @@
 #include "misc/minato.hh"
 #include "tgba/formula2bdd.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlast/atomic_prop.hh"
 
 namespace spot
 {
@@ -252,7 +253,11 @@ namespace spot
     auto d = aut->get_dict();
     for (metadata::vap_t::const_iterator i = md.vap.begin();
 	 i != md.vap.end(); ++i)
-      escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"';
+      {
+	auto f = ltl::is_atomic_prop(d->bdd_map[*i].f);
+	assert(f);
+	escape_str(os << " \"", f->name()) << '"';
+      }
     os << nl;
     unsigned num_acc = aut->acc().num_sets();
     if (num_acc == 0)
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 34d61bc3a..b9c8b80c2 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -456,7 +456,7 @@ States: 2
 Start: 0
 Start: 1
 Start: 0 /* duplicate */
-AP: 2 "a" "b"
+AP: 2 "a" "\"b\""
 Acceptance: 1 Inf(0)
 --BODY--
 State: 0 {0}
@@ -472,7 +472,7 @@ expectok input <<EOF
 HOA: v1
 States: 3
 Start: 0
-AP: 2 "a" "b"
+AP: 2 "a" "\"b\""
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete