Add support for computing operator nesting depth

* spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
function.
* python/spot/__init__.py: Also make it a method of formula in Python
* bin/common_output.cc, bin/common_output.hh: Implement
--stats=%[OP]n.
* NEWS: Mention it.
* tests/core/format.test, tests/python/formulas.ipynb: Test it.

NEWS

@@ -73,6 +73,9 @@ New in spot 2.4.2.dev (not yet released)
     by their acceptance name (Buchi, co-Buchi, Streett, etc.) or
     "other" if no name is known for the acceptance condition.
 
+  - Tools that produce formulas now support --format=%[OP]n to
+    display the nesting depth of operator OP.
+
   - All tools learned to check the SPOT_OOM_ABORT environment
     variable.  This is only useful for debuging out-of-memory
     conditions; see the spot-x(7) man page for detail.
@@ -194,6 +197,9 @@ New in spot 2.4.2.dev (not yet released)
     accept additionnal arguments and pass them to fun().  See
     https://spot.lrde.epita.fr/tut03.html for some examples.
 
+  - A the new function spot::nesting_depth() computes the nesting
+    depth of any LTL operator.
+
   - The new function spot::print_aiger() encodes an automaton as an
     AIGER circuit and prints it. This is only possible for automata
     whose acceptance condition is trivial. It relies on a new named

bin/common_output.cc

@@ -181,6 +181,27 @@ namespace
     }
   };
 
+  class printable_formula_nesting final:
+    public spot::printable_value<spot::formula>
+  {
+  public:
+    printable_formula_nesting&
+    operator=(spot::formula new_val)
+    {
+      val_ = new_val;
+      return *this;
+    }
+
+    virtual void
+    print(std::ostream& os, const char* opt) const override
+    {
+      if (*opt == '[' && opt[1] != ']')
+        os << spot::nesting_depth(val_, opt + 1);
+      else
+        throw std::runtime_error("%n expects arguments, e.g. %[X]n");
+    }
+  };
+
   class printable_formula_with_location final:
     public spot::printable_value<const formula_with_location*>
   {
@@ -214,6 +235,7 @@ namespace
       declare('L', &line_);
       declare('s', &size_);
       declare('h', &class_);
+      declare('n', &nesting_);
       declare('x', &ap_);
       declare('<', &prefix_);
       declare('>', &suffix_);
@@ -245,11 +267,13 @@ namespace
         size_ = spot::length(f);
       if (has('h'))
         class_ = spot::mp_class(f);
+      nesting_ = f;
       auto& res = format(format_);
       // Make sure we do not store the formula until the next one is
       // printed, as the order in which APs are registered may
       // influence the automata output.
       fl_ = nullptr;
+      nesting_ = nullptr;
       ap_.clear();
       return res;
     }
@@ -264,6 +288,7 @@ namespace
     spot::printable_value<const char*> suffix_;
     spot::printable_value<int> size_;
     printable_formula_class class_;
+    printable_formula_nesting nesting_;
     spot::printable_value<int> bool_size_;
     printable_varset ap_;
   };

bin/common_output.hh

@@ -58,6 +58,12 @@ extern bool escape_csv;
         "the class of the formula is the Manna-Pnueli hierarchy "       \
         "([v] replaces abbreviations by class names, [w] for all "      \
         "compatible classes)", 0 },                                     \
+    { "%[OP]n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,               \
+        "the nesting depth of operator OP.  OP should be a single "     \
+        "letter denoting the operator to count, or multiple letters "   \
+        "to fuse several operators during depth evaluation.  Add '~' "  \
+        "to rewrite the formula in negative normal form before "        \
+        "counting.", 0 },                                               \
     { "%x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,                       \
         OPTION_DOC | OPTION_NO_USAGE,                                   \
         COMMON_X_OUTPUT_SPECS(used in the formula), 0 }

python/spot/__init__.py

@@ -851,7 +851,8 @@ for fun in dir(formula):
         _addfilter(fun)
 
 for fun in ['remove_x', 'relabel', 'relabel_bse',
-            'simplify', 'unabbreviate']:
+            'simplify', 'unabbreviate', 'negative_normal_form',
+            'mp_class', 'nesting_depth']:
     _addmap(fun)
 
 

spot/tl/hierarchy.cc

@@ -19,6 +19,7 @@
 
 #include <sstream>
 #include <spot/tl/hierarchy.hh>
+#include <spot/tl/nenoform.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/minimize.hh>
@@ -368,4 +369,80 @@ namespace spot
     return os.str();
   }
 
