python: define our own SVG DisplayObject

This is to workaround differences in minidom's pretty-printing that
occurred between Python 3.7 and 3.8.

* python/spot/jupyter.py (SVG): New class.
* python/spot/__init__.py: Use it.
* tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/automata.ipynb, tests/python/formulas.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2019-12-04 23:05:51 +01:00
parent 44df3c0837
commit e778965730
15 changed files with 14765 additions and 14141 deletions

View file

@ -150,7 +150,7 @@ class twa:
# Load the SVG function only if we need it. This way the
# bindings can still be used outside of IPython if IPython is
# not installed.
from IPython.display import SVG
from spot.jupyter import SVG
return SVG(self._repr_svg_(opt))
def highlight_states(self, states, color):
@ -212,7 +212,7 @@ class twa_graph:
def show_storage(self, opt=None):
ostr = ostringstream()
self.dump_storage_as_dot(ostr, opt)
from IPython.display import SVG
from spot.jupyter import SVG
return SVG(_ostream_to_svg(ostr))
@ -237,7 +237,7 @@ class formula:
# Load the SVG function only if we need it. This way the bindings
# can still be used outside of IPython if IPython is not
# installed.
from IPython.display import SVG
from spot.jupyter import SVG
return SVG(_str_to_svg(self.to_str('d')))
def _repr_latex_(self):
@ -1169,7 +1169,7 @@ def show_mp_hierarchy(cl):
Return a picture of the Manna & Pnueli hierarchy as an SVG object
in the IPython/Jupyter.
"""
from IPython.display import SVG
from spot.jupyter import SVG
return SVG(mp_hierarchy_svg(cl))
@ -1278,7 +1278,7 @@ class twa_word:
"""
Display the word as an SVG picture of signals.
"""
from IPython.display import SVG
from spot.jupyter import SVG
return SVG(self.as_svg())

View file

@ -21,8 +21,23 @@
Auxiliary functions for Spot's Python bindings.
"""
from IPython.display import display, HTML
from IPython.display import display, HTML, DisplayObject
class SVG(DisplayObject):
"""
Replacement for IPython.display.SVG that does not use
minidom to extract the <svg> element.
We need that because prior to Python 3.8, minidom used
sort all attributes, and in Python 3.8 this was changed
to keep the same order, causing test failures in our
diff-based test suite.
We do not need the <svg> extraction when processing
GraphViz output.
"""
def _repr_svg_(self):
return self.data
def display_inline(*args, per_row=None, show=None):
"""

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -503,184 +503,191 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"404pt\" viewBox=\"0.00 0.00 371.00 404.00\" width=\"371pt\" 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 400)\">\n",
"<?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.43.0 (0)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"371pt\" height=\"404pt\"\n",
" viewBox=\"0.00 0.00 371.00 404.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.0 1.0) rotate(0) translate(4 400)\">\n",
"<title>G</title>\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-400 367,-400 367,4 -4,4\" stroke=\"transparent\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-400 367,-400 367,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node1\">\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse cx=\"161\" cy=\"-378\" fill=\"none\" rx=\"40.8928\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"161\" y=\"-374.3\">EConcat</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"161\" cy=\"-378\" rx=\"40.89\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"161\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">EConcat</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node2\">\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse cx=\"129\" cy=\"-306\" fill=\"none\" rx=\"35.9954\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"129\" y=\"-302.3\">Concat</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"129\" cy=\"-306\" rx=\"36\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"129\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M153.0899,-360.2022C149.4473,-352.0064 145.0455,-342.1024 141.0065,-333.0145\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"144.0789,-331.3096 136.8191,-323.593 137.6822,-334.1527 144.0789,-331.3096\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"148.5899\" y=\"-349.0022\">L</text>\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M153.25,-360.05C149.56,-351.97 145.06,-342.12 140.94,-333.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"144.02,-331.43 136.67,-323.79 137.65,-334.34 144.02,-331.43\"/>\n",
"<text text-anchor=\"middle\" x=\"148.75\" y=\"-348.85\" font-family=\"Times,serif\" font-size=\"14.00\">L</text>\n",
"</g>\n",
"<!-- 10 -->\n",
"<g class=\"node\" id=\"node11\">\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>10</title>\n",
"<ellipse cx=\"225\" cy=\"-234\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"225\" y=\"-230.3\">And</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"225\" cy=\"-234\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"225\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">And</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;10 -->\n",
"<g class=\"edge\" id=\"edge14\">\n",
"<title>0-&gt;10</title>\n",
"<path d=\"M168.9762,-360.0535C180.0668,-335.0998 200.23,-289.7326 213.1015,-260.7717\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"216.4602,-261.8321 217.3233,-251.2725 210.0635,-258.9891 216.4602,-261.8321\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"163.9762\" y=\"-348.8535\">R</text>\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>0&#45;&gt;10</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M168.59,-360.15C179.67,-335.57 200.36,-289.68 213.36,-260.82\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"216.7,-261.94 217.61,-251.39 210.31,-259.07 216.7,-261.94\"/>\n",
"<text text-anchor=\"middle\" x=\"163.59\" y=\"-348.95\" font-family=\"Times,serif\" font-size=\"14.00\">R</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\">\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"none\" points=\"54,-36 0,-36 0,0 54,0 54,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"27\" y=\"-14.3\">a</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"54,-36 0,-36 0,0 54,0 54,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>1-&gt;2</title>\n",
"<path d=\"M106.7369,-291.6428C93.666,-282.0164 77.9949,-268.1646 69,-252 31.7473,-185.0541 26.4358,-92.1681 26.3309,-46.1548\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"29.8315,-46.0506 26.3923,-36.0296 22.8317,-46.0081 29.8315,-46.0506\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"103.2369\" y=\"-280.4428\">1</text>\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M107.33,-291.42C94.15,-281.99 78.14,-268.23 69,-252 31.37,-185.16 26.28,-91.96 26.29,-46.34\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"29.79,-46.1 26.38,-36.07 22.79,-46.04 29.79,-46.1\"/>\n",
"<text text-anchor=\"middle\" x=\"103.83\" y=\"-280.22\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\">\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse cx=\"129\" cy=\"-234\" fill=\"none\" rx=\"51.1914\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"129\" y=\"-230.3\">first_match</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"129\" cy=\"-234\" rx=\"51.19\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"129\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">first_match</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>1-&gt;3</title>\n",
"<path d=\"M129,-287.8314C129,-280.131 129,-270.9743 129,-262.4166\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"132.5001,-262.4132 129,-252.4133 125.5001,-262.4133 132.5001,-262.4132\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"125.5\" y=\"-276.6314\">2</text>\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M129,-287.7C129,-279.98 129,-270.71 129,-262.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"132.5,-262.1 129,-252.1 125.5,-262.1 132.5,-262.1\"/>\n",
"<text text-anchor=\"middle\" x=\"125.5\" y=\"-276.5\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\">\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse cx=\"137\" cy=\"-162\" fill=\"none\" rx=\"35.9954\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"137\" y=\"-158.3\">Concat</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"137\" cy=\"-162\" rx=\"36\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"137\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>3-&gt;4</title>\n",
"<path d=\"M131.0187,-215.8314C131.8743,-208.131 132.8917,-198.9743 133.8426,-190.4166\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"137.3283,-190.7386 134.9541,-180.4133 130.3711,-189.9656 137.3283,-190.7386\" stroke=\"#000000\"/>\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M130.98,-215.7C131.86,-207.98 132.92,-198.71 133.9,-190.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"137.39,-190.44 135.05,-180.1 130.43,-189.64 137.39,-190.44\"/>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node6\">\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>5</title>\n",
"<ellipse cx=\"264\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"264\" y=\"-86.3\">Star</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"264\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"264\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>4-&gt;5</title>\n",
"<path d=\"M160.8877,-148.4574C181.7279,-136.6424 212.0459,-119.4543 234.416,-106.772\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"236.191,-109.7891 243.1641,-101.8125 232.7387,-103.6997 236.191,-109.7891\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"157.3877\" y=\"-137.2574\">1</text>\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>4&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M160.29,-148.16C181.31,-136.57 212.32,-119.48 234.95,-107.01\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"236.72,-110.03 243.78,-102.14 233.34,-103.9 236.72,-110.03\"/>\n",
"<text text-anchor=\"middle\" x=\"156.79\" y=\"-136.96\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g class=\"node\" id=\"node8\">\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>7</title>\n",
"<ellipse cx=\"154\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"154\" y=\"-86.3\">Star</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"154\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"154\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>4-&gt;7</title>\n",
"<path d=\"M141.2898,-143.8314C143.1562,-135.9266 145.385,-126.4872 147.4511,-117.7365\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"150.8788,-118.4501 149.7704,-107.9134 144.0661,-116.8415 150.8788,-118.4501\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"137.7898\" y=\"-132.6314\">2</text>\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>4&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M141.12,-144.05C143.01,-136.26 145.3,-126.82 147.42,-118.08\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"150.85,-118.82 149.8,-108.28 144.04,-117.17 150.85,-118.82\"/>\n",
"<text text-anchor=\"middle\" x=\"137.62\" y=\"-132.85\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 9 -->\n",
"<g class=\"node\" id=\"node10\">\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>9</title>\n",
"<polygon fill=\"none\" points=\"126,-36 72,-36 72,0 126,0 126,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"99\" y=\"-14.3\">d</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"126,-36 72,-36 72,0 126,0 126,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"99\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">d</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;9 -->\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>4-&gt;9</title>\n",
"<path d=\"M130.0742,-144.187C126.1822,-133.7494 121.4322,-120.2494 118,-108 112.2642,-87.5291 107.3558,-64.0109 103.9655,-46.1505\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"107.3661,-45.2923 102.1034,-36.097 100.4832,-46.5672 107.3661,-45.2923\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"126.5742\" y=\"-132.987\">3</text>\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>4&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M130.25,-144C126.32,-133.7 121.48,-120.22 118,-108 112.2,-87.61 107.26,-64.15 103.87,-46.44\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"107.24,-45.42 101.97,-36.23 100.36,-46.7 107.24,-45.42\"/>\n",
"<text text-anchor=\"middle\" x=\"126.75\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g class=\"node\" id=\"node7\">\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>6</title>\n",
"<polygon fill=\"none\" points=\"299,-36 245,-36 245,0 299,0 299,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"272\" y=\"-14.3\">b</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"299,-36 245,-36 245,0 299,0 299,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"272\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>5-&gt;6</title>\n",
"<path d=\"M266.0187,-71.8314C266.8743,-64.131 267.8917,-54.9743 268.8426,-46.4166\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"272.3283,-46.7386 269.9541,-36.4133 265.3711,-45.9656 272.3283,-46.7386\" stroke=\"#000000\"/>\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>5&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M265.98,-71.7C266.86,-63.98 267.92,-54.71 268.9,-46.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"272.39,-46.44 270.05,-36.1 265.43,-45.64 272.39,-46.44\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g class=\"node\" id=\"node9\">\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>8</title>\n",
"<polygon fill=\"none\" points=\"213,-36 159,-36 159,0 213,0 213,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"186\" y=\"-14.3\">c</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"213,-36 159,-36 159,0 213,0 213,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"186\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
"</g>\n",
"<!-- 7&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>7-&gt;8</title>\n",
"<path d=\"M161.7463,-72.5708C165.398,-64.3544 169.8396,-54.3608 173.9191,-45.1821\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"177.1277,-46.5802 177.9908,-36.0206 170.7311,-43.7372 177.1277,-46.5802\" stroke=\"#000000\"/>\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>7&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M161.58,-72.41C165.22,-64.45 169.67,-54.72 173.77,-45.76\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"177.05,-47 178.02,-36.45 170.68,-44.09 177.05,-47\"/>\n",
"</g>\n",
"<!-- 10&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge10\">\n",
"<title>10-&gt;8</title>\n",
"<path d=\"M221.742,-215.9555C214.9457,-178.3144 199.2143,-91.1867 191.078,-46.1246\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"194.4974,-45.364 189.2762,-36.1451 187.6088,-46.6079 194.4974,-45.364\" stroke=\"#000000\"/>\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>10&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M221.87,-215.85C215.11,-178.75 199.09,-90.81 190.94,-46.1\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"194.38,-45.44 189.14,-36.23 187.49,-46.7 194.38,-45.44\"/>\n",
"</g>\n",
"<!-- 11 -->\n",
"<g class=\"node\" id=\"node12\">\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>11</title>\n",
"<ellipse cx=\"300\" cy=\"-162\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"300\" y=\"-158.3\">G</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"300\" cy=\"-162\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"300\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">G</text>\n",
"</g>\n",
"<!-- 10&#45;&gt;11 -->\n",
"<g class=\"edge\" id=\"edge13\">\n",
"<title>10-&gt;11</title>\n",
"<path d=\"M240.54,-219.0816C251.099,-208.945 265.2444,-195.3654 277.0892,-183.9944\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"279.6898,-186.3495 284.4799,-176.8993 274.8421,-181.2998 279.6898,-186.3495\" stroke=\"#000000\"/>\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>10&#45;&gt;11</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M240.18,-218.83C250.85,-208.87 265.32,-195.37 277.35,-184.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"279.92,-186.53 284.85,-177.14 275.15,-181.41 279.92,-186.53\"/>\n",
"</g>\n",
"<!-- 12 -->\n",
"<g class=\"node\" id=\"node13\">\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>12</title>\n",
"<ellipse cx=\"336\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"336\" y=\"-86.3\">F</text>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"336\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"336\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">F</text>\n",
"</g>\n",
"<!-- 11&#45;&gt;12 -->\n",
"<g class=\"edge\" id=\"edge12\">\n",
"<title>11-&gt;12</title>\n",
"<path d=\"M308.7146,-144.5708C312.9597,-136.0807 318.1536,-125.6929 322.8663,-116.2674\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"326.024,-117.7782 327.3657,-107.2687 319.763,-114.6477 326.024,-117.7782\" stroke=\"#000000\"/>\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>11&#45;&gt;12</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M308.35,-144.76C312.71,-136.28 318.15,-125.71 323.04,-116.2\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"326.23,-117.64 327.7,-107.15 320.01,-114.44 326.23,-117.64\"/>\n",
"</g>\n",
"<!-- 12&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge11\">\n",
"<title>12-&gt;6</title>\n",
"<path d=\"M322.113,-74.3771C314.1445,-65.4125 303.9417,-53.9344 294.8244,-43.6774\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"297.3785,-41.2826 288.1189,-36.1338 292.1466,-45.9332 297.3785,-41.2826\" stroke=\"#000000\"/>\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>12&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M322.43,-74.15C314.3,-65.26 303.76,-53.74 294.43,-43.53\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"296.91,-41.06 287.58,-36.04 291.74,-45.78 296.91,-41.06\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 18,
@ -707,16 +714,17 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"210\" version=\"1.1\" width=\"220\" xmlns=\"http://www.w3.org/2000/svg\">\n",
"<polygon fill=\"cyan\" opacity=\".2\" points=\"20,0 200,120 200,210 20,210\"/>\n",
"<polygon fill=\"cyan\" opacity=\".2\" points=\"20,120 155,210 20,210\"/>\n",
"<polygon fill=\"magenta\" opacity=\".15\" points=\"200,0 20,120 20,210 200,210\"/>\n",
"<polygon fill=\"magenta\" opacity=\".15\" points=\"200,120 65,210 200,210\"/>\n",
"\n",
"<svg height=\"210\" width=\"220\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n",
"<polygon points=\"20,0 200,120 200,210 20,210\" fill=\"cyan\" opacity=\".2\" />\n",
"<polygon points=\"20,120 155,210 20,210\" fill=\"cyan\" opacity=\".2\" />\n",
"<polygon points=\"200,0 20,120 20,210 200,210\" fill=\"magenta\" opacity=\".15\" />\n",
"<polygon points=\"200,120 65,210 200,210\" fill=\"magenta\" opacity=\".15\" />\n",
"<g transform=\"translate(40,80)\">\n",
" <line stroke=\"red\" stroke-width=\"5\" x1=\"-10\" x2=\"10\" y1=\"-10\" y2=\"10\"/>\n",
" <line stroke=\"red\" stroke-width=\"5\" x1=\"-10\" x2=\"10\" y1=\"10\" y2=\"-10\"/>\n",
" <line x1=\"-10\" y1=\"-10\" x2=\"10\" y2=\"10\" stroke=\"red\" stroke-width=\"5\" />\n",
" <line x1=\"-10\" y1=\"10\" x2=\"10\" y2=\"-10\" stroke=\"red\" stroke-width=\"5\" />\n",
" </g>\n",
"<g font-size=\"14\" text-anchor=\"middle\">\n",
"<g text-anchor=\"middle\" font-size=\"14\">\n",
"<text x=\"110\" y=\"20\">Reactivity</text>\n",
"<text x=\"60\" y=\"65\">Recurrence</text>\n",
"<text x=\"160\" y=\"65\">Persistence</text>\n",
@ -725,15 +733,15 @@
"<text x=\"160\" y=\"185\">Guarantee</text>\n",
"</g>\n",
"<g font-size=\"14\">\n",
"<text fill=\"gray\" text-anchor=\"begin\" transform=\"rotate(-90,18,210)\" x=\"18\" y=\"210\">Monitor</text>\n",
"<text fill=\"gray\" text-anchor=\"end\" transform=\"rotate(-90,18,0)\" x=\"18\" y=\"0\">Deterministic Büchi</text>\n",
"<text fill=\"gray\" text-anchor=\"begin\" transform=\"rotate(-90,214,210)\" x=\"214\" y=\"210\">Terminal Büchi</text>\n",
"<text fill=\"gray\" text-anchor=\"end\" transform=\"rotate(-90,214,0)\" x=\"214\" y=\"0\">Weak Büchi</text>\n",
"<text text-anchor=\"begin\" transform=\"rotate(-90,18,210)\" x=\"18\" y=\"210\" fill=\"gray\">Monitor</text>\n",
"<text text-anchor=\"end\" transform=\"rotate(-90,18,0)\" x=\"18\" y=\"0\" fill=\"gray\">Deterministic Büchi</text>\n",
"<text text-anchor=\"begin\" transform=\"rotate(-90,214,210)\" x=\"214\" y=\"210\" fill=\"gray\">Terminal Büchi</text>\n",
"<text text-anchor=\"end\" transform=\"rotate(-90,214,0)\" x=\"214\" y=\"0\" fill=\"gray\">Weak Büchi</text>\n",
"</g>\n",
"</svg>"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 19,
@ -965,7 +973,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.3"
"version": "3.7.5"
}
},
"nbformat": 4,

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -31,60 +31,60 @@
"<?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.40.1 (20161225.0304)\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"171pt\" height=\"125pt\"\n",
" viewBox=\"0.00 0.00 171.00 124.80\" 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 120.8)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120.8)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" 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\" fill=\"#000000\">0</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\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-22C2.79,-22 17.15,-22 30.63,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22 30.94,-25.15 34.44,-22 30.94,-22 30.94,-22 30.94,-22 34.44,-22 30.94,-18.85 37.94,-22 37.94,-22\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" 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=\"#000000\" stroke=\"#000000\" 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\" fill=\"#000000\">a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.62,-39.04C48.32,-48.86 50.45,-58 56,-58 60.17,-58 62.4,-52.86 62.71,-46.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-39.04 65.85,-45.88 62.54,-42.53 62.71,-46.03 62.71,-46.03 62.71,-46.03 62.54,-42.53 59.56,-46.18 62.38,-39.04 62.38,-39.04\"/>\n",
"<text text-anchor=\"start\" x=\"52.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"#000000\" 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\" fill=\"#000000\">1</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\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.2,-22C85.07,-22 99.39,-22 111.89,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"119,-22 112,-25.15 115.5,-22 112,-22 112,-22 112,-22 115.5,-22 112,-18.85 119,-22 119,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n",
"<text text-anchor=\"start\" x=\"136.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M132.99,-42.58C131.89,-52.84 134.55,-62 141,-62 145.83,-62 148.54,-56.85 149.13,-49.95\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"149.01,-42.58 152.27,-49.53 149.06,-46.08 149.12,-49.58 149.12,-49.58 149.12,-49.58 149.06,-46.08 145.97,-49.63 149.01,-42.58 149.01,-42.58\"/>\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/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d680c3bd0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f930090abd0> >"
]
},
"execution_count": 2,
@ -113,277 +113,284 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"265pt\" viewBox=\"0.00 0.00 734.00 265.23\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(.7054 .7054) rotate(0) translate(4 372)\">\n",
"<?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.43.0 (0)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"265pt\"\n",
" viewBox=\"0.00 0.00 734.00 265.23\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7042253521126761 0.7042253521126761) rotate(0) translate(4 372)\">\n",
"<title>G</title>\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-372 1036.5483,-372 1036.5483,4 -4,4\" stroke=\"transparent\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-372 1036.55,-372 1036.55,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node2\">\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse cx=\"118\" cy=\"-252\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"118\" y=\"-248.3\">init</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-252\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"118\" y=\"-248.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M54.303,-252C63.4811,-252 73.8419,-252 83.4994,-252\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"90.7163,-252 83.7163,-255.1501 87.2163,-252 83.7163,-252.0001 83.7163,-252.0001 83.7163,-252.0001 87.2163,-252 83.7162,-248.8501 90.7163,-252 90.7163,-252\" stroke=\"#000000\"/>\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-252C63.46,-252 73.96,-252 83.7,-252\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-252 83.97,-255.15 87.47,-252 83.97,-252 83.97,-252 83.97,-252 87.47,-252 83.97,-248.85 90.97,-252 90.97,-252\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\">\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse cx=\"540.9691\" cy=\"-197\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"540.9691\" y=\"-200.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"540.9691\" y=\"-185.8\">!a &amp; b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"540.97\" cy=\"-197\" rx=\"37.45\" ry=\"26.74\"/>\n",
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-185.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>1-&gt;2</title>\n",
"<path d=\"M133.5354,-266.9299C168.8984,-299.0637 258.6983,-370.2928 340.7107,-350 412.9957,-332.1141 429.98,-313.6254 482.664,-261 491.6022,-252.0717 492.2837,-248.4539 500.664,-239 504.9963,-234.1127 509.7098,-229.0164 514.3359,-224.128\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"519.2993,-218.925 516.7468,-226.1644 516.8834,-221.4575 514.4676,-223.99 514.4676,-223.99 514.4676,-223.99 516.8834,-221.4575 512.1883,-221.8157 519.2993,-218.925 519.2993,-218.925\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"322.2107\" y=\"-356.8\">!a &amp; b</text>\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M134.19,-266.68C169.2,-298.67 258.8,-370.27 340.71,-350 413,-332.11 429.98,-313.63 482.66,-261 491.6,-252.07 492.34,-248.51 500.66,-239 504.91,-234.14 509.52,-229.06 514.04,-224.18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"518.88,-218.98 516.42,-226.25 516.5,-221.54 514.11,-224.1 514.11,-224.1 514.11,-224.1 516.5,-221.54 511.81,-221.96 518.88,-218.98 518.88,-218.98\"/>\n",
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-356.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\">\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse cx=\"250.3553\" cy=\"-156\" fill=\"#ffffaa\" rx=\"35.2113\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250.3553\" y=\"-159.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250.3553\" y=\"-144.8\">a &amp; b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"250.36\" cy=\"-156\" rx=\"35.21\" ry=\"26.74\"/>\n",
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>1-&gt;3</title>\n",
"<path d=\"M136.4034,-238.6516C157.5778,-223.2935 192.7241,-197.8011 218.3948,-179.1816\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"224.374,-174.8448 220.557,-181.5047 221.5407,-176.8998 218.7075,-178.9548 218.7075,-178.9548 218.7075,-178.9548 221.5407,-176.8998 216.858,-176.4049 224.374,-174.8448 224.374,-174.8448\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-221.8\">a &amp; b</text>\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M136.85,-238.85C157.77,-223.45 192.79,-197.66 218.21,-178.94\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"224.13,-174.58 220.36,-181.27 221.31,-176.65 218.49,-178.73 218.49,-178.73 218.49,-178.73 221.31,-176.65 216.62,-176.19 224.13,-174.58 224.13,-174.58\"/>\n",
"<text text-anchor=\"middle\" x=\"180\" y=\"-221.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\">\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse cx=\"396.1873\" cy=\"-197\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"396.1873\" y=\"-200.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"396.1873\" y=\"-185.8\">a &amp; !b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"396.19\" cy=\"-197\" rx=\"37.45\" ry=\"26.74\"/>\n",
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-185.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>1-&gt;4</title>\n",
"<path d=\"M144.539,-248.3342C177.6921,-243.6154 236.1001,-234.8431 285.7107,-225 310.3484,-220.1117 316.3617,-218.1677 340.7107,-212 345.0267,-210.9067 349.5237,-209.7388 354.0075,-208.5555\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"361.0147,-206.6919 355.0595,-211.5353 357.6323,-207.5915 354.2499,-208.4911 354.2499,-208.4911 354.2499,-208.4911 357.6323,-207.5915 353.4402,-205.447 361.0147,-206.6919 361.0147,-206.6919\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250.3553\" y=\"-240.8\">a &amp; !b</text>\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M144.88,-248.75C186.53,-243.23 270.85,-230.86 340.71,-213 345.2,-211.85 349.88,-210.59 354.53,-209.28\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"361.29,-207.36 355.42,-212.31 357.92,-208.32 354.56,-209.28 354.56,-209.28 354.56,-209.28 357.92,-208.32 353.69,-206.25 361.29,-207.36 361.29,-207.36\"/>\n",
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node6\">\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>5</title>\n",
"<ellipse cx=\"687.6295\" cy=\"-147\" fill=\"#ffffaa\" rx=\"35.2259\" ry=\"26.7574\" stroke=\"#000000\"/>\n",
"<ellipse cx=\"687.6295\" cy=\"-147\" fill=\"none\" rx=\"39.2112\" ry=\"30.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"687.6295\" y=\"-150.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"687.6295\" y=\"-135.8\">a &amp; b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"687.63\" cy=\"-147\" rx=\"35.23\" ry=\"26.76\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"687.63\" cy=\"-147\" rx=\"39.21\" ry=\"30.74\"/>\n",
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>2-&gt;5</title>\n",
"<path d=\"M574.9846,-185.4033C595.7665,-178.3183 622.5296,-169.1941 644.7541,-161.6172\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"651.494,-159.3195 645.8849,-164.5598 648.1812,-160.4489 644.8684,-161.5783 644.8684,-161.5783 644.8684,-161.5783 648.1812,-160.4489 643.8519,-158.5968 651.494,-159.3195 651.494,-159.3195\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"614.7742\" y=\"-179.8\">{a}</text>\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M575.16,-185.53C595.79,-178.4 622.52,-169.16 644.62,-161.52\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"651.32,-159.2 645.74,-164.47 648.02,-160.35 644.71,-161.49 644.71,-161.49 644.71,-161.49 648.02,-160.35 643.68,-158.51 651.32,-159.2 651.32,-159.2\"/>\n",
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g class=\"node\" id=\"node7\">\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>6</title>\n",
"<ellipse cx=\"835.4615\" cy=\"-148\" fill=\"#ffffaa\" rx=\"37.4556\" ry=\"26.7574\" stroke=\"#000000\"/>\n",
"<ellipse cx=\"835.4615\" cy=\"-148\" fill=\"none\" rx=\"41.4533\" ry=\"30.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"835.4615\" y=\"-151.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"835.4615\" y=\"-136.8\">!a &amp; b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"835.46\" cy=\"-148\" rx=\"37.46\" ry=\"26.76\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"835.46\" cy=\"-148\" rx=\"41.45\" ry=\"30.74\"/>\n",
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>2-&gt;6</title>\n",
"<path d=\"M574.6008,-209.3139C612.4084,-221.2984 675.2698,-235.6008 726.9848,-220 755.2712,-211.4669 782.9521,-192.8771 803.2716,-176.7249\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"808.802,-172.2442 805.3461,-179.0984 806.0825,-174.4475 803.3631,-176.6509 803.3631,-176.6509 803.3631,-176.6509 806.0825,-174.4475 801.38,-174.2034 808.802,-172.2442 808.802,-172.2442\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"687.6295\" y=\"-229.8\">{}</text>\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M574.75,-209.11C612.29,-221.14 675.27,-235.72 726.98,-220 755.27,-211.4 782.88,-192.61 803.03,-176.38\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"808.51,-171.88 805.1,-178.76 805.81,-174.1 803.1,-176.32 803.1,-176.32 803.1,-176.32 805.81,-174.1 801.11,-173.89 808.51,-171.88 808.51,-171.88\"/>\n",
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-229.8\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g class=\"node\" id=\"node8\">\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>7</title>\n",
"<ellipse cx=\"988.2433\" cy=\"-61\" fill=\"#ffffaa\" rx=\"37.4556\" ry=\"26.7574\" stroke=\"#000000\"/>\n",
"<ellipse cx=\"988.2433\" cy=\"-61\" fill=\"none\" rx=\"41.4533\" ry=\"30.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"988.2433\" y=\"-64.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"988.2433\" y=\"-49.8\">a &amp; !b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"988.24\" cy=\"-61\" rx=\"37.46\" ry=\"26.76\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"988.24\" cy=\"-61\" rx=\"41.45\" ry=\"30.74\"/>\n",
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>2-&gt;7</title>\n",
"<path d=\"M561.8988,-174.5523C582.1469,-154.1116 614.6347,-124.5248 648.2742,-107 742.5596,-57.8812 870.6426,-54.8953 939.5549,-57.5895\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"946.8476,-57.9047 939.7181,-60.7494 943.3509,-57.7535 939.8541,-57.6023 939.8541,-57.6023 939.8541,-57.6023 943.3509,-57.7535 939.9902,-54.4553 946.8476,-57.9047 946.8476,-57.9047\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"760.4848\" y=\"-76.8\">{a, b}</text>\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M562.66,-174.54C582.69,-154.1 614.86,-124.51 648.27,-107 742.55,-57.61 870.96,-54.83 939.5,-57.6\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"946.75,-57.93 939.62,-60.76 943.25,-57.77 939.76,-57.61 939.76,-57.61 939.76,-57.61 943.25,-57.77 939.9,-54.47 946.75,-57.93 946.75,-57.93\"/>\n",
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g class=\"node\" id=\"node9\">\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>8</title>\n",
"<ellipse cx=\"988.2433\" cy=\"-269\" fill=\"#ffffaa\" rx=\"40.1285\" ry=\"26.7574\" stroke=\"#000000\"/>\n",
"<ellipse cx=\"988.2433\" cy=\"-269\" fill=\"none\" rx=\"44.111\" ry=\"30.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"988.2433\" y=\"-272.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"988.2433\" y=\"-257.8\">!a &amp; !b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"988.24\" cy=\"-269\" rx=\"40.13\" ry=\"26.76\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"988.24\" cy=\"-269\" rx=\"44.11\" ry=\"30.74\"/>\n",
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-272.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-257.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>2-&gt;8</title>\n",
"<path d=\"M567.8944,-216.0651C577.4562,-222.1646 588.5208,-228.4959 599.2742,-233 619.9546,-241.6622 626.2778,-240.6552 648.2742,-245 712.527,-257.6913 728.7543,-261.1278 793.9848,-267 838.692,-271.0246 850.0552,-269.3333 894.9382,-270 908.3318,-270.199 922.8076,-270.1651 936.269,-270.028\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"943.6299,-269.942 936.6672,-273.1736 940.1302,-269.9829 936.6304,-270.0239 936.6304,-270.0239 936.6304,-270.0239 940.1302,-269.9829 936.5936,-266.8741 943.6299,-269.942 943.6299,-269.942\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"760.4848\" y=\"-268.8\">{b}</text>\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>2&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M568.11,-215.9C577.57,-222.05 588.56,-228.46 599.27,-233 619.92,-241.74 626.28,-240.66 648.27,-245 712.53,-257.69 728.75,-261.13 793.98,-267 838.69,-271.02 850.06,-269.33 894.94,-270 908.32,-270.2 922.8,-270.16 936.23,-270.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"943.57,-269.93 936.61,-273.17 940.07,-269.97 936.58,-270.02 936.58,-270.02 936.58,-270.02 940.07,-269.97 936.54,-266.87 943.57,-269.93 943.57,-269.93\"/>\n",
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-268.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge10\">\n",
"<title>3-&gt;2</title>\n",
"<path d=\"M284.6069,-148.5979C321.7859,-141.838 382.6752,-134.4994 433.664,-146 459.3748,-151.7991 486.1534,-164.5155 506.5281,-175.7988\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"512.6374,-179.2453 504.9929,-178.5494 509.589,-177.5256 506.5406,-175.8059 506.5406,-175.8059 506.5406,-175.8059 509.589,-177.5256 508.0884,-173.0623 512.6374,-179.2453 512.6374,-179.2453\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"396.1873\" y=\"-149.8\">{a}</text>\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M284.42,-148.77C321.3,-141.95 382.51,-134.36 433.66,-146 459.24,-151.82 485.84,-164.59 506.04,-175.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"512.36,-179.5 504.72,-178.77 509.32,-177.77 506.28,-176.03 506.28,-176.03 506.28,-176.03 509.32,-177.77 507.85,-173.3 512.36,-179.5 512.36,-179.5\"/>\n",
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-149.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>3-&gt;3</title>\n",
"<path d=\"M237.3457,-181.37C236.4485,-191.9238 240.785,-200.8701 250.3553,-200.8701 257.6826,-200.8701 261.9419,-195.6259 263.1333,-188.4312\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"263.365,-181.37 266.2837,-188.4696 263.2502,-184.8681 263.1354,-188.3662 263.1354,-188.3662 263.1354,-188.3662 263.2502,-184.8681 259.9871,-188.2629 263.365,-181.37 263.365,-181.37\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250.3553\" y=\"-204.6701\">{}</text>\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M237.35,-181.37C236.45,-191.92 240.79,-200.87 250.36,-200.87 257.68,-200.87 261.94,-195.63 263.13,-188.43\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"263.36,-181.37 266.28,-188.47 263.25,-184.87 263.14,-188.37 263.14,-188.37 263.14,-188.37 263.25,-184.87 259.99,-188.26 263.36,-181.37 263.36,-181.37\"/>\n",
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-204.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge11\">\n",
"<title>3-&gt;4</title>\n",
"<path d=\"M277.0942,-173.7422C285.324,-178.4457 294.6179,-183.0341 303.7107,-186 318.7696,-190.912 335.846,-193.6754 351.1905,-195.2153\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"358.5677,-195.8771 351.3142,-198.389 355.0817,-195.5643 351.5957,-195.2516 351.5957,-195.2516 351.5957,-195.2516 355.0817,-195.5643 351.8771,-192.1142 358.5677,-195.8771 358.5677,-195.8771\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"322.2107\" y=\"-196.8\">{b}</text>\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M277.29,-173.59C285.43,-178.34 294.66,-183 303.71,-186 318.72,-190.97 335.77,-193.75 351.05,-195.28\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"358.4,-195.93 351.14,-198.45 354.91,-195.62 351.42,-195.31 351.42,-195.31 351.42,-195.31 354.91,-195.62 351.7,-192.17 358.4,-195.93 358.4,-195.93\"/>\n",
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-197.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge13\">\n",
"<title>3-&gt;5</title>\n",
"<path d=\"M281.8433,-143.7301C288.9363,-141.4312 296.501,-139.3339 303.7107,-138 423.977,-115.7483 569.0261,-130.0094 641.5805,-139.8797\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"648.7954,-140.8795 641.4292,-143.0388 645.3285,-140.399 641.8616,-139.9186 641.8616,-139.9186 641.8616,-139.9186 645.3285,-140.399 642.294,-136.7984 648.7954,-140.8795 648.7954,-140.8795\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"467.164\" y=\"-130.8\">{}</text>\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>3&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M281.96,-143.82C289,-141.48 296.53,-139.35 303.71,-138 424.23,-115.34 569.82,-130 641.82,-139.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"648.98,-140.98 641.61,-143.12 645.51,-140.49 642.05,-140 642.05,-140 642.05,-140 645.51,-140.49 642.49,-136.88 648.98,-140.98 648.98,-140.98\"/>\n",
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-130.8\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge14\">\n",
"<title>3-&gt;6</title>\n",
"<path d=\"M267.102,-132.0313C291.5104,-100.2136 340.1084,-48 396.1873,-48 396.1873,-48 396.1873,-48 614.7742,-48 685.7369,-48 759.0106,-91.4276 800.7319,-121.0456\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"806.6546,-125.3085 799.133,-123.7758 803.8138,-123.2638 800.9731,-121.2192 800.9731,-121.2192 800.9731,-121.2192 803.8138,-123.2638 802.8133,-118.6626 806.6546,-125.3085 806.6546,-125.3085\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"540.9691\" y=\"-51.8\">{a}</text>\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>3&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M267.59,-132.3C291.51,-100.51 339.45,-48 395.19,-48 395.19,-48 395.19,-48 615.77,-48 686.6,-48 759.6,-91.92 800.78,-121.55\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"806.62,-125.81 799.11,-124.23 803.8,-123.74 800.97,-121.68 800.97,-121.68 800.97,-121.68 803.8,-123.74 802.82,-119.14 806.62,-125.81 806.62,-125.81\"/>\n",
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge15\">\n",
"<title>3-&gt;7</title>\n",
"<path d=\"M260.5421,-129.8891C279.779,-85.4797 325.9314,0 396.1873,0 396.1873,0 396.1873,0 835.4615,0 877.1907,0 921.0539,-19.8698 951.0225,-36.9288\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"957.2009,-40.5182 949.5658,-39.7255 954.1745,-38.76 951.1482,-37.0018 951.1482,-37.0018 951.1482,-37.0018 954.1745,-38.76 952.7306,-34.278 957.2009,-40.5182 957.2009,-40.5182\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"614.7742\" y=\"-3.8\">{b}</text>\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>3&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M261.15,-130.24C279.87,-85.93 325.19,0 395.19,0 395.19,0 395.19,0 836.46,0 877.85,0 921.27,-20 950.83,-37.09\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"956.93,-40.69 949.3,-39.84 953.91,-38.91 950.9,-37.13 950.9,-37.13 950.9,-37.13 953.91,-38.91 952.5,-34.42 956.93,-40.69 956.93,-40.69\"/>\n",
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge16\">\n",
"<title>3-&gt;8</title>\n",
"<path d=\"M264.0204,-180.9661C270.6079,-193.0415 278.6036,-207.7566 285.7107,-221 319.2245,-283.4504 325.3126,-336 396.1873,-336 396.1873,-336 396.1873,-336 835.4615,-336 877.7786,-336 921.5587,-314.1757 951.3476,-295.4388\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"957.4863,-291.4964 953.2985,-297.9296 954.5413,-293.3878 951.5963,-295.2791 951.5963,-295.2791 951.5963,-295.2791 954.5413,-293.3878 949.8941,-292.6286 957.4863,-291.4964 957.4863,-291.4964\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"614.7742\" y=\"-339.8\">{a, b}</text>\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>3&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M264.51,-180.92C279.97,-210.18 303.55,-254.79 303.71,-255 337.27,-297.69 340.88,-336 395.19,-336 395.19,-336 395.19,-336 836.46,-336 878.45,-336 921.78,-314.04 951.16,-295.26\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"957.21,-291.31 953.07,-297.77 954.28,-293.22 951.35,-295.14 951.35,-295.14 951.35,-295.14 954.28,-293.22 949.63,-292.5 957.21,-291.31 957.21,-291.31\"/>\n",
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 9 -->\n",
"<g class=\"node\" id=\"node10\">\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>9</title>\n",
"<ellipse cx=\"540.9691\" cy=\"-275\" fill=\"#ffffaa\" rx=\"40.1111\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"540.9691\" y=\"-278.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"540.9691\" y=\"-263.8\">!a &amp; !b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"540.97\" cy=\"-275\" rx=\"40.11\" ry=\"26.74\"/>\n",
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-263.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;9 -->\n",
"<g class=\"edge\" id=\"edge12\">\n",
"<title>3-&gt;9</title>\n",
"<path d=\"M266.002,-180.6084C284.4902,-207.1967 317.9496,-248.149 358.7107,-266 401.6961,-284.8252 455.9566,-284.8785 494.0531,-281.5807\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"501.4487,-280.881 494.7765,-284.6764 497.9643,-281.2107 494.4798,-281.5404 494.4798,-281.5404 494.4798,-281.5404 497.9643,-281.2107 494.1831,-278.4044 501.4487,-280.881 501.4487,-280.881\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"396.1873\" y=\"-285.8\">{a, b}</text>\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>3&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M266.43,-180.23C284.59,-206.89 317.81,-248.31 358.71,-266 401.82,-284.65 456.18,-284.63 494.07,-281.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"501.42,-280.67 494.75,-284.46 497.94,-281 494.45,-281.33 494.45,-281.33 494.45,-281.33 497.94,-281 494.16,-278.19 501.42,-280.67 501.42,-280.67\"/>\n",
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-285.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge18\">\n",
"<title>4-&gt;2</title>\n",
"<path d=\"M433.8491,-197C452.8776,-197 476.1016,-197 496.0552,-197\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"503.2447,-197 496.2447,-200.1501 499.7447,-197 496.2447,-197.0001 496.2447,-197.0001 496.2447,-197.0001 499.7447,-197 496.2446,-193.8501 503.2447,-197 503.2447,-197\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"467.164\" y=\"-200.8\">{a, b}</text>\n",
"<g id=\"edge18\" class=\"edge\">\n",
"<title>4&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M433.96,-197C452.94,-197 476.24,-197 496.15,-197\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"503.32,-197 496.32,-200.15 499.82,-197 496.32,-197 496.32,-197 496.32,-197 499.82,-197 496.32,-193.85 503.32,-197 503.32,-197\"/>\n",
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge17\">\n",
"<title>4-&gt;3</title>\n",
"<path d=\"M368.0179,-179.1334C359.53,-174.4856 349.9958,-169.9583 340.7107,-167 325.5716,-162.1766 308.3862,-159.4452 293.0974,-157.9066\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"285.7616,-157.2431 293.0169,-154.7365 289.2474,-157.5584 292.7331,-157.8737 292.7331,-157.8737 292.7331,-157.8737 289.2474,-157.5584 292.4494,-161.0109 285.7616,-157.2431 285.7616,-157.2431\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"322.2107\" y=\"-170.8\">{b}</text>\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>4&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M367.84,-179.29C359.43,-174.59 349.96,-169.99 340.71,-167 325.63,-162.12 308.48,-159.38 293.26,-157.85\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"285.96,-157.19 293.21,-154.68 289.45,-157.51 292.93,-157.82 292.93,-157.82 292.93,-157.82 289.45,-157.51 292.65,-160.96 285.96,-157.19 285.96,-157.19\"/>\n",
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge19\">\n",
"<title>4-&gt;4</title>\n",
"<path d=\"M383.1777,-222.37C382.2805,-232.9238 386.617,-241.8701 396.1873,-241.8701 403.5146,-241.8701 407.7739,-236.6259 408.9653,-229.4312\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"409.197,-222.37 412.1157,-229.4696 409.0822,-225.8681 408.9674,-229.3662 408.9674,-229.3662 408.9674,-229.3662 409.0822,-225.8681 405.8191,-229.2629 409.197,-222.37 409.197,-222.37\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"396.1873\" y=\"-245.6701\">{}</text>\n",
"<g id=\"edge19\" class=\"edge\">\n",
"<title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M383.18,-222.37C382.28,-232.92 386.62,-241.87 396.19,-241.87 403.51,-241.87 407.77,-236.63 408.97,-229.43\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"409.2,-222.37 412.12,-229.47 409.08,-225.87 408.97,-229.37 408.97,-229.37 408.97,-229.37 409.08,-225.87 405.82,-229.26 409.2,-222.37 409.2,-222.37\"/>\n",
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-245.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;9 -->\n",
"<g class=\"edge\" id=\"edge20\">\n",
"<title>4-&gt;9</title>\n",
"<path d=\"M426.1862,-213.1617C448.5398,-225.2045 479.22,-241.7332 503.2377,-254.6725\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"509.5062,-258.0496 501.8496,-257.5027 506.4249,-256.3896 503.3436,-254.7295 503.3436,-254.7295 503.3436,-254.7295 506.4249,-256.3896 504.8377,-251.9564 509.5062,-258.0496 509.5062,-258.0496\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"467.164\" y=\"-245.8\">{a}</text>\n",
"<g id=\"edge20\" class=\"edge\">\n",
"<title>4&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M426.43,-212.97C448.59,-225.08 479.21,-241.81 503.07,-254.84\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"509.29,-258.24 501.64,-257.65 506.22,-256.56 503.15,-254.88 503.15,-254.88 503.15,-254.88 506.22,-256.56 504.66,-252.12 509.29,-258.24 509.29,-258.24\"/>\n",
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge21\">\n",
"<title>5-&gt;5</title>\n",
"<path d=\"M674.1592,-176.0993C673.7175,-186.9436 678.2076,-195.8701 687.6295,-195.8701 694.8431,-195.8701 699.1658,-190.6375 700.5977,-183.3179\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"701.0998,-176.0993 703.7564,-183.301 700.8569,-179.5908 700.6139,-183.0824 700.6139,-183.0824 700.6139,-183.0824 700.8569,-179.5908 697.4715,-182.8637 701.0998,-176.0993 701.0998,-176.0993\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"687.6295\" y=\"-199.6701\">{}</text>\n",
"<g id=\"edge21\" class=\"edge\">\n",
"<title>5&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M674.16,-176.1C673.72,-186.94 678.21,-195.87 687.63,-195.87 694.84,-195.87 699.17,-190.64 700.6,-183.32\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"701.1,-176.1 703.76,-183.3 700.86,-179.59 700.61,-183.08 700.61,-183.08 700.61,-183.08 700.86,-179.59 697.47,-182.86 701.1,-176.1 701.1,-176.1\"/>\n",
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge22\">\n",
"<title>5-&gt;6</title>\n",
"<path d=\"M726.0974,-140.1215C732.39,-139.2392 738.855,-138.478 744.9848,-138 758.7209,-136.9288 762.2548,-136.8538 775.9848,-138 779.9956,-138.3348 784.1428,-138.7945 788.295,-139.3341\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"795.2645,-140.3096 787.8954,-142.4588 791.7983,-139.8244 788.3321,-139.3392 788.3321,-139.3392 788.3321,-139.3392 791.7983,-139.8244 788.7687,-136.2196 795.2645,-140.3096 795.2645,-140.3096\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"760.4848\" y=\"-141.8\">{a}</text>\n",
"<g id=\"edge22\" class=\"edge\">\n",
"<title>5&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M726.12,-140.17C732.4,-139.26 738.86,-138.49 744.98,-138 758.72,-136.91 762.26,-136.83 775.98,-138 780,-138.34 784.14,-138.81 788.3,-139.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"795.26,-140.36 787.88,-142.48 791.8,-139.86 788.33,-139.37 788.33,-139.37 788.33,-139.37 791.8,-139.86 788.78,-136.25 795.26,-140.36 795.26,-140.36\"/>\n",
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-141.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge23\">\n",
"<title>5-&gt;7</title>\n",
"<path d=\"M719.1038,-127.7822C739.7107,-116.028 767.6145,-101.6376 793.9848,-93 842.1461,-77.2247 899.6839,-68.9884 939.5807,-64.8502\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"946.8188,-64.1242 940.1681,-67.9571 943.3363,-64.4736 939.8537,-64.8229 939.8537,-64.8229 939.8537,-64.8229 943.3363,-64.4736 939.5394,-61.6886 946.8188,-64.1242 946.8188,-64.1242\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"835.4615\" y=\"-96.8\">{b}</text>\n",
"<g id=\"edge23\" class=\"edge\">\n",
"<title>5&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M719.33,-128.04C739.78,-116.24 767.64,-101.7 793.98,-93 842.17,-77.09 899.84,-68.86 939.57,-64.75\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"946.77,-64.04 940.12,-67.87 943.29,-64.38 939.81,-64.73 939.81,-64.73 939.81,-64.73 943.29,-64.38 939.49,-61.6 946.77,-64.04 946.77,-64.04\"/>\n",
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge24\">\n",
"<title>5-&gt;8</title>\n",
"<path d=\"M714.3735,-169.7723C734.929,-186.1996 764.6806,-207.7351 793.9848,-221 840.3144,-241.9716 897.1792,-254.6543 937.3813,-261.6703\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"944.6877,-262.9151 937.258,-264.8446 941.2374,-262.3273 937.7871,-261.7394 937.7871,-261.7394 937.7871,-261.7394 941.2374,-262.3273 938.3162,-258.6341 944.6877,-262.9151 944.6877,-262.9151\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"835.4615\" y=\"-251.8\">{a, b}</text>\n",
"<g id=\"edge24\" class=\"edge\">\n",
"<title>5&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M715.09,-169.77C735.44,-186.2 764.9,-207.74 793.98,-221 840.33,-242.13 897.34,-254.84 937.39,-261.82\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"944.66,-263.06 937.23,-264.99 941.21,-262.47 937.76,-261.88 937.76,-261.88 937.76,-261.88 941.21,-262.47 938.29,-258.78 944.66,-263.06 944.66,-263.06\"/>\n",
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge25\">\n",
"<title>6-&gt;5</title>\n",
"<path d=\"M794.026,-152.1587C778.6278,-153.2119 761.0094,-153.8359 744.9848,-153 741.3902,-152.8125 737.6739,-152.5593 733.9411,-152.2626\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"726.7699,-151.6442 734.0147,-149.1073 730.257,-151.9449 733.744,-152.2457 733.744,-152.2457 733.744,-152.2457 730.257,-151.9449 733.4733,-155.384 726.7699,-151.6442 726.7699,-151.6442\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"760.4848\" y=\"-156.8\">{a}</text>\n",
"<g id=\"edge25\" class=\"edge\">\n",
"<title>6&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M793.93,-152.13C778.6,-153.21 760.99,-153.85 744.98,-153 741.39,-152.81 737.68,-152.55 733.95,-152.25\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"726.78,-151.62 734.03,-149.09 730.27,-151.92 733.75,-152.23 733.75,-152.23 733.75,-152.23 730.27,-151.92 733.48,-155.37 726.78,-151.62 726.78,-151.62\"/>\n",
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge26\">\n",
"<title>6-&gt;6</title>\n",
"<path d=\"M821.6001,-177.5835C821.302,-188.208 825.9224,-196.8701 835.4615,-196.8701 842.7649,-196.8701 847.185,-191.7925 848.722,-184.6442\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"849.323,-177.5835 851.8679,-184.8255 849.0261,-181.0709 848.7292,-184.5583 848.7292,-184.5583 848.7292,-184.5583 849.0261,-181.0709 845.5906,-184.2911 849.323,-177.5835 849.323,-177.5835\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"835.4615\" y=\"-200.6701\">{}</text>\n",
"<g id=\"edge26\" class=\"edge\">\n",
"<title>6&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M821.6,-177.58C821.3,-188.21 825.92,-196.87 835.46,-196.87 842.76,-196.87 847.19,-191.79 848.72,-184.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"849.32,-177.58 851.87,-184.83 849.03,-181.07 848.73,-184.56 848.73,-184.56 848.73,-184.56 849.03,-181.07 845.59,-184.29 849.32,-177.58 849.32,-177.58\"/>\n",
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-200.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge27\">\n",
"<title>6-&gt;7</title>\n",
"<path d=\"M869.1148,-129.7254C886.2048,-120.3634 907.2527,-108.7078 925.9382,-98 933.5276,-93.6508 941.5907,-88.9346 949.3101,-84.3717\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"955.6957,-80.5863 951.2806,-86.8656 952.685,-82.3711 949.6742,-84.1559 949.6742,-84.1559 949.6742,-84.1559 952.685,-82.3711 948.0679,-81.4462 955.6957,-80.5863 955.6957,-80.5863\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"910.4382\" y=\"-118.8\">{a, b}</text>\n",
"<g id=\"edge27\" class=\"edge\">\n",
"<title>6&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M869.33,-129.97C886.31,-120.58 907.32,-108.82 925.94,-98 933.5,-93.61 941.53,-88.84 949.2,-84.23\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"955.54,-80.41 951.18,-86.72 952.55,-82.21 949.55,-84.02 949.55,-84.02 949.55,-84.02 952.55,-82.21 947.92,-81.32 955.54,-80.41 955.54,-80.41\"/>\n",
"<text text-anchor=\"middle\" x=\"910.44\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge28\">\n",
"<title>6-&gt;8</title>\n",
"<path d=\"M864.455,-170.6225C882.2377,-184.5298 905.4493,-202.7405 925.9382,-219 934.9349,-226.1396 944.6309,-233.8923 953.6321,-241.1143\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"959.1345,-245.5321 951.704,-243.6058 956.4053,-243.3409 953.6761,-241.1496 953.6761,-241.1496 953.6761,-241.1496 956.4053,-243.3409 955.6483,-238.6933 959.1345,-245.5321 959.1345,-245.5321\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"910.4382\" y=\"-222.8\">{b}</text>\n",
"<g id=\"edge28\" class=\"edge\">\n",
"<title>6&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M864.75,-170.29C882.39,-184.23 905.54,-202.59 925.94,-219 934.89,-226.2 944.53,-234.03 953.47,-241.32\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"958.92,-245.77 951.51,-243.78 956.21,-243.56 953.5,-241.34 953.5,-241.34 953.5,-241.34 956.21,-243.56 955.49,-238.9 958.92,-245.77 958.92,-245.77\"/>\n",
"<text text-anchor=\"middle\" x=\"910.44\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 3,
@ -412,142 +419,149 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"135pt\" viewBox=\"0.00 0.00 734.00 134.67\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(.9484 .9484) rotate(0) translate(4 138)\">\n",
"<?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.43.0 (0)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"136pt\"\n",
" viewBox=\"0.00 0.00 734.00 135.62\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.9523809523809523 0.9523809523809523) rotate(0) translate(4 139)\">\n",
"<title>G</title>\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-138 769.9533,-138 769.9533,4 -4,4\" stroke=\"transparent\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-139 769.95,-139 769.95,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node2\">\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse cx=\"118\" cy=\"-61\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"118\" y=\"-57.3\">init</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-61\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"118\" y=\"-57.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M54.303,-61C63.4811,-61 73.8419,-61 83.4994,-61\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"90.7163,-61 83.7163,-64.1501 87.2163,-61 83.7163,-61.0001 83.7163,-61.0001 83.7163,-61.0001 87.2163,-61 83.7162,-57.8501 90.7163,-61 90.7163,-61\" stroke=\"#000000\"/>\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-61C63.46,-61 73.96,-61 83.7,-61\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-61 83.97,-64.15 87.47,-61 83.97,-61 83.97,-61 83.97,-61 87.47,-61 83.97,-57.85 90.97,-61 90.97,-61\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\">\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"#ffffaa\" points=\"537.9533,-131 483.9533,-131 483.9533,-93 537.9533,-93 537.9533,-131\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"510.9533\" y=\"-115.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"510.9533\" y=\"-100.8\">!a &amp; b</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"537.95,-131 483.95,-131 483.95,-93 537.95,-93 537.95,-131\"/>\n",
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>1-&gt;2</title>\n",
"<path d=\"M140.6088,-71.4262C147.6839,-74.4492 155.582,-77.5829 163,-80 240.6956,-105.3164 260.8258,-112.6044 342,-122 375.0917,-125.8302 383.6425,-122.3399 416.9533,-122 438.7345,-121.7778 444.3,-123.3674 465.9533,-121 469.5248,-120.6095 473.2342,-120.0774 476.9223,-119.4655\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"483.9465,-118.2071 477.6117,-122.5423 480.5013,-118.8244 477.0562,-119.4416 477.0562,-119.4416 477.0562,-119.4416 480.5013,-118.8244 476.5006,-116.341 483.9465,-118.2071 483.9465,-118.2071\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-122.8\">!a &amp; b</text>\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M140.65,-71.23C147.68,-74.31 155.58,-77.53 163,-80 240.62,-105.87 260.75,-113.38 342,-123 375.08,-126.92 383.65,-123.68 416.95,-123 438.74,-122.56 444.32,-123.64 465.95,-121 469.35,-120.59 472.88,-120.05 476.4,-119.44\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"483.54,-118.12 477.23,-122.49 480.1,-118.76 476.66,-119.39 476.66,-119.39 476.66,-119.39 480.1,-118.76 476.09,-116.3 483.54,-118.12 483.54,-118.12\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\">\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3</title>\n",
"<polygon fill=\"#ffffaa\" points=\"269,-80 215,-80 215,-42 269,-42 269,-80\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"242\" y=\"-64.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"242\" y=\"-49.8\">a &amp; b</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"269,-80 215,-80 215,-42 269,-42 269,-80\"/>\n",
"<text text-anchor=\"middle\" x=\"242\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"242\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>1-&gt;3</title>\n",
"<path d=\"M145.2123,-61C163.6257,-61 188.0917,-61 207.818,-61\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"214.8512,-61 207.8512,-64.1501 211.3512,-61 207.8512,-61.0001 207.8512,-61.0001 207.8512,-61.0001 211.3512,-61 207.8511,-57.8501 214.8512,-61 214.8512,-61\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-64.8\">a &amp; b</text>\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M145.17,-61C163.51,-61 188.15,-61 207.86,-61\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"214.87,-61 207.87,-64.15 211.37,-61 207.87,-61 207.87,-61 207.87,-61 211.37,-61 207.87,-57.85 214.87,-61 214.87,-61\"/>\n",
"<text text-anchor=\"middle\" x=\"180\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\">\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse cx=\"379.4767\" cy=\"-55\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"379.4767\" y=\"-58.8\">0</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"379.4767\" y=\"-43.8\">a &amp; !b</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"379.48\" cy=\"-55\" rx=\"37.45\" ry=\"26.74\"/>\n",
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-58.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-43.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>1-&gt;4</title>\n",
"<path d=\"M138.3381,-48.9634C157.3996,-38.4299 187.0669,-23.9138 215,-18 258.4402,-8.8031 308.1565,-23.5006 341.4546,-37.0022\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"348.3027,-39.8561 340.6296,-40.0709 345.072,-38.5097 341.8413,-37.1633 341.8413,-37.1633 341.8413,-37.1633 345.072,-38.5097 343.0531,-34.2557 348.3027,-39.8561 348.3027,-39.8561\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"242\" y=\"-21.8\">a &amp; !b</text>\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M138.75,-49.17C157.59,-38.62 187.14,-23.95 215,-18 258.44,-8.72 308.19,-23.66 341.29,-37.24\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"348.09,-40.1 340.42,-40.29 344.87,-38.74 341.64,-37.38 341.64,-37.38 341.64,-37.38 344.87,-38.74 342.87,-34.48 348.09,-40.1 348.09,-40.1\"/>\n",
"<text text-anchor=\"middle\" x=\"242\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node6\">\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>5</title>\n",
"<polygon fill=\"#ffffaa\" points=\"647.9533,-102 593.9533,-102 593.9533,-64 647.9533,-64 647.9533,-102\" stroke=\"#000000\"/>\n",
"<polygon fill=\"none\" points=\"651.9533,-106 589.9533,-106 589.9533,-60 651.9533,-60 651.9533,-106\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"620.9533\" y=\"-86.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"620.9533\" y=\"-71.8\">a &amp; b</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"647.95,-102 593.95,-102 593.95,-64 647.95,-64 647.95,-102\"/>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"651.95,-106 589.95,-106 589.95,-60 651.95,-60 651.95,-106\"/>\n",
"<text text-anchor=\"middle\" x=\"620.95\" y=\"-86.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"620.95\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>2-&gt;5</title>\n",
"<path d=\"M538.1443,-104.8315C551.5943,-101.2856 568.0552,-96.9459 582.7475,-93.0724\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"589.7971,-91.2139 583.8314,-96.0444 586.4128,-92.1062 583.0284,-92.9985 583.0284,-92.9985 583.0284,-92.9985 586.4128,-92.1062 582.2253,-89.9525 589.7971,-91.2139 589.7971,-91.2139\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"563.9533\" y=\"-103.8\">{a}</text>\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M538.1,-104.98C551.51,-101.38 568.08,-96.93 582.79,-92.98\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"589.85,-91.08 583.9,-95.94 586.47,-91.99 583.09,-92.9 583.09,-92.9 583.09,-92.9 586.47,-91.99 582.27,-89.86 589.85,-91.08 589.85,-91.08\"/>\n",
"<text text-anchor=\"middle\" x=\"563.95\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>3-&gt;2</title>\n",
"<path d=\"M269.4116,-71.9981C275.1743,-74.1285 281.2496,-76.2423 287,-78 352.3724,-97.9826 432.2202,-106.5042 476.7468,-109.9161\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"483.8463,-110.4395 476.6336,-113.0662 480.3557,-110.1821 476.8652,-109.9247 476.8652,-109.9247 476.8652,-109.9247 480.3557,-110.1821 477.0968,-106.7832 483.8463,-110.4395 483.8463,-110.4395\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"379.4767\" y=\"-106.8\">{a}</text>\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M269.32,-71.84C275.09,-74.03 281.21,-76.21 287,-78 352.37,-98.25 432.39,-106.7 476.6,-110.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"483.64,-110.53 476.43,-113.16 480.15,-110.28 476.66,-110.02 476.66,-110.02 476.66,-110.02 480.15,-110.28 476.89,-106.88 483.64,-110.53 483.64,-110.53\"/>\n",
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>3-&gt;4</title>\n",
"<path d=\"M269.1038,-48.2461C274.8887,-46.0707 281.051,-44.1457 287,-43 303.2676,-39.8672 321.3057,-41.1561 337.0998,-43.8325\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"344.1842,-45.1489 336.7265,-46.967 340.7431,-44.5095 337.3021,-43.87 337.3021,-43.87 337.3021,-43.87 340.7431,-44.5095 337.8776,-40.773 344.1842,-45.1489 344.1842,-45.1489\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-46.8\">{b}</text>\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M269.01,-48.43C274.8,-46.18 281.01,-44.18 287,-43 303.35,-39.78 321.53,-41.17 337.34,-43.94\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"344.42,-45.3 336.96,-47.07 340.99,-44.64 337.55,-43.98 337.55,-43.98 337.55,-43.98 340.99,-44.64 338.14,-40.88 344.42,-45.3 344.42,-45.3\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g class=\"node\" id=\"node7\">\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>6</title>\n",
"<polygon fill=\"#ffffaa\" points=\"761.9533,-64 707.9533,-64 707.9533,-26 761.9533,-26 761.9533,-64\" stroke=\"#000000\"/>\n",
"<polygon fill=\"none\" points=\"765.9533,-68 703.9533,-68 703.9533,-22 765.9533,-22 765.9533,-68\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"734.9533\" y=\"-48.8\">1</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"734.9533\" y=\"-33.8\">!a &amp; b</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"761.95,-64 707.95,-64 707.95,-26 761.95,-26 761.95,-64\"/>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"765.95,-68 703.95,-68 703.95,-22 765.95,-22 765.95,-68\"/>\n",
"<text text-anchor=\"middle\" x=\"734.95\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"middle\" x=\"734.95\" y=\"-33.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>3-&gt;6</title>\n",
"<path d=\"M267.8732,-41.6992C294.441,-23.8281 337.6983,0 379.4767,0 379.4767,0 379.4767,0 620.9533,0 647.8722,0 676.0263,-10.9899 697.6206,-22.1076\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"703.8163,-25.3933 696.1562,-24.8965 700.7242,-23.7534 697.6321,-22.1136 697.6321,-22.1136 697.6321,-22.1136 700.7242,-23.7534 699.1079,-19.3307 703.8163,-25.3933 703.8163,-25.3933\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"510.9533\" y=\"-3.8\">{a}</text>\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>3&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M268.45,-41.7C294.6,-23.83 337.21,0 378.48,0 378.48,0 378.48,0 621.95,0 648.54,0 676.28,-11.05 697.51,-22.2\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"703.88,-25.65 696.22,-25.09 700.8,-23.99 697.72,-22.32 697.72,-22.32 697.72,-22.32 700.8,-23.99 699.22,-19.55 703.88,-25.65 703.88,-25.65\"/>\n",
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge10\">\n",
"<title>4-&gt;2</title>\n",
"<path d=\"M413.0566,-67.325C429.205,-73.4741 448.7467,-81.2426 465.9533,-89 469.6426,-90.6633 473.4633,-92.4739 477.2483,-94.3246\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"483.555,-97.4585 475.8845,-97.1644 480.4206,-95.9009 477.2862,-94.3434 477.2862,-94.3434 477.2862,-94.3434 480.4206,-95.9009 478.688,-91.5225 483.555,-97.4585 483.555,-97.4585\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"450.4533\" y=\"-92.8\">{a, b}</text>\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>4&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M413.28,-67.14C429.33,-73.3 448.82,-81.14 465.95,-89 469.67,-90.7 473.51,-92.57 477.32,-94.47\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"483.65,-97.69 475.98,-97.32 480.53,-96.1 477.41,-94.51 477.41,-94.51 477.41,-94.51 480.53,-96.1 478.84,-91.71 483.65,-97.69 483.65,-97.69\"/>\n",
"<text text-anchor=\"middle\" x=\"450.45\" y=\"-92.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>4-&gt;3</title>\n",
"<path d=\"M341.8805,-57.122C335.9001,-57.4339 329.7813,-57.7379 324,-58 308.4882,-58.7031 291.3199,-59.3514 276.7179,-59.864\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"269.3382,-60.1193 276.2251,-56.729 272.8361,-59.9982 276.334,-59.8772 276.334,-59.8772 276.334,-59.8772 272.8361,-59.9982 276.443,-63.0253 269.3382,-60.1193 269.3382,-60.1193\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-62.8\">{b}</text>\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M341.85,-57.11C335.89,-57.42 329.77,-57.73 324,-58 308.44,-58.72 291.19,-59.37 276.62,-59.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"269.27,-60.15 276.16,-56.75 272.77,-60.02 276.27,-59.9 276.27,-59.9 276.27,-59.9 272.77,-60.02 276.38,-63.05 269.27,-60.15 269.27,-60.15\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-62.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge11\">\n",
"<title>5-&gt;6</title>\n",
"<path d=\"M645.3557,-59.8566C652.7145,-54.2534 661.1829,-49.0146 669.9533,-46 678.3751,-43.1052 687.7805,-41.9 696.7631,-41.6177\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"703.8494,-41.5746 696.8688,-44.7672 700.3495,-41.5959 696.8495,-41.6173 696.8495,-41.6173 696.8495,-41.6173 700.3495,-41.5959 696.8303,-38.4673 703.8494,-41.5746 703.8494,-41.5746\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"677.9533\" y=\"-49.8\">{a}</text>\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>5&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M645.79,-59.86C653,-54.26 661.31,-49.02 669.95,-46 678.31,-43.08 687.67,-41.88 696.59,-41.61\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"703.63,-41.58 696.64,-44.76 700.13,-41.6 696.63,-41.61 696.63,-41.61 696.63,-41.61 700.13,-41.6 696.62,-38.46 703.63,-41.58 703.63,-41.58\"/>\n",
"<text text-anchor=\"middle\" x=\"677.95\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge12\">\n",
"<title>6-&gt;5</title>\n",
"<path d=\"M703.84,-55.3711C690.0211,-59.9774 673.6249,-65.4428 659.0777,-70.2919\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"652.1043,-72.6163 657.749,-67.4143 655.4247,-71.5095 658.7451,-70.4027 658.7451,-70.4027 658.7451,-70.4027 655.4247,-71.5095 659.7413,-73.391 652.1043,-72.6163 652.1043,-72.6163\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"677.9533\" y=\"-69.8\">{a}</text>\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>6&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M703.86,-55.21C690.04,-59.9 673.52,-65.51 658.94,-70.45\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"651.97,-72.82 657.58,-67.58 655.28,-71.69 658.6,-70.57 658.6,-70.57 658.6,-70.57 655.28,-71.69 659.61,-73.55 651.97,-72.82 651.97,-72.82\"/>\n",
"<text text-anchor=\"middle\" x=\"677.95\" y=\"-69.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 4,
@ -575,123 +589,130 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"187pt\" viewBox=\"0.00 0.00 639.00 187.00\" width=\"639pt\" 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 183)\">\n",
"<?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.43.0 (0)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"639pt\" height=\"184pt\"\n",
" viewBox=\"0.00 0.00 639.00 184.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.0 1.0) rotate(0) translate(4 180)\">\n",
"<title>G</title>\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-183 635,-183 635,4 -4,4\" stroke=\"transparent\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-180 635,-180 635,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node2\">\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse cx=\"118\" cy=\"-153\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"118\" y=\"-149.3\">init</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-153\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"118\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M54.303,-153C63.4811,-153 73.8419,-153 83.4994,-153\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"90.7163,-153 83.7163,-156.1501 87.2163,-153 83.7163,-153.0001 83.7163,-153.0001 83.7163,-153.0001 87.2163,-153 83.7162,-149.8501 90.7163,-153 90.7163,-153\" stroke=\"#000000\"/>\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-153C63.46,-153 73.96,-153 83.7,-153\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-153 83.97,-156.15 87.47,-153 83.97,-153 83.97,-153 83.97,-153 87.47,-153 83.97,-149.85 90.97,-153 90.97,-153\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\">\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"#ffffaa\" points=\"517,-105 463,-105 463,-69 517,-69 517,-105\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"490\" y=\"-83.3\">2</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"517,-105 463,-105 463,-69 517,-69 517,-105\"/>\n",
"<text text-anchor=\"middle\" x=\"490\" y=\"-83.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>1-&gt;2</title>\n",
"<path d=\"M144.0789,-158.3499C150.2564,-159.4188 156.8401,-160.397 163,-161 266.4419,-171.1264 295.7434,-168.4113 396,-141 418.5307,-134.8398 424.6775,-133.5141 445,-122 451.3293,-118.414 457.7336,-114.0021 463.6482,-109.534\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"469.3785,-105.0758 465.7879,-111.8604 466.6161,-107.225 463.8536,-109.3742 463.8536,-109.3742 463.8536,-109.3742 466.6161,-107.225 461.9193,-106.888 469.3785,-105.0758 469.3785,-105.0758\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-167.8\">!a &amp; b</text>\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M144.03,-158.27C150.2,-159.37 156.82,-160.38 163,-161 186,-163.3 191.89,-161.78 215,-162 295.98,-162.78 317.88,-162.36 396,-141 418.53,-134.84 424.74,-133.62 445,-122 451.22,-118.43 457.5,-114.02 463.29,-109.56\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"468.89,-105.1 465.37,-111.92 466.15,-107.28 463.41,-109.46 463.41,-109.46 463.41,-109.46 466.15,-107.28 461.45,-106.99 468.89,-105.1 468.89,-105.1\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\">\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3</title>\n",
"<polygon fill=\"#ffffaa\" points=\"269,-103 215,-103 215,-67 269,-67 269,-103\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"242\" y=\"-81.3\">3</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"269,-103 215,-103 215,-67 269,-67 269,-103\"/>\n",
"<text text-anchor=\"middle\" x=\"242\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>1-&gt;3</title>\n",
"<path d=\"M136.9738,-140.091C144.8931,-134.8831 154.2667,-128.9485 163,-124 177.6561,-115.6955 194.3231,-107.3183 208.5582,-100.4679\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"214.9115,-97.4336 209.9525,-103.2928 211.7532,-98.942 208.5949,-100.4504 208.5949,-100.4504 208.5949,-100.4504 211.7532,-98.942 207.2374,-97.6079 214.9115,-97.4336 214.9115,-97.4336\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-127.8\">a &amp; b</text>\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M137.53,-140.08C145.27,-134.87 154.44,-128.94 163,-124 177.67,-115.54 194.41,-107.02 208.62,-100.12\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"214.95,-97.07 210.01,-102.94 211.8,-98.59 208.64,-100.11 208.64,-100.11 208.64,-100.11 211.8,-98.59 207.27,-97.27 214.95,-97.07 214.95,-97.07\"/>\n",
"<text text-anchor=\"middle\" x=\"180\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\">\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse cx=\"369\" cy=\"-114\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"369\" y=\"-110.3\">1</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"369\" cy=\"-114\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"369\" y=\"-110.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>1-&gt;4</title>\n",
"<path d=\"M144.8849,-150.9514C184.425,-147.6359 260.4518,-140.1064 324,-127 328.3903,-126.0945 332.9765,-124.9762 337.4705,-123.7787\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"344.4154,-121.851 338.513,-126.7586 341.0429,-122.7872 337.6704,-123.7233 337.6704,-123.7233 337.6704,-123.7233 341.0429,-122.7872 336.8279,-120.6881 344.4154,-121.851 344.4154,-121.851\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"242\" y=\"-146.8\">a &amp; !b</text>\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M145.11,-151.04C184.28,-147.81 260.45,-140.33 324,-127 328.4,-126.08 333,-124.93 337.49,-123.7\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"344.43,-121.72 338.56,-126.67 341.06,-122.68 337.7,-123.64 337.7,-123.64 337.7,-123.64 341.06,-122.68 336.83,-120.61 344.43,-121.72 344.43,-121.72\"/>\n",
"<text text-anchor=\"middle\" x=\"242\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node6\">\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>5</title>\n",
"<polygon fill=\"#ffffaa\" points=\"627,-40 573,-40 573,-4 627,-4 627,-40\" stroke=\"#000000\"/>\n",
"<polygon fill=\"none\" points=\"631,-44 569,-44 569,0 631,0 631,-44\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"600\" y=\"-18.3\">4</text>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"627,-40 573,-40 573,-4 627,-4 627,-40\"/>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"631,-44 569,-44 569,0 631,0 631,-44\"/>\n",
"<text text-anchor=\"middle\" x=\"600\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>2-&gt;5</title>\n",
"<path d=\"M517.191,-70.9326C530.8855,-62.8404 547.7015,-52.9037 562.5938,-44.1036\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"568.8438,-40.4105 564.4198,-46.6836 565.8305,-42.1911 562.8173,-43.9716 562.8173,-43.9716 562.8173,-43.9716 565.8305,-42.1911 561.2148,-41.2597 568.8438,-40.4105 568.8438,-40.4105\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"543\" y=\"-64.8\">{a}</text>\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M517.14,-71.27C530.8,-63.05 547.73,-52.86 562.64,-43.88\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"568.89,-40.12 564.52,-46.43 565.89,-41.92 562.9,-43.73 562.9,-43.73 562.9,-43.73 565.89,-41.92 561.27,-41.03 568.89,-40.12 568.89,-40.12\"/>\n",
"<text text-anchor=\"middle\" x=\"543\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>3-&gt;2</title>\n",
"<path d=\"M269.0986,-80.5797C274.9927,-79.6756 281.1997,-78.7671 287,-78 335.099,-71.6388 347.634,-68.1653 396,-72 415.8926,-73.5772 437.9326,-77.0038 455.6685,-80.1842\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"462.9873,-81.526 455.534,-83.3619 459.5447,-80.8948 456.1021,-80.2636 456.1021,-80.2636 456.1021,-80.2636 459.5447,-80.8948 456.6702,-77.1652 462.9873,-81.526 462.9873,-81.526\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"369\" y=\"-75.8\">{a}</text>\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M269.03,-80.64C274.93,-79.71 281.17,-78.78 287,-78 335.09,-71.56 347.64,-68.12 396,-72 415.83,-73.59 437.81,-77.05 455.42,-80.25\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"462.68,-81.6 455.22,-83.42 459.24,-80.96 455.8,-80.32 455.8,-80.32 455.8,-80.32 459.24,-80.96 456.37,-77.23 462.68,-81.6 462.68,-81.6\"/>\n",
"<text text-anchor=\"middle\" x=\"369\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>3-&gt;4</title>\n",
"<path d=\"M269.1286,-81.7143C285.3671,-80.6302 306.2351,-80.807 324,-86 331.5733,-88.2138 339.122,-92.0861 345.8129,-96.2575\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"351.6925,-100.1334 344.1144,-98.9106 348.7703,-98.207 345.8481,-96.2806 345.8481,-96.2806 345.8481,-96.2806 348.7703,-98.207 347.5818,-93.6507 351.6925,-100.1334 351.6925,-100.1334\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-89.8\">{b}</text>\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M269.08,-81.75C285.23,-80.6 306.21,-80.7 324,-86 331.29,-88.17 338.53,-91.93 344.97,-96.01\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"351.12,-100.14 343.55,-98.85 348.22,-98.18 345.31,-96.23 345.31,-96.23 345.31,-96.23 348.22,-98.18 347.07,-93.62 351.12,-100.14 351.12,-100.14\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-89.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>3-&gt;5</title>\n",
"<path d=\"M269.3911,-75.0493C275.1553,-73.1874 281.2364,-71.3919 287,-70 384.3702,-46.4854 501.695,-32.1277 561.2432,-25.8042\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"568.5606,-25.0368 561.9274,-28.8998 565.0797,-25.4019 561.5988,-25.767 561.5988,-25.767 561.5988,-25.767 565.0797,-25.4019 561.2702,-22.6342 568.5606,-25.0368 568.5606,-25.0368\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"429.5\" y=\"-49.8\">{a}</text>\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>3&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M269.26,-74.49C275.04,-72.45 281.17,-70.48 287,-69 384.49,-44.2 502.67,-30.79 561.68,-25.2\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"568.92,-24.52 562.25,-28.31 565.44,-24.85 561.95,-25.17 561.95,-25.17 561.95,-25.17 565.44,-24.85 561.66,-22.04 568.92,-24.52 568.92,-24.52\"/>\n",
"<text text-anchor=\"middle\" x=\"429.5\" y=\"-47.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge10\">\n",
"<title>4-&gt;2</title>\n",
"<path d=\"M394.661,-108.274C412.4549,-104.3035 436.3481,-98.9719 455.7635,-94.6395\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"462.6944,-93.093 456.5484,-97.692 459.2784,-93.8553 455.8624,-94.6176 455.8624,-94.6176 455.8624,-94.6176 459.2784,-93.8553 455.1763,-91.5432 462.6944,-93.093 462.6944,-93.093\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"429.5\" y=\"-106.8\">{a, b}</text>\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>4&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M394.95,-108.34C412.67,-104.32 436.65,-98.88 455.97,-94.49\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"462.85,-92.93 456.72,-97.55 459.44,-93.71 456.02,-94.48 456.02,-94.48 456.02,-94.48 459.44,-93.71 455.33,-91.41 462.85,-92.93 462.85,-92.93\"/>\n",
"<text text-anchor=\"middle\" x=\"429.5\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>4-&gt;3</title>\n",
"<path d=\"M342.1573,-111.0138C326.0201,-108.9055 305.1582,-105.6254 287,-101 283.4746,-100.102 279.8358,-99.0418 276.2261,-97.9015\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"269.3576,-95.6312 276.9925,-94.8372 272.6807,-96.7296 276.0039,-97.8281 276.0039,-97.8281 276.0039,-97.8281 272.6807,-96.7296 275.0153,-100.8189 269.3576,-95.6312 269.3576,-95.6312\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"305.5\" y=\"-111.8\">{b}</text>\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M342.21,-111.13C326.16,-109.03 305.2,-105.72 287,-101 283.45,-100.08 279.79,-98.99 276.16,-97.81\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"269.27,-95.47 276.91,-94.74 272.58,-96.6 275.9,-97.72 275.9,-97.72 275.9,-97.72 272.58,-96.6 274.88,-100.7 269.27,-95.47 269.27,-95.47\"/>\n",
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge11\">\n",
"<title>5-&gt;5</title>\n",
"<path d=\"M589.6256,-44.2124C588.7762,-53.7952 592.2344,-62 600,-62 605.7029,-62 609.0827,-57.5751 610.1395,-51.4291\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"610.3744,-44.2124 613.2949,-51.3112 610.2605,-47.7105 610.1465,-51.2086 610.1465,-51.2086 610.1465,-51.2086 610.2605,-47.7105 606.9982,-51.1061 610.3744,-44.2124 610.3744,-44.2124\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"600\" y=\"-65.8\">{a}</text>\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>5&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M589.63,-44.21C588.78,-53.8 592.23,-62 600,-62 605.7,-62 609.08,-57.58 610.14,-51.43\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"610.37,-44.21 613.29,-51.31 610.26,-47.71 610.15,-51.21 610.15,-51.21 610.15,-51.21 610.26,-47.71 607,-51.11 610.37,-44.21 610.37,-44.21\"/>\n",
"<text text-anchor=\"middle\" x=\"600\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 5,
@ -720,7 +741,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.7.5"
}
},
"nbformat": 4,

File diff suppressed because it is too large Load diff

View file

@ -28,145 +28,145 @@
"<?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.40.1 (20161225.0304)\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"465pt\" height=\"232pt\"\n",
" viewBox=\"0.00 0.00 464.50 232.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 228)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-228 460.5,-228 460.5,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"207.25\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 228)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-228 460.5,-228 460.5,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"207.25\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"229.25\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"245.25\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"205.25\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
"<text text-anchor=\"start\" x=\"245.25\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
"<text text-anchor=\"start\" x=\"205.25\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-48C4.178,-48 17.9448,-48 30.9241,-48\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-48 30.9808,-51.1501 34.4807,-48 30.9807,-48.0001 30.9807,-48.0001 30.9807,-48.0001 34.4807,-48 30.9807,-44.8501 37.9807,-48 37.9807,-48\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-48C2.79,-48 17.15,-48 30.63,-48\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-48 30.94,-51.15 34.44,-48 30.94,-48 30.94,-48 30.94,-48 34.44,-48 30.94,-44.85 37.94,-48 37.94,-48\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"139\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"139\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"139\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M74.0098,-48C85.5679,-48 100.7507,-48 113.5345,-48\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"120.7388,-48 113.7388,-51.1501 117.2388,-48 113.7388,-48.0001 113.7388,-48.0001 113.7388,-48.0001 117.2388,-48 113.7387,-44.8501 120.7388,-48 120.7388,-48\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.18,-48C85.67,-48 100.96,-48 113.69,-48\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"120.85,-48 113.85,-51.15 117.35,-48 113.85,-48 113.85,-48 113.85,-48 117.35,-48 113.85,-44.85 120.85,-48 120.85,-48\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"218\" cy=\"-109\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"218\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-109\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"218\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M153.4898,-59.1883C165.9622,-68.8189 184.0861,-82.8133 197.9501,-93.5184\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"203.602,-97.8826 196.1363,-96.0977 200.8318,-95.7435 198.0615,-93.6044 198.0615,-93.6044 198.0615,-93.6044 200.8318,-95.7435 199.9867,-91.1112 203.602,-97.8826 203.602,-97.8826\"/>\n",
"<text text-anchor=\"start\" x=\"175\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M153.77,-58.91C166.03,-68.62 184.1,-82.94 197.79,-93.78\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"203.35,-98.19 195.91,-96.31 200.61,-96.02 197.87,-93.84 197.87,-93.84 197.87,-93.84 200.61,-96.02 199.82,-91.37 203.35,-98.19 203.35,-98.19\"/>\n",
"<text text-anchor=\"start\" x=\"175\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"327\" cy=\"-81\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"327\" y=\"-77.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"327\" cy=\"-81\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"327\" y=\"-77.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M156.8419,-50.6052C185.2996,-54.8346 242.6854,-63.666 291,-73 294.6774,-73.7105 298.5541,-74.514 302.3468,-75.3309\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"309.4626,-76.8975 301.949,-78.4687 306.0445,-76.1449 302.6263,-75.3924 302.6263,-75.3924 302.6263,-75.3924 306.0445,-76.1449 303.3037,-72.316 309.4626,-76.8975 309.4626,-76.8975\"/>\n",
"<text text-anchor=\"start\" x=\"212.5\" y=\"-66.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M157.27,-50.51C185.39,-54.68 242.77,-63.5 291,-73 294.65,-73.72 298.51,-74.54 302.27,-75.37\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"309.31,-76.97 301.79,-78.49 305.9,-76.19 302.48,-75.42 302.48,-75.42 302.48,-75.42 305.9,-76.19 303.18,-72.35 309.31,-76.97 309.31,-76.97\"/>\n",
"<text text-anchor=\"start\" x=\"212.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"436\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"436\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"436\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"436\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M157.1316,-46.1685C207.9791,-41.0324 352.035,-26.4813 410.6856,-20.557\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"417.7283,-19.8456 411.0804,-23.6833 414.246,-20.1974 410.7638,-20.5492 410.7638,-20.5492 410.7638,-20.5492 414.246,-20.1974 410.4472,-17.4152 417.7283,-19.8456 417.7283,-19.8456\"/>\n",
"<text text-anchor=\"start\" x=\"267\" y=\"-39.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M157.14,-46.26C207.03,-41.18 352.37,-26.4 410.53,-20.49\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"417.82,-19.75 411.17,-23.59 414.34,-20.1 410.85,-20.46 410.85,-20.46 410.85,-20.46 414.34,-20.1 410.53,-17.32 417.82,-19.75 417.82,-19.75\"/>\n",
"<text text-anchor=\"start\" x=\"267\" y=\"-39.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M211.2664,-126.0373C209.8922,-135.8579 212.1367,-145 218,-145 222.3975,-145 224.7594,-139.8576 225.0858,-133.1433\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"224.7336,-126.0373 228.2263,-132.8728 224.9069,-129.533 225.0802,-133.0287 225.0802,-133.0287 225.0802,-133.0287 224.9069,-129.533 221.934,-133.1847 224.7336,-126.0373 224.7336,-126.0373\"/>\n",
"<text text-anchor=\"start\" x=\"201\" y=\"-163.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M211.27,-126.04C209.89,-135.86 212.14,-145 218,-145 222.4,-145 224.76,-139.86 225.09,-133.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"224.73,-126.04 228.23,-132.87 224.91,-129.53 225.08,-133.03 225.08,-133.03 225.08,-133.03 224.91,-129.53 221.93,-133.18 224.73,-126.04 224.73,-126.04\"/>\n",
"<text text-anchor=\"start\" x=\"201\" y=\"-163.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"210\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M230.8279,-96.2312C237.2266,-90.7425 245.4224,-84.9246 254,-82 269.3238,-76.7752 287.53,-76.5154 301.927,-77.5667\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"309.0731,-78.2166 301.8165,-80.7195 305.5875,-77.8995 302.1019,-77.5825 302.1019,-77.5825 302.1019,-77.5825 305.5875,-77.8995 302.3872,-74.4454 309.0731,-78.2166 309.0731,-78.2166\"/>\n",
"<text text-anchor=\"start\" x=\"254\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M231.09,-96.52C237.34,-90.95 245.45,-84.98 254,-82 269.38,-76.64 287.75,-76.47 302.09,-77.61\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"309.18,-78.3 301.91,-80.75 305.7,-77.96 302.22,-77.62 302.22,-77.62 302.22,-77.62 305.7,-77.96 302.52,-74.48 309.18,-78.3 309.18,-78.3\"/>\n",
"<text text-anchor=\"start\" x=\"254\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>5</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"327\" cy=\"-170\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"327\" y=\"-166.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"327\" cy=\"-170\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"327\" y=\"-166.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M231.3838,-121.1984C237.9043,-126.7614 246.042,-133.1687 254,-138 269.5528,-147.4421 288.3865,-155.6265 303.0282,-161.3544\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"309.8464,-163.9637 302.1829,-164.4037 306.5776,-162.7127 303.3088,-161.4618 303.3088,-161.4618 303.3088,-161.4618 306.5776,-162.7127 304.4347,-158.5198 309.8464,-163.9637 309.8464,-163.9637\"/>\n",
"<text text-anchor=\"start\" x=\"254\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M231.56,-121.4C237.92,-127.24 245.99,-134 254,-139 269.38,-148.59 288.25,-156.6 302.81,-162.07\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"309.58,-164.54 301.92,-165.1 306.29,-163.34 303.01,-162.14 303.01,-162.14 303.01,-162.14 306.29,-163.34 304.09,-159.18 309.58,-164.54 309.58,-164.54\"/>\n",
"<text text-anchor=\"start\" x=\"254\" y=\"-160.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M310.8472,-89.2341C304.7566,-92.0552 297.6838,-95.0013 291,-97 275.3867,-101.669 257.3176,-104.6576 243.0626,-106.4846\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"235.989,-107.3368 242.5619,-103.372 239.4638,-106.9181 242.9387,-106.4994 242.9387,-106.4994 242.9387,-106.4994 239.4638,-106.9181 243.3156,-109.6268 235.989,-107.3368 235.989,-107.3368\"/>\n",
"<text text-anchor=\"start\" x=\"255.5\" y=\"-122.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"264.5\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M310.66,-89.07C304.67,-91.94 297.64,-94.97 291,-97 275.42,-101.77 257.32,-104.77 243.17,-106.58\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"236.17,-107.43 242.74,-103.46 239.64,-107.01 243.12,-106.59 243.12,-106.59 243.12,-106.59 239.64,-107.01 243.49,-109.72 236.17,-107.43 236.17,-107.43\"/>\n",
"<text text-anchor=\"start\" x=\"255.5\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"264.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M317.7674,-96.5414C315.1685,-106.9087 318.2461,-117 327,-117 333.7022,-117 337.077,-111.0847 337.1245,-103.6591\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"336.2326,-96.5414 340.2286,-103.0955 336.6678,-100.0143 337.103,-103.4871 337.103,-103.4871 337.103,-103.4871 336.6678,-100.0143 333.9775,-103.8788 336.2326,-96.5414 336.2326,-96.5414\"/>\n",
"<text text-anchor=\"start\" x=\"308.5\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M317.77,-96.54C315.17,-106.91 318.25,-117 327,-117 333.7,-117 337.08,-111.08 337.12,-103.66\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"336.23,-96.54 340.23,-103.1 336.67,-100.01 337.1,-103.49 337.1,-103.49 337.1,-103.49 336.67,-100.01 333.98,-103.88 336.23,-96.54 336.23,-96.54\"/>\n",
"<text text-anchor=\"start\" x=\"308.5\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M426.7674,-33.5414C424.1685,-43.9087 427.2461,-54 436,-54 442.7022,-54 446.077,-48.0847 446.1245,-40.6591\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"445.2326,-33.5414 449.2286,-40.0955 445.6678,-37.0143 446.103,-40.4871 446.103,-40.4871 446.103,-40.4871 445.6678,-37.0143 442.9775,-40.8788 445.2326,-33.5414 445.2326,-33.5414\"/>\n",
"<text text-anchor=\"start\" x=\"415.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M426.77,-33.54C424.17,-43.91 427.25,-54 436,-54 442.7,-54 446.08,-48.08 446.12,-40.66\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"445.23,-33.54 449.23,-40.1 445.67,-37.01 446.1,-40.49 446.1,-40.49 446.1,-40.49 445.67,-37.01 442.98,-40.88 445.23,-33.54 445.23,-33.54\"/>\n",
"<text text-anchor=\"start\" x=\"415.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"428\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;4 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>5&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M337.6498,-155.1488C357.2359,-127.8361 399.0029,-69.5923 421.2835,-38.5222\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"425.4674,-32.6877 423.9479,-40.2119 423.4277,-35.5319 421.3881,-38.3762 421.3881,-38.3762 421.3881,-38.3762 423.4277,-35.5319 418.8282,-36.5405 425.4674,-32.6877 425.4674,-32.6877\"/>\n",
"<text text-anchor=\"start\" x=\"363\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M338.07,-155.7C357.19,-128.54 398.8,-69.43 420.76,-38.22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"424.88,-32.37 423.43,-39.91 422.87,-35.23 420.85,-38.1 420.85,-38.1 420.85,-38.1 422.87,-35.23 418.28,-36.28 424.88,-32.37 424.88,-32.37\"/>\n",
"<text text-anchor=\"start\" x=\"363\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e4c5e8de0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f956c0198d0> >"
]
},
"execution_count": 2,
@ -262,7 +262,7 @@
"$\\lnot a; a; \\mathsf{cycle}\\{a \\land b\\}$"
],
"text/plain": [
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c5e8b70> >"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f956c019de0> >"
]
},
"execution_count": 5,
@ -291,15 +291,18 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"112\" version=\"1.1\" width=\"200\" xmlns=\"http://www.w3.org/2000/svg\">\n",
"<rect fill=\"#f4f4f4\" height=\"100\" width=\"200\" x=\"0\" y=\"0\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"100\" x2=\"100\" y1=\"0\" y2=\"100\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"150\" x2=\"150\" y1=\"0\" y2=\"100\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"0\" x2=\"200\" y1=\"0\" y2=\"0\"/><text font-size=\"20\" text-anchor=\"start\" x=\"3\" y=\"30\">a</text><line stroke=\"white\" stroke-width=\"1\" x1=\"50\" x2=\"50\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"0\" x2=\"50\" y1=\"45\" y2=\"45\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"100\" x2=\"100\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"50\" x2=\"50\" y1=\"5\" y2=\"45\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"50\" x2=\"100\" y1=\"5\" y2=\"5\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"150\" x2=\"150\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"150\" y1=\"5\" y2=\"5\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"200\" x2=\"200\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"150\" x2=\"200\" y1=\"5\" y2=\"5\"/><line stroke=\"white\" stroke-width=\"4\" x1=\"0\" x2=\"200\" y1=\"50\" y2=\"50\"/><text font-size=\"20\" text-anchor=\"start\" x=\"3\" y=\"80\">b</text><line stroke=\"white\" stroke-width=\"1\" x1=\"50\" x2=\"50\" y1=\"50\" y2=\"100\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"100\" x2=\"100\" y1=\"50\" y2=\"100\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"150\" x2=\"150\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"150\" y1=\"55\" y2=\"55\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"200\" x2=\"200\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"150\" x2=\"200\" y1=\"55\" y2=\"55\"/><text font-size=\"10\" text-anchor=\"start\" x=\"0\" y=\"110\">prefix</text><text font-size=\"10\" text-anchor=\"start\" x=\"100\" y=\"110\">cycle</text>\n",
"<text font-size=\"10\" text-anchor=\"start\" x=\"150\" y=\"110\">cycle</text></svg>"
"\n",
"<svg height=\"112\" width=\"200\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n",
"<rect x=\"0\" y=\"0\" width=\"200\" height=\"100\" fill=\"#f4f4f4\"/>\n",
"<line x1=\"100\" y1=\"0\" x2=\"100\" y2=\"100\"\n",
" stroke=\"white\" stroke-width=\"4\"/>\n",
"<line x1=\"150\" y1=\"0\" x2=\"150\" y2=\"100\"\n",
" stroke=\"white\" stroke-width=\"4\"/>\n",
"<line x1=\"0\" y1=\"0\" x2=\"200\" y2=\"0\" stroke=\"white\" stroke-width=\"4\"/><text x=\"3\" y=\"30\" text-anchor=\"start\" font-size=\"20\">a</text><line x1=\"50\" y1=\"0\" x2=\"50\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"0\" y1=\"45\" x2=\"50\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"100\" y1=\"0\" x2=\"100\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"50\" y1=\"5\" x2=\"50\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"50\" y1=\"5\" x2=\"100\" y2=\"5\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"150\" y1=\"0\" x2=\"150\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"5\" x2=\"150\" y2=\"5\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"200\" y1=\"0\" x2=\"200\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"150\" y1=\"5\" x2=\"200\" y2=\"5\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"0\" y1=\"50\" x2=\"200\" y2=\"50\" stroke=\"white\" stroke-width=\"4\"/><text x=\"3\" y=\"80\" text-anchor=\"start\" font-size=\"20\">b</text><line x1=\"50\" y1=\"50\" x2=\"50\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"50\" x2=\"100\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"150\" y1=\"50\" x2=\"150\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"55\" x2=\"150\" y2=\"55\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"200\" y1=\"50\" x2=\"200\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"150\" y1=\"55\" x2=\"200\" y2=\"55\" stroke=\"#ff0000\" stroke-width=\"2\"/><text x=\"0\" y=\"110\" text-anchor=\"start\" font-size=\"10\">prefix</text><text x=\"100\" y=\"110\" text-anchor=\"start\" font-size=\"10\">cycle</text>\n",
"<text x=\"150\" y=\"110\" text-anchor=\"start\" font-size=\"10\">cycle</text></svg>"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 6,
@ -382,7 +385,7 @@
"$\\lnot a; \\mathsf{cycle}\\{a \\land b\\}$"
],
"text/plain": [
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c652810> >"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f956c0388a0> >"
]
},
"execution_count": 9,
@ -433,7 +436,7 @@
"$a; a \\land b; \\mathsf{cycle}\\{\\lnot a \\land \\lnot b; \\lnot a \\land b\\}$"
],
"text/plain": [
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c574600> >"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f956c038b70> >"
]
},
"execution_count": 11,
@ -454,15 +457,18 @@
{
"data": {
"image/svg+xml": [
"<svg height=\"112\" version=\"1.1\" width=\"300\" xmlns=\"http://www.w3.org/2000/svg\">\n",
"<rect fill=\"#f4f4f4\" height=\"100\" width=\"300\" x=\"0\" y=\"0\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"100\" x2=\"100\" y1=\"0\" y2=\"100\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"200\" x2=\"200\" y1=\"0\" y2=\"100\"/>\n",
"<line stroke=\"white\" stroke-width=\"4\" x1=\"0\" x2=\"300\" y1=\"0\" y2=\"0\"/><text font-size=\"20\" text-anchor=\"start\" x=\"3\" y=\"30\">a</text><line stroke=\"white\" stroke-width=\"1\" x1=\"50\" x2=\"50\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"0\" x2=\"50\" y1=\"5\" y2=\"5\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"100\" x2=\"100\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"50\" x2=\"100\" y1=\"5\" y2=\"5\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"150\" x2=\"150\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"100\" y1=\"5\" y2=\"45\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"150\" y1=\"45\" y2=\"45\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"200\" x2=\"200\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"150\" x2=\"200\" y1=\"45\" y2=\"45\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"250\" x2=\"250\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"200\" x2=\"250\" y1=\"45\" y2=\"45\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"300\" x2=\"300\" y1=\"0\" y2=\"50\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"250\" x2=\"300\" y1=\"45\" y2=\"45\"/><line stroke=\"white\" stroke-width=\"4\" x1=\"0\" x2=\"300\" y1=\"50\" y2=\"50\"/><text font-size=\"20\" text-anchor=\"start\" x=\"3\" y=\"80\">b</text><line stroke=\"white\" stroke-width=\"1\" x1=\"50\" x2=\"50\" y1=\"50\" y2=\"100\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"100\" x2=\"100\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"50\" x2=\"100\" y1=\"55\" y2=\"55\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"150\" x2=\"150\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"100\" y1=\"55\" y2=\"95\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"100\" x2=\"150\" y1=\"95\" y2=\"95\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"200\" x2=\"200\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"150\" x2=\"150\" y1=\"55\" y2=\"95\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"150\" x2=\"200\" y1=\"55\" y2=\"55\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"250\" x2=\"250\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"200\" x2=\"200\" y1=\"55\" y2=\"95\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"200\" x2=\"250\" y1=\"95\" y2=\"95\"/><line stroke=\"white\" stroke-width=\"1\" x1=\"300\" x2=\"300\" y1=\"50\" y2=\"100\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"250\" x2=\"250\" y1=\"55\" y2=\"95\"/><line stroke=\"#ff0000\" stroke-width=\"2\" x1=\"250\" x2=\"300\" y1=\"55\" y2=\"55\"/><text font-size=\"10\" text-anchor=\"start\" x=\"0\" y=\"110\">prefix</text><text font-size=\"10\" text-anchor=\"start\" x=\"100\" y=\"110\">cycle</text>\n",
"<text font-size=\"10\" text-anchor=\"start\" x=\"200\" y=\"110\">cycle</text></svg>"
"\n",
"<svg height=\"112\" width=\"300\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n",
"<rect x=\"0\" y=\"0\" width=\"300\" height=\"100\" fill=\"#f4f4f4\"/>\n",
"<line x1=\"100\" y1=\"0\" x2=\"100\" y2=\"100\"\n",
" stroke=\"white\" stroke-width=\"4\"/>\n",
"<line x1=\"200\" y1=\"0\" x2=\"200\" y2=\"100\"\n",
" stroke=\"white\" stroke-width=\"4\"/>\n",
"<line x1=\"0\" y1=\"0\" x2=\"300\" y2=\"0\" stroke=\"white\" stroke-width=\"4\"/><text x=\"3\" y=\"30\" text-anchor=\"start\" font-size=\"20\">a</text><line x1=\"50\" y1=\"0\" x2=\"50\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"0\" y1=\"5\" x2=\"50\" y2=\"5\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"100\" y1=\"0\" x2=\"100\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"50\" y1=\"5\" x2=\"100\" y2=\"5\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"150\" y1=\"0\" x2=\"150\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"5\" x2=\"100\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"100\" y1=\"45\" x2=\"150\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"200\" y1=\"0\" x2=\"200\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"150\" y1=\"45\" x2=\"200\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"250\" y1=\"0\" x2=\"250\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"200\" y1=\"45\" x2=\"250\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"300\" y1=\"0\" x2=\"300\" y2=\"50\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"250\" y1=\"45\" x2=\"300\" y2=\"45\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"0\" y1=\"50\" x2=\"300\" y2=\"50\" stroke=\"white\" stroke-width=\"4\"/><text x=\"3\" y=\"80\" text-anchor=\"start\" font-size=\"20\">b</text><line x1=\"50\" y1=\"50\" x2=\"50\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"50\" x2=\"100\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"50\" y1=\"55\" x2=\"100\" y2=\"55\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"150\" y1=\"50\" x2=\"150\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"100\" y1=\"55\" x2=\"100\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"100\" y1=\"95\" x2=\"150\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"200\" y1=\"50\" x2=\"200\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"150\" y1=\"55\" x2=\"150\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"150\" y1=\"55\" x2=\"200\" y2=\"55\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"250\" y1=\"50\" x2=\"250\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"200\" y1=\"55\" x2=\"200\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"200\" y1=\"95\" x2=\"250\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"300\" y1=\"50\" x2=\"300\" y2=\"100\" stroke=\"white\" stroke-width=\"1\"/><line x1=\"250\" y1=\"55\" x2=\"250\" y2=\"95\" stroke=\"#ff0000\" stroke-width=\"2\"/><line x1=\"250\" y1=\"55\" x2=\"300\" y2=\"55\" stroke=\"#ff0000\" stroke-width=\"2\"/><text x=\"0\" y=\"110\" text-anchor=\"start\" font-size=\"10\">prefix</text><text x=\"100\" y=\"110\" text-anchor=\"start\" font-size=\"10\">cycle</text>\n",
"<text x=\"200\" y=\"110\" text-anchor=\"start\" font-size=\"10\">cycle</text></svg>"
],
"text/plain": [
"<IPython.core.display.SVG object>"
"<spot.jupyter.SVG object>"
]
},
"execution_count": 12,
@ -492,79 +498,79 @@
"<?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.40.1 (20161225.0304)\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"380pt\" height=\"86pt\"\n",
" viewBox=\"0.00 0.00 380.00 86.29\" 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 82.2859)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-82.2859 376,-82.2859 376,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"183\" y=\"-63.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">t</text>\n",
"<text text-anchor=\"start\" x=\"175\" y=\"-48.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[all]</text>\n",
" viewBox=\"0.00 0.00 380.00 86.36\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 82.36)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-82.36 376,-82.36 376,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"183\" y=\"-63.16\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
"<text text-anchor=\"start\" x=\"175\" y=\"-48.16\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22.2859\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.5859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22.36\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.66\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22.2859C4.178,-22.2859 17.9448,-22.2859 30.9241,-22.2859\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22.2859 30.9808,-25.436 34.4807,-22.286 30.9807,-22.286 30.9807,-22.286 30.9807,-22.286 34.4807,-22.286 30.9807,-19.136 37.9807,-22.2859 37.9807,-22.2859\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-22.36C2.79,-22.36 17.15,-22.36 30.63,-22.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22.36 30.94,-25.51 34.44,-22.36 30.94,-22.36 30.94,-22.36 30.94,-22.36 34.44,-22.36 30.94,-19.21 37.94,-22.36 37.94,-22.36\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"135\" cy=\"-22.2859\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"135\" y=\"-18.5859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-22.36\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"135\" y=\"-18.66\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M74.3228,-22.2859C84.7921,-22.2859 98.0794,-22.2859 109.5495,-22.2859\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"116.7766,-22.2859 109.7767,-25.436 113.2766,-22.286 109.7766,-22.286 109.7766,-22.286 109.7766,-22.286 113.2766,-22.286 109.7766,-19.136 116.7766,-22.2859 116.7766,-22.2859\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-26.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.09,-22.36C84.56,-22.36 98.12,-22.36 109.69,-22.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"116.96,-22.36 109.96,-25.51 113.46,-22.36 109.96,-22.36 109.96,-22.36 109.96,-22.36 113.46,-22.36 109.96,-19.21 116.96,-22.36 116.96,-22.36\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-26.16\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"241\" cy=\"-22.2859\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"241\" y=\"-18.5859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"241\" cy=\"-22.36\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"241\" y=\"-18.66\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M153.4638,-22.2859C170.6394,-22.2859 196.386,-22.2859 215.5153,-22.2859\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"222.7478,-22.2859 215.7478,-25.436 219.2478,-22.286 215.7478,-22.286 215.7478,-22.286 215.7478,-22.286 219.2478,-22.286 215.7478,-19.136 222.7478,-22.2859 222.7478,-22.2859\"/>\n",
"<text text-anchor=\"start\" x=\"171\" y=\"-26.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M153.17,-22.36C170.18,-22.36 196.4,-22.36 215.57,-22.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"222.8,-22.36 215.8,-25.51 219.3,-22.36 215.8,-22.36 215.8,-22.36 215.8,-22.36 219.3,-22.36 215.8,-19.21 222.8,-22.36 222.8,-22.36\"/>\n",
"<text text-anchor=\"start\" x=\"171\" y=\"-26.16\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"354\" cy=\"-22.2859\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"354\" y=\"-18.5859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"354\" cy=\"-22.36\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"354\" y=\"-18.66\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M259.1554,-22.2859C278.0184,-22.2859 307.6779,-22.2859 328.8045,-22.2859\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"335.8897,-22.2859 328.8897,-25.436 332.3897,-22.286 328.8897,-22.286 328.8897,-22.286 328.8897,-22.286 332.3897,-22.286 328.8896,-19.136 335.8897,-22.2859 335.8897,-22.2859\"/>\n",
"<text text-anchor=\"start\" x=\"277\" y=\"-26.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M259.34,-22.36C278,-22.36 307.8,-22.36 328.76,-22.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"335.78,-22.36 328.78,-25.51 332.28,-22.36 328.78,-22.36 328.78,-22.36 328.78,-22.36 332.28,-22.36 328.78,-19.21 335.78,-22.36 335.78,-22.36\"/>\n",
"<text text-anchor=\"start\" x=\"277\" y=\"-26.16\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M338.8943,-12.2159C332.6932,-8.6541 325.2713,-5.087 318,-3.2859 300.3123,1.0953 294.6877,1.0953 277,-3.2859 272.1146,-4.496 267.1612,-6.5033 262.5558,-8.7706\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"256.1057,-12.2159 260.7959,-6.1393 259.1929,-10.5668 262.2801,-8.9178 262.2801,-8.9178 262.2801,-8.9178 259.1929,-10.5668 263.7642,-11.6963 256.1057,-12.2159 256.1057,-12.2159\"/>\n",
"<text text-anchor=\"start\" x=\"279\" y=\"-7.0859\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M338.69,-12.5C332.6,-8.87 325.24,-5.2 318,-3.36 300.34,1.12 294.66,1.12 277,-3.36 272.14,-4.6 267.22,-6.66 262.67,-8.98\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"256.31,-12.5 260.91,-6.35 259.37,-10.8 262.44,-9.11 262.44,-9.11 262.44,-9.11 259.37,-10.8 263.96,-11.86 256.31,-12.5 256.31,-12.5\"/>\n",
"<text text-anchor=\"start\" x=\"279\" y=\"-7.16\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e4c6528a0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f956c0388d0> >"
]
},
"execution_count": 13,
@ -593,7 +599,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.7"
"version": "3.7.5"
}
},
"nbformat": 4,