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
21
  "name": "",
  "signature": "sha256:8277d563756e7b9333f4900705ae07524e2902b49f4c79ceb40739a865a177c4"
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
63
64
65
       "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",
66
67
68
        "<svg width=\"429pt\" height=\"191pt\"\n",
        " viewBox=\"0.00 0.00 428.74 191.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 187)\">\n",
69
        "<title>G</title>\n",
70
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-187 424.74,-187 424.74,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=\"56\" cy=\"-73\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-69.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
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=\"M1.15491,-73C2.79388,-73 17.1543,-73 30.6317,-73\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-73 30.9419,-76.1501 34.4419,-73 30.9419,-73.0001 30.9419,-73.0001 30.9419,-73.0001 34.4419,-73 30.9418,-69.8501 37.9419,-73 37.9419,-73\"/>\n",
81
82
83
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
84
85
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-90.0373C48.3189,-99.8579 50.4453,-109 56,-109 60.166,-109 62.4036,-103.858 62.7128,-97.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-90.0373 65.8541,-96.8818 62.5434,-93.5335 62.7076,-97.0296 62.7076,-97.0296 62.7076,-97.0296 62.5434,-93.5335 59.561,-97.1774 62.3792,-90.0373 62.3792,-90.0373\"/>\n",
86
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-112.8\" 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=\"177.87\" cy=\"-114\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"173.37\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"169.87\" y=\"-102.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
        "<path fill=\"none\" stroke=\"black\" d=\"M73.1662,-78.5294C91.6622,-84.8558 122.386,-95.3645 145.603,-103.305\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"152.239,-105.575 144.597,-106.29 148.928,-104.443 145.616,-103.31 145.616,-103.31 145.616,-103.31 148.928,-104.443 146.636,-100.329 152.239,-105.575 152.239,-105.575\"/>\n",
98
        "<text text-anchor=\"start\" x=\"108\" y=\"-102.8\" 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=\"177.87\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"177.87\" y=\"-14.3\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M72.6709,-65.8097C93.5799,-56.216 130.728,-39.1714 154.557,-28.2381\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"161.195,-25.1921 156.147,-30.9743 158.014,-26.6517 154.833,-28.1113 154.833,-28.1113 154.833,-28.1113 158.014,-26.6517 153.519,-25.2483 161.195,-25.1921 161.195,-25.1921\"/>\n",
109
        "<text text-anchor=\"start\" x=\"92\" y=\"-60.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M166.755,-138.917C165.845,-149.666 169.55,-158.87 177.87,-158.87 184.24,-158.87 187.905,-153.475 188.865,-146.122\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"188.985,-138.917 192.018,-145.969 188.927,-142.416 188.868,-145.916 188.868,-145.916 188.868,-145.916 188.927,-142.416 185.719,-145.863 188.985,-138.917 188.985,-138.917\"/>\n",
115
        "<text text-anchor=\"start\" x=\"160.87\" y=\"-162.67\" 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=\"402.74\" cy=\"-104\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"402.74\" y=\"-100.3\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M199.294,-130.585C225.134,-149.491 271.166,-176.285 311.74,-164 339.514,-155.591 366.551,-135.471 383.621,-120.843\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"389.014,-116.117 385.825,-123.1 386.382,-118.424 383.749,-120.73 383.749,-120.73 383.749,-120.73 386.382,-118.424 381.674,-118.361 389.014,-116.117 389.014,-116.117\"/>\n",
126
        "<text text-anchor=\"start\" x=\"274.74\" y=\"-171.8\" 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=\"293.24\" cy=\"-104\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"293.24\" y=\"-100.3\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M204.905,-114.011C220.073,-113.765 239.54,-113.015 256.74,-111 260.466,-110.564 264.386,-109.95 268.205,-109.265\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"275.351,-107.89 269.073,-112.306 271.915,-108.551 268.478,-109.213 268.478,-109.213 268.478,-109.213 271.915,-108.551 267.882,-106.12 275.351,-107.89 275.351,-107.89\"/>\n",
137
        "<text text-anchor=\"start\" x=\"233.24\" y=\"-117.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M167.719,-33.1666C164.643,-43.6641 168.026,-54 177.87,-54 185.407,-54 189.157,-47.9413 189.12,-40.39\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"188.021,-33.1666 192.188,-39.6135 188.548,-36.6269 189.074,-40.0871 189.074,-40.0871 189.074,-40.0871 188.548,-36.6269 185.96,-40.5607 188.021,-33.1666 188.021,-33.1666\"/>\n",
143
        "<text text-anchor=\"middle\" x=\"177.87\" y=\"-57.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M387.536,-93.9733C364.34,-78.8215 316.703,-52.7835 274.74,-62 249.65,-67.5106 224.229,-81.784 205.874,-93.9852\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"199.93,-98.0279 203.947,-91.4863 202.824,-96.0594 205.718,-94.0909 205.718,-94.0909 205.718,-94.0909 202.824,-96.0594 207.49,-96.6954 199.93,-98.0279 199.93,-98.0279\"/>\n",
149
        "<text text-anchor=\"start\" x=\"289.74\" y=\"-65.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M393.507,-119.541C390.909,-129.909 393.986,-140 402.74,-140 409.442,-140 412.817,-134.085 412.865,-126.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"411.973,-119.541 415.969,-126.095 412.408,-123.014 412.843,-126.487 412.843,-126.487 412.843,-126.487 412.408,-123.014 409.718,-126.879 411.973,-119.541 411.973,-119.541\"/>\n",
155
        "<text text-anchor=\"start\" x=\"397.24\" y=\"-143.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M276.265,-97.366C270.254,-95.2005 263.288,-93.0768 256.74,-92 241.829,-89.548 237.445,-88.5195 222.74,-92 217.724,-93.1873 212.628,-95.0421 207.771,-97.1827\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"201.326,-100.243 206.298,-94.395 204.487,-98.7417 207.649,-97.2406 207.649,-97.2406 207.649,-97.2406 204.487,-98.7417 209,-100.086 201.326,-100.243 201.326,-100.243\"/>\n",
161
        "<text text-anchor=\"start\" x=\"222.74\" y=\"-95.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M311.512,-104C329.378,-104 357.426,-104 377.507,-104\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"384.511,-104 377.511,-107.15 381.011,-104 377.511,-104 377.511,-104 377.511,-104 381.011,-104 377.511,-100.85 384.511,-104 384.511,-104\"/>\n",
167
        "<text text-anchor=\"start\" x=\"329.74\" y=\"-107.8\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M284.261,-119.916C281.919,-130.15 284.912,-140 293.24,-140 299.616,-140 302.865,-134.226 302.987,-126.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"302.219,-119.916 306.112,-126.532 302.6,-123.395 302.981,-126.874 302.981,-126.874 302.981,-126.874 302.6,-123.395 299.85,-127.217 302.219,-119.916 302.219,-119.916\"/>\n",
