decompose.ipynb 408 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
{
 "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",
   "version": "3.4.3+"
  },
20
  "name": "",
21
  "signature": "sha256:ddf44352825d3260c20b0a4d29b4972c9cd5be57b3a48bcdf8afe8acaee5eba6"
22
23
24
25
26
27
28
29
30
31
32
33
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "from IPython.display import display\n",
      "import spot\n",
34
      "spot.setup(show_default='.bans')"
35
36
37
38
39
40
41
42
43
44
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
45
46
47
      "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",
      "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` option.\n",
48
49
50
      "\n",
      "# Basics\n",
      "\n",
51
      "Let's define the following strengths of accepting SCCs:\n",
52
      "\n",
53
54
55
56
      "- 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",
57
      "\n",
58
59
60
      "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."
61
62
63
64
65
66
67
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.translate('(Ga -> Gb) W c')\n",
68
      "aut"
69
70
71
72
73
74
75
76
77
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "svg": [
78
79
80
81
82
83
84
85
86
        "<?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=\"419pt\" height=\"260pt\"\n",
        " viewBox=\"0.00 0.00 419.00 260.24\" 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 256.243)\">\n",
87
        "<title>G</title>\n",
88
89
90
91
92
93
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-256.243 415,-256.243 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-238.043\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-238.043\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-238.043\" 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,-11.2426 164,-111.243 216,-111.243 216,-11.2426 164,-11.2426\"/>\n",
94
        "</g>\n",
95
96
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-32.2426 351,-132.243 403,-132.243 403,-32.2426 351,-32.2426\"/>\n",
97
        "</g>\n",
98
99
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-32.2426 268,-117.243 320,-117.243 320,-32.2426 268,-32.2426\"/>\n",
100
        "</g>\n",
101
102
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-119.243 30,-221.243 216,-221.243 216,-119.243 30,-119.243\"/>\n",
103
104
105
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 1 -->\n",
106
107
108
        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-145.243\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-141.543\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
109
110
        "</g>\n",
        "<!-- I&#45;&gt;1 -->\n",
111
112
113
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-145.243C2.79388,-145.243 17.1543,-145.243 30.6317,-145.243\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-145.243 30.9419,-148.393 34.4419,-145.243 30.9419,-145.243 30.9419,-145.243 30.9419,-145.243 34.4419,-145.243 30.9418,-142.093 37.9419,-145.243 37.9419,-145.243\"/>\n",
114
115
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
116
117
118
119
120
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-162.28C48.3189,-172.101 50.4453,-181.243 56,-181.243 60.166,-181.243 62.4036,-176.1 62.7128,-169.386\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-162.28 65.8541,-169.124 62.5434,-165.776 62.7076,-169.272 62.7076,-169.272 62.7076,-169.272 62.5434,-165.776 59.561,-169.42 62.3792,-162.28 62.3792,-162.28\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-200.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
        "<text text-anchor=\"start\" x=\"48\" y=\"-185.043\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
121
122
        "</g>\n",
        "<!-- 0 -->\n",
123
124
125
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-37.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-33.5426\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
126
127
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
128
129
130
131
        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M70.6291,-134.092C94.2674,-114.751 142.92,-74.9443 169.91,-52.8619\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.642,-48.1723 172.219,-55.0429 172.933,-50.3886 170.224,-52.605 170.224,-52.605 170.224,-52.605 172.933,-50.3886 168.229,-50.167 175.642,-48.1723 175.642,-48.1723\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-121.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
132
133
        "</g>\n",
        "<!-- 3 -->\n",
134
135
136
        "<g id=\"node4\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"377\" cy=\"-58.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"377\" y=\"-54.5426\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
137
138
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
139
140
141
142
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M61.4186,-127.992C66.5954,-110.192 76.4918,-82.2758 92,-62.2426 116.65,-30.4005 125.855,-20.1451 164,-7.24264 232.475,15.9189 316.751,-23.848 355.157,-45.552\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.35,-49.1217 353.712,-48.355 358.318,-47.3738 355.285,-45.6259 355.285,-45.6259 355.285,-45.6259 358.318,-47.3738 356.859,-42.8969 361.35,-49.1217 361.35,-49.1217\"/>\n",
        "<text text-anchor=\"start\" x=\"238.5\" y=\"-10.0426\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
143
144
        "</g>\n",
        "<!-- 2 -->\n",
145
146
147
        "<g id=\"node6\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-145.243\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-141.543\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
148
149
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
150
151
152
153
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.2567,-145.243C97.2816,-145.243 138.189,-145.243 164.429,-145.243\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.739,-145.243 164.739,-148.393 168.239,-145.243 164.739,-145.243 164.739,-145.243 164.739,-145.243 168.239,-145.243 164.739,-142.093 171.739,-145.243 171.739,-145.243\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-149.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
154
155
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
156
157
158
159
160
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-53.1587C178.679,-63.393 181.672,-73.2426 190,-73.2426 196.376,-73.2426 199.625,-67.469 199.746,-60.1694\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-53.1587 202.872,-59.7742 199.36,-56.6379 199.741,-60.1171 199.741,-60.1171 199.741,-60.1171 199.36,-56.6379 196.61,-60.46 198.979,-53.1587 198.979,-53.1587\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-92.0426\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"182\" y=\"-77.0426\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
161
162
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
163
164
165
166
167
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M369.969,-74.9067C368.406,-84.8676 370.75,-94.2426 377,-94.2426 381.688,-94.2426 384.178,-88.9692 384.471,-82.1302\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"384.031,-74.9067 387.601,-81.7025 384.244,-78.4002 384.456,-81.8938 384.456,-81.8938 384.456,-81.8938 384.244,-78.4002 381.312,-82.0851 384.031,-74.9067 384.031,-74.9067\"/>\n",
        "<text text-anchor=\"start\" x=\"372.5\" y=\"-113.043\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"369\" y=\"-98.0426\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
168
169
        "</g>\n",
        "<!-- 4 -->\n",
170
171
172
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"294\" cy=\"-58.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"294\" y=\"-54.5426\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
173
174
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
175
176
177
178
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M312.178,-58.2426C323.669,-58.2426 338.959,-58.2426 351.693,-58.2426\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"358.847,-58.2426 351.847,-61.3927 355.347,-58.2427 351.847,-58.2427 351.847,-58.2427 351.847,-58.2427 355.347,-58.2427 351.847,-55.0927 358.847,-58.2426 358.847,-58.2426\"/>\n",
        "<text text-anchor=\"start\" x=\"330\" y=\"-62.0426\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
179
180
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
181
182
183
184
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M286.969,-74.9067C285.406,-84.8676 287.75,-94.2426 294,-94.2426 298.688,-94.2426 301.178,-88.9692 301.471,-82.1302\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"301.031,-74.9067 304.601,-81.7025 301.244,-78.4002 301.456,-81.8938 301.456,-81.8938 301.456,-81.8938 301.244,-78.4002 298.312,-82.0851 301.031,-74.9067 301.031,-74.9067\"/>\n",
        "<text text-anchor=\"start\" x=\"290.5\" y=\"-98.0426\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
185
186
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
187
188
189
190
191
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M173.816,-153.903C167.839,-156.847 160.789,-159.764 154,-161.243 127.075,-167.105 118.925,-167.105 92,-161.243 87.5445,-160.273 82.977,-158.682 78.6739,-156.872\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-153.903 79.8596,-153.95 75.3664,-155.359 78.5492,-156.815 78.5492,-156.815 78.5492,-156.815 75.3664,-155.359 77.2387,-159.679 72.1836,-153.903 72.1836,-153.903\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-184.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
        "<text text-anchor=\"start\" x=\"115\" y=\"-169.043\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
192
193
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
194
195
196
197
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M208.055,-145.496C233.928,-145.159 283.898,-141.629 320,-121.243 337.84,-111.169 352.915,-93.2717 362.915,-79.1208\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"366.883,-73.3192 365.531,-80.8754 364.907,-76.2082 362.931,-79.0971 362.931,-79.0971 362.931,-79.0971 364.907,-76.2082 360.331,-77.3188 366.883,-73.3192 366.883,-73.3192\"/>\n",
        "<text text-anchor=\"start\" x=\"276\" y=\"-143.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
198
199
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
200
201
202
203
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M204.335,-133.869C222.203,-118.628 254.008,-91.5003 274.273,-74.2153\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"279.662,-69.6192 276.38,-76.5585 276.999,-71.8905 274.336,-74.1618 274.336,-74.1618 274.336,-74.1618 276.999,-71.8905 272.292,-71.7652 279.662,-69.6192 279.662,-69.6192\"/>\n",
        "<text text-anchor=\"start\" x=\"226\" y=\"-119.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
204
205
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
206
207
208
209
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-161.159C178.679,-171.393 181.672,-181.243 190,-181.243 196.376,-181.243 199.625,-175.469 199.746,-168.169\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-161.159 202.872,-167.774 199.36,-164.638 199.741,-168.117 199.741,-168.117 199.741,-168.117 199.36,-164.638 196.61,-168.46 198.979,-161.159 198.979,-161.159\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-185.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
210
211
        "</g>\n",
        "</g>\n",
212
        "</svg>\n"
213
214
       ],
       "text": [
215
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048a20> >"
216
217
218
219
220
221
222
223
224
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
225
      "The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve.  \n",
226
227
      "\n",
      "The letters used for this specification are as follows:\n",
228
      "\n",
229
230
      "- `t`: (inherently) terminal\n",
      "- `w`: (strictly inherently) weak\n",
231
232
      "- `s`: strong\n",
      "\n",
233
      "For instance if we want to preserve only the **strictly inherently weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it.  However the SCC above is not stricly weak, so it should not accept any word in the new automaton."
234
235
236
237
238
239
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
240
      "spot.decompose_strength(aut, 'w')"
241
242
243
244
245
246
247
248
249
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "svg": [
250
251
252
253
254
255
256
257
258
        "<?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",
259
        "<title>G</title>\n",
260
261
262
263
264
265
        "<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",
266
        "</g>\n",
267
268
        "<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",
269
270
271
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
272
273
274
        "<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",
275
276
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
277
278
279
        "<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",
280
281
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
282
283
284
285
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<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",
286
287
        "</g>\n",
        "<!-- 1 -->\n",
288
289
290
        "<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",
291
292
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
293
294
295
296
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<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",
297
298
        "</g>\n",
        "<!-- 2 -->\n",
299
300
301
        "<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",
302
303
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
304
305
306
307
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<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",
308
309
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
310
311
312
313
314
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<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",
315
316
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
317
318
319
320
        "<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",
321
322
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
323
324
325
326
        "<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",
327
328
        "</g>\n",
        "</g>\n",
329
        "</svg>\n"
330
331
       ],
       "text": [
332
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048990> >"
333
334
335
336
337
338
339
340
341
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
342
      "Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:"
343
344
345
346
347
348
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
349
      "spot.decompose_strength(aut, 't')"
350
351
352
353
354
355
356
357
358
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "svg": [
359
360
361
362
363
364
365
366
367
        "<?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",
368
        "<title>G</title>\n",
369
370
371
372
373
374
        "<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",
375
        "</g>\n",
376
377
        "<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",
378
        "</g>\n",
379
380
        "<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",
381
382
383
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
384
385
386
        "<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",
387
388
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
389
390
391
        "<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",
392
393
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
394
395
396
397
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<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",
398
399
        "</g>\n",
        "<!-- 2 -->\n",
400
401
402
        "<g id=\"node3\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"355\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
403
404
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
405
406
407
408
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<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",
409
410
        "</g>\n",
        "<!-- 1 -->\n",
411
412
413
        "<g id=\"node5\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-37.2072\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"168\" y=\"-33.5072\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
414
415
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
416
417
418
419
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<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",
420
421
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
422
423
424
425
426
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<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",
427
428
        "</g>\n",
        "<!-- 3 -->\n",
429
430
431
        "<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",
432
433
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
434
435
436
437
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<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",
438
439
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
440
441
442
443
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<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",
444
445
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
446
447
448
449
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<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",
450
451
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
452
453
454
455
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<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",
456
457
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
458
459
460
461
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
        "<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",
462
463
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
464
465
466
467
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<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",
468
469
        "</g>\n",
        "</g>\n",
470
        "</svg>\n"
471
472
       ],
       "text": [
473
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f73400489c0> >"
474
475
476
477
478
479
480
481
482
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
483
      "Here is the **strong** part:"
484
485
486
487
488
489
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
490
      "strong = spot.decompose_strength(aut, 's'); strong"
491
492
493
494
495
496
497
498
499
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "svg": [
500
501
502
503
504
505
506
507
508
        "<?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",
509
        "<title>G</title>\n",
510
511
512
513
514
515
        "<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",
516
517
518
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
519
520
521
        "<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",
522
523
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
524
525
526
        "<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",
527
528
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
529
530
531
532
533
        "<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",
534
535
        "</g>\n",
        "<!-- 1 -->\n",
536
537
538
        "<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",
539
540
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
541
542
543
544
        "<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",
545
546
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
547
548
549
550
551
        "<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",
552
553
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
554
555
556
557
        "<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",
558
559
        "</g>\n",
        "</g>\n",
560
        "</svg>\n"
561
562
       ],
       "text": [
563
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048bd0> >"
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
       ]
      }
     ],
     "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",
601
602
603
        "<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",
604
        "<title>G</title>\n",
605
606
607
608
609
610
611
        "<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",
612
613
614
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
615
616
        "<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",
617
618
619
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
620
621
        "<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",
622
623
624
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
625
626
627
        "<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",
628
629
630
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
631
632
633
634
        "<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",
635
636
637
638
639
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
640
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f3c0> >"
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
       ]
      }
     ],
     "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",
