From 778d8fe95b0ec377f7739d597aa144b05ce23629 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 12 May 2015 20:13:19 +0200
Subject: [PATCH] ltl2tgba_fm: make it easier to preserve state names

* src/twa/twagraph.cc, src/twa/twagraph.hh (create_formula_namer,
release_formula_namer): New functions.
* src/twaalgos/ltl2tgba_fm.cc: Use it.
---
 src/twa/twagraph.cc         | 30 ++++++++++++++++++++++++++++++
 src/twa/twagraph.hh         | 11 +++++++++++
 src/twaalgos/ltl2tgba_fm.cc |  5 ++---
 3 files changed, 43 insertions(+), 3 deletions(-)

diff --git a/src/twa/twagraph.cc b/src/twa/twagraph.cc
index 0f29d3393..10eb6a409 100644
--- a/src/twa/twagraph.cc
+++ b/src/twa/twagraph.cc
@@ -19,9 +19,39 @@
 
 #include "twagraph.hh"
 #include "ltlast/constant.hh"
+#include "ltlvisit/tostring.hh"
 
 namespace spot
 {
+  void
+  twa_graph::release_formula_namer(typename namer<const ltl::formula*>::type*
+				   namer, bool keep_names)
+  {
+    if (keep_names)
+      {
+	auto v = new std::vector<std::string>(num_states());
+	auto& n = namer->names();
+	unsigned ns = n.size();
+	assert(n.size() <= v->size());
+	for (unsigned i = 0; i < ns; ++i)
+	  {
+	    auto f = n[i];
+	    if (f)
+	      {
+		(*v)[i] = to_string(f);
+		f->destroy();
+	      }
+	  }
+	set_named_prop("state-names", v);
+      }
+    else
+      {
+	for (auto n: namer->names())
+	  if (n)
+	    n->destroy();
+      }
+    delete namer;
+  }
 
   void twa_graph::merge_transitions()
   {
diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh
index 51b32f252..6d49b39a0 100644
--- a/src/twa/twagraph.hh
+++ b/src/twa/twagraph.hh
@@ -25,6 +25,7 @@
 #include "twa/bdddict.hh"
 #include "twa/twa.hh"
 #include "twaalgos/dupexp.hh"
+#include "ltlast/formula.hh"
 #include <sstream>
 
 namespace spot
@@ -222,6 +223,16 @@ namespace spot
       return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_);
     }
 
+    typename namer<const ltl::formula*>::type*
+    create_formula_namer()
+    {
+      return create_namer<const ltl::formula*>();
+    }
+
+    void
+    release_formula_namer(typename namer<const ltl::formula*>::type* namer,
+			  bool keep_names);
+
     graph_t& get_graph()
     {
       return g_;
diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index add30de53..2d07cfd2c 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -2537,9 +2537,8 @@ namespace spot
 	}
       }
 
-    for (auto n: namer->names())
-      n->destroy();
-    delete namer;
+    // Set the following to true to preserve state names.
+    a->release_formula_namer(namer, false);
 
     dict->register_propositions(fc.used_vars(), a);