introduce is_obligation(f)

This is not optimal yet because it still construct a minimal WDBA
internally, but it's better than the previous way to call
minimize_obligation() since it can avoid constructing the minimized
automaton in a few more cases.

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
is_obligation().
* bin/ltlfilt.cc: Wire it to --obligation.
* spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
needed by the above.
* tests/core/obligation.test: Test it.
* bin/man/spot-x.x, NEWS: Document it.

NEWS

@@ -112,6 +112,11 @@ New in spot 2.4.2.dev (not yet released)
     will work either on f or its negation.
     (see https://spot.lrde.epita.fr/hierarchy.html for details).
 
+  - A new function spot::is_obligation() can be used to test whether a
+    formula is an obligation.  This is used by ltlfilt --obligation,
+    and the algorithm used can be controled by the SPOT_O_CHECK
+    environment variable (see the spot-x(7) man page for details).
+
   - The new function spot::is_colored() checks if an automaton is colored
     (i.e., every transition belongs to exactly one acceptance set)
 

bin/ltlfilt.cc

@@ -732,7 +732,7 @@ namespace
               // Because this is costly, we compute it later, so that we don't
               // have to compute it on formulas that have been discarded for
               // other reasons.
-              if (obligation)
+              if (obligation && (safety || guarantee))
                 {
                   if (!aut)
                     aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
@@ -752,10 +752,10 @@ namespace
                       matched &= !safety || is_safety_automaton(min, &si);
                     }
                 }
-
+              else if (obligation) // just obligation, not safety or guarantee
+                  matched &= is_obligation(f, aut);
               else if (persistence)
                 matched &= spot::is_persistence(f);
-
               else if (recurrence)
                 matched &= spot::is_recurrence(f, aut);
             }

bin/man/spot-x.x

@@ -99,6 +99,23 @@ in third-party tools that output incorrect HOA (e.g., declaring
 the automaton with property "univ-branch" when no universal branching
 is actually used)
 
+.TP
+\fBSPOT_O_CHECK\fR
+Specifies the default algorithm that should be used
+by the \f(CWis_obligation()\fR function.  The value should
+be one of the following:
+.RS
+.IP 1
+Make sure that the formula and its negation are
+realizable by non-deterministic co-Büchi automata.
+.IP 2
+Make sure that the formula and its negation are
+realizable by deterministic Büchi automata.
+.IP 3
+Make sure that the formula is realizable
+by a weak and deterministic Büchi automata.
+.RE
+
 .TP
 \fBSPOT_OOM_ABORT\fR
 If this variable is set, Out-Of-Memory errors will \f(CWabort()\fR the

spot/tl/hierarchy.cc

@@ -35,7 +35,7 @@ namespace spot
   {
     static bool
     cobuchi_realizable(spot::formula f,
-                                 const const_twa_graph_ptr& aut)
+                       const const_twa_graph_ptr& aut)
     {
       twa_graph_ptr cobuchi = nullptr;
       std::vector<acc_cond::rs_pair> pairs;
@@ -135,18 +135,18 @@ namespace spot
       return true;
 
     switch (algo_to_perform(true, aut != nullptr, algo))
-    {
+      {
       case prcheck::PR_via_CoBuchi:
-        return cobuchi_realizable(f,
+        return cobuchi_realizable(f, aut ? aut :
-            aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true));
+                                  ltl_to_tgba_fm(f, make_bdd_dict(), true));
 
       case prcheck::PR_via_Rabin:
-        return detbuchi_realizable(
+        return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f),
-            ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true));
+                                                  make_bdd_dict(), true));
 
       case prcheck::PR_Auto:
         SPOT_UNREACHABLE();
-    }
+      }
 
     SPOT_UNREACHABLE();
   }
@@ -158,22 +158,81 @@ namespace spot
       return true;
 
     switch (algo_to_perform(false, aut != nullptr, algo))
-    {
+      {
       case prcheck::PR_via_CoBuchi:
         return cobuchi_realizable(formula::Not(f),
-            ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true));
+                                  ltl_to_tgba_fm(formula::Not(f),
+                                                 make_bdd_dict(), true));
 
       case prcheck::PR_via_Rabin:
-        return detbuchi_realizable(
+        return detbuchi_realizable(aut ? aut :
-            aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true));
+                                   ltl_to_tgba_fm(f, make_bdd_dict(), true));
 
       case prcheck::PR_Auto:
         SPOT_UNREACHABLE();
-    }
+      }
 
     SPOT_UNREACHABLE();
   }
 