+  unsigned nesting_depth(formula f, op oper)
+  {
+    unsigned max_depth = 0;
+    for (formula child: f)
+      max_depth = std::max(max_depth, nesting_depth(child, oper));
+    return max_depth + f.is(oper);
+  }
+
+  unsigned nesting_depth(formula f, const op* begin, const op* end)
+  {
+    unsigned max_depth = 0;
+    for (formula child: f)
+      max_depth = std::max(max_depth, nesting_depth(child, begin, end));
+    bool matched = std::find(begin, end, f.kind()) != end;
+    return max_depth + matched;
+  }
+
+  unsigned nesting_depth(formula f, const char* opers)
+  {
+    bool want_nnf = false;
+    std::vector<op> v;
+    for (;;)
+      switch (char c = *opers++)
+        {
+        case '~':
+          want_nnf = true;
+          break;
+        case '!':
+          v.push_back(op::Not);
+          break;
+        case '&':
+          v.push_back(op::And);
+          break;
+        case '|':
+          v.push_back(op::Or);
+          break;
+        case 'e':
+          v.push_back(op::Equiv);
+          break;
+        case 'F':
+          v.push_back(op::F);
+          break;
+        case 'G':
+          v.push_back(op::G);
+          break;
+        case 'i':
+          v.push_back(op::Implies);
+          break;
+        case 'M':
+          v.push_back(op::M);
+          break;
+        case 'R':
+          v.push_back(op::R);
+          break;
+        case 'U':
+          v.push_back(op::U);
+          break;
+        case 'W':
+          v.push_back(op::W);
+          break;
+        case 'X':
+          v.push_back(op::X);
+          break;
+        case '\0':
+        case ']':
+          goto break2;
+        default:
+          throw std::runtime_error
+            (std::string("nesting_depth(): unknown operator '") + c + '\'');
+        }
+  break2:
+    if (want_nnf)
+      f = negative_normal_form(f);
+    const op* vd = v.data();
+    return nesting_depth(f, vd, vd + v.size());
+  }
 }

spot/tl/hierarchy.hh

@@ -154,4 +154,34 @@ namespace spot
   /// of each class.  Space and commas are ignored.  Any ']' ends the
   /// processing of the options.
   SPOT_API std::string mp_class(char mpc, const char* opt);
+
+
+  /// \brief Compute the nesting depth of an operator.
+  ///
+  /// Return the maximum number of occurrence of \a oper among all
+  /// branches of the AST of \a f.
+  SPOT_API unsigned nesting_depth(formula f, op oper);
+
+#ifndef SWIG
+  /// \brief Compute the nesting depth of a set of operators.
+  ///
+  /// Return the maximum number of occurrence of any operator between
+  /// \a begin and \a end among all branches of the AST of \a f.
+  SPOT_API unsigned nesting_depth(formula f, const op* begin, const op* end);
+#endif
+
+  /// \brief Compute the nesting depth of a set of operators.
+  ///
+  /// Return the maximum number of occurrence of any operator listed
+  /// \a opers, among all branches of the AST of \a f.
+  ///
+  /// Operators to count should be supplied in \a opers as a string of
+  /// letters among 'X', 'F', 'G', 'U', 'R', 'M', 'W', '&', '|', '!',
+  /// 'i' (implication), 'e' (equivalence).
+  ///
+  /// Add letter '~' to force \a into negative normal form before
+  /// processing it.
+  ///
+  /// The string should be terminated by '\0' or ']'.
+  SPOT_API unsigned nesting_depth(formula f, const char* opers);
 }

tests/core/format.test

@@ -23,21 +23,31 @@
 
 set -e
 
-genltl --dac=1..10 --stats='%s,%b,%x,%f' > output
+genltl --dac=1..10 --stats='%s,%b,%x,%f,%[G]n,%[FUM]n,%[~GUM]n' > output
 cat >expected <<EOF
