automata.ipynb 245 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
22
23
24
25
26
27
28
29
30
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
31
      "from IPython.display import display\n",
Etienne Renault's avatar
Etienne Renault committed
32
      "import spot\n",
33
      "spot.setup()"
34
35
36
37
38
39
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
40
41
42
43
44
45
46
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To build an automaton, simply call `translate()` with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the `ltl2tgba` tool, and they can be abbreviated)."
     ]
    },
47
48
49
50
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
51
      "a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a"
52
53
54
55
56
57
58
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
59
       "prompt_number": 2,
60
61
62
63
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
64
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
65
66
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
67
68
69
        "<svg width=\"419pt\" height=\"184pt\"\n",
        " viewBox=\"0.00 0.00 419.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 180)\">\n",
70
        "<title>G</title>\n",
71
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 415,-180 415,4 -4,4\"/>\n",
72
73
74
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
75
76
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-69\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-65.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
77
78
79
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
80
81
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-69C2.79388,-69 17.1543,-69 30.6317,-69\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-69 30.9419,-72.1501 34.4419,-69 30.9419,-69.0001 30.9419,-69.0001 30.9419,-69.0001 34.4419,-69 30.9418,-65.8501 37.9419,-69 37.9419,-69\"/>\n",
82
83
84
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
85
86
87
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-86.0373C48.3189,-95.8579 50.4453,-105 56,-105 60.166,-105 62.4036,-99.8576 62.7128,-93.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-86.0373 65.8541,-92.8818 62.5434,-89.5335 62.7076,-93.0296 62.7076,-93.0296 62.7076,-93.0296 62.5434,-89.5335 59.561,-93.1774 62.3792,-86.0373 62.3792,-86.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
88
89
90
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
91
92
93
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
94
95
96
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
97
98
99
        "<path fill=\"none\" stroke=\"black\" d=\"M73.4767,-74.731C92.1945,-81.2416 123.014,-91.9614 145.203,-99.6792\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"152.077,-102.07 144.431,-102.746 148.772,-100.921 145.466,-99.7706 145.466,-99.7706 145.466,-99.7706 148.772,-100.921 146.501,-96.7955 152.077,-102.07 152.077,-102.07\"/>\n",
        "<text text-anchor=\"start\" x=\"108\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
100
101
102
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
103
104
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
105
106
107
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
108
109
110
        "<path fill=\"none\" stroke=\"black\" d=\"M72.9903,-61.9087C92.9015,-53.0784 127.032,-37.9422 149.557,-27.9532\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"156.146,-25.0311 151.024,-30.7485 152.946,-26.45 149.747,-27.869 149.747,-27.869 149.747,-27.869 152.946,-26.45 148.47,-24.9894 156.146,-25.0311 156.146,-25.0311\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
111
112
113
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
114
115
116
        "<path fill=\"none\" stroke=\"black\" d=\"M162.933,-128.757C161.223,-139.35 164.578,-149 173,-149 179.448,-149 182.926,-143.343 183.435,-135.938\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"183.067,-128.757 186.571,-135.587 183.246,-132.253 183.425,-135.748 183.425,-135.748 183.425,-135.748 183.246,-132.253 180.279,-135.91 183.067,-128.757 183.067,-128.757\"/>\n",
        "<text text-anchor=\"start\" x=\"156\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
117
118
119
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
120
121
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"393\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"393\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
122
123
124
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
125
126
127
        "<path fill=\"none\" stroke=\"black\" d=\"M190.278,-122.894C214.315,-141.67 260.899,-171.444 302,-159 329.774,-150.591 356.811,-130.471 373.881,-115.843\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"379.274,-111.117 376.085,-118.1 376.642,-113.424 374.009,-115.73 374.009,-115.73 374.009,-115.73 376.642,-113.424 371.933,-113.361 379.274,-111.117 379.274,-111.117\"/>\n",
        "<text text-anchor=\"start\" x=\"265\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
128
129
130
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
131
132
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"283.5\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"283.5\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
133
134
135
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
136
137
138
        "<path fill=\"none\" stroke=\"black\" d=\"M195.152,-108.988C209.762,-108.77 229.617,-108.059 247,-106 250.725,-105.559 254.645,-104.943 258.464,-104.257\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"265.61,-102.881 259.332,-107.298 262.173,-103.543 258.737,-104.204 258.737,-104.204 258.737,-104.204 262.173,-103.543 258.141,-101.111 265.61,-102.881 265.61,-102.881\"/>\n",
        "<text text-anchor=\"start\" x=\"223.5\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
139
140
141
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
142
143
144
        "<path fill=\"none\" stroke=\"black\" d=\"M163.425,-33.5414C160.73,-43.9087 163.922,-54 173,-54 179.95,-54 183.45,-48.0847 183.499,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"182.575,-33.5414 186.6,-40.0771 183.026,-37.0123 183.477,-40.4831 183.477,-40.4831 183.477,-40.4831 183.026,-37.0123 180.353,-40.889 182.575,-33.5414 182.575,-33.5414\"/>\n",
        "<text text-anchor=\"middle\" x=\"173\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
145
146
147
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
148
149
150
        "<path fill=\"none\" stroke=\"black\" d=\"M377.812,-89.0507C354.64,-74.0075 307.035,-48.1189 265,-57 239.248,-62.4409 213.545,-78.3348 196.057,-91.1322\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"190.453,-95.3338 194.164,-88.6143 193.253,-93.2342 196.053,-91.1346 196.053,-91.1346 196.053,-91.1346 193.253,-93.2342 197.943,-93.6549 190.453,-95.3338 190.453,-95.3338\"/>\n",
        "<text text-anchor=\"start\" x=\"280\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
151
152
153
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
154
155
156
        "<path fill=\"none\" stroke=\"black\" d=\"M383.767,-114.541C381.169,-124.909 384.246,-135 393,-135 399.702,-135 403.077,-129.085 403.124,-121.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"402.233,-114.541 406.229,-121.095 402.668,-118.014 403.103,-121.487 403.103,-121.487 403.103,-121.487 402.668,-118.014 399.977,-121.879 402.233,-114.541 402.233,-114.541\"/>\n",
        "<text text-anchor=\"start\" x=\"387.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!c</text>\n",
