diff --git a/NEWS b/NEWS index d63e07b4c..f42fcfc43 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,9 @@ New in spot 2.3.0.dev (not yet released) - The colors used in the output of ltlcross have been adjusted to work better with white backgrounds and black backgrounds. + - The option (y) has been added to --dot. It splits the universal + edges with the same targets but different colors. + Library: - spot::twa_run::as_twa() has an option to preserve state names. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 534a8fbed..ce0944b2c 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -85,7 +85,7 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Output format:", 3 }, { "dot", 'd', - "1|a|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|+INT| #include #include +#include namespace spot @@ -95,6 +96,8 @@ namespace spot bool opt_want_state_names_ = true; unsigned max_states_ = -1U; // related to max_states_given_ + bool opt_shared_univ_dest_ = true; + public: unsigned max_states() @@ -244,6 +247,9 @@ namespace spot case 't': opt_force_acc_trans_ = true; break; + case 'y': + opt_shared_univ_dest_ = false; + break; default: throw std::runtime_error (std::string("unknown option for print_dot(): ") + c); @@ -360,17 +366,24 @@ namespace spot return bdd_format_formula(aut_->get_dict(), label); } - std::set done; + std::set> done; void - print_dst(int dst, const char* style = nullptr) + print_dst(int dst, const char* style = nullptr, int color_num = -1) { - if (!done.emplace(dst).second) + 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; - os_ << " " << dst << " [label=<>,shape=point]\n"; + else 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)) { - os_ << " " << dst << " -> " << d; + os_ << " " << dest << " -> " << d; if (style && *style) os_ << " [" << style << ']'; os_ << '\n'; @@ -574,6 +587,13 @@ namespace spot process_link(const twa_graph::edge_storage_t& t, int number) { 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); + os_ << '.' << iter->second % palette_mod; + } std::string label; if (!opt_state_labels_) label = bdd_format_formula(aut_->get_dict(), t.cond); @@ -616,6 +636,7 @@ namespace spot } std::string highlight; + auto color_num = -1; if (highlight_edges_) { auto idx = aut_->get_graph().index_of_edge(t); @@ -628,13 +649,20 @@ namespace spot << '"'; highlight = o.str(); 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)) - print_dst(t.dst, highlight.c_str()); + { + if (color_num >= 0) + print_dst(t.dst, highlight.c_str(), color_num); + else + print_dst(t.dst, highlight.c_str()); + } } void print(const const_twa_graph_ptr& aut) diff --git a/tests/core/alternating.test b/tests/core/alternating.test old mode 100644 new mode 100755 index 86069a866..7f20b953f --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -353,6 +353,343 @@ State: 0 EOF diff out5 expect +# Test if split option is correct +cat >ex6< ex6.dot + +cat >expect6.dot<⓿)> + labelloc="t" + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> -1 [arrowhead=onormal] + -1 [label=<>,shape=point] + -1 -> 0 + -1 -> 1 + 0 [label=<0>] + 0 -> 0 [label=] + 0 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] + -1.1 [label=<>,shape=point] + -1.1 -> 0 [style=bold, color="#F17CB0"] + -1.1 -> 1 [style=bold, color="#F17CB0"] + 0 -> -1.2 [label=, style=bold, color="#FAA43A", arrowhead=onormal] + -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=] +} +EOF + +diff ex6.dot expect6.dot + +cat >ex7< ex7.dot + +color='⓿' +cat >expect7.dot<❶) & Fin($color)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + subgraph cluster_0 { + color=green + label="" + 4 [label="t"] + 4 -> 4 [label=<1>] + } + subgraph cluster_1 { + color=green + label="" + 1 [label="G(a & b)"] + 1 -> 1 [label=] + } + subgraph cluster_2 { + color=red + label="" + 2 [label="F!a"] + 2 -> 4 [label=] + 2 -> 2 [label=❶>] + } + subgraph cluster_3 { + color=red + label="" + 3 [label="F!b"] + 3 -> 4 [label=] + 3 -> 3 [label=⓿>] + } + subgraph cluster_4 { + color=green + label="" + 0 [label="c R (c | G(a & b) | (F!b & F!a))"] + 0 -> 4 [label=] + 0 -> 0 [label=] + 0 -> -1.4 [label=, arrowhead=onormal] + -1.4 [label=<>,shape=point] + -1.4 -> 0 + -1.4 -> 1 + 0 -> -4.4 [label=, arrowhead=onormal] + -4.4 [label=<>,shape=point] + -4.4 -> 0 + -4.4 -> 2 + 0 -> -7.4 [label=, arrowhead=onormal] + -7.4 [label=<>,shape=point] + -7.4 -> 0 + -7.4 -> 3 + 0 -> -10.4 [label=, arrowhead=onormal] + -10.4 [label=<>,shape=point] + -10.4 -> 0 + -10.4 -> 2 + -10.4 -> 3 + } +} +EOF + +diff ex7.dot expect7.dot + +cat >ex8< ex8.dot + +cat >expect8.dot<❶) & Fin($color)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + subgraph cluster_0 { + color=green + label="" + 4 [label="t"] + 4 -> 4 [label=<1>] + } + subgraph cluster_1 { + color=red + label="" + 2 [label="F!a"] + 2 -> 4 [label=] + 2 -> 2 [label=❶>] + } + subgraph cluster_2 { + color=red + label="" + 3 [label="F!b"] + 3 -> 4 [label=] + 3 -> 3 [label=⓿>] + } + subgraph cluster_3 { + color=green + label="" + 0 [label="c R (c | G(a & b) | (F!b & F!a))"] + 0 -> 4 [label=] + 0 -> 0 [label=] + 0 -> -1.3 [label=, arrowhead=onormal] + -1.3 [label=<>,shape=point] + -1.3 -> 0 + -1.3 -> 1 + 0 -> -4.3 [label=, arrowhead=onormal] + -4.3 [label=<>,shape=point] + -4.3 -> 0 + -4.3 -> 2 + 0 -> -7.3 [label=, arrowhead=onormal] + -7.3 [label=<>,shape=point] + -7.3 -> 0 + -7.3 -> 3 + 1 [label="G(a & b)"] + 1 -> 1 [label=] + 1 -> -10.3 [label=, arrowhead=onormal] + -10.3 [label=<>,shape=point] + -10.3 -> 0 + -10.3 -> 2 + -10.3 -> 3 + } +} +EOF + +diff ex8.dot expect8.dot + +cat >ex9 < ex9.dot + +cat >expect9.dot <⓿)> + labelloc="t" + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label=<0>] + 0 -> -1.1 [label=, 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 [label=<1>] + 1 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] + 2 [label=<2>] + 2 -> -1.2 [label=, style=bold, color="#FAA43A", $style] + -1.2 [label=<>,shape=point] + -1.2 -> 1 [style=bold, color="#FAA43A"] + -1.2 -> 2 [style=bold, color="#FAA43A"] +} +EOF + +diff ex9.dot expect9.dot + +cat >ex10 < ex10.dot + +cat >expect10.dot <⓿)> + labelloc="t" + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label=<0>] + 0 -> -1.1 [label=, 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 [label=<1>] + 1 -> -1.3 [label=, 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"] + 2 [label=<2>] + 2 -> -1.2 [label=, style=bold, color="#FAA43A", $style] + -1.2 [label=<>,shape=point] + -1.2 -> 1 [style=bold, color="#FAA43A"] + -1.2 -> 2 [style=bold, color="#FAA43A"] +} +EOF + +diff ex10.dot expect10.dot + # Detect cases where alternation-removal cannot work. cat >in <