diff --git a/wrap/python/spot.py b/wrap/python/spot.py index dc91a0a08..fcfc1e3cc 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -706,6 +706,6 @@ for fun in dir(formula): fun[:4] == 'has_')): _addfilter(fun) -for fun in ['remove_x', 'get_literal', 'relabel', 'relabel_bse', - 'simplify', 'unabbreviate_ltl']: +for fun in ['remove_x', 'relabel', 'relabel_bse', + 'simplify', 'unabbreviate']: _addmap(fun) diff --git a/wrap/python/tests/randltl.ipynb b/wrap/python/tests/randltl.ipynb index fd163cbce..dca0ebc00 100644 --- a/wrap/python/tests/randltl.ipynb +++ b/wrap/python/tests/randltl.ipynb @@ -17,7 +17,8 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "" + "name": "", + "signature": "sha256:b69bb80f870979f9654dbf2c1bcc0f26f652956e1f1ea4189d5c8078caa067c6" }, "nbformat": 3, "nbformat_minor": 0, @@ -601,8 +602,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "You may have noticed that the return type of randltl is 'formulaiterator'.
\n", - "Since the boolean functions and the 'mapping' functions return an iterator of the same type, this means these operations can be chained like this:" + "Since the boolean filters and mapping functions return an iterator of the same type, these operations can be chained like this:" ] }, { @@ -632,6 +632,43 @@ } ], "prompt_number": 15 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for formula in spot.randltl(3, 10).simplify().unabbreviate(\"WMGFR\"): print(formula)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "!(1 U !p1)\n", + "1 U ((p0 U ((p0 & p1) | (p1 R p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n", + "1 U (!p2 U ((p0 & !p2) | (p0 R !p2)))\n", + "(!p1 U (((1 U !(1 U !p1)) R !p1) | (!p1 & (1 U !(1 U !p1))))) | !(1 U !(p0 | (1 U p1)))\n", + "X(p2 & X(p2 U (!p0 | (p2 W !p0))))\n", + "(1 U p2) | (X(!p2 | !(1 U !p2)) U ((1 U p2) U (!p1 & (1 U p2))))\n", + "XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n", + "XX(1 U (p1 U ((p0 & p1) | (p0 R p1))))\n", + "p2 & Xp0\n" + ] + } + ], + "prompt_number": 16 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 16 } ], "metadata": {}