alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: allow spot.formula(spot.formula(...))

Browse source 
* python/spot/__init__.py: Recognize if the input is already a
formula.
* tests/python/formulas.ipynb: Test this.
This commit is contained in:
Alexandre Duret-Lutz 2017-12-22 17:18:36 +01:00
parent 3b4335d243
commit 31ccab026b
2 changed files with 71 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

5
python/spot/__init__.py
View file

@ -166,7 +166,10 @@ class twa:
class formula: class formula:
def __init__(self, str): def __init__(self, str):
"""Parse the given string to create a formula.""" """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): def show_ast(self):
"""Display the syntax tree of the formula.""" """Display the syntax tree of the formula."""

104
tests/python/formulas.ipynb
View file

@ -15,7 +15,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.6.4rc1" "version": "3.6.4"
}, },
"name": "" "name": ""
}, },
@ -127,6 +127,36 @@
], ],
"prompt_number": 4 "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", "cell_type": "markdown",
"metadata": {}, "metadata": {},
@ -147,13 +177,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 5, "prompt_number": 6,
"text": [ "text": [
"'p1 U (p2 R (p3 & !p4))'" "'p1 U (p2 R (p3 & !p4))'"
] ]
} }
], ],
"prompt_number": 5 "prompt_number": 6
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -186,7 +216,7 @@
] ]
} }
], ],
"prompt_number": 6 "prompt_number": 7
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -223,7 +253,7 @@
] ]
} }
], ],
"prompt_number": 7 "prompt_number": 8
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -288,7 +318,7 @@
] ]
} }
], ],
"prompt_number": 8 "prompt_number": 9
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -309,13 +339,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 9, "prompt_number": 10,
"text": [ "text": [
"True" "True"
] ]
} }
], ],
"prompt_number": 9 "prompt_number": 10
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -329,13 +359,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 10, "prompt_number": 11,
"text": [ "text": [
"False" "False"
] ]
} }
], ],
"prompt_number": 10 "prompt_number": 11
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -356,13 +386,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 11, "prompt_number": 12,
"text": [ "text": [
"True" "True"
] ]
} }
], ],
"prompt_number": 11 "prompt_number": 12
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -376,13 +406,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 12, "prompt_number": 13,
"text": [ "text": [
"False" "False"
] ]
} }
], ],
"prompt_number": 12 "prompt_number": 13
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -396,13 +426,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 13, "prompt_number": 14,
"text": [ "text": [
"True" "True"
] ]
} }
], ],
"prompt_number": 13 "prompt_number": 14
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -426,13 +456,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 14, "prompt_number": 15,
"text": [ "text": [
"\"a > b\" & \"proc[2]@init\" & GF_foo_" "\"a > b\" & \"proc[2]@init\" & GF_foo_"
] ]
} }
], ],
"prompt_number": 14 "prompt_number": 15
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -449,13 +479,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 15, "prompt_number": 16,
"text": [ "text": [
"a & b & GFc" "a & b & GFc"
] ]
} }
], ],
"prompt_number": 15 "prompt_number": 16
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -472,13 +502,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 16, "prompt_number": 17,
"text": [ "text": [
"p0 & p1 & GFp2" "p0 & p1 & GFp2"
] ]
} }
], ],
"prompt_number": 16 "prompt_number": 17
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -506,7 +536,7 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 17, "prompt_number": 18,
"svg": [ "svg": [
"<svg height=\"260pt\" viewBox=\"0.00 0.00 269.00 260.00\" width=\"269pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "<svg height=\"260pt\" viewBox=\"0.00 0.00 269.00 260.00\" width=\"269pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 256)\">\n", "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 256)\">\n",
@ -615,7 +645,7 @@
] ]
} }
], ],
"prompt_number": 17 "prompt_number": 18
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -636,7 +666,7 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 18, "prompt_number": 19,
"svg": [ "svg": [
"<svg height=\"210\" version=\"1.1\" width=\"220\" xmlns=\"http://www.w3.org/2000/svg\">\n", "<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", "<polygon fill=\"cyan\" opacity=\".2\" points=\"20,0 200,120 200,210 20,210\"/>\n",
@ -668,7 +698,7 @@
] ]
} }
], ],
"prompt_number": 18 "prompt_number": 19
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -682,13 +712,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 19, "prompt_number": 20,
"text": [ "text": [
"'recurrence'" "'recurrence'"
] ]
} }
], ],
"prompt_number": 19 "prompt_number": 20
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -705,13 +735,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 20, "prompt_number": 21,
"text": [ "text": [
"F(a & X(!a & b))" "F(a & X(!a & b))"
] ]
} }
], ],
"prompt_number": 20 "prompt_number": 21
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -735,13 +765,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 21, "prompt_number": 22,
"text": [ "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))))" "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", "cell_type": "markdown",
@ -766,13 +796,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 22, "prompt_number": 23,
"text": [ "text": [
"(0 R !(a <-> b)) -> (1 U (a <-> b))" "(0 R !(a <-> b)) -> (1 U (a <-> b))"
] ]
} }
], ],
"prompt_number": 22 "prompt_number": 23
}, },
{ {
"cell_type": "code", "cell_type": "code",
@ -789,13 +819,13 @@
], ],
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 23, "prompt_number": 24,
"text": [ "text": [
"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))" "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))"
] ]
} }
], ],
"prompt_number": 23 "prompt_number": 24
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
@ -833,7 +863,7 @@
] ]
} }
], ],
"prompt_number": 24 "prompt_number": 25
} }
], ],
"metadata": {} "metadata": {}