defrag_states: allow a permutation of state numbers

* spot/misc/permute.hh: New file.
* spot/misc/Makefile.am: Add it.
* spot/graph/graph.hh, spot/twa/twagraph.cc,
spot/twaalgos/randomize.cc: Use the new permute_vector() function.
* spot/twa/twagraph.hh: Update documentation.
* NEWS: Update.

NEWS

@@ -93,6 +93,9 @@ New in spot 2.12.0.dev (not yet released)
      any word accepted by A from state x satisfies V[x].  Related to
      Issue #591.
 
+  - twa_graph::defrag_states(num) no longer require num[i]≤i; num
+    can now describe a permutation of the state numbers.
+
   Bug fixes:
 
   - Generating random formulas without any unary opertor would very

spot/graph/graph.hh

@@ -20,6 +20,7 @@
 
 #include <spot/misc/common.hh>
 #include <spot/misc/_config.h>
+#include <spot/misc/permute.hh>
 #include <vector>
 #include <type_traits>
 #include <tuple>
@@ -1446,8 +1447,7 @@ namespace spot
     /// dangling.
     ///
     /// \param newst A vector indicating how each state should be
-    /// renumbered.  Use -1U to erase an unreachable state.  All other
+    /// renumbered.  Use -1U to erase an unreachable state.
-    /// numbers are expected to satisfy newst[i] ≤ i for all i.
     ///
     /// \param used_states the number of states used (after
     /// renumbering)
@@ -1461,24 +1461,19 @@ namespace spot
       //std::cerr << "\nbefore defrag\n";
       //dump_storage(std::cerr);
 
-      // Shift all states in states_, as indicated by newst.
+      // Permute all states in states_, as indicated by newst.
+      // This will put erased states after used_states.
+      permute_vector(states_, newst);
       unsigned send = states_.size();
-      for (state s = 0; s < send; ++s)
+      for (state s = used_states; s < send; ++s)
         {
-          state dst = newst[s];
+          // This is an erased state.  Mark all its edges as
-          if (dst == s)
+          // dead (i.e., t.next_succ should point to t for each of
-            continue;
+          // them).
-          if (dst == -1U)
+          auto t = states_[s].succ;
-            {
+          while (t)
-              // This is an erased state.  Mark all its edges as
+            std::swap(t, edges_[t].next_succ);
-              // dead (i.e., t.next_succ should point to t for each of
+          continue;
-              // them).
-              auto t = states_[s].succ;
-              while (t)
-                std::swap(t, edges_[t].next_succ);
-              continue;
-            }
-          states_[dst] = std::move(states_[s]);
         }
       states_.resize(used_states);
 

spot/misc/Makefile.am

@@ -46,6 +46,7 @@ misc_HEADERS = \
   memusage.hh \
   mspool.hh \
   optionmap.hh \
+  permute.hh \
   position.hh \
   random.hh \
   satsolver.hh \

spot/misc/permute.hh

@@ -0,0 +1,81 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/misc/common.hh>
+#include <vector>
+#include <algorithm>
+
+namespace spot
+{
+
+  // Reorder `data` according the permutation in `indices` by
+  // following the cycles in the permutation.  Additionally, if an
+  // index is -1, the corresponding value is moved to the end of the
+  // data.
+  //
+  // After running this algorithm, data[i] should be moved to
+  // data[indices[i]] or to the end of the data if indices[i] == -1U.
+  //
+  // If indices.size() != data.size(), the minimum of both size is
+  // used, and indices are expected to stay in this range.
+  template<typename values>
+  void permute_vector(std::vector<values>& data,
+                      const std::vector<unsigned>& indices)
+  {
+    unsigned n = std::min(data.size(), indices.size());
+    if (n == 0)
+      return;
+    std::vector<bool> done(n, false);
+    unsigned end_of_data = n - 1; // index for the first -1
+    for (unsigned i = 0; i < n; ++i)
+      {
+        if (done[i] || indices[i] == i)
+          continue;             // already done or identity
+        unsigned next = indices[i];
+        if (next == -1U)
+          {
+            next = end_of_data--;
+            if (next == i)
+              continue;
+          }
+        values tmp = std::move(data[i]);
+        while (next != i)
+          {
+            SPOT_ASSERT(next < n);
+            if (done[next])
+              throw std::invalid_argument
+                ("permute_vector: invalid permutation");
+            // this is a swap, but std::swap will not work
+            // when data[next] is a bool_reference.
+            values tmp2 = std::move(data[next]);
+            data[next] = std::move(tmp);
+            tmp = std::move(tmp2);
+            done[next] = true;
+
+            next = indices[next];
+            if (next == -1U)
+              next = end_of_data--;
+          }
+        data[i] = std::move(tmp);
+        done[i] = true;
+      }
+  }
+
+}

