is_unambiguous: rewrite more efficiently

Avoid calling scc_info::determine_unknown_acceptance on the product, as
suggested in #188.

* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite.
* tests/core/unambig.test: Add the automaton from #188.
* NEWS: Mention the improved function.
* spot/twaalgos/mask.cc,
spot/twaalgos/mask.hh (mask_keep_accessible_states): New function.

NEWS

@@ -1,6 +1,8 @@
 New in spot 2.1.2.dev (not yet released)
 
-  Nothing yet.
+  Library:
+
+  * is_unambiguous() was rewritten in a more efficient way.
 
 New in spot 2.1.2 (2016-10-14)
 

spot/twaalgos/isunamb.cc

@@ -19,25 +19,114 @@
 
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/product.hh>
-#include <spot/twaalgos/sccfilter.hh>
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/mask.hh>
 #include <set>
 #include <list>
 
 namespace spot
 {
+  // Conceptually, aut is unambiguous if the useful part of aut has
+  // the same size as the useful part of aut*aut.
+  //
+  // However calling scc_info::determine_unknown_acceptance(), which
+  // is needed to decide which states are actually useless, is costly.
+  // We do it on aut, but we avoid doing it on prod.
+  //
+  // This optimization, which requires much more code than what
+  // we used to have, was motivated by issue #188.
   bool is_unambiguous(const const_twa_graph_ptr& aut)
   {
     trival u = aut->prop_unambiguous();
     if (u.is_known())
       return u.is_true();
-
+    if (aut->num_edges() == 0)
-    auto clean_a = scc_filter_states(aut);
-    if (clean_a->num_edges() == 0)
       return true;
-    auto prod = product(clean_a, clean_a);
+
-    auto clean_p = scc_filter_states(prod);
+    scc_info sccmap(aut);
-    return (clean_a->num_states() == clean_p->num_states()
+    sccmap.determine_unknown_acceptance();
-            && clean_a->num_edges() == clean_p->num_edges());
+    unsigned autsz = aut->num_states();
+    std::vector<bool> v;
+    v.reserve(autsz);
+    bool all_useful = true;
+    for (unsigned n = 0; n < autsz; ++n)
+      {
+        bool useful = sccmap.is_useful_state(n);
+        all_useful &= useful;
+        v.push_back(useful);
+      }
+
+    // If the input automaton comes from any /decent/ source, it is
+    // unlikely that it has some useless states, so do not bother too
+    // much optimizing this case.
+    if (!all_useful)
+      return is_unambiguous(mask_keep_accessible_states
+                            (aut, v, aut->get_init_state_number()));
+
+    // Reuse v to remember which states are in an accepting SCC.
+    for (unsigned n = 0; n < autsz; ++n)
+      v[n] = sccmap.is_accepting_scc(sccmap.scc_of(n));
+
+    auto prod = product(aut, aut);
+    auto sprod =
+      prod->get_named_prop<std::vector<std::pair<unsigned,
+                                                 unsigned>>>("product-states");
+    assert(sprod);
+
+    // What follow is a way to compute whether an SCC is useless in
+    // prod, without having to call
+    // scc_map::determine_unknown_acceptance() on scc_map(prod),
+    // because prod has potentially a large acceptance condition.
+    //
+    // We know that an SCC of the product is accepting iff it is the
+    // combination of two accepting SCCs of the original automaton.
+    //
+    // So we can just compute the acceptance of each SCC this way, and
+    // derive the usefulness from that.
+    scc_info sccmap_prod(prod);
+    unsigned psc = sccmap_prod.scc_count();
+    std::vector<bool> useful;
+    useful.reserve(psc);
+    for (unsigned n = 0; n < psc; ++n)
+      {
+        unsigned one_state = sccmap_prod.states_of(n).front();
+        bool accepting =
+          v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
+        if (accepting)
+          {
+            useful[n] = true;
+            continue;
+          }
+        bool uf = false;
+        for (unsigned j: sccmap_prod.succ(n))
+          if (useful[j])
+            {
+              uf = true;
+              break;
+            }
+        useful[n] = uf;
+      }
+
+    // Now we just have to count the number of states && edges that
+    // belong to the useful part of the automaton.
+    unsigned np = prod->num_states();
+    v.resize(np);
+    unsigned useful_states = 0;
+    for (unsigned n = 0; n < np; ++n)
+      {
+        bool uf = useful[sccmap_prod.scc_of(n)];
+        v[n] = uf;
+        useful_states += uf;
+      }
+
+    if (aut->num_states() != useful_states)
+      return false;
+
+    unsigned useful_edges = 0;
+    for (const auto& e: prod->edges())
+      useful_edges += v[e.src] && v[e.dst];
+
+    return aut->num_edges() == useful_edges;
   }
 
   bool check_unambiguous(const twa_graph_ptr& aut)

spot/twaalgos/mask.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -67,4 +67,26 @@ namespace spot
     return res;
   }
 
