tl: mp_class() and --format=%[vw]h

Tools for deciding the class of a formula.

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/common_output.cc, bin/common_output.hh: Implement --format=%h.
* tests/core/hierarchy.test: More tests.
* NEWS: Update.

NEWS

@@ -45,6 +45,11 @@ New in spot 2.2.2.dev (Not yet released)
     --syntactic-recurrence and --syntactic-persistence, the new checks
     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 &
+    Pnueli using %h.  Try to classify the Dwyer & al. patterns with:
+      genltl --dac --format='%[vw]h' | sort | uniq -c
+
   Library:
 
   * A twa is required to have at least one state, the initial state.
@@ -122,6 +127,9 @@ New in spot 2.2.2.dev (Not yet released)
     competition will be generated.  This requires the use of an exteral
     SAT solver, setup with "SPOT_SATSOLVER".  See spot-x(7).
 
+  * The new function mp_class(f) returns the class of the formula
+    f in the temporal hierarchy of Manna & Pnueli.
+
 New in spot 2.2.2 (2016-12-16)
 
   Build:

bin/common_output.cc

@@ -24,6 +24,7 @@
 #include <spot/tl/print.hh>
 #include <spot/tl/length.hh>
 #include <spot/tl/apcollect.hh>
+#include <spot/tl/hierarchy.hh>
 #include <spot/misc/formater.hh>
 #include <spot/misc/escape.hh>
 #include "common_cout.hh"
@@ -157,6 +158,109 @@ namespace
     const char* suffix;
   };
 
+  class printable_formula_class final:
+    public spot::printable_value<char>
+  {
+  public:
+    printable_formula_class&
+    operator=(char new_val)
+    {
+      val_ = new_val;
+      return *this;
+    }
+
+    virtual void
+    print(std::ostream& os, const char* opt) const override
+    {
+      bool verbose = false;
+      bool wide = false;
+      if (*opt == '[')
+        do
+          switch (*++opt)
+            {
+            case 'v':
+              verbose = true;
+              break;
+            case 'w':
+              wide = true;
+              break;
+            case ' ':
+            case '\t':
+            case '\n':
+            case ',':
+            case ']':
+              break;
+            }
+        while (*opt != ']');
+
+      std::string c(1, val_);
+      if (wide)
+        {
+          switch (val_)
+            {
+            case 'B':
+              c = "GSOPRT";
+              break;
+            case 'G':
+              c = "GOPRT";
+              break;
+            case 'S':
+              c = "SOPRT";
+              break;
+            case 'O':
+              c = "OPRT";
+              break;
+            case 'P':
+              c = "PT";
+              break;
+            case 'R':
+              c = "RT";
+              break;
+            case 'T':
+              break;
+            }
+        }
+      if (!verbose)
+        {
+          os << c;
+          return;
+        }
+
+      bool first = true;
+      for (char ch: c)
+        {
+          if (first)
+            first = false;
+          else
+            os << ' ';
+          switch (ch)
+            {
+            case 'B':
+              os << "guarantee safety";
+              break;
+            case 'G':
+              os << "guarantee";
+              break;
+            case 'S':
+              os << "safety";
+              break;
+            case 'O':
+              os << "obligation";
+              break;
+            case 'P':
+              os << "persistence";
+              break;
+            case 'R':
+              os << "recurrence";
+              break;
+            case 'T':
+              os << "reactivity";
+              break;
+            }
+        }
+    }
+  };
+
   class printable_formula final:
     public spot::printable_value<const formula_with_location*>
   {
@@ -187,6 +291,7 @@ namespace
       declare('F', &filename_);
       declare('L', &line_);
       declare('s', &size_);
+      declare('h', &class_);
       declare('<', &prefix_);
       declare('>', &suffix_);
       set_output(os);
@@ -212,6 +317,8 @@ namespace
         bool_size_ = spot::length_boolone(f);
       if (has('s'))
         size_ = spot::length(f);
+      if (has('h'))
+        class_ = spot::mp_class(f);
       return format(format_);
     }
 
@@ -223,6 +330,7 @@ namespace
     spot::printable_value<const char*> prefix_;
     spot::printable_value<const char*> suffix_;
     spot::printable_value<int> size_;
+    printable_formula_class class_;
     spot::printable_value<int> bool_size_;
     spot::printable_value<int> ap_num_;
   };

bin/common_output.hh

 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 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.
@@ -36,14 +36,18 @@ extern output_format_t output_format;
 extern bool full_parenth;
 extern bool escape_csv;
 
-#define COMMON_LTL_OUTPUT_SPECS                                 \
-    { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
-      "number of atomic propositions used in the formula", 0 }, \
-    { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
-      "the length (or size) of the formula", 0 },               \
-    { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
-      "the Boolean-length of the formula (i.e., all Boolean "   \
-      "subformulas count as 1)", 0 }
+#define COMMON_LTL_OUTPUT_SPECS                                         \
+    { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,                   \
+        "number of atomic propositions used in the formula", 0 },       \
+    { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,                   \
+        "the length (or size) of the formula", 0 },                     \
+    { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,                   \
+        "the Boolean-length of the formula (i.e., all Boolean "         \
+        "subformulas count as 1)", 0 },                                 \
+    { "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
+        "the class of the formula is the Manna-Pnueli hierarchy "       \
+        "([v] replaces abbreviations by class names, [w] for all "      \
+        "compatible classes)", 0 }
 
 extern const struct argp output_argp;
 

