From 049684d5a040dd11443ebc835f1c7201af7bde5c Mon Sep 17 00:00:00 2001
From: vhavlena <vohavlena@gmail.com>
Date: Wed, 11 Oct 2023 08:45:44 +0200
Subject: [PATCH 1/3] notebook showing basic visualization possibilities

---
 .../notebooks/example-04-visualization.ipynb  | 1376 +++++++++++++++++
 1 file changed, 1376 insertions(+)
 create mode 100644 examples/notebooks/example-04-visualization.ipynb

diff --git a/examples/notebooks/example-04-visualization.ipynb b/examples/notebooks/example-04-visualization.ipynb
new file mode 100644
index 000000000..7470ca893
--- /dev/null
+++ b/examples/notebooks/example-04-visualization.ipynb
@@ -0,0 +1,1376 @@
+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 38,
+   "id": "ec3e8285-352f-49ab-8f27-040e3684dabd",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import libmata as mata\n",
+    "from libmata.nfa.nfa import *\n",
+    "import libmata.plotting\n",
+    "\n",
+    "import matplotlib.pyplot as plt\n",
+    "import networkx as nx\n",
+    "import graphviz\n",
+    "import IPython\n",
+    "from  matplotlib.colors import LinearSegmentedColormap"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "1c61551c-2385-481a-9344-d687f3c893f7",
+   "metadata": {},
+   "source": [
+    "## Auxiliary Functions"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 39,
+   "id": "cfae9f5c-a084-4654-a1a5-dfcdd4d2b54c",
+   "metadata": {
+    "jupyter": {
+     "source_hidden": true
+    }
+   },
+   "outputs": [],
+   "source": [
+    "def distance_from(aut: Nfa) -> dict[int,int]:\n",
+    "    queue = []\n",
+    "    dist = dict()\n",
+    "    for q in aut.initial_states:\n",
+    "        dist[q] = 0\n",
+    "        queue.append(q)\n",
+    "\n",
+    "    while len(queue) != 0:\n",
+    "        act = queue.pop(0)\n",
+    "        for trans in aut.get_trans_from_state_as_sequence(act):\n",
+    "            if not trans.target in dist:\n",
+    "                dist[trans.target] = dist[act] + 1\n",
+    "                queue.append(trans.target)\n",
+    "    return dist\n",
+    "\n",
+    "def hexa_heat(minimum, maximum, value):\n",
+    "    ratio = 2 * (value-float(minimum)) / float((maximum - minimum))\n",
+    "    b = int(max(0, 255 * (1 - ratio)))\n",
+    "    r = int(max(0, 255 * (ratio - 1)))\n",
+    "    g = 255 - b - r\n",
+    "    return \"#{:02x}{:02x}{:02x}\".format(r, g, b)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3a10d72c-e5ad-443b-b223-d0f517883e10",
+   "metadata": {},
+   "source": [
+    "Creation of example automata"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 40,
+   "id": "7954d84f-386d-480c-bad8-b0f9bb2760d8",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "libmata.plotting.store()['alphabet'] = mata.alphabets.OnTheFlyAlphabet.from_symbol_map({\"0\":0, \"1\":1})\n",
+    "lhs = divisible_by(4)\n",
+    "lhs.label = \"aut1\"\n",
+    "rhs = divisible_by(3)\n",
+    "rhs.label = \"aut2\"\n",
+    "result = concatenate(lhs, rhs)\n",
+    "result.label = \"aut1.aut2\""
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "1594d6c5-27c9-4b29-a460-b615d3dc6ba6",
+   "metadata": {},
+   "source": [
+    "## Conditional State/Transition Formatting"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 41,
+   "id": "77230c54-2aed-4e8b-812a-b1f470316e81",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"90pt\" height=\"430pt\"\n",
+       " viewBox=\"0.00 0.00 90.35 430.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 426)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-426 86.35,-426 86.35,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"41.17\" y=\"-404.7\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut1</text>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"42.8\" cy=\"-315.2\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.8\" y=\"-310.93\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M42.8,-363.24C42.8,-355.67 42.8,-346.63 42.8,-338.5\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"46.3,-338.74 42.8,-328.74 39.3,-338.74 46.3,-338.74\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M52.84,-319.72C61.9,-321.91 71.6,-320.41 71.6,-315.2 71.6,-312.43 68.86,-310.71 64.94,-310.04\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"64.9,-306.53 55.1,-310.56 65.28,-313.52 64.9,-306.53\"/>\n",
+       "<text text-anchor=\"middle\" x=\"74.97\" y=\"-310.15\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"42.8\" cy=\"-241.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.8\" y=\"-236.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M42.8,-304.17C42.8,-293.84 42.8,-277.41 42.8,-264.04\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"46.3,-264.31 42.8,-254.31 39.3,-264.31 46.3,-264.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.17\" y=\"-273.1\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M52.54,-246.72C61.68,-249.63 71.6,-247.76 71.6,-241.1 71.6,-237.46 68.63,-235.25 64.45,-234.47\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"64.47,-230.96 54.8,-235.29 65.06,-237.93 64.47,-230.96\"/>\n",
+       "<text text-anchor=\"middle\" x=\"74.97\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-167\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-162.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M38.62,-230.67C33.85,-219.93 25.91,-202.05 19.74,-188.13\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"23.06,-187 15.8,-179.28 16.66,-189.84 23.06,-187\"/>\n",
+       "<text text-anchor=\"middle\" x=\"33.17\" y=\"-199\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-172.62C29.68,-175.53 39.6,-173.66 39.6,-167 39.6,-163.36 36.63,-161.15 32.45,-160.37\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.47,-156.86 22.8,-161.19 33.06,-163.83 32.47,-156.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-161.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-92.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-88.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M10.8,-155.97C10.8,-145.64 10.8,-129.21 10.8,-115.84\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"14.3,-116.11 10.8,-106.11 7.3,-116.11 14.3,-116.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"14.17\" y=\"-124.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-98.52C29.68,-101.43 39.6,-99.56 39.6,-92.9 39.6,-89.26 36.63,-87.05 32.45,-86.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.47,-82.76 22.8,-87.09 33.06,-89.73 32.47,-82.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"42.8\" cy=\"-14.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"42.8\" cy=\"-14.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.8\" y=\"-10.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M14.72,-82.57C19.13,-72.09 26.46,-54.66 32.53,-40.23\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"35.7,-41.71 36.35,-31.14 29.25,-39 35.7,-41.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"32.17\" y=\"-50.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;1 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>4&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M46.33,-29.65C49.53,-42.99 54.02,-63.77 55.8,-82.1 59.91,-124.43 60.17,-135.49 55.8,-177.8 54.38,-191.53 51.25,-206.71 48.42,-218.64\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"45.04,-217.73 46,-228.28 51.83,-219.43 45.04,-217.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"63.17\" y=\"-124.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.28,-21.67C65.96,-23.9 75.6,-21.61 75.6,-14.8 75.6,-11.07 72.72,-8.7 68.52,-7.68\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.47,-4.18 58.55,-7.89 68.62,-11.18 68.47,-4.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-9.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"94pt\" height=\"356pt\"\n",
+       " viewBox=\"0.00 0.00 94.35 355.90\" 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 351.9)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-351.9 90.35,-351.9 90.35,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"43.17\" y=\"-330.6\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut2</text>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-241.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-236.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M46.8,-289.14C46.8,-281.57 46.8,-272.53 46.8,-264.4\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.3,-264.64 46.8,-254.64 43.3,-264.64 50.3,-264.64\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.84,-245.62C65.9,-247.81 75.6,-246.31 75.6,-241.1 75.6,-238.33 72.86,-236.61 68.94,-235.94\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.9,-232.43 59.1,-236.46 69.28,-239.42 68.9,-232.43\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-167\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-162.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M46.8,-230.07C46.8,-219.74 46.8,-203.31 46.8,-189.94\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"50.3,-190.21 46.8,-180.21 43.3,-190.21 50.3,-190.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"50.17\" y=\"-199\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-172.62C65.68,-175.53 75.6,-173.66 75.6,-167 75.6,-163.36 72.63,-161.15 68.45,-160.37\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.47,-156.86 58.8,-161.19 69.06,-163.83 68.47,-156.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-161.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-92.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-88.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M42.24,-156.87C36.86,-146.09 27.76,-127.86 20.73,-113.78\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"24.05,-112.6 16.45,-105.22 17.79,-115.73 24.05,-112.6\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-124.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-98.52C29.68,-101.43 39.6,-99.56 39.6,-92.9 39.6,-89.26 36.63,-87.05 32.45,-86.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.47,-82.76 22.8,-87.09 33.06,-89.73 32.47,-82.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-10.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M15.21,-82.57C20.25,-71.92 28.68,-54.1 35.57,-39.55\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"38.58,-41.36 39.69,-30.83 32.25,-38.37 38.58,-41.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"35.17\" y=\"-50.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;1 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M49.74,-29.78C53.03,-47.11 57.68,-77.54 55.8,-103.7 54.83,-117.16 52.7,-132.14 50.76,-144.03\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"47.35,-143.22 49.1,-153.67 54.25,-144.41 47.35,-143.22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60.17\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M60.28,-21.67C69.96,-23.9 79.6,-21.61 79.6,-14.8 79.6,-11.07 76.72,-8.7 72.52,-7.68\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"72.47,-4.18 62.55,-7.89 72.62,-11.18 72.47,-4.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"82.97\" y=\"-9.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"94pt\" height=\"726pt\"\n",
+       " viewBox=\"0.00 0.00 94.35 726.40\" 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 722.4)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-722.4 90.35,-722.4 90.35,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"43.17\" y=\"-701.1\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut1.aut2</text>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-611.6\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-607.33\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M46.8,-659.64C46.8,-652.07 46.8,-643.03 46.8,-634.9\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.3,-635.14 46.8,-625.14 43.3,-635.14 50.3,-635.14\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.84,-616.12C65.9,-618.31 75.6,-616.81 75.6,-611.6 75.6,-608.83 72.86,-607.11 68.94,-606.44\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.9,-602.93 59.1,-606.96 69.28,-609.92 68.9,-602.93\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-606.55\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-537.5\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-533.23\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M46.8,-600.57C46.8,-590.24 46.8,-573.81 46.8,-560.44\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"50.3,-560.71 46.8,-550.71 43.3,-560.71 50.3,-560.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"50.17\" y=\"-569.5\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-543.12C65.68,-546.03 75.6,-544.16 75.6,-537.5 75.6,-533.86 72.63,-531.65 68.45,-530.87\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.47,-527.36 58.8,-531.69 69.06,-534.33 68.47,-527.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-532.45\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"14.8\" cy=\"-463.4\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"14.8\" y=\"-459.13\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M42.62,-527.07C37.85,-516.33 29.91,-498.45 23.74,-484.53\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"27.06,-483.4 19.8,-475.68 20.66,-486.24 27.06,-483.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.17\" y=\"-495.4\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M24.54,-469.02C33.68,-471.93 43.6,-470.06 43.6,-463.4 43.6,-459.76 40.63,-457.55 36.45,-456.77\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"36.47,-453.26 26.8,-457.59 37.06,-460.23 36.47,-453.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.97\" y=\"-458.35\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"14.8\" cy=\"-389.3\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"14.8\" y=\"-385.03\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M14.8,-452.37C14.8,-442.04 14.8,-425.61 14.8,-412.24\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"18.3,-412.51 14.8,-402.51 11.3,-412.51 18.3,-412.51\"/>\n",
+       "<text text-anchor=\"middle\" x=\"18.17\" y=\"-421.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M24.54,-394.92C33.68,-397.83 43.6,-395.96 43.6,-389.3 43.6,-385.66 40.63,-383.45 36.45,-382.67\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"36.47,-379.16 26.8,-383.49 37.06,-386.13 36.47,-379.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.97\" y=\"-384.25\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-315.2\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-310.93\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M18.98,-378.87C23.75,-368.13 31.69,-350.25 37.86,-336.33\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"40.94,-338.04 41.8,-327.48 34.54,-335.2 40.94,-338.04\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.17\" y=\"-347.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;1 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>4&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M49.45,-325.82C52.65,-337.97 57.85,-359.6 59.8,-378.5 64.17,-420.81 64.17,-431.89 59.8,-474.2 58.38,-487.93 55.25,-503.11 52.42,-515.04\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"49.04,-514.13 50,-524.68 55.83,-515.83 49.04,-514.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"67.17\" y=\"-421.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-320.82C65.68,-323.73 75.6,-321.86 75.6,-315.2 75.6,-311.56 72.63,-309.35 68.45,-308.57\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.47,-305.06 58.8,-309.39 69.06,-312.03 68.47,-305.06\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-310.15\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-241.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-236.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;5 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>4&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M42.24,-305.07C36.86,-294.29 27.76,-276.06 20.73,-261.98\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"24.05,-260.8 16.45,-253.42 17.79,-263.93 24.05,-260.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-273.1\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-167\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-162.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M48.71,-304.11C50.94,-291.82 54.47,-270.43 55.8,-251.9 57.32,-230.8 54.26,-206.81 51.3,-189.9\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"54.78,-189.45 49.47,-180.28 47.91,-190.76 54.78,-189.45\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60.17\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;5 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>5&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-246.72C29.68,-249.63 39.6,-247.76 39.6,-241.1 39.6,-237.46 36.63,-235.25 32.45,-234.47\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.47,-230.96 22.8,-235.29 33.06,-237.93 32.47,-230.96\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M15.36,-230.97C20.74,-220.19 29.84,-201.96 36.87,-187.88\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"39.81,-189.83 41.15,-179.32 33.55,-186.7 39.81,-189.83\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-199\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;6 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>6&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-172.62C65.68,-175.53 75.6,-173.66 75.6,-167 75.6,-163.36 72.63,-161.15 68.45,-160.37\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"68.47,-156.86 58.8,-161.19 69.06,-163.83 68.47,-156.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-161.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-92.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-88.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>6&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M42.24,-156.87C36.86,-146.09 27.76,-127.86 20.73,-113.78\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"24.05,-112.6 16.45,-105.22 17.79,-115.73 24.05,-112.6\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-124.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;7 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>7&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-98.52C29.68,-101.43 39.6,-99.56 39.6,-92.9 39.6,-89.26 36.63,-87.05 32.45,-86.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.47,-82.76 22.8,-87.09 33.06,-89.73 32.47,-82.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-10.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M15.21,-82.57C20.25,-71.92 28.68,-54.1 35.57,-39.55\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"38.58,-41.36 39.69,-30.83 32.25,-38.37 38.58,-41.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"35.17\" y=\"-50.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;6 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>8&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M49.74,-29.78C53.03,-47.11 57.68,-77.54 55.8,-103.7 54.83,-117.16 52.7,-132.14 50.76,-144.03\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"47.35,-143.22 49.1,-153.67 54.25,-144.41 47.35,-143.22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60.17\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;8 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>8&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M60.28,-21.67C69.96,-23.9 79.6,-21.61 79.6,-14.8 79.6,-11.07 76.72,-8.7 72.52,-7.68\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"72.47,-4.18 62.55,-7.89 72.62,-11.18 72.47,-4.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"82.97\" y=\"-9.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "e_h = [\n",
+    "    (lambda aut, edge: edge.symbol == 1, {'color': 'grey'}),\n",
+    "    (lambda aut, edge: edge.symbol == 0, {'style': 'dashed', 'color': 'grey'})\n",
+    "]\n",
+    "n_h = [\n",
+    "    (lambda aut, state: state in aut.final_states, {'color': 'red', 'fillcolor': 'red'}),\n",
+    "    (lambda aut, state: state in aut.initial_states, {'color': 'green', 'fillcolor': 'green'}),\n",
+    "]\n",
+    "libmata.plotting.plot(lhs, rhs, result, node_highlight=n_h, edge_highlight=e_h)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "dcfcf6e9-6ce5-4378-8743-fbe550813b42",
+   "metadata": {},
+   "source": [
+    "## SCC Visualization"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 42,
+   "id": "2f615ee8-e334-46d0-baab-4dbb8cc5de0b",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"107pt\" height=\"462pt\"\n",
+       " viewBox=\"0.00 0.00 107.00 462.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 458)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-458 103,-458 103,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"49.5\" y=\"-436.7\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut1</text>\n",
+       "<g id=\"clust1\" class=\"cluster\">\n",
+       "<title>cluster_0</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-8 8,-275.9 91,-275.9 91,-8 8,-8\"/>\n",
+       "</g>\n",
+       "<g id=\"clust2\" class=\"cluster\">\n",
+       "<title>cluster_1</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-312.4 8,-423 78,-423 78,-312.4 8,-312.4\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"34\" cy=\"-257.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34\" y=\"-252.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M43.74,-262.72C52.88,-265.63 62.8,-263.76 62.8,-257.1 62.8,-253.46 59.83,-251.25 55.65,-250.47\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"55.67,-246.96 46,-251.29 56.26,-253.93 55.67,-246.96\"/>\n",
+       "<text text-anchor=\"middle\" x=\"66.17\" y=\"-252.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-183\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-178.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M33.03,-246.07C32.02,-235.74 30.43,-219.31 29.13,-205.94\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.63,-205.81 28.18,-196.2 25.67,-206.49 32.63,-205.81\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34.38\" y=\"-215\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M36.74,-188.62C45.88,-191.53 55.8,-189.66 55.8,-183 55.8,-179.36 52.83,-177.15 48.65,-176.37\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"48.67,-172.86 39,-177.19 49.26,-179.83 48.67,-172.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"59.17\" y=\"-177.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-108.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-104.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M27,-171.97C27,-161.64 27,-145.21 27,-131.84\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"30.5,-132.11 27,-122.11 23.5,-132.11 30.5,-132.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.38\" y=\"-140.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M36.74,-114.52C45.88,-117.43 55.8,-115.56 55.8,-108.9 55.8,-105.26 52.83,-103.05 48.65,-102.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"48.67,-98.76 39,-103.09 49.26,-105.73 48.67,-98.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"59.17\" y=\"-103.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"40\" cy=\"-30.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"40\" cy=\"-30.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"40\" y=\"-26.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M28.7,-97.95C30.44,-87.77 33.21,-71.53 35.58,-57.69\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"38.98,-58.58 37.21,-48.13 32.08,-57.4 38.98,-58.58\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.38\" y=\"-66.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;1 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>4&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M47.91,-43.89C55.8,-56.73 67.38,-77.92 72,-98.1 81.48,-139.56 83.5,-152.85 72,-193.8 67.33,-210.42 56.86,-227 48.1,-238.87\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"45.52,-236.49 42.13,-246.53 51.04,-240.79 45.52,-236.49\"/>\n",
+       "<text text-anchor=\"middle\" x=\"82.38\" y=\"-140.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M53.48,-37.67C63.16,-39.9 72.8,-37.61 72.8,-30.8 72.8,-27.07 69.92,-24.7 65.72,-23.68\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"65.67,-20.18 55.75,-23.89 65.82,-27.18 65.67,-20.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"76.17\" y=\"-25.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"34\" cy=\"-331.2\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34\" y=\"-326.93\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M40.64,-379.24C39.55,-371.58 38.26,-362.4 37.1,-354.19\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"40.58,-353.76 35.71,-344.35 33.64,-354.74 40.58,-353.76\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M34,-320.17C34,-309.84 34,-293.41 34,-280.04\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"37.5,-280.31 34,-270.31 30.5,-280.31 37.5,-280.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.38\" y=\"-289.1\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M44.04,-335.72C53.1,-337.91 62.8,-336.41 62.8,-331.2 62.8,-328.43 60.06,-326.71 56.14,-326.04\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"56.1,-322.53 46.3,-326.56 56.48,-329.52 56.1,-322.53\"/>\n",
+       "<text text-anchor=\"middle\" x=\"66.17\" y=\"-326.15\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"130pt\" height=\"388pt\"\n",
+       " viewBox=\"0.00 0.00 130.00 387.90\" 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 383.9)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-383.9 126,-383.9 126,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"61\" y=\"-362.6\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut2</text>\n",
+       "<g id=\"clust1\" class=\"cluster\">\n",
+       "<title>cluster_0</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-8 8,-201.8 114,-201.8 114,-8 8,-8\"/>\n",
+       "</g>\n",
+       "<g id=\"clust2\" class=\"cluster\">\n",
+       "<title>cluster_1</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-238.3 8,-348.9 78,-348.9 78,-238.3 8,-238.3\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"34\" cy=\"-183\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34\" y=\"-178.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M43.74,-188.62C52.88,-191.53 62.8,-189.66 62.8,-183 62.8,-179.36 59.83,-177.15 55.65,-176.37\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"55.67,-172.86 46,-177.19 56.26,-179.83 55.67,-172.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"66.17\" y=\"-177.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-108.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-104.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M33.03,-171.97C32.02,-161.64 30.43,-145.21 29.13,-131.84\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"32.63,-131.71 28.18,-122.1 25.67,-132.39 32.63,-131.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34.38\" y=\"-140.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M36.74,-114.52C45.88,-117.43 55.8,-115.56 55.8,-108.9 55.8,-105.26 52.83,-103.05 48.65,-102.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"48.67,-98.76 39,-103.09 49.26,-105.73 48.67,-98.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"59.17\" y=\"-103.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"58\" cy=\"-30.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"58\" cy=\"-30.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"58\" y=\"-26.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M30.8,-98.57C35.07,-88.09 42.17,-70.66 48.05,-56.23\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"51.22,-57.73 51.75,-47.15 44.73,-55.09 51.22,-57.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"47.38\" y=\"-66.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;1 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M63.51,-44.81C70.09,-62.15 79.31,-93.67 72,-119.7 67.33,-136.32 56.86,-152.9 48.1,-164.77\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"45.52,-162.39 42.13,-172.43 51.04,-166.69 45.52,-162.39\"/>\n",
+       "<text text-anchor=\"middle\" x=\"77.38\" y=\"-103.85\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M71.48,-37.67C81.16,-39.9 90.8,-37.61 90.8,-30.8 90.8,-27.07 87.92,-24.7 83.72,-23.68\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"83.67,-20.18 73.75,-23.89 83.82,-27.18 83.67,-20.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"94.17\" y=\"-25.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"34\" cy=\"-257.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34\" y=\"-252.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M40.64,-305.14C39.55,-297.48 38.26,-288.3 37.1,-280.09\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"40.58,-279.66 35.71,-270.25 33.64,-280.64 40.58,-279.66\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M34,-246.07C34,-235.74 34,-219.31 34,-205.94\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"37.5,-206.21 34,-196.21 30.5,-206.21 37.5,-206.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.38\" y=\"-215\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M44.04,-261.62C53.1,-263.81 62.8,-262.31 62.8,-257.1 62.8,-254.33 60.06,-252.61 56.14,-251.94\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"56.1,-248.43 46.3,-252.46 56.48,-255.42 56.1,-248.43\"/>\n",
+       "<text text-anchor=\"middle\" x=\"66.17\" y=\"-252.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"204pt\" height=\"684pt\"\n",
+       " viewBox=\"0.00 0.00 204.00 684.30\" 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 680.3)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-680.3 200,-680.3 200,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"98\" y=\"-659\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut1.aut2</text>\n",
+       "<g id=\"clust1\" class=\"cluster\">\n",
+       "<title>cluster_0</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-8 8,-201.8 114,-201.8 114,-8 8,-8\"/>\n",
+       "</g>\n",
+       "<g id=\"clust2\" class=\"cluster\">\n",
+       "<title>cluster_1</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"125,-160.2 125,-197.8 188,-197.8 188,-160.2 125,-160.2\"/>\n",
+       "</g>\n",
+       "<g id=\"clust3\" class=\"cluster\">\n",
+       "<title>cluster_2</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"87,-238.3 87,-498.2 170,-498.2 170,-238.3 87,-238.3\"/>\n",
+       "</g>\n",
+       "<g id=\"clust4\" class=\"cluster\">\n",
+       "<title>cluster_3</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"96,-534.7 96,-645.3 166,-645.3 166,-534.7 96,-534.7\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"32\" cy=\"-179\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"32\" cy=\"-179\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"32\" y=\"-174.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;8 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>8&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M45.48,-185.87C55.16,-188.1 64.8,-185.81 64.8,-179 64.8,-175.27 61.92,-172.9 57.72,-171.88\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"57.67,-168.38 47.75,-172.09 57.82,-175.38 57.67,-168.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"68.17\" y=\"-173.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"70\" cy=\"-100.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"70\" y=\"-96.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;6 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>8&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M38.27,-165.43C44.21,-153.55 53.21,-135.52 60.11,-121.71\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"63.15,-123.45 64.49,-112.94 56.89,-120.32 63.15,-123.45\"/>\n",
+       "<text text-anchor=\"middle\" x=\"58.38\" y=\"-132.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;6 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>6&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M79.74,-106.52C88.88,-109.43 98.8,-107.56 98.8,-100.9 98.8,-97.26 95.83,-95.05 91.65,-94.27\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"91.67,-90.76 82,-95.09 92.26,-97.73 91.67,-90.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"102.17\" y=\"-95.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46\" cy=\"-26.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46\" y=\"-22.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>6&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M66.76,-90.18C63.24,-79.58 57.49,-62.32 52.94,-48.63\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"56.38,-47.91 49.9,-39.52 49.74,-50.12 56.38,-47.91\"/>\n",
+       "<text text-anchor=\"middle\" x=\"63.38\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M45.06,-37.9C42.91,-60.95 37.59,-118.03 34.44,-151.79\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"30.97,-151.33 33.53,-161.61 37.94,-151.98 30.97,-151.33\"/>\n",
+       "<text text-anchor=\"middle\" x=\"43.38\" y=\"-95.85\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;7 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>7&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M55.74,-32.42C64.88,-35.33 74.8,-33.46 74.8,-26.8 74.8,-23.16 71.83,-20.95 67.65,-20.17\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"67.67,-16.66 58,-20.99 68.26,-23.63 67.67,-16.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.17\" y=\"-21.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"144\" cy=\"-179\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"144\" y=\"-174.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M141.17,-168.46C137.64,-157.91 130.73,-140.94 120,-129.7 111.99,-121.32 100.9,-114.8 91.19,-110.19\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"92.63,-107 82.06,-106.27 89.87,-113.43 92.63,-107\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.38\" y=\"-132.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;5 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>5&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M153.44,-185.12C162.66,-188.5 172.8,-186.46 172.8,-179 172.8,-174.92 169.77,-172.46 165.51,-171.63\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"165.28,-168.13 155.7,-172.65 166.01,-175.1 165.28,-168.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"176.18\" y=\"-173.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"122\" cy=\"-479.4\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"122\" y=\"-475.13\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M131.74,-485.02C140.88,-487.93 150.8,-486.06 150.8,-479.4 150.8,-475.76 147.83,-473.55 143.65,-472.77\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"143.67,-469.26 134,-473.59 144.26,-476.23 143.67,-469.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"154.18\" y=\"-474.35\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"106\" cy=\"-405.3\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"106\" y=\"-401.03\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M119.78,-468.37C117.46,-457.94 113.76,-441.26 110.78,-427.82\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"114.28,-427.46 108.7,-418.46 107.45,-428.98 114.28,-427.46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"118.38\" y=\"-437.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M115.74,-410.92C124.88,-413.83 134.8,-411.96 134.8,-405.3 134.8,-401.66 131.83,-399.45 127.65,-398.67\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"127.67,-395.16 118,-399.49 128.26,-402.13 127.67,-395.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"138.18\" y=\"-400.25\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"106\" cy=\"-331.2\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"106\" y=\"-326.93\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M106,-394.27C106,-383.94 106,-367.51 106,-354.14\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"109.5,-354.41 106,-344.41 102.5,-354.41 109.5,-354.41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"109.38\" y=\"-363.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M115.74,-336.82C124.88,-339.73 134.8,-337.86 134.8,-331.2 134.8,-327.56 131.83,-325.35 127.65,-324.57\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"127.67,-321.06 118,-325.39 128.26,-328.03 127.67,-321.06\"/>\n",
+       "<text text-anchor=\"middle\" x=\"138.18\" y=\"-326.15\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"125\" cy=\"-257.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"125\" y=\"-252.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M108.56,-320.48C111.33,-309.99 115.81,-292.97 119.4,-279.35\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"122.74,-280.43 121.9,-269.87 115.97,-278.64 122.74,-280.43\"/>\n",
+       "<text text-anchor=\"middle\" x=\"120.38\" y=\"-289.1\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M121.56,-246.45C112.8,-221.9 89.5,-156.58 77.45,-122.8\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"80.86,-121.92 74.2,-113.68 74.26,-124.28 80.86,-121.92\"/>\n",
+       "<text text-anchor=\"middle\" x=\"107.38\" y=\"-173.95\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;5 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>4&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M127.48,-246.15C130.32,-234.81 135.03,-215.94 138.69,-201.25\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"142,-202.46 141.03,-191.91 135.21,-200.77 142,-202.46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"138.38\" y=\"-215\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;1 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>4&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M130.06,-267.03C136.42,-278.81 146.99,-300.4 151,-320.4 159.35,-362.1 160.19,-374.57 151,-416.1 147.6,-431.48 139.99,-447.56 133.43,-459.53\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"130.51,-457.58 128.53,-467.99 136.57,-461.09 130.51,-457.58\"/>\n",
+       "<text text-anchor=\"middle\" x=\"160.38\" y=\"-363.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M134.74,-262.72C143.88,-265.63 153.8,-263.76 153.8,-257.1 153.8,-253.46 150.83,-251.25 146.65,-250.47\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"146.67,-246.96 137,-251.29 147.26,-253.93 146.67,-246.96\"/>\n",
+       "<text text-anchor=\"middle\" x=\"157.18\" y=\"-252.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"green\" stroke=\"green\" stroke-width=\"1.5\" cx=\"122\" cy=\"-553.5\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"122\" y=\"-549.23\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M128.64,-601.54C127.55,-593.88 126.26,-584.7 125.1,-576.49\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"128.58,-576.06 123.71,-566.65 121.64,-577.04 128.58,-576.06\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" d=\"M122,-542.47C122,-532.14 122,-515.71 122,-502.34\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"125.5,-502.61 122,-492.61 118.5,-502.61 125.5,-502.61\"/>\n",
+       "<text text-anchor=\"middle\" x=\"125.38\" y=\"-511.4\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"grey\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M132.04,-558.02C141.1,-560.21 150.8,-558.71 150.8,-553.5 150.8,-550.73 148.06,-549.01 144.14,-548.34\"/>\n",
+       "<polygon fill=\"grey\" stroke=\"grey\" stroke-width=\"1.5\" points=\"144.1,-544.83 134.3,-548.86 144.48,-551.82 144.1,-544.83\"/>\n",
+       "<text text-anchor=\"middle\" x=\"154.18\" y=\"-548.45\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "e_h = [\n",
+    "    (lambda aut, edge: edge.symbol == 1, {'color': 'grey'}),\n",
+    "    (lambda aut, edge: edge.symbol == 0, {'style': 'dashed', 'color': 'grey'})\n",
+    "]\n",
+    "n_h = [\n",
+    "    (lambda aut, state: state in aut.final_states, {'color': 'red', 'fillcolor': 'red'}),\n",
+    "    (lambda aut, state: state in aut.initial_states, {'color': 'green', 'fillcolor': 'green'}),\n",
+    "]\n",
+    "libmata.plotting.plot(lhs, rhs, result, with_scc=True, node_highlight=n_h, edge_highlight=e_h)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "dccb8027-97a8-4e0d-b02b-19238d8648b1",
+   "metadata": {},
+   "source": [
+    "## Example of a Heatmap"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 45,
+   "id": "07df7d90-13f4-41c5-8bf9-ea4cea33c333",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"94pt\" height=\"726pt\"\n",
+       " viewBox=\"0.00 0.00 94.35 726.40\" 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 722.4)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-722.4 90.35,-722.4 90.35,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"43.17\" y=\"-701.1\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">aut1.aut2</text>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#0000ff\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-611.6\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-607.33\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M46.8,-659.64C46.8,-652.07 46.8,-643.03 46.8,-634.9\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.3,-635.14 46.8,-625.14 43.3,-635.14 50.3,-635.14\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.84,-616.12C65.9,-618.31 75.6,-616.81 75.6,-611.6 75.6,-608.83 72.86,-607.11 68.94,-606.44\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"68.9,-602.93 59.1,-606.96 69.28,-609.92 68.9,-602.93\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-606.55\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#0049b6\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-537.5\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-533.23\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M46.8,-600.57C46.8,-590.24 46.8,-573.81 46.8,-560.44\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"50.3,-560.71 46.8,-550.71 43.3,-560.71 50.3,-560.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"50.17\" y=\"-569.5\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-543.12C65.68,-546.03 75.6,-544.16 75.6,-537.5 75.6,-533.86 72.63,-531.65 68.45,-530.87\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"68.47,-527.36 58.8,-531.69 69.06,-534.33 68.47,-527.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-532.45\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#00926d\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"14.8\" cy=\"-463.4\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"14.8\" y=\"-459.13\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M42.62,-527.07C37.85,-516.33 29.91,-498.45 23.74,-484.53\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"27.06,-483.4 19.8,-475.68 20.66,-486.24 27.06,-483.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.17\" y=\"-495.4\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M24.54,-469.02C33.68,-471.93 43.6,-470.06 43.6,-463.4 43.6,-459.76 40.63,-457.55 36.45,-456.77\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"36.47,-453.26 26.8,-457.59 37.06,-460.23 36.47,-453.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.97\" y=\"-458.35\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"#00db24\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"14.8\" cy=\"-389.3\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"14.8\" y=\"-385.03\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M14.8,-452.37C14.8,-442.04 14.8,-425.61 14.8,-412.24\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"18.3,-412.51 14.8,-402.51 11.3,-412.51 18.3,-412.51\"/>\n",
+       "<text text-anchor=\"middle\" x=\"18.17\" y=\"-421.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M24.54,-394.92C33.68,-397.83 43.6,-395.96 43.6,-389.3 43.6,-385.66 40.63,-383.45 36.45,-382.67\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"36.47,-379.16 26.8,-383.49 37.06,-386.13 36.47,-379.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.97\" y=\"-384.25\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"#24db00\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-315.2\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-310.93\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M18.98,-378.87C23.75,-368.13 31.69,-350.25 37.86,-336.33\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"40.94,-338.04 41.8,-327.48 34.54,-335.2 40.94,-338.04\"/>\n",
+       "<text text-anchor=\"middle\" x=\"37.17\" y=\"-347.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;1 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>4&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M49.45,-325.82C52.65,-337.97 57.85,-359.6 59.8,-378.5 64.17,-420.81 64.17,-431.89 59.8,-474.2 58.38,-487.93 55.25,-503.11 52.42,-515.04\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"49.04,-514.13 50,-524.68 55.83,-515.83 49.04,-514.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"67.17\" y=\"-421.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-320.82C65.68,-323.73 75.6,-321.86 75.6,-315.2 75.6,-311.56 72.63,-309.35 68.45,-308.57\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"68.47,-305.06 58.8,-309.39 69.06,-312.03 68.47,-305.06\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-310.15\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<ellipse fill=\"#6d9200\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-241.1\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-236.83\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;5 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>4&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M42.24,-305.07C36.86,-294.29 27.76,-276.06 20.73,-261.98\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"24.05,-260.8 16.45,-253.42 17.79,-263.93 24.05,-260.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-273.1\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"#6d9200\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-167\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-162.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M48.71,-304.11C50.94,-291.82 54.47,-270.43 55.8,-251.9 57.32,-230.8 54.26,-206.81 51.3,-189.9\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"54.78,-189.45 49.47,-180.28 47.91,-190.76 54.78,-189.45\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60.17\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;5 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>5&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-246.72C29.68,-249.63 39.6,-247.76 39.6,-241.1 39.6,-237.46 36.63,-235.25 32.45,-234.47\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"32.47,-230.96 22.8,-235.29 33.06,-237.93 32.47,-230.96\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-236.05\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M15.36,-230.97C20.74,-220.19 29.84,-201.96 36.87,-187.88\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"39.81,-189.83 41.15,-179.32 33.55,-186.7 39.81,-189.83\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-199\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;6 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>6&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M56.54,-172.62C65.68,-175.53 75.6,-173.66 75.6,-167 75.6,-163.36 72.63,-161.15 68.45,-160.37\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"68.47,-156.86 58.8,-161.19 69.06,-163.83 68.47,-156.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"78.97\" y=\"-161.95\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"#b64900\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"10.8\" cy=\"-92.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"10.8\" y=\"-88.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>6&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M42.24,-156.87C36.86,-146.09 27.76,-127.86 20.73,-113.78\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"24.05,-112.6 16.45,-105.22 17.79,-115.73 24.05,-112.6\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.17\" y=\"-124.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;7 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>7&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M20.54,-98.52C29.68,-101.43 39.6,-99.56 39.6,-92.9 39.6,-89.26 36.63,-87.05 32.45,-86.27\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"32.47,-82.76 22.8,-87.09 33.06,-89.73 32.47,-82.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"42.97\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"#ff0000\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"46.8\" cy=\"-14.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"46.8\" y=\"-10.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M15.21,-82.57C20.25,-71.92 28.68,-54.1 35.57,-39.55\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"38.58,-41.36 39.69,-30.83 32.25,-38.37 38.58,-41.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"35.17\" y=\"-50.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;6 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>8&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"gray\" stroke-width=\"1.5\" d=\"M49.74,-29.78C53.03,-47.11 57.68,-77.54 55.8,-103.7 54.83,-117.16 52.7,-132.14 50.76,-144.03\"/>\n",
+       "<polygon fill=\"gray\" stroke=\"gray\" stroke-width=\"1.5\" points=\"47.35,-143.22 49.1,-153.67 54.25,-144.41 47.35,-143.22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60.17\" y=\"-87.85\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;8 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>8&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M60.28,-21.67C69.96,-23.9 79.6,-21.61 79.6,-14.8 79.6,-11.07 76.72,-8.7 72.52,-7.68\"/>\n",
+       "<polygon fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" points=\"72.47,-4.18 62.55,-7.89 72.62,-11.18 72.47,-4.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"82.97\" y=\"-9.75\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "heat_map = distance_from(result)\n",
+    "max_heat = max(heat_map.values())\n",
+    "e_h = [\n",
+    "    (lambda aut, edge: edge.symbol == 1, {'color': 'gray'}),\n",
+    "    (lambda aut, edge: edge.source == edge.target, {'style': 'dashed', 'color': 'red'})\n",
+    "]\n",
+    "n_h = [\n",
+    "    (lambda aut, state, j=i: state == j, libmata.plotting.Style.filled(hexa_heat(0, max_heat, heat_map[i]))) for i in range(0,result.num_of_states())\n",
+    "]\n",
+    "libmata.plotting.plot(result, node_highlight=n_h, edge_highlight=e_h)"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.10.13"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

From 4eee12095d0a51a32c071f0ca01d8bd0c643c901 Mon Sep 17 00:00:00 2001
From: vhavlena <vohavlena@gmail.com>
Date: Wed, 11 Oct 2023 15:16:34 +0200
Subject: [PATCH 2/3] visualisation: aut from regex

---
 .../notebooks/example-04-visualization.ipynb  | 215 +++++++++++++++++-
 1 file changed, 209 insertions(+), 6 deletions(-)

diff --git a/examples/notebooks/example-04-visualization.ipynb b/examples/notebooks/example-04-visualization.ipynb
index 7470ca893..fe0a4d77d 100644
--- a/examples/notebooks/example-04-visualization.ipynb
+++ b/examples/notebooks/example-04-visualization.ipynb
@@ -9,13 +9,13 @@
    "source": [
     "import libmata as mata\n",
     "from libmata.nfa.nfa import *\n",
+    "from libmata.parser import *\n",
     "import libmata.plotting\n",
     "\n",
-    "import matplotlib.pyplot as plt\n",
-    "import networkx as nx\n",
-    "import graphviz\n",
-    "import IPython\n",
-    "from  matplotlib.colors import LinearSegmentedColormap"
+    "# import matplotlib.pyplot as plt\n",
+    "#import networkx as nx\n",
+    "#import graphviz\n",
+    "#import IPython"
    ]
   },
   {
@@ -1102,7 +1102,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 45,
+   "execution_count": 43,
    "id": "07df7d90-13f4-41c5-8bf9-ea4cea33c333",
    "metadata": {},
    "outputs": [
@@ -1350,6 +1350,209 @@
     "]\n",
     "libmata.plotting.plot(result, node_highlight=n_h, edge_highlight=e_h)"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "22a0477d-b02c-4c02-8629-bb415e8e685e",
+   "metadata": {},
+   "source": [
+    "## Regex Example"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b1710914-765b-418b-aa8b-27ae3b1f140d",
+   "metadata": {},
+   "source": [
+    "Setting a correct alphabet"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 44,
+   "id": "f6d84372-0dd4-4646-b331-00fc80e43f86",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "libmata.plotting.store()['alphabet'] = mata.alphabets.OnTheFlyAlphabet.from_symbol_map({\"a\":97, \"b\":98})"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d571e4e3-7685-4ac3-aba0-5b413a88efa4",
+   "metadata": {},
+   "source": [
+    "Plot the automaton"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 47,
+   "id": "3a6ababe-3d20-4ebd-8f0d-b9fe44786f7c",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?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 9.0.0 (20230911.1827)\n",
+       " -->\n",
+       "<!-- Title: dot Pages: 1 -->\n",
+       "<svg width=\"207pt\" height=\"291pt\"\n",
+       " viewBox=\"0.00 0.00 207.00 290.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 286.8)\">\n",
+       "<title>dot</title>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-286.8 203,-286.8 203,4 -4,4\"/>\n",
+       "<g id=\"clust1\" class=\"cluster\">\n",
+       "<title>cluster_0</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"120,-8 120,-53.6 191,-53.6 191,-8 120,-8\"/>\n",
+       "</g>\n",
+       "<g id=\"clust2\" class=\"cluster\">\n",
+       "<title>cluster_1</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"122,-90.1 122,-127.7 160,-127.7 160,-90.1 122,-90.1\"/>\n",
+       "</g>\n",
+       "<g id=\"clust3\" class=\"cluster\">\n",
+       "<title>cluster_2</title>\n",
+       "<polygon fill=\"lightgray\" stroke=\"black\" points=\"8,-12 8,-274.8 112,-274.8 112,-12 8,-12\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"red\" stroke=\"red\" stroke-width=\"1.5\" cx=\"143\" cy=\"-30.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" stroke-width=\"1.5\" cx=\"143\" cy=\"-30.8\" rx=\"14.8\" ry=\"14.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"143\" y=\"-26.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;4 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" d=\"M156.48,-37.67C166.16,-39.9 175.8,-37.61 175.8,-30.8 175.8,-27.07 172.92,-24.7 168.72,-23.68\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"168.67,-20.18 158.75,-23.89 168.82,-27.18 168.67,-20.18\"/>\n",
+       "<text text-anchor=\"start\" x=\"175.8\" y=\"-25.75\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"141\" cy=\"-108.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"141\" y=\"-104.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M141.27,-97.64C141.53,-87.55 141.95,-71.74 142.31,-58.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"145.8,-58.4 142.57,-48.31 138.8,-58.22 145.8,-58.4\"/>\n",
+       "<text text-anchor=\"start\" x=\"142\" y=\"-66.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- q0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>q0</title>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"orange\" stroke=\"orange\" stroke-width=\"1.5\" cx=\"69\" cy=\"-183\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"69\" y=\"-178.72\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
+       "</g>\n",
+       "<!-- q0&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>q0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M69,-231.04C69,-223.47 69,-214.43 69,-206.3\"/>\n",
+       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"72.5,-206.54 69,-196.54 65.5,-206.54 72.5,-206.54\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M77.45,-175.76C84.55,-170.36 94.82,-162.19 103,-154.2 111.46,-145.94 120.11,-136 127.01,-127.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"129.7,-129.87 133.25,-119.89 124.25,-125.48 129.7,-129.87\"/>\n",
+       "<text text-anchor=\"start\" x=\"118\" y=\"-140.9\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M79.04,-187.52C88.1,-189.71 97.8,-188.21 97.8,-183 97.8,-180.23 95.06,-178.51 91.14,-177.84\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"91.1,-174.33 81.3,-178.36 91.48,-181.32 91.1,-174.33\"/>\n",
+       "<text text-anchor=\"start\" x=\"97.8\" y=\"-177.95\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-108.9\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-104.62\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M63.85,-173.16C57.49,-162.24 46.49,-143.36 38.16,-129.06\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"41.39,-127.65 33.33,-120.77 35.34,-131.18 41.39,-127.65\"/>\n",
+       "<text text-anchor=\"start\" x=\"52\" y=\"-140.9\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M36.74,-114.52C45.88,-117.43 55.8,-115.56 55.8,-108.9 55.8,-105.26 52.83,-103.05 48.65,-102.27\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"48.67,-98.76 39,-103.09 49.26,-105.73 48.67,-98.76\"/>\n",
+       "<text text-anchor=\"start\" x=\"55.8\" y=\"-103.85\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"64\" cy=\"-30.8\" rx=\"10.8\" ry=\"10.8\"/>\n",
+       "<text text-anchor=\"middle\" x=\"64\" y=\"-26.52\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" d=\"M27.95,-97.94C29.14,-88.66 31.75,-74.62 37.25,-63.6 40.08,-57.93 44.12,-52.4 48.21,-47.59\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"50.49,-50.28 54.74,-40.57 45.37,-45.51 50.49,-50.28\"/>\n",
+       "<text text-anchor=\"start\" x=\"38\" y=\"-66.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M65.55,-41.67C67.28,-53.24 69.98,-73 71,-90.1 72,-106.78 71.31,-110.99 71,-127.7 70.8,-138.33 70.39,-150.13 69.99,-160.01\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"66.51,-159.59 69.58,-169.73 73.5,-159.89 66.51,-159.59\"/>\n",
+       "<text text-anchor=\"start\" x=\"71\" y=\"-103.85\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;1 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>2&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-width=\"1.5\" stroke-dasharray=\"5,2\" d=\"M59.97,-41.15C55.69,-50.94 48.64,-66.73 42,-80.1 40.64,-82.84 39.16,-85.7 37.68,-88.5\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" stroke-width=\"1.5\" points=\"34.65,-86.76 32.96,-97.22 40.8,-90.09 34.65,-86.76\"/>\n",
+       "<text text-anchor=\"start\" x=\"50\" y=\"-66.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "reg_aut = from_regex(\"((a+b)*a)*aab*\")\n",
+    "e_h = [\n",
+    "    (lambda aut, edge: edge.symbol == 98, {'color': 'black'}),\n",
+    "    (lambda aut, edge: edge.symbol == 97, {'style': 'dashed', 'color': 'black'})\n",
+    "]\n",
+    "n_h = [\n",
+    "    (lambda aut, state: state in aut.final_states, {'color': 'red', 'fillcolor': 'red'}),\n",
+    "    (lambda aut, state: state in aut.initial_states, {'color': 'orange', 'fillcolor': 'orange'}),\n",
+    "]\n",
+    "libmata.plotting.plot(reg_aut, with_scc=True, node_highlight=n_h, edge_highlight=e_h)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "7b9c56d6-578b-4375-b92b-b39077b86b91",
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {

From c721e11362e86585ca9ba4b197099895521a3273 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20Chocholat=C3=BD?= <chocholaty.david@protonmail.com>
Date: Sat, 14 Oct 2023 12:51:22 +0200
Subject: [PATCH 3/3] Remove commented out code

---
 examples/notebooks/example-04-visualization.ipynb | 15 +--------------
 1 file changed, 1 insertion(+), 14 deletions(-)

diff --git a/examples/notebooks/example-04-visualization.ipynb b/examples/notebooks/example-04-visualization.ipynb
index fe0a4d77d..4b95d14f3 100644
--- a/examples/notebooks/example-04-visualization.ipynb
+++ b/examples/notebooks/example-04-visualization.ipynb
@@ -10,12 +10,7 @@
     "import libmata as mata\n",
     "from libmata.nfa.nfa import *\n",
     "from libmata.parser import *\n",
-    "import libmata.plotting\n",
-    "\n",
-    "# import matplotlib.pyplot as plt\n",
-    "#import networkx as nx\n",
-    "#import graphviz\n",
-    "#import IPython"
+    "import libmata.plotting"
    ]
   },
   {
@@ -1545,14 +1540,6 @@
     "]\n",
     "libmata.plotting.plot(reg_aut, with_scc=True, node_highlight=n_h, edge_highlight=e_h)"
    ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "7b9c56d6-578b-4375-b92b-b39077b86b91",
-   "metadata": {},
-   "outputs": [],
-   "source": []
   }
  ],
  "metadata": {