1{ 2 "cells": [ 3 { 4 "cell_type": "code", 5 "execution_count": 1, 6 "metadata": {}, 7 "outputs": [], 8 "source": [ 9 "import spot\n", 10 "import spot.ltsmin\n", 11 "# The following line causes the notebook to exit with 77 if divine is not \n", 12 "# installed, therefore skipping this test in the test suite.\n", 13 "spot.ltsmin.require('divine')\n", 14 "# This notebook also tests the limitation of the number of states in the GraphViz output\n", 15 "spot.setup(max_states=10)" 16 ] 17 }, 18 { 19 "cell_type": "markdown", 20 "metadata": {}, 21 "source": [ 22 "There are two ways to load a DiVinE model: from a file or from a cell. \n", 23 "\n", 24 "Loading from a file\n", 25 "-------------------\n", 26 "\n", 27 "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." 28 ] 29 }, 30 { 31 "cell_type": "code", 32 "execution_count": 2, 33 "metadata": {}, 34 "outputs": [], 35 "source": [ 36 "!rm -f test1.dve" 37 ] 38 }, 39 { 40 "cell_type": "code", 41 "execution_count": 3, 42 "metadata": {}, 43 "outputs": [ 44 { 45 "name": "stdout", 46 "output_type": "stream", 47 "text": [ 48 "Writing test1.dve\n" 49 ] 50 } 51 ], 52 "source": [ 53 "%%file test1.dve\n", 54 "int a = 0, b = 0;\n", 55 "\n", 56 "process P {\n", 57 " state x;\n", 58 " init x;\n", 59 "\n", 60 " trans\n", 61 " x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n", 62 " x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n", 63 "}\n", 64 "\n", 65 "process Q {\n", 66 " state wait, work;\n", 67 " init wait;\n", 68 " trans\n", 69 " wait -> work { guard b > 1; },\n", 70 " work -> wait { guard a > 1; };\n", 71 "}\n", 72 "\n", 73 "system async;" 74 ] 75 }, 76 { 77 "cell_type": "markdown", 78 "metadata": {}, 79 "source": [ 80 "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." 81 ] 82 }, 83 { 84 "cell_type": "code", 85 "execution_count": 4, 86 "metadata": {}, 87 "outputs": [], 88 "source": [ 89 "m = spot.ltsmin.load('test1.dve')" 90 ] 91 }, 92 { 93 "cell_type": "markdown", 94 "metadata": {}, 95 "source": [ 96 "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", 97 "\n", 98 "For editing and loading DVE file from a notebook, it is a better to use the `%%dve` as shown next." 99 ] 100 }, 101 { 102 "cell_type": "code", 103 "execution_count": 5, 104 "metadata": {}, 105 "outputs": [], 106 "source": [ 107 "!rm -f test1.dve test1.dve.cpp test1.dve2C" 108 ] 109 }, 110 { 111 "cell_type": "markdown", 112 "metadata": {}, 113 "source": [ 114 "Loading from a notebook cell\n", 115 "----------------------------\n", 116 "\n", 117 "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`." 118 ] 119 }, 120 { 121 "cell_type": "code", 122 "execution_count": 6, 123 "metadata": {}, 124 "outputs": [], 125 "source": [ 126 "%%dve m\n", 127 "int a = 0, b = 0;\n", 128 "\n", 129 "process P {\n", 130 " state x;\n", 131 " init x;\n", 132 "\n", 133 " trans\n", 134 " x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n", 135 " x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n", 136 "}\n", 137 "\n", 138 "process Q {\n", 139 " state wait, work;\n", 140 " init wait;\n", 141 " trans\n", 142 " wait -> work { guard b > 1; },\n", 143 " work -> wait { guard a > 1; };\n", 144 "}\n", 145 "\n", 146 "system async;" 147 ] 148 }, 149 { 150 "cell_type": "markdown", 151 "metadata": {}, 152 "source": [ 153 "Working with an ltsmin model\n", 154 "----------------------------\n", 155 "\n", 156 "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." 157 ] 158 }, 159 { 160 "cell_type": "code", 161 "execution_count": 7, 162 "metadata": {}, 163 "outputs": [ 164 { 165 "data": { 166 "text/plain": [ 167 "ltsmin model with the following variables:\n", 168 " a: int\n", 169 " b: int\n", 170 " P: ['x']\n", 171 " Q: ['wait', 'work']" 172 ] 173 }, 174 "execution_count": 7, 175 "metadata": {}, 176 "output_type": "execute_result" 177 } 178 ], 179 "source": [ 180 "m" 181 ] 182 }, 183 { 184 "cell_type": "code", 185 "execution_count": 8, 186 "metadata": {}, 187 "outputs": [ 188 { 189 "data": { 190 "text/plain": [ 191 "[('state_size', 4),\n", 192 " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n", 193 " ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]" 194 ] 195 }, 196 "execution_count": 8, 197 "metadata": {}, 198 "output_type": "execute_result" 199 } 200 ], 201 "source": [ 202 "sorted(m.info().items())" 203 ] 204 }, 205 { 206 "cell_type": "markdown", 207 "metadata": {}, 208 "source": [ 209 "To obtain a Kripke structure, call `kripke` and supply a list of atomic propositions to observe in the model." 210 ] 211 }, 212 { 213 "cell_type": "code", 214 "execution_count": 9, 215 "metadata": {}, 216 "outputs": [ 217 { 218 "data": { 219 "image/svg+xml": [ 220 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 221 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 222 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 223 "<!-- Generated by graphviz version 2.43.0 (0)\n", 224 " -->\n", 225 "<!-- Pages: 1 -->\n", 226 "<svg width=\"734pt\" height=\"270pt\"\n", 227 " viewBox=\"0.00 0.00 734.00 270.38\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 228 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8695652173913044 0.8695652173913044) rotate(0) translate(4 308)\">\n", 229 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-308 843,-308 843,4 -4,4\"/>\n", 230 "<text text-anchor=\"start\" x=\"416.5\" y=\"-288.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n", 231 "<text text-anchor=\"start\" x=\"408.5\" y=\"-273.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n", 232 "<!-- I -->\n", 233 "<!-- 0 -->\n", 234 "<g id=\"node2\" class=\"node\">\n", 235 "<title>0</title>\n", 236 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M181,-143C181,-143 49,-143 49,-143 43,-143 37,-137 37,-131 37,-131 37,-117 37,-117 37,-111 43,-105 49,-105 49,-105 181,-105 181,-105 187,-105 193,-111 193,-117 193,-117 193,-131 193,-131 193,-137 187,-143 181,-143\"/>\n", 237 "<text text-anchor=\"start\" x=\"70.5\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n", 238 "<text text-anchor=\"start\" x=\"45\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 239 "</g>\n", 240 "<!-- I->0 -->\n", 241 "<g id=\"edge1\" class=\"edge\">\n", 242 "<title>I->0</title>\n", 243 "<path fill=\"none\" stroke=\"black\" d=\"M1.08,-124C2.17,-124 13.89,-124 29.41,-124\"/>\n", 244 "<polygon fill=\"black\" stroke=\"black\" points=\"36.78,-124 29.78,-127.15 33.28,-124 29.78,-124 29.78,-124 29.78,-124 33.28,-124 29.78,-120.85 36.78,-124 36.78,-124\"/>\n", 245 "</g>\n", 246 "<!-- 1 -->\n", 247 "<g id=\"node3\" class=\"node\">\n", 248 "<title>1</title>\n", 249 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M377,-171C377,-171 241,-171 241,-171 235,-171 229,-165 229,-159 229,-159 229,-145 229,-145 229,-139 235,-133 241,-133 241,-133 377,-133 377,-133 383,-133 389,-139 389,-145 389,-145 389,-159 389,-159 389,-165 383,-171 377,-171\"/>\n", 250 "<text text-anchor=\"start\" x=\"264.5\" y=\"-155.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n", 251 "<text text-anchor=\"start\" x=\"237\" y=\"-140.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 252 "</g>\n", 253 "<!-- 0->1 -->\n", 254 "<g id=\"edge2\" class=\"edge\">\n", 255 "<title>0->1</title>\n", 256 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-135.27C202.56,-136.62 212.11,-138.02 221.53,-139.39\"/>\n", 257 "<polygon fill=\"black\" stroke=\"black\" points=\"228.7,-140.44 221.32,-142.54 225.24,-139.93 221.78,-139.43 221.78,-139.43 221.78,-139.43 225.24,-139.93 222.23,-136.31 228.7,-140.44 228.7,-140.44\"/>\n", 258 "</g>\n", 259 "<!-- 2 -->\n", 260 "<g id=\"node4\" class=\"node\">\n", 261 "<title>2</title>\n", 262 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M375,-115C375,-115 243,-115 243,-115 237,-115 231,-109 231,-103 231,-103 231,-89 231,-89 231,-83 237,-77 243,-77 243,-77 375,-77 375,-77 381,-77 387,-83 387,-89 387,-89 387,-103 387,-103 387,-109 381,-115 375,-115\"/>\n", 263 "<text text-anchor=\"start\" x=\"264.5\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n", 264 "<text text-anchor=\"start\" x=\"239\" y=\"-84.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 265 "</g>\n", 266 "<!-- 0->2 -->\n", 267 "<g id=\"edge3\" class=\"edge\">\n", 268 "<title>0->2</title>\n", 269 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-112.73C203.34,-111.26 213.7,-109.75 223.88,-108.27\"/>\n", 270 "<polygon fill=\"black\" stroke=\"black\" points=\"230.89,-107.24 224.42,-111.37 227.43,-107.75 223.97,-108.25 223.97,-108.25 223.97,-108.25 227.43,-107.75 223.51,-105.14 230.89,-107.24 230.89,-107.24\"/>\n", 271 "</g>\n", 272 "<!-- 3 -->\n", 273 "<g id=\"node5\" class=\"node\">\n", 274 "<title>3</title>\n", 275 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-199C573,-199 437,-199 437,-199 431,-199 425,-193 425,-187 425,-187 425,-173 425,-173 425,-167 431,-161 437,-161 437,-161 573,-161 573,-161 579,-161 585,-167 585,-173 585,-173 585,-187 585,-187 585,-193 579,-199 573,-199\"/>\n", 276 "<text text-anchor=\"start\" x=\"460.5\" y=\"-183.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n", 277 "<text text-anchor=\"start\" x=\"433\" y=\"-168.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 278 "</g>\n", 279 "<!-- 1->3 -->\n", 280 "<g id=\"edge4\" class=\"edge\">\n", 281 "<title>1->3</title>\n", 282 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-163.43C398.54,-164.78 408.12,-166.16 417.56,-167.52\"/>\n", 283 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-168.56 417.37,-170.68 421.29,-168.06 417.82,-167.56 417.82,-167.56 417.82,-167.56 421.29,-168.06 418.27,-164.44 424.75,-168.56 424.75,-168.56\"/>\n", 284 "</g>\n", 285 "<!-- 4 -->\n", 286 "<g id=\"node6\" class=\"node\">\n", 287 "<title>4</title>\n", 288 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-143C573,-143 437,-143 437,-143 431,-143 425,-137 425,-131 425,-131 425,-117 425,-117 425,-111 431,-105 437,-105 437,-105 573,-105 573,-105 579,-105 585,-111 585,-117 585,-117 585,-131 585,-131 585,-137 579,-143 573,-143\"/>\n", 289 "<text text-anchor=\"start\" x=\"460.5\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n", 290 "<text text-anchor=\"start\" x=\"433\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 291 "</g>\n", 292 "<!-- 1->4 -->\n", 293 "<g id=\"edge5\" class=\"edge\">\n", 294 "<title>1->4</title>\n", 295 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-140.57C398.54,-139.22 408.12,-137.84 417.56,-136.48\"/>\n", 296 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-135.44 418.27,-139.56 421.29,-135.94 417.82,-136.44 417.82,-136.44 417.82,-136.44 421.29,-135.94 417.37,-133.32 424.75,-135.44 424.75,-135.44\"/>\n", 297 "</g>\n", 298 "<!-- 2->4 -->\n", 299 "<g id=\"edge6\" class=\"edge\">\n", 300 "<title>2->4</title>\n", 301 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-107.15C397.28,-108.6 407.62,-110.09 417.8,-111.56\"/>\n", 302 "<polygon fill=\"black\" stroke=\"black\" points=\"424.81,-112.57 417.43,-114.69 421.35,-112.07 417.88,-111.57 417.88,-111.57 417.88,-111.57 421.35,-112.07 418.33,-108.45 424.81,-112.57 424.81,-112.57\"/>\n", 303 "</g>\n", 304 "<!-- 5 -->\n", 305 "<g id=\"node7\" class=\"node\">\n", 306 "<title>5</title>\n", 307 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M571,-87C571,-87 439,-87 439,-87 433,-87 427,-81 427,-75 427,-75 427,-61 427,-61 427,-55 433,-49 439,-49 439,-49 571,-49 571,-49 577,-49 583,-55 583,-61 583,-61 583,-75 583,-75 583,-81 577,-87 571,-87\"/>\n", 308 "<text text-anchor=\"start\" x=\"460.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n", 309 "<text text-anchor=\"start\" x=\"435\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 310 "</g>\n", 311 "<!-- 2->5 -->\n", 312 "<g id=\"edge7\" class=\"edge\">\n", 313 "<title>2->5</title>\n", 314 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-84.85C397.89,-83.31 408.89,-81.73 419.67,-80.17\"/>\n", 315 "<polygon fill=\"black\" stroke=\"black\" points=\"426.72,-79.15 420.24,-83.27 423.25,-79.65 419.79,-80.15 419.79,-80.15 419.79,-80.15 423.25,-79.65 419.34,-77.04 426.72,-79.15 426.72,-79.15\"/>\n", 316 "</g>\n", 317 "<!-- 6 -->\n", 318 "<g id=\"node8\" class=\"node\">\n", 319 "<title>6</title>\n", 320 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M765,-248C765,-248 633,-248 633,-248 627,-248 621,-242 621,-236 621,-236 621,-222 621,-222 621,-216 627,-210 633,-210 633,-210 765,-210 765,-210 771,-210 777,-216 777,-222 777,-222 777,-236 777,-236 777,-242 771,-248 765,-248\"/>\n", 321 "<text text-anchor=\"start\" x=\"654.5\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n", 322 "<text text-anchor=\"start\" x=\"629\" y=\"-217.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 323 "</g>\n", 324 "<!-- 3->6 -->\n", 325 "<g id=\"edge8\" class=\"edge\">\n", 326 "<title>3->6</title>\n", 327 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-199.01C592.31,-202.03 604.58,-205.16 616.54,-208.21\"/>\n", 328 "<polygon fill=\"black\" stroke=\"black\" points=\"623.53,-210 615.97,-211.32 620.14,-209.13 616.75,-208.26 616.75,-208.26 616.75,-208.26 620.14,-209.13 617.53,-205.21 623.53,-210 623.53,-210\"/>\n", 329 "</g>\n", 330 "<!-- 7 -->\n", 331 "<g id=\"node9\" class=\"node\">\n", 332 "<title>7</title>\n", 333 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-192C739.5,-192 658.5,-192 658.5,-192 652.5,-192 646.5,-186 646.5,-180 646.5,-180 646.5,-166 646.5,-166 646.5,-160 652.5,-154 658.5,-154 658.5,-154 739.5,-154 739.5,-154 745.5,-154 751.5,-160 751.5,-166 751.5,-166 751.5,-180 751.5,-180 751.5,-186 745.5,-192 739.5,-192\"/>\n", 334 "<text text-anchor=\"start\" x=\"654.5\" y=\"-176.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n", 335 "<text text-anchor=\"start\" x=\"694\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 336 "</g>\n", 337 "<!-- 3->7 -->\n", 338 "<g id=\"edge9\" class=\"edge\">\n", 339 "<title>3->7</title>\n", 340 "<path fill=\"none\" stroke=\"black\" d=\"M585.2,-177.11C603.28,-176.45 622.18,-175.76 639.22,-175.14\"/>\n", 341 "<polygon fill=\"black\" stroke=\"black\" points=\"646.41,-174.88 639.52,-178.28 642.91,-175.01 639.41,-175.14 639.41,-175.14 639.41,-175.14 642.91,-175.01 639.3,-171.99 646.41,-174.88 646.41,-174.88\"/>\n", 342 "</g>\n", 343 "<!-- 4->7 -->\n", 344 "<g id=\"edge10\" class=\"edge\">\n", 345 "<title>4->7</title>\n", 346 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-143.01C599.96,-147.98 620.65,-153.26 639.16,-157.98\"/>\n", 347 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-159.83 638.84,-161.15 643.01,-158.97 639.62,-158.1 639.62,-158.1 639.62,-158.1 643.01,-158.97 640.4,-155.05 646.4,-159.83 646.4,-159.83\"/>\n", 348 "</g>\n", 349 "<!-- 8 -->\n", 350 "<g id=\"node10\" class=\"node\">\n", 351 "<title>8</title>\n", 352 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-136C739.5,-136 658.5,-136 658.5,-136 652.5,-136 646.5,-130 646.5,-124 646.5,-124 646.5,-110 646.5,-110 646.5,-104 652.5,-98 658.5,-98 658.5,-98 739.5,-98 739.5,-98 745.5,-98 751.5,-104 751.5,-110 751.5,-110 751.5,-124 751.5,-124 751.5,-130 745.5,-136 739.5,-136\"/>\n", 353 "<text text-anchor=\"start\" x=\"654.5\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n", 354 "<text text-anchor=\"start\" x=\"694\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 355 "</g>\n", 356 "<!-- 4->8 -->\n", 357 "<g id=\"edge11\" class=\"edge\">\n", 358 "<title>4->8</title>\n", 359 "<path fill=\"none\" stroke=\"black\" d=\"M585.2,-121.11C603.28,-120.45 622.18,-119.76 639.22,-119.14\"/>\n", 360 "<polygon fill=\"black\" stroke=\"black\" points=\"646.41,-118.88 639.52,-122.28 642.91,-119.01 639.41,-119.14 639.41,-119.14 639.41,-119.14 642.91,-119.01 639.3,-115.99 646.41,-118.88 646.41,-118.88\"/>\n", 361 "</g>\n", 362 "<!-- 5->8 -->\n", 363 "<g id=\"edge13\" class=\"edge\">\n", 364 "<title>5->8</title>\n", 365 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-87.01C599.96,-91.98 620.65,-97.26 639.16,-101.98\"/>\n", 366 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-103.83 638.84,-105.15 643.01,-102.97 639.62,-102.1 639.62,-102.1 639.62,-102.1 643.01,-102.97 640.4,-99.05 646.4,-103.83 646.4,-103.83\"/>\n", 367 "</g>\n", 368 "<!-- u5 -->\n", 369 "<g id=\"node11\" class=\"node\">\n", 370 "<title>u5</title>\n", 371 "<g id=\"a_node11\"><a xlink:title=\"hidden successors\">\n", 372 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M704.33,-79.5C704.33,-79.5 693.67,-79.5 693.67,-79.5 689.83,-79.5 686,-75.67 686,-71.83 686,-71.83 686,-64.17 686,-64.17 686,-60.33 689.83,-56.5 693.67,-56.5 693.67,-56.5 704.33,-56.5 704.33,-56.5 708.17,-56.5 712,-60.33 712,-64.17 712,-64.17 712,-71.83 712,-71.83 712,-75.67 708.17,-79.5 704.33,-79.5\"/>\n", 373 "<text text-anchor=\"middle\" x=\"699\" y=\"-64.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 374 "</a>\n", 375 "</g>\n", 376 "</g>\n", 377 "<!-- 5->u5 -->\n", 378 "<g id=\"edge12\" class=\"edge\">\n", 379 "<title>5->u5</title>\n", 380 "<g id=\"a_edge12\"><a xlink:title=\"hidden successors\">\n", 381 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M583.26,-68C618.13,-68 656.42,-68 678.77,-68\"/>\n", 382 "<polygon fill=\"black\" stroke=\"black\" points=\"685.98,-68 678.98,-71.15 682.48,-68 678.98,-68 678.98,-68 678.98,-68 682.48,-68 678.98,-64.85 685.98,-68 685.98,-68\"/>\n", 383 "</a>\n", 384 "</g>\n", 385 "</g>\n", 386 "<!-- 9 -->\n", 387 "<g id=\"node12\" class=\"node\">\n", 388 "<title>9</title>\n", 389 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-38C739.5,-38 658.5,-38 658.5,-38 652.5,-38 646.5,-32 646.5,-26 646.5,-26 646.5,-12 646.5,-12 646.5,-6 652.5,0 658.5,0 658.5,0 739.5,0 739.5,0 745.5,0 751.5,-6 751.5,-12 751.5,-12 751.5,-26 751.5,-26 751.5,-32 745.5,-38 739.5,-38\"/>\n", 390 "<text text-anchor=\"start\" x=\"654.5\" y=\"-22.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n", 391 "<text text-anchor=\"start\" x=\"694\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 392 "</g>\n", 393 "<!-- 5->9 -->\n", 394 "<g id=\"edge14\" class=\"edge\">\n", 395 "<title>5->9</title>\n", 396 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-48.99C599.96,-44.02 620.65,-38.74 639.16,-34.02\"/>\n", 397 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-32.17 640.4,-36.95 643.01,-33.03 639.62,-33.9 639.62,-33.9 639.62,-33.9 643.01,-33.03 638.84,-30.85 646.4,-32.17 646.4,-32.17\"/>\n", 398 "</g>\n", 399 "<!-- 6->6 -->\n", 400 "<g id=\"edge15\" class=\"edge\">\n", 401 "<title>6->6</title>\n", 402 "<path fill=\"none\" stroke=\"black\" d=\"M676.07,-248.04C672.9,-257.53 680.54,-266 699,-266 712.55,-266 720.28,-261.43 722.17,-255.25\"/>\n", 403 "<polygon fill=\"black\" stroke=\"black\" points=\"721.93,-248.04 725.31,-254.93 722.04,-251.54 722.16,-255.03 722.16,-255.03 722.16,-255.03 722.04,-251.54 719.01,-255.14 721.93,-248.04 721.93,-248.04\"/>\n", 404 "</g>\n", 405 "<!-- u7 -->\n", 406 "<g id=\"node13\" class=\"node\">\n", 407 "<title>u7</title>\n", 408 "<g id=\"a_node13\"><a xlink:title=\"hidden successors\">\n", 409 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-184.5C831.33,-184.5 820.67,-184.5 820.67,-184.5 816.83,-184.5 813,-180.67 813,-176.83 813,-176.83 813,-169.17 813,-169.17 813,-165.33 816.83,-161.5 820.67,-161.5 820.67,-161.5 831.33,-161.5 831.33,-161.5 835.17,-161.5 839,-165.33 839,-169.17 839,-169.17 839,-176.83 839,-176.83 839,-180.67 835.17,-184.5 831.33,-184.5\"/>\n", 410 "<text text-anchor=\"middle\" x=\"826\" y=\"-169.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 411 "</a>\n", 412 "</g>\n", 413 "</g>\n", 414 "<!-- 7->u7 -->\n", 415 "<g id=\"edge16\" class=\"edge\">\n", 416 "<title>7->u7</title>\n", 417 "<g id=\"a_edge16\"><a xlink:title=\"hidden successors\">\n", 418 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-173C770.63,-173 791.1,-173 805.57,-173\"/>\n", 419 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-173 805.94,-176.15 809.44,-173 805.94,-173 805.94,-173 805.94,-173 809.44,-173 805.94,-169.85 812.94,-173 812.94,-173\"/>\n", 420 "</a>\n", 421 "</g>\n", 422 "</g>\n", 423 "<!-- u8 -->\n", 424 "<g id=\"node14\" class=\"node\">\n", 425 "<title>u8</title>\n", 426 "<g id=\"a_node14\"><a xlink:title=\"hidden successors\">\n", 427 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-128.5C831.33,-128.5 820.67,-128.5 820.67,-128.5 816.83,-128.5 813,-124.67 813,-120.83 813,-120.83 813,-113.17 813,-113.17 813,-109.33 816.83,-105.5 820.67,-105.5 820.67,-105.5 831.33,-105.5 831.33,-105.5 835.17,-105.5 839,-109.33 839,-113.17 839,-113.17 839,-120.83 839,-120.83 839,-124.67 835.17,-128.5 831.33,-128.5\"/>\n", 428 "<text text-anchor=\"middle\" x=\"826\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 429 "</a>\n", 430 "</g>\n", 431 "</g>\n", 432 "<!-- 8->u8 -->\n", 433 "<g id=\"edge17\" class=\"edge\">\n", 434 "<title>8->u8</title>\n", 435 "<g id=\"a_edge17\"><a xlink:title=\"hidden successors\">\n", 436 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-117C770.63,-117 791.1,-117 805.57,-117\"/>\n", 437 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-117 805.94,-120.15 809.44,-117 805.94,-117 805.94,-117 805.94,-117 809.44,-117 805.94,-113.85 812.94,-117 812.94,-117\"/>\n", 438 "</a>\n", 439 "</g>\n", 440 "</g>\n", 441 "<!-- u9 -->\n", 442 "<g id=\"node15\" class=\"node\">\n", 443 "<title>u9</title>\n", 444 "<g id=\"a_node15\"><a xlink:title=\"hidden successors\">\n", 445 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-30.5C831.33,-30.5 820.67,-30.5 820.67,-30.5 816.83,-30.5 813,-26.67 813,-22.83 813,-22.83 813,-15.17 813,-15.17 813,-11.33 816.83,-7.5 820.67,-7.5 820.67,-7.5 831.33,-7.5 831.33,-7.5 835.17,-7.5 839,-11.33 839,-15.17 839,-15.17 839,-22.83 839,-22.83 839,-26.67 835.17,-30.5 831.33,-30.5\"/>\n", 446 "<text text-anchor=\"middle\" x=\"826\" y=\"-15.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 447 "</a>\n", 448 "</g>\n", 449 "</g>\n", 450 "<!-- 9->u9 -->\n", 451 "<g id=\"edge18\" class=\"edge\">\n", 452 "<title>9->u9</title>\n", 453 "<g id=\"a_edge18\"><a xlink:title=\"hidden successors\">\n", 454 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-19C770.63,-19 791.1,-19 805.57,-19\"/>\n", 455 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-19 805.94,-22.15 809.44,-19 805.94,-19 805.94,-19 805.94,-19 809.44,-19 805.94,-15.85 812.94,-19 812.94,-19\"/>\n", 456 "</a>\n", 457 "</g>\n", 458 "</g>\n", 459 "</g>\n", 460 "</svg>\n" 461 ], 462 "text/plain": [ 463 "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fe6bc6afba0> >" 464 ] 465 }, 466 "execution_count": 9, 467 "metadata": {}, 468 "output_type": "execute_result" 469 } 470 ], 471 "source": [ 472 "k = m.kripke([\"a<1\", \"b>2\"])\n", 473 "k" 474 ] 475 }, 476 { 477 "cell_type": "code", 478 "execution_count": 10, 479 "metadata": {}, 480 "outputs": [ 481 { 482 "data": { 483 "image/svg+xml": [ 484 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 485 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 486 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 487 "<!-- Generated by graphviz version 2.43.0 (0)\n", 488 " -->\n", 489 "<!-- Pages: 1 -->\n", 490 "<svg width=\"734pt\" height=\"248pt\"\n", 491 " viewBox=\"0.00 0.00 734.00 248.07\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 492 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7042253521126761 0.7042253521126761) rotate(0) translate(4 348.5)\">\n", 493 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348.5 1039,-348.5 1039,4 -4,4\"/>\n", 494 "<text text-anchor=\"start\" x=\"514.5\" y=\"-329.3\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n", 495 "<text text-anchor=\"start\" x=\"506.5\" y=\"-314.3\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n", 496 "<!-- I -->\n", 497 "<!-- 0 -->\n", 498 "<g id=\"node2\" class=\"node\">\n", 499 "<title>0</title>\n", 500 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M181,-176.5C181,-176.5 49,-176.5 49,-176.5 43,-176.5 37,-170.5 37,-164.5 37,-164.5 37,-150.5 37,-150.5 37,-144.5 43,-138.5 49,-138.5 49,-138.5 181,-138.5 181,-138.5 187,-138.5 193,-144.5 193,-150.5 193,-150.5 193,-164.5 193,-164.5 193,-170.5 187,-176.5 181,-176.5\"/>\n", 501 "<text text-anchor=\"start\" x=\"70.5\" y=\"-161.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n", 502 "<text text-anchor=\"start\" x=\"45\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 503 "</g>\n", 504 "<!-- I->0 -->\n", 505 "<g id=\"edge1\" class=\"edge\">\n", 506 "<title>I->0</title>\n", 507 "<path fill=\"none\" stroke=\"black\" d=\"M1.08,-157.5C2.17,-157.5 13.89,-157.5 29.41,-157.5\"/>\n", 508 "<polygon fill=\"black\" stroke=\"black\" points=\"36.78,-157.5 29.78,-160.65 33.28,-157.5 29.78,-157.5 29.78,-157.5 29.78,-157.5 33.28,-157.5 29.78,-154.35 36.78,-157.5 36.78,-157.5\"/>\n", 509 "</g>\n", 510 "<!-- 1 -->\n", 511 "<g id=\"node3\" class=\"node\">\n", 512 "<title>1</title>\n", 513 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M377,-204.5C377,-204.5 241,-204.5 241,-204.5 235,-204.5 229,-198.5 229,-192.5 229,-192.5 229,-178.5 229,-178.5 229,-172.5 235,-166.5 241,-166.5 241,-166.5 377,-166.5 377,-166.5 383,-166.5 389,-172.5 389,-178.5 389,-178.5 389,-192.5 389,-192.5 389,-198.5 383,-204.5 377,-204.5\"/>\n", 514 "<text text-anchor=\"start\" x=\"264.5\" y=\"-189.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n", 515 "<text text-anchor=\"start\" x=\"237\" y=\"-174.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 516 "</g>\n", 517 "<!-- 0->1 -->\n", 518 "<g id=\"edge2\" class=\"edge\">\n", 519 "<title>0->1</title>\n", 520 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-168.77C202.56,-170.12 212.11,-171.52 221.53,-172.89\"/>\n", 521 "<polygon fill=\"black\" stroke=\"black\" points=\"228.7,-173.94 221.32,-176.04 225.24,-173.43 221.78,-172.93 221.78,-172.93 221.78,-172.93 225.24,-173.43 222.23,-169.81 228.7,-173.94 228.7,-173.94\"/>\n", 522 "</g>\n", 523 "<!-- 2 -->\n", 524 "<g id=\"node4\" class=\"node\">\n", 525 "<title>2</title>\n", 526 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M375,-148.5C375,-148.5 243,-148.5 243,-148.5 237,-148.5 231,-142.5 231,-136.5 231,-136.5 231,-122.5 231,-122.5 231,-116.5 237,-110.5 243,-110.5 243,-110.5 375,-110.5 375,-110.5 381,-110.5 387,-116.5 387,-122.5 387,-122.5 387,-136.5 387,-136.5 387,-142.5 381,-148.5 375,-148.5\"/>\n", 527 "<text text-anchor=\"start\" x=\"264.5\" y=\"-133.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n", 528 "<text text-anchor=\"start\" x=\"239\" y=\"-118.3\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 529 "</g>\n", 530 "<!-- 0->2 -->\n", 531 "<g id=\"edge3\" class=\"edge\">\n", 532 "<title>0->2</title>\n", 533 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-146.23C203.34,-144.76 213.7,-143.25 223.88,-141.77\"/>\n", 534 "<polygon fill=\"black\" stroke=\"black\" points=\"230.89,-140.74 224.42,-144.87 227.43,-141.25 223.97,-141.75 223.97,-141.75 223.97,-141.75 227.43,-141.25 223.51,-138.64 230.89,-140.74 230.89,-140.74\"/>\n", 535 "</g>\n", 536 "<!-- 3 -->\n", 537 "<g id=\"node5\" class=\"node\">\n", 538 "<title>3</title>\n", 539 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-232.5C573,-232.5 437,-232.5 437,-232.5 431,-232.5 425,-226.5 425,-220.5 425,-220.5 425,-206.5 425,-206.5 425,-200.5 431,-194.5 437,-194.5 437,-194.5 573,-194.5 573,-194.5 579,-194.5 585,-200.5 585,-206.5 585,-206.5 585,-220.5 585,-220.5 585,-226.5 579,-232.5 573,-232.5\"/>\n", 540 "<text text-anchor=\"start\" x=\"460.5\" y=\"-217.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n", 541 "<text text-anchor=\"start\" x=\"433\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 542 "</g>\n", 543 "<!-- 1->3 -->\n", 544 "<g id=\"edge4\" class=\"edge\">\n", 545 "<title>1->3</title>\n", 546 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-196.93C398.54,-198.28 408.12,-199.66 417.56,-201.02\"/>\n", 547 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-202.06 417.37,-204.18 421.29,-201.56 417.82,-201.06 417.82,-201.06 417.82,-201.06 421.29,-201.56 418.27,-197.94 424.75,-202.06 424.75,-202.06\"/>\n", 548 "</g>\n", 549 "<!-- 4 -->\n", 550 "<g id=\"node6\" class=\"node\">\n", 551 "<title>4</title>\n", 552 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-176.5C573,-176.5 437,-176.5 437,-176.5 431,-176.5 425,-170.5 425,-164.5 425,-164.5 425,-150.5 425,-150.5 425,-144.5 431,-138.5 437,-138.5 437,-138.5 573,-138.5 573,-138.5 579,-138.5 585,-144.5 585,-150.5 585,-150.5 585,-164.5 585,-164.5 585,-170.5 579,-176.5 573,-176.5\"/>\n", 553 "<text text-anchor=\"start\" x=\"460.5\" y=\"-161.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n", 554 "<text text-anchor=\"start\" x=\"433\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 555 "</g>\n", 556 "<!-- 1->4 -->\n", 557 "<g id=\"edge5\" class=\"edge\">\n", 558 "<title>1->4</title>\n", 559 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-174.07C398.54,-172.72 408.12,-171.34 417.56,-169.98\"/>\n", 560 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-168.94 418.27,-173.06 421.29,-169.44 417.82,-169.94 417.82,-169.94 417.82,-169.94 421.29,-169.44 417.37,-166.82 424.75,-168.94 424.75,-168.94\"/>\n", 561 "</g>\n", 562 "<!-- 2->4 -->\n", 563 "<g id=\"edge6\" class=\"edge\">\n", 564 "<title>2->4</title>\n", 565 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-140.65C397.28,-142.1 407.62,-143.59 417.8,-145.06\"/>\n", 566 "<polygon fill=\"black\" stroke=\"black\" points=\"424.81,-146.07 417.43,-148.19 421.35,-145.57 417.88,-145.07 417.88,-145.07 417.88,-145.07 421.35,-145.57 418.33,-141.95 424.81,-146.07 424.81,-146.07\"/>\n", 567 "</g>\n", 568 "<!-- 5 -->\n", 569 "<g id=\"node7\" class=\"node\">\n", 570 "<title>5</title>\n", 571 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M571,-120.5C571,-120.5 439,-120.5 439,-120.5 433,-120.5 427,-114.5 427,-108.5 427,-108.5 427,-94.5 427,-94.5 427,-88.5 433,-82.5 439,-82.5 439,-82.5 571,-82.5 571,-82.5 577,-82.5 583,-88.5 583,-94.5 583,-94.5 583,-108.5 583,-108.5 583,-114.5 577,-120.5 571,-120.5\"/>\n", 572 "<text text-anchor=\"start\" x=\"460.5\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n", 573 "<text text-anchor=\"start\" x=\"435\" y=\"-90.3\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 574 "</g>\n", 575 "<!-- 2->5 -->\n", 576 "<g id=\"edge7\" class=\"edge\">\n", 577 "<title>2->5</title>\n", 578 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-118.35C397.89,-116.81 408.89,-115.23 419.67,-113.67\"/>\n", 579 "<polygon fill=\"black\" stroke=\"black\" points=\"426.72,-112.65 420.24,-116.77 423.25,-113.15 419.79,-113.65 419.79,-113.65 419.79,-113.65 423.25,-113.15 419.34,-110.54 426.72,-112.65 426.72,-112.65\"/>\n", 580 "</g>\n", 581 "<!-- 6 -->\n", 582 "<g id=\"node8\" class=\"node\">\n", 583 "<title>6</title>\n", 584 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M767,-288.5C767,-288.5 635,-288.5 635,-288.5 629,-288.5 623,-282.5 623,-276.5 623,-276.5 623,-262.5 623,-262.5 623,-256.5 629,-250.5 635,-250.5 635,-250.5 767,-250.5 767,-250.5 773,-250.5 779,-256.5 779,-262.5 779,-262.5 779,-276.5 779,-276.5 779,-282.5 773,-288.5 767,-288.5\"/>\n", 585 "<text text-anchor=\"start\" x=\"656.5\" y=\"-273.3\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n", 586 "<text text-anchor=\"start\" x=\"631\" y=\"-258.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 587 "</g>\n", 588 "<!-- 3->6 -->\n", 589 "<g id=\"edge8\" class=\"edge\">\n", 590 "<title>3->6</title>\n", 591 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-232.54C589.6,-237.63 608.78,-243.17 626.8,-248.37\"/>\n", 592 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-250.42 626.3,-251.51 630.54,-249.45 627.18,-248.48 627.18,-248.48 627.18,-248.48 630.54,-249.45 628.05,-245.45 633.9,-250.42 633.9,-250.42\"/>\n", 593 "</g>\n", 594 "<!-- 7 -->\n", 595 "<g id=\"node9\" class=\"node\">\n", 596 "<title>7</title>\n", 597 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M769,-232.5C769,-232.5 633,-232.5 633,-232.5 627,-232.5 621,-226.5 621,-220.5 621,-220.5 621,-206.5 621,-206.5 621,-200.5 627,-194.5 633,-194.5 633,-194.5 769,-194.5 769,-194.5 775,-194.5 781,-200.5 781,-206.5 781,-206.5 781,-220.5 781,-220.5 781,-226.5 775,-232.5 769,-232.5\"/>\n", 598 "<text text-anchor=\"start\" x=\"656.5\" y=\"-217.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n", 599 "<text text-anchor=\"start\" x=\"629\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 600 "</g>\n", 601 "<!-- 3->7 -->\n", 602 "<g id=\"edge9\" class=\"edge\">\n", 603 "<title>3->7</title>\n", 604 "<path fill=\"none\" stroke=\"black\" d=\"M585.19,-213.5C594.54,-213.5 604.12,-213.5 613.56,-213.5\"/>\n", 605 "<polygon fill=\"black\" stroke=\"black\" points=\"620.75,-213.5 613.75,-216.65 617.25,-213.5 613.75,-213.5 613.75,-213.5 613.75,-213.5 617.25,-213.5 613.75,-210.35 620.75,-213.5 620.75,-213.5\"/>\n", 606 "</g>\n", 607 "<!-- 4->7 -->\n", 608 "<g id=\"edge10\" class=\"edge\">\n", 609 "<title>4->7</title>\n", 610 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-176.54C589.6,-181.63 608.78,-187.17 626.8,-192.37\"/>\n", 611 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-194.42 626.3,-195.51 630.54,-193.45 627.18,-192.48 627.18,-192.48 627.18,-192.48 630.54,-193.45 628.05,-189.45 633.9,-194.42 633.9,-194.42\"/>\n", 612 "</g>\n", 613 "<!-- 8 -->\n", 614 "<g id=\"node10\" class=\"node\">\n", 615 "<title>8</title>\n", 616 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M769,-176.5C769,-176.5 633,-176.5 633,-176.5 627,-176.5 621,-170.5 621,-164.5 621,-164.5 621,-150.5 621,-150.5 621,-144.5 627,-138.5 633,-138.5 633,-138.5 769,-138.5 769,-138.5 775,-138.5 781,-144.5 781,-150.5 781,-150.5 781,-164.5 781,-164.5 781,-170.5 775,-176.5 769,-176.5\"/>\n", 617 "<text text-anchor=\"start\" x=\"656.5\" y=\"-161.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n", 618 "<text text-anchor=\"start\" x=\"629\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 619 "</g>\n", 620 "<!-- 4->8 -->\n", 621 "<g id=\"edge11\" class=\"edge\">\n", 622 "<title>4->8</title>\n", 623 "<path fill=\"none\" stroke=\"black\" d=\"M585.19,-157.5C594.54,-157.5 604.12,-157.5 613.56,-157.5\"/>\n", 624 "<polygon fill=\"black\" stroke=\"black\" points=\"620.75,-157.5 613.75,-160.65 617.25,-157.5 613.75,-157.5 613.75,-157.5 613.75,-157.5 617.25,-157.5 613.75,-154.35 620.75,-157.5 620.75,-157.5\"/>\n", 625 "</g>\n", 626 "<!-- 5->8 -->\n", 627 "<g id=\"edge12\" class=\"edge\">\n", 628 "<title>5->8</title>\n", 629 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-120.54C589.6,-125.63 608.78,-131.17 626.8,-136.37\"/>\n", 630 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-138.42 626.3,-139.51 630.54,-137.45 627.18,-136.48 627.18,-136.48 627.18,-136.48 630.54,-137.45 628.05,-133.45 633.9,-138.42 633.9,-138.42\"/>\n", 631 "</g>\n", 632 "<!-- 9 -->\n", 633 "<g id=\"node11\" class=\"node\">\n", 634 "<title>9</title>\n", 635 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M741.5,-47.5C741.5,-47.5 660.5,-47.5 660.5,-47.5 654.5,-47.5 648.5,-41.5 648.5,-35.5 648.5,-35.5 648.5,-21.5 648.5,-21.5 648.5,-15.5 654.5,-9.5 660.5,-9.5 660.5,-9.5 741.5,-9.5 741.5,-9.5 747.5,-9.5 753.5,-15.5 753.5,-21.5 753.5,-21.5 753.5,-35.5 753.5,-35.5 753.5,-41.5 747.5,-47.5 741.5,-47.5\"/>\n", 636 "<text text-anchor=\"start\" x=\"656.5\" y=\"-32.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n", 637 "<text text-anchor=\"start\" x=\"696\" y=\"-17.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 638 "</g>\n", 639 "<!-- 5->9 -->\n", 640 "<g id=\"edge13\" class=\"edge\">\n", 641 "<title>5->9</title>\n", 642 "<path fill=\"none\" stroke=\"black\" d=\"M556.72,-82.42C583.01,-72.52 615.22,-60.4 642.44,-50.16\"/>\n", 643 "<polygon fill=\"black\" stroke=\"black\" points=\"649.24,-47.6 643.8,-53.01 645.97,-48.83 642.69,-50.07 642.69,-50.07 642.69,-50.07 645.97,-48.83 641.58,-47.12 649.24,-47.6 649.24,-47.6\"/>\n", 644 "</g>\n", 645 "<!-- 10 -->\n", 646 "<g id=\"node12\" class=\"node\">\n", 647 "<title>10</title>\n", 648 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M767,-120.5C767,-120.5 635,-120.5 635,-120.5 629,-120.5 623,-114.5 623,-108.5 623,-108.5 623,-94.5 623,-94.5 623,-88.5 629,-82.5 635,-82.5 635,-82.5 767,-82.5 767,-82.5 773,-82.5 779,-88.5 779,-94.5 779,-94.5 779,-108.5 779,-108.5 779,-114.5 773,-120.5 767,-120.5\"/>\n", 649 "<text text-anchor=\"start\" x=\"656.5\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1</text>\n", 650 "<text text-anchor=\"start\" x=\"631\" y=\"-90.3\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 651 "</g>\n", 652 "<!-- 5->10 -->\n", 653 "<g id=\"edge14\" class=\"edge\">\n", 654 "<title>5->10</title>\n", 655 "<path fill=\"none\" stroke=\"black\" d=\"M583.23,-101.5C593.89,-101.5 604.89,-101.5 615.67,-101.5\"/>\n", 656 "<polygon fill=\"black\" stroke=\"black\" points=\"622.72,-101.5 615.72,-104.65 619.22,-101.5 615.72,-101.5 615.72,-101.5 615.72,-101.5 619.22,-101.5 615.72,-98.35 622.72,-101.5 622.72,-101.5\"/>\n", 657 "</g>\n", 658 "<!-- 6->6 -->\n", 659 "<g id=\"edge15\" class=\"edge\">\n", 660 "<title>6->6</title>\n", 661 "<path fill=\"none\" stroke=\"black\" d=\"M665.7,-288.54C660.82,-298.03 672.58,-306.5 701,-306.5 721.87,-306.5 733.76,-301.93 736.67,-295.75\"/>\n", 662 "<polygon fill=\"black\" stroke=\"black\" points=\"736.3,-288.54 739.8,-295.37 736.48,-292.03 736.66,-295.53 736.66,-295.53 736.66,-295.53 736.48,-292.03 733.51,-295.69 736.3,-288.54 736.3,-288.54\"/>\n", 663 "</g>\n", 664 "<!-- 11 -->\n", 665 "<g id=\"node13\" class=\"node\">\n", 666 "<title>11</title>\n", 667 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M961,-288.5C961,-288.5 829,-288.5 829,-288.5 823,-288.5 817,-282.5 817,-276.5 817,-276.5 817,-262.5 817,-262.5 817,-256.5 823,-250.5 829,-250.5 829,-250.5 961,-250.5 961,-250.5 967,-250.5 973,-256.5 973,-262.5 973,-262.5 973,-276.5 973,-276.5 973,-282.5 967,-288.5 961,-288.5\"/>\n", 668 "<text text-anchor=\"start\" x=\"850.5\" y=\"-273.3\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=1, Q=0</text>\n", 669 "<text text-anchor=\"start\" x=\"825\" y=\"-258.3\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 670 "</g>\n", 671 "<!-- 7->11 -->\n", 672 "<g id=\"edge16\" class=\"edge\">\n", 673 "<title>7->11</title>\n", 674 "<path fill=\"none\" stroke=\"black\" d=\"M767.27,-232.54C784.74,-237.63 803.72,-243.17 821.55,-248.37\"/>\n", 675 "<polygon fill=\"black\" stroke=\"black\" points=\"828.58,-250.42 820.98,-251.48 825.22,-249.44 821.86,-248.46 821.86,-248.46 821.86,-248.46 825.22,-249.44 822.75,-245.44 828.58,-250.42 828.58,-250.42\"/>\n", 676 "</g>\n", 677 "<!-- 12 -->\n", 678 "<g id=\"node14\" class=\"node\">\n", 679 "<title>12</title>\n", 680 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M935.5,-232.5C935.5,-232.5 854.5,-232.5 854.5,-232.5 848.5,-232.5 842.5,-226.5 842.5,-220.5 842.5,-220.5 842.5,-206.5 842.5,-206.5 842.5,-200.5 848.5,-194.5 854.5,-194.5 854.5,-194.5 935.5,-194.5 935.5,-194.5 941.5,-194.5 947.5,-200.5 947.5,-206.5 947.5,-206.5 947.5,-220.5 947.5,-220.5 947.5,-226.5 941.5,-232.5 935.5,-232.5\"/>\n", 681 "<text text-anchor=\"start\" x=\"850.5\" y=\"-217.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=2, Q=0</text>\n", 682 "<text text-anchor=\"start\" x=\"890\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 683 "</g>\n", 684 "<!-- 7->12 -->\n", 685 "<g id=\"edge17\" class=\"edge\">\n", 686 "<title>7->12</title>\n", 687 "<path fill=\"none\" stroke=\"black\" d=\"M781.2,-213.5C799.28,-213.5 818.18,-213.5 835.22,-213.5\"/>\n", 688 "<polygon fill=\"black\" stroke=\"black\" points=\"842.41,-213.5 835.41,-216.65 838.91,-213.5 835.41,-213.5 835.41,-213.5 835.41,-213.5 838.91,-213.5 835.41,-210.35 842.41,-213.5 842.41,-213.5\"/>\n", 689 "</g>\n", 690 "<!-- 8->12 -->\n", 691 "<g id=\"edge18\" class=\"edge\">\n", 692 "<title>8->12</title>\n", 693 "<path fill=\"none\" stroke=\"black\" d=\"M767.27,-176.54C789.34,-182.97 813.84,-190.12 835.36,-196.4\"/>\n", 694 "<polygon fill=\"black\" stroke=\"black\" points=\"842.24,-198.4 834.64,-199.47 838.88,-197.42 835.52,-196.44 835.52,-196.44 835.52,-196.44 838.88,-197.42 836.4,-193.42 842.24,-198.4 842.24,-198.4\"/>\n", 695 "</g>\n", 696 "<!-- 13 -->\n", 697 "<g id=\"node15\" class=\"node\">\n", 698 "<title>13</title>\n", 699 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M935.5,-176.5C935.5,-176.5 854.5,-176.5 854.5,-176.5 848.5,-176.5 842.5,-170.5 842.5,-164.5 842.5,-164.5 842.5,-150.5 842.5,-150.5 842.5,-144.5 848.5,-138.5 854.5,-138.5 854.5,-138.5 935.5,-138.5 935.5,-138.5 941.5,-138.5 947.5,-144.5 947.5,-150.5 947.5,-150.5 947.5,-164.5 947.5,-164.5 947.5,-170.5 941.5,-176.5 935.5,-176.5\"/>\n", 700 "<text text-anchor=\"start\" x=\"850.5\" y=\"-161.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=3, Q=0</text>\n", 701 "<text text-anchor=\"start\" x=\"890\" y=\"-146.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 702 "</g>\n", 703 "<!-- 8->13 -->\n", 704 "<g id=\"edge19\" class=\"edge\">\n", 705 "<title>8->13</title>\n", 706 "<path fill=\"none\" stroke=\"black\" d=\"M781.2,-157.5C799.28,-157.5 818.18,-157.5 835.22,-157.5\"/>\n", 707 "<polygon fill=\"black\" stroke=\"black\" points=\"842.41,-157.5 835.41,-160.65 838.91,-157.5 835.41,-157.5 835.41,-157.5 835.41,-157.5 838.91,-157.5 835.41,-154.35 842.41,-157.5 842.41,-157.5\"/>\n", 708 "</g>\n", 709 "<!-- 14 -->\n", 710 "<g id=\"node16\" class=\"node\">\n", 711 "<title>14</title>\n", 712 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M935.5,-120.5C935.5,-120.5 854.5,-120.5 854.5,-120.5 848.5,-120.5 842.5,-114.5 842.5,-108.5 842.5,-108.5 842.5,-94.5 842.5,-94.5 842.5,-88.5 848.5,-82.5 854.5,-82.5 854.5,-82.5 935.5,-82.5 935.5,-82.5 941.5,-82.5 947.5,-88.5 947.5,-94.5 947.5,-94.5 947.5,-108.5 947.5,-108.5 947.5,-114.5 941.5,-120.5 935.5,-120.5\"/>\n", 713 "<text text-anchor=\"start\" x=\"850.5\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1</text>\n", 714 "<text text-anchor=\"start\" x=\"890\" y=\"-90.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 715 "</g>\n", 716 "<!-- 8->14 -->\n", 717 "<g id=\"edge20\" class=\"edge\">\n", 718 "<title>8->14</title>\n", 719 "<path fill=\"none\" stroke=\"black\" d=\"M767.27,-138.46C789.34,-132.03 813.84,-124.88 835.36,-118.6\"/>\n", 720 "<polygon fill=\"black\" stroke=\"black\" points=\"842.24,-116.6 836.4,-121.58 838.88,-117.58 835.52,-118.56 835.52,-118.56 835.52,-118.56 838.88,-117.58 834.64,-115.53 842.24,-116.6 842.24,-116.6\"/>\n", 721 "</g>\n", 722 "<!-- u9 -->\n", 723 "<g id=\"node17\" class=\"node\">\n", 724 "<title>u9</title>\n", 725 "<g id=\"a_node17\"><a xlink:title=\"hidden successors\">\n", 726 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M900.33,-23C900.33,-23 889.67,-23 889.67,-23 885.83,-23 882,-19.17 882,-15.33 882,-15.33 882,-7.67 882,-7.67 882,-3.83 885.83,0 889.67,0 889.67,0 900.33,0 900.33,0 904.17,0 908,-3.83 908,-7.67 908,-7.67 908,-15.33 908,-15.33 908,-19.17 904.17,-23 900.33,-23\"/>\n", 727 "<text text-anchor=\"middle\" x=\"895\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 728 "</a>\n", 729 "</g>\n", 730 "</g>\n", 731 "<!-- 9->u9 -->\n", 732 "<g id=\"edge21\" class=\"edge\">\n", 733 "<title>9->u9</title>\n", 734 "<g id=\"a_edge21\"><a xlink:title=\"hidden successors\">\n", 735 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M753.71,-23.92C793.5,-20.4 846.31,-15.72 874.42,-13.23\"/>\n", 736 "<polygon fill=\"black\" stroke=\"black\" points=\"881.67,-12.59 874.97,-16.35 878.18,-12.9 874.69,-13.21 874.69,-13.21 874.69,-13.21 878.18,-12.9 874.42,-10.07 881.67,-12.59 881.67,-12.59\"/>\n", 737 "</a>\n", 738 "</g>\n", 739 "</g>\n", 740 "<!-- 10->14 -->\n", 741 "<g id=\"edge23\" class=\"edge\">\n", 742 "<title>10->14</title>\n", 743 "<path fill=\"none\" stroke=\"black\" d=\"M779.26,-101.5C797.86,-101.5 817.44,-101.5 835.05,-101.5\"/>\n", 744 "<polygon fill=\"black\" stroke=\"black\" points=\"842.47,-101.5 835.47,-104.65 838.97,-101.5 835.47,-101.5 835.47,-101.5 835.47,-101.5 838.97,-101.5 835.47,-98.35 842.47,-101.5 842.47,-101.5\"/>\n", 745 "</g>\n", 746 "<!-- u10 -->\n", 747 "<g id=\"node18\" class=\"node\">\n", 748 "<title>u10</title>\n", 749 "<g id=\"a_node18\"><a xlink:title=\"hidden successors\">\n", 750 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M900.33,-64C900.33,-64 889.67,-64 889.67,-64 885.83,-64 882,-60.17 882,-56.33 882,-56.33 882,-48.67 882,-48.67 882,-44.83 885.83,-41 889.67,-41 889.67,-41 900.33,-41 900.33,-41 904.17,-41 908,-44.83 908,-48.67 908,-48.67 908,-56.33 908,-56.33 908,-60.17 904.17,-64 900.33,-64\"/>\n", 751 "<text text-anchor=\"middle\" x=\"895\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 752 "</a>\n", 753 "</g>\n", 754 "</g>\n", 755 "<!-- 10->u10 -->\n", 756 "<g id=\"edge22\" class=\"edge\">\n", 757 "<title>10->u10</title>\n", 758 "<g id=\"a_edge22\"><a xlink:title=\"hidden successors\">\n", 759 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M776.51,-82.49C812.27,-73.36 852.23,-63.16 875.12,-57.32\"/>\n", 760 "<polygon fill=\"black\" stroke=\"black\" points=\"881.92,-55.58 875.92,-60.37 878.53,-56.45 875.14,-57.31 875.14,-57.31 875.14,-57.31 878.53,-56.45 874.36,-54.26 881.92,-55.58 881.92,-55.58\"/>\n", 761 "</a>\n", 762 "</g>\n", 763 "</g>\n", 764 "<!-- 11->11 -->\n", 765 "<g id=\"edge24\" class=\"edge\">\n", 766 "<title>11->11</title>\n", 767 "<path fill=\"none\" stroke=\"black\" d=\"M872.07,-288.54C868.9,-298.03 876.54,-306.5 895,-306.5 908.55,-306.5 916.28,-301.93 918.17,-295.75\"/>\n", 768 "<polygon fill=\"black\" stroke=\"black\" points=\"917.93,-288.54 921.31,-295.43 918.04,-292.04 918.16,-295.53 918.16,-295.53 918.16,-295.53 918.04,-292.04 915.01,-295.64 917.93,-288.54 917.93,-288.54\"/>\n", 769 "</g>\n", 770 "<!-- u12 -->\n", 771 "<g id=\"node19\" class=\"node\">\n", 772 "<title>u12</title>\n", 773 "<g id=\"a_node19\"><a xlink:title=\"hidden successors\">\n", 774 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M1027.33,-225C1027.33,-225 1016.67,-225 1016.67,-225 1012.83,-225 1009,-221.17 1009,-217.33 1009,-217.33 1009,-209.67 1009,-209.67 1009,-205.83 1012.83,-202 1016.67,-202 1016.67,-202 1027.33,-202 1027.33,-202 1031.17,-202 1035,-205.83 1035,-209.67 1035,-209.67 1035,-217.33 1035,-217.33 1035,-221.17 1031.17,-225 1027.33,-225\"/>\n", 775 "<text text-anchor=\"middle\" x=\"1022\" y=\"-209.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 776 "</a>\n", 777 "</g>\n", 778 "</g>\n", 779 "<!-- 12->u12 -->\n", 780 "<g id=\"edge25\" class=\"edge\">\n", 781 "<title>12->u12</title>\n", 782 "<g id=\"a_edge25\"><a xlink:title=\"hidden successors\">\n", 783 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M947.56,-213.5C966.63,-213.5 987.1,-213.5 1001.57,-213.5\"/>\n", 784 "<polygon fill=\"black\" stroke=\"black\" points=\"1008.94,-213.5 1001.94,-216.65 1005.44,-213.5 1001.94,-213.5 1001.94,-213.5 1001.94,-213.5 1005.44,-213.5 1001.94,-210.35 1008.94,-213.5 1008.94,-213.5\"/>\n", 785 "</a>\n", 786 "</g>\n", 787 "</g>\n", 788 "<!-- u13 -->\n", 789 "<g id=\"node20\" class=\"node\">\n", 790 "<title>u13</title>\n", 791 "<g id=\"a_node20\"><a xlink:title=\"hidden successors\">\n", 792 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M1027.33,-169C1027.33,-169 1016.67,-169 1016.67,-169 1012.83,-169 1009,-165.17 1009,-161.33 1009,-161.33 1009,-153.67 1009,-153.67 1009,-149.83 1012.83,-146 1016.67,-146 1016.67,-146 1027.33,-146 1027.33,-146 1031.17,-146 1035,-149.83 1035,-153.67 1035,-153.67 1035,-161.33 1035,-161.33 1035,-165.17 1031.17,-169 1027.33,-169\"/>\n", 793 "<text text-anchor=\"middle\" x=\"1022\" y=\"-153.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 794 "</a>\n", 795 "</g>\n", 796 "</g>\n", 797 "<!-- 13->u13 -->\n", 798 "<g id=\"edge26\" class=\"edge\">\n", 799 "<title>13->u13</title>\n", 800 "<g id=\"a_edge26\"><a xlink:title=\"hidden successors\">\n", 801 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M947.56,-157.5C966.63,-157.5 987.1,-157.5 1001.57,-157.5\"/>\n", 802 "<polygon fill=\"black\" stroke=\"black\" points=\"1008.94,-157.5 1001.94,-160.65 1005.44,-157.5 1001.94,-157.5 1001.94,-157.5 1001.94,-157.5 1005.44,-157.5 1001.94,-154.35 1008.94,-157.5 1008.94,-157.5\"/>\n", 803 "</a>\n", 804 "</g>\n", 805 "</g>\n", 806 "<!-- u14 -->\n", 807 "<g id=\"node21\" class=\"node\">\n", 808 "<title>u14</title>\n", 809 "<g id=\"a_node21\"><a xlink:title=\"hidden successors\">\n", 810 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M1027.33,-113C1027.33,-113 1016.67,-113 1016.67,-113 1012.83,-113 1009,-109.17 1009,-105.33 1009,-105.33 1009,-97.67 1009,-97.67 1009,-93.83 1012.83,-90 1016.67,-90 1016.67,-90 1027.33,-90 1027.33,-90 1031.17,-90 1035,-93.83 1035,-97.67 1035,-97.67 1035,-105.33 1035,-105.33 1035,-109.17 1031.17,-113 1027.33,-113\"/>\n", 811 "<text text-anchor=\"middle\" x=\"1022\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 812 "</a>\n", 813 "</g>\n", 814 "</g>\n", 815 "<!-- 14->u14 -->\n", 816 "<g id=\"edge27\" class=\"edge\">\n", 817 "<title>14->u14</title>\n", 818 "<g id=\"a_edge27\"><a xlink:title=\"hidden successors\">\n", 819 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M947.56,-101.5C966.63,-101.5 987.1,-101.5 1001.57,-101.5\"/>\n", 820 "<polygon fill=\"black\" stroke=\"black\" points=\"1008.94,-101.5 1001.94,-104.65 1005.44,-101.5 1001.94,-101.5 1001.94,-101.5 1001.94,-101.5 1005.44,-101.5 1001.94,-98.35 1008.94,-101.5 1008.94,-101.5\"/>\n", 821 "</a>\n", 822 "</g>\n", 823 "</g>\n", 824 "</g>\n", 825 "</svg>\n" 826 ], 827 "text/plain": [ 828 "<spot.jupyter.SVG object>" 829 ] 830 }, 831 "execution_count": 10, 832 "metadata": {}, 833 "output_type": "execute_result" 834 } 835 ], 836 "source": [ 837 "k.show('.<15')" 838 ] 839 }, 840 { 841 "cell_type": "code", 842 "execution_count": 11, 843 "metadata": {}, 844 "outputs": [ 845 { 846 "data": { 847 "image/svg+xml": [ 848 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 849 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 850 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 851 "<!-- Generated by graphviz version 2.43.0 (0)\n", 852 " -->\n", 853 "<!-- Pages: 1 -->\n", 854 "<svg width=\"734pt\" height=\"183pt\"\n", 855 " viewBox=\"0.00 0.00 734.00 183.37\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 856 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.5319148936170213 0.5319148936170213) rotate(0) translate(4 340)\">\n", 857 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-340 1373,-340 1373,4 -4,4\"/>\n", 858 "<text text-anchor=\"start\" x=\"681.5\" y=\"-320.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n", 859 "<text text-anchor=\"start\" x=\"673.5\" y=\"-305.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n", 860 "<!-- I -->\n", 861 "<!-- 0 -->\n", 862 "<g id=\"node2\" class=\"node\">\n", 863 "<title>0</title>\n", 864 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M181,-168C181,-168 49,-168 49,-168 43,-168 37,-162 37,-156 37,-156 37,-142 37,-142 37,-136 43,-130 49,-130 49,-130 181,-130 181,-130 187,-130 193,-136 193,-142 193,-142 193,-156 193,-156 193,-162 187,-168 181,-168\"/>\n", 865 "<text text-anchor=\"start\" x=\"70.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n", 866 "<text text-anchor=\"start\" x=\"45\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 867 "</g>\n", 868 "<!-- I->0 -->\n", 869 "<g id=\"edge1\" class=\"edge\">\n", 870 "<title>I->0</title>\n", 871 "<path fill=\"none\" stroke=\"black\" d=\"M1.08,-149C2.17,-149 13.89,-149 29.41,-149\"/>\n", 872 "<polygon fill=\"black\" stroke=\"black\" points=\"36.78,-149 29.78,-152.15 33.28,-149 29.78,-149 29.78,-149 29.78,-149 33.28,-149 29.78,-145.85 36.78,-149 36.78,-149\"/>\n", 873 "</g>\n", 874 "<!-- 1 -->\n", 875 "<g id=\"node3\" class=\"node\">\n", 876 "<title>1</title>\n", 877 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M377,-196C377,-196 241,-196 241,-196 235,-196 229,-190 229,-184 229,-184 229,-170 229,-170 229,-164 235,-158 241,-158 241,-158 377,-158 377,-158 383,-158 389,-164 389,-170 389,-170 389,-184 389,-184 389,-190 383,-196 377,-196\"/>\n", 878 "<text text-anchor=\"start\" x=\"264.5\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n", 879 "<text text-anchor=\"start\" x=\"237\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 880 "</g>\n", 881 "<!-- 0->1 -->\n", 882 "<g id=\"edge2\" class=\"edge\">\n", 883 "<title>0->1</title>\n", 884 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-160.27C202.56,-161.62 212.11,-163.02 221.53,-164.39\"/>\n", 885 "<polygon fill=\"black\" stroke=\"black\" points=\"228.7,-165.44 221.32,-167.54 225.24,-164.93 221.78,-164.43 221.78,-164.43 221.78,-164.43 225.24,-164.93 222.23,-161.31 228.7,-165.44 228.7,-165.44\"/>\n", 886 "</g>\n", 887 "<!-- 2 -->\n", 888 "<g id=\"node4\" class=\"node\">\n", 889 "<title>2</title>\n", 890 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M375,-140C375,-140 243,-140 243,-140 237,-140 231,-134 231,-128 231,-128 231,-114 231,-114 231,-108 237,-102 243,-102 243,-102 375,-102 375,-102 381,-102 387,-108 387,-114 387,-114 387,-128 387,-128 387,-134 381,-140 375,-140\"/>\n", 891 "<text text-anchor=\"start\" x=\"264.5\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n", 892 "<text text-anchor=\"start\" x=\"239\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 893 "</g>\n", 894 "<!-- 0->2 -->\n", 895 "<g id=\"edge3\" class=\"edge\">\n", 896 "<title>0->2</title>\n", 897 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-137.73C203.34,-136.26 213.7,-134.75 223.88,-133.27\"/>\n", 898 "<polygon fill=\"black\" stroke=\"black\" points=\"230.89,-132.24 224.42,-136.37 227.43,-132.75 223.97,-133.25 223.97,-133.25 223.97,-133.25 227.43,-132.75 223.51,-130.14 230.89,-132.24 230.89,-132.24\"/>\n", 899 "</g>\n", 900 "<!-- 3 -->\n", 901 "<g id=\"node5\" class=\"node\">\n", 902 "<title>3</title>\n", 903 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-224C573,-224 437,-224 437,-224 431,-224 425,-218 425,-212 425,-212 425,-198 425,-198 425,-192 431,-186 437,-186 437,-186 573,-186 573,-186 579,-186 585,-192 585,-198 585,-198 585,-212 585,-212 585,-218 579,-224 573,-224\"/>\n", 904 "<text text-anchor=\"start\" x=\"460.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n", 905 "<text text-anchor=\"start\" x=\"433\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 906 "</g>\n", 907 "<!-- 1->3 -->\n", 908 "<g id=\"edge4\" class=\"edge\">\n", 909 "<title>1->3</title>\n", 910 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-188.43C398.54,-189.78 408.12,-191.16 417.56,-192.52\"/>\n", 911 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-193.56 417.37,-195.68 421.29,-193.06 417.82,-192.56 417.82,-192.56 417.82,-192.56 421.29,-193.06 418.27,-189.44 424.75,-193.56 424.75,-193.56\"/>\n", 912 "</g>\n", 913 "<!-- 4 -->\n", 914 "<g id=\"node6\" class=\"node\">\n", 915 "<title>4</title>\n", 916 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-168C573,-168 437,-168 437,-168 431,-168 425,-162 425,-156 425,-156 425,-142 425,-142 425,-136 431,-130 437,-130 437,-130 573,-130 573,-130 579,-130 585,-136 585,-142 585,-142 585,-156 585,-156 585,-162 579,-168 573,-168\"/>\n", 917 "<text text-anchor=\"start\" x=\"460.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n", 918 "<text text-anchor=\"start\" x=\"433\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 919 "</g>\n", 920 "<!-- 1->4 -->\n", 921 "<g id=\"edge5\" class=\"edge\">\n", 922 "<title>1->4</title>\n", 923 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-165.57C398.54,-164.22 408.12,-162.84 417.56,-161.48\"/>\n", 924 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-160.44 418.27,-164.56 421.29,-160.94 417.82,-161.44 417.82,-161.44 417.82,-161.44 421.29,-160.94 417.37,-158.32 424.75,-160.44 424.75,-160.44\"/>\n", 925 "</g>\n", 926 "<!-- 2->4 -->\n", 927 "<g id=\"edge6\" class=\"edge\">\n", 928 "<title>2->4</title>\n", 929 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-132.15C397.28,-133.6 407.62,-135.09 417.8,-136.56\"/>\n", 930 "<polygon fill=\"black\" stroke=\"black\" points=\"424.81,-137.57 417.43,-139.69 421.35,-137.07 417.88,-136.57 417.88,-136.57 417.88,-136.57 421.35,-137.07 418.33,-133.45 424.81,-137.57 424.81,-137.57\"/>\n", 931 "</g>\n", 932 "<!-- 5 -->\n", 933 "<g id=\"node7\" class=\"node\">\n", 934 "<title>5</title>\n", 935 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M571,-112C571,-112 439,-112 439,-112 433,-112 427,-106 427,-100 427,-100 427,-86 427,-86 427,-80 433,-74 439,-74 439,-74 571,-74 571,-74 577,-74 583,-80 583,-86 583,-86 583,-100 583,-100 583,-106 577,-112 571,-112\"/>\n", 936 "<text text-anchor=\"start\" x=\"460.5\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n", 937 "<text text-anchor=\"start\" x=\"435\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 938 "</g>\n", 939 "<!-- 2->5 -->\n", 940 "<g id=\"edge7\" class=\"edge\">\n", 941 "<title>2->5</title>\n", 942 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-109.85C397.89,-108.31 408.89,-106.73 419.67,-105.17\"/>\n", 943 "<polygon fill=\"black\" stroke=\"black\" points=\"426.72,-104.15 420.24,-108.27 423.25,-104.65 419.79,-105.15 419.79,-105.15 419.79,-105.15 423.25,-104.65 419.34,-102.04 426.72,-104.15 426.72,-104.15\"/>\n", 944 "</g>\n", 945 "<!-- 6 -->\n", 946 "<g id=\"node8\" class=\"node\">\n", 947 "<title>6</title>\n", 948 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M767,-280C767,-280 635,-280 635,-280 629,-280 623,-274 623,-268 623,-268 623,-254 623,-254 623,-248 629,-242 635,-242 635,-242 767,-242 767,-242 773,-242 779,-248 779,-254 779,-254 779,-268 779,-268 779,-274 773,-280 767,-280\"/>\n", 949 "<text text-anchor=\"start\" x=\"656.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n", 950 "<text text-anchor=\"start\" x=\"631\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 951 "</g>\n", 952 "<!-- 3->6 -->\n", 953 "<g id=\"edge8\" class=\"edge\">\n", 954 "<title>3->6</title>\n", 955 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-224.04C589.6,-229.13 608.78,-234.67 626.8,-239.87\"/>\n", 956 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-241.92 626.3,-243.01 630.54,-240.95 627.18,-239.98 627.18,-239.98 627.18,-239.98 630.54,-240.95 628.05,-236.95 633.9,-241.92 633.9,-241.92\"/>\n", 957 "</g>\n", 958 "<!-- 7 -->\n", 959 "<g id=\"node9\" class=\"node\">\n", 960 "<title>7</title>\n", 961 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M769,-224C769,-224 633,-224 633,-224 627,-224 621,-218 621,-212 621,-212 621,-198 621,-198 621,-192 627,-186 633,-186 633,-186 769,-186 769,-186 775,-186 781,-192 781,-198 781,-198 781,-212 781,-212 781,-218 775,-224 769,-224\"/>\n", 962 "<text text-anchor=\"start\" x=\"656.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n", 963 "<text text-anchor=\"start\" x=\"629\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 964 "</g>\n", 965 "<!-- 3->7 -->\n", 966 "<g id=\"edge9\" class=\"edge\">\n", 967 "<title>3->7</title>\n", 968 "<path fill=\"none\" stroke=\"black\" d=\"M585.19,-205C594.54,-205 604.12,-205 613.56,-205\"/>\n", 969 "<polygon fill=\"black\" stroke=\"black\" points=\"620.75,-205 613.75,-208.15 617.25,-205 613.75,-205 613.75,-205 613.75,-205 617.25,-205 613.75,-201.85 620.75,-205 620.75,-205\"/>\n", 970 "</g>\n", 971 "<!-- 4->7 -->\n", 972 "<g id=\"edge10\" class=\"edge\">\n", 973 "<title>4->7</title>\n", 974 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-168.04C589.6,-173.13 608.78,-178.67 626.8,-183.87\"/>\n", 975 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-185.92 626.3,-187.01 630.54,-184.95 627.18,-183.98 627.18,-183.98 627.18,-183.98 630.54,-184.95 628.05,-180.95 633.9,-185.92 633.9,-185.92\"/>\n", 976 "</g>\n", 977 "<!-- 8 -->\n", 978 "<g id=\"node10\" class=\"node\">\n", 979 "<title>8</title>\n", 980 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M769,-168C769,-168 633,-168 633,-168 627,-168 621,-162 621,-156 621,-156 621,-142 621,-142 621,-136 627,-130 633,-130 633,-130 769,-130 769,-130 775,-130 781,-136 781,-142 781,-142 781,-156 781,-156 781,-162 775,-168 769,-168\"/>\n", 981 "<text text-anchor=\"start\" x=\"656.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n", 982 "<text text-anchor=\"start\" x=\"629\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 983 "</g>\n", 984 "<!-- 4->8 -->\n", 985 "<g id=\"edge11\" class=\"edge\">\n", 986 "<title>4->8</title>\n", 987 "<path fill=\"none\" stroke=\"black\" d=\"M585.19,-149C594.54,-149 604.12,-149 613.56,-149\"/>\n", 988 "<polygon fill=\"black\" stroke=\"black\" points=\"620.75,-149 613.75,-152.15 617.25,-149 613.75,-149 613.75,-149 613.75,-149 617.25,-149 613.75,-145.85 620.75,-149 620.75,-149\"/>\n", 989 "</g>\n", 990 "<!-- 5->8 -->\n", 991 "<g id=\"edge12\" class=\"edge\">\n", 992 "<title>5->8</title>\n", 993 "<path fill=\"none\" stroke=\"black\" d=\"M571.95,-112.04C589.6,-117.13 608.78,-122.67 626.8,-127.87\"/>\n", 994 "<polygon fill=\"black\" stroke=\"black\" points=\"633.9,-129.92 626.3,-131.01 630.54,-128.95 627.18,-127.98 627.18,-127.98 627.18,-127.98 630.54,-128.95 628.05,-124.95 633.9,-129.92 633.9,-129.92\"/>\n", 995 "</g>\n", 996 "<!-- 9 -->\n", 997 "<g id=\"node11\" class=\"node\">\n", 998 "<title>9</title>\n", 999 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M765,-47C765,-47 637,-47 637,-47 631,-47 625,-41 625,-35 625,-35 625,-21 625,-21 625,-15 631,-9 637,-9 637,-9 765,-9 765,-9 771,-9 777,-15 777,-21 777,-21 777,-35 777,-35 777,-41 771,-47 765,-47\"/>\n", 1000 "<text text-anchor=\"start\" x=\"656.5\" y=\"-31.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n", 1001 "<text text-anchor=\"start\" x=\"633\" y=\"-16.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & !dead</text>\n", 1002 "</g>\n", 1003 "<!-- 5->9 -->\n", 1004 "<g id=\"edge13\" class=\"edge\">\n", 1005 "<title>5->9</title>\n", 1006 "<path fill=\"none\" stroke=\"black\" d=\"M562.9,-73.94C585.89,-66.23 612.54,-57.3 636.19,-49.38\"/>\n", 1007 "<polygon fill=\"black\" stroke=\"black\" points=\"643.11,-47.06 637.47,-52.27 639.79,-48.17 636.47,-49.29 636.47,-49.29 636.47,-49.29 639.79,-48.17 635.47,-46.3 643.11,-47.06 643.11,-47.06\"/>\n", 1008 "</g>\n", 1009 "<!-- 10 -->\n", 1010 "<g id=\"node12\" class=\"node\">\n", 1011 "<title>10</title>\n", 1012 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M767,-112C767,-112 635,-112 635,-112 629,-112 623,-106 623,-100 623,-100 623,-86 623,-86 623,-80 629,-74 635,-74 635,-74 767,-74 767,-74 773,-74 779,-80 779,-86 779,-86 779,-100 779,-100 779,-106 773,-112 767,-112\"/>\n", 1013 "<text text-anchor=\"start\" x=\"656.5\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1</text>\n", 1014 "<text text-anchor=\"start\" x=\"631\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1015 "</g>\n", 1016 "<!-- 5->10 -->\n", 1017 "<g id=\"edge14\" class=\"edge\">\n", 1018 "<title>5->10</title>\n", 1019 "<path fill=\"none\" stroke=\"black\" d=\"M583.23,-93C593.89,-93 604.89,-93 615.67,-93\"/>\n", 1020 "<polygon fill=\"black\" stroke=\"black\" points=\"622.72,-93 615.72,-96.15 619.22,-93 615.72,-93 615.72,-93 615.72,-93 619.22,-93 615.72,-89.85 622.72,-93 622.72,-93\"/>\n", 1021 "</g>\n", 1022 "<!-- 6->6 -->\n", 1023 "<g id=\"edge15\" class=\"edge\">\n", 1024 "<title>6->6</title>\n", 1025 "<path fill=\"none\" stroke=\"black\" d=\"M665.34,-280.04C660.4,-289.53 672.29,-298 701,-298 722.08,-298 734.1,-293.43 737.04,-287.25\"/>\n", 1026 "<polygon fill=\"black\" stroke=\"black\" points=\"736.66,-280.04 740.17,-286.87 736.84,-283.53 737.02,-287.03 737.02,-287.03 737.02,-287.03 736.84,-283.53 733.88,-287.19 736.66,-280.04 736.66,-280.04\"/>\n", 1027 "</g>\n", 1028 "<!-- 11 -->\n", 1029 "<g id=\"node13\" class=\"node\">\n", 1030 "<title>11</title>\n", 1031 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M963,-280C963,-280 831,-280 831,-280 825,-280 819,-274 819,-268 819,-268 819,-254 819,-254 819,-248 825,-242 831,-242 831,-242 963,-242 963,-242 969,-242 975,-248 975,-254 975,-254 975,-268 975,-268 975,-274 969,-280 963,-280\"/>\n", 1032 "<text text-anchor=\"start\" x=\"852.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=1, Q=0</text>\n", 1033 "<text text-anchor=\"start\" x=\"827\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 1034 "</g>\n", 1035 "<!-- 7->11 -->\n", 1036 "<g id=\"edge16\" class=\"edge\">\n", 1037 "<title>7->11</title>\n", 1038 "<path fill=\"none\" stroke=\"black\" d=\"M767.95,-224.04C785.6,-229.13 804.78,-234.67 822.8,-239.87\"/>\n", 1039 "<polygon fill=\"black\" stroke=\"black\" points=\"829.9,-241.92 822.3,-243.01 826.54,-240.95 823.18,-239.98 823.18,-239.98 823.18,-239.98 826.54,-240.95 824.05,-236.95 829.9,-241.92 829.9,-241.92\"/>\n", 1040 "</g>\n", 1041 "<!-- 12 -->\n", 1042 "<g id=\"node14\" class=\"node\">\n", 1043 "<title>12</title>\n", 1044 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M965,-224C965,-224 829,-224 829,-224 823,-224 817,-218 817,-212 817,-212 817,-198 817,-198 817,-192 823,-186 829,-186 829,-186 965,-186 965,-186 971,-186 977,-192 977,-198 977,-198 977,-212 977,-212 977,-218 971,-224 965,-224\"/>\n", 1045 "<text text-anchor=\"start\" x=\"852.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=2, Q=0</text>\n", 1046 "<text text-anchor=\"start\" x=\"825\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1047 "</g>\n", 1048 "<!-- 7->12 -->\n", 1049 "<g id=\"edge17\" class=\"edge\">\n", 1050 "<title>7->12</title>\n", 1051 "<path fill=\"none\" stroke=\"black\" d=\"M781.19,-205C790.54,-205 800.12,-205 809.56,-205\"/>\n", 1052 "<polygon fill=\"black\" stroke=\"black\" points=\"816.75,-205 809.75,-208.15 813.25,-205 809.75,-205 809.75,-205 809.75,-205 813.25,-205 809.75,-201.85 816.75,-205 816.75,-205\"/>\n", 1053 "</g>\n", 1054 "<!-- 8->12 -->\n", 1055 "<g id=\"edge18\" class=\"edge\">\n", 1056 "<title>8->12</title>\n", 1057 "<path fill=\"none\" stroke=\"black\" d=\"M767.95,-168.04C785.6,-173.13 804.78,-178.67 822.8,-183.87\"/>\n", 1058 "<polygon fill=\"black\" stroke=\"black\" points=\"829.9,-185.92 822.3,-187.01 826.54,-184.95 823.18,-183.98 823.18,-183.98 823.18,-183.98 826.54,-184.95 824.05,-180.95 829.9,-185.92 829.9,-185.92\"/>\n", 1059 "</g>\n", 1060 "<!-- 13 -->\n", 1061 "<g id=\"node15\" class=\"node\">\n", 1062 "<title>13</title>\n", 1063 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M963,-168C963,-168 831,-168 831,-168 825,-168 819,-162 819,-156 819,-156 819,-142 819,-142 819,-136 825,-130 831,-130 831,-130 963,-130 963,-130 969,-130 975,-136 975,-142 975,-142 975,-156 975,-156 975,-162 969,-168 963,-168\"/>\n", 1064 "<text text-anchor=\"start\" x=\"852.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=3, Q=0</text>\n", 1065 "<text text-anchor=\"start\" x=\"827\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & "b>2" & !dead</text>\n", 1066 "</g>\n", 1067 "<!-- 8->13 -->\n", 1068 "<g id=\"edge19\" class=\"edge\">\n", 1069 "<title>8->13</title>\n", 1070 "<path fill=\"none\" stroke=\"black\" d=\"M781.19,-149C791.32,-149 801.72,-149 811.92,-149\"/>\n", 1071 "<polygon fill=\"black\" stroke=\"black\" points=\"818.95,-149 811.95,-152.15 815.45,-149 811.95,-149 811.95,-149 811.95,-149 815.45,-149 811.95,-145.85 818.95,-149 818.95,-149\"/>\n", 1072 "</g>\n", 1073 "<!-- 14 -->\n", 1074 "<g id=\"node16\" class=\"node\">\n", 1075 "<title>14</title>\n", 1076 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M965,-112C965,-112 829,-112 829,-112 823,-112 817,-106 817,-100 817,-100 817,-86 817,-86 817,-80 823,-74 829,-74 829,-74 965,-74 965,-74 971,-74 977,-80 977,-86 977,-86 977,-100 977,-100 977,-106 971,-112 965,-112\"/>\n", 1077 "<text text-anchor=\"start\" x=\"852.5\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1</text>\n", 1078 "<text text-anchor=\"start\" x=\"825\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1079 "</g>\n", 1080 "<!-- 8->14 -->\n", 1081 "<g id=\"edge20\" class=\"edge\">\n", 1082 "<title>8->14</title>\n", 1083 "<path fill=\"none\" stroke=\"black\" d=\"M767.95,-129.96C785.6,-124.87 804.78,-119.33 822.8,-114.13\"/>\n", 1084 "<polygon fill=\"black\" stroke=\"black\" points=\"829.9,-112.08 824.05,-117.05 826.54,-113.05 823.18,-114.02 823.18,-114.02 823.18,-114.02 826.54,-113.05 822.3,-110.99 829.9,-112.08 829.9,-112.08\"/>\n", 1085 "</g>\n", 1086 "<!-- 15 -->\n", 1087 "<g id=\"node17\" class=\"node\">\n", 1088 "<title>15</title>\n", 1089 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M959.5,-38C959.5,-38 834.5,-38 834.5,-38 828.5,-38 822.5,-32 822.5,-26 822.5,-26 822.5,-12 822.5,-12 822.5,-6 828.5,0 834.5,0 834.5,0 959.5,0 959.5,0 965.5,0 971.5,-6 971.5,-12 971.5,-12 971.5,-26 971.5,-26 971.5,-32 965.5,-38 959.5,-38\"/>\n", 1090 "<text text-anchor=\"start\" x=\"852.5\" y=\"-22.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1</text>\n", 1091 "<text text-anchor=\"start\" x=\"830.5\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & dead</text>\n", 1092 "</g>\n", 1093 "<!-- 9->15 -->\n", 1094 "<g id=\"edge21\" class=\"edge\">\n", 1095 "<title>9->15</title>\n", 1096 "<path fill=\"none\" stroke=\"black\" d=\"M777.01,-24.52C789.6,-23.94 802.72,-23.33 815.45,-22.74\"/>\n", 1097 "<polygon fill=\"black\" stroke=\"black\" points=\"822.47,-22.41 815.62,-25.88 818.97,-22.57 815.48,-22.74 815.48,-22.74 815.48,-22.74 818.97,-22.57 815.33,-19.59 822.47,-22.41 822.47,-22.41\"/>\n", 1098 "</g>\n", 1099 "<!-- 10->14 -->\n", 1100 "<g id=\"edge22\" class=\"edge\">\n", 1101 "<title>10->14</title>\n", 1102 "<path fill=\"none\" stroke=\"black\" d=\"M779.23,-93C789.28,-93 799.62,-93 809.8,-93\"/>\n", 1103 "<polygon fill=\"black\" stroke=\"black\" points=\"816.81,-93 809.81,-96.15 813.31,-93 809.81,-93 809.81,-93 809.81,-93 813.31,-93 809.81,-89.85 816.81,-93 816.81,-93\"/>\n", 1104 "</g>\n", 1105 "<!-- 10->15 -->\n", 1106 "<g id=\"edge23\" class=\"edge\">\n", 1107 "<title>10->15</title>\n", 1108 "<path fill=\"none\" stroke=\"black\" d=\"M751.96,-73.94C778.67,-63.75 811.66,-51.17 839.33,-40.62\"/>\n", 1109 "<polygon fill=\"black\" stroke=\"black\" points=\"845.87,-38.12 840.46,-43.56 842.6,-39.37 839.33,-40.62 839.33,-40.62 839.33,-40.62 842.6,-39.37 838.21,-37.67 845.87,-38.12 845.87,-38.12\"/>\n", 1110 "</g>\n", 1111 "<!-- 11->11 -->\n", 1112 "<g id=\"edge24\" class=\"edge\">\n", 1113 "<title>11->11</title>\n", 1114 "<path fill=\"none\" stroke=\"black\" d=\"M861.34,-280.04C856.4,-289.53 868.29,-298 897,-298 918.08,-298 930.1,-293.43 933.04,-287.25\"/>\n", 1115 "<polygon fill=\"black\" stroke=\"black\" points=\"932.66,-280.04 936.17,-286.87 932.84,-283.53 933.02,-287.03 933.02,-287.03 933.02,-287.03 932.84,-283.53 929.88,-287.19 932.66,-280.04 932.66,-280.04\"/>\n", 1116 "</g>\n", 1117 "<!-- 16 -->\n", 1118 "<g id=\"node18\" class=\"node\">\n", 1119 "<title>16</title>\n", 1120 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1161,-280C1161,-280 1025,-280 1025,-280 1019,-280 1013,-274 1013,-268 1013,-268 1013,-254 1013,-254 1013,-248 1019,-242 1025,-242 1025,-242 1161,-242 1161,-242 1167,-242 1173,-248 1173,-254 1173,-254 1173,-268 1173,-268 1173,-274 1167,-280 1161,-280\"/>\n", 1121 "<text text-anchor=\"start\" x=\"1048.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=2, Q=0</text>\n", 1122 "<text text-anchor=\"start\" x=\"1021\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1123 "</g>\n", 1124 "<!-- 12->16 -->\n", 1125 "<g id=\"edge25\" class=\"edge\">\n", 1126 "<title>12->16</title>\n", 1127 "<path fill=\"none\" stroke=\"black\" d=\"M963.95,-224.04C981.6,-229.13 1000.78,-234.67 1018.8,-239.87\"/>\n", 1128 "<polygon fill=\"black\" stroke=\"black\" points=\"1025.9,-241.92 1018.3,-243.01 1022.54,-240.95 1019.18,-239.98 1019.18,-239.98 1019.18,-239.98 1022.54,-240.95 1020.05,-236.95 1025.9,-241.92 1025.9,-241.92\"/>\n", 1129 "</g>\n", 1130 "<!-- 17 -->\n", 1131 "<g id=\"node19\" class=\"node\">\n", 1132 "<title>17</title>\n", 1133 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1159,-168C1159,-168 1027,-168 1027,-168 1021,-168 1015,-162 1015,-156 1015,-156 1015,-142 1015,-142 1015,-136 1021,-130 1027,-130 1027,-130 1159,-130 1159,-130 1165,-130 1171,-136 1171,-142 1171,-142 1171,-156 1171,-156 1171,-162 1165,-168 1159,-168\"/>\n", 1134 "<text text-anchor=\"start\" x=\"1048.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=3, Q=0</text>\n", 1135 "<text text-anchor=\"start\" x=\"1023\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & "b>2" & !dead</text>\n", 1136 "</g>\n", 1137 "<!-- 12->17 -->\n", 1138 "<g id=\"edge26\" class=\"edge\">\n", 1139 "<title>12->17</title>\n", 1140 "<path fill=\"none\" stroke=\"black\" d=\"M963.95,-185.96C981.6,-180.87 1000.78,-175.33 1018.8,-170.13\"/>\n", 1141 "<polygon fill=\"black\" stroke=\"black\" points=\"1025.9,-168.08 1020.05,-173.05 1022.54,-169.05 1019.18,-170.02 1019.18,-170.02 1019.18,-170.02 1022.54,-169.05 1018.3,-166.99 1025.9,-168.08 1025.9,-168.08\"/>\n", 1142 "</g>\n", 1143 "<!-- 18 -->\n", 1144 "<g id=\"node20\" class=\"node\">\n", 1145 "<title>18</title>\n", 1146 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1161,-224C1161,-224 1025,-224 1025,-224 1019,-224 1013,-218 1013,-212 1013,-212 1013,-198 1013,-198 1013,-192 1019,-186 1025,-186 1025,-186 1161,-186 1161,-186 1167,-186 1173,-192 1173,-198 1173,-198 1173,-212 1173,-212 1173,-218 1167,-224 1161,-224\"/>\n", 1147 "<text text-anchor=\"start\" x=\"1048.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=2, Q=1</text>\n", 1148 "<text text-anchor=\"start\" x=\"1021\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1149 "</g>\n", 1150 "<!-- 12->18 -->\n", 1151 "<g id=\"edge27\" class=\"edge\">\n", 1152 "<title>12->18</title>\n", 1153 "<path fill=\"none\" stroke=\"black\" d=\"M977.19,-198.35C986.54,-198.24 996.12,-198.22 1005.56,-198.29\"/>\n", 1154 "<polygon fill=\"black\" stroke=\"black\" points=\"1012.75,-198.35 1005.72,-201.44 1009.25,-198.32 1005.75,-198.29 1005.75,-198.29 1005.75,-198.29 1009.25,-198.32 1005.78,-195.14 1012.75,-198.35 1012.75,-198.35\"/>\n", 1155 "</g>\n", 1156 "<!-- 19 -->\n", 1157 "<g id=\"node21\" class=\"node\">\n", 1158 "<title>19</title>\n", 1159 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1157,-94C1157,-94 1029,-94 1029,-94 1023,-94 1017,-88 1017,-82 1017,-82 1017,-68 1017,-68 1017,-62 1023,-56 1029,-56 1029,-56 1157,-56 1157,-56 1163,-56 1169,-62 1169,-68 1169,-68 1169,-82 1169,-82 1169,-88 1163,-94 1157,-94\"/>\n", 1160 "<text text-anchor=\"start\" x=\"1048.5\" y=\"-78.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=3, Q=1</text>\n", 1161 "<text text-anchor=\"start\" x=\"1025\" y=\"-63.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & "b>2" & dead</text>\n", 1162 "</g>\n", 1163 "<!-- 13->19 -->\n", 1164 "<g id=\"edge28\" class=\"edge\">\n", 1165 "<title>13->19</title>\n", 1166 "<path fill=\"none\" stroke=\"black\" d=\"M952.93,-129.85C961.02,-126.94 969.24,-123.93 977,-121 997.25,-113.37 1019.35,-104.62 1038.72,-96.83\"/>\n", 1167 "<polygon fill=\"black\" stroke=\"black\" points=\"1045.44,-94.11 1040.13,-99.65 1042.2,-95.42 1038.95,-96.73 1038.95,-96.73 1038.95,-96.73 1042.2,-95.42 1037.77,-93.81 1045.44,-94.11 1045.44,-94.11\"/>\n", 1168 "</g>\n", 1169 "<!-- 14->18 -->\n", 1170 "<g id=\"edge29\" class=\"edge\">\n", 1171 "<title>14->18</title>\n", 1172 "<path fill=\"none\" stroke=\"black\" d=\"M963.26,-112.07C968.13,-114.69 972.78,-117.66 977,-121 1000.19,-139.37 989.81,-158.63 1013,-177 1015.37,-178.88 1017.88,-180.64 1020.49,-182.29\"/>\n", 1173 "<polygon fill=\"black\" stroke=\"black\" points=\"1026.74,-185.93 1019.1,-185.12 1023.71,-184.16 1020.69,-182.4 1020.69,-182.4 1020.69,-182.4 1023.71,-184.16 1022.28,-179.68 1026.74,-185.93 1026.74,-185.93\"/>\n", 1174 "</g>\n", 1175 "<!-- 14->19 -->\n", 1176 "<g id=\"edge30\" class=\"edge\">\n", 1177 "<title>14->19</title>\n", 1178 "<path fill=\"none\" stroke=\"black\" d=\"M977.19,-85.65C987.93,-84.66 998.98,-83.63 1009.77,-82.63\"/>\n", 1179 "<polygon fill=\"black\" stroke=\"black\" points=\"1016.82,-81.98 1010.14,-85.76 1013.34,-82.3 1009.85,-82.62 1009.85,-82.62 1009.85,-82.62 1013.34,-82.3 1009.56,-79.49 1016.82,-81.98 1016.82,-81.98\"/>\n", 1180 "</g>\n", 1181 "<!-- 15->15 -->\n", 1182 "<g id=\"edge31\" class=\"edge\">\n", 1183 "<title>15->15</title>\n", 1184 "<path fill=\"none\" stroke=\"black\" d=\"M861.34,-38.04C856.4,-47.53 868.29,-56 897,-56 918.08,-56 930.1,-51.43 933.04,-45.25\"/>\n", 1185 "<polygon fill=\"black\" stroke=\"black\" points=\"932.66,-38.04 936.17,-44.87 932.84,-41.53 933.02,-45.03 933.02,-45.03 933.02,-45.03 932.84,-41.53 929.88,-45.19 932.66,-38.04 932.66,-38.04\"/>\n", 1186 "</g>\n", 1187 "<!-- 20 -->\n", 1188 "<g id=\"node22\" class=\"node\">\n", 1189 "<title>20</title>\n", 1190 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1357,-280C1357,-280 1221,-280 1221,-280 1215,-280 1209,-274 1209,-268 1209,-268 1209,-254 1209,-254 1209,-248 1215,-242 1221,-242 1221,-242 1357,-242 1357,-242 1363,-242 1369,-248 1369,-254 1369,-254 1369,-268 1369,-268 1369,-274 1363,-280 1357,-280\"/>\n", 1191 "<text text-anchor=\"start\" x=\"1244.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=2, Q=1</text>\n", 1192 "<text text-anchor=\"start\" x=\"1217\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1193 "</g>\n", 1194 "<!-- 16->20 -->\n", 1195 "<g id=\"edge32\" class=\"edge\">\n", 1196 "<title>16->20</title>\n", 1197 "<path fill=\"none\" stroke=\"black\" d=\"M1173.19,-254.35C1182.54,-254.24 1192.12,-254.22 1201.56,-254.29\"/>\n", 1198 "<polygon fill=\"black\" stroke=\"black\" points=\"1208.75,-254.35 1201.72,-257.44 1205.25,-254.32 1201.75,-254.29 1201.75,-254.29 1201.75,-254.29 1205.25,-254.32 1201.78,-251.14 1208.75,-254.35 1208.75,-254.35\"/>\n", 1199 "</g>\n", 1200 "<!-- 21 -->\n", 1201 "<g id=\"node23\" class=\"node\">\n", 1202 "<title>21</title>\n", 1203 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1355,-168C1355,-168 1223,-168 1223,-168 1217,-168 1211,-162 1211,-156 1211,-156 1211,-142 1211,-142 1211,-136 1217,-130 1223,-130 1223,-130 1355,-130 1355,-130 1361,-130 1367,-136 1367,-142 1367,-142 1367,-156 1367,-156 1367,-162 1361,-168 1355,-168\"/>\n", 1204 "<text text-anchor=\"start\" x=\"1244.5\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=3, Q=1</text>\n", 1205 "<text text-anchor=\"start\" x=\"1219\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & "b>2" & !dead</text>\n", 1206 "</g>\n", 1207 "<!-- 17->21 -->\n", 1208 "<g id=\"edge33\" class=\"edge\">\n", 1209 "<title>17->21</title>\n", 1210 "<path fill=\"none\" stroke=\"black\" d=\"M1171.23,-142.38C1181.89,-142.24 1192.89,-142.21 1203.67,-142.3\"/>\n", 1211 "<polygon fill=\"black\" stroke=\"black\" points=\"1210.72,-142.38 1203.68,-145.45 1207.22,-142.34 1203.72,-142.3 1203.72,-142.3 1203.72,-142.3 1207.22,-142.34 1203.75,-139.15 1210.72,-142.38 1210.72,-142.38\"/>\n", 1212 "</g>\n", 1213 "<!-- 18->12 -->\n", 1214 "<g id=\"edge36\" class=\"edge\">\n", 1215 "<title>18->12</title>\n", 1216 "<path fill=\"none\" stroke=\"black\" d=\"M1012.75,-211.65C1003.4,-211.76 993.82,-211.78 984.38,-211.71\"/>\n", 1217 "<polygon fill=\"black\" stroke=\"black\" points=\"977.19,-211.65 984.22,-208.56 980.69,-211.68 984.19,-211.71 984.19,-211.71 984.19,-211.71 980.69,-211.68 984.16,-214.86 977.19,-211.65 977.19,-211.65\"/>\n", 1218 "</g>\n", 1219 "<!-- 18->20 -->\n", 1220 "<g id=\"edge34\" class=\"edge\">\n", 1221 "<title>18->20</title>\n", 1222 "<path fill=\"none\" stroke=\"black\" d=\"M1159.95,-224.04C1177.6,-229.13 1196.78,-234.67 1214.8,-239.87\"/>\n", 1223 "<polygon fill=\"black\" stroke=\"black\" points=\"1221.9,-241.92 1214.3,-243.01 1218.54,-240.95 1215.18,-239.98 1215.18,-239.98 1215.18,-239.98 1218.54,-240.95 1216.05,-236.95 1221.9,-241.92 1221.9,-241.92\"/>\n", 1224 "</g>\n", 1225 "<!-- 18->21 -->\n", 1226 "<g id=\"edge35\" class=\"edge\">\n", 1227 "<title>18->21</title>\n", 1228 "<path fill=\"none\" stroke=\"black\" d=\"M1159.95,-185.96C1177.6,-180.87 1196.78,-175.33 1214.8,-170.13\"/>\n", 1229 "<polygon fill=\"black\" stroke=\"black\" points=\"1221.9,-168.08 1216.05,-173.05 1218.54,-169.05 1215.18,-170.02 1215.18,-170.02 1215.18,-170.02 1218.54,-169.05 1214.3,-166.99 1221.9,-168.08 1221.9,-168.08\"/>\n", 1230 "</g>\n", 1231 "<!-- 19->19 -->\n", 1232 "<g id=\"edge37\" class=\"edge\">\n", 1233 "<title>19->19</title>\n", 1234 "<path fill=\"none\" stroke=\"black\" d=\"M1057.34,-94.04C1052.4,-103.53 1064.29,-112 1093,-112 1114.08,-112 1126.1,-107.43 1129.04,-101.25\"/>\n", 1235 "<polygon fill=\"black\" stroke=\"black\" points=\"1128.66,-94.04 1132.17,-100.87 1128.84,-97.53 1129.02,-101.03 1129.02,-101.03 1129.02,-101.03 1128.84,-97.53 1125.88,-101.19 1128.66,-94.04 1128.66,-94.04\"/>\n", 1236 "</g>\n", 1237 "<!-- 20->16 -->\n", 1238 "<g id=\"edge38\" class=\"edge\">\n", 1239 "<title>20->16</title>\n", 1240 "<path fill=\"none\" stroke=\"black\" d=\"M1208.75,-267.65C1199.4,-267.76 1189.82,-267.78 1180.38,-267.71\"/>\n", 1241 "<polygon fill=\"black\" stroke=\"black\" points=\"1173.19,-267.65 1180.22,-264.56 1176.69,-267.68 1180.19,-267.71 1180.19,-267.71 1180.19,-267.71 1176.69,-267.68 1180.16,-270.86 1173.19,-267.65 1173.19,-267.65\"/>\n", 1242 "</g>\n", 1243 "<!-- 21->17 -->\n", 1244 "<g id=\"edge39\" class=\"edge\">\n", 1245 "<title>21->17</title>\n", 1246 "<path fill=\"none\" stroke=\"black\" d=\"M1210.72,-155.62C1200.05,-155.76 1189.06,-155.79 1178.28,-155.7\"/>\n", 1247 "<polygon fill=\"black\" stroke=\"black\" points=\"1171.23,-155.62 1178.26,-152.55 1174.73,-155.66 1178.23,-155.7 1178.23,-155.7 1178.23,-155.7 1174.73,-155.66 1178.2,-158.85 1171.23,-155.62 1171.23,-155.62\"/>\n", 1248 "</g>\n", 1249 "</g>\n", 1250 "</svg>\n" 1251 ], 1252 "text/plain": [ 1253 "<spot.jupyter.SVG object>" 1254 ] 1255 }, 1256 "execution_count": 11, 1257 "metadata": {}, 1258 "output_type": "execute_result" 1259 } 1260 ], 1261 "source": [ 1262 "k.show('.<0') # unlimited output" 1263 ] 1264 }, 1265 { 1266 "cell_type": "markdown", 1267 "metadata": {}, 1268 "source": [ 1269 "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). " 1270 ] 1271 }, 1272 { 1273 "cell_type": "code", 1274 "execution_count": 12, 1275 "metadata": {}, 1276 "outputs": [ 1277 { 1278 "data": { 1279 "image/svg+xml": [ 1280 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 1281 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 1282 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 1283 "<!-- Generated by graphviz version 2.43.0 (0)\n", 1284 " -->\n", 1285 "<!-- Pages: 1 -->\n", 1286 "<svg width=\"197pt\" height=\"125pt\"\n", 1287 " viewBox=\"0.00 0.00 197.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 1288 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120.8)\">\n", 1289 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 193,-120.8 193,4 -4,4\"/>\n", 1290 "<text text-anchor=\"start\" x=\"73\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n", 1291 "<!-- I -->\n", 1292 "<!-- 1 -->\n", 1293 "<g id=\"node2\" class=\"node\">\n", 1294 "<title>1</title>\n", 1295 "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 1296 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n", 1297 "</g>\n", 1298 "<!-- I->1 -->\n", 1299 "<g id=\"edge1\" class=\"edge\">\n", 1300 "<title>I->1</title>\n", 1301 "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-22C2.79,-22 17.15,-22 30.63,-22\"/>\n", 1302 "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22 30.94,-25.15 34.44,-22 30.94,-22 30.94,-22 30.94,-22 34.44,-22 30.94,-18.85 37.94,-22 37.94,-22\"/>\n", 1303 "</g>\n", 1304 "<!-- 1->1 -->\n", 1305 "<g id=\"edge4\" class=\"edge\">\n", 1306 "<title>1->1</title>\n", 1307 "<path fill=\"none\" stroke=\"black\" d=\"M49.62,-39.04C48.32,-48.86 50.45,-58 56,-58 60.17,-58 62.4,-52.86 62.71,-46.14\"/>\n", 1308 "<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-39.04 65.85,-45.88 62.54,-42.53 62.71,-46.03 62.71,-46.03 62.71,-46.03 62.54,-42.53 59.56,-46.18 62.38,-39.04 62.38,-39.04\"/>\n", 1309 "<text text-anchor=\"start\" x=\"11\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2"</text>\n", 1310 "</g>\n", 1311 "<!-- 0 -->\n", 1312 "<g id=\"node3\" class=\"node\">\n", 1313 "<title>0</title>\n", 1314 "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 1315 "<ellipse fill=\"none\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 1316 "<text text-anchor=\"middle\" x=\"167\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n", 1317 "</g>\n", 1318 "<!-- 1->0 -->\n", 1319 "<g id=\"edge3\" class=\"edge\">\n", 1320 "<title>1->0</title>\n", 1321 "<path fill=\"none\" stroke=\"black\" d=\"M74.03,-22C91.1,-22 117.66,-22 137.86,-22\"/>\n", 1322 "<polygon fill=\"black\" stroke=\"black\" points=\"144.98,-22 137.98,-25.15 141.48,-22 137.98,-22 137.98,-22 137.98,-22 141.48,-22 137.98,-18.85 144.98,-22 144.98,-22\"/>\n", 1323 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">"b>2"</text>\n", 1324 "</g>\n", 1325 "<!-- 0->0 -->\n", 1326 "<g id=\"edge2\" class=\"edge\">\n", 1327 "<title>0->0</title>\n", 1328 "<path fill=\"none\" stroke=\"black\" d=\"M156.93,-41.76C155.22,-52.35 158.58,-62 167,-62 173.45,-62 176.93,-56.34 177.43,-48.94\"/>\n", 1329 "<polygon fill=\"black\" stroke=\"black\" points=\"177.07,-41.76 180.57,-48.59 177.25,-45.25 177.43,-48.75 177.43,-48.75 177.43,-48.75 177.25,-45.25 174.28,-48.91 177.07,-41.76 177.07,-41.76\"/>\n", 1330 "<text text-anchor=\"middle\" x=\"167\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n", 1331 "</g>\n", 1332 "</g>\n", 1333 "</svg>\n" 1334 ], 1335 "text/plain": [ 1336 "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe6bc6bf660> >" 1337 ] 1338 }, 1339 "execution_count": 12, 1340 "metadata": {}, 1341 "output_type": "execute_result" 1342 } 1343 ], 1344 "source": [ 1345 "a = spot.translate('\"a<1\" U \"b>2\"'); a" 1346 ] 1347 }, 1348 { 1349 "cell_type": "code", 1350 "execution_count": 13, 1351 "metadata": {}, 1352 "outputs": [ 1353 { 1354 "data": { 1355 "image/svg+xml": [ 1356 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 1357 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 1358 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 1359 "<!-- Generated by graphviz version 2.43.0 (0)\n", 1360 " -->\n", 1361 "<!-- Pages: 1 -->\n", 1362 "<svg width=\"734pt\" height=\"137pt\"\n", 1363 " viewBox=\"0.00 0.00 734.00 137.49\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 1364 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.5291005291005292 0.5291005291005292) rotate(0) translate(4 256)\">\n", 1365 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-256 1384,-256 1384,4 -4,4\"/>\n", 1366 "<text text-anchor=\"start\" x=\"669.5\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n", 1367 "<text text-anchor=\"start\" x=\"690.5\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 1368 "<text text-anchor=\"start\" x=\"706.5\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n", 1369 "<text text-anchor=\"start\" x=\"668.5\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n", 1370 "<!-- I -->\n", 1371 "<!-- 0 -->\n", 1372 "<g id=\"node2\" class=\"node\">\n", 1373 "<title>0</title>\n", 1374 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M153,-189C153,-189 50,-189 50,-189 44,-189 38,-183 38,-177 38,-177 38,-165 38,-165 38,-159 44,-153 50,-153 50,-153 153,-153 153,-153 159,-153 165,-159 165,-165 165,-165 165,-177 165,-177 165,-183 159,-189 153,-189\"/>\n", 1375 "<text text-anchor=\"start\" x=\"46\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0 * 1</text>\n", 1376 "</g>\n", 1377 "<!-- I->0 -->\n", 1378 "<g id=\"edge1\" class=\"edge\">\n", 1379 "<title>I->0</title>\n", 1380 "<path fill=\"none\" stroke=\"black\" d=\"M1.07,-171C2.14,-171 14.89,-171 30.93,-171\"/>\n", 1381 "<polygon fill=\"black\" stroke=\"black\" points=\"37.98,-171 30.98,-174.15 34.48,-171 30.98,-171 30.98,-171 30.98,-171 34.48,-171 30.98,-167.85 37.98,-171 37.98,-171\"/>\n", 1382 "</g>\n", 1383 "<!-- 1 -->\n", 1384 "<g id=\"node3\" class=\"node\">\n", 1385 "<title>1</title>\n", 1386 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M456,-216C456,-216 353,-216 353,-216 347,-216 341,-210 341,-204 341,-204 341,-192 341,-192 341,-186 347,-180 353,-180 353,-180 456,-180 456,-180 462,-180 468,-186 468,-192 468,-192 468,-204 468,-204 468,-210 462,-216 456,-216\"/>\n", 1387 "<text text-anchor=\"start\" x=\"349\" y=\"-194.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0 * 1</text>\n", 1388 "</g>\n", 1389 "<!-- 0->1 -->\n", 1390 "<g id=\"edge2\" class=\"edge\">\n", 1391 "<title>0->1</title>\n", 1392 "<path fill=\"none\" stroke=\"black\" d=\"M165.23,-176.63C214.43,-181.04 282.87,-187.18 333.78,-191.75\"/>\n", 1393 "<polygon fill=\"black\" stroke=\"black\" points=\"340.85,-192.38 333.59,-194.89 337.36,-192.07 333.88,-191.75 333.88,-191.75 333.88,-191.75 337.36,-192.07 334.16,-188.62 340.85,-192.38 340.85,-192.38\"/>\n", 1394 "<text text-anchor=\"start\" x=\"183\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1395 "</g>\n", 1396 "<!-- 2 -->\n", 1397 "<g id=\"node4\" class=\"node\">\n", 1398 "<title>2</title>\n", 1399 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M456,-162C456,-162 353,-162 353,-162 347,-162 341,-156 341,-150 341,-150 341,-138 341,-138 341,-132 347,-126 353,-126 353,-126 456,-126 456,-126 462,-126 468,-132 468,-138 468,-138 468,-150 468,-150 468,-156 462,-162 456,-162\"/>\n", 1400 "<text text-anchor=\"start\" x=\"349\" y=\"-140.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0 * 1</text>\n", 1401 "</g>\n", 1402 "<!-- 0->2 -->\n", 1403 "<g id=\"edge3\" class=\"edge\">\n", 1404 "<title>0->2</title>\n", 1405 "<path fill=\"none\" stroke=\"black\" d=\"M165.28,-161.15C171.26,-160.36 177.24,-159.62 183,-159 233.23,-153.56 290.12,-149.74 333.53,-147.33\"/>\n", 1406 "<polygon fill=\"black\" stroke=\"black\" points=\"340.65,-146.93 333.84,-150.46 337.16,-147.13 333.66,-147.32 333.66,-147.32 333.66,-147.32 337.16,-147.13 333.49,-144.17 340.65,-146.93 340.65,-146.93\"/>\n", 1407 "<text text-anchor=\"start\" x=\"183\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1408 "</g>\n", 1409 "<!-- 3 -->\n", 1410 "<g id=\"node5\" class=\"node\">\n", 1411 "<title>3</title>\n", 1412 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M759,-189C759,-189 656,-189 656,-189 650,-189 644,-183 644,-177 644,-177 644,-165 644,-165 644,-159 650,-153 656,-153 656,-153 759,-153 759,-153 765,-153 771,-159 771,-165 771,-165 771,-177 771,-177 771,-183 765,-189 759,-189\"/>\n", 1413 "<text text-anchor=\"start\" x=\"652\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0 * 1</text>\n", 1414 "</g>\n", 1415 "<!-- 2->3 -->\n", 1416 "<g id=\"edge4\" class=\"edge\">\n", 1417 "<title>2->3</title>\n", 1418 "<path fill=\"none\" stroke=\"black\" d=\"M468.23,-149.63C517.43,-154.04 585.87,-160.18 636.78,-164.75\"/>\n", 1419 "<polygon fill=\"black\" stroke=\"black\" points=\"643.85,-165.38 636.59,-167.89 640.36,-165.07 636.88,-164.75 636.88,-164.75 636.88,-164.75 640.36,-165.07 637.16,-161.62 643.85,-165.38 643.85,-165.38\"/>\n", 1420 "<text text-anchor=\"start\" x=\"486\" y=\"-166.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1421 "</g>\n", 1422 "<!-- 4 -->\n", 1423 "<g id=\"node6\" class=\"node\">\n", 1424 "<title>4</title>\n", 1425 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M759,-135C759,-135 656,-135 656,-135 650,-135 644,-129 644,-123 644,-123 644,-111 644,-111 644,-105 650,-99 656,-99 656,-99 759,-99 759,-99 765,-99 771,-105 771,-111 771,-111 771,-123 771,-123 771,-129 765,-135 759,-135\"/>\n", 1426 "<text text-anchor=\"start\" x=\"652\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0 * 1</text>\n", 1427 "</g>\n", 1428 "<!-- 2->4 -->\n", 1429 "<g id=\"edge5\" class=\"edge\">\n", 1430 "<title>2->4</title>\n", 1431 "<path fill=\"none\" stroke=\"black\" d=\"M468.28,-134.15C474.26,-133.36 480.24,-132.62 486,-132 536.23,-126.56 593.12,-122.74 636.53,-120.33\"/>\n", 1432 "<polygon fill=\"black\" stroke=\"black\" points=\"643.65,-119.93 636.84,-123.46 640.16,-120.13 636.66,-120.32 636.66,-120.32 636.66,-120.32 640.16,-120.13 636.49,-117.17 643.65,-119.93 643.65,-119.93\"/>\n", 1433 "<text text-anchor=\"start\" x=\"486\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1434 "</g>\n", 1435 "<!-- 5 -->\n", 1436 "<g id=\"node7\" class=\"node\">\n", 1437 "<title>5</title>\n", 1438 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1062,-189C1062,-189 959,-189 959,-189 953,-189 947,-183 947,-177 947,-177 947,-165 947,-165 947,-159 953,-153 959,-153 959,-153 1062,-153 1062,-153 1068,-153 1074,-159 1074,-165 1074,-165 1074,-177 1074,-177 1074,-183 1068,-189 1062,-189\"/>\n", 1439 "<text text-anchor=\"start\" x=\"955\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0 * 1</text>\n", 1440 "</g>\n", 1441 "<!-- 4->5 -->\n", 1442 "<g id=\"edge6\" class=\"edge\">\n", 1443 "<title>4->5</title>\n", 1444 "<path fill=\"none\" stroke=\"black\" d=\"M771.24,-132.29C777.23,-133.6 783.22,-134.86 789,-136 839.07,-145.87 895.97,-154.85 939.42,-161.24\"/>\n", 1445 "<polygon fill=\"black\" stroke=\"black\" points=\"946.55,-162.28 939.17,-164.38 943.09,-161.77 939.62,-161.27 939.62,-161.27 939.62,-161.27 943.09,-161.77 940.08,-158.15 946.55,-162.28 946.55,-162.28\"/>\n", 1446 "<text text-anchor=\"start\" x=\"789\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1447 "</g>\n", 1448 "<!-- 6 -->\n", 1449 "<g id=\"node8\" class=\"node\">\n", 1450 "<title>6</title>\n", 1451 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1062,-135C1062,-135 959,-135 959,-135 953,-135 947,-129 947,-123 947,-123 947,-111 947,-111 947,-105 953,-99 959,-99 959,-99 1062,-99 1062,-99 1068,-99 1074,-105 1074,-111 1074,-111 1074,-123 1074,-123 1074,-129 1068,-135 1062,-135\"/>\n", 1452 "<text text-anchor=\"start\" x=\"955\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0 * 1</text>\n", 1453 "</g>\n", 1454 "<!-- 4->6 -->\n", 1455 "<g id=\"edge7\" class=\"edge\">\n", 1456 "<title>4->6</title>\n", 1457 "<path fill=\"none\" stroke=\"black\" d=\"M771.23,-117C820.43,-117 888.87,-117 939.78,-117\"/>\n", 1458 "<polygon fill=\"black\" stroke=\"black\" points=\"946.85,-117 939.85,-120.15 943.35,-117 939.85,-117 939.85,-117 939.85,-117 943.35,-117 939.85,-113.85 946.85,-117 946.85,-117\"/>\n", 1459 "<text text-anchor=\"start\" x=\"789\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1460 "</g>\n", 1461 "<!-- 7 -->\n", 1462 "<g id=\"node9\" class=\"node\">\n", 1463 "<title>7</title>\n", 1464 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1062,-81C1062,-81 959,-81 959,-81 953,-81 947,-75 947,-69 947,-69 947,-57 947,-57 947,-51 953,-45 959,-45 959,-45 1062,-45 1062,-45 1068,-45 1074,-51 1074,-57 1074,-57 1074,-69 1074,-69 1074,-75 1068,-81 1062,-81\"/>\n", 1465 "<text text-anchor=\"start\" x=\"955\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1 * 1</text>\n", 1466 "</g>\n", 1467 "<!-- 4->7 -->\n", 1468 "<g id=\"edge8\" class=\"edge\">\n", 1469 "<title>4->7</title>\n", 1470 "<path fill=\"none\" stroke=\"black\" d=\"M771.24,-101.71C777.23,-100.4 783.22,-99.14 789,-98 839.07,-88.13 895.97,-79.15 939.42,-72.76\"/>\n", 1471 "<polygon fill=\"black\" stroke=\"black\" points=\"946.55,-71.72 940.08,-75.85 943.09,-72.23 939.62,-72.73 939.62,-72.73 939.62,-72.73 943.09,-72.23 939.17,-69.62 946.55,-71.72 946.55,-71.72\"/>\n", 1472 "<text text-anchor=\"start\" x=\"789\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1473 "</g>\n", 1474 "<!-- 8 -->\n", 1475 "<g id=\"node10\" class=\"node\">\n", 1476 "<title>8</title>\n", 1477 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1365,-135C1365,-135 1262,-135 1262,-135 1256,-135 1250,-129 1250,-123 1250,-123 1250,-111 1250,-111 1250,-105 1256,-99 1262,-99 1262,-99 1365,-99 1365,-99 1371,-99 1377,-105 1377,-111 1377,-111 1377,-123 1377,-123 1377,-129 1371,-135 1365,-135\"/>\n", 1478 "<text text-anchor=\"start\" x=\"1258\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1 * 0</text>\n", 1479 "</g>\n", 1480 "<!-- 6->8 -->\n", 1481 "<g id=\"edge9\" class=\"edge\">\n", 1482 "<title>6->8</title>\n", 1483 "<path fill=\"none\" stroke=\"black\" d=\"M1074.23,-117C1123.43,-117 1191.87,-117 1242.78,-117\"/>\n", 1484 "<polygon fill=\"black\" stroke=\"black\" points=\"1249.85,-117 1242.85,-120.15 1246.35,-117 1242.85,-117 1242.85,-117 1242.85,-117 1246.35,-117 1242.85,-113.85 1249.85,-117 1249.85,-117\"/>\n", 1485 "<text text-anchor=\"start\" x=\"1094\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & !dead</text>\n", 1486 "</g>\n", 1487 "<!-- u7 -->\n", 1488 "<g id=\"node11\" class=\"node\">\n", 1489 "<title>u7</title>\n", 1490 "<g id=\"a_node11\"><a xlink:title=\"hidden successors\">\n", 1491 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M1318.83,-77.5C1318.83,-77.5 1308.17,-77.5 1308.17,-77.5 1304.33,-77.5 1300.5,-73.67 1300.5,-69.83 1300.5,-69.83 1300.5,-62.17 1300.5,-62.17 1300.5,-58.33 1304.33,-54.5 1308.17,-54.5 1308.17,-54.5 1318.83,-54.5 1318.83,-54.5 1322.67,-54.5 1326.5,-58.33 1326.5,-62.17 1326.5,-62.17 1326.5,-69.83 1326.5,-69.83 1326.5,-73.67 1322.67,-77.5 1318.83,-77.5\"/>\n", 1492 "<text text-anchor=\"middle\" x=\"1313.5\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 1493 "</a>\n", 1494 "</g>\n", 1495 "</g>\n", 1496 "<!-- 7->u7 -->\n", 1497 "<g id=\"edge10\" class=\"edge\">\n", 1498 "<title>7->u7</title>\n", 1499 "<g id=\"a_edge10\"><a xlink:title=\"hidden successors\">\n", 1500 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1074.23,-63.63C1143.15,-64.31 1249.8,-65.38 1293.17,-65.81\"/>\n", 1501 "<polygon fill=\"black\" stroke=\"black\" points=\"1300.28,-65.88 1293.25,-68.96 1296.78,-65.84 1293.28,-65.81 1293.28,-65.81 1293.28,-65.81 1296.78,-65.84 1293.31,-62.66 1300.28,-65.88 1300.28,-65.88\"/>\n", 1502 "</a>\n", 1503 "</g>\n", 1504 "</g>\n", 1505 "<!-- 9 -->\n", 1506 "<g id=\"node12\" class=\"node\">\n", 1507 "<title>9</title>\n", 1508 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1365,-36C1365,-36 1262,-36 1262,-36 1256,-36 1250,-30 1250,-24 1250,-24 1250,-12 1250,-12 1250,-6 1256,0 1262,0 1262,0 1365,0 1365,0 1371,0 1377,-6 1377,-12 1377,-12 1377,-24 1377,-24 1377,-30 1371,-36 1365,-36\"/>\n", 1509 "<text text-anchor=\"start\" x=\"1258\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1 * 1</text>\n", 1510 "</g>\n", 1511 "<!-- 7->9 -->\n", 1512 "<g id=\"edge11\" class=\"edge\">\n", 1513 "<title>7->9</title>\n", 1514 "<path fill=\"none\" stroke=\"black\" d=\"M1074.2,-47.47C1080.2,-46.21 1086.2,-45.02 1092,-44 1142.16,-35.15 1199.29,-28.51 1242.83,-24.16\"/>\n", 1515 "<polygon fill=\"black\" stroke=\"black\" points=\"1249.97,-23.45 1243.31,-27.27 1246.49,-23.79 1243,-24.14 1243,-24.14 1243,-24.14 1246.49,-23.79 1242.69,-21 1249.97,-23.45 1249.97,-23.45\"/>\n", 1516 "<text text-anchor=\"start\" x=\"1092\" y=\"-47.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1517 "</g>\n", 1518 "<!-- 8->8 -->\n", 1519 "<g id=\"edge12\" class=\"edge\">\n", 1520 "<title>8->8</title>\n", 1521 "<path fill=\"none\" stroke=\"black\" d=\"M1286.36,-135.15C1282.19,-144.54 1291.23,-153 1313.5,-153 1329.85,-153 1339.07,-148.44 1341.16,-142.3\"/>\n", 1522 "<polygon fill=\"black\" stroke=\"black\" points=\"1340.64,-135.15 1344.29,-141.9 1340.89,-138.64 1341.15,-142.13 1341.15,-142.13 1341.15,-142.13 1340.89,-138.64 1338.01,-142.37 1340.64,-135.15 1340.64,-135.15\"/>\n", 1523 "<text text-anchor=\"start\" x=\"1247\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & dead</text>\n", 1524 "<text text-anchor=\"start\" x=\"1305.5\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 1525 "</g>\n", 1526 "</g>\n", 1527 "</svg>\n" 1528 ], 1529 "text/plain": [ 1530 "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fe6bc6afc30> >" 1531 ] 1532 }, 1533 "execution_count": 13, 1534 "metadata": {}, 1535 "output_type": "execute_result" 1536 } 1537 ], 1538 "source": [ 1539 "spot.otf_product(k, a)" 1540 ] 1541 }, 1542 { 1543 "cell_type": "markdown", 1544 "metadata": {}, 1545 "source": [ 1546 "If we want to create a `model_check` function that takes a model and formula, we need to get the list of atomic propositions used in the formula using `atomic_prop_collect()`. This returns an `atomic_prop_set`:" 1547 ] 1548 }, 1549 { 1550 "cell_type": "code", 1551 "execution_count": 14, 1552 "metadata": {}, 1553 "outputs": [ 1554 { 1555 "data": { 1556 "text/latex": [ 1557 "$\\{\\unicode{x201C}\\mathit{a < 2}\\unicode{x201D}, \\unicode{x201C}\\mathit{b == 1}\\unicode{x201D}\\}$" 1558 ], 1559 "text/plain": [ 1560 "spot.atomic_prop_set([spot.formula(\"\\\"a < 2\\\"\"), spot.formula(\"\\\"b == 1\\\"\")])" 1561 ] 1562 }, 1563 "execution_count": 14, 1564 "metadata": {}, 1565 "output_type": "execute_result" 1566 } 1567 ], 1568 "source": [ 1569 "a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"')); a" 1570 ] 1571 }, 1572 { 1573 "cell_type": "code", 1574 "execution_count": 15, 1575 "metadata": {}, 1576 "outputs": [], 1577 "source": [ 1578 "def model_check(f, m):\n", 1579 " nf = spot.formula.Not(f)\n", 1580 " ss = m.kripke(spot.atomic_prop_collect(nf))\n", 1581 " return spot.otf_product(ss, nf.translate()).is_empty() " 1582 ] 1583 }, 1584 { 1585 "cell_type": "code", 1586 "execution_count": 16, 1587 "metadata": {}, 1588 "outputs": [ 1589 { 1590 "data": { 1591 "text/plain": [ 1592 "False" 1593 ] 1594 }, 1595 "execution_count": 16, 1596 "metadata": {}, 1597 "output_type": "execute_result" 1598 } 1599 ], 1600 "source": [ 1601 "model_check('\"a<1\" R \"b > 1\"', m)" 1602 ] 1603 }, 1604 { 1605 "cell_type": "markdown", 1606 "metadata": {}, 1607 "source": [ 1608 "Instead of `otf_product(x, y).is_empty()` we prefer to call `!x.intersects(y)`. There is also `x.intersecting_run(y)` that can be used to return a counterexample." 1609 ] 1610 }, 1611 { 1612 "cell_type": "code", 1613 "execution_count": 17, 1614 "metadata": {}, 1615 "outputs": [], 1616 "source": [ 1617 "def model_debug(f, m):\n", 1618 " nf = spot.formula.Not(f)\n", 1619 " ss = m.kripke(spot.atomic_prop_collect(nf))\n", 1620 " return ss.intersecting_run(nf.translate())" 1621 ] 1622 }, 1623 { 1624 "cell_type": "code", 1625 "execution_count": 18, 1626 "metadata": {}, 1627 "outputs": [ 1628 { 1629 "name": "stdout", 1630 "output_type": "stream", 1631 "text": [ 1632 "Prefix:\n", 1633 " a=0, b=0, Q=0\n", 1634 " | \"a<1\" & !\"b > 1\" & !dead\n", 1635 " a=1, b=0, Q=0\n", 1636 " | !\"a<1\" & !\"b > 1\" & !dead\n", 1637 " a=2, b=0, Q=0\n", 1638 " | !\"a<1\" & !\"b > 1\" & !dead\n", 1639 "Cycle:\n", 1640 " a=3, b=0, Q=0\n", 1641 " | !\"a<1\" & !\"b > 1\" & dead\n", 1642 "\n" 1643 ] 1644 } 1645 ], 1646 "source": [ 1647 "run = model_debug('\"a<1\" R \"b > 1\"', m); print(run)" 1648 ] 1649 }, 1650 { 1651 "cell_type": "markdown", 1652 "metadata": {}, 1653 "source": [ 1654 "This accepting run can be represented as an automaton (the `True` argument requires the state names to be preserved). This can be more readable." 1655 ] 1656 }, 1657 { 1658 "cell_type": "code", 1659 "execution_count": 19, 1660 "metadata": {}, 1661 "outputs": [ 1662 { 1663 "data": { 1664 "image/svg+xml": [ 1665 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 1666 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 1667 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 1668 "<!-- Generated by graphviz version 2.43.0 (0)\n", 1669 " -->\n", 1670 "<!-- Pages: 1 -->\n", 1671 "<svg width=\"734pt\" height=\"81pt\"\n", 1672 " viewBox=\"0.00 0.00 734.00 80.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 1673 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7042253521126761 0.7042253521126761) rotate(0) translate(4 111)\">\n", 1674 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 1041.5,-111 1041.5,4 -4,4\"/>\n", 1675 "<text text-anchor=\"start\" x=\"515.75\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n", 1676 "<text text-anchor=\"start\" x=\"507.75\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n", 1677 "<!-- I -->\n", 1678 "<!-- 0 -->\n", 1679 "<g id=\"node2\" class=\"node\">\n", 1680 "<title>0</title>\n", 1681 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M131,-36C131,-36 50,-36 50,-36 44,-36 38,-30 38,-24 38,-24 38,-12 38,-12 38,-6 44,0 50,0 50,0 131,0 131,0 137,0 143,-6 143,-12 143,-12 143,-24 143,-24 143,-30 137,-36 131,-36\"/>\n", 1682 "<text text-anchor=\"start\" x=\"46\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n", 1683 "</g>\n", 1684 "<!-- I->0 -->\n", 1685 "<g id=\"edge1\" class=\"edge\">\n", 1686 "<title>I->0</title>\n", 1687 "<path fill=\"none\" stroke=\"black\" d=\"M1.06,-18C2.08,-18 14.94,-18 30.56,-18\"/>\n", 1688 "<polygon fill=\"black\" stroke=\"black\" points=\"37.9,-18 30.9,-21.15 34.4,-18 30.9,-18 30.9,-18 30.9,-18 34.4,-18 30.9,-14.85 37.9,-18 37.9,-18\"/>\n", 1689 "</g>\n", 1690 "<!-- 1 -->\n", 1691 "<g id=\"node3\" class=\"node\">\n", 1692 "<title>1</title>\n", 1693 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M420,-36C420,-36 339,-36 339,-36 333,-36 327,-30 327,-24 327,-24 327,-12 327,-12 327,-6 333,0 339,0 339,0 420,0 420,0 426,0 432,-6 432,-12 432,-12 432,-24 432,-24 432,-30 426,-36 420,-36\"/>\n", 1694 "<text text-anchor=\"start\" x=\"335\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n", 1695 "</g>\n", 1696 "<!-- 0->1 -->\n", 1697 "<g id=\"edge2\" class=\"edge\">\n", 1698 "<title>0->1</title>\n", 1699 "<path fill=\"none\" stroke=\"black\" d=\"M143.14,-18C192.77,-18 267.7,-18 319.62,-18\"/>\n", 1700 "<polygon fill=\"black\" stroke=\"black\" points=\"326.79,-18 319.79,-21.15 323.29,-18 319.79,-18 319.79,-18 319.79,-18 323.29,-18 319.79,-14.85 326.79,-18 326.79,-18\"/>\n", 1701 "<text text-anchor=\"start\" x=\"161\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b > 1" & !dead</text>\n", 1702 "</g>\n", 1703 "<!-- 2 -->\n", 1704 "<g id=\"node4\" class=\"node\">\n", 1705 "<title>2</title>\n", 1706 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M712,-36C712,-36 631,-36 631,-36 625,-36 619,-30 619,-24 619,-24 619,-12 619,-12 619,-6 625,0 631,0 631,0 712,0 712,0 718,0 724,-6 724,-12 724,-12 724,-24 724,-24 724,-30 718,-36 712,-36\"/>\n", 1707 "<text text-anchor=\"start\" x=\"627\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n", 1708 "</g>\n", 1709 "<!-- 1->2 -->\n", 1710 "<g id=\"edge3\" class=\"edge\">\n", 1711 "<title>1->2</title>\n", 1712 "<path fill=\"none\" stroke=\"black\" d=\"M432.01,-18C482.38,-18 558.98,-18 611.7,-18\"/>\n", 1713 "<polygon fill=\"black\" stroke=\"black\" points=\"618.98,-18 611.98,-21.15 615.48,-18 611.98,-18 611.98,-18 611.98,-18 615.48,-18 611.98,-14.85 618.98,-18 618.98,-18\"/>\n", 1714 "<text text-anchor=\"start\" x=\"450\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b > 1" & !dead</text>\n", 1715 "</g>\n", 1716 "<!-- 3 -->\n", 1717 "<g id=\"node5\" class=\"node\">\n", 1718 "<title>3</title>\n", 1719 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M1004,-36C1004,-36 923,-36 923,-36 917,-36 911,-30 911,-24 911,-24 911,-12 911,-12 911,-6 917,0 923,0 923,0 1004,0 1004,0 1010,0 1016,-6 1016,-12 1016,-12 1016,-24 1016,-24 1016,-30 1010,-36 1004,-36\"/>\n", 1720 "<text text-anchor=\"start\" x=\"919\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n", 1721 "</g>\n", 1722 "<!-- 2->3 -->\n", 1723 "<g id=\"edge4\" class=\"edge\">\n", 1724 "<title>2->3</title>\n", 1725 "<path fill=\"none\" stroke=\"black\" d=\"M724.01,-18C774.38,-18 850.98,-18 903.7,-18\"/>\n", 1726 "<polygon fill=\"black\" stroke=\"black\" points=\"910.98,-18 903.98,-21.15 907.48,-18 903.98,-18 903.98,-18 903.98,-18 907.48,-18 903.98,-14.85 910.98,-18 910.98,-18\"/>\n", 1727 "<text text-anchor=\"start\" x=\"742\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b > 1" & !dead</text>\n", 1728 "</g>\n", 1729 "<!-- 3->3 -->\n", 1730 "<g id=\"edge5\" class=\"edge\">\n", 1731 "<title>3->3</title>\n", 1732 "<path fill=\"none\" stroke=\"black\" d=\"M937.09,-36.15C933.02,-45.54 941.83,-54 963.5,-54 979.42,-54 988.39,-49.44 990.43,-43.3\"/>\n", 1733 "<polygon fill=\"black\" stroke=\"black\" points=\"989.91,-36.15 993.56,-42.91 990.16,-39.64 990.42,-43.13 990.42,-43.13 990.42,-43.13 990.16,-39.64 987.27,-43.36 989.91,-36.15 989.91,-36.15\"/>\n", 1734 "<text text-anchor=\"start\" x=\"889.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b > 1" & dead</text>\n", 1735 "</g>\n", 1736 "</g>\n", 1737 "</svg>\n" 1738 ], 1739 "text/plain": [ 1740 "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe6bc6cbcc0> >" 1741 ] 1742 }, 1743 "execution_count": 19, 1744 "metadata": {}, 1745 "output_type": "execute_result" 1746 } 1747 ], 1748 "source": [ 1749 "run.as_twa(True)" 1750 ] 1751 }, 1752 { 1753 "cell_type": "markdown", 1754 "metadata": {}, 1755 "source": [ 1756 "# Saving Kripke structures to some file\n", 1757 "\n", 1758 "For experiments, it is sometime useful to save a Kripke structure in the HOA format. The HOA printer will automatically use `state-labels` for Kripke structures." 1759 ] 1760 }, 1761 { 1762 "cell_type": "code", 1763 "execution_count": 20, 1764 "metadata": {}, 1765 "outputs": [ 1766 { 1767 "name": "stdout", 1768 "output_type": "stream", 1769 "text": [ 1770 "HOA: v1\n", 1771 "States: 22\n", 1772 "Start: 0\n", 1773 "AP: 3 \"a<1\" \"b>2\" \"dead\"\n", 1774 "acc-name: all\n", 1775 "Acceptance: 0 t\n", 1776 "properties: state-labels explicit-labels state-acc\n", 1777 "--BODY--\n", 1778 "State: [0&!1&!2] 0 \"a=0, b=0, Q=0\"\n", 1779 "1 2\n", 1780 "State: [!0&!1&!2] 1 \"a=1, b=0, Q=0\"\n", 1781 "3 4\n", 1782 "State: [0&!1&!2] 2 \"a=0, b=1, Q=0\"\n", 1783 "4 5\n", 1784 "State: [!0&!1&!2] 3 \"a=2, b=0, Q=0\"\n", 1785 "6 7\n", 1786 "State: [!0&!1&!2] 4 \"a=1, b=1, Q=0\"\n", 1787 "7 8\n", 1788 "State: [0&!1&!2] 5 \"a=0, b=2, Q=0\"\n", 1789 "8 9 10\n", 1790 "State: [!0&!1&2] 6 \"a=3, b=0, Q=0\"\n", 1791 "6\n", 1792 "State: [!0&!1&!2] 7 \"a=2, b=1, Q=0\"\n", 1793 "11 12\n", 1794 "State: [!0&!1&!2] 8 \"a=1, b=2, Q=0\"\n", 1795 "12 13 14\n", 1796 "State: [0&1&!2] 9 \"a=0, b=3, Q=0\"\n", 1797 "15\n", 1798 "State: [0&!1&!2] 10 \"a=0, b=2, Q=1\"\n", 1799 "14 15\n", 1800 "State: [!0&!1&2] 11 \"a=3, b=1, Q=0\"\n", 1801 "11\n", 1802 "State: [!0&!1&!2] 12 \"a=2, b=2, Q=0\"\n", 1803 "16 17 18\n", 1804 "State: [!0&1&!2] 13 \"a=1, b=3, Q=0\"\n", 1805 "19\n", 1806 "State: [!0&!1&!2] 14 \"a=1, b=2, Q=1\"\n", 1807 "18 19\n", 1808 "State: [0&1&2] 15 \"a=0, b=3, Q=1\"\n", 1809 "15\n", 1810 "State: [!0&!1&!2] 16 \"a=3, b=2, Q=0\"\n", 1811 "20\n", 1812 "State: [!0&1&!2] 17 \"a=2, b=3, Q=0\"\n", 1813 "21\n", 1814 "State: [!0&!1&!2] 18 \"a=2, b=2, Q=1\"\n", 1815 "20 21 12\n", 1816 "State: [!0&1&2] 19 \"a=1, b=3, Q=1\"\n", 1817 "19\n", 1818 "State: [!0&!1&!2] 20 \"a=3, b=2, Q=1\"\n", 1819 "16\n", 1820 "State: [!0&1&!2] 21 \"a=2, b=3, Q=1\"\n", 1821 "17\n", 1822 "--END--\n" 1823 ] 1824 } 1825 ], 1826 "source": [ 1827 "string = k.to_str('hoa')\n", 1828 "print(string)" 1829 ] 1830 }, 1831 { 1832 "cell_type": "markdown", 1833 "metadata": {}, 1834 "source": [ 1835 "You can load this as a Kripke structure by passing the `want_kripke` option to `spot.automaton()`. The type `kripke_graph` stores the Kripke structure explicitely (like a `twa_graph` stores an automaton explicitely), so you may want to avoid it for very large modelsand use it only for development." 1836 ] 1837 }, 1838 { 1839 "cell_type": "code", 1840 "execution_count": 21, 1841 "metadata": {}, 1842 "outputs": [ 1843 { 1844 "name": "stdout", 1845 "output_type": "stream", 1846 "text": [ 1847 "<class 'spot.impl.kripke_graph'>\n" 1848 ] 1849 }, 1850 { 1851 "data": { 1852 "image/svg+xml": [ 1853 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 1854 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 1855 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 1856 "<!-- Generated by graphviz version 2.43.0 (0)\n", 1857 " -->\n", 1858 "<!-- Pages: 1 -->\n", 1859 "<svg width=\"734pt\" height=\"270pt\"\n", 1860 " viewBox=\"0.00 0.00 734.00 270.38\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 1861 "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8695652173913044 0.8695652173913044) rotate(0) translate(4 308)\">\n", 1862 "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-308 843,-308 843,4 -4,4\"/>\n", 1863 "<text text-anchor=\"start\" x=\"416.5\" y=\"-288.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n", 1864 "<text text-anchor=\"start\" x=\"408.5\" y=\"-273.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n", 1865 "<!-- I -->\n", 1866 "<!-- 0 -->\n", 1867 "<g id=\"node2\" class=\"node\">\n", 1868 "<title>0</title>\n", 1869 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M181,-143C181,-143 49,-143 49,-143 43,-143 37,-137 37,-131 37,-131 37,-117 37,-117 37,-111 43,-105 49,-105 49,-105 181,-105 181,-105 187,-105 193,-111 193,-117 193,-117 193,-131 193,-131 193,-137 187,-143 181,-143\"/>\n", 1870 "<text text-anchor=\"start\" x=\"70.5\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n", 1871 "<text text-anchor=\"start\" x=\"45\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1872 "</g>\n", 1873 "<!-- I->0 -->\n", 1874 "<g id=\"edge1\" class=\"edge\">\n", 1875 "<title>I->0</title>\n", 1876 "<path fill=\"none\" stroke=\"black\" d=\"M1.08,-124C2.17,-124 13.89,-124 29.41,-124\"/>\n", 1877 "<polygon fill=\"black\" stroke=\"black\" points=\"36.78,-124 29.78,-127.15 33.28,-124 29.78,-124 29.78,-124 29.78,-124 33.28,-124 29.78,-120.85 36.78,-124 36.78,-124\"/>\n", 1878 "</g>\n", 1879 "<!-- 1 -->\n", 1880 "<g id=\"node3\" class=\"node\">\n", 1881 "<title>1</title>\n", 1882 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M377,-171C377,-171 241,-171 241,-171 235,-171 229,-165 229,-159 229,-159 229,-145 229,-145 229,-139 235,-133 241,-133 241,-133 377,-133 377,-133 383,-133 389,-139 389,-145 389,-145 389,-159 389,-159 389,-165 383,-171 377,-171\"/>\n", 1883 "<text text-anchor=\"start\" x=\"264.5\" y=\"-155.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n", 1884 "<text text-anchor=\"start\" x=\"237\" y=\"-140.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1885 "</g>\n", 1886 "<!-- 0->1 -->\n", 1887 "<g id=\"edge2\" class=\"edge\">\n", 1888 "<title>0->1</title>\n", 1889 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-135.27C202.56,-136.62 212.11,-138.02 221.53,-139.39\"/>\n", 1890 "<polygon fill=\"black\" stroke=\"black\" points=\"228.7,-140.44 221.32,-142.54 225.24,-139.93 221.78,-139.43 221.78,-139.43 221.78,-139.43 225.24,-139.93 222.23,-136.31 228.7,-140.44 228.7,-140.44\"/>\n", 1891 "</g>\n", 1892 "<!-- 2 -->\n", 1893 "<g id=\"node4\" class=\"node\">\n", 1894 "<title>2</title>\n", 1895 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M375,-115C375,-115 243,-115 243,-115 237,-115 231,-109 231,-103 231,-103 231,-89 231,-89 231,-83 237,-77 243,-77 243,-77 375,-77 375,-77 381,-77 387,-83 387,-89 387,-89 387,-103 387,-103 387,-109 381,-115 375,-115\"/>\n", 1896 "<text text-anchor=\"start\" x=\"264.5\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n", 1897 "<text text-anchor=\"start\" x=\"239\" y=\"-84.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1898 "</g>\n", 1899 "<!-- 0->2 -->\n", 1900 "<g id=\"edge3\" class=\"edge\">\n", 1901 "<title>0->2</title>\n", 1902 "<path fill=\"none\" stroke=\"black\" d=\"M193.26,-112.73C203.34,-111.26 213.7,-109.75 223.88,-108.27\"/>\n", 1903 "<polygon fill=\"black\" stroke=\"black\" points=\"230.89,-107.24 224.42,-111.37 227.43,-107.75 223.97,-108.25 223.97,-108.25 223.97,-108.25 227.43,-107.75 223.51,-105.14 230.89,-107.24 230.89,-107.24\"/>\n", 1904 "</g>\n", 1905 "<!-- 3 -->\n", 1906 "<g id=\"node5\" class=\"node\">\n", 1907 "<title>3</title>\n", 1908 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-199C573,-199 437,-199 437,-199 431,-199 425,-193 425,-187 425,-187 425,-173 425,-173 425,-167 431,-161 437,-161 437,-161 573,-161 573,-161 579,-161 585,-167 585,-173 585,-173 585,-187 585,-187 585,-193 579,-199 573,-199\"/>\n", 1909 "<text text-anchor=\"start\" x=\"460.5\" y=\"-183.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n", 1910 "<text text-anchor=\"start\" x=\"433\" y=\"-168.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1911 "</g>\n", 1912 "<!-- 1->3 -->\n", 1913 "<g id=\"edge4\" class=\"edge\">\n", 1914 "<title>1->3</title>\n", 1915 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-163.43C398.54,-164.78 408.12,-166.16 417.56,-167.52\"/>\n", 1916 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-168.56 417.37,-170.68 421.29,-168.06 417.82,-167.56 417.82,-167.56 417.82,-167.56 421.29,-168.06 418.27,-164.44 424.75,-168.56 424.75,-168.56\"/>\n", 1917 "</g>\n", 1918 "<!-- 4 -->\n", 1919 "<g id=\"node6\" class=\"node\">\n", 1920 "<title>4</title>\n", 1921 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M573,-143C573,-143 437,-143 437,-143 431,-143 425,-137 425,-131 425,-131 425,-117 425,-117 425,-111 431,-105 437,-105 437,-105 573,-105 573,-105 579,-105 585,-111 585,-117 585,-117 585,-131 585,-131 585,-137 579,-143 573,-143\"/>\n", 1922 "<text text-anchor=\"start\" x=\"460.5\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n", 1923 "<text text-anchor=\"start\" x=\"433\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n", 1924 "</g>\n", 1925 "<!-- 1->4 -->\n", 1926 "<g id=\"edge5\" class=\"edge\">\n", 1927 "<title>1->4</title>\n", 1928 "<path fill=\"none\" stroke=\"black\" d=\"M389.19,-140.57C398.54,-139.22 408.12,-137.84 417.56,-136.48\"/>\n", 1929 "<polygon fill=\"black\" stroke=\"black\" points=\"424.75,-135.44 418.27,-139.56 421.29,-135.94 417.82,-136.44 417.82,-136.44 417.82,-136.44 421.29,-135.94 417.37,-133.32 424.75,-135.44 424.75,-135.44\"/>\n", 1930 "</g>\n", 1931 "<!-- 2->4 -->\n", 1932 "<g id=\"edge6\" class=\"edge\">\n", 1933 "<title>2->4</title>\n", 1934 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-107.15C397.28,-108.6 407.62,-110.09 417.8,-111.56\"/>\n", 1935 "<polygon fill=\"black\" stroke=\"black\" points=\"424.81,-112.57 417.43,-114.69 421.35,-112.07 417.88,-111.57 417.88,-111.57 417.88,-111.57 421.35,-112.07 418.33,-108.45 424.81,-112.57 424.81,-112.57\"/>\n", 1936 "</g>\n", 1937 "<!-- 5 -->\n", 1938 "<g id=\"node7\" class=\"node\">\n", 1939 "<title>5</title>\n", 1940 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M571,-87C571,-87 439,-87 439,-87 433,-87 427,-81 427,-75 427,-75 427,-61 427,-61 427,-55 433,-49 439,-49 439,-49 571,-49 571,-49 577,-49 583,-55 583,-61 583,-61 583,-75 583,-75 583,-81 577,-87 571,-87\"/>\n", 1941 "<text text-anchor=\"start\" x=\"460.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n", 1942 "<text text-anchor=\"start\" x=\"435\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n", 1943 "</g>\n", 1944 "<!-- 2->5 -->\n", 1945 "<g id=\"edge7\" class=\"edge\">\n", 1946 "<title>2->5</title>\n", 1947 "<path fill=\"none\" stroke=\"black\" d=\"M387.23,-84.85C397.89,-83.31 408.89,-81.73 419.67,-80.17\"/>\n", 1948 "<polygon fill=\"black\" stroke=\"black\" points=\"426.72,-79.15 420.24,-83.27 423.25,-79.65 419.79,-80.15 419.79,-80.15 419.79,-80.15 423.25,-79.65 419.34,-77.04 426.72,-79.15 426.72,-79.15\"/>\n", 1949 "</g>\n", 1950 "<!-- 6 -->\n", 1951 "<g id=\"node8\" class=\"node\">\n", 1952 "<title>6</title>\n", 1953 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M765,-248C765,-248 633,-248 633,-248 627,-248 621,-242 621,-236 621,-236 621,-222 621,-222 621,-216 627,-210 633,-210 633,-210 765,-210 765,-210 771,-210 777,-216 777,-222 777,-222 777,-236 777,-236 777,-242 771,-248 765,-248\"/>\n", 1954 "<text text-anchor=\"start\" x=\"654.5\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n", 1955 "<text text-anchor=\"start\" x=\"629\" y=\"-217.8\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n", 1956 "</g>\n", 1957 "<!-- 3->6 -->\n", 1958 "<g id=\"edge8\" class=\"edge\">\n", 1959 "<title>3->6</title>\n", 1960 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-199.01C592.31,-202.03 604.58,-205.16 616.54,-208.21\"/>\n", 1961 "<polygon fill=\"black\" stroke=\"black\" points=\"623.53,-210 615.97,-211.32 620.14,-209.13 616.75,-208.26 616.75,-208.26 616.75,-208.26 620.14,-209.13 617.53,-205.21 623.53,-210 623.53,-210\"/>\n", 1962 "</g>\n", 1963 "<!-- 7 -->\n", 1964 "<g id=\"node9\" class=\"node\">\n", 1965 "<title>7</title>\n", 1966 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-192C739.5,-192 658.5,-192 658.5,-192 652.5,-192 646.5,-186 646.5,-180 646.5,-180 646.5,-166 646.5,-166 646.5,-160 652.5,-154 658.5,-154 658.5,-154 739.5,-154 739.5,-154 745.5,-154 751.5,-160 751.5,-166 751.5,-166 751.5,-180 751.5,-180 751.5,-186 745.5,-192 739.5,-192\"/>\n", 1967 "<text text-anchor=\"start\" x=\"654.5\" y=\"-176.8\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n", 1968 "<text text-anchor=\"start\" x=\"694\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 1969 "</g>\n", 1970 "<!-- 3->7 -->\n", 1971 "<g id=\"edge9\" class=\"edge\">\n", 1972 "<title>3->7</title>\n", 1973 "<path fill=\"none\" stroke=\"black\" d=\"M585.2,-177.11C603.28,-176.45 622.18,-175.76 639.22,-175.14\"/>\n", 1974 "<polygon fill=\"black\" stroke=\"black\" points=\"646.41,-174.88 639.52,-178.28 642.91,-175.01 639.41,-175.14 639.41,-175.14 639.41,-175.14 642.91,-175.01 639.3,-171.99 646.41,-174.88 646.41,-174.88\"/>\n", 1975 "</g>\n", 1976 "<!-- 4->7 -->\n", 1977 "<g id=\"edge10\" class=\"edge\">\n", 1978 "<title>4->7</title>\n", 1979 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-143.01C599.96,-147.98 620.65,-153.26 639.16,-157.98\"/>\n", 1980 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-159.83 638.84,-161.15 643.01,-158.97 639.62,-158.1 639.62,-158.1 639.62,-158.1 643.01,-158.97 640.4,-155.05 646.4,-159.83 646.4,-159.83\"/>\n", 1981 "</g>\n", 1982 "<!-- 8 -->\n", 1983 "<g id=\"node10\" class=\"node\">\n", 1984 "<title>8</title>\n", 1985 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-136C739.5,-136 658.5,-136 658.5,-136 652.5,-136 646.5,-130 646.5,-124 646.5,-124 646.5,-110 646.5,-110 646.5,-104 652.5,-98 658.5,-98 658.5,-98 739.5,-98 739.5,-98 745.5,-98 751.5,-104 751.5,-110 751.5,-110 751.5,-124 751.5,-124 751.5,-130 745.5,-136 739.5,-136\"/>\n", 1986 "<text text-anchor=\"start\" x=\"654.5\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n", 1987 "<text text-anchor=\"start\" x=\"694\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 1988 "</g>\n", 1989 "<!-- 4->8 -->\n", 1990 "<g id=\"edge11\" class=\"edge\">\n", 1991 "<title>4->8</title>\n", 1992 "<path fill=\"none\" stroke=\"black\" d=\"M585.2,-121.11C603.28,-120.45 622.18,-119.76 639.22,-119.14\"/>\n", 1993 "<polygon fill=\"black\" stroke=\"black\" points=\"646.41,-118.88 639.52,-122.28 642.91,-119.01 639.41,-119.14 639.41,-119.14 639.41,-119.14 642.91,-119.01 639.3,-115.99 646.41,-118.88 646.41,-118.88\"/>\n", 1994 "</g>\n", 1995 "<!-- 5->8 -->\n", 1996 "<g id=\"edge13\" class=\"edge\">\n", 1997 "<title>5->8</title>\n", 1998 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-87.01C599.96,-91.98 620.65,-97.26 639.16,-101.98\"/>\n", 1999 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-103.83 638.84,-105.15 643.01,-102.97 639.62,-102.1 639.62,-102.1 639.62,-102.1 643.01,-102.97 640.4,-99.05 646.4,-103.83 646.4,-103.83\"/>\n", 2000 "</g>\n", 2001 "<!-- u5 -->\n", 2002 "<g id=\"node11\" class=\"node\">\n", 2003 "<title>u5</title>\n", 2004 "<g id=\"a_node11\"><a xlink:title=\"hidden successors\">\n", 2005 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M704.33,-79.5C704.33,-79.5 693.67,-79.5 693.67,-79.5 689.83,-79.5 686,-75.67 686,-71.83 686,-71.83 686,-64.17 686,-64.17 686,-60.33 689.83,-56.5 693.67,-56.5 693.67,-56.5 704.33,-56.5 704.33,-56.5 708.17,-56.5 712,-60.33 712,-64.17 712,-64.17 712,-71.83 712,-71.83 712,-75.67 708.17,-79.5 704.33,-79.5\"/>\n", 2006 "<text text-anchor=\"middle\" x=\"699\" y=\"-64.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 2007 "</a>\n", 2008 "</g>\n", 2009 "</g>\n", 2010 "<!-- 5->u5 -->\n", 2011 "<g id=\"edge12\" class=\"edge\">\n", 2012 "<title>5->u5</title>\n", 2013 "<g id=\"a_edge12\"><a xlink:title=\"hidden successors\">\n", 2014 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M583.26,-68C618.13,-68 656.42,-68 678.77,-68\"/>\n", 2015 "<polygon fill=\"black\" stroke=\"black\" points=\"685.98,-68 678.98,-71.15 682.48,-68 678.98,-68 678.98,-68 678.98,-68 682.48,-68 678.98,-64.85 685.98,-68 685.98,-68\"/>\n", 2016 "</a>\n", 2017 "</g>\n", 2018 "</g>\n", 2019 "<!-- 9 -->\n", 2020 "<g id=\"node12\" class=\"node\">\n", 2021 "<title>9</title>\n", 2022 "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M739.5,-38C739.5,-38 658.5,-38 658.5,-38 652.5,-38 646.5,-32 646.5,-26 646.5,-26 646.5,-12 646.5,-12 646.5,-6 652.5,0 658.5,0 658.5,0 739.5,0 739.5,0 745.5,0 751.5,-6 751.5,-12 751.5,-12 751.5,-26 751.5,-26 751.5,-32 745.5,-38 739.5,-38\"/>\n", 2023 "<text text-anchor=\"start\" x=\"654.5\" y=\"-22.8\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n", 2024 "<text text-anchor=\"start\" x=\"694\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 2025 "</g>\n", 2026 "<!-- 5->9 -->\n", 2027 "<g id=\"edge14\" class=\"edge\">\n", 2028 "<title>5->9</title>\n", 2029 "<path fill=\"none\" stroke=\"black\" d=\"M580.51,-48.99C599.96,-44.02 620.65,-38.74 639.16,-34.02\"/>\n", 2030 "<polygon fill=\"black\" stroke=\"black\" points=\"646.4,-32.17 640.4,-36.95 643.01,-33.03 639.62,-33.9 639.62,-33.9 639.62,-33.9 643.01,-33.03 638.84,-30.85 646.4,-32.17 646.4,-32.17\"/>\n", 2031 "</g>\n", 2032 "<!-- 6->6 -->\n", 2033 "<g id=\"edge15\" class=\"edge\">\n", 2034 "<title>6->6</title>\n", 2035 "<path fill=\"none\" stroke=\"black\" d=\"M676.07,-248.04C672.9,-257.53 680.54,-266 699,-266 712.55,-266 720.28,-261.43 722.17,-255.25\"/>\n", 2036 "<polygon fill=\"black\" stroke=\"black\" points=\"721.93,-248.04 725.31,-254.93 722.04,-251.54 722.16,-255.03 722.16,-255.03 722.16,-255.03 722.04,-251.54 719.01,-255.14 721.93,-248.04 721.93,-248.04\"/>\n", 2037 "</g>\n", 2038 "<!-- u7 -->\n", 2039 "<g id=\"node13\" class=\"node\">\n", 2040 "<title>u7</title>\n", 2041 "<g id=\"a_node13\"><a xlink:title=\"hidden successors\">\n", 2042 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-184.5C831.33,-184.5 820.67,-184.5 820.67,-184.5 816.83,-184.5 813,-180.67 813,-176.83 813,-176.83 813,-169.17 813,-169.17 813,-165.33 816.83,-161.5 820.67,-161.5 820.67,-161.5 831.33,-161.5 831.33,-161.5 835.17,-161.5 839,-165.33 839,-169.17 839,-169.17 839,-176.83 839,-176.83 839,-180.67 835.17,-184.5 831.33,-184.5\"/>\n", 2043 "<text text-anchor=\"middle\" x=\"826\" y=\"-169.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 2044 "</a>\n", 2045 "</g>\n", 2046 "</g>\n", 2047 "<!-- 7->u7 -->\n", 2048 "<g id=\"edge16\" class=\"edge\">\n", 2049 "<title>7->u7</title>\n", 2050 "<g id=\"a_edge16\"><a xlink:title=\"hidden successors\">\n", 2051 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-173C770.63,-173 791.1,-173 805.57,-173\"/>\n", 2052 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-173 805.94,-176.15 809.44,-173 805.94,-173 805.94,-173 805.94,-173 809.44,-173 805.94,-169.85 812.94,-173 812.94,-173\"/>\n", 2053 "</a>\n", 2054 "</g>\n", 2055 "</g>\n", 2056 "<!-- u8 -->\n", 2057 "<g id=\"node14\" class=\"node\">\n", 2058 "<title>u8</title>\n", 2059 "<g id=\"a_node14\"><a xlink:title=\"hidden successors\">\n", 2060 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-128.5C831.33,-128.5 820.67,-128.5 820.67,-128.5 816.83,-128.5 813,-124.67 813,-120.83 813,-120.83 813,-113.17 813,-113.17 813,-109.33 816.83,-105.5 820.67,-105.5 820.67,-105.5 831.33,-105.5 831.33,-105.5 835.17,-105.5 839,-109.33 839,-113.17 839,-113.17 839,-120.83 839,-120.83 839,-124.67 835.17,-128.5 831.33,-128.5\"/>\n", 2061 "<text text-anchor=\"middle\" x=\"826\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 2062 "</a>\n", 2063 "</g>\n", 2064 "</g>\n", 2065 "<!-- 8->u8 -->\n", 2066 "<g id=\"edge17\" class=\"edge\">\n", 2067 "<title>8->u8</title>\n", 2068 "<g id=\"a_edge17\"><a xlink:title=\"hidden successors\">\n", 2069 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-117C770.63,-117 791.1,-117 805.57,-117\"/>\n", 2070 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-117 805.94,-120.15 809.44,-117 805.94,-117 805.94,-117 805.94,-117 809.44,-117 805.94,-113.85 812.94,-117 812.94,-117\"/>\n", 2071 "</a>\n", 2072 "</g>\n", 2073 "</g>\n", 2074 "<!-- u9 -->\n", 2075 "<g id=\"node15\" class=\"node\">\n", 2076 "<title>u9</title>\n", 2077 "<g id=\"a_node15\"><a xlink:title=\"hidden successors\">\n", 2078 "<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M831.33,-30.5C831.33,-30.5 820.67,-30.5 820.67,-30.5 816.83,-30.5 813,-26.67 813,-22.83 813,-22.83 813,-15.17 813,-15.17 813,-11.33 816.83,-7.5 820.67,-7.5 820.67,-7.5 831.33,-7.5 831.33,-7.5 835.17,-7.5 839,-11.33 839,-15.17 839,-15.17 839,-22.83 839,-22.83 839,-26.67 835.17,-30.5 831.33,-30.5\"/>\n", 2079 "<text text-anchor=\"middle\" x=\"826\" y=\"-15.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n", 2080 "</a>\n", 2081 "</g>\n", 2082 "</g>\n", 2083 "<!-- 9->u9 -->\n", 2084 "<g id=\"edge18\" class=\"edge\">\n", 2085 "<title>9->u9</title>\n", 2086 "<g id=\"a_edge18\"><a xlink:title=\"hidden successors\">\n", 2087 "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M751.56,-19C770.63,-19 791.1,-19 805.57,-19\"/>\n", 2088 "<polygon fill=\"black\" stroke=\"black\" points=\"812.94,-19 805.94,-22.15 809.44,-19 805.94,-19 805.94,-19 805.94,-19 809.44,-19 805.94,-15.85 812.94,-19 812.94,-19\"/>\n", 2089 "</a>\n", 2090 "</g>\n", 2091 "</g>\n", 2092 "</g>\n", 2093 "</svg>\n" 2094 ], 2095 "text/plain": [ 2096 "<spot.impl.kripke_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke_graph > *' at 0x7fe6bc6c4210> >" 2097 ] 2098 }, 2099 "execution_count": 21, 2100 "metadata": {}, 2101 "output_type": "execute_result" 2102 } 2103 ], 2104 "source": [ 2105 "k2 = spot.automaton(string, want_kripke=True)\n", 2106 "print(type(k2))\n", 2107 "k2" 2108 ] 2109 } 2110 ], 2111 "metadata": { 2112 "kernelspec": { 2113 "display_name": "Python 3", 2114 "language": "python", 2115 "name": "python3" 2116 }, 2117 "language_info": { 2118 "codemirror_mode": { 2119 "name": "ipython", 2120 "version": 3 2121 }, 2122 "file_extension": ".py", 2123 "mimetype": "text/x-python", 2124 "name": "python", 2125 "nbconvert_exporter": "python", 2126 "pygments_lexer": "ipython3", 2127 "version": "3.8.2" 2128 } 2129 }, 2130 "nbformat": 4, 2131 "nbformat_minor": 2 2132} 2133
