automata.ipynb 124 KB
Newer Older
1
2
{
 "metadata": {
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
  "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",
   "version": "3.4.2"
  },
20
  "name": "",
21
  "signature": "sha256:7bcd29a20e60c508a998923ed5875f91f69cd4f3e77dca19795b976dab016b90"
22
23
24
25
26
27
28
29
30
31
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
32
      "import os\n",
33
34
35
36
      "# Note that Spot (loaded by the kernel) will store a copy of\n",
      "# the environment variable the first time it reads them, so\n",
      "# if you change those variables, the new values will be ignored\n",
      "# until you restart the kernel.\n",
37
      "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
38
39
      "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
      "import spot"
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = spot.translate('(a U b) & GFc & GFd', 'BA', complete=True); a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
58
       "prompt_number": 2,
59
60
61
62
       "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",
63
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
64
65
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
66
67
68
        "<svg width=\"432pt\" height=\"197pt\"\n",
        " viewBox=\"0.00 0.00 432.00 196.80\" 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 192.8)\">\n",
69
        "<title>G</title>\n",
70
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-192.8 428,-192.8 428,4 -4,4\"/>\n",
71
72
73
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
74
75
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-74\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-71.2\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
76
77
78
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
79
80
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-74C3.85328,-74 18.9155,-74 32.8257,-74\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-74 32.918,-77.1501 36.4179,-74 32.9179,-74.0001 32.9179,-74.0001 32.9179,-74.0001 36.4179,-74 32.9179,-70.8501 39.9179,-74 39.9179,-74\"/>\n",
81
82
83
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
84
85
86
        "<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-91.0373C50.3189,-100.858 52.4453,-110 58,-110 62.166,-110 64.4036,-104.858 64.7128,-98.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-91.0373 67.8541,-97.8818 64.5434,-94.5335 64.7076,-98.0296 64.7076,-98.0296 64.7076,-98.0296 64.5434,-94.5335 61.561,-98.1774 64.3792,-91.0373 64.3792,-91.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"40.15\" y=\"-115.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
87
88
89
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
90
91
92
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"182\" cy=\"-117\" rx=\"29.3314\" ry=\"29.3314\"/>\n",
        "<text text-anchor=\"start\" x=\"177.94\" y=\"-122.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"174.262\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
93
94
95
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
96
97
98
        "<path fill=\"none\" stroke=\"black\" d=\"M75.2007,-79.7101C93.4887,-86.1559 123.75,-96.8217 147.234,-105.099\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"153.973,-107.474 146.324,-108.118 150.672,-106.311 147.371,-105.147 147.371,-105.147 147.371,-105.147 150.672,-106.311 148.418,-102.176 153.973,-107.474 153.973,-107.474\"/>\n",
        "<text text-anchor=\"start\" x=\"110.08\" y=\"-105.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
99
100
101
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
102
103
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"182\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"182\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
104
105
106
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
107
108
109
        "<path fill=\"none\" stroke=\"black\" d=\"M74.9494,-66.679C96.4393,-56.8147 134.784,-39.214 159.002,-28.0974\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"165.432,-25.1458 160.385,-30.9288 162.252,-26.6059 159.071,-28.066 159.071,-28.066 159.071,-28.066 162.252,-26.6059 157.757,-25.2032 165.432,-25.1458 165.432,-25.1458\"/>\n",
        "<text text-anchor=\"start\" x=\"94.267\" y=\"-63.6\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
110
111
112
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
113
114
115
        "<path fill=\"none\" stroke=\"black\" d=\"M170.073,-144.047C169.399,-154.895 173.375,-164 182,-164 188.604,-164 192.482,-158.663 193.634,-151.292\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"193.927,-144.047 196.792,-151.168 193.786,-147.544 193.644,-151.041 193.644,-151.041 193.644,-151.041 193.786,-147.544 190.497,-150.914 193.927,-144.047 193.927,-144.047\"/>\n",
        "<text text-anchor=\"start\" x=\"166.169\" y=\"-169.6\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
116
117
118
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
119
120
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"406\" cy=\"-107\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"406\" y=\"-104.2\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
121
122
123
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
124
125
126
        "<path fill=\"none\" stroke=\"black\" d=\"M205.275,-135.294C231.438,-154.489 276.315,-180.295 316,-168 343.651,-159.434 370.349,-138.982 387.17,-124.116\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"392.482,-119.313 389.402,-126.344 389.886,-121.66 387.289,-124.007 387.289,-124.007 387.289,-124.007 389.886,-121.66 385.177,-121.67 392.482,-119.313 392.482,-119.313\"/>\n",
        "<text text-anchor=\"start\" x=\"280.286\" y=\"-177.6\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
127
128
129
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
130
131
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"298\" cy=\"-107\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"298\" y=\"-104.2\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
132
133
134
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
135
136
137
        "<path fill=\"none\" stroke=\"black\" d=\"M211.625,-117.645C226.672,-117.639 245.393,-117.087 262,-115 265.693,-114.536 269.568,-113.853 273.339,-113.079\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"280.386,-111.51 274.238,-116.106 276.97,-112.27 273.553,-113.031 273.553,-113.031 273.553,-113.031 276.97,-112.27 272.869,-109.956 280.386,-111.51 280.386,-111.51\"/>\n",
        "<text text-anchor=\"start\" x=\"240.197\" y=\"-123.6\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
138
139
140
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
141
142
143
        "<path fill=\"none\" stroke=\"black\" d=\"M171.292,-32.7917C167.806,-43.4165 171.375,-54 182,-54 190.135,-54 194.134,-47.7961 193.997,-40.1197\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"192.708,-32.7917 197.023,-39.1403 193.314,-36.2388 193.92,-39.6859 193.92,-39.6859 193.92,-39.6859 193.314,-36.2388 190.818,-40.2315 192.708,-32.7917 192.708,-32.7917\"/>\n",
        "<text text-anchor=\"middle\" x=\"182\" y=\"-59.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
144
145
146
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
147
148
149
        "<path fill=\"none\" stroke=\"black\" d=\"M391.028,-96.4454C368.21,-80.5064 321.34,-53.1631 280,-63.2 255.285,-69.2006 230.254,-83.3288 211.811,-95.6014\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"205.819,-99.6779 209.835,-93.136 208.713,-97.7092 211.607,-95.7404 211.607,-95.7404 211.607,-95.7404 208.713,-97.7092 213.379,-98.3449 205.819,-99.6779 205.819,-99.6779\"/>\n",
        "<text text-anchor=\"start\" x=\"294.658\" y=\"-69.6\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
150
151
152
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
153
154
155
        "<path fill=\"none\" stroke=\"black\" d=\"M396.767,-122.541C394.169,-132.909 397.246,-143 406,-143 412.702,-143 416.077,-137.085 416.124,-129.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"415.233,-122.541 419.229,-129.095 415.668,-126.014 416.103,-129.487 416.103,-129.487 416.103,-129.487 415.668,-126.014 412.977,-129.879 415.233,-122.541 415.233,-122.541\"/>\n",
        "<text text-anchor=\"start\" x=\"400.774\" y=\"-148.6\" font-family=\"Lato\" font-size=\"14.00\">!c</text>\n",
156
157
158
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
159
160
161
        "<path fill=\"none\" stroke=\"black\" d=\"M281.296,-99.9264C275.375,-97.6168 268.498,-95.351 262,-94.2 247.996,-91.7196 243.861,-91.0155 230,-94.2 224.655,-95.428 219.213,-97.3479 214.018,-99.5644\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"207.595,-102.501 212.652,-96.7254 210.778,-101.046 213.961,-99.5902 213.961,-99.5902 213.961,-99.5902 210.778,-101.046 215.271,-102.455 207.595,-102.501 207.595,-102.501\"/>\n",
        "<text text-anchor=\"start\" x=\"230.169\" y=\"-100.6\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
162
163
164
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
165
166
167
        "<path fill=\"none\" stroke=\"black\" d=\"M316.031,-107C333.467,-107 360.737,-107 380.492,-107\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"387.659,-107 380.659,-110.15 384.159,-107 380.659,-107 380.659,-107 380.659,-107 384.159,-107 380.659,-103.85 387.659,-107 387.659,-107\"/>\n",
        "<text text-anchor=\"start\" x=\"334.286\" y=\"-112.6\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
168
169
170
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
171
172
173
        "<path fill=\"none\" stroke=\"black\" d=\"M289.021,-122.916C286.679,-133.15 289.672,-143 298,-143 304.376,-143 307.625,-137.226 307.746,-129.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"306.979,-122.916 310.872,-129.532 307.36,-126.395 307.741,-129.874 307.741,-129.874 307.741,-129.874 307.36,-126.395 304.61,-130.217 306.979,-122.916 306.979,-122.916\"/>\n",
        "<text text-anchor=\"start\" x=\"292.197\" y=\"-148.6\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
174
175
176
177
178
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
179
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x1052702d0> >"
180
181
182
       ]
      }
     ],
