automata.ipynb 272 KB
Newer Older
1
2
{
 "metadata": {
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
18
   "version": "3.5.3+"
19
  },
20
  "name": ""
21
22
23
24
25
26
27
28
29
30
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
31
      "from IPython.display import display\n",
Etienne Renault's avatar
Etienne Renault committed
32
      "import spot\n",
33
      "spot.setup()"
34
35
36
37
38
39
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
40
41
42
43
44
45
46
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To build an automaton, simply call `translate()` with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the `ltl2tgba` tool, and they can be abbreviated)."
     ]
    },
47
48
49
50
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
51
      "a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a"
52
53
54
55
56
57
58
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
59
       "prompt_number": 2,
60
61
62
63
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
64
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
65
66
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
67
68
69
        "<svg width=\"419pt\" height=\"184pt\"\n",
        " viewBox=\"0.00 0.00 419.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 1) rotate(0) translate(4 180)\">\n",
70
        "<title>G</title>\n",
71
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 415,-180 415,4 -4,4\"/>\n",
72
73
74
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
75
76
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-69\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-65.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
77
78
79
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
80
81
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-69C2.79388,-69 17.1543,-69 30.6317,-69\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-69 30.9419,-72.1501 34.4419,-69 30.9419,-69.0001 30.9419,-69.0001 30.9419,-69.0001 34.4419,-69 30.9418,-65.8501 37.9419,-69 37.9419,-69\"/>\n",
82
83
84
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
85
86
87
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-86.0373C48.3189,-95.8579 50.4453,-105 56,-105 60.166,-105 62.4036,-99.8576 62.7128,-93.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-86.0373 65.8541,-92.8818 62.5434,-89.5335 62.7076,-93.0296 62.7076,-93.0296 62.7076,-93.0296 62.5434,-89.5335 59.561,-93.1774 62.3792,-86.0373 62.3792,-86.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
88
89
90
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
91
92
93
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
94
95
96
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
97
98
99
        "<path fill=\"none\" stroke=\"black\" d=\"M73.4767,-74.731C92.1945,-81.2416 123.014,-91.9614 145.203,-99.6792\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"152.077,-102.07 144.431,-102.746 148.772,-100.921 145.466,-99.7706 145.466,-99.7706 145.466,-99.7706 148.772,-100.921 146.501,-96.7955 152.077,-102.07 152.077,-102.07\"/>\n",
        "<text text-anchor=\"start\" x=\"108\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
100
101
102
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
103
104
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
105
106
107
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
108
109
110
        "<path fill=\"none\" stroke=\"black\" d=\"M72.9903,-61.9087C92.9015,-53.0784 127.032,-37.9422 149.557,-27.9532\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"156.146,-25.0311 151.024,-30.7485 152.946,-26.45 149.747,-27.869 149.747,-27.869 149.747,-27.869 152.946,-26.45 148.47,-24.9894 156.146,-25.0311 156.146,-25.0311\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
111
112
113
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
114
115
116
        "<path fill=\"none\" stroke=\"black\" d=\"M162.933,-128.757C161.223,-139.35 164.578,-149 173,-149 179.448,-149 182.926,-143.343 183.435,-135.938\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"183.067,-128.757 186.571,-135.587 183.246,-132.253 183.425,-135.748 183.425,-135.748 183.425,-135.748 183.246,-132.253 180.279,-135.91 183.067,-128.757 183.067,-128.757\"/>\n",
        "<text text-anchor=\"start\" x=\"156\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
117
118
119
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
120
121
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"393\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"393\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
122
123
124
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
125
126
127
        "<path fill=\"none\" stroke=\"black\" d=\"M190.278,-122.894C214.315,-141.67 260.899,-171.444 302,-159 329.774,-150.591 356.811,-130.471 373.881,-115.843\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"379.274,-111.117 376.085,-118.1 376.642,-113.424 374.009,-115.73 374.009,-115.73 374.009,-115.73 376.642,-113.424 371.933,-113.361 379.274,-111.117 379.274,-111.117\"/>\n",
        "<text text-anchor=\"start\" x=\"265\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
128
129
130
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
131
132
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"283.5\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"283.5\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
133
134
135
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
136
137
138
        "<path fill=\"none\" stroke=\"black\" d=\"M195.152,-108.988C209.762,-108.77 229.617,-108.059 247,-106 250.725,-105.559 254.645,-104.943 258.464,-104.257\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"265.61,-102.881 259.332,-107.298 262.173,-103.543 258.737,-104.204 258.737,-104.204 258.737,-104.204 262.173,-103.543 258.141,-101.111 265.61,-102.881 265.61,-102.881\"/>\n",
        "<text text-anchor=\"start\" x=\"223.5\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
139
140
141
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
142
143
144
        "<path fill=\"none\" stroke=\"black\" d=\"M163.425,-33.5414C160.73,-43.9087 163.922,-54 173,-54 179.95,-54 183.45,-48.0847 183.499,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"182.575,-33.5414 186.6,-40.0771 183.026,-37.0123 183.477,-40.4831 183.477,-40.4831 183.477,-40.4831 183.026,-37.0123 180.353,-40.889 182.575,-33.5414 182.575,-33.5414\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
145
146
147
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
148
149
150
        "<path fill=\"none\" stroke=\"black\" d=\"M377.812,-89.0507C354.64,-74.0075 307.035,-48.1189 265,-57 239.248,-62.4409 213.545,-78.3348 196.057,-91.1322\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"190.453,-95.3338 194.164,-88.6143 193.253,-93.2342 196.053,-91.1346 196.053,-91.1346 196.053,-91.1346 193.253,-93.2342 197.943,-93.6549 190.453,-95.3338 190.453,-95.3338\"/>\n",
        "<text text-anchor=\"start\" x=\"280\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
151
152
153
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
154
155
156
        "<path fill=\"none\" stroke=\"black\" d=\"M383.767,-114.541C381.169,-124.909 384.246,-135 393,-135 399.702,-135 403.077,-129.085 403.124,-121.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"402.233,-114.541 406.229,-121.095 402.668,-118.014 403.103,-121.487 403.103,-121.487 403.103,-121.487 402.668,-118.014 399.977,-121.879 402.233,-114.541 402.233,-114.541\"/>\n",
        "<text text-anchor=\"start\" x=\"387.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!c</text>\n",
157
158
159
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
160
161
162
        "<path fill=\"none\" stroke=\"black\" d=\"M266.525,-92.366C260.514,-90.2005 253.548,-88.0768 247,-87 232.089,-84.548 227.616,-83.1619 213,-87 207.831,-88.3574 202.625,-90.5725 197.776,-93.0866\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"191.42,-96.6478 195.987,-90.4779 194.474,-94.9369 197.527,-93.2259 197.527,-93.2259 197.527,-93.2259 194.474,-94.9369 199.067,-95.9739 191.42,-96.6478 191.42,-96.6478\"/>\n",
        "<text text-anchor=\"start\" x=\"213\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
