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.4.3+"
19
  },
20
  "name": "",
21
  "signature": "sha256:4ddb9b8fc1c41bacd7e47f70861303cde0ad425f842ade8e1f23ee74738914b0"
22
23
24
25
26
27
28
29
30
31
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
32
      "from IPython.display import display\n",
Etienne Renault's avatar
Etienne Renault committed
33
      "import spot\n",
34
      "spot.setup()"
35
36
37
38
39
40
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
41
42
43
44
45
46
47
    {
     "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)."
     ]
    },
48
49
50
51
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
52
      "a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a"
53
54
55
56
57
58
59
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
60
       "prompt_number": 2,
61
62
63
64
       "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",
65
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
66
67
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
68
69
70
        "<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",
71
        "<title>G</title>\n",
72
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 415,-180 415,4 -4,4\"/>\n",
73
74
75
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
76
77
        "<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",
78
79
80
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
81
82
        "<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",
83
84
85
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
86
87
88
        "<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",
89
90
91
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
92
93
94
        "<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",
95
96
97
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
98
99
100
        "<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",
101
102
103
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
104
105
        "<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",
106
107
108
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
109
110
111
        "<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",
112
113
114
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
115
116
117
        "<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",
118
119
120
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
121
122
        "<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",
123
124
125
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
126
127
128
        "<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",
129
130
131
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
132
133
        "<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",
134
135
136
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
137
138
139
        "<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",
140
141
142
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
143
144
145
        "<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",
146
147
148
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
149
150
151
        "<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",
152
153
154
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
155
156
157
        "<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",
158
159
160
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
161
162
163
        "<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",
164
165
166
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
167
168
169
        "<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",
170
171
172
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
173
174
175
        "<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",
176
177
178
179
180
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
181
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe334de9900> >"
182
183
184
       ]
      }
     ],
185
     "prompt_number": 2
186
    },
187
188
189
190
191
192
193
    {
     "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."
     ]
    },
194
195
196
197
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
198
      "a.show(\"v\")"
199
200
201
202
203
204
205
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
206
       "prompt_number": 3,
207
       "svg": [
208
209
        "<svg height=\"351pt\" viewBox=\"0.00 0.00 226.36 351.00\" width=\"226pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 347)\">\n",
210
        "<title>G</title>\n",
211
        "<polygon fill=\"white\" points=\"-4,4 -4,-347 222.356,-347 222.356,4 -4,4\" stroke=\"none\"/>\n",
212
213
214
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
215
        "<ellipse cx=\"120.356\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
216
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.356\" y=\"-283.3\">0</text>\n",
217
218
219
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
220
221
        "<path d=\"M120.356,-341.845C120.356,-340.206 120.356,-325.846 120.356,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.356,-305.058 123.506,-312.058 120.356,-308.558 120.356,-312.058 120.356,-312.058 120.356,-312.058 120.356,-308.558 117.206,-312.058 120.356,-305.058 120.356,-305.058\" stroke=\"black\"/>\n",
222
223
224
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
225
226
227
        "<path d=\"M137.393,-293.379C147.214,-294.681 156.356,-292.555 156.356,-287 156.356,-282.834 151.214,-280.596 144.499,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.393,-280.621 144.238,-277.146 140.89,-280.457 144.386,-280.292 144.386,-280.292 144.386,-280.292 140.89,-280.457 144.533,-283.439 137.393,-280.621 137.393,-280.621\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"174.856\" y=\"-283.3\">a &amp; !b</text>\n",
228
229
230
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
231
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
232
233
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67.3561\" y=\"-192.3\">1</text>\n",
234
235
236
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
237
238
239
        "<path d=\"M111.365,-270.902C103.283,-257.33 91.2671,-237.152 81.832,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"78.2263,-215.254 84.5144,-219.656 80.0171,-218.261 81.808,-221.268 81.808,-221.268 81.808,-221.268 80.0171,-218.261 79.1015,-222.88 78.2263,-215.254 78.2263,-215.254\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102.856\" y=\"-239.8\">b</text>\n",
240
241
242
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
243
        "<ellipse cx=\"175.356\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
244
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"175.356\" y=\"-192.3\">4</text>\n",
245
246
247
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
248
249
250
        "<path d=\"M129.438,-271.303C138.435,-256.746 152.298,-234.312 162.439,-217.902\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"166.26,-211.718 165.26,-219.329 164.42,-214.696 162.581,-217.673 162.581,-217.673 162.581,-217.673 164.42,-214.696 159.901,-216.017 166.26,-211.718 166.26,-211.718\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.856\" y=\"-239.8\">!a &amp; !b</text>\n",
251
252
253
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
254
255
256
        "<path d=\"M87.9369,-204.37C98.2008,-205.528 107.356,-202.738 107.356,-196 107.356,-190.946 102.206,-188.113 95.3012,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"87.9369,-187.63 94.8809,-184.358 91.4364,-187.569 94.9358,-187.508 94.9358,-187.508 94.9358,-187.508 91.4364,-187.569 94.9907,-190.657 87.9369,-187.63 87.9369,-187.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"123.356\" y=\"-192.3\">c &amp; d</text>\n",
257
258
259
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
260
        "<ellipse cx=\"68.3561\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
261
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-14.3\">2</text>\n",
262
263
264
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
265
266
267
        "<path d=\"M50.199,-181.727C34.8703,-168.686 13.4697,-147.255 4.35608,-123 -1.27155,-108.022 -1.54226,-101.873 4.35608,-87 13.1144,-64.9152 32.818,-45.8318 48.0656,-33.5506\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"53.866,-29.0284 50.2823,-35.8166 51.1058,-31.1804 48.3455,-33.3324 48.3455,-33.3324 48.3455,-33.3324 51.1058,-31.1804 46.4087,-30.8481 53.866,-29.0284 53.866,-29.0284\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.8561\" y=\"-101.3\">!c &amp; d</text>\n",
268
269
270
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
271
        "<ellipse cx=\"68.3561\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
272
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-101.3\">3</text>\n",
273
274
275
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
276
277
278
        "<path d=\"M56.8135,-176.159C52.3073,-165.855 48.6383,-152.816 51.3561,-141 52.4094,-136.42 54.1455,-131.745 56.1156,-127.365\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"59.3394,-120.78 59.0906,-128.452 57.8004,-123.923 56.2615,-127.067 56.2615,-127.067 56.2615,-127.067 57.8004,-123.923 53.4323,-125.682 59.3394,-120.78 59.3394,-120.78\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"57.3561\" y=\"-144.8\">!d</text>\n",
279
280
281
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
282
283
284
        "<path d=\"M191.646,-204.016C201.745,-205.949 211.356,-203.277 211.356,-196 211.356,-190.542 205.95,-187.674 198.986,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"191.646,-187.984 198.373,-184.286 195.135,-187.705 198.624,-187.426 198.624,-187.426 198.624,-187.426 195.135,-187.705 198.875,-190.566 191.646,-187.984 191.646,-187.984\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"214.856\" y=\"-192.3\">1</text>\n",
285
286
287
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
288
289
290
        "<path d=\"M82.9697,-29.0929C91.4609,-35.4971 101.918,-44.3722 109.356,-54 128.603,-78.9113 134.158,-92.7751 125.356,-123 119.215,-144.088 103.068,-163.203 89.3663,-176.43\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"84.0682,-181.376 87.035,-174.297 86.6265,-178.988 89.1847,-176.599 89.1847,-176.599 89.1847,-176.599 86.6265,-178.988 91.3345,-178.901 84.0682,-181.376 84.0682,-181.376\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132.856\" y=\"-101.3\">c</text>\n",
291
292
293
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
294
295
296
        "<path d=\"M85.0201,-25.3828C94.9811,-27.0234 104.356,-24.5625 104.356,-18 104.356,-13.0781 99.0826,-10.4634 92.2436,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-10.6172 91.8051,-7.02727 88.513,-10.394 92.0059,-10.1709 92.0059,-10.1709 92.0059,-10.1709 88.513,-10.394 92.2067,-13.3145 85.0201,-10.6172 85.0201,-10.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109.856\" y=\"-14.3\">!c</text>\n",
297
298
299
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
300
301
302
        "<path d=\"M68.1643,-123.066C68.0258,-135.398 67.8354,-152.339 67.6743,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"67.5931,-173.908 64.522,-166.873 67.6324,-170.408 67.6718,-166.909 67.6718,-166.909 67.6718,-166.909 67.6324,-170.408 70.8216,-166.944 67.5931,-173.908 67.5931,-173.908\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"84.3561\" y=\"-144.8\">c &amp; d</text>\n",
303
304
305
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
306
307
308
        "<path d=\"M68.3561,-86.799C68.3561,-74.3561 68.3561,-57.3644 68.3561,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"68.3561,-36.1754 71.5062,-43.1754 68.3561,-39.6754 68.3562,-43.1754 68.3562,-43.1754 68.3562,-43.1754 68.3561,-39.6754 65.2062,-43.1755 68.3561,-36.1754 68.3561,-36.1754\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"86.8561\" y=\"-57.8\">!c &amp; d</text>\n",
309
310
311
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
312
313
314
        "<path d=\"M85.0201,-112.383C94.9811,-114.023 104.356,-111.562 104.356,-105 104.356,-100.078 99.0826,-97.4634 92.2436,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-97.6172 91.8051,-94.0273 88.513,-97.394 92.0059,-97.1709 92.0059,-97.1709 92.0059,-97.1709 88.513,-97.394 92.2067,-100.314 85.0201,-97.6172 85.0201,-97.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"110.356\" y=\"-101.3\">!d</text>\n",
315
316
317
318
319
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
320
        "<IPython.core.display.SVG at 0x7fe335a6c0f0>"
321
322
323
       ]
      }
     ],
324
     "prompt_number": 3
325
    },
326
327
328
329
330
331
332
    {
     "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:"
     ]
    },
333
334
335
336
337
338
339
340
341
342
343
344
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.show(\".ast\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
345
       "prompt_number": 4,
346
       "svg": [
347
348
        "<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",
349
        "<title>G</title>\n",
350
351
352
353
        "<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",
354
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
355
        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
356
357
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
358
        "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
359
360
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
361
        "<polygon fill=\"none\" points=\"30,-23 30,-108 82,-108 82,-23 30,-23\" stroke=\"red\"/>\n",
362
363
364
365
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
366
367
        "<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",
368
369
370
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
371
372
        "<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",
373
374
375
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
376
377
378
        "<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",
379
380
381
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
382
383
        "<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",
384
385
386
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
387
388
389
        "<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",
390
391
392
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
393
394
        "<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",
395
396
397
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
398
399
400
        "<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",
401
402
403
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
404
405
406
407
        "<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",
408
409
        "</g>\n",
        "<!-- 2 -->\n",
410
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
411
412
        "<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",
413
414
415
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
416
417
418
419
        "<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",
420
        "</g>\n",
421
422
423
424
        "<!-- 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",
425
        "</g>\n",
426
427
428
429
430
431
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
        "<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",
432
433
434
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
435
436
437
        "<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",
438
439
440
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
441
442
443
        "<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",
444
        "</g>\n",
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
        "<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",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
        "<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",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
        "<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",
463
464
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
465
466
467
        "<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",
468
469
470
471
472
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
473
        "<IPython.core.display.SVG at 0x7fe3340e5588>"
474
475
476
       ]
      }
     ],
477
     "prompt_number": 4
478
    },
479
480
481
482
483
484
485
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `translate()` function can also be called with a formula object.  Either as a function, or as a method."
     ]
    },
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
    {
     "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",
501
       "prompt_number": 5,
502
503
504
505
506
       "text": [
        "a U b"
       ]
      }
     ],
507
     "prompt_number": 5
508
509
510
511
512
513
514
515
516
517
518
519
520
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate(f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
521
       "prompt_number": 6,
522
523
524
525
       "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",
526
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
527
528
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
529
530
531
        "<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",
532
        "<title>G</title>\n",
533
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
534
535
536
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
537
538
        "<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",
539
540
541
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
542
543
        "<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",
544
545
546
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
547
548
549
        "<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",
550
551
552
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
553
554
555
        "<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",
556
557
558
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
559
560
561
        "<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",
562
563
564
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
565
566
567
        "<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",
568
569
570
571
572
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
573
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8331b0> >"
574
575
576
       ]
      }
     ],
