Commit e1465278 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

twa_run: add a highlight method

* spot/twaalgos/emptiness.hh, spot/twaalgos/emptiness.cc: Add
the method.
* tests/python/highlighting.ipynb: Add a small test.
parent 77b0b5b3
......@@ -21,6 +21,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <sstream>
#include <memory>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/gtec/gtec.hh>
......@@ -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<twa_graph>
(std::const_pointer_cast<twa>(aut));
if (!a)
throw std::runtime_error("highlight() only work for twa_graph");
auto h = new std::map<unsigned, unsigned>; // 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
{
......
// -*- 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.
......
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