automata-io.ipynb 46.4 KB
Newer Older
1
2
{
 "metadata": {
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
18
   "version": "3.4.3+"
19
  },
20
21
  "name": "",
  "signature": "sha256:79ee85572b2a0147d88b2d3d355977e3f34dadb82bd7e8589bdbb2cf2a539b0b"
22
23
24
25
26
27
28
29
30
31
32
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "from IPython.display import display\n",
33
34
      "import spot\n",
      "spot.setup()"
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = spot.translate('a U b')\n",
      "for fmt in ('hoa', 'spin', 'dot', 'lbtt'):\n",
      "    print(a.to_str(fmt))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "HOA: v1\n",
        "States: 2\n",
        "Start: 1\n",
        "AP: 2 \"a\" \"b\"\n",
        "acc-name: Buchi\n",
        "Acceptance: 1 Inf(0)\n",
        "properties: trans-labels explicit-labels state-acc deterministic\n",
63
        "properties: stutter-invariant terminal\n",
64
65
66
67
68
69
70
71
72
73
        "--BODY--\n",
        "State: 0 {0}\n",
        "[t] 0\n",
        "State: 1\n",
        "[1] 0\n",
        "[0&!1] 1\n",
        "--END--\n",
        "never {\n",
        "T0_init:\n",
        "  if\n",
74
        "  :: (b) -> goto accept_all\n",
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
        "  :: ((a) && (!(b))) -> goto T0_init\n",
        "  fi;\n",
        "accept_all:\n",
        "  skip\n",
        "}\n",
        "\n",
        "digraph G {\n",
        "  rankdir=LR\n",
        "  node [shape=\"circle\"]\n",
        "  fontname=\"Lato\"\n",
        "  node [fontname=\"Lato\"]\n",
        "  edge [fontname=\"Lato\"]\n",
        "  size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]\n",
        "  I [label=\"\", style=invis, width=0]\n",
        "  I -> 1\n",
90
        "  0 [label=\"0\", peripheries=2]\n",
91
        "  0 -> 0 [label=<1>]\n",
92
        "  1 [label=\"1\"]\n",
93
94
95
96
        "  1 -> 0 [label=<b>]\n",
        "  1 -> 1 [label=<a &amp; !b>]\n",
        "}\n",
        "\n",
97
98
99
100
        "2 1\n",
        "0 1 -1\n",
        "1 \"b\"\n",
        "0 & \"a\" ! \"b\"\n",
101
        "-1\n",
102
103
        "1 0 0 -1\n",
        "1 t\n",
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
        "-1\n",
        "\n"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.save('example.aut').save('example.aut', format='lbtt', append=True)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "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",
131
132
133
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
134
        "<title>G</title>\n",
135
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
136
137
138
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
139
140
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
141
142
143
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
144
145
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
146
147
148
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
149
150
151
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
152
153
154
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
155
156
157
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
158
159
160
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
161
162
163
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
164
165
166
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
167
168
169
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
170
171
172
173
174
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
175
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4414147600> >"
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "!cat example.aut"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "HOA: v1\r\n",
        "States: 2\r\n",
        "Start: 1\r\n",
        "AP: 2 \"a\" \"b\"\r\n",
        "acc-name: Buchi\r\n",
        "Acceptance: 1 Inf(0)\r\n",
        "properties: trans-labels explicit-labels state-acc deterministic\r\n",
201
        "properties: stutter-invariant terminal\r\n",
202
203
204
205
206
207
208
        "--BODY--\r\n",
        "State: 0 {0}\r\n",
        "[t] 0\r\n",
        "State: 1\r\n",
        "[1] 0\r\n",
        "[0&!1] 1\r\n",
        "--END--\r\n",
209
210
211
212
        "2 1\r\n",
        "0 1 -1\r\n",
        "1 \"b\"\r\n",
        "0 & \"a\" ! \"b\"\r\n",
213
        "-1\r\n",
214
215
        "1 0 0 -1\r\n",
        "1 t\r\n",
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
        "-1\r\n"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for a in spot.automata('example.aut'):\n",
      "    display(a)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "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",
242
243
244
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
245
        "<title>G</title>\n",
246
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
247
248
249
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
250
251
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
252
253
254
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
255
256
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
257
258
259
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
260
261
262
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
263
264
265
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
266
267
268
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
269
270
271
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
272
273
274
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
275
276
277
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
278
279
280
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
281
282
283
284
285
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
286
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4414157570> >"
287
288
289
290
291
292
293
294
295
296
297
298
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "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",
299
300
301
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
302
        "<title>G</title>\n",
303
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
304
305
306
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
307
308
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
309
310
311
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
312
313
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
314
315
316
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
317
318
319
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
320
321
322
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
323
324
325
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
326
327
328
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
329
330
331
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
332
333
334
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
335
336
337
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
338
339
340
341
342
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
343
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4414157660> >"
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Test `--ABORT--`\n",
      "----------------"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "%%file example.aut\n",
      "HOA: v1\n",
      "States: 2\n",
      "Start: 1\n",
      "AP: 2 \"a\" \"b\"\n",
      "acc-name: Buchi\n",
      "Acceptance: 1 Inf(0)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[t] 0\n",
      "--ABORT--   /* the previous automaton should be ignored */\n",
      "HOA: v1\n",
      "States: 2\n",
      "Start: 1\n",
      "AP: 2 \"a\" \"b\"\n",
      "Acceptance: 1 Inf(0)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[t] 0\n",
      "State: 1\n",
      "[1] 0\n",
      "[0&!1] 1\n",
      "--END--"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "Overwriting example.aut\n"
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for a in spot.automata('example.aut'):\n",
      "    display(a)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "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",
418
419
420
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
421
        "<title>G</title>\n",
422
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
423
424
425
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
426
427
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
428
429
430
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
431
432
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
433
434
435
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
436
437
438
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
439
440
441
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
442
443
444
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
445
446
447
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
448
449
450
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
451
452
453
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
454
455
456
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
457
458
459
460
461
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
462
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f441765be40> >"
463
464
465
466
467
       ]
      }
     ],
     "prompt_number": 7
    },
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for a in spot.automata(\"\"\"\n",
      "HOA: v1\n",
      "States: 2\n",
      "Start: 1\n",
      "name: \"Hello world\"\n",
      "AP: 2 \"a\" \"b\"\n",
      "Acceptance: 1 Inf(0)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[t] 0\n",
      "State: 1\n",
      "[1] 0\n",
      "[0&!1] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 1\n",
      "Start: 0\n",
      "name: \"Hello world 2\"\n",
      "AP: 2 \"a\" \"b\"\n",
      "Acceptance: 2 Inf(0)&Inf(1)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[t] 0 {1}\n",
      "[0&!1] 0\n",
      "--END--\n",
      "\"\"\"):\n",
      "    display(a)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "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",
513
514
515
        "<svg width=\"171pt\" height=\"85pt\"\n",
        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
516
        "<title>G</title>\n",
517
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
518
519
520
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
521
522
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
523
524
525
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
526
527
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
528
529
530
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
531
532
533
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
534
535
536
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
537
538
539
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
540
541
542
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
543
544
545
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
546
547
548
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
549
550
551
        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
552
553
554
555
556
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
557
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4414157690> >"
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "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=\"83pt\" height=\"138pt\"\n",
        " viewBox=\"0.00 0.00 82.50 138.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 134)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-134 78.5,-134 78.5,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-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",
        "<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",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"59.2357,-35.7817 62.4756,-42.7406 59.2808,-39.2814 59.3258,-42.7812 59.3258,-42.7812 59.3258,-42.7812 59.2808,-39.2814 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"40\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"56\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M50.9375,-35.5938C47.5625,-56.125 49.25,-82 56,-82 61.9854,-82 63.9902,-61.6553 62.0146,-42.7315\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"61.0625,-35.5938 65.1104,-42.1158 61.5253,-39.063 61.9881,-42.5323 61.9881,-42.5323 61.9881,-42.5323 61.5253,-39.063 58.8657,-42.9488 61.0625,-35.5938 61.0625,-35.5938\"/>\n",
        "<text text-anchor=\"start\" x=\"37.5\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "<text text-anchor=\"start\" x=\"48\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
605
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f441765be40> >"
606
607
608
609
610
       ]
      }
     ],
     "prompt_number": 8
    },
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Test syntax errors\n",
      "------------------"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "%%file example.aut\n",
      "HOA: v1\n",
      "States: 2\n",
      "Start: 1\n",
      "AP: 2 \"a\" \"b\"\n",
      "acc-name: Buchi\n",
      "Acceptance: 1 Inf(0)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[t] 1\n",
      "State: 1\n",
      "[t] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 2\n",
      "Start: 1\n",
      "AP: 2 \"a\" \"b\"\n",
      "Acceptance: 1 Inf(0)\n",
      "--BODY--\n",
      "State: 0 {0}\n",
      "[a] 3\n",
      "State: 1\n",
      "[1] 0\n",
      "[0&!1] 1\n",
      "--END--"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "Overwriting example.aut\n"
       ]
      }
     ],
660
     "prompt_number": 9
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for a in spot.automata('example.aut'):\n",
      "    display(a)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "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",
682
683
684
        "<svg width=\"133pt\" height=\"101pt\"\n",
        " viewBox=\"0.00 0.00 133.00 101.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 97)\">\n",
685
        "<title>G</title>\n",
686
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-97 129,-97 129,4 -4,4\"/>\n",
687
688
689
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
690
691
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
692
693
694
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
695
696
        "<path fill=\"none\" stroke=\"black\" d=\"M23.0602,-62.9848C24.6706,-62.5773 58.2688,-54.0766 82.2014,-48.0213\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"89.2724,-46.2323 83.2589,-51.0031 85.8793,-47.0908 82.4862,-47.9493 82.4862,-47.9493 82.4862,-47.9493 85.8793,-47.0908 81.7135,-44.8956 89.2724,-46.2323 89.2724,-46.2323\"/>\n",
697
698
699
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
700
701
702
        "<path fill=\"none\" stroke=\"black\" d=\"M99.9688,-58.6641C98.4062,-68.625 100.75,-78 107,-78 111.688,-78 114.178,-72.7266 114.471,-65.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"114.031,-58.6641 117.601,-65.4598 114.244,-62.1576 114.456,-65.6511 114.456,-65.6511 114.456,-65.6511 114.244,-62.1576 111.312,-65.8425 114.031,-58.6641 114.031,-58.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