577
     "prompt_number": 6
578
579
580
581
582
583
584
585
586
587
588
589
590
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
591
       "prompt_number": 7,
592
593
594
595
       "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",
596
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
597
598
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
599
600
601
        "<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",
602
        "<title>G</title>\n",
603
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
604
605
606
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
607
608
        "<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",
609
610
611
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
612
613
        "<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",
614
615
616
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
617
618
619
        "<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",
620
621
622
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
623
624
625
        "<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",
626
627
628
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
629
630
631
        "<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",
632
633
634
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
635
636
637
        "<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",
638
639
640
641
642
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
643
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833060> >"
644
645
646
       ]
      }
     ],
647
     "prompt_number": 7
648
    },
649
650
651
652
653
654
655
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "When used as a method, all the arguments are translation options.  Here is a monitor:"
     ]
    },
656
657
658
659
660
661
662
663
664
665
666
667
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate('mon')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
668
       "prompt_number": 8,
669
670
671
672
       "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",
673
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
674
675
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
676
677
678
        "<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",
679
        "<title>G</title>\n",
680
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
681
682
683
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
684
685
        "<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",
686
687
688
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
689
690
        "<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",
691
692
693
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
694
695
696
        "<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",
697
698
699
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
700
701
        "<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",
702
703
704
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
705
706
707
        "<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",
708
709
710
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
711
712
713
        "<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",
714
715
716
717
718
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
719
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8330f0> >"
720
721
722
       ]
      }
     ],
723
     "prompt_number": 8
724
    },
