diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 0560dd12b..0de670db5 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -56,8 +56,9 @@ static const argp_option options[] = "(a) acceptance display, (b) acceptance sets as bullets," "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " "(v) vertical layout, (n) with name, (N) without name, " - "(r) rainbow colors for acceptance set, " - "(R) color acceptance set by Inf/Fin, (s) with SCCs, " + "(o) ordered transitions, " + "(r) rainbow colors for acceptance sets, " + "(R) color acceptance sets by Inf/Fin, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 5df53f4d5..f96084016 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -78,8 +78,9 @@ static const argp_option options[] = "(a) acceptance display, (b) acceptance sets as bullets," "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " "(v) vertical layout, (n) with name, (N) without name, " - "(r) rainbow colors for acceptance set, " - "(R) color acceptance set by Inf/Fin, (s) with SCCs, " + "(o) ordered transitions, " + "(r) rainbow colors for acceptance sets, " + "(R) color acceptance sets by Inf/Fin, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 35b71ed6a..5b58866c9 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -88,6 +88,7 @@ namespace spot case 'b': case 'n': case 'N': + case 'o': case 'r': case 'R': case 's': diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index faf1a5552..904474f55 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -60,6 +60,7 @@ namespace spot bool opt_rainbow = false; bool opt_bullet = false; bool opt_all_bullets = false; + bool opt_numbered_trans = false; std::string opt_font_; const char* const palette9[9] = @@ -137,6 +138,9 @@ namespace spot case 'N': opt_name_ = false; break; + case 'o': + opt_numbered_trans = true; + break; case 'r': opt_html_labels_ = true; opt_rainbow = true; @@ -396,7 +400,7 @@ namespace spot } void - process_link(const tgba_digraph::trans_storage_t& t) + process_link(const tgba_digraph::trans_storage_t& t, int number) { std::string label = bdd_format_formula(aut_->get_dict(), t.cond); os_ << " " << t.src << " -> " << t.dst; @@ -410,7 +414,7 @@ namespace spot os_ << "\\n"; output_set(a); } - os_ << "\"]\n"; + os_ << '"'; } else { @@ -422,8 +426,11 @@ namespace spot os_ << "
"; output_html_set(a); } - os_ << ">]\n"; + os_ << '>'; } + if (opt_numbered_trans) + os_ << ",taillabel=\"" << number << '"'; + os_ << "]\n"; } void print(const const_tgba_digraph_ptr& aut) @@ -471,8 +478,9 @@ namespace spot { if (!si || !si->reachable_state(n)) process_state(n); + int trans_num = 0; for (auto& t: aut_->out(n)) - process_link(t); + process_link(t, trans_num++); } end(); } diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 63479c277..af52809aa 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -464,48 +464,48 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 1 [label="!a & !b"] - 0 -> 2 [label="a & !b"] - 0 -> 3 [label="!a & b"] - 0 -> 4 [label="a & b"] + 0 -> 1 [label="!a & !b",taillabel="0"] + 0 -> 2 [label="a & !b",taillabel="1"] + 0 -> 3 [label="!a & b",taillabel="2"] + 0 -> 4 [label="a & b",taillabel="3"] 1 [label="test me\n⓿❸"] - 1 -> 1 [label="!a & !b"] - 1 -> 2 [label="a & !b"] - 1 -> 6 [label="!a & b"] - 1 -> 7 [label="a & b"] + 1 -> 1 [label="!a & !b",taillabel="0"] + 1 -> 2 [label="a & !b",taillabel="1"] + 1 -> 6 [label="!a & b",taillabel="2"] + 1 -> 7 [label="a & b",taillabel="3"] 2 [label="2\n⓿❷❸"] - 2 -> 1 [label="!a & !b"] - 2 -> 2 [label="a & !b"] - 2 -> 6 [label="!a & b"] - 2 -> 7 [label="a & b"] + 2 -> 1 [label="!a & !b",taillabel="0"] + 2 -> 2 [label="a & !b",taillabel="1"] + 2 -> 6 [label="!a & b",taillabel="2"] + 2 -> 7 [label="a & b",taillabel="3"] 3 [label="3\n❸"] - 3 -> 5 [label="1"] + 3 -> 5 [label="1",taillabel="0"] 4 [label="hihi\n❷❸"] - 4 -> 5 [label="1"] + 4 -> 5 [label="1",taillabel="0"] 5 [label="5\n❶❸"] - 5 -> 5 [label="1"] + 5 -> 5 [label="1",taillabel="0"] 6 [label="6\n⓿"] - 6 -> 8 [label="!a & !b"] - 6 -> 6 [label="!a & b"] - 6 -> 9 [label="a & !b"] - 6 -> 7 [label="a & b"] + 6 -> 8 [label="!a & !b",taillabel="0"] + 6 -> 6 [label="!a & b",taillabel="1"] + 6 -> 9 [label="a & !b",taillabel="2"] + 6 -> 7 [label="a & b",taillabel="3"] 7 [label="7\n⓿❷"] - 7 -> 8 [label="!a & !b"] - 7 -> 6 [label="!a & b"] - 7 -> 9 [label="a & !b"] - 7 -> 7 [label="a & b"] + 7 -> 8 [label="!a & !b",taillabel="0"] + 7 -> 6 [label="!a & b",taillabel="1"] + 7 -> 9 [label="a & !b",taillabel="2"] + 7 -> 7 [label="a & b",taillabel="3"] 8 [label="8\n⓿❸"] - 8 -> 8 [label="!a & !b"] - 8 -> 6 [label="!a & b"] - 8 -> 9 [label="a & !b"] - 8 -> 7 [label="a & b"] + 8 -> 8 [label="!a & !b",taillabel="0"] + 8 -> 6 [label="!a & b",taillabel="1"] + 8 -> 9 [label="a & !b",taillabel="2"] + 8 -> 7 [label="a & b",taillabel="3"] 9 [label="9\n⓿❷❸"] - 9 -> 8 [label="!a & !b"] - 9 -> 6 [label="!a & b"] - 9 -> 9 [label="a & !b"] - 9 -> 7 [label="a & b"] + 9 -> 8 [label="!a & !b",taillabel="0"] + 9 -> 6 [label="!a & b",taillabel="1"] + 9 -> 9 [label="a & !b",taillabel="2"] + 9 -> 7 [label="a & b",taillabel="3"] } EOF -$autfilt --dot=ba in >out +$autfilt --dot=bao in >out diff out expected