173
        "<text text-anchor=\"start\" x=\"286.74\" y=\"-143.8\" 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 0x7f87301e0180> >"
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=\"186pt\" viewBox=\"0.00 0.00 488.00 186.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 182)\">\n",
201
        "<title>G</title>\n",
202
203
204
205
206
207
208
209
210
        "<polygon fill=\"white\" points=\"-4,4 -4,-182 484,-182 484,4 -4,4\" stroke=\"none\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
        "<ellipse cx=\"65\" cy=\"-69\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"65\" y=\"-65.3\">0</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
211
212
        "<path d=\"M1.04566,-69C1.94863,-69 16.101,-69 30.7579,-69\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9378,-69 30.9378,-72.1501 34.4378,-69 30.9378,-69.0001 30.9378,-69.0001 30.9378,-69.0001 34.4378,-69 30.9378,-65.8501 37.9378,-69 37.9378,-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
        "<path d=\"M57.1448,-86.4099C55.6785,-96.0879 58.2969,-105 65,-105 69.9226,-105 72.6423,-100.194 73.1591,-93.8073\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"72.8552,-86.4099 76.2899,-93.2747 72.9989,-89.9069 73.1426,-93.404 73.1426,-93.404 73.1426,-93.404 72.9989,-89.9069 69.9953,-93.5333 72.8552,-86.4099 72.8552,-86.4099\" stroke=\"black\"/>\n",
218
219
220
221
222
223
224
225
226
227
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"65\" y=\"-108.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
        "<ellipse cx=\"200\" cy=\"-109\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"200\" cy=\"-109\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"200\" y=\"-105.3\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
228
229
        "<path d=\"M89.7777,-76.1512C110.587,-82.4097 141.076,-91.5792 164.556,-98.6409\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"171.288,-100.666 163.678,-101.666 167.937,-99.6576 164.585,-98.6495 164.585,-98.6495 164.585,-98.6495 167.937,-99.6576 165.492,-95.633 171.288,-100.666 171.288,-100.666\" stroke=\"black\"/>\n",
230
231
232
233
234
235
236
237
238
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"130.5\" y=\"-96.8\">b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
        "<ellipse cx=\"200\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"200\" y=\"-14.3\">4</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
239
240
        "<path d=\"M88.8635,-60.2328C111.131,-51.6942 145.085,-38.6741 169.404,-29.3489\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"175.99,-26.8235 170.582,-32.271 172.722,-28.0766 169.454,-29.3298 169.454,-29.3298 169.454,-29.3298 172.722,-28.0766 168.326,-26.3886 175.99,-26.8235 175.99,-26.8235\" stroke=\"black\"/>\n",
241
242
243
244
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"130.5\" y=\"-54.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
245
246
        "<path d=\"M188.354,-129.581C186.743,-139.845 190.625,-149 200,-149 207.031,-149 210.973,-143.85 211.824,-136.945\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"211.646,-129.581 214.964,-136.502 211.73,-133.08 211.815,-136.579 211.815,-136.579 211.815,-136.579 211.73,-133.08 208.666,-136.655 211.646,-129.581 211.646,-129.581\" stroke=\"black\"/>\n",
247
248
249
250
251
252
253
254
255
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"200\" y=\"-152.8\">c &amp; d</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
        "<ellipse cx=\"453\" cy=\"-99\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-95.3\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
256
257
        "<path d=\"M222.782,-123.932C241.9,-136.075 270.957,-152.26 299,-159 322.335,-164.609 329.885,-165.458 353,-159 381.944,-150.914 410.852,-131.803 429.891,-117.306\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"435.472,-112.972 431.875,-119.753 432.708,-115.119 429.943,-117.265 429.943,-117.265 429.943,-117.265 432.708,-115.119 428.011,-114.777 435.472,-112.972 435.472,-112.972\" stroke=\"black\"/>\n",
258
259
260
261
262
263
264
265
266
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-166.8\">!c &amp; d</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
        "<ellipse cx=\"326\" cy=\"-99\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-95.3\">3</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
267
268
        "<path d=\"M231.069,-108.727C246.096,-108.374 264.539,-107.612 281,-106 284.659,-105.642 288.476,-105.175 292.266,-104.653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"299.474,-103.594 293.006,-107.728 296.011,-104.102 292.548,-104.611 292.548,-104.611 292.548,-104.611 296.011,-104.102 292.09,-101.495 299.474,-103.594 299.474,-103.594\" stroke=\"black\"/>\n",
269
270
271
272
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"265\" y=\"-111.8\">!d</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
273
274
        "<path d=\"M188.75,-34.6641C186.25,-44.625 190,-54 200,-54 207.5,-54 211.484,-48.7266 211.953,-41.8876\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"211.25,-34.6641 215.063,-41.3259 211.589,-38.1476 211.928,-41.6311 211.928,-41.6311 211.928,-41.6311 211.589,-38.1476 208.793,-41.9363 211.25,-34.6641 211.25,-34.6641\" stroke=\"black\"/>\n",
275
276
277
278
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"200\" y=\"-57.8\">1</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
279
280
        "<path d=\"M431.922,-87.6352C412.452,-77.3145 381.724,-62.8411 353,-57 329.481,-52.2175 322.402,-51.6745 299,-57 273.353,-62.8365 247.181,-77.2435 228.343,-89.4163\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"222.246,-93.4432 226.351,-86.9567 225.167,-91.5141 228.087,-89.585 228.087,-89.585 228.087,-89.585 225.167,-91.5141 229.823,-92.2134 222.246,-93.4432 222.246,-93.4432\" stroke=\"black\"/>\n",
281
282
283
284
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-60.8\">c</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
285
286
        "<path d=\"M442.102,-115.664C439.68,-125.625 443.312,-135 453,-135 460.266,-135 464.125,-129.727 464.58,-122.888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"463.898,-115.664 467.692,-122.337 464.227,-119.149 464.556,-122.633 464.556,-122.633 464.556,-122.633 464.227,-119.149 461.42,-122.929 463.898,-115.664 463.898,-115.664\" stroke=\"black\"/>\n",
287
288
289
290
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-138.8\">!c</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
291
292
        "<path d=\"M301.585,-90.8211C286.491,-86.65 266.488,-83.1832 249,-87 243.078,-88.2925 237.012,-90.3852 231.273,-92.7783\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"224.713,-95.6958 229.829,-89.9729 227.911,-94.2735 231.109,-92.8511 231.109,-92.8511 231.109,-92.8511 227.911,-94.2735 232.389,-95.7293 224.713,-95.6958 224.713,-95.6958\" stroke=\"black\"/>\n",
293
294
295
296
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"265\" y=\"-90.8\">c &amp; d</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
297
298
        "<path d=\"M353.204,-99C372.288,-99 398.281,-99 418.815,-99\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"425.83,-99 418.83,-102.15 422.33,-99 418.83,-99.0001 418.83,-99.0001 418.83,-99.0001 422.33,-99 418.83,-95.8501 425.83,-99 425.83,-99\" stroke=\"black\"/>\n",
299
300
301
302
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"389.5\" y=\"-102.8\">!c &amp; d</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
303
304
        "<path d=\"M315.453,-115.664C313.109,-125.625 316.625,-135 326,-135 333.031,-135 336.767,-129.727 337.206,-122.888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"336.547,-115.664 340.32,-122.349 336.865,-119.15 337.183,-122.635 337.183,-122.635 337.183,-122.635 336.865,-119.15 334.046,-122.921 336.547,-115.664 336.547,-115.664\" stroke=\"black\"/>\n",
305
306
307
308
309
310
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-138.8\">!d</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
311
        "<IPython.core.display.SVG at 0x7f873301c0f0>"
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
        "<svg height=\"342pt\" viewBox=\"0.00 0.00 427.00 342.00\" width=\"427pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
332
333
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 338)\">\n",
        "<title>G</title>\n",
334
335
336
337
        "<polygon fill=\"white\" points=\"-4,4 -4,-338 423,-338 423,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-319.8\">Inf(</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-319.8\">\u24ff</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-319.8\">)</text>\n",
338
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
339
        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
340
341
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
342
        "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
343
344
345
346
347
348
349
        "</g>\n",
        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" points=\"30,-18 30,-103 82,-103 82,-18 30,-18\" stroke=\"red\"/>\n",
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
350
        "<ellipse cx=\"56\" cy=\"-44\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
351
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.3\">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=\"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",
357
358
359
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
360
361
        "<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",
362
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-83.8\">a &amp; !b</text>\n",
363
364
365
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
366
        "<ellipse cx=\"169\" cy=\"-151\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
367
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-147.3\">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
        "<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",
373
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-120.8\">b</text>\n",
374
375
376
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
377
        "<ellipse cx=\"169\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
378
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">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
        "<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",
384
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-44.8\">!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
        "<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",
390
391
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-205.8\">c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-190.8\">\u24ff</text>\n",
392
393
394
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
395
396
        "<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\">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
        "<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",
402
403
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-170.8\">!d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-155.8\">\u24ff</text>\n",
404
405
406
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
407
408
        "<ellipse cx=\"385\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"385\" y=\"-189.3\">2</text>\n",
409
410
411
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
412
413
        "<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",
414
415
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-154.8\">!c &amp; d</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-139.8\">\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
        "<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",
421
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-195.8\">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
        "<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",
427
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-232.8\">!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
        "<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",
433
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-196.8\">!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
        "<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",
439
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-259.8\">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
        "<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",
445
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-232.8\">!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
        "<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",
451
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
452
453
454
455
456
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
457
        "<IPython.core.display.SVG at 0x7f8730135c88>"
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
503
504
505
       "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",
506
507
508
        "<svg width=\"181pt\" height=\"95pt\"\n",
        " viewBox=\"0.00 0.00 180.74 94.74\" 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 90.7401)\">\n",
509
        "<title>G</title>\n",
510
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-90.7401 176.74,-90.7401 176.74,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=\"56\" cy=\"-26.8701\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-23.1701\" 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=\"M1.15491,-26.8701C2.79388,-26.8701 17.1543,-26.8701 30.6317,-26.8701\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-26.8701 30.9419,-30.0202 34.4419,-26.8701 30.9419,-26.8702 30.9419,-26.8702 30.9419,-26.8702 34.4419,-26.8701 30.9418,-23.7202 37.9419,-26.8701 37.9419,-26.8701\"/>\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
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-43.9074C48.3189,-53.728 50.4453,-62.8701 56,-62.8701 60.166,-62.8701 62.4036,-57.7276 62.7128,-51.0134\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-43.9074 65.8541,-50.7519 62.5434,-47.4035 62.7076,-50.8997 62.7076,-50.8997 62.7076,-50.8997 62.5434,-47.4035 59.561,-51.0474 62.3792,-43.9074 62.3792,-43.9074\"/>\n",
526
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-66.6701\" 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=\"145.87\" cy=\"-26.8701\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"141.37\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"137.87\" y=\"-15.6701\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M74.3603,-26.8701C84.98,-26.8701 98.9179,-26.8701 111.595,-26.8701\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.879,-26.8701 111.88,-30.0202 115.379,-26.8701 111.879,-26.8702 111.879,-26.8702 111.879,-26.8702 115.379,-26.8701 111.879,-23.7202 118.879,-26.8701 118.879,-26.8701\"/>\n",
538
        "<text text-anchor=\"start\" x=\"92\" y=\"-30.6701\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M136.949,-52.2401C136.334,-62.7939 139.308,-71.7401 145.87,-71.7401 150.894,-71.7401 153.815,-66.496 154.632,-59.3013\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"154.791,-52.2401 157.783,-59.3092 154.712,-55.7392 154.633,-59.2383 154.633,-59.2383 154.633,-59.2383 154.712,-55.7392 151.484,-59.1674 154.791,-52.2401 154.791,-52.2401\"/>\n",
544
        "<text text-anchor=\"middle\" x=\"145.87\" y=\"-75.5401\" 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 0x7f87301b6990> >"
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
573
574
575
       "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",
576
577
578
        "<svg width=\"181pt\" height=\"95pt\"\n",
        " viewBox=\"0.00 0.00 180.74 94.74\" 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 90.7401)\">\n",
579
        "<title>G</title>\n",
580
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-90.7401 176.74,-90.7401 176.74,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=\"56\" cy=\"-26.8701\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-23.1701\" 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=\"M1.15491,-26.8701C2.79388,-26.8701 17.1543,-26.8701 30.6317,-26.8701\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-26.8701 30.9419,-30.0202 34.4419,-26.8701 30.9419,-26.8702 30.9419,-26.8702 30.9419,-26.8702 34.4419,-26.8701 30.9418,-23.7202 37.9419,-26.8701 37.9419,-26.8701\"/>\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
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-43.9074C48.3189,-53.728 50.4453,-62.8701 56,-62.8701 60.166,-62.8701 62.4036,-57.7276 62.7128,-51.0134\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-43.9074 65.8541,-50.7519 62.5434,-47.4035 62.7076,-50.8997 62.7076,-50.8997 62.7076,-50.8997 62.5434,-47.4035 59.561,-51.0474 62.3792,-43.9074 62.3792,-43.9074\"/>\n",
596
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-66.6701\" 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=\"145.87\" cy=\"-26.8701\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"141.37\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"137.87\" y=\"-15.6701\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M74.3603,-26.8701C84.98,-26.8701 98.9179,-26.8701 111.595,-26.8701\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.879,-26.8701 111.88,-30.0202 115.379,-26.8701 111.879,-26.8702 111.879,-26.8702 111.879,-26.8702 115.379,-26.8701 111.879,-23.7202 118.879,-26.8701 118.879,-26.8701\"/>\n",
608
        "<text text-anchor=\"start\" x=\"92\" y=\"-30.6701\" 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
        "<path fill=\"none\" stroke=\"black\" d=\"M136.949,-52.2401C136.334,-62.7939 139.308,-71.7401 145.87,-71.7401 150.894,-71.7401 153.815,-66.496 154.632,-59.3013\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"154.791,-52.2401 157.783,-59.3092 154.712,-55.7392 154.633,-59.2383 154.633,-59.2383 154.633,-59.2383 154.712,-55.7392 151.484,-59.1674 154.791,-52.2401 154.791,-52.2401\"/>\n",
614
        "<text text-anchor=\"middle\" x=\"145.87\" y=\"-75.5401\" 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 0x7f87301b6bd0> >"
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
643
644
645
       "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",
646
647
        "<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",
648
649
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 73)\">\n",
        "<title>G</title>\n",
650
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
651
652
653
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
654
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
655
        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" 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=\"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",
661
662
663
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
664
665
        "<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",
666
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" 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=\"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",
672
673
674
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
675
676
        "<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",
677
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" 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
        "<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",
683
        "<text text-anchor=\"middle\" x=\"137\" y=\"-57.8\" 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 0x7f87301b6a20> >"
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
        "<svg height=\"177pt\" viewBox=\"0.00 0.00 305.00 177.00\" width=\"305pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
733
734
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
        "<title>G</title>\n",
735
        "<polygon fill=\"white\" points=\"-4,4 -4,-173 301,-173 301,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=\"136\" cy=\"-113\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"136\" y=\"-109.3\">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=\"M136,-167.845C136,-166.206 136,-151.846 136,-138.368\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"136,-131.058 139.15,-138.058 136,-134.558 136,-138.058 136,-138.058 136,-138.058 136,-134.558 132.85,-138.058 136,-131.058 136,-131.058\" stroke=\"black\"/>\n",
746
747
748
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
749
750
751
        "<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",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"31\" y=\"-18.3\">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
        "<path d=\"M119.594,-98.0938C102.512,-83.6149 75.5496,-60.7611 55.8524,-44.0653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"50.5036,-39.5316 57.8803,-41.6549 53.1736,-41.7947 55.8435,-44.0578 55.8435,-44.0578 55.8435,-44.0578 53.1736,-41.7947 53.8067,-46.4608 50.5036,-39.5316 50.5036,-39.5316\" stroke=\"black\"/>\n",
757
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"96.5\" y=\"-65.8\">c</text>\n",
758
759
760
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
761
762
763
        "<ellipse cx=\"136\" cy=\"-22\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"136\" cy=\"-22\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"136\" y=\"-18.3\">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
        "<path d=\"M136,-94.8399C136,-82.5378 136,-65.6842 136,-51.3928\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"136,-44.1905 139.15,-51.1905 136,-47.6905 136,-51.1905 136,-51.1905 136,-51.1905 136,-47.6905 132.85,-51.1906 136,-44.1905 136,-44.1905\" stroke=\"black\"/>\n",
769
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"139.5\" y=\"-65.8\">a</text>\n",
770
771
772
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
773
774
775
        "<ellipse cx=\"241\" cy=\"-22\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
        "<ellipse cx=\"241\" cy=\"-22\" fill=\"none\" rx=\"31\" ry=\"22\" stroke=\"black\"/>\n",
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"241\" y=\"-18.3\">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
        "<path d=\"M152.406,-98.0938C169.488,-83.6149 196.45,-60.7611 216.148,-44.0653\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"221.496,-39.5316 218.193,-46.4608 218.826,-41.7947 216.157,-44.0578 216.157,-44.0578 216.157,-44.0578 218.826,-41.7947 214.12,-41.6549 221.496,-39.5316 221.496,-39.5316\" stroke=\"black\"/>\n",
781
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"197.5\" y=\"-65.8\">b</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.5\" y=\"-18.3\">c</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
        "<path d=\"M164.689,-30.5913C175.781,-30.9731 185,-28.1094 185,-22 185,-17.3225 179.596,-14.5475 172.084,-13.6751\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"164.689,-13.4087 171.797,-10.5128 168.186,-13.5347 171.684,-13.6607 171.684,-13.6607 171.684,-13.6607 168.186,-13.5347 171.571,-16.8087 164.689,-13.4087 164.689,-13.4087\" stroke=\"black\"/>\n",
793
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"188.5\" y=\"-18.3\">a</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
        "<path d=\"M269.689,-30.5913C280.781,-30.9731 290,-28.1094 290,-22 290,-17.3225 284.596,-14.5475 277.084,-13.6751\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"269.689,-13.4087 276.797,-10.5128 273.186,-13.5347 276.684,-13.6607 276.684,-13.6607 276.684,-13.6607 273.186,-13.5347 276.571,-16.8087 269.689,-13.4087 269.689,-13.4087\" stroke=\"black\"/>\n",
799
        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"293.5\" y=\"-18.3\">b</text>\n",
800
801
802
803
804
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
805
        "<IPython.core.display.SVG at 0x7f87300b6cc0>"
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=\"309pt\" viewBox=\"0.00 0.00 629.71 309.22\" width=\"630pt\" 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 305.22)\">\n",
827
        "<title>G</title>\n",
828
        "<polygon fill=\"white\" points=\"-4,4 -4,-305.22 625.706,-305.22 625.706,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=\"300.706\" cy=\"-236.35\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"296.206\" y=\"-240.15\">6</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292.706\" y=\"-225.15\">\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=\"M300.706,-300.175C300.706,-299.274 300.706,-285.15 300.706,-270.524\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"300.706,-263.359 303.856,-270.359 300.706,-266.859 300.706,-270.359 300.706,-270.359 300.706,-270.359 300.706,-266.859 297.556,-270.359 300.706,-263.359 300.706,-263.359\" 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
        "<path d=\"M326.527,-244.55C336.884,-245.013 345.576,-242.28 345.576,-236.35 345.576,-231.903 340.687,-229.254 333.873,-228.403\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"326.527,-228.151 333.631,-225.242 330.025,-228.271 333.523,-228.391 333.523,-228.391 333.523,-228.391 330.025,-228.271 333.415,-231.539 326.527,-228.151 326.527,-228.151\" stroke=\"black\"/>\n",
