{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Formulas & Automata generators\n",
    "\n",
    "The `spot.gen` package contains the functions used to generate the patterns produced by [`genltl`](https://spot.lrde.epita.fr/genltl.html) and [`genaut`](https://spot.lrde.epita.fr/genaut.html)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import spot\n",
    "import spot.gen as sg\n",
    "spot.setup()\n",
    "from IPython.display import display"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## LTL patterns\n",
    "\n",
    "Generation of LTL formulas is done via the `ltl_pattern()` function.  This takes two arguments: a pattern id, and a pattern size (or index if the id refers to a list)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3}$"
      ],
      "text/plain": [
       "GFp1 & GFp2 & GFp3"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sg.ltl_pattern(sg.LTL_AND_GF, 3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} (p \\land \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} p) \\land \\mathsf{F} (q \\land \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} q)$"
      ],
      "text/plain": [
       "F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sg.ltl_pattern(sg.LTL_CCJ_BETA_PRIME, 4)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see the list of supported patterns, the easiest way is to look at the `--help` output of `genltl`.  The above pattern for instance is attached to option `--ccj-beta-prime`.  The name of the pattern identifier is the same using capital letters, underscores, and an `LTL_` prefix.  If a pattern has multiple aliased options in `genltl`, the first one used for the identifier (e.g., `genltl` accept both `--dac-patterns` and `--spec-patterns` as synonyms to denote the patterns of `spot.gen.LTL_DAC_PATTERNS`).\n",
    "\n",
    "Multiple patterns can be generated using the `ltl_patterns()` function.  It's arguments should be either can be:\n",
    "  - pairs of the form `(id, n)`: in this case the pattern `id` with size/index `n` is returned,\n",
    "  - triplets of the form `(id, min, max)`: in this case the patterns are output for all `n` between `min` and `max` included,\n",
    "  - an integer `id`: then this is equivalent to `(id, 1, 10)` if the pattern has now upper bound, or `(id, 1, upper)` if the patter `id` has an upper bound `upper`.  This is mostly used when the pattern id correspond to a hard-coded list of formulas.\n",
    "\n",
    "Here is an example showing these three types of arguments:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$(\\mathsf{G} \\mathsf{F} p_{1} \\lor \\mathsf{F} \\mathsf{G} p_{2}) \\land (\\mathsf{G} \\mathsf{F} p_{2} \\lor \\mathsf{F} \\mathsf{G} p_{3}) \\land (\\mathsf{G} \\mathsf{F} p_{3} \\lor \\mathsf{F} \\mathsf{G} p_{4})$"
      ],
      "text/plain": [
       "(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} \\mathsf{G} p_{1}$"
      ],
      "text/plain": [
       "FGp1"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2}$"
      ],
      "text/plain": [
       "FGp1 & FGp2"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2} \\land \\mathsf{F} \\mathsf{G} p_{3}$"
      ],
      "text/plain": [
       "FGp1 & FGp2 & FGp3"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{G} p_{2})$"
      ],
      "text/plain": [
       "p0 U (p1 & Gp2)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\mathbin{\\mathsf{U}} p_{3}))$"
      ],
      "text/plain": [
       "p0 U (p1 & X(p2 U p3))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\land \\mathsf{F} (p_{3} \\land \\mathsf{X} \\mathsf{F} (p_{4} \\land \\mathsf{X} \\mathsf{F} (p_{5} \\land \\mathsf{X} \\mathsf{F} p_{6})))))$"
      ],
      "text/plain": [
       "p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} (p_{0} \\land \\mathsf{X} \\mathsf{G} p_{1})$"
      ],
      "text/plain": [
       "F(p0 & XGp1)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\land \\mathsf{X} \\mathsf{F} p_{2}))$"
      ],
      "text/plain": [
       "F(p0 & X(p1 & XFp2))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
      ],
      "text/plain": [
       "F(p0 & X(p1 U p2))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} p_{0} \\lor \\mathsf{F} \\mathsf{G} p_{1}$"
      ],
      "text/plain": [
       "GFp0 | FGp1"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
      ],
      "text/plain": [
       "G(p0 -> (p1 U p2))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} (p_{0} \\land \\mathsf{X} \\mathsf{F} (p_{1} \\land \\mathsf{X} \\mathsf{F} (p_{2} \\land \\mathsf{X} \\mathsf{F} p_{3})))$"
      ],
      "text/plain": [
       "G(p0 & XF(p1 & XF(p2 & XFp3)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3} \\land \\mathsf{G} \\mathsf{F} p_{0} \\land \\mathsf{G} \\mathsf{F} p_{4}$"
      ],
      "text/plain": [
       "GFp1 & GFp2 & GFp3 & GFp0 & GFp4"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$(p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\mathbin{\\mathsf{U}} p_{2})) \\lor (p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{U}} p_{0})) \\lor (p_{2} \\mathbin{\\mathsf{U}} (p_{0} \\mathbin{\\mathsf{U}} p_{1}))$"
      ],
      "text/plain": [
       "(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} (\\mathsf{G} p_{2} \\lor \\mathsf{G} p_{3})))$"
      ],
      "text/plain": [
       "G(p0 -> (p1 U (Gp2 | Gp3)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "for f in sg.ltl_patterns((sg.LTL_GH_R, 3), (sg.LTL_AND_FG, 1, 3), sg.LTL_EH_PATTERNS):\n",
    "    display(f)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Some LTL patterns take two arguments.  In this case, the arguments passed to `ltl_pattern()` should be one of:\n",
    "- `(id, n, m)` giving the value of both arguments,\n",
    "- `(id, min1, max1, min2, max2)` specifying a range for both arguments,\n",
    "- `(id, n)` equivalent to `(id, n, n)`,\n",
    "- `id` equivalent to `(id, 1, 3, 1, 3)`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$"
      ],
      "text/plain": [
       "GFa1 U G(GFa0 U Xb)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$"
      ],
      "text/plain": [
       "GFa1 U G(GFa0 U XXb)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)$"
      ],
      "text/plain": [
       "GFa1 U G(GFa0 U XXXb)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U Xb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U XXb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U XXXb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)))$"
      ],
      "text/plain": [
       "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U Xb)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)))$"
      ],
      "text/plain": [
       "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXb)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)))$"
      ],
      "text/plain": [
       "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXXb)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "for f in sg.ltl_patterns(sg.LTL_SEJK_F):\n",
    "    display(f)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U XXXb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U XXb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$"
      ],
      "text/plain": [
       "GFa1 U G(GFa0 U Xb)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$"
      ],
      "text/plain": [
       "GFa1 U G(GFa0 U XXb)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U Xb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/latex": [
       "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
      ],
      "text/plain": [
       "GFa2 U G(GFa1 U G(GFa0 U XXb))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "for f in sg.ltl_patterns((sg.LTL_SEJK_F, 2, 3), (sg.LTL_SEJK_F, 2), (sg.LTL_SEJK_F, 1, 2, 1, 2)):\n",
    "    display(f)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Automata patterns\n",
    "\n",
    "We currently have only a couple of generators of automata:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<svg height=\"311pt\" viewBox=\"0.00 0.00 734.00 310.64\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g class=\"graph\" id=\"graph0\" transform=\"scale(.9062 .9062) rotate(0) translate(4 338.8)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-338.8 806,-338.8 806,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368.5\" y=\"-304.6\">[co-Büchi]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"60\" cy=\"-127\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<ellipse cx=\"60\" cy=\"-127\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-123.3\">0</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g class=\"edge\" id=\"edge1\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.1682,-127C4.2491,-127 17.4946,-127 30.6388,-127\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"37.8655,-127 30.8656,-130.1501 34.3655,-127 30.8655,-127.0001 30.8655,-127.0001 30.8655,-127.0001 34.3655,-127 30.8655,-123.8501 37.8655,-127 37.8655,-127\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g class=\"node\" id=\"node3\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"177\" cy=\"-244\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"177\" y=\"-240.3\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge2\">\n",
       "<title>0-&gt;1</title>\n",
       "<path d=\"M63.6171,-149.0457C68.3054,-170.6455 78.5739,-203.0065 100,-222 114.2547,-234.6363 135.3079,-240.0484 151.7989,-242.3495\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"159.014,-243.2026 151.6925,-245.5087 155.5382,-242.7916 152.0624,-242.3805 152.0624,-242.3805 152.0624,-242.3805 155.5382,-242.7916 152.4324,-239.2523 159.014,-243.2026 159.014,-243.2026\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.5\" y=\"-243.8\">1</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g class=\"node\" id=\"node4\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"348\" cy=\"-188\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"348\" y=\"-184.3\">2</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge3\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M80.5768,-134.8623C86.7616,-137.0455 93.6042,-139.285 100,-141 180.3896,-162.5563 278.0005,-177.9969 323.0318,-184.5314\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"330.0516,-185.5394 322.6749,-187.6624 326.5871,-185.0419 323.1227,-184.5443 323.1227,-184.5443 323.1227,-184.5443 326.5871,-185.0419 323.5704,-181.4263 330.0516,-185.5394 330.0516,-185.5394\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"177\" y=\"-165.8\">1</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g class=\"node\" id=\"node5\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"457\" cy=\"-135\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-131.3\">3</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge4\">\n",
       "<title>0-&gt;3</title>\n",
       "<path d=\"M82.1951,-127.4473C150.7303,-128.8283 358.7626,-133.0204 431.5353,-134.4869\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"438.9382,-134.636 431.8761,-137.6443 435.4389,-134.5655 431.9396,-134.4949 431.9396,-134.4949 431.9396,-134.4949 435.4389,-134.5655 432.0031,-131.3456 438.9382,-134.636 438.9382,-134.636\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"262.5\" y=\"-135.8\">1</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g class=\"node\" id=\"node6\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"566\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"566\" y=\"-85.3\">4</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge5\">\n",
       "<title>0-&gt;4</title>\n",
       "<path d=\"M79.6587,-116.4149C102.4112,-105.171 141.3338,-89 177,-89 177,-89 177,-89 457,-89 485.7328,-89 518.7261,-89 540.8184,-89\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"547.8708,-89 540.8708,-92.1501 544.3708,-89 540.8708,-89.0001 540.8708,-89.0001 540.8708,-89.0001 544.3708,-89 540.8707,-85.8501 547.8708,-89 547.8708,-89\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"348\" y=\"-92.8\">1</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g class=\"node\" id=\"node7\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"675\" cy=\"-67\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"675\" y=\"-63.3\">5</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;5 -->\n",
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>0-&gt;5</title>\n",
       "<path d=\"M72.9119,-109.1858C92.4324,-84.5283 131.9902,-43 177,-43 177,-43 177,-43 566,-43 595.8987,-43 629.3541,-51.719 651.2168,-58.6465\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"657.8885,-60.8194 650.2571,-61.6467 654.5606,-59.7355 651.2326,-58.6516 651.2326,-58.6516 651.2326,-58.6516 654.5606,-59.7355 652.2081,-55.6564 657.8885,-60.8194 657.8885,-60.8194\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"402.5\" y=\"-46.8\">1</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g class=\"node\" id=\"node8\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"784\" cy=\"-67\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"784\" y=\"-63.3\">6</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge7\">\n",
       "<title>0-&gt;6</title>\n",
       "<path d=\"M67.0184,-105.9904C73.5237,-88.8889 84.5373,-64.8994 100,-48 127.2228,-18.2478 136.6729,0 177,0 177,0 177,0 675,0 712.1109,0 747.2075,-28.536 767.1131,-48.3618\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"772.0762,-53.4416 764.9311,-50.636 769.6302,-50.9381 767.1842,-48.4346 767.1842,-48.4346 767.1842,-48.4346 769.6302,-50.9381 769.4374,-46.2332 772.0762,-53.4416 772.0762,-53.4416\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-3.8\">1</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g class=\"edge\" id=\"edge8\">\n",
       "<title>1-&gt;0</title>\n",
       "<path d=\"M166.2826,-228.946C159.7101,-220.5113 150.7101,-210.2613 141,-203 124.9161,-190.9723 115.4071,-196.8833 100,-184 89.6889,-175.3779 80.7894,-163.494 74.0203,-152.8077\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"70.2863,-146.6878 76.6213,-151.0227 72.1093,-149.6756 73.9323,-152.6634 73.9323,-152.6634 73.9323,-152.6634 72.1093,-149.6756 71.2433,-154.304 70.2863,-146.6878 70.2863,-146.6878\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-206.8\">!a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge9\">\n",
       "<title>1-&gt;1</title>\n",
       "<path d=\"M167.4254,-259.5414C164.7303,-269.9087 167.9219,-280 177,-280 183.9504,-280 187.4503,-274.0847 187.4995,-266.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"186.5746,-259.5414 190.6004,-266.0771 187.0256,-263.0123 187.4767,-266.4831 187.4767,-266.4831 187.4767,-266.4831 187.0256,-263.0123 184.353,-266.889 186.5746,-259.5414 186.5746,-259.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160\" y=\"-283.8\">a &amp; b</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>1-&gt;2</title>\n",
       "<path d=\"M187.6307,-229.0188C194.0507,-221.1519 202.929,-212.1088 213,-207 248.0712,-189.2089 294.4856,-186.5082 322.7454,-186.8039\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"329.8655,-186.9464 322.8038,-189.9556 326.3662,-186.8763 322.8669,-186.8063 322.8669,-186.8063 322.8669,-186.8063 326.3662,-186.8763 322.9299,-183.6569 329.8655,-186.9464 329.8655,-186.9464\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213\" y=\"-210.8\">(!a &amp; b) | (a &amp; !b)</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge11\">\n",
       "<title>2-&gt;1</title>\n",
       "<path d=\"M336.4631,-202.3735C330.0184,-209.4117 321.4017,-217.3514 312,-222 276.6315,-239.4876 230.3057,-243.5425 202.1447,-244.2347\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"195.0511,-244.3469 202.0004,-241.0865 198.5507,-244.2915 202.0503,-244.2361 202.0503,-244.2361 202.0503,-244.2361 198.5507,-244.2915 202.1001,-247.3857 195.0511,-244.3469 195.0511,-244.3469\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244\" y=\"-246.8\">!a &amp; b</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>2-&gt;2</title>\n",
       "<path d=\"M338.7674,-203.5414C336.1685,-213.9087 339.2461,-224 348,-224 354.7022,-224 358.077,-218.0847 358.1245,-210.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"357.2326,-203.5414 361.2286,-210.0955 357.6678,-207.0143 358.103,-210.4871 358.103,-210.4871 358.103,-210.4871 357.6678,-207.0143 354.9775,-210.8788 357.2326,-203.5414 357.2326,-203.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"298.5\" y=\"-227.8\">(!a &amp; !b) | (a &amp; b)</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>2-&gt;3</title>\n",
       "<path d=\"M364.5548,-179.9504C383.1486,-170.9094 413.4408,-156.1802 434.2503,-146.0618\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"440.6466,-142.9517 435.7288,-148.8456 437.499,-144.4822 434.3513,-146.0127 434.3513,-146.0127 434.3513,-146.0127 437.499,-144.4822 432.9739,-143.1798 440.6466,-142.9517 440.6466,-142.9517\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384\" y=\"-172.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge14\">\n",
       "<title>3-&gt;3</title>\n",
       "<path d=\"M447.7674,-150.5414C445.1685,-160.9087 448.2461,-171 457,-171 463.7022,-171 467.077,-165.0847 467.1245,-157.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"466.2326,-150.5414 470.2286,-157.0955 466.6678,-154.0143 467.103,-157.4871 467.103,-157.4871 467.103,-157.4871 466.6678,-154.0143 463.9775,-157.8788 466.2326,-150.5414 466.2326,-150.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"441.5\" y=\"-174.8\">!a | b</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>3-&gt;4</title>\n",
       "<path d=\"M474.0313,-127.8125C492.4289,-120.0483 521.8676,-107.6247 542.4692,-98.9304\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"549.0883,-96.137 543.8639,-101.7609 545.8637,-97.4979 542.6391,-98.8588 542.6391,-98.8588 542.6391,-98.8588 545.8637,-97.4979 541.4143,-95.9566 549.0883,-96.137 549.0883,-96.137\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-121.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge16\">\n",
       "<title>4-&gt;4</title>\n",
       "<path d=\"M556.7674,-104.5414C554.1685,-114.9087 557.2461,-125 566,-125 572.7022,-125 576.077,-119.0847 576.1245,-111.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"575.2326,-104.5414 579.2286,-111.0955 575.6678,-108.0143 576.103,-111.4871 576.103,-111.4871 576.103,-111.4871 575.6678,-108.0143 572.9775,-111.8788 575.2326,-104.5414 575.2326,-104.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"550.5\" y=\"-128.8\">!a | b</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;5 -->\n",
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>4-&gt;5</title>\n",
       "<path d=\"M583.9991,-85.3671C602.0939,-81.715 630.1235,-76.0576 650.2934,-71.9867\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"657.3358,-70.5653 651.0974,-75.038 653.905,-71.2578 650.4742,-71.9502 650.4742,-71.9502 650.4742,-71.9502 653.905,-71.2578 649.8509,-68.8625 657.3358,-70.5653 657.3358,-70.5653\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"602\" y=\"-84.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;5 -->\n",
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>5-&gt;5</title>\n",
       "<path d=\"M665.7674,-82.5414C663.1685,-92.9087 666.2461,-103 675,-103 681.7022,-103 685.077,-97.0847 685.1245,-89.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"684.2326,-82.5414 688.2286,-89.0955 684.6678,-86.0143 685.103,-89.4871 685.103,-89.4871 685.103,-89.4871 684.6678,-86.0143 681.9775,-89.8788 684.2326,-82.5414 684.2326,-82.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"659.5\" y=\"-106.8\">!a | b</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge19\">\n",
       "<title>5-&gt;6</title>\n",
       "<path d=\"M693.4904,-67C711.3712,-67 738.6126,-67 758.5388,-67\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"765.7827,-67 758.7828,-70.1501 762.2827,-67 758.7827,-67.0001 758.7827,-67.0001 758.7827,-67.0001 762.2827,-67 758.7827,-63.8501 765.7827,-67 765.7827,-67\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"711\" y=\"-70.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge20\">\n",
       "<title>6-&gt;1</title>\n",
       "<path d=\"M782.9398,-85.0078C778.9099,-135.3696 760.0892,-274 675,-274 348,-274 348,-274 348,-274 287.6782,-274 271.2823,-275.553 213,-260 208.5766,-258.8196 204.0051,-257.1626 199.6655,-255.3589\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"193.0913,-252.4512 200.7673,-252.4019 196.2922,-253.867 199.4931,-255.2827 199.4931,-255.2827 199.4931,-255.2827 196.2922,-253.867 198.219,-258.1635 193.0913,-252.4512 193.0913,-252.4512\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-277.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge21\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M774.7674,-82.5414C772.1685,-92.9087 775.2461,-103 784,-103 790.7022,-103 794.077,-97.0847 794.1245,-89.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"793.2326,-82.5414 797.2286,-89.0955 793.6678,-86.0143 794.103,-89.4871 794.103,-89.4871 794.103,-89.4871 793.6678,-86.0143 790.9775,-89.8788 793.2326,-82.5414 793.2326,-82.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"768.5\" y=\"-106.8\">!a | b</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/svg+xml": [
       "<svg height=\"272pt\" viewBox=\"0.00 0.00 734.00 272.28\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g class=\"graph\" id=\"graph0\" transform=\"scale(.818 .818) rotate(0) translate(4 328.8701)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-328.8701 893.3369,-328.8701 893.3369,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269.1684\" y=\"-310.6701\">(Fin(</text>\n",
       "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"297.1684\" y=\"-310.6701\">⓿</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.1684\" y=\"-310.6701\">) | Inf(</text>\n",
       "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"350.1684\" y=\"-310.6701\">❶</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.1684\" y=\"-310.6701\">)) &amp; (Fin(</text>\n",
       "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"420.1684\" y=\"-310.6701\">❷</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"436.1684\" y=\"-310.6701\">) | Inf(</text>\n",
       "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"473.1684\" y=\"-310.6701\">❸</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"489.1684\" y=\"-310.6701\">)) &amp; (Fin(</text>\n",
       "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"543.1684\" y=\"-310.6701\">❹</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"559.1684\" y=\"-310.6701\">) | Inf(</text>\n",
       "<text fill=\"#e31a1c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"596.1684\" y=\"-310.6701\">❺</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"612.1684\" y=\"-310.6701\">))</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"412.6684\" y=\"-296.6701\">[Streett 3]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"64.8701\" cy=\"-207.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-211.6701\">0</text>\n",
       "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-196.6701\">⓿</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g class=\"edge\" id=\"edge1\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.2229,-207.8701C4.3751,-207.8701 17.3629,-207.8701 30.7917,-207.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"37.8045,-207.8701 30.8046,-211.0202 34.3045,-207.8701 30.8045,-207.8702 30.8045,-207.8702 30.8045,-207.8702 34.3045,-207.8701 30.8045,-204.7202 37.8045,-207.8701 37.8045,-207.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g class=\"node\" id=\"node3\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"152.7401\" cy=\"-133.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"152.7401\" y=\"-130.1701\">2</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge2\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M85.694,-190.3331C100.0819,-178.2163 119.0923,-162.2066 133.195,-150.33\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"138.9107,-145.5165 135.5856,-152.4351 136.2336,-147.7711 133.5565,-150.0256 133.5565,-150.0256 133.5565,-150.0256 136.2336,-147.7711 131.5273,-147.6162 138.9107,-145.5165 138.9107,-145.5165\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.7401\" y=\"-171.6701\">a</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g class=\"node\" id=\"node6\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"298.6102\" cy=\"-52.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"294.1102\" y=\"-56.6701\">3</text>\n",
       "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"290.6102\" y=\"-41.6701\">❶</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge5\">\n",
       "<title>2-&gt;3</title>\n",
       "<path d=\"M168.6285,-125.0474C192.6185,-111.726 238.5007,-86.2482 268.8318,-69.4057\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"275.0546,-65.9502 270.464,-72.1024 271.9947,-67.6493 268.9348,-69.3485 268.9348,-69.3485 268.9348,-69.3485 271.9947,-67.6493 267.4056,-66.5946 275.0546,-65.9502 275.0546,-65.9502\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.7401\" y=\"-116.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g class=\"node\" id=\"node7\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"235.7401\" cy=\"-133.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"235.7401\" y=\"-130.1701\">6</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;6</title>\n",
       "<path d=\"M170.7499,-133.8701C182.308,-133.8701 197.4908,-133.8701 210.2747,-133.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"217.4789,-133.8701 210.4789,-137.0202 213.9789,-133.8701 210.4789,-133.8702 210.4789,-133.8702 210.4789,-133.8702 213.9789,-133.8701 210.4788,-130.7202 217.4789,-133.8701 217.4789,-133.8701\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.7401\" y=\"-137.6701\">a</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g class=\"node\" id=\"node4\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"590.8567\" cy=\"-119.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"590.8567\" y=\"-116.1701\">1</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g class=\"edge\" id=\"edge3\">\n",
       "<title>1-&gt;0</title>\n",
       "<path d=\"M589.0384,-137.8372C583.8352,-178.4607 565.0126,-273.8701 502.9866,-273.8701 152.7401,-273.8701 152.7401,-273.8701 152.7401,-273.8701 125.594,-273.8701 101.4799,-253.4828 85.4128,-235.3701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"80.6904,-229.8471 87.6337,-233.1203 82.9649,-232.5073 85.2395,-235.1674 85.2395,-235.1674 85.2395,-235.1674 82.9649,-232.5073 82.8454,-237.2145 80.6904,-229.8471 80.6904,-229.8471\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293.1102\" y=\"-277.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g class=\"node\" id=\"node5\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"669.8567\" cy=\"-119.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.8567\" y=\"-116.1701\">5</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;5 -->\n",
       "<g class=\"edge\" id=\"edge4\">\n",
       "<title>1-&gt;5</title>\n",
       "<path d=\"M609.1794,-119.8701C619.6488,-119.8701 632.9361,-119.8701 644.4061,-119.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"651.6333,-119.8701 644.6333,-123.0202 648.1333,-119.8701 644.6333,-119.8702 644.6333,-119.8702 644.6333,-119.8702 648.1333,-119.8701 644.6332,-116.7202 651.6333,-119.8701 651.6333,-119.8701\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"626.8567\" y=\"-123.6701\">a</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g class=\"node\" id=\"node8\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"761.7267\" cy=\"-211.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"757.2267\" y=\"-215.6701\">4</text>\n",
       "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"753.7267\" y=\"-200.6701\">❷</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge9\">\n",
       "<title>5-&gt;4</title>\n",
       "<path d=\"M682.6308,-132.6623C696.7501,-146.8015 719.8196,-169.9037 737.41,-187.519\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"742.6772,-192.7936 735.502,-190.0662 740.2041,-190.317 737.731,-187.8404 737.731,-187.8404 737.731,-187.8404 740.2041,-190.317 739.9599,-185.6145 742.6772,-192.7936 742.6772,-192.7936\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"705.8567\" y=\"-169.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 9 -->\n",
       "<g class=\"node\" id=\"node9\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"761.7267\" cy=\"-100.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"761.7267\" y=\"-97.1701\">9</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>5-&gt;9</title>\n",
       "<path d=\"M687.5701,-116.2067C701.5505,-113.3153 721.2253,-109.2463 736.7963,-106.026\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"744.0676,-104.5222 737.8507,-109.0247 740.6402,-105.2311 737.2127,-105.94 737.2127,-105.94 737.2127,-105.94 740.6402,-105.2311 736.5747,-102.8553 744.0676,-104.5222 744.0676,-104.5222\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"707.8567\" y=\"-115.6701\">a</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge7\">\n",
       "<title>3-&gt;1</title>\n",
       "<path d=\"M325.0536,-47.943C357.0874,-42.9418 412.4381,-37.4213 458.1165,-48.8701 501.1173,-59.6477 545.4113,-87.3144 570.4059,-104.7571\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"576.3321,-108.9549 568.7991,-107.4792 573.476,-106.9318 570.6199,-104.9087 570.6199,-104.9087 570.6199,-104.9087 573.476,-106.9318 572.4407,-102.3382 576.3321,-108.9549 576.3321,-108.9549\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427.7465\" y=\"-52.6701\">a</text>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g class=\"node\" id=\"node10\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"431.2465\" cy=\"-99.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426.7465\" y=\"-103.6701\">7</text>\n",
       "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"423.2465\" y=\"-88.6701\">❸</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;7 -->\n",
       "<g class=\"edge\" id=\"edge11\">\n",
       "<title>6-&gt;7</title>\n",
       "<path d=\"M252.2565,-125.8632C258.2653,-123.2538 265.1911,-120.5889 271.7401,-118.8701 314.1213,-107.7465 364.5626,-103.12 397.2065,-101.2056\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"404.2966,-100.8161 397.4799,-104.3454 400.8018,-101.0081 397.3071,-101.2002 397.3071,-101.2002 397.3071,-101.2002 400.8018,-101.0081 397.1343,-98.0549 404.2966,-100.8161 404.2966,-100.8161\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293.1102\" y=\"-122.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 10 -->\n",
       "<g class=\"node\" id=\"node11\">\n",
       "<title>10</title>\n",
       "<ellipse cx=\"364.9283\" cy=\"-148.8701\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"364.9283\" y=\"-145.1701\">10</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;10 -->\n",
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>6-&gt;10</title>\n",
       "<path d=\"M253.7032,-135.9557C275.0316,-138.4322 310.8838,-142.595 336.1068,-145.5236\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"343.2414,-146.352 335.9248,-148.6735 339.7648,-145.9483 336.2881,-145.5446 336.2881,-145.5446 336.2881,-145.5446 339.7648,-145.9483 336.6515,-142.4156 343.2414,-146.352 343.2414,-146.352\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"295.1102\" y=\"-147.6701\">a</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge8\">\n",
       "<title>4-&gt;2</title>\n",
       "<path d=\"M735.8849,-220.1485C717.635,-225.2686 692.4959,-230.8701 669.8567,-230.8701 235.7401,-230.8701 235.7401,-230.8701 235.7401,-230.8701 197.3699,-230.8701 172.9382,-186.51 161.1405,-157.7873\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"158.546,-151.2117 164.0454,-156.567 159.8306,-154.4675 161.1152,-157.7232 161.1152,-157.7232 161.1152,-157.7232 159.8306,-154.4675 158.1851,-158.8794 158.546,-151.2117 158.546,-151.2117\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"499.4866\" y=\"-234.6701\">a</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;9 -->\n",
       "<g class=\"edge\" id=\"edge16\">\n",
       "<title>9-&gt;9</title>\n",
       "<path d=\"M753.0933,-116.7861C750.8411,-127.0204 753.7189,-136.8701 761.7267,-136.8701 767.8577,-136.8701 770.9816,-131.0964 771.0983,-123.7969\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"770.3601,-116.7861 774.2259,-123.4177 770.7267,-120.2668 771.0932,-123.7476 771.0932,-123.7476 771.0932,-123.7476 770.7267,-120.2668 767.9605,-124.0775 770.3601,-116.7861 770.3601,-116.7861\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"758.2267\" y=\"-140.6701\">a</text>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g class=\"node\" id=\"node12\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"862.4668\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"857.9668\" y=\"-30.6701\">8</text>\n",
       "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"854.4668\" y=\"-15.6701\">❹</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;8 -->\n",
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>9-&gt;8</title>\n",
       "<path d=\"M776.5913,-89.9511C791.8682,-78.7292 816.0109,-60.9949 834.8124,-47.184\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"840.4601,-43.0354 836.6834,-49.7182 837.6394,-45.1074 834.8186,-47.1795 834.8186,-47.1795 834.8186,-47.1795 837.6394,-45.1074 832.9538,-44.6408 840.4601,-43.0354 840.4601,-43.0354\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"806.5968\" y=\"-70.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>7-&gt;1</title>\n",
       "<path d=\"M458.1038,-101.6843C477.9722,-103.181 505.6666,-105.5915 529.8567,-108.8701 541.8407,-110.4943 555.0586,-112.8124 566.1175,-114.9021\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"573.0384,-116.2327 565.5695,-118.0043 569.6013,-115.5718 566.1643,-114.911 566.1643,-114.911 566.1643,-114.911 569.6013,-115.5718 566.759,-111.8176 573.0384,-116.2327 573.0384,-116.2327\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"499.4866\" y=\"-112.6701\">a</text>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;10 -->\n",
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>10-&gt;10</title>\n",
       "<path d=\"M353.3268,-167.1302C350.7486,-178.0452 354.6158,-188.3182 364.9283,-188.3182 372.985,-188.3182 377.1077,-182.048 377.2965,-174.1002\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"376.5299,-167.1302 380.4264,-173.7438 376.9126,-170.6092 377.2953,-174.0882 377.2953,-174.0882 377.2953,-174.0882 376.9126,-170.6092 374.1642,-174.4327 376.5299,-167.1302 376.5299,-167.1302\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"361.4283\" y=\"-192.1182\">a</text>\n",
       "</g>\n",
       "<!-- 11 -->\n",
       "<g class=\"node\" id=\"node13\">\n",
       "<title>11</title>\n",
       "<ellipse cx=\"502.9866\" cy=\"-159.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"494.4866\" y=\"-163.6701\">11</text>\n",
       "<text fill=\"#e31a1c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"494.9866\" y=\"-148.6701\">❺</text>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;11 -->\n",
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>10-&gt;11</title>\n",
       "<path d=\"M386.4999,-150.5888C408.5438,-152.3452 443.1024,-155.0987 468.8612,-157.1511\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"475.8755,-157.7099 468.6473,-160.2939 472.3865,-157.4319 468.8976,-157.1539 468.8976,-157.1539 468.8976,-157.1539 472.3865,-157.4319 469.1478,-154.0138 475.8755,-157.7099 475.8755,-157.7099\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"425.7465\" y=\"-159.6701\">!a</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge14\">\n",
       "<title>8-&gt;2</title>\n",
       "<path d=\"M836.1349,-20.3622C815.9146,-15.9326 787.2274,-10.8701 761.7267,-10.8701 235.7401,-10.8701 235.7401,-10.8701 235.7401,-10.8701 188.9619,-10.8701 166.7851,-72.7543 157.8448,-108.7323\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"156.1339,-115.9848 154.6754,-108.4485 156.9375,-112.5783 157.7412,-109.1718 157.7412,-109.1718 157.7412,-109.1718 156.9375,-112.5783 160.807,-109.8951 156.1339,-115.9848 156.1339,-115.9848\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"547.8567\" y=\"-14.6701\">a</text>\n",
       "</g>\n",
       "<!-- 11&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge19\">\n",
       "<title>11-&gt;1</title>\n",
       "<path d=\"M527.4633,-148.7278C540.0602,-142.9935 555.3316,-136.0417 567.7289,-130.3982\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"574.2854,-127.4136 569.2196,-133.1807 571.0999,-128.8637 567.9145,-130.3138 567.9145,-130.3138 567.9145,-130.3138 571.0999,-128.8637 566.6094,-127.4469 574.2854,-127.4136 574.2854,-127.4136\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"547.8567\" y=\"-141.6701\">a</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/svg+xml": [
       "<svg height=\"172pt\" viewBox=\"0.00 0.00 734.00 172.28\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g class=\"graph\" id=\"graph0\" transform=\"scale(.763 .763) rotate(0) translate(4 221.8)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-221.8 958,-221.8 958,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"454\" y=\"-187.6\">[Büchi]</text>\n",
       "<!-- I -->\n",
       "<!-- 1 -->\n",
       "<g class=\"node\" id=\"node2\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"56\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-75.3\">1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge1\">\n",
       "<title>I-&gt;1</title>\n",
       "<path d=\"M1.1233,-79C4.178,-79 17.9448,-79 30.9241,-79\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"37.9807,-79 30.9808,-82.1501 34.4807,-79 30.9807,-79.0001 30.9807,-79.0001 30.9807,-79.0001 34.4807,-79 30.9807,-75.8501 37.9807,-79 37.9807,-79\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge3\">\n",
       "<title>1-&gt;1</title>\n",
       "<path d=\"M49.6208,-96.0373C48.3189,-105.8579 50.4453,-115 56,-115 60.166,-115 62.4036,-109.8576 62.7128,-103.1433\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"62.3792,-96.0373 65.8541,-102.8818 62.5434,-99.5335 62.7076,-103.0296 62.7076,-103.0296 62.7076,-103.0296 62.5434,-99.5335 59.561,-103.1774 62.3792,-96.0373 62.3792,-96.0373\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.5\" y=\"-118.8\">a | b</text>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g class=\"node\" id=\"node5\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"165\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"165\" y=\"-109.3\">7</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;7 -->\n",
       "<g class=\"edge\" id=\"edge4\">\n",
       "<title>1-&gt;7</title>\n",
       "<path d=\"M73.5127,-84.4627C91.708,-90.1383 120.3176,-99.0624 140.6963,-105.419\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"147.5307,-107.5509 139.9102,-108.4735 144.1895,-106.5086 140.8483,-105.4664 140.8483,-105.4664 140.8483,-105.4664 144.1895,-106.5086 141.7863,-102.4593 147.5307,-107.5509 147.5307,-107.5509\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-104.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g class=\"node\" id=\"node3\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"278\" cy=\"-113\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<ellipse cx=\"278\" cy=\"-113\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"278\" y=\"-109.3\">0</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g class=\"node\" id=\"node4\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"391\" cy=\"-80\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"391\" y=\"-76.3\">4</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge2\">\n",
       "<title>0-&gt;4</title>\n",
       "<path d=\"M299.2544,-106.793C318.4701,-101.1813 346.7417,-92.925 366.8151,-87.0629\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"373.5451,-85.0975 367.7088,-90.0835 370.1854,-86.0786 366.8257,-87.0598 366.8257,-87.0598 366.8257,-87.0598 370.1854,-86.0786 365.9427,-84.0361 373.5451,-85.0975 373.5451,-85.0975\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"318\" y=\"-103.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;1 -->\n",
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>4-&gt;1</title>\n",
       "<path d=\"M372.8999,-79.946C316.8834,-79.7788 146.2408,-79.2694 81.3815,-79.0758\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"74.0111,-79.0538 81.0205,-75.9248 77.511,-79.0643 81.011,-79.0748 81.011,-79.0748 81.011,-79.0748 77.511,-79.0643 81.0016,-82.2247 74.0111,-79.0538 74.0111,-79.0538\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201\" y=\"-82.8\">!a &amp; b</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g class=\"node\" id=\"node10\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"500\" cy=\"-80\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"500\" y=\"-76.3\">5</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;5 -->\n",
       "<g class=\"edge\" id=\"edge9\">\n",
       "<title>4-&gt;5</title>\n",
       "<path d=\"M409.4904,-80C427.3712,-80 454.6126,-80 474.5388,-80\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"481.7827,-80 474.7828,-83.1501 478.2827,-80 474.7827,-80.0001 474.7827,-80.0001 474.7827,-80.0001 478.2827,-80 474.7827,-76.8501 481.7827,-80 481.7827,-80\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427\" y=\"-83.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;0 -->\n",
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>7-&gt;0</title>\n",
       "<path d=\"M183.1554,-113C200.7906,-113 227.8626,-113 248.576,-113\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"255.6115,-113 248.6116,-116.1501 252.1115,-113 248.6115,-113.0001 248.6115,-113.0001 248.6115,-113.0001 252.1115,-113 248.6115,-109.8501 255.6115,-113 255.6115,-113\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201\" y=\"-116.8\">!a &amp; b</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g class=\"node\" id=\"node6\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"663.5\" cy=\"-97\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"663.5\" y=\"-93.3\">2</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge5\">\n",
       "<title>2-&gt;2</title>\n",
       "<path d=\"M654.2674,-112.5414C651.6685,-122.9087 654.7461,-133 663.5,-133 670.2022,-133 673.577,-127.0847 673.6245,-119.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"672.7326,-112.5414 676.7286,-119.0955 673.1678,-116.0143 673.603,-119.4871 673.603,-119.4871 673.603,-119.4871 673.1678,-116.0143 670.4775,-119.8788 672.7326,-112.5414 672.7326,-112.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"650\" y=\"-136.8\">a | b</text>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g class=\"node\" id=\"node7\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"936\" cy=\"-97\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"936\" y=\"-93.3\">8</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;8 -->\n",
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;8</title>\n",
       "<path d=\"M681.8026,-97C729.2146,-97 856.1151,-97 910.5873,-97\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"917.777,-97 910.7771,-100.1501 914.277,-97 910.777,-97.0001 910.777,-97.0001 910.777,-97.0001 914.277,-97 910.777,-93.8501 917.777,-97 917.777,-97\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"754\" y=\"-100.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;7 -->\n",
       "<g class=\"edge\" id=\"edge16\">\n",
       "<title>8-&gt;7</title>\n",
       "<path d=\"M923.7255,-110.6752C904.9501,-130.007 867.0414,-163 827,-163 278,-163 278,-163 278,-163 243.2449,-163 207.2234,-142.9755 185.4575,-128.2712\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"179.4435,-124.0966 186.9901,-125.5006 182.3187,-126.0924 185.1939,-128.0882 185.1939,-128.0882 185.1939,-128.0882 182.3187,-126.0924 183.3977,-130.6759 179.4435,-124.0966 179.4435,-124.0966\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536\" y=\"-166.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g class=\"node\" id=\"node8\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"718\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"718\" y=\"-14.3\">3</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge7\">\n",
       "<title>3-&gt;3</title>\n",
       "<path d=\"M708.7674,-33.5414C706.1685,-43.9087 709.2461,-54 718,-54 724.7022,-54 728.077,-48.0847 728.1245,-40.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"727.2326,-33.5414 731.2286,-40.0955 727.6678,-37.0143 728.103,-40.4871 728.103,-40.4871 728.103,-40.4871 727.6678,-37.0143 724.9775,-40.8788 727.2326,-33.5414 727.2326,-33.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"704.5\" y=\"-57.8\">a | b</text>\n",
       "</g>\n",
       "<!-- 9 -->\n",
       "<g class=\"node\" id=\"node9\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"827\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"827\" y=\"-14.3\">9</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;9 -->\n",
       "<g class=\"edge\" id=\"edge8\">\n",
       "<title>3-&gt;9</title>\n",
       "<path d=\"M736.4904,-18C754.3712,-18 781.6126,-18 801.5388,-18\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"808.7827,-18 801.7828,-21.1501 805.2827,-18 801.7827,-18.0001 801.7827,-18.0001 801.7827,-18.0001 805.2827,-18 801.7827,-14.8501 808.7827,-18 808.7827,-18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"754\" y=\"-21.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;8 -->\n",
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>9-&gt;8</title>\n",
       "<path d=\"M842.34,-28.0053C857.2804,-37.8666 880.5226,-53.5185 900,-68 905.4865,-72.0793 911.308,-76.6549 916.6339,-80.9448\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"922.1793,-85.4507 914.7602,-83.4811 919.463,-83.2435 916.7466,-81.0364 916.7466,-81.0364 916.7466,-81.0364 919.463,-83.2435 918.7331,-78.5917 922.1793,-85.4507 922.1793,-85.4507\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"863\" y=\"-71.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;9 -->\n",
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>9-&gt;9</title>\n",
       "<path d=\"M817.7674,-33.5414C815.1685,-43.9087 818.2461,-54 827,-54 833.7022,-54 837.077,-48.0847 837.1245,-40.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"836.2326,-33.5414 840.2286,-40.0955 836.6678,-37.0143 837.103,-40.4871 837.103,-40.4871 837.103,-40.4871 836.6678,-37.0143 833.9775,-40.8788 836.2326,-33.5414 836.2326,-33.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"808.5\" y=\"-57.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;2 -->\n",
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>5-&gt;2</title>\n",
       "<path d=\"M518.1221,-81.8843C547.3403,-84.9222 604.9377,-90.911 638.1922,-94.3686\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"645.2968,-95.1073 638.0085,-97.5164 641.8155,-94.7453 638.3343,-94.3833 638.3343,-94.3833 638.3343,-94.3833 641.8155,-94.7453 638.6601,-91.2502 645.2968,-95.1073 645.2968,-95.1073\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536\" y=\"-90.8\">!a &amp; b</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g class=\"node\" id=\"node11\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"609\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"609\" y=\"-14.3\">6</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge11\">\n",
       "<title>5-&gt;6</title>\n",
       "<path d=\"M516.0833,-70.8517C534.8669,-60.1675 566.0377,-42.4373 587.0389,-30.4916\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"593.2051,-26.9843 588.6779,-33.1833 590.1628,-28.7148 587.1205,-30.4453 587.1205,-30.4453 587.1205,-30.4453 590.1628,-28.7148 585.5631,-27.7072 593.2051,-26.9843 593.2051,-26.9843\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536\" y=\"-62.8\">a &amp; !b</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;3 -->\n",
       "<g class=\"edge\" id=\"edge14\">\n",
       "<title>6-&gt;3</title>\n",
       "<path d=\"M627.4904,-18C645.3712,-18 672.6126,-18 692.5388,-18\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"699.7827,-18 692.7828,-21.1501 696.2827,-18 692.7827,-18.0001 692.7827,-18.0001 692.7827,-18.0001 696.2827,-18 692.7827,-14.8501 699.7827,-18 699.7827,-18\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"645\" y=\"-21.8\">!a &amp; b</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M599.7674,-33.5414C597.1685,-43.9087 600.2461,-54 609,-54 615.7022,-54 619.077,-48.0847 619.1245,-40.6591\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"618.2326,-33.5414 622.2286,-40.0955 618.6678,-37.0143 619.103,-40.4871 619.103,-40.4871 619.103,-40.4871 618.6678,-37.0143 615.9775,-40.8788 618.2326,-33.5414 618.2326,-33.5414\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"590.5\" y=\"-57.8\">a &amp; !b</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "display(sg.aut_pattern(sg.AUT_KS_NCA, 3).show('.a'),\n",
    "        sg.aut_pattern(sg.AUT_L_DSA, 3).show('.a'),\n",
    "        sg.aut_pattern(sg.AUT_L_NBA, 3).show('.a'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Multiple automata can be generated using the `aut_patterns()` function, which works similarly to `ltl_patterns()`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "3\n",
      "5\n",
      "7\n",
      "9\n",
      "11\n",
      "13\n",
      "15\n",
      "17\n",
      "19\n",
      "21\n"
     ]
    }
   ],
   "source": [
    "for aut in sg.aut_patterns(sg.AUT_KS_NCA):\n",
    "    print(aut.num_states())"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.6.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}