dfa_minimization.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Deterministic Finite Automaton Minimization"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Input format\n",
    "\n",
    "    states number\n",
    "    final states list\n",
    "    states transitions by zero\n",
    "    states transitions by one\n",
    "\n",
    "#### Example\n",
    "\n",
    "    8\n",
    "    5 6\n",
    "    7 7 4 4 5 5 6 2\n",
    "    1 0 5 5 6 5 5 2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [],
   "source": [
    "from graphviz import Digraph\n",
    "from copy import deepcopy\n",
    "\n",
    "\n",
    "class Automaton:\n",
    "    def __init__(self, states=None, final_states=None, by_zero=None, by_one=None):\n",
    "        self.states = states\n",
    "        self.final_states = final_states\n",
    "        self.by_zero = by_zero\n",
    "        self.by_one = by_one\n",
    "\n",
    "    def visualize(self):\n",
    "        graph = Digraph()\n",
    "\n",
    "        for state in self.states:\n",
    "            if state in self.final_states:\n",
    "                graph.node(name=str(state), label=str(state), shape='doublecircle')\n",
    "            else:\n",
    "                graph.node(name=str(state), label=str(state), shape='circle')\n",
    "\n",
    "        for tail, head in zip(self.states, self.by_zero):\n",
    "            graph.edge(tail_name=str(tail), head_name=str(head), label='0')\n",
    "\n",
    "        for tail, head in zip(self.states, self.by_one):\n",
    "            graph.edge(tail_name=str(tail), head_name=str(head), label='1')\n",
    "\n",
    "        return graph\n",
    "\n",
    "\n",
    "def read_automaton(input_file):\n",
    "    automaton = Automaton()\n",
    "\n",
    "    with open(input_file) as file:\n",
    "        automaton.states = list(range(int(file.readline())))\n",
    "        lines = []\n",
    "        for line in file.readlines():\n",
    "            lines.append([int(i) for i in line.split()])\n",
    "        automaton.final_states, automaton.by_zero, automaton.by_one = lines\n",
    "\n",
    "    return automaton\n",
    "\n",
    "\n",
    "def get_equivalence_classes(automaton):\n",
    "    equivalence_classes = []\n",
    "\n",
    "    marked_states = []\n",
    "    for state in automaton.states:\n",
    "        if state in automaton.final_states:\n",
    "            marked_states.append((1, (None, None)))  # (<class>, (<transition_by_zero_class>, <transition_by_one_class>))\n",
    "        else:\n",
    "            marked_states.append((0, (None, None)))\n",
    "\n",
    "    old_classes_count = len(set(marked_states))\n",
    "\n",
    "    while True:\n",
    "        for state, state_marks in enumerate(marked_states):\n",
    "            marked_states[state] = \\\n",
    "                (state_marks[0],\n",
    "                 (marked_states[automaton.by_zero[state]][0], marked_states[automaton.by_one[state]][0]))\n",
    "\n",
    "        unique_marks = list(set(marked_states))\n",
    "        for state, state_marks in enumerate(marked_states):\n",
    "            marked_states[state] = (unique_marks.index(state_marks), (None, None))\n",
    "\n",
    "        if len(unique_marks) == old_classes_count:\n",
    "            for equivalence_class in range(len(unique_marks)):\n",
    "                equivalence_classes.append([state for state, state_marks in enumerate(marked_states)\n",
    "                                           if state_marks[0] == equivalence_class])\n",
    "            break\n",
    "\n",
    "        old_classes_count = len(unique_marks)\n",
    "\n",
    "    return equivalence_classes\n",
    "\n",
    "\n",
    "def minimize_automaton(automaton, equivalence_classes):\n",
    "    minimal_automaton = deepcopy(automaton)\n",
    "\n",
    "    for equivalence_class in equivalence_classes:\n",
    "        for state in equivalence_class:\n",
    "            if minimal_automaton.by_zero[state] in equivalence_class:\n",
    "                minimal_automaton.by_zero[state] = state\n",
    "            else:\n",
    "                minimal_automaton.by_zero[state] = \\\n",
    "                    min(equivalence_classes[[equivalence_classes.index(equivalence_class)\n",
    "                                             for equivalence_class in equivalence_classes\n",
    "                                             if minimal_automaton.by_zero[state] in equivalence_class][0]])\n",
    "            if minimal_automaton.by_one[state] in equivalence_class:\n",
    "                minimal_automaton.by_one[state] = state\n",
    "            else:\n",
    "                minimal_automaton.by_one[state] = \\\n",
    "                    min(equivalence_classes[[equivalence_classes.index(equivalence_class)\n",
    "                                             for equivalence_class in equivalence_classes\n",
    "                                             if minimal_automaton.by_one[state] in equivalence_class][0]])\n",
    "\n",
    "    for equivalence_class in equivalence_classes:\n",
    "        for state in equivalence_class[1:]:\n",
    "            minimal_automaton.by_zero[state] = -1\n",
    "            minimal_automaton.by_one[state] = -1\n",
    "            if state in minimal_automaton.final_states:\n",
    "                minimal_automaton.final_states.remove(state)\n",
    "            minimal_automaton.states[minimal_automaton.states.index(state)] = -1\n",
    "\n",
    "    not_deleted = lambda x: x != -1\n",
    "    minimal_automaton.states = list(filter(not_deleted, minimal_automaton.states))\n",
    "    minimal_automaton.by_zero = list(filter(not_deleted, minimal_automaton.by_zero))\n",
    "    minimal_automaton.by_one = list(filter(not_deleted, minimal_automaton.by_one))\n",
    "\n",
    "    for i, state in enumerate(minimal_automaton.states):\n",
    "        if i < len(minimal_automaton.final_states):\n",
    "            minimal_automaton.final_states[i] = minimal_automaton.states.index(minimal_automaton.final_states[i])\n",
    "        minimal_automaton.by_zero[i] = minimal_automaton.states.index(minimal_automaton.by_zero[i])\n",
    "        minimal_automaton.by_one[i] = minimal_automaton.states.index(minimal_automaton.by_one[i])\n",
    "    minimal_automaton.states = list(range(len(minimal_automaton.states)))\n",
    "\n",
    "    return minimal_automaton"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Random DFA generator"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Test generated\n"
     ]
    }
   ],
   "source": [
    "import random\n",
    "\n",
    "def generate_test_dfa(states_number):\n",
    "    final_states_number = random.randint(0, states_number - 1)\n",
    "    final_states = [random.randint(0, states_number - 1) for i in range(final_states_number)]\n",
    "    by_zero = [random.randint(0, states_number - 1) for i in range(states_number)]\n",
    "    by_one = [random.randint(0, states_number - 1) for i in range(states_number)]\n",
    "    test_data = str(states_number) + '\\n' + ' '.join(str(v) for v in final_states) + '\\n' + ' '.join(str(v) for v in by_zero) + '\\n' + ' '.join(str(v) for v in by_one)\n",
    "    with open('test_dfa.txt', 'w') as file:\n",
    "        file.write(test_data)\n",
    "    print('Test generated')\n",
    "\n",
    "\n",
    "generate_test_dfa(5)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Reading random DFA"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "initial_automaton = read_automaton('test_dfa.txt')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Reading DFA from file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "initial_automaton = read_automaton('input.txt')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [],
   "source": [
    "equivalence_classes = get_equivalence_classes(initial_automaton)\n",
    "minimal_automaton = minimize_automaton(initial_automaton, equivalence_classes)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Initial automaton"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": "<graphviz.dot.Digraph at 0x2597c027a48>",
      "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\r\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\r\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\r\n<!-- Generated by graphviz version 2.38.0 (20140413.2041)\r\n -->\r\n<!-- Title: %3 Pages: 1 -->\r\n<svg width=\"214pt\" height=\"582pt\"\r\n viewBox=\"0.00 0.00 214.00 582.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\r\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 578)\">\r\n<title>%3</title>\r\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-578 210,-578 210,4 -4,4\"/>\r\n<!-- 0 -->\r\n<g id=\"node1\" class=\"node\"><title>0</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"48\" cy=\"-556\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"48\" y=\"-552.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 1 -->\r\n<g id=\"node2\" class=\"node\"><title>1</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"18\" cy=\"-469\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"18\" y=\"-465.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 0&#45;&gt;1 -->\r\n<g id=\"edge9\" class=\"edge\"><title>0&#45;&gt;1</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M35.6911,-542.846C30.1621,-536.579 24.1774,-528.48 21,-520 18.3454,-512.915 17.1486,-504.871 16.7254,-497.338\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"20.2227,-497.128 16.5708,-487.182 13.2235,-497.235 20.2227,-497.128\"/>\r\n<text text-anchor=\"middle\" x=\"24.5\" y=\"-508.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 7 -->\r\n<g id=\"node8\" class=\"node\"><title>7</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"53\" cy=\"-382\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"53\" y=\"-378.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">7</text>\r\n</g>\r\n<!-- 0&#45;&gt;7 -->\r\n<g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;7</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M48.4977,-537.879C49.3662,-508.001 51.1653,-446.113 52.2072,-410.274\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"55.7122,-410.149 52.5043,-400.052 48.7151,-409.946 55.7122,-410.149\"/>\r\n<text text-anchor=\"middle\" x=\"53.5\" y=\"-465.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 1&#45;&gt;0 -->\r\n<g id=\"edge10\" class=\"edge\"><title>1&#45;&gt;0</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M23.7665,-486.339C28.0368,-498.438 33.941,-515.166 38.8524,-529.082\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"35.587,-530.346 42.2157,-538.611 42.1879,-528.016 35.587,-530.346\"/>\r\n<text text-anchor=\"middle\" x=\"37.5\" y=\"-508.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 1&#45;&gt;7 -->\r\n<g id=\"edge2\" class=\"edge\"><title>1&#45;&gt;7</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M24.5832,-452.012C29.6185,-439.784 36.6614,-422.679 42.4759,-408.559\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"45.8751,-409.496 46.4463,-398.916 39.4024,-406.83 45.8751,-409.496\"/>\r\n<text text-anchor=\"middle\" x=\"40.5\" y=\"-421.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 2 -->\r\n<g id=\"node3\" class=\"node\"><title>2</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"53\" cy=\"-295\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"53\" y=\"-291.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">2</text>\r\n</g>\r\n<!-- 4 -->\r\n<g id=\"node5\" class=\"node\"><title>4</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"104\" cy=\"-208\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"104\" y=\"-204.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">4</text>\r\n</g>\r\n<!-- 2&#45;&gt;4 -->\r\n<g id=\"edge3\" class=\"edge\"><title>2&#45;&gt;4</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M61.8835,-279.194C69.5881,-266.353 80.8772,-247.538 89.8287,-232.619\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"92.9034,-234.297 95.0472,-223.921 86.9009,-230.696 92.9034,-234.297\"/>\r\n<text text-anchor=\"middle\" x=\"84.5\" y=\"-247.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 5 -->\r\n<g id=\"node6\" class=\"node\"><title>5</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"103\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"103\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\r\n<text text-anchor=\"middle\" x=\"103\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">5</text>\r\n</g>\r\n<!-- 2&#45;&gt;5 -->\r\n<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M54.527,-276.893C58.2281,-238.164 68.8873,-141 89,-62 89.8164,-58.7931 90.7915,-55.4795 91.8418,-52.201\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"95.1967,-53.2077 95.1352,-42.613 88.5764,-50.9336 95.1967,-53.2077\"/>\r\n<text text-anchor=\"middle\" x=\"72.5\" y=\"-160.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 3 -->\r\n<g id=\"node4\" class=\"node\"><title>3</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"174\" cy=\"-295\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"174\" y=\"-291.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">3</text>\r\n</g>\r\n<!-- 3&#45;&gt;4 -->\r\n<g id=\"edge4\" class=\"edge\"><title>3&#45;&gt;4</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M162.753,-280.343C151.666,-266.881 134.559,-246.107 121.658,-230.441\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"124.047,-227.837 114.988,-222.343 118.643,-232.287 124.047,-227.837\"/>\r\n<text text-anchor=\"middle\" x=\"146.5\" y=\"-247.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 3&#45;&gt;5 -->\r\n<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M179.861,-277.851C191.598,-242.722 214.523,-157.503 186,-95 174.788,-70.4302 150.591,-51.0151 131.201,-38.568\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"132.776,-35.4282 122.422,-33.1857 129.118,-41.3961 132.776,-35.4282\"/>\r\n<text text-anchor=\"middle\" x=\"202.5\" y=\"-160.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 4&#45;&gt;5 -->\r\n<g id=\"edge5\" class=\"edge\"><title>4&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M100.221,-190.341C97.3165,-176.64 93.5476,-156.675 92,-139 90.2943,-119.519 90.5191,-114.499 92,-95 93.0324,-81.4062 95.1462,-66.4923 97.2475,-53.7811\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"100.736,-54.1485 98.9855,-43.6992 93.8374,-52.9592 100.736,-54.1485\"/>\r\n<text text-anchor=\"middle\" x=\"95.5\" y=\"-113.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 6 -->\r\n<g id=\"node7\" class=\"node\"><title>6</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"130\" cy=\"-117\" rx=\"18\" ry=\"18\"/>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"130\" cy=\"-117\" rx=\"22\" ry=\"22\"/>\r\n<text text-anchor=\"middle\" x=\"130\" y=\"-113.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">6</text>\r\n</g>\r\n<!-- 4&#45;&gt;6 -->\r\n<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;6</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M108.89,-190.26C112.347,-178.428 117.077,-162.238 121.183,-148.181\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"124.591,-148.995 124.036,-138.415 117.872,-147.032 124.591,-148.995\"/>\r\n<text text-anchor=\"middle\" x=\"121.5\" y=\"-160.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 5&#45;&gt;5 -->\r\n<g id=\"edge6\" class=\"edge\"><title>5&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M124.807,-26.2451C134.563,-26.6494 143,-25.2344 143,-22 143,-19.9785 139.704,-18.6677 134.85,-18.0676\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"134.911,-14.5679 124.807,-17.7549 134.693,-21.5645 134.911,-14.5679\"/>\r\n<text text-anchor=\"middle\" x=\"146.5\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 5&#45;&gt;5 -->\r\n<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M123.813,-29.2015C141.884,-32.4865 161,-30.0859 161,-22 161,-15.4302 148.38,-12.6136 133.955,-13.5503\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"133.311,-10.1032 123.813,-14.7985 134.166,-17.0508 133.311,-10.1032\"/>\r\n<text text-anchor=\"middle\" x=\"164.5\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 6&#45;&gt;5 -->\r\n<g id=\"edge15\" class=\"edge\"><title>6&#45;&gt;5</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M124.008,-95.3603C120.382,-82.8726 115.698,-66.7364 111.672,-52.8716\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"115.032,-51.8896 108.883,-43.262 108.309,-53.8414 115.032,-51.8896\"/>\r\n<text text-anchor=\"middle\" x=\"121.5\" y=\"-65.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 6&#45;&gt;6 -->\r\n<g id=\"edge7\" class=\"edge\"><title>6&#45;&gt;6</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M150.581,-125.37C160.845,-126.528 170,-123.738 170,-117 170,-112.683 166.243,-109.987 160.844,-108.911\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"160.673,-105.405 150.581,-108.63 160.481,-112.402 160.673,-105.405\"/>\r\n<text text-anchor=\"middle\" x=\"173.5\" y=\"-113.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 7&#45;&gt;2 -->\r\n<g id=\"edge8\" class=\"edge\"><title>7&#45;&gt;2</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M46.3664,-365.258C44.201,-359.332 42.0772,-352.463 41,-346 39.653,-337.918 40.8143,-329.204 42.8585,-321.351\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"46.2489,-322.237 45.9176,-311.647 39.5728,-320.132 46.2489,-322.237\"/>\r\n<text text-anchor=\"middle\" x=\"44.5\" y=\"-334.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 7&#45;&gt;2 -->\r\n<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;2</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M53,-363.799C53,-352.163 53,-336.548 53,-323.237\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"56.5001,-323.175 53,-313.175 49.5001,-323.175 56.5001,-323.175\"/>\r\n<text text-anchor=\"middle\" x=\"56.5\" y=\"-334.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n</g>\r\n</svg>\r\n"
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "initial_automaton.visualize()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Minimal automaton"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": "<graphviz.dot.Digraph at 0x2597c02c348>",
      "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\r\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\r\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\r\n<!-- Generated by graphviz version 2.38.0 (20140413.2041)\r\n -->\r\n<!-- Title: %3 Pages: 1 -->\r\n<svg width=\"128pt\" height=\"400pt\"\r\n viewBox=\"0.00 0.00 128.00 400.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\r\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 396)\">\r\n<title>%3</title>\r\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-396 124,-396 124,4 -4,4\"/>\r\n<!-- 0 -->\r\n<g id=\"node1\" class=\"node\"><title>0</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"58\" cy=\"-374\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"58\" y=\"-370.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 0&#45;&gt;0 -->\r\n<g id=\"edge6\" class=\"edge\"><title>0&#45;&gt;0</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M74.6641,-381.383C84.625,-383.023 94,-380.563 94,-374 94,-369.796 90.1525,-367.275 84.7682,-366.438\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"84.6002,-362.94 74.6641,-366.617 84.7247,-369.939 84.6002,-362.94\"/>\r\n<text text-anchor=\"middle\" x=\"97.5\" y=\"-370.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 4 -->\r\n<g id=\"node5\" class=\"node\"><title>4</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"58\" cy=\"-287\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"58\" y=\"-283.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">4</text>\r\n</g>\r\n<!-- 0&#45;&gt;4 -->\r\n<g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;4</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M58,-355.799C58,-344.163 58,-328.548 58,-315.237\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"61.5001,-315.175 58,-305.175 54.5001,-315.175 61.5001,-315.175\"/>\r\n<text text-anchor=\"middle\" x=\"61.5\" y=\"-326.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 1 -->\r\n<g id=\"node2\" class=\"node\"><title>1</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"58\" cy=\"-200\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"58\" y=\"-196.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 2 -->\r\n<g id=\"node3\" class=\"node\"><title>2</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"18\" cy=\"-113\" rx=\"18\" ry=\"18\"/>\r\n<text text-anchor=\"middle\" x=\"18\" y=\"-109.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">2</text>\r\n</g>\r\n<!-- 1&#45;&gt;2 -->\r\n<g id=\"edge2\" class=\"edge\"><title>1&#45;&gt;2</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M50.6634,-183.41C44.7993,-170.949 36.4679,-153.244 29.6873,-138.835\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"32.715,-137.049 25.2901,-129.491 26.3813,-140.03 32.715,-137.049\"/>\r\n<text text-anchor=\"middle\" x=\"44.5\" y=\"-152.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 3 -->\r\n<g id=\"node4\" class=\"node\"><title>3</title>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"48\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\r\n<ellipse fill=\"none\" stroke=\"black\" cx=\"48\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\r\n<text text-anchor=\"middle\" x=\"48\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">3</text>\r\n</g>\r\n<!-- 1&#45;&gt;3 -->\r\n<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M57.023,-181.804C55.3456,-152.282 51.8949,-91.5505 49.7806,-54.3381\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"53.2582,-53.8436 49.1965,-44.0583 46.2695,-54.2408 53.2582,-53.8436\"/>\r\n<text text-anchor=\"middle\" x=\"57.5\" y=\"-109.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 2&#45;&gt;3 -->\r\n<g id=\"edge3\" class=\"edge\"><title>2&#45;&gt;3</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M16.7732,-94.8904C16.6142,-85.0206 17.3642,-72.5206 21,-62 22.7375,-56.9724 25.3171,-51.999 28.2033,-47.3725\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"31.1949,-49.1995 33.9905,-38.9802 25.4322,-45.2257 31.1949,-49.1995\"/>\r\n<text text-anchor=\"middle\" x=\"24.5\" y=\"-65.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 2&#45;&gt;3 -->\r\n<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;3</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M23.5025,-95.676C27.5706,-83.6071 33.2222,-66.8409 38.0719,-52.4532\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"41.3945,-53.5536 41.2721,-42.9595 34.7612,-51.3176 41.3945,-53.5536\"/>\r\n<text text-anchor=\"middle\" x=\"38.5\" y=\"-65.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 3&#45;&gt;3 -->\r\n<g id=\"edge4\" class=\"edge\"><title>3&#45;&gt;3</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M69.8066,-26.2451C79.5625,-26.6494 88,-25.2344 88,-22 88,-19.9785 84.7041,-18.6677 79.8504,-18.0676\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"79.9107,-14.5679 69.8066,-17.7549 79.6928,-21.5645 79.9107,-14.5679\"/>\r\n<text text-anchor=\"middle\" x=\"91.5\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 3&#45;&gt;3 -->\r\n<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;3</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M68.813,-29.2015C86.8838,-32.4865 106,-30.0859 106,-22 106,-15.4302 93.3803,-12.6136 78.9552,-13.5503\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"78.3106,-10.1032 68.813,-14.7985 79.1656,-17.0508 78.3106,-10.1032\"/>\r\n<text text-anchor=\"middle\" x=\"109.5\" y=\"-18.3\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n<!-- 4&#45;&gt;1 -->\r\n<g id=\"edge5\" class=\"edge\"><title>4&#45;&gt;1</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M51.3664,-270.258C49.201,-264.332 47.0772,-257.463 46,-251 44.653,-242.918 45.8143,-234.204 47.8585,-226.351\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"51.2489,-227.237 50.9176,-216.647 44.5728,-225.132 51.2489,-227.237\"/>\r\n<text text-anchor=\"middle\" x=\"49.5\" y=\"-239.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">0</text>\r\n</g>\r\n<!-- 4&#45;&gt;1 -->\r\n<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;1</title>\r\n<path fill=\"none\" stroke=\"black\" d=\"M58,-268.799C58,-257.163 58,-241.548 58,-228.237\"/>\r\n<polygon fill=\"black\" stroke=\"black\" points=\"61.5001,-228.175 58,-218.175 54.5001,-228.175 61.5001,-228.175\"/>\r\n<text text-anchor=\"middle\" x=\"61.5\" y=\"-239.8\" font-family=\"Times New Roman,serif\" font-size=\"14.00\">1</text>\r\n</g>\r\n</g>\r\n</svg>\r\n"
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minimal_automaton.visualize()"
   ]
  }
 ],
 "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.8.2-final"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}