genem: implement a generic emptiness check for twa_graph_ptr

* spot/twa/acc.cc, spot/twa/acc.hh (fin_unit, one_fin): New function.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: New files.
* spot/twaalgos/Makefile.am: Add it.
* tests/python/genem.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i: Add bindings for genem.hh.
* NEWS: Mention the new function.

spot/twa/acc.cc

@@ -2121,4 +2121,62 @@ namespace spot
 
     std::swap(c, *this);
   }
+  int acc_cond::acc_code::fin_one() const
+  {
+    if (empty() || is_f())
+      return -1;
+    const acc_cond::acc_word* pos = &back();
+    do
+      {
+        switch (pos->sub.op)
+          {
+          case acc_cond::acc_op::And:
+          case acc_cond::acc_op::Or:
+            --pos;
+            break;
+          case acc_cond::acc_op::Inf:
+          case acc_cond::acc_op::InfNeg:
+          case acc_cond::acc_op::FinNeg:
+            pos -= 2;
+            break;
+          case acc_cond::acc_op::Fin:
+            return pos[-1].mark.min_set() - 1;
+          }
+      }
+    while (pos >= &front());
+    return -1;
+  }
+
+  acc_cond::mark_t acc_cond::acc_code::fin_unit() const
+  {
+    mark_t res = {};
+    if (empty() || is_f())
+      return res;
+    const acc_cond::acc_word* pos = &back();
+    do
+      {
+        switch (pos->sub.op)
+          {
+          case acc_cond::acc_op::And:
+            --pos;
+            break;
+          case acc_cond::acc_op::Or:
+            pos -= pos->sub.size + 1;
+            break;
+          case acc_cond::acc_op::Inf:
+          case acc_cond::acc_op::InfNeg:
+          case acc_cond::acc_op::FinNeg:
+            pos -= 2;
+            break;
+          case acc_cond::acc_op::Fin:
+            auto m = pos[-1].mark;
+            if (m.count() == 1)
+              res |= m;
+            pos -= 2;
+            break;
+          }
+      }
+    while (pos >= &front());
+    return res;
+  }
 }

spot/twa/acc.hh

@@ -886,6 +886,9 @@ namespace spot
 
       acc_code complement() const;
 
+      mark_t fin_unit() const;
+      int fin_one() const;
+
       // Return a list of acceptance marks needed to close a cycle
       // that already visit INF infinitely often, so that the cycle is
       // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
@@ -977,6 +980,12 @@ namespace spot
       {
       }
 
+      /// \brief Copy a part of another acceptance condition
+      acc_code(const acc_word* other)
+        : std::vector<acc_word>(other - other->sub.size, other + 1)
+      {
+      }
+
       // Calls to_text
       SPOT_API
       friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
@@ -1399,6 +1408,16 @@ namespace spot
     /// 'other', (s) shorthand for 'lo0'.
     std::string name(const char* fmt = "alo") const;
 
