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

python: export tgba_determinize

Browse source 
* python/spot/impl.i: Here.
* tests/python/automata.ipynb: Use it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-04-22 18:48:03 +02:00
parent 8641271cad
commit 33391798a3
3 changed files with 270 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -24,6 +24,10 @@ New in spot 2.0a (not yet released)
* Add missing documentation for the option string passed to
spot::make_emptiness_check_instantiator().
Python:
* The tgba_determinize() function is now accessible in Python.
Bug fixes:
* Typo in documentation of the -H option in --help output.

2
python/spot/impl.i
View file

@ -123,6 +123,7 @@
#include <spot/twaalgos/ltl2taa.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/magic.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/neverclaim.hh>
@ -428,6 +429,7 @@ namespace std {
%include <spot/twaalgos/ltl2taa.hh>
%include <spot/twaalgos/ltl2tgba_fm.hh>
%include <spot/twaalgos/compsusp.hh>
%include <spot/twaalgos/determinize.hh>
%include <spot/twaalgos/magic.hh>
%include <spot/twaalgos/minimize.hh>
%include <spot/twaalgos/neverclaim.hh>

291
tests/python/automata.ipynb
View file

@ -18,7 +18,7 @@
"version": "3.4.3+"
},
"name": "",
"signature": "sha256:93ecf5f37287bb2a03dcd63d41faa06f0ed9d8bcc403c73b24d1bf10404b3b1c"
"signature": "sha256:29d335e40a65f0ca04a3b2b07bfcbf92f794407b413644546d957487dcbf4bb1"
},
"nbformat": 3,
"nbformat_minor": 0,
@ -178,7 +178,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cfc093810> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8369240> >"
]
}
],
@ -317,7 +317,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7cff347ef0>"
"<IPython.core.display.SVG at 0x7f09a13dd5f8>"
]
}
],
@ -470,7 +470,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7d034410f0>"
"<IPython.core.display.SVG at 0x7f09a074abe0>"
]
}
],
@ -570,7 +570,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ee10> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323fc0> >"
]
}
],
@ -640,7 +640,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecc0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323e70> >"
]
}
],
@ -716,7 +716,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ed50> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f00> >"
]
}
],
@ -839,7 +839,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced200cc0>"
"<IPython.core.display.SVG at 0x7f09a0773da0>"
]
}
],
@ -1029,7 +1029,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced19d7f0>"
"<IPython.core.display.SVG at 0x7f098bfe96d8>"
]
}
],
@ -1176,7 +1176,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef60> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f30> >"
]
}
],
@ -1277,7 +1277,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef30> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3210> >"
]
}
],
@ -1395,7 +1395,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef00> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3240> >"
]
}
],
@ -1494,7 +1494,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ed20> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3270> >"
]
}
],
@ -1964,7 +1964,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef90> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323ed0> >"
]
}
],
@ -2161,7 +2161,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced19d5c0>"
"<IPython.core.display.SVG at 0x7f09a0703dd8>"
]
},
{
@ -2286,7 +2286,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7d03411e10>"
"<IPython.core.display.SVG at 0x7f09a0734198>"
]
},
{
@ -2428,7 +2428,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced1fa710>"
"<IPython.core.display.SVG at 0x7f09a06db400>"
]
},
{
@ -2579,7 +2579,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecf0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff33f0> >"
]
}
],
@ -2735,7 +2735,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37eed0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323c60> >"
]
}
],
@ -2805,7 +2805,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecf0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff31b0> >"
]
}
],
@ -2877,7 +2877,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced1863c8>"
"<IPython.core.display.SVG at 0x7f09a06980f0>"
]
},
{
@ -2930,7 +2930,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced1913c8>"
"<IPython.core.display.SVG at 0x7f09a0682358>"
]
},
{
@ -3042,7 +3042,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced18d160>"
"<IPython.core.display.SVG at 0x7f09a0742908>"
]
},
{
@ -3154,20 +3154,257 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f7ced1b7668>"
"<IPython.core.display.SVG at 0x7f09a0742828>"
]
}
],
"prompt_number": 23
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Explicit determinization after translation:"
]
},
{
"cell_type": "code",
"collapsed": true,
"input": [],
"input": [
"a = spot.translate('FGa')\n",
"display(a)\n",
"display(a.is_deterministic())"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 23
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"161pt\" height=\"92pt\"\n",
" viewBox=\"0.00 0.00 161.00 92.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 88)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-88 157,-88 157,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=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-14.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,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\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,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"135\" y=\"-14.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.0888,-18C84.5562,-18 98.1196,-18 109.693,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"116.959,-18 109.959,-21.1501 113.459,-18 109.959,-18.0001 109.959,-18.0001 109.959,-18.0001 113.459,-18 109.959,-14.8501 116.959,-18 116.959,-18\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a</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=\"M128.266,-35.0373C126.892,-44.8579 129.137,-54 135,-54 139.397,-54 141.759,-48.8576 142.086,-42.1433\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"141.734,-35.0373 145.226,-41.8728 141.907,-38.533 142.08,-42.0287 142.08,-42.0287 142.08,-42.0287 141.907,-38.533 138.934,-42.1847 141.734,-35.0373 141.734,-35.0373\"/>\n",
"<text text-anchor=\"start\" x=\"131.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"127\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</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 0x7f09a82ac5d0> >"
]
},
{
"metadata": {},
"output_type": "display_data",
"text": [
"False"
]
}
],
"prompt_number": 24
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.tgba_determinize(a).show('.ba')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 25,
"svg": [
"<svg height=\"127pt\" viewBox=\"0.00 0.00 170.00 127.47\" width=\"170pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 123.465)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-123.465 166,-123.465 166,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"29\" y=\"-105.265\">Fin(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-105.265\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"70\" y=\"-105.265\">) &amp; Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113\" y=\"-105.265\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"129\" y=\"-105.265\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-30.4654\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-26.7654\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
"<path d=\"M1.15491,-30.4654C2.79388,-30.4654 17.1543,-30.4654 30.6317,-30.4654\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-30.4654 30.9419,-33.6155 34.4419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 34.4419,-30.4655 30.9418,-27.3155 37.9419,-30.4654 37.9419,-30.4654\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-47.5027C48.3189,-57.3234 50.4453,-66.4654 56,-66.4654 60.166,-66.4654 62.4036,-61.323 62.7128,-54.6087\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-47.5027 65.8541,-54.3473 62.5434,-50.9989 62.7076,-54.495 62.7076,-54.495 62.7076,-54.495 62.5434,-50.9989 59.561,-54.6428 62.3792,-47.5027 62.3792,-47.5027\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"50.5\" y=\"-70.2654\">!a</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"144\" cy=\"-30.4654\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"144\" y=\"-26.7654\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M74.0378,-33.3939C79.731,-34.2402 86.1223,-35.0477 92,-35.4654 99.0932,-35.9695 100.907,-35.9695 108,-35.4654 111.49,-35.2174 115.161,-34.832 118.759,-34.3826\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"125.962,-33.3939 119.456,-37.4666 122.495,-33.8699 119.027,-34.3459 119.027,-34.3459 119.027,-34.3459 122.495,-33.8699 118.599,-31.2251 125.962,-33.3939 125.962,-33.3939\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"96.5\" y=\"-54.2654\">a</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-39.2654\">\u2776</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
"<path d=\"M131.404,-17.3266C125.156,-11.2493 116.908,-4.67653 108,-1.46544 95.985,2.86544 83.5046,-4.00369 73.8973,-12.1402\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"68.5978,-17.0022 71.6264,-9.94872 71.1769,-14.636 73.7559,-12.2699 73.7559,-12.2699 73.7559,-12.2699 71.1769,-14.636 75.8855,-14.591 68.5978,-17.0022 68.5978,-17.0022\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-20.2654\">!a</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-5.26544\">\u24ff</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
"<path d=\"M136.332,-46.7557C134.483,-56.8546 137.039,-66.4654 144,-66.4654 149.221,-66.4654 151.964,-61.0593 152.229,-54.0958\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"151.668,-46.7557 155.342,-53.4954 151.935,-50.2455 152.201,-53.7354 152.201,-53.7354 152.201,-53.7354 151.935,-50.2455 149.06,-53.9754 151.668,-46.7557 151.668,-46.7557\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"140.5\" y=\"-85.2654\">a</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-70.2654\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f09a06db4a8>"
]
}
],
"prompt_number": 25
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Determinization by `translate()`. The `generic` option allows any acceptance condition to be used instead of the default generalized B\u00fcchi."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate('FGa', 'generic', 'deterministic')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 26,
"svg": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"170pt\" height=\"104pt\"\n",
" viewBox=\"0.00 0.00 170.00 104.47\" 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 100.465)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-100.465 166,-100.465 166,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-30.4654\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-26.7654\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-30.4654C2.79388,-30.4654 17.1543,-30.4654 30.6317,-30.4654\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-30.4654 30.9419,-33.6155 34.4419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 34.4419,-30.4655 30.9418,-27.3155 37.9419,-30.4654 37.9419,-30.4654\"/>\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=\"M49.6208,-47.5027C48.3189,-57.3234 50.4453,-66.4654 56,-66.4654 60.166,-66.4654 62.4036,-61.323 62.7128,-54.6087\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-47.5027 65.8541,-54.3473 62.5434,-50.9989 62.7076,-54.495 62.7076,-54.495 62.7076,-54.495 62.5434,-50.9989 59.561,-54.6428 62.3792,-47.5027 62.3792,-47.5027\"/>\n",
"<text text-anchor=\"start\" x=\"50.5\" y=\"-70.2654\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-30.4654\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"144\" y=\"-26.7654\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.0378,-33.3939C79.731,-34.2402 86.1223,-35.0477 92,-35.4654 99.0932,-35.9695 100.907,-35.9695 108,-35.4654 111.49,-35.2174 115.161,-34.832 118.759,-34.3826\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"125.962,-33.3939 119.456,-37.4666 122.495,-33.8699 119.027,-34.3459 119.027,-34.3459 119.027,-34.3459 122.495,-33.8699 118.599,-31.2251 125.962,-33.3939 125.962,-33.3939\"/>\n",
"<text text-anchor=\"start\" x=\"96.5\" y=\"-54.2654\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-39.2654\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M131.404,-17.3266C125.156,-11.2493 116.908,-4.67653 108,-1.46544 95.985,2.86544 83.5046,-4.00369 73.8973,-12.1402\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"68.5978,-17.0022 71.6264,-9.94872 71.1769,-14.636 73.7559,-12.2699 73.7559,-12.2699 73.7559,-12.2699 71.1769,-14.636 75.8855,-14.591 68.5978,-17.0022 68.5978,-17.0022\"/>\n",
"<text text-anchor=\"start\" x=\"94.5\" y=\"-20.2654\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-5.26544\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M136.332,-46.7557C134.483,-56.8546 137.039,-66.4654 144,-66.4654 149.221,-66.4654 151.964,-61.0593 152.229,-54.0958\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"151.668,-46.7557 155.342,-53.4954 151.935,-50.2455 152.201,-53.7354 152.201,-53.7354 152.201,-53.7354 151.935,-50.2455 149.06,-53.9754 151.668,-46.7557 151.668,-46.7557\"/>\n",
"<text text-anchor=\"start\" x=\"140.5\" y=\"-85.2654\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"136\" y=\"-70.2654\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</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 0x7f09a82ac480> >"
]
}
],
"prompt_number": 26
}
],
"metadata": {}