845
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.576\" y=\"-232.65\">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.706\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.206\" y=\"-30.6701\">0</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.706\" y=\"-15.6701\">\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
        "<path d=\"M274.072,-232.409C208.518,-224.565 42.3069,-200.811 9.70612,-158.48 -4.86736,-139.557 -0.950588,-126.115 9.70612,-104.74 24.4189,-75.2291 56.4579,-54.0645 80.7287,-41.5079\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"87.0313,-38.348 82.1855,-44.3013 83.9025,-39.9167 80.7737,-41.4853 80.7737,-41.4853 80.7737,-41.4853 83.9025,-39.9167 79.3619,-38.6694 87.0313,-38.348 87.0313,-38.348\" stroke=\"black\"/>\n",
857
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"9.70612\" y=\"-127.91\">!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=\"348.706\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344.206\" y=\"-30.6701\">1</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.706\" y=\"-15.6701\">\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
        "<path d=\"M319.29,-216.332C325.246,-209.113 331.201,-200.456 334.706,-191.48 351.387,-148.77 352.634,-95.147 351.256,-61.1816\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"350.904,-53.8257 354.385,-60.667 351.071,-57.3217 351.238,-60.8177 351.238,-60.8177 351.238,-60.8177 351.071,-57.3217 348.092,-60.9684 350.904,-53.8257 350.904,-53.8257\" stroke=\"black\"/>\n",
869
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351.706\" y=\"-127.91\">!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=\"500.706\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"496.206\" y=\"-30.6701\">2</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"492.706\" y=\"-15.6701\">\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
        "<path d=\"M327.292,-231.204C385.67,-221.486 521.925,-195.254 547.706,-158.48 570.566,-125.873 544.331,-80.9412 522.857,-53.1817\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"518.367,-47.5294 525.187,-51.0507 520.544,-50.2698 522.721,-53.0102 522.721,-53.0102 522.721,-53.0102 520.544,-50.2698 520.255,-54.9697 518.367,-47.5294 518.367,-47.5294\" stroke=\"black\"/>\n",
881
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"555.706\" y=\"-127.91\">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=\"111.706\" cy=\"-131.61\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.206\" y=\"-135.41\">3</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.706\" y=\"-120.41\">\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
        "<path d=\"M275.502,-226.223C254.239,-218.148 223.271,-205.495 197.706,-191.48 177.075,-180.17 155.215,-165.162 138.697,-153.129\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"132.865,-148.843 140.371,-150.451 135.685,-150.916 138.506,-152.989 138.506,-152.989 138.506,-152.989 135.685,-150.916 136.64,-155.527 132.865,-148.843 132.865,-148.843\" stroke=\"black\"/>\n",
893
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"197.706\" y=\"-180.28\">!a &amp; b &amp; c</text>\n",
894
895
896
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node7\"><title>4</title>\n",
897
898
899
        "<ellipse cx=\"459.706\" cy=\"-131.61\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"455.206\" y=\"-135.41\">4</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"451.706\" y=\"-120.41\">\u24ff</text>\n",
900
901
902
        "</g>\n",
        "<!-- 6&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
903
904
        "<path d=\"M322.814,-221.065C351.213,-202.714 400.533,-170.846 431.577,-150.786\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"437.53,-146.94 433.36,-153.384 434.59,-148.839 431.65,-150.739 431.65,-150.739 431.65,-150.739 434.59,-148.839 429.941,-148.093 437.53,-146.94 437.53,-146.94\" stroke=\"black\"/>\n",
905
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"390.706\" y=\"-180.28\">a &amp; b &amp; !c</text>\n",
906
907
908
        "</g>\n",
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node8\"><title>5</title>\n",
909
910
911
        "<ellipse cx=\"235.706\" cy=\"-131.61\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.206\" y=\"-135.41\">5</text>\n",
        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"227.706\" y=\"-120.41\">\u24ff</text>\n",
912
913
914
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
915
916
        "<path d=\"M286.432,-213.052C282.021,-206.144 277.154,-198.503 272.706,-191.48 266.401,-181.525 259.524,-170.602 253.429,-160.897\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"249.55,-154.718 255.94,-158.972 251.411,-157.682 253.272,-160.647 253.272,-160.647 253.272,-160.647 251.411,-157.682 250.604,-162.321 249.55,-154.718 249.55,-154.718\" stroke=\"black\"/>\n",
917
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272.706\" y=\"-180.28\">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
        "<path d=\"M137.076,-36.5344C147.63,-37.2009 156.576,-33.9794 156.576,-26.8701 156.576,-21.4269 151.332,-18.2629 144.137,-17.3778\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.076,-17.2058 144.151,-14.2273 140.575,-17.2911 144.074,-17.3764 144.074,-17.3764 144.074,-17.3764 140.575,-17.2911 143.997,-20.5254 137.076,-17.2058 137.076,-17.2058\" stroke=\"black\"/>\n",
923
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.576\" y=\"-23.1701\">c</text>\n",
924
925
926
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
927
928
        "<path d=\"M374.076,-36.5344C384.63,-37.2009 393.576,-33.9794 393.576,-26.8701 393.576,-21.4269 388.332,-18.2629 381.137,-17.3778\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"374.076,-17.2058 381.151,-14.2273 377.575,-17.2911 381.074,-17.3764 381.074,-17.3764 381.074,-17.3764 377.575,-17.2911 380.997,-20.5254 374.076,-17.2058 374.076,-17.2058\" stroke=\"black\"/>\n",
929
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"393.576\" y=\"-23.1701\">b</text>\n",
930
931
932
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
933
934
        "<path d=\"M526.076,-36.5344C536.63,-37.2009 545.576,-33.9794 545.576,-26.8701 545.576,-21.4269 540.332,-18.2629 533.137,-17.3778\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"526.076,-17.2058 533.151,-14.2273 529.575,-17.2911 533.074,-17.3764 533.074,-17.3764 533.074,-17.3764 529.575,-17.2911 532.997,-20.5254 526.076,-17.2058 526.076,-17.2058\" stroke=\"black\"/>\n",
935
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"545.576\" y=\"-23.1701\">a</text>\n",
936
937
938
        "</g>\n",
        "<!-- 3&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>3-&gt;0</title>\n",
939
940
        "<path d=\"M111.706,-104.685C111.706,-91.4217 111.706,-75.1317 111.706,-60.9711\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"111.706,-53.7874 114.856,-60.7874 111.706,-57.2874 111.706,-60.7874 111.706,-60.7874 111.706,-60.7874 111.706,-57.2874 108.556,-60.7875 111.706,-53.7874 111.706,-53.7874\" stroke=\"black\"/>\n",