+
+  [[noreturn]] static void invalid_spot_o_check()
+  {
+    throw std::runtime_error("invalid value for SPOT_O_CHECK "
+                             "(should be 1, 2, or 3)");
+  }
+
+  // This private function is defined in minimize.cc for technical
+  // reasons.
+  SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr);
+
+  bool
+  is_obligation(formula f, twa_graph_ptr aut, ocheck algo)
+  {
+    if (algo == ocheck::Auto)
+      {
+        static ocheck env_algo = []()
+          {
+            int val;
+            try
+              {
+                auto s = getenv("SPOT_O_CHECK");
+                val = s ? std::stoi(s) : 0;
+              }
+            catch (const std::exception& e)
+              {
+                invalid_spot_o_check();
+              }
+            if (val == 0)
+              return ocheck::via_WDBA;
+            else if (val == 1)
+              return ocheck::via_CoBuchi;
+            else if (val == 2)
+              return ocheck::via_Rabin;
+            else if (val == 3)
+              return ocheck::via_WDBA;
+            else
+              invalid_spot_o_check();
+          }();
+        algo = env_algo;
+      }
+    switch (algo)
+      {
+      case ocheck::via_WDBA:
+        return is_wdba_realizable(f, aut);
+      case ocheck::via_CoBuchi:
+        return (is_persistence(f, aut, prcheck::PR_via_CoBuchi)
+                && is_recurrence(f, aut, prcheck::PR_via_CoBuchi));
+      case ocheck::via_Rabin:
+        return (is_persistence(f, aut, prcheck::PR_via_Rabin)
+                && is_recurrence(f, aut, prcheck::PR_via_Rabin));
+      case ocheck::Auto:
+        SPOT_UNREACHABLE();
+      }
+    SPOT_UNREACHABLE();
+  }
+
+
   char mp_class(formula f)
   {
     if (f.is_syntactic_safety() && f.is_syntactic_guarantee())

spot/tl/hierarchy.hh

@@ -24,9 +24,9 @@
 
 namespace spot
 {
-  /// Enum used to change the behaviour of is_persistence() or is_recurrence().
+  /// Enum used to change the behavior of is_persistence() or is_recurrence().
   ///
-  /// If PR_Auto, both methodes will first check the environment variable
+  /// If PR_Auto, both methods will first check the environment variable
   /// <code>SPOT_PR_CHECK</code> to see if one algorithm or the other is wanted
   /// to be forced. Otherwise, it will make the most appropriate decision.
   ///
@@ -42,12 +42,12 @@ namespace spot
   /// if !f is cobuchi_realizable.
   enum class prcheck
   {
-    PR_Auto,
+    PR_Auto,             // FIXME: Remove the useless PR_ prefix since
-    PR_via_CoBuchi,
+    PR_via_CoBuchi,      // we already have a prcheck:: prefix.
-    PR_via_Rabin
+    PR_via_Rabin,
   };
 
-  /// \brief Return true if \a f has the persistence property.
+  /// \brief Return true if \a f represents a persistence property.
   ///
   /// \param f the formula to check.
   /// \param aut the corresponding automaton (not required).
@@ -57,7 +57,7 @@ namespace spot
                  twa_graph_ptr aut = nullptr,
                  prcheck algo = prcheck::PR_Auto);
 
-  /// \brief Return true if \a f has the recurrence property.
+  /// \brief Return true if \a f represents a recurrence property.
   ///
   /// Actually, it calls is_persistence() with the negation of \a f.
   ///
@@ -69,6 +69,39 @@ namespace spot
                 twa_graph_ptr aut = nullptr,
                 prcheck algo = prcheck::PR_Auto);
 
+  /// Enum used to change the behavior of is_obligation().
+  enum class ocheck
+  {
+    Auto,
+    via_CoBuchi,
+    via_Rabin,
+    via_WDBA,
+  };
+
+  /// \brief Return true if \a f has the recurrence property.
+  ///
+  /// Actually, it calls is_persistence() with the negation of \a f.
+  ///
+  /// \param f the formula to check.
+  /// \param aut the corresponding automaton (not required).
+  /// \param algo the algorithm to use.
+  ///
+  /// \a aut is constructed from f if not supplied.
+  ///
+  /// If \a algo is ocheck::via_WDBA, aut is converted into a WDBA
+  /// which is then checked for equivalence with aut.  If \a algo is
+  /// ocheck::via_CoBuchi, we test that both f and !f are co-Büchi
+  /// realizable.  If \a algo is ocheck::via_Rabin, we test that both
+  /// f and !f are DBA-realizable.
+  ///
+  /// Auto currently defaults to via_WDBA, unless the
+  /// <code>SPOT_O_CHECK</code> environment variable specifies
+  /// otherwise.
+  SPOT_API bool
+  is_obligation(formula f,
+                twa_graph_ptr aut = nullptr,
+                ocheck algo = ocheck::Auto);
+
   /// \brief Return the class of \a f in the temporal hierarchy of Manna
   /// and Pnueli (PODC'90).
   ///

