From 93271bed6f1188a5324bca32c74c62e7cf9189ca Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Jan 2015 18:36:45 +0100
Subject: [PATCH] randomize: reorder state names

* src/tgbaalgos/randomize.cc: Reorder state names.
* src/tgbatest/randomize.test: Add a new test.
---
 src/tgbaalgos/randomize.cc  | 10 +++++++
 src/tgbatest/randomize.test | 56 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 65 insertions(+), 1 deletion(-)

diff --git a/src/tgbaalgos/randomize.cc b/src/tgbaalgos/randomize.cc
index acf3c1a0e..675fdffd0 100644
--- a/src/tgbaalgos/randomize.cc
+++ b/src/tgbaalgos/randomize.cc
@@ -39,6 +39,16 @@ namespace spot
 	std::random_shuffle(nums.begin(), nums.end(), spot::mrand);
 	g.rename_states_(nums);
 	aut->set_init_state(nums[aut->get_init_state_number()]);
+
+	if (auto sn =
+	    aut->get_named_prop<std::vector<std::string>>("state-names"))
+	  {
+	    unsigned sns = sn->size(); // Might be != n.
+	    auto nn = new std::vector<std::string>(n);
+	    for (unsigned i = 0; i < sns && i < n; ++i)
+	      (*nn)[nums[i]] = (*sn)[i];
+	    aut->set_named_prop("state-names", nn);
+	  }
       }
     if (randomize_transitions)
       {
diff --git a/src/tgbatest/randomize.test b/src/tgbatest/randomize.test
index 7f922afb7..201d07520 100755
--- a/src/tgbatest/randomize.test
+++ b/src/tgbatest/randomize.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014 Laboratoire de Recherche et Développement de
+# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -80,3 +80,57 @@ diff 4.dot 4b.dot
 
 $autfilt --randomize=foo out 2>stderr && exit 1
 grep "unknown argument for --randomize: 'f'" stderr
+
+
+# Make sure names are moved.
+cat >input <<EOF
+HOA: v1
+States: 5
+Start: 0
+AP: 4 "a" "b" "c" "d"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 "s0"
+[0] 1
+[1] 2
+[2] 3
+[3] 4
+State: 1 "s1"
+[0] 1
+State: 2 "s2"
+[1] 2
+State: 3 "s3"
+[2] 3
+State: 4 "s4"
+[3] 4
+--END--
+EOF
+$autfilt --randomize --seed=1 input -H > output
+cat >expected <<EOF
+HOA: v1
+States: 5
+Start: 1
+AP: 4 "a" "b" "c" "d"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 "s1"
+[0] 0
+State: 1 "s0"
+[1] 3
+[0] 0
+[2] 2
+[3] 4
+State: 2 "s3"
+[2] 2
+State: 3 "s2"
+[1] 3
+State: 4 "s4"
+[3] 4
+--END--
+EOF
+
+diff output expected