1{ 2 "cells": [ 3 { 4 "cell_type": "code", 5 "execution_count": 1, 6 "metadata": {}, 7 "outputs": [], 8 "source": [ 9 "from IPython.display import display\n", 10 "import spot\n", 11 "spot.setup()" 12 ] 13 }, 14 { 15 "cell_type": "markdown", 16 "metadata": {}, 17 "source": [ 18 "# Converting automata to strings" 19 ] 20 }, 21 { 22 "cell_type": "markdown", 23 "metadata": {}, 24 "source": [ 25 "Use `to_str()` to output a string representing the automaton in different formats." 26 ] 27 }, 28 { 29 "cell_type": "code", 30 "execution_count": 2, 31 "metadata": {}, 32 "outputs": [ 33 { 34 "name": "stdout", 35 "output_type": "stream", 36 "text": [ 37 "HOA: v1\n", 38 "States: 2\n", 39 "Start: 1\n", 40 "AP: 2 \"a\" \"b\"\n", 41 "acc-name: Buchi\n", 42 "Acceptance: 1 Inf(0)\n", 43 "properties: trans-labels explicit-labels state-acc deterministic\n", 44 "properties: stutter-invariant terminal\n", 45 "--BODY--\n", 46 "State: 0 {0}\n", 47 "[t] 0\n", 48 "State: 1\n", 49 "[1] 0\n", 50 "[0&!1] 1\n", 51 "--END--\n", 52 "never {\n", 53 "T0_init:\n", 54 " if\n", 55 " :: (b) -> goto accept_all\n", 56 " :: ((a) && (!(b))) -> goto T0_init\n", 57 " fi;\n", 58 "accept_all:\n", 59 " skip\n", 60 "}\n", 61 "\n", 62 "digraph \"\" {\n", 63 " rankdir=LR\n", 64 " label=<<br/>[Büchi]>\n", 65 " labelloc=\"t\"\n", 66 " node [shape=\"circle\"]\n", 67 " node [style=\"filled\", fillcolor=\"#ffffaa\"]\n", 68 " fontname=\"Lato\"\n", 69 " node [fontname=\"Lato\"]\n", 70 " edge [fontname=\"Lato\"]\n", 71 " size=\"10.13,5\" edge[arrowhead=vee, arrowsize=.7]\n", 72 " I [label=\"\", style=invis, width=0]\n", 73 " I -> 1\n", 74 " 0 [label=<0>, peripheries=2]\n", 75 " 0 -> 0 [label=<1>]\n", 76 " 1 [label=<1>]\n", 77 " 1 -> 0 [label=<b>]\n", 78 " 1 -> 1 [label=<a & !b>]\n", 79 "}\n", 80 "\n", 81 "2 1\n", 82 "0 1 -1\n", 83 "1 \"b\"\n", 84 "0 & \"a\" ! \"b\"\n", 85 "-1\n", 86 "1 0 0 -1\n", 87 "1 t\n", 88 "-1\n", 89 "\n" 90 ] 91 } 92 ], 93 "source": [ 94 "a = spot.translate('a U b')\n", 95 "for fmt in ('hoa', 'spin', 'dot', 'lbtt'):\n", 96 " print(a.to_str(fmt))" 97 ] 98 }, 99 { 100 "cell_type": "markdown", 101 "metadata": {}, 102 "source": [ 103 "# Saving automata to files" 104 ] 105 }, 106 { 107 "cell_type": "markdown", 108 "metadata": {}, 109 "source": [ 110 "Use `save()` to save the automaton into a file." 111 ] 112 }, 113 { 114 "cell_type": "code", 115 "execution_count": 3, 116 "metadata": {}, 117 "outputs": [ 118 { 119 "data": { 120 "image/svg+xml": [ 121 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 122 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 123 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 124 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 125 " -->\n", 126 "<!-- Pages: 1 -->\n", 127 "<svg width=\"171pt\" height=\"125pt\"\n", 128 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 129 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 130 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 131 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 132 "<!-- I -->\n", 133 "<!-- 1 -->\n", 134 "<g id=\"node2\" class=\"node\">\n", 135 "<title>1</title>\n", 136 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 137 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 138 "</g>\n", 139 "<!-- I->1 -->\n", 140 "<g id=\"edge1\" class=\"edge\">\n", 141 "<title>I->1</title>\n", 142 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 143 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 144 "</g>\n", 145 "<!-- 1->1 -->\n", 146 "<g id=\"edge4\" class=\"edge\">\n", 147 "<title>1->1</title>\n", 148 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 149 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 150 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 151 "</g>\n", 152 "<!-- 0 -->\n", 153 "<g id=\"node3\" class=\"node\">\n", 154 "<title>0</title>\n", 155 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 156 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 157 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 158 "</g>\n", 159 "<!-- 1->0 -->\n", 160 "<g id=\"edge3\" class=\"edge\">\n", 161 "<title>1->0</title>\n", 162 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 163 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 164 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 165 "</g>\n", 166 "<!-- 0->0 -->\n", 167 "<g id=\"edge2\" class=\"edge\">\n", 168 "<title>0->0</title>\n", 169 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 170 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 171 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 172 "</g>\n", 173 "</g>\n", 174 "</svg>\n" 175 ], 176 "text/plain": [ 177 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5770723f00> >" 178 ] 179 }, 180 "execution_count": 3, 181 "metadata": {}, 182 "output_type": "execute_result" 183 } 184 ], 185 "source": [ 186 "a.save('example.aut').save('example.aut', format='lbtt', append=True)" 187 ] 188 }, 189 { 190 "cell_type": "code", 191 "execution_count": 4, 192 "metadata": {}, 193 "outputs": [ 194 { 195 "name": "stdout", 196 "output_type": "stream", 197 "text": [ 198 "HOA: v1\r\n", 199 "States: 2\r\n", 200 "Start: 1\r\n", 201 "AP: 2 \"a\" \"b\"\r\n", 202 "acc-name: Buchi\r\n", 203 "Acceptance: 1 Inf(0)\r\n", 204 "properties: trans-labels explicit-labels state-acc deterministic\r\n", 205 "properties: stutter-invariant terminal\r\n", 206 "--BODY--\r\n", 207 "State: 0 {0}\r\n", 208 "[t] 0\r\n", 209 "State: 1\r\n", 210 "[1] 0\r\n", 211 "[0&!1] 1\r\n", 212 "--END--\r\n", 213 "2 1\r\n", 214 "0 1 -1\r\n", 215 "1 \"b\"\r\n", 216 "0 & \"a\" ! \"b\"\r\n", 217 "-1\r\n", 218 "1 0 0 -1\r\n", 219 "1 t\r\n", 220 "-1\r\n" 221 ] 222 } 223 ], 224 "source": [ 225 "!cat example.aut" 226 ] 227 }, 228 { 229 "cell_type": "markdown", 230 "metadata": {}, 231 "source": [ 232 "# Reading automata from files" 233 ] 234 }, 235 { 236 "cell_type": "markdown", 237 "metadata": {}, 238 "source": [ 239 "Use `spot.automata()` to read multiple automata from a file, and `spot.automaton()` to read only one." 240 ] 241 }, 242 { 243 "cell_type": "code", 244 "execution_count": 5, 245 "metadata": {}, 246 "outputs": [ 247 { 248 "data": { 249 "image/svg+xml": [ 250 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 251 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 252 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 253 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 254 " -->\n", 255 "<!-- Pages: 1 -->\n", 256 "<svg width=\"171pt\" height=\"125pt\"\n", 257 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 258 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 259 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 260 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 261 "<!-- I -->\n", 262 "<!-- 1 -->\n", 263 "<g id=\"node2\" class=\"node\">\n", 264 "<title>1</title>\n", 265 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 266 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 267 "</g>\n", 268 "<!-- I->1 -->\n", 269 "<g id=\"edge1\" class=\"edge\">\n", 270 "<title>I->1</title>\n", 271 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 272 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 273 "</g>\n", 274 "<!-- 1->1 -->\n", 275 "<g id=\"edge4\" class=\"edge\">\n", 276 "<title>1->1</title>\n", 277 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 278 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 279 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 280 "</g>\n", 281 "<!-- 0 -->\n", 282 "<g id=\"node3\" class=\"node\">\n", 283 "<title>0</title>\n", 284 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 285 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 286 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 287 "</g>\n", 288 "<!-- 1->0 -->\n", 289 "<g id=\"edge3\" class=\"edge\">\n", 290 "<title>1->0</title>\n", 291 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 292 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 293 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 294 "</g>\n", 295 "<!-- 0->0 -->\n", 296 "<g id=\"edge2\" class=\"edge\">\n", 297 "<title>0->0</title>\n", 298 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 299 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 300 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 301 "</g>\n", 302 "</g>\n", 303 "</svg>\n" 304 ], 305 "text/plain": [ 306 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706f5690> >" 307 ] 308 }, 309 "metadata": {}, 310 "output_type": "display_data" 311 }, 312 { 313 "data": { 314 "image/svg+xml": [ 315 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 316 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 317 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 318 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 319 " -->\n", 320 "<!-- Pages: 1 -->\n", 321 "<svg width=\"171pt\" height=\"125pt\"\n", 322 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 323 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 324 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 325 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 326 "<!-- I -->\n", 327 "<!-- 0 -->\n", 328 "<g id=\"node2\" class=\"node\">\n", 329 "<title>0</title>\n", 330 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 331 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 332 "</g>\n", 333 "<!-- I->0 -->\n", 334 "<g id=\"edge1\" class=\"edge\">\n", 335 "<title>I->0</title>\n", 336 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 337 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 338 "</g>\n", 339 "<!-- 0->0 -->\n", 340 "<g id=\"edge3\" class=\"edge\">\n", 341 "<title>0->0</title>\n", 342 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 343 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 344 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 345 "</g>\n", 346 "<!-- 1 -->\n", 347 "<g id=\"node3\" class=\"node\">\n", 348 "<title>1</title>\n", 349 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 350 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 351 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 352 "</g>\n", 353 "<!-- 0->1 -->\n", 354 "<g id=\"edge2\" class=\"edge\">\n", 355 "<title>0->1</title>\n", 356 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 357 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 358 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 359 "</g>\n", 360 "<!-- 1->1 -->\n", 361 "<g id=\"edge4\" class=\"edge\">\n", 362 "<title>1->1</title>\n", 363 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 364 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 365 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 366 "</g>\n", 367 "</g>\n", 368 "</svg>\n" 369 ], 370 "text/plain": [ 371 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706daa80> >" 372 ] 373 }, 374 "metadata": {}, 375 "output_type": "display_data" 376 } 377 ], 378 "source": [ 379 "for a in spot.automata('example.aut'):\n", 380 " display(a)" 381 ] 382 }, 383 { 384 "cell_type": "markdown", 385 "metadata": {}, 386 "source": [ 387 "The `--ABORT--` feature of the HOA format allows discarding the automaton being read and starting over." 388 ] 389 }, 390 { 391 "cell_type": "code", 392 "execution_count": 6, 393 "metadata": {}, 394 "outputs": [ 395 { 396 "name": "stdout", 397 "output_type": "stream", 398 "text": [ 399 "Overwriting example.aut\n" 400 ] 401 } 402 ], 403 "source": [ 404 "%%file example.aut\n", 405 "HOA: v1\n", 406 "States: 2\n", 407 "Start: 1\n", 408 "AP: 2 \"a\" \"b\"\n", 409 "acc-name: Buchi\n", 410 "Acceptance: 1 Inf(0)\n", 411 "--BODY--\n", 412 "State: 0 {0}\n", 413 "[t] 0\n", 414 "--ABORT-- /* the previous automaton should be ignored */\n", 415 "HOA: v1\n", 416 "States: 2\n", 417 "Start: 1\n", 418 "AP: 2 \"a\" \"b\"\n", 419 "Acceptance: 1 Inf(0)\n", 420 "--BODY--\n", 421 "State: 0 {0}\n", 422 "[t] 0\n", 423 "State: 1\n", 424 "[1] 0\n", 425 "[0&!1] 1\n", 426 "--END--" 427 ] 428 }, 429 { 430 "cell_type": "code", 431 "execution_count": 7, 432 "metadata": {}, 433 "outputs": [ 434 { 435 "data": { 436 "image/svg+xml": [ 437 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 438 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 439 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 440 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 441 " -->\n", 442 "<!-- Pages: 1 -->\n", 443 "<svg width=\"171pt\" height=\"125pt\"\n", 444 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 445 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 446 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 447 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 448 "<!-- I -->\n", 449 "<!-- 1 -->\n", 450 "<g id=\"node2\" class=\"node\">\n", 451 "<title>1</title>\n", 452 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 453 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 454 "</g>\n", 455 "<!-- I->1 -->\n", 456 "<g id=\"edge1\" class=\"edge\">\n", 457 "<title>I->1</title>\n", 458 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 459 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 460 "</g>\n", 461 "<!-- 1->1 -->\n", 462 "<g id=\"edge4\" class=\"edge\">\n", 463 "<title>1->1</title>\n", 464 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 465 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 466 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 467 "</g>\n", 468 "<!-- 0 -->\n", 469 "<g id=\"node3\" class=\"node\">\n", 470 "<title>0</title>\n", 471 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 472 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 473 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 474 "</g>\n", 475 "<!-- 1->0 -->\n", 476 "<g id=\"edge3\" class=\"edge\">\n", 477 "<title>1->0</title>\n", 478 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 479 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 480 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 481 "</g>\n", 482 "<!-- 0->0 -->\n", 483 "<g id=\"edge2\" class=\"edge\">\n", 484 "<title>0->0</title>\n", 485 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 486 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 487 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 488 "</g>\n", 489 "</g>\n", 490 "</svg>\n" 491 ], 492 "text/plain": [ 493 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706f5840> >" 494 ] 495 }, 496 "metadata": {}, 497 "output_type": "display_data" 498 } 499 ], 500 "source": [ 501 "for a in spot.automata('example.aut'):\n", 502 " display(a)" 503 ] 504 }, 505 { 506 "cell_type": "markdown", 507 "metadata": {}, 508 "source": [ 509 "# Reading automata from strings" 510 ] 511 }, 512 { 513 "cell_type": "markdown", 514 "metadata": {}, 515 "source": [ 516 "Instead of passing a filename, you can also pass the contents of a file. `spot.automata()` and `spot.automaton()` look for the absence of newline to decide if this is a filename or a string containing some actual automaton text." 517 ] 518 }, 519 { 520 "cell_type": "code", 521 "execution_count": 8, 522 "metadata": {}, 523 "outputs": [ 524 { 525 "data": { 526 "image/svg+xml": [ 527 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 528 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 529 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 530 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 531 " -->\n", 532 "<!-- Title: Hello world Pages: 1 -->\n", 533 "<svg width=\"171pt\" height=\"125pt\"\n", 534 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 535 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 536 "<title>Hello world</title>\n", 537 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 538 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 539 "<!-- I -->\n", 540 "<!-- 1 -->\n", 541 "<g id=\"node2\" class=\"node\">\n", 542 "<title>1</title>\n", 543 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 544 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 545 "</g>\n", 546 "<!-- I->1 -->\n", 547 "<g id=\"edge1\" class=\"edge\">\n", 548 "<title>I->1</title>\n", 549 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 550 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 551 "</g>\n", 552 "<!-- 1->1 -->\n", 553 "<g id=\"edge4\" class=\"edge\">\n", 554 "<title>1->1</title>\n", 555 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 556 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 557 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 558 "</g>\n", 559 "<!-- 0 -->\n", 560 "<g id=\"node3\" class=\"node\">\n", 561 "<title>0</title>\n", 562 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 563 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 564 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 565 "</g>\n", 566 "<!-- 1->0 -->\n", 567 "<g id=\"edge3\" class=\"edge\">\n", 568 "<title>1->0</title>\n", 569 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 570 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 571 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 572 "</g>\n", 573 "<!-- 0->0 -->\n", 574 "<g id=\"edge2\" class=\"edge\">\n", 575 "<title>0->0</title>\n", 576 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 577 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 578 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 579 "</g>\n", 580 "</g>\n", 581 "</svg>\n" 582 ], 583 "text/plain": [ 584 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57707760f0> >" 585 ] 586 }, 587 "metadata": {}, 588 "output_type": "display_data" 589 }, 590 { 591 "data": { 592 "image/svg+xml": [ 593 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 594 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 595 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 596 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 597 " -->\n", 598 "<!-- Title: Hello world 2 Pages: 1 -->\n", 599 "<svg width=\"118pt\" height=\"174pt\"\n", 600 " viewBox=\"0.00 0.00 118.00 174.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 601 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 170)\">\n", 602 "<title>Hello world 2</title>\n", 603 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-170 114,-170 114,4 -4,4\"/>\n", 604 "<text text-anchor=\"start\" x=\"8\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n", 605 "<text text-anchor=\"start\" x=\"30\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 606 "<text text-anchor=\"start\" x=\"46\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)&Inf(</text>\n", 607 "<text text-anchor=\"start\" x=\"82\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n", 608 "<text text-anchor=\"start\" x=\"98\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n", 609 "<text text-anchor=\"start\" x=\"11\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[gen. Büchi 2]</text>\n", 610 "<!-- I -->\n", 611 "<!-- 0 -->\n", 612 "<g id=\"node2\" class=\"node\">\n", 613 "<title>0</title>\n", 614 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"73.75\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n", 615 "<text text-anchor=\"middle\" x=\"73.75\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 616 "</g>\n", 617 "<!-- I->0 -->\n", 618 "<g id=\"edge1\" class=\"edge\">\n", 619 "<title>I->0</title>\n", 620 "<path fill=\"none\" stroke=\"#000000\" d=\"M18.8733,-18C21.928,-18 35.6948,-18 48.6741,-18\"/>\n", 621 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"55.7307,-18 48.7308,-21.1501 52.2307,-18 48.7307,-18.0001 48.7307,-18.0001 48.7307,-18.0001 52.2307,-18 48.7307,-14.8501 55.7307,-18 55.7307,-18\"/>\n", 622 "</g>\n", 623 "<!-- 0->0 -->\n", 624 "<g id=\"edge2\" class=\"edge\">\n", 625 "<title>0->0</title>\n", 626 "<path fill=\"none\" stroke=\"#000000\" d=\"M70.5143,-35.7817C69.9644,-45.3149 71.043,-54 73.75,-54 75.738,-54 76.8477,-49.3161 77.0792,-43.0521\"/>\n", 627 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"76.9857,-35.7817 80.2256,-42.7406 77.0308,-39.2814 77.0758,-42.7812 77.0758,-42.7812 77.0758,-42.7812 77.0308,-39.2814 73.9261,-42.8217 76.9857,-35.7817 76.9857,-35.7817\"/>\n", 628 "<text text-anchor=\"start\" x=\"69.25\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 629 "<text text-anchor=\"start\" x=\"57.75\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 630 "<text text-anchor=\"start\" x=\"73.75\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n", 631 "</g>\n", 632 "<!-- 0->0 -->\n", 633 "<g id=\"edge3\" class=\"edge\">\n", 634 "<title>0->0</title>\n", 635 "<path fill=\"none\" stroke=\"#000000\" d=\"M68.6875,-35.5938C65.3125,-56.125 67,-82 73.75,-82 79.7354,-82 81.7402,-61.6553 79.7646,-42.7315\"/>\n", 636 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"78.8125,-35.5938 82.8604,-42.1158 79.2753,-39.063 79.7381,-42.5323 79.7381,-42.5323 79.7381,-42.5323 79.2753,-39.063 76.6157,-42.9488 78.8125,-35.5938 78.8125,-35.5938\"/>\n", 637 "<text text-anchor=\"start\" x=\"55.25\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 638 "<text text-anchor=\"start\" x=\"65.75\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 639 "</g>\n", 640 "</g>\n", 641 "</svg>\n" 642 ], 643 "text/plain": [ 644 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5770685930> >" 645 ] 646 }, 647 "metadata": {}, 648 "output_type": "display_data" 649 } 650 ], 651 "source": [ 652 "for a in spot.automata(\"\"\"\n", 653 "HOA: v1\n", 654 "States: 2\n", 655 "Start: 1\n", 656 "name: \"Hello world\"\n", 657 "AP: 2 \"a\" \"b\"\n", 658 "Acceptance: 1 Inf(0)\n", 659 "--BODY--\n", 660 "State: 0 {0}\n", 661 "[t] 0\n", 662 "State: 1\n", 663 "[1] 0\n", 664 "[0&!1] 1\n", 665 "--END--\n", 666 "HOA: v1\n", 667 "States: 1\n", 668 "Start: 0\n", 669 "name: \"Hello world 2\"\n", 670 "AP: 2 \"a\" \"b\"\n", 671 "Acceptance: 2 Inf(0)&Inf(1)\n", 672 "--BODY--\n", 673 "State: 0 {0}\n", 674 "[t] 0 {1}\n", 675 "[0&!1] 0\n", 676 "--END--\n", 677 "\"\"\"):\n", 678 " display(a)" 679 ] 680 }, 681 { 682 "cell_type": "markdown", 683 "metadata": {}, 684 "source": [ 685 "# Reading automata output from processes\n", 686 "\n", 687 "If an argument of `spot.automata` ends with `|`, then it is interpreted as a shell command that outputs one automaton or more." 688 ] 689 }, 690 { 691 "cell_type": "code", 692 "execution_count": 9, 693 "metadata": {}, 694 "outputs": [ 695 { 696 "data": { 697 "image/svg+xml": [ 698 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 699 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 700 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 701 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 702 " -->\n", 703 "<!-- Pages: 1 -->\n", 704 "<svg width=\"171pt\" height=\"125pt\"\n", 705 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 706 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 707 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 708 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 709 "<!-- I -->\n", 710 "<!-- 0 -->\n", 711 "<g id=\"node2\" class=\"node\">\n", 712 "<title>0</title>\n", 713 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 714 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 715 "</g>\n", 716 "<!-- I->0 -->\n", 717 "<g id=\"edge1\" class=\"edge\">\n", 718 "<title>I->0</title>\n", 719 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 720 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 721 "</g>\n", 722 "<!-- 0->0 -->\n", 723 "<g id=\"edge3\" class=\"edge\">\n", 724 "<title>0->0</title>\n", 725 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 726 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 727 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 728 "</g>\n", 729 "<!-- 1 -->\n", 730 "<g id=\"node3\" class=\"node\">\n", 731 "<title>1</title>\n", 732 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 733 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 734 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 735 "</g>\n", 736 "<!-- 0->1 -->\n", 737 "<g id=\"edge2\" class=\"edge\">\n", 738 "<title>0->1</title>\n", 739 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 740 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 741 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 742 "</g>\n", 743 "<!-- 1->1 -->\n", 744 "<g id=\"edge4\" class=\"edge\">\n", 745 "<title>1->1</title>\n", 746 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 747 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 748 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 749 "</g>\n", 750 "</g>\n", 751 "</svg>\n" 752 ], 753 "text/plain": [ 754 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706f5720> >" 755 ] 756 }, 757 "metadata": {}, 758 "output_type": "display_data" 759 }, 760 { 761 "data": { 762 "image/svg+xml": [ 763 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 764 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 765 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 766 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 767 " -->\n", 768 "<!-- Pages: 1 -->\n", 769 "<svg width=\"171pt\" height=\"125pt\"\n", 770 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 771 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 772 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 773 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 774 "<!-- I -->\n", 775 "<!-- 0 -->\n", 776 "<g id=\"node2\" class=\"node\">\n", 777 "<title>0</title>\n", 778 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 779 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 780 "</g>\n", 781 "<!-- I->0 -->\n", 782 "<g id=\"edge1\" class=\"edge\">\n", 783 "<title>I->0</title>\n", 784 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 785 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 786 "</g>\n", 787 "<!-- 1 -->\n", 788 "<g id=\"node3\" class=\"node\">\n", 789 "<title>1</title>\n", 790 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 791 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 792 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 793 "</g>\n", 794 "<!-- 0->1 -->\n", 795 "<g id=\"edge2\" class=\"edge\">\n", 796 "<title>0->1</title>\n", 797 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 798 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 799 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 800 "</g>\n", 801 "<!-- 1->1 -->\n", 802 "<g id=\"edge3\" class=\"edge\">\n", 803 "<title>1->1</title>\n", 804 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 805 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 806 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 807 "</g>\n", 808 "</g>\n", 809 "</svg>\n" 810 ], 811 "text/plain": [ 812 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706f5900> >" 813 ] 814 }, 815 "metadata": {}, 816 "output_type": "display_data" 817 }, 818 { 819 "data": { 820 "image/svg+xml": [ 821 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 822 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 823 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 824 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 825 " -->\n", 826 "<!-- Title: GFa Pages: 1 -->\n", 827 "<svg width=\"82pt\" height=\"161pt\"\n", 828 " viewBox=\"0.00 0.00 82.00 161.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 829 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 157)\">\n", 830 "<title>GFa</title>\n", 831 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-157 78,-157 78,4 -4,4\"/>\n", 832 "<text text-anchor=\"start\" x=\"16\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n", 833 "<text text-anchor=\"start\" x=\"38\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 834 "<text text-anchor=\"start\" x=\"54\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n", 835 "<text text-anchor=\"start\" x=\"14\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 836 "<!-- I -->\n", 837 "<!-- 0 -->\n", 838 "<g id=\"node2\" class=\"node\">\n", 839 "<title>0</title>\n", 840 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n", 841 "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 842 "</g>\n", 843 "<!-- I->0 -->\n", 844 "<g id=\"edge1\" class=\"edge\">\n", 845 "<title>I->0</title>\n", 846 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-18C4.178,-18 17.9448,-18 30.9241,-18\"/>\n", 847 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-18 30.9808,-21.1501 34.4807,-18 30.9807,-18.0001 30.9807,-18.0001 30.9807,-18.0001 34.4807,-18 30.9807,-14.8501 37.9807,-18 37.9807,-18\"/>\n", 848 "</g>\n", 849 "<!-- 0->0 -->\n", 850 "<g id=\"edge2\" class=\"edge\">\n", 851 "<title>0->0</title>\n", 852 "<path fill=\"none\" stroke=\"#000000\" d=\"M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521\"/>\n", 853 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"59.2357,-35.7817 62.4756,-42.7406 59.2808,-39.2814 59.3258,-42.7812 59.3258,-42.7812 59.3258,-42.7812 59.2808,-39.2814 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817\"/>\n", 854 "<text text-anchor=\"start\" x=\"50.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n", 855 "</g>\n", 856 "<!-- 0->0 -->\n", 857 "<g id=\"edge3\" class=\"edge\">\n", 858 "<title>0->0</title>\n", 859 "<path fill=\"none\" stroke=\"#000000\" d=\"M50.6841,-35.4203C47.6538,-52.791 49.4258,-72 56,-72 61.7011,-72 63.7908,-57.5545 62.2691,-42.3894\"/>\n", 860 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.3159,-35.4203 65.3856,-41.9288 61.7902,-38.888 62.2646,-42.3557 62.2646,-42.3557 62.2646,-42.3557 61.7902,-38.888 59.1437,-42.7826 61.3159,-35.4203 61.3159,-35.4203\"/>\n", 861 "<text text-anchor=\"start\" x=\"52.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n", 862 "<text text-anchor=\"start\" x=\"48\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 863 "</g>\n", 864 "</g>\n", 865 "</svg>\n" 866 ], 867 "text/plain": [ 868 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5770798e70> >" 869 ] 870 }, 871 "metadata": {}, 872 "output_type": "display_data" 873 }, 874 { 875 "data": { 876 "image/svg+xml": [ 877 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 878 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 879 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 880 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 881 " -->\n", 882 "<!-- Title: a & GFb Pages: 1 -->\n", 883 "<svg width=\"161pt\" height=\"161pt\"\n", 884 " viewBox=\"0.00 0.00 161.00 161.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 885 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 157)\">\n", 886 "<title>a & GFb</title>\n", 887 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-157 157,-157 157,4 -4,4\"/>\n", 888 "<text text-anchor=\"start\" x=\"55.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n", 889 "<text text-anchor=\"start\" x=\"77.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 890 "<text text-anchor=\"start\" x=\"93.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n", 891 "<text text-anchor=\"start\" x=\"53.5\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 892 "<!-- I -->\n", 893 "<!-- 0 -->\n", 894 "<g id=\"node2\" class=\"node\">\n", 895 "<title>0</title>\n", 896 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n", 897 "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 898 "</g>\n", 899 "<!-- I->0 -->\n", 900 "<g id=\"edge1\" class=\"edge\">\n", 901 "<title>I->0</title>\n", 902 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-18C4.178,-18 17.9448,-18 30.9241,-18\"/>\n", 903 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-18 30.9808,-21.1501 34.4807,-18 30.9807,-18.0001 30.9807,-18.0001 30.9807,-18.0001 34.4807,-18 30.9807,-14.8501 37.9807,-18 37.9807,-18\"/>\n", 904 "</g>\n", 905 "<!-- 1 -->\n", 906 "<g id=\"node3\" class=\"node\">\n", 907 "<title>1</title>\n", 908 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n", 909 "<text text-anchor=\"middle\" x=\"135\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 910 "</g>\n", 911 "<!-- 0->1 -->\n", 912 "<g id=\"edge2\" class=\"edge\">\n", 913 "<title>0->1</title>\n", 914 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.3228,-18C84.7921,-18 98.0794,-18 109.5495,-18\"/>\n", 915 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"116.7766,-18 109.7767,-21.1501 113.2766,-18 109.7766,-18.0001 109.7766,-18.0001 109.7766,-18.0001 113.2766,-18 109.7766,-14.8501 116.7766,-18 116.7766,-18\"/>\n", 916 "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n", 917 "</g>\n", 918 "<!-- 1->1 -->\n", 919 "<g id=\"edge3\" class=\"edge\">\n", 920 "<title>1->1</title>\n", 921 "<path fill=\"none\" stroke=\"#000000\" d=\"M131.5845,-35.7817C131.0041,-45.3149 132.1426,-54 135,-54 137.0984,-54 138.2698,-49.3161 138.5142,-43.0521\"/>\n", 922 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"138.4155,-35.7817 141.6603,-42.7383 138.4631,-39.2814 138.5106,-42.7811 138.5106,-42.7811 138.5106,-42.7811 138.4631,-39.2814 135.3609,-42.8239 138.4155,-35.7817 138.4155,-35.7817\"/>\n", 923 "<text text-anchor=\"start\" x=\"128.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n", 924 "</g>\n", 925 "<!-- 1->1 -->\n", 926 "<g id=\"edge4\" class=\"edge\">\n", 927 "<title>1->1</title>\n", 928 "<path fill=\"none\" stroke=\"#000000\" d=\"M129.4406,-35.1418C126.1703,-52.585 128.0234,-72 135,-72 141.05,-72 143.2471,-57.3996 141.5913,-42.146\"/>\n", 929 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"140.5594,-35.1418 144.6961,-41.6079 141.0696,-38.6044 141.5798,-42.067 141.5798,-42.067 141.5798,-42.067 141.0696,-38.6044 138.4634,-42.5262 140.5594,-35.1418 140.5594,-35.1418\"/>\n", 930 "<text text-anchor=\"start\" x=\"130.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 931 "<text text-anchor=\"start\" x=\"127\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", 932 "</g>\n", 933 "</g>\n", 934 "</svg>\n" 935 ], 936 "text/plain": [ 937 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f57706f5720> >" 938 ] 939 }, 940 "metadata": {}, 941 "output_type": "display_data" 942 } 943 ], 944 "source": [ 945 "for a in spot.automata('ltl2tgba -s \"a U b\"; ltl2tgba --lbtt \"b\"|', 'ltl2tgba -H \"GFa\" \"a & GFb\"|'):\n", 946 " display(a)" 947 ] 948 }, 949 { 950 "cell_type": "markdown", 951 "metadata": {}, 952 "source": [ 953 "A single automaton can be read using `spot.automaton()`, with the same convention." 954 ] 955 }, 956 { 957 "cell_type": "code", 958 "execution_count": 10, 959 "metadata": {}, 960 "outputs": [ 961 { 962 "data": { 963 "image/svg+xml": [ 964 "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", 965 "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", 966 " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", 967 "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", 968 " -->\n", 969 "<!-- Pages: 1 -->\n", 970 "<svg width=\"171pt\" height=\"125pt\"\n", 971 " viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", 972 "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n", 973 "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n", 974 "<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n", 975 "<!-- I -->\n", 976 "<!-- 0 -->\n", 977 "<g id=\"node2\" class=\"node\">\n", 978 "<title>0</title>\n", 979 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 980 "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", 981 "</g>\n", 982 "<!-- I->0 -->\n", 983 "<g id=\"edge1\" class=\"edge\">\n", 984 "<title>I->0</title>\n", 985 "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n", 986 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n", 987 "</g>\n", 988 "<!-- 0->0 -->\n", 989 "<g id=\"edge3\" class=\"edge\">\n", 990 "<title>0->0</title>\n", 991 "<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n", 992 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n", 993 "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a & !b</text>\n", 994 "</g>\n", 995 "<!-- 1 -->\n", 996 "<g id=\"node3\" class=\"node\">\n", 997 "<title>1</title>\n", 998 "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n", 999 "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n", 1000 "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 1001 "</g>\n", 1002 "<!-- 0->1 -->\n", 1003 "<g id=\"edge2\" class=\"edge\">\n", 1004 "<title>0->1</title>\n", 1005 "<path fill=\"none\" stroke=\"#000000\" d=\"M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22\"/>\n", 1006 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22\"/>\n", 1007 "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n", 1008 "</g>\n", 1009 "<!-- 1->1 -->\n", 1010 "<g id=\"edge4\" class=\"edge\">\n", 1011 "<title>1->1</title>\n", 1012 "<path fill=\"none\" stroke=\"#000000\" d=\"M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451\"/>\n", 1013 "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808\"/>\n", 1014 "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", 1015 "</g>\n", 1016 "</g>\n", 1017 "</svg>\n" 1018 ], 1019 "text/plain": [ 1020 "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f577072d060> >" 1021 ] 1022 }, 1023 "execution_count": 10, 1024 "metadata": {}, 1025 "output_type": "execute_result" 1026 } 1027 ], 1028 "source": [ 1029 "spot.automaton('ltl2tgba -s6 \"a U b\"|')" 1030 ] 1031 }, 1032 { 1033 "cell_type": "code", 1034 "execution_count": 11, 1035 "metadata": {}, 1036 "outputs": [], 1037 "source": [ 1038 "!rm example.aut" 1039 ] 1040 } 1041 ], 1042 "metadata": { 1043 "kernelspec": { 1044 "display_name": "Python 3", 1045 "language": "python", 1046 "name": "python3" 1047 }, 1048 "language_info": { 1049 "codemirror_mode": { 1050 "name": "ipython", 1051 "version": 3 1052 }, 1053 "file_extension": ".py", 1054 "mimetype": "text/x-python", 1055 "name": "python", 1056 "nbconvert_exporter": "python", 1057 "pygments_lexer": "ipython3", 1058 "version": "3.6.5" 1059 } 1060 }, 1061 "nbformat": 4, 1062 "nbformat_minor": 2 1063} 1064