+    mark_t fin_unit() const
+    {
+      return code_.fin_unit();
+    }
+
+    int fin_one() const
+    {
+      return code_.fin_one();
+    }
+
   protected:
     mark_t all_sets_() const
     {

spot/twaalgos/Makefile.am

@@ -50,6 +50,7 @@ twaalgos_HEADERS = \
   dualize.hh \
   emptiness.hh \
   emptiness_stats.hh \
+  genem.hh \
   gfguarantee.hh \
   gv04.hh \
   hoa.hh \
@@ -117,6 +118,7 @@ libtwaalgos_la_SOURCES = \
   dtwasat.cc \
   dualize.cc \
   emptiness.cc \
+  genem.cc \
   gfguarantee.cc \
   gv04.cc \
   hoa.cc \

spot/twaalgos/genem.cc

@@ -0,0 +1,222 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "config.h"
+#include <spot/twaalgos/genem.hh>
+#include <spot/twaalgos/cleanacc.hh>
+
+namespace spot
+{
+  namespace
+  {
+    class temporary_acc_set
+    {
+      twa_graph_ptr aut_;
+      acc_cond old_acc_;
+
+    public:
+      temporary_acc_set(const const_twa_graph_ptr& aut,
+                        acc_cond new_acc)
+        : aut_(std::const_pointer_cast<twa_graph>(aut)),
+          old_acc_(aut->acc())
+      {
+        set(new_acc);
+      }
+
+      void set(acc_cond new_acc)
+      {
+        aut_->set_acceptance(new_acc);
+      }
+
+      ~temporary_acc_set()
+      {
+        aut_->set_acceptance(old_acc_);
+      }
+    };
+
+    bool scc_split_check(const scc_info& si, unsigned scc,
+                         acc_cond::mark_t tocut,
+                         bool (*ec_scc)(const scc_info& si,
+                                        unsigned scc,
+                                        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 = acc.remove(si.common_sets_of(scc), false);
+      temporary_acc_set tmp(si.get_aut(), acc);
+      scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data,
+                        scc_info_options::STOP_ON_ACC);
+      if (upper_si.one_accepting_scc() >= 0)
+        return false;
+      if (!acc.uses_fin_acceptance())
+        return true;
+      unsigned nscc = upper_si.scc_count();
+      for (unsigned scc = 0; scc < nscc; ++scc)
+        if (!ec_scc(upper_si, scc, tocut))
+          return false;
+      return true;
+    }
+
+    template <bool deal_with_disjunct>
+    bool generic_emptiness_check_for_scc_nocopy(const scc_info& si,
+                                                unsigned scc,
+                                                acc_cond::mark_t
+                                                tocut = {})
+    {
+      if (si.is_rejecting_scc(scc))
+        return true;
+      acc_cond::mark_t sets = si.acc_sets_of(scc);
+      auto& autacc = si.get_aut()->acc();
+      acc_cond acc = autacc.restrict_to(sets);
+      acc = acc.remove(si.common_sets_of(scc), false);
+      if (acc.is_f())
+        return true;
+      if (acc.is_t())
+        return false;
+      temporary_acc_set tmp(si.get_aut(), acc);
+      if (acc_cond::mark_t fu = acc.fin_unit())
+        return scc_split_check
+          (si, scc, tocut | fu,
+           generic_emptiness_check_for_scc_nocopy<deal_with_disjunct>);
+
+      if (deal_with_disjunct)
+        {
+          acc_cond::acc_code& code = acc.get_acceptance();
+          assert(!code.empty());
+          auto pos = &code.back();
+          auto start = &code.front();
+          assert(pos - pos->sub.size == start);
+          if (pos->sub.op == acc_cond::acc_op::Or)
+            {
+              do
+                {
+                  --pos;
+                  if (pos->sub.op != acc_cond::acc_op::Inf)
+                    {
+                      acc_cond::acc_code one(pos);
+                      tmp.set(one);
+                      if (si.get_aut()->acc().uses_fin_acceptance())
+                        {
+                          acc_cond::mark_t plus = {};
+                          if (acc_cond::mark_t fu = one.fin_unit())
+                            plus = fu;
+                          if (!scc_split_check
+                              (si, scc, tocut | plus,
+                               generic_emptiness_check_for_scc_nocopy
+                               <deal_with_disjunct>))
+                            return false;
+                        }
+                    }
+                  pos -= pos->sub.size;
+                }
+              while (pos > start);
+              return true;
+            }
+          if (pos->sub.op == acc_cond::acc_op::Fin)
+            {
+              tmp.set(acc_cond::acc_code());
+              for (unsigned d: pos[-1].mark.sets())
+                if (!scc_split_check
+                    (si, scc,
+                     tocut | acc_cond::mark_t({d}),
+                     generic_emptiness_check_for_scc_nocopy
+                     <deal_with_disjunct>))
+                  return false;
+              return true;
+            }
+        }
+
+      int fo = acc.fin_one();
+      assert(fo >= 0);
+      // Try to accept when Fin(fo) == true
+      if (!scc_split_check
+          (si, scc, tocut | acc_cond::mark_t({(unsigned) fo}),
+           generic_emptiness_check_for_scc_nocopy
+           <deal_with_disjunct>))
+        return false;
+      // Try to accept when Fin(fo) == false
+      tmp.set(acc.remove({(unsigned) fo}, false));
+      return generic_emptiness_check_for_scc_nocopy
+        <deal_with_disjunct>(si, scc, tocut);
+      return true;
+    }
+
+    template <bool deal_with_disjunct>
+    bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut)
+    {
+      cleanup_acceptance_here(aut, false);
+      auto& aut_acc = aut->acc();
+      if (aut_acc.is_f())
+        return true;
+      if (!aut->acc().uses_fin_acceptance())
+        return aut->is_empty();
+
+      scc_info si(aut, scc_info_options::STOP_ON_ACC
+                  | scc_info_options::TRACK_STATES);
+      if (si.one_accepting_scc() >= 0)
+        return false;
+
+      unsigned nscc = si.scc_count();
+      for (unsigned scc = 0; scc < nscc; ++scc)
+        if (!generic_emptiness_check_for_scc_nocopy
+            <deal_with_disjunct>(si, scc))
+          return false;
+      return true;
+    }
+  }
+
+  bool generic_emptiness_check(const const_twa_graph_ptr& aut)
+  {
+    auto aut_ = std::const_pointer_cast<twa_graph>(aut);
+    acc_cond old = aut_->acc();
+    bool res = generic_emptiness_check_main_nocopy<true>(aut_);
+    aut_->set_acceptance(old);
+    return res;
+  }
+
+  bool generic_emptiness_check_for_scc(const scc_info& si,
+                                       unsigned scc)
+  {
+    return generic_emptiness_check_for_scc_nocopy<true>(si, scc);
+  }
+}

spot/twaalgos/genem.hh

@@ -0,0 +1,35 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/twaalgos/sccinfo.hh>
+
+namespace spot
+{
+  /// \ingroup emptiness_check_algorithms
+  /// \brief Emptiness check of on automaton, for any acceptance condition.
+  SPOT_API bool
+  generic_emptiness_check(const const_twa_graph_ptr& aut);
+
+  /// \ingroup emptiness_check_algorithms
+  /// \brief Emptiness check of one SCC, for any acceptance condition.
+  SPOT_API bool
+  generic_emptiness_check_for_scc(const scc_info& si, unsigned scc);
+}