183
     "prompt_number": 2
184
185
186
187
188
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
189
      "a.show(\"\")"
190
191
192
193
194
195
196
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
197
       "prompt_number": 3,
198
       "svg": [
199
200
        "<svg height=\"181pt\" viewBox=\"0.00 0.00 488.00 181.00\" width=\"488pt\" 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 177)\">\n",
201
        "<title>G</title>\n",
202
        "<polygon fill=\"white\" points=\"-4,4 -4,-177 484,-177 484,4 -4,4\" stroke=\"none\"/>\n",
203
204
205
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
206
207
        "<ellipse cx=\"67\" cy=\"-69\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67\" y=\"-64.8\">0</text>\n",
208
209
210
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
211
212
        "<path d=\"M2.04639,-69C2.9702,-69 17.5453,-69 32.5471,-69\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"39.888,-69 32.888,-72.1501 36.388,-69 32.888,-69.0001 32.888,-69.0001 32.888,-69.0001 36.388,-69 32.8879,-65.8501 39.888,-69 39.888,-69\" stroke=\"black\"/>\n",
213
214
215
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
216
217
218
        "<path d=\"M58.7877,-86.4099C57.2548,-96.0879 59.9922,-105 67,-105 72.1464,-105 74.9897,-100.194 75.5299,-93.8073\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"75.2123,-86.4099 78.6598,-93.2683 75.3625,-89.9067 75.5127,-93.4035 75.5127,-93.4035 75.5127,-93.4035 75.3625,-89.9067 72.3656,-93.5386 75.2123,-86.4099 75.2123,-86.4099\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67\" y=\"-107.8\">a &amp; !b</text>\n",
219
220
221
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
222
223
224
        "<ellipse cx=\"201\" cy=\"-108\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"201\" cy=\"-108\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"201\" y=\"-103.8\">1</text>\n",
225
226
227
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
228
229
230
        "<path d=\"M91.9042,-76.0626C112.372,-82.11 142.111,-90.8964 165.217,-97.7232\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"172.157,-99.7738 164.552,-100.811 168.801,-98.782 165.444,-97.7903 165.444,-97.7903 165.444,-97.7903 168.801,-98.782 166.337,-94.7694 172.157,-99.7738 172.157,-99.7738\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132\" y=\"-95.8\">b</text>\n",
231
232
233
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
234
235
        "<ellipse cx=\"201\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"201\" y=\"-13.8\">4</text>\n",
236
237
238
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
239
240
241
        "<path d=\"M90.6916,-60.2328C112.792,-51.6942 146.49,-38.6741 170.626,-29.3489\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.163,-26.8235 171.768,-32.2847 173.898,-28.0849 170.633,-29.3463 170.633,-29.3463 170.633,-29.3463 173.898,-28.0849 169.498,-26.408 177.163,-26.8235 177.163,-26.8235\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132\" y=\"-53.8\">!a &amp; !b</text>\n",
242
243
244
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
245
246
247
        "<path d=\"M189.354,-128.581C187.743,-138.845 191.625,-148 201,-148 208.031,-148 211.973,-142.85 212.824,-135.945\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"212.646,-128.581 215.964,-135.502 212.73,-132.08 212.815,-135.579 212.815,-135.579 212.815,-135.579 212.73,-132.08 209.666,-135.655 212.646,-128.581 212.646,-128.581\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"201\" y=\"-150.8\">c &amp; d</text>\n",
248
249
250
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
251
252
        "<ellipse cx=\"453\" cy=\"-97\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-92.8\">2</text>\n",
253
254
255
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
256
257
258
        "<path d=\"M223.756,-123.11C253.134,-141.617 307.205,-168.999 354,-156 382.194,-148.168 410.398,-129.807 429.26,-115.631\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"435.285,-111.005 431.651,-117.767 432.509,-113.137 429.733,-115.268 429.733,-115.268 429.733,-115.268 432.509,-113.137 427.815,-112.769 435.285,-111.005 435.285,-111.005\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"327\" y=\"-161.8\">!c &amp; d</text>\n",
259
260
261
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
262
263
        "<ellipse cx=\"327\" cy=\"-97\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"327\" y=\"-92.8\">3</text>\n",
264
265
266
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
267
268
269
        "<path d=\"M232.07,-107.263C247.097,-106.701 265.541,-105.716 282,-104 285.657,-103.619 289.472,-103.138 293.262,-102.607\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"300.468,-101.539 294.006,-105.682 297.006,-102.052 293.544,-102.566 293.544,-102.566 293.544,-102.566 297.006,-102.052 293.082,-99.4497 300.468,-101.539 300.468,-101.539\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"266\" y=\"-108.8\">!d</text>\n",
270
271
272
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
273
274
275
        "<path d=\"M189.75,-34.6641C187.25,-44.625 191,-54 201,-54 208.5,-54 212.484,-48.7266 212.953,-41.8876\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"212.25,-34.6641 216.063,-41.3259 212.589,-38.1476 212.928,-41.6311 212.928,-41.6311 212.928,-41.6311 212.589,-38.1476 209.793,-41.9363 212.25,-34.6641 212.25,-34.6641\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"201\" y=\"-56.8\">1</text>\n",
276
277
278
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
279
280
281
        "<path d=\"M431.734,-85.7115C412.429,-75.649 382.208,-61.6629 354,-56 330.469,-51.2762 323.402,-50.6745 300,-56 274.353,-61.8365 248.181,-76.2435 229.343,-88.4163\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"223.246,-92.4432 227.351,-85.9567 226.167,-90.5141 229.087,-88.585 229.087,-88.585 229.087,-88.585 226.167,-90.5141 230.823,-91.2134 223.246,-92.4432 223.246,-92.4432\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"327\" y=\"-58.8\">c</text>\n",
282
283
284
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
285
286
287
        "<path d=\"M442.102,-113.664C439.68,-123.625 443.312,-133 453,-133 460.266,-133 464.125,-127.727 464.58,-120.888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"463.898,-113.664 467.692,-120.337 464.227,-117.149 464.556,-120.633 464.556,-120.633 464.556,-120.633 464.227,-117.149 461.42,-120.929 463.898,-113.664 463.898,-113.664\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-135.8\">!c</text>\n",
288
289
290
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
291
292
293
        "<path d=\"M302.562,-89.291C287.459,-85.3831 267.454,-82.1907 250,-86 244.078,-87.2925 238.012,-89.3852 232.273,-91.7783\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"225.713,-94.6958 230.829,-88.9729 228.911,-93.2735 232.109,-91.8511 232.109,-91.8511 232.109,-91.8511 228.911,-93.2735 233.389,-94.7293 225.713,-94.6958 225.713,-94.6958\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"266\" y=\"-88.8\">c &amp; d</text>\n",
294
295
296
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
297
298
299
        "<path d=\"M354.297,-97C373.039,-97 398.383,-97 418.562,-97\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"425.741,-97 418.741,-100.15 422.241,-97 418.741,-97.0001 418.741,-97.0001 418.741,-97.0001 422.241,-97 418.741,-93.8501 425.741,-97 425.741,-97\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"390\" y=\"-99.8\">!c &amp; d</text>\n",
300
301
302
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
303
304
305
        "<path d=\"M316.453,-113.664C314.109,-123.625 317.625,-133 327,-133 334.031,-133 337.767,-127.727 338.206,-120.888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"337.547,-113.664 341.32,-120.349 337.865,-117.15 338.183,-120.635 338.183,-120.635 338.183,-120.635 337.865,-117.15 335.046,-120.921 337.547,-113.664 337.547,-113.664\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"327\" y=\"-135.8\">!d</text>\n",
306
307
308
309
310
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
311
        "<IPython.core.display.SVG at 0x104c5a390>"
312
313
314
       ]
      }
     ],
