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>("state-names")) + { + unsigned sns = sn->size(); // Might be != n. + auto nn = new std::vector(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 < output +cat >expected <