+  twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
+                                            std::vector<bool>& to_keep,
+                                            unsigned int init)
+  {
+    if (to_keep.size() < in->num_states())
+      to_keep.resize(in->num_states(), false);
+
+    auto res = make_twa_graph(in->get_dict());
+    res->copy_ap_of(in);
+    res->prop_copy(in, { true, true, true, false });
+    res->copy_acceptance_of(in);
+    transform_accessible(in, res, [&](unsigned src,
+                                      bdd& cond,
+                                      acc_cond::mark_t&,
+                                      unsigned dst)
+                   {
+                     if (!to_keep[src] || !to_keep[dst])
+                       cond = bddfalse;
+                   }, init);
+    return res;
+  }
+
 }

spot/twaalgos/mask.hh

@@ -140,10 +140,29 @@ namespace spot
 
   /// \brief Keep only the states as specified by \a to_keep.
   ///
-  /// Each index in the vector \a to_keep specifies wether or not to keep that
+  /// Each index in the vector \a to_keep specifies wether or not to
-  /// state.  The initial state will be set to \a init.
+  /// keep the transition that exit this state.  The initial state
+  /// will be set to \a init.
+  ///
+  /// Note that the number of states in the result automaton is the
+  /// same as in the input: only transitions have been removed.
+  ///
+  /// \see mask_keep_accessible_states
   SPOT_API
   twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in,
                                  std::vector<bool>& to_keep,
                                  unsigned int init);
+
+  /// \brief Keep only the states specified by \a to_keep that are accessible.
+  ///
+  /// Each index in the vector \a to_keep specifies wether or not to
+  /// keep the transition that exit this state.  The initial state
+  /// will be set to \a init.  Only states that are accessible from \a
+  /// init via states in \a to_keep will be preserved.
+  ///
+  /// \see mask_keep_states
+  SPOT_API
+  twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
+                                            std::vector<bool>& to_keep,
+                                            unsigned int init);
 }

tests/core/unambig.test

@@ -244,3 +244,47 @@ cat >expected <<EOF
 1
 EOF
 diff expected ltlcross.res
+
+
+# This automaton was supplied by František Blahoudek, and is discussed
+# in #188.  Our initial implementation of is_unambiguous() on this
+# automaton used to take 38s, while the new version takes 0.2s.  Using
+# valgrind on this is a way to ensure that the test is procedure
+# enough: it would have been too long on the previous version.
+
+cat >smaller.hoa<<EOF
+HOA: v1
+States: 7
+Start: 1
+AP: 2 "a" "b"
+Acceptance: 12 (Inf(11) | Fin(5)) & (Inf(10) | Fin(4)) & (Inf(9) |
+  Fin(3)) & (Inf(8) | Fin(2)) & (Inf(7) | Fin(1)) & (Inf(6) | Fin(0))
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 0
+State: 1
+[!0] 1 {0}
+[0] 2
+[0&1] 3
+State: 2
+[t] 2 {1}
+[1] 3
+State: 3
+[t] 3 {2}
+[!1] 4
+State: 4
+[t] 4 {3}
+[1] 5
+State: 5
+[t] 5 {4}
+[!1] 6
+State: 6
+[1] 0 {11}
+[!1] 6 {5}
+--END--
+EOF
+
+run 1 autfilt -q --is-unambiguous smaller.hoa
+
+true