Preserve named-states during defrag

* spot/twa/twagraph.cc, spot/twa/twagraph.hh,
tests/core/tgbagraph.test, tests/core/twagraph.cc,
NEWS: here.

NEWS

@@ -111,6 +111,8 @@ New in spot 1.99.6a (not yet released)
 
   Bug fixes:
 
+  * twa_graph would incorrectly replace named-states during
+    purge_dead_states and purge_unreachable_states.
   * twa::ap() would contain duplicates when an atomic proposition
     was registered several times.
   * product() would incorrectly mark the product of two

spot/twa/twagraph.cc

 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement de
 // l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -190,7 +190,7 @@ namespace spot
     if (current == todo.size())
       return;			// No unreachable state.
     init_number_ = todo[init_number_];
-    g_.defrag_states(std::move(todo), current);
+    defrag_states(std::move(todo), current);
   }
 
   void twa_graph::purge_dead_states()
@@ -266,6 +266,25 @@ namespace spot
     if (current == num_states)
       return;			// No useless state.
     init_number_ = useful[init_number_];
-    g_.defrag_states(std::move(useful), current);
+    defrag_states(std::move(useful), current);
+  }
+
+  void twa_graph::defrag_states(std::vector<unsigned>&& newst,
+				unsigned used_states)
+  {
+    auto* names = get_named_prop<std::vector<std::string>>("state-names");
+    if (names)
+      {
+	unsigned size = names->size();
+	for (unsigned s = 0; s < size; ++s)
+	  {
+	    unsigned dst = newst[s];
+	    if (dst == s || dst == -1U)
+	      continue;
+	    (*names)[dst] = std::move((*names)[s]);
+	  }
+	names->resize(used_states);
+      }
+    g_.defrag_states(std::move(newst), used_states);
   }
 }

spot/twa/twagraph.hh

 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -479,6 +479,8 @@ namespace spot
       return std::equal(trans1.begin() + 1, trans1.end(),
                         trans2.begin() + 1);
     }
+
+    void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
   };
 
   inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict)

tests/core/tgbagraph.test

 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -221,6 +221,20 @@ digraph G {
   101 [label="101"]
   102 [label="102"]
 }
+digraph G {
+  rankdir=LR
+  I [label="", style=invis, width=0]
+  I -> 2
+  0 [label="s1"]
+  1 [label="s2"]
+  2 [label="s3"]
+}
+digraph G {
+  rankdir=LR
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="s3"]
+}
 EOF
 
 diff stdout expected

tests/core/twagraph.cc

 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -84,7 +84,29 @@ static void f1()
   spot::print_dot(std::cout, tg);
 }
 
+// Test purge with named states.
+static void f2()
+{
+  auto d = spot::make_bdd_dict();
+  auto tg = make_twa_graph(d);
+
+  auto s1 = tg->new_state();
+  auto s2 = tg->new_state();
+  auto s3 = tg->new_state();
+  (void) s1;
+  (void) s2;
+  std::vector<std::string>* names;
+  names = new std::vector<std::string>({"s1", "s2", "s3"});
+
+  tg->set_named_prop<std::vector<std::string>>("state-names", names);
+  tg->set_init_state(s3);
+  spot::print_dot(std::cout, tg);
+  tg->purge_unreachable_states();
+  spot::print_dot(std::cout, tg);
+}
+
 int main()
 {
   f1();
+  f2();
 }