From 8df616ee0d76374dc3b10430682a89ffb3900650 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 4 Feb 2020 13:47:44 +0100
Subject: [PATCH] partial_degeneralization: generalize to terms that contain
 todegen

* spot/twaalgos/degen.cc: Implement this.
* tests/python/pdegen.py: Add tests.
---
 spot/twaalgos/degen.cc | 38 +++++++++++++----------
 tests/python/pdegen.py | 68 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 91 insertions(+), 15 deletions(-)

diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc
index 50ccdbb41..1f73efd09 100644
--- a/spot/twaalgos/degen.cc
+++ b/spot/twaalgos/degen.cc
@@ -767,10 +767,14 @@ namespace spot
               SPOT_FALLTHROUGH;
             case acc_cond::acc_op::Inf:
             case acc_cond::acc_op::InfNeg:
-              pos -= 2;
-              if (code[pos].mark != todegen)
-                tostrip -= code[pos].mark;
-              break;
+              {
+                pos -= 2;
+                acc_cond::mark_t m = code[pos].mark;
+                if (todegen.subset(m))
+                  m -= todegen;
+                tostrip -= m;
+                break;
+              }
             }
         }
       while (pos > 0);
@@ -812,17 +816,21 @@ namespace spot
               SPOT_FALLTHROUGH;
             case acc_cond::acc_op::Inf:
             case acc_cond::acc_op::InfNeg:
-              pos -= 2;
-              if (code[pos].mark == todegen)
-                {
-                  code[pos].mark = accmark;
-                  updated = true;
-                }
-              else
-                {
-                  code[pos].mark = code[pos].mark.strip(tostrip);
-                }
-              break;
+              {
+                pos -= 2;
+                acc_cond::mark_t m = code[pos].mark;
+                if (todegen.subset(m))
+                  {
+                    m -= todegen;
+                    code[pos].mark = m.strip(tostrip) | accmark;
+                    updated = true;
+                  }
+                else
+                  {
+                    code[pos].mark = m.strip(tostrip);
+                  }
+                break;
+              }
             }
         }
       while (pos > 0);
diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py
index 8a387e7cf..1c27330a8 100644
--- a/tests/python/pdegen.py
+++ b/tests/python/pdegen.py
@@ -212,3 +212,71 @@ pdaut9 = spot.partial_degeneralize(aut9, sets)
 assert pdaut9.equivalent_to(aut9)
 # one more state than aut9, because dualize completed the automaton.
 assert pdaut9.num_states() == 10
+
+aut10 = spot.automaton("""HOA: v1
+States: 3
+Start: 0
+AP: 1 "p0"
+Acceptance: 3 (Fin(0)|Fin(1))&Inf(2) | Inf(0)&Inf(1)
+--BODY--
+State: 0
+[0] 1 {0}
+State: 1
+[0] 2 {2}
+[!0] 2
+State: 2
+[0] 0 {1}
+[!0] 1
+--END--""")
+pdaut10 = spot.partial_degeneralize(aut10, [0, 1])
+assert pdaut10.equivalent_to(aut10)
+assert pdaut10.to_str() ==  """HOA: v1
+States: 3
+Start: 0
+AP: 1 "p0"
+Acceptance: 2 (Fin(1) & Inf(0)) | Inf(1)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0] 1 {1}
+State: 1
+[!0] 2
+[0] 2 {0}
+State: 2
+[0] 0 {1}
+[!0] 1
+--END--"""
+
+aut11 = spot.automaton("""HOA: v1
+States: 3
+Start: 0
+AP: 1 "p0"
+Acceptance: 4 (Fin(0)|Fin(1))&Inf(2) | Inf(0)&Inf(1)&Inf(3)
+--BODY--
+State: 0
+[0] 1 {0}
+State: 1
+[0] 2 {2}
+[!0] 2
+State: 2
+[0] 0 {1}
+[!0] 1
+--END--""")
+pdaut11 = spot.partial_degeneralize(aut11, [0, 1])
+assert pdaut11.equivalent_to(aut11)
+assert pdaut11.to_str() ==  """HOA: v1
+States: 3
+Start: 0
+AP: 1 "p0"
+Acceptance: 3 (Fin(2) & Inf(0)) | (Inf(1)&Inf(2))
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0] 1 {2}
+State: 1
+[!0] 2
+[0] 2 {0}
+State: 2
+[0] 0 {2}
+[!0] 1
+--END--"""