Commit 7b6cfd44 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 f6607f1a
......@@ -6,6 +6,11 @@ New in spot 2.3.4.dev (not yet released)
single ltl2tgba run could produce automata different from those
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.
New in spot 2.3.4 (2017-05-11)
Bugs fixed:
......
......@@ -69,6 +69,8 @@ namespace spot
std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
std::set<unsigned>* incomplete_ = 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 fin_sets_ = 0U;
unsigned opt_shift_sets_ = 0;
......@@ -366,28 +368,39 @@ namespace spot
return bdd_format_formula(aut_->get_dict(), label);
}
std::set<std::pair<int, int>> done;
void
print_dst(int dst, const char* style = nullptr, int scc_num = -1,
int color_num = -1)
std::string string_dst(int dst, int color_num = -1)
{
std::ostringstream tmp_dst;
tmp_dst << dst;
if (scc_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)
if (!opt_shared_univ_dest_ && color_num >= 0)
tmp_dst << '.' << color_num;
std::string dest = tmp_dst.str();
os_ << " " << dest << " [label=<>,shape=point]\n";
for (unsigned d: aut_->univ_dests(dst))
return tmp_dst.str();
}
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;
if (style && *style)
os_ << " [" << style << ']';
os_ << '\n';
for (unsigned d: aut_->univ_dests(dst))
{
os_ << " " << dest << " -> " << d;
if (style && *style)
os_ << " [" << style << ']';
os_ << '\n';
}
univ = 2;
}
else
{
univ = 1;
}
}
......@@ -478,14 +491,9 @@ namespace spot
int init = (int) aut_->get_init_state_number();
os_ << "=0]\n I -> " << init;
if (init >= 0)
{
os_ << '\n';
}
os_ << '\n';
else
{
os_ << " [arrowhead=onormal]\n";
print_dst(init);
}
os_ << " [arrowhead=onormal]\n";
}
void
......@@ -586,63 +594,63 @@ namespace spot
void
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 (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
if (print_edges)
{
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_ << '"';
os_ << " " << t.src << " -> " << (int)t.dst;
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);
if (iter != highlight_edges_->end())
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=<";
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;
auto color_num = -1;
int color_num = -1;
if (highlight_edges_)
{
auto idx = aut_->get_graph().index_of_edge(t);
......@@ -654,21 +662,20 @@ namespace spot
<< palette[iter->second % palette_mod]
<< '"';
highlight = o.str();
os_ << ", " << highlight;
if (print_edges)
os_ << ", " << highlight;
if (!opt_shared_univ_dest_)
color_num = iter->second % palette_mod;
}
}
if (aut_->is_univ_dest(t.dst))
os_ << ", arrowhead=onormal";
os_ << "]\n";
if (aut_->is_univ_dest(t.dst))
if (print_edges)
{
if (color_num >= 0)
print_dst(t.dst, highlight.c_str(), scc_num, color_num);
else
print_dst(t.dst, highlight.c_str(), scc_num);
if (aut_->is_univ_dest(t.dst))
os_ << ", arrowhead=onormal";
os_ << "]\n";
}
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)
......@@ -773,39 +780,29 @@ namespace spot
{
process_state(s);
int trans_num = 0;
unsigned scc_of_s = si->scc_of(s);
for (auto& t : aut_->out(s))
{
if (aut_->is_univ_dest(t.dst))
for (unsigned d: aut_->univ_dests(t.dst))
if (si->scc_of(d) == scc_of_s)
{
bool to_write = false;
for (unsigned d: aut_->univ_dests(t.dst))
{
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++);
process_link(t, trans_num++, false);
break;
}
else
process_link(t, trans_num++);
}
}
os_ << " }\n";
}
}
int init = (int) aut_->get_init_state_number();
if (init < 0)
print_dst(init, true);
unsigned ns = aut_->num_states();
for (unsigned n = 0; n < ns; ++n)
{
if (!si || !si->reachable_state(n))
{
process_state(n);
int trans_num = 0;
for (auto& t: aut_->out(n))
process_link(t, trans_num++);
}
process_state(n);
int trans_num = 0;
for (auto& t: aut_->out(n))
process_link(t, trans_num++, true);
}
end();
}
......
......@@ -62,66 +62,66 @@ digraph G {
labelloc="t"
I [label="", style=invis, width=0]
I -> -11 [arrowhead=onormal]
-11 [label=<>,shape=point]
-11 -> 0
-11 -> 2
subgraph cluster_0 {
color=green
label=""
2 [label="G(a)"]
2 -> 2 [label="a"]
}
subgraph cluster_1 {
color=red
label=""
1 [label="FG(a)\n⓿"]
1 -> 2 [label="a"]
1 -> 1 [label="1"]
}
subgraph cluster_2 {
color=green
label=""
6 [label="t"]
6 -> 6 [label="1"]
}
subgraph cluster_3 {
color=red
label=""
4 [label="F(b)\n⓿"]
4 -> 6 [label="b"]
4 -> 4 [label="!b"]
}
subgraph cluster_4 {
color=green
label=""
3 [label="GF(b)"]
3 -> 3 [label="b"]
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"]
-8 [label=<>,shape=point]
}
subgraph cluster_5 {
color=red
label=""
5 [label="((a) U (b))\n⓿"]
5 -> 6 [label="b"]
5 -> 5 [label="a & !b"]
}
subgraph cluster_6 {
color=black
label=""
0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
}
-11 [label=<>,shape=point]
-11 -> 0
-11 -> 2
0 -> -1 [label="b", arrowhead=onormal]
-1 [label=<>,shape=point]
-1 -> 1
-1 -> 3
-1 [label=<>,shape=point]
-1 -> 1
-1 -> 3
0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal]
-4 [label=<>,shape=point]
-4 -> 1 [style=bold, color="#F15854"]
-4 -> 3 [style=bold, color="#F15854"]
-4 -> 5 [style=bold, color="#F15854"]
}
-4 [label=<>,shape=point]
-4 -> 1 [style=bold, color="#F15854"]
-4 -> 3 [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
......@@ -508,19 +508,19 @@ digraph G {
edge [fontname="Lato"]
I [label="", style=invis, width=0]
I -> -1 [arrowhead=onormal]
-1 [label=<>,shape=point]
-1 -> 0
-1 -> 1
-1 [label=<>,shape=point]
-1 -> 0
-1 -> 1
0 [label=<0>]
0 -> 0 [label=<!a &amp; !c>]
0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", $style]
-1.1 [label=<>,shape=point]
-1.1 -> 0 [style=bold, color="#F17CB0"]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 [label=<>,shape=point]
-1.1 -> 0 [style=bold, color="#F17CB0"]
-1.1 -> 1 [style=bold, color="#F17CB0"]
0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point]
-1.2 -> 0 [style=bold, color="#FAA43A"]
-1.2 -> 1 [style=bold, color="#FAA43A"]
-1.2 [label=<>,shape=point]
-1.2 -> 0 [style=bold, color="#FAA43A"]
-1.2 -> 1 [style=bold, color="#FAA43A"]
1 [label=<1>]
1 -> 1 [label=<b>]
}
......@@ -574,52 +574,52 @@ digraph G {
color=green
label=""
4 [label="t"]
4 -> 4 [label=<1>]
}
subgraph cluster_1 {
color=green
label=""
1 [label="G(a & b)"]
1 -> 1 [label=<a &amp; b>]
}
subgraph cluster_2 {
color=red
label=""
2 [label="F!a"]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
}
subgraph cluster_3 {
color=red
label=""
3 [label="F!b"]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
}
subgraph cluster_4 {
color=green
label=""
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 -> 0 [label=<!a &amp; !b &amp; !c>]
0 -> -1.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1.4 [label=<>,shape=point]
-1.4 -> 0
-1.4 -> 1
0 -> -4.4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4.4 [label=<>,shape=point]
-4.4 -> 0
-4.4 -> 2
0 -> -7.4 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7.4 [label=<>,shape=point]
-7.4 -> 0
-7.4 -> 3
0 -> -10.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10.4 [label=<>,shape=point]
-10.4 -> 0
-10.4 -> 2
-10.4 -> 3
}
0 -> -1 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1 -> 0
-1 -> 1
0 -> -4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4 -> 0
-4 -> 2
0 -> -7 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7 -> 0
-7 -> 3
0 -> -10 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10 -> 0
-10 -> 2
-10 -> 3
1 -> 1 [label=<a &amp; b>]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
4 -> 4 [label=<1>]
}
EOF
......@@ -670,48 +670,48 @@ digraph G {
color=green
label=""
4 [label="t"]
4 -> 4 [label=<1>]
}
subgraph cluster_1 {
color=red
label=""
2 [label="F!a"]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
}
subgraph cluster_2 {
color=red
label=""
3 [label="F!b"]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
}
subgraph cluster_3 {
color=green
label=""
0 [label="c R (c | G(a & b) | (F!b & F!a))"]
-1 [label=<>,shape=point]
-4 [label=<>,shape=point]
-7 [label=<>,shape=point]
1 [label="G(a & b)"]
-10 [label=<>,shape=point]
}
0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>]
0 -> -1.3 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 -> 0
-1.3 -> 1
0 -> -4.3 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4.3 [label=<>,shape=point]
-4.3 -> 0
-4.3 -> 2
0 -> -7.3 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7.3 [label=<>,shape=point]
-7.3 -> 0
-7.3 -> 3
1 [label="G(a & b)"]
0 -> -1 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1 -> 0
-1 -> 1
0 -> -4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4 -> 0
-4 -> 2
0 -> -7 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7 -> 0
-7 -> 3
1 -> 1 [label=<a &amp; b>]
1 -> -10.3 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10.3 [label=<>,shape=point]
-10.3 -> 0
-10.3 -> 2
-10.3 -> 3
}
1 -> -10 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10 -> 0
-10 -> 2
-10 -> 3
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
4 -> 4 [label=<1>]
}
EOF
......@@ -749,16 +749,16 @@ digraph G {
I -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#F17CB0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
1 [label=<1>]
1 -> -1.1 [label=<a &amp; b>, style=bold, color="#F17CB0", arrowhead=onormal]
2 [label=<2>]
2 -> -1.2 [label=<!a &amp; !b &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point]
-1.2 -> 1 [style=bold, color="#FAA43A"]
-1.2 -> 2 [style=bold, color="#FAA43A"]
-1.2 [label=<>,shape=point]
-1.2 -> 1 [style=bold, color="#FAA43A"]
-1.2 -> 2 [style=bold, color="#FAA43A"]
}
EOF
......@@ -796,19 +796,19 @@ digraph G {
I -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#F17CB0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
1 [label=<1>]
1 -> -1.3 [label=<a &amp; b>, style=bold, color="#B276B2", arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 -> 1 [style=bold, color="#B276B2"]
-1.3 -> 2 [style=bold, color="#B276B2"]