Commit ff4c4a72 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: render the M&P hierarchy in SVG

* python/spot/__init__.py (show_mp_hierarchy, mp_hierarchy_svg): New
functions.
* tests/python/formulas.ipynb: Illustrate show_mp_hierarchy.
* python/ajax/spotcgi.in: Use mp_hierarchy_svg.
* python/ajax/css/trans.css: Adjust for possible overflows.
* NEWS: Mention this new feature.
parent 0e2ab5de
......@@ -144,6 +144,15 @@ New in spot 2.2.2.dev (Not yet released)
* The new function mp_class(f) returns the class of the formula
f in the temporal hierarchy of Manna & Pnueli.
Python:
* spot.show_mp_hierarchy() can be used to display the membership of
a formula to the Manna & Pnueli hierarchy, in notebooks. An
example is in https://spot.lrde.epita.fr/ipynb/formulas.html
* The on-line translator will now display the temporal hierarchy
in the "Formula > property information" output.
Bugs fixed:
* The minimize_wdba() function was not correctly minimizing automata
......
......@@ -42,7 +42,9 @@ div.ltl2tgba {
top:84px;
z-index:1;
}
#results-body {
overflow: auto;
}
.ltldoc {
text-align: right;
}
......
......@@ -502,23 +502,11 @@ if output_type == 'f':
else:
s = str(f)
unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
unbufprint('<div style="float:right">' +
spot.mp_hierarchy_svg(f) + '</div>')
for p in spot.list_formula_props(f):
unbufprint('<li>%s</li>\n' % p)
mpc = spot.mp_class(f, 'w')
if 'S' in mpc:
unbufprint('<li>safety</li>')
if 'G' in mpc:
unbufprint('<li>guarantee</li>')
if 'O' in mpc:
unbufprint('<li>obligation</li>')
if 'R' in mpc:
unbufprint('<li>recurrence</li>')
if 'P' in mpc:
unbufprint('<li>persistence</li>')
if 'T' == mpc:
unbufprint('<li>not a persistence nor a recurrence</li>')
if not f.is_syntactic_stutter_invariant():
if spot.is_stutter_invariant(f):
unbufprint('<li>stutter invariant</li>')
......
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016 Laboratoire de
# Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -886,10 +886,76 @@ def sat_minimize(aut, acc=None, colored=False,
from spot.impl import sat_minimize as sm
return sm(aut, args, state_based)
def parse_word(word, dic=_bdd_dict):
from spot.impl import parse_word as pw
return pw(word, dic)
def language_containment_checker(dic=_bdd_dict):
from spot.impl import language_containment_checker as c
return c(dic)
def mp_hierarchy_svg(cl=None):
"""
Return an some string containing an SVG picture of the Manna &
Pnueli hierarchy, highlighting class `cl` if given.
If not None, `cl` should be one of 'TPROGSB'. For convenience,
if `cl` is an instance of `spot.formula`, it is replaced by
`mp_class(cl)`.
"""
if type(cl)==formula:
cl = mp_class(cl)
ch = None
coords = {
'T': '110,35',
'R': '40,80',
'P': '175,80',
'O': '110,140',
'S': '40,160',
'G': '175,160',
'B': '110,198',
}
if cl in coords:
highlight='''<g transform="translate({})">
<line x1="-10" y1="-10" x2="10" y2="10" stroke="red" stroke-width="5" />
<line x1="-10" y1="10" x2="10" y2="-10" stroke="red" stroke-width="5" />
</g>'''.format(coords[cl])
else:
highlight=''
return '''
<svg height="210" width="220" xmlns="http://www.w3.org/2000/svg" version="1.1">
<polygon points="20,0 200,120 200,210 20,210" fill="cyan" opacity=".2" />
<polygon points="20,120 155,210 20,210" fill="cyan" opacity=".2" />
<polygon points="200,0 20,120 20,210 200,210" fill="magenta" opacity=".15" />
<polygon points="200,120 65,210 200,210" fill="magenta" opacity=".15" />
''' + highlight + '''
<g text-anchor="middle" font-size="14">
<text x="110" y="20">Reactivity</text>
<text x="60" y="65">Recurrence</text>
<text x="160" y="65">Persistence</text>
<text x="110" y="125">Obligation</text>
<text x="60" y="185">Safety</text>
<text x="160" y="185">Guarantee</text>
</g>
<g font-size="14">
<text text-anchor="begin" transform="rotate(-90,18,210)" x="18" y="210" fill="gray">Monitor</text>
<text text-anchor="end" transform="rotate(-90,18,0)" x="18" y="0" fill="gray">Deterministic Büchi</text>
<text text-anchor="begin" transform="rotate(-90,214,210)" x="214" y="210" fill="gray">Terminal Büchi</text>
<text text-anchor="end" transform="rotate(-90,214,0)" x="214" y="0" fill="gray">Weak Büchi</text>
</g>
</svg>'''
def show_mp_hierarchy(cl):
"""
Return a picture of the Manna & Pnueli hierarchy as an SVG object
in the IPython/Jupyter.
"""
from IPython.display import SVG
return SVG(mp_hierarchy_svg(cl))
formula.show_mp_hierarchy = show_mp_hierarchy
......@@ -15,7 +15,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.4.3+"
"version": "3.5.3rc1"
},
"name": ""
},
......@@ -617,6 +617,79 @@
],
"prompt_number": 17
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Any formula can also be classified in the temporal hierarchy of Manna & Pnueli"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"g.show_mp_hierarchy()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 22,
"svg": [
"<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,120 155,210 20,210\"/>\n",
"<polygon fill=\"magenta\" opacity=\".15\" points=\"200,0 20,120 20,210 200,210\"/>\n",
"<polygon fill=\"magenta\" opacity=\".15\" points=\"200,120 65,210 200,210\"/>\n",
"<g transform=\"translate(40,80)\">\n",
" <line stroke=\"red\" stroke-width=\"5\" x1=\"-10\" x2=\"10\" y1=\"-10\" y2=\"10\"/>\n",
" <line stroke=\"red\" stroke-width=\"5\" x1=\"-10\" x2=\"10\" y1=\"10\" y2=\"-10\"/>\n",
" </g>\n",
"<g font-size=\"14\" text-anchor=\"middle\">\n",
"<text x=\"110\" y=\"20\">Reactivity</text>\n",
"<text x=\"60\" y=\"65\">Recurrence</text>\n",
"<text x=\"160\" y=\"65\">Persistence</text>\n",
"<text x=\"110\" y=\"125\">Obligation</text>\n",
"<text x=\"60\" y=\"185\">Safety</text>\n",
"<text x=\"160\" y=\"185\">Guarantee</text>\n",
"</g>\n",
"<g font-size=\"14\">\n",
"<text fill=\"gray\" text-anchor=\"begin\" transform=\"rotate(-90,18,210)\" x=\"18\" y=\"210\">Monitor</text>\n",
"<text fill=\"gray\" text-anchor=\"end\" transform=\"rotate(-90,18,0)\" x=\"18\" y=\"0\">Deterministic B\u00fcchi</text>\n",
"<text fill=\"gray\" text-anchor=\"begin\" transform=\"rotate(-90,214,210)\" x=\"214\" y=\"210\">Terminal B\u00fcchi</text>\n",
"<text fill=\"gray\" text-anchor=\"end\" transform=\"rotate(-90,214,0)\" x=\"214\" y=\"0\">Weak B\u00fcchi</text>\n",
"</g>\n",
"</svg>"
],
"text": [
"<IPython.core.display.SVG object>"
]
}
],
"prompt_number": 22
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mp_class(g, 'v')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 24,
"text": [
"'recurrence'"
]
}
],
"prompt_number": 24
},
{
"cell_type": "code",
"collapsed": false,
......@@ -728,4 +801,4 @@
"metadata": {}
}
]
}
\ No newline at end of file
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment