decompose.ipynb 422 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.3"
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
45
      "This notebook demonstrates how to use the `decompose_strength()` 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",
      "\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-strength` and `--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=\"289pt\"\n",
        " viewBox=\"0.00 0.00 419.00 289.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 285)\">\n",
86
        "<title>G</title>\n",
87
88
89
90
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-285 415,-285 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-266.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-266.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-266.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
91
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
92
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-148 351,-248 403,-248 403,-148 351,-148\"/>\n",
93
        "</g>\n",
94
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
95
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
96
        "</g>\n",
97
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
98
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-148 268,-233 320,-233 320,-148 268,-148\"/>\n",
99
        "</g>\n",
100
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
101
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-135 30,-237 216,-237 216,-135 30,-135\"/>\n",
102
103
        "</g>\n",
        "<!-- I -->\n",
104
105
106
107
        "<!-- 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",
108
        "</g>\n",
109
110
111
112
        "<!-- 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",
113
        "</g>\n",
114
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",
        "<text text-anchor=\"start\" x=\"48\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
120
        "</g>\n",
121
122
123
124
        "<!-- 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",
125
        "</g>\n",
126
127
128
129
130
        "<!-- 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",
131
        "</g>\n",
132
133
134
135
        "<!-- 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",
136
        "</g>\n",
137
138
139
140
141
        "<!-- 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",
142
        "</g>\n",
143
144
145
146
        "<!-- 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",
147
        "</g>\n",
148
149
150
151
152
        "<!-- 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",
153
        "</g>\n",
154
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",
        "<text text-anchor=\"start\" x=\"369\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
160
        "</g>\n",
161
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",
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
167
168
        "</g>\n",
        "<!-- 4 -->\n",
169
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
170
171
        "<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",
172
        "</g>\n",
173
174
175
176
177
        "<!-- 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",
178
179
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
180
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
181
182
183
        "<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",
184
        "</g>\n",
185
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",
        "<text text-anchor=\"start\" x=\"115\" y=\"-184.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
191
        "</g>\n",
192
193
194
195
196
        "<!-- 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",
197
        "</g>\n",
198
199
200
201
202
        "<!-- 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",
203
        "</g>\n",
204
205
206
207
208
        "<!-- 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",
209
210
        "</g>\n",
        "</g>\n",
211
        "</svg>\n"
212
213
       ],
       "text": [
214
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9690> >"
215
216
217
218
219
220
221
222
223
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
224
      "The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve.  \n",
225
226
      "\n",
      "The letters used for this specification are as follows:\n",
227
      "\n",
228
229
      "- `t`: (inherently) terminal\n",
      "- `w`: (strictly inherently) weak\n",
230
231
      "- `s`: strong\n",
      "\n",
232
      "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."
233
234
235
236
237
238
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
239
      "spot.decompose_strength(aut, 'w')"
240
241
242
243
244
245
246
247
248
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "svg": [
249
250
251
252
253
254
255
256
257
        "<?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=\"232pt\" height=\"242pt\"\n",
        " viewBox=\"0.00 0.00 232.00 242.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 238)\">\n",
258
        "<title>G</title>\n",
259
260
261
262
263
264
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-238 228,-238 228,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"91\" y=\"-219.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"113\" y=\"-219.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"129\" y=\"-219.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
265
        "</g>\n",
266
267
        "<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",
268
269
270
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
271
272
273
        "<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",
274
275
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
276
277
278
        "<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",
279
280
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
281
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
282
283
284
        "<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",
285
286
        "</g>\n",
        "<!-- 1 -->\n",
287
288
289
        "<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",
290
291
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
292
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
293
294
295
        "<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",
296
297
        "</g>\n",
        "<!-- 2 -->\n",
298
299
300
        "<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",
301
302
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
303
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
304
305
306
        "<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",
307
308
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
309
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
310
311
312
313
        "<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",
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
314
315
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
316
317
318
319
        "<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",
320
321
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
322
323
324
325
        "<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",
326
327
        "</g>\n",
        "</g>\n",
328
        "</svg>\n"
329
330
       ],
       "text": [
331
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9360> >"
332
333
334
335
336
337
338
339
340
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
341
      "Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:"
342
343
344
345
346
347
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
348
      "spot.decompose_strength(aut, 't')"
349
350
351
352
353
354
355
356
357
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "svg": [
358
359
360
361
362
363
364
365
366
        "<?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=\"397pt\" height=\"152pt\"\n",
        " viewBox=\"0.00 0.00 397.00 152.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 148.207)\">\n",
367
        "<title>G</title>\n",
368
369
370
371
372
373
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-148.207 393,-148.207 393,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"173.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"195.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"211.5\" y=\"-130.007\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
374
        "</g>\n",
375
376
        "<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",
377
        "</g>\n",
378
379
        "<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",
380
381
382
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
383
384
385
        "<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",
386
387
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
388
389
390
        "<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",
391
392
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
393
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
394
395
396
        "<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",
397
        "</g>\n",
398
399
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
400
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
401
        "<text text-anchor=\"middle\" x=\"355\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
402
        "</g>\n",
403
404
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
405
406
407
        "<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",
408
        "</g>\n",
409
410
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
411
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
412
        "<text text-anchor=\"middle\" x=\"168\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
413
        "</g>\n",
414
415
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
416
417
418
        "<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",
419
        "</g>\n",
420
421
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
422
423
424
425
        "<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",
        "<text text-anchor=\"start\" x=\"347\" y=\"-77.0072\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
426
427
        "</g>\n",
        "<!-- 3 -->\n",
428
429
430
        "<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",
431
        "</g>\n",
432
433
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
434
435
436
        "<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",
437
438
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
439
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
440
441
442
        "<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",
443
        "</g>\n",
444
445
        "<!-- 2&#45;&gt;0 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
446
447
448
        "<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",
449
        "</g>\n",
450
451
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
452
453
454
        "<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",
455
        "</g>\n",
456
457
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
458
459
460
        "<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",
461
        "</g>\n",
462
463
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
464
465
466
        "<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",
467
468
        "</g>\n",
        "</g>\n",
469
        "</svg>\n"
470
471
       ],
       "text": [
472
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9510> >"
473
474
475
476
477
478
479
480
481
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
482
      "Here is the **strong** part:"
483
484
485
486
487
488
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
489
      "strong = spot.decompose_strength(aut, 's'); strong"
490
491
492
493
494
495
496
497
498
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "svg": [
499
500
501
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",
        "<svg width=\"210pt\" height=\"149pt\"\n",
        " viewBox=\"0.00 0.00 210.00 149.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 145)\">\n",
508
        "<title>G</title>\n",
509
510
511
512
513
514
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-145 206,-145 206,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"80\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"102\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"118\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
515
516
517
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
518
519
520
        "<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",
521
522
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
523
524
525
        "<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",
526
527
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
528
529
530
531
532
        "<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",
        "<text text-anchor=\"start\" x=\"48\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
533
534
        "</g>\n",
        "<!-- 1 -->\n",
535
536
537
        "<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",
538
539
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
540
541
542
543
        "<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",
544
545
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
546
547
548
549
550
        "<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",
        "<text text-anchor=\"start\" x=\"104\" y=\"-54.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
551
552
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
553
554
555
556
        "<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",
557
558
        "</g>\n",
        "</g>\n",
559
        "</svg>\n"
560
561
       ],
       "text": [
562
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9660> >"
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
       ]
      }
     ],
     "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",
600
601
602
        "<svg width=\"98pt\" height=\"180pt\"\n",
        " viewBox=\"0.00 0.00 98.00 180.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 176)\">\n",
603
        "<title>G</title>\n",
604
605
606
607
608
609
610
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-176 94,-176 94,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"24\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"46\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"62\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
611
612
613
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
614
615
        "<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",
616
617
618
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
619
620
        "<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",
621
622
623
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
624
625
626
        "<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",
        "<text text-anchor=\"start\" x=\"38\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
627
628
629
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
630
631
632
633
        "<path fill=\"none\" stroke=\"black\" d=\"M50.6841,-51.4203C47.6538,-68.791 49.4258,-88 56,-88 61.7011,-88 63.7908,-73.5545 62.2691,-58.3894\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"61.3159,-51.4203 65.3856,-57.9288 61.7902,-54.888 62.2646,-58.3557 62.2646,-58.3557 62.2646,-58.3557 61.7902,-54.888 59.1437,-58.7826 61.3159,-51.4203 61.3159,-51.4203\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
        "<text text-anchor=\"start\" x=\"48\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
634
635
636
637
638
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
639
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9ed0> >"
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
       ]
      }
     ],
     "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",
      "    a = spot.decompose_strength(aut, opt)\n",
      "    a.set_name(\"option: \" + opt)\n",
