diff --git a/notebooks/models/NFA_to_DFA.ipynb b/notebooks/models/NFA_to_DFA.ipynb index 63bcc66fe48a5883b20a2e185b1139907201c3a1..f6bbcac2873d56ecf3129151a2902cd76f2cbe87 100644 --- a/notebooks/models/NFA_to_DFA.ipynb +++ b/notebooks/models/NFA_to_DFA.ipynb @@ -1,5 +1,28 @@ { "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\newcommand{\\Inter}{\\bigcap\\nolimits}\\newcommand{\\bfalse}{\\mathord\\bot}\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\newcommand{\\dprod}{\\mathbin\\otimes}\\newcommand{\\usucc}{\\mathop{\\mathrm{succ}}\\nolimits}\\newcommand{\\trel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\strel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\newcommand{\\Bool}{\\mathord{\\mathrm{BOOL}}}\\newcommand{\\rel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\pprod}{\\mathbin\\mid}\\newcommand{\\id}{\\mathop{\\mathrm{id}}\\nolimits}\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\ran}{\\mathop{\\mathrm{ran}}\\nolimits}\\newcommand{\\nat}{\\mathord{\\mathbb N}}\\newcommand{\\pown}{\\mathop{\\mathbb P_1}\\nolimits}\\newcommand{\\finite}{\\mathop{\\mathrm{finite}}\\nolimits}\\newcommand{\\inter}{\\mathop{\\mathrm{inter}}\\nolimits}\\newcommand{\\prjone}{\\mathop{\\mathrm{prj}_1}\\nolimits}\\newcommand{\\defi}{\\mathrel{≙}}\\newcommand{\\ranres}{\\mathbin▷}\\newcommand{\\prjtwo}{\\mathop{\\mathrm{prj}_2}\\nolimits}\\newcommand{\\upred}{\\mathop{\\mathrm{pred}}\\nolimits}\\newcommand{\\fcomp}{\\mathbin;}\\newcommand{\\tbij}{\\mathbin⤖}\\newcommand{\\pfun}{\\mathbin↦}\\newcommand{\\tfun}{\\mathbin→}\\newcommand{\\card}{\\mathop{\\mathrm{card}}\\nolimits}\\newcommand{\\pinj}{\\mathbin⤔}\\newcommand{\\dom}{\\mathop{\\mathrm{dom}}\\nolimits}\\newcommand{\\bool}{\\mathop{\\mathrm{bool}}\\nolimits}\\newcommand{\\tinj}{\\mathbin↣}\\newcommand{\\domsub}{\\mathbin⩤}\\newcommand{\\Union}{\\bigcup\\nolimits}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\newcommand{\\ransub}{\\mathbin⩥}\\newcommand{\\psur}{\\mathbin⤅}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\bcmsuch}{\\mathrel{:\\mkern1mu\\mid}}\\newcommand{\\natn}{\\mathord{\\mathbb N_1}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\bcomp}{\\circ}\\newcommand{\\bcmin}{\\mathrel{:\\mkern1mu\\in}}\\newcommand{\\ovl}{\\mathbin{<\\mkern-11mu+}}\\newcommand{\\intg}{\\mathord{\\mathbb Z}}\\newcommand{\\domres}{\\mathbin◁}\\newcommand{\\tsur}{\\mathbin↠}\\newcommand{\\btrue}{\\mathord\\top}\\newcommand{\\union}{\\mathop{\\mathrm{union}}\\nolimits}\\newcommand{\\bcmeq}{\\mathrel{:\\mkern1mu=}}\\newcommand{\\leqv}{\\mathbin\\Leftrightarrow}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\newcommand{\\srel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\text{All bsymb.sty definitions have been loaded.}$" + ], + "text/plain": [ + "Your current environment uses plain text output; the bsymb.sty LaTeX commands will not be loaded." + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":bsymb" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -41,7 +64,7 @@ "Wie laden nun ein B Modell welches diese Definitionen beinhaltet.\n", "Wörter werden dabei in der B Sprache mit eckigen Klammern und Kommas geschrieben; aus 101 wird [1,0,1].\n", "Gewisse griechische Zeichen sind in der B Sprache als Schlüsselwörter reserviert, zB $\\lambda$.\n", - "Auch kann man leider $\\hat$ in Bezeichnern verwenden.\n", + "Auch kann man leider kein $\\hat{~}$ in Bezeichnern verwenden.\n", "Deshalb wird aus\n", "* $\\Sigma^*$ wird ```seq(Σ)```\n", "* $\\widehat{\\delta}$ wird ```δs```" @@ -49,7 +72,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -58,7 +81,7 @@ "Loaded machine: NFA_nach_DFA" ] }, - "execution_count": 3, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -94,7 +117,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 3, "metadata": {}, "outputs": [ { @@ -103,7 +126,7 @@ "Machine constants set up using operation 0: $setup_constants()" ] }, - "execution_count": 4, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -114,7 +137,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -123,7 +146,7 @@ "Machine initialised using operation 1: $initialise_machine()" ] }, - "execution_count": 5, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -141,7 +164,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -153,7 +176,7 @@ "{z0,z1}" ] }, - "execution_count": 6, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -173,7 +196,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 6, "metadata": {}, "outputs": [ { @@ -202,7 +225,7 @@ "z3\t1\t{z3}\n" ] }, - "execution_count": 7, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } @@ -220,7 +243,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -229,73 +252,84 @@ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", - "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"144pt\" height=\"368pt\"\n", - " viewBox=\"0.00 0.00 144.00 368.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", - "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 364)\">\n", + "<svg width=\"146pt\" height=\"472pt\"\n", + " viewBox=\"0.00 0.00 146.00 472.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 468)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-364 141,-364 141,5 -4,5\"/>\n", - "<g id=\"graph2\" class=\"cluster\"><title>cluster_Z</title>\n", - "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-352 128,-352 128,-8 8,-8\"/>\n", - "<text text-anchor=\"middle\" x=\"68\" y=\"-337.2\" font-family=\"Times,serif\" font-size=\"12.00\">Z</text>\n", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-468 142,-468 142,4 -4,4\"/>\n", + "<g id=\"clust1\" class=\"cluster\">\n", + "<title>cluster_Z</title>\n", + "<polygon fill=\"#d3d3d3\" stroke=\"#d3d3d3\" points=\"8,-8 8,-456 130,-456 130,-8 8,-8\"/>\n", + "<text text-anchor=\"middle\" x=\"69\" y=\"-442.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">Z</text>\n", "</g>\n", "<!-- z0 -->\n", - "<g id=\"node1\" class=\"node\"><title>z0</title>\n", - "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-322 16,-322 16,-286 70,-286 70,-322\"/>\n", - "<text text-anchor=\"middle\" x=\"43\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">z0</text>\n", + "<g id=\"node1\" class=\"node\">\n", + "<title>z0</title>\n", + "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-427 16,-427 16,-391 70,-391 70,-427\"/>\n", + "<text text-anchor=\"middle\" x=\"43\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z0</text>\n", "</g>\n", "<!-- z0->z0 -->\n", - "<g id=\"edge4\" class=\"edge\"><title>z0->z0</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.2408,-308.121C80.0239,-308.21 88,-306.836 88,-304 88,-302.272 85.0382,-301.087 80.5105,-300.445\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.4181,-296.934 70.2408,-299.879 80.0332,-303.924 80.4181,-296.934\"/>\n", - "<text text-anchor=\"middle\" x=\"91.5\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge2\" class=\"edge\">\n", + "<title>z0->z0</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M70.2408,-412.3717C80.0239,-412.4442 88,-411.3203 88,-409 88,-407.5861 85.0382,-406.6164 80.5105,-406.091\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"80.3882,-402.582 70.2408,-405.6283 80.0731,-409.5749 80.3882,-402.582\"/>\n", + "<text text-anchor=\"middle\" x=\"92\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- z0->z0 -->\n", - "<g id=\"edge12\" class=\"edge\"><title>z0->z0</title>\n", - "<path fill=\"none\" stroke=\"sienna\" d=\"M70.1975,-319.251C88.3402,-323.544 106,-318.46 106,-304 106,-292.251 94.3418,-286.692 80.2386,-287.323\"/>\n", - "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"79.6061,-283.878 70.1975,-288.749 80.5903,-290.808 79.6061,-283.878\"/>\n", - "<text text-anchor=\"middle\" x=\"109.5\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge6\" class=\"edge\">\n", + "<title>z0->z0</title>\n", + "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.1975,-415.1551C88.3402,-416.8876 106,-414.8359 106,-409 106,-404.2583 94.3418,-402.0148 80.2386,-402.2695\"/>\n", + "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"79.9809,-398.7784 70.1975,-402.8449 80.3814,-405.7669 79.9809,-398.7784\"/>\n", + "<text text-anchor=\"middle\" x=\"110\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- z1 -->\n", - "<g id=\"node3\" class=\"node\"><title>z1</title>\n", - "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-232 16,-232 16,-196 70,-196 70,-232\"/>\n", - "<text text-anchor=\"middle\" x=\"43\" y=\"-209.8\" font-family=\"Times,serif\" font-size=\"14.00\">z1</text>\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>z1</title>\n", + "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-302 16,-302 16,-266 70,-266 70,-302\"/>\n", + "<text text-anchor=\"middle\" x=\"43\" y=\"-280.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z1</text>\n", "</g>\n", "<!-- z0->z1 -->\n", - "<g id=\"edge2\" class=\"edge\"><title>z0->z1</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-285.614C43,-273.24 43,-256.369 43,-242.22\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5001,-242.05 43,-232.05 39.5001,-242.05 46.5001,-242.05\"/>\n", - "<text text-anchor=\"middle\" x=\"46.5\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge1\" class=\"edge\">\n", + "<title>z0->z1</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M43,-390.8239C43,-370.2723 43,-336.5472 43,-312.4893\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"46.5001,-312.198 43,-302.198 39.5001,-312.198 46.5001,-312.198\"/>\n", + "<text text-anchor=\"middle\" x=\"47\" y=\"-342.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- z2 -->\n", - "<g id=\"node7\" class=\"node\"><title>z2</title>\n", - "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-142 16,-142 16,-106 70,-106 70,-142\"/>\n", - "<text text-anchor=\"middle\" x=\"43\" y=\"-119.8\" font-family=\"Times,serif\" font-size=\"14.00\">z2</text>\n", + "<g id=\"node4\" class=\"node\">\n", + "<title>z2</title>\n", + "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-177 16,-177 16,-141 70,-141 70,-177\"/>\n", + "<text text-anchor=\"middle\" x=\"43\" y=\"-155.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z2</text>\n", "</g>\n", "<!-- z1->z2 -->\n", - "<g id=\"edge10\" class=\"edge\"><title>z1->z2</title>\n", - "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-195.614C43,-183.24 43,-166.369 43,-152.22\"/>\n", - "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5001,-152.05 43,-142.05 39.5001,-152.05 46.5001,-152.05\"/>\n", - "<text text-anchor=\"middle\" x=\"46.5\" y=\"-164.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge5\" class=\"edge\">\n", + "<title>z1->z2</title>\n", + "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-265.8239C43,-245.2723 43,-211.5472 43,-187.4893\"/>\n", + "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-187.198 43,-177.198 39.5001,-187.198 46.5001,-187.198\"/>\n", + "<text text-anchor=\"middle\" x=\"47\" y=\"-217.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- z3 -->\n", - "<g id=\"node5\" class=\"node\"><title>z3</title>\n", + "<g id=\"node3\" class=\"node\">\n", + "<title>z3</title>\n", "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n", - "<text text-anchor=\"middle\" x=\"43\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">z3</text>\n", + "<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z3</text>\n", "</g>\n", "<!-- z3->z3 -->\n", - "<g id=\"edge6\" class=\"edge\"><title>z3->z3</title>\n", - "<path fill=\"none\" stroke=\"sienna\" d=\"M70.2408,-42.2419C80.0239,-42.4192 88,-39.6719 88,-34 88,-30.5437 85.0382,-28.1734 80.5105,-26.8891\"/>\n", - "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"80.5639,-23.3739 70.2408,-25.7581 79.7975,-30.3318 80.5639,-23.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"91.5\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge3\" class=\"edge\">\n", + "<title>z3->z3</title>\n", + "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.2408,-40.7434C80.0239,-40.8884 88,-38.6406 88,-34 88,-31.1721 85.0382,-29.2328 80.5105,-28.182\"/>\n", + "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"80.5146,-24.6683 70.2408,-27.2566 79.8863,-31.64 80.5146,-24.6683\"/>\n", + "<text text-anchor=\"middle\" x=\"92\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- z2->z3 -->\n", - "<g id=\"edge8\" class=\"edge\"><title>z2->z3</title>\n", - "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-105.614C43,-93.2403 43,-76.3686 43,-62.2198\"/>\n", - "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5001,-62.0504 43,-52.0504 39.5001,-62.0504 46.5001,-62.0504\"/>\n", - "<text text-anchor=\"middle\" x=\"46.5\" y=\"-74.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge4\" class=\"edge\">\n", + "<title>z2->z3</title>\n", + "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-140.8239C43,-120.2723 43,-86.5472 43,-62.4893\"/>\n", + "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-62.198 43,-52.198 39.5001,-62.198 46.5001,-62.198\"/>\n", + "<text text-anchor=\"middle\" x=\"47\" y=\"-92.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "</g>\n", "</svg>" @@ -304,7 +338,7 @@ "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:δ(x, 0)})]>" ] }, - "execution_count": 8, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -323,7 +357,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -335,7 +369,7 @@ "{z0,z1,z2,z3}" ] }, - "execution_count": 9, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -353,7 +387,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -365,7 +399,7 @@ "{z2}" ] }, - "execution_count": 10, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -383,7 +417,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -404,7 +438,7 @@ "1\t1\t1\n" ] }, - "execution_count": 11, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -422,7 +456,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -443,7 +477,7 @@ "1\t0\t1\n" ] }, - "execution_count": 12, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -486,7 +520,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -498,7 +532,7 @@ "{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}" ] }, - "execution_count": 13, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -511,12 +545,12 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Tabellarisch k¨ønnen wir $\\widehat{\\delta}$ für $\\pow(Z)$ wie folgt ausrechnen:" + "Tabellarisch können wir $\\widehat{\\delta}$ für $\\pow(Z)$ wie folgt ausrechnen:" ] }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -593,7 +627,7 @@ "{z3}\t1\t{z3}\n" ] }, - "execution_count": 14, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -611,7 +645,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -620,7 +654,7 @@ "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n" ] }, - "execution_count": 15, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -631,7 +665,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -640,339 +674,396 @@ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", - "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"648pt\" height=\"584pt\"\n", - " viewBox=\"0.00 0.00 648.00 584.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", - "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 580)\">\n", + "<svg width=\"662pt\" height=\"566pt\"\n", + " viewBox=\"0.00 0.00 662.00 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 562)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-580 645,-580 645,5 -4,5\"/>\n", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-562 658,-562 658,4 -4,4\"/>\n", "<!-- \\{z2,z3\\} -->\n", - "<g id=\"node1\" class=\"node\"><title>\\{z2,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"230.524,-486 171.476,-486 171.476,-450 230.524,-450 230.524,-486\"/>\n", - "<text text-anchor=\"middle\" x=\"201\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z2,z3}</text>\n", + "<g id=\"node1\" class=\"node\">\n", + "<title>\\{z2,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"226,-471 166,-471 166,-435 226,-435 226,-471\"/>\n", + "<text text-anchor=\"middle\" x=\"196\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2,z3}</text>\n", "</g>\n", "<!-- \\{z2,z3\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge2\" class=\"edge\"><title>\\{z2,z3\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M230.375,-476.25C240.167,-476.25 248,-473.5 248,-468 248,-464.648 245.091,-462.318 240.603,-461.009\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.728,-457.498 230.375,-459.75 239.873,-464.445 240.728,-457.498\"/>\n", - "<text text-anchor=\"middle\" x=\"258.107\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge1\" class=\"edge\">\n", + "<title>\\{z2,z3\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M226.4673,-460.8731C236.248,-460.7923 244,-458.168 244,-453 244,-449.8508 241.1214,-447.6461 236.6593,-446.3859\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"236.8209,-442.8794 226.4673,-445.1269 235.9627,-449.8266 236.8209,-442.8794\"/>\n", + "<text text-anchor=\"middle\" x=\"254.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z3\\} -->\n", - "<g id=\"node19\" class=\"node\"><title>\\{z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"147,-396 93,-396 93,-360 147,-360 147,-396\"/>\n", - "<text text-anchor=\"middle\" x=\"120\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z3}</text>\n", + "<g id=\"node10\" class=\"node\">\n", + "<title>\\{z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"185,-384 131,-384 131,-348 185,-348 185,-384\"/>\n", + "<text text-anchor=\"middle\" x=\"158\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z3}</text>\n", "</g>\n", "<!-- \\{z2,z3\\}->\\{z3\\} -->\n", - "<g id=\"edge22\" class=\"edge\"><title>\\{z2,z3\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M171.56,-453.384C161.851,-447.811 151.604,-440.623 144,-432 137.328,-424.433 132.209,-414.704 128.447,-405.651\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"131.695,-404.345 124.887,-396.227 125.146,-406.819 131.695,-404.345\"/>\n", - "<text text-anchor=\"middle\" x=\"147.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge11\" class=\"edge\">\n", + "<title>\\{z2,z3\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.1924,-434.6451C169.3745,-429.4531 164.8587,-423.4437 162,-417 158.8801,-409.9675 157.4136,-401.8548 156.8388,-394.1981\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.3368,-394.0739 156.5362,-384.1842 153.34,-394.2854 160.3368,-394.0739\"/>\n", + "<text text-anchor=\"middle\" x=\"166\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z2,z3\\}->\\{z3\\} -->\n", - "<g id=\"edge54\" class=\"edge\"><title>\\{z2,z3\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M184.997,-449.614C172.938,-436.512 156.237,-418.368 142.784,-403.753\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"145.042,-401.038 135.694,-396.05 139.891,-405.778 145.042,-401.038\"/>\n", - "<text text-anchor=\"middle\" x=\"171.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge27\" class=\"edge\">\n", + "<title>\\{z2,z3\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M188.1264,-434.9735C182.8784,-422.9585 175.8819,-406.9401 169.9523,-393.3646\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.0737,-391.7664 165.8635,-384.0034 166.6589,-394.5683 173.0737,-391.7664\"/>\n", + "<text text-anchor=\"middle\" x=\"184\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z1,z2,z3\\} -->\n", - "<g id=\"node3\" class=\"node\"><title>\\{z1,z2,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"148.061,-576 71.9392,-576 71.9392,-540 148.061,-540 148.061,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"110\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2,z3}</text>\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>\\{z1,z2,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"149.5,-558 72.5,-558 72.5,-522 149.5,-522 149.5,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"111\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2,z3}</text>\n", "</g>\n", "<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge24\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M112.276,-539.994C114.566,-528.65 119.102,-514.033 128,-504 137.141,-493.694 149.984,-486.149 162.353,-480.761\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"163.66,-484.008 171.651,-477.052 161.066,-477.507 163.66,-484.008\"/>\n", - "<text text-anchor=\"middle\" x=\"131.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge12\" class=\"edge\">\n", + "<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M111.9305,-521.819C113.3101,-511.2556 116.546,-498.2486 124,-489 132.3732,-478.611 144.5156,-470.9638 156.4511,-465.4583\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"158.0369,-468.5886 165.9028,-461.4908 155.3275,-462.1342 158.0369,-468.5886\"/>\n", + "<text text-anchor=\"middle\" x=\"128\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge56\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M127.979,-539.614C141.652,-526.391 160.638,-508.032 175.822,-493.348\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"178.613,-495.518 183.368,-486.05 173.747,-490.486 178.613,-495.518\"/>\n", - "<text text-anchor=\"middle\" x=\"167.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge28\" class=\"edge\">\n", + "<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M128.6121,-521.9735C140.9208,-509.3752 157.5297,-492.3755 171.1785,-478.4055\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.9256,-480.6021 178.4105,-471.0034 168.9186,-475.7103 173.9256,-480.6021\"/>\n", + "<text text-anchor=\"middle\" x=\"163\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z1,z2,z3\\}->\\{z1,z2,z3\\} -->\n", - "<g id=\"edge4\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z1,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M148.214,-566.177C158.335,-565.71 166,-562.984 166,-558 166,-554.885 163.006,-552.652 158.289,-551.301\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"158.616,-547.812 148.214,-549.823 157.6,-554.737 158.616,-547.812\"/>\n", - "<text text-anchor=\"middle\" x=\"176.107\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge2\" class=\"edge\">\n", + "<title>\\{z1,z2,z3\\}->\\{z1,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M149.5552,-547.8058C159.7662,-547.3597 167.5,-544.7578 167.5,-540 167.5,-537.0264 164.479,-534.8949 159.7203,-533.6055\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"159.9415,-530.1027 149.5552,-532.1942 158.9788,-537.0362 159.9415,-530.1027\"/>\n", + "<text text-anchor=\"middle\" x=\"178\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z2,z3\\} -->\n", - "<g id=\"node5\" class=\"node\"><title>\\{z0,z2,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"403.061,-306 326.939,-306 326.939,-270 403.061,-270 403.061,-306\"/>\n", - "<text text-anchor=\"middle\" x=\"365\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2,z3}</text>\n", + "<g id=\"node3\" class=\"node\">\n", + "<title>\\{z0,z2,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-297 272.5,-297 272.5,-261 349.5,-261 349.5,-297\"/>\n", + "<text text-anchor=\"middle\" x=\"311\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2,z3}</text>\n", "</g>\n", "<!-- \\{z0,z2,z3\\}->\\{z0,z2,z3\\} -->\n", - "<g id=\"edge6\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M403.214,-296.177C413.335,-295.71 421,-292.984 421,-288 421,-284.885 418.006,-282.652 413.289,-281.301\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"413.616,-277.812 403.214,-279.823 412.6,-284.737 413.616,-277.812\"/>\n", - "<text text-anchor=\"middle\" x=\"431.107\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge3\" class=\"edge\">\n", + "<title>\\{z0,z2,z3\\}->\\{z0,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-286.8058C359.7662,-286.3597 367.5,-283.7578 367.5,-279 367.5,-276.0264 364.479,-273.8949 359.7203,-272.6055\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-269.1027 349.5552,-271.1942 358.9788,-276.0362 359.9415,-269.1027\"/>\n", + "<text text-anchor=\"middle\" x=\"378\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z1,z3\\} -->\n", - "<g id=\"node24\" class=\"node\"><title>\\{z0,z1,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"446.061,-126 369.939,-126 369.939,-90 446.061,-90 446.061,-126\"/>\n", - "<text text-anchor=\"middle\" x=\"408\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z3}</text>\n", + "<g id=\"node11\" class=\"node\">\n", + "<title>\\{z0,z1,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"393.5,-123 316.5,-123 316.5,-87 393.5,-87 393.5,-123\"/>\n", + "<text text-anchor=\"middle\" x=\"355\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z3}</text>\n", "</g>\n", "<!-- \\{z0,z2,z3\\}->\\{z0,z1,z3\\} -->\n", - "<g id=\"edge26\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z1,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M365.892,-269.687C367.306,-248.306 370.797,-210.968 379,-180 383.021,-164.82 389.492,-148.558 395.302,-135.432\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"398.604,-136.628 399.565,-126.076 392.234,-133.725 398.604,-136.628\"/>\n", - "<text text-anchor=\"middle\" x=\"382.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge13\" class=\"edge\">\n", + "<title>\\{z0,z2,z3\\}->\\{z0,z1,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.8901,-260.86C313.2776,-239.6836 316.7192,-203.7656 325,-174 328.9228,-159.8994 335.1587,-144.9239 340.9314,-132.5406\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"344.2285,-133.7603 345.4087,-123.2314 337.9202,-130.7263 344.2285,-133.7603\"/>\n", + "<text text-anchor=\"middle\" x=\"329\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z0,z3\\} -->\n", - "<g id=\"node34\" class=\"node\"><title>\\{z0,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"536.524,-216 477.476,-216 477.476,-180 536.524,-180 536.524,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"507\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z3}</text>\n", + "<g id=\"node14\" class=\"node\">\n", + "<title>\\{z0,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"487,-210 427,-210 427,-174 487,-174 487,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"457\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z3}</text>\n", "</g>\n", "<!-- \\{z0,z2,z3\\}->\\{z0,z3\\} -->\n", - "<g id=\"edge58\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M392.716,-269.824C415,-256.014 446.483,-236.503 470.764,-221.456\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"472.697,-224.376 479.354,-216.133 469.01,-218.426 472.697,-224.376\"/>\n", - "<text text-anchor=\"middle\" x=\"452.5\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge29\" class=\"edge\">\n", + "<title>\\{z0,z2,z3\\}->\\{z0,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M341.2513,-260.9735C363.47,-247.7336 393.8464,-229.6326 417.9059,-215.2958\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"419.9886,-218.1291 426.7875,-210.0034 416.4053,-212.1157 419.9886,-218.1291\"/>\n", + "<text text-anchor=\"middle\" x=\"396\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z2\\} -->\n", - "<g id=\"node7\" class=\"node\"><title>\\{z2\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"84,-486 30,-486 30,-450 84,-450 84,-486\"/>\n", - "<text text-anchor=\"middle\" x=\"57\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z2}</text>\n", + "<g id=\"node4\" class=\"node\">\n", + "<title>\\{z2\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"92,-471 38,-471 38,-435 92,-435 92,-471\"/>\n", + "<text text-anchor=\"middle\" x=\"65\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2}</text>\n", "</g>\n", "<!-- \\{z2\\}->\\{z2\\} -->\n", - "<g id=\"edge8\" class=\"edge\"><title>\\{z2\\}->\\{z2\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M84.2408,-476.242C94.0239,-476.419 102,-473.672 102,-468 102,-464.544 99.0382,-462.173 94.5105,-460.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"94.5639,-457.374 84.2408,-459.758 93.7975,-464.332 94.5639,-457.374\"/>\n", - "<text text-anchor=\"middle\" x=\"112.107\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge4\" class=\"edge\">\n", + "<title>\\{z2\\}->\\{z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M92.2408,-460.8673C102.0239,-461.0365 110,-458.4141 110,-453 110,-449.7008 107.0382,-447.4382 102.5105,-446.2123\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"102.5519,-442.6975 92.2408,-445.1327 101.82,-449.6591 102.5519,-442.6975\"/>\n", + "<text text-anchor=\"middle\" x=\"120.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z2\\}->\\{z3\\} -->\n", - "<g id=\"edge28\" class=\"edge\"><title>\\{z2\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M60.6361,-449.617C63.525,-438.671 68.3732,-424.649 76,-414 78.8347,-410.042 82.2349,-406.298 85.8727,-402.835\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"88.3202,-405.344 93.5685,-396.141 83.7263,-400.063 88.3202,-405.344\"/>\n", - "<text text-anchor=\"middle\" x=\"79.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge14\" class=\"edge\">\n", + "<title>\\{z2\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M70.7229,-434.7868C74.7704,-424.2121 81.0778,-411.2043 90,-402 98.8615,-392.8583 110.5505,-385.5335 121.7332,-379.9399\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"123.3523,-383.0468 130.9344,-375.6466 120.3924,-376.7033 123.3523,-383.0468\"/>\n", + "<text text-anchor=\"middle\" x=\"94\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z2\\}->\\{z3\\} -->\n", - "<g id=\"edge60\" class=\"edge\"><title>\\{z2\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M69.7965,-449.984C74.0351,-444.293 78.753,-437.897 83,-432 89.3945,-423.122 96.2851,-413.319 102.367,-404.583\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"105.305,-406.487 108.13,-396.276 99.5535,-402.497 105.305,-406.487\"/>\n", - "<text text-anchor=\"middle\" x=\"99.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge30\" class=\"edge\">\n", + "<title>\\{z2\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M84.2697,-434.9735C97.8615,-422.2586 116.2459,-405.0603 131.2563,-391.0183\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"133.8433,-393.3909 138.755,-384.0034 129.0612,-388.279 133.8433,-393.3909\"/>\n", + "<text text-anchor=\"middle\" x=\"122\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1,z2,z3\\} -->\n", - "<g id=\"node9\" class=\"node\"><title>\\{z0,z1,z2,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"365.097,-36 272.903,-36 272.903,-0 365.097,-0 365.097,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"319\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2,z3}</text>\n", + "<g id=\"node5\" class=\"node\">\n", + "<title>\\{z0,z1,z2,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"311.5,-36 218.5,-36 218.5,0 311.5,0 311.5,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"265\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2,z3}</text>\n", "</g>\n", "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\} -->\n", - "<g id=\"edge62\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M321.923,-36.0293C329.684,-81.2458 350.861,-204.624 360.324,-259.755\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"356.911,-260.564 362.053,-269.828 363.81,-259.38 356.911,-260.564\"/>\n", - "<text text-anchor=\"middle\" x=\"347.5\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge31\" class=\"edge\">\n", + "<title>\\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M268.2311,-36.3327C276.1454,-81.2381 296.5441,-196.9783 306.0223,-250.7568\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"302.5827,-251.4063 307.7654,-260.647 309.4765,-250.1912 302.5827,-251.4063\"/>\n", + "<text text-anchor=\"middle\" x=\"294\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n", - "<g id=\"edge30\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M365.462,-34.5249C385.713,-35.8778 403.215,-30.3695 403.215,-18 403.215,-7.75648 391.212,-2.21833 375.585,-1.38554\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"375.43,2.11332 365.462,-1.47508 375.492,-4.88641 375.43,2.11332\"/>\n", - "<text text-anchor=\"middle\" x=\"406.715\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge5\" class=\"edge\">\n", + "<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M311.6737,-21.8315C321.988,-21.4715 329.5,-20.1943 329.5,-18 329.5,-16.6285 326.5656,-15.6153 321.8467,-14.9604\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"321.9152,-11.4553 311.6737,-14.1685 321.3718,-18.4341 321.9152,-11.4553\"/>\n", + "<text text-anchor=\"middle\" x=\"340\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n", - "<g id=\"edge10\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M365.312,-22.014C375.546,-21.6368 383,-20.2988 383,-18 383,-16.5632 380.088,-15.5018 375.406,-14.8157\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"375.565,-11.317 365.312,-13.986 374.992,-18.2935 375.565,-11.317\"/>\n", - "<text text-anchor=\"middle\" x=\"393.107\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge15\" class=\"edge\">\n", + "<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.6325,-25.7669C332.4024,-26.4542 350.5,-23.8652 350.5,-18 350.5,-13.1429 338.0889,-10.5326 322.0269,-10.1691\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"321.6107,-6.6715 311.6325,-10.2331 321.6539,-13.6714 321.6107,-6.6715\"/>\n", + "<text text-anchor=\"middle\" x=\"354.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1,z2\\} -->\n", - "<g id=\"node11\" class=\"node\"><title>\\{z1,z2\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"263.524,-576 204.476,-576 204.476,-540 263.524,-540 263.524,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"234\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2}</text>\n", + "<g id=\"node6\" class=\"node\">\n", + "<title>\\{z1,z2\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"267,-558 207,-558 207,-522 267,-522 267,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"237\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2}</text>\n", "</g>\n", "<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge34\" class=\"edge\"><title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M216.969,-539.766C212.679,-534.468 208.568,-528.348 206,-522 202.783,-514.048 201.242,-504.896 200.584,-496.458\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"204.074,-496.145 200.163,-486.298 197.08,-496.434 204.074,-496.145\"/>\n", - "<text text-anchor=\"middle\" x=\"209.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge17\" class=\"edge\">\n", + "<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M212.1632,-521.6958C206.9289,-516.5786 202.0676,-510.5913 199,-504 195.7581,-497.0343 194.3667,-488.9431 193.9447,-481.2858\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"197.4445,-481.239 193.8872,-471.2593 190.4447,-481.2792 197.4445,-481.239\"/>\n", + "<text text-anchor=\"middle\" x=\"203\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge66\" class=\"edge\"><title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M227.48,-539.614C222.795,-527.119 216.389,-510.037 211.052,-495.804\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"214.182,-494.185 207.394,-486.05 207.628,-496.643 214.182,-494.185\"/>\n", - "<text text-anchor=\"middle\" x=\"224.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge33\" class=\"edge\">\n", + "<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M228.5048,-521.9735C222.8425,-509.9585 215.2936,-493.9401 208.8959,-480.3646\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"211.9134,-478.5571 204.4843,-471.0034 205.5813,-481.5413 211.9134,-478.5571\"/>\n", + "<text text-anchor=\"middle\" x=\"223\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z1,z2\\}->\\{z1,z2\\} -->\n", - "<g id=\"edge12\" class=\"edge\"><title>\\{z1,z2\\}->\\{z1,z2\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.375,-566.25C273.167,-566.25 281,-563.5 281,-558 281,-554.648 278.091,-552.318 273.603,-551.009\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"273.728,-547.498 263.375,-549.75 272.873,-554.445 273.728,-547.498\"/>\n", - "<text text-anchor=\"middle\" x=\"291.107\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge6\" class=\"edge\">\n", + "<title>\\{z1,z2\\}->\\{z1,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M267.4673,-547.8731C277.248,-547.7923 285,-545.168 285,-540 285,-536.8508 282.1214,-534.6461 277.6593,-533.3859\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"277.8209,-529.8794 267.4673,-532.1269 276.9627,-536.8266 277.8209,-529.8794\"/>\n", + "<text text-anchor=\"middle\" x=\"295.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z1,z2\\} -->\n", - "<g id=\"node13\" class=\"node\"><title>\\{z0,z1,z2\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"403.061,-396 326.939,-396 326.939,-360 403.061,-360 403.061,-396\"/>\n", - "<text text-anchor=\"middle\" x=\"365\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2}</text>\n", + "<g id=\"node7\" class=\"node\">\n", + "<title>\\{z0,z1,z2\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-384 272.5,-384 272.5,-348 349.5,-348 349.5,-384\"/>\n", + "<text text-anchor=\"middle\" x=\"311\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2}</text>\n", "</g>\n", "<!-- \\{z0,z1,z2\\}->\\{z0,z2,z3\\} -->\n", - "<g id=\"edge70\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M365,-359.614C365,-347.24 365,-330.369 365,-316.22\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"368.5,-316.05 365,-306.05 361.5,-316.05 368.5,-316.05\"/>\n", - "<text text-anchor=\"middle\" x=\"368.5\" y=\"-328.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge35\" class=\"edge\">\n", + "<title>\\{z0,z1,z2\\}->\\{z0,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M311,-347.9735C311,-336.1918 311,-320.5607 311,-307.1581\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"314.5001,-307.0033 311,-297.0034 307.5001,-307.0034 314.5001,-307.0033\"/>\n", + "<text text-anchor=\"middle\" x=\"315\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\} -->\n", - "<g id=\"edge38\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M332.764,-359.919C309.075,-344.787 281,-320.259 281,-289 281,-289 281,-289 281,-107 281,-84.815 291.305,-61.8717 301.182,-44.9761\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"304.29,-46.6044 306.557,-36.255 298.331,-42.9315 304.29,-46.6044\"/>\n", - "<text text-anchor=\"middle\" x=\"284.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge19\" class=\"edge\">\n", + "<title>\\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M276.834,-347.9744C253.5781,-332.9816 227,-309.2335 227,-279 227,-279 227,-279 227,-105 227,-83.4445 236.9173,-61.2074 246.6192,-44.6107\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"249.6526,-46.3596 251.9226,-36.0108 243.6945,-42.6853 249.6526,-46.3596\"/>\n", + "<text text-anchor=\"middle\" x=\"231\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2\\} -->\n", - "<g id=\"edge14\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z1,z2\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M403.214,-386.177C413.335,-385.71 421,-382.984 421,-378 421,-374.885 418.006,-372.652 413.289,-371.301\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"413.616,-367.812 403.214,-369.823 412.6,-374.737 413.616,-367.812\"/>\n", - "<text text-anchor=\"middle\" x=\"431.107\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge7\" class=\"edge\">\n", + "<title>\\{z0,z1,z2\\}->\\{z0,z1,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-373.8058C359.7662,-373.3597 367.5,-370.7578 367.5,-366 367.5,-363.0264 364.479,-360.8949 359.7203,-359.6055\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-356.1027 349.5552,-358.1942 358.9788,-363.0362 359.9415,-356.1027\"/>\n", + "<text text-anchor=\"middle\" x=\"378\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z2\\} -->\n", - "<g id=\"node15\" class=\"node\"><title>\\{z0,z2\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"518.524,-306 459.476,-306 459.476,-270 518.524,-270 518.524,-306\"/>\n", - "<text text-anchor=\"middle\" x=\"489\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2}</text>\n", + "<g id=\"node8\" class=\"node\">\n", + "<title>\\{z0,z2\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"467,-297 407,-297 407,-261 467,-261 467,-297\"/>\n", + "<text text-anchor=\"middle\" x=\"437\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2}</text>\n", "</g>\n", "<!-- \\{z0,z2\\}->\\{z0,z2\\} -->\n", - "<g id=\"edge16\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z2\\}</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M518.375,-296.25C528.167,-296.25 536,-293.5 536,-288 536,-284.648 533.091,-282.318 528.603,-281.009\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"528.728,-277.498 518.375,-279.75 527.873,-284.445 528.728,-277.498\"/>\n", - "<text text-anchor=\"middle\" x=\"546.107\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n", + "<g id=\"edge8\" class=\"edge\">\n", + "<title>\\{z0,z2\\}->\\{z0,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M467.4673,-286.8731C477.248,-286.7923 485,-284.168 485,-279 485,-275.8508 482.1214,-273.6461 477.6593,-272.3859\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"477.8209,-268.8794 467.4673,-271.1269 476.9627,-275.8266 477.8209,-268.8794\"/>\n", + "<text text-anchor=\"middle\" x=\"495.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n", "</g>\n", "<!-- \\{z0,z2\\}->\\{z0,z1,z3\\} -->\n", - "<g id=\"edge44\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z1,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M481.233,-269.933C467.021,-238.7 436.745,-172.169 419.913,-135.178\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"423.071,-133.668 415.743,-126.016 416.699,-136.567 423.071,-133.668\"/>\n", - "<text text-anchor=\"middle\" x=\"460.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge22\" class=\"edge\">\n", + "<title>\\{z0,z2\\}->\\{z0,z1,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M428.3795,-260.7078C413.9466,-230.0818 384.8161,-168.2682 367.9228,-132.4216\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"370.934,-130.6009 363.505,-123.0471 364.6019,-133.585 370.934,-130.6009\"/>\n", + "<text text-anchor=\"middle\" x=\"408\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z0,z2\\}->\\{z0,z3\\} -->\n", - "<g id=\"edge76\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M492.556,-269.614C495.087,-257.24 498.538,-240.369 501.432,-226.22\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"504.937,-226.549 503.512,-216.05 498.079,-225.146 504.937,-226.549\"/>\n", - "<text text-anchor=\"middle\" x=\"502.5\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge38\" class=\"edge\">\n", + "<title>\\{z0,z2\\}->\\{z0,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M441.144,-260.9735C443.8793,-249.0751 447.5171,-233.2508 450.6182,-219.7606\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"454.0318,-220.5333 452.8613,-210.0034 447.2098,-218.965 454.0318,-220.5333\"/>\n", + "<text text-anchor=\"middle\" x=\"452\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0\\} -->\n", - "<g id=\"node17\" class=\"node\"><title>\\{z0\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"451,-576 397,-576 397,-540 451,-540 451,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"424\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0}</text>\n", + "<g id=\"node9\" class=\"node\">\n", + "<title>\\{z0\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"461,-558 407,-558 407,-522 461,-522 461,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"434\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0}</text>\n", "</g>\n", "<!-- \\{z0\\}->\\{z0\\} -->\n", - "<g id=\"edge80\" class=\"edge\"><title>\\{z0\\}->\\{z0\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M451.128,-572.838C471.639,-577.842 493.101,-572.896 493.101,-558 493.101,-545.548 478.104,-540.049 461.201,-541.503\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"460.426,-538.083 451.128,-543.162 461.564,-544.99 460.426,-538.083\"/>\n", - "<text text-anchor=\"middle\" x=\"496.601\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge9\" class=\"edge\">\n", + "<title>\\{z0\\}->\\{z0\\}</title>\n", + "<path fill=\"none\" stroke=\"#a0522d\" d=\"M461.2408,-543.9337C471.0239,-544.0182 479,-542.707 479,-540 479,-538.3504 476.0382,-537.2191 471.5105,-536.6062\"/>\n", + "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"471.4107,-533.0962 461.2408,-536.0663 471.0432,-540.0865 471.4107,-533.0962\"/>\n", + "<text text-anchor=\"middle\" x=\"491.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">start</text>\n", "</g>\n", "<!-- \\{z0\\}->\\{z0\\} -->\n", - "<g id=\"edge18\" class=\"edge\"><title>\\{z0\\}->\\{z0\\}</title>\n", - "<path fill=\"none\" stroke=\"sienna\" d=\"M451.241,-562.121C461.024,-562.21 469,-560.836 469,-558 469,-556.272 466.038,-555.087 461.51,-554.445\"/>\n", - "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"461.418,-550.934 451.241,-553.879 461.033,-557.924 461.418,-550.934\"/>\n", - "<text text-anchor=\"middle\" x=\"481.05\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">start</text>\n", + "<g id=\"edge40\" class=\"edge\">\n", + "<title>\\{z0\\}->\\{z0\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M461.36,-546.9863C482.1371,-549.3424 504,-547.0137 504,-540 504,-534.137 488.7224,-531.5478 471.5725,-532.2324\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"471.0638,-528.761 461.36,-533.0137 471.5979,-535.7406 471.0638,-528.761\"/>\n", + "<text text-anchor=\"middle\" x=\"508\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1\\} -->\n", - "<g id=\"node37\" class=\"node\"><title>\\{z0,z1\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"453.524,-486 394.476,-486 394.476,-450 453.524,-450 453.524,-486\"/>\n", - "<text text-anchor=\"middle\" x=\"424\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1}</text>\n", + "<g id=\"node15\" class=\"node\">\n", + "<title>\\{z0,z1\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"464,-471 404,-471 404,-435 464,-435 464,-471\"/>\n", + "<text text-anchor=\"middle\" x=\"434\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1}</text>\n", "</g>\n", "<!-- \\{z0\\}->\\{z0,z1\\} -->\n", - "<g id=\"edge48\" class=\"edge\"><title>\\{z0\\}->\\{z0,z1\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M424,-539.614C424,-527.24 424,-510.369 424,-496.22\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"427.5,-496.05 424,-486.05 420.5,-496.05 427.5,-496.05\"/>\n", - "<text text-anchor=\"middle\" x=\"427.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge24\" class=\"edge\">\n", + "<title>\\{z0\\}->\\{z0,z1\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M434,-521.9735C434,-510.1918 434,-494.5607 434,-481.1581\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"437.5001,-481.0033 434,-471.0034 430.5001,-481.0034 437.5001,-481.0033\"/>\n", + "<text text-anchor=\"middle\" x=\"438\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z3\\}->\\{z3\\} -->\n", - "<g id=\"edge52\" class=\"edge\"><title>\\{z3\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M147.198,-393.251C165.34,-397.544 183,-392.46 183,-378 183,-366.251 171.342,-360.692 157.239,-361.323\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"156.606,-357.878 147.198,-362.749 157.59,-364.808 156.606,-357.878\"/>\n", - "<text text-anchor=\"middle\" x=\"186.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge10\" class=\"edge\">\n", + "<title>\\{z3\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.2408,-369.9337C195.0239,-370.0182 203,-368.707 203,-366 203,-364.3504 200.0382,-363.2191 195.5105,-362.6062\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"195.4107,-359.0962 185.2408,-362.0663 195.0432,-366.0865 195.4107,-359.0962\"/>\n", + "<text text-anchor=\"middle\" x=\"207\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z3\\}->\\{z3\\} -->\n", - "<g id=\"edge20\" class=\"edge\"><title>\\{z3\\}->\\{z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M147.241,-382.121C157.024,-382.21 165,-380.836 165,-378 165,-376.272 162.038,-375.087 157.51,-374.445\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"157.418,-370.934 147.241,-373.879 157.033,-377.924 157.418,-370.934\"/>\n", - "<text text-anchor=\"middle\" x=\"168.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge26\" class=\"edge\">\n", + "<title>\\{z3\\}->\\{z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M185.1975,-373.1809C203.3402,-375.2022 221,-372.8086 221,-366 221,-360.468 209.3418,-357.8506 195.2386,-358.1477\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"194.9417,-354.6597 185.1975,-358.8191 195.4088,-361.6441 194.9417,-354.6597\"/>\n", + "<text text-anchor=\"middle\" x=\"225\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1,z3\\}->\\{z0,z2,z3\\} -->\n", - "<g id=\"edge68\" class=\"edge\"><title>\\{z0,z1,z3\\}->\\{z0,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M406.684,-126.14C404.221,-153.399 397.765,-208.04 383,-252 382.062,-254.793 380.929,-257.639 379.693,-260.439\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"376.442,-259.123 375.232,-269.649 382.742,-262.175 376.442,-259.123\"/>\n", - "<text text-anchor=\"middle\" x=\"403.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge34\" class=\"edge\">\n", + "<title>\\{z0,z1,z3\\}->\\{z0,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M353.1903,-123.2704C350.1723,-150.0824 343.0098,-201.4126 329,-243 328.0589,-245.7937 326.9391,-248.6443 325.7251,-251.4571\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"322.4489,-250.1992 321.3575,-260.7377 328.7826,-253.18 322.4489,-250.1992\"/>\n", + "<text text-anchor=\"middle\" x=\"350\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\} -->\n", - "<g id=\"edge36\" class=\"edge\"><title>\\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M390.416,-89.614C377.043,-76.3912 358.475,-58.0317 343.624,-43.3476\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"345.816,-40.5926 336.244,-36.0504 340.894,-45.5703 345.816,-40.5926\"/>\n", - "<text text-anchor=\"middle\" x=\"375.5\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge18\" class=\"edge\">\n", + "<title>\\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M336.3519,-86.9735C323.1985,-74.2586 305.4072,-57.0603 290.881,-43.0183\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"293.2467,-40.4371 283.6242,-36.0034 288.3815,-45.4701 293.2467,-40.4371\"/>\n", + "<text text-anchor=\"middle\" x=\"320\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1,z3\\} -->\n", - "<g id=\"node27\" class=\"node\"><title>\\{z1,z3\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"378.524,-576 319.476,-576 319.476,-540 378.524,-540 378.524,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"349\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z3}</text>\n", + "<g id=\"node12\" class=\"node\">\n", + "<title>\\{z1,z3\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"384,-558 324,-558 324,-522 384,-522 384,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"354\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z3}</text>\n", "</g>\n", "<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge32\" class=\"edge\"><title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M320.113,-539.824C296.785,-525.953 263.786,-506.332 238.434,-491.258\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"240.199,-488.235 229.814,-486.133 236.621,-494.252 240.199,-488.235\"/>\n", - "<text text-anchor=\"middle\" x=\"292.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge16\" class=\"edge\">\n", + "<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M323.9095,-523.4312C298.7311,-509.5671 262.6249,-489.6859 235.1903,-474.5795\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"236.6952,-471.4126 226.2471,-469.6551 233.3187,-477.5445 236.6952,-471.4126\"/>\n", + "<text text-anchor=\"middle\" x=\"289\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n", - "<g id=\"edge64\" class=\"edge\"><title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M336.572,-539.66C327.555,-528.167 314.444,-513.509 300,-504 281.93,-492.104 259.339,-483.716 240.302,-478.14\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"241,-474.702 230.429,-475.402 239.13,-481.447 241,-474.702\"/>\n", - "<text text-anchor=\"middle\" x=\"325.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge32\" class=\"edge\">\n", + "<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M337.4415,-521.9971C326.7521,-511.2333 312.0684,-497.9537 297,-489 278.0574,-477.7442 255.0393,-469.2008 235.7642,-463.2678\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"236.649,-459.8798 226.0671,-460.4027 234.6655,-466.5929 236.649,-459.8798\"/>\n", + "<text text-anchor=\"middle\" x=\"322\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z1\\} -->\n", - "<g id=\"node32\" class=\"node\"><title>\\{z1\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-576 0,-576 0,-540 54,-540 54,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"27\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1}</text>\n", + "<g id=\"node13\" class=\"node\">\n", + "<title>\\{z1\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-558 0,-558 0,-522 54,-522 54,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"27\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1}</text>\n", "</g>\n", "<!-- \\{z1\\}->\\{z2\\} -->\n", - "<g id=\"edge40\" class=\"edge\"><title>\\{z1\\}->\\{z2\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M25.4389,-539.765C25.086,-529.134 25.7508,-515.399 30,-504 31.1794,-500.836 32.751,-497.726 34.5452,-494.744\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"37.6054,-496.473 40.4255,-486.26 31.8522,-492.485 37.6054,-496.473\"/>\n", - "<text text-anchor=\"middle\" x=\"33.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge20\" class=\"edge\">\n", + "<title>\\{z1\\}->\\{z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.0007,-521.8438C27.6026,-511.7804 29.3707,-499.2653 34,-489 35.4686,-485.7435 37.3276,-482.5584 39.4029,-479.5137\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.3516,-481.4212 45.6797,-471.3626 36.8054,-477.1503 42.3516,-481.4212\"/>\n", + "<text text-anchor=\"middle\" x=\"38\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z1\\}->\\{z2\\} -->\n", - "<g id=\"edge72\" class=\"edge\"><title>\\{z1\\}->\\{z2\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M32.927,-539.614C37.1867,-527.119 43.01,-510.037 47.8621,-495.804\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"51.2733,-496.645 51.1874,-486.05 44.6478,-494.386 51.2733,-496.645\"/>\n", - "<text text-anchor=\"middle\" x=\"48.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge36\" class=\"edge\">\n", + "<title>\\{z1\\}->\\{z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M34.8736,-521.9735C40.1216,-509.9585 47.1181,-493.9401 53.0477,-480.3646\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"56.3411,-481.5683 57.1365,-471.0034 49.9263,-478.7664 56.3411,-481.5683\"/>\n", + "<text text-anchor=\"middle\" x=\"53\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z3\\}->\\{z0,z1,z3\\} -->\n", - "<g id=\"edge42\" class=\"edge\"><title>\\{z0,z3\\}->\\{z0,z1,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M496.207,-179.918C488.647,-168.823 477.814,-154.523 466,-144 460.985,-139.533 455.32,-135.317 449.547,-131.462\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"451.391,-128.487 441.072,-126.087 447.641,-134.399 451.391,-128.487\"/>\n", - "<text text-anchor=\"middle\" x=\"485.5\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge21\" class=\"edge\">\n", + "<title>\\{z0,z3\\}->\\{z0,z1,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M444.3424,-173.6871C436.6232,-163.3329 426.1232,-150.5829 415,-141 409.8677,-136.5784 404.1243,-132.3749 398.2795,-128.5043\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"400.0264,-125.468 389.7031,-123.0849 396.2871,-131.3856 400.0264,-125.468\"/>\n", + "<text text-anchor=\"middle\" x=\"433\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z0,z3\\}->\\{z0,z3\\} -->\n", - "<g id=\"edge74\" class=\"edge\"><title>\\{z0,z3\\}->\\{z0,z3\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M536.375,-206.25C546.167,-206.25 554,-203.5 554,-198 554,-194.648 551.091,-192.318 546.603,-191.009\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"546.728,-187.498 536.375,-189.75 545.873,-194.445 546.728,-187.498\"/>\n", - "<text text-anchor=\"middle\" x=\"557.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge37\" class=\"edge\">\n", + "<title>\\{z0,z3\\}->\\{z0,z3\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M487.4673,-199.8731C497.248,-199.7923 505,-197.168 505,-192 505,-188.8508 502.1214,-186.6461 497.6593,-185.3859\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"497.8209,-181.8794 487.4673,-184.1269 496.9627,-188.8266 497.8209,-181.8794\"/>\n", + "<text text-anchor=\"middle\" x=\"509\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{z0,z1\\}->\\{z0,z1,z2\\} -->\n", - "<g id=\"edge46\" class=\"edge\"><title>\\{z0,z1\\}->\\{z0,z1,z2\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M412.343,-449.614C403.722,-436.755 391.844,-419.038 382.142,-404.568\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"384.907,-402.407 376.432,-396.05 379.093,-406.305 384.907,-402.407\"/>\n", - "<text text-anchor=\"middle\" x=\"403.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge23\" class=\"edge\">\n", + "<title>\\{z0,z1\\}->\\{z0,z1,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M408.5143,-434.9735C390.0432,-421.9086 364.8799,-404.1102 344.7418,-389.8662\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"346.6383,-386.9206 336.453,-384.0034 342.5961,-392.6355 346.6383,-386.9206\"/>\n", + "<text text-anchor=\"middle\" x=\"383\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{z0,z1\\}->\\{z0,z2\\} -->\n", - "<g id=\"edge78\" class=\"edge\"><title>\\{z0,z1\\}->\\{z0,z2\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M430.312,-449.786C435.582,-435.409 443.288,-414.371 450,-396 460.016,-368.585 471.449,-337.208 479.334,-315.554\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"482.661,-316.646 482.794,-306.052 476.084,-314.251 482.661,-316.646\"/>\n", - "<text text-anchor=\"middle\" x=\"466.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge39\" class=\"edge\">\n", + "<title>\\{z0,z1\\}->\\{z0,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M434.3154,-434.7078C434.8389,-404.3436 435.891,-343.3226 436.5113,-307.3464\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"440.0158,-307.106 436.6888,-297.0471 433.0169,-306.9852 440.0158,-307.106\"/>\n", + "<text text-anchor=\"middle\" x=\"439\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "<!-- \\{\\} -->\n", - "<g id=\"node40\" class=\"node\"><title>\\{\\}</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"590,-576 536,-576 536,-540 590,-540 590,-576\"/>\n", - "<text text-anchor=\"middle\" x=\"563\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{}</text>\n", + "<g id=\"node16\" class=\"node\">\n", + "<title>\\{\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"602,-558 548,-558 548,-522 602,-522 602,-558\"/>\n", + "<text text-anchor=\"middle\" x=\"575\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{}</text>\n", "</g>\n", "<!-- \\{\\}->\\{\\} -->\n", - "<g id=\"edge50\" class=\"edge\"><title>\\{\\}->\\{\\}</title>\n", - "<path fill=\"none\" stroke=\"#473c8b\" d=\"M590.241,-562.121C600.024,-562.21 608,-560.836 608,-558 608,-556.272 605.038,-555.087 600.51,-554.445\"/>\n", - "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"600.418,-550.934 590.241,-553.879 600.033,-557.924 600.418,-550.934\"/>\n", - "<text text-anchor=\"middle\" x=\"611.5\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"edge25\" class=\"edge\">\n", + "<title>\\{\\}->\\{\\}</title>\n", + "<path fill=\"none\" stroke=\"#473c8b\" d=\"M602.2408,-543.9337C612.0239,-544.0182 620,-542.707 620,-540 620,-538.3504 617.0382,-537.2191 612.5105,-536.6062\"/>\n", + "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"612.4107,-533.0962 602.2408,-536.0663 612.0432,-540.0865 612.4107,-533.0962\"/>\n", + "<text text-anchor=\"middle\" x=\"624\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n", "</g>\n", "<!-- \\{\\}->\\{\\} -->\n", - "<g id=\"edge82\" class=\"edge\"><title>\\{\\}->\\{\\}</title>\n", - "<path fill=\"none\" stroke=\"black\" d=\"M590.198,-573.251C608.34,-577.544 626,-572.46 626,-558 626,-546.251 614.342,-540.692 600.239,-541.323\"/>\n", - "<polygon fill=\"black\" stroke=\"black\" points=\"599.606,-537.878 590.198,-542.749 600.59,-544.808 599.606,-537.878\"/>\n", - "<text text-anchor=\"middle\" x=\"629.5\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "<g id=\"edge41\" class=\"edge\">\n", + "<title>\\{\\}->\\{\\}</title>\n", + "<path fill=\"none\" stroke=\"#000000\" d=\"M602.1975,-547.1809C620.3402,-549.2022 638,-546.8086 638,-540 638,-534.468 626.3418,-531.8506 612.2386,-532.1477\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"611.9417,-528.6597 602.1975,-532.8191 612.4088,-535.6441 611.9417,-528.6597\"/>\n", + "<text text-anchor=\"middle\" x=\"642\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n", "</g>\n", "</g>\n", "</svg>" @@ -981,7 +1072,7 @@ "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & δs(x, [0])=y})]>" ] }, - "execution_count": 16, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" }