automata.ipynb 272 KB
Newer Older
1
2
{
 "metadata": {
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
18
   "version": "3.5.4"
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=\"202pt\"\n",
        " viewBox=\"0.00 0.00 419.00 202.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 198)\">\n",
70
        "<title>G</title>\n",
71
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-198 415,-198 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=\"283.5\" cy=\"-143\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"283.5\" y=\"-139.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=\"M188.416,-124.722C195.199,-131.009 203.812,-137.563 213,-141 227.404,-146.388 244.685,-146.908 258.412,-146.072\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"265.631,-145.49 258.907,-149.192 262.143,-145.771 258.654,-146.052 258.654,-146.052 258.654,-146.052 262.143,-145.771 258.401,-142.912 265.631,-145.49 265.631,-145.49\"/>\n",
        "<text text-anchor=\"start\" x=\"223.5\" y=\"-149.8\" font-family=\"Lato\" font-size=\"14.00\">!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=\"393\" cy=\"-92\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"393\" y=\"-88.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=\"M194.955,-107.056C213.394,-105.37 240.969,-102.908 265,-101 300.698,-98.1662 342.076,-95.3147 367.648,-93.6028\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"374.738,-93.1303 367.963,-96.7389 371.246,-93.363 367.753,-93.5958 367.753,-93.5958 367.753,-93.5958 371.246,-93.363 367.544,-90.4528 374.738,-93.1303 374.738,-93.1303\"/>\n",
        "<text text-anchor=\"start\" x=\"265\" y=\"-104.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; 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=\"M268.237,-132.973C261.978,-129.002 254.385,-124.739 247,-122 232.611,-116.663 215.792,-113.477 201.927,-111.597\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"194.974,-110.728 202.311,-108.47 198.447,-111.162 201.92,-111.596 201.92,-111.596 201.92,-111.596 198.447,-111.162 201.53,-114.722 194.974,-110.728 194.974,-110.728\"/>\n",
        "<text text-anchor=\"start\" x=\"213\" y=\"-125.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</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=\"M274.521,-158.916C272.179,-169.15 275.172,-179 283.5,-179 289.876,-179 293.125,-173.226 293.246,-165.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"292.479,-158.916 296.372,-165.532 292.86,-162.395 293.241,-165.874 293.241,-165.874 293.241,-165.874 292.86,-162.395 290.11,-166.217 292.479,-158.916 292.479,-158.916\"/>\n",
        "<text text-anchor=\"start\" x=\"277\" y=\"-182.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
157
        "</g>\n",
158
159
160
161
162
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M300.362,-135.475C318.807,-126.724 349.364,-112.227 370.073,-102.403\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"376.422,-99.3903 371.448,-105.237 373.26,-100.891 370.098,-102.391 370.098,-102.391 370.098,-102.391 373.26,-100.891 368.748,-99.5448 376.422,-99.3903 376.422,-99.3903\"/>\n",
        "<text text-anchor=\"start\" x=\"320\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
163
        "</g>\n",
164
165
166
167
168
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M375.482,-87.5706C351.175,-81.6713 304.39,-72.6745 265,-79 242.525,-82.6091 218.077,-90.9312 200.187,-97.8967\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"193.429,-100.585 198.769,-95.0706 196.681,-99.2911 199.933,-97.9975 199.933,-97.9975 199.933,-97.9975 196.681,-99.2911 201.098,-100.924 193.429,-100.585 193.429,-100.585\"/>\n",
        "<text text-anchor=\"start\" x=\"280\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">c</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=\"M383.767,-107.541C381.169,-117.909 384.246,-128 393,-128 399.702,-128 403.077,-122.085 403.124,-114.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"402.233,-107.541 406.229,-114.095 402.668,-111.014 403.103,-114.487 403.103,-114.487 403.103,-114.487 402.668,-111.014 399.977,-114.879 402.233,-107.541 402.233,-107.541\"/>\n",
        "<text text-anchor=\"start\" x=\"387.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">!c</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 0x7f23c1786450> >"
181
182
183
       ]
      }
     ],
184
     "prompt_number": 2
185
    },
186
187
188
189
190
191
192
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The call the `spot.setup()` in the first cells has installed a default style for the graphviz output.  If you want to change this style temporarily, you can call the `show(style)` method explicitely.  For instance here is a vertical layout with the default font of GraphViz."
     ]
    },
193
194
195
196
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
197
      "a.show(\"v\")"
198
199
200
201
202
203
204
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
205
       "prompt_number": 3,
206
       "svg": [
207
        "<svg height=\"351pt\" viewBox=\"0.00 0.00 237.00 351.00\" width=\"237pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
208
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 347)\">\n",
209
        "<title>G</title>\n",
210
        "<polygon fill=\"white\" points=\"-4,4 -4,-347 233,-347 233,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=\"131\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"131\" 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=\"M131,-341.845C131,-340.206 131,-325.846 131,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"131,-305.058 134.15,-312.058 131,-308.558 131,-312.058 131,-312.058 131,-312.058 131,-308.558 127.85,-312.058 131,-305.058 131,-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=\"M148.037,-293.379C157.858,-294.681 167,-292.555 167,-287 167,-282.834 161.858,-280.596 155.143,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"148.037,-280.621 154.882,-277.146 151.533,-280.457 155.03,-280.292 155.03,-280.292 155.03,-280.292 151.533,-280.457 155.177,-283.439 148.037,-280.621 148.037,-280.621\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"185.5\" 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=\"78\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"78\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"78\" 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=\"M122.009,-270.902C113.927,-257.33 101.911,-237.152 92.4759,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"88.8703,-215.254 95.1583,-219.656 90.6611,-218.261 92.4519,-221.268 92.4519,-221.268 92.4519,-221.268 90.6611,-218.261 89.7454,-222.88 88.8703,-215.254 88.8703,-215.254\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"113.5\" 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=\"186\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"186\" 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=\"M140.082,-271.303C149.079,-256.746 162.942,-234.312 173.083,-217.902\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"176.904,-211.718 175.904,-219.329 175.064,-214.696 173.224,-217.673 173.224,-217.673 173.224,-217.673 175.064,-214.696 170.545,-216.017 176.904,-211.718 176.904,-211.718\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"181.5\" 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=\"M98.5808,-204.37C108.845,-205.528 118,-202.738 118,-196 118,-190.946 112.85,-188.113 105.945,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"98.5808,-187.63 105.525,-184.358 102.08,-187.569 105.58,-187.508 105.58,-187.508 105.58,-187.508 102.08,-187.569 105.635,-190.657 98.5808,-187.63 98.5808,-187.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"134\" 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=\"18\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-101.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=\"M57.5964,-187.099C44.382,-180.81 28.1659,-170.619 20,-156 15.6311,-148.178 14.4575,-138.545 14.6139,-129.828\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"15.017,-122.782 17.7619,-129.95 14.8171,-126.276 14.6171,-129.77 14.6171,-129.77 14.6171,-129.77 14.8171,-126.276 11.4722,-129.59 15.017,-122.782 15.017,-122.782\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"26\" y=\"-144.8\">!d</text>\n",
267
268
269
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
270
271
        "<ellipse cx=\"102\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102\" y=\"-14.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=\"M83.8727,-174.481C85.4014,-168.556 86.9204,-162.056 88,-156 94.9806,-116.843 98.8007,-70.7236 100.62,-43.2262\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"101.081,-35.9857 103.78,-43.1718 100.859,-39.4786 100.636,-42.9715 100.636,-42.9715 100.636,-42.9715 100.859,-39.4786 97.4927,-42.7713 101.081,-35.9857 101.081,-35.9857\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"116.5\" y=\"-101.3\">!c &amp; 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=\"M202.29,-204.016C212.389,-205.949 222,-203.277 222,-196 222,-190.542 216.594,-187.674 209.63,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"202.29,-187.984 209.017,-184.286 205.779,-187.705 209.268,-187.426 209.268,-187.426 209.268,-187.426 205.779,-187.705 209.519,-190.566 202.29,-187.984 202.29,-187.984\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"225.5\" 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=\"M27.6536,-120.319C36.9047,-134.042 51.0376,-155.006 61.9772,-171.233\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"66.1459,-177.416 59.621,-173.373 64.1894,-174.514 62.2329,-171.612 62.2329,-171.612 62.2329,-171.612 64.1894,-174.514 64.8448,-169.851 66.1459,-177.416 66.1459,-177.416\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68\" y=\"-144.8\">c &amp; d</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=\"M34.6641,-112.383C44.625,-114.023 54,-111.562 54,-105 54,-100.078 48.7266,-97.4634 41.8876,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"34.6641,-97.6172 41.449,-94.0273 38.1569,-97.394 41.6498,-97.1709 41.6498,-97.1709 41.6498,-97.1709 38.1569,-97.394 41.8507,-100.314 34.6641,-97.6172 34.6641,-97.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-101.3\">!d</text>\n",
296
        "</g>\n",
297
298
299
300
301
        "<!-- 2&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;3</title>\n",
        "<path d=\"M26.1601,-88.4509C32.1393,-77.9698 40.9431,-64.2405 51,-54 59.6413,-45.201 70.7932,-37.2529 80.4641,-31.163\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"86.5641,-27.4392 82.2308,-33.7752 83.5768,-29.2629 80.5894,-31.0865 80.5894,-31.0865 80.5894,-31.0865 83.5768,-29.2629 78.9481,-28.3979 86.5641,-27.4392 86.5641,-27.4392\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"69.5\" y=\"-57.8\">!c &amp; d</text>\n",
302
        "</g>\n",
303
304
305
306
307
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;1</title>\n",
        "<path d=\"M112.987,-32.4924C127.759,-52.3541 150.875,-90.6129 139,-123 131.283,-144.048 114.387,-163.166 100.33,-176.403\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"94.9106,-181.355 97.9539,-174.308 97.4946,-178.994 100.079,-176.633 100.079,-176.633 100.079,-176.633 97.4946,-178.994 102.203,-178.959 94.9106,-181.355 94.9106,-181.355\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"145.5\" y=\"-101.3\">c</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=\"M118.664,-25.3828C128.625,-27.0234 138,-24.5625 138,-18 138,-13.0781 132.727,-10.4634 125.888,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"118.664,-10.6172 125.449,-7.02727 122.157,-10.394 125.65,-10.1709 125.65,-10.1709 125.65,-10.1709 122.157,-10.394 125.851,-13.3145 118.664,-10.6172 118.664,-10.6172\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"143.5\" y=\"-14.3\">!c</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=\"355pt\" viewBox=\"0.00 0.00 427.00 355.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 351)\">\n",
348
        "<title>G</title>\n",
349
350
351
352
353
        "<polygon fill=\"white\" points=\"-4,4 -4,-351 423,-351 423,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-332.8\">Inf(</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-332.8\">\u24ff</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-332.8\">)</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.5\" y=\"-318.8\">[B\u00fcchi]</text>\n",
354
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
355
        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
356
357
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
358
        "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
359
360
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
361
        "<polygon fill=\"none\" points=\"30,-18 30,-103 82,-103 82,-18 30,-18\" stroke=\"red\"/>\n",
362
363
364
365
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
366
367
        "<ellipse cx=\"56\" cy=\"-44\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.3\">0</text>\n",
368
369
370
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
371
372
        "<path d=\"M1.15491,-44C2.79388,-44 17.1543,-44 30.6317,-44\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9419,-44 30.9419,-47.1501 34.4419,-44 30.9419,-44.0001 30.9419,-44.0001 30.9419,-44.0001 34.4419,-44 30.9418,-40.8501 37.9419,-44 37.9419,-44\" stroke=\"black\"/>\n",
373
374
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
375
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
376
377
378
        "<path d=\"M49.6208,-61.0373C48.3189,-70.8579 50.4453,-80 56,-80 60.166,-80 62.4036,-74.8576 62.7128,-68.1433\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"62.3792,-61.0373 65.8541,-67.8818 62.5434,-64.5335 62.7076,-68.0296 62.7076,-68.0296 62.7076,-68.0296 62.5434,-64.5335 59.561,-68.1774 62.3792,-61.0373 62.3792,-61.0373\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-83.8\">a &amp; !b</text>\n",
379
380
381
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
382
383
        "<ellipse cx=\"169\" cy=\"-151\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-147.3\">1</text>\n",
384
385
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
386
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
387
388
389
        "<path d=\"M69.7331,-56.2743C89.5555,-75.3823 127.846,-112.293 150.33,-133.967\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"155.415,-138.869 148.189,-136.279 152.896,-136.44 150.376,-134.011 150.376,-134.011 150.376,-134.011 152.896,-136.44 152.562,-131.743 155.415,-138.869 155.415,-138.869\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-120.8\">b</text>\n",
390
391
392
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
393
394
        "<ellipse cx=\"169\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
395
396
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
397
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
398
399
400
        "<path d=\"M74.3438,-42.4375C92.9975,-40.757 122.797,-38.0723 143.763,-36.1835\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"150.778,-35.5515 144.089,-39.317 147.292,-35.8656 143.806,-36.1797 143.806,-36.1797 143.806,-36.1797 147.292,-35.8656 143.524,-33.0424 150.778,-35.5515 150.778,-35.5515\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-44.8\">!a &amp; !b</text>\n",
401
402
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
403
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
404
405
406
407
        "<path d=\"M160.021,-166.916C157.679,-177.15 160.672,-187 169,-187 175.376,-187 178.625,-181.226 178.746,-173.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-166.916 181.872,-173.532 178.36,-170.395 178.741,-173.874 178.741,-173.874 178.741,-173.874 178.36,-170.395 175.61,-174.217 177.979,-166.916 177.979,-166.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-205.8\">c &amp; d</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-190.8\">\u24ff</text>\n",
408
409
        "</g>\n",
        "<!-- 2 -->\n",
410
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
411
412
        "<ellipse cx=\"275.5\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"275.5\" y=\"-189.3\">2</text>\n",
413
414
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
415
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
416
417
418
419
        "<path d=\"M186.737,-147.555C201.262,-145.401 222.492,-144.312 239,-152 248.114,-156.244 255.801,-164.081 261.667,-171.775\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"265.79,-177.569 259.165,-173.693 263.76,-174.718 261.731,-171.866 261.731,-171.866 261.731,-171.866 263.76,-174.718 264.297,-170.04 265.79,-177.569 265.79,-177.569\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-170.8\">!d</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-155.8\">\u24ff</text>\n",
420
        "</g>\n",
421
422
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
423
424
        "<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\">3</text>\n",
425
        "</g>\n",
426
        "<!-- 1&#45;&gt;3 -->\n",
427
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
428
429
430
431
        "<path d=\"M186.385,-144.944C210.438,-136.96 256.512,-125.127 294,-136 321.45,-143.961 348.554,-163.081 365.728,-176.986\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"371.158,-181.479 363.756,-179.443 368.461,-179.247 365.764,-177.016 365.764,-177.016 365.764,-177.016 368.461,-179.247 367.772,-174.589 371.158,-181.479 371.158,-181.479\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-154.8\">!c &amp; d</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-139.8\">\u24ff</text>\n",
432
433
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
434
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
435
436
437
        "<path d=\"M257.435,-192.94C242.865,-192.285 221.682,-189.872 205,-182 198.283,-178.83 191.897,-173.966 186.462,-169.024\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"181.368,-164.115 188.595,-166.704 183.889,-166.544 186.409,-168.972 186.409,-168.972 186.409,-168.972 183.889,-166.544 184.223,-171.241 181.368,-164.115 181.368,-164.115\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-195.8\">c &amp; d</text>\n",
438
439
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
440
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
441
442
443
        "<path d=\"M266.521,-208.916C264.179,-219.15 267.172,-229 275.5,-229 281.876,-229 285.125,-223.226 285.246,-215.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"284.479,-208.916 288.372,-215.532 284.86,-212.395 285.241,-215.874 285.241,-215.874 285.241,-215.874 284.86,-212.395 282.11,-216.217 284.479,-208.916 284.479,-208.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-232.8\">!d</text>\n",
444
        "</g>\n",
445
446
447
448
449
        "<!-- 2&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;3</title>\n",
        "<path d=\"M293.772,-193C311.638,-193 339.686,-193 359.767,-193\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"366.771,-193 359.771,-196.15 363.271,-193 359.771,-193 359.771,-193 359.771,-193 363.271,-193 359.771,-189.85 366.771,-193 366.771,-193\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-196.8\">!c &amp; d</text>\n",
450
        "</g>\n",
451
452
453
454
455
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;1</title>\n",
        "<path d=\"M372.089,-205.642C349.996,-227.482 300.914,-268.52 257,-253 219.934,-239.901 193.906,-199.684 180.487,-173.836\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.192,-167.28 183.15,-172.121 178.764,-170.408 180.336,-173.535 180.336,-173.535 180.336,-173.535 178.764,-170.408 177.521,-174.949 177.192,-167.28 177.192,-167.28\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-259.8\">c</text>\n",
456
457
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
458
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
459
460
461
        "<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",
462
        "</g>\n",
463
        "<!-- 4&#45;&gt;4 -->\n",
464
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
465
466
467
        "<path d=\"M160.021,-49.916C157.679,-60.1504 160.672,-70 169,-70 175.376,-70 178.625,-64.2263 178.746,-56.9268\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.979,-49.916 181.872,-56.5315 178.36,-53.3952 178.741,-56.8744 178.741,-56.8744 178.741,-56.8744 178.36,-53.3952 175.61,-57.2174 177.979,-49.916 177.979,-49.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
468
469
470
471
472
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
473
        "<IPython.core.display.SVG object>"
474
475
476
       ]
      }
     ],
477
     "prompt_number": 4
478
    },
479
480
481
482
483
484
485
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `translate()` function can also be called with a formula object.  Either as a function, or as a method."
     ]
    },
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U b'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$a \\mathbin{\\mathsf{U}} b$"
       ],
       "metadata": {},
       "output_type": "pyout",
501
       "prompt_number": 5,
502
503
504
505
506
       "text": [
        "a U b"
       ]
      }
     ],
507
     "prompt_number": 5
508
509
510
511
512
513
514
515
516
517
518
519
520
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate(f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
521
       "prompt_number": 6,
522
523
524
525
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
526
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
527
528
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
529
530
531
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
532
        "<title>G</title>\n",
533
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
534
535
536
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
537
538
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
539
540
541
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
542
543
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
544
545
546
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
547
548
549
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
550
551
552
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
553
554
555
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
556
557
558
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
559
560
561
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
562
563
564
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
565
566
567
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
568
569
570
571
572
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
573
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f23c17168d0> >"
574
575
576
       ]
      }
     ],
577
     "prompt_number": 6
578
579
580
581
582
583
584
585
586
587
588
589
590
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
591
       "prompt_number": 7,
592
593
594
595
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
596
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
597
598
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
599
600
601
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
602
        "<title>G</title>\n",
603
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
604
605
606
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
607
608
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
609
610
611
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
612
613
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
614
615
616
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
617
618
619
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
620
621
622
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
623
624
625
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
626
627
628
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
629
630
631
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
632
633
634
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
635
636
637
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
638
639
640
641
642
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
643
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f23c1716330> >"
644
645
646
       ]
      }
     ],
647
     "prompt_number": 7
648
    },
649
650
651
652
653
654
655
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "When used as a method, all the arguments are translation options.  Here is a monitor:"
     ]
    },
656
657
658
659
660
661
662
663
664
665
666
667
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate('mon')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
668
       "prompt_number": 8,
669
670
671
672
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
673
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
674
675
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
676
677
678
        "<svg width=\"163pt\" height=\"77pt\"\n",
        " viewBox=\"0.00 0.00 163.00 77.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 73)\">\n",
679
        "<title>G</title>\n",
680
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
681
682
683
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
684
685
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
686
687
688
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
689
690
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\n",
691
692
693
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
694
695
696
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
697
698
699
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
700
701
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
702
703
704
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
705
706
707
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-18C85.1153,-18 99.5214,-18 111.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-18 111.892,-21.1501 115.392,-18 111.892,-18.0001 111.892,-18.0001 111.892,-18.0001 115.392,-18 111.892,-14.8501 118.892,-18 118.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
708
709
710
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
711
712
713
        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
714
715
716
717
718
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
719
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f23c1716180> >"
720
721
722
       ]
      }
     ],
723
     "prompt_number": 8
724
    },
725
726
727
728
729
730
731
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`."
     ]
    },
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('Ga | Gb | Gc'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
       ],
       "metadata": {},
       "output_type": "pyout",
747
       "prompt_number": 9,
748
749
750
751
752
       "text": [
        "Ga | Gb | Gc"
       ]
      }
     ],
753
     "prompt_number": 9
754
755
756
757
758
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
759
      "f.translate('ba', 'small').show('.v')"
760
761
762
763
764
765
766
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
767
       "prompt_number": 10,
768
       "svg": [
769
        "<svg height=\"177pt\" viewBox=\"0.00 0.00 253.00 177.00\" width=\"253pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
770
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
771
        "<title>G</title>\n",
772
        "<polygon fill=\"white\" points=\"-4,4 -4,-173 249,-173 249,4 -4,4\" stroke=\"none\"/>\n",
773
774
775
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
776
        "<ellipse cx=\"109\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
777
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-109.3\">0</text>\n",
778
779
780
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
781
782
        "<path d=\"M109,-167.845C109,-166.206 109,-151.846 109,-138.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"109,-131.058 112.15,-138.058 109,-134.558 109,-138.058 109,-138.058 109,-138.058 109,-134.558 105.85,-138.058 109,-131.058 109,-131.058\" stroke=\"black\"/>\n",
783
784
785
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
786
787
        "<ellipse cx=\"22\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"22\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
788
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22\" y=\"-18.3\">1</text>\n",
789
790
791
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
792
793
        "<path d=\"M96.903,-99.6249C82.686,-85.081 58.8862,-60.7342 41.9306,-43.3887\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"36.9064,-38.2491 44.0522,-41.0528 39.353,-40.7519 41.7996,-43.2548 41.7996,-43.2548 41.7996,-43.2548 39.353,-40.7519 39.547,-45.4567 36.9064,-38.2491 36.9064,-38.2491\" stroke=\"black\"/>\n",
794
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"74\" y=\"-65.8\">a</text>\n",
795
796
797
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
798
799
        "<ellipse cx=\"109\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"109\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
800
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-18.3\">2</text>\n",
801
802
803
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
804
805
        "<path d=\"M109,-94.8399C109,-82.5378 109,-65.6842 109,-51.3928\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"109,-44.1905 112.15,-51.1905 109,-47.6905 109,-51.1905 109,-51.1905 109,-51.1905 109,-47.6905 105.85,-51.1906 109,-44.1905 109,-44.1905\" stroke=\"black\"/>\n",
806
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-65.8\">b</text>\n",
807
808
809
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
810
811
812
        "<ellipse cx=\"198\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"198\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198\" y=\"-18.3\">3</text>\n",
813
814
815
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
816
817
818
        "<path d=\"M121.375,-99.6249C135.919,-85.081 160.266,-60.7342 177.611,-43.3887\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"182.751,-38.2491 180.029,-45.4262 180.276,-40.7239 177.801,-43.1988 177.801,-43.1988 177.801,-43.1988 180.276,-40.7239 175.574,-40.9714 182.751,-38.2491 182.751,-38.2491\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158\" y=\"-65.8\">c</text>\n",
819
820
821
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
822
823
        "<path d=\"M42.5808,-30.3702C52.8447,-31.5284 62,-28.7383 62,-22 62,-16.9463 56.8502,-14.1134 49.9451,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"42.5808,-13.6298 49.5248,-10.3582 46.0803,-13.5688 49.5797,-13.5077 49.5797,-13.5077 49.5797,-13.5077 46.0803,-13.5688 49.6347,-16.6573 42.5808,-13.6298 42.5808,-13.6298\" stroke=\"black\"/>\n",
824
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62\" y=\"-18.3\">a</text>\n",
825
826
827
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
828
829
        "<path d=\"M129.581,-30.3702C139.845,-31.5284 149,-28.7383 149,-22 149,-16.9463 143.85,-14.1134 136.945,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"129.581,-13.6298 136.525,-10.3582 133.08,-13.5688 136.58,-13.5077 136.58,-13.5077 136.58,-13.5077 133.08,-13.5688 136.635,-16.6573 129.581,-13.6298 129.581,-13.6298\" stroke=\"black\"/>\n",
830
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"149\" y=\"-18.3\">b</text>\n",
831
832
833
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
834
835
836
        "<path d=\"M218.581,-30.3702C228.845,-31.5284 238,-28.7383 238,-22 238,-16.9463 232.85,-14.1134 225.945,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"218.581,-13.6298 225.525,-10.3582 222.08,-13.5688 225.58,-13.5077 225.58,-13.5077 225.58,-13.5077 222.08,-13.5688 225.635,-16.6573 218.581,-13.6298 218.581,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-18.3\">c</text>\n",
837
838
839
840
841
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
842
        "<IPython.core.display.SVG object>"
843
844
845
       ]
      }
     ],
846
     "prompt_number": 10
847
848
849
850
851
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
852
      "f.translate('ba', 'det').show('v.')"
853
854
855
856
857
858
859
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
860
       "prompt_number": 11,
861
       "svg": [
862
863
        "<svg height=\"280pt\" viewBox=\"0.00 0.00 596.88 280.00\" width=\"597pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 276)\">\n",
864
        "<title>G</title>\n",
865
        "<polygon fill=\"white\" points=\"-4,4 -4,-276 592.883,-276 592.883,4 -4,4\" stroke=\"none\"/>\n",
866
867
868
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node2\"><title>6</title>\n",
869
870
871
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"279.883\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"279.883\" y=\"-208.3\">6</text>\n",
872
873
874
        "</g>\n",
        "<!-- I&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
875
876
        "<path d=\"M279.883,-270.834C279.883,-269.159 279.883,-255.116 279.883,-241.289\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"279.883,-234.144 283.033,-241.144 279.883,-237.644 279.883,-241.144 279.883,-241.144 279.883,-241.144 279.883,-237.644 276.733,-241.145 279.883,-234.144 279.883,-234.144\" stroke=\"black\"/>\n",
877
878
879
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
880
881
882
        "<path d=\"M300.874,-219.317C310.971,-220.22 319.883,-217.781 319.883,-212 319.883,-207.664 314.87,-205.208 308.104,-204.632\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"300.874,-204.683 307.852,-201.484 304.374,-204.658 307.874,-204.634 307.874,-204.634 307.874,-204.634 304.374,-204.658 307.896,-207.784 300.874,-204.683 300.874,-204.683\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"319.883\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
883
884
885
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
886
887
888
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"98.8834\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.8834\" y=\"-18.3\">0</text>\n",
889
890
891
        "</g>\n",
        "<!-- 6&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
892
893
894
        "<path d=\"M258.05,-208.601C199.066,-201.628 38.871,-179.258 7.88337,-139 -20.5572,-102.052 37.5535,-58.9513 73.4411,-37.1624\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"79.8576,-33.3483 75.45,-39.6328 76.849,-35.1367 73.8404,-36.9251 73.8404,-36.9251 73.8404,-36.9251 76.849,-35.1367 72.2309,-34.2174 79.8576,-33.3483 79.8576,-33.3483\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"7.88337\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
895
896
897
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
898
899
900
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"104.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.883\" y=\"-113.3\">1</text>\n",
901
902
903
        "</g>\n",
        "<!-- 6&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
904
905
906
        "<path d=\"M258.548,-205.147C236.734,-198.695 202.263,-187.184 174.883,-172 157.384,-162.295 139.553,-148.469 126.267,-137.237\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"120.866,-132.602 128.229,-134.77 123.522,-134.881 126.178,-137.161 126.178,-137.161 126.178,-137.161 123.522,-134.881 124.126,-139.551 120.866,-132.602 120.866,-132.602\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.883\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
907
908
909
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
910
911
912
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"326.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326.883\" y=\"-18.3\">2</text>\n",
913
914
915
        "</g>\n",
        "<!-- 6&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
916
917
918
        "<path d=\"M295.807,-196.555C302.236,-189.767 309.034,-181.157 312.883,-172 329.476,-132.531 330.508,-82.1352 329.137,-51.2346\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"328.768,-44.1943 332.28,-51.0197 328.951,-47.6895 329.135,-51.1847 329.135,-51.1847 329.135,-51.1847 328.951,-47.6895 325.989,-51.3498 328.768,-44.1943 328.768,-44.1943\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"327.883\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
919
920
921
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
922
923
        "<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",
924
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.883\" y=\"-18.3\">3</text>\n",
925
        "</g>\n",
926
927
        "<!-- 6&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
928
929
930
        "<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",
931
932
        "</g>\n",
        "<!-- 4 -->\n",
933
        "<g class=\"node\" id=\"node7\"><title>4</title>\n",
934
935
936
        "<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",
937
938
939
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
940
941
942
        "<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",
943
        "</g>\n",
944
945
946
947
948
949
950
951
952
953
954
955
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node8\"><title>5</title>\n",
        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"432.883\" y=\"-113.3\">5</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
        "<path d=\"M298.339,-199.782C325.793,-183.094 377.444,-151.699 408.145,-133.037\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"414.363,-129.258 410.017,-135.585 411.372,-131.076 408.381,-132.894 408.381,-132.894 408.381,-132.894 411.372,-131.076 406.745,-130.202 414.363,-129.258 414.363,-129.258\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.883\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
        "</g>\n",
956
957
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
958
959
960
        "<path d=\"M119.464,-30.3702C129.728,-31.5284 138.883,-28.7383 138.883,-22 138.883,-16.9463 133.734,-14.1134 126.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"119.464,-13.6298 126.408,-10.3582 122.964,-13.5688 126.463,-13.5077 126.463,-13.5077 126.463,-13.5077 122.964,-13.5688 126.518,-16.6573 119.464,-13.6298 119.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.883\" y=\"-18.3\">c</text>\n",
961
962
963
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
964
965
966
        "<path d=\"M101.764,-94.9925C101.016,-89.1774 100.312,-82.8549 99.8834,-77 99.2697,-68.6098 98.9633,-59.468 98.8243,-51.1319\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"98.7416,-44.0528 101.973,-51.0155 98.7825,-47.5526 98.8234,-51.0524 98.8234,-51.0524 98.8234,-51.0524 98.7825,-47.5526 95.6736,-51.0892 98.7416,-44.0528 98.7416,-44.0528\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.8834\" y=\"-65.8\">!b &amp; c</text>\n",
967
968
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
969
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
970
971
972
        "<path d=\"M125.464,-125.37C135.728,-126.528 144.883,-123.738 144.883,-117 144.883,-111.946 139.734,-109.113 132.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"125.464,-108.63 132.408,-105.358 128.964,-108.569 132.463,-108.508 132.463,-108.508 132.463,-108.508 128.964,-108.569 132.518,-111.657 125.464,-108.63 125.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"144.883\" y=\"-113.3\">b &amp; c</text>\n",
973
        "</g>\n",
974
975
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
976
977
978
        "<path d=\"M118.615,-99.4594C130.558,-85.4667 147.262,-66.9259 155.883,-62 201.053,-36.1916 262.094,-27.4608 297.704,-24.508\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"304.902,-23.9616 298.16,-27.6325 301.412,-24.2266 297.922,-24.4916 297.922,-24.4916 297.922,-24.4916 301.412,-24.2266 297.683,-21.3506 304.902,-23.9616 304.902,-23.9616\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.883\" y=\"-65.8\">b &amp; !c</text>\n",
979
        "</g>\n",
980
981
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
982
983
984
        "<path d=\"M347.464,-30.3702C357.728,-31.5284 366.883,-28.7383 366.883,-22 366.883,-16.9463 361.734,-14.1134 354.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"347.464,-13.6298 354.408,-10.3582 350.964,-13.5688 354.463,-13.5077 354.463,-13.5077 354.463,-13.5077 350.964,-13.5688 354.518,-16.6573 347.464,-13.6298 347.464,-13.6298\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.883\" y=\"-18.3\">b</text>\n",
985
986
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
987
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
988
989
990
        "<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",
991
992
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
993
        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;0</title>\n",
994
995
996
        "<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",
997
        "</g>\n",
998
999
        "<!-- 4&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;3</title>\n",
1000
1001
1002
        "<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",
1003
1004
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
1005
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
1006
1007
1008
        "<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",
1009
        "</g>\n",
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
        "<!-- 5&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;2</title>\n",
        "<path d=\"M423.273,-97.1109C416.901,-85.9186 407.728,-72.013 396.883,-62 384.323,-50.4024 367.69,-40.9523 353.79,-34.2605\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"347.216,-31.1996 354.891,-31.2984 350.389,-32.6769 353.562,-34.1541 353.562,-34.1541 353.562,-34.1541 350.389,-32.6769 352.232,-37.0098 347.216,-31.1996 347.216,-31.1996\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.883\" y=\"-65.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;3</title>\n",
        "<path d=\"M444.753,-98.1028C448.839,-91.5928 453.288,-84.0908 456.883,-77 461.334,-68.2222 465.577,-58.3236 469.128,-49.4213\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"471.701,-42.843 472.085,-50.5095 470.426,-46.1025 469.152,-49.3621 469.152,-49.3621 469.152,-49.3621 470.426,-46.1025 466.218,-48.2147 471.701,-42.843 471.701,-42.843\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462.883\" y=\"-65.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
        "<path d=\"M453.464,-125.37C463.728,-126.528 472.883,-123.738 472.883,-117 472.883,-111.946 467.734,-109.113 460.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"453.464,-108.63 460.408,-105.358 456.964,-108.569 460.463,-108.508 460.463,-108.508 460.463,-108.508 456.964,-108.569 460.518,-111.657 453.464,-108.63 453.464,-108.63\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"472.883\" y=\"-113.3\">a &amp; b</text>\n",
        "</g>\n",
1028
1029
1030
1031
        "</g>\n",
        "</svg>"
       ],
       "text": [
1032
        "<IPython.core.display.SVG object>"
1033
1034
1035
1036
1037
       ]
      }
     ],
     "prompt_number": 11
    },
1038
1039
1040
1041
1042
1043
1044
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Here is how to build an unambiguous automaton:"
     ]
    },
1045
1046
1047
1048
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
1049
      "spot.translate('GFa -> GFb', 'unambig')"
1050
1051
1052
1053
1054
1055
1056
1057
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
1058
1059
1060
1061
1062
1063
1064
       "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",
1065
1066
1067
        "<svg width=\"302pt\" height=\"311pt\"\n",
        " viewBox=\"0.00 0.00 301.50 311.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 307)\">\n",
1068
        "<title>G</title>\n",
1069
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-307 297.5,-307 297.5,4 -4,4\"/>\n",
1070
1071
1072
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1073
1074
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-123\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-119.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1075
1076
1077
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1078
1079
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-123C2.79388,-123 17.1543,-123 30.6317,-123\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-123 30.9419,-126.15 34.4419,-123 30.9419,-123 30.9419,-123 30.9419,-123 34.4419,-123 30.9418,-119.85 37.9419,-123 37.9419,-123\"/>\n",
1080
1081
1082
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1083
1084
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-204\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-200.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1085
1086
1087
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1088
1089
1090
        "<path fill=\"none\" stroke=\"black\" d=\"M66.5112,-137.647C72.9549,-146.82 82.0794,-158.476 92,-167 104.757,-177.961 121.236,-187.349 134.344,-193.926\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"140.854,-197.102 133.181,-196.863 137.708,-195.567 134.563,-194.032 134.563,-194.032 134.563,-194.032 137.708,-195.567 135.944,-191.202 140.854,-197.102 140.854,-197.102\"/>\n",
        "<text text-anchor=\"middle\" x=\"105.5\" y=\"-188.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1091
1092
1093
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
1094
1095
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"157.5\" cy=\"-66\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"157.5\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1096
1097
1098
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
1099
1100
1101
        "<path fill=\"none\" stroke=\"black\" d=\"M72.1119,-114.343C89.0117,-104.662 116.498,-88.9157 135.486,-78.0382\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"141.572,-74.5518 137.064,-80.7647 138.535,-76.2916 135.498,-78.0314 135.498,-78.0314 135.498,-78.0314 138.535,-76.2916 133.932,-75.2981 141.572,-74.5518 141.572,-74.5518\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1102
1103
1104
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1105
1106
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-123\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-119.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1107
1108
1109
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
1110
1111
1112
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0034,-126.729C106.092,-133.193 177.685,-144.886 237,-135 241.14,-134.31 245.447,-133.19 249.566,-131.905\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.258,-129.634 250.642,-134.867 252.943,-130.759 249.629,-131.884 249.629,-131.884 249.629,-131.884 252.943,-130.759 248.617,-128.901 256.258,-129.634 256.258,-129.634\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-141.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1113
1114
1115
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
1116
1117
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"273\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
1118
1119
1120
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
1121
1122
1123
        "<path fill=\"none\" stroke=\"black\" d=\"M64.5788,-106.747C76.3694,-83.5932 101.497,-41.9353 137,-24 172.369,-6.13214 219.835,-9.23041 248.037,-13.4066\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.114,-14.5378 247.705,-16.5434 251.658,-13.9853 248.202,-13.4328 248.202,-13.4328 248.202,-13.4328 251.658,-13.9853 248.699,-10.3223 255.114,-14.5378 255.114,-14.5378\"/>\n",
        "<text text-anchor=\"start\" x=\"137\" y=\"-27.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1124
1125
1126
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1127
1128
        "<path fill=\"none\" stroke=\"black\" d=\"M152.858,-221.41C151.992,-231.088 153.539,-240 157.5,-240 160.409,-240 162.016,-235.194 162.321,-228.807\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"162.142,-221.41 165.461,-228.331 162.227,-224.909 162.312,-228.408 162.312,-228.408 162.312,-228.408 162.227,-224.909 159.163,-228.484 162.142,-221.41 162.142,-221.41\"/>\n",
1129
        "<text text-anchor=\"start\" x=\"151\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
1130
1131
1132
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1133
1134
1135
1136
        "<path fill=\"none\" stroke=\"black\" d=\"M150.038,-220.586C145.364,-238.17 147.852,-258 157.5,-258 165.867,-258 168.849,-243.087 166.446,-227.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"164.962,-220.586 169.482,-226.79 165.681,-224.011 166.399,-227.437 166.399,-227.437 166.399,-227.437 165.681,-224.011 163.316,-228.083 164.962,-220.586 164.962,-220.586\"/>\n",
        "<text text-anchor=\"start\" x=\"153\" y=\"-276.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"149.5\" y=\"-261.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
1137
1138
1139
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
1140
1141
1142
        "<path fill=\"none\" stroke=\"black\" d=\"M148.521,-81.916C146.179,-92.1504 149.172,-102 157.5,-102 163.876,-102 167.125,-96.2263 167.246,-88.9268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"166.479,-81.916 170.372,-88.5315 166.86,-85.3952 167.241,-88.8744 167.241,-88.8744 167.241,-88.8744 166.86,-85.3952 164.11,-89.2174 166.479,-81.916 166.479,-81.916\"/>\n",
        "<text text-anchor=\"start\" x=\"144\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1143
        "</g>\n",
1144
1145
1146
1147
1148
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M169.815,-79.2791C176.712,-86.6222 186.087,-95.3722 196,-101 212.117,-110.15 232.356,-115.766 247.895,-119.032\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.107,-120.451 247.631,-122.19 251.673,-119.775 248.239,-119.099 248.239,-119.099 248.239,-119.099 251.673,-119.775 248.847,-116.009 255.107,-120.451 255.107,-120.451\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1149
        "</g>\n",
1150
1151
1152
1153
1154
        "<!-- 2&#45;&gt;4 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M174.076,-58.2162C180.773,-54.9495 188.72,-51.1791 196,-48 213.699,-40.2709 234.068,-32.2776 249.262,-26.4873\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.85,-23.9908 250.42,-29.4169 252.577,-25.231 249.304,-26.4713 249.304,-26.4713 249.304,-26.4713 252.577,-25.231 248.188,-23.5256 255.85,-23.9908 255.85,-23.9908\"/>\n",
        "<text text-anchor=\"start\" x=\"196\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1155
        "</g>\n",
1156
1157
1158
1159
1160
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M262.811,-107.876C256.615,-98.9778 247.642,-88.2732 237,-82 220.479,-72.2616 198.982,-68.372 182.662,-66.8559\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.564,-66.3138 182.784,-63.7061 179.054,-66.5804 182.544,-66.8469 182.544,-66.8469 182.544,-66.8469 179.054,-66.5804 182.304,-69.9878 175.564,-66.3138 175.564,-66.3138\"/>\n",
        "<text text-anchor=\"start\" x=\"203\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
1161
        "</g>\n",
1162
1163
1164
1165
1166
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-138.541C260.73,-148.909 263.922,-159 273,-159 279.95,-159 283.45,-153.085 283.499,-145.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-138.541 286.6,-145.077 283.026,-142.012 283.477,-145.483 283.477,-145.483 283.477,-145.483 283.026,-142.012 280.353,-145.889 282.575,-138.541 282.575,-138.541\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1167
1168
1169
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
1170
1171
1172
        "<path fill=\"none\" stroke=\"black\" d=\"M263.425,-33.5414C260.73,-43.9087 263.922,-54 273,-54 279.95,-54 283.45,-48.0847 283.499,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"282.575,-33.5414 286.6,-40.0771 283.026,-37.0123 283.477,-40.4831 283.477,-40.4831 283.477,-40.4831 283.026,-37.0123 280.353,-40.889 282.575,-33.5414 282.575,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"252.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1173
        "<text text-anchor=\"start\" x=\"265\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
1174
1175
1176
1177
1178
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1179
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f23c1716b10> >"
1180
1181
1182
1183
1184
1185
1186