703
704
705
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
706
707
708
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
709
710
711
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
712
713
714
        "<path fill=\"none\" stroke=\"black\" d=\"M43.5169,-26.9438C55.3149,-29.7867 70.1833,-33.3695 82.4561,-36.3268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"89.3394,-37.9854 81.7962,-39.4079 85.9368,-37.1655 82.5342,-36.3455 82.5342,-36.3455 82.5342,-36.3455 85.9368,-37.1655 83.2721,-33.2832 89.3394,-37.9854 89.3394,-37.9854\"/>\n",
        "<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
715
716
717
718
719
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
720
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44141578d0> >"
721
722
723
724
725
726
727
       ]
      },
      {
       "ename": "SyntaxError",
       "evalue": "\nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\n (<string>)",
       "output_type": "pyerr",
       "traceback": [
728
        "\u001b[0;36m  File \u001b[0;32m\"<string>\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\n\n"
729
730
731
       ]
      }
     ],
732
     "prompt_number": 10
733
734
735
736
737
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
738
      "spot.automaton('example.aut', timeout=100)"
739
740
741
     ],
     "language": "python",
     "metadata": {},
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 11,
       "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=\"133pt\" height=\"101pt\"\n",
        " viewBox=\"0.00 0.00 133.00 101.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 97)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-97 129,-97 129,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M23.0602,-62.9848C24.6706,-62.5773 58.2688,-54.0766 82.2014,-48.0213\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"89.2724,-46.2323 83.2589,-51.0031 85.8793,-47.0908 82.4862,-47.9493 82.4862,-47.9493 82.4862,-47.9493 85.8793,-47.0908 81.7135,-44.8956 89.2724,-46.2323 89.2724,-46.2323\"/>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M99.9688,-58.6641C98.4062,-68.625 100.75,-78 107,-78 111.688,-78 114.178,-72.7266 114.471,-65.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"114.031,-58.6641 117.601,-65.4598 114.244,-62.1576 114.456,-65.6511 114.456,-65.6511 114.456,-65.6511 114.244,-62.1576 111.312,-65.8425 114.031,-58.6641 114.031,-58.6641\"/>\n",
        "<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
        "<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M43.5169,-26.9438C55.3149,-29.7867 70.1833,-33.3695 82.4561,-36.3268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"89.3394,-37.9854 81.7962,-39.4079 85.9368,-37.1655 82.5342,-36.3455 82.5342,-36.3455 82.5342,-36.3455 85.9368,-37.1655 83.2721,-33.2832 89.3394,-37.9854 89.3394,-37.9854\"/>\n",
        "<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