315
     "prompt_number": 3
316
317
318
319
320
321
322
323
324
325
326
327
328
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.show(\".ast\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
329
       "prompt_number": 4,
330
       "svg": [
331
332
        "<svg height=\"352pt\" viewBox=\"0.00 0.00 424.00 351.80\" width=\"424pt\" 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.8)\">\n",
333
        "<title>G</title>\n",
334
335
336
337
        "<polygon fill=\"white\" points=\"-4,4 -4,-347.8 420,-347.8 420,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.312\" y=\"-329.6\">Inf(</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208.472\" y=\"-329.6\">\u24ff</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223.95\" y=\"-329.6\">)</text>\n",
338
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
339
        "<polygon fill=\"none\" points=\"144,-102 144,-311 408,-311 408,-102 144,-102\" stroke=\"green\"/>\n",
340
341
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
342
        "<polygon fill=\"none\" points=\"144,-8 144,-94 196,-94 196,-8 144,-8\" stroke=\"grey\"/>\n",
343
344
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
345
        "<polygon fill=\"none\" points=\"32,-18 32,-104 84,-104 84,-18 32,-18\" stroke=\"red\"/>\n",
346
347
348
349
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
350
351
        "<ellipse cx=\"58\" cy=\"-44\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-41.2\">0</text>\n",
352
353
354
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
355
356
        "<path d=\"M2.15778,-44C3.85328,-44 18.9155,-44 32.8257,-44\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"39.9179,-44 32.918,-47.1501 36.4179,-44 32.9179,-44.0001 32.9179,-44.0001 32.9179,-44.0001 36.4179,-44 32.9179,-40.8501 39.9179,-44 39.9179,-44\" stroke=\"black\"/>\n",
357
358
359
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
360
361
362
        "<path d=\"M51.6208,-61.0373C50.3189,-70.8579 52.4453,-80 58,-80 62.166,-80 64.4036,-74.8576 64.7128,-68.1433\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"64.3792,-61.0373 67.8541,-67.8818 64.5434,-64.5335 64.7076,-68.0296 64.7076,-68.0296 64.7076,-68.0296 64.5434,-64.5335 61.561,-68.1774 64.3792,-61.0373 64.3792,-61.0373\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"40.15\" y=\"-85.6\">a &amp; !b</text>\n",
363
364
365
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
366
367
        "<ellipse cx=\"170\" cy=\"-152\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170\" y=\"-149.2\">1</text>\n",
368
369
370
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
371
372
373
        "<path d=\"M71.6184,-56.389C91.2622,-75.6756 129.208,-112.931 151.489,-134.808\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"156.529,-139.756 149.327,-137.099 154.031,-137.303 151.534,-134.851 151.534,-134.851 151.534,-134.851 154.031,-137.303 153.741,-132.604 156.529,-139.756 156.529,-139.756\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.08\" y=\"-123.6\">b</text>\n",
374
375
376
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
377
378
        "<ellipse cx=\"170\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170\" y=\"-31.2\">4</text>\n",
379
380
381
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
382
383
384
        "<path d=\"M76.1875,-42.4375C94.5925,-40.7643 123.947,-38.0957 144.709,-36.2083\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"151.933,-35.5515 145.247,-39.3224 148.448,-35.8684 144.962,-36.1854 144.962,-36.1854 144.962,-36.1854 148.448,-35.8684 144.677,-33.0483 151.933,-35.5515 151.933,-35.5515\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.267\" y=\"-46.6\">!a &amp; !b</text>\n",
385
386
387
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
388
389
390
391
        "<path d=\"M161.021,-167.916C158.679,-178.15 161.672,-188 170,-188 176.376,-188 179.625,-182.226 179.746,-174.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"178.979,-167.916 182.872,-174.532 179.36,-171.395 179.741,-174.874 179.741,-174.874 179.741,-174.874 179.36,-171.395 176.61,-175.217 178.979,-167.916 178.979,-167.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"154.169\" y=\"-210.4\">c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162.262\" y=\"-193.6\">\u24ff</text>\n",
392
393
394
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
395
396
        "<ellipse cx=\"274\" cy=\"-198\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"274\" y=\"-195.2\">3</text>\n",
397
398
399
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
400
401
402
403
        "<path d=\"M187.918,-148.511C202.068,-146.463 222.387,-145.603 238,-153.4 247.778,-158.283 255.659,-167.322 261.449,-175.992\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"265.292,-182.176 258.921,-177.894 263.444,-179.203 261.597,-176.231 261.597,-176.231 261.597,-176.231 263.444,-179.203 264.272,-174.568 265.292,-182.176 265.292,-182.176\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216.197\" y=\"-176.4\">!d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.262\" y=\"-159.6\">\u24ff</text>\n",
404
405
406
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
407
408
        "<ellipse cx=\"382\" cy=\"-198\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"382\" y=\"-195.2\">2</text>\n",
409
410
411
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
412
413
414
415
        "<path d=\"M187.037,-145.938C210.568,-137.959 255.602,-126.185 292,-137.4 319.606,-145.906 346.314,-166.224 363.148,-180.995\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"368.466,-185.766 361.152,-183.436 365.861,-183.429 363.256,-181.091 363.256,-181.091 363.256,-181.091 365.861,-183.429 365.36,-178.747 368.466,-185.766 368.466,-185.766\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256.286\" y=\"-160.4\">!c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.262\" y=\"-143.6\">\u24ff</text>\n",
416
417
418
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
419
420
421
        "<path d=\"M255.86,-198.043C241.76,-197.429 221.627,-195.018 206,-187 198.624,-183.216 191.837,-177.313 186.243,-171.427\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"181.457,-166.086 188.475,-169.197 183.793,-168.693 186.129,-171.3 186.129,-171.3 186.129,-171.3 183.793,-168.693 183.783,-173.402 181.457,-166.086 181.457,-166.086\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.169\" y=\"-202.6\">c &amp; d</text>\n",
422
423
424
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
425
426
427
        "<path d=\"M265.021,-213.916C262.679,-224.15 265.672,-234 274,-234 280.376,-234 283.625,-228.226 283.746,-220.927\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"282.979,-213.916 286.872,-220.532 283.36,-217.395 283.741,-220.874 283.741,-220.874 283.741,-220.874 283.36,-217.395 280.61,-221.217 282.979,-213.916 282.979,-213.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"268.197\" y=\"-239.6\">!d</text>\n",
428
429
430
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
431
432
433
        "<path d=\"M292.031,-198C309.467,-198 336.737,-198 356.492,-198\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"363.659,-198 356.659,-201.15 360.159,-198 356.659,-198 356.659,-198 356.659,-198 360.159,-198 356.659,-194.85 363.659,-198 363.659,-198\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"310.286\" y=\"-203.6\">!c &amp; d</text>\n",
434
435
436
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
437
438
439
        "<path d=\"M369.298,-210.854C347.589,-233.06 299.336,-274.786 256,-259 217.982,-245.151 192.895,-202.266 180.382,-175.178\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"177.472,-168.659 183.202,-173.767 178.898,-171.855 180.325,-175.051 180.325,-175.051 180.325,-175.051 178.898,-171.855 177.449,-176.335 177.472,-168.659 177.472,-168.659\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270.658\" y=\"-267.6\">c</text>\n",
440
441
442
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
443
444
445
        "<path d=\"M372.767,-213.541C370.169,-223.909 373.246,-234 382,-234 388.702,-234 392.077,-228.085 392.124,-220.659\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"391.233,-213.541 395.229,-220.095 391.668,-217.014 392.103,-220.487 392.103,-220.487 392.103,-220.487 391.668,-217.014 388.977,-220.879 391.233,-213.541 391.233,-213.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376.774\" y=\"-239.6\">!c</text>\n",
446
447
448
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
449
450
451
        "<path d=\"M161.021,-49.916C158.679,-60.1504 161.672,-70 170,-70 176.376,-70 179.625,-64.2263 179.746,-56.9268\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"178.979,-49.916 182.872,-56.5315 179.36,-53.3952 179.741,-56.8744 179.741,-56.8744 179.741,-56.8744 179.36,-53.3952 176.61,-57.2174 178.979,-49.916 178.979,-49.916\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170\" y=\"-75.6\">1</text>\n",
452
453
454
455
456
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
457
        "<IPython.core.display.SVG at 0x106c689b0>"
458
459
460
       ]
      }
     ],
