alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

dot: add support for option +N

Browse source 
* src/twaalgos/dot.cc: Here.
* NEWS, src/bin/common_aoutput.cc: Document it.
* wrap/python/tests/automata.ipynb: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-11-14 14:49:31 +01:00
parent f86beb3c68
commit b3ff5655fb
4 changed files with 41 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -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 with spot.product() or spot.product_or() and in the shell with
autfilt's --product or --product-or options. 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: * Renamings:
is_guarantee_automaton() -> is_terminal_automaton() is_guarantee_automaton() -> is_terminal_automaton()
tgba_run -> twa_run tgba_run -> twa_run

5
src/bin/common_aoutput.cc
View file

@ -84,7 +84,7 @@ static const argp_option options[] =
{ {
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Output format:", 3 }, { 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, OPTION_ARG_OPTIONAL,
"GraphViz's format (default). Add letters for " "GraphViz's format (default). Add letters for "
"(1) force numbered states, " "(1) force numbered states, "
@ -96,7 +96,8 @@ static const argp_option options[] =
"(o) ordered transitions, " "(o) ordered transitions, "
"(r) rainbow colors for acceptance sets, " "(r) rainbow colors for acceptance sets, "
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, " "(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, { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format. Add letters to select " "Output the automaton in HOA format. Add letters to select "
"(i) use implicit labels for complete deterministic automata, " "(i) use implicit labels for complete deterministic automata, "

14
src/twaalgos/dot.cc
View file

@ -66,6 +66,7 @@ namespace spot
bool opt_all_bullets = false; bool opt_all_bullets = false;
bool opt_numbered_trans = false; bool opt_numbered_trans = false;
bool opt_want_state_names_ = true; bool opt_want_state_names_ = true;
unsigned opt_shift_sets_ = 0;
std::string opt_font_; std::string opt_font_;
const char* const palette9[9] = const char* const palette9[9] =
@ -112,6 +113,16 @@ namespace spot
parse_opts(def.c_str()); parse_opts(def.c_str());
break; 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': case '1':
opt_want_state_names_ = false; opt_want_state_names_ = false;
break; break;
@ -189,6 +200,7 @@ namespace spot
void void
output_set(std::ostream& os, int v) const output_set(std::ostream& os, int v) const
{ {
v += opt_shift_sets_;
if (opt_bullet && (v >= 0) & (v <= MAX_BULLET)) if (opt_bullet && (v >= 0) & (v <= MAX_BULLET))
{ {
static const char* const tab[MAX_BULLET + 1] = { static const char* const tab[MAX_BULLET + 1] = {
@ -228,7 +240,7 @@ namespace spot
html_set_color(int v) const html_set_color(int v) const
{ {
if (opt_rainbow) if (opt_rainbow)
return palette[v % palette_mod]; return palette[(v + opt_shift_sets_) % palette_mod];
// Color according to Fin/Inf // Color according to Fin/Inf
if (inf_sets_.has(v)) if (inf_sets_.has(v))
{ {

34
wrap/python/tests/automata.ipynb
View file

@ -177,7 +177,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee805b4b0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c25174540> >"
] ]
} }
], ],
@ -569,7 +569,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042780> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b810> >"
] ]
} }
], ],
@ -639,7 +639,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042600> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b690> >"
] ]
} }
], ],
@ -715,7 +715,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042660> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b6f0> >"
] ]
} }
], ],
@ -1175,7 +1175,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042d80> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515be10> >"
] ]
} }
], ],
@ -1276,7 +1276,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042e40> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515bed0> >"
] ]
} }
], ],
@ -1394,7 +1394,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80425a0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b630> >"
] ]
} }
], ],
@ -1493,7 +1493,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042630> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b6c0> >"
] ]
} }
], ],
@ -1963,7 +1963,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80423c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b450> >"
] ]
} }
], ],
@ -2578,7 +2578,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042ed0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b840> >"
] ]
} }
], ],
@ -2734,7 +2734,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80426c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c250f61e0> >"
] ]
} }
], ],
@ -2804,7 +2804,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faedb3750f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c250f6150> >"
] ]
} }
], ],
@ -2814,9 +2814,11 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "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", "a1 = spot.translate('a W c'); display(a1.show('.bat'))\n",
"a2 = spot.translate('a U b'); display(a2.show('.bat'))\n", "a2 = spot.translate('a U b'); display(a2.show('.bat+1'))\n",
"# the product should display pairs of states, unless asked not to\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'))" "p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))"
], ],
"language": "python", "language": "python",
@ -2886,7 +2888,7 @@
"<title>G</title>\n", "<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-111 159,-111 159,4 -4,4\" stroke=\"none\"/>\n", "<polygon fill=\"white\" points=\"-4,4 -4,-111 159,-111 159,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.5\" y=\"-92.8\">Inf(</text>\n", "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.5\" y=\"-92.8\">Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5\" y=\"-92.8\">\u24ff</text>\n", "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5\" y=\"-92.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-92.8\">)</text>\n", "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-92.8\">)</text>\n",
"<!-- I -->\n", "<!-- I -->\n",
"<!-- 1 -->\n", "<!-- 1 -->\n",
@ -2921,7 +2923,7 @@
"<path d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\" fill=\"none\" stroke=\"black\"/>\n", "<path d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\" stroke=\"black\"/>\n", "<polygon fill=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"132.5\" y=\"-72.8\">1</text>\n", "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"132.5\" y=\"-72.8\">1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"129\" y=\"-57.8\">\u24ff</text>\n", "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"129\" y=\"-57.8\">\u2776</text>\n",
"</g>\n", "</g>\n",
"</g>\n", "</g>\n",
"</svg>" "</svg>"