decompose.ipynb 467 KB
Newer Older
1
{
2
3
4
5
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
   "metadata": {},
7
8
9
10
11
12
   "outputs": [],
   "source": [
    "from IPython.display import display\n",
    "import spot\n",
    "spot.setup(show_default='.bans')"
   ]
13
14
  },
  {
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This notebook demonstrates how to use the `decompose_scc()` function to split an automaton in up to three automata capturing different behaviors.   This is based on the paper [Strength-based decomposition of the property Büchi 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-scc` option.\n",
    "\n",
    "# Basics\n",
    "\n",
    "Let's define the following strengths of accepting SCCs:\n",
    "\n",
    "- 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",
    "\n",
    "The strengths **strong**, **stricly inherently weak**, and **inherently terminal** define a partition of all accepting SCCs.  The following Büchi 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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
   "metadata": {},
40
   "outputs": [
41
    {
42
43
44
45
46
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
47
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
48
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
       "<!-- Pages: 1 -->\n",
       "<svg width=\"496pt\" height=\"315pt\"\n",
       " viewBox=\"0.00 0.00 496.00 315.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 311)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-311 492,-311 492,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"223\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"245\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"261\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"221\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"428,-148 428,-248 480,-248 480,-148 428,-148\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"166,-8 166,-108 218,-108 218,-8 166,-8\"/>\n",
       "</g>\n",
       "<g id=\"clust3\" class=\"cluster\">\n",
       "<title>cluster_2</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"345,-148 345,-233 397,-233 397,-148 345,-148\"/>\n",
       "</g>\n",
       "<g id=\"clust4\" class=\"cluster\">\n",
       "<title>cluster_3</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"30,-148 30,-263 293,-263 293,-148 30,-148\"/>\n",
73
74
75
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
77
78
79
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
80
81
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
82
83
84
85
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-174C4.178,-174 17.9448,-174 30.9241,-174\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-174 30.9808,-177.1501 34.4807,-174 30.9807,-174.0001 30.9807,-174.0001 30.9807,-174.0001 34.4807,-174 30.9807,-170.8501 37.9807,-174 37.9807,-174\"/>\n",
86
87
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
88
89
90
91
92
93
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-191.0373C48.3189,-200.8579 50.4453,-210 56,-210 60.166,-210 62.4036,-204.8576 62.7128,-198.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-191.0373 65.8541,-197.8818 62.5434,-194.5335 62.7076,-198.0296 62.7076,-198.0296 62.7076,-198.0296 62.5434,-194.5335 59.561,-198.1774 62.3792,-191.0373 62.3792,-191.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"48\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
94
95
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
96
97
98
99
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"454\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"454\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
100
101
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
102
103
104
105
106
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M71.7423,-164.9119C96.4901,-151.5061 146.387,-128 192,-128 192,-128 192,-128 371,-128 395.5036,-128 419.5513,-143.5275 435.4016,-156.5397\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"440.8559,-161.1864 433.4846,-159.0447 438.1916,-158.9167 435.5274,-156.6469 435.5274,-156.6469 435.5274,-156.6469 438.1916,-158.9167 437.5702,-154.249 440.8559,-161.1864 440.8559,-161.1864\"/>\n",
       "<text text-anchor=\"start\" x=\"263.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
107
108
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
110
111
112
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"192\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"192\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
113
114
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
116
117
118
119
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M61.2718,-156.6681C66.8826,-140.3827 77.0314,-116.0332 92,-99 113.6775,-74.3325 146.8751,-55.2821 168.9997,-44.3562\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"175.4855,-41.2291 170.5482,-47.1067 172.3328,-42.7492 169.1801,-44.2693 169.1801,-44.2693 169.1801,-44.2693 172.3328,-42.7492 167.812,-41.4319 175.4855,-41.2291 175.4855,-41.2291\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
120
121
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
122
123
124
125
       "<g id=\"node6\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"267\" cy=\"-192\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"267\" y=\"-188.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
126
127
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
129
130
131
132
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>0&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M73.9897,-175.5347C111.6735,-178.7494 198.968,-186.1963 242.0423,-189.8709\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"249.0558,-190.4692 241.8133,-193.0127 245.5685,-190.1717 242.0811,-189.8741 242.0811,-189.8741 242.0811,-189.8741 245.5685,-190.1717 242.3489,-186.7355 249.0558,-190.4692 249.0558,-190.4692\"/>\n",
       "<text text-anchor=\"start\" x=\"174\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
133
134
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
135
136
137
138
139
140
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M446.9688,-190.6641C445.4063,-200.625 447.75,-210 454,-210 458.6875,-210 461.1777,-204.7266 461.4707,-197.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"461.0313,-190.6641 464.6006,-197.4598 461.2438,-194.1576 461.4564,-197.6511 461.4564,-197.6511 461.4564,-197.6511 461.2438,-194.1576 458.3122,-197.8425 461.0313,-190.6641 461.0313,-190.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"449.5\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "<text text-anchor=\"start\" x=\"446\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
141
142
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
143
144
145
146
147
148
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.2664,-51.0373C183.8922,-60.8579 186.1367,-70 192,-70 196.3975,-70 198.7594,-64.8576 199.0858,-58.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"198.7336,-51.0373 202.2263,-57.8728 198.9069,-54.533 199.0802,-58.0287 199.0802,-58.0287 199.0802,-58.0287 198.9069,-54.533 195.934,-58.1847 198.7336,-51.0373 198.7336,-51.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"187.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
149
150
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
151
152
153
154
       "<g id=\"node5\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"371\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"371\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
155
156
       "</g>\n",
       "<!-- 4&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
158
159
160
161
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>4&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M389.0098,-174C400.5679,-174 415.7507,-174 428.5345,-174\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"435.7388,-174 428.7388,-177.1501 432.2388,-174 428.7388,-174.0001 428.7388,-174.0001 428.7388,-174.0001 432.2388,-174 428.7387,-170.8501 435.7388,-174 435.7388,-174\"/>\n",
       "<text text-anchor=\"start\" x=\"407\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
162
163
       "</g>\n",
       "<!-- 4&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
164
165
166
167
168
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>4&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M363.9688,-190.6641C362.4063,-200.625 364.75,-210 371,-210 375.6875,-210 378.1777,-204.7266 378.4707,-197.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"378.0313,-190.6641 381.6006,-197.4598 378.2438,-194.1576 378.4564,-197.6511 378.4564,-197.6511 378.4564,-197.6511 378.2438,-194.1576 375.3122,-197.8425 378.0313,-190.6641 378.0313,-190.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"367.5\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
169
170
       "</g>\n",
       "<!-- 3&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
171
172
173
174
175
176
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>3&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M249.4684,-196.923C240.196,-199.2748 228.572,-201.8279 218,-203 161.7118,-209.2404 146.7131,-198.6215 92,-184 88.24,-182.9952 84.2649,-181.912 80.3822,-180.8425\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"73.5593,-178.9519 81.1463,-177.7856 76.9322,-179.8866 80.3051,-180.8212 80.3051,-180.8212 80.3051,-180.8212 76.9322,-179.8866 79.4639,-183.8568 73.5593,-178.9519 73.5593,-178.9519\"/>\n",
       "<text text-anchor=\"start\" x=\"172\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
177
178
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
179
180
181
182
183
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M280.9572,-203.6937C305.0872,-222.4071 355.9593,-255.2135 397,-237 415.8745,-228.6237 431.1522,-210.5674 441.1221,-195.9237\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"445.0651,-189.895 443.8698,-197.4775 443.1493,-192.8242 441.2336,-195.7533 441.2336,-195.7533 441.2336,-195.7533 443.1493,-192.8242 438.5973,-194.0292 445.0651,-189.895 445.0651,-189.895\"/>\n",
       "<text text-anchor=\"start\" x=\"353\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
184
185
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
186
187
188
189
190
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>3&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M285.1154,-188.8646C301.967,-185.948 327.2278,-181.576 345.9961,-178.3276\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"353.0922,-177.0994 346.732,-181.3972 349.6434,-177.6964 346.1947,-178.2933 346.1947,-178.2933 346.1947,-178.2933 349.6434,-177.6964 345.6575,-175.1894 353.0922,-177.0994 353.0922,-177.0994\"/>\n",
       "<text text-anchor=\"start\" x=\"303\" y=\"-188.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
191
192
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
193
194
195
196
197
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M260.6208,-209.0373C259.3189,-218.8579 261.4453,-228 267,-228 271.166,-228 273.4036,-222.8576 273.7128,-216.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"273.3792,-209.0373 276.8541,-215.8818 273.5434,-212.5335 273.7076,-216.0296 273.7076,-216.0296 273.7076,-216.0296 273.5434,-212.5335 270.561,-216.1774 273.3792,-209.0373 273.3792,-209.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"249\" y=\"-231.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
198
199
200
201
202
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
203
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c40f0> >"
204
205
206
      ]
     },
     "execution_count": 2,
207
     "metadata": {},
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
     "output_type": "execute_result"
    }
   ],
   "source": [
    "aut = spot.translate('(Ga -> Gb) W c')\n",
    "aut"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve.  \n",
    "\n",
    "The letters used for this specification are as follows:\n",
    "\n",
    "- `t`: (inherently) terminal\n",
    "- `w`: (strictly inherently) weak\n",
    "- `s`: strong\n",
    "\n",
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
234
   "metadata": {},
235
   "outputs": [
236
    {
237
238
239
240
241
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
242
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
243
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
       "<!-- Pages: 1 -->\n",
       "<svg width=\"309pt\" height=\"268pt\"\n",
       " viewBox=\"0.00 0.00 309.00 268.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 264)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-264 305,-264 305,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"129.5\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"151.5\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"167.5\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"127.5\" y=\"-231.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"166,-8 166,-108 218,-108 218,-8 166,-8\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"30,-116 30,-216 293,-216 293,-116 30,-116\"/>\n",
260
261
262
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
263
264
265
266
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" 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\" fill=\"#000000\">0</text>\n",
267
268
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
269
270
271
272
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-142C4.178,-142 17.9448,-142 30.9241,-142\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-142 30.9808,-145.1501 34.4807,-142 30.9807,-142.0001 30.9807,-142.0001 30.9807,-142.0001 34.4807,-142 30.9807,-138.8501 37.9807,-142 37.9807,-142\"/>\n",
273
274
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
275
276
277
278
279
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-159.0373C48.3189,-168.8579 50.4453,-178 56,-178 60.166,-178 62.4036,-172.8576 62.7128,-166.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-159.0373 65.8541,-165.8818 62.5434,-162.5335 62.7076,-166.0296 62.7076,-166.0296 62.7076,-166.0296 62.5434,-162.5335 59.561,-166.1774 62.3792,-159.0373 62.3792,-159.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
280
281
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
282
283
284
285
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"192\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"192\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
286
287
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
288
289
290
291
292
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M70.2973,-130.6462C94.7464,-111.2308 144.6248,-71.6215 172.3348,-49.6165\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"177.8942,-45.2016 174.3714,-52.0217 175.1533,-47.3782 172.4124,-49.5549 172.4124,-49.5549 172.4124,-49.5549 175.1533,-47.3782 170.4535,-47.088 177.8942,-45.2016 177.8942,-45.2016\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-116.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
293
294
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
295
296
297
298
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"267\" cy=\"-150\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"267\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
299
300
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
301
302
303
304
305
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M73.9897,-142.6821C111.5793,-144.1073 198.5319,-147.4041 241.7184,-149.0415\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"248.7561,-149.3083 241.6417,-152.1907 245.2586,-149.1756 241.7611,-149.043 241.7611,-149.043 241.7611,-149.043 245.2586,-149.1756 241.8805,-145.8952 248.7561,-149.3083 248.7561,-149.3083\"/>\n",
       "<text text-anchor=\"start\" x=\"174\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
306
307
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
309
310
311
312
313
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.2664,-51.0373C183.8922,-60.8579 186.1367,-70 192,-70 196.3975,-70 198.7594,-64.8576 199.0858,-58.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"198.7336,-51.0373 202.2263,-57.8728 198.9069,-54.533 199.0802,-58.0287 199.0802,-58.0287 199.0802,-58.0287 198.9069,-54.533 195.934,-58.1847 198.7336,-51.0373 198.7336,-51.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"187.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
314
315
       "</g>\n",
       "<!-- 2&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
316
317
318
319
320
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M250.1337,-157.4182C240.8505,-161.0978 229.0101,-165.1443 218,-167 168.9526,-175.2665 111.3649,-160.592 79.761,-150.4486\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"73.0512,-148.2368 80.6855,-147.4367 76.3753,-149.3325 79.6993,-150.4283 79.6993,-150.4283 79.6993,-150.4283 76.3753,-149.3325 78.7131,-153.42 73.0512,-148.2368 73.0512,-148.2368\"/>\n",
       "<text text-anchor=\"start\" x=\"172\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
321
322
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
323
324
325
326
327
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M260.6208,-167.0373C259.3189,-176.8579 261.4453,-186 267,-186 271.166,-186 273.4036,-180.8576 273.7128,-174.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"273.3792,-167.0373 276.8541,-173.8818 273.5434,-170.5335 273.7076,-174.0296 273.7076,-174.0296 273.7076,-174.0296 273.5434,-170.5335 270.561,-174.1774 273.3792,-167.0373 273.3792,-167.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"249\" y=\"-189.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
328
329
330
331
332
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
333
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c40c0> >"
334
335
336
      ]
     },
     "execution_count": 3,
337
     "metadata": {},
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
     "output_type": "execute_result"
    }
   ],
   "source": [
    "spot.decompose_scc(aut, 'w')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
355
   "metadata": {},
356
   "outputs": [
357
    {
358
359
360
361
362
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
363
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
364
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
       "<!-- Pages: 1 -->\n",
       "<svg width=\"435pt\" height=\"173pt\"\n",
       " viewBox=\"0.00 0.00 435.00 173.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 169)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-169 431,-169 431,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"192.5\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"214.5\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"230.5\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"190.5\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"367,-20 367,-120 419,-120 419,-20 367,-20\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"284,-20 284,-105 336,-105 336,-20 284,-20\"/>\n",
       "</g>\n",
       "<g id=\"clust3\" class=\"cluster\">\n",
       "<title>cluster_2</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"30,-20 30,-120 232,-120 232,-20 30,-20\"/>\n",
385
386
387
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388
389
390
391
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
392
393
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394
395
396
397
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-46C4.178,-46 17.9448,-46 30.9241,-46\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-46 30.9808,-49.1501 34.4807,-46 30.9807,-46.0001 30.9807,-46.0001 30.9807,-46.0001 34.4807,-46 30.9807,-42.8501 37.9807,-46 37.9807,-46\"/>\n",
398
399
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400
401
402
403
404
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-63.0373C48.3189,-72.8579 50.4453,-82 56,-82 60.166,-82 62.4036,-76.8576 62.7128,-70.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-63.0373 65.8541,-69.8818 62.5434,-66.5335 62.7076,-70.0296 62.7076,-70.0296 62.7076,-70.0296 62.5434,-66.5335 59.561,-70.1774 62.3792,-63.0373 62.3792,-63.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
405
406
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407
408
409
410
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"393\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"393\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
411
412
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
413
414
415
416
417
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M68.1391,-32.6949C81.9254,-19.1093 105.7965,0 131,0 131,0 131,0 310,0 334.5036,0 358.5513,-15.5275 374.4016,-28.5397\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"379.8559,-33.1864 372.4846,-31.0447 377.1916,-30.9167 374.5274,-28.6469 374.5274,-28.6469 374.5274,-28.6469 377.1916,-30.9167 376.5702,-26.249 379.8559,-33.1864 379.8559,-33.1864\"/>\n",
       "<text text-anchor=\"start\" x=\"202.5\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
418
419
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
420
421
422
423
       "<g id=\"node5\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"206\" cy=\"-56\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"206\" y=\"-52.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
424
425
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
426
427
428
429
430
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0935,-47.2062C100.6718,-48.9781 150.3801,-52.292 180.604,-54.3069\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"187.8423,-54.7895 180.6483,-57.4668 184.3501,-54.5566 180.8578,-54.3238 180.8578,-54.3238 180.8578,-54.3238 184.3501,-54.5566 181.0674,-51.1807 187.8423,-54.7895 187.8423,-54.7895\"/>\n",
       "<text text-anchor=\"start\" x=\"113\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
431
432
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
433
434
435
436
437
438
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M385.9688,-62.6641C384.4063,-72.625 386.75,-82 393,-82 397.6875,-82 400.1777,-76.7266 400.4707,-69.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"400.0313,-62.6641 403.6006,-69.4598 400.2438,-66.1576 400.4564,-69.6511 400.4564,-69.6511 400.4564,-69.6511 400.2438,-66.1576 397.3122,-69.8425 400.0313,-62.6641 400.0313,-62.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"388.5\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "<text text-anchor=\"start\" x=\"385\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
439
440
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
441
442
443
444
       "<g id=\"node4\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"310\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"310\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
445
446
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
447
448
449
450
451
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M328.0098,-46C339.5679,-46 354.7507,-46 367.5345,-46\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"374.7388,-46 367.7388,-49.1501 371.2388,-46 367.7388,-46.0001 367.7388,-46.0001 367.7388,-46.0001 371.2388,-46 367.7387,-42.8501 374.7388,-46 374.7388,-46\"/>\n",
       "<text text-anchor=\"start\" x=\"346\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
452
453
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
454
455
456
457
458
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M302.9688,-62.6641C301.4063,-72.625 303.75,-82 310,-82 314.6875,-82 317.1777,-76.7266 317.4707,-69.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"317.0313,-62.6641 320.6006,-69.4598 317.2438,-66.1576 317.4564,-69.6511 317.4564,-69.6511 317.4564,-69.6511 317.2438,-66.1576 314.3122,-69.8425 317.0313,-62.6641 317.0313,-62.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"306.5\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
459
460
       "</g>\n",
       "<!-- 2&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
461
462
463
464
465
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M189.0754,-62.434C169.992,-68.8187 138.0894,-76.8678 111,-71 99.6726,-68.5464 87.8767,-63.5531 78.1272,-58.6697\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"71.7353,-55.339 79.3988,-55.7804 74.8392,-56.9564 77.9431,-58.5739 77.9431,-58.5739 77.9431,-58.5739 74.8392,-56.9564 76.4875,-61.3673 71.7353,-55.339 71.7353,-55.339\"/>\n",
       "<text text-anchor=\"start\" x=\"111\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
466
467
       "</g>\n",
       "<!-- 2&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
468
469
470
471
472
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M219.0266,-68.4976C242.5652,-89.4912 293.6722,-127.7847 336,-109 354.8745,-100.6237 370.1522,-82.5674 380.1221,-67.9237\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"384.0651,-61.895 382.8698,-69.4775 382.1493,-64.8242 380.2336,-67.7533 380.2336,-67.7533 380.2336,-67.7533 382.1493,-64.8242 377.5973,-66.0292 384.0651,-61.895 384.0651,-61.895\"/>\n",
       "<text text-anchor=\"start\" x=\"292\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
473
474
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
475
476
477
478
479
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M224.1154,-54.2581C240.8642,-52.6477 265.92,-50.2385 284.6521,-48.4373\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"291.7432,-47.7555 285.0769,-51.5611 288.2593,-48.0905 284.7754,-48.4255 284.7754,-48.4255 284.7754,-48.4255 288.2593,-48.0905 284.4738,-45.29 291.7432,-47.7555 291.7432,-47.7555\"/>\n",
       "<text text-anchor=\"start\" x=\"242\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
480
481
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
482
483
484
485
486
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M199.6208,-73.0373C198.3189,-82.8579 200.4453,-92 206,-92 210.166,-92 212.4036,-86.8576 212.7128,-80.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"212.3792,-73.0373 215.8541,-79.8818 212.5434,-76.5335 212.7076,-80.0296 212.7076,-80.0296 212.7076,-80.0296 212.5434,-76.5335 209.561,-80.1774 212.3792,-73.0373 212.3792,-73.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"188\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
487
488
489
490
491
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
492
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d860a060> >"
493
494
495
      ]
     },
     "execution_count": 4,
496
     "metadata": {},
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
     "output_type": "execute_result"
    }
   ],
   "source": [
    "spot.decompose_scc(aut, 't')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here is the **strong** part:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
514
   "metadata": {},
515
   "outputs": [
516
    {
517
518
519
520
521
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
522
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
523
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
524
525
526
527
528
529
530
531
532
533
534
535
       "<!-- Pages: 1 -->\n",
       "<svg width=\"248pt\" height=\"175pt\"\n",
       " viewBox=\"0.00 0.00 248.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",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-171 244,-171 244,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"99\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"121\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"137\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"97\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"30,-8 30,-123 232,-123 232,-8 30,-8\"/>\n",
536
537
538
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
539
540
541
542
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
543
544
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
545
546
547
548
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-42C4.178,-42 17.9448,-42 30.9241,-42\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-42 30.9808,-45.1501 34.4807,-42 30.9807,-42.0001 30.9807,-42.0001 30.9807,-42.0001 34.4807,-42 30.9807,-38.8501 37.9807,-42 37.9807,-42\"/>\n",
549
550
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
551
552
553
554
555
556
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-59.0373C48.3189,-68.8579 50.4453,-78 56,-78 60.166,-78 62.4036,-72.8576 62.7128,-66.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-59.0373 65.8541,-65.8818 62.5434,-62.5335 62.7076,-66.0296 62.7076,-66.0296 62.7076,-66.0296 62.5434,-62.5335 59.561,-66.1774 62.3792,-59.0373 62.3792,-59.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"48\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
557
558
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
559
560
561
562
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"206\" cy=\"-49\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"206\" y=\"-45.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
563
564
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
565
566
567
568
569
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0935,-42.8444C100.6718,-44.0847 150.3801,-46.4044 180.604,-47.8149\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"187.8423,-48.1526 180.7031,-50.9728 184.3461,-47.9894 180.8499,-47.8262 180.8499,-47.8262 180.8499,-47.8262 184.3461,-47.9894 180.9968,-44.6797 187.8423,-48.1526 187.8423,-48.1526\"/>\n",
       "<text text-anchor=\"start\" x=\"113\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
570
571
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
572
573
574
575
576
577
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M188.7765,-54.9405C169.6967,-60.7308 138.0513,-67.9887 111,-63 100.1617,-61.0012 88.696,-56.9606 79.0542,-52.9528\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"72.3909,-50.0699 80.0663,-49.9585 75.6032,-51.4597 78.8154,-52.8495 78.8154,-52.8495 78.8154,-52.8495 75.6032,-51.4597 77.5646,-55.7405 72.3909,-50.0699 72.3909,-50.0699\"/>\n",
       "<text text-anchor=\"start\" x=\"111\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"123\" y=\"-67.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
578
579
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
580
581
582
583
584
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M199.6208,-66.0373C198.3189,-75.8579 200.4453,-85 206,-85 210.166,-85 212.4036,-79.8576 212.7128,-73.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"212.3792,-66.0373 215.8541,-72.8818 212.5434,-69.5335 212.7076,-73.0296 212.7076,-73.0296 212.7076,-73.0296 212.5434,-69.5335 209.561,-73.1774 212.3792,-66.0373 212.3792,-66.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"188\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
585
586
587
588
589
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
590
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c4120> >"
591
592
593
      ]
     },
     "execution_count": 5,
594
     "metadata": {},
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
     "output_type": "execute_result"
    }
   ],
   "source": [
    "strong = spot.decompose_scc(aut, 's'); strong"
   ]
  },
  {
   "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",
   "execution_count": 6,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
617
   "metadata": {},
618
   "outputs": [
619
    {
620
621
622
623
624
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
625
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
626
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
627
       "<!-- Pages: 1 -->\n",
628
629
630
       "<svg width=\"98pt\" height=\"193pt\"\n",
       " viewBox=\"0.00 0.00 98.00 193.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 189)\">\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
631
632
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-189 94,-189 94,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"24\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
633
       "<text text-anchor=\"start\" x=\"46\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
634
635
636
637
638
       "<text text-anchor=\"start\" x=\"62\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"22\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"30,-8 30,-141 82,-141 82,-8 30,-8\"/>\n",
639
640
641
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
642
643
644
645
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" 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\" fill=\"#000000\">0</text>\n",
646
647
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
648
649
650
651
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-34C4.178,-34 17.9448,-34 30.9241,-34\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-34 30.9808,-37.1501 34.4807,-34 30.9807,-34.0001 30.9807,-34.0001 30.9807,-34.0001 34.4807,-34 30.9807,-30.8501 37.9807,-34 37.9807,-34\"/>\n",
652
653
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
655
656
657
658
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" 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=\"#000000\" stroke=\"#000000\" 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=\"36\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
659
660
661
       "<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
662
663
664
665
666
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M50.9906,-51.5771C47.5451,-72.718 49.2148,-100 56,-100 62.043,-100 64.0285,-78.3596 61.9564,-58.6907\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.0094,-51.5771 65.0556,-58.1002 61.4713,-55.0465 61.9332,-58.5159 61.9332,-58.5159 61.9332,-58.5159 61.4713,-55.0465 58.8107,-58.9316 61.0094,-51.5771 61.0094,-51.5771\"/>\n",
       "<text text-anchor=\"start\" x=\"38\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
667
668
669
670
671
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
672
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d8571690> >"
673
674
675
      ]
     },
     "execution_count": 6,
676
     "metadata": {},
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
     "output_type": "execute_result"
    }
   ],
   "source": [
    "strong.postprocess('small')"
   ]
  },
  {
   "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",
   "execution_count": 7,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
696
   "metadata": {},
697
   "outputs": [
698
    {
699
700
701
702
703
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
704
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
705
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
       "<!-- Title: option: sw Pages: 1 -->\n",
       "<svg width=\"309pt\" height=\"297pt\"\n",
       " viewBox=\"0.00 0.00 309.00 297.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 293)\">\n",
       "<title>option: sw</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-293 305,-293 305,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"117\" y=\"-274.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">option: sw</text>\n",
       "<text text-anchor=\"start\" x=\"129.5\" y=\"-260.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"151.5\" y=\"-260.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"167.5\" y=\"-260.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"127.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"166,-8 166,-108 218,-108 218,-8 166,-8\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"30,-116 30,-231 293,-231 293,-116 30,-116\"/>\n",
724
725
726
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
727
728
729
730
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" 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\" fill=\"#000000\">0</text>\n",
731
732
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
733
734
735
736
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-142C4.178,-142 17.9448,-142 30.9241,-142\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-142 30.9808,-145.1501 34.4807,-142 30.9807,-142.0001 30.9807,-142.0001 30.9807,-142.0001 34.4807,-142 30.9807,-138.8501 37.9807,-142 37.9807,-142\"/>\n",
737
738
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
739
740
741
742
743
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-159.0373C48.3189,-168.8579 50.4453,-178 56,-178 60.166,-178 62.4036,-172.8576 62.7128,-166.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-159.0373 65.8541,-165.8818 62.5434,-162.5335 62.7076,-166.0296 62.7076,-166.0296 62.7076,-166.0296 62.5434,-162.5335 59.561,-166.1774 62.3792,-159.0373 62.3792,-159.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
744
745
746
       "<text text-anchor=\"start\" x=\"48\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
747
748
749
750
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"192\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"192\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
751
752
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
753
754
755
756
757
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M70.2973,-130.6462C94.7464,-111.2308 144.6248,-71.6215 172.3348,-49.6165\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"177.8942,-45.2016 174.3714,-52.0217 175.1533,-47.3782 172.4124,-49.5549 172.4124,-49.5549 172.4124,-49.5549 175.1533,-47.3782 170.4535,-47.088 177.8942,-45.2016 177.8942,-45.2016\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-116.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
758
759
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
760
761
762
763
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"267\" cy=\"-157\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"267\" y=\"-153.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
764
765
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
766
767
768
769
770
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M73.9897,-143.2789C111.5793,-145.9511 198.5319,-152.1326 241.7184,-155.2027\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"248.7561,-155.703 241.5503,-158.3486 245.2649,-155.4548 241.7737,-155.2066 241.7737,-155.2066 241.7737,-155.2066 245.2649,-155.4548 241.9971,-152.0645 248.7561,-155.703 248.7561,-155.703\"/>\n",
       "<text text-anchor=\"start\" x=\"174\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
771
772
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
773
774
775
776
777
778
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.2664,-51.0373C183.8922,-60.8579 186.1367,-70 192,-70 196.3975,-70 198.7594,-64.8576 199.0858,-58.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"198.7336,-51.0373 202.2263,-57.8728 198.9069,-54.533 199.0802,-58.0287 199.0802,-58.0287 199.0802,-58.0287 198.9069,-54.533 195.934,-58.1847 198.7336,-51.0373 198.7336,-51.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"187.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
779
780
       "</g>\n",
       "<!-- 2&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
781
782
783
784
785
786
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M250.0177,-163.1143C240.7005,-166.1461 228.8647,-169.4783 218,-171 168.544,-177.9266 111.1056,-161.8772 79.6376,-150.9963\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"72.9582,-148.6284 80.6084,-147.9985 76.257,-149.7979 79.5559,-150.9674 79.5559,-150.9674 79.5559,-150.9674 76.257,-149.7979 78.5033,-153.9364 72.9582,-148.6284 72.9582,-148.6284\"/>\n",
       "<text text-anchor=\"start\" x=\"172\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-175.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
787
788
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
789
790
791
792
793
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M260.6208,-174.0373C259.3189,-183.8579 261.4453,-193 267,-193 271.166,-193 273.4036,-187.8576 273.7128,-181.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"273.3792,-174.0373 276.8541,-180.8818 273.5434,-177.5335 273.7076,-181.0296 273.7076,-181.0296 273.7076,-181.0296 273.5434,-177.5335 270.561,-181.1774 273.3792,-174.0373 273.3792,-174.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"249\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
794
795
796
797
798
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
799
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d8571360> >"
800
801
      ]
     },
802
     "metadata": {},
803
     "output_type": "display_data"
804
805
    },
    {
806
807
808
809
810
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
811
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
812
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
       "<!-- Title: option: st Pages: 1 -->\n",
       "<svg width=\"435pt\" height=\"201pt\"\n",
       " viewBox=\"0.00 0.00 435.00 201.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 197)\">\n",
       "<title>option: st</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-197 431,-197 431,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"183\" y=\"-178.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">option: st</text>\n",
       "<text text-anchor=\"start\" x=\"192.5\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"214.5\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"230.5\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"190.5\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"367,-20 367,-120 419,-120 419,-20 367,-20\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"284,-20 284,-105 336,-105 336,-20 284,-20\"/>\n",
       "</g>\n",
       "<g id=\"clust3\" class=\"cluster\">\n",
       "<title>cluster_2</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"30,-20 30,-135 232,-135 232,-20 30,-20\"/>\n",
835
836
837
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
838
839
840
841
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
842
843
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
844
845
846
847
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-46C4.178,-46 17.9448,-46 30.9241,-46\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-46 30.9808,-49.1501 34.4807,-46 30.9807,-46.0001 30.9807,-46.0001 30.9807,-46.0001 34.4807,-46 30.9807,-42.8501 37.9807,-46 37.9807,-46\"/>\n",
848
849
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
850
851
852
853
854
855
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-63.0373C48.3189,-72.8579 50.4453,-82 56,-82 60.166,-82 62.4036,-76.8576 62.7128,-70.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-63.0373 65.8541,-69.8818 62.5434,-66.5335 62.7076,-70.0296 62.7076,-70.0296 62.7076,-70.0296 62.5434,-66.5335 59.561,-70.1774 62.3792,-63.0373 62.3792,-63.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"48\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
856
857
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
858
859
860
861
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"393\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"393\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
862
863
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
864
865
866
867
868
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M68.1391,-32.6949C81.9254,-19.1093 105.7965,0 131,0 131,0 131,0 310,0 334.5036,0 358.5513,-15.5275 374.4016,-28.5397\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"379.8559,-33.1864 372.4846,-31.0447 377.1916,-30.9167 374.5274,-28.6469 374.5274,-28.6469 374.5274,-28.6469 377.1916,-30.9167 376.5702,-26.249 379.8559,-33.1864 379.8559,-33.1864\"/>\n",
       "<text text-anchor=\"start\" x=\"202.5\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
869
870
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
871
872
873
874
       "<g id=\"node5\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"206\" cy=\"-64\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"206\" y=\"-60.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
875
876
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
877
878
879
880
881
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0935,-48.1712C100.6718,-51.3606 150.3801,-57.3256 180.604,-60.9525\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"187.8423,-61.8211 180.5168,-64.1145 184.3673,-61.404 180.8922,-60.987 180.8922,-60.987 180.8922,-60.987 184.3673,-61.404 181.2675,-57.8594 187.8423,-61.8211 187.8423,-61.8211\"/>\n",
       "<text text-anchor=\"start\" x=\"113\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
882
883
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
884
885
886
887
888
889
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M385.9688,-62.6641C384.4063,-72.625 386.75,-82 393,-82 397.6875,-82 400.1777,-76.7266 400.4707,-69.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"400.0313,-62.6641 403.6006,-69.4598 400.2438,-66.1576 400.4564,-69.6511 400.4564,-69.6511 400.4564,-69.6511 400.2438,-66.1576 397.3122,-69.8425 400.0313,-62.6641 400.0313,-62.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"388.5\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "<text text-anchor=\"start\" x=\"385\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
890
891
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
892
893
894
895
       "<g id=\"node4\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"310\" cy=\"-46\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"310\" y=\"-42.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
896
897
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
898
899
900
901
902
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M328.0098,-46C339.5679,-46 354.7507,-46 367.5345,-46\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"374.7388,-46 367.7388,-49.1501 371.2388,-46 367.7388,-46.0001 367.7388,-46.0001 367.7388,-46.0001 371.2388,-46 367.7387,-42.8501 374.7388,-46 374.7388,-46\"/>\n",
       "<text text-anchor=\"start\" x=\"346\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
903
904
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905
906
907
908
909
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M302.9688,-62.6641C301.4063,-72.625 303.75,-82 310,-82 314.6875,-82 317.1777,-76.7266 317.4707,-69.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"317.0313,-62.6641 320.6006,-69.4598 317.2438,-66.1576 317.4564,-69.6511 317.4564,-69.6511 317.4564,-69.6511 317.2438,-66.1576 314.3122,-69.8425 317.0313,-62.6641 317.0313,-62.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"306.5\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
910
911
       "</g>\n",
       "<!-- 2&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
912
913
914
915
916
917
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M188.6028,-69.6765C169.3709,-75.1094 137.593,-81.5815 111,-75 99.138,-72.0643 87.012,-66.0542 77.175,-60.2629\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"71.067,-56.5232 78.6818,-57.4919 74.052,-58.3508 77.037,-60.1784 77.037,-60.1784 77.037,-60.1784 74.052,-58.3508 75.3921,-62.8648 71.067,-56.5232 71.067,-56.5232\"/>\n",
       "<text text-anchor=\"start\" x=\"111\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
       "<text text-anchor=\"start\" x=\"123\" y=\"-80.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
918
919
       "</g>\n",
       "<!-- 2&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
920
921
922
923
924
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M219.9572,-75.6937C244.0872,-94.4071 294.9593,-127.2135 336,-109 354.8745,-100.6237 370.1522,-82.5674 380.1221,-67.9237\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"384.0651,-61.895 382.8698,-69.4775 382.1493,-64.8242 380.2336,-67.7533 380.2336,-67.7533 380.2336,-67.7533 382.1493,-64.8242 377.5973,-66.0292 384.0651,-61.895 384.0651,-61.895\"/>\n",
       "<text text-anchor=\"start\" x=\"292\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
925
926
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
927
928
929
930
931
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M224.1154,-60.8646C240.967,-57.948 266.2278,-53.576 284.9961,-50.3276\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"292.0922,-49.0994 285.732,-53.3972 288.6434,-49.6964 285.1947,-50.2933 285.1947,-50.2933 285.1947,-50.2933 288.6434,-49.6964 284.6575,-47.1894 292.0922,-49.0994 292.0922,-49.0994\"/>\n",
       "<text text-anchor=\"start\" x=\"242\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
932
933
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
934
935
936
937
938
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M199.6208,-81.0373C198.3189,-90.8579 200.4453,-100 206,-100 210.166,-100 212.4036,-94.8576 212.7128,-88.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"212.3792,-81.0373 215.8541,-87.8818 212.5434,-84.5335 212.7076,-88.0296 212.7076,-88.0296 212.7076,-88.0296 212.5434,-84.5335 209.561,-88.1774 212.3792,-81.0373 212.3792,-81.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"188\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
939
940
941
942
943
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
944
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d860a240> >"
945
946
      ]
     },
947
     "metadata": {},
948
     "output_type": "display_data"
949
950
    },
    {
951
952
953
954
955
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
956
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
957
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
       "<!-- Title: option: wt Pages: 1 -->\n",
       "<svg width=\"496pt\" height=\"315pt\"\n",
       " viewBox=\"0.00 0.00 496.00 315.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 311)\">\n",
       "<title>option: wt</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-311 492,-311 492,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"210.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">option: wt</text>\n",
       "<text text-anchor=\"start\" x=\"223\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"245\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"261\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"221\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"428,-148 428,-248 480,-248 480,-148 428,-148\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"166,-8 166,-108 218,-108 218,-8 166,-8\"/>\n",
       "</g>\n",
       "<g id=\"clust3\" class=\"cluster\">\n",
       "<title>cluster_2</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"345,-148 345,-233 397,-233 397,-148 345,-148\"/>\n",
       "</g>\n",
       "<g id=\"clust4\" class=\"cluster\">\n",
       "<title>cluster_3</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"30,-148 30,-248 293,-248 293,-148 30,-148\"/>\n",
984
985
986
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
987
988
989
990
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
991
992
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
993
994
995
996
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-174C4.178,-174 17.9448,-174 30.9241,-174\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-174 30.9808,-177.1501 34.4807,-174 30.9807,-174.0001 30.9807,-174.0001 30.9807,-174.0001 34.4807,-174 30.9807,-170.8501 37.9807,-174 37.9807,-174\"/>\n",
997
998
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
999
1000
1001
1002
1003
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-191.0373C48.3189,-200.8579 50.4453,-210 56,-210 60.166,-210 62.4036,-204.8576 62.7128,-198.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-191.0373 65.8541,-197.8818 62.5434,-194.5335 62.7076,-198.0296 62.7076,-198.0296 62.7076,-198.0296 62.5434,-194.5335 59.561,-198.1774 62.3792,-191.0373 62.3792,-191.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"36\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1004
1005
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1006
1007
1008
1009
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"454\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"454\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
1010
1011
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1012
1013
1014
1015
1016
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M71.7423,-164.9119C96.4901,-151.5061 146.387,-128 192,-128 192,-128 192,-128 371,-128 395.5036,-128 419.5513,-143.5275 435.4016,-156.5397\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"440.8559,-161.1864 433.4846,-159.0447 438.1916,-158.9167 435.5274,-156.6469 435.5274,-156.6469 435.5274,-156.6469 438.1916,-158.9167 437.5702,-154.249 440.8559,-161.1864 440.8559,-161.1864\"/>\n",
       "<text text-anchor=\"start\" x=\"263.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
1017
1018
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1019
1020
1021
1022
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"192\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"192\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
1023
1024
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1025
1026
1027
1028
1029
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M61.2718,-156.6681C66.8826,-140.3827 77.0314,-116.0332 92,-99 113.6775,-74.3325 146.8751,-55.2821 168.9997,-44.3562\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"175.4855,-41.2291 170.5482,-47.1067 172.3328,-42.7492 169.1801,-44.2693 169.1801,-44.2693 169.1801,-44.2693 172.3328,-42.7492 167.812,-41.4319 175.4855,-41.2291 175.4855,-41.2291\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
1030
1031
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1032
1033
1034
1035
       "<g id=\"node6\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"267\" cy=\"-184\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"267\" y=\"-180.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
1036
1037
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1038
1039
1040
1041
1042
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>0&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M73.9897,-174.8526C111.5793,-176.6341 198.5319,-180.7551 241.7184,-182.8018\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"248.7561,-183.1354 241.6148,-185.9504 245.26,-182.9696 241.7639,-182.8039 241.7639,-182.8039 241.7639,-182.8039 245.26,-182.9696 241.9131,-179.6574 248.7561,-183.1354 248.7561,-183.1354\"/>\n",
       "<text text-anchor=\"start\" x=\"174\" y=\"-184.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
1043
1044
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1045
1046
1047
1048
1049
1050
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M446.9688,-190.6641C445.4063,-200.625 447.75,-210 454,-210 458.6875,-210 461.1777,-204.7266 461.4707,-197.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"461.0313,-190.6641 464.6006,-197.4598 461.2438,-194.1576 461.4564,-197.6511 461.4564,-197.6511 461.4564,-197.6511 461.2438,-194.1576 458.3122,-197.8425 461.0313,-190.6641 461.0313,-190.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"449.5\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "<text text-anchor=\"start\" x=\"446\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
1051
1052
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1053
1054
1055
1056
1057
1058
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.2664,-51.0373C183.8922,-60.8579 186.1367,-70 192,-70 196.3975,-70 198.7594,-64.8576 199.0858,-58.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"198.7336,-51.0373 202.2263,-57.8728 198.9069,-54.533 199.0802,-58.0287 199.0802,-58.0287 199.0802,-58.0287 198.9069,-54.533 195.934,-58.1847 198.7336,-51.0373 198.7336,-51.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"187.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
       "<text text-anchor=\"start\" x=\"184\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
1059
1060
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1061
1062
1063
1064
       "<g id=\"node5\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"371\" cy=\"-174\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"371\" y=\"-170.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
1065
1066
       "</g>\n",
       "<!-- 4&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1067
1068
1069
1070
1071
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>4&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M389.0098,-174C400.5679,-174 415.7507,-174 428.5345,-174\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"435.7388,-174 428.7388,-177.1501 432.2388,-174 428.7388,-174.0001 428.7388,-174.0001 428.7388,-174.0001 432.2388,-174 428.7387,-170.8501 435.7388,-174 435.7388,-174\"/>\n",
       "<text text-anchor=\"start\" x=\"407\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
1072
1073
       "</g>\n",
       "<!-- 4&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1074
1075
1076
1077
1078
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>4&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M363.9688,-190.6641C362.4063,-200.625 364.75,-210 371,-210 375.6875,-210 378.1777,-204.7266 378.4707,-197.8876\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"378.0313,-190.6641 381.6006,-197.4598 378.2438,-194.1576 378.4564,-197.6511 378.4564,-197.6511 378.4564,-197.6511 378.2438,-194.1576 375.3122,-197.8425 378.0313,-190.6641 378.0313,-190.6641\"/>\n",
       "<text text-anchor=\"start\" x=\"367.5\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
1079
1080
       "</g>\n",
       "<!-- 3&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1081
1082
1083
1084
1085
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>3&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M250.0928,-190.9839C240.7976,-194.4477 228.9588,-198.2561 218,-200 168.8323,-207.8241 111.2885,-192.8451 79.7247,-182.5531\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"73.0238,-180.3102 80.6617,-179.545 76.3428,-181.4212 79.6619,-182.5321 79.6619,-182.5321 79.6619,-182.5321 76.3428,-181.4212 78.662,-185.5192 73.0238,-180.3102 73.0238,-180.3102\"/>\n",
       "<text text-anchor=\"start\" x=\"172\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1086
1087
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1088
1089
1090
1091
1092
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M280.0266,-196.4976C303.5652,-217.4912 354.6722,-255.7847 397,-237 415.8745,-228.6237 431.1522,-210.5674 441.1221,-195.9237\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"445.0651,-189.895 443.8698,-197.4775 443.1493,-192.8242 441.2336,-195.7533 441.2336,-195.7533 441.2336,-195.7533 443.1493,-192.8242 438.5973,-194.0292 445.0651,-189.895 445.0651,-189.895\"/>\n",
       "<text text-anchor=\"start\" x=\"353\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
1093
1094
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1095
1096
1097
1098
1099
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>3&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M285.1154,-182.2581C301.8642,-180.6477 326.92,-178.2385 345.6521,-176.4373\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"352.7432,-175.7555 346.0769,-179.5611 349.2593,-176.0905 345.7754,-176.4255 345.7754,-176.4255 345.7754,-176.4255 349.2593,-176.0905 345.4738,-173.29 352.7432,-175.7555 352.7432,-175.7555\"/>\n",
       "<text text-anchor=\"start\" x=\"303\" y=\"-183.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
1100
1101
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1102
1103
1104
1105
1106
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M260.6208,-201.0373C259.3189,-210.8579 261.4453,-220 267,-220 271.166,-220 273.4036,-214.8576 273.7128,-208.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"273.3792,-201.0373 276.8541,-207.8818 273.5434,-204.5335 273.7076,-208.0296 273.7076,-208.0296 273.7076,-208.0296 273.5434,-204.5335 270.561,-208.1774 273.3792,-201.0373 273.3792,-201.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"249\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
1107
1108
1109
1110
1111
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
1112
       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d862fed0> >"
1113
1114
      ]
     },
1115
     "metadata": {},
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
     "output_type": "display_data"
    }
   ],
   "source": [
    "for opt in ('sw', 'st', 'wt'):\n",
    "    a = spot.decompose_scc(aut, opt)\n",
    "    a.set_name(\"option: \" + opt)\n",
    "    display(a)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Generalized acceptance\n",
    "\n",
    "There is nothing that prevents the above decomposition to work with other types of acceptance.\n",
    "\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",
   "execution_count": 8,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1146
   "metadata": {},
1147
   "outputs": [
1148
    {
1149
1150
1151
1152
1153
     "data": {
      "image/svg+xml": [
       "<?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",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1154
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
1155
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
       "<!-- Pages: 1 -->\n",
       "<svg width=\"658pt\" height=\"360pt\"\n",
       " viewBox=\"0.00 0.00 657.76 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(.5302 .5302) rotate(0) translate(4 675)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-675 1236.6072,-675 1236.6072,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"499.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">(Fin(</text>\n",
       "<text text-anchor=\"start\" x=\"527.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"543.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">) &amp; Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"586.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
       "<text text-anchor=\"start\" x=\"602.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)) | (Fin(</text>\n",
       "<text text-anchor=\"start\" x=\"649.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
       "<text text-anchor=\"start\" x=\"665.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">) &amp; Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"708.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
       "<text text-anchor=\"start\" x=\"724.8036\" y=\"-656.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">))</text>\n",
       "<text text-anchor=\"start\" x=\"587.3036\" y=\"-642.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Rabin 2]</text>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_0</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"1140.725,-272 1140.725,-389 1224.6072,-389 1224.6072,-272 1140.725,-272\"/>\n",
       "</g>\n",
       "<g id=\"clust2\" class=\"cluster\">\n",
       "<title>cluster_1</title>\n",
       "<polygon fill=\"none\" stroke=\"#ff0000\" points=\"1039.9848,-215 1039.9848,-318 1109.725,-318 1109.725,-215 1039.9848,-215\"/>\n",
       "</g>\n",
       "<g id=\"clust3\" class=\"cluster\">\n",
       "<title>cluster_2</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"888.2447,-20 888.2447,-123 957.9848,-123 957.9848,-20 888.2447,-20\"/>\n",
       "</g>\n",
       "<g id=\"clust4\" class=\"cluster\">\n",
       "<title>cluster_3</title>\n",
       "<polygon fill=\"none\" stroke=\"#00ff00\" points=\"355.6224,-277 355.6224,-445 957.9848,-445 957.9848,-277 355.6224,-277\"/>\n",
       "</g>\n",
       "<g id=\"clust5\" class=\"cluster\">\n",
       "<title>cluster_4</title>\n",
       "<polygon fill=\"none\" stroke=\"#000000\" points=\"185.7401,-469 185.7401,-553 269.6224,-553 269.6224,-469 185.7401,-469\"/>\n",
       "</g>\n",
       "<g id=\"clust6\" class=\"cluster\">\n",
       "<title>cluster_5</title>\n",
       "<polygon fill=\"none\" stroke=\"#000000\" points=\"185.7401,-177 185.7401,-261 269.6224,-261 269.6224,-177 185.7401,-177\"/>\n",
       "</g>\n",
       "<g id=\"clust7\" class=\"cluster\">\n",
       "<title>cluster_6</title>\n",
       "<polygon fill=\"none\" stroke=\"#000000\" points=\"30,-437 30,-507 99.7401,-507 99.7401,-437 30,-437\"/>\n",
1198
1199
1200
       "</g>\n",
       "<!-- I -->\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1201
1202
1203
1204
1205
       "<g id=\"node2\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"64.8701\" cy=\"-472\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"60.3701\" y=\"-475.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
       "<text text-anchor=\"start\" x=\"56.8701\" y=\"-460.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1206
1207
       "</g>\n",
       "<!-- I&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1208
1209
1210
1211
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.2229,-472C4.3751,-472 17.3629,-472 30.7917,-472\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.8045,-472 30.8046,-475.1501 34.3045,-472 30.8045,-472.0001 30.8045,-472.0001 30.8045,-472.0001 34.3045,-472 30.8045,-468.8501 37.8045,-472 37.8045,-472\"/>\n",
1212
1213
       "</g>\n",
       "<!-- 6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1214
1215
1216
1217
1218
1219
       "<g id=\"node3\" class=\"node\">\n",
       "<title>6</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1182.6661\" cy=\"-314\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
       "<text text-anchor=\"start\" x=\"1178.1661\" y=\"-317.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">6</text>\n",
       "<text text-anchor=\"start\" x=\"1166.6661\" y=\"-303.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
       "<text text-anchor=\"start\" x=\"1182.6661\" y=\"-303.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1220
1221
       "</g>\n",
       "<!-- 2&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1222
1223
1224
1225
1226
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>2&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M77.0996,-496.1081C100.288,-538.0457 154.9122,-620 227.6812,-620 227.6812,-620 227.6812,-620 1074.8549,-620 1130.4065,-620 1164.358,-438.3314 1177.0154,-354.9498\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1178.0678,-347.9165 1180.1471,-355.3057 1177.5498,-351.378 1177.0318,-354.8394 1177.0318,-354.8394 1177.0318,-354.8394 1177.5498,-351.378 1173.9165,-354.3732 1178.0678,-347.9165 1178.0678,-347.9165\"/>\n",
       "<text text-anchor=\"start\" x=\"687.8036\" y=\"-623.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
1227
1228
       "</g>\n",
       "<!-- 5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1229
1230
1231
1232
1233
1234
       "<g id=\"node7\" class=\"node\">\n",
       "<title>5</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"691.3036\" cy=\"-370\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
       "<text text-anchor=\"start\" x=\"686.8036\" y=\"-373.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
       "<text text-anchor=\"start\" x=\"675.3036\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
       "<text text-anchor=\"start\" x=\"691.3036\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1235
1236
       "</g>\n",
       "<!-- 2&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1237
1238
1239
1240
1241
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>2&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M91.696,-469.1165C166.0462,-461.0797 381.0316,-437.5356 559.3625,-415 594.9694,-410.5004 605.7493,-416.5799 639.3625,-404 645.6633,-401.6419 651.9796,-398.4122 657.9292,-394.8763\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"664.2232,-390.946 659.9542,-397.3256 661.2544,-392.7999 658.2857,-394.6537 658.2857,-394.6537 658.2857,-394.6537 661.2544,-392.7999 656.6172,-391.9819 664.2232,-390.946 664.2232,-390.946\"/>\n",
       "<text text-anchor=\"start\" x=\"370.4924\" y=\"-442.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1242
1243
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1244
1245
1246
1247
1248
1249
       "<g id=\"node9\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"227.6812\" cy=\"-511\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
       "<text text-anchor=\"start\" x=\"223.1812\" y=\"-514.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
       "<text text-anchor=\"start\" x=\"211.6812\" y=\"-500.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
       "<text text-anchor=\"start\" x=\"227.6812\" y=\"-500.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1250
1251
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1252
1253
1254
1255
1256
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M91.0285,-478.266C117.0755,-484.5053 157.4103,-494.1672 187.5174,-501.3791\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"194.5485,-503.0633 187.0072,-504.4959 191.1448,-502.248 187.741,-501.4326 187.741,-501.4326 187.741,-501.4326 191.1448,-502.248 188.4749,-498.3693 194.5485,-503.0633 194.5485,-503.0633\"/>\n",
       "<text text-anchor=\"start\" x=\"109.7401\" y=\"-501.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b &amp; !c</text>\n",
1257
1258
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1259
1260
1261
1262
1263
1264
       "<g id=\"node10\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"227.6812\" cy=\"-219\" rx=\"33.8824\" ry=\"33.8824\"/>\n",
       "<text text-anchor=\"start\" x=\"223.1812\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
       "<text text-anchor=\"start\" x=\"211.6812\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
       "<text text-anchor=\"start\" x=\"227.6812\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1265
1266
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1267
1268
1269
1270
1271
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M79.6056,-449.1017C108.1887,-404.6851 171.3195,-306.5832 205.1807,-253.9646\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"209.1608,-247.7798 208.0216,-255.371 207.2667,-250.7231 205.3727,-253.6663 205.3727,-253.6663 205.3727,-253.6663 207.2667,-250.7231 202.7237,-251.9617 209.1608,-247.7798 209.1608,-247.7798\"/>\n",
       "<text text-anchor=\"start\" x=\"111.7401\" y=\"-400.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
1272
1273
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1274
1275
1276
1277
1278
       "<g id=\"edge26\" class=\"edge\">\n",
       "<title>6&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1172.1661,-346.4632C1172.1661,-357.2843 1175.6661,-365.9411 1182.6661,-365.9411 1188.0255,-365.9411 1191.3332,-360.8666 1192.5893,-353.6315\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1193.1661,-346.4632 1195.7444,-353.6933 1192.8853,-349.9519 1192.6046,-353.4407 1192.6046,-353.4407 1192.6046,-353.4407 1192.8853,-349.9519 1189.4647,-353.188 1193.1661,-346.4632 1193.1661,-346.4632\"/>\n",
       "<text text-anchor=\"middle\" x=\"1182.6661\" y=\"-369.7411\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
1279
1280
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1281
1282
1283
1284
1285
       "<g id=\"node4\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1074.8549\" cy=\"-250\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"1070.3549\" y=\"-253.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "<text text-anchor=\"start\" x=\"1066.8549\" y=\"-238.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1286
1287
       "</g>\n",
       "<!-- 1&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1288
1289
1290
1291
1292
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>1&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1097.9831,-263.7296C1112.2939,-272.2249 1130.9569,-283.3039 1147.1194,-292.8984\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1153.4075,-296.6312 1145.7802,-295.7666 1150.3979,-294.8446 1147.3882,-293.0579 1147.3882,-293.0579 1147.3882,-293.0579 1150.3979,-294.8446 1148.9962,-290.3492 1153.4075,-296.6312 1153.4075,-296.6312\"/>\n",
       "<text text-anchor=\"start\" x=\"1119.725\" y=\"-285.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
1293
1294
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1295
1296
1297
1298
1299
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1065.5623,-275.37C1064.9214,-285.9238 1068.019,-294.8701 1074.8549,-294.8701 1080.0887,-294.8701 1083.1311,-289.6259 1083.982,-282.4312\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1084.1475,-275.37 1087.1326,-282.4419 1084.0655,-278.869 1083.9834,-282.3681 1083.9834,-282.3681 1083.9834,-282.3681 1084.0655,-278.869 1080.8343,-282.2943 1084.1475,-275.37 1084.1475,-275.37\"/>\n",
       "<text text-anchor=\"start\" x=\"1071.3549\" y=\"-298.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
1300
1301
       "</g>\n",
       "<!-- 8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1302
1303
1304
1305
1306
       "<g id=\"node5\" class=\"node\">\n",
       "<title>8</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"923.1148\" cy=\"-55\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"918.6148\" y=\"-58.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">8</text>\n",
       "<text text-anchor=\"start\" x=\"915.1148\" y=\"-43.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
1307
1308
       "</g>\n",
       "<!-- 8&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1309
1310
1311
1312
1313
       "<g id=\"edge34\" class=\"edge\">\n",
       "<title>8&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M950.3154,-56.3267C972.7236,-58.3389 1004.794,-63.3829 1029.9848,-76 1083.9322,-103.0201 1097.2618,-116.7942 1130.725,-167 1152.5666,-199.7697 1166.3589,-242.7737 1174.1962,-273.7936\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1175.8732,-280.6165 1171.1434,-274.5707 1175.0377,-277.2177 1174.2023,-273.8188 1174.2023,-273.8188 1174.2023,-273.8188 1175.0377,-277.2177 1177.2613,-273.067 1175.8732,-280.6165 1175.8732,-280.6165\"/>\n",
       "<text text-anchor=\"start\" x=\"1069.3549\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
1314
1315
       "</g>\n",
       "<!-- 8&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1316
1317
1318
1319
1320
       "<g id=\"edge33\" class=\"edge\">\n",
       "<title>8&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M947.1733,-67.0983C976.8427,-82.198 1024.0986,-106.9046 1029.9848,-114 1054.2778,-143.2833 1065.561,-186.1548 1070.7075,-215.9051\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1071.8879,-223.1697 1067.6559,-216.7656 1071.3265,-219.715 1070.7651,-216.2603 1070.7651,-216.2603 1070.7651,-216.2603 1071.3265,-219.715 1073.8744,-215.7551 1071.8879,-223.1697 1071.8879,-223.1697\"/>\n",
       "<text text-anchor=\"start\" x=\"980.4848\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
1321
1322
       "</g>\n",
       "<!-- 8&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1323
1324
1325
1326
1327
       "<g id=\"edge35\" class=\"edge\">\n",
       "<title>8&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M914.9151,-80.8213C914.4519,-91.1776 917.1851,-99.8701 923.1148,-99.8701 927.5621,-99.8701 930.2113,-94.9805 931.0625,-88.1667\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"931.3144,-80.8213 934.2226,-87.9252 931.1944,-84.3193 931.0744,-87.8172 931.0744,-87.8172 931.0744,-87.8172 931.1944,-84.3193 927.9263,-87.7092 931.3144,-80.8213 931.3144,-80.8213\"/>\n",
       "<text text-anchor=\"start\" x=\"906.1148\" y=\"-103.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
1328
1329
       "</g>\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1330
1331
1332
1333
1334
       "<g id=\"node6\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"390.4924\" cy=\"-312\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"385.9924\" y=\"-315.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "<text text-anchor=\"start\" x=\"382.4924\" y=\"-300.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
1335
1336
       "</g>\n",
       "<!-- 0&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1337
1338
1339
1340
1341
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>0&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M401.9009,-287.6669C421.5449,-249.7827 465.58,-181 526.3625,-181 526.3625,-181 526.3625,-181 1074.8549,-181 1123.6052,-181 1154.1418,-235.5911 1169.7926,-274.8234\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1172.3601,-281.4645 1166.8978,-276.0713 1171.098,-278.2 1169.8359,-274.9355 1169.8359,-274.9355 1169.8359,-274.9355 1171.098,-278.2 1172.774,-273.7996 1172.3601,-281.4645 1172.3601,-281.4645\"/>\n",
       "<text text-anchor=\"start\" x=\"810.2447\" y=\"-184.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
1342
1343
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1344
1345
1346
1347
1348
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M416.979,-306.1612C423,-304.9808 429.3836,-303.8445 435.3625,-303 665.4293,-270.5033 945.0867,-255.7784 1040.8222,-251.4374\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1047.926,-251.1192 1041.074,-254.5794 1044.4295,-251.2759 1040.933,-251.4326 1040.933,-251.4326 1040.933,-251.4326 1044.4295,-251.2759 1040.7919,-248.2857 1047.926,-251.1192 1047.926,-251.1192\"/>\n",
       "<text text-anchor=\"start\" x=\"745.2447\" y=\"-273.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
1349
1350
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1351
1352
1353
1354
1355
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M378.6799,-336.4616C377.5549,-347.4053 381.4924,-356.8701 390.4924,-356.8701 397.383,-356.8701 401.3061,-351.322 402.2617,-343.8099\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"402.3049,-336.4616 405.4136,-343.4801 402.2843,-339.9616 402.2636,-343.4615 402.2636,-343.4615 402.2636,-343.4615 402.2843,-339.9616 399.1137,-343.4429 402.3049,-336.4616 402.3049,-336.4616\"/>\n",
       "<text text-anchor=\"start\" x=\"372.4924\" y=\"-360.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
1356
1357
       "</g>\n",
       "<!-- 0&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1358
1359
1360
1361
1362
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M415.9648,-321.6091C422.2623,-323.8388 429.0219,-326.11 435.3625,-328 509.19,-350.0061 598.6502,-361.3571 649.8747,-366.4662\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"657.1485,-367.1752 649.8759,-369.6311 653.665,-366.8356 650.1815,-366.496 650.1815,-366.496 650.1815,-366.496 653.665,-366.8356 650.4872,-363.3609 657.1485,-367.1752 657.1485,-367.1752\"/>\n",
       "<text text-anchor=\"start\" x=\"506.3625\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1363
1364
       "</g>\n",
       "<!-- 5&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1365
1366
1367
1368
1369
       "<g id=\"edge24\" class=\"edge\">\n",
       "<title>5&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M718.1657,-391.1334C744.6041,-409.7751 786.9123,-434 828.2447,-434 828.2447,-434 828.2447,-434 1074.8549,-434 1119.5444,-434 1150.4095,-387.3776 1167.3214,-352.2535\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1170.317,-345.8427 1170.2074,-353.5181 1168.8353,-349.0136 1167.3536,-352.1846 1167.3536,-352.1846 1167.3536,-352.1846 1168.8353,-349.0136 1164.4998,-350.851 1170.317,-345.8427 1170.317,-345.8427\"/>\n",
       "<text text-anchor=\"start\" x=\"919.6148\" y=\"-437.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c</text>\n",
1370
1371
       "</g>\n",
       "<!-- 5&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1372
1373
1374
1375
1376
       "<g id=\"edge22\" class=\"edge\">\n",
       "<title>5&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M659.9762,-356.4323C633.6526,-345.6806 594.7642,-331.2944 559.3625,-324 513.2714,-314.5031 458.7775,-312.1916 424.4211,-311.7923\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"417.4057,-311.7343 424.4316,-308.6424 420.9056,-311.7633 424.4055,-311.7923 424.4055,-311.7923 424.4055,-311.7923 420.9056,-311.7633 424.3794,-314.9422 417.4057,-311.7343 417.4057,-311.7343\"/>\n",
       "<text text-anchor=\"start\" x=\"493.3625\" y=\"-327.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b &amp; !c</text>\n",
1377
1378
       "</g>\n",
       "<!-- 5&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1379
1380
1381
1382
1383
       "<g id=\"edge23\" class=\"edge\">\n",
       "<title>5&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M678.5606,-401.6989C678.3567,-412.8737 682.6044,-421.9411 691.3036,-421.9411 697.9639,-421.9411 702.0149,-416.626 703.4564,-409.1193\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"704.0466,-401.6989 706.6316,-408.9266 703.769,-405.1878 703.4915,-408.6768 703.4915,-408.6768 703.4915,-408.6768 703.769,-405.1878 700.3514,-408.427 704.0466,-401.6989 704.0466,-401.6989\"/>\n",
       "<text text-anchor=\"start\" x=\"671.3036\" y=\"-425.7411\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1384
1385
       "</g>\n",
       "<!-- 7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1386
1387
1388
1389
1390
       "<g id=\"node8\" class=\"node\">\n",
       "<title>7</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"923.1148\" cy=\"-335\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"918.6148\" y=\"-338.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">7</text>\n",
       "<text text-anchor=\"start\" x=\"915.1148\" y=\"-323.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
1391
1392
       "</g>\n",
       "<!-- 5&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1393
1394
1395
1396
1397
       "<g id=\"edge25\" class=\"edge\">\n",
       "<title>5&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M725.483,-370.6777C759.7067,-370.6776 813.6881,-368.8255 859.2447,-359 870.1682,-356.6441 881.7141,-352.7655 891.9404,-348.8063\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"898.4502,-346.2081 893.1166,-351.7286 895.1995,-347.5055 891.9489,-348.803 891.9489,-348.803 891.9489,-348.803 895.1995,-347.5055 890.7812,-345.8774 898.4502,-346.2081 898.4502,-346.2081\"/>\n",
       "<text text-anchor=\"start\" x=\"797.2447\" y=\"-370.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
1398
1399
       "</g>\n",
       "<!-- 7&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1400
1401
1402
1403
1404
       "<g id=\"edge30\" class=\"edge\">\n",
       "<title>7&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M950.0311,-333.5082C986.3302,-331.4089 1052.9713,-327.246 1109.725,-322 1120.1348,-321.0378 1131.3659,-319.8704 1141.8221,-318.7283\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1148.9176,-317.9444 1142.3059,-321.8441 1145.4388,-318.3288 1141.9599,-318.7131 1141.9599,-318.7131 1141.9599,-318.7131 1145.4388,-318.3288 1141.614,-315.5822 1148.9176,-317.9444 1148.9176,-317.9444\"/>\n",
       "<text text-anchor=\"start\" x=\"1056.8549\" y=\"-330.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
1405
1406
       "</g>\n",
       "<!-- 7&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1407
1408
1409
1410
1411
       "<g id=\"edge28\" class=\"edge\">\n",
       "<title>7&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M946.9633,-322.018C968.6735,-310.1564 1001.5771,-292.0698 1029.9848,-276 1034.9438,-273.1948 1040.1928,-270.1878 1045.2856,-267.2501\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1051.6192,-263.5865 1047.1371,-269.8182 1048.5895,-265.339 1045.5598,-267.0915 1045.5598,-267.0915 1045.5598,-267.0915 1048.5895,-265.339 1043.9826,-264.3648 1051.6192,-263.5865 1051.6192,-263.5865\"/>\n",
       "<text text-anchor=\"start\" x=\"967.9848\" y=\"-312.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b &amp; c</text>\n",
1412
1413
       "</g>\n",
       "<!-- 7&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1414
1415
1416
1417
1418
       "<g id=\"edge32\" class=\"edge\">\n",
       "<title>7&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M923.1148,-307.8831C923.1148,-256.646 923.1148,-145.7094 923.1148,-89.3525\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"923.1148,-82.102 926.2649,-89.1019 923.1148,-85.602 923.1149,-89.102 923.1149,-89.102 923.1149,-89.102 923.1148,-85.602 919.9649,-89.102 923.1148,-82.102 923.1148,-82.102\"/>\n",
       "<text text-anchor=\"start\" x=\"883.6148\" y=\"-191.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; c</text>\n",
1419
1420
       "</g>\n",
       "<!-- 7&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1421
1422
1423
1424
1425
       "<g id=\"edge27\" class=\"edge\">\n",
       "<title>7&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M896.3082,-331.0239C858.3381,-325.5884 786.6703,-316.0515 725.2447,-312 614.4125,-304.6898 586.4319,-308.8889 475.3625,-308 457.5853,-307.8577 453.1227,-307.2099 435.3625,-308 431.8393,-308.1567 428.165,-308.3824 424.5023,-308.6477\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"417.5156,-309.1994 424.2459,-305.5081 421.0047,-308.9239 424.4939,-308.6483 424.4939,-308.6483 424.4939,-308.6483 421.0047,-308.9239 424.7419,-311.7885 417.5156,-309.1994 417.5156,-309.1994\"/>\n",
       "<text text-anchor=\"start\" x=\"658.3036\" y=\"-315.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b &amp; !c</text>\n",
1426
1427
       "</g>\n",
       "<!-- 7&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1428
1429
1430
1431
1432
       "<g id=\"edge29\" class=\"edge\">\n",
       "<title>7&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M895.9242,-334.2381C870.3074,-333.9541 830.9374,-334.6378 797.2447,-340 774.7849,-343.5745 750.3196,-350.306 730.5639,-356.4882\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"723.7834,-358.6459 729.4986,-353.5214 727.1186,-357.5845 730.4538,-356.5231 730.4538,-356.5231 730.4538,-356.5231 727.1186,-357.5845 731.4091,-359.5248 723.7834,-358.6459 723.7834,-358.6459\"/>\n",
       "<text text-anchor=\"start\" x=\"808.2447\" y=\"-343.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1433
1434
       "</g>\n",
       "<!-- 7&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1435
1436
1437
1438
1439
       "<g id=\"edge31\" class=\"edge\">\n",
       "<title>7&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M914.9151,-360.8213C914.4519,-371.1776 917.1851,-379.8701 923.1148,-379.8701 927.5621,-379.8701 930.2113,-374.9805 931.0625,-368.1667\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"931.3144,-360.8213 934.2226,-367.9252 931.1944,-364.3193 931.0744,-367.8172 931.0744,-367.8172 931.0744,-367.8172 931.1944,-364.3193 927.9263,-367.7092 931.3144,-360.8213 931.3144,-360.8213\"/>\n",
       "<text text-anchor=\"start\" x=\"892.1148\" y=\"-383.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b &amp; !c</text>\n",
1440
1441
       "</g>\n",
       "<!-- 3&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1442
1443
1444
1445
1446
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>3&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M256.391,-529.5613C287.9489,-548.1448 340.787,-574 390.4924,-574 390.4924,-574 390.4924,-574 1074.8549,-574 1121.7438,-574 1158.919,-427.8883 1174.5942,-354.7288\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1176.1326,-347.4582 1177.7652,-354.9587 1175.408,-350.8824 1174.6834,-354.3065 1174.6834,-354.3065 1174.6834,-354.3065 1175.408,-350.8824 1171.6017,-353.6544 1176.1326,-347.4582 1176.1326,-347.4582\"/>\n",
       "<text text-anchor=\"start\" x=\"743.2447\" y=\"-577.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; c</text>\n",
1447
1448
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1449
1450
1451
1452
1453
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M261.1108,-517.5451C267.2463,-518.5316 273.6106,-519.4138 279.6224,-520 492.7219,-540.7793 547.1345,-531 761.2447,-531 761.2447,-531 761.2447,-531 923.1148,-531 930.1785,-531 1022.2054,-352.8287 1059.4077,-280.2345\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1062.6225,-273.9579 1062.235,-281.6243 1061.0269,-277.0731 1059.4314,-280.1883 1059.4314,-280.1883 1059.4314,-280.1883 1061.0269,-277.0731 1056.6277,-278.7522 1062.6225,-273.9579 1062.6225,-273.9579\"/>\n",
       "<text text-anchor=\"start\" x=\"675.3036\" y=\"-534.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; c</text>\n",
1454
1455
       "</g>\n",
       "<!-- 3&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1456
1457
1458
1459
1460
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>3&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M249.3013,-484.5743C280.3378,-446.6392 337.2141,-377.1207 368.4714,-338.9157\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"373.2602,-333.0626 371.2656,-340.475 371.0439,-335.7715 368.8276,-338.4804 368.8276,-338.4804 368.8276,-338.4804 371.0439,-335.7715 366.3896,-336.4857 373.2602,-333.0626 373.2602,-333.0626\"/>\n",
       "<text text-anchor=\"start\" x=\"294.6224\" y=\"-449.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !c</text>\n",
1461
1462
       "</g>\n",
       "<!-- 3&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1463
1464
1465
1466
1467
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>3&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M261.7374,-509.3655C354.7689,-504.6452 608.3422,-489.9791 639.3625,-469 659.6732,-455.2638 672.5868,-430.9767 680.4579,-409.8967\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"682.8392,-403.1827 683.468,-410.833 681.6692,-406.4814 680.4992,-409.78 680.4992,-409.78 680.4992,-409.78 681.6692,-406.4814 677.5304,-408.727 682.8392,-403.1827 682.8392,-403.1827\"/>\n",
       "<text text-anchor=\"start\" x=\"435.3625\" y=\"-501.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !c</text>\n",
1468
1469
       "</g>\n",
       "<!-- 4&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1470
1471
1472
1473
1474
       "<g id=\"edge19\" class=\"edge\">\n",