diff --git a/NEWS b/NEWS index 9f4f3c85d..d7c9ded5a 100644 --- a/NEWS +++ b/NEWS @@ -53,6 +53,13 @@ New in spot 1.99.5a (not yet released) with spot.product() or spot.product_or() and in the shell with autfilt's --product or --product-or options. + * The print_dot() function supports a new option, +N, where N is a + positive integer that will be added to all set numbers in the + output. This is convenient when displaying two automata before + building their product: use +N to shift the displayed sets of the + second automaton by the number of acceptance sets N of the first + one. + * Renamings: is_guarantee_automaton() -> is_terminal_automaton() tgba_run -> twa_run diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index ac6ee52f1..811412e02 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -84,7 +84,7 @@ static const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v", + { "dot", OPT_DOT, "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for " "(1) force numbered states, " @@ -96,7 +96,8 @@ static const argp_option options[] = "(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 }, + "(t) force transition-based acceptance, " + "(+INT) add INT to all set numbers", 0 }, { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(i) use implicit labels for complete deterministic automata, " diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc index e9de09c3f..0910a120a 100644 --- a/src/twaalgos/dot.cc +++ b/src/twaalgos/dot.cc @@ -66,6 +66,7 @@ namespace spot bool opt_all_bullets = false; bool opt_numbered_trans = false; bool opt_want_state_names_ = true; + unsigned opt_shift_sets_ = 0; std::string opt_font_; const char* const palette9[9] = @@ -112,6 +113,16 @@ namespace spot parse_opts(def.c_str()); break; } + case '+': + { + char* end; + opt_shift_sets_ = strtoul(options, &end, 10); + if (options == end) + throw std::runtime_error + ("missing number after '+' in print_dot() options"); + options = end; + break; + } case '1': opt_want_state_names_ = false; break; @@ -189,6 +200,7 @@ namespace spot void output_set(std::ostream& os, int v) const { + v += opt_shift_sets_; if (opt_bullet && (v >= 0) & (v <= MAX_BULLET)) { static const char* const tab[MAX_BULLET + 1] = { @@ -228,7 +240,7 @@ namespace spot html_set_color(int v) const { if (opt_rainbow) - return palette[v % palette_mod]; + return palette[(v + opt_shift_sets_) % palette_mod]; // Color according to Fin/Inf if (inf_sets_.has(v)) { diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index c576294be..74f0c9b08 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -177,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7faee805b4b0> >" + " *' at 0x7f3c25174540> >" ] } ], @@ -569,7 +569,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042780> >" + " *' at 0x7f3c2515b810> >" ] } ], @@ -639,7 +639,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042600> >" + " *' at 0x7f3c2515b690> >" ] } ], @@ -715,7 +715,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042660> >" + " *' at 0x7f3c2515b6f0> >" ] } ], @@ -1175,7 +1175,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042d80> >" + " *' at 0x7f3c2515be10> >" ] } ], @@ -1276,7 +1276,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042e40> >" + " *' at 0x7f3c2515bed0> >" ] } ], @@ -1394,7 +1394,7 @@ "\n" ], "text": [ - " *' at 0x7faee80425a0> >" + " *' at 0x7f3c2515b630> >" ] } ], @@ -1493,7 +1493,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042630> >" + " *' at 0x7f3c2515b6c0> >" ] } ], @@ -1963,7 +1963,7 @@ "\n" ], "text": [ - " *' at 0x7faee80423c0> >" + " *' at 0x7f3c2515b450> >" ] } ], @@ -2578,7 +2578,7 @@ "\n" ], "text": [ - " *' at 0x7faee8042ed0> >" + " *' at 0x7f3c2515b840> >" ] } ], @@ -2734,7 +2734,7 @@ "\n" ], "text": [ - " *' at 0x7faee80426c0> >" + " *' at 0x7f3c250f61e0> >" ] } ], @@ -2804,7 +2804,7 @@ "\n" ], "text": [ - " *' at 0x7faedb3750f0> >" + " *' at 0x7f3c250f6150> >" ] } ], @@ -2814,9 +2814,11 @@ "cell_type": "code", "collapsed": false, "input": [ + "# Using +1 in the display options is a convient way to shift the \n", + "# set numbers in the output, as an aid in reading the product.\n", "a1 = spot.translate('a W c'); display(a1.show('.bat'))\n", - "a2 = spot.translate('a U b'); display(a2.show('.bat'))\n", - "# the product should display pairs of states, unless asked not to\n", + "a2 = spot.translate('a U b'); display(a2.show('.bat+1'))\n", + "# the product should display pairs of states, unless asked not to (using 1).\n", "p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))" ], "language": "python", @@ -2886,7 +2888,7 @@ "G\n", "\n", "Inf(\n", - "\u24ff\n", + "\u2776\n", ")\n", "\n", "\n", @@ -2921,7 +2923,7 @@ "\n", "\n", "1\n", - "\u24ff\n", + "\u2776\n", "\n", "\n", ""