scc_info: introduce scc_and_mark_filter

* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Here.
* spot/twaalgos/genem.cc: Use it.
* python/spot/impl.i, python/spot/__init__.py: Add bindings.
* tests/python/genem.py: Test it.
* NEWS: Mention it.

NEWS

@@ -29,6 +29,12 @@ New in spot 2.7.2.dev (not yet released)
     allows "autfilt [-D] --small" to minimize very-weak automata
     whenever they are found to represent obligation properties.)
 
+  - There is a new spot::scc_and_mark_filter objet that simplify the
+    creation of filters to restrict spot::scc_info to some particular
+    SCC while cutting new SCCs on given acceptance sets.  This is used
+    by spot::generic_emptiness_check() when processing SCCs
+    recursively, and makes it easier to write similar code in Python.
+
   Bugs fixed:
 
   - When processing CSV files with MSDOS-style \r\n line endings,

python/spot/__init__.py

@@ -1244,3 +1244,12 @@ class twa_word:
         """
         from IPython.display import SVG
         return SVG(self.as_svg())
+
+
+# Make scc_and_mark filter usable as context manager
+@_extend(scc_and_mark_filter)
+class scc_and_mark_filter:
+    def __enter__(self):
+        return self
+    def __exit__(self, exc_type, exc_value, traceback):
+        self.restore_acceptance()

python/spot/impl.i

@@ -832,7 +832,6 @@ def state_is_accepting(self, src) -> "bool":
   std::string __str__() { return spot::str_psl(*self); }
 }
 
-
 %runtime %{
 #include <memory>
 

spot/twaalgos/genem.cc

@@ -57,36 +57,16 @@ namespace spot
                                         twa_run_ptr run,
                                         acc_cond::mark_t tocut))
     {
-      struct filter_data_t {
-        const scc_info& lower_si;
-        unsigned lower_scc;
-        acc_cond::mark_t cut_sets;
-      }
-      data = {si, scc, tocut};
-
-      scc_info::edge_filter filter =
-        [](const twa_graph::edge_storage_t& e, unsigned dst,
-           void* filter_data) -> scc_info::edge_filter_choice
-        {
-          auto& data = *reinterpret_cast<filter_data_t*>(filter_data);
-          if (data.lower_si.scc_of(dst) != data.lower_scc)
-            return scc_info::edge_filter_choice::ignore;
-          if (data.cut_sets & e.acc)
-            return scc_info::edge_filter_choice::cut;
-          return scc_info::edge_filter_choice::keep;
-        };
-
       // We want to remove tocut from the acceptance condition right
       // now, because hopefully this will convert the acceptance
       // condition into a Fin-less one, and then we do not have to
       // recurse it.
-      acc_cond::mark_t sets = si.acc_sets_of(scc) - tocut;
       auto& autacc = si.get_aut()->acc();
-      acc_cond acc = autacc.restrict_to(sets);
+      acc_cond acc = autacc.restrict_to(si.acc_sets_of(scc) - tocut);
       acc = acc.remove(si.common_sets_of(scc), false);
-      temporary_acc_set tmp(si.get_aut(), acc);
+      scc_and_mark_filter filt(si, scc, tocut);
-      scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data,
+      filt.override_acceptance(acc);
-                        scc_info_options::STOP_ON_ACC);
+      scc_info upper_si(filt, scc_info_options::STOP_ON_ACC);
 
       const int accepting_scc = upper_si.one_accepting_scc();
       if (accepting_scc >= 0)

spot/twaalgos/sccinfo.cc

@@ -75,6 +75,12 @@ namespace spot
     };
   }
 
+  scc_info::scc_info(scc_and_mark_filter& filt, scc_info_options options)
+    : scc_info(filt.get_aut(), filt.start_state(),
+               filt.get_filter(), &filt, options)
+  {
+  }
+
   scc_info::scc_info(const_twa_graph_ptr aut,
                      unsigned initial_state,
                      edge_filter filter,
@@ -716,6 +722,19 @@ namespace spot
                                              unsigned dst)
                              {
                                cur[src] = seen[src] = true;
+                               // if (filter_)
+                               //   {
+                               //     twa_graph::edge_storage_t e;
+                               //     e.cond = cond;
+                               //     e.src = src;
+                               //     e.dst = dst;
+                               //     if (filter_(e, dst, filter_data_)
+                               //         != edge_filter_choice::keep)
+                               //       {
+                               //         cond = bddfalse;
+                               //         return;
+                               //       }
+                               //   }
                                if (scc_of(dst) != scc
                                    || (m & sets)
                                    || (seen[dst] && !cur[dst]))

spot/twaalgos/sccinfo.hh

@@ -350,6 +350,8 @@ namespace spot
                                          | static_cast<ut>(right));
   }
 
+  class SPOT_API scc_and_mark_filter;
+
   /// \ingroup twa_misc
   /// \brief Compute an SCC map and gather assorted information.
   ///
@@ -449,11 +451,31 @@ namespace spot
       }
     /// @}
 
+    /// @{
+    /// \brief Create an scc_info map from some filter.
+    ///
+    /// This is usually used to prevent some edges from being
+    /// considered as part of cycles, and can additionally restrict
+    /// to exploration to some SCC discovered by another SCC.
+    scc_info(scc_and_mark_filter& filt,
+             scc_info_options options = scc_info_options::ALL);
+    /// @}
+
     const_twa_graph_ptr get_aut() const
     {
       return aut_;
     }
 
+    scc_info_options get_options() const
+    {
+      return options_;
+    }
+
+    const void* get_filter_data() const
+    {
+      return filter_data_;
+    }
+
     unsigned scc_count() const
     {
       return node_.size();
@@ -687,6 +709,111 @@ namespace spot
   };
 
 
+  /// \brief Create a filter for SCC and marks.
+  ///
+  /// An scc_and_mark_filter can be passed to scc_info to explore only
+  /// a specific SCC of the original automaton, and to prevent some
+  /// acceptance sets from being considered as part of SCCs.
+  class SPOT_API scc_and_mark_filter
+  {
+  protected:
+    const scc_info* lower_si_;
+    unsigned lower_scc_;
+    acc_cond::mark_t cut_sets_;
+    const_twa_graph_ptr aut_;
+    acc_cond old_acc_;
+    bool restore_old_acc_ = false;
+
+    static scc_info::edge_filter_choice
+    filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
+                         unsigned dst, void* data)
+    {
+      auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
+      if (d.lower_si_->scc_of(dst) != d.lower_scc_)
+        return scc_info::edge_filter_choice::ignore;
+      if (d.cut_sets_ & e.acc)
+        return scc_info::edge_filter_choice::cut;
+      return scc_info::edge_filter_choice::keep;
+    };
+
+    static scc_info::edge_filter_choice
+    filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data)
+    {
+      auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
+      if (d.cut_sets_ & e.acc)
+        return scc_info::edge_filter_choice::cut;
+      return scc_info::edge_filter_choice::keep;
+    };
+
+  public:
+    /// \brief Specify how to restrict scc_info to some SCC and acceptance sets
+    ///
+    /// \param lower_si the original scc_info that specifies the SCC
+    /// \param lower_scc the SCC number in lower_si
+    /// \param cut_sets the acceptance sets that should not be part of SCCs.
+    scc_and_mark_filter(const scc_info& lower_si,
+                        unsigned lower_scc,
+                        acc_cond::mark_t cut_sets)
+      : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
+        aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
+    {
+      const void* data = lower_si.get_filter_data();
+      if (data)
+        {
+          auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
+          cut_sets_ |= d.cut_sets_;
+        }
+    }
+
+    /// \brief Specify how to restrict scc_info to some acceptance sets
+    ///
+    /// \param aut the automaton to filter
+    /// \param cut_sets the acceptance sets that should not be part of SCCs.
+    scc_and_mark_filter(const const_twa_graph_ptr& aut,
+                        acc_cond::mark_t cut_sets)
+      : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
+        old_acc_(aut_->get_acceptance())
+    {
+    }
+
+    ~scc_and_mark_filter()
+    {
+      restore_acceptance();
+    }
+
+    void override_acceptance(const acc_cond& new_acc)
+    {
+      std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
+      restore_old_acc_ = true;
+    }
+
+    void restore_acceptance()
+    {
+      if (!restore_old_acc_)
+        return;
+      std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
+      restore_old_acc_ = false;
+    }
+
+    const_twa_graph_ptr get_aut() const
+    {
+      return aut_;
+    }
+
+    unsigned start_state() const
+    {
+      if (lower_si_)
+        return lower_si_->one_state_of(lower_scc_);
+      return aut_->get_init_state_number();
+    }
+
+    scc_info::edge_filter get_filter()
+    {
+      return lower_si_ ? filter_scc_and_mark_ : filter_mark_;
+    }
+  };
+
+
   /// \brief Dump the SCC graph of \a aut on \a out.
   ///
   /// If \a sccinfo is not given, it will be computed.

tests/python/genem.py

@@ -107,25 +107,12 @@ HOA: v1 States: 2 Acceptance: 6 (Fin(0)|Fin(1))&(Fin(2)|Fin(3))&
 1 {1 4} State: 1 [t] 0 {2 5} [t] 1 {3 0 1} --END--""")
 
 # From issue #360.
