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

twa_graph: honor state-names & product-states in format_state()

* spot/twa/twagraph.cc, spot/twa/twagraph.hh (format_state): Honor
the state-names and product-states properties.
* tests/python/highlighting.ipynb: Adjust.
parent 46d8aaaa
......@@ -19,9 +19,44 @@
#include <spot/twa/twagraph.hh>
#include <spot/tl/print.hh>
#include <vector>
namespace spot
{
std::string twa_graph::format_state(unsigned n) const
{
if (is_univ_dest(n))
{
std::stringstream ss;
bool notfirst = false;
for (unsigned d: univ_dests(n))
{
if (notfirst)
ss << '&';
notfirst = true;
ss << format_state(d);
}
return ss.str();
}
auto named = get_named_prop<std::vector<std::string>>("state-names");
if (named && n < named->size())
return (*named)[n];
auto prod = get_named_prop
<std::vector<std::pair<unsigned, unsigned>>>("product-states");
if (prod && n < prod->size())
{
auto& p = (*prod)[n];
std::stringstream ss;
ss << p.first << ',' << p.second;
return ss.str();
}
return std::to_string(n);
}
void
twa_graph::release_formula_namer(namer<formula>* namer,
bool keep_names)
......
......@@ -336,26 +336,7 @@ namespace spot
return &g_.state_data(n);
}
std::string format_state(unsigned n) const
{
std::stringstream ss;
if (is_univ_dest(n))
{
bool notfirst = false;
for (unsigned d: univ_dests(n))
{
if (notfirst)
ss << '&';
notfirst = true;
ss << d;
}
}
else
{
ss << n;
}
return ss.str();
}
std::string format_state(unsigned n) const;
virtual std::string format_state(const state* st) const override
{
......
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