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 0x7f7fe56a0540> >"
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 220.18 351.00\" width=\"220pt\" 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 216.176,-347 216.176,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=\"116.176\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"116.176\" 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=\"M116.176,-341.845C116.176,-340.206 116.176,-325.846 116.176,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"116.176,-305.058 119.326,-312.058 116.176,-308.558 116.176,-312.058 116.176,-312.058 116.176,-312.058 116.176,-308.558 113.026,-312.058 116.176,-305.058 116.176,-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=\"M133.213,-293.379C143.033,-294.681 152.176,-292.555 152.176,-287 152.176,-282.834 147.033,-280.596 140.319,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"133.213,-280.621 140.057,-277.146 136.709,-280.457 140.205,-280.292 140.205,-280.292 140.205,-280.292 136.709,-280.457 140.353,-283.439 133.213,-280.621 133.213,-280.621\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168.676\" 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=\"63.1755\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"63.1755\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"63.1755\" 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=\"M107.185,-270.902C99.1023,-257.33 87.0865,-237.152 77.6514,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"74.0458,-215.254 80.3339,-219.656 75.8366,-218.261 77.6274,-221.268 77.6274,-221.268 77.6274,-221.268 75.8366,-218.261 74.9209,-222.88 74.0458,-215.254 74.0458,-215.254\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.6755\" 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=\"169.176\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169.176\" 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=\"M125.166,-270.902C133.822,-256.367 146.99,-234.255 156.667,-218.005\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"160.318,-211.875 159.442,-219.501 158.527,-214.882 156.736,-217.889 156.736,-217.889 156.736,-217.889 158.527,-214.882 154.029,-216.277 160.318,-211.875 160.318,-211.875\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"163.176\" 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=\"M83.7563,-204.37C94.0202,-205.528 103.176,-202.738 103.176,-196 103.176,-190.946 98.0257,-188.113 91.1207,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"83.7563,-187.63 90.7003,-184.358 87.2558,-187.569 90.7553,-187.508 90.7553,-187.508 90.7553,-187.508 87.2558,-187.569 90.8102,-190.657 83.7563,-187.63 83.7563,-187.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"118.176\" 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=\"64.1755\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"64.1755\" 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=\"M46.8076,-181.236C32.4563,-168.007 12.6056,-146.588 4.17551,-123 -1.20916,-107.933 -1.48317,-101.966 4.17551,-87 12.2372,-65.6786 30.3712,-46.7242 44.6062,-34.2791\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"50.0362,-29.6769 46.7329,-36.6059 47.3662,-31.9399 44.6962,-34.2029 44.6962,-34.2029 44.6962,-34.2029 47.3662,-31.9399 42.6595,-31.7998 50.0362,-29.6769 50.0362,-29.6769\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"20.6755\" 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=\"64.1755\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"64.1755\" 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=\"M53.2767,-176.138C49.0477,-165.827 45.6086,-152.789 48.1755,-141 49.1456,-136.544 50.7357,-131.977 52.5462,-127.674\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"55.5153,-121.184 55.4677,-128.86 54.0593,-124.366 52.6032,-127.549 52.6032,-127.549 52.6032,-127.549 54.0593,-124.366 49.7387,-126.239 55.5153,-121.184 55.5153,-121.184\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.1755\" 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=\"M185.466,-204.016C195.565,-205.949 205.176,-203.277 205.176,-196 205.176,-190.542 199.769,-187.674 192.806,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"185.466,-187.984 192.193,-184.286 188.955,-187.705 192.444,-187.426 192.444,-187.426 192.444,-187.426 188.955,-187.705 192.694,-190.566 185.466,-187.984 185.466,-187.984\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"208.676\" 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=\"M77.8501,-30.0814C85.3082,-36.5564 94.3776,-45.173 101.176,-54 120.513,-79.1097 128.036,-92.5709 119.176,-123 113.156,-143.671 97.7364,-162.693 84.5983,-175.987\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"79.5143,-180.969 82.3093,-173.82 82.0142,-178.52 84.514,-176.07 84.514,-176.07 84.514,-176.07 82.0142,-178.52 86.7187,-178.32 79.5143,-180.969 79.5143,-180.969\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"125.676\" 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=\"M80.8396,-25.3828C90.8005,-27.0234 100.176,-24.5625 100.176,-18 100.176,-13.0781 94.9021,-10.4634 88.0631,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"80.8396,-10.6172 87.6245,-7.02727 84.3325,-10.394 87.8253,-10.1709 87.8253,-10.1709 87.8253,-10.1709 84.3325,-10.394 88.0262,-13.3145 80.8396,-10.6172 80.8396,-10.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"105.176\" 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=\"M63.9838,-123.066C63.8452,-135.398 63.6549,-152.339 63.4937,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"63.4125,-173.908 60.3414,-166.873 63.4519,-170.408 63.4912,-166.909 63.4912,-166.909 63.4912,-166.909 63.4519,-170.408 66.641,-166.944 63.4125,-173.908 63.4125,-173.908\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"79.1755\" 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=\"M64.1755,-86.799C64.1755,-74.3561 64.1755,-57.3644 64.1755,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"64.1755,-36.1754 67.3256,-43.1754 64.1756,-39.6754 64.1756,-43.1754 64.1756,-43.1754 64.1756,-43.1754 64.1756,-39.6754 61.0256,-43.1755 64.1755,-36.1754 64.1755,-36.1754\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"80.6755\" 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=\"M80.8396,-112.383C90.8005,-114.023 100.176,-111.562 100.176,-105 100.176,-100.078 94.9021,-97.4634 88.0631,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"80.8396,-97.6172 87.6245,-94.0273 84.3325,-97.394 87.8253,-97.1709 87.8253,-97.1709 87.8253,-97.1709 84.3325,-97.394 88.0262,-100.314 80.8396,-97.6172 80.8396,-97.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"105.176\" 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
351
352
        "<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",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-319.8\">\u24ff</text>\n",
        "<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=\"edge11\"><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=\"edge12\"><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=\"edge13\"><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=\"edge2\"><title>1-&gt;1</title>\n",