662
      "    display(a)"
663
664
665
666
667
668
669
670
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
671
672
673
674
675
676
677
678
679
        "<?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",
680
        "<title>G</title>\n",
681
682
683
684
685
686
687
        "<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",
688
        "</g>\n",
689
690
        "<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",
691
692
693
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
694
695
696
        "<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",
697
698
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
699
700
701
        "<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",
702
703
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
704
705
706
707
708
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<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",
709
710
        "</g>\n",
        "<!-- 1 -->\n",
711
712
713
        "<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",
714
715
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
716
717
718
719
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<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",
720
721
        "</g>\n",
        "<!-- 2 -->\n",
722
723
724
        "<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",
725
726
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
727
728
729
730
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<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",
731
732
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
733
734
735
736
737
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<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",
738
739
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
740
741
742
743
744
        "<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",
745
746
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
747
748
749
750
        "<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",
751
752
        "</g>\n",
        "</g>\n",
753
        "</svg>\n"
754
755
       ],
       "text": [
756
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f060> >"
757
758
759
760
761
762
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
763
764
765
766
767
768
769
770
771
        "<?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",
772
        "<title>G</title>\n",
773
774
775
776
777
778
779
        "<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",
780
        "</g>\n",
781
782
        "<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",
783
        "</g>\n",
784
785
        "<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",
786
787
788
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
789
790
791
        "<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",
792
793
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
794
795
796
        "<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",
797
798
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
799
800
801
802
803
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<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",
804
805
        "</g>\n",
        "<!-- 2 -->\n",
806
807
808
        "<g id=\"node3\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"355\" cy=\"-47\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"355\" y=\"-43.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
809
810
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
811
812
813
814
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<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",
815
816
        "</g>\n",
        "<!-- 1 -->\n",
817
818
819
        "<g id=\"node5\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-50\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"168\" y=\"-46.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
820
821
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
822
823
824
825
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<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",
826
827
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
828
829
830
831
832
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<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",
833
834
        "</g>\n",
        "<!-- 3 -->\n",
835
836
837
        "<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",
838
839
        "</g>\n",
        "<!-- 3&#45;&gt;2 -->\n",
840
841
842
843
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
        "<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",
844
845
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
846
847
848
849
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<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",
850
851
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
852
853
854
855
856
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<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",
857
858
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
859
860
861
862
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<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",
863
864
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
865
866
867
868
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
        "<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",
869
870
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
871
872
873
874
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<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",
875
876
        "</g>\n",
        "</g>\n",
877
        "</svg>\n"
878
879
       ],
       "text": [
880
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f3f0> >"
881
882
883
884
885
886
       ]
      },
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
887
888
889
890
891
892
893
894
895
        "<?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=\"419pt\" height=\"258pt\"\n",
        " viewBox=\"0.00 0.00 419.00 258.24\" 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 254.243)\">\n",