792
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44141578a0> >"
793
794
795
       ]
      }
     ],
796
     "prompt_number": 11
797
798
799
800
801
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
802
      "spot.automaton('non-existing-cmd |')"
803
804
805
806
807
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
808
809
       "ename": "CalledProcessError",
       "evalue": "Command 'non-existing-cmd ' returned non-zero exit status 127",
810
811
       "output_type": "pyerr",
       "traceback": [
812
813
814
815
816
        "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m                        Traceback (most recent call last)",
        "\u001b[0;32m<ipython-input-12-2b2d1b66dcd6>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'non-existing-cmd |'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
        "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m    404\u001b[0m     See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m    405\u001b[0m     \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 406\u001b[0;31m         \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    407\u001b[0m     \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    408\u001b[0m         \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, *sources)\u001b[0m\n\u001b[1;32m    395\u001b[0m                 \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    396\u001b[0m                 \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 397\u001b[0;31m                     \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    398\u001b[0m     \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    399\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;31mCalledProcessError\u001b[0m: Command 'non-existing-cmd ' returned non-zero exit status 127"
817
818
819
       ]
      }
     ],
820
     "prompt_number": 12
821
822
823
824
825
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
826
      "spot.automaton('sleep 3; cat example.aut |', timeout=1)"
827
828
829
830
831
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
832
833
       "ename": "TimeoutExpired",
       "evalue": "Command 'sleep 3; cat example.aut ' timed out after 1 seconds",
834
835
       "output_type": "pyerr",
       "traceback": [
836
837
838
839
840
841
        "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mTimeoutExpired\u001b[0m                            Traceback (most recent call last)",
        "\u001b[0;32m<ipython-input-13-d9c814f4e517>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'sleep 3; cat example.aut |'\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
        "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m    404\u001b[0m     See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m    405\u001b[0m     \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 406\u001b[0;31m         \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    407\u001b[0m     \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    408\u001b[0m         \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, *sources)\u001b[0m\n\u001b[1;32m    366\u001b[0m                 \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    367\u001b[0m                     out = subprocess.check_output(filename[:-1], shell=True,\n\u001b[0;32m--> 368\u001b[0;31m                                                   timeout=timeout)\n\u001b[0m\u001b[1;32m    369\u001b[0m                     \u001b[0mp\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mautomaton_stream_parser\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    370\u001b[0m             \u001b[0;32melif\u001b[0m \u001b[0;34m'\\n'\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;32m/usr/lib/python3.4/subprocess.py\u001b[0m in \u001b[0;36mcheck_output\u001b[0;34m(timeout, *popenargs, **kwargs)\u001b[0m\n\u001b[1;32m    611\u001b[0m             \u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mkill\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    612\u001b[0m             \u001b[0moutput\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0munused_err\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcommunicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 613\u001b[0;31m             \u001b[0;32mraise\u001b[0m \u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0moutput\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0moutput\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    614\u001b[0m         \u001b[0;32mexcept\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    615\u001b[0m             \u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mkill\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;31mTimeoutExpired\u001b[0m: Command 'sleep 3; cat example.aut ' timed out after 1 seconds"
842
843
844
       ]
      }
     ],
845
     "prompt_number": 13
846
847
848
849
    },
    {
     "cell_type": "code",
     "collapsed": false,
850
851
852
     "input": [
      "rm example.aut"
     ],
853
854
     "language": "python",
     "metadata": {},
855
     "outputs": [],
856
     "prompt_number": 14
857
858
859
860
861
    }
   ],
   "metadata": {}
  }
 ]
862
}