Commit 23c2cbf4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent be441825
...@@ -64,3 +64,5 @@ real notebooks instead. ...@@ -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 - [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=ltsmin.ipynb=]] minimal test for loading a DiVinE model using
the LTSmin interface. 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][=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.
...@@ -147,6 +147,15 @@ class twa: ...@@ -147,6 +147,15 @@ class twa:
from IPython.display import SVG from IPython.display import SVG
return SVG(self._repr_svg_(opt)) 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) @_extend(twa)
class twa: class twa:
......
...@@ -546,6 +546,32 @@ namespace std { ...@@ -546,6 +546,32 @@ namespace std {
{ {
return self->get_named_prop<std::vector<std::string>>("state-names"); return self->get_named_prop<std::vector<std::string>>("state-names");
} }
twa* highlight_state(unsigned state, unsigned color)
{
auto hs =
self->get_named_prop<std::map<unsigned, unsigned>>("highlight-states");
if (!hs)
{
hs = new std::map<unsigned, unsigned>;
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<std::map<unsigned, unsigned>>("highlight-edges");
if (!ht)
{
ht = new std::map<unsigned, unsigned>;
self->set_named_prop("highlight-edges", ht);
}
(*ht)[edge] = color;
return self;
}
} }
......
...@@ -107,6 +107,7 @@ namespace spot ...@@ -107,6 +107,7 @@ namespace spot
case 't': case 't':
case '+': case '+':
case '<': case '<':
case '#':
// All these options are implemented by dotty() on TGBA, // All these options are implemented by dotty() on TGBA,
// but are not implemented here. We simply ignore them, // but are not implemented here. We simply ignore them,
// because raising an exception if they are in // because raising an exception if they are in
......
...@@ -71,6 +71,7 @@ namespace spot ...@@ -71,6 +71,7 @@ namespace spot
bool opt_bullet_but_buchi = false; bool opt_bullet_but_buchi = false;
bool opt_all_bullets = false; bool opt_all_bullets = false;
bool opt_ordered_edges_ = false; bool opt_ordered_edges_ = false;
bool opt_numbered_edges_ = false;
bool opt_want_state_names_ = true; bool opt_want_state_names_ = true;
unsigned opt_shift_sets_ = 0; unsigned opt_shift_sets_ = 0;
std::string opt_font_; std::string opt_font_;
...@@ -160,6 +161,9 @@ namespace spot ...@@ -160,6 +161,9 @@ namespace spot
options = end; options = end;
break; break;
} }
case '#':
opt_numbered_edges_ = true;
break;
case '1': case '1':
opt_want_state_names_ = false; opt_want_state_names_ = false;
break; break;
...@@ -550,8 +554,17 @@ namespace spot ...@@ -550,8 +554,17 @@ namespace spot
} }
os_ << '>'; os_ << '>';
} }
if (opt_ordered_edges_) if (opt_ordered_edges_ || opt_numbered_edges_)
os_ << ", taillabel=\"" << number << '"'; {
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_) if (highlight_edges_)
{ {
auto idx = aut_->get_graph().index_of_edge(t); auto idx = aut_->get_graph().index_of_edge(t);
......
...@@ -291,6 +291,7 @@ TESTS_python = \ ...@@ -291,6 +291,7 @@ TESTS_python = \
python/bddnqueen.py \ python/bddnqueen.py \
python/decompose.ipynb \ python/decompose.ipynb \
python/formulas.ipynb \ python/formulas.ipynb \
python/highlighting.ipynb \
python/implies.py \ python/implies.py \
python/interdep.py \ python/interdep.py \
python/ltl2tgba.test \ python/ltl2tgba.test \
......
This diff is collapsed.
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