163
164
165
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
166
167
168
        "<path fill=\"none\" stroke=\"black\" d=\"M301.772,-99C319.638,-99 347.686,-99 367.767,-99\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"374.771,-99 367.771,-102.15 371.271,-99 367.771,-99.0001 367.771,-99.0001 367.771,-99.0001 371.271,-99 367.771,-95.8501 374.771,-99 374.771,-99\"/>\n",
        "<text text-anchor=\"start\" x=\"320\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
169
170
171
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
172
173
174
        "<path fill=\"none\" stroke=\"black\" d=\"M274.521,-114.916C272.179,-125.15 275.172,-135 283.5,-135 289.876,-135 293.125,-129.226 293.246,-121.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"292.479,-114.916 296.372,-121.532 292.86,-118.395 293.241,-121.874 293.241,-121.874 293.241,-121.874 292.86,-118.395 290.11,-122.217 292.479,-114.916 292.479,-114.916\"/>\n",
        "<text text-anchor=\"start\" x=\"277\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
175
176
177
178
179
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
180
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff810> >"
181
182
183
       ]
      }
     ],
184
     "prompt_number": 2
185
    },
186
187
188
189
190
191
192
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The call the `spot.setup()` in the first cells has installed a default style for the graphviz output.  If you want to change this style temporarily, you can call the `show(style)` method explicitely.  For instance here is a vertical layout with the default font of GraphViz."
     ]
    },
193
194
195
196
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
197
      "a.show(\"v\")"
198
199
200
201
202
203
204
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
205
       "prompt_number": 3,
206
       "svg": [
207
        "<svg height=\"351pt\" viewBox=\"0.00 0.00 226.36 351.00\" width=\"226pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
208
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 347)\">\n",
209
        "<title>G</title>\n",
210
        "<polygon fill=\"white\" points=\"-4,4 -4,-347 222.356,-347 222.356,4 -4,4\" stroke=\"none\"/>\n",
211
212
213
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
214
215
        "<ellipse cx=\"120.356\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.356\" y=\"-283.3\">0</text>\n",
216
217
218
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
219
220
        "<path d=\"M120.356,-341.845C120.356,-340.206 120.356,-325.846 120.356,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.356,-305.058 123.506,-312.058 120.356,-308.558 120.356,-312.058 120.356,-312.058 120.356,-312.058 120.356,-308.558 117.206,-312.058 120.356,-305.058 120.356,-305.058\" stroke=\"black\"/>\n",
221
222
223
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
224
225
226
        "<path d=\"M137.393,-293.379C147.214,-294.681 156.356,-292.555 156.356,-287 156.356,-282.834 151.214,-280.596 144.499,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.393,-280.621 144.238,-277.146 140.89,-280.457 144.386,-280.292 144.386,-280.292 144.386,-280.292 140.89,-280.457 144.533,-283.439 137.393,-280.621 137.393,-280.621\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"174.856\" y=\"-283.3\">a &amp; !b</text>\n",
227
228
229
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
230
231
232
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67.3561\" y=\"-192.3\">1</text>\n",
233
234
235
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
236
237
238
        "<path d=\"M111.365,-270.902C103.283,-257.33 91.2671,-237.152 81.832,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"78.2263,-215.254 84.5144,-219.656 80.0171,-218.261 81.808,-221.268 81.808,-221.268 81.808,-221.268 80.0171,-218.261 79.1015,-222.88 78.2263,-215.254 78.2263,-215.254\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102.856\" y=\"-239.8\">b</text>\n",
239
240
241
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
242
243
        "<ellipse cx=\"175.356\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"175.356\" y=\"-192.3\">4</text>\n",
244
245
246
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
247
248
249
        "<path d=\"M129.438,-271.303C138.435,-256.746 152.298,-234.312 162.439,-217.902\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"166.26,-211.718 165.26,-219.329 164.42,-214.696 162.581,-217.673 162.581,-217.673 162.581,-217.673 164.42,-214.696 159.901,-216.017 166.26,-211.718 166.26,-211.718\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.856\" y=\"-239.8\">!a &amp; !b</text>\n",
250
251
252
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
253
254
255
        "<path d=\"M87.9369,-204.37C98.2008,-205.528 107.356,-202.738 107.356,-196 107.356,-190.946 102.206,-188.113 95.3012,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"87.9369,-187.63 94.8809,-184.358 91.4364,-187.569 94.9358,-187.508 94.9358,-187.508 94.9358,-187.508 91.4364,-187.569 94.9907,-190.657 87.9369,-187.63 87.9369,-187.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"123.356\" y=\"-192.3\">c &amp; d</text>\n",
256
257
258
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
259
260
        "<ellipse cx=\"68.3561\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-14.3\">2</text>\n",
261
262
263
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
264
265
266
        "<path d=\"M50.199,-181.727C34.8703,-168.686 13.4697,-147.255 4.35608,-123 -1.27155,-108.022 -1.54226,-101.873 4.35608,-87 13.1144,-64.9152 32.818,-45.8318 48.0656,-33.5506\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"53.866,-29.0284 50.2823,-35.8166 51.1058,-31.1804 48.3455,-33.3324 48.3455,-33.3324 48.3455,-33.3324 51.1058,-31.1804 46.4087,-30.8481 53.866,-29.0284 53.866,-29.0284\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.8561\" y=\"-101.3\">!c &amp; d</text>\n",
267
268
269
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
270
271
        "<ellipse cx=\"68.3561\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-101.3\">3</text>\n",
272
273
274
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
275
276
277
        "<path d=\"M56.8135,-176.159C52.3073,-165.855 48.6383,-152.816 51.3561,-141 52.4094,-136.42 54.1455,-131.745 56.1156,-127.365\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"59.3394,-120.78 59.0906,-128.452 57.8004,-123.923 56.2615,-127.067 56.2615,-127.067 56.2615,-127.067 57.8004,-123.923 53.4323,-125.682 59.3394,-120.78 59.3394,-120.78\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"57.3561\" y=\"-144.8\">!d</text>\n",
278
279
280
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
281
282
283
        "<path d=\"M191.646,-204.016C201.745,-205.949 211.356,-203.277 211.356,-196 211.356,-190.542 205.95,-187.674 198.986,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"191.646,-187.984 198.373,-184.286 195.135,-187.705 198.624,-187.426 198.624,-187.426 198.624,-187.426 195.135,-187.705 198.875,-190.566 191.646,-187.984 191.646,-187.984\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"214.856\" y=\"-192.3\">1</text>\n",
