Skip to content

GitLab

Commit da051e11 authored by Clément Gillard's avatar Clément Gillard
1 Browse files
Options

decompose_scc: Update 'decompose' notebook 

* tests/python/decompose.ipynb: Add about `decompose_scc`.
* doc/org/tut.org: Update description.
parent 5d143cc1
Hide whitespace changes
Inline Side-by-side
Showing with 255 additions and 5 deletions
doc/org/tut.org
View file @ da051e11
...@@ -68,7 +68,7 @@ real notebooks instead. ...@@ -68,7 +68,7 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
in Python in Python
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
- [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()= function - [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()=, =decompose_acc_scc()= and =decompose_scc()= functions
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing
automaton automaton
- [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface. - [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface.
......
tests/python/decompose.ipynb
View file @ da051e11
...@@ -43,7 +43,7 @@ ...@@ -43,7 +43,7 @@
"source": [ "source": [
"This notebook demonstrates how to use the `decompose_strength()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n", "This notebook demonstrates how to use the `decompose_strength()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n",
"\n", "\n",
"This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-strength` option.\n", "This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-strength` and `--decompose-scc` option.\n",
"\n", "\n",
"# Basics\n", "# Basics\n",
"\n", "\n",
...@@ -4993,14 +4993,264 @@ ...@@ -4993,14 +4993,264 @@
], ],
"prompt_number": 20 "prompt_number": 20
}, },
{
"cell_type": "markdown",
"metadata": {
"collapsed": false
},
"source": [
"# `decompose_acc_scc()`\n",
"\n",
"Similarly to `decompose_strength()`, the `decompose_acc_scc()` function takes an automaton and the index of an accepting SCC, and preserves only this SCC and its upstream SCCs:"
]
},
{ {
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [], "input": [
"aut = spot.translate('(Ga -> Gb) W c')\n",
"spot.decompose_acc_scc(aut, 1)"
],
"language": "python", "language": "python",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [
"prompt_number": null {
"metadata": {},
"output_type": "pyout",
"prompt_number": 21,
"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=\"397pt\" height=\"152pt\"\n",
" viewBox=\"0.00 0.00 397.00 152.21\" 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 148.207)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-148.207 393,-148.207 393,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"173.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"195.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"211.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
"<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
"<polygon fill=\"none\" stroke=\"green\" points=\"329,-11.2072 329,-111.207 381,-111.207 381,-11.2072 329,-11.2072\"/>\n",
"</g>\n",
"<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
"<polygon fill=\"none\" stroke=\"red\" points=\"246,-11.2072 246,-96.2072 298,-96.2072 298,-11.2072 246,-11.2072\"/>\n",
"</g>\n",
"<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
"<polygon fill=\"none\" stroke=\"red\" points=\"30,-9.20721 30,-96.2072 194,-96.2072 194,-9.20721 30,-9.20721\"/>\n",
"</g>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-35.2072\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-31.5072\" 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,-35.2072C2.79388,-35.2072 17.1543,-35.2072 30.6317,-35.2072\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-35.2072 30.9419,-38.3573 34.4419,-35.2073 30.9419,-35.2073 30.9419,-35.2073 30.9419,-35.2073 34.4419,-35.2073 30.9418,-32.0573 37.9419,-35.2072 37.9419,-35.2072\"/>\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,-52.2445C48.3189,-62.0651 50.4453,-71.2072 56,-71.2072 60.166,-71.2072 62.4036,-66.0648 62.7128,-59.3505\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-52.2445 65.8541,-59.0891 62.5434,-55.7407 62.7076,-59.2368 62.7076,-59.2368 62.7076,-59.2368 62.5434,-55.7407 59.561,-59.3846 62.3792,-52.2445 62.3792,-52.2445\"/>\n",
"<text text-anchor=\"start\" x=\"36\" y=\"-75.0072\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"355\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M73.0478,-29.4272C112.119,-16.1948 215.065,13.6081 298,-7.20721 310.58,-10.3645 323.419,-16.9513 333.624,-23.1507\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"339.612,-26.9265 332.011,-25.8575 336.652,-25.0597 333.691,-23.1929 333.691,-23.1929 333.691,-23.1929 336.652,-25.0597 335.371,-20.5284 339.612,-26.9265 339.612,-26.9265\"/>\n",
"<text text-anchor=\"start\" x=\"216.5\" y=\"-6.00721\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node5\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"168\" y=\"-33.5072\" 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.2788,-35.363C89.4809,-35.5178 112.211,-35.7926 132,-36.2072 135.464,-36.2798 139.121,-36.3696 142.713,-36.4654\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"149.911,-36.6669 142.826,-39.6197 146.413,-36.5689 142.914,-36.471 142.914,-36.471 142.914,-36.471 146.413,-36.5689 143.002,-33.3222 149.911,-36.6669 149.911,-36.6669\"/>\n",
"<text text-anchor=\"start\" x=\"94\" y=\"-40.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M347.969,-53.8713C346.406,-63.8322 348.75,-73.2072 355,-73.2072 359.688,-73.2072 362.178,-67.9338 362.471,-61.0948\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"362.031,-53.8713 365.601,-60.667 362.244,-57.3648 362.456,-60.8584 362.456,-60.8584 362.456,-60.8584 362.244,-57.3648 359.312,-61.0497 362.031,-53.8713 362.031,-53.8713\"/>\n",
"<text text-anchor=\"start\" x=\"350.5\" y=\"-92.0072\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"start\" x=\"347\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node4\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"272\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M290.178,-37.2072C301.669,-37.2072 316.959,-37.2072 329.693,-37.2072\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"336.847,-37.2072 329.847,-40.3573 333.347,-37.2073 329.847,-37.2073 329.847,-37.2073 329.847,-37.2073 333.347,-37.2073 329.847,-34.0573 336.847,-37.2072 336.847,-37.2072\"/>\n",
"<text text-anchor=\"start\" x=\"308\" y=\"-41.0072\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M264.969,-53.8713C263.406,-63.8322 265.75,-73.2072 272,-73.2072 276.688,-73.2072 279.178,-67.9338 279.471,-61.0948\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"279.031,-53.8713 282.601,-60.667 279.244,-57.3648 279.456,-60.8584 279.456,-60.8584 279.456,-60.8584 279.244,-57.3648 276.312,-61.0497 279.031,-53.8713 279.031,-53.8713\"/>\n",
"<text text-anchor=\"start\" x=\"268.5\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M151.358,-44.9402C145.443,-47.4659 138.555,-49.9449 132,-51.2072 114.543,-54.5691 109.371,-54.9894 92,-51.2072 87.5445,-50.2371 82.977,-48.647 78.6739,-46.8365\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-43.8674 79.8596,-43.915 75.3664,-45.3234 78.5492,-46.7795 78.5492,-46.7795 78.5492,-46.7795 75.3664,-45.3234 77.2387,-49.644 72.1836,-43.8674 72.1836,-43.8674\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-58.0072\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M180.109,-50.6899C193.757,-66.0814 218.509,-90.3938 246,-100.207 267.766,-107.977 276.917,-109.675 298,-100.207 316.806,-91.762 331.873,-73.5336 341.62,-58.8467\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"345.468,-52.808 344.363,-60.4043 343.587,-55.7599 341.706,-58.7117 341.706,-58.7117 341.706,-58.7117 343.587,-55.7599 339.05,-57.0191 345.468,-52.808 345.468,-52.808\"/>\n",
"<text text-anchor=\"start\" x=\"254\" y=\"-110.007\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M186.303,-37.2072C202.962,-37.2072 228.303,-37.2072 246.927,-37.2072\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"253.953,-37.2072 246.953,-40.3573 250.453,-37.2073 246.953,-37.2073 246.953,-37.2073 246.953,-37.2073 250.453,-37.2073 246.953,-34.0573 253.953,-37.2072 253.953,-37.2072\"/>\n",
"<text text-anchor=\"start\" x=\"204\" y=\"-41.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M159.021,-53.1232C156.679,-63.3576 159.672,-73.2072 168,-73.2072 174.376,-73.2072 177.625,-67.4336 177.746,-60.134\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"176.979,-53.1232 180.872,-59.7387 177.36,-56.6024 177.741,-60.0816 177.741,-60.0816 177.741,-60.0816 177.36,-56.6024 174.61,-60.4246 176.979,-53.1232 176.979,-53.1232\"/>\n",
"<text text-anchor=\"start\" x=\"150\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</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 0x7ff37c13b1b0> >"
]
}
],
"prompt_number": 21
},
{
"cell_type": "markdown",
"metadata": {
"collapsed": true
},
"source": [
"# `decompose_scc()`\n",
"\n",
"You can also, like in the C++ interface, use a `scc_info` to extract a particular SCC and its parents, even non accepting."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"si = spot.scc_info(aut)\n",
"spot.decompose_scc(si, 2)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 30,
"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=\"314pt\" height=\"134pt\"\n",
" viewBox=\"0.00 0.00 314.00 134.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 130)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-130 310,-130 310,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"132\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"154\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"170\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
"<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
"<polygon fill=\"none\" stroke=\"grey\" points=\"246,-9 246,-94 298,-94 298,-9 246,-9\"/>\n",
"</g>\n",
"<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
"<polygon fill=\"none\" stroke=\"grey\" points=\"30,-8 30,-95 194,-95 194,-8 30,-8\"/>\n",
"</g>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-35\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-31.3\" 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,-35C2.79388,-35 17.1543,-35 30.6317,-35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-35 30.9419,-38.1501 34.4419,-35 30.9419,-35.0001 30.9419,-35.0001 30.9419,-35.0001 34.4419,-35 30.9418,-31.8501 37.9419,-35 37.9419,-35\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-52.0373C48.3189,-61.8579 50.4453,-71 56,-71 60.166,-71 62.4036,-65.8576 62.7128,-59.1433\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-52.0373 65.8541,-58.8818 62.5434,-55.5335 62.7076,-59.0296 62.7076,-59.0296 62.7076,-59.0296 62.5434,-55.5335 59.561,-59.1774 62.3792,-52.0373 62.3792,-52.0373\"/>\n",
"<text text-anchor=\"start\" x=\"36\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node4\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-35\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"168\" y=\"-31.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.1875,-35C92.5925,-35 121.947,-35 142.709,-35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"149.933,-35 142.933,-38.1501 146.433,-35 142.933,-35.0001 142.933,-35.0001 142.933,-35.0001 146.433,-35 142.933,-31.8501 149.933,-35 149.933,-35\"/>\n",
"<text text-anchor=\"start\" x=\"94\" y=\"-38.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-35\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"272\" y=\"-31.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M263.021,-50.916C260.679,-61.1504 263.672,-71 272,-71 278.376,-71 281.625,-65.2263 281.746,-57.9268\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"280.979,-50.916 284.872,-57.5315 281.36,-54.3952 281.741,-57.8744 281.741,-57.8744 281.741,-57.8744 281.36,-54.3952 278.61,-58.2174 280.979,-50.916 280.979,-50.916\"/>\n",
"<text text-anchor=\"start\" x=\"268.5\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M151.759,-43.1226C145.774,-45.8828 138.735,-48.6176 132,-50 114.585,-53.5745 109.415,-53.5745 92,-50 87.5802,-49.0928 83.0294,-47.6032 78.7315,-45.9062\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"72.2412,-43.1226 79.9161,-42.9868 75.4579,-44.5022 78.6745,-45.8818 78.6745,-45.8818 78.6745,-45.8818 75.4579,-44.5022 77.4329,-48.7768 72.2412,-43.1226 72.2412,-43.1226\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M186.303,-35C202.962,-35 228.303,-35 246.927,-35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"253.953,-35 246.953,-38.1501 250.453,-35 246.953,-35.0001 246.953,-35.0001 246.953,-35.0001 250.453,-35 246.953,-31.8501 253.953,-35 253.953,-35\"/>\n",
"<text text-anchor=\"start\" x=\"204\" y=\"-38.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M159.021,-50.916C156.679,-61.1504 159.672,-71 168,-71 174.376,-71 177.625,-65.2263 177.746,-57.9268\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"176.979,-50.916 180.872,-57.5315 177.36,-54.3952 177.741,-57.8744 177.741,-57.8744 177.741,-57.8744 177.36,-54.3952 174.61,-58.2174 176.979,-50.916 176.979,-50.916\"/>\n",
"<text text-anchor=\"start\" x=\"150\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</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 0x7f6aa02181e0> >"
]
}
],
"prompt_number": 30
}, },
{ {
"cell_type": "code", "cell_type": "code",
......
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