-a360 = spot.automaton("""HOA: v1
+a360 = spot.automaton("""HOA: v1 States: 2 Start: 0 AP: 2 "a"
-States: 2
+"b" Acceptance: 8 Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) &
-Start: 0
+Inf(0))))) & (Inf(6) | Inf(7)) & (Fin(6)|Fin(7)) properties: trans-labels
-AP: 2 "a" "b"
+explicit-labels trans-acc complete properties: deterministic --BODY--
-Acceptance: 8 Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))) &
+State: 0 [0&1] 0 {4 6 7} [0&!1] 1 {0 6} [!0&1] 0 {3 7} [!0&!1] 0 {0}
-              (Inf(6) | Inf(7)) & (Fin(6)|Fin(7))
+State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0}
-properties: trans-labels explicit-labels trans-acc complete
-properties: deterministic
---BODY--
-State: 0
-[0&1] 0 {4 6 7}
-[0&!1] 1 {0 6}
-[!0&1] 0 {3 7}
-[!0&!1] 0 {0}
-State: 1
-[0&1] 0 {4 6 7}
-[0&!1] 1 {3 6}
-[!0&1] 0 {4 7}
-[!0&!1] 1 {0}
 --END--""")
 
 
@@ -172,7 +159,7 @@ def generic_emptiness2_rec(aut):
                     return False
     return True
 
-# The python version of spot.generic_emptiness_check()
+# A very old python version of spot.generic_emptiness_check()
 def generic_emptiness2(aut):
     old_a = spot.acc_cond(aut.acc())
     res = generic_emptiness2_rec(aut)
@@ -180,16 +167,97 @@ def generic_emptiness2(aut):
     aut.set_acceptance(old_a)
     return res
 
+# A more modern python version of spot.generic_emptiness_check()
+def is_empty1(g):
+    si = spot.scc_info(g, spot.scc_info_options_NONE)
+    for scc_num in range(si.scc_count()):
+        if si.is_trivial(scc_num):
+            continue
+        if not is_scc_empty1(si, scc_num):
+            return False
+    return True
+
+def is_scc_empty1(si, scc_num, acc=None):
+    if acc is None: # acceptance isn't forced, get it from the automaton
+        acc = si.get_aut().acc()
+    occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num)
+    acc = acc.restrict_to(occur)
+    acc = acc.remove(common, False)
+    if acc.is_t(): return False
+    if acc.is_f(): return True
+    if acc.accepting(occur): return False
+    for cl in acc.top_disjuncts():
+        fu = cl.fin_unit() # Is there Fin at the top level
+        if fu:
+            with spot.scc_and_mark_filter(si, scc_num, fu) as filt:
+                filt.override_acceptance(cl.remove(fu, True))
+                if not is_empty1(filt):
+                    return False
+        else:
+            # Pick some Fin term anywhere in the formula
+            fo = cl.fin_one()
+            # Try to solve assuming Fin(fo)=True
+            with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt:
+                filt.override_acceptance(cl.remove([fo], True))
+                if not is_empty1(filt):
+                    return False
+            # Try to solve assuming Fin(fo)=False
+            if not is_scc_empty1(si, scc_num, acc.force_inf([fo])):
+                return False
+    return True
+
+def is_empty2(g):
+    si = spot.scc_info(g, spot.scc_info_options_STOP_ON_ACC)
+    if si.one_accepting_scc() >= 0:
+        return False
+    for scc_num in range(si.scc_count()):
+        if si.is_rejecting_scc(scc_num): # this includes trivial SCCs
+            continue
+        if not is_scc_empty2(si, scc_num):
+            return False
+    return True
+
+def is_scc_empty2(si, scc_num, acc=None):
+    if acc is None: # acceptance isn't forced, get it from the automaton
+        acc = si.get_aut().acc()
+    occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num)
+    acc = acc.restrict_to(occur)
+    acc = acc.remove(common, False)
+    # 3 stop conditions removed here, because they are caught by
+    # one_accepting_scc() or is_rejecting_scc() in is_empty2()
+    for cl in acc.top_disjuncts():
+        fu = cl.fin_unit() # Is there Fin at the top level
+        if fu:
+            with spot.scc_and_mark_filter(si, scc_num, fu) as filt:
+                filt.override_acceptance(cl.remove(fu, True))
+                if not is_empty1(filt):
+                    return False
+        else:
+            # Pick some Fin term anywhere in the formula
+            fo = cl.fin_one()
+            # Try to solve assuming Fin(fo)=True
+            with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt:
+                filt.override_acceptance(cl.remove([fo], True))
+                if not is_empty2(filt):
+                    return False
+            # Try to solve assuming Fin(fo)=False
+            if not is_scc_empty2(si, scc_num, acc.force_inf([fo])):
+                return False
+    return True
+
 def run_bench(automata):
     for aut in automata:
         # Make sure our three implementation behave identically
+        res5 = is_empty2(aut)
+        res4 = is_empty1(aut)
         res3 = spot.generic_emptiness_check(aut)
         res2 = spot.remove_fin(aut).is_empty()
         res1 = generic_emptiness2(aut)
-        res = str(res1)[0] + str(res2)[0] + str(res3)[0]
+        res = (str(res1)[0] + str(res2)[0] + str(res3)[0]
+               + str(res4)[0] + str(res5)[0])
         print(res)
-        assert res in ('TTT', 'FFF')
+        assert res in ('TTTTT', 'FFFFF')
-        if res == 'FFF':
+        if res == 'FFFFF':
             run3 = spot.generic_accepting_run(aut)
             assert run3.replay(spot.get_cout()) is True