From 23c2cbf46a7975b8885594fc583232547c99a602 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Feb 2016 17:29:30 +0100 Subject: [PATCH] python: highlighting functions for edges and states * python/spot/impl.i (highlight_state, highlight_edge): New function. * python/spot/__init__.py (highlight_states, highlight_edges): New functions. * spot/twaalgos/dot.cc: Add a '#' option. * spot/taalgos/dot.cc: Ignore '#'. * tests/python/highlighting.ipynb: New file to illustrate everything. * tests/Makefile.am, doc/org/tut.org: Add it. --- doc/org/tut.org | 2 + python/spot/__init__.py | 9 + python/spot/impl.i | 26 +++ spot/taalgos/dot.cc | 1 + spot/twaalgos/dot.cc | 17 +- tests/Makefile.am | 1 + tests/python/highlighting.ipynb | 339 ++++++++++++++++++++++++++++++++ 7 files changed, 393 insertions(+), 2 deletions(-) create mode 100644 tests/python/highlighting.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index 7e04511e3..9fdf9336a 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -64,3 +64,5 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=ltsmin.ipynb=]] minimal test for loading a DiVinE model using the LTSmin interface. - [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes. +- [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=highlighting.ipynb=]] shows how to highlight states or edges in + automata. diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 29f9e3509..8b523df5a 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -147,6 +147,15 @@ class twa: from IPython.display import SVG return SVG(self._repr_svg_(opt)) + def highlight_states(self, states, color): + for state in states: + self.highlight_state(state, color) + return self + + def highlight_edges(self, edges, color): + for edge in edges: + self.highlight_edge(edge, color) + return self @_extend(twa) class twa: diff --git a/python/spot/impl.i b/python/spot/impl.i index 81053ec42..30bca14bf 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -546,6 +546,32 @@ namespace std { { return self->get_named_prop>("state-names"); } + + twa* highlight_state(unsigned state, unsigned color) + { + auto hs = + self->get_named_prop>("highlight-states"); + if (!hs) + { + hs = new std::map; + self->set_named_prop("highlight-states", hs); + } + (*hs)[state] = color; + return self; + } + + twa* highlight_edge(unsigned edge, unsigned color) + { + auto ht = + self->get_named_prop>("highlight-edges"); + if (!ht) + { + ht = new std::map; + self->set_named_prop("highlight-edges", ht); + } + (*ht)[edge] = color; + return self; + } } diff --git a/spot/taalgos/dot.cc b/spot/taalgos/dot.cc index 5e2e4d9a0..b42ec87b2 100644 --- a/spot/taalgos/dot.cc +++ b/spot/taalgos/dot.cc @@ -107,6 +107,7 @@ namespace spot case 't': case '+': case '<': + case '#': // All these options are implemented by dotty() on TGBA, // but are not implemented here. We simply ignore them, // because raising an exception if they are in diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 95aa8296f..a3d00975c 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -71,6 +71,7 @@ namespace spot bool opt_bullet_but_buchi = false; bool opt_all_bullets = false; bool opt_ordered_edges_ = false; + bool opt_numbered_edges_ = false; bool opt_want_state_names_ = true; unsigned opt_shift_sets_ = 0; std::string opt_font_; @@ -160,6 +161,9 @@ namespace spot options = end; break; } + case '#': + opt_numbered_edges_ = true; + break; case '1': opt_want_state_names_ = false; break; @@ -550,8 +554,17 @@ namespace spot } os_ << '>'; } - if (opt_ordered_edges_) - os_ << ", taillabel=\"" << number << '"'; + if (opt_ordered_edges_ || opt_numbered_edges_) + { + os_ << ", taillabel=\""; + if (opt_ordered_edges_) + os_ << number; + if (opt_ordered_edges_ && opt_numbered_edges_) + os_ << ' '; + if (opt_numbered_edges_) + os_ << '#' << aut_->get_graph().index_of_edge(t); + os_ << '"'; + } if (highlight_edges_) { auto idx = aut_->get_graph().index_of_edge(t); diff --git a/tests/Makefile.am b/tests/Makefile.am index 2d6b1c297..3b67497f2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -291,6 +291,7 @@ TESTS_python = \ python/bddnqueen.py \ python/decompose.ipynb \ python/formulas.ipynb \ + python/highlighting.ipynb \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb new file mode 100644 index 000000000..37132f41d --- /dev/null +++ b/tests/python/highlighting.ipynb @@ -0,0 +1,339 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:f1eb908ff21cb1cb844770da8e495a79965a4e6417793313eb447ba80378f4b4" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a = spot.translate('a U b U c')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `#` option of `print_dot()` can be used to display the internal number of each transition " + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.show('.#')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "#6\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "c\n", + "#4\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b & !c\n", + "#5\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "#1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "c\n", + "#2\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "#3\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Using these numbers you can selectively hightlight some transitions. The second argument is a color number (from a list of predefined colors)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.highlight_edges([2, 4, 5], 1)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f29585c6810> >" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that these `highlight_` functions work for edges and states, and come with both singular (changing the color of single state or edge) and plural versions.\n", + "\n", + "They modify the automaton in place." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.highlight_edge(6, 2).highlight_states((0, 1), 0)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f295853bcc0> >" + ] + } + ], + "prompt_number": 5 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file