661
      "    display(a)"
662
663
664
665
666
667
668
669
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
670
671
672
673
674
675
676
677
678
        "<?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=\"232pt\" height=\"270pt\"\n",
        " viewBox=\"0.00 0.00 232.00 270.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 266)\">\n",
679
        "<title>G</title>\n",
680
681
682
683
684
685
686
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-266 228,-266 228,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"78.5\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">option: sw</text>\n",
        "<text text-anchor=\"start\" x=\"91\" y=\"-233.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"113\" y=\"-233.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"129\" y=\"-233.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
687
        "</g>\n",
688
689
        "<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",
690
691
692
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
693
694
695
        "<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",
696
697
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
698
699
700
        "<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",
701
702
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
703
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
704
705
706
707
        "<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",
        "<text text-anchor=\"start\" x=\"48\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
708
709
        "</g>\n",
        "<!-- 1 -->\n",
710
711
712
        "<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",
713
714
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
715
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
716
717
718
        "<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",
719
720
        "</g>\n",
        "<!-- 2 -->\n",
721
722
723
        "<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",
724
725
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
726
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
727
728
729
        "<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",
730
731
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
732
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
733
734
735
736
        "<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",
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
737
738
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
739
740
741
742
743
        "<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",
        "<text text-anchor=\"start\" x=\"115\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
744
745
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
746
747
748
749
        "<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",
750
751
        "</g>\n",
        "</g>\n",
752
        "</svg>\n"