403
404
405
406
        "<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",
        "<text fill=\"#5da5da\" 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=\"edge3\"><title>1-&gt;2</title>\n",
415
416
417
418
        "<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",
        "<text fill=\"#5da5da\" 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=\"edge4\"><title>1-&gt;3</title>\n",
427
428
429
430
        "<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",
        "<text fill=\"#5da5da\" 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=\"edge5\"><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=\"edge6\"><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=\"edge7\"><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=\"edge8\"><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=\"edge9\"><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=\"edge10\"><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 0x7f7fe4d87f90> >"
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 0x7f7fe4da41b0> >"
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 0x7f7fe4e0f330> >"
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
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
       "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=\"302pt\" height=\"295pt\"\n",
        " viewBox=\"0.00 0.00 301.50 295.16\" 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 291.16)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-291.16 297.5,-291.16 297.5,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-107.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-103.46\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-107.16C2.79388,-107.16 17.1543,-107.16 30.6317,-107.16\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-107.16 30.9419,-110.31 34.4419,-107.16 30.9419,-107.16 30.9419,-107.16 30.9419,-107.16 34.4419,-107.16 30.9418,-104.01 37.9419,-107.16 37.9419,-107.16\"/>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-188.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-184.46\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M66.5112,-121.807C72.9549,-130.98 82.0794,-142.636 92,-151.16 104.757,-162.122 121.236,-171.509 134.344,-178.086\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"140.854,-181.263 133.181,-181.024 137.708,-179.728 134.563,-178.193 134.563,-178.193 134.563,-178.193 137.708,-179.728 135.944,-175.362 140.854,-181.263 140.854,-181.263\"/>\n",
        "<text text-anchor=\"middle\" x=\"105.5\" y=\"-172.96\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-127.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-123.46\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1079,-109.003C100.327,-111.801 152.035,-117.211 196,-121.16 213.175,-122.703 232.554,-124.23 247.444,-125.357\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"254.786,-125.908 247.57,-128.525 251.296,-125.646 247.806,-125.384 247.806,-125.384 247.806,-125.384 251.296,-125.646 248.042,-122.243 254.786,-125.908 254.786,-125.908\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-122.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-50.1603\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-46.4603\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M72.1119,-98.5032C89.0117,-88.8219 116.498,-73.076 135.486,-62.1985\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"141.572,-58.7121 137.064,-64.925 138.535,-60.4519 135.498,-62.1917 135.498,-62.1917 135.498,-62.1917 138.535,-60.4519 133.932,-59.4584 141.572,-58.7121 141.572,-58.7121\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-89.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-31.1603\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-27.4603\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M64.2827,-91.086C75.861,-67.75 100.908,-25.398 137,-8.1603 173.984,9.50377 222.376,-7.05194 250.041,-19.7503\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.608,-22.8724 248.934,-22.7117 253.447,-21.3696 250.286,-19.8668 250.286,-19.8668 250.286,-19.8668 253.447,-21.3696 251.639,-17.0219 256.608,-22.8724 256.608,-22.8724\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-11.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M152.858,-205.57C151.992,-215.248 153.539,-224.16 157.5,-224.16 160.409,-224.16 162.016,-219.354 162.321,-212.968\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"162.142,-205.57 165.461,-212.492 162.227,-209.069 162.312,-212.568 162.312,-212.568 162.312,-212.568 162.227,-209.069 159.163,-212.645 162.142,-205.57 162.142,-205.57\"/>\n",
        "<text text-anchor=\"start\" x=\"153\" y=\"-242.96\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"149.5\" y=\"-227.96\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M150.502,-204.756C145.214,-226.024 147.547,-254.16 157.5,-254.16 166.403,-254.16 169.209,-231.646 165.917,-211.673\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"164.498,-204.756 168.991,-210.981 165.202,-208.185 165.905,-211.613 165.905,-211.613 165.905,-211.613 165.202,-208.185 162.819,-212.246 164.498,-204.756 164.498,-204.756\"/>\n",
        "<text text-anchor=\"start\" x=\"151\" y=\"-257.96\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-142.702C260.73,-153.069 263.922,-163.16 273,-163.16 279.95,-163.16 283.45,-157.245 283.499,-149.819\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-142.702 286.6,-149.237 283.026,-146.173 283.477,-149.643 283.477,-149.643 283.477,-149.643 283.026,-146.173 280.353,-150.049 282.575,-142.702 282.575,-142.702\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-181.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "<text text-anchor=\"start\" x=\"265\" y=\"-166.96\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M172.875,-59.9124C192.831,-73.4509 229.029,-98.0082 251.724,-113.405\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"257.742,-117.487 250.181,-116.164 254.845,-115.522 251.949,-113.557 251.949,-113.557 251.949,-113.557 254.845,-115.522 253.718,-110.951 257.742,-117.487 257.742,-117.487\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-105.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M148.521,-66.0763C146.179,-76.3107 149.172,-86.1603 157.5,-86.1603 163.876,-86.1603 167.125,-80.3866 167.246,-73.0871\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"166.479,-66.0763 170.372,-72.6918 166.86,-69.5555 167.241,-73.0347 167.241,-73.0347 167.241,-73.0347 166.86,-69.5555 164.11,-73.3777 166.479,-66.0763 166.479,-66.0763\"/>\n",
        "<text text-anchor=\"start\" x=\"144\" y=\"-89.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M175.601,-51.3981C191.679,-52.1201 216.301,-52.083 237,-47.1603 241.436,-46.1053 245.995,-44.4755 250.295,-42.6526\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.785,-39.6836 251.73,-45.4601 253.602,-41.1396 250.42,-42.5956 250.42,-42.5956 250.42,-42.5956 253.602,-41.1396 249.109,-39.7311 256.785,-39.6836 256.785,-39.6836\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-54.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M255.068,-27.6221C239.446,-25.0259 215.751,-22.7942 196,-28.1603 189.927,-29.8102 183.832,-32.719 178.374,-35.8916\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"172.298,-39.6776 176.573,-33.3021 175.268,-37.8266 178.239,-35.9756 178.239,-35.9756 178.239,-35.9756 175.268,-37.8266 179.905,-38.649 172.298,-39.6776 172.298,-39.6776\"/>\n",
        "<text text-anchor=\"start\" x=\"203\" y=\"-31.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-46.7018C260.73,-57.069 263.922,-67.1603 273,-67.1603 279.95,-67.1603 283.45,-61.245 283.499,-53.8194\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-46.7018 286.6,-53.2374 283.026,-50.1726 283.477,-53.6434 283.477,-53.6434 283.477,-53.6434 283.026,-50.1726 280.353,-54.0493 282.575,-46.7018 282.575,-46.7018\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-70.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</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 0x7f7fe4da4510> >"
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
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
       ]
      }
     ],
     "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",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-97\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-93.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-97C2.79388,-97 17.1543,-97 30.6317,-97\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-97 30.9419,-100.15 34.4419,-97 30.9419,-97.0001 30.9419,-97.0001 30.9419,-97.0001 34.4419,-97 30.9418,-93.8501 37.9419,-97 37.9419,-97\"/>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-114.037C48.3189,-123.858 50.4453,-133 56,-133 60.166,-133 62.4036,-127.858 62.7128,-121.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-114.037 65.8541,-120.882 62.5434,-117.533 62.7076,-121.03 62.7076,-121.03 62.7076,-121.03 62.5434,-117.533 59.561,-121.177 62.3792,-114.037 62.3792,-114.037\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"139\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M71.4812,-107.012C84.3818,-115.931 103.39,-129.072 117.788,-139.026\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"123.644,-143.075 116.095,-141.685 120.765,-141.085 117.886,-139.094 117.886,-139.094 117.886,-139.094 120.765,-141.085 119.678,-136.503 123.644,-143.075 123.644,-143.075\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"139\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M69.6562,-84.6562C83.209,-71.4381 104.825,-50.3563 120.113,-35.4454\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"125.433,-30.2571 122.621,-37.3997 122.927,-32.7008 120.421,-35.1446 120.421,-35.1446 120.421,-35.1446 122.927,-32.7008 118.222,-32.8895 125.433,-30.2571 125.433,-30.2571\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M131.969,-169.664C130.406,-179.625 132.75,-189 139,-189 143.688,-189 146.178,-183.727 146.471,-176.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"146.031,-169.664 149.601,-176.46 146.244,-173.158 146.456,-176.651 146.456,-176.651 146.456,-176.651 146.244,-173.158 143.312,-176.842 146.031,-169.664 146.031,-169.664\"/>\n",
        "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"131\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M135.405,-35.7817C134.794,-45.3149 135.992,-54 139,-54 141.209,-54 142.442,-49.3161 142.699,-43.0521\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"142.595,-35.7817 145.845,-42.736 142.645,-39.2814 142.695,-42.781 142.695,-42.781 142.695,-42.781 142.645,-39.2814 139.546,-42.8261 142.595,-35.7817 142.595,-35.7817\"/>\n",
        "<text text-anchor=\"start\" x=\"134.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"131\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M133.494,-35.249C129.587,-56.4346 131.422,-84 139,-84 145.749,-84 147.943,-62.1347 145.582,-42.3851\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.506,-35.249 148.665,-41.7011 145.028,-38.7099 145.55,-42.1708 145.55,-42.1708 145.55,-42.1708 145.028,-38.7099 142.435,-42.6405 144.506,-35.249 144.506,-35.249\"/>\n",
        "<text text-anchor=\"start\" x=\"132.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1279
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4540> >"
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
       ]
      }
     ],
     "prompt_number": 13
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "And here is the automaton above with state-based acceptance:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate('GFa -> GFb', 'sbacc')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 14,
       "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",