284
285
286
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
287
288
289
        "<path d=\"M82.9697,-29.0929C91.4609,-35.4971 101.918,-44.3722 109.356,-54 128.603,-78.9113 134.158,-92.7751 125.356,-123 119.215,-144.088 103.068,-163.203 89.3663,-176.43\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"84.0682,-181.376 87.035,-174.297 86.6265,-178.988 89.1847,-176.599 89.1847,-176.599 89.1847,-176.599 86.6265,-178.988 91.3345,-178.901 84.0682,-181.376 84.0682,-181.376\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132.856\" y=\"-101.3\">c</text>\n",
290
291
292
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
293
294
295
        "<path d=\"M85.0201,-25.3828C94.9811,-27.0234 104.356,-24.5625 104.356,-18 104.356,-13.0781 99.0826,-10.4634 92.2436,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-10.6172 91.8051,-7.02727 88.513,-10.394 92.0059,-10.1709 92.0059,-10.1709 92.0059,-10.1709 88.513,-10.394 92.2067,-13.3145 85.0201,-10.6172 85.0201,-10.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109.856\" y=\"-14.3\">!c</text>\n",
296
297
298
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
299
300
301
        "<path d=\"M68.1643,-123.066C68.0258,-135.398 67.8354,-152.339 67.6743,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"67.5931,-173.908 64.522,-166.873 67.6324,-170.408 67.6718,-166.909 67.6718,-166.909 67.6718,-166.909 67.6324,-170.408 70.8216,-166.944 67.5931,-173.908 67.5931,-173.908\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"84.3561\" y=\"-144.8\">c &amp; d</text>\n",
302
303
304
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
305
306
307
        "<path d=\"M68.3561,-86.799C68.3561,-74.3561 68.3561,-57.3644 68.3561,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"68.3561,-36.1754 71.5062,-43.1754 68.3561,-39.6754 68.3562,-43.1754 68.3562,-43.1754 68.3562,-43.1754 68.3561,-39.6754 65.2062,-43.1755 68.3561,-36.1754 68.3561,-36.1754\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"86.8561\" y=\"-57.8\">!c &amp; d</text>\n",
308
309
310
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
311
312
313
        "<path d=\"M85.0201,-112.383C94.9811,-114.023 104.356,-111.562 104.356,-105 104.356,-100.078 99.0826,-97.4634 92.2436,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-97.6172 91.8051,-94.0273 88.513,-97.394 92.0059,-97.1709 92.0059,-97.1709 92.0059,-97.1709 88.513,-97.394 92.2067,-100.314 85.0201,-97.6172 85.0201,-97.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"110.356\" y=\"-101.3\">!d</text>\n",
314
315
316
317
318
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
319
        "<IPython.core.display.SVG object>"
320
321
322
       ]
      }
     ],
323
     "prompt_number": 3
324
    },
325
326
327
328
329
330
331
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "If you want to add some style options to the existing one, pass a dot to the `show()` function in addition to your own style options:"
     ]
    },