461
     "prompt_number": 4
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
    },
    {
     "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",
478
       "prompt_number": 5,
479
480
481
482
483
       "text": [
        "a U b"
       ]
      }
     ],
484
     "prompt_number": 5
485
486
487
488
489
490
491
492
493
494
495
496
497
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.translate(f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
498
       "prompt_number": 6,
499
500
501
502
       "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",
503
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
504
505
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
506
507
508
        "<svg width=\"188pt\" height=\"101pt\"\n",
        " viewBox=\"0.00 0.00 188.00 100.80\" 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 96.8)\">\n",
509
        "<title>G</title>\n",
510
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-96.8 184,-96.8 184,4 -4,4\"/>\n",
511
512
513
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
514
515
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-29\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-26.2\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
516
517
518
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
519
520
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-29C3.85328,-29 18.9155,-29 32.8257,-29\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-29 32.918,-32.1501 36.4179,-29 32.9179,-29.0001 32.9179,-29.0001 32.9179,-29.0001 36.4179,-29 32.9179,-25.8501 39.9179,-29 39.9179,-29\"/>\n",
521
522
523
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
524
525
526
        "<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-46.0373C50.3189,-55.8579 52.4453,-65 58,-65 62.166,-65 64.4036,-59.8576 64.7128,-53.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-46.0373 67.8541,-52.8818 64.5434,-49.5335 64.7076,-53.0296 64.7076,-53.0296 64.7076,-53.0296 64.5434,-49.5335 61.561,-53.1774 64.3792,-46.0373 64.3792,-46.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"40.15\" y=\"-70.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
527
528
529
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
530
531
532
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"150\" cy=\"-29\" rx=\"29.3314\" ry=\"29.3314\"/>\n",
        "<text text-anchor=\"start\" x=\"145.94\" y=\"-34.6\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"142.262\" y=\"-17.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
533
534
535
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
536
537
538
        "<path fill=\"none\" stroke=\"black\" d=\"M76.3529,-29C86.7716,-29 100.419,-29 113.068,-29\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"120.369,-29 113.369,-32.1501 116.869,-29 113.369,-29.0001 113.369,-29.0001 113.369,-29.0001 116.869,-29 113.369,-25.8501 120.369,-29 120.369,-29\"/>\n",
        "<text text-anchor=\"start\" x=\"94.08\" y=\"-34.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
539
540
541
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
542
543
544
        "<path fill=\"none\" stroke=\"black\" d=\"M140.271,-56.9857C139.952,-67.4151 143.195,-76 150,-76 155.104,-76 158.204,-71.171 159.3,-64.3566\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"159.729,-56.9857 162.467,-64.1568 159.525,-60.4798 159.322,-63.9739 159.322,-63.9739 159.322,-63.9739 159.525,-60.4798 156.177,-63.791 159.729,-56.9857 159.729,-56.9857\"/>\n",
        "<text text-anchor=\"middle\" x=\"150\" y=\"-81.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
545
546
547
548
549
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
550
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x106ca0060> >"
551
552
553
       ]
      }
     ],
554
     "prompt_number": 6
555
556
557
558
559
560
561
562
563
564
565
566
567
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
568
       "prompt_number": 7,
569
570
571
572
       "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",
573
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
574
575
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
576
577
578
        "<svg width=\"188pt\" height=\"101pt\"\n",
        " viewBox=\"0.00 0.00 188.00 100.80\" 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 96.8)\">\n",
579
        "<title>G</title>\n",
580
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-96.8 184,-96.8 184,4 -4,4\"/>\n",
581
582
583
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
584
585
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-29\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-26.2\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
586
587
588
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
589
590
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-29C3.85328,-29 18.9155,-29 32.8257,-29\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-29 32.918,-32.1501 36.4179,-29 32.9179,-29.0001 32.9179,-29.0001 32.9179,-29.0001 36.4179,-29 32.9179,-25.8501 39.9179,-29 39.9179,-29\"/>\n",
591
592
593
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
594
595
596
        "<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-46.0373C50.3189,-55.8579 52.4453,-65 58,-65 62.166,-65 64.4036,-59.8576 64.7128,-53.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-46.0373 67.8541,-52.8818 64.5434,-49.5335 64.7076,-53.0296 64.7076,-53.0296 64.7076,-53.0296 64.5434,-49.5335 61.561,-53.1774 64.3792,-46.0373 64.3792,-46.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"40.15\" y=\"-70.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
597
598
599
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
600
601
602
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"150\" cy=\"-29\" rx=\"29.3314\" ry=\"29.3314\"/>\n",
        "<text text-anchor=\"start\" x=\"145.94\" y=\"-34.6\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"142.262\" y=\"-17.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
603
604
605
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
606
607
608
        "<path fill=\"none\" stroke=\"black\" d=\"M76.3529,-29C86.7716,-29 100.419,-29 113.068,-29\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"120.369,-29 113.369,-32.1501 116.869,-29 113.369,-29.0001 113.369,-29.0001 113.369,-29.0001 116.869,-29 113.369,-25.8501 120.369,-29 120.369,-29\"/>\n",
        "<text text-anchor=\"start\" x=\"94.08\" y=\"-34.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
609
610
611
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
612
613
614
        "<path fill=\"none\" stroke=\"black\" d=\"M140.271,-56.9857C139.952,-67.4151 143.195,-76 150,-76 155.104,-76 158.204,-71.171 159.3,-64.3566\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"159.729,-56.9857 162.467,-64.1568 159.525,-60.4798 159.322,-63.9739 159.322,-63.9739 159.322,-63.9739 159.525,-60.4798 156.177,-63.791 159.729,-56.9857 159.729,-56.9857\"/>\n",
        "<text text-anchor=\"middle\" x=\"150\" y=\"-81.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
