Commit 8aa88c29 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

dot: --dot=B to use bullets for all automata but Büchi and co-Büchi

* src/twaalgos/dotty.cc: Add option 'B'.
* src/taalgos/dotty.cc: Ignore it.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it.
* wrap/python/spot.py (setup): Use it by default, and rewrite
the function to be a bit more flexible.
* wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb,
wrap/python/tests/piperead.ipynb, wrap/python/tests/randaut.ipynb,
wrap/python/tests/testingaut.ipynb: Use setup() everywhere.
parent 51309cf7
......@@ -51,10 +51,12 @@ static const argp_option options[] =
{
/**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 },
{ "dot", OPT_DOT, "1|a|b|c|f(FONT)|h|n|N|o|r|R|s|t|v", OPTION_ARG_OPTIONAL,
{ "dot", OPT_DOT, "1|a|b|B|c|f(FONT)|h|n|N|o|r|R|s|t|v",
OPTION_ARG_OPTIONAL,
"GraphViz's format (default). Add letters for "
"(1) force numbered states, "
"(a) acceptance display, (b) acceptance sets as bullets, "
"(B) bullets except for Büchi/co-Büchi automata, "
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
"(v) vertical layout, (n) with name, (N) without name, "
"(o) ordered transitions, "
......
......@@ -73,10 +73,12 @@ static const argp_option options[] =
"of the given property)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 },
{ "dot", OPT_DOT, "1|a|b|c|f(FONT)|h|n|N|o|r|R|s|t|v", OPTION_ARG_OPTIONAL,
{ "dot", OPT_DOT, "1|a|b|B|c|f(FONT)|h|n|N|o|r|R|s|t|v",
OPTION_ARG_OPTIONAL,
"GraphViz's format (default). Add letters for "
"(1) force numbered states, "
"(a) acceptance display, (b) acceptance sets as bullets, "
"(B) bullets except for Büchi automata, "
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
"(v) vertical layout, (n) with name, (N) without name, "
"(o) ordered transitions, "
......
......@@ -87,6 +87,7 @@ namespace spot
case '1':
case 'a':
case 'b':
case 'B':
case 'n':
case 'N':
case 'o':
......
......@@ -59,6 +59,7 @@ namespace spot
acc_cond::mark_t fin_sets_ = 0U;
bool opt_rainbow = false;
bool opt_bullet = false;
bool opt_bullet_but_buchi = false;
bool opt_all_bullets = false;
bool opt_numbered_trans = false;
bool opt_want_state_names_ = true;
......@@ -117,6 +118,10 @@ namespace spot
case 'b':
opt_bullet = true;
break;
case 'B':
opt_bullet = true;
opt_bullet_but_buchi = true;
break;
case 'c':
opt_circles_ = true;
break;
......@@ -346,7 +351,9 @@ namespace spot
void
process_state(unsigned s)
{
if (mark_states_ && (opt_bullet || aut_->acc().num_sets() != 1))
if (mark_states_ &&
((opt_bullet && !opt_bullet_but_buchi)
|| aut_->acc().num_sets() != 1))
{
acc_cond::mark_t acc = 0U;
for (auto& t: aut_->out(s))
......
......@@ -22,18 +22,38 @@ import subprocess
import sys
from functools import lru_cache
def setup(**kwargs):
"""Configure Spot for fancy display.
This is manly useful in IPython.
Note that this function needs to be called before any automaton is
displayed. Afterwards it will have no effect (you should restart
Python, or the IPython Kernel).
Keywords arguments:
bullets -- a Boolean indicating whether to display acceptance conditions
as UTF8 bullets (default: True)
fillcolor -- a string indicating the color to use for states
(default: '#ffffaa')
size -- a string giving the width and height of the GraphViz output
in inches (default: '10.2,5')
font -- the name of the font to use in the GraphViz output
(default: 'Lato')
"""
import os
s = 'size="{}" node[style=filled,fillcolor="{}"] edge[arrowhead=vee, arrowsize=.7]'
os.environ['SPOT_DOTEXTRA'] = s.format(kwargs.get('size', '10.2,5'),
kwargs.get('fillcolor', '#ffffaa'))
bullets = 'B' if kwargs.get('bullets', True) else ''
d = 'rcf({})'.format(kwargs.get('font', 'Lato')) + bullets
os.environ['SPOT_DOTDEFAULT'] = d
# Global BDD dict so that we do not have to create one in user code.
_bdd_dict = make_bdd_dict()
# Load all preliminaries for a fancy display
def setup(show_bullet=True):
import os
os.environ['SPOT_DOTEXTRA'] = 'size="10.2,5" node[style=filled,fillcolor="#ffffaa"] edge[arrowhead=vee, arrowsize=.7]'
if show_bullet:
os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'
else:
os.environ['SPOT_DOTDEFAULT'] = 'rcf(Lato)'
# Add a small LRU cache so that when we display automata into a
# interactive widget, we avoid some repeated calls to dot for
# identical inputs.
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
{
"metadata": {
"name": "",
"signature": "sha256:f4c7efdcb7b97c3b11c230a6b18c8e46c1708289918a5dd8df73fe6baae3c8f6"
"signature": "sha256:0282f226c25df3a47177f96c3d474c1f5191fa8f7d87a35445a3d0d978bb8e35"
},
"nbformat": 3,
"nbformat_minor": 0,
......@@ -12,15 +12,9 @@
"cell_type": "code",
"collapsed": false,
"input": [
"import os\n",
"from IPython.display import display, HTML\n",
"# Note that Spot (loaded by the kernel) will store a copy of\n",
"# the environment variables the first time it reads them, so\n",
"# if you change those variables, the new values will be ignored\n",
"# until you restart the kernel.\n",
"os.environ['SPOT_DOTEXTRA'] = 'size=\"5.4,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
"os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
"import spot"
"import spot\n",
"spot.setup(size='5.4,5')"
],
"language": "python",
"metadata": {},
......@@ -2034,7 +2028,7 @@
"output_type": "pyout",
"prompt_number": 2,
"text": [
"<IPython.core.display.HTML at 0x7f5ca02a7b70>"
"<IPython.core.display.HTML at 0x7fc4e010a6d8>"
]
}
],
......
{
"metadata": {
"name": "",
"signature": "sha256:89d455537d395ae2842b209c6c14a262e15747fd501a731df0cd235f8c95011f"
"signature": "sha256:1a85b698ebae51aaba0387d782d1cf5c6cdf54f69dd6b4b9c7189f8676eb4c88"
},
"nbformat": 3,
"nbformat_minor": 0,
......@@ -12,15 +12,9 @@
"cell_type": "code",
"collapsed": false,
"input": [
"import os\n",
"from IPython.display import display, HTML\n",
"# Note that Spot (loaded by the kernel) will store a copy of\n",
"# the environment variables the first time it reads them, so\n",
"# if you change those variables, the new values will be ignored\n",
"# until you restart the kernel.\n",
"os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
"os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
"import spot"
"import spot\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
......@@ -58,51 +52,51 @@
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"181pt\" height=\"95pt\"\n",
" viewBox=\"0.00 0.00 180.74 94.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 90.7401)\">\n",
"<svg width=\"171pt\" height=\"85pt\"\n",
" viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-90.7401 176.74,-90.7401 176.74,4 -4,4\"/>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-26.8701\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-26.8701C2.79388,-26.8701 17.1543,-26.8701 30.6317,-26.8701\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-26.8701 30.9419,-30.0202 34.4419,-26.8701 30.9419,-26.8702 30.9419,-26.8702 30.9419,-26.8702 34.4419,-26.8701 30.9418,-23.7202 37.9419,-26.8701 37.9419,-26.8701\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-43.9074C48.3189,-53.728 50.4453,-62.8701 56,-62.8701 60.166,-62.8701 62.4036,-57.7276 62.7128,-51.0134\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-43.9074 65.8541,-50.7519 62.5434,-47.4035 62.7076,-50.8997 62.7076,-50.8997 62.7076,-50.8997 62.5434,-47.4035 59.561,-51.0474 62.3792,-43.9074 62.3792,-43.9074\"/>\n",
"<text text-anchor=\"start\" x=\"52.5\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
"<text text-anchor=\"start\" x=\"52.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"145.87\" cy=\"-26.8701\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"start\" x=\"141.37\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"start\" x=\"137.87\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.3603,-26.8701C84.98,-26.8701 98.9179,-26.8701 111.595,-26.8701\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"118.879,-26.8701 111.88,-30.0202 115.379,-26.8701 111.879,-26.8702 111.879,-26.8702 111.879,-26.8702 115.379,-26.8701 111.879,-23.7202 118.879,-26.8701 118.879,-26.8701\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M136.949,-52.2401C136.334,-62.7939 139.308,-71.7401 145.87,-71.7401 150.894,-71.7401 153.815,-66.496 154.632,-59.3013\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"154.791,-52.2401 157.783,-59.3092 154.712,-55.7392 154.633,-59.2383 154.633,-59.2383 154.633,-59.2383 154.712,-55.7392 151.484,-59.1674 154.791,-52.2401 154.791,-52.2401\"/>\n",
"<text text-anchor=\"start\" x=\"141.37\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
"<text text-anchor=\"start\" x=\"136.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1eb80416f0> >"
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e817bf6c0> >"
]
}
],
......@@ -364,7 +358,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f1eb80687b8>"
"<IPython.core.display.SVG at 0x7f2e80d6fc50>"
]
}
],
......@@ -509,7 +503,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f1eba67beb8>"
"<IPython.core.display.SVG at 0x7f2e89e119b0>"
]
}
],
......@@ -636,7 +630,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f1eba67bc18>"
"<IPython.core.display.SVG at 0x7f2e884949e8>"
]
}
],
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment