From 6a988f6884937fd1f45ac82b8e6de1ca847e4266 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 10 Feb 2020 14:55:13 +0100
Subject: [PATCH] degen: always compose original-states with the input

* spot/twaalgos/degen.cc (degeneralize, partial_degeneralize): Here.
* spot/twaalgos/degen.hh: Mention it.
---
 spot/twaalgos/degen.cc | 39 +++++++++++++++------------------------
 spot/twaalgos/degen.hh | 13 +++++++++++--
 2 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc
index af5368786..744c581c9 100644
--- a/spot/twaalgos/degen.cc
+++ b/spot/twaalgos/degen.cc
@@ -351,6 +351,9 @@ namespace spot
       // Preserve determinism, weakness, and stutter-invariance
       res->prop_copy(a, { false, true, true, true, true, true });
 
+      auto old_orig_states =
+        a->get_named_prop<std::vector<unsigned>>("original-states");
+
       auto orig_states = new std::vector<unsigned>();
       auto levels = new std::vector<unsigned>();
       orig_states->reserve(a->num_states()); // likely more are needed.
@@ -459,7 +462,10 @@ namespace spot
             todo.emplace_back(ds);
 
           assert(ns == orig_states->size());
-          orig_states->emplace_back(ds.first);
+          unsigned orig = ds.first;
+          if (old_orig_states)
+            orig = (*old_orig_states)[orig];
+          orig_states->emplace_back(orig);
           levels->emplace_back(ds.second);
 
           // Level cache stores one encountered level for each state
@@ -935,6 +941,8 @@ namespace spot
 
     // auto* names = new std::vector<std::string>;
     // res->set_named_prop("state-names", names);
+    auto old_orig_states =
+      a->get_named_prop<std::vector<unsigned>>("original-states");
     auto orig_states = new std::vector<unsigned>();
     auto levels = new std::vector<unsigned>();
     unsigned ns = a->num_states();
@@ -988,8 +996,12 @@ namespace spot
                        // std::ostringstream os;
                        // os << ds.first << ',' << ds.second;
                        // names->push_back(os.str());
+
+                       unsigned orig = ds.first;
+                       if (old_orig_states)
+                         orig = (*old_orig_states)[orig];
                        assert(ns == orig_states->size());
-                       orig_states->emplace_back(ds.first);
+                       orig_states->emplace_back(orig);
                        levels->emplace_back(ds.second);
                        return ns;
                      };
@@ -1094,32 +1106,11 @@ namespace spot
   twa_graph_ptr
   partial_degeneralize(twa_graph_ptr a)
   {
-    bool composeorig = false;
     while (acc_cond::mark_t m = is_partially_degeneralizable(a))
-      {
-        twa_graph_ptr b = partial_degeneralize(a, m);
-        // After the first partial degeneralization, we need to compose
-        // the original-states, so that original-states still appear
-        // to reference the original automaton.
-        if (composeorig)
-          {
-            auto origa =
-              a->get_named_prop<std::vector<unsigned>>("original-states");
-            auto origb =
-              b->get_named_prop<std::vector<unsigned>>("original-states");
-            for (auto& s: *origb)
-              s = (*origa)[s];
-          }
-        else
-          {
-            composeorig = true;
-          }
-        a = b;
-      }
+      a = partial_degeneralize(a, m);
     return a;
   }
 
-
   std::vector<acc_cond::mark_t>
   propagate_marks_vector(const const_twa_graph_ptr& aut,
                          scc_info* si)
diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh
index ca3a96ca9..27ba43f5a 100644
--- a/spot/twaalgos/degen.hh
+++ b/spot/twaalgos/degen.hh
@@ -57,9 +57,16 @@ namespace spot
   /// and the original state of the input automaton is stored in the
   /// "original-states" named property of the produced automaton.  Call
   /// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
-  /// to retrieve it.  Note that these functions may return the original
+  /// to retrieve it.  However be aware that if the input automaton
+  /// already defines the "original-states" named property, it will
+  /// be composed with the new one, so the "original-states" of the
+  /// degeneralized automaton will refer to the same automaton as the
+  /// "original-states" of the input automaton.
+  ///
+  /// Note that these functions may return the original
   /// automaton as-is if it is already degeneralized; in this case
-  /// the "original-states" property is not defined.
+  /// the "original-states" property is not defined (or not changed).
+  ///
   /// Similarly, the property "degen-levels" keeps track of the degeneralization
   /// levels.  To retrieve it, call
   /// `aut->get_named_prop<std::vector<unsigned>>("degen-levels")`.
@@ -113,6 +120,8 @@ namespace spot
   /// the input automaton unmodified if no partial degeneralization is
   /// possible.
   ///
+  /// The "original-state" and "degen-levels" named properties are
+  /// updated as for degeneralize() and degeneralize_tba().
   /// @{
   SPOT_API twa_graph_ptr
   partial_degeneralize(const const_twa_graph_ptr& a,