615
616
617
618
619
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
620
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x106ca0120> >"
621
622
623
       ]
      }
     ],
624
     "prompt_number": 7
625
626
627
628
629
630
631
632
633
634
635
636
637
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate('mon')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
638
       "prompt_number": 8,
639
640
641
642
       "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",
643
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
644
645
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
646
647
648
        "<svg width=\"164pt\" height=\"79pt\"\n",
        " viewBox=\"0.00 0.00 164.00 78.80\" 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 74.8)\">\n",
649
        "<title>G</title>\n",
650
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-74.8 160,-74.8 160,4 -4,4\"/>\n",
651
652
653
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
654
655
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
656
657
658
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
659
660
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-18C3.85328,-18 18.9155,-18 32.8257,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-18 32.918,-21.1501 36.4179,-18 32.9179,-18.0001 32.9179,-18.0001 32.9179,-18.0001 36.4179,-18 32.9179,-14.8501 39.9179,-18 39.9179,-18\"/>\n",
661
662
663
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
664
665
666
        "<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-35.0373C50.3189,-44.8579 52.4453,-54 58,-54 62.166,-54 64.4036,-48.8576 64.7128,-42.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-35.0373 67.8541,-41.8818 64.5434,-38.5335 64.7076,-42.0296 64.7076,-42.0296 64.7076,-42.0296 64.5434,-38.5335 61.561,-42.1774 64.3792,-35.0373 64.3792,-35.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"40.15\" y=\"-59.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
667
668
669
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
670
671
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"138\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"138\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
672
673
674
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
675
676
677
        "<path fill=\"none\" stroke=\"black\" d=\"M76.3107,-18C87.015,-18 100.916,-18 112.712,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"119.738,-18 112.738,-21.1501 116.238,-18 112.738,-18.0001 112.738,-18.0001 112.738,-18.0001 116.238,-18 112.738,-14.8501 119.738,-18 119.738,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"94.08\" y=\"-23.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
678
679
680
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
681
682
683
        "<path fill=\"none\" stroke=\"black\" d=\"M130.969,-34.6641C129.406,-44.625 131.75,-54 138,-54 142.688,-54 145.178,-48.7266 145.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"145.031,-34.6641 148.601,-41.4598 145.244,-38.1576 145.456,-41.6511 145.456,-41.6511 145.456,-41.6511 145.244,-38.1576 142.312,-41.8425 145.031,-34.6641 145.031,-34.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"138\" y=\"-59.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
684
685
686
687
688
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
689
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x106ca0030> >"
690
691
692
       ]
      }
     ],
693
     "prompt_number": 8
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
    },
    {
     "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",
710
       "prompt_number": 9,
711
712
713
714
715
       "text": [
        "Ga | Gb | Gc"
       ]
      }
     ],
716
     "prompt_number": 9
717
718
719
720
721
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
722
      "f.translate('ba', 'small').show('v')"
723
724
725
726
727
728
729
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
730
       "prompt_number": 10,
731
       "svg": [
732
733
        "<svg height=\"178pt\" viewBox=\"0.00 0.00 303.21 178.00\" width=\"303pt\" 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 174)\">\n",
734
        "<title>G</title>\n",
735
        "<polygon fill=\"white\" points=\"-4,4 -4,-174 299.214,-174 299.214,4 -4,4\" stroke=\"none\"/>\n",
736
737
738
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
739
740
        "<ellipse cx=\"135\" cy=\"-112\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"135\" y=\"-107.8\">0</text>\n",
741
742
743
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
744
745
        "<path d=\"M135,-167.842C135,-166.147 135,-151.084 135,-137.174\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"135,-130.082 138.15,-137.082 135,-133.582 135,-137.082 135,-137.082 135,-137.082 135,-133.582 131.85,-137.082 135,-130.082 135,-130.082\" stroke=\"black\"/>\n",
746
747
748
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
749
750
        "<ellipse cx=\"31\" cy=\"-22\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"31\" cy=\"-22\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
751
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"31\" y=\"-17.8\">1</text>\n",
752
753
754
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
755
756
757
        "<path d=\"M118.75,-97.25C101.976,-83.0562 75.5811,-60.7225 56.1175,-44.2532\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"50.3179,-39.3459 57.6963,-41.4628 52.9897,-41.6067 55.6616,-43.8675 55.6616,-43.8675 55.6616,-43.8675 52.9897,-41.6067 53.6269,-46.2722 50.3179,-39.3459 50.3179,-39.3459\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"96.1069\" y=\"-64.8\">a</text>\n",
758
759
760
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
761
762
763
        "<ellipse cx=\"135\" cy=\"-22\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"135\" cy=\"-22\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"135\" y=\"-17.8\">2</text>\n",
764
765
766
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
767
768
769
        "<path d=\"M135,-93.614C135,-81.5002 135,-65.0752 135,-51.1146\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"135,-44.0747 138.15,-51.0747 135,-47.5747 135,-51.0747 135,-51.0747 135,-51.0747 135,-47.5747 131.85,-51.0747 135,-44.0747 135,-44.0747\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"138.5\" y=\"-64.8\">b</text>\n",
770
771
772
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
773
774
775
        "<ellipse cx=\"240\" cy=\"-22\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"240\" cy=\"-22\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"240\" y=\"-17.8\">3</text>\n",
776
777
778
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
779
780
781
        "<path d=\"M151.406,-97.25C168.415,-82.995 195.22,-60.5298 214.895,-44.0406\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"220.496,-39.3459 217.155,-46.2565 217.814,-41.5941 215.131,-43.8423 215.131,-43.8423 215.131,-43.8423 217.814,-41.5941 213.108,-41.428 220.496,-39.3459 220.496,-39.3459\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"193.107\" y=\"-64.8\">c</text>\n",
782
783
784
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
785
786
        "<path d=\"M59.6885,-30.5913C70.7806,-30.9731 80,-28.1094 80,-22 80,-17.3225 74.5958,-14.5475 67.0844,-13.6751\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"59.6885,-13.4087 66.7974,-10.5128 63.1862,-13.5347 66.684,-13.6607 66.684,-13.6607 66.684,-13.6607 63.1862,-13.5347 66.5705,-16.8087 59.6885,-13.4087 59.6885,-13.4087\" stroke=\"black\"/>\n",
787
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"83.1069\" y=\"-17.8\">a</text>\n",
788
789
790
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
791
792
793
        "<path d=\"M163.689,-30.5913C174.781,-30.9731 184,-28.1094 184,-22 184,-17.3225 178.596,-14.5475 171.084,-13.6751\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"163.689,-13.4087 170.797,-10.5128 167.186,-13.5347 170.684,-13.6607 170.684,-13.6607 170.684,-13.6607 167.186,-13.5347 170.571,-16.8087 163.689,-13.4087 163.689,-13.4087\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"187.5\" y=\"-17.8\">b</text>\n",
794
795
796
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
797
798
799
        "<path d=\"M268.689,-30.5913C279.781,-30.9731 289,-28.1094 289,-22 289,-17.3225 283.596,-14.5475 276.084,-13.6751\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"268.689,-13.4087 275.797,-10.5128 272.186,-13.5347 275.684,-13.6607 275.684,-13.6607 275.684,-13.6607 272.186,-13.5347 275.571,-16.8087 268.689,-13.4087 268.689,-13.4087\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"292.107\" y=\"-17.8\">c</text>\n",
800
801
802
803
804
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
805
        "<IPython.core.display.SVG at 0x106ca70b8>"
806
807
808
       ]
      }
     ],
809
     "prompt_number": 10
810
811
812
813
814
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
815
      "f.translate('ba', 'det').show('v.')"
816
817
818
819
820
821
822
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
823
       "prompt_number": 11,