157
158
159
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
160
161
162
        "<path fill=\"none\" stroke=\"black\" d=\"M266.525,-92.366C260.514,-90.2005 253.548,-88.0768 247,-87 232.089,-84.548 227.616,-83.1619 213,-87 207.831,-88.3574 202.625,-90.5725 197.776,-93.0866\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"191.42,-96.6478 195.987,-90.4779 194.474,-94.9369 197.527,-93.2259 197.527,-93.2259 197.527,-93.2259 194.474,-94.9369 199.067,-95.9739 191.42,-96.6478 191.42,-96.6478\"/>\n",
        "<text text-anchor=\"start\" x=\"213\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
163
164
165
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
166
167
168
        "<path fill=\"none\" stroke=\"black\" d=\"M301.772,-99C319.638,-99 347.686,-99 367.767,-99\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"374.771,-99 367.771,-102.15 371.271,-99 367.771,-99.0001 367.771,-99.0001 367.771,-99.0001 371.271,-99 367.771,-95.8501 374.771,-99 374.771,-99\"/>\n",
        "<text text-anchor=\"start\" x=\"320\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
169
170
171
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
172
173
174
        "<path fill=\"none\" stroke=\"black\" d=\"M274.521,-114.916C272.179,-125.15 275.172,-135 283.5,-135 289.876,-135 293.125,-129.226 293.246,-121.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"292.479,-114.916 296.372,-121.532 292.86,-118.395 293.241,-121.874 293.241,-121.874 293.241,-121.874 292.86,-118.395 290.11,-122.217 292.479,-114.916 292.479,-114.916\"/>\n",
        "<text text-anchor=\"start\" x=\"277\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
175
176
177
178
179
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
180
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c25174540> >"
181
182
183
       ]
      }
     ],
184
     "prompt_number": 2
185
    },
186
187
188
189
190
191
192
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The call the `spot.setup()` in the first cells has installed a default style for the graphviz output.  If you want to change this style temporarily, you can call the `show(style)` method explicitely.  For instance here is a vertical layout with the default font of GraphViz."
     ]
    },
193
194
195
196
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
197
      "a.show(\"v\")"
198
199
200
201
202
203
204
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
205
       "prompt_number": 3,
206
       "svg": [
207
208
        "<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",
209
        "<title>G</title>\n",
210
        "<polygon fill=\"white\" points=\"-4,4 -4,-347 222.356,-347 222.356,4 -4,4\" stroke=\"none\"/>\n",
211
212
213
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
214
215
        "<ellipse cx=\"120.356\" cy=\"-287\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.356\" y=\"-283.3\">0</text>\n",
216
217
218
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
219
220
        "<path d=\"M120.356,-341.845C120.356,-340.206 120.356,-325.846 120.356,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.356,-305.058 123.506,-312.058 120.356,-308.558 120.356,-312.058 120.356,-312.058 120.356,-312.058 120.356,-308.558 117.206,-312.058 120.356,-305.058 120.356,-305.058\" stroke=\"black\"/>\n",
221
222
223
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
224
225
226
        "<path d=\"M137.393,-293.379C147.214,-294.681 156.356,-292.555 156.356,-287 156.356,-282.834 151.214,-280.596 144.499,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.393,-280.621 144.238,-277.146 140.89,-280.457 144.386,-280.292 144.386,-280.292 144.386,-280.292 140.89,-280.457 144.533,-283.439 137.393,-280.621 137.393,-280.621\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"174.856\" y=\"-283.3\">a &amp; !b</text>\n",
227
228
229
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
230
231
232
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67.3561\" y=\"-192.3\">1</text>\n",
233
234
235
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
236
237
238
        "<path d=\"M111.365,-270.902C103.283,-257.33 91.2671,-237.152 81.832,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"78.2263,-215.254 84.5144,-219.656 80.0171,-218.261 81.808,-221.268 81.808,-221.268 81.808,-221.268 80.0171,-218.261 79.1015,-222.88 78.2263,-215.254 78.2263,-215.254\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102.856\" y=\"-239.8\">b</text>\n",
239
240
241
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
242
243
        "<ellipse cx=\"175.356\" cy=\"-196\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"175.356\" y=\"-192.3\">4</text>\n",
244
245
246
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
247
248
249
        "<path d=\"M129.438,-271.303C138.435,-256.746 152.298,-234.312 162.439,-217.902\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"166.26,-211.718 165.26,-219.329 164.42,-214.696 162.581,-217.673 162.581,-217.673 162.581,-217.673 164.42,-214.696 159.901,-216.017 166.26,-211.718 166.26,-211.718\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.856\" y=\"-239.8\">!a &amp; !b</text>\n",
250
251
252
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
253
254
255
        "<path d=\"M87.9369,-204.37C98.2008,-205.528 107.356,-202.738 107.356,-196 107.356,-190.946 102.206,-188.113 95.3012,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"87.9369,-187.63 94.8809,-184.358 91.4364,-187.569 94.9358,-187.508 94.9358,-187.508 94.9358,-187.508 91.4364,-187.569 94.9907,-190.657 87.9369,-187.63 87.9369,-187.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"123.356\" y=\"-192.3\">c &amp; d</text>\n",
256
257
258
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
259
260
        "<ellipse cx=\"68.3561\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-14.3\">2</text>\n",
261
262
263
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
264
265
266
        "<path d=\"M50.199,-181.727C34.8703,-168.686 13.4697,-147.255 4.35608,-123 -1.27155,-108.022 -1.54226,-101.873 4.35608,-87 13.1144,-64.9152 32.818,-45.8318 48.0656,-33.5506\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"53.866,-29.0284 50.2823,-35.8166 51.1058,-31.1804 48.3455,-33.3324 48.3455,-33.3324 48.3455,-33.3324 51.1058,-31.1804 46.4087,-30.8481 53.866,-29.0284 53.866,-29.0284\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.8561\" y=\"-101.3\">!c &amp; d</text>\n",
267
268
269
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
270
271
        "<ellipse cx=\"68.3561\" cy=\"-105\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-101.3\">3</text>\n",
272
273
274
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
275
276
277
        "<path d=\"M56.8135,-176.159C52.3073,-165.855 48.6383,-152.816 51.3561,-141 52.4094,-136.42 54.1455,-131.745 56.1156,-127.365\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"59.3394,-120.78 59.0906,-128.452 57.8004,-123.923 56.2615,-127.067 56.2615,-127.067 56.2615,-127.067 57.8004,-123.923 53.4323,-125.682 59.3394,-120.78 59.3394,-120.78\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"57.3561\" y=\"-144.8\">!d</text>\n",
278
279
280
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
281
282
283
        "<path d=\"M191.646,-204.016C201.745,-205.949 211.356,-203.277 211.356,-196 211.356,-190.542 205.95,-187.674 198.986,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"191.646,-187.984 198.373,-184.286 195.135,-187.705 198.624,-187.426 198.624,-187.426 198.624,-187.426 195.135,-187.705 198.875,-190.566 191.646,-187.984 191.646,-187.984\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"214.856\" y=\"-192.3\">1</text>\n",
284
285
286
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
287
288
289
        "<path d=\"M82.9697,-29.0929C91.4609,-35.4971 101.918,-44.3722 109.356,-54 128.603,-78.9113 134.158,-92.7751 125.356,-123 119.215,-144.088 103.068,-163.203 89.3663,-176.43\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"84.0682,-181.376 87.035,-174.297 86.6265,-178.988 89.1847,-176.599 89.1847,-176.599 89.1847,-176.599 86.6265,-178.988 91.3345,-178.901 84.0682,-181.376 84.0682,-181.376\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132.856\" y=\"-101.3\">c</text>\n",
290
291
292
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
293
294
295
        "<path d=\"M85.0201,-25.3828C94.9811,-27.0234 104.356,-24.5625 104.356,-18 104.356,-13.0781 99.0826,-10.4634 92.2436,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-10.6172 91.8051,-7.02727 88.513,-10.394 92.0059,-10.1709 92.0059,-10.1709 92.0059,-10.1709 88.513,-10.394 92.2067,-13.3145 85.0201,-10.6172 85.0201,-10.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109.856\" y=\"-14.3\">!c</text>\n",
296
297
298
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
299
300
301
        "<path d=\"M68.1643,-123.066C68.0258,-135.398 67.8354,-152.339 67.6743,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"67.5931,-173.908 64.522,-166.873 67.6324,-170.408 67.6718,-166.909 67.6718,-166.909 67.6718,-166.909 67.6324,-170.408 70.8216,-166.944 67.5931,-173.908 67.5931,-173.908\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"84.3561\" y=\"-144.8\">c &amp; d</text>\n",
302
303
304
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
305
306
307
        "<path d=\"M68.3561,-86.799C68.3561,-74.3561 68.3561,-57.3644 68.3561,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"68.3561,-36.1754 71.5062,-43.1754 68.3561,-39.6754 68.3562,-43.1754 68.3562,-43.1754 68.3562,-43.1754 68.3561,-39.6754 65.2062,-43.1755 68.3561,-36.1754 68.3561,-36.1754\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"86.8561\" y=\"-57.8\">!c &amp; d</text>\n",
308
309
310
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
311
312
313
        "<path d=\"M85.0201,-112.383C94.9811,-114.023 104.356,-111.562 104.356,-105 104.356,-100.078 99.0826,-97.4634 92.2436,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.0201,-97.6172 91.8051,-94.0273 88.513,-97.394 92.0059,-97.1709 92.0059,-97.1709 92.0059,-97.1709 88.513,-97.394 92.2067,-100.314 85.0201,-97.6172 85.0201,-97.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"110.356\" y=\"-101.3\">!d</text>\n",
314
315
316
317
318
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
319
        "<IPython.core.display.SVG object>"
320
321
322
       ]
      }
     ],
