minimize_wdba: fix handling of input with useless SCCs

* spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
terminal SCCs that are incomplete, as if they had a non-accepting
sink as successor.
* spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
(is_terminal_automaton): Add an option to ignore trivial SCC as we did
before, since it matters for deciding membership to the guarantee
class.
(is_safety_mwdba): Rewrite as ...
(is_safety_automaton): ... generalizating to any acceptance, and
ignoring trivial SCCs.
* bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
is_safety_automaton().
* tests/core/hierarchy.test: Add a problematic formula as test-case.
* NEWS: Mention the bug.

NEWS

@@ -46,7 +46,7 @@ New in spot 2.2.2.dev (Not yet released)
     are automata-based and will also match pathological formulas.
 
   * The --format option of ltlfilt/genltl/randltl/ltlgrind learned to
-    print the class of a formula in the temporal hierachy of Manna &
+    print the class of a formula in the temporal hierarchy of Manna &
     Pnueli using %h.  Try to classify the Dwyer & al. patterns with:
       genltl --dac --format='%[vw]h' | sort | uniq -c
 
@@ -130,6 +130,15 @@ New in spot 2.2.2.dev (Not yet released)
   * The new function mp_class(f) returns the class of the formula
     f in the temporal hierarchy of Manna & Pnueli.
 
+Bug fixed:
+
+  * The minimize_wdba() function was not correctly minimizing automata
+    with useless SCCs.  This was not an issue for the LTL translation
+    (where useless SCCs are always removed first), but it was an issue
+    when deciding if a formula was safety or guarantee.  As a
+    consequence, some tricky safety or guarantee properties were only
+    recognized as obligations.
+
 New in spot 2.2.2 (2016-12-16)
 
   Build:

bin/ltlfilt.cc

@@ -734,8 +734,10 @@ namespace
                     }
                   else
                     {
-                      matched &= !guarantee || is_terminal_automaton(min);
+                      spot::scc_info si(min);
-                      matched &= !safety || is_safety_mwdba(min);
+                      matched &= !guarantee
+                        || is_terminal_automaton(min, &si, true);
+                      matched &= !safety || is_safety_automaton(min, &si);
                     }
                 }
               // Recurrence properties are those that can be translated to

python/ajax/spotcgi.in

@@ -1,7 +1,7 @@
 #!@PYTHON@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
+# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
-# Développement de l'Epita (LRDE).
+# Recherche et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -511,8 +511,8 @@ if output_type == 'f':
             automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
             minimized = spot.minimize_obligation(automaton, f)
             if minimized != automaton:
-                g = spot.is_terminal_automaton(minimized)
+                g = spot.is_terminal_automaton(minimized, None, True)
-                s = spot.is_safety_mwdba(minimized)
+                s = spot.is_safety_automaton(minimized)
                 if s and not f.is_syntactic_safety():
                     unbufprint('<li>pathologic safety</li>')
                 if g and not f.is_syntactic_guarantee():

spot/tl/hierarchy.cc

@@ -66,8 +66,11 @@ namespace spot
     auto min = minimize_obligation(aut, f);
     if (aut != min) // An obligation.
       {
-        bool g = is_terminal_automaton(min);
+        scc_info si(min);
-        bool s = is_safety_mwdba(min);
+        // The minimba WDBA can have some trivial accepting SCCs
+        // that we should ignore in is_terminal_automaton().
+        bool g = is_terminal_automaton(min, &si, true);
+        bool s = is_safety_automaton(min, &si);
         if (g)
           return s ? 'B' : 'G';
         else

spot/twaalgos/minimize.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -520,7 +520,7 @@ namespace spot
       // (i.e., it is not the start of any accepting word).
 
       scc_info sm(det_a);
-      sm.determine_unknown_acceptance();
+
       unsigned scc_count = sm.scc_count();
       // SCC that have been marked as useless.
       std::vector<bool> useless(scc_count);
@@ -539,18 +539,13 @@ namespace spot
           bool transient = sm.is_trivial(m);
           auto& succ = sm.succ(m);
 
-          if (transient && succ.empty())
+          // Compute the minimum color l of the successors.  Also SCCs
-            {
+          // are useless if all their successor are useless.  Note
-              // A trivial SCC without successor is useless.
+          // that Löding uses k-1 as level for non-final SCCs without
-              useless[m] = true;
+          // successors but that seems bogus: using k+1 will make sure
-              d[m] = k - 1;
+          // that a non-final SCCs without successor (i.e., a useless
-              continue;
+          // SCC) will be ignored in the computation of the level.
-            }
+          unsigned l = k + 1;
-
-          // Compute the minimum color l of the successors.
-          // Also SCCs are useless if all their successor are
-          // useless.
-          unsigned l = k;
           for (unsigned j: succ)
             {
               is_useless &= useless[j];
@@ -575,6 +570,8 @@ namespace spot
                 }
               else
                 {
+                  if (succ.empty())
+                    is_useless = true;
                   d[m] = (l - 1) | 1; // largest odd number inferior or equal
                 }
             }

