diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc
index 5b486866f..8e6b90e02 100644
--- a/spot/twaalgos/emptiness.cc
+++ b/spot/twaalgos/emptiness.cc
@@ -21,6 +21,7 @@
// along with this program. If not, see .
#include
+#include
#include
#include
#include
@@ -658,6 +659,52 @@ namespace spot
return true;
}
+ /// Note that this works only if the automaton is a twa_graph_ptr.
+ void twa_run::highlight(unsigned color)
+ {
+ auto a = std::dynamic_pointer_cast
+ (std::const_pointer_cast(aut));
+ if (!a)
+ throw std::runtime_error("highlight() only work for twa_graph");
+
+ auto h = new std::map; // highlighted edges
+
+ unsigned src = a->get_init_state_number();
+ auto l = prefix.empty() ? &cycle : &prefix;
+ auto e = l->end();
+ for (auto i = l->begin(); i != e;)
+ {
+ bdd label = i->label;
+ acc_cond::mark_t acc = i->acc;
+ unsigned dst;
+ ++i;
+ if (i != e)
+ {
+ dst = a->state_number(i->s);
+ }
+ else if (l == &prefix)
+ {
+ l = &cycle;
+ i = l->begin();
+ e = l->end();
+ dst = a->state_number(i->s);
+ }
+ else
+ {
+ dst = a->state_number(l->begin()->s);
+ }
+
+ for (auto& t: a->out(src))
+ if (t.dst == dst && t.cond == label && t.acc == acc)
+ {
+ (*h)[a->get_graph().index_of_edge(t)] = color;
+ break;
+ }
+ src = dst;
+ }
+ a->set_named_prop("highlight-edges", h);
+ }
+
twa_graph_ptr
twa_run::as_twa() const
{
diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh
index 6c4e14d7e..a6f9ae193 100644
--- a/spot/twaalgos/emptiness.hh
+++ b/spot/twaalgos/emptiness.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -312,6 +312,11 @@ namespace spot
/// \return true iff the run could be completed
bool replay(std::ostream& os, bool debug = false) const;
+ /// \brief Highlight the accepting run on the automaton.
+ ///
+ /// Note that this works only if the automaton is a twa_graph_ptr.
+ void highlight(unsigned color);
+
/// \brief Return a twa_graph_ptr corresponding to \a run
///
/// Identical states are merged.
diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb
index 68d96658b..1595234e6 100644
--- a/tests/python/highlighting.ipynb
+++ b/tests/python/highlighting.ipynb
@@ -1,7 +1,23 @@
{
"metadata": {
- "name": "",
- "signature": "sha256:c89800970357ab95bbed91a11bd8f6c61d1861b3fb1fb1edf133500904e3a355"
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.4.3+"
+ },
+ "name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
@@ -124,7 +140,7 @@
""
],
"text": [
- ""
+ ""
]
}
],
@@ -224,7 +240,7 @@
"\n"
],
"text": [
- " *' at 0x7f6f600c1690> >"
+ " *' at 0x7fd034659540> >"
]
}
],
@@ -326,11 +342,326 @@
"\n"
],
"text": [
- " *' at 0x7f6f60140b40> >"
+ " *' at 0x7fd034190180> >"
]
}
],
"prompt_number": 5
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "One use of this highlighting is to highlight a run in an automaton.\n",
+ "\n",
+ "The following few command generate an automaton, then an accepting run on this automaton, and highlight that accepting run on the automaton. Note that a run knows the automaton from which it was generated, so calling `highlight()` will directly decorate that automaton."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "b = spot.translate('X (F(Ga <-> b) & GF!b)'); b"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 6,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7fd034190240> >"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "r = spot.couvreur99(b).check().accepting_run(); r"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 7,
+ "text": [
+ "Prefix:\n",
+ " 0\n",
+ " | 1\n",
+ " 1\n",
+ " | !a & !b\n",
+ "Cycle:\n",
+ " 2\n",
+ " | !b\t{0}"
+ ]
+ }
+ ],
+ "prompt_number": 7
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "r.highlight(5) # the parameter is a color number"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 8
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "b"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 9,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7fd034190240> >"
+ ]
+ }
+ ],
+ "prompt_number": 9
}
],
"metadata": {}