323
     "prompt_number": 3
324
    },
325
326
327
328
329
330
331
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "If you want to add some style options to the existing one, pass a dot to the `show()` function in addition to your own style options:"
     ]
    },
332
333
334
335
336
337
338
339
340
341
342
343
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.show(\".ast\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
344
       "prompt_number": 4,
345
       "svg": [
346
347
        "<svg height=\"342pt\" viewBox=\"0.00 0.00 427.00 342.00\" width=\"427pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 338)\">\n",
348
        "<title>G</title>\n",
349
350
351
352
        "<polygon fill=\"white\" points=\"-4,4 -4,-338 423,-338 423,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-319.8\">Inf(</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-319.8\">\u24ff</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-319.8\">)</text>\n",
353
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
354
        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
355
356
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
357
        "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
358
359
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
360
        "<polygon fill=\"none\" points=\"30,-23 30,-108 82,-108 82,-23 30,-23\" stroke=\"red\"/>\n",
361
362
363
364
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
365
366
        "<ellipse cx=\"56\" cy=\"-49\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-45.3\">0</text>\n",
367
368
369
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
370
371
        "<path d=\"M1.15491,-49C2.79388,-49 17.1543,-49 30.6317,-49\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9419,-49 30.9419,-52.1501 34.4419,-49 30.9419,-49.0001 30.9419,-49.0001 30.9419,-49.0001 34.4419,-49 30.9418,-45.8501 37.9419,-49 37.9419,-49\" stroke=\"black\"/>\n",
372
373
374
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
375
376
377
        "<path d=\"M49.6208,-66.0373C48.3189,-75.8579 50.4453,-85 56,-85 60.166,-85 62.4036,-79.8576 62.7128,-73.1433\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"62.3792,-66.0373 65.8541,-72.8818 62.5434,-69.5335 62.7076,-73.0296 62.7076,-73.0296 62.7076,-73.0296 62.5434,-69.5335 59.561,-73.1774 62.3792,-66.0373 62.3792,-66.0373\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-88.8\">a &amp; !b</text>\n",
378
379
380
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
381
382
        "<ellipse cx=\"169\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-189.3\">1</text>\n",
383
384
385
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
386
387
388
        "<path d=\"M67.6431,-62.8073C87.4829,-88.5454 130.165,-143.916 152.947,-173.472\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"157.226,-179.023 150.458,-175.402 155.089,-176.251 152.952,-173.479 152.952,-173.479 152.952,-173.479 155.089,-176.251 155.447,-171.556 157.226,-179.023 157.226,-179.023\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-150.8\">b</text>\n",
389
390
391
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
392
393
        "<ellipse cx=\"169\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
394
395
396
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
397
398
399
        "<path d=\"M73.8585,-46.7218C92.5211,-44.1998 122.756,-40.114 143.912,-37.2551\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"150.983,-36.2996 144.468,-40.3588 147.514,-36.7684 144.046,-37.2371 144.046,-37.2371 144.046,-37.2371 147.514,-36.7684 143.624,-34.1155 150.983,-36.2996 150.983,-36.2996\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-48.8\">!a &amp; !b</text>\n",
400
401
402
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
403
404
405
406
        "<path d=\"M160.021,-208.916C157.679,-219.15 160.672,-229 169,-229 175.376,-229 178.625,-223.226 178.746,-215.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-208.916 181.872,-215.532 178.36,-212.395 178.741,-215.874 178.741,-215.874 178.741,-215.874 178.36,-212.395 175.61,-216.217 177.979,-208.916 177.979,-208.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-247.8\">c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-232.8\">\u24ff</text>\n",
407
408
        "</g>\n",
        "<!-- 2 -->\n",
409
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
410
411
        "<ellipse cx=\"385\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"385\" y=\"-189.3\">2</text>\n",
412
413
414
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
415
416
417
418
        "<path d=\"M183.382,-181.807C199.601,-169.041 228.334,-148.914 257,-141 296.803,-130.011 340.921,-157.735 365.268,-176.79\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"371.017,-181.419 363.59,-179.483 368.291,-179.224 365.565,-177.029 365.565,-177.029 365.565,-177.029 368.291,-179.224 367.54,-174.576 371.017,-181.419 371.017,-181.419\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-159.8\">!c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-144.8\">\u24ff</text>\n",
419
        "</g>\n",
420
421
422
423
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
        "<ellipse cx=\"275.5\" cy=\"-244\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"275.5\" y=\"-240.3\">3</text>\n",
424
        "</g>\n",
425
426
427
428
429
430
        "<!-- 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",
431
432
433
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
434
435
436
        "<path d=\"M366.768,-193C328.813,-193 237.915,-193 194.238,-193\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"187.151,-193 194.151,-189.85 190.651,-193 194.151,-193 194.151,-193 194.151,-193 190.651,-193 194.151,-196.15 187.151,-193 187.151,-193\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-196.8\">c</text>\n",
437
438
439
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
440
441
442
        "<path d=\"M375.767,-208.541C373.169,-218.909 376.246,-229 385,-229 391.702,-229 395.077,-223.085 395.124,-215.659\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"394.233,-208.541 398.229,-215.095 394.668,-212.014 395.103,-215.487 395.103,-215.487 395.103,-215.487 394.668,-212.014 391.977,-215.879 394.233,-208.541 394.233,-208.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-232.8\">!c</text>\n",
443
        "</g>\n",
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
        "<!-- 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",
462
463
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
464
465
466
        "<path d=\"M160.021,-49.916C157.679,-60.1504 160.672,-70 169,-70 175.376,-70 178.625,-64.2263 178.746,-56.9268\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-49.916 181.872,-56.5315 178.36,-53.3952 178.741,-56.8744 178.741,-56.8744 178.741,-56.8744 178.36,-53.3952 175.61,-57.2174 177.979,-49.916 177.979,-49.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
467
468
469
470
471
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
472
        "<IPython.core.display.SVG object>"
473
474
475
       ]
      }
     ],