824
       "svg": [
825
826
        "<svg height=\"336pt\" viewBox=\"0.00 0.00 629.18 336.00\" width=\"629pt\" 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 332)\">\n",
827
        "<title>G</title>\n",
828
        "<polygon fill=\"white\" points=\"-4,4 -4,-332 625.177,-332 625.177,4 -4,4\" stroke=\"none\"/>\n",
829
830
831
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node2\"><title>6</title>\n",
832
833
834
        "<ellipse cx=\"303.89\" cy=\"-258\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"299.83\" y=\"-263.6\">6</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"296.152\" y=\"-246.8\">\u24ff</text>\n",
835
836
837
        "</g>\n",
        "<!-- I&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
838
839
        "<path d=\"M303.89,-325.951C303.89,-324.996 303.89,-310.097 303.89,-294.597\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"303.89,-287.481 307.04,-294.481 303.89,-290.981 303.89,-294.481 303.89,-294.481 303.89,-294.481 303.89,-290.981 300.74,-294.481 303.89,-287.481 303.89,-287.481\" stroke=\"black\"/>\n",
840
841
842
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
843
844
845
        "<path d=\"M331.876,-266.98C342.305,-267.275 350.89,-264.281 350.89,-258 350.89,-253.289 346.061,-250.428 339.247,-249.415\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"331.876,-249.02 339.035,-246.25 335.371,-249.207 338.866,-249.395 338.866,-249.395 338.866,-249.395 335.371,-249.207 338.697,-252.541 331.876,-249.02 331.876,-249.02\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"350.89\" y=\"-255.2\">a &amp; b &amp; c</text>\n",
846
847
848
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
849
850
851
        "<ellipse cx=\"111.89\" cy=\"-30\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.83\" y=\"-35.6\">0</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.152\" y=\"-18.8\">\u24ff</text>\n",
852
853
854
        "</g>\n",
        "<!-- 6&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
855
856
857
        "<path d=\"M275.051,-253.239C207.623,-243.795 42.9218,-216.734 10.603,-174 -5.48225,-152.731 -0.807273,-138.102 10.603,-114 24.8014,-84.0085 55.7344,-61.2356 79.7043,-47.1992\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"85.9465,-43.6466 81.4208,-49.8467 82.9046,-45.3778 79.8627,-47.109 79.8627,-47.109 79.8627,-47.109 82.9046,-45.3778 78.3047,-44.3713 85.9465,-43.6466 85.9465,-43.6466\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"10.89\" y=\"-141.2\">!a &amp; !b &amp; c</text>\n",
858
859
860
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
861
862
863
        "<ellipse cx=\"111.89\" cy=\"-144\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.83\" y=\"-149.6\">1</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.152\" y=\"-132.8\">\u24ff</text>\n",
864
865
866
        "</g>\n",
        "<!-- 6&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
867
868
869
        "<path d=\"M277.068,-245.829C256.668,-236.978 228.152,-223.837 204.369,-210 182.119,-197.055 158.391,-180.31 140.54,-167.059\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"134.723,-162.709 142.215,-164.378 137.526,-164.805 140.329,-166.901 140.329,-166.901 140.329,-166.901 137.526,-164.805 138.443,-169.424 134.723,-162.709 134.723,-162.709\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"204.89\" y=\"-198.2\">!a &amp; b &amp; c</text>\n",
870
871
872
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
873
874
875
        "<ellipse cx=\"350.89\" cy=\"-30\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"346.83\" y=\"-35.6\">2</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343.152\" y=\"-18.8\">\u24ff</text>\n",
876
877
878
        "</g>\n",
        "<!-- 6&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
879
880
881
        "<path d=\"M322.654,-235.426C328.202,-227.868 333.652,-219.007 336.89,-210 353.943,-162.562 355.038,-103.627 353.531,-66.6503\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"353.199,-59.5577 356.673,-66.4027 353.363,-63.0539 353.527,-66.5501 353.527,-66.5501 353.527,-66.5501 353.363,-63.0539 350.38,-66.6974 353.199,-59.5577 353.199,-59.5577\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"353.89\" y=\"-141.2\">!a &amp; b &amp; !c</text>\n",
882
883
884
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
885
886
887
        "<ellipse cx=\"461.89\" cy=\"-144\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"457.83\" y=\"-149.6\">3</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"454.152\" y=\"-132.8\">\u24ff</text>\n",
888
889
890
        "</g>\n",
        "<!-- 6&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
891
892
893
        "<path d=\"M327.544,-240.232C355.55,-220.381 402.203,-187.31 432.501,-165.833\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"438.333,-161.699 434.443,-168.317 435.477,-163.723 432.622,-165.747 432.622,-165.747 432.622,-165.747 435.477,-163.723 430.8,-163.177 438.333,-161.699 438.333,-161.699\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392.89\" y=\"-198.2\">a &amp; b &amp; !c</text>\n",
894
895
        "</g>\n",
        "<!-- 5 -->\n",
896
897
898
899
        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
        "<ellipse cx=\"500.89\" cy=\"-30\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"496.83\" y=\"-35.6\">5</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493.152\" y=\"-18.8\">\u24ff</text>\n",
900
901
902
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
        "<path d=\"M333.453,-257.359C387.299,-256.194 500.278,-244.944 548.89,-174 573.314,-138.355 546.314,-89.2538 524.032,-58.8496\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"519.655,-53.0276 526.38,-56.73 521.759,-55.8252 523.862,-58.6228 523.862,-58.6228 523.862,-58.6228 521.759,-55.8252 521.344,-60.5157 519.655,-53.0276 519.655,-53.0276\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"557.89\" y=\"-141.2\">a &amp; !b &amp; !c</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node8\"><title>4</title>\n",
        "<ellipse cx=\"237.89\" cy=\"-144\" fill=\"#ffffaa\" rx=\"29.1242\" ry=\"29.3314\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233.83\" y=\"-149.6\">4</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230.152\" y=\"-132.8\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
        "<path d=\"M289.406,-232.421C279.673,-215.904 266.763,-193.996 256.301,-176.243\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"252.568,-169.909 258.836,-174.34 254.345,-172.924 256.122,-175.939 256.122,-175.939 256.122,-175.939 254.345,-172.924 253.408,-177.539 252.568,-169.909 252.568,-169.909\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"274.89\" y=\"-198.2\">a &amp; !b &amp; c</text>\n",
918
919
920
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
921
922
923
924
925
926
927
928
929
        "<path d=\"M139.408,-40.459C150.047,-40.9238 158.89,-37.4375 158.89,-30 158.89,-24.3057 153.706,-20.9274 146.502,-19.8653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"139.408,-19.541 146.544,-16.7141 142.904,-19.7009 146.4,-19.8608 146.4,-19.8608 146.4,-19.8608 142.904,-19.7009 146.256,-23.0075 139.408,-19.541 139.408,-19.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158.89\" y=\"-27.2\">c</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
        "<path d=\"M111.89,-114.448C111.89,-99.9669 111.89,-82.2326 111.89,-66.8424\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"111.89,-59.5 115.04,-66.4999 111.89,-63 111.89,-66.5 111.89,-66.5 111.89,-66.5 111.89,-63 108.74,-66.5 111.89,-59.5 111.89,-59.5\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.89\" y=\"-84.2\">!b &amp; c</text>\n",
930
931
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
932
933
934
935
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
        "<path d=\"M139.408,-154.459C150.047,-154.924 158.89,-151.438 158.89,-144 158.89,-138.306 153.706,-134.927 146.502,-133.865\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"139.408,-133.541 146.544,-130.714 142.904,-133.701 146.4,-133.861 146.4,-133.861 146.4,-133.861 142.904,-133.701 146.256,-137.007 139.408,-133.541 139.408,-133.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158.89\" y=\"-141.2\">b &amp; c</text>\n",
936
        "</g>\n",
937
938
939
940
941
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
        "<path d=\"M130.191,-120.849C144.205,-104.389 162.734,-83.8202 172.463,-78 217.049,-51.3285 276.757,-39.5873 314.531,-34.5638\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"321.782,-33.6463 315.233,-37.6502 318.31,-34.0857 314.837,-34.5251 314.837,-34.5251 314.837,-34.5251 318.31,-34.0857 314.442,-31.4001 321.782,-33.6463 321.782,-33.6463\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172.89\" y=\"-84.2\">b &amp; !c</text>\n",
942
        "</g>\n",
943
944
945
946
947
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
        "<path d=\"M378.408,-40.459C389.047,-40.9238 397.89,-37.4375 397.89,-30 397.89,-24.3057 392.706,-20.9274 385.502,-19.8653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"378.408,-19.541 385.544,-16.7141 381.904,-19.7009 385.4,-19.8608 385.4,-19.8608 385.4,-19.8608 381.904,-19.7009 385.256,-23.0075 378.408,-19.541 378.408,-19.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"397.89\" y=\"-27.2\">b</text>\n",
948
        "</g>\n",
949
950
951
952
953
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
        "<path d=\"M448.642,-117.543C441.249,-104.792 431.245,-89.6343 419.89,-78 408.928,-66.7683 394.895,-56.6294 382.349,-48.6683\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"376.33,-44.9398 383.94,-45.9482 379.306,-46.7829 382.281,-48.626 382.281,-48.626 382.281,-48.626 379.306,-46.7829 380.622,-51.3039 376.33,-44.9398 376.33,-44.9398\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"434.89\" y=\"-84.2\">!a &amp; b</text>\n",
954
955
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
956
957
958
959
        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
        "<path d=\"M489.408,-154.459C500.047,-154.924 508.89,-151.438 508.89,-144 508.89,-138.306 503.706,-134.927 496.502,-133.865\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"489.408,-133.541 496.544,-130.714 492.904,-133.701 496.4,-133.861 496.4,-133.861 496.4,-133.861 492.904,-133.701 496.256,-137.007 489.408,-133.541 489.408,-133.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"508.89\" y=\"-141.2\">a &amp; b</text>\n",
960
        "</g>\n",
961
962
963
964
965
        "<!-- 3&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;5</title>\n",
        "<path d=\"M471.695,-116.191C474.076,-109.599 476.597,-102.552 478.89,-96 482.408,-85.9502 486.151,-74.995 489.533,-64.9915\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"491.81,-58.241 492.558,-65.8806 490.691,-61.5574 489.573,-64.8739 489.573,-64.8739 489.573,-64.8739 490.691,-61.5574 486.588,-63.8672 491.81,-58.241 491.81,-58.241\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484.89\" y=\"-84.2\">a &amp; !b</text>\n",
966
967
968
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
        "<path d=\"M528.408,-40.459C539.047,-40.9238 547.89,-37.4375 547.89,-30 547.89,-24.3057 542.706,-20.9274 535.502,-19.8653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"528.408,-19.541 535.544,-16.7141 531.904,-19.7009 535.4,-19.8608 535.4,-19.8608 535.4,-19.8608 531.904,-19.7009 535.256,-23.0075 528.408,-19.541 528.408,-19.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"547.89\" y=\"-27.2\">a</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
        "<path d=\"M231.745,-115.147C227.807,-102.566 221.562,-88.2583 211.89,-78 194.435,-59.4859 168.221,-47.5395 147.011,-40.3253\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"140.318,-38.147 147.949,-37.3181 143.646,-39.2302 146.974,-40.3135 146.974,-40.3135 146.974,-40.3135 143.646,-39.2302 146,-43.3088 140.318,-38.147 140.318,-38.147\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223.89\" y=\"-84.2\">!a &amp; c</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>4-&gt;5</title>\n",
        "<path d=\"M264.153,-130.615C292.785,-117.227 340.043,-95.4628 381.345,-78 409.948,-65.9064 442.806,-53.0627 466.826,-43.8634\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"473.668,-41.2499 468.253,-46.6903 470.399,-42.4987 467.129,-43.7476 467.129,-43.7476 467.129,-43.7476 470.399,-42.4987 466.005,-40.805 473.668,-41.2499 473.668,-41.2499\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381.89\" y=\"-84.2\">a &amp; !c</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;4</title>\n",
        "<path d=\"M265.408,-154.459C276.047,-154.924 284.89,-151.438 284.89,-144 284.89,-138.306 279.706,-134.927 272.502,-133.865\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"265.408,-133.541 272.544,-130.714 268.904,-133.701 272.4,-133.861 272.4,-133.861 272.4,-133.861 268.904,-133.701 272.256,-137.007 265.408,-133.541 265.408,-133.541\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"284.89\" y=\"-141.2\">a &amp; c</text>\n",
990
991
992
993
994
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
995
        "<IPython.core.display.SVG at 0x106cb6940>"
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
       ]
      }
     ],
     "prompt_number": 11
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = spot.translate('F(a & X(!a &Xb))', pref=\"any\"); a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
       "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",
1018
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
1019
1020
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
1021
1022
1023
        "<svg width=\"336pt\" height=\"96pt\"\n",
        " viewBox=\"0.00 0.00 336.00 95.60\" 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 91.5999)\">\n",
1024
        "<title>G</title>\n",
1025
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-91.5999 332,-91.5999 332,4 -4,4\"/>\n",
1026
1027
1028
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1029
1030
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1031
1032
1033
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1034
1035
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-18C3.85328,-18 18.9155,-18 32.8257,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-18 32.918,-21.1501 36.4179,-18 32.9179,-18.0001 32.9179,-18.0001 32.9179,-18.0001 36.4179,-18 32.9179,-14.8501 39.9179,-18 39.9179,-18\"/>\n",
1036
1037
1038
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
1039
1040
1041
        "<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-35.0373C50.3189,-44.8579 52.4453,-54 58,-54 62.166,-54 64.4036,-48.8576 64.7128,-42.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-35.0373 67.8541,-41.8818 64.5434,-38.5335 64.7076,-42.0296 64.7076,-42.0296 64.7076,-42.0296 64.5434,-38.5335 61.561,-42.1774 64.3792,-35.0373 64.3792,-35.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"53.94\" y=\"-59.6\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1042
1043
1044
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1045
1046
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"138\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"133.94\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1047
1048
1049
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1050
1051
1052
        "<path fill=\"none\" stroke=\"black\" d=\"M76.3107,-18C87.015,-18 100.916,-18 112.712,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"119.738,-18 112.738,-21.1501 116.238,-18 112.738,-18.0001 112.738,-18.0001 112.738,-18.0001 116.238,-18 112.738,-14.8501 119.738,-18 119.738,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"94.521\" y=\"-23.6\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
1053
1054
1055
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
1056
1057
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"222\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"222\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1058
1059
1060
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
1061
1062
1063
        "<path fill=\"none\" stroke=\"black\" d=\"M156.39,-18C168.101,-18 183.711,-18 196.654,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"203.916,-18 196.916,-21.1501 200.416,-18 196.916,-18.0001 196.916,-18.0001 196.916,-18.0001 200.416,-18 196.916,-14.8501 203.916,-18 203.916,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"174.638\" y=\"-23.6\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1064
1065
1066
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1067
1068
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"310\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"310\" y=\"-15.2\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1069
1070
1071
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1072
1073
1074
1075
        "<path fill=\"none\" stroke=\"black\" d=\"M240.403,-18C253.193,-18 270.732,-18 284.874,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"291.916,-18 284.916,-21.1501 288.416,-18 284.916,-18.0001 284.916,-18.0001 284.916,-18.0001 288.416,-18 284.916,-14.8501 291.916,-18 291.916,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"262.08\" y=\"-40.3999\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"258.262\" y=\"-23.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
1076
1077
1078
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
1079
1080
1081
1082
        "<path fill=\"none\" stroke=\"black\" d=\"M302.332,-34.2903C300.483,-44.3892 303.039,-54 310,-54 315.221,-54 317.964,-48.5939 318.229,-41.6304\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"317.668,-34.2903 321.342,-41.0299 317.935,-37.7801 318.201,-41.2699 318.201,-41.2699 318.201,-41.2699 317.935,-37.7801 315.06,-41.5099 317.668,-34.2903 317.668,-34.2903\"/>\n",
        "<text text-anchor=\"start\" x=\"305.94\" y=\"-76.3999\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"302.262\" y=\"-59.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
1083
1084
1085
1086
1087
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
1088
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x1052dcfc0> >"
1089
1090
1091
       ]
      }
     ],