896
        "<title>G</title>\n",
897
898
899
900
901
902
903
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-254.243 415,-254.243 415,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-236.043\" font-family=\"Lato\" font-size=\"14.00\">option: wt</text>\n",
        "<text text-anchor=\"start\" x=\"184.5\" y=\"-222.043\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"206.5\" y=\"-222.043\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"222.5\" y=\"-222.043\" 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,-11.2426 164,-111.243 216,-111.243 216,-11.2426 164,-11.2426\"/>\n",
904
        "</g>\n",
905
906
        "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" stroke=\"green\" points=\"351,-32.2426 351,-132.243 403,-132.243 403,-32.2426 351,-32.2426\"/>\n",
907
        "</g>\n",
908
909
        "<g id=\"clust3\" class=\"cluster\"><title>cluster_2</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"268,-32.2426 268,-117.243 320,-117.243 320,-32.2426 268,-32.2426\"/>\n",
910
        "</g>\n",
911
912
        "<g id=\"clust4\" class=\"cluster\"><title>cluster_3</title>\n",
        "<polygon fill=\"none\" stroke=\"red\" points=\"30,-119.243 30,-206.243 216,-206.243 216,-119.243 30,-119.243\"/>\n",
913
914
915
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
916
917
918
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-145.243\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-141.543\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
919
920
        "</g>\n",
        "<!-- I&#45;&gt;0 -->\n",
921
922
923
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-145.243C2.79388,-145.243 17.1543,-145.243 30.6317,-145.243\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-145.243 30.9419,-148.393 34.4419,-145.243 30.9419,-145.243 30.9419,-145.243 30.9419,-145.243 34.4419,-145.243 30.9418,-142.093 37.9419,-145.243 37.9419,-145.243\"/>\n",
924
925
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
926
927
928
929
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-162.28C48.3189,-172.101 50.4453,-181.243 56,-181.243 60.166,-181.243 62.4036,-176.1 62.7128,-169.386\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-162.28 65.8541,-169.124 62.5434,-165.776 62.7076,-169.272 62.7076,-169.272 62.7076,-169.272 62.5434,-165.776 59.561,-169.42 62.3792,-162.28 62.3792,-162.28\"/>\n",
        "<text text-anchor=\"start\" x=\"36\" y=\"-185.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
930
931
        "</g>\n",
        "<!-- 1 -->\n",
932
933
934
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-37.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-33.5426\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
935
936
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
937
938
939
940
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M70.6291,-134.092C94.2674,-114.751 142.92,-74.9443 169.91,-52.8619\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"175.642,-48.1723 172.219,-55.0429 172.933,-50.3886 170.224,-52.605 170.224,-52.605 170.224,-52.605 172.933,-50.3886 168.229,-50.167 175.642,-48.1723 175.642,-48.1723\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-121.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
941
942
        "</g>\n",
        "<!-- 3 -->\n",
943
944
945
        "<g id=\"node4\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"377\" cy=\"-58.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"377\" y=\"-54.5426\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
946
947
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
948
949
950
951
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M61.4186,-127.992C66.5954,-110.192 76.4918,-82.2758 92,-62.2426 116.65,-30.4005 125.855,-20.1451 164,-7.24264 232.475,15.9189 316.751,-23.848 355.157,-45.552\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.35,-49.1217 353.712,-48.355 358.318,-47.3738 355.285,-45.6259 355.285,-45.6259 355.285,-45.6259 358.318,-47.3738 356.859,-42.8969 361.35,-49.1217 361.35,-49.1217\"/>\n",
        "<text text-anchor=\"start\" x=\"238.5\" y=\"-10.0426\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
952
953
        "</g>\n",
        "<!-- 2 -->\n",
954
955
956
        "<g id=\"node6\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"190\" cy=\"-145.243\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"190\" y=\"-141.543\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
957
958
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
959
960
961
962
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.2567,-145.243C97.2816,-145.243 138.189,-145.243 164.429,-145.243\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.739,-145.243 164.739,-148.393 168.239,-145.243 164.739,-145.243 164.739,-145.243 164.739,-145.243 168.239,-145.243 164.739,-142.093 171.739,-145.243 171.739,-145.243\"/>\n",
        "<text text-anchor=\"start\" x=\"105\" y=\"-149.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
963
964
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
965
966
967
968
969
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-53.1587C178.679,-63.393 181.672,-73.2426 190,-73.2426 196.376,-73.2426 199.625,-67.469 199.746,-60.1694\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-53.1587 202.872,-59.7742 199.36,-56.6379 199.741,-60.1171 199.741,-60.1171 199.741,-60.1171 199.36,-56.6379 196.61,-60.46 198.979,-53.1587 198.979,-53.1587\"/>\n",
        "<text text-anchor=\"start\" x=\"185.5\" y=\"-92.0426\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "<text text-anchor=\"start\" x=\"182\" y=\"-77.0426\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
970
971
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
972
973
974
975
976
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M369.969,-74.9067C368.406,-84.8676 370.75,-94.2426 377,-94.2426 381.688,-94.2426 384.178,-88.9692 384.471,-82.1302\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"384.031,-74.9067 387.601,-81.7025 384.244,-78.4002 384.456,-81.8938 384.456,-81.8938 384.456,-81.8938 384.244,-78.4002 381.312,-82.0851 384.031,-74.9067 384.031,-74.9067\"/>\n",
        "<text text-anchor=\"start\" x=\"372.5\" y=\"-113.043\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"369\" y=\"-98.0426\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
977
978
        "</g>\n",
        "<!-- 4 -->\n",
979
980
981
        "<g id=\"node5\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"294\" cy=\"-58.2426\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"294\" y=\"-54.5426\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
982
983
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
984
985
986
987
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M312.178,-58.2426C323.669,-58.2426 338.959,-58.2426 351.693,-58.2426\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"358.847,-58.2426 351.847,-61.3927 355.347,-58.2427 351.847,-58.2427 351.847,-58.2427 351.847,-58.2427 355.347,-58.2427 351.847,-55.0927 358.847,-58.2426 358.847,-58.2426\"/>\n",
        "<text text-anchor=\"start\" x=\"330\" y=\"-62.0426\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
988
989
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
990
991
992
993
        "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M286.969,-74.9067C285.406,-84.8676 287.75,-94.2426 294,-94.2426 298.688,-94.2426 301.178,-88.9692 301.471,-82.1302\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"301.031,-74.9067 304.601,-81.7025 301.244,-78.4002 301.456,-81.8938 301.456,-81.8938 301.456,-81.8938 301.244,-78.4002 298.312,-82.0851 301.031,-74.9067 301.031,-74.9067\"/>\n",
        "<text text-anchor=\"start\" x=\"290.5\" y=\"-98.0426\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