476
     "prompt_number": 4
477
    },
478
479
480
481
482
483
484
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `translate()` function can also be called with a formula object.  Either as a function, or as a method."
     ]
    },
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U b'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$a \\mathbin{\\mathsf{U}} b$"
       ],
       "metadata": {},
       "output_type": "pyout",
500
       "prompt_number": 5,
501
502
503
504
505
       "text": [
        "a U b"
       ]
      }
     ],
506
     "prompt_number": 5
507
508
509
510
511
512
513
514
515
516
517
518
519
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate(f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
520
       "prompt_number": 6,
521
522
523
524
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
525
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
526
527
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
528
529
530
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
531
        "<title>G</title>\n",
532
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
533
534
535
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
536
537
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
538
539
540
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
541
542
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
543
544
545
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
546
547
548
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
549
550
551
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
552
553
554
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
555
556
557
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
558
559
560
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
561
562
563
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
564
565
566
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
567
568
569
570
571
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
572
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b810> >"
573
574
575
       ]
      }
     ],
576
     "prompt_number": 6
577
578
579
580
581
582
583
584
585
586
587
588
589
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
590
       "prompt_number": 7,
591
592
593
594
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
595
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
596
597
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
598
599
600
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
601
        "<title>G</title>\n",
602
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
603
604
605
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
606
607
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
608
609
610
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
611
612
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
613
614
615
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
616
617
618
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
619
620
621
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
622
623
624
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
625
626
627
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
628
629
630
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
631
632
633
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
634
635
636
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
637
638
639
640
641
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
642
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b690> >"
643
644
645
       ]
      }
     ],
646
     "prompt_number": 7
647
    },
648
649
650
651
652
653
654
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "When used as a method, all the arguments are translation options.  Here is a monitor:"
     ]
    },
655
656
657
658
659
660
661
662
663
664
665
666
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate('mon')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
667
       "prompt_number": 8,
668
669
670
671
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
672
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
673
674
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
675
676
677
        "<svg width=\"163pt\" height=\"77pt\"\n",
        " viewBox=\"0.00 0.00 163.00 77.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 73)\">\n",
678
        "<title>G</title>\n",
679
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
680
681
682
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
683
684
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
685
686
687
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
688
689
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\n",
690
691
692
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
693
694
695
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
696
697
698
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
699
700
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
701
702
703
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
704
705
706
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-18C85.1153,-18 99.5214,-18 111.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-18 111.892,-21.1501 115.392,-18 111.892,-18.0001 111.892,-18.0001 111.892,-18.0001 115.392,-18 111.892,-14.8501 118.892,-18 118.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
707
708
709
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
710
711
712
        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
713
714
715
716
717
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
718
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b6f0> >"
719
720
721
       ]
      }
     ],
722
     "prompt_number": 8
723
    },
