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

dot: fix printing of alternating automata

Related to #208.

* spot/twaalgos/dot.cc: Fix missing definitions of universal nodes,
and inclusion of universal nodes inside of SCC when none of the
destination comes back to the SCC.
* tests/python/_altscc.ipynb: Adjust and add more test cases.
* tests/core/alternating.test, tests/core/neverclaimread.test,
tests/core/readsave.test, tests/core/sccdot.test,
tests/python/decompose.ipynb: Adjust test cases.
* NEWS: Mention the bug.
parent 617a7187
...@@ -108,6 +108,11 @@ New in spot 2.3.4.dev (not yet released) ...@@ -108,6 +108,11 @@ New in spot 2.3.4.dev (not yet released)
single ltl2tgba run could produce automata different from those single ltl2tgba run could produce automata different from those
produced by individual runs. produced by individual runs.
- The print_dot() function had a couple of issues when printing
alternating automata: in particular, when using flag 's' (display
SCC) or 'y' (split universal destination by colors) universal
edges could be connected to undefined states.
Backward-incompatible changes: Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as - spot::acc_cond::mark_t::operator bool() has been marked as
......
...@@ -70,6 +70,8 @@ namespace spot ...@@ -70,6 +70,8 @@ namespace spot
std::vector<unsigned>* orig_ = nullptr; std::vector<unsigned>* orig_ = nullptr;
std::set<unsigned>* incomplete_ = nullptr; std::set<unsigned>* incomplete_ = nullptr;
std::string* name_ = nullptr; std::string* name_ = nullptr;
std::map<std::pair<int, int>, int> univ_done;
acc_cond::mark_t inf_sets_ = 0U; acc_cond::mark_t inf_sets_ = 0U;
acc_cond::mark_t fin_sets_ = 0U; acc_cond::mark_t fin_sets_ = 0U;
unsigned opt_shift_sets_ = 0; unsigned opt_shift_sets_ = 0;
...@@ -371,28 +373,39 @@ namespace spot ...@@ -371,28 +373,39 @@ namespace spot
return bdd_format_formula(aut_->get_dict(), label); return bdd_format_formula(aut_->get_dict(), label);
} }
std::set<std::pair<int, int>> done; std::string string_dst(int dst, int color_num = -1)
void
print_dst(int dst, const char* style = nullptr, int scc_num = -1,
int color_num = -1)
{ {
std::ostringstream tmp_dst; std::ostringstream tmp_dst;
tmp_dst << dst; tmp_dst << dst;
if (scc_num >= 0) if (!opt_shared_univ_dest_ && color_num >= 0)
tmp_dst << '.' << scc_num;
if (!done.emplace(std::make_pair(dst, color_num)).second)
return;
else if (!opt_shared_univ_dest_ && color_num > 0)
tmp_dst << '.' << color_num; tmp_dst << '.' << color_num;
std::string dest = tmp_dst.str(); return tmp_dst.str();
os_ << " " << dest << " [label=<>,shape=point]\n"; }
for (unsigned d: aut_->univ_dests(dst))
void
print_dst(int dst, bool print_edges = false,
const char* style = nullptr, int color_num = -1)
{
int& univ = univ_done[std::make_pair(dst, color_num)];
if (univ == 2)
return;
std::string dest = string_dst(dst, color_num);
if (univ == 0)
os_ << " " << dest << " [label=<>,shape=point]\n";
if (print_edges)
{ {
os_ << " " << dest << " -> " << d; for (unsigned d: aut_->univ_dests(dst))
if (style && *style) {
os_ << " [" << style << ']'; os_ << " " << dest << " -> " << d;
os_ << '\n'; if (style && *style)
os_ << " [" << style << ']';
os_ << '\n';
}
univ = 2;
}
else
{
univ = 1;
} }
} }
...@@ -483,14 +496,9 @@ namespace spot ...@@ -483,14 +496,9 @@ namespace spot
int init = (int) aut_->get_init_state_number(); int init = (int) aut_->get_init_state_number();
os_ << "=0]\n I -> " << init; os_ << "=0]\n I -> " << init;
if (init >= 0) if (init >= 0)
{ os_ << '\n';
os_ << '\n';
}
else else
{ os_ << " [arrowhead=onormal]\n";
os_ << " [arrowhead=onormal]\n";
print_dst(init);
}
} }
void void
...@@ -597,63 +605,63 @@ namespace spot ...@@ -597,63 +605,63 @@ namespace spot
void void
process_link(const twa_graph::edge_storage_t& t, int number, process_link(const twa_graph::edge_storage_t& t, int number,
int scc_num = -1) bool print_edges)
{ {
os_ << " " << t.src << " -> " << (int)t.dst; if (print_edges)
if (scc_num >= 0)
{
os_ << '.' << scc_num;
}
if (aut_->is_univ_dest(t.dst) && highlight_edges_
&& !opt_shared_univ_dest_)
{
auto idx = aut_->get_graph().index_of_edge(t);
auto iter = highlight_edges_->find(idx);
os_ << '.' << iter->second % palette_mod;
}
std::string label;
if (!opt_state_labels_)
label = bdd_format_formula(aut_->get_dict(), t.cond);
if (!opt_html_labels_)
{
os_ << " [label=\"";
escape_str(os_, label);
if (!mark_states_)
if (auto a = t.acc)
{
if (!opt_state_labels_)
os_ << "\\n";
output_set(a);
}
os_ << '"';
}
else
{ {
os_ << " [label=<"; os_ << " " << t.src << " -> " << (int)t.dst;
escape_html(os_, label); if (aut_->is_univ_dest(t.dst) && highlight_edges_
if (!mark_states_) && !opt_shared_univ_dest_)
if (auto a = t.acc) {
{ auto idx = aut_->get_graph().index_of_edge(t);
if (!opt_state_labels_) auto iter = highlight_edges_->find(idx);
os_ << "<br/>"; if (iter != highlight_edges_->end())
output_html_set(a); os_ << '.' << iter->second % palette_mod;
} }
os_ << '>'; std::string label;
} if (!opt_state_labels_)
if (opt_ordered_edges_ || opt_numbered_edges_) label = bdd_format_formula(aut_->get_dict(), t.cond);
{ if (!opt_html_labels_)
os_ << ", taillabel=\""; {
if (opt_ordered_edges_) os_ << " [label=\"";
os_ << number; escape_str(os_, label);
if (opt_ordered_edges_ && opt_numbered_edges_) if (!mark_states_)
os_ << ' '; if (auto a = t.acc)
if (opt_numbered_edges_) {
os_ << '#' << aut_->get_graph().index_of_edge(t); if (!opt_state_labels_)
os_ << '"'; os_ << "\\n";
output_set(a);
}
os_ << '"';
}
else
{
os_ << " [label=<";
escape_html(os_, label);
if (!mark_states_)
if (auto a = t.acc)
{
if (!opt_state_labels_)
os_ << "<br/>";
output_html_set(a);
}
os_ << '>';
}
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_ << '"';
}
} }
std::string highlight; std::string highlight;
auto color_num = -1; int color_num = -1;
if (highlight_edges_) if (highlight_edges_)
{ {
auto idx = aut_->get_graph().index_of_edge(t); auto idx = aut_->get_graph().index_of_edge(t);
...@@ -665,21 +673,20 @@ namespace spot ...@@ -665,21 +673,20 @@ namespace spot
<< palette[iter->second % palette_mod] << palette[iter->second % palette_mod]
<< '"'; << '"';
highlight = o.str(); highlight = o.str();
os_ << ", " << highlight; if (print_edges)
os_ << ", " << highlight;
if (!opt_shared_univ_dest_) if (!opt_shared_univ_dest_)
color_num = iter->second % palette_mod; color_num = iter->second % palette_mod;
} }
} }
if (aut_->is_univ_dest(t.dst)) if (print_edges)
os_ << ", arrowhead=onormal";
os_ << "]\n";
if (aut_->is_univ_dest(t.dst))
{ {
if (color_num >= 0) if (aut_->is_univ_dest(t.dst))
print_dst(t.dst, highlight.c_str(), scc_num, color_num); os_ << ", arrowhead=onormal";
else os_ << "]\n";
print_dst(t.dst, highlight.c_str(), scc_num);
} }
if (aut_->is_univ_dest(t.dst))
print_dst(t.dst, print_edges, highlight.c_str(), color_num);
} }
void print(const const_twa_graph_ptr& aut) void print(const const_twa_graph_ptr& aut)
...@@ -787,39 +794,29 @@ namespace spot ...@@ -787,39 +794,29 @@ namespace spot
{ {
process_state(s); process_state(s);
int trans_num = 0; int trans_num = 0;
unsigned scc_of_s = si->scc_of(s);
for (auto& t : aut_->out(s)) for (auto& t : aut_->out(s))
{ for (unsigned d: aut_->univ_dests(t.dst))
if (aut_->is_univ_dest(t.dst)) if (si->scc_of(d) == scc_of_s)
{ {
bool to_write = false; process_link(t, trans_num++, false);
for (unsigned d: aut_->univ_dests(t.dst)) break;
{
to_write = si->scc_of(d) == si->scc_of(s);
if (to_write)
break;
}
if (to_write)
process_link(t, trans_num++, i);
else
process_link(t, trans_num++);
} }
else
process_link(t, trans_num++);
}
} }
os_ << " }\n"; os_ << " }\n";
} }
} }
int init = (int) aut_->get_init_state_number();
if (init < 0)
print_dst(init, true);
unsigned ns = aut_->num_states(); unsigned ns = aut_->num_states();
for (unsigned n = 0; n < ns; ++n) for (unsigned n = 0; n < ns; ++n)
{ {
if (!si || !si->reachable_state(n)) if (!si || !si->reachable_state(n))
{ process_state(n);
process_state(n); int trans_num = 0;
int trans_num = 0; for (auto& t: aut_->out(n))
for (auto& t: aut_->out(n)) process_link(t, trans_num++, true);
process_link(t, trans_num++);
}
} }
end(); end();
} }
......
...@@ -62,66 +62,66 @@ digraph G { ...@@ -62,66 +62,66 @@ digraph G {
labelloc="t" labelloc="t"
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> -11 [arrowhead=onormal] I -> -11 [arrowhead=onormal]
-11 [label=<>,shape=point]
-11 -> 0
-11 -> 2
subgraph cluster_0 { subgraph cluster_0 {
color=green color=green
label="" label=""
2 [label="G(a)"] 2 [label="G(a)"]
2 -> 2 [label="a"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=red color=red
label="" label=""
1 [label="FG(a)\n⓿"] 1 [label="FG(a)\n⓿"]
1 -> 2 [label="a"]
1 -> 1 [label="1"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=green color=green
label="" label=""
6 [label="t"] 6 [label="t"]
6 -> 6 [label="1"]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=red color=red
label="" label=""
4 [label="F(b)\n⓿"] 4 [label="F(b)\n⓿"]
4 -> 6 [label="b"]
4 -> 4 [label="!b"]
} }
subgraph cluster_4 { subgraph cluster_4 {
color=green color=green
label="" label=""
3 [label="GF(b)"] 3 [label="GF(b)"]
3 -> 3 [label="b"] -8 [label=<>,shape=point]
3 -> -8.4 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal]
-8.4 [label=<>,shape=point]
-8.4 -> 3 [style=bold, color="#FAA43A"]
-8.4 -> 4 [style=bold, color="#FAA43A"]
} }
subgraph cluster_5 { subgraph cluster_5 {
color=red color=red
label="" label=""
5 [label="((a) U (b))\n⓿"] 5 [label="((a) U (b))\n⓿"]
5 -> 6 [label="b"]
5 -> 5 [label="a & !b"]
} }
subgraph cluster_6 { subgraph cluster_6 {
color=black color=black
label="" label=""
0 [label="((((a) U (b)) && GF(b)) && FG(a))"] 0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
}
-11 [label=<>,shape=point]
-11 -> 0
-11 -> 2
0 -> -1 [label="b", arrowhead=onormal] 0 -> -1 [label="b", arrowhead=onormal]
-1 [label=<>,shape=point] -1 [label=<>,shape=point]
-1 -> 1 -1 -> 1
-1 -> 3 -1 -> 3
0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal] 0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal]
-4 [label=<>,shape=point] -4 [label=<>,shape=point]
-4 -> 1 [style=bold, color="#F15854"] -4 -> 1 [style=bold, color="#F15854"]
-4 -> 3 [style=bold, color="#F15854"] -4 -> 3 [style=bold, color="#F15854"]
-4 -> 5 [style=bold, color="#F15854"] -4 -> 5 [style=bold, color="#F15854"]
} 1 -> 2 [label="a"]
1 -> 1 [label="1"]
2 -> 2 [label="a"]
3 -> 3 [label="b"]
3 -> -8 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal]
-8 -> 3 [style=bold, color="#FAA43A"]
-8 -> 4 [style=bold, color="#FAA43A"]
4 -> 6 [label="b"]
4 -> 4 [label="!b"]
5 -> 6 [label="b"]
5 -> 5 [label="a & !b"]
6 -> 6 [label="1"]
} }
EOF EOF
...@@ -508,19 +508,19 @@ digraph G { ...@@ -508,19 +508,19 @@ digraph G {
edge [fontname="Lato"] edge [fontname="Lato"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> -1 [arrowhead=onormal] I -> -1 [arrowhead=onormal]
-1 [label=<>,shape=point] -1 [label=<>,shape=point]
-1 -> 0 -1 -> 0
-1 -> 1 -1 -> 1
0 [label=<0>] 0 [label=<0>]
0 -> 0 [label=<!a &amp; !c>] 0 -> 0 [label=<!a &amp; !c>]
0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", $style] 0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", $style]
-1.1 [label=<>,shape=point] -1.1 [label=<>,shape=point]
-1.1 -> 0 [style=bold, color="#F17CB0"] -1.1 -> 0 [style=bold, color="#F17CB0"]
-1.1 -> 1 [style=bold, color="#F17CB0"] -1.1 -> 1 [style=bold, color="#F17CB0"]
0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", $style] 0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point] -1.2 [label=<>,shape=point]
-1.2 -> 0 [style=bold, color="#FAA43A"] -1.2 -> 0 [style=bold, color="#FAA43A"]
-1.2 -> 1 [style=bold, color="#FAA43A"] -1.2 -> 1 [style=bold, color="#FAA43A"]
1 [label=<1>] 1 [label=<1>]
1 -> 1 [label=<b>] 1 -> 1 [label=<b>]
} }
...@@ -574,52 +574,52 @@ digraph G { ...@@ -574,52 +574,52 @@ digraph G {
color=green color=green
label="" label=""
4 [label="t"] 4 [label="t"]
4 -> 4 [label=<1>]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=green color=green
label="" label=""
1 [label="G(a & b)"] 1 [label="G(a & b)"]
1 -> 1 [label=<a &amp; b>]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=red color=red
label="" label=""
2 [label="F!a"] 2 [label="F!a"]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=red color=red
label="" label=""
3 [label="F!b"] 3 [label="F!b"]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
} }
subgraph cluster_4 { subgraph cluster_4 {
color=green color=green
label="" label=""
0 [label="c R (c | G(a & b) | (F!b & F!a))"] 0 [label="c R (c | G(a & b) | (F!b & F!a))"]
-1 [label=<>,shape=point]
-4 [label=<>,shape=point]
-7 [label=<>,shape=point]
-10 [label=<>,shape=point]
}
0 -> 4 [label=<c>] 0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>] 0 -> 0 [label=<!a &amp; !b &amp; !c>]
0 -> -1.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal] 0 -> -1 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1.4 [label=<>,shape=point] -1 -> 0
-1.4 -> 0 -1 -> 1
-1.4 -> 1 0 -> -4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
0 -> -4.4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal] -4 -> 0
-4.4 [label=<>,shape=point] -4 -> 2
-4.4 -> 0 0 -> -7 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-4.4 -> 2 -7 -> 0
0 -> -7.4 [label=<!a &amp; b &amp; !c>, arrowhead=onormal] -7 -> 3
-7.4 [label=<>,shape=point] 0 -> -10 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-7.4 -> 0 -10 -> 0
-7.4 -> 3 -10 -> 2
0 -> -10.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal] -10 -> 3
-10.4 [label=<>,shape=point] 1 -> 1 [label=<a &amp; b>]
-10.4 -> 0 2 -> 4 [label=<!a>]
-10.4 -> 2 2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
-10.4 -> 3 3 -> 4 [label=<!b>]
} 3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
4 -> 4 [label=<1>]
} }
EOF EOF
...@@ -670,48 +670,48 @@ digraph G { ...@@ -670,48 +670,48 @@ digraph G {
color=green color=green
label="" label=""
4 [label="t"] 4 [label="t"]
4 -> 4 [label=<1>]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=red