spot/twaalgos/minimize.cc

@@ -46,6 +46,7 @@
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/remfin.hh>
+#include <spot/tl/hierarchy.hh>
 
 namespace spot
 {
@@ -581,6 +582,54 @@ namespace spot
     return res;
   }
 
+  // Declared in tl/hierarchy.cc, but defined here because it relies on
+  // other internal functions from this file.
+  SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr);
+
+  bool is_wdba_realizable(formula f, twa_graph_ptr aut)
+  {
+    if (f.is_syntactic_obligation())
+      return true;
+
+    if (aut == nullptr)
+      aut = ltl_to_tgba_fm(f, make_bdd_dict(), true);
+
+    if (!aut->is_existential())
+      throw std::runtime_error
+        ("is_wdba_realizable() does not support alternation");
+
+    if ((f.is_syntactic_persistence() || aut->prop_weak())
+        && (f.is_syntactic_recurrence() || is_deterministic(aut)))
+      return true;
+
+    if (is_terminal_automaton(aut))
+      return true;
+
+    // FIXME: we do not need to minimize the wdba to test realizability.
+    auto min_aut = minimize_wdba(aut);
+
+    if (!is_deterministic(aut)
+        && !product(aut, remove_fin(dualize(min_aut)))->is_empty())
+      return false;
+
+    twa_graph_ptr aut_neg;
+    if (is_deterministic(aut))
+      {
+        aut_neg = remove_fin(dualize(aut));
+      }
+    else
+      {
+        aut_neg = ltl_to_tgba_fm(formula::Not(f), aut->get_dict());
+        aut_neg = scc_filter(aut_neg, true);
+      }
+
+    if (is_terminal_automaton(aut_neg))
+      return true;
+
+    return product(min_aut, aut_neg)->is_empty();
+  }
+
+
   twa_graph_ptr
   minimize_obligation(const const_twa_graph_ptr& aut_f,
                       formula f,
@@ -591,6 +640,9 @@ namespace spot
       throw std::runtime_error
         ("minimize_obligation() does not support alternation");
 
+    // FIXME: We should build scc_info once, pass it to minimize_wdba
+    // and reuse it for is_terminal_automaton(), and
+    // is_weak_automaton().
     auto min_aut_f = minimize_wdba(aut_f);
 
     if (reject_bigger)
@@ -601,16 +653,16 @@ namespace spot
           return std::const_pointer_cast<twa_graph>(aut_f);
       }
 
-    // If the input automaton was already weak and deterministic, the
-    // output is necessary correct.
-    if (aut_f->prop_weak() && is_deterministic(aut_f))
-      return min_aut_f;
-
     // if f is a syntactic obligation formula, the WDBA minimization
     // must be correct.
     if (f && f.is_syntactic_obligation())
       return min_aut_f;
 
+    // If the input automaton was already weak and deterministic, the
+    // output is necessary correct.
+    if (aut_f->prop_weak() && is_deterministic(aut_f))
+      return min_aut_f;
+
     // If aut_f is a guarantee automaton, the WDBA minimization must be
     // correct.
     if (is_terminal_automaton(aut_f))

tests/core/obligation.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2010, 2011, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2010, 2011, 2014, 2015, 2017 Laboratoire de Recherche
-# Développement de l'Epita (LRDE).
+# et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -117,4 +117,23 @@ while read exp f; do
   esac
 done < formulas.txt
 
+set -x
+
+cut -c 4- formulas.txt | ltlfilt --obligation > o0
+for i in 1 2 3; do
+  cut -c 4- formulas.txt | SPOT_O_CHECK=$i ltlfilt --obligation > o$i
+done
+# make sure SPOT_O_CHECK is actually read
+cut -c 4- formulas.txt | SPOT_O_CHECK=x ltlfilt --obligation 2>err && exit 1
+cut -c 4- formulas.txt | SPOT_O_CHECK=9 ltlfilt --obligation 2>err && exit 1
+grep SPOT_O_CHECK err
+diff o0 o2
+diff o1 o2
+diff o2 o3
+cut -c 4- formulas.txt | ltlfilt -o %h.ltl
+cat O.ltl G.ltl S.ltl B.ltl | sort > ogsb.ltl
+sort o3 > o4
+diff o4 ogsb.ltl
+
+
 exit 0