1092
     "prompt_number": 12
1093
1094
1095
1096
    },
    {
     "cell_type": "code",
     "collapsed": false,
1097
1098
1099
     "input": [
      "spot.sl(a)"
     ],
1100
1101
     "language": "python",
     "metadata": {},
1102
1103
1104
1105
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
1106
       "prompt_number": 13,
1107
1108
1109
1110
       "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",
1111
        "<!-- Generated by graphviz version 2.36.0 (20140111.2315)\n",
1112
1113
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
1114
1115
1116
        "<svg width=\"734pt\" height=\"347pt\"\n",
        " viewBox=\"0.00 0.00 734.00 347.31\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.607616 0.607616) rotate(0) translate(4 567.6)\">\n",
1117
        "<title>G</title>\n",
1118
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-567.6 1204,-567.6 1204,4 -4,4\"/>\n",
1119
1120
1121
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
1122
1123
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-288\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"58\" y=\"-285.2\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
1124
1125
1126
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1127
1128
        "<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-288C3.85328,-288 18.9155,-288 32.8257,-288\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-288 32.918,-291.15 36.4179,-288 32.9179,-288 32.9179,-288 32.9179,-288 36.4179,-288 32.9179,-284.85 39.9179,-288 39.9179,-288\"/>\n",
1129
1130
1131
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
1132
1133
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"162\" cy=\"-230\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"162\" y=\"-227.2\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1134
1135
1136
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1137
1138
1139
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0505,-279.442C91.3766,-269.59 119.966,-253.333 139.601,-242.168\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"145.888,-238.593 141.36,-244.792 142.845,-240.323 139.803,-242.053 139.803,-242.053 139.803,-242.053 142.845,-240.323 138.246,-239.315 145.888,-238.593 145.888,-238.593\"/>\n",
        "<text text-anchor=\"start\" x=\"94.033\" y=\"-273.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
1140
1141
1142
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
1143
1144
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-286\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"272\" y=\"-283.2\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1145
1146
1147
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
1148
1149
1150
        "<path fill=\"none\" stroke=\"black\" d=\"M76.0315,-291.658C107.479,-297.841 176.684,-308.776 234,-299 238.78,-298.185 243.764,-296.817 248.468,-295.267\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.105,-292.909 249.563,-298.221 251.807,-294.081 248.509,-295.253 248.509,-295.253 248.509,-295.253 251.807,-294.081 247.454,-292.285 255.105,-292.909 255.105,-292.909\"/>\n",
        "<text text-anchor=\"start\" x=\"144.15\" y=\"-308.6\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
1151
1152
1153
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
1154
1155
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"388\" cy=\"-185\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"388\" y=\"-182.2\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
1156
1157
1158
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
1159
1160
1161
        "<path fill=\"none\" stroke=\"black\" d=\"M68.1212,-272.695C87.4899,-241.852 136.068,-172.817 198,-145.2 259.768,-117.656 289.159,-108.464 350,-138 360.882,-143.283 369.522,-153.489 375.706,-163.044\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"379.415,-169.171 373.095,-164.814 377.603,-166.177 375.79,-163.183 375.79,-163.183 375.79,-163.183 377.603,-166.177 378.485,-161.552 379.415,-169.171 379.415,-169.171\"/>\n",
        "<text text-anchor=\"start\" x=\"198.15\" y=\"-151.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
1162
1163
1164
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
1165
1166
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"502\" cy=\"-290\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"502\" y=\"-287.2\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
1167
1168
1169
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
1170
1171
1172
        "<path fill=\"none\" stroke=\"black\" d=\"M59.3883,-306.075C61.5384,-357.343 75.2276,-500 161,-500 161,-500 161,-500 331,-500 404.882,-500 431.279,-468.215 466,-403 481.22,-374.414 490.969,-338.17 496.213,-314.548\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"497.697,-307.645 499.305,-315.151 496.961,-311.067 496.226,-314.489 496.226,-314.489 496.226,-314.489 496.961,-311.067 493.146,-313.827 497.697,-307.645 497.697,-307.645\"/>\n",
        "<text text-anchor=\"start\" x=\"252.267\" y=\"-505.6\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
1173
1174
1175
        "</g>\n",
        "<!-- 5 -->\n",
        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
1176
1177
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"610\" cy=\"-162\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"610\" y=\"-159.2\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
1178
1179
1180
        "</g>\n",
        "<!-- 0&#45;&gt;5 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>0&#45;&gt;5</title>\n",
1181
1182
1183
        "<path fill=\"none\" stroke=\"black\" d=\"M61.3735,-269.984C70.1755,-206.934 103.448,-0 161,-0 161,-0 161,-0 503,-0 567.791,-0 595.11,-91.856 604.652,-137.232\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"606.084,-144.355 601.616,-138.113 605.394,-140.923 604.704,-137.492 604.704,-137.492 604.704,-137.492 605.394,-140.923 607.793,-136.871 606.084,-144.355 606.084,-144.355\"/>\n",
        "<text text-anchor=\"start\" x=\"314.033\" y=\"-5.59996\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
1184
1185
1186
        "</g>\n",
        "<!-- 6 -->\n",
        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
1187
1188
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"610\" cy=\"-290\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"610\" y=\"-287.2\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
1189
1190
1191
        "</g>\n",
        "<!-- 0&#45;&gt;6 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>0&#45;&gt;6</title>\n",
1192
1193
1194
        "<path fill=\"none\" stroke=\"black\" d=\"M60.539,-305.955C64.4936,-349.185 75.9828,-457.786 94,-489 113.401,-522.612 122.191,-545 161,-545 161,-545 161,-545 503,-545 601.591,-545 610.187,-380.458 609.754,-315.721\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"609.662,-308.339 612.899,-315.299 609.705,-311.839 609.749,-315.338 609.749,-315.338 609.749,-315.338 609.705,-311.839 606.599,-315.378 609.662,-308.339 609.662,-308.339\"/>\n",
        "<text text-anchor=\"start\" x=\"312.15\" y=\"-550.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
1195
1196
1197
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1198
1199
1200
        "<path fill=\"none\" stroke=\"black\" d=\"M153.021,-245.916C150.679,-256.15 153.672,-266 162,-266 168.376,-266 171.625,-260.226 171.746,-252.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"170.979,-245.916 174.872,-252.532 171.36,-249.395 171.741,-252.874 171.741,-252.874 171.741,-252.874 171.36,-249.395 168.61,-253.217 170.979,-245.916 170.979,-245.916\"/>\n",
        "<text text-anchor=\"start\" x=\"146.033\" y=\"-271.6\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
1201
1202
1203
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
1204
1205
1206
        "<path fill=\"none\" stroke=\"black\" d=\"M174.