753
754
       ],
       "text": [
755
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a30923420> >"
756
757
758
759
760
761
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
762
763
764
765
766
767
768
769
770
        "<?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=\"397pt\" height=\"175pt\"\n",
        " viewBox=\"0.00 0.00 397.00 175.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 171)\">\n",
771
        "<title>G</title>\n",
772
773
774
775
776
777
778
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-171 393,-171 393,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"164\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">option: st</text>\n",
        "<text text-anchor=\"start\" x=\"173.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"195.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"211.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<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",
779
        "</g>\n",
780
781
        "<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",
782
        "</g>\n",
783
784
        "<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",
785
786
787
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
788
789
790
        "<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",
791
792
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
793
794
795
        "<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",
796
797
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
798
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
799
800
801
802
        "<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",
        "<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
803
        "</g>\n",
804
805
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
806
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-47\" rx=\"18\" ry=\"18\"/>\n",
807
        "<text text-anchor=\"middle\" x=\"355\" y=\"-43.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
808
        "</g>\n",
809
810
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
811
812
813
        "<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",
814
        "</g>\n",
815
816
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
817
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-50\" rx=\"18\" ry=\"18\"/>\n",
818
        "<text text-anchor=\"middle\" x=\"168\" y=\"-46.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
819
        "</g>\n",
820
821
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
822
823
824
        "<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",
825
        "</g>\n",
826
827
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
828
829
830
831
        "<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",
        "<text text-anchor=\"start\" x=\"347\" y=\"-86.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
832
833
        "</g>\n",
        "<!-- 3 -->\n",
834
835
836
        "<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",
837
        "</g>\n",
838
839
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
840
841
842
        "<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",
843
844
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
845
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
846
847
848
        "<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",
849
        "</g>\n",
850
851
        "<!-- 2&#45;&gt;0 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
852
853
854
855
        "<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",
        "<text text-anchor=\"start\" x=\"104\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
856
        "</g>\n",
857
858
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
859
860
861
        "<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",
862
        "</g>\n",
863
864
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
865
866
867
        "<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",
868
        "</g>\n",
869
870
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
871
872
873
        "<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",
874
875
        "</g>\n",
        "</g>\n",
876
        "</svg>\n"
877
878
       ],
       "text": [
879
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9e40> >"
880
881
882
883
884
885
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
886
887
888
889
890
891
        "<?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",
892
893
894
        "<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",
895
        "<title>G</title>\n",
896
897
898
899
900
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-298 415,-298 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-279.8\" font-family=\"Lato\" font-size=\"14.00\">option: wt</text>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
901
        "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
902
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-148 351,-248 403,-248 403,-148 351,-148\"/>\n",
903
        "</g>\n",
904
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
905
        "<polygon fill=\"none\" stroke=\"green\" points=\"164,-8 164,-108 216,-108 216,-8 164,-8\"/>\n",
906
        "</g>\n",
907
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
908
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-148 268,-233 320,-233 320,-148 268,-148\"/>\n",
909
        "</g>\n",
910
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
911
        "<polygon fill=\"none\" stroke=\"red\" points=\"30,-146 30,-233 216,-233 216,-146 30,-146\"/>\n",
912
913
914
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
915
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
916
917
        "<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",
918
919
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
920
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
921
922
        "<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",
923
924
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
925
926
927
928
        "<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",
929
930
        "</g>\n",
        "<!-- 1 -->\n",
931
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
932
933
        "<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",
934
935
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
936
937
938
939
        "<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",
940
941
        "</g>\n",
        "<!-- 2 -->\n",
942
943
944
        "<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",
945
946
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
947
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
948
949
950
951
952
953
954
955
956
957
958
959
960
961
        "<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",
962
963
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
964
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
965
966
967
968
        "<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",
        "<text text-anchor=\"start\" x=\"369\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
969
        "</g>\n",
970
971
972
973
974
975
        "<!-- 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",
        "<text text-anchor=\"start\" x=\"182\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
976
977
        "</g>\n",
        "<!-- 4 -->\n",
978
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
979
980
        "<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",
981
        "</g>\n",
982
983
984
985
986
        "<!-- 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",
987
988
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
989
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
990
991
992
        "<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",
993
        "</g>\n",
994
995
996
997
998
        "<!-- 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",
999
        "</g>\n",
1000
1001
1002
1003
1004
        "<!-- 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",
1005
        "</g>\n",
1006
1007
1008
1009
1010
        "<!-- 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",
1011
        "</g>\n",
1012
1013
1014
1015
1016
        "<!-- 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",
1017
1018
        "</g>\n",
        "</g>\n",
1019
        "</svg>\n"
1020
1021
       ],
       "text": [
1022
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3a2c7d9540> >"
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Generalized acceptance\n",
      "\n",
1034
      "There is nothing that prevents the above decomposition to work with other types of acceptance.\n",
1035
1036
1037
1038
1039
1040
1041
1042
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
      "\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",
1104
      "aut"
1105
1106
1107
1108
1109
1110
1111
1112
1113
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 8,
       "svg": [
1114
1115
1116
1117
1118
1119
1120
1121
1122
        "<?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=\"594pt\" height=\"360pt\"\n",
        " viewBox=\"0.00 0.00 594.00 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.576923 0.576923) rotate(0) translate(4 620)\">\n",
1123
        "<title>G</title>\n",
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-620 1025.61,-620 1025.61,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"394.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\">(Fin(</text>\n",
        "<text text-anchor=\"start\" x=\"422.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"438.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"481.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"497.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\">)) | (Fin(</text>\n",
        "<text text-anchor=\"start\" x=\"544.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
        "<text text-anchor=\"start\" x=\"560.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"603.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
        "<text text-anchor=\"start\" x=\"619.304\" y=\"-601.8\" font-family=\"Lato\" font-size=\"14.00\">))</text>\n",
        "<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",
1136
        "</g>\n",
1137
1138
        "<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",
1139
        "</g>\n",
1140
1141
        "<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",
1142
        "</g>\n",
1143
1144
        "<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",
1145
        "</g>\n",
1146
1147
        "<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",
1148
        "</g>\n",
1149
1150
        "<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",
1151
        "</g>\n",
1152
1153
        "<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",
1154
1155
1156
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 2 -->\n",
1157
1158
1159
1160
        "<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",
        "<text text-anchor=\"start\" x=\"56.8701\" y=\"-328.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1161
1162
        "</g>\n",
        "<!-- I&#45;&gt;2 -->\n",
1163
1164
1165
        "<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",
1166
1167
        "</g>\n",
        "<!-- 6 -->\n",
1168
1169
1170
1171
1172
        "<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",
        "<text text-anchor=\"start\" x=\"955.666\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"971.666\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1173
1174
        "</g>\n",
        "<!-- 2&#45;&gt;6 -->\n",
1175
        "<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;6</title>\n",
1176
1177
1178
        "<path fill=\"none\" stroke=\"black\" d=\"M70.6773,-366.38C83.6475,-428.346 125.451,-578 226.681,-578 226.681,-578 226.681,-578 864.855,-578 955.533,-578 969.853,-437.963 971.242,-366.258\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"971.341,-359.121 974.393,-366.164 971.292,-362.62 971.243,-366.12 971.243,-366.12 971.243,-366.12 971.292,-362.62 968.094,-366.076 971.341,-359.121 971.341,-359.121\"/>\n",
        "<text text-anchor=\"start\" x=\"549.804\" y=\"-581.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
1179
1180
        "</g>\n",
        "<!-- 5 -->\n",
1181
1182
1183
1184
1185
        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"553.304\" cy=\"-310\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
        "<text text-anchor=\"start\" x=\"548.804\" y=\"-313.8\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "<text text-anchor=\"start\" x=\"537.304\" y=\"-299.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"553.304\" y=\"-299.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1186
1187
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
1188
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
1189
1190
1191
        "<path fill=\"none\" stroke=\"black\" d=\"M89.1564,-328.414C127.645,-309.98 207.462,-274.755 279.622,-262 363.655,-247.147 462.273,-275.978 514.835,-295.048\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"521.631,-297.553 513.973,-298.088 518.347,-296.342 515.063,-295.132 515.063,-295.132 515.063,-295.132 518.347,-296.342 516.152,-292.176 521.631,-297.553 521.631,-297.553\"/>\n",
        "<text text-anchor=\"start\" x=\"292.622\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1192
1193
        "</g>\n",
        "<!-- 3 -->\n",
1194
1195
1196
1197
1198
        "<g id=\"node9\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"227.681\" cy=\"-418\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
        "<text text-anchor=\"start\" x=\"223.181\" y=\"-421.8\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "<text text-anchor=\"start\" x=\"211.681\" y=\"-407.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"227.681\" y=\"-407.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1199
1200
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
1201
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
1202
1203
1204
        "<path fill=\"none\" stroke=\"black\" d=\"M89.2534,-351.342C115.766,-364.201 159.319,-385.327 190.285,-400.347\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"196.692,-403.454 189.019,-403.233 193.543,-401.926 190.393,-400.399 190.393,-400.399 190.393,-400.399 193.543,-401.926 191.768,-397.565 196.692,-403.454 196.692,-403.454\"/>\n",
        "<text text-anchor=\"start\" x=\"109.74\" y=\"-396.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; !c</text>\n",
1205
1206
        "</g>\n",
        "<!-- 4 -->\n",
1207
1208
1209
1210
1211
        "<g id=\"node10\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"227.681\" cy=\"-173\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
        "<text text-anchor=\"start\" x=\"223.181\" y=\"-176.8\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "<text text-anchor=\"start\" x=\"211.681\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"227.681\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1212
1213
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
1214
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
1215
1216
1217
        "<path fill=\"none\" stroke=\"black\" d=\"M71.2529,-313.422C77.1981,-289.867 88.8254,-255.772 109.74,-233 130.994,-209.859 163.216,-194.254 188.458,-184.772\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"195.045,-182.376 189.544,-187.729 191.756,-183.572 188.467,-184.769 188.467,-184.769 188.467,-184.769 191.756,-183.572 187.39,-181.809 195.045,-182.376 195.045,-182.376\"/>\n",
        "<text text-anchor=\"start\" x=\"111.74\" y=\"-236.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
1218
1219
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
1220
        "<g id=\"edge26\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
1221
1222
        "<path fill=\"none\" stroke=\"black\" d=\"M961.166,-357.463C961.166,-368.284 964.666,-376.941 971.666,-376.941 977.025,-376.941 980.333,-371.867 981.589,-364.632\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"982.166,-357.463 984.744,-364.693 981.885,-360.952 981.605,-364.441 981.605,-364.441 981.605,-364.441 981.885,-360.952 978.465,-364.188 982.166,-357.463 982.166,-357.463\"/>\n",
1223
        "<text text-anchor=\"middle\" x=\"971.666\" y=\"-380.741\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1224
1225
        "</g>\n",
        "<!-- 1 -->\n",
1226
1227
1228
1229
        "<g id=\"node4\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"863.855\" cy=\"-256\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"859.355\" y=\"-259.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"855.855\" y=\"-244.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",