724
725
726
727
728
729
730
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`."
     ]
    },
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('Ga | Gb | Gc'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
       ],
       "metadata": {},
       "output_type": "pyout",
746
       "prompt_number": 9,
747
748
749
750
751
       "text": [
        "Ga | Gb | Gc"
       ]
      }
     ],
752
     "prompt_number": 9
753
754
755
756
757
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
758
      "f.translate('ba', 'small').show('v')"
759
760
761
762
763
764
765
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
766
       "prompt_number": 10,
767
       "svg": [
768
        "<svg height=\"177pt\" viewBox=\"0.00 0.00 251.00 177.00\" width=\"251pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
769
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
770
        "<title>G</title>\n",
771
        "<polygon fill=\"white\" points=\"-4,4 -4,-173 247,-173 247,4 -4,4\" stroke=\"none\"/>\n",
772
773
774
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
775
776
        "<ellipse cx=\"109\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-109.3\">0</text>\n",
777
778
779
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
780
781
        "<path d=\"M109,-167.845C109,-166.206 109,-151.846 109,-138.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"109,-131.058 112.15,-138.058 109,-134.558 109,-138.058 109,-138.058 109,-138.058 109,-134.558 105.85,-138.058 109,-131.058 109,-131.058\" stroke=\"black\"/>\n",
782
783
784
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
785
786
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22\" y=\"-18.3\">1</text>\n",
788
789
790
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
791
792
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"77.5\" y=\"-65.8\">a</text>\n",
794
795
796
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
797
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-18.3\">2</text>\n",
800
801
802
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
803
804
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"112.5\" y=\"-65.8\">b</text>\n",
806
807
808
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
809
810
811
        "<ellipse cx=\"196\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"196\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196\" y=\"-18.3\">3</text>\n",
812
813
814
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
815
816
817
        "<path d=\"M121.097,-99.6249C135.314,-85.081 159.114,-60.7342 176.069,-43.3887\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"181.094,-38.2491 178.453,-45.4567 178.647,-40.7519 176.2,-43.2548 176.2,-43.2548 176.2,-43.2548 178.647,-40.7519 173.948,-41.0528 181.094,-38.2491 181.094,-38.2491\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"160.5\" y=\"-65.8\">c</text>\n",
818
819
820
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
821
822
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"65.5\" y=\"-18.3\">a</text>\n",
824
825
826
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
827
828
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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"152.5\" y=\"-18.3\">b</text>\n",
830
831
832
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
833
834
835
        "<path d=\"M216.581,-30.3702C226.845,-31.5284 236,-28.7383 236,-22 236,-16.9463 230.85,-14.1134 223.945,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"216.581,-13.6298 223.525,-10.3582 220.08,-13.5688 223.58,-13.5077 223.58,-13.5077 223.58,-13.5077 220.08,-13.5688 223.635,-16.6573 216.581,-13.6298 216.581,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"239.5\" y=\"-18.3\">c</text>\n",
836
837
838
839
840
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
841
        "<IPython.core.display.SVG object>"
842
843
844
       ]
      }
     ],
845
     "prompt_number": 10
846
847
848
849
850
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
851
      "f.translate('ba', 'det').show('v.')"
852
853
854
855
856
857
858
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
859
       "prompt_number": 11,
860
       "svg": [
861
862
        "<svg height=\"280pt\" viewBox=\"0.00 0.00 596.88 280.00\" width=\"597pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 276)\">\n",
863
        "<title>G</title>\n",
864
        "<polygon fill=\"white\" points=\"-4,4 -4,-276 592.883,-276 592.883,4 -4,4\" stroke=\"none\"/>\n",
865
866
867
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node2\"><title>6</title>\n",
868
869
870
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"279.883\" y=\"-208.3\">6</text>\n",
871
872
873
        "</g>\n",
        "<!-- I&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
874
875
        "<path d=\"M279.883,-270.834C279.883,-269.159 279.883,-255.116 279.883,-241.289\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"279.883,-234.144 283.033,-241.144 279.883,-237.644 279.883,-241.144 279.883,-241.144 279.883,-241.144 279.883,-237.644 276.733,-241.145 279.883,-234.144 279.883,-234.144\" stroke=\"black\"/>\n",
876
877
878
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
879
880
881
        "<path d=\"M300.874,-219.317C310.971,-220.22 319.883,-217.781 319.883,-212 319.883,-207.664 314.87,-205.208 308.104,-204.632\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"300.874,-204.683 307.852,-201.484 304.374,-204.658 307.874,-204.634 307.874,-204.634 307.874,-204.634 304.374,-204.658 307.896,-207.784 300.874,-204.683 300.874,-204.683\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"319.883\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
882
883
884
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
885
886
887
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.8834\" y=\"-18.3\">0</text>\n",
888
889
890
        "</g>\n",
        "<!-- 6&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
891
892
893
        "<path d=\"M258.05,-208.601C199.066,-201.628 38.871,-179.258 7.88337,-139 -20.5572,-102.052 37.5535,-58.9513 73.4411,-37.1624\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"79.8576,-33.3483 75.45,-39.6328 76.849,-35.1367 73.8404,-36.9251 73.8404,-36.9251 73.8404,-36.9251 76.849,-35.1367 72.2309,-34.2174 79.8576,-33.3483 79.8576,-33.3483\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"7.88337\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
894
895
896
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
897
898
899
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.883\" y=\"-113.3\">1</text>\n",
900
901
902
        "</g>\n",
        "<!-- 6&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
903
904
905
        "<path d=\"M258.548,-205.147C236.734,-198.695 202.263,-187.184 174.883,-172 157.384,-162.295 139.553,-148.469 126.267,-137.237\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.866,-132.602 128.229,-134.77 123.522,-134.881 126.178,-137.161 126.178,-137.161 126.178,-137.161 123.522,-134.881 124.126,-139.551 120.866,-132.602 120.866,-132.602\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.883\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
906
907
908
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
909
910
911
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326.883\" y=\"-18.3\">2</text>\n",
912
913
914
        "</g>\n",
        "<!-- 6&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
915
916
917
        "<path d=\"M295.807,-196.555C302.236,-189.767 309.034,-181.157 312.883,-172 329.476,-132.531 330.508,-82.1352 329.137,-51.2346\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"328.768,-44.1943 332.28,-51.0197 328.951,-47.6895 329.135,-51.1847 329.135,-51.1847 329.135,-51.1847 328.951,-47.6895 325.989,-51.3498 328.768,-44.1943 328.768,-44.1943\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"327.883\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
918
919
920
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
921
922
923
        "<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",
924
925
926
        "</g>\n",
        "<!-- 6&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
927
928
929
        "<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",
930
931
        "</g>\n",
        "<!-- 5 -->\n",
932
        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
933
934
935
        "<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",
936
937
938
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
939
940
941
        "<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",
942
943
944
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node8\"><title>4</title>\n",
945
946
947
        "<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",
948
949
950
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
951
952
953
        "<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",
954
955
956
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
957
958
959
        "<path d=\"M119.464,-30.3702C129.728,-31.5284 138.883,-28.7383 138.883,-22 138.883,-16.9463 133.734,-14.1134 126.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"119.464,-13.6298 126.408,-10.3582 122.964,-13.5688 126.463,-13.5077 126.463,-13.5077 126.463,-13.5077 122.964,-13.5688 126.518,-16.6573 119.464,-13.6298 119.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.883\" y=\"-18.3\">c</text>\n",
960
961
962
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
963
964
965
        "<path d=\"M101.764,-94.9925C101.016,-89.1774 100.312,-82.8549 99.8834,-77 99.2697,-68.6098 98.9633,-59.468 98.8243,-51.1319\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"98.7416,-44.0528 101.973,-51.0155 98.7825,-47.5526 98.8234,-51.0524 98.8234,-51.0524 98.8234,-51.0524 98.7825,-47.5526 95.6736,-51.0892 98.7416,-44.0528 98.7416,-44.0528\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.8834\" y=\"-65.8\">!b &amp; c</text>\n",
966
967
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
968
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
969
970
971
        "<path d=\"M125.464,-125.37C135.728,-126.528 144.883,-123.738 144.883,-117 144.883,-111.946 139.734,-109.113 132.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"125.464,-108.63 132.408,-105.358 128.964,-108.569 132.463,-108.508 132.463,-108.508 132.463,-108.508 128.964,-108.569 132.518,-111.657 125.464,-108.63 125.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"144.883\" y=\"-113.3\">b &amp; c</text>\n",
972
        "</g>\n",
973
974
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
975
976
977
        "<path d=\"M118.615,-99.4594C130.558,-85.4667 147.262,-66.9259 155.883,-62 201.053,-36.1916 262.094,-27.4608 297.704,-24.508\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"304.902,-23.9616 298.16,-27.6325 301.412,-24.2266 297.922,-24.4916 297.922,-24.4916 297.922,-24.4916 301.412,-24.2266 297.683,-21.3506 304.902,-23.9616 304.902,-23.9616\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.883\" y=\"-65.8\">b &amp; !c</text>\n",
978
        "</g>\n",
979
980
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
981
982
983
        "<path d=\"M347.464,-30.3702C357.728,-31.5284 366.883,-28.7383 366.883,-22 366.883,-16.9463 361.734,-14.1134 354.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"347.464,-13.6298 354.408,-10.3582 350.964,-13.5688 354.463,-13.5077 354.463,-13.5077 354.463,-13.5077 350.964,-13.5688 354.518,-16.6573 347.464,-13.6298 347.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.883\" y=\"-18.3\">b</text>\n",
984
        "</g>\n",
985
986
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
987
988
989
        "<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",
990
991
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
992
        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
993
994
995
        "<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",
996
        "</g>\n",
997
998
        "<!-- 3&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;5</title>\n",
999
1000
1001
        "<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",
1002
1003
1004
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
1005
1006
1007
        "<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",
1008
1009
1010
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
1011
1012
1013
        "<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",
1014
1015
1016
        "</g>\n",
        "<!-- 4&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>4-&gt;5</title>\n",
1017
1018
1019
        "<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",
1020
1021
1022
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;4</title>\n",
1023
1024
1025
        "<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",
1026
1027
1028
1029
1030
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
1031
        "<IPython.core.display.SVG object>"
1032
1033
1034
1035
1036
       ]
      }
     ],
     "prompt_number": 11
    },
1037
1038
1039
1040
1041
1042
1043
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Here is how to build an unambiguous automaton:"
     ]
    },
1044
1045
1046
1047
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
1048
      "spot.translate('GFa -> GFb', 'unambig')"
1049
1050
1051
1052
1053
1054
1055
1056
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
        "<svg width=\"302pt\" height=\"295pt\"\n",
        " viewBox=\"0.00 0.00 301.50 295.16\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 291.16)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-291.16 297.5,-291.16 297.5,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-107.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-103.46\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-107.16C2.79388,-107.16 17.1543,-107.16 30.6317,-107.16\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-107.16 30.9419,-110.31 34.4419,-107.16 30.9419,-107.16 30.9419,-107.16 30.9419,-107.16 34.4419,-107.16 30.9418,-104.01 37.9419,-107.16 37.9419,-107.16\"/>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-188.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-184.46\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M66.5112,-121.807C72.9549,-130.98 82.0794,-142.636 92,-151.16 104.757,-162.122 121.236,-171.509 134.344,-178.086\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"140.854,-181.263 133.181,-181.024 137.708,-179.728 134.563,-178.193 134.563,-178.193 134.563,-178.193 137.708,-179.728 135.944,-175.362 140.854,-181.263 140.854,-181.263\"/>\n",
        "<text text-anchor=\"middle\" x=\"105.5\" y=\"-172.96\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-127.16\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-123.46\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1079,-109.003C100.327,-111.801 152.035,-117.211 196,-121.16 213.175,-122.703 232.554,-124.23 247.444,-125.357\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"254.786,-125.908 247.57,-128.525 251.296,-125.646 247.806,-125.384 247.806,-125.384 247.806,-125.384 251.296,-125.646 248.042,-122.243 254.786,-125.908 254.786,-125.908\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-122.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-50.1603\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-46.4603\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M72.1119,-98.5032C89.0117,-88.8219 116.498,-73.076 135.486,-62.1985\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"141.572,-58.7121 137.064,-64.925 138.535,-60.4519 135.498,-62.1917 135.498,-62.1917 135.498,-62.1917 138.535,-60.4519 133.932,-59.4584 141.572,-58.7121 141.572,-58.7121\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-89.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-31.1603\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-27.4603\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M64.2827,-91.086C75.861,-67.75 100.908,-25.398 137,-8.1603 173.984,9.50377 222.376,-7.05194 250.041,-19.7503\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.608,-22.8724 248.934,-22.7117 253.447,-21.3696 250.286,-19.8668 250.286,-19.8668 250.286,-19.8668 253.447,-21.3696 251.639,-17.0219 256.608,-22.8724 256.608,-22.8724\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-11.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M152.858,-205.57C151.992,-215.248 153.539,-224.16 157.5,-224.16 160.409,-224.16 162.016,-219.354 162.321,-212.968\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"162.142,-205.57 165.461,-212.492 162.227,-209.069 162.312,-212.568 162.312,-212.568 162.312,-212.568 162.227,-209.069 159.163,-212.645 162.142,-205.57 162.142,-205.57\"/>\n",
        "<text text-anchor=\"start\" x=\"153\" y=\"-242.96\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"149.5\" y=\"-227.96\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M150.502,-204.756C145.214,-226.024 147.547,-254.16 157.5,-254.16 166.403,-254.16 169.209,-231.646 165.917,-211.673\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"164.498,-204.756 168.991,-210.981 165.202,-208.185 165.905,-211.613 165.905,-211.613 165.905,-211.613 165.202,-208.185 162.819,-212.246 164.498,-204.756 164.498,-204.756\"/>\n",
        "<text text-anchor=\"start\" x=\"151\" y=\"-257.96\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-142.702C260.73,-153.069 263.922,-163.16 273,-163.16 279.95,-163.16 283.45,-157.245 283.499,-149.819\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-142.702 286.6,-149.237 283.026,-146.173 283.477,-149.643 283.477,-149.643 283.477,-149.643 283.026,-146.173 280.353,-150.049 282.575,-142.702 282.575,-142.702\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-181.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "<text text-anchor=\"start\" x=\"265\" y=\"-166.96\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M172.875,-59.9124C192.831,-73.4509 229.029,-98.0082 251.724,-113.405\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"257.742,-117.487 250.181,-116.164 254.845,-115.522 251.949,-113.557 251.949,-113.557 251.949,-113.557 254.845,-115.522 253.718,-110.951 257.742,-117.487 257.742,-117.487\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-105.96\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M148.521,-66.0763C146.179,-76.3107 149.172,-86.1603 157.5,-86.1603 163.876,-86.1603 167.125,-80.3866 167.246,-73.0871\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"166.479,-66.0763 170.372,-72.6918 166.86,-69.5555 167.241,-73.0347 167.241,-73.0347 167.241,-73.0347 166.86,-69.5555 164.11,-73.3777 166.479,-66.0763 166.479,-66.0763\"/>\n",
        "<text text-anchor=\"start\" x=\"144\" y=\"-89.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M175.601,-51.3981C191.679,-52.1201 216.301,-52.083 237,-47.1603 241.436,-46.1053 245.995,-44.4755 250.295,-42.6526\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.785,-39.6836 251.73,-45.4601 253.602,-41.1396 250.42,-42.5956 250.42,-42.5956 250.42,-42.5956 253.602,-41.1396 249.109,-39.7311 256.785,-39.6836 256.785,-39.6836\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-54.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M255.068,-27.6221C239.446,-25.0259 215.751,-22.7942 196,-28.1603 189.927,-29.8102 183.832,-32.719 178.374,-35.8916\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"172.298,-39.6776 176.573,-33.3021 175.268,-37.8266 178.239,-35.9756 178.239,-35.9756 178.239,-35.9756 175.268,-37.8266 179.905,-38.649 172.298,-39.6776 172.298,-39.6776\"/>\n",
        "<text text-anchor=\"start\" x=\"203\" y=\"-31.9603\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-46.7018C260.73,-57.069 263.922,-67.1603 273,-67.1603 279.95,-67.1603 283.45,-61.245 283.499,-53.8194\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-46.7018 286.6,-53.2374 283.026,-50.1726 283.477,-53.6434 283.477,-53.6434 283.477,-53.6434 283.026,-50.1726 280.353,-54.0493 282.575,-46.7018 282.575,-46.7018\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-70.9603\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1178
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515be10> >"
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
       ]
      }
     ],
     "prompt_number": 12
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Compare with the standard translation:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate('GFa -> GFb')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 13,
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
        "<svg width=\"165pt\" height=\"227pt\"\n",
        " viewBox=\"0.00 0.00 165.00 227.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 223)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-223 161,-223 161,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-97\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-93.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-97C2.79388,-97 17.1543,-97 30.6317,-97\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-97 30.9419,-100.15 34.4419,-97 30.9419,-97.0001 30.9419,-97.0001 30.9419,-97.0001 34.4419,-97 30.9418,-93.8501 37.9419,-97 37.9419,-97\"/>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-114.037C48.3189,-123.858 50.4453,-133 56,-133 60.166,-133 62.4036,-127.858 62.7128,-121.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-114.037 65.8541,-120.882 62.5434,-117.533 62.7076,-121.03 62.7076,-121.03 62.7076,-121.03 62.5434,-117.533 59.561,-121.177 62.3792,-114.037 62.3792,-114.037\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"139\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M71.4812,-107.012C84.3818,-115.931 103.39,-129.072 117.788,-139.026\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"123.644,-143.075 116.095,-141.685 120.765,-141.085 117.886,-139.094 117.886,-139.094 117.886,-139.094 120.765,-141.085 119.678,-136.503 123.644,-143.075 123.644,-143.075\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"139\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M69.6562,-84.6562C83.209,-71.4381 104.825,-50.3563 120.113,-35.4454\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"125.433,-30.2571 122.621,-37.3997 122.927,-32.7008 120.421,-35.1446 120.421,-35.1446 120.421,-35.1446 122.927,-32.7008 118.222,-32.8895 125.433,-30.2571 125.433,-30.2571\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M131.969,-169.664C130.406,-179.625 132.75,-189 139,-189 143.688,-189 146.178,-183.727 146.471,-176.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"146.031,-169.664 149.601,-176.46 146.244,-173.158 146.456,-176.651 146.456,-176.651 146.456,-176.651 146.244,-173.158 143.312,-176.842 146.031,-169.664 146.031,-169.664\"/>\n",
        "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"131\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M135.405,-35.7817C134.794,-45.3149 135.992,-54 139,-54 141.209,-54 142.442,-49.3161 142.699,-43.0521\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"142.595,-35.7817 145.845,-42.736 142.645,-39.2814 142.695,-42.781 142.695,-42.781 142.695,-42.781 142.645,-39.2814 139.546,-42.8261 142.595,-35.7817 142.595,-35.7817\"/>\n",
        "<text text-anchor=\"start\" x=\"134.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"131\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M133.494,-35.249C129.587,-56.4346 131.422,-84 139,-84 145.749,-84 147.943,-62.1347 145.582,-42.3851\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.506,-35.249 148.665,-41.7011 145.028,-38.7099 145.55,-42.1708 145.55,-42.1708 145.55,-42.1708 145.028,-38.7099 142.435,-42.6405 144.506,-35.249 144.506,-35.249\"/>\n",
        "<text text-anchor=\"start\" x=\"132.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1279
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515bed0> >"
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
       ]
      }
     ],
     "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",
        "<svg width=\"258pt\" height=\"180pt\"\n",
        " viewBox=\"0.00 0.00 258.00 180.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 176)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-176 254,-176 254,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=\"-76\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-76C2.79388,-76 17.1543,-76 30.6317,-76\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-76 30.9419,-79.1501 34.4419,-76 30.9419,-76.0001 30.9419,-76.0001 30.9419,-76.0001 34.4419,-76 30.9418,-72.8501 37.9419,-76 37.9419,-76\"/>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-93.0373C48.3189,-102.858 50.4453,-112 56,-112 60.166,-112 62.4036,-106.858 62.7128,-100.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-93.0373 65.8541,-99.8818 62.5434,-96.5335 62.7076,-100.03 62.7076,-100.03 62.7076,-100.03 62.5434,-96.5335 59.561,-100.177 62.3792,-93.0373 62.3792,-93.0373\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"143\" cy=\"-117\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"143\" cy=\"-117\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"143\" y=\"-113.3\" 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=\"M72.5903,-83.52C84.8926,-89.4541 102.305,-97.8532 116.612,-104.754\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"122.938,-107.805 115.264,-107.601 119.785,-106.285 116.633,-104.764 116.633,-104.764 116.633,-104.764 119.785,-106.285 118.001,-101.927 122.938,-107.805 122.938,-107.805\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-100.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=\"143\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"143\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\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",
        "<path fill=\"none\" stroke=\"black\" d=\"M71.8059,-66.5939C84.5413,-58.5032 103.153,-46.6792 118.012,-37.2391\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"124.123,-33.3572 119.904,-39.7697 121.169,-35.234 118.214,-37.1109 118.214,-37.1109 118.214,-37.1109 121.169,-35.234 116.525,-34.452 124.123,-33.3572 124.123,-33.3572\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M134.994,-137.581C133.886,-147.845 136.555,-157 143,-157 147.834,-157 150.544,-151.85 151.129,-144.945\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.006,-137.581 154.273,-144.527 151.065,-141.08 151.123,-144.58 151.123,-144.58 151.123,-144.58 151.065,-141.08 147.973,-144.632 151.006,-137.581 151.006,-137.581\"/>\n",
        "<text text-anchor=\"start\" x=\"137.5\" y=\"-160.8\" font-family=\"Lato\" font-size=\"14.00\">!a</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=\"M134.994,-42.5808C133.886,-52.8447 136.555,-62 143,-62 147.834,-62 150.544,-56.8502 151.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.006,-42.5808 154.273,-49.5273 151.065,-46.0803 151.123,-49.5798 151.123,-49.5798 151.123,-49.5798 151.065,-46.0803 147.973,-49.6324 151.006,-42.5808 151.006,-42.5808\"/>\n",
        "<text text-anchor=\"start\" x=\"138.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"232\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"232\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M165.06,-22C177.588,-22 193.534,-22 206.607,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"213.925,-22 206.925,-25.1501 210.425,-22 206.925,-22.0001 206.925,-22.0001 206.925,-22.0001 210.425,-22 206.925,-18.8501 213.925,-22 213.925,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"183\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M216.689,-12.1343C210.598,-8.50652 203.237,-4.83778 196,-3 186.646,-0.624833 176.631,-3.03558 167.911,-6.84342\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"161.529,-9.97151 166.428,-4.06232 164.671,-8.4312 167.814,-6.8909 167.814,-6.8909 167.814,-6.8909 164.671,-8.4312 169.201,-9.71947 161.529,-9.97151 161.529,-9.97151\"/>\n",
        "<text text-anchor=\"start\" x=\"185\" y=\"-6.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M224.617,-38.6641C222.977,-48.625 225.438,-58 232,-58 236.922,-58 239.537,-52.7266 239.844,-45.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"239.383,-38.6641 242.973,-45.449 239.606,-42.1569 239.829,-45.6498 239.829,-45.6498 239.829,-45.6498 239.606,-42.1569 236.686,-45.8507 239.383,-38.6641 239.383,-38.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"225.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1397
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3c2515b630> >"
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
       ]
      }
     ],
     "prompt_number": 14
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Some example of running the self-loopization algorithm on an automaton:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = spot.translate('F(a & X(!a &Xb))', \"any\"); a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 15,
1423
1424
1425
1426
       "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",
1427
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
1428
1429
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
1430
1431
        "<svg width=\"325pt\" height=\"92pt\"\n",
        " viewBox=\"0.00 0.00 325.00 92.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
1432
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 88)\">\n",
1433
        "<title>G</title>\n",
1434
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-88 321,-88 321,4 -4,4\"/>\n",
1435
1436
1437
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1438
1439
        "<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\">0</text>\n",
1440
1441
1442
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1443
1444
        "<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",
1445
1446
1447
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
1448
1449
1450
        "<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=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1451
1452
1453
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1454
1455
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"130.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1456
1457
1458
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1459
1460
1461
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0888,-18C84.5562,-18 98.1196,-18 109.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"116.959,-18 109.959,-21.1501 113.459,-18 109.959,-18.0001 109.959,-18.0001 109.959,-18.0001 113.459,-18 109.959,-14.8501 116.959,-18 116.959,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
1462
1463
1464
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
1465
1466
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1467
1468
1469
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
1470
1471
1472
        "<path fill=\"none\" stroke=\"black\" d=\"M153.178,-18C164.669,-18 179.959,-18 192.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"199.847,-18 192.847,-21.1501 196.347,-18 192.847,-18.0001 192.847,-18.0001 192.847,-18.0001 196.347,-18 192.847,-14.8501 199.847,-18 199.847,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"171\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1473
1474
1475
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1476
1477
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"299\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"299\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1478
1479
1480
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1481
1482
1483
        "<path fill=\"none\" stroke=\"black\" d=\"M236.142,-18C247.115,-18 261.521,-18 273.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"280.892,-18 273.892,-21.1501 277.392,-18 273.892,-18.0001 273.892,-18.0001 273.892,-18.0001 277.392,-18 273.892,-14.8501 280.892,-18 280.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
Alexandre Duret-Lutz's avatar