941
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.706\" y=\"-75.5401\">!b &amp; c</text>\n",
942
943
944
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;1</title>\n",
945
946
        "<path d=\"M129.367,-110.824C143.115,-95.8501 161.377,-76.9951 170.706,-71.7401 216.462,-45.9673 277.181,-35.1927 314.566,-30.7893\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"321.721,-29.991 315.113,-33.8979 318.242,-30.3791 314.764,-30.7673 314.764,-30.7673 314.764,-30.7673 318.242,-30.3791 314.415,-27.6367 321.721,-29.991 321.721,-29.991\" stroke=\"black\"/>\n",
947
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"170.706\" y=\"-75.5401\">b &amp; !c</text>\n",
948
949
950
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
951
952
        "<path d=\"M137.076,-141.274C147.63,-141.941 156.576,-138.72 156.576,-131.61 156.576,-126.167 151.332,-123.003 144.137,-122.118\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.076,-121.946 144.151,-118.967 140.575,-122.031 144.074,-122.116 144.074,-122.116 144.074,-122.116 140.575,-122.031 143.997,-125.266 137.076,-121.946 137.076,-121.946\" stroke=\"black\"/>\n",
953
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.576\" y=\"-127.91\">b &amp; c</text>\n",
954
955
956
        "</g>\n",
        "<!-- 4&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;1</title>\n",
957
958
        "<path d=\"M446.809,-107.722C439.535,-96.0823 429.708,-82.2209 418.706,-71.7401 406.926,-60.5183 391.842,-50.6276 378.694,-43.0919\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"372.418,-39.5861 380.065,-40.2499 375.474,-41.293 378.529,-42.9999 378.529,-42.9999 378.529,-42.9999 375.474,-41.293 376.993,-45.75 372.418,-39.5861 372.418,-39.5861\" stroke=\"black\"/>\n",
959
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432.706\" y=\"-75.5401\">!a &amp; b</text>\n",
960
961
962
        "</g>\n",
        "<!-- 4&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
963
964
        "<path d=\"M470.382,-106.567C473.158,-100.153 476.1,-93.2065 478.706,-86.7401 482.314,-77.789 486.056,-67.9953 489.407,-59.0099\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"491.885,-52.3236 492.406,-59.9821 490.669,-55.6054 489.452,-58.8873 489.452,-58.8873 489.452,-58.8873 490.669,-55.6054 486.499,-57.7924 491.885,-52.3236 491.885,-52.3236\" stroke=\"black\"/>\n",
965
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484.706\" y=\"-75.5401\">a &amp; !b</text>\n",
966
967
968
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
969
970
        "<path d=\"M485.076,-141.274C495.63,-141.941 504.576,-138.72 504.576,-131.61 504.576,-126.167 499.332,-123.003 492.137,-122.118\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"485.076,-121.946 492.151,-118.967 488.575,-122.031 492.074,-122.116 492.074,-122.116 492.074,-122.116 488.575,-122.031 491.997,-125.266 485.076,-121.946 485.076,-121.946\" stroke=\"black\"/>\n",
971
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"504.576\" y=\"-127.91\">a &amp; b</text>\n",
972
973
974
        "</g>\n",
        "<!-- 5&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;0</title>\n",
975
976
        "<path d=\"M230.039,-105.277C226.405,-93.8588 220.639,-80.9116 211.706,-71.7401 193.563,-53.1133 166.156,-41.853 144.62,-35.4125\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"137.853,-33.4876 145.448,-32.3732 141.22,-34.4453 144.586,-35.403 144.586,-35.403 144.586,-35.403 141.22,-34.4453 143.724,-38.4328 137.853,-33.4876 137.853,-33.4876\" stroke=\"black\"/>\n",
977
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222.706\" y=\"-75.5401\">!a &amp; c</text>\n",
978
979
980
        "</g>\n",
        "<!-- 5&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;2</title>\n",
981
982
        "<path d=\"M260.115,-120.166C288.475,-108.124 336.745,-87.9124 378.706,-71.7401 409.038,-60.0499 443.975,-47.5875 468.667,-38.9447\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"475.348,-36.6121 469.777,-41.8937 472.043,-37.7659 468.739,-38.9197 468.739,-38.9197 468.739,-38.9197 472.043,-37.7659 467.7,-35.9458 475.348,-36.6121 475.348,-36.6121\" stroke=\"black\"/>\n",
983
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378.706\" y=\"-75.5401\">a &amp; !c</text>\n",
984
985
986
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
987
988
        "<path d=\"M261.076,-141.274C271.63,-141.941 280.576,-138.72 280.576,-131.61 280.576,-126.167 275.332,-123.003 268.137,-122.118\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"261.076,-121.946 268.151,-118.967 264.575,-122.031 268.074,-122.116 268.074,-122.116 268.074,-122.116 264.575,-122.031 267.997,-125.266 261.076,-121.946 261.076,-121.946\" stroke=\"black\"/>\n",
989
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"280.576\" y=\"-127.91\">a &amp; c</text>\n",
990
991
992
993
994
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
995
        "<IPython.core.display.SVG at 0x7f87300d64e0>"
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
       ]
      }
     ],
     "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",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
        "<svg width=\"332pt\" height=\"92pt\"\n",
        " viewBox=\"0.00 0.00 332.00 92.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 88)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-88 328,-88 328,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</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=\"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",
1036
1037
1038
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
1039
1040
        "<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",
1041
1042
1043
1044
1045
1046
1047
1048
1049
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"130.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1050
1051
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0888,-18C84.5562,-18 98.1196,-18 109.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"116.959,-18 109.959,-21.1501 113.459,-18 109.959,-18.0001 109.959,-18.0001 109.959,-18.0001 113.459,-18 109.959,-14.8501 116.959,-18 116.959,-18\"/>\n",
1052
1053
1054
1055
1056
1057
1058
1059
1060
        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
1061
1062
        "<path fill=\"none\" stroke=\"black\" d=\"M153.178,-18C164.669,-18 179.959,-18 192.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"199.847,-18 192.847,-21.1501 196.347,-18 192.847,-18.0001 192.847,-18.0001 192.847,-18.0001 196.347,-18 192.847,-14.8501 199.847,-18 199.847,-18\"/>\n",
1063
1064
1065
1066
1067
1068
1069
1070
1071
        "<text text-anchor=\"start\" x=\"171\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"306\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"306\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1072
1073
        "<path fill=\"none\" stroke=\"black\" d=\"M236.403,-18C249.193,-18 266.732,-18 280.874,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"287.916,-18 280.916,-21.1501 284.416,-18 280.916,-18.0001 280.916,-18.0001 280.916,-18.0001 284.416,-18 280.916,-14.8501 287.916,-18 287.916,-18\"/>\n",
1074
1075
1076
1077
1078
        "<text text-anchor=\"start\" x=\"257.5\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