spot/twaalgos/strength.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
-// Recherche et Développement de l'Epita (LRDE)
+// de Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -28,7 +28,8 @@ namespace spot
   namespace
   {
     template <bool terminal, bool inweak = false, bool set = false>
-    bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si)
+    bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si,
+                           bool ignore_trivial_term = false)
     {
       // Create an scc_info if the user did not give one to us.
       bool need_si = !si;
@@ -89,7 +90,7 @@ namespace spot
       // A terminal automaton should accept any word that as a prefix
       // leading to an accepting edge.  In other words, we cannot have
       // an accepting edge that goes into a rejecting SCC.
-      if (terminal && is_term)
+      if (terminal && is_term && !ignore_trivial_term)
         for (auto& e: aut->edges())
           if (si->is_rejecting_scc(si->scc_of(e.dst))
               && aut->acc().accepting(e.acc))
@@ -103,7 +104,12 @@ namespace spot
       if (set)
         {
           if (terminal)
+            {
+              if (!ignore_trivial_term)
                 aut->prop_terminal(is_term && is_weak);
+              else if (is_term && is_weak)
+                aut->prop_terminal(true);
+            }
           aut->prop_weak(is_weak);
           aut->prop_very_weak(is_single_state_scc && is_weak);
           if (inweak)
@@ -116,13 +122,15 @@ namespace spot
   }
 
   bool
-  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si,
+                        bool ignore_trivial_term)
   {
     trival v = aut->prop_terminal();
     if (v.is_known())
       return v.is_true();
     bool res =
-      is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si);
+      is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si,
+                              ignore_trivial_term);
     std::const_pointer_cast<twa_graph>(aut)->prop_terminal(res);
     return res;
   }
@@ -170,16 +178,27 @@ namespace spot
       is_type_automaton<true, true, true>(aut, si);
   }
 
-  bool is_safety_mwdba(const const_twa_graph_ptr& aut)
+  bool is_safety_automaton(const const_twa_graph_ptr& aut, scc_info* si)
   {
-    if (!(aut->acc().is_buchi() || aut->acc().is_all()))
+    if (aut->acc().is_t())
-      throw std::runtime_error
-        ("is_safety_mwdba() should be called on a Buchi automaton");
-
-    for (auto& t: aut->edges())
-      if (!aut->acc().accepting(t.acc))
-        return false;
       return true;
+
+    bool need_si = !si;
+    if (need_si)
+      si = new scc_info(aut);
+
+    bool res = true;
+    unsigned scount = si->scc_count();
+    for (unsigned scc = 0; scc < scount; ++scc)
+      if (!si->is_trivial(scc) && si->is_rejecting_scc(scc))
+        {
+          res = false;
+          break;
+        }
+
+    if (need_si)
+      delete si;
+    return res;
   }
 
 

spot/twaalgos/strength.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
-// Recherche et Développement de l'Epita (LRDE)
+// de Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -29,6 +29,9 @@ namespace spot
   /// are complete, and no accepting transitions lead to a
   /// non-accepting SCC.
   ///
+  /// If ignore_trivial_scc is set, accepting transitions from trivial
+  /// SCCs are ignored.
+  ///
   /// This property guarantees that a word is accepted if it has some
   /// prefix that reaches an accepting transition.
   ///
@@ -41,8 +44,8 @@ namespace spot
   /// the prop_terminal() property of the automaton as a side-effect,
   /// so further calls will return in constant-time.
   SPOT_API bool
-  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr,
-
+                        bool ignore_trivial_scc = false);
 
   /// \brief Check whether an automaton is weak.
   ///
@@ -95,16 +98,22 @@ namespace spot
   is_inherently_weak_automaton(const const_twa_graph_ptr& aut,
                                scc_info* sm = nullptr);
 
-  /// \brief Check whether a minimized WDBA represents a safety
+  /// \brief Check whether an automaton is a safety automaton.
-  /// property.
+  ///
+  /// A safety automaton has only accepting SCCs (or trivial
+  /// SCCs).
   ///
   /// A minimized WDBA (as returned by a successful run of
-  /// minimize_obligation()) represent safety property if it contains
+  /// minimize_obligation()) represent safety property if it is a
-  /// only accepting transitions.
+  /// safety automaton.
   ///
   /// \param aut the automaton to check
+  ///
+  /// \param sm an scc_info object for the automaton if available (it
+  /// will be built otherwise).
   SPOT_API bool
-  is_safety_mwdba(const const_twa_graph_ptr& aut);
+  is_safety_automaton(const const_twa_graph_ptr& aut,
+                      scc_info* sm = nullptr);
 
   /// \brief Check whether an automaton is weak or terminal.
   ///

tests/core/hierarchy.test

@@ -62,3 +62,7 @@ cat >expected <<EOF
 37 safety obligation persistence recurrence reactivity
 EOF
 diff out expected
+
+
+test B = `ltlfilt --format=%h -f '(Gb R (b xor Gb)) W (a W Xa)'`
+ltlfilt -q --safety --guarantee -f '(Gb R (b xor Gb)) W (a W Xa)'

tests/core/ikwiad.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2007-2016 Laboratoire de Recherche et Développement
+// Copyright (C) 2007-2017 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -1373,8 +1373,9 @@ checked_main(int argc, char** argv)
                 }
               else
                 {
-                  bool g = is_terminal_automaton(ensure_digraph(a));
+                  bool g = is_terminal_automaton(ensure_digraph(a),
-                  bool s = is_safety_mwdba(ensure_digraph(a));
+                                                 nullptr, true);
+                  bool s = is_safety_automaton(ensure_digraph(a));
                   if (g && !s)
                     {
                       std::cout << "this is a guarantee property (hence, "