From 17b295e10fdd2bd3381d6c5c72871bf0d574db3f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Jan 2018 18:43:12 +0100 Subject: [PATCH] python: SVG display of word as signals Fixes #309. * python/spot/__init__.py (twa_word.as_svg, twa_word.show): New methods. * tests/python/word.ipynb: Use them. * NEWS: Mention them. --- NEWS | 4 + python/spot/__init__.py | 89 ++++++++++++ tests/python/word.ipynb | 290 ++++++++++++++++++++++------------------ 3 files changed, 255 insertions(+), 128 deletions(-) diff --git a/NEWS b/NEWS index c50079e42..e7973d198 100644 --- a/NEWS +++ b/NEWS @@ -227,6 +227,10 @@ New in spot 2.4.4.dev (net yet released) - The "product-states" property of automata is now accessible via spot.twa.get_product_states() and spot.set.get_product_states(). + - twa_word instances can be displayed as SVG pictures, with one + signal per atomic proposition. For some examples, see the use of + the show() method in https://spot.lrde.epita.fr/ipynb/word.html + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 1a4856264..b8064e6d4 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1010,3 +1010,92 @@ def show_mp_hierarchy(cl): return SVG(mp_hierarchy_svg(cl)) formula.show_mp_hierarchy = show_mp_hierarchy + +@_extend(twa_word) +class twa_word: + def as_svg(self): + """ + Build an SVG picture representing the word as a collection of + signals for each atomic proposition. + """ + # Get the list of atomic proposition used + sup = buddy.bddtrue + for cond in list(self.prefix) + list(self.cycle): + sup = sup & buddy.bdd_support(cond) + ap = [] + while sup != buddy.bddtrue: + a = buddy.bdd_var(sup) + ap.append(a) + sup = buddy.bdd_high(sup) + + # Prepare canvas + psize = len(self.prefix) + csize = len(self.cycle) + d = { + 'endprefix': 50 * psize, + 'endcycle': 50 * (psize + csize), + 'w': 50 * (psize + csize * 2), + 'height': 50 * len(ap), + 'height2': 50 * len(ap) + 10, + 'h3': 50 * len(ap) + 12, + 'bgcolor': '#f4f4f4', + 'bgl': 'stroke="white" stroke-width="4"', + 'bgt': 'stroke="white" stroke-width="1"', + 'txt': 'text-anchor="start" font-size="20"', + 'red': 'stroke="#ff0000" stroke-width="2"', + 'sml': 'text-anchor="start" font-size="10"' + } + txt = ''' + + + + +'''.format(**d) + + # Iterate over all used atomic propositions, and fill each line + l = list(self.prefix) + list(self.cycle) + list(self.cycle) + bd = self.get_dict() + for ypos, a in enumerate(ap): + pa = buddy.bdd_ithvar(a) + na = buddy.bdd_nithvar(a) + name = bdd_format_formula(bd, pa) + # Whether the last state was down (-1), up (1), or unknown (0) + last = 0 + txt += ('' + .format(y=ypos*50, **d)) + txt += ('{name}' + .format(x=3, y=ypos*50+30, name=name, **d)) + for xpos, step in enumerate(l): + if buddy.bdd_implies(step, pa): + cur = 1 + elif buddy.bdd_implies(step, na): + cur = -1 + else: + cur = 0 + txt += ('' + .format(x=(xpos+1)*50, y1=ypos*50, y2=ypos*50+50, **d)) + if cur != 0: + if last == -cur: + txt += \ + ('' + .format(x=xpos*50, y1=ypos*50+5, + y2=ypos*50+45, **d)) + txt += \ + ('' + .format(x1=xpos*50, x2=(xpos+1)*50, + y=ypos*50+25-20*cur, **d)) + last = cur + if psize > 0: + txt += 'prefix'.format(**d) + txt += '''cycle +cycle'''.format(**d) + return txt + '' + + def show(self): + """ + Display the word as an SVG picture of signals. + """ + from IPython.display import SVG + return SVG(self.as_svg()) diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 2ee85888a..4bc52263c 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3" + "version": "3.6.4" }, "name": "" }, @@ -47,7 +47,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "aut = spot.translate('G(Fa <-> XXb)'); aut" + "aut = spot.translate('!a & G(Fa <-> XXb)'); aut" ], "language": "python", "metadata": {}, @@ -63,150 +63,121 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "1->5\n", - "\n", - "\n", - "!a\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a & b\n", "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "2->6\n", - "\n", - "\n", - "!a\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "6->6\n", + "4->4\n", "\n", "\n", "!a & !b\n", "\u24ff\n", "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7fdf783f0510> >" + " *' at 0x7fb74c39da80> >" ] } ], @@ -235,11 +206,11 @@ "text": [ "Prefix:\n", " 0\n", - " | a\n", + " | !a\n", " 1\n", " | a\n", "Cycle:\n", - " 3\n", + " 2\n", " | a & b\t{0}" ] } @@ -267,7 +238,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "a\n", + "!a\n", "{0}\n" ] } @@ -295,12 +266,47 @@ "output_type": "pyout", "prompt_number": 5, "text": [ - "a; a; cycle{a & b}" + "!a; a; cycle{a & b}" ] } ], "prompt_number": 5 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "A word can be represented as a collection of signals (one for each atomic proposition). The cycle part is shown twice." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "word.show()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 6, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "abprefixcycle\n", + "cycle" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 6 + }, { "cell_type": "markdown", "metadata": {}, @@ -323,13 +329,13 @@ "output_type": "stream", "stream": "stdout", "text": [ - "a\n", + "!a\n", "a\n", "a & b\n" ] } ], - "prompt_number": 6 + "prompt_number": 7 }, { "cell_type": "markdown", @@ -351,13 +357,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 7, + "prompt_number": 8, "text": [ - "cycle{a & b}" + "!a; cycle{a & b}" ] } ], - "prompt_number": 7 + "prompt_number": 8 }, { "cell_type": "markdown", @@ -378,13 +384,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 8, + "prompt_number": 9, "text": [ - "cycle{a & b}" + "!a; cycle{a & b}" ] } ], - "prompt_number": 8 + "prompt_number": 9 }, { "cell_type": "markdown", @@ -414,14 +420,14 @@ ] } ], - "prompt_number": 9 + "prompt_number": 10 }, { "cell_type": "code", "collapsed": false, "input": [ "# make sure that we can parse a word back after it has been printed\n", - "spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b}')))" + "w = spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b;!a&b}'))); w" ], "language": "python", "metadata": {}, @@ -429,13 +435,41 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 10, + "prompt_number": 11, "text": [ - "a; a & b; cycle{!a & !b}" + "a; a & b; cycle{!a & !b; !a & b}" ] } ], - "prompt_number": 10 + "prompt_number": 11 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "w.show()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 12, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "abprefixcycle\n", + "cycle" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 12 }, { "cell_type": "markdown", @@ -453,7 +487,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 11 + "prompt_number": 13 }, { "cell_type": "code", @@ -467,7 +501,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 12, + "prompt_number": 14, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7fdf783f0e40> >" + " *' at 0x7fb74c39d990> >" ] } ], - "prompt_number": 12 + "prompt_number": 14 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "The rest of this pages tests some syntax errors, you (humans) may skip it, but the test suite will not." + "The rest of this page tests some syntax errors, you (humans) may skip it, but the test suite will not." ] }, { @@ -576,7 +610,7 @@ ] } ], - "prompt_number": 13 + "prompt_number": 15 }, { "cell_type": "code", @@ -596,7 +630,7 @@ ] } ], - "prompt_number": 14 + "prompt_number": 16 }, { "cell_type": "code", @@ -616,7 +650,7 @@ ] } ], - "prompt_number": 15 + "prompt_number": 17 }, { "cell_type": "code", @@ -636,7 +670,7 @@ ] } ], - "prompt_number": 16 + "prompt_number": 18 }, { "cell_type": "code", @@ -648,7 +682,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 17 + "prompt_number": 19 }, { "cell_type": "code", @@ -667,13 +701,13 @@ "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", - "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 4160\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4161\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 4162\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4163\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4164\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", + "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 4922\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4923\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 4924\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4925\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4926\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle" ] } ], - "prompt_number": 18 + "prompt_number": 20 } ], "metadata": {} -- GitLab