autfilt: better handling of chain of products with -B

Fixes #348, reported by Jeroen Meijer.

* bin/autfilt.cc: If -B is used with many --product,
degeneralize intermediate products as needed.
* NEWS: Mention the change.
* tests/core/prodchain.test: New file.
* tests/Makefile.am: Add it.
* spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of
overflow.
* tests/core/acc.cc: Adjust.

NEWS

@@ -15,6 +15,13 @@ New in spot 2.5.3.dev  (not yet released)
   - ltlcross, ltldo, and autcross learned shorthands to call
     delag, ltl2dra, ltl2dgra, and nba2dpa.
 
+  - When autfilt is asked to build a Büchi automaton from
+    of a chain of many products, as in
+    "autfilt -B --product 1.hoa ... --product n.hoa in.hoa"
+    then it will automatically degeneralize the intermediate
+    product to avoid exceeding the number of supported
+    acceptance sets.
+
   Library:
 
   - You can now specify to Spot the number of acceptance marks you

bin/autfilt.cc

@@ -50,6 +50,7 @@
 #include <spot/twaalgos/cobuchi.hh>
 #include <spot/twaalgos/cleanacc.hh>
 #include <spot/twaalgos/contains.hh>
+#include <spot/twaalgos/degen.hh>
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/gtec/gtec.hh>
@@ -634,6 +635,40 @@ ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
   return p.run(aut);
 }
 
+static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut)
+{
+  spot::postprocessor p;
+  p.set_type(spot::postprocessor::TGBA);
+  p.set_pref(spot::postprocessor::Any);
+  p.set_level(spot::postprocessor::Low);
+  return spot::degeneralize_tba(p.run(aut));
+
+}
+
+static spot::twa_graph_ptr
+product(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
+{
+  if ((type == spot::postprocessor::BA)
+      && (left->num_sets() + right->num_sets() > SPOT_NB_ACC))
+    {
+      left = ensure_tba(left);
+      right = ensure_tba(right);
+    }
+  return spot::product(left, right);
+}
+
+static spot::twa_graph_ptr
+product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
+{
+  if ((type == spot::postprocessor::BA)
+      && (left->num_sets() + right->num_sets() > SPOT_NB_ACC))
+    {
+      left = ensure_tba(left);
+      right = ensure_tba(right);
+    }
+  return spot::product_or(left, right);
+}
+
 static int
 parse_opt(int key, char* arg, struct argp_state*)
 {
@@ -947,7 +982,7 @@ parse_opt(int key, char* arg, struct argp_state*)
         if (!opt->product_and)
           opt->product_and = std::move(a);
         else
-          opt->product_and = spot::product(std::move(opt->product_and),
+          opt->product_and = ::product(std::move(opt->product_and),
                                        std::move(a));
       }
       break;
@@ -957,7 +992,7 @@ parse_opt(int key, char* arg, struct argp_state*)
         if (!opt->product_or)
           opt->product_or = std::move(a);
         else
-          opt->product_or = spot::product_or(std::move(opt->product_or),
+          opt->product_or = ::product_or(std::move(opt->product_or),
                                          std::move(a));
       }
       break;
@@ -1410,9 +1445,9 @@ namespace
         aut->purge_unreachable_states();
 
       if (opt->product_and)
-        aut = spot::product(std::move(aut), opt->product_and);
+        aut = ::product(std::move(aut), opt->product_and);
       if (opt->product_or)
-        aut = spot::product_or(std::move(aut), opt->product_or);
+        aut = ::product_or(std::move(aut), opt->product_or);
 
       if (opt->sum_or)
         aut = spot::sum(std::move(aut), opt->sum_or);

spot/twa/acc.cc

@@ -32,6 +32,14 @@
 
 namespace spot
 {
+  void acc_cond::report_too_many_sets()
+  {
+#define STR(x) #x
+#define VALUESTR(x) STR(x)
+    throw std::runtime_error("Too many acceptance sets used.  "
+                             "The limit is " VALUESTR(SPOT_NB_ACC) ".");
+  }
+
   std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m)
   {
     auto a = m;

spot/twa/acc.hh

@@ -46,6 +46,11 @@ namespace spot
 
   class SPOT_API acc_cond
   {
+
+#ifndef SWIG
+  private:
+      [[noreturn]] static void report_too_many_sets();
+#endif
   public:
     struct mark_t : public internal::_32acc<SPOT_NB_ACC == 8*sizeof(unsigned)>
     {
@@ -213,26 +218,54 @@ namespace spot
       }
 
       mark_t operator<<(unsigned i) const
+      {
+        try
           {
             return id << i;
           }
+        catch (const std::runtime_error& e)
+          {
+            report_too_many_sets();
+          }
+      }
 
       mark_t& operator<<=(unsigned i)
+      {
+        try
           {
             id <<= i;
             return *this;
           }
+        catch (const std::runtime_error& e)
+          {
+            report_too_many_sets();
+          }
+      }
 
       mark_t operator>>(unsigned i) const
+      {
+        try
           {
             return id >> i;
           }
+        catch (const std::runtime_error& e)
+          {
+            report_too_many_sets();
+          }
+      }
 
       mark_t& operator>>=(unsigned i)
+      {
+        try
           {
             id >>= i;
             return *this;
           }
+        catch (const std::runtime_error& e)
+          {
+            report_too_many_sets();
+          }
+      }
 
       mark_t strip(mark_t y) const
       {
@@ -1229,7 +1262,7 @@ namespace spot
       unsigned j = num_;
       num_ += num;
       if (num_ > SPOT_NB_ACC)
-        throw std::runtime_error("Too many acceptance sets used.");
+        report_too_many_sets();
       all_ = all_sets_();
       return j;
     }

tests/Makefile.am

@@ -229,6 +229,7 @@ TESTS_twa = \
   core/ltldo2.test \
   core/maskacc.test \
   core/maskkeep.test \
+  core/prodchain.test \
   core/prodor.test \
   core/simdet.test \
   core/sim2.test \

tests/core/acc.cc

@@ -189,8 +189,7 @@ int main()
   }
   catch (const std::runtime_error& e)
   {
-    if (std::strcmp(e.what(), "Too many acceptance sets used."))
-      return 1;
+    assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30));
   }
 
   try
@@ -200,8 +199,7 @@ int main()
   }
   catch (const std::runtime_error& e)
   {
-    if (std::strcmp(e.what(), "bit shift overflow is undefined behavior"))
-      return 1;
+    assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30));
   }
 
   try
@@ -211,8 +209,7 @@ int main()
   }
   catch (const std::runtime_error& e)
   {
-    if (std::strcmp(e.what(), "bit shift overflow is undefined behavior"))
-      return 1;
+    assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30));
   }
 
   return 0;

tests/core/prodchain.test

@@ -0,0 +1,49 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2018 Laboratoire de Recherche et Développement
+# 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/>.
+
+. ./defs
+set -e
+
+set x
+shift
+for i in `seq 1 42`; do
+  ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa
+done
+for i in *.hoa; do
+  set x "$@" --product $i
+  shift
+done
+shift
+autfilt "$@" 2> error && exit 1
+grep 'Too many acceptance sets used' error
+autfilt -B "$@" > result
+test "127,253,508,1" = `autfilt --stats=%s,%e,%t,%a result`
+
+set x
+shift
+for i in *.hoa; do
+  set x "$@" --product-or $i
+  shift
+done
+shift
+autfilt "$@" 2> error && exit 1
+grep 'Too many acceptance sets used' error
+autfilt -B "$@" > result
+test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`