spot/twa/twagraph.cc

@@ -1257,18 +1257,10 @@ namespace spot
         for (auto& e: edges())
           fixup(e.dst);
       }
-
+    // Update properties...
     if (auto* names = get_named_prop<std::vector<std::string>>("state-names"))
       {
-        unsigned size = names->size();
+        permute_vector(*names, newst);
-        for (unsigned s = 0; s < size; ++s)
-          {
-            unsigned dst = newst[s];
-            if (dst == s || dst == -1U)
-              continue;
-            assert(dst < s);
-            (*names)[dst] = std::move((*names)[s]);
-          }
         names->resize(used_states);
       }
     if (auto hs = get_named_prop<std::map<unsigned, unsigned>>
@@ -1325,15 +1317,7 @@ namespace spot
                             "degen-levels"})
       if (auto os = get_named_prop<std::vector<unsigned>>(prop))
         {
-          unsigned size = os->size();
+          permute_vector(*os, newst);
-          for (unsigned s = 0; s < size; ++s)
-            {
-              unsigned dst = newst[s];
-              if (dst == s || dst == -1U)
-                continue;
-              assert(dst < s);
-              (*os)[dst] = (*os)[s];
-            }
           os->resize(used_states);
         }
     if (auto ss = get_named_prop<std::vector<unsigned>>("simulated-states"))
@@ -1349,19 +1333,10 @@ namespace spot
     // Reassign the state-players
     if (auto sp = get_named_prop<std::vector<bool>>("state-player"))
       {
-        const auto ns = (unsigned) used_states;
+        permute_vector(*sp, newst);
-        const auto sps = (unsigned) sp->size();
+        sp->resize(used_states);
-        assert(ns <= sps);
-        assert(sps == newst.size());
-
-        for (unsigned i = 0; i < sps; ++i)
-          {
-            if (newst[i] == -1u)
-              continue;
-            (*sp)[newst[i]] = (*sp)[i];
-          }
-        sp->resize(ns);
       }
+    // Finally, update all states and edges.
     init_number_ = newst[init_number_];
     g_.defrag_states(newst, used_states);
   }

spot/twa/twagraph.hh

@@ -734,8 +734,7 @@ namespace spot
     ///
     /// \param newst A vector indicating how each state should be
     /// renumbered.  Use -1U to mark an unreachable state for removal.
-    /// Ignoring the occurrences of -1U, the renumbering is expected
+    /// Ignoring the occurrences of -1U.   If the automaton contains
-    /// to satisfy newst[i] ≤ i for all i.   If the automaton contains
     /// universal branching, this vector is likely to be modified by
     /// this function, so do not reuse it afterwards.
     ///

spot/twaalgos/randomize.cc

@@ -20,6 +20,7 @@
 #include <algorithm>
 #include <numeric>
 #include <spot/twaalgos/randomize.hh>
+#include <spot/misc/permute.hh>
 #include <spot/misc/random.hh>
 
 namespace spot
@@ -47,11 +48,8 @@ namespace spot
         if (auto sn =
             aut->get_named_prop<std::vector<std::string>>("state-names"))
           {
-            unsigned sns = sn->size(); // Might be != n.
+            sn->resize(n);
-            auto nn = new std::vector<std::string>(n);
+            permute_vector(*sn, nums);
-            for (unsigned i = 0; i < sns && i < n; ++i)
-              (*nn)[nums[i]] = (*sn)[i];
-            aut->set_named_prop("state-names", nn);
           }
         if (auto hs = aut->get_named_prop<std::map<unsigned, unsigned>>
             ("highlight-states"))