1079
1080
        "<path fill=\"none\" stroke=\"black\" d=\"M298.332,-34.2903C296.483,-44.3892 299.039,-54 306,-54 311.221,-54 313.964,-48.5939 314.229,-41.6304\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"313.668,-34.2903 317.342,-41.0299 313.935,-37.7801 314.201,-41.2699 314.201,-41.2699 314.201,-41.2699 313.935,-37.7801 311.06,-41.5099 313.668,-34.2903 313.668,-34.2903\"/>\n",
1081
1082
1083
1084
1085
1086
1087
        "<text text-anchor=\"start\" x=\"301.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"298\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</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 0x7f87301b6cc0> >"
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
1111
1112
1113
       "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",
1114
1115
1116
        "<svg width=\"734pt\" height=\"335pt\"\n",
        " viewBox=\"0.00 0.00 734.00 334.60\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.601793 0.601793) rotate(0) translate(4 552)\">\n",
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-552 1215.69,-552 1215.69,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-282\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-278.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
1127
1128
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-282C2.79388,-282 17.1543,-282 30.6317,-282\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-282 30.9419,-285.15 34.4419,-282 30.9419,-282 30.9419,-282 30.9419,-282 34.4419,-282 30.9418,-278.85 37.9419,-282 37.9419,-282\"/>\n",
1129
1130
1131
1132
1133
1134
1135
1136
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"162.5\" cy=\"-225\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"162.5\" y=\"-221.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
1137
1138
        "<path fill=\"none\" stroke=\"black\" d=\"M72.4193,-273.589C90.3498,-263.809 120.054,-247.607 140.185,-236.627\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"146.357,-233.26 141.72,-239.377 143.285,-234.936 140.212,-236.612 140.212,-236.612 140.212,-236.612 143.285,-234.936 138.703,-233.846 146.357,-233.26 146.357,-233.26\"/>\n",
1139
1140
1141
1142
1143
1144
1145
1146
1147
        "<text text-anchor=\"start\" x=\"92\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"274.5\" cy=\"-282\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"274.5\" y=\"-278.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
1148
1149
        "<path fill=\"none\" stroke=\"black\" d=\"M73.874,-285.312C105.727,-291.062 176.828,-301.499 236,-293 240.783,-292.313 245.807,-291.157 250.568,-289.846\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"257.296,-287.851 251.48,-292.861 253.94,-288.846 250.585,-289.841 250.585,-289.841 250.585,-289.841 253.94,-288.846 249.689,-286.821 257.296,-287.851 257.296,-287.851\"/>\n",
1150
1151
1152
1153
1154
1155
1156
1157
1158
        "<text text-anchor=\"start\" x=\"144\" y=\"-299.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"392.5\" cy=\"-182\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"392.5\" y=\"-178.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
1159
1160
        "<path fill=\"none\" stroke=\"black\" d=\"M66.4817,-266.974C86.5703,-236.695 136.724,-168.943 199,-142 262.31,-114.61 292.001,-103.76 354,-134 365.071,-139.4 373.832,-149.824 380.091,-159.582\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"383.843,-165.838 377.542,-161.455 382.043,-162.836 380.243,-159.835 380.243,-159.835 380.243,-159.835 382.043,-162.836 382.945,-158.215 383.843,-165.838 383.843,-165.838\"/>\n",
1161
1162
1163
1164
1165
1166
1167
1168
1169
        "<text text-anchor=\"start\" x=\"199\" y=\"-145.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"508.5\" cy=\"-283\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"508.5\" y=\"-279.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
1170
1171
        "<path fill=\"none\" stroke=\"black\" d=\"M57.7109,-300.095C60.7583,-350.7 76.8361,-490 161.5,-490 161.5,-490 161.5,-490 334.5,-490 409.803,-490 436.423,-457.369 472,-391 486.472,-364.002 496.445,-330.044 502.054,-307.488\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"503.722,-300.589 505.139,-308.133 502.9,-303.991 502.077,-307.393 502.077,-307.393 502.077,-307.393 502.9,-303.991 499.015,-306.653 503.722,-300.589 503.722,-300.589\"/>\n",
1172
1173
1174
1175
1176
1177
1178
1179
1180
        "<text text-anchor=\"start\" x=\"254\" y=\"-493.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"618\" cy=\"-159\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"618\" y=\"-155.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;5 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>0&#45;&gt;5</title>\n",
1181
1182
        "<path fill=\"none\" stroke=\"black\" d=\"M59.5927,-264.36C69.1541,-202.623 104.85,-0 161.5,-0 161.5,-0 161.5,-0 509.5,-0 573.575,-0 602.045,-89.7125 612.246,-134.362\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"613.783,-141.377 609.207,-135.213 613.034,-137.958 612.285,-134.539 612.285,-134.539 612.285,-134.539 613.034,-137.958 615.362,-133.865 613.783,-141.377 613.783,-141.377\"/>\n",
1183
1184
1185
1186
1187
1188
1189
1190
1191
        "<text text-anchor=\"start\" x=\"316.5\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"618\" cy=\"-283\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"618\" y=\"-279.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;6 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>0&#45;&gt;6</title>\n",
1192
1193
        "<path fill=\"none\" stroke=\"black\" d=\"M56.3587,-300.051C55.3315,-357.603 60.4873,-533 161.5,-533 161.5,-533 161.5,-533 509.5,-533 606.428,-533 617.041,-372.437 617.433,-308.663\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"617.435,-301.383 620.583,-308.384 617.434,-304.883 617.433,-308.383 617.433,-308.383 617.433,-308.383 617.434,-304.883 614.283,-308.382 617.435,-301.383 617.435,-301.383\"/>\n",
1194
1195
1196
1197
        "<text text-anchor=\"start\" x=\"315\" y=\"-536.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
1198
1199
        "<path fill=\"none\" stroke=\"black\" d=\"M153.521,-240.916C151.179,-251.15 154.172,-261 162.5,-261 168.876,-261 172.125,-255.226 172.246,-247.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.479,-240.916 175.372,-247.532 171.86,-244.395 172.241,-247.874 172.241,-247.874 172.241,-247.874 171.86,-244.395 169.11,-248.217 171.479,-240.916 171.479,-240.916\"/>\n",
1200
1201
1202
1203
        "<text text-anchor=\"start\" x=\"145.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
1204
1205
        "<path fill=\"none\" stroke=\"black\" d=\"M174.399,-238.625C180.859,-245.896 189.606,-254.461 199,-260 214.575,-269.182 234.268,-274.781 249.495,-278.031\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"256.574,-279.443 249.093,-281.163 253.141,-278.758 249.709,-278.073 249.709,-278.073 249.709,-278.073 253.141,-278.758 250.325,-274.984 256.574,-279.443 256.574,-279.443\"/>\n",