332
333
334
335
336
337
338
339
340
341
342
343
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.show(\".ast\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
344
       "prompt_number": 4,
345
       "svg": [
346
347
        "<svg height=\"342pt\" viewBox=\"0.00 0.00 427.00 342.00\" width=\"427pt\" 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 338)\">\n",
348
        "<title>G</title>\n",
349
350
        "<polygon fill=\"white\" points=\"-4,4 -4,-338 423,-338 423,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-319.8\">Inf(</text>\n",
351
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-319.8\">\u24ff</text>\n",
352
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-319.8\">)</text>\n",
353
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
354
        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
355
356
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
357
        "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
358
359
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
360
        "<polygon fill=\"none\" points=\"30,-23 30,-108 82,-108 82,-23 30,-23\" stroke=\"red\"/>\n",
361
362
363
364
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
365
366
        "<ellipse cx=\"56\" cy=\"-49\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-45.3\">0</text>\n",
367
368
369
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
370
371
        "<path d=\"M1.15491,-49C2.79388,-49 17.1543,-49 30.6317,-49\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9419,-49 30.9419,-52.1501 34.4419,-49 30.9419,-49.0001 30.9419,-49.0001 30.9419,-49.0001 34.4419,-49 30.9418,-45.8501 37.9419,-49 37.9419,-49\" stroke=\"black\"/>\n",
372
373
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
374
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
375
376
377
        "<path d=\"M49.6208,-66.0373C48.3189,-75.8579 50.4453,-85 56,-85 60.166,-85 62.4036,-79.8576 62.7128,-73.1433\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"62.3792,-66.0373 65.8541,-72.8818 62.5434,-69.5335 62.7076,-73.0296 62.7076,-73.0296 62.7076,-73.0296 62.5434,-69.5335 59.561,-73.1774 62.3792,-66.0373 62.3792,-66.0373\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-88.8\">a &amp; !b</text>\n",
378
379
380
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
381
382
        "<ellipse cx=\"169\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-189.3\">1</text>\n",
383
384
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
385
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
386
387
388
        "<path d=\"M67.6431,-62.8073C87.4829,-88.5454 130.165,-143.916 152.947,-173.472\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"157.226,-179.023 150.458,-175.402 155.089,-176.251 152.952,-173.479 152.952,-173.479 152.952,-173.479 155.089,-176.251 155.447,-171.556 157.226,-179.023 157.226,-179.023\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-150.8\">b</text>\n",
389
390
391
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
392
393
        "<ellipse cx=\"169\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
394
395
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
396
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
397
398
399
        "<path d=\"M73.8585,-46.7218C92.5211,-44.1998 122.756,-40.114 143.912,-37.2551\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"150.983,-36.2996 144.468,-40.3588 147.514,-36.7684 144.046,-37.2371 144.046,-37.2371 144.046,-37.2371 147.514,-36.7684 143.624,-34.1155 150.983,-36.2996 150.983,-36.2996\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-48.8\">!a &amp; !b</text>\n",
400
401
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
402
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
403
404
405
        "<path d=\"M160.021,-208.916C157.679,-219.15 160.672,-229 169,-229 175.376,-229 178.625,-223.226 178.746,-215.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-208.916 181.872,-215.532 178.36,-212.395 178.741,-215.874 178.741,-215.874 178.741,-215.874 178.36,-212.395 175.61,-216.217 177.979,-208.916 177.979,-208.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-247.8\">c &amp; d</text>\n",
406
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-232.8\">\u24ff</text>\n",
407
408
        "</g>\n",
        "<!-- 2 -->\n",
409
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
410
411
        "<ellipse cx=\"385\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"385\" y=\"-189.3\">2</text>\n",
412
413
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
414
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
415
416
417
        "<path d=\"M183.382,-181.807C199.601,-169.041 228.334,-148.914 257,-141 296.803,-130.011 340.921,-157.735 365.268,-176.79\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"371.017,-181.419 363.59,-179.483 368.291,-179.224 365.565,-177.029 365.565,-177.029 365.565,-177.029 368.291,-179.224 367.54,-174.576 371.017,-181.419 371.017,-181.419\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-159.8\">!c &amp; d</text>\n",
418
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-144.8\">\u24ff</text>\n",
419
        "</g>\n",
420
421
422
423
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
        "<ellipse cx=\"275.5\" cy=\"-244\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"275.5\" y=\"-240.3\">3</text>\n",
424
        "</g>\n",
425
        "<!-- 1&#45;&gt;3 -->\n",
426
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
427
428
429
        "<path d=\"M186.45,-197.514C200.79,-201.783 221.911,-208.888 239,-218 244.62,-220.997 250.345,-224.799 255.51,-228.565\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"261.277,-232.918 253.792,-231.215 258.484,-230.809 255.69,-228.701 255.69,-228.701 255.69,-228.701 258.484,-230.809 257.588,-226.187 261.277,-232.918 261.277,-232.918\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-236.8\">!d</text>\n",
430
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-221.8\">\u24ff</text>\n",
431
432
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
433
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
434
435
436
        "<path d=\"M366.768,-193C328.813,-193 237.915,-193 194.238,-193\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"187.151,-193 194.151,-189.85 190.651,-193 194.151,-193 194.151,-193 194.151,-193 190.651,-193 194.151,-196.15 187.151,-193 187.151,-193\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-196.8\">c</text>\n",
437
438
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
439
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
440
441
442
        "<path d=\"M375.767,-208.541C373.169,-218.909 376.246,-229 385,-229 391.702,-229 395.077,-223.085 395.124,-215.659\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"394.233,-208.541 398.229,-215.095 394.668,-212.014 395.103,-215.487 395.103,-215.487 395.103,-215.487 394.668,-212.014 391.977,-215.879 394.233,-208.541 394.233,-208.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-232.8\">!c</text>\n",
443
        "</g>\n",
444
        "<!-- 3&#45;&gt;1 -->\n",
445
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
446
447
448
449
450
        "<path d=\"M258.25,-249.586C243.436,-253.647 221.422,-257.015 205,-248 192.725,-241.262 184.14,-228.191 178.545,-216.482\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"175.592,-209.803 181.304,-214.931 177.007,-213.004 178.423,-216.205 178.423,-216.205 178.423,-216.205 177.007,-213.004 175.542,-217.479 175.592,-209.803 175.592,-209.803\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-256.8\">c &amp; d</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
451
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
452
453
454
455
456
        "<path d=\"M292.362,-236.475C310.807,-227.724 341.364,-213.227 362.073,-203.403\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"368.422,-200.39 363.448,-206.237 365.26,-201.891 362.098,-203.391 362.098,-203.391 362.098,-203.391 365.26,-201.891 360.748,-200.545 368.422,-200.39 368.422,-200.39\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-229.8\">!c &amp; d</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
457
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
458
459
460
461
        "<path d=\"M266.521,-259.916C264.179,-270.15 267.172,-280 275.5,-280 281.876,-280 285.125,-274.226 285.246,-266.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"284.479,-259.916 288.372,-266.532 284.86,-263.395 285.241,-266.874 285.241,-266.874 285.241,-266.874 284.86,-263.395 282.11,-267.217 284.479,-259.916 284.479,-259.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-283.8\">!d</text>\n",
        "</g>\n",
462
        "<!-- 4&#45;&gt;4 -->\n",
463
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
464
465
466
        "<path d=\"M160.021,-49.916C157.679,-60.1504 160.672,-70 169,-70 175.376,-70 178.625,-64.2263 178.746,-56.9268\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-49.916 181.872,-56.5315 178.36,-53.3952 178.741,-56.8744 178.741,-56.8744 178.741,-56.8744 178.36,-53.3952 175.61,-57.2174 177.979,-49.916 177.979,-49.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
467
468
469
470
471
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
472
        "<IPython.core.display.SVG object>"
473
474
475
       ]
      }
     ],
476
     "prompt_number": 4
477
    },
478
479
480
481
482
483
484
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `translate()` function can also be called with a formula object.  Either as a function, or as a method."
     ]
    },
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U b'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$a \\mathbin{\\mathsf{U}} b$"
       ],
       "metadata": {},
       "output_type": "pyout",
500
       "prompt_number": 5,
501
502
503
504
505
       "text": [
        "a U b"
       ]
      }
     ],
506
     "prompt_number": 5
507
508
509
510
511
512
513
514
515
516
517
518
519
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate(f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
520
       "prompt_number": 6,
521
522
523
524
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
525
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
526
527
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
528
529
530
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
531
        "<title>G</title>\n",
532
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
533
534
535
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
536
537
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
538
539
540
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
541
542
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
543
544
545
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
546
547
548
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
549
550
551
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
552
553
554
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
555
556
557
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
558
559
560
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
561
562
563
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
564
565
566
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
567
568
569
570
571
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
572
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff720> >"
573
574
575
       ]
      }
     ],
576
     "prompt_number": 6
577
578
579
580
581
582
583
584
585
586
587
588
589
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
590
       "prompt_number": 7,
591
592
593
594
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
595
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
596
597
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
598
599
600
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
601
        "<title>G</title>\n",
602
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
603
604
605
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
606
607
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
608
609
610
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
611
612
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
613
614
615
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
616
617
618
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
619
620
621
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
622
623
624
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
625
626
627
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
628
629
630
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
631
632
633
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
634
635
636
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
637
638
639
640
641
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
642
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18dbd0> >"
643
644
645
       ]
      }
     ],
646
     "prompt_number": 7
647
    },
648
649
650
651
652
653
654
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "When used as a method, all the arguments are translation options.  Here is a monitor:"
     ]
    },
655
656
657
658
659
660
661
662
663
664
665
666
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate('mon')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
667
       "prompt_number": 8,
668
669
670
671
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
672
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
673
674
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
675
676
677
        "<svg width=\"163pt\" height=\"77pt\"\n",
        " viewBox=\"0.00 0.00 163.00 77.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 73)\">\n",
678
        "<title>G</title>\n",
679
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
680
681
682
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
683
684
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
685
686
687
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
688
689
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\n",
690
691
692
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
693
694
695
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
696
697
698
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
699
700
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
701
702
703
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
704
705
706
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-18C85.1153,-18 99.5214,-18 111.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-18 111.892,-21.1501 115.392,-18 111.892,-18.0001 111.892,-18.0001 111.892,-18.0001 115.392,-18 111.892,-14.8501 118.892,-18 118.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
707
708
709
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
710
711
712
        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