1312
1313
1314
        "<svg width=\"266pt\" height=\"176pt\"\n",
        " viewBox=\"0.00 0.00 266.00 176.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 172)\">\n",
1315
        "<title>G</title>\n",
1316
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-172 262,-172 262,4 -4,4\"/>\n",
1317
1318
1319
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1320
1321
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-73\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-69.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1322
1323
1324
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1325
1326
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-73C2.79388,-73 17.1543,-73 30.6317,-73\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-73 30.9419,-76.1501 34.4419,-73 30.9419,-73.0001 30.9419,-73.0001 30.9419,-73.0001 34.4419,-73 30.9418,-69.8501 37.9419,-73 37.9419,-73\"/>\n",
1327
1328
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
1329
1330
1331
1332
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-90.0373C48.3189,-99.8579 50.4453,-109 56,-109 60.166,-109 62.4036,-103.858 62.7128,-97.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-90.0373 65.8541,-96.8818 62.5434,-93.5335 62.7076,-97.0296 62.7076,-97.0296 62.7076,-97.0296 62.5434,-93.5335 59.561,-97.1774 62.3792,-90.0373 62.3792,-90.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1333
1334
1335
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1336
1337
1338
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"143\" cy=\"-113\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"143\" cy=\"-113\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"start\" x=\"138.5\" y=\"-109.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1339
1340
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
1341
1342
1343
1344
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M72.5903,-80.3366C84.6994,-86.035 101.76,-94.0634 115.936,-100.735\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"122.629,-103.884 114.954,-103.754 119.462,-102.394 116.295,-100.904 116.295,-100.904 116.295,-100.904 119.462,-102.394 117.637,-98.0535 122.629,-103.884 122.629,-103.884\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1345
1346
1347
1348
1349
1350
1351
1352
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"143\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"143\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
1353
1354
1355
        "<path fill=\"none\" stroke=\"black\" d=\"M71.8059,-64.1165C85.3737,-55.9758 105.611,-43.8333 120.875,-34.6748\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"127.079,-30.9528 122.697,-37.2555 124.077,-32.7536 121.076,-34.5544 121.076,-34.5544 121.076,-34.5544 124.077,-32.7536 119.455,-31.8532 127.079,-30.9528 127.079,-30.9528\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-53.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
