testingaut.ipynb 50 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
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
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
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
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
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
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
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
605
606
607
608
609
610
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
{
 "metadata": {
  "name": "",
  "signature": "sha256:89d455537d395ae2842b209c6c14a262e15747fd501a731df0cd235f8c95011f"
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import os\n",
      "from IPython.display import display, HTML\n",
      "# Note that Spot (loaded by the kernel) will store a copy of\n",
      "# the environment variables 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",
      "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
      "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
      "import spot"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To translate a formula into a Testing Automaton\n",
      "\n",
      "Start by building a Buchi automaton"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U Gb')\n",
      "a = f.translate('ba')\n",
      "a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "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=\"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",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-90.7401 176.74,-90.7401 176.74,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-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",
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-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",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-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",
        "<text text-anchor=\"start\" x=\"52.5\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<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",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"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",
        "<text text-anchor=\"start\" x=\"92\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"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",
        "<text text-anchor=\"start\" x=\"141.37\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f1eb80416f0> >"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Then, gather all the atomic proposition in the formula, and create an automaton with changesets"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "propset = spot.atomic_prop_collect_as_bdd(f, a)\n",
      "ta = spot.tgba_to_ta(a, propset, True, True, False, False, True)\n",
      "ta.show('.A')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "svg": [
        "<svg height=\"295pt\" viewBox=\"0.00 0.00 734.00 295.42\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.749788 0.749788) rotate(0) translate(4 390)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" points=\"-4,4 -4,-390 974.944,-390 974.944,4 -4,4\" stroke=\"none\"/>\n",
        "<!-- 0 -->\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
        "<ellipse cx=\"62.6978\" cy=\"-256\" fill=\"#ffffaa\" rx=\"24.8972\" ry=\"24.8972\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"62.6978\" y=\"-252.3\">init</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>0-&gt;1</title>\n",
        "<path d=\"M1.04399,-256C1.93865,-256 16.3331,-256 30.8732,-256\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9642,-256 30.9643,-259.15 34.4642,-256 30.9642,-256 30.9642,-256 30.9642,-256 34.4642,-256 30.9642,-252.85 37.9642,-256 37.9642,-256\" stroke=\"black\"/>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
        "<ellipse cx=\"482.365\" cy=\"-190\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"37.4533\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"482.365\" y=\"-193.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"482.365\" y=\"-178.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>1-&gt;2</title>\n",
        "<path d=\"M80.0021,-274.105C115.083,-310.768 201.199,-388.632 283.106,-368 356.606,-349.486 378.744,-332.757 424.06,-272 434.518,-257.978 432.39,-251.576 442.06,-237 445.119,-232.388 448.559,-227.709 452.097,-223.181\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"456.612,-217.543 454.696,-224.976 454.424,-220.275 452.237,-223.008 452.237,-223.008 452.237,-223.008 454.424,-220.275 449.778,-221.039 456.612,-217.543 456.612,-217.543\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"264.606\" y=\"-374.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
        "<ellipse cx=\"192.751\" cy=\"-152\" fill=\"#ffffaa\" rx=\"35.2113\" ry=\"35.2113\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.751\" y=\"-155.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.751\" y=\"-140.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
        "<path d=\"M82.3178,-240.878C102.354,-224.605 134.612,-198.406 158.925,-178.66\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"164.609,-174.044 161.161,-180.902 161.892,-176.25 159.175,-178.457 159.175,-178.457 159.175,-178.457 161.892,-176.25 157.189,-176.012 164.609,-174.044 164.609,-174.044\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"122.396\" y=\"-223.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
        "<ellipse cx=\"338.583\" cy=\"-205\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"37.4533\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"338.583\" y=\"-208.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"338.583\" y=\"-193.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
        "<path d=\"M87.1814,-252.544C119.148,-247.749 178.107,-238.579 228.106,-229 250.158,-224.775 274.574,-219.483 294.742,-214.943\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"301.687,-213.372 295.555,-217.989 298.274,-214.145 294.86,-214.917 294.86,-214.917 294.86,-214.917 298.274,-214.145 294.165,-211.844 301.687,-213.372 301.687,-213.372\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.751\" y=\"-245.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node6\"><title>5</title>\n",
        "<ellipse cx=\"628.025\" cy=\"-158\" fill=\"#ffffaa\" rx=\"35.2259\" ry=\"35.2259\" stroke=\"black\"/>\n",
        "<ellipse cx=\"628.025\" cy=\"-158\" fill=\"none\" rx=\"39.2112\" ry=\"39.2112\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"628.025\" y=\"-161.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"628.025\" y=\"-146.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;5</title>\n",
        "<path d=\"M519.246,-182.008C538.352,-177.752 562.03,-172.478 582.322,-167.958\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"589.345,-166.393 583.198,-170.99 585.929,-167.154 582.513,-167.915 582.513,-167.915 582.513,-167.915 585.929,-167.154 581.828,-164.84 589.345,-166.393 589.345,-166.393\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"555.67\" y=\"-180.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node7\"><title>6</title>\n",
        "<ellipse cx=\"774.857\" cy=\"-158\" fill=\"#ffffaa\" rx=\"37.4556\" ry=\"37.4556\" stroke=\"black\"/>\n",
        "<ellipse cx=\"774.857\" cy=\"-158\" fill=\"none\" rx=\"41.4533\" ry=\"41.4533\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"774.857\" y=\"-161.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"774.857\" y=\"-146.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;6</title>\n",
        "<path d=\"M514.661,-209.497C551.574,-229.937 614.593,-256.796 667.38,-239 694.942,-229.708 721.017,-210.125 740.465,-192.542\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"745.771,-187.646 742.763,-194.708 743.199,-190.02 740.627,-192.393 740.627,-192.393 740.627,-192.393 743.199,-190.02 738.49,-190.078 745.771,-187.646 745.771,-187.646\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"628.025\" y=\"-248.8\">{}</text>\n",
        "</g>\n",
        "<!-- 7 -->\n",
        "<g class=\"node\" id=\"node8\"><title>7</title>\n",
        "<ellipse cx=\"926.639\" cy=\"-61\" fill=\"#ffffaa\" rx=\"37.4556\" ry=\"37.4556\" stroke=\"black\"/>\n",
        "<ellipse cx=\"926.639\" cy=\"-61\" fill=\"none\" rx=\"41.4533\" ry=\"41.4533\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"926.639\" y=\"-64.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"926.639\" y=\"-49.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;7 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;7</title>\n",
        "<path d=\"M510.516,-164.88C530.742,-147.339 559.75,-124.548 588.67,-110 683.063,-62.5163 809.91,-57.452 877.879,-58.7202\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"885.07,-58.8824 878.001,-61.8737 881.571,-58.8034 878.072,-58.7245 878.072,-58.7245 878.072,-58.7245 881.571,-58.8034 878.143,-55.5753 885.07,-58.8824 885.07,-58.8824\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"700.38\" y=\"-80.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 8 -->\n",
        "<g class=\"node\" id=\"node9\"><title>8</title>\n",
        "<ellipse cx=\"926.639\" cy=\"-289\" fill=\"#ffffaa\" rx=\"40.1285\" ry=\"40.1285\" stroke=\"black\"/>\n",
        "<ellipse cx=\"926.639\" cy=\"-289\" fill=\"none\" rx=\"44.111\" ry=\"44.111\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"926.639\" y=\"-292.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"926.639\" y=\"-277.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;8 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;8</title>\n",
        "<path d=\"M508.636,-216.791C518.105,-225.87 529.33,-235.58 540.67,-243 560.155,-255.749 566.391,-257.228 588.67,-264 693.763,-295.945 724.494,-290.456 834.334,-291 847.667,-291.066 851.002,-291.217 864.334,-291 867.837,-290.943 871.453,-290.867 875.095,-290.779\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"882.106,-290.595 875.191,-293.928 878.607,-290.687 875.108,-290.779 875.108,-290.779 875.108,-290.779 878.607,-290.687 875.026,-287.63 882.106,-290.595 882.106,-290.595\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"700.38\" y=\"-292.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>3-&gt;2</title>\n",
        "<path d=\"M227.758,-145.527C264.685,-139.647 325.2,-133.376 376.06,-144 399.22,-148.838 423.521,-159.065 442.935,-168.65\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"449.323,-171.868 441.655,-171.532 446.198,-170.293 443.072,-168.719 443.072,-168.719 443.072,-168.719 446.198,-170.293 444.489,-165.906 449.323,-171.868 449.323,-171.868\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"338.583\" y=\"-147.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>3-&gt;3</title>\n",
        "<path d=\"M179.627,-185.086C179.558,-196.323 183.933,-205.355 192.751,-205.355 199.64,-205.355 203.817,-199.843 205.282,-192.073\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"205.875,-185.086 208.422,-192.327 205.579,-188.574 205.283,-192.061 205.283,-192.061 205.283,-192.061 205.579,-188.574 202.145,-191.795 205.875,-185.086 205.875,-185.086\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.751\" y=\"-209.155\">{}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>3-&gt;4</title>\n",
        "<path d=\"M222.222,-171.683C229.739,-176.234 238.017,-180.702 246.106,-184 261.284,-190.188 278.659,-194.756 294.16,-198.021\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"301.135,-199.43 293.65,-201.131 297.705,-198.737 294.274,-198.044 294.274,-198.044 294.274,-198.044 297.705,-198.737 294.898,-194.956 301.135,-199.43 301.135,-199.43\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"264.606\" y=\"-199.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;5</title>\n",
        "<path d=\"M226.397,-140.622C232.858,-138.77 239.641,-137.1 246.106,-136 366.378,-115.533 510.752,-135.902 582.298,-148.943\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"589.408,-150.259 581.951,-152.082 585.966,-149.622 582.525,-148.985 582.525,-148.985 582.525,-148.985 585.966,-149.622 583.098,-145.887 589.408,-150.259 589.408,-150.259\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"409.06\" y=\"-133.8\">{}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;6</title>\n",
        "<path d=\"M224.377,-135.817C231.353,-132.741 238.851,-129.896 246.106,-128 427.419,-80.611 484.163,-70.6112 667.38,-110 689.822,-114.825 713.237,-124.768 732.376,-134.36\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"738.695,-137.592 731.028,-137.209 735.579,-135.998 732.463,-134.405 732.463,-134.405 732.463,-134.405 735.579,-135.998 733.897,-131.6 738.695,-137.592 738.695,-137.592\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"482.365\" y=\"-91.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;7 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;7</title>\n",
        "<path d=\"M207.136,-119.392C227.894,-74.7296 272.369,-0 337.583,-0 337.583,-0 337.583,-0 775.857,-0 815.143,-0 856.228,-18.222 885.41,-34.7474\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"891.821,-38.4592 884.185,-37.6779 888.792,-36.7055 885.763,-34.9518 885.763,-34.9518 885.763,-34.9518 888.792,-36.7055 887.342,-32.2257 891.821,-38.4592 891.821,-38.4592\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"555.67\" y=\"-3.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;8 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;8</title>\n",
        "<path d=\"M209.097,-183.411C215.207,-196.222 222.181,-211.233 228.106,-225 257.834,-294.071 262.386,-354 337.583,-354 337.583,-354 337.583,-354 775.857,-354 814.76,-354 854.998,-335.32 883.959,-317.988\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"889.963,-314.317 885.634,-320.656 886.977,-316.142 883.991,-317.968 883.991,-317.968 883.991,-317.968 886.977,-316.142 882.348,-315.281 889.963,-314.317 889.963,-314.317\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"555.67\" y=\"-357.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 9 -->\n",
        "<g class=\"node\" id=\"node10\"><title>9</title>\n",
        "<ellipse cx=\"482.365\" cy=\"-286\" fill=\"#ffffaa\" rx=\"40.1111\" ry=\"40.1111\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"482.365\" y=\"-289.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"482.365\" y=\"-274.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;9 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>3-&gt;9</title>\n",
        "<path d=\"M208.952,-183.615C226.27,-215.577 257.875,-263.141 301.106,-284 343.123,-304.273 397.325,-301.615 435.276,-295.857\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"442.641,-294.67 436.231,-298.894 439.186,-295.227 435.73,-295.784 435.73,-295.784 435.73,-295.784 439.186,-295.227 435.229,-292.674 442.641,-294.67 442.641,-294.67\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"338.583\" y=\"-302.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge18\"><title>4-&gt;2</title>\n",
        "<path d=\"M376.095,-201.137C394.949,-199.143 418.082,-196.695 437.857,-194.603\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"444.976,-193.85 438.346,-197.719 441.496,-194.218 438.015,-194.586 438.015,-194.586 438.015,-194.586 441.496,-194.218 437.684,-191.454 444.976,-193.85 444.976,-193.85\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"409.06\" y=\"-202.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge17\"><title>4-&gt;3</title>\n",
        "<path d=\"M309.772,-180.571C301.655,-174.596 292.444,-168.826 283.106,-165 268.272,-158.921 251.03,-155.624 235.672,-153.857\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"228.302,-153.107 235.585,-150.682 231.784,-153.461 235.266,-153.816 235.266,-153.816 235.266,-153.816 231.784,-153.461 234.947,-156.95 228.302,-153.107 228.302,-153.107\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"264.606\" y=\"-168.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge19\"><title>4-&gt;4</title>\n",
        "<path d=\"M325.461,-240.213C325.596,-251.517 329.97,-260.477 338.583,-260.477 345.312,-260.477 349.454,-255.008 351.008,-247.226\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"351.705,-240.213 354.147,-247.49 351.359,-243.696 351.012,-247.179 351.012,-247.179 351.012,-247.179 351.359,-243.696 347.878,-246.867 351.705,-240.213 351.705,-240.213\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"338.583\" y=\"-264.277\">{}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;9 -->\n",
        "<g class=\"edge\" id=\"edge20\"><title>4-&gt;9</title>\n",
        "<path d=\"M371.402,-223.178C391.924,-234.903 418.8,-250.257 440.845,-262.851\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"446.925,-266.325 439.285,-265.587 443.886,-264.589 440.847,-262.852 440.847,-262.852 440.847,-262.852 443.886,-264.589 442.41,-260.117 446.925,-266.325 446.925,-266.325\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"409.06\" y=\"-256.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge21\"><title>5-&gt;5</title>\n",
        "<path d=\"M614.546,-195.236C614.884,-206.528 619.377,-215.355 628.025,-215.355 634.782,-215.355 639.002,-209.968 640.686,-202.226\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"641.505,-195.236 643.819,-202.555 641.098,-198.712 640.691,-202.189 640.691,-202.189 640.691,-202.189 641.098,-198.712 637.562,-201.822 641.505,-195.236 641.505,-195.236\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"628.025\" y=\"-219.155\">{}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge22\"><title>5-&gt;6</title>\n",
        "<path d=\"M666.037,-146.689C672.431,-145.156 679.056,-143.827 685.38,-143 698.601,-141.271 702.152,-141.33 715.38,-143 719.444,-143.513 723.629,-144.219 727.805,-145.047\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"734.8,-146.543 727.296,-148.159 731.377,-145.811 727.955,-145.078 727.955,-145.078 727.955,-145.078 731.377,-145.811 728.613,-141.998 734.8,-146.543 734.8,-146.543\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"700.38\" y=\"-146.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;7 -->\n",
        "<g class=\"edge\" id=\"edge23\"><title>5-&gt;7</title>\n",
        "<path d=\"M659.754,-134.347C679.693,-120.18 706.822,-103.027 733.38,-93 780.616,-75.1666 838.104,-67.2507 877.845,-63.7498\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"885.052,-63.146 878.34,-66.8694 881.565,-63.4382 878.077,-63.7304 878.077,-63.7304 878.077,-63.7304 881.565,-63.4382 877.814,-60.5914 885.052,-63.146 885.052,-63.146\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"774.857\" y=\"-96.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;8 -->\n",
        "<g class=\"edge\" id=\"edge24\"><title>5-&gt;8</title>\n",
        "<path d=\"M656.84,-185.638C676.645,-203.852 704.731,-226.867 733.38,-241 778.691,-263.352 835.286,-275.855 875.308,-282.454\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"882.581,-283.618 875.171,-285.622 879.125,-283.065 875.669,-282.512 875.669,-282.512 875.669,-282.512 879.125,-283.065 876.167,-279.401 882.581,-283.618 882.581,-283.618\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"774.857\" y=\"-274.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge25\"><title>6-&gt;5</title>\n",
        "<path d=\"M733.217,-158C715.031,-158 693.51,-158 674.762,-158\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"667.457,-158 674.457,-154.85 670.957,-158 674.457,-158 674.457,-158 674.457,-158 670.957,-158 674.457,-161.15 667.457,-158 667.457,-158\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"700.38\" y=\"-161.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge26\"><title>6-&gt;6</title>\n",
        "<path d=\"M761.024,-197.182C761.502,-208.618 766.113,-217.477 774.857,-217.477 781.688,-217.477 785.997,-212.07 787.784,-204.251\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"788.691,-197.182 790.924,-204.526 788.245,-200.654 787.8,-204.125 787.8,-204.125 787.8,-204.125 788.245,-200.654 784.675,-203.724 788.691,-197.182 788.691,-197.182\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"774.857\" y=\"-221.277\">{}</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;7 -->\n",
        "<g class=\"edge\" id=\"edge27\"><title>6-&gt;7</title>\n",
        "<path d=\"M810.22,-135.746C832.578,-121.267 861.832,-102.322 885.294,-87.1277\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"891.436,-83.1502 887.273,-89.5993 888.498,-85.0527 885.56,-86.9553 885.56,-86.9553 885.56,-86.9553 888.498,-85.0527 883.848,-84.3113 891.436,-83.1502 891.436,-83.1502\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"849.334\" y=\"-122.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;8 -->\n",
        "<g class=\"edge\" id=\"edge28\"><title>6-&gt;8</title>\n",
        "<path d=\"M806.529,-184.826C829.843,-205.216 862.064,-233.397 887.115,-255.307\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"892.669,-260.165 885.327,-257.927 890.035,-257.861 887.4,-255.556 887.4,-255.556 887.4,-255.556 890.035,-257.861 889.474,-253.185 892.669,-260.165 892.669,-260.165\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"849.334\" y=\"-239.8\">{b}</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
        "<IPython.core.display.SVG at 0x7f1eb80687b8>"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by `{}`), marking as *livelock accepting* (rectangles) any states from which there exists a an accepting path labeled by `{}`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "ta = spot.tgba_to_ta(a, propset, True, True, False, False, False)\n",
      "ta.show('.A')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "svg": [
        "<svg height=\"161pt\" viewBox=\"0.00 0.00 715.35 161.00\" width=\"715pt\" 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 157)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" points=\"-4,4 -4,-157 711.349,-157 711.349,4 -4,4\" stroke=\"none\"/>\n",
        "<!-- 0 -->\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
        "<ellipse cx=\"62.6978\" cy=\"-68\" fill=\"#ffffaa\" rx=\"24.8972\" ry=\"24.8972\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"62.6978\" y=\"-64.3\">init</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>0-&gt;1</title>\n",
        "<path d=\"M1.04399,-68C1.93865,-68 16.3331,-68 30.8732,-68\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9642,-68 30.9643,-71.1501 34.4642,-68 30.9642,-68.0001 30.9642,-68.0001 30.9642,-68.0001 34.4642,-68 30.9642,-64.8501 37.9642,-68 37.9642,-68\" stroke=\"black\"/>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"479.349,-148 425.349,-148 425.349,-110 479.349,-110 479.349,-148\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"452.349\" y=\"-132.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"452.349\" y=\"-117.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>1-&gt;2</title>\n",
        "<path d=\"M85.1066,-78.4223C91.5527,-81.3783 98.6955,-84.476 105.396,-87 183.158,-116.294 202.189,-128.87 284.396,-141 317.351,-145.863 326.044,-141.694 359.349,-141 380.696,-140.555 386.184,-141.822 407.349,-139 410.85,-138.533 414.484,-137.92 418.093,-137.228\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"424.966,-135.815 418.744,-140.31 421.537,-136.52 418.109,-137.225 418.109,-137.225 418.109,-137.225 421.537,-136.52 417.475,-134.139 424.966,-135.815 424.966,-135.815\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-141.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"211.396,-87 157.396,-87 157.396,-49 211.396,-49 211.396,-87\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"184.396\" y=\"-71.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"184.396\" y=\"-56.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
        "<path d=\"M87.6328,-68C105.497,-68 130.135,-68 149.947,-68\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"157.006,-68 150.006,-71.1501 153.506,-68 150.006,-68.0001 150.006,-68.0001 150.006,-68.0001 153.506,-68 150.006,-64.8501 157.006,-68 157.006,-68\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"122.396\" y=\"-71.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
        "<ellipse cx=\"321.872\" cy=\"-65\" fill=\"#ffffaa\" rx=\"37.4533\" ry=\"37.4533\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"321.872\" y=\"-68.8\">1</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"321.872\" y=\"-53.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
        "<path d=\"M84.3656,-55.3514C102.769,-44.8778 130.817,-30.8075 157.396,-25 199.902,-15.7122 248.27,-30.763 281.299,-44.9807\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"288.106,-47.9929 280.43,-48.041 284.905,-46.5767 281.705,-45.1604 281.705,-45.1604 281.705,-45.1604 284.905,-46.5767 282.979,-42.2798 288.106,-47.9929 288.106,-47.9929\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"184.396\" y=\"-28.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node6\"><title>5</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"589.349,-123 535.349,-123 535.349,-85 589.349,-85 589.349,-123\" stroke=\"black\"/>\n",
        "<polygon fill=\"none\" points=\"593.349,-127 531.349,-127 531.349,-81 593.349,-81 593.349,-127\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"562.349\" y=\"-107.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"562.349\" y=\"-92.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;5</title>\n",
        "<path d=\"M479.493,-122.948C492.905,-119.844 509.474,-116.008 524.19,-112.602\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"531.242,-110.969 525.133,-115.617 527.833,-111.758 524.423,-112.548 524.423,-112.548 524.423,-112.548 527.833,-111.758 523.712,-109.479 531.242,-110.969 531.242,-110.969\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"505.349\" y=\"-121.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
        "<path d=\"M211.569,-81.698C231.123,-91.3492 258.782,-103.791 284.396,-111 324.55,-122.302 335.856,-119.702 377.349,-124 390.625,-125.375 405.282,-126.456 418.026,-127.256\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"425.283,-127.695 418.105,-130.417 421.789,-127.484 418.295,-127.273 418.295,-127.273 418.295,-127.273 421.789,-127.484 418.485,-124.128 425.283,-127.695 425.283,-127.695\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"321.872\" y=\"-125.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
        "<path d=\"M211.405,-55.4294C217.198,-53.1796 223.403,-51.1784 229.396,-50 245.554,-46.8226 263.411,-48.582 279.026,-51.8391\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"286.029,-53.4287 278.505,-54.951 282.616,-52.6539 279.203,-51.8791 279.203,-51.8791 279.203,-51.8791 282.616,-52.6539 279.9,-48.8073 286.029,-53.4287 286.029,-53.4287\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-53.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
        "<g class=\"node\" id=\"node7\"><title>6</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"703.349,-85 649.349,-85 649.349,-47 703.349,-47 703.349,-85\" stroke=\"black\"/>\n",
        "<polygon fill=\"none\" points=\"707.349,-89 645.349,-89 645.349,-43 707.349,-43 707.349,-89\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"676.349\" y=\"-69.8\">0</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"676.349\" y=\"-54.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;6</title>\n",
        "<path d=\"M207.657,-48.6958C233.192,-28.592 277.186,-0 320.872,-0 320.872,-0 320.872,-0 563.349,-0 595.255,-0 626.076,-20.1262 647.282,-38.1505\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"652.73,-42.9164 645.387,-40.6786 650.096,-40.612 647.461,-38.3076 647.461,-38.3076 647.461,-38.3076 650.096,-40.612 649.535,-35.9367 652.73,-42.9164 652.73,-42.9164\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"452.349\" y=\"-3.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
        "<path d=\"M355.625,-81.3155C374.995,-90.9647 399.44,-103.142 418.778,-112.775\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"425.126,-115.937 417.456,-115.635 421.993,-114.376 418.86,-112.816 418.86,-112.816 418.86,-112.816 421.993,-114.376 420.265,-109.996 425.126,-115.937 425.126,-115.937\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"392.349\" y=\"-109.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;3</title>\n",
        "<path d=\"M284.333,-65.8091C263.851,-66.2627 238.5,-66.824 218.588,-67.265\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"211.517,-67.4216 218.445,-64.1173 215.016,-67.344 218.515,-67.2665 218.515,-67.2665 218.515,-67.2665 215.016,-67.344 218.585,-70.4157 211.517,-67.4216 211.517,-67.4216\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-70.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;6</title>\n",
        "<path d=\"M587.188,-80.8632C594.396,-75.2601 602.707,-70.0196 611.349,-67 619.709,-64.0787 629.067,-62.8793 637.99,-62.6129\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"645.027,-62.5842 638.04,-65.7628 641.527,-62.5985 638.027,-62.6128 638.027,-62.6128 638.027,-62.6128 641.527,-62.5985 638.014,-59.4629 645.027,-62.5842 645.027,-62.5842\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"619.349\" y=\"-70.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>6-&gt;5</title>\n",
        "<path d=\"M645.252,-76.2114C631.432,-80.9005 614.911,-86.5056 600.339,-91.4496\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"593.363,-93.8167 598.98,-88.5846 596.677,-92.6921 599.992,-91.5676 599.992,-91.5676 599.992,-91.5676 596.677,-92.6921 601.004,-94.5505 593.363,-93.8167 593.363,-93.8167\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"619.349\" y=\"-90.8\">{a}</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
        "<IPython.core.display.SVG at 0x7f1eba67beb8>"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Finally, use bisimulation to minimize the number of states."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.minimize_ta(ta).show('.A')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "svg": [
        "<svg height=\"178pt\" viewBox=\"0.00 0.00 562.40 178.00\" width=\"562pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 174)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" points=\"-4,4 -4,-174 558.396,-174 558.396,4 -4,4\" stroke=\"none\"/>\n",
        "<!-- 0 -->\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
        "<ellipse cx=\"62.6978\" cy=\"-144\" fill=\"#ffffaa\" rx=\"24.8972\" ry=\"24.8972\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"62.6978\" y=\"-140.3\">init</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>0-&gt;1</title>\n",
        "<path d=\"M1.04399,-144C1.93865,-144 16.3331,-144 30.8732,-144\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9642,-144 30.9643,-147.15 34.4642,-144 30.9642,-144 30.9642,-144 30.9642,-144 34.4642,-144 30.9642,-140.85 37.9642,-144 37.9642,-144\" stroke=\"black\"/>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"440.396,-84 386.396,-84 386.396,-48 440.396,-48 440.396,-84\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"413.396\" y=\"-62.3\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>1-&gt;2</title>\n",
        "<path d=\"M86.9099,-150.505C92.8863,-151.92 99.3405,-153.225 105.396,-154 200.719,-166.201 229.01,-160.734 320.396,-131 342.539,-123.795 349.163,-123.127 368.396,-110 376.786,-104.273 384.949,-96.8174 391.919,-89.675\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"397.001,-84.3081 394.476,-91.5568 394.595,-86.8495 392.188,-89.3909 392.188,-89.3909 392.188,-89.3909 394.595,-86.8495 389.901,-87.225 397.001,-84.3081 397.001,-84.3081\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-158.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"211.396,-94 157.396,-94 157.396,-58 211.396,-58 211.396,-94\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"184.396\" y=\"-72.3\">3</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
        "<path d=\"M83.2503,-129.536C90.1123,-124.694 97.9646,-119.411 105.396,-115 119.96,-106.355 136.69,-97.8185 150.912,-90.9462\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"157.253,-87.9113 152.299,-93.7747 154.096,-89.4223 150.939,-90.9333 150.939,-90.9333 150.939,-90.9333 154.096,-89.4223 149.579,-88.092 157.253,-87.9113 157.253,-87.9113\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"122.396\" y=\"-118.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
        "<ellipse cx=\"302.396\" cy=\"-104\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"302.396\" y=\"-100.3\">1</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
        "<path d=\"M87.4738,-142.898C125.721,-140.694 203.038,-134.451 266.396,-118 270.535,-116.925 274.841,-115.487 278.96,-113.941\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"285.651,-111.282 280.309,-116.794 282.399,-112.575 279.146,-113.867 279.146,-113.867 279.146,-113.867 282.399,-112.575 277.983,-110.94 285.651,-111.282 285.651,-111.282\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"184.396\" y=\"-139.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node6\"><title>5</title>\n",
        "<polygon fill=\"#ffffaa\" points=\"550.396,-40 496.396,-40 496.396,-4 550.396,-4 550.396,-40\" stroke=\"black\"/>\n",
        "<polygon fill=\"none\" points=\"554.396,-44 492.396,-44 492.396,-3.55271e-15 554.396,-3.55271e-15 554.396,-44\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"523.396\" y=\"-18.3\">4</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;5</title>\n",
        "<path d=\"M440.539,-55.3488C454.074,-49.8349 470.822,-43.0113 485.637,-36.9757\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"492.289,-34.2656 486.995,-39.8239 489.048,-35.5862 485.807,-36.9067 485.807,-36.9067 485.807,-36.9067 489.048,-35.5862 484.618,-33.9895 492.289,-34.2656 492.289,-34.2656\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"466.396\" y=\"-51.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
        "<path d=\"M211.404,-70.9547C217.306,-69.898 223.556,-68.8483 229.396,-68 269.507,-62.1732 279.873,-61.1195 320.396,-62 339.836,-62.4224 361.57,-63.3463 379.03,-64.1999\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"386.233,-64.5597 379.084,-67.3564 382.737,-64.385 379.241,-64.2103 379.241,-64.2103 379.241,-64.2103 382.737,-64.385 379.399,-61.0642 386.233,-64.5597 386.233,-64.5597\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"302.396\" y=\"-65.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
        "<path d=\"M211.657,-72.1843C227.874,-70.8265 248.862,-70.9018 266.396,-77 272.543,-79.1381 278.459,-82.823 283.622,-86.7951\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"289.305,-91.5145 281.908,-89.4661 286.613,-89.2786 283.92,-87.0426 283.92,-87.0426 283.92,-87.0426 286.613,-89.2786 285.932,-84.6192 289.305,-91.5145 289.305,-91.5145\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-80.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;5</title>\n",
        "<path d=\"M211.649,-65.47C217.427,-63.4301 223.564,-61.4721 229.396,-60 319.354,-37.2923 428.464,-27.7027 484.752,-24.03\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"492.008,-23.5705 485.221,-27.1567 488.515,-23.7917 485.022,-24.013 485.022,-24.013 485.022,-24.013 488.515,-23.7917 484.823,-20.8693 492.008,-23.5705 492.008,-23.5705\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"353.396\" y=\"-42.8\">{a}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
        "<path d=\"M319.95,-98.2286C335.72,-92.7311 359.903,-84.3003 379.58,-77.4404\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"386.331,-75.0869 380.758,-80.3657 383.026,-76.2391 379.721,-77.3913 379.721,-77.3913 379.721,-77.3913 383.026,-76.2391 378.684,-74.4168 386.331,-75.0869 386.331,-75.0869\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"353.396\" y=\"-94.8\">{a, b}</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;3</title>\n",
        "<path d=\"M284.335,-102.054C269.627,-100.164 247.903,-96.8631 229.396,-92 225.851,-91.0685 222.189,-89.9687 218.563,-88.7888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"211.671,-86.4443 219.312,-85.7166 214.984,-87.5715 218.298,-88.6988 218.298,-88.6988 218.298,-88.6988 214.984,-87.5715 217.283,-91.6809 211.671,-86.4443 211.671,-86.4443\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"247.896\" y=\"-102.8\">{b}</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;5</title>\n",
        "<path d=\"M513.021,-44.2124C512.172,-53.7952 515.63,-62 523.396,-62 529.098,-62 532.478,-57.5751 533.535,-51.4291\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"533.77,-44.2124 536.69,-51.3112 533.656,-47.7105 533.542,-51.2086 533.542,-51.2086 533.542,-51.2086 533.656,-47.7105 530.394,-51.1061 533.77,-44.2124 533.77,-44.2124\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"523.396\" y=\"-65.8\">{a}</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
        "<IPython.core.display.SVG at 0x7f1eba67bc18>"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": []
    }
   ],
   "metadata": {}
  }
 ]
}