725
726
727
728
729
730
731
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`."
     ]
    },
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
    {
     "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",
747
       "prompt_number": 9,
748
749
750
751
752
       "text": [
        "Ga | Gb | Gc"
       ]
      }
     ],
753
     "prompt_number": 9
754
755
756
757
758
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
759
      "f.translate('ba', 'small').show('.v')"
760
761
762
763
764
765
766
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
767
       "prompt_number": 10,
768
       "svg": [
769
        "<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",
770
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
771
        "<title>G</title>\n",
772
        "<polygon fill=\"white\" points=\"-4,4 -4,-173 249,-173 249,4 -4,4\" stroke=\"none\"/>\n",
773
774
775
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
776
        "<ellipse cx=\"109\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
777
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-109.3\">0</text>\n",
778
779
780
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
781
782
        "<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",
783
784
785
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
786
787
        "<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",
788
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22\" y=\"-18.3\">1</text>\n",
789
790
791
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
792
793
        "<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",
794
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"74\" y=\"-65.8\">a</text>\n",
795
796
797
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
798
799
        "<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",
800
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-18.3\">2</text>\n",
801
802
803
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
804
805
        "<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",
806
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-65.8\">b</text>\n",
807
808
809
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
810
811
812
        "<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",
813
814
815
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
816
817
818
        "<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",
819
820
821
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
822
823
        "<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",
824
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62\" y=\"-18.3\">a</text>\n",
825
826
827
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
828
829
        "<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",
830
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"149\" y=\"-18.3\">b</text>\n",
831
832
833
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
834
835
836
        "<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",
837
838
839
840
841
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
842
        "<IPython.core.display.SVG at 0x7fe3340e56d8>"
843
844
845
       ]
      }
     ],
846
     "prompt_number": 10
847
848
849
850
851
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
852
      "f.translate('ba', 'det').show('v.')"
853
854
855
856
857
858
859
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
860
       "prompt_number": 11,
861
       "svg": [
862
863
        "<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",
864
        "<title>G</title>\n",
865
        "<polygon fill=\"white\" points=\"-4,4 -4,-276 592.883,-276 592.883,4 -4,4\" stroke=\"none\"/>\n",
866
867
868
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node2\"><title>6</title>\n",
869
870
871
        "<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",
872
873
874
        "</g>\n",
        "<!-- I&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
875
876
        "<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",
877
878
879
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
880
881
882
        "<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",
883
884
885
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
886
887
888
        "<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",
889
890
891
        "</g>\n",
        "<!-- 6&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
892
893
894
        "<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",
895
896
897
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
898
899
900
        "<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",
901
902
903
        "</g>\n",
        "<!-- 6&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
904
905
906
        "<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",
907
908
909
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
910
911
912
        "<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",
913
914
915
        "</g>\n",
        "<!-- 6&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
916
917
918
        "<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",
919
920
921
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
922
923
924
        "<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\">3</text>\n",
925
926
927
        "</g>\n",
        "<!-- 6&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
928
929
930
        "<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",
931
932
        "</g>\n",
        "<!-- 5 -->\n",
933
        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
934
935
936
        "<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",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.883\" y=\"-18.3\">5</text>\n",
937
938
939
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
940
941
942
        "<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",
943
944
945
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node8\"><title>4</title>\n",
946
947
948
        "<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",
949
950
951
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
952
953
954
        "<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",
955
956
957
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
958
959
960
        "<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",
961
962
963
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
964
965
966
        "<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",
967
968
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
969
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
970
971
972
        "<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",
973
        "</g>\n",
974
975
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
976
977
978
        "<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",
979
        "</g>\n",
980
981
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
982
983
984
        "<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",
985
        "</g>\n",
986
987
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
988
989
990
        "<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",
991
992
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
993
        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
994
995
996
        "<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",
997
        "</g>\n",
998
999
        "<!-- 3&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;5</title>\n",
1000
1001
1002
        "<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",
1003
1004
1005
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
1006
1007
1008
        "<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",
1009
1010
1011
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
1012
1013
1014
        "<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",
1015
1016
1017
        "</g>\n",
        "<!-- 4&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>4-&gt;5</title>\n",
1018
1019
1020
        "<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",
1021
1022
1023
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;4</title>\n",
1024
1025
1026
        "<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",
1027
1028
1029
1030
1031
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
1032
        "<IPython.core.display.SVG at 0x7fe3340aba20>"
1033
1034
1035
1036
1037
       ]
      }
     ],
     "prompt_number": 11
    },
1038
1039
1040
1041
1042
1043
1044
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Here is how to build an unambiguous automaton:"
     ]
    },
1045
1046
1047
1048
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
1049
      "spot.translate('GFa -> GFb', 'unambig')"
1050
1051
1052
1053
1054
1055
1056
1057
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
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
1178
       "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": [
1179
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833300> >"
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
1279
       ]
      }
     ],
     "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": [
1280
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8332d0> >"
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
1312
       ]
      }
     ],
     "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",
1313
1314
1315
        "<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",
1316
        "<title>G</title>\n",
1317
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-172 262,-172 262,4 -4,4\"/>\n",
1318
1319
1320
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1321
1322
        "<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",
1323
1324
1325
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1326
1327
        "<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",
1328
1329
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
1330
1331
1332
1333
        "<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",
1334
1335
1336
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1337
1338
1339
        "<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",
1340
1341
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
1342
1343
1344
1345
        "<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",
1346
1347
1348
1349
1350
1351
1352
1353
        "</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",
1354
1355
1356
        "<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",
1357
1358
1359
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1360
1361
1362
        "<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",
1363
1364
1365
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
1366
1367
1368
        "<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",
1369
1370
1371
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1372
1373
1374
        "<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",
1375
1376
1377
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1378
1379
1380
        "<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",
1381
1382
1383
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
1384
1385
1386
        "<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",
1387
1388
1389
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
1390
1391
1392
        "<path fill=\"none\" stroke=\"black\" d=\"M227.63,-42.5808C226.472,-52.8447 229.262,-62 236,-62 241.054,-62 243.887,-56.8502 244.499,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"244.37,-42.5808 247.642,-49.5248 244.431,-46.0803 244.492,-49.5797 244.492,-49.5797 244.492,-49.5797 244.431,-46.0803 241.343,-49.6347 244.37,-42.5808 244.37,-42.5808\"/>\n",
        "<text text-anchor=\"start\" x=\"231.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
1393
1394
1395
1396
1397
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1398
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833120> >"
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413