1356
1357
1358
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1359
1360
1361
        "<path fill=\"none\" stroke=\"black\" d=\"M134.994,-133.581C133.886,-143.845 136.555,-153 143,-153 147.834,-153 150.544,-147.85 151.129,-140.945\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.006,-133.581 154.273,-140.527 151.065,-137.08 151.123,-140.58 151.123,-140.58 151.123,-140.58 151.065,-137.08 147.973,-140.632 151.006,-133.581 151.006,-133.581\"/>\n",
        "<text text-anchor=\"start\" x=\"137.5\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1362
1363
1364
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
1365
1366
1367
        "<path fill=\"none\" stroke=\"black\" d=\"M135.332,-38.2903C133.483,-48.3892 136.039,-58 143,-58 148.221,-58 150.964,-52.5939 151.229,-45.6304\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"150.668,-38.2903 154.342,-45.0299 150.935,-41.7801 151.201,-45.2699 151.201,-45.2699 151.201,-45.2699 150.935,-41.7801 148.06,-45.5099 150.668,-38.2903 150.668,-38.2903\"/>\n",
        "<text text-anchor=\"start\" x=\"136.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
1368
1369
1370
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1371
1372
1373
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"236\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"236\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"236\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1374
1375
1376
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1377
1378
1379
        "<path fill=\"none\" stroke=\"black\" d=\"M161.116,-22C173.948,-22 191.793,-22 206.731,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"213.796,-22 206.796,-25.1501 210.296,-22 206.796,-22.0001 206.796,-22.0001 206.796,-22.0001 210.296,-22 206.795,-18.8501 213.796,-22 213.796,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"185\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
1380
1381
1382
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
1383
1384
1385
        "<path fill=\"none\" stroke=\"black\" d=\"M217.045,-9.91849C207.177,-4.69562 194.613,-0.32156 183,-3 176.881,-4.41121 170.611,-6.91853 164.938,-9.6583\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"158.596,-12.9296 163.373,-6.92094 161.707,-11.325 164.817,-9.72043 164.817,-9.72043 164.817,-9.72043 161.707,-11.325 166.261,-12.5199 158.596,-12.9296 158.596,-12.9296\"/>\n",
        "<text text-anchor=\"start\" x=\"183\" y=\"-6.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
1386
1387
1388
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;3</title>\n",