is_unambiguous: fix false negatives again

Reported by Simon Jantsch and David Müller.

* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite wihtout assuming
that the product of two accepting SCCs is accepting,  Also use
the result of is_accepting_scc()/is_rejectng_scc() when available.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Make it
possible to check the acceptance of a unique SCC.
* tests/core/unambig.test: Add more test cases.

spot/twaalgos/isunamb.cc

@@ -80,36 +80,48 @@ namespace spot
     assert(sprod);
 
     // What follow is a way to compute whether an SCC is useless in
-    // prod, without having to call
+    // prod, avoiding scc_info::determine_unknown_acceptance() on the
-    // scc_map::determine_unknown_acceptance() on scc_map(prod),
+    // product, because prod may have a large acceptance condition.
-    // 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(psc);
     for (unsigned n = 0; n < psc; ++n)
       {
-        unsigned one_state = sccmap_prod.states_of(n).front();
+        // If scc_info could determinate acceptance easily, use it.
-        bool accepting =
+        // An accepting SCC is useful.
-          v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
+        bool uf = sccmap_prod.is_accepting_scc(n);
-        if (accepting && !sccmap_prod.is_trivial(n))
+        // If any of the successor is useful, this SCC is useful as
+        // well regardless of its acceptance.
+        if (!uf)
+          for (unsigned j: sccmap_prod.succ(n))
+            if (useful[j])
+              {
+                uf = true;
+                break;
+              }
+        if (uf)
           {
             useful[n] = true;
             continue;
           }
-        bool uf = false;
+        if (!sccmap_prod.is_rejecting_scc(n))
-        for (unsigned j: sccmap_prod.succ(n))
+          {
-          if (useful[j])
+            // This SCC has no useful successors, but we still do not
-            {
+            // known if it is accepting.
-              uf = true;
+            //
-              break;
+            // A necessary condition for the SCC to be accepting is that
-            }
+            // its it the combination of two accepting SCCs.  So let's
-        useful[n] = uf;
+            // test that first.
+            unsigned one_state = sccmap_prod.states_of(n).front();
+            bool accepting =
+              v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
+            if (!accepting)
+              continue;
+            // We can't avoid it any more, we have to check the
+            // acceptance if the SCC.
+            std::vector<bool> k;
+            useful[n] = !sccmap_prod.check_scc_emptiness(n, &k);
+          }
       }
 
     // Now we just have to count the number of states && edges that

spot/twaalgos/sccinfo.cc

@@ -423,6 +423,20 @@ namespace spot
     return support;
   }
 
+  bool scc_info::check_scc_emptiness(unsigned n, std::vector<bool>* k)
+  {
+    if (SPOT_UNLIKELY(!aut_->is_existential()))
+      throw std::runtime_error("scc_info::check_scc_emptiness() "
+                               "does not support alternating automata");
+    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
+      report_need_track_states();
+    k->assign(aut_->num_states(), false);
+    auto& node = node_[n];
+    for (auto i: node.states_)
+      (*k)[i] = true;
+    return mask_keep_accessible_states(aut_, *k, node.one_state_)->is_empty();
+  }
+
   void scc_info::determine_unknown_acceptance()
   {
     std::vector<bool> k;
@@ -438,15 +452,8 @@ namespace spot
               throw std::runtime_error(
                   "scc_info::determine_unknown_acceptance() "
                   "does not support alternating automata");
-            if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
-              report_need_track_states();
             auto& node = node_[s];
-            if (k.empty())
+            if (check_scc_emptiness(s, &k))
-              k.resize(aut_->num_states());
-            for (auto i: node.states_)
-              k[i] = true;
-            if (mask_keep_accessible_states(aut_, k, node.one_state_)
-                ->is_empty())
               node.rejecting_ = true;
             else
               node.accepting_ = true;

spot/twaalgos/sccinfo.hh

@@ -583,10 +583,20 @@ namespace spot
       return node(scc).is_rejecting();
     }
 
-    // Study the SCC that are currently reported neither as accepting
+    /// \brief Study the SCCs that are currently reported neither as
-    // nor rejecting because of the presence of Fin sets
+    /// accepting nor as rejecting because of the presence of Fin sets
+    ///
+    /// This simply calls check_scc_emptiness() on undeterminate SCCs.
     void determine_unknown_acceptance();
 
+    /// \brief Recompute whether an SCC is accepting or not.
+    ///
+    /// This is an internal function of
+    /// determine_unknown_acceptance().  The Boolean vector k will be
+    /// used by the method to mark the state that belong to the SCC.
+    /// It can be shared between multiple calls.
+    bool check_scc_emptiness(unsigned n, std::vector<bool>* k);
+
     bool is_useful_scc(unsigned scc) const
     {
       if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))

tests/core/unambig.test

@@ -285,6 +285,7 @@ EOF
 run 1 autfilt -q --is-unambiguous smaller.hoa
 
 # These automata come from Simon Jantsch and David Müller.
+# They exposed bugs in the optimized version of our unambiguous check.
 cat >sjdb.hoa <<EOF
 HOA: v1
 name: "G(!a | !b) & (Ga | G(b | XGb))"
@@ -332,6 +333,51 @@ State: 3
 State: 4 {0}
 [!0&1] 4
 --END--
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0 "((G (! (p0))) R ((! (p1)) | (G (! (p0)))))"
+[!0] 1 {0}
+[0&!1] 0 {0}
+[!0&!1] 2
+State: 1 "(G (! (p0)))"
+[!0] 1 {0}
+State: 2 "((G (! (p0))) R ((! (p1)) | (G (! (p0))))) & (F (p0))"
+[0&!1] 0 {0}
+[!0&!1] 2
+--END--
 EOF
 
-test 2 = `autfilt -c --is-unambiguous sjdb.hoa`
+test 3 = `autfilt -c --is-unambiguous sjdb.hoa`
+
+# This automaton requires emptiness of SCC with Fin-acceptance.
+cat >ambig.hoa<<EOF
+HOA: v1
+States: 5
+Start: 4
+AP: 2 "p0" "p1"
+Acceptance: 4 Fin(0) & Fin(1)
+--BODY--
+State: 0
+[0] 0 {0}
+[!0] 1
+State: 1
+[1] 1 {1}
+[!1] 0
+State: 2
+[0] 2 {0}
+[!0] 3
+State: 3
+[1] 3 {1}
+[!1] 2
+State: 4
+[0] 0
+[0] 2
+--END--
+EOF
+test 0 = `autfilt -c --is-unambiguous ambig.hoa`