713
714
715
716
717
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
718
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d150> >"
719
720
721
       ]
      }
     ],
722
     "prompt_number": 8
723
    },
724
725
726
727
728
729
730
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`."
     ]
    },
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('Ga | Gb | Gc'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
       ],
       "metadata": {},
       "output_type": "pyout",
746
       "prompt_number": 9,
747
748
749
750
751
       "text": [
        "Ga | Gb | Gc"
       ]
      }
     ],
752
     "prompt_number": 9
753
754
755
756
757
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
758
      "f.translate('ba', 'small').show('.v')"
759
760
761
762
763
764
765
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
766
       "prompt_number": 10,
767
       "svg": [
768
        "<svg height=\"177pt\" viewBox=\"0.00 0.00 253.00 177.00\" width=\"253pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
769
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
770
        "<title>G</title>\n",
771
        "<polygon fill=\"white\" points=\"-4,4 -4,-173 249,-173 249,4 -4,4\" stroke=\"none\"/>\n",
772
773
774
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
775
        "<ellipse cx=\"109\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
776
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-109.3\">0</text>\n",
777
778
779
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
780
781
        "<path d=\"M109,-167.845C109,-166.206 109,-151.846 109,-138.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"109,-131.058 112.15,-138.058 109,-134.558 109,-138.058 109,-138.058 109,-138.058 109,-134.558 105.85,-138.058 109,-131.058 109,-131.058\" stroke=\"black\"/>\n",
782
783
784
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
785
786
        "<ellipse cx=\"22\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"22\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
787
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22\" y=\"-18.3\">1</text>\n",
788
789
790
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
791
792
        "<path d=\"M96.903,-99.6249C82.686,-85.081 58.8862,-60.7342 41.9306,-43.3887\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"36.9064,-38.2491 44.0522,-41.0528 39.353,-40.7519 41.7996,-43.2548 41.7996,-43.2548 41.7996,-43.2548 39.353,-40.7519 39.547,-45.4567 36.9064,-38.2491 36.9064,-38.2491\" stroke=\"black\"/>\n",
793
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"74\" y=\"-65.8\">a</text>\n",
794
795
796
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
797
798
        "<ellipse cx=\"109\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"109\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
799
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-18.3\">2</text>\n",
800
801
802
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
803
804
        "<path d=\"M109,-94.8399C109,-82.5378 109,-65.6842 109,-51.3928\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"109,-44.1905 112.15,-51.1905 109,-47.6905 109,-51.1905 109,-51.1905 109,-51.1905 109,-47.6905 105.85,-51.1906 109,-44.1905 109,-44.1905\" stroke=\"black\"/>\n",
805
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-65.8\">b</text>\n",
806
807
808
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
809
810
811
        "<ellipse cx=\"198\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"198\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198\" y=\"-18.3\">3</text>\n",
812
813
814
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
815
816
817
        "<path d=\"M121.375,-99.6249C135.919,-85.081 160.266,-60.7342 177.611,-43.3887\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"182.751,-38.2491 180.029,-45.4262 180.276,-40.7239 177.801,-43.1988 177.801,-43.1988 177.801,-43.1988 180.276,-40.7239 175.574,-40.9714 182.751,-38.2491 182.751,-38.2491\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158\" y=\"-65.8\">c</text>\n",
818
819
820
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
821
822
        "<path d=\"M42.5808,-30.3702C52.8447,-31.5284 62,-28.7383 62,-22 62,-16.9463 56.8502,-14.1134 49.9451,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"42.5808,-13.6298 49.5248,-10.3582 46.0803,-13.5688 49.5797,-13.5077 49.5797,-13.5077 49.5797,-13.5077 46.0803,-13.5688 49.6347,-16.6573 42.5808,-13.6298 42.5808,-13.6298\" stroke=\"black\"/>\n",
823
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62\" y=\"-18.3\">a</text>\n",
824
825
826
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
827
828
        "<path d=\"M129.581,-30.3702C139.845,-31.5284 149,-28.7383 149,-22 149,-16.9463 143.85,-14.1134 136.945,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"129.581,-13.6298 136.525,-10.3582 133.08,-13.5688 136.58,-13.5077 136.58,-13.5077 136.58,-13.5077 133.08,-13.5688 136.635,-16.6573 129.581,-13.6298 129.581,-13.6298\" stroke=\"black\"/>\n",
829
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"149\" y=\"-18.3\">b</text>\n",
830
831
832
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
833
834
835
        "<path d=\"M218.581,-30.3702C228.845,-31.5284 238,-28.7383 238,-22 238,-16.9463 232.85,-14.1134 225.945,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"218.581,-13.6298 225.525,-10.3582 222.08,-13.5688 225.58,-13.5077 225.58,-13.5077 225.58,-13.5077 222.08,-13.5688 225.635,-16.6573 218.581,-13.6298 218.581,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-18.3\">c</text>\n",
836
837
838
839
840
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
841
        "<IPython.core.display.SVG object>"
842
843
844
       ]
      }
     ],
845
     "prompt_number": 10
846
847
848
849
850
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
851
      "f.translate('ba', 'det').show('v.')"
852
853
854
855
856
857
858
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
859
       "prompt_number": 11,
860
       "svg": [
861
862
        "<svg height=\"280pt\" viewBox=\"0.00 0.00 596.88 280.00\" width=\"597pt\" 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 276)\">\n",
863
        "<title>G</title>\n",
864
        "<polygon fill=\"white\" points=\"-4,4 -4,-276 592.883,-276 592.883,4 -4,4\" stroke=\"none\"/>\n",
865
866
867
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node2\"><title>6</title>\n",
868
869
870
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"279.883\" y=\"-208.3\">6</text>\n",
871
872
873
        "</g>\n",
        "<!-- I&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
874
875
        "<path d=\"M279.883,-270.834C279.883,-269.159 279.883,-255.116 279.883,-241.289\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"279.883,-234.144 283.033,-241.144 279.883,-237.644 279.883,-241.144 279.883,-241.144 279.883,-241.144 279.883,-237.644 276.733,-241.145 279.883,-234.144 279.883,-234.144\" stroke=\"black\"/>\n",
876
877
878
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
879
880
881
        "<path d=\"M300.874,-219.317C310.971,-220.22 319.883,-217.781 319.883,-212 319.883,-207.664 314.87,-205.208 308.104,-204.632\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"300.874,-204.683 307.852,-201.484 304.374,-204.658 307.874,-204.634 307.874,-204.634 307.874,-204.634 304.374,-204.658 307.896,-207.784 300.874,-204.683 300.874,-204.683\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"319.883\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
882
883
884
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
885
886
887
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.8834\" y=\"-18.3\">0</text>\n",
888
889
890
        "</g>\n",
        "<!-- 6&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
891
892
893
        "<path d=\"M258.05,-208.601C199.066,-201.628 38.871,-179.258 7.88337,-139 -20.5572,-102.052 37.5535,-58.9513 73.4411,-37.1624\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"79.8576,-33.3483 75.45,-39.6328 76.849,-35.1367 73.8404,-36.9251 73.8404,-36.9251 73.8404,-36.9251 76.849,-35.1367 72.2309,-34.2174 79.8576,-33.3483 79.8576,-33.3483\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"7.88337\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
894
895
896
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
897
898
899
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.883\" y=\"-113.3\">1</text>\n",
900
901
902
        "</g>\n",
        "<!-- 6&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
903
904
905
        "<path d=\"M258.548,-205.147C236.734,-198.695 202.263,-187.184 174.883,-172 157.384,-162.295 139.553,-148.469 126.267,-137.237\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.866,-132.602 128.229,-134.77 123.522,-134.881 126.178,-137.161 126.178,-137.161 126.178,-137.161 123.522,-134.881 124.126,-139.551 120.866,-132.602 120.866,-132.602\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.883\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
906
907
908
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
909
910
911
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326.883\" y=\"-18.3\">2</text>\n",
912
913
914
        "</g>\n",
        "<!-- 6&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
915
916
917
        "<path d=\"M295.807,-196.555C302.236,-189.767 309.034,-181.157 312.883,-172 329.476,-132.531 330.508,-82.1352 329.137,-51.2346\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"328.768,-44.1943 332.28,-51.0197 328.951,-47.6895 329.135,-51.1847 329.135,-51.1847 329.135,-51.1847 328.951,-47.6895 325.989,-51.3498 328.768,-44.1943 328.768,-44.1943\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"327.883\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
918
919
920
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
921
922
        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
923
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.883\" y=\"-18.3\">3</text>\n",
924
        "</g>\n",
925
926
        "<!-- 6&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
927
928
929
        "<path d=\"M301.69,-207.819C355.332,-199.487 491.143,-175.144 515.883,-139 535.586,-110.215 514.515,-70.3416 497.048,-45.6345\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"492.712,-39.6958 499.384,-43.4919 494.776,-42.5226 496.84,-45.3493 496.84,-45.3493 496.84,-45.3493 494.776,-42.5226 494.296,-47.2068 492.712,-39.6958 492.712,-39.6958\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"522.883\" y=\"-113.3\">a &amp; !b &amp; !c</text>\n",
930
931
        "</g>\n",
        "<!-- 4 -->\n",
932
        "<g class=\"node\" id=\"node7\"><title>4</title>\n",
933
934
935
        "<ellipse cx=\"218.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"218.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"218.883\" y=\"-113.3\">4</text>\n",
936
937
938
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
939
940
941
        "<path d=\"M266.785,-194.191C261.662,-187.412 255.838,-179.446 250.883,-172 244.654,-162.639 238.247,-152.05 232.818,-142.746\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"229.23,-136.54 235.461,-141.023 230.982,-139.57 232.734,-142.6 232.734,-142.6 232.734,-142.6 230.982,-139.57 230.007,-144.176 229.23,-136.54 229.23,-136.54\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"250.883\" y=\"-160.8\">a &amp; !b &amp; c</text>\n",
942
        "</g>\n",
943
944
945
946
947
948
949
950
951
952
953
954
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node8\"><title>5</title>\n",
        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"432.883\" y=\"-113.3\">5</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
        "<path d=\"M298.339,-199.782C325.793,-183.094 377.444,-151.699 408.145,-133.037\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"414.363,-129.258 410.017,-135.585 411.372,-131.076 408.381,-132.894 408.381,-132.894 408.381,-132.894 411.372,-131.076 406.745,-130.202 414.363,-129.258 414.363,-129.258\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.883\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
        "</g>\n",
955
956
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
957
958
959
        "<path d=\"M119.464,-30.3702C129.728,-31.5284 138.883,-28.7383 138.883,-22 138.883,-16.9463 133.734,-14.1134 126.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"119.464,-13.6298 126.408,-10.3582 122.964,-13.5688 126.463,-13.5077 126.463,-13.5077 126.463,-13.5077 122.964,-13.5688 126.518,-16.6573 119.464,-13.6298 119.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.883\" y=\"-18.3\">c</text>\n",
960
961
962
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
963
964
965
        "<path d=\"M101.764,-94.9925C101.016,-89.1774 100.312,-82.8549 99.8834,-77 99.2697,-68.6098 98.9633,-59.468 98.8243,-51.1319\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"98.7416,-44.0528 101.973,-51.0155 98.7825,-47.5526 98.8234,-51.0524 98.8234,-51.0524 98.8234,-51.0524 98.7825,-47.5526 95.6736,-51.0892 98.7416,-44.0528 98.7416,-44.0528\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.8834\" y=\"-65.8\">!b &amp; c</text>\n",
966
967
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
968
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
969
970
971
        "<path d=\"M125.464,-125.37C135.728,-126.528 144.883,-123.738 144.883,-117 144.883,-111.946 139.734,-109.113 132.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"125.464,-108.63 132.408,-105.358 128.964,-108.569 132.463,-108.508 132.463,-108.508 132.463,-108.508 128.964,-108.569 132.518,-111.657 125.464,-108.63 125.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"144.883\" y=\"-113.3\">b &amp; c</text>\n",
972
        "</g>\n",
973
974
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
975
976
977
        "<path d=\"M118.615,-99.4594C130.558,-85.4667 147.262,-66.9259 155.883,-62 201.053,-36.1916 262.094,-27.4608 297.704,-24.508\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"304.902,-23.9616 298.16,-27.6325 301.412,-24.2266 297.922,-24.4916 297.922,-24.4916 297.922,-24.4916 301.412,-24.2266 297.683,-21.3506 304.902,-23.9616 304.902,-23.9616\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.883\" y=\"-65.8\">b &amp; !c</text>\n",
978
        "</g>\n",
979
980
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
981
982
983
        "<path d=\"M347.464,-30.3702C357.728,-31.5284 366.883,-28.7383 366.883,-22 366.883,-16.9463 361.734,-14.1134 354.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"347.464,-13.6298 354.408,-10.3582 350.964,-13.5688 354.463,-13.5077 354.463,-13.5077 354.463,-13.5077 350.964,-13.5688 354.518,-16.6573 347.464,-13.6298 347.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.883\" y=\"-18.3\">b</text>\n",
984
985
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
986
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
987
988
989
        "<path d=\"M499.464,-30.3702C509.728,-31.5284 518.883,-28.7383 518.883,-22 518.883,-16.9463 513.734,-14.1134 506.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"499.464,-13.6298 506.408,-10.3582 502.964,-13.5688 506.463,-13.5077 506.463,-13.5077 506.463,-13.5077 502.964,-13.5688 506.518,-16.6573 499.464,-13.6298 499.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"518.883\" y=\"-18.3\">a</text>\n",
990
991
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
992
        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;0</title>\n",
993
994
995
        "<path d=\"M214.631,-95.3163C211.41,-84.2043 205.939,-70.9826 196.883,-62 178.078,-43.3468 149.236,-33.3217 127.704,-28.1297\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.707,-26.5487 128.229,-25.019 124.121,-27.3201 127.534,-28.0915 127.534,-28.0915 127.534,-28.0915 124.121,-27.3201 126.84,-31.1641 120.707,-26.5487 120.707,-26.5487\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.883\" y=\"-65.8\">!a &amp; c</text>\n",
996
        "</g>\n",
997
998
        "<!-- 4&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;3</title>\n",
999
1000
1001
        "<path d=\"M238.845,-107.727C265.547,-96.7677 314.456,-77.0653 356.883,-62 388.924,-50.6228 426.214,-38.9231 451.051,-31.345\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"458.026,-29.2257 452.244,-34.2749 454.677,-30.2433 451.328,-31.261 451.328,-31.261 451.328,-31.261 454.677,-30.2433 450.412,-28.2471 458.026,-29.2257 458.026,-29.2257\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.883\" y=\"-65.8\">a &amp; !c</text>\n",
1002
1003
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
1004
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
1005
1006
1007
        "<path d=\"M239.464,-125.37C249.728,-126.528 258.883,-123.738 258.883,-117 258.883,-111.946 253.734,-109.113 246.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"239.464,-108.63 246.408,-105.358 242.964,-108.569 246.463,-108.508 246.463,-108.508 246.463,-108.508 242.964,-108.569 246.518,-111.657 239.464,-108.63 239.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.883\" y=\"-113.3\">a &amp; c</text>\n",
1008
        "</g>\n",
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
        "<!-- 5&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;2</title>\n",
        "<path d=\"M423.273,-97.1109C416.901,-85.9186 407.728,-72.013 396.883,-62 384.323,-50.4024 367.69,-40.9523 353.79,-34.2605\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"347.216,-31.1996 354.891,-31.2984 350.389,-32.6769 353.562,-34.1541 353.562,-34.1541 353.562,-34.1541 350.389,-32.6769 352.232,-37.0098 347.216,-31.1996 347.216,-31.1996\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.883\" y=\"-65.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;3</title>\n",
        "<path d=\"M444.753,-98.1028C448.839,-91.5928 453.288,-84.0908 456.883,-77 461.334,-68.2222 465.577,-58.3236 469.128,-49.4213\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"471.701,-42.843 472.085,-50.5095 470.426,-46.1025 469.152,-49.3621 469.152,-49.3621 469.152,-49.3621 470.426,-46.1025 466.218,-48.2147 471.701,-42.843 471.701,-42.843\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462.883\" y=\"-65.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
        "<path d=\"M453.464,-125.37C463.728,-126.528 472.883,-123.738 472.883,-117 472.883,-111.946 467.734,-109.113 460.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"453.464,-108.63 460.408,-105.358 456.964,-108.569 460.463,-108.508 460.463,-108.508 460.463,-108.508 456.964,-108.569 460.518,-111.657 453.464,-108.63 453.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"472.883\" y=\"-113.3\">a &amp; b</text>\n",
        "</g>\n",
1027
1028
1029
1030
        "</g>\n",
        "</svg>"
       ],
       "text": [
1031
        "<IPython.core.display.SVG object>"
1032
1033
1034
1035
1036
       ]
      }
     ],
     "prompt_number": 11
    },
1037
1038
1039
1040
1041
1042
1043
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Here is how to build an unambiguous automaton:"
     ]
    },
1044
1045
1046
1047
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
1048
      "spot.translate('GFa -> GFb', 'unambig')"
1049
1050
1051
1052
1053
1054
1055
1056
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
1057
1058
1059
1060
1061
1062
1063
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
1064
1065
1066
        "<svg width=\"302pt\" height=\"311pt\"\n",
        " viewBox=\"0.00 0.00 301.50 311.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 307)\">\n",
1067
        "<title>G</title>\n",
1068
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-307 297.5,-307 297.5,4 -4,4\"/>\n",
1069
1070
1071
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1072
1073
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-123\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-119.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1074
1075
1076
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1077
1078
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-123C2.79388,-123 17.1543,-123 30.6317,-123\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-123 30.9419,-126.15 34.4419,-123 30.9419,-123 30.9419,-123 30.9419,-123 34.4419,-123 30.9418,-119.85 37.9419,-123 37.9419,-123\"/>\n",
1079
1080
1081
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1082
1083
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-204\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-200.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1084
1085
1086
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1087
1088
1089
        "<path fill=\"none\" stroke=\"black\" d=\"M66.5112,-137.647C72.9549,-146.82 82.0794,-158.476 92,-167 104.757,-177.961 121.236,-187.349 134.344,-193.926\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"140.854,-197.102 133.181,-196.863 137.708,-195.567 134.563,-194.032 134.563,-194.032 134.563,-194.032 137.708,-195.567 135.944,-191.202 140.854,-197.102 140.854,-197.102\"/>\n",
        "<text text-anchor=\"middle\" x=\"105.5\" y=\"-188.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1090
1091
1092
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
1093
1094
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-66\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1095
1096
1097
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
1098
1099
1100
        "<path fill=\"none\" stroke=\"black\" d=\"M72.1119,-114.343C89.0117,-104.662 116.498,-88.9157 135.486,-78.0382\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"141.572,-74.5518 137.064,-80.7647 138.535,-76.2916 135.498,-78.0314 135.498,-78.0314 135.498,-78.0314 138.535,-76.2916 133.932,-75.2981 141.572,-74.5518 141.572,-74.5518\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1101
1102
1103
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1104
1105
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-123\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-119.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1106
1107
1108
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
1109
1110
1111
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0034,-126.729C106.092,-133.193 177.685,-144.886 237,-135 241.14,-134.31 245.447,-133.19 249.566,-131.905\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.258,-129.634 250.642,-134.867 252.943,-130.759 249.629,-131.884 249.629,-131.884 249.629,-131.884 252.943,-130.759 248.617,-128.901 256.258,-129.634 256.258,-129.634\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-141.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1112
1113
1114
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
1115
1116
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
1117
1118
1119
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
1120
1121
1122
        "<path fill=\"none\" stroke=\"black\" d=\"M64.5788,-106.747C76.3694,-83.5932 101.497,-41.9353 137,-24 172.369,-6.13214 219.835,-9.23041 248.037,-13.4066\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.114,-14.5378 247.705,-16.5434 251.658,-13.9853 248.202,-13.4328 248.202,-13.4328 248.202,-13.4328 251.658,-13.9853 248.699,-10.3223 255.114,-14.5378 255.114,-14.5378\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-27.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1123
1124
1125
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1126
1127
1128
        "<path fill=\"none\" stroke=\"black\" d=\"M152.858,-221.41C151.992,-231.088 153.539,-240 157.5,-240 160.409,-240 162.016,-235.194 162.321,-228.807\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"162.142,-221.41 165.461,-228.331 162.227,-224.909 162.312,-228.408 162.312,-228.408 162.312,-228.408 162.227,-224.909 159.163,-228.484 162.142,-221.41 162.142,-221.41\"/>\n",
        "<text text-anchor=\"start\" x=\"153\" y=\"-258.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
1129
        "<text text-anchor=\"start\" x=\"149.5\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
1130
1131
1132
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1133
1134
1135
        "<path fill=\"none\" stroke=\"black\" d=\"M150.502,-220.596C145.214,-241.863 147.547,-270 157.5,-270 166.403,-270 169.209,-247.485 165.917,-227.513\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"164.498,-220.596 168.991,-226.82 165.202,-224.025 165.905,-227.453 165.905,-227.453 165.905,-227.453 165.202,-224.025 162.819,-228.086 164.498,-220.596 164.498,-220.596\"/>\n",
        "<text text-anchor=\"start\" x=\"151\" y=\"-273.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
1136
1137
1138
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
1139
1140
1141
        "<path fill=\"none\" stroke=\"black\" d=\"M148.521,-81.916C146.179,-92.1504 149.172,-102 157.5,-102 163.876,-102 167.125,-96.2263 167.246,-88.9268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"166.479,-81.916 170.372,-88.5315 166.86,-85.3952 167.241,-88.8744 167.241,-88.8744 167.241,-88.8744 166.86,-85.3952 164.11,-89.2174 166.479,-81.916 166.479,-81.916\"/>\n",
        "<text text-anchor=\"start\" x=\"144\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1142
        "</g>\n",
1143
1144
1145
1146
1147
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M169.815,-79.2791C176.712,-86.6222 186.087,-95.3722 196,-101 212.117,-110.15 232.356,-115.766 247.895,-119.032\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.107,-120.451 247.631,-122.19 251.673,-119.775 248.239,-119.099 248.239,-119.099 248.239,-119.099 251.673,-119.775 248.847,-116.009 255.107,-120.451 255.107,-120.451\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1148
        "</g>\n",
1149
1150
1151
1152
1153
        "<!-- 2&#45;&gt;4 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M174.076,-58.2162C180.773,-54.9495 188.72,-51.1791 196,-48 213.699,-40.2709 234.068,-32.2776 249.262,-26.4873\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.85,-23.9908 250.42,-29.4169 252.577,-25.231 249.304,-26.4713 249.304,-26.4713 249.304,-26.4713 252.577,-25.231 248.188,-23.5256 255.85,-23.9908 255.85,-23.9908\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1154
        "</g>\n",
1155
1156
1157
1158
1159
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M262.811,-107.876C256.615,-98.9778 247.642,-88.2732 237,-82 220.479,-72.2616 198.982,-68.372 182.662,-66.8559\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.564,-66.3138 182.784,-63.7061 179.054,-66.5804 182.544,-66.8469 182.544,-66.8469 182.544,-66.8469 179.054,-66.5804 182.304,-69.9878 175.564,-66.3138 175.564,-66.3138\"/>\n",
        "<text text-anchor=\"start\" x=\"203\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1160
        "</g>\n",
1161
1162
1163
1164
1165
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-138.541C260.73,-148.909 263.922,-159 273,-159 279.95,-159 283.45,-153.085 283.499,-145.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-138.541 286.6,-145.077 283.026,-142.012 283.477,-145.483 283.477,-145.483 283.477,-145.483 283.026,-142.012 280.353,-145.889 282.575,-138.541 282.575,-138.541\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1166
1167
1168
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
1169
1170
1171
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-33.5414C260.73,-43.9087 263.922,-54 273,-54 279.95,-54 283.45,-48.0847 283.499,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-33.5414 286.6,-40.0771 283.026,-37.0123 283.477,-40.4831 283.477,-40.4831 283.477,-40.4831 283.026,-37.0123 280.353,-40.889 282.575,-33.5414 282.575,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1172
        "<text text-anchor=\"start\" x=\"265\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
1173
1174
1175
1176
1177
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1178
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18df00> >"
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
       ]
      }
     ],
     "prompt_number": 12
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Compare with the standard translation:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate('GFa -> GFb')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 13,
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
        "<svg width=\"165pt\" height=\"227pt\"\n",
        " viewBox=\"0.00 0.00 165.00 227.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 223)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-223 161,-223 161,4 -4,4\"/>\n",
        "<!-- I -->\n",
1217
1218
1219
1220
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-77\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-73.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1221
        "</g>\n",
1222
1223
1224
1225
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-77C2.79388,-77 17.1543,-77 30.6317,-77\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-77 30.9419,-80.1501 34.4419,-77 30.9419,-77.0001 30.9419,-77.0001 30.9419,-77.0001 34.4419,-77 30.9418,-73.8501 37.9419,-77 37.9419,-77\"/>\n",
1226
        "</g>\n",
1227
1228
1229
1230
1231
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-94.0373C48.3189,-103.858 50.4453,-113 56,-113 60.166,-113 62.4036,-107.858 62.7128,-101.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-94.0373 65.8541,-100.882 62.5434,-97.5335 62.7076,-101.03 62.7076,-101.03 62.7076,-101.03 62.5434,-97.5335 59.561,-101.177 62.3792,-94.0373 62.3792,-94.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-116.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1232
        "</g>\n",
1233
1234
1235
1236
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"134.5\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1237
        "</g>\n",
1238
1239
1240
1241
1242
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M72.2355,-85.088C84.6805,-91.6946 102.425,-101.114 116.346,-108.505\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"122.833,-111.948 115.173,-111.448 119.741,-110.307 116.65,-108.666 116.65,-108.666 116.65,-108.666 119.741,-110.307 118.127,-105.884 122.833,-111.948 122.833,-111.948\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-104.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",