From ff4c4a723122ffba2864ddbde4730cb149a74487 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 18 Jan 2017 20:58:20 +0100
Subject: [PATCH] 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.
---
 NEWS                        |  9 +++++
 python/ajax/css/trans.css   |  4 +-
 python/ajax/spotcgi.in      | 16 +-------
 python/spot/__init__.py     | 68 +++++++++++++++++++++++++++++++-
 tests/python/formulas.ipynb | 77 ++++++++++++++++++++++++++++++++++++-
 5 files changed, 156 insertions(+), 18 deletions(-)

diff --git a/NEWS b/NEWS
index 3d612f917..9e112080a 100644
--- a/NEWS
+++ b/NEWS
@@ -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
diff --git a/python/ajax/css/trans.css b/python/ajax/css/trans.css
index d336a77a1..1a980dddb 100644
--- a/python/ajax/css/trans.css
+++ b/python/ajax/css/trans.css
@@ -42,7 +42,9 @@ div.ltl2tgba {
   top:84px;
   z-index:1;
 }
-
+#results-body {
+  overflow: auto;
+}
 .ltldoc {
     text-align: right;
 }
diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in
index d0f940208..aa03ec7d6 100755
--- a/python/ajax/spotcgi.in
+++ b/python/ajax/spotcgi.in
@@ -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>')
diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index 292f24bd4..0f34693d8 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -1,5 +1,5 @@
 # -*- 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
diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index ca075be66..40833ab95 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.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
+}