ltsmin-dve.ipynb 133 KB
Newer Older
1
{
2
3
4
5
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
6
   "metadata": {},
7
8
9
10
11
12
13
   "outputs": [],
   "source": [
    "import spot\n",
    "import spot.ltsmin\n",
    "# The following line causes the notebook to exit with 77 if divine is not \n",
    "# installed, therefore skipping this test in the test suite.\n",
    "spot.ltsmin.require('divine')\n",
Clément Gillard's avatar
Clément Gillard committed
14
    "# This notebook also tests the limitation of the number of states in the GraphViz output\n",
15
16
    "spot.setup(max_states=10)"
   ]
17
  },
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are two ways to load a DiVinE model: from a file or from a cell.   \n",
    "\n",
    "Loading from a file\n",
    "-------------------\n",
    "\n",
    "We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
33
   "metadata": {},
34
35
36
37
   "outputs": [],
   "source": [
    "!rm -f test1.dve"
   ]
38
  },
39
  {
40
41
   "cell_type": "code",
   "execution_count": 3,
42
   "metadata": {},
43
   "outputs": [
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
44
    {
45
46
47
48
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Writing test1.dve\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
73
74
75
76
77
78
79
80
81
82
83
84
85
    }
   ],
   "source": [
    "%%file test1.dve\n",
    "int a = 0, b = 0;\n",
    "\n",
    "process P {\n",
    " state x;\n",
    " init x;\n",
    "\n",
    " trans\n",
    "   x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
    "   x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
    "}\n",
    "\n",
    "process Q {\n",
    "  state wait, work;\n",
    "  init wait;\n",
    "  trans\n",
    "    wait -> work { guard b > 1; },\n",
    "    work -> wait { guard a > 1; };\n",
    "}\n",
    "\n",
    "system async;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `spot.ltsmin.load` function compiles the model using the `ltlmin` interface and load it.  This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
86
   "metadata": {},
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
   "outputs": [],
   "source": [
    "m = spot.ltsmin.load('test1.dve')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Compiling the model creates all several kinds of files.  The `test1.dve` file is converted into a C++ source code `test1.dve.cpp` which is then compiled into a shared library `test1.dve2c`.  Becauce `spot.ltsmin.load()` has already loaded this shared library, all those files can be erased.  If you do not erase the files, `spot.ltsmin.load()` will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.\n",
    "\n",
    "For editing and loading DVE file from a notebook, it is a better to use the `%%dve` as shown next."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
104
   "metadata": {},
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
   "outputs": [],
   "source": [
    "!rm -f test1.dve test1.dve.cpp test1.dve2C"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Loading from a notebook cell\n",
    "----------------------------\n",
    "\n",
    "The `%%dve` cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files).  The variable name that should receive the model (here `m`) should be indicated on the first line, after `%dve`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
123
   "metadata": {},
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
   "outputs": [],
   "source": [
    "%%dve m\n",
    "int a = 0, b = 0;\n",
    "\n",
    "process P {\n",
    " state x;\n",
    " init x;\n",
    "\n",
    " trans\n",
    "   x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
    "   x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
    "}\n",
    "\n",
    "process Q {\n",
    "  state wait, work;\n",
    "  init wait;\n",
    "  trans\n",
    "    wait -> work { guard b > 1; },\n",
    "    work -> wait { guard a > 1; };\n",
    "}\n",
    "\n",
    "system async;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Working with an ltsmin model\n",
    "----------------------------\n",
    "\n",
    "Printing an ltsmin model shows some information about the variables it contains and their types, however the `info()` methods provide the data in a map that is easier to work with."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
162
   "metadata": {},
163
   "outputs": [
164
    {
165
166
167
168
169
170
171
172
173
174
     "data": {
      "text/plain": [
       "ltsmin model with the following variables:\n",
       "  a: int\n",
       "  b: int\n",
       "  P: ['x']\n",
       "  Q: ['wait', 'work']"
      ]
     },
     "execution_count": 7,
175
     "metadata": {},
176
177
178
179
180
181
182
183
184
185
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
186
   "metadata": {},
187
   "outputs": [
188
    {
189
190
191
192
193
194
195
196
     "data": {
      "text/plain": [
       "[('state_size', 4),\n",
       " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
       " ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
      ]
     },
     "execution_count": 8,
197
     "metadata": {},
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sorted(m.info().items())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To obtain a Kripke structure, call `kripke` and supply a list of atomic propositions to observe in the model."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
215
   "metadata": {},
216
   "outputs": [
217
    {
218
219
220
221
222
     "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
223
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
224
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
225
       "<!-- Pages: 1 -->\n",
226
227
       "<svg width=\"734pt\" height=\"242pt\"\n",
       " viewBox=\"0.00 0.00 734.00 242.46\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
228
229
230
231
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.6487 .6487) rotate(0) translate(4 369.7401)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-369.7401 1127.4104,-369.7401 1127.4104,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"558.7052\" y=\"-350.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">t</text>\n",
       "<text text-anchor=\"start\" x=\"550.7052\" y=\"-335.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[all]</text>\n",
232
233
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
234
235
236
237
238
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"150.1371\" cy=\"-154.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"105.1371\" y=\"-158.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"78.1371\" y=\"-143.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
239
240
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
241
242
243
244
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1671,-154.8701C3.9097,-154.8701 14.8741,-154.8701 29.7057,-154.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"36.7767,-154.8701 29.7767,-158.0202 33.2767,-154.8701 29.7767,-154.8702 29.7767,-154.8702 29.7767,-154.8702 33.2767,-154.8701 29.7766,-151.7202 36.7767,-154.8701 36.7767,-154.8701\"/>\n",
245
246
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
247
248
249
250
251
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"415.2397\" cy=\"-190.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"370.2397\" y=\"-194.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"341.2397\" y=\"-179.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
252
253
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
254
255
256
257
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M248.4748,-168.224C267.7667,-170.8437 288.0966,-173.6045 307.6721,-176.2628\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"314.8467,-177.237 307.4865,-179.4164 311.3786,-176.766 307.9104,-176.295 307.9104,-176.295 307.9104,-176.295 311.3786,-176.766 308.3343,-173.1737 314.8467,-177.237 314.8467,-177.237\"/>\n",
258
259
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
260
261
262
263
264
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"415.2397\" cy=\"-118.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"370.2397\" y=\"-122.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"343.2397\" y=\"-107.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
265
266
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
267
268
269
270
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M248.4748,-141.5161C268.3786,-138.8133 289.3872,-135.9604 309.5324,-133.2247\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"316.6187,-132.2624 310.1063,-136.3258 313.1506,-132.7334 309.6824,-133.2045 309.6824,-133.2045 309.6824,-133.2045 313.1506,-132.7334 309.2585,-130.0831 316.6187,-132.2624 316.6187,-132.2624\"/>\n",
271
272
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
273
274
275
276
277
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-226.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-230.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=2, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"609.1707\" y=\"-215.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
278
279
       "</g>\n",
       "<!-- 1&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
280
281
282
283
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M515.7696,-204.3776C535.2954,-207.0011 555.8335,-209.7607 575.576,-212.4133\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5231,-213.3467 575.1659,-215.5364 579.0543,-212.8806 575.5854,-212.4145 575.5854,-212.4145 575.5854,-212.4145 579.0543,-212.8806 576.0049,-209.2926 582.5231,-213.3467 582.5231,-213.3467\"/>\n",
284
285
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
286
287
288
289
290
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-154.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-158.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"609.1707\" y=\"-143.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
291
292
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293
294
295
296
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M515.7696,-177.3626C535.2954,-174.739 555.8335,-171.9795 575.576,-169.3268\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5231,-168.3934 576.0049,-172.4476 579.0543,-168.8595 575.5854,-169.3256 575.5854,-169.3256 575.5854,-169.3256 579.0543,-168.8595 575.1659,-166.2037 582.5231,-168.3934 582.5231,-168.3934\"/>\n",
297
298
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
299
300
301
302
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M513.8659,-132.1218C533.8869,-134.8118 555.0421,-137.6543 575.3619,-140.3845\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5112,-141.3451 575.154,-143.5348 579.0423,-140.879 575.5735,-140.4129 575.5735,-140.4129 575.5735,-140.4129 579.0423,-140.879 575.993,-137.291 582.5112,-141.3451 582.5112,-141.3451\"/>\n",
303
304
       "</g>\n",
       "<!-- 5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
305
306
307
308
309
       "<g id=\"node7\" class=\"node\">\n",
       "<title>5</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-82.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=2, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"611.1707\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
310
311
       "</g>\n",
       "<!-- 2&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
312
313
314
315
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M513.8659,-105.6184C534.5106,-102.8445 556.3611,-99.9086 577.2583,-97.1008\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"584.3054,-96.1539 577.7873,-100.2081 580.8366,-96.62 577.3678,-97.0861 577.3678,-97.0861 577.3678,-97.0861 580.8366,-96.62 576.9483,-93.9642 584.3054,-96.1539 584.3054,-96.1539\"/>\n",
316
317
       "</g>\n",
       "<!-- 6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
318
319
320
321
322
       "<g id=\"node8\" class=\"node\">\n",
       "<title>6</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-282.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-286.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=3, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"876.2733\" y=\"-271.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
323
324
       "</g>\n",
       "<!-- 3&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
325
326
327
328
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>3&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M768.8758,-244.9743C796.7674,-250.8661 827.8348,-257.4288 856.1739,-263.4151\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"863.3164,-264.9239 855.8165,-266.559 859.892,-264.2004 856.4676,-263.477 856.4676,-263.477 856.4676,-263.477 859.892,-264.2004 857.1186,-260.395 863.3164,-264.9239 863.3164,-264.9239\"/>\n",
329
330
       "</g>\n",
       "<!-- 7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
331
332
333
334
335
       "<g id=\"node9\" class=\"node\">\n",
       "<title>7</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-210.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-214.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=2, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-199.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
336
337
       "</g>\n",
       "<!-- 3&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
338
339
340
341
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M795.5981,-220.0846C819.5378,-218.6398 844.3743,-217.1408 866.8851,-215.7822\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"874.108,-215.3462 867.3105,-218.9123 870.6144,-215.5571 867.1207,-215.768 867.1207,-215.768 867.1207,-215.768 870.6144,-215.5571 866.9309,-212.6238 874.108,-215.3462 874.108,-215.3462\"/>\n",
342
343
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
344
345
346
347
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>4&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M768.8758,-172.9743C803.6186,-180.3133 843.289,-188.6933 876.4758,-195.7036\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.455,-197.1779 875.9551,-198.8131 880.0306,-196.4545 876.6062,-195.7311 876.6062,-195.7311 876.6062,-195.7311 880.0306,-196.4545 877.2572,-192.6491 883.455,-197.1779 883.455,-197.1779\"/>\n",
348
349
       "</g>\n",
       "<!-- 8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
350
351
352
353
354
       "<g id=\"node10\" class=\"node\">\n",
       "<title>8</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-138.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-142.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=2, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-127.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
355
356
       "</g>\n",
       "<!-- 4&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
357
358
359
360
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>4&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M795.5981,-148.0846C819.5378,-146.6398 844.3743,-145.1408 866.8851,-143.7822\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"874.108,-143.3462 867.3105,-146.9123 870.6144,-143.5571 867.1207,-143.768 867.1207,-143.768 867.1207,-143.768 870.6144,-143.5571 866.9309,-140.6238 874.108,-143.3462 874.108,-143.3462\"/>\n",
361
362
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
363
364
365
366
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>5&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M767.7797,-100.7428C802.7225,-108.1241 842.8025,-116.5905 876.3042,-123.6674\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.349,-125.1555 875.8491,-126.7907 879.9246,-124.4321 876.5001,-123.7087 876.5001,-123.7087 876.5001,-123.7087 879.9246,-124.4321 877.1512,-120.6267 883.349,-125.1555 883.349,-125.1555\"/>\n",
367
368
       "</g>\n",
       "<!-- u5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
369
370
371
372
       "<g id=\"node11\" class=\"node\">\n",
       "<title>u5</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"961.2733,-94.3701 935.2733,-94.3701 935.2733,-71.3701 961.2733,-71.3701 961.2733,-94.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"948.2733\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
373
374
       "</g>\n",
       "<!-- 5&#45;&gt;u5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
375
376
377
378
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>5&#45;&gt;u5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M796.367,-82.8701C846.0208,-82.8701 899.3777,-82.8701 927.7542,-82.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"935.0716,-82.8701 928.0716,-86.0202 931.5716,-82.8701 928.0716,-82.8702 928.0716,-82.8702 928.0716,-82.8702 931.5716,-82.8701 928.0715,-79.7202 935.0716,-82.8701 935.0716,-82.8701\"/>\n",
379
380
       "</g>\n",
       "<!-- 9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
382
383
384
385
       "<g id=\"node12\" class=\"node\">\n",
       "<title>9</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-26.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=3, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
386
387
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388
389
390
391
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>5&#45;&gt;9</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M767.7797,-64.9973C802.7225,-57.6161 842.8025,-49.1496 876.3042,-42.0727\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.349,-40.5846 877.1512,-45.1134 879.9246,-41.308 876.5001,-42.0314 876.5001,-42.0314 876.5001,-42.0314 879.9246,-41.308 875.8491,-38.9494 883.349,-40.5846 883.349,-40.5846\"/>\n",
392
393
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394
395
396
397
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>6&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M918.017,-309.1406C916.6722,-319.2978 926.7577,-327.7401 948.2733,-327.7401 964.41,-327.7401 974.1173,-322.9913 977.395,-316.3318\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"978.5297,-309.1406 980.5501,-316.546 977.9841,-312.5978 977.4386,-316.055 977.4386,-316.055 977.4386,-316.055 977.9841,-312.5978 974.3271,-315.5641 978.5297,-309.1406 978.5297,-309.1406\"/>\n",
398
399
       "</g>\n",
       "<!-- u7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400
401
402
403
       "<g id=\"node13\" class=\"node\">\n",
       "<title>u7</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-222.3701 1097.4104,-222.3701 1097.4104,-199.3701 1123.4104,-199.3701 1123.4104,-222.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-207.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
404
405
       "</g>\n",
       "<!-- 7&#45;&gt;u7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
406
407
408
409
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>7&#45;&gt;u7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-210.8701C1048.0287,-210.8701 1073.1021,-210.8701 1089.9848,-210.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-210.8701 1090.1335,-214.0202 1093.6334,-210.8701 1090.1334,-210.8702 1090.1334,-210.8702 1090.1334,-210.8702 1093.6334,-210.8701 1090.1334,-207.7202 1097.1334,-210.8701 1097.1334,-210.8701\"/>\n",
410
411
       "</g>\n",
       "<!-- u8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
412
413
414
415
       "<g id=\"node14\" class=\"node\">\n",
       "<title>u8</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-150.3701 1097.4104,-150.3701 1097.4104,-127.3701 1123.4104,-127.3701 1123.4104,-150.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-135.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
416
417
       "</g>\n",
       "<!-- 8&#45;&gt;u8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
418
419
420
421
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>8&#45;&gt;u8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-138.8701C1048.0287,-138.8701 1073.1021,-138.8701 1089.9848,-138.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-138.8701 1090.1335,-142.0202 1093.6334,-138.8701 1090.1334,-138.8702 1090.1334,-138.8702 1090.1334,-138.8702 1093.6334,-138.8701 1090.1334,-135.7202 1097.1334,-138.8701 1097.1334,-138.8701\"/>\n",
422
423
       "</g>\n",
       "<!-- u9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
424
425
426
427
       "<g id=\"node15\" class=\"node\">\n",
       "<title>u9</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-38.3701 1097.4104,-38.3701 1097.4104,-15.3701 1123.4104,-15.3701 1123.4104,-38.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
428
429
       "</g>\n",
       "<!-- 9&#45;&gt;u9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
430
431
432
433
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>9&#45;&gt;u9</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-26.8701C1048.0287,-26.8701 1073.1021,-26.8701 1089.9848,-26.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-26.8701 1090.1335,-30.0202 1093.6334,-26.8701 1090.1334,-26.8702 1090.1334,-26.8702 1090.1334,-26.8702 1093.6334,-26.8701 1090.1334,-23.7202 1097.1334,-26.8701 1097.1334,-26.8701\"/>\n",
434
435
436
437
438
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
439
       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fb8f84f9870> >"
440
441
442
      ]
     },
     "execution_count": 9,
443
     "metadata": {},
444
445
446
447
448
449
450
451
452
453
454
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k = m.kripke([\"a<1\", \"b>2\"])\n",
    "k"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
455
   "metadata": {},
456
   "outputs": [
457
    {
458
459
     "data": {
      "image/svg+xml": [
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
460
461
462
463
464
       "<svg height=\"219pt\" viewBox=\"0.00 0.00 734.00 219.12\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g class=\"graph\" id=\"graph0\" transform=\"scale(.5245 .5245) rotate(0) translate(4 413.7401)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-413.7401 1395.3414,-413.7401 1395.3414,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"692.6707\" y=\"-394.5401\">t</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"684.6707\" y=\"-379.5401\">[all]</text>\n",
465
466
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
467
468
469
470
471
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"150.1371\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"105.1371\" y=\"-186.6701\">a=0, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.1371\" y=\"-171.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
472
473
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
474
475
476
477
       "<g class=\"edge\" id=\"edge1\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.1671,-182.8701C3.9097,-182.8701 14.8741,-182.8701 29.7057,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"36.7767,-182.8701 29.7767,-186.0202 33.2767,-182.8701 29.7767,-182.8702 29.7767,-182.8702 29.7767,-182.8702 33.2767,-182.8701 29.7766,-179.7202 36.7767,-182.8701 36.7767,-182.8701\" stroke=\"#000000\"/>\n",
478
479
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
480
481
482
483
484
       "<g class=\"node\" id=\"node3\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-218.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-222.6701\">a=1, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341.2397\" y=\"-207.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
485
486
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
487
488
489
490
       "<g class=\"edge\" id=\"edge2\">\n",
       "<title>0-&gt;1</title>\n",
       "<path d=\"M248.4748,-196.224C267.7667,-198.8437 288.0966,-201.6045 307.6721,-204.2628\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"314.8467,-205.237 307.4865,-207.4164 311.3786,-204.766 307.9104,-204.295 307.9104,-204.295 307.9104,-204.295 311.3786,-204.766 308.3343,-201.1737 314.8467,-205.237 314.8467,-205.237\" stroke=\"#000000\"/>\n",
491
492
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
493
494
495
496
497
       "<g class=\"node\" id=\"node4\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-146.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-150.6701\">a=0, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343.2397\" y=\"-135.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
498
499
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
500
501
502
503
       "<g class=\"edge\" id=\"edge3\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M248.4748,-169.5161C268.3786,-166.8133 289.3872,-163.9604 309.5324,-161.2247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"316.6187,-160.2624 310.1063,-164.3258 313.1506,-160.7334 309.6824,-161.2045 309.6824,-161.2045 309.6824,-161.2045 313.1506,-160.7334 309.2585,-158.0831 316.6187,-160.2624 316.6187,-160.2624\" stroke=\"#000000\"/>\n",
504
505
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
506
507
508
509
510
       "<g class=\"node\" id=\"node5\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-258.6701\">a=2, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-243.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
511
512
       "</g>\n",
       "<!-- 1&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
513
514
515
516
       "<g class=\"edge\" id=\"edge4\">\n",
       "<title>1-&gt;3</title>\n",
       "<path d=\"M515.7696,-232.3776C535.2954,-235.0011 555.8335,-237.7607 575.576,-240.4133\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-241.3467 575.1659,-243.5364 579.0543,-240.8806 575.5854,-240.4145 575.5854,-240.4145 575.5854,-240.4145 579.0543,-240.8806 576.0049,-237.2926 582.5231,-241.3467 582.5231,-241.3467\" stroke=\"#000000\"/>\n",
517
518
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
519
520
521
522
523
       "<g class=\"node\" id=\"node6\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-186.6701\">a=1, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-171.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
524
525
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
526
527
528
529
       "<g class=\"edge\" id=\"edge5\">\n",
       "<title>1-&gt;4</title>\n",
       "<path d=\"M515.7696,-205.3626C535.2954,-202.739 555.8335,-199.9795 575.576,-197.3268\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-196.3934 576.0049,-200.4476 579.0543,-196.8595 575.5854,-197.3256 575.5854,-197.3256 575.5854,-197.3256 579.0543,-196.8595 575.1659,-194.2037 582.5231,-196.3934 582.5231,-196.3934\" stroke=\"#000000\"/>\n",
530
531
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
532
533
534
535
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;4</title>\n",
       "<path d=\"M513.8659,-160.1218C533.8869,-162.8118 555.0421,-165.6543 575.3619,-168.3845\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5112,-169.3451 575.154,-171.5348 579.0423,-168.879 575.5735,-168.4129 575.5735,-168.4129 575.5735,-168.4129 579.0423,-168.879 575.993,-165.291 582.5112,-169.3451 582.5112,-169.3451\" stroke=\"#000000\"/>\n",
536
537
       "</g>\n",
       "<!-- 5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
538
539
540
541
542
       "<g class=\"node\" id=\"node7\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-114.6701\">a=0, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"611.1707\" y=\"-99.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
543
544
       "</g>\n",
       "<!-- 2&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
545
546
547
548
       "<g class=\"edge\" id=\"edge7\">\n",
       "<title>2-&gt;5</title>\n",
       "<path d=\"M513.8659,-133.6184C534.5106,-130.8445 556.3611,-127.9086 577.2583,-125.1008\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"584.3054,-124.1539 577.7873,-128.2081 580.8366,-124.62 577.3678,-125.0861 577.3678,-125.0861 577.3678,-125.0861 580.8366,-124.62 576.9483,-121.9642 584.3054,-124.1539 584.3054,-124.1539\" stroke=\"#000000\"/>\n",
549
550
       "</g>\n",
       "<!-- 6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
551
552
553
554
555
       "<g class=\"node\" id=\"node8\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-326.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-330.6701\">a=3, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-315.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
556
557
       "</g>\n",
       "<!-- 3&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
558
559
560
561
       "<g class=\"edge\" id=\"edge8\">\n",
       "<title>3-&gt;6</title>\n",
       "<path d=\"M759.2323,-275.3098C793.4622,-284.5082 833.9374,-295.385 868.8685,-304.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.7773,-306.6284 868.1996,-307.8538 872.3972,-305.7201 869.0171,-304.8117 869.0171,-304.8117 869.0171,-304.8117 872.3972,-305.7201 869.8346,-301.7697 875.7773,-306.6284 875.7773,-306.6284\" stroke=\"#000000\"/>\n",
562
563
       "</g>\n",
       "<!-- 7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
564
565
566
567
568
       "<g class=\"node\" id=\"node9\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-258.6701\">a=2, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-243.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
569
570
       "</g>\n",
       "<!-- 3&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
571
572
573
574
       "<g class=\"edge\" id=\"edge9\">\n",
       "<title>3-&gt;7</title>\n",
       "<path d=\"M799.5202,-254.8701C808.8609,-254.8701 818.3179,-254.8701 827.7052,-254.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-254.8701 827.8671,-258.0202 831.3671,-254.8701 827.8671,-254.8702 827.8671,-254.8702 827.8671,-254.8702 831.3671,-254.8701 827.867,-251.7202 834.8671,-254.8701 834.8671,-254.8701\" stroke=\"#000000\"/>\n",
575
576
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
577
578
579
580
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>4-&gt;7</title>\n",
       "<path d=\"M759.2323,-203.3098C793.3171,-212.4693 833.5945,-223.2928 868.4242,-232.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.314,-234.5039 867.7363,-235.7293 871.9339,-233.5956 868.5538,-232.6872 868.5538,-232.6872 868.5538,-232.6872 871.9339,-233.5956 869.3714,-229.6452 875.314,-234.5039 875.314,-234.5039\" stroke=\"#000000\"/>\n",
581
582
       "</g>\n",
       "<!-- 8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
583
584
585
586
587
       "<g class=\"node\" id=\"node10\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-186.6701\">a=1, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-171.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
588
589
       "</g>\n",
       "<!-- 4&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
590
591
592
593
       "<g class=\"edge\" id=\"edge11\">\n",
       "<title>4-&gt;8</title>\n",
       "<path d=\"M799.5202,-182.8701C808.8609,-182.8701 818.3179,-182.8701 827.7052,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-182.8701 827.8671,-186.0202 831.3671,-182.8701 827.8671,-182.8702 827.8671,-182.8702 827.8671,-182.8702 831.3671,-182.8701 827.867,-179.7202 834.8671,-182.8701 834.8671,-182.8701\" stroke=\"#000000\"/>\n",
594
595
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
596
597
598
599
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>5-&gt;8</title>\n",
       "<path d=\"M758.1607,-131.0218C792.4127,-140.2262 833.0911,-151.1575 868.2457,-160.6045\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.1995,-162.4732 867.6218,-163.6985 871.8194,-161.5648 868.4393,-160.6564 868.4393,-160.6564 868.4393,-160.6564 871.8194,-161.5648 869.2568,-157.6144 875.1995,-162.4732 875.1995,-162.4732\" stroke=\"#000000\"/>\n",
600
601
       "</g>\n",
       "<!-- 9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
602
603
604
605
606
       "<g class=\"node\" id=\"node11\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"946.1017\" y=\"-15.6701\">...</text>\n",
607
608
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
609
610
611
612
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>5-&gt;9</title>\n",
       "<path d=\"M751.8217,-89.3471C793.6799,-76.2239 846.8016,-59.5696 887.6708,-46.7565\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"894.3784,-44.6536 888.6413,-49.7535 891.0386,-45.7007 887.6989,-46.7478 887.6989,-46.7478 887.6989,-46.7478 891.0386,-45.7007 886.7565,-43.742 894.3784,-44.6536 894.3784,-44.6536\" stroke=\"#000000\"/>\n",
613
614
       "</g>\n",
       "<!-- 10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
615
616
617
618
619
       "<g class=\"node\" id=\"node12\">\n",
       "<title>10</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-114.6701\">a=0, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-99.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
620
621
       "</g>\n",
       "<!-- 5&#45;&gt;10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
622
623
624
625
       "<g class=\"edge\" id=\"edge14\">\n",
       "<title>5-&gt;10</title>\n",
       "<path d=\"M796.4092,-110.8701C807.7635,-110.8701 819.3214,-110.8701 830.7458,-110.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"837.8389,-110.8701 830.839,-114.0202 834.3389,-110.8701 830.8389,-110.8702 830.8389,-110.8702 830.8389,-110.8702 834.3389,-110.8701 830.8389,-107.7202 837.8389,-110.8701 837.8389,-110.8701\" stroke=\"#000000\"/>\n",
626
627
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
628
629
630
631
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M902.3752,-351.3317C897.7345,-362.2753 913.9767,-371.7401 951.1017,-371.7401 979.5256,-371.7401 995.7083,-366.192 999.6499,-358.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"999.8283,-351.3317 1002.8073,-358.4061 999.7433,-354.8307 999.6583,-358.3296 999.6583,-358.3296 999.6583,-358.3296 999.7433,-354.8307 996.5092,-358.2531 999.8283,-351.3317 999.8283,-351.3317\" stroke=\"#000000\"/>\n",
632
633
       "</g>\n",
       "<!-- 11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
634
635
636
637
638
       "<g class=\"node\" id=\"node13\">\n",
       "<title>11</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-326.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-330.6701\">a=3, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1144.2043\" y=\"-315.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
639
640
       "</g>\n",
       "<!-- 7&#45;&gt;11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
641
642
643
644
       "<g class=\"edge\" id=\"edge16\">\n",
       "<title>7-&gt;11</title>\n",
       "<path d=\"M1026.7147,-275.406C1060.4316,-284.5633 1100.2171,-295.3687 1134.6056,-304.7084\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.408,-306.5559 1133.827,-307.761 1138.0303,-305.6385 1134.6527,-304.7211 1134.6527,-304.7211 1134.6527,-304.7211 1138.0303,-305.6385 1135.4783,-301.6813 1141.408,-306.5559 1141.408,-306.5559\" stroke=\"#000000\"/>\n",
645
646
       "</g>\n",
       "<!-- 12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
647
648
649
650
651
       "<g class=\"node\" id=\"node14\">\n",
       "<title>12</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-258.6701\">a=2, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-243.6701\">...</text>\n",
652
653
       "</g>\n",
       "<!-- 7&#45;&gt;12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
655
656
657
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>7-&gt;12</title>\n",
       "<path d=\"M1067.3796,-254.8701C1089.878,-254.8701 1113.0114,-254.8701 1134.1342,-254.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.2167,-254.8701 1134.2167,-258.0202 1137.7167,-254.8701 1134.2167,-254.8702 1134.2167,-254.8702 1134.2167,-254.8702 1137.7167,-254.8701 1134.2166,-251.7202 1141.2167,-254.8701 1141.2167,-254.8701\" stroke=\"#000000\"/>\n",
658
659
       "</g>\n",
       "<!-- 8&#45;&gt;12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
660
661
662
663
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>8-&gt;12</title>\n",
       "<path d=\"M1026.7147,-203.406C1065.3265,-213.8927 1111.8969,-226.5409 1149.2066,-236.674\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1156.0614,-238.5357 1148.4805,-239.7408 1152.6837,-237.6183 1149.3061,-236.7009 1149.3061,-236.7009 1149.3061,-236.7009 1152.6837,-237.6183 1150.1317,-233.661 1156.0614,-238.5357 1156.0614,-238.5357\" stroke=\"#000000\"/>\n",
664
665
       "</g>\n",
       "<!-- 13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
666
667
668
669
670
       "<g class=\"node\" id=\"node15\">\n",
       "<title>13</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-186.6701\">a=1, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-171.6701\">...</text>\n",
671
672
       "</g>\n",
       "<!-- 8&#45;&gt;13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
673
674
675
676
       "<g class=\"edge\" id=\"edge19\">\n",
       "<title>8-&gt;13</title>\n",
       "<path d=\"M1067.3796,-182.8701C1089.878,-182.8701 1113.0114,-182.8701 1134.1342,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.2167,-182.8701 1134.2167,-186.0202 1137.7167,-182.8701 1134.2167,-182.8702 1134.2167,-182.8702 1134.2167,-182.8702 1137.7167,-182.8701 1134.2166,-179.7202 1141.2167,-182.8701 1141.2167,-182.8701\" stroke=\"#000000\"/>\n",
677
678
       "</g>\n",
       "<!-- 14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
679
680
681
682
683
       "<g class=\"node\" id=\"node16\">\n",
       "<title>14</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-114.6701\">a=1, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-99.6701\">...</text>\n",
684
685
       "</g>\n",
       "<!-- 8&#45;&gt;14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
686
687
688
689
       "<g class=\"edge\" id=\"edge20\">\n",
       "<title>8-&gt;14</title>\n",
       "<path d=\"M1026.7147,-162.3341C1065.3265,-151.8474 1111.8969,-139.1992 1149.2066,-129.0662\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1156.0614,-127.2045 1150.1317,-132.0791 1152.6837,-128.1218 1149.3061,-129.0392 1149.3061,-129.0392 1149.3061,-129.0392 1152.6837,-128.1218 1148.4805,-125.9993 1156.0614,-127.2045 1156.0614,-127.2045\" stroke=\"#000000\"/>\n",
690
691
       "</g>\n",
       "<!-- u9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
692
693
694
695
       "<g class=\"node\" id=\"node17\">\n",
       "<title>u9</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1229.2043,-25.3701 1203.2043,-25.3701 1203.2043,-2.3701 1229.2043,-2.3701 1229.2043,-25.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2043\" y=\"-10.1701\">...</text>\n",
696
697
       "</g>\n",
       "<!-- 9&#45;&gt;u9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
698
699
700
701
       "<g class=\"edge\" id=\"edge21\">\n",
       "<title>9-&gt;u9</title>\n",
       "<path d=\"M1025.6531,-23.2142C1083.7014,-20.3677 1160.2356,-16.6146 1196.0712,-14.8573\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1203.0791,-14.5137 1196.2418,-18.0029 1199.5833,-14.6852 1196.0875,-14.8566 1196.0875,-14.8566 1196.0875,-14.8566 1199.5833,-14.6852 1195.9331,-11.7104 1203.0791,-14.5137 1203.0791,-14.5137\" stroke=\"#000000\"/>\n",
702
703
       "</g>\n",
       "<!-- 10&#45;&gt;14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
704
705
706
707
       "<g class=\"edge\" id=\"edge23\">\n",
       "<title>10-&gt;14</title>\n",
       "<path d=\"M1064.2981,-110.8701C1087.6637,-110.8701 1111.8495,-110.8701 1133.8663,-110.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1140.9346,-110.8701 1133.9347,-114.0202 1137.4346,-110.8701 1133.9346,-110.8702 1133.9346,-110.8702 1133.9346,-110.8702 1137.4346,-110.8701 1133.9346,-107.7202 1140.9346,-110.8701 1140.9346,-110.8701\" stroke=\"#000000\"/>\n",
708
709
       "</g>\n",
       "<!-- u10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
710
711
712
713
       "<g class=\"node\" id=\"node18\">\n",
       "<title>u10</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1229.2043,-66.3701 1203.2043,-66.3701 1203.2043,-43.3701 1229.2043,-43.3701 1229.2043,-66.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2043\" y=\"-51.1701\">...</text>\n",
714
715
       "</g>\n",
       "<!-- 10&#45;&gt;u10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
716
717
718
719
       "<g class=\"edge\" id=\"edge22\">\n",
       "<title>10-&gt;u10</title>\n",
       "<path d=\"M1029.3911,-91.4126C1053.0061,-85.7898 1079.0376,-79.8359 1103.0672,-74.8701 1135.3588,-68.1968 1173.1233,-61.8022 1195.8271,-58.109\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1202.9195,-56.9636 1196.5113,-61.1894 1199.4643,-57.5217 1196.0091,-58.0797 1196.0091,-58.0797 1196.0091,-58.0797 1199.4643,-57.5217 1195.5068,-54.97 1202.9195,-56.9636 1202.9195,-56.9636\" stroke=\"#000000\"/>\n",
720
721
       "</g>\n",
       "<!-- 11&#45;&gt;11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
722
723
724
725
       "<g class=\"edge\" id=\"edge24\">\n",
       "<title>11-&gt;11</title>\n",
       "<path d=\"M1185.948,-353.1406C1184.6033,-363.2978 1194.6887,-371.7401 1216.2043,-371.7401 1232.341,-371.7401 1242.0483,-366.9913 1245.3261,-360.3318\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1246.4607,-353.1406 1248.4812,-360.546 1245.9152,-356.5978 1245.3697,-360.055 1245.3697,-360.055 1245.3697,-360.055 1245.9152,-356.5978 1242.2581,-359.5641 1246.4607,-353.1406 1246.4607,-353.1406\" stroke=\"#000000\"/>\n",
726
727
       "</g>\n",
       "<!-- u12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
728
729
730
731
       "<g class=\"node\" id=\"node19\">\n",
       "<title>u12</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-266.3701 1365.3414,-266.3701 1365.3414,-243.3701 1391.3414,-243.3701 1391.3414,-266.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-251.1701\">...</text>\n",
732
733
       "</g>\n",
       "<!-- 12&#45;&gt;u12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
734
735
736
737
       "<g class=\"edge\" id=\"edge25\">\n",
       "<title>12-&gt;u12</title>\n",
       "<path d=\"M1291.5769,-254.8701C1315.9597,-254.8701 1341.0331,-254.8701 1357.9158,-254.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-254.8701 1358.0645,-258.0202 1361.5645,-254.8701 1358.0645,-254.8702 1358.0645,-254.8702 1358.0645,-254.8702 1361.5645,-254.8701 1358.0644,-251.7202 1365.0645,-254.8701 1365.0645,-254.8701\" stroke=\"#000000\"/>\n",
738
739
       "</g>\n",
       "<!-- u13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
740
741
742
743
       "<g class=\"node\" id=\"node20\">\n",
       "<title>u13</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-194.3701 1365.3414,-194.3701 1365.3414,-171.3701 1391.3414,-171.3701 1391.3414,-194.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-179.1701\">...</text>\n",
744
745
       "</g>\n",
       "<!-- 13&#45;&gt;u13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
746
747
748
749
       "<g class=\"edge\" id=\"edge26\">\n",
       "<title>13-&gt;u13</title>\n",
       "<path d=\"M1291.5769,-182.8701C1315.9597,-182.8701 1341.0331,-182.8701 1357.9158,-182.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-182.8701 1358.0645,-186.0202 1361.5645,-182.8701 1358.0645,-182.8702 1358.0645,-182.8702 1358.0645,-182.8702 1361.5645,-182.8701 1358.0644,-179.7202 1365.0645,-182.8701 1365.0645,-182.8701\" stroke=\"#000000\"/>\n",
750
751
       "</g>\n",
       "<!-- u14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
753
754
755
       "<g class=\"node\" id=\"node21\">\n",
       "<title>u14</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-122.3701 1365.3414,-122.3701 1365.3414,-99.3701 1391.3414,-99.3701 1391.3414,-122.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-107.1701\">...</text>\n",
756
757
       "</g>\n",
       "<!-- 14&#45;&gt;u14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
758
759
760
761
       "<g class=\"edge\" id=\"edge27\">\n",
       "<title>14-&gt;u14</title>\n",
       "<path d=\"M1291.5769,-110.8701C1315.9597,-110.8701 1341.0331,-110.8701 1357.9158,-110.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-110.8701 1358.0645,-114.0202 1361.5645,-110.8701 1358.0645,-110.8702 1358.0645,-110.8702 1358.0645,-110.8702 1361.5645,-110.8701 1358.0644,-107.7202 1365.0645,-110.8701 1365.0645,-110.8701\" stroke=\"#000000\"/>\n",
762
763
764
765
766
767
768
769
770
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "execution_count": 10,
771
     "metadata": {},
772
773
774
775
776
777
778
779
780
781
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k.show('.<15')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
782
   "metadata": {},
783
   "outputs": [
784
    {
785
786
     "data": {
      "image/svg+xml": [
787
       "<svg height=\"166pt\" viewBox=\"0.00 0.00 734.00 165.54\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
788
789
790
791
       "<g class=\"graph\" id=\"graph0\" transform=\"scale(.3907 .3907) rotate(0) translate(4 419.7401)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-419.7401 1874.8603,-419.7401 1874.8603,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"932.4302\" y=\"-400.5401\">t</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"924.4302\" y=\"-385.5401\">[all]</text>\n",
792
793
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
794
795
796
797
798
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"150.1371\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"105.1371\" y=\"-192.6701\">a=0, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.1371\" y=\"-177.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
799
800
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
801
802
803
804
       "<g class=\"edge\" id=\"edge1\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.1671,-188.8701C3.9097,-188.8701 14.8741,-188.8701 29.7057,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"36.7767,-188.8701 29.7767,-192.0202 33.2767,-188.8701 29.7767,-188.8702 29.7767,-188.8702 29.7767,-188.8702 33.2767,-188.8701 29.7766,-185.7202 36.7767,-188.8701 36.7767,-188.8701\" stroke=\"#000000\"/>\n",
805
806
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
807
808
809
810
811
       "<g class=\"node\" id=\"node3\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-224.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-228.6701\">a=1, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341.2397\" y=\"-213.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
812
813
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
814
815
816
817
       "<g class=\"edge\" id=\"edge2\">\n",
       "<title>0-&gt;1</title>\n",
       "<path d=\"M248.4748,-202.224C267.7667,-204.8437 288.0966,-207.6045 307.6721,-210.2628\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"314.8467,-211.237 307.4865,-213.4164 311.3786,-210.766 307.9104,-210.295 307.9104,-210.295 307.9104,-210.295 311.3786,-210.766 308.3343,-207.1737 314.8467,-211.237 314.8467,-211.237\" stroke=\"#000000\"/>\n",
818
819
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
820
821
822
823
824
       "<g class=\"node\" id=\"node4\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-152.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-156.6701\">a=0, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343.2397\" y=\"-141.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
825
826
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
827
828
829
830
       "<g class=\"edge\" id=\"edge3\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M248.4748,-175.5161C268.3786,-172.8133 289.3872,-169.9604 309.5324,-167.2247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"316.6187,-166.2624 310.1063,-170.3258 313.1506,-166.7334 309.6824,-167.2045 309.6824,-167.2045 309.6824,-167.2045 313.1506,-166.7334 309.2585,-164.0831 316.6187,-166.2624 316.6187,-166.2624\" stroke=\"#000000\"/>\n",
831
832
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
833
834
835
836
837
       "<g class=\"node\" id=\"node5\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-264.6701\">a=2, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-249.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
838
839
       "</g>\n",
       "<!-- 1&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
840
841
842
843
       "<g class=\"edge\" id=\"edge4\">\n",
       "<title>1-&gt;3</title>\n",
       "<path d=\"M515.7696,-238.3776C535.2954,-241.0011 555.8335,-243.7607 575.576,-246.4133\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-247.3467 575.1659,-249.5364 579.0543,-246.8806 575.5854,-246.4145 575.5854,-246.4145 575.5854,-246.4145 579.0543,-246.8806 576.0049,-243.2926 582.5231,-247.3467 582.5231,-247.3467\" stroke=\"#000000\"/>\n",
844
845
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
846
847
848
849
850
       "<g class=\"node\" id=\"node6\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-192.6701\">a=1, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-177.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
851
852
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
853
854
855
856
       "<g class=\"edge\" id=\"edge5\">\n",
       "<title>1-&gt;4</title>\n",
       "<path d=\"M515.7696,-211.3626C535.2954,-208.739 555.8335,-205.9795 575.576,-203.3268\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-202.3934 576.0049,-206.4476 579.0543,-202.8595 575.5854,-203.3256 575.5854,-203.3256 575.5854,-203.3256 579.0543,-202.8595 575.1659,-200.2037 582.5231,-202.3934 582.5231,-202.3934\" stroke=\"#000000\"/>\n",
857
858
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
859
860
861
862
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;4</title>\n",
       "<path d=\"M513.8659,-166.1218C533.8869,-168.8118 555.0421,-171.6543 575.3619,-174.3845\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5112,-175.3451 575.154,-177.5348 579.0423,-174.879 575.5735,-174.4129 575.5735,-174.4129 575.5735,-174.4129 579.0423,-174.879 575.993,-171.291 582.5112,-175.3451 582.5112,-175.3451\" stroke=\"#000000\"/>\n",
863
864
       "</g>\n",
       "<!-- 5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
865
866
867
868
869
       "<g class=\"node\" id=\"node7\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-120.6701\">a=0, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"611.1707\" y=\"-105.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
870
871
       "</g>\n",
       "<!-- 2&#45;&gt;5 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
872
873
874
875
       "<g class=\"edge\" id=\"edge7\">\n",
       "<title>2-&gt;5</title>\n",
       "<path d=\"M513.8659,-139.6184C534.5106,-136.8445 556.3611,-133.9086 577.2583,-131.1008\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"584.3054,-130.1539 577.7873,-134.2081 580.8366,-130.62 577.3678,-131.0861 577.3678,-131.0861 577.3678,-131.0861 580.8366,-130.62 576.9483,-127.9642 584.3054,-130.1539 584.3054,-130.1539\" stroke=\"#000000\"/>\n",
876
877
       "</g>\n",
       "<!-- 6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
878
879
880
881
882
       "<g class=\"node\" id=\"node8\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-336.6701\">a=3, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-321.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
883
884
       "</g>\n",
       "<!-- 3&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
885
886
887
888
       "<g class=\"edge\" id=\"edge8\">\n",
       "<title>3-&gt;6</title>\n",
       "<path d=\"M759.2323,-281.3098C793.4622,-290.5082 833.9374,-301.385 868.8685,-310.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.7773,-312.6284 868.1996,-313.8538 872.3972,-311.7201 869.0171,-310.8117 869.0171,-310.8117 869.0171,-310.8117 872.3972,-311.7201 869.8346,-307.7697 875.7773,-312.6284 875.7773,-312.6284\" stroke=\"#000000\"/>\n",
889
890
       "</g>\n",
       "<!-- 7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
891
892
893
894
895
       "<g class=\"node\" id=\"node9\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-264.6701\">a=2, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-249.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
896
897
       "</g>\n",
       "<!-- 3&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
898
899
900
901
       "<g class=\"edge\" id=\"edge9\">\n",
       "<title>3-&gt;7</title>\n",
       "<path d=\"M799.5202,-260.8701C808.8609,-260.8701 818.3179,-260.8701 827.7052,-260.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-260.8701 827.8671,-264.0202 831.3671,-260.8701 827.8671,-260.8702 827.8671,-260.8702 827.8671,-260.8702 831.3671,-260.8701 827.867,-257.7202 834.8671,-260.8701 834.8671,-260.8701\" stroke=\"#000000\"/>\n",
902
903
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
904
905
906
907
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>4-&gt;7</title>\n",
       "<path d=\"M759.2323,-209.3098C793.3171,-218.4693 833.5945,-229.2928 868.4242,-238.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.314,-240.5039 867.7363,-241.7293 871.9339,-239.5956 868.5538,-238.6872 868.5538,-238.6872 868.5538,-238.6872 871.9339,-239.5956 869.3714,-235.6452 875.314,-240.5039 875.314,-240.5039\" stroke=\"#000000\"/>\n",
908
909
       "</g>\n",
       "<!-- 8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
910
911
912
913
914
       "<g class=\"node\" id=\"node10\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-192.6701\">a=1, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-177.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
915
916
       "</g>\n",
       "<!-- 4&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
917
918
919
920
       "<g class=\"edge\" id=\"edge11\">\n",
       "<title>4-&gt;8</title>\n",
       "<path d=\"M799.5202,-188.8701C808.8609,-188.8701 818.3179,-188.8701 827.7052,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-188.8701 827.8671,-192.0202 831.3671,-188.8701 827.8671,-188.8702 827.8671,-188.8702 827.8671,-188.8702 831.3671,-188.8701 827.867,-185.7202 834.8671,-188.8701 834.8671,-188.8701\" stroke=\"#000000\"/>\n",
921
922
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
923
924
925
926
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>5-&gt;8</title>\n",
       "<path d=\"M758.1607,-137.0218C792.4127,-146.2262 833.0911,-157.1575 868.2457,-166.6045\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.1995,-168.4732 867.6218,-169.6985 871.8194,-167.5648 868.4393,-166.6564 868.4393,-166.6564 868.4393,-166.6564 871.8194,-167.5648 869.2568,-163.6144 875.1995,-168.4732 875.1995,-168.4732\" stroke=\"#000000\"/>\n",
927
928
       "</g>\n",
       "<!-- 9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
929
930
931
932
933
       "<g class=\"node\" id=\"node11\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-35.8701\" fill=\"#ffffaa\" rx=\"110.1176\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-39.6701\">a=0, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"881.1017\" y=\"-24.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
934
935
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
936
937
938
939
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>5-&gt;9</title>\n",
       "<path d=\"M753.2165,-95.6941C790.4375,-84.4415 836.2572,-70.5895 874.4299,-59.0492\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"881.4648,-56.9225 875.6759,-61.9634 878.1145,-57.9353 874.7643,-58.9482 874.7643,-58.9482 874.7643,-58.9482 878.1145,-57.9353 873.8527,-55.933 881.4648,-56.9225 881.4648,-56.9225\" stroke=\"#000000\"/>\n",
940
941
       "</g>\n",
       "<!-- 10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
942
943
944
945
946
       "<g class=\"node\" id=\"node12\">\n",
       "<title>10</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-120.6701\">a=0, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-105.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
947
948
       "</g>\n",
       "<!-- 5&#45;&gt;10 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
949
950
951
952
       "<g class=\"edge\" id=\"edge14\">\n",
       "<title>5-&gt;10</title>\n",
       "<path d=\"M796.4092,-116.8701C807.7635,-116.8701 819.3214,-116.8701 830.7458,-116.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"837.8389,-116.8701 830.839,-120.0202 834.3389,-116.8701 830.8389,-116.8702 830.8389,-116.8702 830.8389,-116.8702 834.3389,-116.8701 830.8389,-113.7202 837.8389,-116.8701 837.8389,-116.8701\" stroke=\"#000000\"/>\n",
953
954
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
955
956
957
958
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M902.006,-357.3317C897.3302,-368.2753 913.6955,-377.7401 951.1017,-377.7401 979.7409,-377.7401 996.0462,-372.192 1000.0176,-364.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1000.1974,-357.3317 1003.1752,-364.4067 1000.1118,-360.8306 1000.0261,-364.3296 1000.0261,-364.3296 1000.0261,-364.3296 1000.1118,-360.8306 996.8771,-364.2525 1000.1974,-357.3317 1000.1974,-357.3317\" stroke=\"#000000\"/>\n",
959
960
       "</g>\n",
       "<!-- 11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
961
962
963
964
965
       "<g class=\"node\" id=\"node13\">\n",
       "<title>11</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-336.6701\">a=3, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1147.0328\" y=\"-321.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
966
967
       "</g>\n",
       "<!-- 7&#45;&gt;11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
968
969
970
971
       "<g class=\"edge\" id=\"edge16\">\n",
       "<title>7-&gt;11</title>\n",
       "<path d=\"M1027.1633,-281.3098C1061.3932,-290.5082 1101.8684,-301.385 1136.7995,-310.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.7083,-312.6284 1136.1306,-313.8538 1140.3282,-311.7201 1136.9482,-310.8117 1136.9482,-310.8117 1136.9482,-310.8117 1140.3282,-311.7201 1137.7657,-307.7697 1143.7083,-312.6284 1143.7083,-312.6284\" stroke=\"#000000\"/>\n",
972
973
       "</g>\n",
       "<!-- 12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
974
975
976
977
978
       "<g class=\"node\" id=\"node14\">\n",
       "<title>12</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-264.6701\">a=2, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1145.0328\" y=\"-249.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
979
980
       "</g>\n",
       "<!-- 7&#45;&gt;12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
981
982
983
984
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>7-&gt;12</title>\n",
       "<path d=\"M1067.4513,-260.8701C1076.7919,-260.8701 1086.2489,-260.8701 1095.6362,-260.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1102.7981,-260.8701 1095.7981,-264.0202 1099.2981,-260.8701 1095.7981,-260.8702 1095.7981,-260.8702 1095.7981,-260.8702 1099.2981,-260.8701 1095.798,-257.7202 1102.7981,-260.8701 1102.7981,-260.8701\" stroke=\"#000000\"/>\n",
985
986
       "</g>\n",
       "<!-- 8&#45;&gt;12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
987
988
989
990
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>8-&gt;12</title>\n",
       "<path d=\"M1027.1633,-209.3098C1061.2481,-218.4693 1101.5255,-229.2928 1136.3552,-238.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.245,-240.5039 1135.6673,-241.7293 1139.8649,-239.5956 1136.4849,-238.6872 1136.4849,-238.6872 1136.4849,-238.6872 1139.8649,-239.5956 1137.3024,-235.6452 1143.245,-240.5039 1143.245,-240.5039\" stroke=\"#000000\"/>\n",
991
992
       "</g>\n",
       "<!-- 13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
993
994
995
996
997
       "<g class=\"node\" id=\"node15\">\n",
       "<title>13</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-192.6701\">a=1, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1147.0328\" y=\"-177.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
998
999
       "</g>\n",
       "<!-- 8&#45;&gt;13 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1000
1001
1002
1003
       "<g class=\"edge\" id=\"edge19\">\n",
       "<title>8-&gt;13</title>\n",
       "<path d=\"M1067.4513,-188.8701C1077.7783,-188.8701 1088.2475,-188.8701 1098.6075,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1105.7593,-188.8701 1098.7594,-192.0202 1102.2593,-188.8701 1098.7593,-188.8702 1098.7593,-188.8702 1098.7593,-188.8702 1102.2593,-188.8701 1098.7593,-185.7202 1105.7593,-188.8701 1105.7593,-188.8701\" stroke=\"#000000\"/>\n",
1004
1005
       "</g>\n",
       "<!-- 14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1006
1007
1008
1009
1010
       "<g class=\"node\" id=\"node16\">\n",
       "<title>14</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-120.6701\">a=1, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1145.0328\" y=\"-105.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1011
1012
       "</g>\n",
       "<!-- 8&#45;&gt;14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1013
1014
1015
1016
       "<g class=\"edge\" id=\"edge20\">\n",
       "<title>8-&gt;14</title>\n",
       "<path d=\"M1027.1633,-168.4303C1061.2481,-159.2709 1101.5255,-148.4473 1136.3552,-139.0877\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.245,-137.2362 1137.3024,-142.095 1139.8649,-138.1445 1136.4849,-139.0529 1136.4849,-139.0529 1136.4849,-139.0529 1139.8649,-138.1445 1135.6673,-136.0108 1143.245,-137.2362 1143.245,-137.2362\" stroke=\"#000000\"/>\n",
1017
1018
       "</g>\n",
       "<!-- 15 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1019
1020
1021
1022
1023
       "<g class=\"node\" id=\"node17\">\n",
       "<title>15</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"107.4605\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-30.6701\">a=0, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1151.0328\" y=\"-15.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
1024
1025
       "</g>\n",
       "<!-- 9&#45;&gt;15 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1026
1027
1028
1029
       "<g class=\"edge\" id=\"edge21\">\n",
       "<title>9-&gt;15</title>\n",
       "<path d=\"M1060.466,-32.1964C1075.1393,-31.7035 1090.2205,-31.197 1104.9723,-30.7014\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1112.1844,-30.4592 1105.2941,-33.8425 1108.6864,-30.5767 1105.1883,-30.6943 1105.1883,-30.6943 1105.1883,-30.6943 1108.6864,-30.5767 1105.0825,-27.546 1112.1844,-30.4592 1112.1844,-30.4592\" stroke=\"#000000\"/>\n",
1030
1031
       "</g>\n",
       "<!-- 10&#45;&gt;14 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1032
1033
1034
1035
       "<g class=\"edge\" id=\"edge22\">\n",
       "<title>10-&gt;14</title>\n",
       "<path d=\"M1064.3403,-116.8701C1074.668,-116.8701 1085.1642,-116.8701 1095.5752,-116.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1102.7661,-116.8701 1095.7662,-120.0202 1099.2661,-116.8701 1095.7661,-116.8702 1095.7661,-116.8702 1095.7661,-116.8702 1099.2661,-116.8701 1095.7661,-113.7202 1102.7661,-116.8701 1102.7661,-116.8701\" stroke=\"#000000\"/>\n",
1036
1037
       "</g>\n",
       "<!-- 10&#45;&gt;15 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1038
1039
1040
1041
       "<g class=\"edge\" id=\"edge23\">\n",
       "<title>10-&gt;15</title>\n",
       "<path d=\"M1016.645,-94.8536C1056.4152,-81.4945 1107.1826,-64.4413 1147.9219,-50.7567\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1154.6289,-48.5038 1148.9963,-53.7189 1151.3111,-49.6183 1147.9933,-50.7328 1147.9933,-50.7328 1147.9933,-50.7328 1151.3111,-49.6183 1146.9902,-47.7468 1154.6289,-48.5038 1154.6289,-48.5038\" stroke=\"#000000\"/>\n",
1042
1043
       "</g>\n",
       "<!-- 11&#45;&gt;11 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1044
1045
1046
1047
       "<g class=\"edge\" id=\"edge24\">\n",
       "<title>11-&gt;11</title>\n",
       "<path d=\"M1169.9371,-357.3317C1165.2613,-368.2753 1181.6265,-377.7401 1219.0328,-377.7401 1247.6719,-377.7401 1263.9772,-372.192 1267.9487,-364.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1268.1285,-357.3317 1271.1062,-364.4067 1268.0428,-360.8306 1267.9571,-364.3296 1267.9571,-364.3296 1267.9571,-364.3296 1268.0428,-360.8306 1264.8081,-364.2525 1268.1285,-357.3317 1268.1285,-357.3317\" stroke=\"#000000\"/>\n",
1048
1049
       "</g>\n",
       "<!-- 16 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1050
1051
1052
1053
1054
       "<g class=\"node\" id=\"node18\">\n",
       "<title>16</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-336.6701\">a=3, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1412.9638\" y=\"-321.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1055
1056
       "</g>\n",
       "<!-- 12&#45;&gt;16 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1057
1058
1059
1060
       "<g class=\"edge\" id=\"edge25\">\n",
       "<title>12-&gt;16</title>\n",
       "<path d=\"M1295.0944,-281.3098C1329.1792,-290.4693 1369.4566,-301.2928 1404.2862,-310.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1411.1761,-312.5039 1403.5984,-313.7293 1407.796,-311.5956 1404.4159,-310.6872 1404.4159,-310.6872 1404.4159,-310.6872 1407.796,-311.5956 1405.2334,-307.6452 1411.1761,-312.5039 1411.1761,-312.5039\" stroke=\"#000000\"/>\n",
1061
1062
       "</g>\n",
       "<!-- 17 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1063
1064
1065
1066
1067
       "<g class=\"node\" id=\"node19\">\n",
       "<title>17</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-192.6701\">a=2, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1414.9638\" y=\"-177.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
1068
1069
       "</g>\n",
       "<!-- 12&#45;&gt;17 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1070
1071
1072
1073
       "<g class=\"edge\" id=\"edge26\">\n",
       "<title>12-&gt;17</title>\n",
       "<path d=\"M1295.0944,-240.4303C1329.3242,-231.2319 1369.7995,-220.3551 1404.7305,-210.9683\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1411.6393,-209.1117 1405.6967,-213.9705 1408.2593,-210.02 1404.8792,-210.9284 1404.8792,-210.9284 1404.8792,-210.9284 1408.2593,-210.02 1404.0617,-207.8863 1411.6393,-209.1117 1411.6393,-209.1117\" stroke=\"#000000\"/>\n",
1074
1075
       "</g>\n",
       "<!-- 18 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1076
1077
1078
1079
1080
       "<g class=\"node\" id=\"node20\">\n",
       "<title>18</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-264.6701\">a=2, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1412.9638\" y=\"-249.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1081
1082
       "</g>\n",
       "<!-- 12&#45;&gt;18 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1083
1084
1085
1086
       "<g class=\"edge\" id=\"edge27\">\n",
       "<title>12-&gt;18</title>\n",
       "<path d=\"M1331.4951,-254.1979C1343.3466,-254.1114 1355.4287,-254.097 1367.3571,-254.1546\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1374.3598,-254.1969 1367.3408,-257.3045 1370.8598,-254.1757 1367.3599,-254.1546 1367.3599,-254.1546 1367.3599,-254.1546 1370.8598,-254.1757 1367.379,-251.0046 1374.3598,-254.1969 1374.3598,-254.1969\" stroke=\"#000000\"/>\n",
1087
1088
       "</g>\n",
       "<!-- 19 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1089
1090
1091
1092
1093
       "<g class=\"node\" id=\"node21\">\n",
       "<title>19</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-98.8701\" fill=\"#ffffaa\" rx=\"110.1176\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-102.6701\">a=1, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1416.9638\" y=\"-87.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
1094
1095
       "</g>\n",
       "<!-- 13&#45;&gt;19 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1096
1097
1098
1099
       "<g class=\"edge\" id=\"edge28\">\n",
       "<title>13-&gt;19</title>\n",
       "<path d=\"M1289.087,-167.6232C1304.2622,-162.8811 1320.1964,-157.7952 1334.9983,-152.8701 1362.5563,-143.7004 1392.7319,-133.0958 1418.8792,-123.7247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1425.7876,-121.2438 1420.2641,-126.5743 1422.4936,-122.4268 1419.1995,-123.6097 1419.1995,-123.6097 1419.1995,-123.6097 1422.4936,-122.4268 1418.1349,-120.645 1425.7876,-121.2438 1425.7876,-121.2438\" stroke=\"#000000\"/>\n",
1100
1101
       "</g>\n",
       "<!-- 14&#45;&gt;18 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1102
1103
1104
1105
       "<g class=\"edge\" id=\"edge29\">\n",
       "<title>14-&gt;18</title>\n",
       "<path d=\"M1305.4887,-134.9763C1316.1455,-139.6391 1326.3216,-145.5011 1334.9983,-152.8701 1362.2679,-176.0296 1343.7286,-201.7105 1370.9983,-224.8701 1377.9125,-230.7422 1385.7788,-235.6574 1394.0818,-239.7714\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1400.5078,-242.7638 1392.8323,-242.6643 1397.335,-241.2863 1394.1621,-239.8087 1394.1621,-239.8087 1394.1621,-239.8087 1397.335,-241.2863 1395.4919,-236.9532 1400.5078,-242.7638 1400.5078,-242.7638\" stroke=\"#000000\"/>\n",
1106
1107
       "</g>\n",
       "<!-- 14&#45;&gt;19 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1108
1109
1110
1111
       "<g class=\"edge\" id=\"edge30\">\n",
       "<title>14-&gt;19</title>\n",
       "<path d=\"M1330.7195,-109.3668C1344.7811,-108.4221 1359.1795,-107.4548 1373.2717,-106.5081\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1380.6096,-106.0151 1373.8365,-109.6273 1377.1175,-106.2497 1373.6253,-106.4844 1373.6253,-106.4844 1373.6253,-106.4844 1377.1175,-106.2497 1373.4141,-103.3415 1380.6096,-106.0151 1380.6096,-106.0151\" stroke=\"#000000\"/>\n",
1112
1113
       "</g>\n",
       "<!-- 15&#45;&gt;15 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1114
1115
1116
1117
       "<g class=\"edge\" id=\"edge31\">\n",
       "<title>15-&gt;15</title>\n",
       "<path d=\"M1170.1441,-50.8749C1164.8107,-62.0106 1181.107,-71.7401 1219.0328,-71.7401 1248.6623,-71.7401 1265.0902,-65.8017 1268.3164,-57.8937\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1267.9215,-50.8749 1271.4599,-57.6868 1268.1181,-54.3693 1268.3148,-57.8638 1268.3148,-57.8638 1268.3148,-57.8638 1268.1181,-54.3693 1265.1698,-58.0408 1267.9215,-50.8749 1267.9215,-50.8749\" stroke=\"#000000\"/>\n",
1118
1119
       "</g>\n",
       "<!-- 20 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1120
1121
1122
1123
1124
       "<g class=\"node\" id=\"node22\">\n",
       "<title>20</title>\n",
       "<ellipse cx=\"1754.8948\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1709.8948\" y=\"-336.6701\">a=3, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1680.8948\" y=\"-321.6701\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1125
1126
       "</g>\n",
       "<!-- 16&#45;&gt;20 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1127
1128
1129
1130
       "<g class=\"edge\" id=\"edge32\">\n",
       "<title>16-&gt;20</title>\n",
       "<path d=\"M1599.4261,-326.1979C1611.2776,-326.1114 1623.3597,-326.097 1635.2882,-326.1546\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1642.2908,-326.1969 1635.2719,-329.3045 1638.7909,-326.1757 1635.2909,-326.1546 1635.2909,-326.1546 1635.2909,-326.1546 1638.7909,-326.1757 1635.31,-323.0046 1642.2908,-326.1969 1642.2908,-326.1969\" stroke=\"#000000\"/>\n",
1131
1132
       "</g>\n",
       "<!-- 21 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1133
1134
1135
1136
1137
       "<g class=\"node\" id=\"node23\">\n",
       "<title>21</title>\n",
       "<ellipse cx=\"1754.8948\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1709.8948\" y=\"-192.6701\">a=2, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1682.8948\" y=\"-177.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
1138
1139
       "</g>\n",
       "<!-- 17&#45;&gt;21 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1140
1141
1142
1143
       "<g class=\"edge\" id=\"edge33\">\n",
       "<title>17-&gt;21</title>\n",
       "<path d=\"M1596.7147,-182.219C1610.2518,-182.1073 1624.1303,-182.0902 1637.772,-182.1677\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1644.881,-182.2169 1637.8594,-185.3183 1641.3811,-182.1926 1637.8812,-182.1684 1637.8812,-182.1684 1637.8812,-182.1684 1641.3811,-182.1926 1637.903,-179.0184 1644.881,-182.2169 1644.881,-182.2169\" stroke=\"#000000\"/>\n",
1144
1145
       "</g>\n",
       "<!-- 18&#45;&gt;12 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1146
1147
1148
1149
       "<g class=\"edge\" id=\"edge36\">\n",
       "<title>18-&gt;12</title>\n",
       "<path d=\"M1374.3598,-267.5432C1362.5064,-267.6292 1350.424,-267.643 1338.4968,-267.5848\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1331.4951,-267.5422 1338.5141,-264.4349 1334.995,-267.5635 1338.4949,-267.5849 1338.4949,-267.5849 1338.4949,-267.5849 1334.995,-267.5635 1338.4757,-270.7348 1331.4951,-267.5422 1331.4951,-267.5422\" stroke=\"#000000\"/>\n",
1150
1151
       "</g>\n",
       "<!-- 18&#45;&gt;20 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1152
1153
1154
1155
       "<g class=\"edge\" id=\"edge34\">\n",
       "<title>18-&gt;20</title>\n",
       "<path d=\"M1563.0254,-281.3098C1597.1102,-290.4693 1637.3876,-301.2928 1672.2172,-310.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1679.1071,-312.5039 1671.5294,-313.7293 1675.727,-311.5956 1672.3469,-310.6872 1672.3469,-310.6872 1672.3469,-310.6872 1675.727,-311.5956 1673.1644,-307.6452 1679.1071,-312.5039 1679.1071,-312.5039\" stroke=\"#000000\"/>\n",
1156
1157
       "</g>\n",
       "<!-- 18&#45;&gt;21 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1158
1159
1160
1161
       "<g class=\"edge\" id=\"edge35\">\n",
       "<title>18-&gt;21</title>\n",
       "<path d=\"M1563.0254,-240.4303C1597.2552,-231.2319 1637.7305,-220.3551 1672.6616,-210.9683\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1679.5704,-209.1117 1673.6277,-213.9705 1676.1903,-210.02 1672.8102,-210.9284 1672.8102,-210.9284 1672.8102,-210.9284 1676.1903,-210.02 1671.9927,-207.8863 1679.5704,-209.1117 1679.5704,-209.1117\" stroke=\"#000000\"/>\n",
1162
1163
       "</g>\n",
       "<!-- 19&#45;&gt;19 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1164
1165
1166
1167
       "<g class=\"edge\" id=\"edge37\">\n",
       "<title>19-&gt;19</title>\n",
       "<path d=\"M1437.8681,-123.3317C1433.1923,-134.2753 1449.5575,-143.7401 1486.9638,-143.7401 1515.6029,-143.7401 1531.9082,-138.192 1535.8797,-130.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1536.0595,-123.3317 1539.0372,-130.4067 1535.9738,-126.8306 1535.8882,-130.3296 1535.8882,-130.3296 1535.8882,-130.3296 1535.9738,-126.8306 1532.7391,-130.2525 1536.0595,-123.3317 1536.0595,-123.3317\" stroke=\"#000000\"/>\n",
1168
1169
       "</g>\n",
       "<!-- 20&#45;&gt;16 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1170
1171
1172
1173
       "<g class=\"edge\" id=\"edge38\">\n",
       "<title>20-&gt;16</title>\n",
       "<path d=\"M1642.2908,-339.5432C1630.4374,-339.6292 1618.3551,-339.643 1606.4278,-339.5848\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1599.4261,-339.5422 1606.4452,-336.4349 1602.926,-339.5635 1606.426,-339.5849 1606.426,-339.5849 1606.426,-339.5849 1602.926,-339.5635 1606.4067,-342.7348 1599.4261,-339.5422 1599.4261,-339.5422\" stroke=\"#000000\"/>\n",
1174
1175
       "</g>\n",
       "<!-- 21&#45;&gt;17 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1176
1177
1178
1179
       "<g class=\"edge\" id=\"edge39\">\n",
       "<title>21-&gt;17</title>\n",
       "<path d=\"M1644.881,-195.5232C1631.3394,-195.6338 1617.4604,-195.6497 1603.8218,-195.5709\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1596.7147,-195.5211 1603.7366,-192.4203 1600.2146,-195.5457 1603.7145,-195.5702 1603.7145,-195.5702 1603.7145,-195.5702 1600.2146,-195.5457 1603.6924,-198.7202 1596.7147,-195.5211 1596.7147,-195.5211\" stroke=\"#000000\"/>\n",
1180
1181
1182
1183
1184
1185
1186
1187
1188
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "execution_count": 11,
1189
     "metadata": {},
1190
1191
1192
1193
1194
1195
1196
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k.show('.<0')  # unlimited output"
   ]
  },
1197
1198
1199
1200
1201
1202
1203
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we have an LTL proposition to check, we can convert it into an automaton using `spot.translate()`, and synchronize that automaton with the Kripke structure using `spot.otf_product()`.  This `otf_product()` function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm \"consumes\" it (here the display routine). "
   ]
  },
1204
1205
1206
  {
   "cell_type": "code",
   "execution_count": 12,
1207
   "metadata": {},
1208
   "outputs": [
1209
    {
1210
1211
1212
1213
1214
     "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
1215
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
1216
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1217
       "<!-- Pages: 1 -->\n",
1218
1219
1220
       "<svg width=\"198pt\" height=\"125pt\"\n",
       " viewBox=\"0.00 0.00 198.00 124.80\" 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 120.8)\">\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1221
1222
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 194,-120.8 194,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"72\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
1223
1224
       "<!-- I -->\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1225
1226
1227
1228
       "<g id=\"node2\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
1229
1230
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1231
1232
1233
1234
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n",
1235
1236
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1237
1238
1239
1240
1241
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
       "<text text-anchor=\"start\" x=\"10.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot;</text>\n",
1242
1243
       "</g>\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1244
1245
1246
1247
1248
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"168\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
       "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"168\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
       "<text text-anchor=\"middle\" x=\"168\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
1249
1250
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1251
1252
1253
1254
1255
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M74.4945,-22C91.8699,-22 118.1605,-22 138.4436,-22\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"145.6169,-22 138.6169,-25.1501 142.1169,-22 138.6169,-22.0001 138.6169,-22.0001 138.6169,-22.0001 142.1169,-22 138.6169,-18.8501 145.6169,-22 145.6169,-22\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;b&gt;2&quot;</text>\n",
1256
1257
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1258
1259
1260
1261
1262
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M157.5737,-41.7575C155.8019,-52.3499 159.2773,-62 168,-62 174.6783,-62 178.2807,-56.3433 178.8074,-48.9379\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"178.4263,-41.7575 181.9429,-48.5807 178.6118,-45.2526 178.7974,-48.7476 178.7974,-48.7476 178.7974,-48.7476 178.6118,-45.2526 175.6518,-48.9146 178.4263,-41.7575 178.4263,-41.7575\"/>\n",
       "<text text-anchor=\"middle\" x=\"168\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
1263
1264
1265
1266
1267
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
1268
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb8f84691e0> >"
1269
1270
1271
      ]
     },
     "execution_count": 12,
1272
     "metadata": {},
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = spot.translate('\"a<1\" U \"b>2\"'); a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
1283
   "metadata": {},
1284
   "outputs": [
1285
    {
1286
1287
1288
1289
1290
     "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
1291
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
1292
       " -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1293
1294
1295
1296
1297
1298
1299
1300
1301
       "<!-- Pages: 1 -->\n",
       "<svg width=\"734pt\" height=\"119pt\"\n",
       " viewBox=\"0.00 0.00 734.00 119.43\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.4593 .4593) rotate(0) translate(4 256)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-256 1593.9262,-256 1593.9262,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"773.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"795.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"811.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"771.9631\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
1302
1303
       "<!-- I -->\n",
       "<!-- 0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1304
1305
1306
1307
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"121.1926\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"65.1926\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=0, Q=0 * 1</text>\n",
1308
1309
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1310
1311
1312
1313
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.2707,-171C4.3,-171 15.9594,-171 30.899,-171\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9747,-171 30.9748,-174.1501 34.4747,-171 30.9747,-171.0001 30.9747,-171.0001 30.9747,-171.0001 34.4747,-171 30.9747,-167.8501 37.9747,-171 37.9747,-171\"/>\n",
1314
1315
       "</g>\n",
       "<!-- 1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1316
1317
1318
1319
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"467.5779\" cy=\"-198\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"411.5779\" y=\"-194.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=0, Q=0 * 1</text>\n",
1320
1321
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1322
1323
1324
1325
1326
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M199.7928,-177.1267C254.1557,-181.3642 326.4549,-186.9998 382.2262,-191.347\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"389.2887,-191.8975 382.0651,-194.4939 385.7993,-191.6255 382.3099,-191.3535 382.3099,-191.3535 382.3099,-191.3535 385.7993,-191.6255 382.5547,-188.213 389.2887,-191.8975 389.2887,-191.8975\"/>\n",
       "<text text-anchor=\"start\" x=\"222.3852\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1327
1328
       "</g>\n",
       "<!-- 2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1329
1330
1331
1332
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"467.5779\" cy=\"-144\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"411.5779\" y=\"-140.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=1, Q=0 * 1</text>\n",
1333
1334
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1335
1336
1337
1338
1339
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M193.2785,-161.9424C203.0521,-160.8635 212.9584,-159.8466 222.3852,-159 274.2017,-154.3465 332.3106,-150.7219 378.9492,-148.2023\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"386.0386,-147.823 379.217,-151.3426 382.5436,-148.0101 379.0486,-148.1971 379.0486,-148.1971 379.0486,-148.1971 382.5436,-148.0101 378.8803,-145.0516 386.0386,-147.823 386.0386,-147.823\"/>\n",
       "<text text-anchor=\"start\" x=\"222.3852\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1340
1341
       "</g>\n",
       "<!-- 3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1342
1343
1344
1345
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"813.9631\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"757.9631\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=1, Q=0 * 1</text>\n",
1346
1347
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1348
1349
1350
1351
1352
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M546.178,-150.1267C600.541,-154.3642 672.8402,-159.9998 728.6114,-164.347\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"735.674,-164.8975 728.4503,-167.4939 732.1846,-164.6255 728.6951,-164.3535 728.6951,-164.3535 728.6951,-164.3535 732.1846,-164.6255 728.94,-161.213 735.674,-164.8975 735.674,-164.8975\"/>\n",
       "<text text-anchor=\"start\" x=\"568.7705\" y=\"-166.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1353
1354
       "</g>\n",
       "<!-- 4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1355
1356
1357
1358
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"813.9631\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"757.9631\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=2, Q=0 * 1</text>\n",
1359
1360
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1361
1362
1363
1364
1365
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M539.6637,-134.9424C549.4373,-133.8635 559.3436,-132.8466 568.7705,-132 620.587,-127.3465 678.6958,-123.7219 725.3344,-121.2023\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"732.4239,-120.823 725.6022,-124.3426 728.9289,-121.0101 725.4339,-121.1971 725.4339,-121.1971 725.4339,-121.1971 728.9289,-121.0101 725.2655,-118.0516 732.4239,-120.823 732.4239,-120.823\"/>\n",
       "<text text-anchor=\"start\" x=\"568.7705\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
1366
1367
       "</g>\n",
       "<!-- 5 -->\n",