diff --git a/python/spot/__init__.py b/python/spot/__init__.py index dcaba0910..a78277c5b 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -166,7 +166,10 @@ class twa: class formula: def __init__(self, str): """Parse the given string to create a formula.""" - self.this = parse_formula(str) + if type(str) == formula: + self.this = str + else: + self.this = parse_formula(str) def show_ast(self): """Display the syntax tree of the formula.""" diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index ed7e042de..4786cfd19 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4rc1" + "version": "3.6.4" }, "name": "" }, @@ -127,6 +127,36 @@ ], "prompt_number": 4 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Passing a `formula` to `spot.formula` simply returns the formula." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.formula(h)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$c \\land (a \\lor b)$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "text": [ + "c & (a | b)" + ] + } + ], + "prompt_number": 5 + }, { "cell_type": "markdown", "metadata": {}, @@ -147,13 +177,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 5, + "prompt_number": 6, "text": [ "'p1 U (p2 R (p3 & !p4))'" ] } ], - "prompt_number": 5 + "prompt_number": 6 }, { "cell_type": "markdown", @@ -186,7 +216,7 @@ ] } ], - "prompt_number": 6 + "prompt_number": 7 }, { "cell_type": "markdown", @@ -223,7 +253,7 @@ ] } ], - "prompt_number": 7 + "prompt_number": 8 }, { "cell_type": "markdown", @@ -288,7 +318,7 @@ ] } ], - "prompt_number": 8 + "prompt_number": 9 }, { "cell_type": "markdown", @@ -309,13 +339,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 9, + "prompt_number": 10, "text": [ "True" ] } ], - "prompt_number": 9 + "prompt_number": 10 }, { "cell_type": "code", @@ -329,13 +359,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 10, + "prompt_number": 11, "text": [ "False" ] } ], - "prompt_number": 10 + "prompt_number": 11 }, { "cell_type": "markdown", @@ -356,13 +386,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 11, + "prompt_number": 12, "text": [ "True" ] } ], - "prompt_number": 11 + "prompt_number": 12 }, { "cell_type": "code", @@ -376,13 +406,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 12, + "prompt_number": 13, "text": [ "False" ] } ], - "prompt_number": 12 + "prompt_number": 13 }, { "cell_type": "code", @@ -396,13 +426,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 13, + "prompt_number": 14, "text": [ "True" ] } ], - "prompt_number": 13 + "prompt_number": 14 }, { "cell_type": "markdown", @@ -426,13 +456,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 14, + "prompt_number": 15, "text": [ "\"a > b\" & \"proc[2]@init\" & GF_foo_" ] } ], - "prompt_number": 14 + "prompt_number": 15 }, { "cell_type": "code", @@ -449,13 +479,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 15, + "prompt_number": 16, "text": [ "a & b & GFc" ] } ], - "prompt_number": 15 + "prompt_number": 16 }, { "cell_type": "code", @@ -472,13 +502,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 16, + "prompt_number": 17, "text": [ "p0 & p1 & GFp2" ] } ], - "prompt_number": 16 + "prompt_number": 17 }, { "cell_type": "markdown", @@ -506,7 +536,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 17, + "prompt_number": 18, "svg": [ "\n", "\n", @@ -615,7 +645,7 @@ ] } ], - "prompt_number": 17 + "prompt_number": 18 }, { "cell_type": "markdown", @@ -636,7 +666,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 18, + "prompt_number": 19, "svg": [ "\n", "\n", @@ -668,7 +698,7 @@ ] } ], - "prompt_number": 18 + "prompt_number": 19 }, { "cell_type": "code", @@ -682,13 +712,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 19, + "prompt_number": 20, "text": [ "'recurrence'" ] } ], - "prompt_number": 19 + "prompt_number": 20 }, { "cell_type": "code", @@ -705,13 +735,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 20, + "prompt_number": 21, "text": [ "F(a & X(!a & b))" ] } ], - "prompt_number": 20 + "prompt_number": 21 }, { "cell_type": "markdown", @@ -735,13 +765,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 21, + "prompt_number": 22, "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": 21 + "prompt_number": 22 }, { "cell_type": "markdown", @@ -766,13 +796,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 22, + "prompt_number": 23, "text": [ "(0 R !(a <-> b)) -> (1 U (a <-> b))" ] } ], - "prompt_number": 22 + "prompt_number": 23 }, { "cell_type": "code", @@ -789,13 +819,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 23, + "prompt_number": 24, "text": [ "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))" ] } ], - "prompt_number": 23 + "prompt_number": 24 }, { "cell_type": "markdown", @@ -833,7 +863,7 @@ ] } ], - "prompt_number": 24 + "prompt_number": 25 } ], "metadata": {}