powerset: deal with accepting sinks more effectively

Part of #444.

* spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh: Implement
accepting sink handling.
* spot/twaalgos/minimize.cc (minimize_wdba): Pass sinks to
tgba_powerset.
* spot/misc/bitvect.hh: Add an interesects method.
* tests/core/ltl2tgba2.test: More tests.
* NEWS: Mention this new feature.

NEWS

@@ -141,6 +141,10 @@ New in spot 2.9.5.dev (not yet released)
                      automata-based implication checks for formula
                      simplifications.  Defaults to 64.
 
+  - tgba_powerset() now takes an extra optional argument to specify a
+    list of accepting sinks states if some are known.  Doing so can
+    cut the size of the powerset automaton by 2^|sinks| in favorable
+    cases.
 
   Python:
 

spot/misc/bitvect.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -255,6 +255,16 @@ namespace spot
       return *this;
     }
 
+    bool intersects(const bitvect& other)
+    {
+      SPOT_ASSERT(other.size_ <= size_);
+      unsigned m = std::min(other.block_count_, block_count_);
+      for (size_t i = 0; i < m; ++i)
+        if (storage_[i] & other.storage_[i])
+          return true;
+      return false;
+    }
+
     bitvect& operator^=(const bitvect& other)
     {
       SPOT_ASSERT(other.size_ <= size_);

spot/twaalgos/minimize.cc

@@ -393,7 +393,25 @@ namespace spot
         }
       else
         {
-          det_a = tgba_powerset(a, aborter);
+          // Find any accepting sink state, to speed up the
+          // determinization by merging all states containing a sink
+          // state.
+          //
+          // We only as consider as "accepting sink" any state
+          // that have an accepting self-loop labeled by true.
+          std::vector<unsigned> acc_sinks;
+          unsigned ns = a->num_states();
+          for (unsigned n = 0; n < ns; ++n)
+            {
+              for (auto& e: a->out(n))
+                if (e.dst == n && e.cond == bddtrue
+                    && a->acc().accepting(e.acc))
+                  {
+                    acc_sinks.push_back(n);
+                    break;
+                  }
+            }
+          det_a = tgba_powerset(a, aborter, &acc_sinks);
           if (!det_a)
             return nullptr;
         }

spot/twaalgos/powerset.cc

@@ -82,7 +82,8 @@ namespace spot
 
   twa_graph_ptr
   tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge,
-                const output_aborter* aborter)
+                const output_aborter* aborter,
+                std::vector<unsigned>* accepting_sinks)
   {
     unsigned ns = aut->num_states();
     unsigned nap = aut->ap().size();
@@ -207,6 +208,23 @@ namespace spot
     auto res = make_twa_graph(aut->get_dict());
     res->copy_ap_of(aut);
 
+    bitvect* acc_sinks = nullptr;
+    if (accepting_sinks)
+      {
+        acc_sinks = make_bitvect(ns);
+        for (unsigned s: *accepting_sinks)
+          acc_sinks->set(s);
+        toclean.emplace_back(acc_sinks);
+
+        // The accepting sink is the first registered state by
+        // convention.
+        power_state ps = bv_to_ps(acc_sinks);
+        unsigned num = res->new_state();
+        seen[acc_sinks] = num;
+        assert(pm.map_.size() == num);
+        pm.map_.emplace_back(std::move(ps));
+      }
+
     {
       unsigned init_num = aut->get_init_state_number();
       auto bvi = make_bitvect(ns);
@@ -239,6 +257,8 @@ namespace spot
             auto dst = &om->at(c);
             if (dst->is_fully_clear())
               continue;
+            if (acc_sinks && dst->intersects(*acc_sinks))
+              *dst = *acc_sinks;
             auto i = seen.find(dst);
             unsigned dst_num;
             if (i != seen.end())
@@ -274,10 +294,11 @@ namespace spot
 
   twa_graph_ptr
   tgba_powerset(const const_twa_graph_ptr& aut,
-                const output_aborter* aborter)
+                const output_aborter* aborter,
+                std::vector<unsigned>* accepting_sinks)
   {
     power_map pm;
-    return tgba_powerset(aut, pm, true, aborter);
+    return tgba_powerset(aut, pm, true, aborter, accepting_sinks);
   }
 
 

spot/twaalgos/powerset.hh

@@ -94,14 +94,21 @@ namespace spot
   ///
   /// If ab \a aborter is given, abort the construction whenever it
   /// would build an automaton that is too large, and return nullptr.
+  ///
+  /// If a vector of accepting sinks is given, all power-state that
+  /// contains any accepting sink will be merged into a single state
+  /// with number 0.
+  ///
   //@{
   SPOT_API twa_graph_ptr
   tgba_powerset(const const_twa_graph_ptr& aut,
                 power_map& pm, bool merge = true,
-                const output_aborter* aborter = nullptr);
+                const output_aborter* aborter = nullptr,
+                std::vector<unsigned>* accepting_sinks = nullptr);
   SPOT_API twa_graph_ptr
   tgba_powerset(const const_twa_graph_ptr& aut,
-                const output_aborter* aborter = nullptr);
+                const output_aborter* aborter = nullptr,
+                std::vector<unsigned>* accepting_sinks = nullptr);
   //@}
 
 

tests/core/ltl2tgba2.test

@@ -477,4 +477,11 @@ test 28 = `ltl2tgba -D -G -S --stats=%s "$f"`
 
 # Issue #443.  This used to be too long.
 f='(!(G({(a)} |=> {(b)[*32]})))'
-test 34 = `ltl2tgba -B --stats=%s "$f"`
+test 34,0 = `ltl2tgba -B --stats=%s,%d "$f"`
+# Issue #444.  Because WDBA-minimization disables itself for large
+# automata, the output is only deterministic up to a certain point,
+# and the goal is to raise that point.
+f='(!(G({(a)} |=> {(b)[*9]})))'
+test 11,1 = `ltl2tgba -B --stats=%s,%d "$f"`
+f='(!(G({(a)} |=> {(b)[*10]})))'
+test 12,0 = `ltl2tgba -B --stats=%s,%d "$f"`