Degeneralization keeps track of levels.

* NEWS: Document this.
* spot/twa/twagraph.cc: `copy_state_names_from` handles this new info.
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
* tests/python/origstate.py, tests/python/simstate.py: Update tests to
  reflect the change.

NEWS

@@ -54,6 +54,10 @@ New in spot 2.3.4.dev (not yet released)
     the second command outputs an automaton with states that show
     references to the first one.
 
+  - A new named property for automata called "degen-levels" keeps track
+    of the level of a state in a degeneralization. This information
+    complements the one carried in "original-states".
+
   - A new named property for automata called "simulated-states" can be
     used to record the origin of a state through simulation. The
     behavior is similar to "original-states" above. Determinization

spot/twa/twagraph.cc

@@ -607,6 +607,19 @@ namespace spot
           }
         os->resize(used_states);
       }
+    if (auto dl = get_named_prop<std::vector<unsigned>>("degen-levels"))
+      {
+        unsigned size = dl->size();
+        for (unsigned s = 0; s < size; ++s)
+          {
+            unsigned dst = newst[s];
+            if (dst == s || dst == -1U)
+              continue;
+            assert(dst < s);
+            (*dl)[dst] = (*dl)[s];
+          }
+        dl->resize(used_states);
+      }
     init_number_ = newst[init_number_];
     g_.defrag_states(std::move(newst), used_states);
   }
@@ -637,8 +650,11 @@ namespace spot
       return;
 
     auto orig = get_named_prop<std::vector<unsigned>>("original-states");
+    auto lvl = get_named_prop<std::vector<unsigned>>("degen-levels");
     auto sims = get_named_prop<std::vector<unsigned>>("simulated-states");
 
+    assert(!lvl || orig);
+
     if (orig && sims)
       throw std::runtime_error("copy_state_names_from(): original-states and "
                                "simulated-states are both set");
@@ -646,6 +662,9 @@ namespace spot
     if (orig && orig->size() != num_states())
       throw std::runtime_error("copy_state_names_from(): unexpected size "
                                "for original-states");
+    if (lvl && lvl->size() != num_states())
+      throw std::runtime_error("copy_state_names_from(): unexpected size "
+                               "for degen-levels");
 
     if (sims && sims->size() != other->num_states())
       throw std::runtime_error("copy_state_names_from(): unexpected size "
@@ -677,6 +696,8 @@ namespace spot
               throw std::runtime_error("copy_state_names_from(): state does not"
                                        " exist in source automaton");
             newname = other->format_state(other_s);
+            if (lvl)
+              newname += '#' + std::to_string((*lvl)[s]);
           }
         names->emplace_back(newname);
       }

spot/twaalgos/degen.cc

@@ -240,8 +240,11 @@ namespace spot
       res->prop_copy(a, { false, true, true, true, true, true });
 
       auto orig_states = new std::vector<unsigned>();
+      auto levels = new std::vector<unsigned>();
       orig_states->reserve(a->num_states()); // likely more are needed.
+      levels->reserve(a->num_states());
       res->set_named_prop("original-states", orig_states);
+      res->set_named_prop("degen-levels", levels);
 
       // Create an order of acceptance conditions.  Each entry in this
       // vector correspond to an acceptance set.  Each index can
@@ -328,6 +331,7 @@ namespace spot
 
           assert(ns == orig_states->size());
           orig_states->emplace_back(ds.first);
+          levels->emplace_back(ds.second);
 
           // Level cache stores one encountered level for each state
           // (the value of use_lvl_cache determinates which level

spot/twaalgos/degen.hh

@@ -56,6 +56,9 @@ namespace spot
   /// to retrieve it.  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.
+  /// Similarly, the property "degen-levels" keeps track of the degeneralization
+  /// levels.  To retrieve it, call
+  /// `aut->get_named_prop<std::vector<unsigned>>("degen-levels")`.
   /// \@{
   SPOT_API twa_graph_ptr
   degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true,

tests/python/origstate.py

@@ -67,15 +67,15 @@ acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc
 --BODY--
-State: 0 "0" {0}
+State: 0 "0#1" {0}
 [0] 0
 [!0] 1
 [1] 2
-State: 1 "0"
+State: 1 "0#0"
 [0] 0
 [!0] 1
 [1] 2
-State: 2 "1" {0}
+State: 2 "1#1" {0}
 [1] 2
 --END--"""
 
@@ -90,7 +90,7 @@ Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc colored
 properties: deterministic
 --BODY--
-State: 0 "1" {0}
+State: 0 "1#1" {0}
 [1] 0
 --END--"""
 assert aut2.to_str() == ref

tests/python/simstate.py

@@ -117,51 +117,51 @@ acc-name: parity min odd 4
 Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
 properties: trans-labels explicit-labels trans-acc deterministic
 --BODY--
-State: 0 "{₀[0,0]₀}"
+State: 0 "{₀[0#0,0#1]₀}"
 [0&!1] 0
 [0&1] 1
 [!0&1] 2
-State: 1 "{₀[0,0] [1]₀}"
+State: 1 "{₀[0#0,0#1] [1#1]₀}"
 [0&!1] 3
 [0&1] 4
 [!0&1] 1
-State: 2 "{₀[1]₀}"
+State: 2 "{₀[1#1]₀}"
 [0&!1] 5 {1}
 [0&1] 3
 [!0&1] 0
-State: 3 "{₀[0,0]{₁[1]₁}₀}"
+State: 3 "{₀[0#0,0#1]{₁[1#0]₁}₀}"
 [0&!1] 3
 [0&1] 6
 [!0&1] 7
-State: 4 "{₀[0,0] [1]{₁[1]₁}₀}"
+State: 4 "{₀[0#0,0#1] [1#1]{₁[1#0]₁}₀}"
 [0&!1] 3
 [0&1] 6
 [!0&1] 7
-State: 5 "{₀[1]₀}"
+State: 5 "{₀[1#0]₀}"
 [0&!1] 5
 [0&1] 8
 [!0&1] 0
-State: 6 "{₀[1]{₁[0,0] [1]₁}₀}"
+State: 6 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}"
 [0&!1] 8 {1}
 [0&1] 9 {1}
 [!0&1] 1 {1}
-State: 7 "{₀[1]{₁[0,0]₁}₀}"
+State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}"
 [0&!1] 8 {1}
 [0&1] 9 {1}
 [!0&1] 10
-State: 8 "{₀[0,0] [1]₀}"
+State: 8 "{₀[0#0,0#1] [1#0]₀}"
 [0&!1] 8
 [0&1] 9
 [!0&1] 1
-State: 9 "{₀[0,0] [1] [1]₀}"
+State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}"
 [0&!1] 3
 [0&1] 4
 [!0&1] 1
-State: 10 "{₀[0,0]{₁[1]₁}₀}"
+State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}"
 [0&!1] 3 {3}
 [0&1] 11
 [!0&1] 7
-State: 11 "{₀[1]{₁[0,0]{₂[1]₂}₁}₀}"
+State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
 [0&!1] 8 {1}
 [0&1] 9 {1}
 [!0&1] 1 {1}