decompose.ipynb 439 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
{
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
18
   "version": "3.5.4"
19
  },
20
  "name": ""
21
22
23
24
25
26
27
28
29
30
31
32
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "from IPython.display import display\n",
      "import spot\n",
33
      "spot.setup(show_default='.bans')"
34
35
36
37
38
39
40
41
42
43
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
44
      "This notebook demonstrates how to use the `decompose_scc()` function to split an automaton in up to three automata capturing different behaviors.   This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n",
45
      "\n",
46
      "This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-scc` option.\n",
47
48
49
      "\n",
      "# Basics\n",
      "\n",
50
      "Let's define the following strengths of accepting SCCs:\n",
51
      "\n",
52
53
54
55
      "- an accepting SCC is **inherently weak** if it does not contain any rejecting cycle\n",
      "- an accepting SCC is **inherently terminal** if it is *inherently weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)\n",
      "- an accepting SCC is **strictly inherently weak** if it is *inherently weak* and not complete (in other words: *weak* but not *terminal*)\n",
      "- an accepting SCC is **strong** if it is not inherently weak.\n",
56
      "\n",
57
58
59
      "The strengths **strong**, **stricly inherently weak**, and **inherently terminal** define a partition of all accepting SCCs.  The following B\u00fcchi automaton has 4 SCCs, and its 3 accepting SCCs show an example of each strength.\n",
      "\n",
      "Note: the reason we use the word *inherently* is that the *weak* and *terminal* properties are usually defined syntactically: an accepting SCC would be weak if all its transitions belong to the same acceptance sets.  This syntactic criterion is a sufficient condition for an accepting SCC to not have any rejecting cycle, but it is not necessary.  Hence a *weak* SCC is *inherently weak*; but while an *inherently weak* SCC is not necessarily *weak*, it can be modified to be *weak* without alterning the langage."
60
61
62
63
64
65
66
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.translate('(Ga -> Gb) W c')\n",
67
      "aut"
68
69
70
71
72
73
74
75
76
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "svg": [
77
78
79
80
81
82
        "<?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",
83
84
85
        "<svg width=\"419pt\" height=\"302pt\"\n",
        " viewBox=\"0.00 0.00 419.00 302.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 298)\">\n",
86
        "<title>G</title>\n",
87
88
89
90
91
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-298 415,-298 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"182.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
92
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
93
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-148 351,-248 403,-248 403,-148 351,-148\"/>\n",
94
        "</g>\n",
95
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
96
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
97
        "</g>\n",
98
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
99
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-148 268,-233 320,-233 320,-148 268,-148\"/>\n",
100
        "</g>\n",
101
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
102
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-135 30,-237 216,-237 216,-135 30,-135\"/>\n",
103
104
        "</g>\n",
        "<!-- I -->\n",
105
106
107
108
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-161\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-157.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
109
        "</g>\n",
110
111
112
113
        "<!-- 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,-161C2.79388,-161 17.1543,-161 30.6317,-161\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-161 30.9419,-164.15 34.4419,-161 30.9419,-161 30.9419,-161 30.9419,-161 34.4419,-161 30.9418,-157.85 37.9419,-161 37.9419,-161\"/>\n",
114
        "</g>\n",
115
116
117
118
119
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-178.037C48.3189,-187.858 50.4453,-197 56,-197 60.166,-197 62.4036,-191.858 62.7128,-185.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-178.037 65.8541,-184.882 62.5434,-181.533 62.7076,-185.03 62.7076,-185.03 62.7076,-185.03 62.5434,-181.533 59.561,-185.177 62.3792,-178.037 62.3792,-178.037\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-215.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
120
        "<text text-anchor=\"start\" x=\"48\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
121
        "</g>\n",
122
123
124
125
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"377\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"377\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
126
        "</g>\n",
127
128
129
130
131
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.63,-156.447C115.658,-145.684 229.246,-121.222 320,-144 332.58,-147.157 345.419,-153.744 355.624,-159.943\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.612,-163.719 354.011,-162.65 358.652,-161.852 355.691,-159.986 355.691,-159.986 355.691,-159.986 358.652,-161.852 357.371,-157.321 361.612,-163.719 361.612,-163.719\"/>\n",
        "<text text-anchor=\"start\" x=\"238.5\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
132
        "</g>\n",
133
134
135
136
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
137
        "</g>\n",
138
139
140
141
142
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M63.6726,-144.642C69.681,-131.298 79.4843,-112.511 92,-99 113.848,-75.4146 145.853,-56.1055 167.046,-44.8262\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"173.253,-41.5877 168.504,-47.6186 170.15,-43.2068 167.047,-44.8259 167.047,-44.8259 167.047,-44.8259 170.15,-43.2068 165.59,-42.0332 173.253,-41.5877 173.253,-41.5877\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
143
        "</g>\n",
144
145
146
147
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-176\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-172.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
148
        "</g>\n",
149
150
151
152
153
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0161,-159.298C93.5381,-157.777 126.41,-156.539 154,-162 158.195,-162.83 162.529,-164.149 166.657,-165.652\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"173.35,-168.304 165.682,-168.654 170.096,-167.015 166.842,-165.726 166.842,-165.726 166.842,-165.726 170.096,-167.015 168.002,-162.797 173.35,-168.304 173.35,-168.304\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
154
        "</g>\n",
155
156
157
158
159
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M369.969,-190.664C368.406,-200.625 370.75,-210 377,-210 381.688,-210 384.178,-204.727 384.471,-197.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"384.031,-190.664 387.601,-197.46 384.244,-194.158 384.456,-197.651 384.456,-197.651 384.456,-197.651 384.244,-194.158 381.312,-197.842 384.031,-190.664 384.031,-190.664\"/>\n",
        "<text text-anchor=\"start\" x=\"372.5\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
160
        "<text text-anchor=\"start\" x=\"369\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
161
        "</g>\n",
162
163
164
165
166
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-49.916C178.679,-60.1504 181.672,-70 190,-70 196.376,-70 199.625,-64.2263 199.746,-56.9268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-49.916 202.872,-56.5315 199.36,-53.3952 199.741,-56.8744 199.741,-56.8744 199.741,-56.8744 199.36,-53.3952 196.61,-57.2174 198.979,-49.916 198.979,-49.916\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
167
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
168
169
        "</g>\n",
        "<!-- 4 -->\n",
170
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
171
172
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"294\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"294\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
173
        "</g>\n",
174
175
176
177
178
        "<!-- 4&#45;&gt;1 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M312.178,-174C323.669,-174 338.959,-174 351.693,-174\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"358.847,-174 351.847,-177.15 355.347,-174 351.847,-174 351.847,-174 351.847,-174 355.347,-174 351.847,-170.85 358.847,-174 358.847,-174\"/>\n",
        "<text text-anchor=\"start\" x=\"330\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
179
180
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
181
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
182
183
184
        "<path fill=\"none\" stroke=\"black\" d=\"M286.969,-190.664C285.406,-200.625 287.75,-210 294,-210 298.688,-210 301.178,-204.727 301.471,-197.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"301.031,-190.664 304.601,-197.46 301.244,-194.158 301.456,-197.651 301.456,-197.651 301.456,-197.651 301.244,-194.158 298.312,-197.842 301.031,-190.664 301.031,-190.664\"/>\n",
        "<text text-anchor=\"start\" x=\"290.5\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
185
        "</g>\n",
186
187
188
189
190
        "<!-- 3&#45;&gt;0 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M171.945,-178.448C152.386,-180.735 119.481,-182.984 92,-177 87.5445,-176.03 82.977,-174.44 78.6739,-172.629\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-169.66 79.8596,-169.708 75.3664,-171.116 78.5492,-172.572 78.5492,-172.572 78.5492,-172.572 75.3664,-171.116 77.2387,-175.437 72.1836,-169.66 72.1836,-169.66\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-199.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
191
        "<text text-anchor=\"start\" x=\"115\" y=\"-184.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
192
        "</g>\n",
193
194
195
196
197
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M202.448,-189.329C216.236,-204.254 240.941,-227.581 268,-237 289.826,-244.598 298.917,-246.468 320,-237 338.806,-228.555 353.873,-210.326 363.62,-195.64\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"367.468,-189.601 366.363,-197.197 365.587,-192.553 363.706,-195.504 363.706,-195.504 363.706,-195.504 365.587,-192.553 361.05,-193.812 367.468,-189.601 367.468,-189.601\"/>\n",
        "<text text-anchor=\"start\" x=\"276\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
198
        "</g>\n",
199
200
201
202
203
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M208.303,-175.661C224.962,-175.334 250.303,-174.837 268.927,-174.472\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"275.953,-174.334 269.016,-177.621 272.453,-174.403 268.954,-174.472 268.954,-174.472 268.954,-174.472 272.453,-174.403 268.892,-171.322 275.953,-174.334 275.953,-174.334\"/>\n",
        "<text text-anchor=\"start\" x=\"226\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
204
        "</g>\n",
205
206
207
208
209
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-191.916C178.679,-202.15 181.672,-212 190,-212 196.376,-212 199.625,-206.226 199.746,-198.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-191.916 202.872,-198.532 199.36,-195.395 199.741,-198.874 199.741,-198.874 199.741,-198.874 199.36,-195.395 196.61,-199.217 198.979,-191.916 198.979,-191.916\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-215.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
210
211
        "</g>\n",
        "</g>\n",
212
        "</svg>\n"
213
214
       ],
       "text": [
215
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc5466510> >"
216
217
218
219
220
221
222
223
224
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
225
      "The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve.  \n",
226
227
      "\n",
      "The letters used for this specification are as follows:\n",
228
      "\n",
229
230
      "- `t`: (inherently) terminal\n",
      "- `w`: (strictly inherently) weak\n",
231
232
      "- `s`: strong\n",
      "\n",
233
      "For instance if we want to preserve only the **strictly inherently weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it.  However the SCC above is not stricly weak, so it should not accept any word in the new automaton."
234
235
236
237
238
239
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
240
      "spot.decompose_scc(aut, 'w')"
241
242
243
244
245
246
247
248
249
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "svg": [
250
251
252
253
254
255
        "<?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",
256
257
258
        "<svg width=\"232pt\" height=\"255pt\"\n",
        " viewBox=\"0.00 0.00 232.00 255.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 251)\">\n",
259
        "<title>G</title>\n",
260
261
262
263
264
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-251 228,-251 228,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"91\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"113\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"129\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"89\" y=\"-218.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
265
266
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
267
        "</g>\n",
268
269
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"30,-116 30,-203 216,-203 216,-116 30,-116\"/>\n",
270
271
272
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
273
274
275
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-142\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-138.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
276
277
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
278
279
280
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-142C2.79388,-142 17.1543,-142 30.6317,-142\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-142 30.9419,-145.15 34.4419,-142 30.9419,-142 30.9419,-142 30.9419,-142 34.4419,-142 30.9418,-138.85 37.9419,-142 37.9419,-142\"/>\n",
281
282
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
283
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
284
285
286
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-159.037C48.3189,-168.858 50.4453,-178 56,-178 60.166,-178 62.4036,-172.858 62.7128,-166.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-159.037 65.8541,-165.882 62.5434,-162.533 62.7076,-166.03 62.7076,-166.03 62.7076,-166.03 62.5434,-162.533 59.561,-166.177 62.3792,-159.037 62.3792,-159.037\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
287
288
        "</g>\n",
        "<!-- 1 -->\n",
289
290
291
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
292
293
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
294
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
295
296
297
        "<path fill=\"none\" stroke=\"black\" d=\"M70.6291,-130.849C94.2674,-111.508 142.92,-71.7016 169.91,-49.6192\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.642,-44.9296 172.219,-51.8003 172.933,-47.146 170.224,-49.3623 170.224,-49.3623 170.224,-49.3623 172.933,-47.146 168.229,-46.9243 175.642,-44.9296 175.642,-44.9296\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
298
299
        "</g>\n",
        "<!-- 2 -->\n",
300
301
302
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-143\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-139.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
303
304
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
305
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
306
307
308
        "<path fill=\"none\" stroke=\"black\" d=\"M74.2567,-142.131C97.2816,-142.305 138.189,-142.615 164.429,-142.814\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.739,-142.869 164.715,-145.966 168.239,-142.843 164.739,-142.816 164.739,-142.816 164.739,-142.816 168.239,-142.843 164.763,-139.666 171.739,-142.869 171.739,-142.869\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-145.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
309
310
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
311
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
312
313
314
        "<path fill=\"none\" stroke=\"black\" d=\"M179.087,-48.4167C175.276,-59.166 178.914,-70 190,-70 198.661,-70 202.776,-63.3875 202.344,-55.3688\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"200.913,-48.4167 205.41,-54.6375 201.619,-51.8447 202.325,-55.2728 202.325,-55.2728 202.325,-55.2728 201.619,-51.8447 199.239,-55.9082 200.913,-48.4167 200.913,-48.4167\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
315
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
316
317
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
318
319
320
321
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M173.759,-151.123C167.774,-153.883 160.735,-156.618 154,-158 127.007,-163.54 118.925,-163.862 92,-158 87.5445,-157.03 82.977,-155.44 78.6739,-153.629\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-150.66 79.8596,-150.708 75.3664,-152.116 78.5492,-153.572 78.5492,-153.572 78.5492,-153.572 75.3664,-152.116 77.2387,-156.437 72.1836,-150.66 72.1836,-150.66\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
322
323
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
324
325
326
327
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M179.087,-157.417C175.276,-168.166 178.914,-179 190,-179 198.661,-179 202.776,-172.387 202.344,-164.369\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"200.913,-157.417 205.41,-163.637 201.619,-160.845 202.325,-164.273 202.325,-164.273 202.325,-164.273 201.619,-160.845 199.239,-164.908 200.913,-157.417 200.913,-157.417\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-182.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
328
329
        "</g>\n",
        "</g>\n",
330
        "</svg>\n"
331
332
       ],
       "text": [
333
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca420> >"
334
335
336
337
338
339
340
341
342
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
343
      "Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:"
344
345
346
347
348
349
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
350
      "spot.decompose_scc(aut, 't')"
351
352
353
354
355
356
357
358
359
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "svg": [
360
361
362
363
364
365
        "<?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",
366
367
368
        "<svg width=\"397pt\" height=\"165pt\"\n",
        " viewBox=\"0.00 0.00 397.00 165.21\" 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 161.207)\">\n",
369
        "<title>G</title>\n",
370
371
372
373
374
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-161.207 393,-161.207 393,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"173.5\" y=\"-143.007\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"195.5\" y=\"-143.007\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"211.5\" y=\"-143.007\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"171.5\" y=\"-129.007\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
375
376
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"329,-11.2072 329,-111.207 381,-111.207 381,-11.2072 329,-11.2072\"/>\n",
377
        "</g>\n",
378
379
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"246,-11.2072 246,-96.2072 298,-96.2072 298,-11.2072 246,-11.2072\"/>\n",
380
        "</g>\n",
381
382
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"30,-9.20721 30,-96.2072 194,-96.2072 194,-9.20721 30,-9.20721\"/>\n",
383
384
385
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
386
387
388
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-35.2072\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-31.5072\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
389
390
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
391
392
393
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-35.2072C2.79388,-35.2072 17.1543,-35.2072 30.6317,-35.2072\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-35.2072 30.9419,-38.3573 34.4419,-35.2073 30.9419,-35.2073 30.9419,-35.2073 30.9419,-35.2073 34.4419,-35.2073 30.9418,-32.0573 37.9419,-35.2072 37.9419,-35.2072\"/>\n",
394
395
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
396
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
397
398
399
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-52.2445C48.3189,-62.0651 50.4453,-71.2072 56,-71.2072 60.166,-71.2072 62.4036,-66.0648 62.7128,-59.3505\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-52.2445 65.8541,-59.0891 62.5434,-55.7407 62.7076,-59.2368 62.7076,-59.2368 62.7076,-59.2368 62.5434,-55.7407 59.561,-59.3846 62.3792,-52.2445 62.3792,-52.2445\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-75.0072\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
400
        "</g>\n",
401
402
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
403
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
404
        "<text text-anchor=\"middle\" x=\"355\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
405
        "</g>\n",
406
407
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
408
409
410
        "<path fill=\"none\" stroke=\"black\" d=\"M73.0478,-29.4272C112.119,-16.1948 215.065,13.6081 298,-7.20721 310.58,-10.3645 323.419,-16.9513 333.624,-23.1507\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"339.612,-26.9265 332.011,-25.8575 336.652,-25.0597 333.691,-23.1929 333.691,-23.1929 333.691,-23.1929 336.652,-25.0597 335.371,-20.5284 339.612,-26.9265 339.612,-26.9265\"/>\n",
        "<text text-anchor=\"start\" x=\"216.5\" y=\"-6.00721\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
411
        "</g>\n",
412
413
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
414
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
415
        "<text text-anchor=\"middle\" x=\"168\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
416
        "</g>\n",
417
418
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
419
420
421
        "<path fill=\"none\" stroke=\"black\" d=\"M74.2788,-35.363C89.4809,-35.5178 112.211,-35.7926 132,-36.2072 135.464,-36.2798 139.121,-36.3696 142.713,-36.4654\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"149.911,-36.6669 142.826,-39.6197 146.413,-36.5689 142.914,-36.471 142.914,-36.471 142.914,-36.471 146.413,-36.5689 143.002,-33.3222 149.911,-36.6669 149.911,-36.6669\"/>\n",
        "<text text-anchor=\"start\" x=\"94\" y=\"-40.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
422
        "</g>\n",
423
424
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
425
426
427
        "<path fill=\"none\" stroke=\"black\" d=\"M347.969,-53.8713C346.406,-63.8322 348.75,-73.2072 355,-73.2072 359.688,-73.2072 362.178,-67.9338 362.471,-61.0948\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"362.031,-53.8713 365.601,-60.667 362.244,-57.3648 362.456,-60.8584 362.456,-60.8584 362.456,-60.8584 362.244,-57.3648 359.312,-61.0497 362.031,-53.8713 362.031,-53.8713\"/>\n",
        "<text text-anchor=\"start\" x=\"350.5\" y=\"-92.0072\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
428
        "<text text-anchor=\"start\" x=\"347\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
429
430
        "</g>\n",
        "<!-- 3 -->\n",
431
432
433
        "<g id=\"node4\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"272\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
434
        "</g>\n",
435
436
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
437
438
439
        "<path fill=\"none\" stroke=\"black\" d=\"M290.178,-37.2072C301.669,-37.2072 316.959,-37.2072 329.693,-37.2072\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"336.847,-37.2072 329.847,-40.3573 333.347,-37.2073 329.847,-37.2073 329.847,-37.2073 329.847,-37.2073 333.347,-37.2073 329.847,-34.0573 336.847,-37.2072 336.847,-37.2072\"/>\n",
        "<text text-anchor=\"start\" x=\"308\" y=\"-41.0072\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
440
441
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
442
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
443
444
445
        "<path fill=\"none\" stroke=\"black\" d=\"M264.969,-53.8713C263.406,-63.8322 265.75,-73.2072 272,-73.2072 276.688,-73.2072 279.178,-67.9338 279.471,-61.0948\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"279.031,-53.8713 282.601,-60.667 279.244,-57.3648 279.456,-60.8584 279.456,-60.8584 279.456,-60.8584 279.244,-57.3648 276.312,-61.0497 279.031,-53.8713 279.031,-53.8713\"/>\n",
        "<text text-anchor=\"start\" x=\"268.5\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
446
        "</g>\n",
447
448
        "<!-- 2&#45;&gt;0 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
449
450
451
        "<path fill=\"none\" stroke=\"black\" d=\"M151.358,-44.9402C145.443,-47.4659 138.555,-49.9449 132,-51.2072 114.543,-54.5691 109.371,-54.9894 92,-51.2072 87.5445,-50.2371 82.977,-48.647 78.6739,-46.8365\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-43.8674 79.8596,-43.915 75.3664,-45.3234 78.5492,-46.7795 78.5492,-46.7795 78.5492,-46.7795 75.3664,-45.3234 77.2387,-49.644 72.1836,-43.8674 72.1836,-43.8674\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-58.0072\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
452
        "</g>\n",
453
454
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
455
456
457
        "<path fill=\"none\" stroke=\"black\" d=\"M180.109,-50.6899C193.757,-66.0814 218.509,-90.3938 246,-100.207 267.766,-107.977 276.917,-109.675 298,-100.207 316.806,-91.762 331.873,-73.5336 341.62,-58.8467\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"345.468,-52.808 344.363,-60.4043 343.587,-55.7599 341.706,-58.7117 341.706,-58.7117 341.706,-58.7117 343.587,-55.7599 339.05,-57.0191 345.468,-52.808 345.468,-52.808\"/>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-110.007\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
458
        "</g>\n",
459
460
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
461
462
463
        "<path fill=\"none\" stroke=\"black\" d=\"M186.303,-37.2072C202.962,-37.2072 228.303,-37.2072 246.927,-37.2072\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"253.953,-37.2072 246.953,-40.3573 250.453,-37.2073 246.953,-37.2073 246.953,-37.2073 246.953,-37.2073 250.453,-37.2073 246.953,-34.0573 253.953,-37.2072 253.953,-37.2072\"/>\n",
        "<text text-anchor=\"start\" x=\"204\" y=\"-41.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
464
        "</g>\n",
465
466
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
467
468
469
        "<path fill=\"none\" stroke=\"black\" d=\"M159.021,-53.1232C156.679,-63.3576 159.672,-73.2072 168,-73.2072 174.376,-73.2072 177.625,-67.4336 177.746,-60.134\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"176.979,-53.1232 180.872,-59.7387 177.36,-56.6024 177.741,-60.0816 177.741,-60.0816 177.741,-60.0816 177.36,-56.6024 174.61,-60.4246 176.979,-53.1232 176.979,-53.1232\"/>\n",
        "<text text-anchor=\"start\" x=\"150\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
470
471
        "</g>\n",
        "</g>\n",
472
        "</svg>\n"
473
474
       ],
       "text": [
475
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca1b0> >"
476
477
478
479
480
481
482
483
484
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
485
      "Here is the **strong** part:"
486
487
488
489
490
491
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
492
      "strong = spot.decompose_scc(aut, 's'); strong"
493
494
495
496
497
498
499
500
501
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "svg": [
502
503
504
505
506
507
        "<?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",
508
509
510
        "<svg width=\"210pt\" height=\"162pt\"\n",
        " viewBox=\"0.00 0.00 210.00 162.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 158)\">\n",
511
        "<title>G</title>\n",
512
513
514
515
516
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-158 206,-158 206,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"80\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"102\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"118\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"78\" y=\"-125.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
517
518
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-8 30,-110 194,-110 194,-8 30,-8\"/>\n",
519
520
521
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
522
523
524
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-35\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-31.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
525
526
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
527
528
529
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-35C2.79388,-35 17.1543,-35 30.6317,-35\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-35 30.9419,-38.1501 34.4419,-35 30.9419,-35.0001 30.9419,-35.0001 30.9419,-35.0001 34.4419,-35 30.9418,-31.8501 37.9419,-35 37.9419,-35\"/>\n",
530
531
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
532
533
534
535
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-52.0373C48.3189,-61.8579 50.4453,-71 56,-71 60.166,-71 62.4036,-65.8576 62.7128,-59.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-52.0373 65.8541,-58.8818 62.5434,-55.5335 62.7076,-59.0296 62.7076,-59.0296 62.7076,-59.0296 62.5434,-55.5335 59.561,-59.1774 62.3792,-52.0373 62.3792,-52.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-89.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
536
        "<text text-anchor=\"start\" x=\"48\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
537
538
        "</g>\n",
        "<!-- 1 -->\n",
539
540
541
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"168\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
542
543
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
544
545
546
547
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.0256,-34.0467C89.2577,-33.4204 112.175,-33.0369 132,-35 135.683,-35.3646 139.552,-35.9401 143.32,-36.6081\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"150.366,-37.9759 142.894,-39.7343 146.93,-37.3089 143.495,-36.642 143.495,-36.642 143.495,-36.642 146.93,-37.3089 144.095,-33.5497 150.366,-37.9759 150.366,-37.9759\"/>\n",
        "<text text-anchor=\"start\" x=\"94\" y=\"-38.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
548
549
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
550
551
552
553
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M150.474,-46.6588C135.183,-50.2874 111.882,-54.081 92,-50 87.5802,-49.0928 83.0294,-47.6032 78.7315,-45.9062\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.2412,-43.1226 79.9161,-42.9868 75.4579,-44.5022 78.6745,-45.8818 78.6745,-45.8818 78.6745,-45.8818 75.4579,-44.5022 77.4329,-48.7768 72.2412,-43.1226 72.2412,-43.1226\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-69.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
554
        "<text text-anchor=\"start\" x=\"104\" y=\"-54.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
555
556
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
557
558
559
560
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M158.425,-57.5414C155.73,-67.9087 158.922,-78 168,-78 174.95,-78 178.45,-72.0847 178.499,-64.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"177.575,-57.5414 181.6,-64.0771 178.026,-61.0123 178.477,-64.4831 178.477,-64.4831 178.477,-64.4831 178.026,-61.0123 175.353,-64.889 177.575,-57.5414 177.575,-57.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"150\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
561
562
        "</g>\n",
        "</g>\n",
563
        "</svg>\n"
564
565
       ],
       "text": [
566
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc5466330> >"
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
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The union of these three automata recognize the same language as the original automaton.\n",
      "\n",
      "\n",
      "The application proposed in the aforementioned TACAS'13 paper is for parallelizing model checking.  Instead of testing the emptiness of the product between `aut` and a system, one could test the emptiness **3** products in parallel: each with a sub-automaton of different strength.  Model checking using weak and terminal automata can be done with much more simpler emptiness check procedures than needed for the general case.  So in effect, we have isolated the \"hard\" (i.e. strong) part of the original automaton in a smaller automaton, and we only need to use a full-fledged emptiness check for this case.\n",
      "\n",
      "An additional bonus is that it is possible that the simplification algorithms will do a better job at simplifying the sub-automata than at simplifying the original `aut`.  For instance here the `strong` automaton can be further simplified:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "strong.postprocess('small')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 6,
       "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",
604
605
606
        "<svg width=\"98pt\" height=\"193pt\"\n",
        " viewBox=\"0.00 0.00 98.00 193.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 189)\">\n",
607
        "<title>G</title>\n",
608
609
610
611
612
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-189 94,-189 94,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"24\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"46\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"62\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"22\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
613
614
615
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-8 30,-141 82,-141 82,-8 30,-8\"/>\n",
        "</g>\n",
616
617
618
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
619
620
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
621
622
623
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
624
625
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-34C2.79388,-34 17.1543,-34 30.6317,-34\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-34 30.9419,-37.1501 34.4419,-34 30.9419,-34.0001 30.9419,-34.0001 30.9419,-34.0001 34.4419,-34 30.9418,-30.8501 37.9419,-34 37.9419,-34\"/>\n",
626
627
628
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
629
630
        "<path fill=\"none\" stroke=\"black\" d=\"M52.7643,-51.7817C52.2144,-61.3149 53.293,-70 56,-70 57.988,-70 59.0977,-65.3161 59.3292,-59.0521\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"59.2357,-51.7817 62.4756,-58.7406 59.2808,-55.2814 59.3258,-58.7812 59.3258,-58.7812 59.3258,-58.7812 59.2808,-55.2814 56.1761,-58.8217 59.2357,-51.7817 59.2357,-51.7817\"/>\n",
631
632
        "<text text-anchor=\"start\" x=\"36\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
        "<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
633
634
635
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
636
637
638
        "<path fill=\"none\" stroke=\"black\" d=\"M50.9906,-51.5771C47.5451,-72.718 49.2148,-100 56,-100 62.043,-100 64.0285,-78.3596 61.9564,-58.6907\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"61.0094,-51.5771 65.0556,-58.1002 61.4713,-55.0465 61.9332,-58.5159 61.9332,-58.5159 61.9332,-58.5159 61.4713,-55.0465 58.8107,-58.9316 61.0094,-51.5771 61.0094,-51.5771\"/>\n",
        "<text text-anchor=\"start\" x=\"38\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
639
640
641
642
643
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
644
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca180> >"
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Multi-strength extraction\n",
      "\n",
      "The string passed to `decompose_strength()` can include multiple letters to extract multiple strengths at once."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for opt in ('sw', 'st', 'wt'):\n",
664
      "    a = spot.decompose_scc(aut, opt)\n",
665
      "    a.set_name(\"option: \" + opt)\n",
666
      "    display(a)"
667
668
669
670
671
672
673
674
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
675
676
677
678
679
680
        "<?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",
681
682
683
        "<svg width=\"232pt\" height=\"284pt\"\n",
        " viewBox=\"0.00 0.00 232.00 284.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 280)\">\n",
684
        "<title>G</title>\n",
685
686
687
688
689
690
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-280 228,-280 228,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"78.5\" y=\"-261.8\" font-family=\"Lato\" font-size=\"14.00\">option: sw</text>\n",
        "<text text-anchor=\"start\" x=\"91\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"113\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"129\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"89\" y=\"-233.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
691
692
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
693
        "</g>\n",
694
695
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-116 30,-218 216,-218 216,-116 30,-116\"/>\n",
696
697
698
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
699
700
701
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-142\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-138.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
702
703
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
704
705
706
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-142C2.79388,-142 17.1543,-142 30.6317,-142\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-142 30.9419,-145.15 34.4419,-142 30.9419,-142 30.9419,-142 30.9419,-142 34.4419,-142 30.9418,-138.85 37.9419,-142 37.9419,-142\"/>\n",
707
708
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
709
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
710
711
712
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-159.037C48.3189,-168.858 50.4453,-178 56,-178 60.166,-178 62.4036,-172.858 62.7128,-166.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-159.037 65.8541,-165.882 62.5434,-162.533 62.7076,-166.03 62.7076,-166.03 62.7076,-166.03 62.5434,-162.533 59.561,-166.177 62.3792,-159.037 62.3792,-159.037\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
713
        "<text text-anchor=\"start\" x=\"48\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
714
715
        "</g>\n",
        "<!-- 1 -->\n",
716
717
718
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
719
720
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
721
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
722
723
724
        "<path fill=\"none\" stroke=\"black\" d=\"M70.6291,-130.849C94.2674,-111.508 142.92,-71.7016 169.91,-49.6192\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.642,-44.9296 172.219,-51.8003 172.933,-47.146 170.224,-49.3623 170.224,-49.3623 170.224,-49.3623 172.933,-47.146 168.229,-46.9243 175.642,-44.9296 175.642,-44.9296\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
725
726
        "</g>\n",
        "<!-- 2 -->\n",
727
728
729
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-150\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
730
731
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
732
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
733
734
735
        "<path fill=\"none\" stroke=\"black\" d=\"M74.2268,-141.209C93.6634,-140.542 126.194,-140.102 154,-143 157.681,-143.384 161.549,-143.969 165.316,-144.642\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"172.363,-146.011 164.89,-147.768 168.927,-145.344 165.491,-144.676 165.491,-144.676 165.491,-144.676 168.927,-145.344 166.092,-141.583 172.363,-146.011 172.363,-146.011\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
736
737
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
738
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
739
740
741
        "<path fill=\"none\" stroke=\"black\" d=\"M179.087,-48.4167C175.276,-59.166 178.914,-70 190,-70 198.661,-70 202.776,-63.3875 202.344,-55.3688\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"200.913,-48.4167 205.41,-54.6375 201.619,-51.8447 202.325,-55.2728 202.325,-55.2728 202.325,-55.2728 201.619,-51.8447 199.239,-55.9082 200.913,-48.4167 200.913,-48.4167\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
742
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
743
744
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
745
746
747
748
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M172.397,-154.598C166.622,-155.982 160.07,-157.315 154,-158 126.618,-161.09 118.925,-163.862 92,-158 87.5445,-157.03 82.977,-155.44 78.6739,-153.629\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-150.66 79.8596,-150.708 75.3664,-152.116 78.5492,-153.572 78.5492,-153.572 78.5492,-153.572 75.3664,-152.116 77.2387,-156.437 72.1836,-150.66 72.1836,-150.66\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
749
        "<text text-anchor=\"start\" x=\"115\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
750
751
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
752
753
754
755
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M179.087,-164.417C175.276,-175.166 178.914,-186 190,-186 198.661,-186 202.776,-179.387 202.344,-171.369\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"200.913,-164.417 205.41,-170.637 201.619,-167.845 202.325,-171.273 202.325,-171.273 202.325,-171.273 201.619,-167.845 199.239,-171.908 200.913,-164.417 200.913,-164.417\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-189.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
756
757
        "</g>\n",
        "</g>\n",
758
        "</svg>\n"
759
760
       ],
       "text": [
761
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca360> >"
762
763
764
765
766
767
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
768
769
770
771
772
773
        "<?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",
774
775
776
        "<svg width=\"397pt\" height=\"189pt\"\n",
        " viewBox=\"0.00 0.00 397.00 189.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 185)\">\n",
777
        "<title>G</title>\n",
778
779
780
781
782
783
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-185 393,-185 393,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"164\" y=\"-166.8\" font-family=\"Lato\" font-size=\"14.00\">option: st</text>\n",
        "<text text-anchor=\"start\" x=\"173.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"195.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"211.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"171.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
784
785
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"329,-21 329,-121 381,-121 381,-21 329,-21\"/>\n",
786
        "</g>\n",
787
788
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"246,-21 246,-106 298,-106 298,-21 246,-21\"/>\n",
789
        "</g>\n",
790
791
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-8 30,-110 194,-110 194,-8 30,-8\"/>\n",
792
793
794
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
795
796
797
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
798
799
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
800
801
802
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-34C2.79388,-34 17.1543,-34 30.6317,-34\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-34 30.9419,-37.1501 34.4419,-34 30.9419,-34.0001 30.9419,-34.0001 30.9419,-34.0001 34.4419,-34 30.9418,-30.8501 37.9419,-34 37.9419,-34\"/>\n",
803
804
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
805
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
806
807
808
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-51.0373C48.3189,-60.8579 50.4453,-70 56,-70 60.166,-70 62.4036,-64.8576 62.7128,-58.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-51.0373 65.8541,-57.8818 62.5434,-54.5335 62.7076,-58.0296 62.7076,-58.0296 62.7076,-58.0296 62.5434,-54.5335 59.561,-58.1774 62.3792,-51.0373 62.3792,-51.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
809
        "<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
810
        "</g>\n",
811
812
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
813
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-47\" rx=\"18\" ry=\"18\"/>\n",
814
        "<text text-anchor=\"middle\" x=\"355\" y=\"-43.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
815
        "</g>\n",
816
817
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
818
819
820
        "<path fill=\"none\" stroke=\"black\" d=\"M73.6763,-29.2967C113.28,-18.8831 215.821,3.62551 298,-17 310.58,-20.1573 323.419,-26.7441 333.624,-32.9435\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"339.612,-36.7193 332.011,-35.6503 336.652,-34.8525 333.691,-32.9857 333.691,-32.9857 333.691,-32.9857 336.652,-34.8525 335.371,-30.3212 339.612,-36.7193 339.612,-36.7193\"/>\n",
        "<text text-anchor=\"start\" x=\"216.5\" y=\"-12.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
821
        "</g>\n",
822
823
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
824
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-50\" rx=\"18\" ry=\"18\"/>\n",
825
        "<text text-anchor=\"middle\" x=\"168\" y=\"-46.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
826
        "</g>\n",
827
828
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
829
830
831
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1884,-32.3468C89.5275,-31.3146 112.51,-30.864 132,-35 136.414,-35.9366 140.962,-37.44 145.259,-39.1413\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.749,-41.9248 144.074,-42.0607 148.532,-40.5453 145.316,-39.1657 145.316,-39.1657 145.316,-39.1657 148.532,-40.5453 146.557,-36.2707 151.749,-41.9248 151.749,-41.9248\"/>\n",
        "<text text-anchor=\"start\" x=\"94\" y=\"-38.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
832
        "</g>\n",
833
834
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
835
836
837
        "<path fill=\"none\" stroke=\"black\" d=\"M347.969,-63.6641C346.406,-73.625 348.75,-83 355,-83 359.688,-83 362.178,-77.7266 362.471,-70.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"362.031,-63.6641 365.601,-70.4598 362.244,-67.1576 362.456,-70.6511 362.456,-70.6511 362.456,-70.6511 362.244,-67.1576 359.312,-70.8425 362.031,-63.6641 362.031,-63.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"350.5\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
838
        "<text text-anchor=\"start\" x=\"347\" y=\"-86.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
839
840
        "</g>\n",
        "<!-- 3 -->\n",
841
842
843
        "<g id=\"node4\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-47\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"272\" y=\"-43.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
844
        "</g>\n",
845
846
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
847
848
849
        "<path fill=\"none\" stroke=\"black\" d=\"M290.178,-47C301.669,-47 316.959,-47 329.693,-47\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"336.847,-47 329.847,-50.1501 333.347,-47 329.847,-47.0001 329.847,-47.0001 329.847,-47.0001 333.347,-47 329.847,-43.8501 336.847,-47 336.847,-47\"/>\n",
        "<text text-anchor=\"start\" x=\"308\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
850
851
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
852
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
853
854
855
        "<path fill=\"none\" stroke=\"black\" d=\"M264.969,-63.6641C263.406,-73.625 265.75,-83 272,-83 276.688,-83 279.178,-77.7266 279.471,-70.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"279.031,-63.6641 282.601,-70.4598 279.244,-67.1576 279.456,-70.6511 279.456,-70.6511 279.456,-70.6511 279.244,-67.1576 276.312,-70.8425 279.031,-63.6641 279.031,-63.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"268.5\" y=\"-86.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
856
        "</g>\n",
857
858
        "<!-- 2&#45;&gt;0 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
859
860
861
        "<path fill=\"none\" stroke=\"black\" d=\"M150.1,-52.0318C134.754,-53.3995 111.593,-54.2661 92,-50 87.5445,-49.0299 82.977,-47.4398 78.6739,-45.6293\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-42.6602 79.8596,-42.7078 75.3664,-44.1162 78.5492,-45.5723 78.5492,-45.5723 78.5492,-45.5723 75.3664,-44.1162 77.2387,-48.4368 72.1836,-42.6602 72.1836,-42.6602\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
862
        "<text text-anchor=\"start\" x=\"104\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
863
        "</g>\n",
864
865
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
866
867
868
        "<path fill=\"none\" stroke=\"black\" d=\"M180.495,-63.1155C194.327,-77.7993 219.074,-100.748 246,-110 267.857,-117.51 276.917,-119.468 298,-110 316.806,-101.555 331.873,-83.3264 341.62,-68.6395\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"345.468,-62.6008 344.363,-70.1971 343.587,-65.5526 341.706,-68.5045 341.706,-68.5045 341.706,-68.5045 343.587,-65.5526 339.05,-66.8119 345.468,-62.6008 345.468,-62.6008\"/>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
869
        "</g>\n",
870
871
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
872
873
874
        "<path fill=\"none\" stroke=\"black\" d=\"M186.303,-49.4911C202.962,-49.0011 228.303,-48.2558 246.927,-47.708\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"253.953,-47.5014 247.048,-50.8559 250.454,-47.6043 246.956,-47.7073 246.956,-47.7073 246.956,-47.7073 250.454,-47.6043 246.863,-44.5586 253.953,-47.5014 253.953,-47.5014\"/>\n",
        "<text text-anchor=\"start\" x=\"204\" y=\"-52.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
875
        "</g>\n",
876
877
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
878
879
880
        "<path fill=\"none\" stroke=\"black\" d=\"M159.021,-65.916C156.679,-76.1504 159.672,-86 168,-86 174.376,-86 177.625,-80.2263 177.746,-72.9268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"176.979,-65.916 180.872,-72.5315 177.36,-69.3952 177.741,-72.8744 177.741,-72.8744 177.741,-72.8744 177.36,-69.3952 174.61,-73.2174 176.979,-65.916 176.979,-65.916\"/>\n",
        "<text text-anchor=\"start\" x=\"150\" y=\"-89.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
881
882
        "</g>\n",
        "</g>\n",
883
        "</svg>\n"
884
885
       ],
       "text": [
886
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca120> >"
887
888
889
890
891
892
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
893
894
895
896
897
898
        "<?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",
899
900
901
        "<svg width=\"419pt\" height=\"316pt\"\n",
        " viewBox=\"0.00 0.00 419.00 316.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 312)\">\n",
902
        "<title>G</title>\n",
903
904
905
906
907
908
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-312 415,-312 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-293.8\" font-family=\"Lato\" font-size=\"14.00\">option: wt</text>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"182.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
909
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
910
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-148 351,-248 403,-248 403,-148 351,-148\"/>\n",
911
        "</g>\n",
912
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
913
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
914
        "</g>\n",
915
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
916
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-148 268,-233 320,-233 320,-148 268,-148\"/>\n",
917
        "</g>\n",
918
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
919
        "<polygon fill=\"none\" stroke=\"red\" points=\"30,-146 30,-233 216,-233 216,-146 30,-146\"/>\n",
920
921
922
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
923
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
924
925
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
926
927
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
928
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
929
930
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-172C2.79388,-172 17.1543,-172 30.6317,-172\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-172 30.9419,-175.15 34.4419,-172 30.9419,-172 30.9419,-172 30.9419,-172 34.4419,-172 30.9418,-168.85 37.9419,-172 37.9419,-172\"/>\n",
931
932
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
933
934
935
936
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-189.037C48.3189,-198.858 50.4453,-208 56,-208 60.166,-208 62.4036,-202.858 62.7128,-196.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-189.037 65.8541,-195.882 62.5434,-192.533 62.7076,-196.03 62.7076,-196.03 62.7076,-196.03 62.5434,-192.533 59.561,-196.177 62.3792,-189.037 62.3792,-189.037\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-211.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
937
938
        "</g>\n",
        "<!-- 1 -->\n",
939
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
940
941
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"377\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"377\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
942
943
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
944
945
946
947
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.2845,-166.381C114.974,-152.825 228.7,-121.085 320,-144 332.58,-147.157 345.419,-153.744 355.624,-159.943\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.612,-163.719 354.011,-162.65 358.652,-161.852 355.691,-159.986 355.691,-159.986 355.691,-159.986 358.652,-161.852 357.371,-157.321 361.612,-163.719 361.612,-163.719\"/>\n",
        "<text text-anchor=\"start\" x=\"238.5\" y=\"-140.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
948
949
        "</g>\n",
        "<!-- 2 -->\n",
950
951
952
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
953
954
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
955
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
956
957
958
959
960
961
962
963
964
965
966
967
968
969
        "<path fill=\"none\" stroke=\"black\" d=\"M62.2786,-154.873C67.789,-139.056 77.6458,-115.574 92,-99 113.168,-74.5588 145.613,-55.3414 167.065,-44.3263\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"173.345,-41.1744 168.502,-47.1297 170.217,-42.7444 167.089,-44.3144 167.089,-44.3144 167.089,-44.3144 170.217,-42.7444 165.676,-41.499 173.345,-41.1744 173.345,-41.1744\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1729,-172.082C93.5612,-172.197 126.049,-172.457 154,-173 157.464,-173.067 161.121,-173.154 164.713,-173.249\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.912,-173.449 164.827,-176.403 168.413,-173.352 164.914,-173.254 164.914,-173.254 164.914,-173.254 168.413,-173.352 165.002,-170.105 171.912,-173.449 171.912,-173.449\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-176.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
970
971
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
972
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
973
974
975
        "<path fill=\"none\" stroke=\"black\" d=\"M369.969,-190.664C368.406,-200.625 370.75,-210 377,-210 381.688,-210 384.178,-204.727 384.471,-197.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"384.031,-190.664 387.601,-197.46 384.244,-194.158 384.456,-197.651 384.456,-197.651 384.456,-197.651 384.244,-194.158 381.312,-197.842 384.031,-190.664 384.031,-190.664\"/>\n",
        "<text text-anchor=\"start\" x=\"372.5\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
976
        "<text text-anchor=\"start\" x=\"369\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
977
        "</g>\n",
978
979
980
981
982
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-49.916C178.679,-60.1504 181.672,-70 190,-70 196.376,-70 199.625,-64.2263 199.746,-56.9268\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-49.916 202.872,-56.5315 199.36,-53.3952 199.741,-56.8744 199.741,-56.8744 199.741,-56.8744 199.36,-53.3952 196.61,-57.2174 198.979,-49.916 198.979,-49.916\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
983
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
984
985
        "</g>\n",
        "<!-- 4 -->\n",
986
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
987
988
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"294\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"294\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
989
        "</g>\n",
990
991
992
993
994
        "<!-- 4&#45;&gt;1 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M312.178,-174C323.669,-174 338.959,-174 351.693,-174\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"358.847,-174 351.847,-177.15 355.347,-174 351.847,-174 351.847,-174 351.847,-174 355.347,-174 351.847,-170.85 358.847,-174 358.847,-174\"/>\n",
        "<text text-anchor=\"start\" x=\"330\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
995
996
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
997
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
998
999
1000
        "<path fill=\"none\" stroke=\"black\" d=\"M286.969,-190.664C285.406,-200.625 287.75,-210 294,-210 298.688,-210 301.178,-204.727 301.471,-197.888\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"301.031,-190.664 304.601,-197.46 301.244,-194.158 301.456,-197.651 301.456,-197.651 301.456,-197.651 301.244,-194.158 298.312,-197.842 301.031,-190.664 301.031,-190.664\"/>\n",
        "<text text-anchor=\"start\" x=\"290.5\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
1001
        "</g>\n",
1002
1003
1004
1005
1006
        "<!-- 3&#45;&gt;0 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M173.358,-181.733C167.443,-184.259 160.555,-186.738 154,-188 126.942,-193.211 118.925,-193.862 92,-188 87.5445,-187.03 82.977,-185.44 78.6739,-183.629\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-180.66 79.8596,-180.708 75.3664,-182.116 78.5492,-183.572 78.5492,-183.572 78.5492,-183.572 75.3664,-182.116 77.2387,-186.437 72.1836,-180.66 72.1836,-180.66\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1007
        "</g>\n",
1008
1009
1010
1011
1012
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M202.109,-187.483C215.757,-202.874 240.509,-227.187 268,-237 289.766,-244.77 298.917,-246.468 320,-237 338.806,-228.555 353.873,-210.326 363.62,-195.64\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"367.468,-189.601 366.363,-197.197 365.587,-192.553 363.706,-195.504 363.706,-195.504 363.706,-195.504 365.587,-192.553 361.05,-193.812 367.468,-189.601 367.468,-189.601\"/>\n",
        "<text text-anchor=\"start\" x=\"276\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1013
        "</g>\n",
1014
1015
1016
1017
1018
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M208.303,-174C224.962,-174 250.303,-174 268.927,-174\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"275.953,-174 268.953,-177.15 272.453,-174 268.953,-174 268.953,-174 268.953,-174 272.453,-174 268.953,-170.85 275.953,-174 275.953,-174\"/>\n",
        "<text text-anchor=\"start\" x=\"226\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
1019
        "</g>\n",
1020
1021
1022
1023
1024
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-189.916C178.679,-200.15 181.672,-210 190,-210 196.376,-210 199.625,-204.226 199.746,-196.927\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-189.916 202.872,-196.532 199.36,-193.395 199.741,-196.874 199.741,-196.874 199.741,-196.874 199.36,-193.395 196.61,-197.217 198.979,-189.916 198.979,-189.916\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
1025
1026
        "</g>\n",
        "</g>\n",
1027
        "</svg>\n"
1028
1029
       ],
       "text": [
1030
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca390> >"
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Generalized acceptance\n",
      "\n",
1042
      "There is nothing that prevents the above decomposition to work with other types of acceptance.\n",
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
      "\n",
      "## Rabin\n",
      "\n",
      "The following Rabin automaton was generated with\n",
      "\n",
      "    ltldo -f '(Ga -> Gb) W c' 'ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds' -H | autfilt -H --merge-transitions\n",
      "    \n",
      "(The `autfilt -H --merge-transitions` pass is just here to reduce the size of the file and make the automaton more readable.)"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.automaton(\"\"\"\n",
      "HOA: v1\n",
      "States: 9\n",
      "Start: 2\n",
      "AP: 3 \"a\" \"b\" \"c\"\n",
      "acc-name: Rabin 2\n",
      "Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
      "properties: trans-labels explicit-labels state-acc complete\n",
      "properties: deterministic\n",
      "--BODY--\n",
      "State: 0 {2}\n",
      "[0&!2] 0\n",
      "[0&2] 1\n",
      "[!0&!2] 5\n",
      "[!0&2] 6\n",
      "State: 1 {2}\n",
      "[0] 1\n",
      "[!0] 6\n",
      "State: 2 {2}\n",
      "[0&!1&!2] 3\n",
      "[0&1&!2] 4\n",
      "[!0&!2] 5\n",
      "[2] 6\n",
      "State: 3 {1 2}\n",
      "[0&!2] 0\n",
      "[0&2] 1\n",
      "[!0&!2] 5\n",
      "[!0&2] 6\n",
      "State: 4 {1 2}\n",
      "[0&!1&!2] 0\n",
      "[0&!1&2] 1\n",
      "[!0&!2] 5\n",
      "[!0&2] 6\n",
      "[0&1&!2] 7\n",
      "[0&1&2] 8\n",
      "State: 5 {1 2}\n",
      "[0&!1&!2] 0\n",
      "[!0&!2] 5\n",
      "[2] 6\n",
      "[0&1&!2] 7\n",
      "State: 6 {1 2}\n",
      "[t] 6\n",
      "State: 7 {3}\n",
      "[0&!1&!2] 0\n",
      "[0&!1&2] 1\n",
      "[!0&!2] 5\n",
      "[!0&2] 6\n",
      "[0&1&!2] 7\n",
      "[0&1&2] 8\n",
      "State: 8 {3}\n",
      "[0&!1] 1\n",
      "[!0] 6\n",
      "[0&1] 8\n",
      "--END--\n",
      "\"\"\")\n",
1112
      "aut"
1113
1114
1115
1116
1117
1118
1119
1120
1121
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 8,
       "svg": [
1122
1123
1124
1125
1126
1127
        "<?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",
1128
1129
1130
        "<svg width=\"582pt\" height=\"360pt\"\n",
        " viewBox=\"0.00 0.00 581.88 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.565149 0.565149) rotate(0) translate(4 633)\">\n",
1131
        "<title>G</title>\n",
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-633 1025.61,-633 1025.61,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"394.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\">(Fin(</text>\n",
        "<text text-anchor=\"start\" x=\"422.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"438.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"481.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"497.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\">)) | (Fin(</text>\n",
        "<text text-anchor=\"start\" x=\"544.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",
        "<text text-anchor=\"start\" x=\"560.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"603.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">\u2778</text>\n",
        "<text text-anchor=\"start\" x=\"619.304\" y=\"-614.8\" font-family=\"Lato\" font-size=\"14.00\">))</text>\n",
        "<text text-anchor=\"start\" x=\"481.804\" y=\"-600.8\" font-family=\"Lato\" font-size=\"14.00\">[Rabin 2]</text>\n",
1143
1144
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"929.725,-283 929.725,-400 1013.61,-400 1013.61,-283 929.725,-283\"/>\n",
1145
        "</g>\n",
1146
1147
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"828.985,-221 828.985,-324 898.725,-324 898.725,-221 828.985,-221\"/>\n",
1148
        "</g>\n",
1149
1150
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"828.985,-8 828.985,-111 898.725,-111 898.725,-8 828.985,-8\"/>\n",
1151
        "</g>\n",
1152
1153
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"355.622,-217 355.622,-385 746.985,-385 746.985,-217 355.622,-217\"/>\n",
1154
        "</g>\n",
1155
1156
        "<g id=\"clust5\" class=\"cluster\"><title>cluster_4</title>\n",
        "<polygon fill=\"none\" stroke=\"black\" points=\"185.74,-376 185.74,-460 269.622,-460 269.622,-376 185.74,-376\"/>\n",
1157
        "</g>\n",
1158
1159
        "<g id=\"clust6\" class=\"cluster\"><title>cluster_5</title>\n",
        "<polygon fill=\"none\" stroke=\"black\" points=\"185.74,-131 185.74,-215 269.622,-215 269.622,-131 185.74,-131\"/>\n",
1160
        "</g>\n",
1161
1162
        "<g id=\"clust7\" class=\"cluster\"><title>cluster_6</title>\n",
        "<polygon fill=\"none\" stroke=\"black\" points=\"30,-305 30,-375 99.7401,-375 99.7401,-305 30,-305\"/>\n",
1163
1164
1165
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 2 -->\n",
1166
1167
1168
        "<g id=\"node2\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"64.8701\" cy=\"-340\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"60.3701\" y=\"-343.8\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
1169
        "<text text-anchor=\"start\" x=\"56.8701\" y=\"-328.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",
1170
1171
        "</g>\n",
        "<!-- I&#45;&gt;2 -->\n",
1172
1173
1174
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.04557,-340C1.94668,-340 16.0699,-340 30.6965,-340\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.8616,-340 30.8617,-343.15 34.3616,-340 30.8616,-340 30.8616,-340 30.8616,-340 34.3616,-340 30.8616,-336.85 37.8616,-340 37.8616,-340\"/>\n",
1175
1176
        "</g>\n",
        "<!-- 6 -->\n",
1177
1178
1179
        "<g id=\"node3\" class=\"node\"><title>6</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"971.666\" cy=\"-325\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
        "<text text-anchor=\"start\" x=\"967.166\" y=\"-328.8\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
1180
1181
        "<text text-anchor=\"start\" x=\"955.666\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"971.666\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",