1206
1207
1208
1209
        "<text text-anchor=\"start\" x=\"199\" y=\"-277.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
1210
1211
        "<path fill=\"none\" stroke=\"black\" d=\"M180.265,-221.838C220.288,-214.29 321.514,-195.199 367.775,-186.474\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"374.71,-185.167 368.415,-189.559 371.271,-185.815 367.831,-186.464 367.831,-186.464 367.831,-186.464 371.271,-185.815 367.247,-183.368 374.71,-185.167 374.71,-185.167\"/>\n",
1212
1213
1214
1215
        "<text text-anchor=\"start\" x=\"256\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
1216
1217
        "<path fill=\"none\" stroke=\"black\" d=\"M172.479,-209.649C178.749,-200.27 187.958,-188.807 199,-182 280.605,-131.693 320.87,-128.502 413,-155 442.746,-163.556 452.659,-167.835 472,-192 487.02,-210.766 481.177,-220.641 490,-243 492.191,-248.553 494.69,-254.474 497.1,-260.012\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"500.076,-266.765 494.371,-261.63 498.665,-263.563 497.253,-260.36 497.253,-260.36 497.253,-260.36 498.665,-263.563 500.136,-259.09 500.076,-266.765 500.076,-266.765\"/>\n",
1218
1219
1220
1221
        "<text text-anchor=\"start\" x=\"313\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;5 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>1&#45;&gt;5</title>\n",
1222
1223
        "<path fill=\"none\" stroke=\"black\" d=\"M168.516,-208.006C173.818,-192.756 183.579,-170.722 199,-157 218.547,-139.606 228.567,-142.149 254,-136 371.942,-107.483 406.242,-121.118 527,-133 551.471,-135.408 558.612,-131.407 582,-139 586.83,-140.568 591.734,-142.854 596.282,-145.325\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"602.64,-149.015 595.005,-148.226 599.613,-147.258 596.586,-145.501 596.586,-145.501 596.586,-145.501 599.613,-147.258 598.167,-142.777 602.64,-149.015 602.64,-149.015\"/>\n",
1224
1225
1226
1227
        "<text text-anchor=\"start\" x=\"375.5\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;6 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>1&#45;&gt;6</title>\n",
1228
1229
        "<path fill=\"none\" stroke=\"black\" d=\"M168.227,-242.485C175.273,-267.677 188.792,-312.631 199,-326 234.13,-372.011 256.369,-376.996 313,-389 382.136,-403.654 403.101,-406.733 472,-391 524.906,-378.919 541.436,-374.049 582,-338 592.089,-329.034 600.373,-316.487 606.345,-305.64\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"609.76,-299.154 609.286,-306.815 608.129,-302.251 606.499,-305.348 606.499,-305.348 606.499,-305.348 608.129,-302.251 603.711,-303.88 609.76,-299.154 609.76,-299.154\"/>\n",
1230
1231
1232
1233
        "<text text-anchor=\"start\" x=\"374\" y=\"-404.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge14\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
1234
1235
        "<path fill=\"none\" stroke=\"black\" d=\"M263.695,-267.344C256.944,-258.393 247.194,-247.463 236,-241 221.361,-232.548 202.695,-228.557 187.969,-226.674\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"180.67,-225.869 187.973,-223.506 184.149,-226.253 187.628,-226.637 187.628,-226.637 187.628,-226.637 184.149,-226.253 187.282,-229.768 180.67,-225.869 180.67,-225.869\"/>\n",
1236
1237
1238
1239
        "<text text-anchor=\"start\" x=\"200.5\" y=\"-244.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge15\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
1240
1241
        "<path fill=\"none\" stroke=\"black\" d=\"M264.925,-297.541C262.23,-307.909 265.422,-318 274.5,-318 281.45,-318 284.95,-312.085 284.999,-304.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"284.075,-297.541 288.1,-304.077 284.526,-301.012 284.977,-304.483 284.977,-304.483 284.977,-304.483 284.526,-301.012 281.853,-304.889 284.075,-297.541 284.075,-297.541\"/>\n",
1242
1243
1244
1245
        "<text text-anchor=\"start\" x=\"256\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge16\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1246
1247
        "<path fill=\"none\" stroke=\"black\" d=\"M283.767,-266.383C290.49,-254.757 300.835,-239.052 313,-228 328.464,-213.95 335.98,-215.575 354,-205 359.397,-201.833 365.181,-198.337 370.551,-195.047\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"376.617,-191.312 372.308,-197.664 373.637,-193.147 370.657,-194.982 370.657,-194.982 370.657,-194.982 373.637,-193.147 369.005,-192.3 376.617,-191.312 376.617,-191.312\"/>\n",
1248
1249
1250
1251
        "<text text-anchor=\"start\" x=\"315\" y=\"-231.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
        "<g id=\"edge17\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
1252
1253
        "<path fill=\"none\" stroke=\"black\" d=\"M292.56,-282.074C333.285,-282.249 436.286,-282.693 483.359,-282.896\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"490.415,-282.926 483.402,-286.046 486.916,-282.911 483.416,-282.896 483.416,-282.896 483.416,-282.896 486.916,-282.911 483.429,-279.746 490.415,-282.926 490.415,-282.926\"/>\n",
1254
1255
1256
1257
        "<text text-anchor=\"start\" x=\"372\" y=\"-285.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g id=\"edge18\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
1258
1259
        "<path fill=\"none\" stroke=\"black\" d=\"M280.75,-264.887C286.653,-247.539 297.486,-220.539 313,-201 333.676,-174.96 341.248,-167.646 372,-155 447.842,-123.811 548.384,-141.861 593.424,-152.68\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"600.416,-154.41 592.864,-155.787 597.019,-153.569 593.621,-152.729 593.621,-152.729 593.621,-152.729 597.019,-153.569 594.378,-149.671 600.416,-154.41 600.416,-154.41\"/>\n",
1260
1261
1262
1263
        "<text text-anchor=\"start\" x=\"434.5\" y=\"-143.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;6 -->\n",
        "<g id=\"edge19\" class=\"edge\"><title>2&#45;&gt;6</title>\n",
1264
1265
        "<path fill=\"none\" stroke=\"black\" d=\"M287.591,-294.625C294.456,-301.07 303.549,-308.484 313,-313 399.658,-354.404 435.08,-370.831 527,-343 554.774,-334.591 581.811,-314.471 598.881,-299.843\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"604.274,-295.117 601.085,-302.1 601.642,-297.424 599.009,-299.73 599.009,-299.73 599.009,-299.73 601.642,-297.424 596.933,-297.361 604.274,-295.117 604.274,-295.117\"/>\n",
1266
1267
1268
1269
        "<text text-anchor=\"start\" x=\"433\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge20\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
1270
1271