From 62d1e0219d831caa6885511389cd3ae7d2b9aa0f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 10 Dec 2017 20:22:40 +0100 Subject: [PATCH] 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 | 6 +++ bin/common_output.cc | 25 ++++++++++++ bin/common_output.hh | 6 +++ python/spot/__init__.py | 3 +- spot/tl/hierarchy.cc | 77 +++++++++++++++++++++++++++++++++++++ spot/tl/hierarchy.hh | 30 +++++++++++++++ tests/core/format.test | 32 +++++++++------ tests/python/formulas.ipynb | 64 +++++++++++++++++++++++------- 8 files changed, 218 insertions(+), 25 deletions(-) diff --git a/NEWS b/NEWS index cbcfe8b28..2b8697d29 100644 --- a/NEWS +++ b/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 diff --git a/bin/common_output.cc b/bin/common_output.cc index 0d47928c3..c3407a7fd 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -181,6 +181,27 @@ namespace } }; + class printable_formula_nesting final: + public spot::printable_value + { + 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 { @@ -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 suffix_; spot::printable_value size_; printable_formula_class class_; + printable_formula_nesting nesting_; spot::printable_value bool_size_; printable_varset ap_; }; diff --git a/bin/common_output.hh b/bin/common_output.hh index a200f1324..751160898 100644 --- a/bin/common_output.hh +++ b/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 } diff --git a/python/spot/__init__.py b/python/spot/__init__.py index acaad47c0..dcaba0910 100644 --- a/python/spot/__init__.py +++ b/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) diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 47cfb38a4..f3c90f652 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -19,6 +19,7 @@ #include #include +#include #include #include #include @@ -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 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()); + } } diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index c567983ed..41d852d89 100644 --- a/spot/tl/hierarchy.hh +++ b/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); } diff --git a/tests/core/format.test b/tests/core/format.test index 7785b94ab..4e6f4a4d5 100644 --- a/tests/core/format.test +++ b/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 < (!p1 U p0) -6,5,2,G(p0 -> G!p1) -13,9,3,G((p0 & !p1 & Fp1) -> (!p2 U p1)) -10,6,3,G((p0 & !p1) -> (!p2 W p1)) -2,2,1,Fp0 -7,3,2,!p0 W (!p0 & p1) -9,8,2,G!p0 | F(p0 & Fp1) -13,6,3,G((p0 & !p1) -> (!p1 W (!p1 & p2))) -13,6,3,G((p0 & !p1) -> (!p1 U (!p1 & p2))) +3,2,1,G!p0,1,0,1 +7,6,2,Fp0 -> (!p1 U p0),0,1,1 +6,5,2,G(p0 -> G!p1),2,0,2 +13,9,3,G((p0 & !p1 & Fp1) -> (!p2 U p1)),1,1,2 +10,6,3,G((p0 & !p1) -> (!p2 W p1)),1,0,1 +2,2,1,Fp0,0,1,0 +7,3,2,!p0 W (!p0 & p1),0,0,0 +9,8,2,G!p0 | F(p0 & Fp1),1,2,1 +13,6,3,G((p0 & !p1) -> (!p1 W (!p1 & p2))),1,0,1 +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\n", "\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": {}