spot/tl/Makefile.am

 ## -*- coding: utf-8 -*-
-## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
-## l'Epita (LRDE).
+## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -31,6 +31,7 @@ tl_HEADERS =					\
   environment.hh				\
   exclusive.hh					\
   formula.hh					\
+  hierarchy.hh					\
   length.hh					\
   ltlf.hh					\
   mutation.hh					\
@@ -53,6 +54,7 @@ libtl_la_SOURCES =				\
   dot.cc					\
   exclusive.cc					\
   formula.cc					\
+  hierarchy.cc					\
   length.cc					\
   ltlf.cc					\
   mark.cc					\

spot/tl/hierarchy.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE)
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include <spot/tl/hierarchy.hh>
+#include <spot/twaalgos/isdet.hh>
+#include <spot/twaalgos/ltl2tgba_fm.hh>
+#include <spot/twaalgos/minimize.hh>
+#include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/totgba.hh>
+
+
+namespace spot
+{
+  namespace
+  {
+    static bool is_recurrence(formula f, const twa_graph_ptr& aut)
+    {
+      if (f.is_syntactic_recurrence() || is_deterministic(aut))
+        return true;
+      // If aut is a non-deterministic TGBA, we do
+      // TGBA->DPA->DRA->(D?)BA.  The conversion from DRA to
+      // BA will preserve determinism if possible.
+      spot::postprocessor p;
+      p.set_type(spot::postprocessor::Generic);
+      p.set_pref(spot::postprocessor::Deterministic
+                 | spot::postprocessor::SBAcc);
+      p.set_level(spot::postprocessor::Low);
+      auto dra = p.run(aut);
+      if (dra->acc().is_generalized_buchi())
+        {
+          return true;
+        }
+      else
+        {
+          auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra));
+          assert(ba);
+          return is_deterministic(ba);
+        }
+    }
+  }
+
+  char mp_class(formula f)
+  {
+    if (f.is_syntactic_safety() && f.is_syntactic_guarantee())
+      return 'B';
+    auto dict = make_bdd_dict();
+    auto aut = ltl_to_tgba_fm(f, dict, true);
+    auto min = minimize_obligation(aut, f);
+    if (aut != min) // An obligation.
+      {
+        bool g = is_terminal_automaton(min);
+        bool s = is_safety_mwdba(min);
+        if (g)
+          return s ? 'B' : 'G';
+        else
+          return s ? 'S' : 'O';
+      }
+    // Not an obligation.  Could by 'P', 'R', or 'T'.
+    if (is_recurrence(f, aut))
+      return 'R';
+    f = formula::Not(f);
+    aut = ltl_to_tgba_fm(f, dict, true);
+    if (is_recurrence(f, aut))
+      return 'P';
+    return 'T';
+  }
+}

spot/tl/hierarchy.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE)
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/tl/formula.hh>
+
+namespace spot
+{
+  /// \brief Return the class of \a f in the temporal hierarchy of Manna
+  /// and Pnueli (PODC'90).
+  ///
+  /// The class is indicated using a character among:
+  /// - 'B' (bottom) safety properties that are also guarantee properties
+  /// - 'G' guarantee properties that are not also safety properties
+  /// - 'S' safety properties that are not also guarantee properties
+  /// - 'O' obligation properties that are not safety or guarantee
+  ///       properties
+  /// - 'P' persistence properties that are not obligations
+  /// - 'R' recurrence properties that are not obligations
+  /// - 'T' (top) properties that are not persistence or recurrence
+  ///   properties
+  SPOT_API char mp_class(formula f);
+}

tests/core/hierarchy.test

@@ -44,3 +44,21 @@ test 3 -eq `genltl --dac | ltlfilt --recurrence -v -c`
 test 3 -eq `genltl --dac | ltl2tgba -G -D -S |
      autfilt --generalized-rabin | dstar2tgba |
      autfilt --is-deterministic -v -c`
+
+test "$(echo $(genltl --dac --format='%h') | sed 's/ //g')" = \
+     SSSSSGSOSRSSSSSSSSSSSSPSSRSRSRSSSSSSSSSSRORRRRSRSTRSRST
+
+
+# Implementations of uniq differ in the number of leading spaces, so
+# we remove them all.
+genltl --dac --format='%[vw]h' | sort | uniq -c |
+    sed 's/^ *\([0-9]\+\) \+/\1 /g' >out
+cat >expected <<EOF
+1 guarantee obligation persistence recurrence reactivity
+2 obligation persistence recurrence reactivity
+1 persistence reactivity
+2 reactivity
+12 recurrence reactivity
+37 safety obligation persistence recurrence reactivity
+EOF
+diff out expected