-3,2,1,G!p0
+3,2,1,G!p0,1,0,1
-7,6,2,Fp0 -> (!p1 U p0)
+7,6,2,Fp0 -> (!p1 U p0),0,1,1
-6,5,2,G(p0 -> G!p1)
+6,5,2,G(p0 -> G!p1),2,0,2
-13,9,3,G((p0 & !p1 & Fp1) -> (!p2 U p1))
+13,9,3,G((p0 & !p1 & Fp1) -> (!p2 U p1)),1,1,2
-10,6,3,G((p0 & !p1) -> (!p2 W p1))
+10,6,3,G((p0 & !p1) -> (!p2 W p1)),1,0,1
-2,2,1,Fp0
+2,2,1,Fp0,0,1,0
-7,3,2,!p0 W (!p0 & p1)
+7,3,2,!p0 W (!p0 & p1),0,0,0
-9,8,2,G!p0 | F(p0 & Fp1)
+9,8,2,G!p0 | F(p0 & Fp1),1,2,1
-13,6,3,G((p0 & !p1) -> (!p1 W (!p1 & p2)))
+13,6,3,G((p0 & !p1) -> (!p1 W (!p1 & p2))),1,0,1
-13,6,3,G((p0 & !p1) -> (!p1 U (!p1 & p2)))
+13,6,3,G((p0 & !p1) -> (!p1 U (!p1 & p2))),1,1,2
 EOF
 diff output expected
 
+genltl --dac --stats='%n' 2> stderr && exit 1
+cat stderr
+grep -F "genltl: %n expects arguments" stderr
+ltlfilt -f a --stats='%[]n' 2> stderr && exit 1
+cat stderr
+grep -F "ltlfilt: %n expects arguments" stderr
+randltl 2 --stats='%[;]n' 2> stderr && exit 1
+cat stderr
+grep "randltl: .*unknown.*;" stderr
+
 genltl --dac | ltlfilt --output='ap-%x.ltl'
 test 4 = `wc -l<ap-1.ltl`
 test 10 = `wc -l<ap-2.ltl`

tests/python/formulas.ipynb

@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.3rc1"
+   "version": "3.6.4rc1"
   },
   "name": ""
  },
@@ -636,7 +636,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 22,
+       "prompt_number": 18,
        "svg": [
         "<svg height=\"210\" version=\"1.1\" width=\"220\" xmlns=\"http://www.w3.org/2000/svg\">\n",
         "<polygon fill=\"cyan\" opacity=\".2\" points=\"20,0 200,120 200,210 20,210\"/>\n",
@@ -668,7 +668,7 @@
        ]
       }
      ],
-     "prompt_number": 22
+     "prompt_number": 18
     },
     {
      "cell_type": "code",
@@ -682,13 +682,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 24,
+       "prompt_number": 19,
        "text": [
         "'recurrence'"
        ]
       }
      ],
-     "prompt_number": 24
+     "prompt_number": 19
     },
     {
      "cell_type": "code",
@@ -705,13 +705,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 18,
+       "prompt_number": 20,
        "text": [
         "F(a & X(!a & b))"
        ]
       }
      ],
-     "prompt_number": 18
+     "prompt_number": 20
     },
     {
      "cell_type": "markdown",
@@ -735,13 +735,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 19,
+       "prompt_number": 21,
        "text": [
         "F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))"
        ]
       }
      ],
-     "prompt_number": 19
+     "prompt_number": 21
     },
     {
      "cell_type": "markdown",
@@ -766,13 +766,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 20,
+       "prompt_number": 22,
        "text": [
         "(0 R !(a <-> b)) -> (1 U (a <-> b))"
        ]
       }
      ],
-     "prompt_number": 20
+     "prompt_number": 22
     },
     {
      "cell_type": "code",
@@ -789,13 +789,51 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 21,
+       "prompt_number": 23,
        "text": [
         "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))"
        ]
       }
      ],
-     "prompt_number": 21
+     "prompt_number": 23
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Nesting level of operators"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "f = spot.formula('F(b & X(a U b U ((a W Fb) | (c U d))))')\n",
+      "print(\"U\", spot.nesting_depth(f, spot.op_U))\n",
+      "print(\"F\", spot.nesting_depth(f, spot.op_F))\n",
+      "# These following two are syntactic sugar for the above two\n",
+      "print(\"U\", spot.nesting_depth(f, \"U\"))\n",
+      "print(\"F\", spot.nesting_depth(f, \"F\"))\n",
+      "# If you want to consider \"U\" and \"F\" are a similar type of\n",
+      "# operator, you can count both with\n",
+      "print(\"FU\", spot.nesting_depth(f, \"FU\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "output_type": "stream",
+       "stream": "stdout",
+       "text": [
+        "U 3\n",
+        "F 2\n",
+        "U 3\n",
+        "F 2\n",
+        "FU 4\n"
+       ]
+      }
+     ],
+     "prompt_number": 24
     }
    ],
    "metadata": {}