994
995
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
996
997
998
999
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M173.816,-153.903C167.839,-156.847 160.789,-159.764 154,-161.243 127.075,-167.105 118.925,-167.105 92,-161.243 87.5445,-160.273 82.977,-158.682 78.6739,-156.872\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.1836,-153.903 79.8596,-153.95 75.3664,-155.359 78.5492,-156.815 78.5492,-156.815 78.5492,-156.815 75.3664,-155.359 77.2387,-159.679 72.1836,-153.903 72.1836,-153.903\"/>\n",
        "<text text-anchor=\"start\" x=\"103\" y=\"-169.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1000
1001
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
1002
1003
1004
1005
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M208.055,-145.496C233.928,-145.159 283.898,-141.629 320,-121.243 337.84,-111.169 352.915,-93.2717 362.915,-79.1208\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"366.883,-73.3192 365.531,-80.8754 364.907,-76.2082 362.931,-79.0971 362.931,-79.0971 362.931,-79.0971 364.907,-76.2082 360.331,-77.3188 366.883,-73.3192 366.883,-73.3192\"/>\n",
        "<text text-anchor=\"start\" x=\"276\" y=\"-143.043\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1006
1007
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
1008
1009
1010
1011
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M204.335,-133.869C222.203,-118.628 254.008,-91.5003 274.273,-74.2153\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"279.662,-69.6192 276.38,-76.5585 276.999,-71.8905 274.336,-74.1618 274.336,-74.1618 274.336,-74.1618 276.999,-71.8905 272.292,-71.7652 279.662,-69.6192 279.662,-69.6192\"/>\n",
        "<text text-anchor=\"start\" x=\"226\" y=\"-119.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
1012
1013
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
1014
1015
1016
1017
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M181.021,-161.159C178.679,-171.393 181.672,-181.243 190,-181.243 196.376,-181.243 199.625,-175.469 199.746,-168.169\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"198.979,-161.159 202.872,-167.774 199.36,-164.638 199.741,-168.117 199.741,-168.117 199.741,-168.117 199.36,-164.638 196.61,-168.46 198.979,-161.159 198.979,-161.159\"/>\n",
        "<text text-anchor=\"start\" x=\"172\" y=\"-185.043\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
1018
1019
        "</g>\n",
        "</g>\n",
1020
        "</svg>\n"
