Remove marks from acceptance condition without stripping

Author: Alexandre Duret-Lutz.

* NEWS: mention the modification.
* spot/twa/acc.cc, spot/twa/acc.hh: Implement the removal.
* spot/twa/twa.hh: Allow directly setting a new acceptance condition.

NEWS

@@ -93,6 +93,12 @@ New in spot 2.3.4.dev (not yet released)
     scc_info::common_sets_of(scc), and they are used by scc_info to
     classify some SCCs as rejecting more easily.
 
+  - The new function acc_code::remove() removes all the given
+    acceptance sets from the acceptance condition.
+
+  - It is now possible to change an automaton acceptance condition
+    directly by calling twa::set_acceptance().
+
   Python:
 
   - The 'spot.gen' package exports the functions from libspotgen.

spot/twa/acc.cc

@@ -1253,10 +1253,8 @@ namespace spot
       SPOT_UNREACHABLE();
       return {};
     }
-
   }
 
-
   acc_cond::acc_code acc_cond::acc_code::complement() const
   {
     if (is_t())
@@ -1267,7 +1265,8 @@ namespace spot
   namespace
   {
     static acc_cond::acc_code
-    strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing)
+    strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing,
+              bool strip)
     {
       auto start = pos - pos->sub.size;
       switch (pos->sub.op)
@@ -1278,7 +1277,7 @@ namespace spot
             auto res = acc_cond::acc_code::t();
             do
               {
-                auto tmp = strip_rec(pos, rem, missing) & std::move(res);
+                auto tmp = strip_rec(pos, rem, missing, strip) & std::move(res);
                 std::swap(tmp, res);
                 pos -= pos->sub.size + 1;
               }
@@ -1291,7 +1290,7 @@ namespace spot
             auto res = acc_cond::acc_code::f();
             do
               {
-                auto tmp = strip_rec(pos, rem, missing) | std::move(res);
+                auto tmp = strip_rec(pos, rem, missing, strip) | std::move(res);
                 std::swap(tmp, res);
                 pos -= pos->sub.size + 1;
               }
@@ -1301,11 +1300,15 @@ namespace spot
         case acc_cond::acc_op::Fin:
           if (missing && (pos[-1].mark & rem))
             return acc_cond::acc_code::t();
-          return acc_cond::acc_code::fin(pos[-1].mark.strip(rem));
+          return acc_cond::acc_code::fin(strip
+                                         ? pos[-1].mark.strip(rem)
+                                         : pos[-1].mark - rem);
         case acc_cond::acc_op::Inf:
           if (missing && (pos[-1].mark & rem))
             return acc_cond::acc_code::f();
-          return acc_cond::acc_code::inf(pos[-1].mark.strip(rem));
+          return acc_cond::acc_code::inf(strip
+                                         ? pos[-1].mark.strip(rem)
+                                         : pos[-1].mark - rem);
         case acc_cond::acc_op::FinNeg:
         case acc_cond::acc_op::InfNeg:
           SPOT_UNREACHABLE();
@@ -1321,7 +1324,15 @@ namespace spot
   {
     if (is_t() || is_f())
       return *this;
-    return strip_rec(&back(), rem, missing);
+    return strip_rec(&back(), rem, missing, true);
+  }
+
+  acc_cond::acc_code
+  acc_cond::acc_code::remove(acc_cond::mark_t rem, bool missing) const
+  {
+    if (is_t() || is_f())
+      return *this;
+    return strip_rec(&back(), rem, missing, false);
   }
 
   acc_cond::mark_t

spot/twa/acc.hh

@@ -387,14 +387,16 @@ namespace spot
               case acc_cond::acc_op::InfNeg:
               case acc_cond::acc_op::Fin:
               case acc_cond::acc_op::FinNeg:
-                pos -= 2;
+                {
-                auto m = (*this)[pos].mark;
+                  pos -= 2;
-                auto om = other[pos].mark;
+                  auto m = (*this)[pos].mark;
-                if (m < om)
+                  auto om = other[pos].mark;
-                  return true;
+                  if (m < om)
-                if (m > om)
+                    return true;
-                  return false;
+                  if (m > om)
-                break;
+                    return false;
+                  break;
+                }
               }
           }
         return false;
@@ -906,6 +908,8 @@ namespace spot
       // If MISSING is unset, Inf(rem) become t while Fin(rem) become
       // f.  Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
       // Inf(1)|Fin(3).
+      acc_code remove(acc_cond::mark_t rem, bool missing) const;
+      // Same as remove, but also shift numbers
       acc_code strip(acc_cond::mark_t rem, bool missing) const;
 
       // Return the set of sets appearing in the condition.
@@ -1295,6 +1299,38 @@ namespace spot
       return u;
     }
 
+    // Remove all the acceptance sets in rem.
+    //
+    // If MISSING is set, the acceptance sets are assumed to be
+    // missing from the automaton, and the acceptance is updated to
+    // reflect this.  For instance (Inf(1)&Inf(2))|Fin(3) will
+    // become Fin(3) if we remove 2 because it is missing from this
+    // automaton, because there is no way to fulfill Inf(1)&Inf(2)
+    // in this case.  So essentially MISSING causes Inf(rem) to
+    // become f, and Fin(rem) to become t.
+    //
+    // If MISSING is unset, Inf(rem) become t while Fin(rem) become
+    // f.  Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
+    // Inf(1)|Fin(3).
+    acc_cond remove(mark_t rem, bool missing) const
+    {
+      return {num_sets(), code_.remove(rem, missing)};
+    }
+
+    // Same as remove, but also shift the set numbers
+    acc_cond strip(mark_t rem, bool missing) const
+    {
+      return
+        { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
+    }
+
+    // Restrict an acceptance condition to a subset of set numbers
+    // that are occurring at some point.
+    acc_cond restrict_to(mark_t rem) const
+    {
+      return {num_sets(), code_.remove(all_sets() - rem, true)};
+    }
+
   protected:
     mark_t::value_t all_sets_() const
     {

spot/twa/twa.hh

@@ -924,6 +924,14 @@ namespace spot
       acc_.set_acceptance(c);
     }
 
+    /// \brief Set the acceptance condition of the automaton.
+    ///
+    /// \param c another acceptance condition
+    void set_acceptance(const acc_cond& c)
+    {
+      acc_ = c;
+    }
+
     /// Copy the acceptance condition of another TωA.
     void copy_acceptance_of(const const_twa_ptr& a)
     {