From 540b971355c2a9c79296b6e11fc6863526758acc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Apr 2017 14:32:01 +0200 Subject: [PATCH] gen: rename genltl() to ltl_pattern() and introduce ltl_patterns() * spot/gen/formulas.hh, spot/gen/formulas.cc (genltl): Rename as... (ltl_pattern): This. (ltl_pattern_max): New function. * bin/genltl.cc: Adjust names, and simplify using ltl_pattern_max(). * python/spot/gen.i (ltl_patterns): New function. * tests/python/gen.py: Test it. * tests/python/gen.ipynb: New file to document the spot.gen package. * tests/Makefile.am, doc/org/tut.org: Add gen.ipynb. --- bin/genltl.cc | 69 ++---- doc/org/tut.org | 1 + python/spot/gen.i | 33 +++ spot/gen/formulas.cc | 58 ++++- spot/gen/formulas.hh | 14 +- tests/Makefile.am | 1 + tests/python/gen.ipynb | 509 +++++++++++++++++++++++++++++++++++++++++ tests/python/gen.py | 10 +- 8 files changed, 640 insertions(+), 55 deletions(-) create mode 100644 tests/python/gen.ipynb diff --git a/bin/genltl.cc b/bin/genltl.cc index b08d6650b..51a01cc7b 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -48,7 +48,7 @@ using namespace spot; const char argp_program_doc[] ="\ Generate temporal logic formulas from predefined patterns."; -// We reuse the values from spot::gen::ltl_patterns as option keys. +// We reuse the values from spot::gen::ltl_pattern_id as option keys. // Additional options should therefore start after // spot::gen::LAST_CLASS. enum { @@ -171,7 +171,7 @@ static const argp_option options[] = struct job { - spot::gen::ltl_pattern pattern; + spot::gen::ltl_pattern_id pattern; struct range range; }; @@ -188,54 +188,36 @@ const struct argp_child children[] = }; static void -enqueue_job(int pattern, const char* range_str) +enqueue_job(int pattern, const char* range_str = nullptr) { job j; - j.pattern = static_cast(pattern); - j.range = parse_range(range_str); - jobs.push_back(j); -} - -static void -enqueue_job(int pattern, int min, int max) -{ - job j; - j.pattern = static_cast(pattern); - j.range = {min, max}; + j.pattern = static_cast(pattern); + if (range_str) + { + j.range = parse_range(range_str); + } + else + { + j.range.min = 1; + j.range.max = spot::gen::ltl_pattern_max(j.pattern); + if (j.range.max == 0) + error(2, 0, "missing range for %s", + spot::gen::ltl_pattern_name(j.pattern)); + } jobs.push_back(j); } static int parse_opt(int key, char* arg, struct argp_state*) { + if (key >= spot::gen::FIRST_CLASS && key < spot::gen::LAST_CLASS) + { + enqueue_job(key, arg); + return 0; + } // This switch is alphabetically-ordered. switch (key) { - case spot::gen::DAC_PATTERNS: - case spot::gen::HKRSS_PATTERNS: - if (arg) - enqueue_job(key, arg); - else - enqueue_job(key, 1, 55); - break; - case spot::gen::EH_PATTERNS: - if (arg) - enqueue_job(key, arg); - else - enqueue_job(key, 1, 12); - break; - case spot::gen::P_PATTERNS: - if (arg) - enqueue_job(key, arg); - else - enqueue_job(key, 1, 20); - break; - case spot::gen::SB_PATTERNS: - if (arg) - enqueue_job(key, arg); - else - enqueue_job(key, 1, 27); - break; case OPT_POSITIVE: opt_positive = true; break; @@ -243,11 +225,6 @@ parse_opt(int key, char* arg, struct argp_state*) opt_negative = true; break; default: - if (key >= spot::gen::FIRST_CLASS && key < spot::gen::LAST_CLASS) - { - enqueue_job(key, arg); - break; - } return ARGP_ERR_UNKNOWN; } return 0; @@ -255,9 +232,9 @@ parse_opt(int key, char* arg, struct argp_state*) static void -output_pattern(spot::gen::ltl_pattern pattern, int n) +output_pattern(spot::gen::ltl_pattern_id pattern, int n) { - formula f = spot::gen::genltl(pattern, n); + formula f = spot::gen::ltl_pattern(pattern, n); // Make sure we use only "p42"-style of atomic propositions // in lbt's output. diff --git a/doc/org/tut.org b/doc/org/tut.org index 89e6e79ab..12154f4cb 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -69,6 +69,7 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata in Python - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] +- [[https://spot.lrde.epita.fr/ipynb/gen.html][=gen.ipynb=]] show how to generate families of LTL formulas (as done in [[file:genltl.org][=genltl=]]) or automata ([[file:genaut.org][=genaut=]]) - [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()=, =decompose_acc_scc()= and =decompose_scc()= functions - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing automaton diff --git a/python/spot/gen.i b/python/spot/gen.i index 150f21ec5..7b91093cd 100644 --- a/python/spot/gen.i +++ b/python/spot/gen.i @@ -53,3 +53,36 @@ using namespace spot; %include %include + +%pythoncode %{ +def ltl_patterns(*args): + """ + Generate LTL patterns. + + The arguments should be have one of these three forms: + - (id, n) + - (id, min, max) + - id + In the first case, the pattern id=n is generated. In the second + case, all pattern id=n for min<=n<=max are generated. The + third case is a shorthand for (id, 1, 10), except when + id denotes one of the hard-coded list of LTL formulas (like, + DAC_PATTERNS, EH_PATTERNS, etc.) where all formulas from that + list are output. + """ + for spec in args: + if type(spec) is int: + pat = spec + min = 1 + max = ltl_pattern_max(spec) or 10 + else: + ls = len(spec) + if ls == 2: + pat, min, max = spec[0], spec[1], spec[1] + elif ls == 3: + pat, min, max = spec + else: + raise RuntimeError("invalid pattern specification") + for n in range(min, max + 1): + yield ltl_pattern(pat, n) +%} diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index 541bc9e2d..c07128735 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -1041,7 +1041,7 @@ namespace spot } } - formula genltl(ltl_pattern pattern, int n) + formula ltl_pattern(ltl_pattern_id pattern, int n) { if (n < 0) { @@ -1127,7 +1127,7 @@ namespace spot } - const char* ltl_pattern_name(ltl_pattern pattern) + const char* ltl_pattern_name(ltl_pattern_id pattern) { static const char* const class_name[] = { @@ -1174,6 +1174,60 @@ namespace spot return class_name[pattern - FIRST_CLASS]; } + int ltl_pattern_max(ltl_pattern_id pattern) + { + switch (pattern) + { + // Keep this alphabetically-ordered! + case AND_F: + case AND_FG: + case AND_GF: + case CCJ_ALPHA: + case CCJ_BETA: + case CCJ_BETA_PRIME: + return 0; + case DAC_PATTERNS: + return 55; + case EH_PATTERNS: + return 12; + case GH_Q: + case GH_R: + case GO_THETA: + return 0; + case HKRSS_PATTERNS: + return 55; + case KR_N: + case KR_NLOGN: + case KV_PSI: + case OR_FG: + case OR_G: + case OR_GF: + return 0; + case P_PATTERNS: + return 20; + case R_LEFT: + case R_RIGHT: + case RV_COUNTER_CARRY: + case RV_COUNTER_CARRY_LINEAR: + case RV_COUNTER: + case RV_COUNTER_LINEAR: + return 0; + case SB_PATTERNS: + return 27; + case TV_F1: + case TV_F2: + case TV_G1: + case TV_G2: + case TV_UU: + case U_LEFT: + case U_RIGHT: + return 0; + case LAST_CLASS: + break; + } + throw std::runtime_error("unsupported pattern"); + + } } } diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index 0283041cb..102c0a428 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -165,7 +165,7 @@ namespace spot { namespace gen { - enum ltl_pattern { + enum ltl_pattern_id { FIRST_CLASS = 256, AND_F = FIRST_CLASS, AND_FG, @@ -205,15 +205,21 @@ namespace spot /// \brief generate an LTL from a known pattern /// - /// The pattern is specified using one value from the ltl_pattern + /// The pattern is specified using one value from the ltl_pattern_id /// enum. See the man page of the `genltl` binary for a /// description of those pattern, and bibliographic references. - SPOT_API formula genltl(ltl_pattern pattern, int n); + SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n); /// \brief convert an ltl_pattern value into a name /// /// The returned name is suitable to be used as an option /// key for the genltl binary. - SPOT_API const char* ltl_pattern_name(ltl_pattern pattern); + SPOT_API const char* ltl_pattern_name(ltl_pattern_id pattern); + + /// \brief upper bound for LTL patterns + /// + /// If an LTL pattern has an upper bound, this returns it. + /// Otherwise, this returns 0. + SPOT_API int ltl_pattern_max(ltl_pattern_id pattern); } } diff --git a/tests/Makefile.am b/tests/Makefile.am index e8eec9428..16be77658 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -310,6 +310,7 @@ TESTS_ipython = \ python/automata.ipynb \ python/decompose.ipynb \ python/formulas.ipynb \ + python/gen.ipynb \ python/highlighting.ipynb \ python/ltsmin-dve.ipynb \ python/ltsmin-pml.ipynb \ diff --git a/tests/python/gen.ipynb b/tests/python/gen.ipynb new file mode 100644 index 000000000..7160d7bd1 --- /dev/null +++ b/tests/python/gen.ipynb @@ -0,0 +1,509 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.3" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Formulas & Automata generators\n", + "\n", + "The `spot.gen` package contains the functions used to generate the patterns produced by [`genltl`](https://spot.lrde.epita.fr/genltl.html) and [`genaut`](https://spot.lrde.epita.fr/genaut.html)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "import spot.gen as sg\n", + "spot.setup()\n", + "from IPython.display import display" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 13 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## LTL patterns\n", + "\n", + "Generation of LTL formulas is done via the `ltl_pattern()` function. This takes two arguments: a pattern id, and a pattern size (or index if the id refers to a list)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sg.ltl_pattern(sg.AND_GF, 3)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3}$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 14, + "text": [ + "GFp1 & GFp2 & GFp3" + ] + } + ], + "prompt_number": 14 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sg.ltl_pattern(sg.CCJ_BETA_PRIME, 4)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$\\mathsf{F} (p \\land \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} p) \\land \\mathsf{F} (q \\land \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} q)$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 15, + "text": [ + "F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)" + ] + } + ], + "prompt_number": 15 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To see the list of supported patterns, the easiest way is to look at the `--help` output of `genltl`. The above pattern for instance is attached to option `--ccj-beta-prime`. The name of the pattern identifier is the same using capital letters and underscores. If a pattern has multiple aliased options in `genltl`, the first one used for the identifier (e.g., `genltl` accept both `--dac-patterns` and `--spec-patterns` as synonyms to denote the patterns of `spot.gen.DAC_PATTERNS`).\n", + "\n", + "Multiple patterns can be generated using the `ltl_patterns()` function. It's arguments should be either can be:\n", + " - pairs of the form `(id, n)`: in this case the pattern `id` with size/index `n` is returned,\n", + " - triplets of the form `(id, min, max)`: in this case the patterns are output for all `n` between `min` and `max` included,\n", + " - an integer `id`: then this is equivalent to `(id, 1, 10)` if the pattern has now upper bound, or `(id, 1, upper)` if the patter `id` has an upper bound `upper`. This is mostly used when the pattern id correspond to a hard-coded list of formulas.\n", + "\n", + "Here is an example showing these three types of arguments:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for f in sg.ltl_patterns((sg.GH_R, 3), (sg.AND_FG, 1, 3), sg.EH_PATTERNS):\n", + " display(f)" + ], + "language": "python", + "metadata": { + "scrolled": false + }, + "outputs": [ + { + "latex": [ + "$(\\mathsf{G} \\mathsf{F} p_{1} \\lor \\mathsf{F} \\mathsf{G} p_{2}) \\land (\\mathsf{G} \\mathsf{F} p_{2} \\lor \\mathsf{F} \\mathsf{G} p_{3}) \\land (\\mathsf{G} \\mathsf{F} p_{3} \\lor \\mathsf{F} \\mathsf{G} p_{4})$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)" + ] + }, + { + "latex": [ + "$\\mathsf{F} \\mathsf{G} p_{1}$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "FGp1" + ] + }, + { + "latex": [ + "$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2}$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "FGp1 & FGp2" + ] + }, + { + "latex": [ + "$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2} \\land \\mathsf{F} \\mathsf{G} p_{3}$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "FGp1 & FGp2 & FGp3" + ] + }, + { + "latex": [ + "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{G} p_{2})$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "p0 U (p1 & Gp2)" + ] + }, + { + "latex": [ + "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\mathbin{\\mathsf{U}} p_{3}))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "p0 U (p1 & X(p2 U p3))" + ] + }, + { + "latex": [ + "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\land \\mathsf{F} (p_{3} \\land \\mathsf{X} \\mathsf{F} (p_{4} \\land \\mathsf{X} \\mathsf{F} (p_{5} \\land \\mathsf{X} \\mathsf{F} p_{6})))))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))" + ] + }, + { + "latex": [ + "$\\mathsf{F} (p_{0} \\land \\mathsf{X} \\mathsf{G} p_{1})$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "F(p0 & XGp1)" + ] + }, + { + "latex": [ + "$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\land \\mathsf{X} \\mathsf{F} p_{2}))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "F(p0 & X(p1 & XFp2))" + ] + }, + { + "latex": [ + "$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "F(p0 & X(p1 U p2))" + ] + }, + { + "latex": [ + "$\\mathsf{G} \\mathsf{F} p_{0} \\lor \\mathsf{F} \\mathsf{G} p_{1}$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "GFp0 | FGp1" + ] + }, + { + "latex": [ + "$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "G(p0 -> (p1 U p2))" + ] + }, + { + "latex": [ + "$\\mathsf{G} (p_{0} \\land \\mathsf{X} \\mathsf{F} (p_{1} \\land \\mathsf{X} \\mathsf{F} (p_{2} \\land \\mathsf{X} \\mathsf{F} p_{3})))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "G(p0 & XF(p1 & XF(p2 & XFp3)))" + ] + }, + { + "latex": [ + "$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3} \\land \\mathsf{G} \\mathsf{F} p_{0} \\land \\mathsf{G} \\mathsf{F} p_{4}$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "GFp1 & GFp2 & GFp3 & GFp0 & GFp4" + ] + }, + { + "latex": [ + "$(p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\mathbin{\\mathsf{U}} p_{2})) \\lor (p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{U}} p_{0})) \\lor (p_{2} \\mathbin{\\mathsf{U}} (p_{0} \\mathbin{\\mathsf{U}} p_{1}))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))" + ] + }, + { + "latex": [ + "$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} (\\mathsf{G} p_{2} \\lor \\mathsf{G} p_{3})))$" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "G(p0 -> (p1 U (Gp2 | Gp3)))" + ] + } + ], + "prompt_number": 20 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Automata patterns\n", + "\n", + "We currently have only one generator of automata:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sg.ks_cobuchi(3).show('.a')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 23, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "(!a & b) | (a & !b)\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !b) | (a & b)\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 23 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": null + } + ], + "metadata": {} + } + ] +} diff --git a/tests/python/gen.py b/tests/python/gen.py index f6b0d6eab..ff3514195 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -38,21 +38,25 @@ except RuntimeError as e: else: exit(2) -f = gen.genltl(gen.AND_F, 3) +f = gen.ltl_pattern(gen.AND_F, 3) assert f.size() == 3 assert gen.ltl_pattern_name(gen.AND_F) == "and-f" try: - gen.genltl(1000, 3) + gen.ltl_pattern(1000, 3) except RuntimeError as e: assert 'unsupported pattern' in str(e) else: exit(2) try: - gen.genltl(gen.OR_G, -10) + gen.ltl_pattern(gen.OR_G, -10) except RuntimeError as e: assert 'or-g' in str(e) assert 'positive' in str(e) else: exit(2) + +assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.OR_G, 1, 5), + (gen.GH_Q, 3), + gen.EH_PATTERNS))