1021
1022
       ],
       "text": [
1023
        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f060> >"
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Generalized acceptance\n",
      "\n",
1035
      "There is nothing that prevents the above decomposition to work with other types of acceptance.\n",
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
1104
      "\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",
1105
      "aut"
1106
1107
1108
1109
1110
1111
1112
1113
1114
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 8,
       "svg": [
1115
1116
1117
1118
1119
1120
1121
1122
1123
        "<?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",
1124
        "<title>G</title>\n",
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
        "<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",
1137
        "</g>\n",
1138
1139
        "<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",
1140
        "</g>\n",
1141
1142
        "<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",
1143
        "</g>\n",
1144
1145
        "<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",
1146
        "</g>\n",
1147
1148
        "<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",
1149
        "</g>\n",
1150
1151
        "<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",
1152
        "</g>\n",
1153
1154
        "<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",
1155
1156
1157
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 2 -->\n",
1158
1159
1160
1161
        "<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",
1162
1163
        "</g>\n",
        "<!-- I&#45;&gt;2 -->\n",
1164
1165
1166
        "<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",
1167
1168
        "</g>\n",
        "<!-- 6 -->\n",
1169
1170
1171
1172
1173
        "<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",
1174
1175
        "</g>\n",
        "<!-- 2&#45;&gt;6 -->\n",
1176
1177
1178
1179
        "<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;6</title>\n",
        "<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",
1180
1181
        "</g>\n",
        "<!-- 5 -->\n",
1182
1183
1184
1185
1186
        "<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",
1187
1188
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
1189
1190
1191
1192
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
        "<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",
1193
1194
        "</g>\n",
        "<!-- 3 -->\n",
1195
1196
1197
1198
1199
        "<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",
1200
1201
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
1202
1203
1204
1205
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<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",
1206
1207
        "</g>\n",
        "<!-- 4 -->\n",
1208
1209
1210
1211
1212
        "<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",
1213
1214
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
1215
1216
1217
1218
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<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",
1219
1220
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
1221
1222
1223
1224
        "<g id=\"edge26\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
        "<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",
        "<text text-anchor=\"middle\" x=\"971.666\" y=\"-380.741\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
1225
1226
        "</g>\n",
        "<!-- 1 -->\n",
1227
1228
1229
1230
        "<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",
1231
1232
        "</g>\n",
        "<!-- 1&#45;&gt;6 -->\n",
1233
1234
1235
1236
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M886.779,-270.297C901.227,-279.719 920.436,-292.245 936.826,-302.933\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"942.723,-306.778 935.139,-305.593 939.791,-304.866 936.859,-302.954 936.859,-302.954 936.859,-302.954 939.791,-304.866 938.58,-300.316 942.723,-306.778 942.723,-306.778\"/>\n",
        "<text text-anchor=\"start\" x=\"908.725\" y=\"-294.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1237
1238
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
1239
1240
1241
1242
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M854.562,-281.37C853.921,-291.924 857.019,-300.87 863.855,-300.87 869.089,-300.87 872.131,-295.626 872.982,-288.431\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"873.148,-281.37 876.133,-288.442 873.065,-284.869 872.983,-288.368 872.983,-288.368 872.983,-288.368 873.065,-284.869 869.834,-288.294 873.148,-281.37 873.148,-281.37\"/>\n",
        "<text text-anchor=\"start\" x=\"860.355\" y=\"-304.67\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
1243
1244
        "</g>\n",
        "<!-- 8 -->\n",
1245
1246
1247
1248
        "<g id=\"node5\" class=\"node\"><title>8</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"863.855\" cy=\"-43\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"859.355\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
        "<text text-anchor=\"start\" x=\"855.855\" y=\"-31.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
1249
1250
        "</g>\n",
        "<!-- 8&#45;&gt;6 -->\n",
1251
1252
1253
1254
        "<g id=\"edge34\" class=\"edge\"><title>8&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M885.194,-59.8794C896.985,-70.7349 911.152,-85.8048 919.725,-102 950.677,-160.469 962.917,-237.273 967.692,-283.79\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"968.395,-290.989 964.579,-284.329 968.055,-287.505 967.714,-284.022 967.714,-284.022 967.714,-284.022 968.055,-287.505 970.849,-283.715 968.395,-290.989 968.395,-290.989\"/>\n",
        "<text text-anchor=\"start\" x=\"908.725\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
1255
1256
        "</g>\n",
        "<!-- 8&#45;&gt;1 -->\n",
1257
1258
1259
1260
        "<g id=\"edge33\" class=\"edge\"><title>8&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M847.171,-64.7811C827.002,-92.619 794.184,-143.137 781.485,-192.5 779.824,-198.956 778.176,-201.712 781.485,-207.5 792.194,-226.234 813.276,-238.449 831.429,-245.935\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"837.96,-248.482 830.294,-248.874 834.7,-247.211 831.439,-245.939 831.439,-245.939 831.439,-245.939 834.7,-247.211 832.584,-243.004 837.96,-248.482 837.96,-248.482\"/>\n",
        "<text text-anchor=\"start\" x=\"769.485\" y=\"-196.3\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
1261
1262
        "</g>\n",
        "<!-- 8&#45;&gt;8 -->\n",
1263
1264
1265
1266
        "<g id=\"edge35\" class=\"edge\"><title>8&#45;&gt;8</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M854.562,-68.37C853.921,-78.9238 857.019,-87.8701 863.855,-87.8701 869.089,-87.8701 872.131,-82.6259 872.982,-75.4312\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"873.148,-68.37 876.133,-75.4419 873.065,-71.869 872.983,-75.3681 872.983,-75.3681 872.983,-75.3681 873.065,-71.869 869.834,-75.2943 873.148,-68.37 873.148,-68.37\"/>\n",
        "<text text-anchor=\"start\" x=\"846.855\" y=\"-91.6701\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
1267
1268
        "</g>\n",
        "<!-- 0 -->\n",
1269
1270
1271
1272
        "<g id=\"node6\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"390.492\" cy=\"-317\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"385.992\" y=\"-320.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"382.492\" y=\"-305.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
1273
1274
        "</g>\n",
        "<!-- 0&#45;&gt;6 -->\n",
1275
1276
1277
1278
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M405.588,-339.236C430.449,-375.408 485.801,-443 552.304,-443 552.304,-443 552.304,-443 864.855,-443 908.58,-443 938.792,-397.534 955.419,-363.046\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"958.563,-356.312 958.456,-363.987 957.082,-359.483 955.602,-362.655 955.602,-362.655 955.602,-362.655 957.082,-359.483 952.747,-361.322 958.563,-356.312 958.563,-356.312\"/>\n",
        "<text text-anchor=\"start\" x=\"694.115\" y=\"-446.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1279
1280
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
1281
1282
1283
1284
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M414.107,-330.764C420.892,-334.795 428.385,-339.151 435.362,-343 472.087,-363.257 478.59,-376.171 519.362,-386 548.692,-393.071 557.636,-391.793 587.245,-386 684.636,-366.944 787.277,-306.018 835.186,-274.812\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"841.303,-270.795 837.181,-277.27 838.377,-272.716 835.452,-274.637 835.452,-274.637 835.452,-274.637 838.377,-272.716 833.722,-272.004 841.303,-270.795 841.303,-270.795\"/>\n",
        "<text text-anchor=\"start\" x=\"620.245\" y=\"-385.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
1285
1286
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
1287
1288
1289
1290
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M376.663,-340.087C374.75,-351.6 379.36,-361.87 390.492,-361.87 399.19,-361.87 403.906,-355.602 404.641,-347.369\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"404.321,-340.087 407.775,-346.942 404.475,-343.583 404.628,-347.08 404.628,-347.08 404.628,-347.08 404.475,-343.583 401.481,-347.218 404.321,-340.087 404.321,-340.087\"/>\n",
        "<text text-anchor=\"start\" x=\"372.492\" y=\"-365.67\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
1291
1292
        "</g>\n",
        "<!-- 0&#45;&gt;5 -->\n",
1293
1294
1295
1296
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M416.844,-310.208C422.87,-308.876 429.308,-307.681 435.362,-307 460.857,-304.131 489.667,-304.824 512.312,-306.262\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"519.435,-306.752 512.235,-309.414 515.943,-306.512 512.452,-306.272 512.452,-306.272 512.452,-306.272 515.943,-306.512 512.668,-303.129 519.435,-306.752 519.435,-306.752\"/>\n",
        "<text text-anchor=\"start\" x=\"448.362\" y=\"-310.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1297
1298
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
1299
1300
1301
1302
        "<g id=\"edge24\" class=\"edge\"><title>5&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M585.837,-319.983C592.202,-321.623 598.89,-323.085 605.245,-324 734.36,-342.596 768.306,-330.718 898.725,-328 909.083,-327.784 920.274,-327.394 930.673,-326.964\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"937.726,-326.662 930.867,-330.109 934.229,-326.812 930.732,-326.962 930.732,-326.962 930.732,-326.962 934.229,-326.812 930.598,-323.815 937.726,-326.662 937.726,-326.662\"/>\n",
        "<text text-anchor=\"start\" x=\"784.485\" y=\"-337.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
1303
1304
        "</g>\n",
        "<!-- 5&#45;&gt;0 -->\n",
1305
1306
1307
1308
        "<g id=\"edge22\" class=\"edge\"><title>5&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M520.438,-318.696C514.161,-320.071 507.59,-321.276 501.362,-322 472.225,-325.386 464.649,-323.664 435.362,-322 431.818,-321.799 428.12,-321.507 424.441,-321.163\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"417.432,-320.45 424.715,-318.025 420.914,-320.804 424.396,-321.159 424.396,-321.159 424.396,-321.159 420.914,-320.804 424.077,-324.292 417.432,-320.45 417.432,-320.45\"/>\n",
        "<text text-anchor=\"start\" x=\"435.362\" y=\"-327.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; !c</text>\n",
1309
1310
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
1311
1312
1313
1314
        "<g id=\"edge23\" class=\"edge\"><title>5&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M537.989,-340.41C537.308,-352.168 542.413,-361.941 553.304,-361.941 561.812,-361.941 566.789,-355.976 568.235,-347.76\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"568.619,-340.41 571.399,-347.565 568.436,-343.906 568.253,-347.401 568.253,-347.401 568.253,-347.401 568.436,-343.906 565.108,-347.237 568.619,-340.41 568.619,-340.41\"/>\n",
        "<text text-anchor=\"start\" x=\"533.304\" y=\"-365.741\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1315
1316
        "</g>\n",
        "<!-- 7 -->\n",
1317
1318
1319
1320
        "<g id=\"node8\" class=\"node\"><title>7</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"712.115\" cy=\"-252\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"707.615\" y=\"-255.8\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
        "<text text-anchor=\"start\" x=\"704.115\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
1321
1322
        "</g>\n",
        "<!-- 5&#45;&gt;7 -->\n",
1323
1324
1325
1326
        "<g id=\"edge25\" class=\"edge\"><title>5&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M587.223,-307.418C610.467,-304.627 641.865,-298.86 667.245,-287 673.865,-283.906 680.372,-279.621 686.263,-275.108\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"691.931,-270.555 688.446,-277.395 689.202,-272.747 686.473,-274.939 686.473,-274.939 686.473,-274.939 689.202,-272.747 684.501,-272.484 691.931,-270.555 691.931,-270.555\"/>\n",
        "<text text-anchor=\"start\" x=\"605.245\" y=\"-308.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
1327
1328
        "</g>\n",
        "<!-- 7&#45;&gt;6 -->\n",
1329
1330
1331
1332
        "<g id=\"edge30\" class=\"edge\"><title>7&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M723.736,-227.525C730.987,-214.105 742.01,-198.676 756.985,-191 813.214,-162.179 846.198,-166.882 898.725,-202 928.236,-221.73 947.267,-257.988 958.294,-286.045\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"960.793,-292.622 955.362,-287.198 959.55,-289.351 958.307,-286.079 958.307,-286.079 958.307,-286.079 959.55,-289.351 961.251,-284.96 960.793,-292.622 960.793,-292.622\"/>\n",
        "<text text-anchor=\"start\" x=\"845.855\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1333
1334
        "</g>\n",
        "<!-- 7&#45;&gt;1 -->\n",
1335
1336
1337
1338
        "<g id=\"edge28\" class=\"edge\"><title>7&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M739.198,-252.697C764.35,-253.369 802.514,-254.388 829.787,-255.117\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"836.82,-255.305 829.739,-258.266 833.322,-255.211 829.823,-255.118 829.823,-255.118 829.823,-255.118 833.322,-255.211 829.907,-251.969 836.82,-255.305 836.82,-255.305\"/>\n",
        "<text text-anchor=\"start\" x=\"756.985\" y=\"-258.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; c</text>\n",
1339
1340
        "</g>\n",
        "<!-- 7&#45;&gt;8 -->\n",
1341
1342
1343
1344
        "<g id=\"edge32\" class=\"edge\"><title>7&#45;&gt;8</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M720.839,-226.238C728.129,-204.294 740.415,-172.516 756.985,-148 779.396,-114.841 813.352,-83.4366 836.734,-63.7617\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"842.142,-59.2611 838.776,-66.16 839.452,-61.4999 836.761,-63.7388 836.761,-63.7388 836.761,-63.7388 839.452,-61.4999 834.746,-61.3175 842.142,-59.2611 842.142,-59.2611\"/>\n",
        "<text text-anchor=\"start\" x=\"758.985\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; c</text>\n",
1345
1346
        "</g>\n",
        "<!-- 7&#45;&gt;0 -->\n",
1347
1348
1349
1350
        "<g id=\"edge27\" class=\"edge\"><title>7&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M685.502,-248.089C648.268,-243.276 577.308,-237.402 519.362,-252 482.63,-261.254 444.405,-282.459 419.429,-298.146\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"413.373,-302.004 417.584,-295.586 416.325,-300.123 419.277,-298.243 419.277,-298.243 419.277,-298.243 416.325,-300.123 420.97,-300.899 413.373,-302.004 413.373,-302.004\"/>\n",
        "<text text-anchor=\"start\" x=\"520.304\" y=\"-255.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; !c</text>\n",
1351
1352
        "</g>\n",
        "<!-- 7&#45;&gt;5 -->\n",
1353
1354
1355
1356
        "<g id=\"edge29\" class=\"edge\"><title>7&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M685.23,-252.094C663.105,-253.05 630.877,-256.561 605.245,-268 597.558,-271.43 590.089,-276.349 583.346,-281.619\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"577.863,-286.105 581.287,-279.234 580.572,-283.888 583.281,-281.672 583.281,-281.672 583.281,-281.672 580.572,-283.888 585.276,-284.11 577.863,-286.105 577.863,-286.105\"/>\n",
        "<text text-anchor=\"start\" x=\"616.245\" y=\"-271.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1357
1358
        "</g>\n",
        "<!-- 7&#45;&gt;7 -->\n",
1359
1360
1361
1362
        "<g id=\"edge31\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M698.579,-275.546C696.907,-286.872 701.419,-296.87 712.115,-296.87 720.471,-296.87 725.052,-290.768 725.86,-282.698\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"725.651,-275.546 729.004,-282.451 725.753,-279.045 725.856,-282.543 725.856,-282.543 725.856,-282.543 725.753,-279.045 722.707,-282.636 725.651,-275.546 725.651,-275.546\"/>\n",
        "<text text-anchor=\"start\" x=\"681.115\" y=\"-300.67\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; !c</text>\n",
1363
1364
        "</g>\n",
        "<!-- 3&#45;&gt;6 -->\n",
1365
1366
1367
1368
        "<g id=\"edge15\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M248.804,-445.016C276.447,-478.728 329.604,-532 389.492,-532 389.492,-532 389.492,-532 864.855,-532 938.544,-532 960.944,-426.71 967.732,-366.314\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"968.485,-359.182 970.882,-366.474 968.117,-362.663 967.75,-366.143 967.75,-366.143 967.75,-366.143 968.117,-362.663 964.617,-365.813 968.485,-359.182 968.485,-359.182\"/>\n",
        "<text text-anchor=\"start\" x=\"618.245\" y=\"-535.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1369
1370
        "</g>\n",
        "<!-- 3&#45;&gt;1 -->\n",
1371
1372
1373
1374
        "<g id=\"edge13\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M259.066,-431.446C342.79,-466.322 581.561,-550.984 746.985,-462 812.598,-426.705 843.426,-337.849 855.806,-289.164\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"857.5,-282.283 858.885,-289.834 856.663,-285.682 855.826,-289.08 855.826,-289.08 855.826,-289.08 856.663,-285.682 852.768,-288.327 857.5,-282.283 857.5,-282.283\"/>\n",
        "<text text-anchor=\"start\" x=\"537.304\" y=\"-505.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; c</text>\n",
1375
1376
        "</g>\n",
        "<!-- 3&#45;&gt;0 -->\n",
1377
1378
1379
1380
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M257.061,-400.176C286.355,-381.777 331.797,-353.237 361.097,-334.834\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"367.093,-331.069 362.84,-337.459 364.129,-332.93 361.165,-334.792 361.165,-334.792 361.165,-334.792 364.129,-332.93 359.489,-332.124 367.093,-331.069 367.093,-331.069\"/>\n",
        "<text text-anchor=\"start\" x=\"294.622\" y=\"-389.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
1381
1382
        "</g>\n",
        "<!-- 3&#45;&gt;5 -->\n",
1383
1384
1385
1386
        "<g id=\"edge14\" class=\"edge\"><title>3&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M261.614,-415.181C285.137,-412.895 317.472,-409.195 345.622,-404 418.726,-390.509 436.998,-380.193 501.362,-343 506.991,-339.748 512.864,-336.147 518.538,-332.554\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"524.596,-328.675 520.399,-335.103 521.648,-330.563 518.701,-332.45 518.701,-332.45 518.701,-332.45 521.648,-330.563 517.002,-329.797 524.596,-328.675 524.596,-328.675\"/>\n",
        "<text text-anchor=\"start\" x=\"370.492\" y=\"-405.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
1387
1388
        "</g>\n",
        "<!-- 4&#45;&gt;6 -->\n",
1389
1390
1391
1392
        "<g id=\"edge19\" class=\"edge\"><title>4&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M259.868,-162.119C349.094,-132.667 612.268,-57.5477 818.985,-118 859.362,-129.808 869.773,-138.478 898.725,-169 929.959,-201.928 949.481,-250.832 960.178,-285.084\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"962.327,-292.159 957.278,-286.377 961.31,-288.81 960.292,-285.461 960.292,-285.461 960.292,-285.461 961.31,-288.81 963.306,-284.546 962.327,-292.159 962.327,-292.159\"/>\n",
        "<text text-anchor=\"start\" x=\"618.245\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; c</text>\n",
1393
1394
        "</g>\n",
        "<!-- 4&#45;&gt;1 -->\n",
1395
1396
1397
1398
        "<g id=\"edge17\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M261.724,-171.805C344.713,-169.603 568.065,-168.64 746.985,-213 776.744,-220.378 809.383,-232.917 832.414,-242.557\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"838.942,-245.319 831.267,-245.492 835.718,-243.955 832.495,-242.591 832.495,-242.591 832.495,-242.591 835.718,-243.955 833.723,-239.69 838.942,-245.319 838.942,-245.319\"/>\n",
        "<text text-anchor=\"start\" x=\"522.304\" y=\"-188.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; c</text>\n",
1399
1400
        "</g>\n",
        "<!-- 4&#45;&gt;8 -->\n",
1401
1402
1403
1404
        "<g id=\"edge21\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M239.866,-141.113C248.12,-121.831 261.148,-98.1297 279.622,-83 319.378,-50.4424 338.107,-47 389.492,-47 389.492,-47 389.492,-47 713.115,-47 753.152,-47 799.188,-45.5534 829.529,-44.4001\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"836.891,-44.1142 830.019,-47.5335 833.394,-44.2501 829.897,-44.3859 829.897,-44.3859 829.897,-44.3859 833.394,-44.2501 829.774,-41.2382 836.891,-44.1142 836.891,-44.1142\"/>\n",
        "<text text-anchor=\"start\" x=\"524.304\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b &amp; c</text>\n",
1405
1406
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
1407
1408
1409
1410
        "<g id=\"edge16\" class=\"edge\"><title>4&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M236.628,-205.831C244.017,-229.759 257.323,-261.309 279.622,-281 301.03,-299.903 332.58,-308.915 356.386,-313.19\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"363.506,-314.371 356.085,-316.333 360.053,-313.798 356.6,-313.226 356.6,-313.226 356.6,-313.226 360.053,-313.798 357.115,-310.118 363.506,-314.371 363.506,-314.371\"/>\n",
        "<text text-anchor=\"start\" x=\"279.622\" y=\"-315.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b &amp; !c</text>\n",
1411
1412
        "</g>\n",
        "<!-- 4&#45;&gt;5 -->\n",