FDFALearning.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# FDFA Learning"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![logo](https://iscasmc.ios.ac.cn/roll/lib/exe/fetch.php?media=wiki:logo.png)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is a tutorial for the Java Library [```Regular Omega Language Learning (ROLL)```](https://iscasmc.ios.ac.cn/roll/doku.php) in a Groovy kernel Jupyter Notebook.\n",
    "Groovy is very similar to Java and you can write all code in Java syntax.\n",
    "\n",
    "**Tips** : If something goes strange, use the menu bar above ```Kernel -> Restart``` to reboot this notebook and run following code again.\n",
    "\n",
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**First of all, load the jar file of the learning library ROLL.**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Added jar: [ROLL.jar]\n"
     ]
    }
   ],
   "source": [
    "%classpath add jar ROLL.jar"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In the active automata learning setting proposed by Angluin, there are a `teacher`, which knows the target language $L$, and a `learner`, whose task is to learn the target language, represented by an automaton, from the teacher by means of two kinds of queries: `membership queries` and `equivalence queries`. \n",
    "A membership query $MQ[w]$ asks whether a string $w$ belongs to $L$ while an equivalence query $EQ[A]$ asks whether the hypothesis automaton $A$ recognizes $L$. \n",
    "The teacher replies with a witness if the hypothesis is incorrect otherwise the learner completes its job.\n",
    "\n",
    "In the following, we introduce two ways to learn the $\\omega$-regular language  $L =\\Sigma^* b^\\omega$ over the alphabet $\\Sigma = \\{a, b\\}$.\n",
    "The first way is to use FDFA operations with the help of [DK package](http://www.brics.dk/automaton/) to play as the teacher.\n",
    "The second way is to allow youself to play as the teacher.\n",
    "\n",
    "**1. Learning the $\\omega$-regular language L from DK by giving a target FDFA $F$ **"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "we first need to create the target FDFA $F$ which accepts the language $L$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[0->a, 1->b]"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import roll.words.Alphabet\n",
    "// you can always import all the classes in roll.jupyter package\n",
    "import roll.jupyter.*\n",
    "import java.util.List\n",
    "import java.util.ArrayList\n",
    "\n",
    "// in order to create an alphabet, you need an array of Characters\n",
    "// the variable apList is local since there is type in front of it\n",
    "List<Character> apList = new ArrayList<Character>();\n",
    "\n",
    "// in Groovy, we have to do strong cast for Characters \n",
    "apList.add((char)'a');\n",
    "apList.add((char)'b');\n",
    "\n",
    "// create an alphabet with a Character list\n",
    "// the created alphabet is global in this notebook\n",
    "JupyterROLL.createAlphabet(apList);\n",
    "\n",
    "\n",
    "\n",
    "// now we can get the alphabet\n",
    "alphabet = JupyterROLL.getAlphabet();"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"301pt\" height=\"120pt\" viewBox=\"0.00 0.00 301.00 120.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 116)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-116 297,-116 297,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-53.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M125.618,-25.5196C136.095,-30.5642 150.2,-37.3554 162.626,-43.3386\"/><polygon fill=\"black\" stroke=\"black\" points=\"161.186,-46.5296 171.714,-47.7143 164.223,-40.2225 161.186,-46.5296\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-40.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title><ellipse fill=\"none\" stroke=\"black\" cx=\"275\" cy=\"-24\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"275\" y=\"-20.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 0&#45;&gt;2 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M126.969,-15.0518C147.586,-11.8859 183.411,-7.7242 214,-11 225.128,-12.1917 237.221,-14.5928 247.616,-17.0107\"/><polygon fill=\"black\" stroke=\"black\" points=\"246.8,-20.4144 257.345,-19.3901 248.463,-13.6147 246.8,-20.4144\"/><text text-anchor=\"middle\" x=\"192\" y=\"-14.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-77.9908C183.369,-88.0872 185.93,-97 192,-97 195.889,-97 198.337,-93.3422 199.346,-88.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-88.1023 199.683,-77.9908 195.85,-87.868 202.846,-88.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-100.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M212.608,-49.0116C223.399,-44.6151 236.916,-39.1083 248.517,-34.3819\"/><polygon fill=\"black\" stroke=\"black\" points=\"250.162,-37.491 258.103,-30.4767 247.521,-31.0084 250.162,-37.491\"/><text text-anchor=\"middle\" x=\"235.5\" y=\"-43.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M271.584,-41.7817C271.004,-51.3149 272.143,-60 275,-60 276.741,-60 277.844,-56.7749 278.309,-52.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"281.812,-51.8174 278.416,-41.7817 274.812,-51.745 281.812,-51.8174\"/><text text-anchor=\"middle\" x=\"275\" y=\"-63.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M269.441,-41.1418C266.17,-58.585 268.023,-78 275,-78 280.614,-78 282.91,-65.4283 281.889,-51.4287\"/><polygon fill=\"black\" stroke=\"black\" points=\"285.313,-50.6105 280.559,-41.1418 278.37,-51.508 285.313,-50.6105\"/><text text-anchor=\"middle\" x=\"275\" y=\"-81.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3 --><g id=\"node4\" class=\"node\"><title>3</title></g><!-- 3&#45;&gt;0 --><g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import java.util.List\n",
    "import java.util.ArrayList\n",
    "import roll.jupyter.*\n",
    "import roll.automata.DFA\n",
    "\n",
    "\n",
    "// use JupyterROLL to create a leading DFA of F\n",
    "// the variable target is global since there is no type in front of it\n",
    "// so we can use this variable everywhere in this notebook\n",
    "M = JupyterROLL.createDFA();\n",
    "\n",
    "//now we are ready to create a state in the learning DFA M\n",
    "M.createState();\n",
    "\n",
    "// 3 indices for the states\n",
    "int fst = 0;\n",
    "M.getState(fst).addTransition(alphabet.indexOf((char)'a'), fst); // 0 -> 0 via a\n",
    "M.getState(fst).addTransition(alphabet.indexOf((char)'b'), fst); // 0 -> 0 via b\n",
    "M.setInitial(fst);\n",
    "\n",
    "// now we create the progress DFA A for the state 0 in M\n",
    "A = JupyterROLL.createDFA();\n",
    "\n",
    "A.createState();\n",
    "A.createState();\n",
    "A.createState();\n",
    "\n",
    "int snd = 1, thd = 2;\n",
    "// the function getState is to get a state object by its state index\n",
    "A.getState(fst).addTransition(alphabet.indexOf((char)'b'), snd); // 0 -> 1 via a\n",
    "A.getState(fst).addTransition(alphabet.indexOf((char)'a'), thd); // 0 -> 2 via b\n",
    "A.getState(snd).addTransition(alphabet.indexOf((char)'b'), snd); // 1 -> 1 via a\n",
    "A.getState(snd).addTransition(alphabet.indexOf((char)'a'), thd); // 1 -> 2 via b\n",
    "A.getState(thd).addTransition(alphabet.indexOf((char)'a'), thd); // 2 -> 2 via a\n",
    "A.getState(thd).addTransition(alphabet.indexOf((char)'b'), thd); // 2 -> 2 via b\n",
    "\n",
    "// set 0 as the initial state\n",
    "A.setInitial(fst);\n",
    "// set 2 as a final state\n",
    "A.setFinal(snd);\n",
    "\n",
    "List<DFA> proDFAs = new ArrayList<>();\n",
    "proDFAs.add(A);\n",
    "\n",
    "F = JupyterROLL.createFDFA(M, proDFAs);\n",
    "// now we can output target in a DOT graph\n",
    "F"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we are ready to create an FDFA learner to learn a hypothesis FDFA $H$ from DK. \n",
    "\n",
    "We have 3 types of algorithms and 2 types of data structures to store the membership results during the learning process.\n",
    "\n",
    "|                              | tree | table |\n",
    "|:----------------------------:|:----------------------:|:-----------------------:|\n",
    "| periodic     | ✔️                     | ✔️                      |\n",
    "| syntactic | ✔️                     | ✔️                      |\n",
    "| recurrent | ✔️                     | ✔️                      |\n",
    "\n",
    "In the following, we will demostrate how to use the table-based recurrent learning algorithm to learn the target language $L$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import roll.jupyter.*\n",
    "    \n",
    "// we create a global variable sequence which stores the learning procedure as a\n",
    "// list of Triple object, the Triple object has three elements\n",
    "// the first is the table/tree data structure, the second is the current hypothesis FDFA, and the third is the counterexample\n",
    "// which refines the previous hypothesis FDFA to the current hypothesis\n",
    "sequence = JupyterROLL.learningSeq(\"recurrent\", \"table\", F);\n",
    "\n",
    "// sequence is a java.util.List instance\n",
    "sequence.size()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "From the output of the learning list, the target language $L$ has been learned by the learning algorithm only with only 2 equivalence queries.\n",
    "\n",
    "we now can check the Triple object at each step of the learning procedure"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<table border=\"1\" cellspacing=\"0\" bordercolor=\"#000000\"  style=\"border-collapse:collapse;\">\n",
       "  <tr>\n",
       "    <th><center> Learner</center></th>\n",
       "    <th><center>  Hypothesis </center></th>\n",
       "    <th><center> Counterexample </center></th>\n",
       "  </tr>\n",
       "  <tr>\n",
       "    <td><pre> Leading Learner: \n",
       "  || (ϵ, ϵ) | \n",
       "=============\n",
       "ϵ || -      | \n",
       "=============\n",
       "a || -      | \n",
       "b || -      | \n",
       "\n",
       "Progress Learner for ϵ: \n",
       "   || ϵ      | \n",
       "==============\n",
       "ϵ  || (+, -) | \n",
       "b  || (+, +) | \n",
       "==============\n",
       "a  || (+, -) | \n",
       "ba || (+, -) | \n",
       "bb || (+, +) | \n",
       "</pre></td>\n",
       "    <td><center><p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br></center></td>\n",
       "    <td><center></center></td>\n",
       "  </tr>\n",
       "</table>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// initial learner data\n",
    "sequence.get(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<table border=\"1\" cellspacing=\"0\" bordercolor=\"#000000\"  style=\"border-collapse:collapse;\">\n",
       "  <tr>\n",
       "    <th><center> Learner</center></th>\n",
       "    <th><center>  Hypothesis </center></th>\n",
       "    <th><center> Counterexample </center></th>\n",
       "  </tr>\n",
       "  <tr>\n",
       "    <td><pre> Leading Learner: \n",
       "  || (ϵ, ϵ) | \n",
       "=============\n",
       "ϵ || -      | \n",
       "=============\n",
       "a || -      | \n",
       "b || -      | \n",
       "\n",
       "Progress Learner for ϵ: \n",
       "   || ϵ      | b      | \n",
       "=======================\n",
       "ϵ  || (+, -) | (+, +) | \n",
       "b  || (+, +) | (+, +) | \n",
       "a  || (+, -) | (+, -) | \n",
       "=======================\n",
       "ba || (+, -) | (+, -) | \n",
       "bb || (+, +) | (+, +) | \n",
       "aa || (+, -) | (+, -) | \n",
       "ab || (+, -) | (+, -) | \n",
       "</pre></td>\n",
       "    <td><center><p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"301pt\" height=\"120pt\" viewBox=\"0.00 0.00 301.00 120.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 116)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-116 297,-116 297,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-53.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M125.618,-25.5196C136.095,-30.5642 150.2,-37.3554 162.626,-43.3386\"/><polygon fill=\"black\" stroke=\"black\" points=\"161.186,-46.5296 171.714,-47.7143 164.223,-40.2225 161.186,-46.5296\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-40.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title><ellipse fill=\"none\" stroke=\"black\" cx=\"275\" cy=\"-24\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"275\" y=\"-20.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 0&#45;&gt;2 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M126.969,-15.0518C147.586,-11.8859 183.411,-7.7242 214,-11 225.128,-12.1917 237.221,-14.5928 247.616,-17.0107\"/><polygon fill=\"black\" stroke=\"black\" points=\"246.8,-20.4144 257.345,-19.3901 248.463,-13.6147 246.8,-20.4144\"/><text text-anchor=\"middle\" x=\"192\" y=\"-14.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-77.9908C183.369,-88.0872 185.93,-97 192,-97 195.889,-97 198.337,-93.3422 199.346,-88.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-88.1023 199.683,-77.9908 195.85,-87.868 202.846,-88.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-100.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M212.608,-49.0116C223.399,-44.6151 236.916,-39.1083 248.517,-34.3819\"/><polygon fill=\"black\" stroke=\"black\" points=\"250.162,-37.491 258.103,-30.4767 247.521,-31.0084 250.162,-37.491\"/><text text-anchor=\"middle\" x=\"235.5\" y=\"-43.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M271.584,-41.7817C271.004,-51.3149 272.143,-60 275,-60 276.741,-60 277.844,-56.7749 278.309,-52.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"281.812,-51.8174 278.416,-41.7817 274.812,-51.745 281.812,-51.8174\"/><text text-anchor=\"middle\" x=\"275\" y=\"-63.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M269.441,-41.1418C266.17,-58.585 268.023,-78 275,-78 280.614,-78 282.91,-65.4283 281.889,-51.4287\"/><polygon fill=\"black\" stroke=\"black\" points=\"285.313,-50.6105 280.559,-41.1418 278.37,-51.508 285.313,-50.6105\"/><text text-anchor=\"middle\" x=\"275\" y=\"-81.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3 --><g id=\"node4\" class=\"node\"><title>3</title></g><!-- 3&#45;&gt;0 --><g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br></center></td>\n",
       "    <td><center>$ϵ(ab)^\\omega$</center></td>\n",
       "  </tr>\n",
       "</table>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// we get a new hypothesis after one counterexample refinement\n",
    "sequence.get(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**We have just learned how to learn the target language $L$ from DK. Sometimes we may not have the target FDFA in hand but we know exactly the language we want to learn in mind. ** \n",
    "\n",
    "In this case, we can first specify what kind of strings really belong to the target language $L$ and then refine the hypothesis if it does not recognize the target language by ourselves. \n",
    "We are going to use the tree-based recurrent learning algorithm to show how to learn the target language $L$ from ourselves. Note that for infinite words, we only care about the ultimately periodic words, which are the words represented by a finite prefix u and a periodic finite word v, i.e., $uv^\\omega$.\n",
    "\n",
    "**2. Learning the $\\omega$-regular language $L = a^\\omega + ab^\\omega$ in an interactive way**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<pre> Leading Learner: \n",
       "  || (ϵ, ϵ) | \n",
       "=============\n",
       "ϵ || -      | \n",
       "=============\n",
       "a || -      | \n",
       "b || -      | \n",
       "\n",
       "Progress Learner for ϵ: \n",
       "   || ϵ      | \n",
       "==============\n",
       "ϵ  || (+, -) | \n",
       "a  || (+, +) | \n",
       "==============\n",
       "b  || (+, -) | \n",
       "aa || (+, +) | \n",
       "ab || (+, -) | \n",
       "</pre>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import roll.jupyter.*;\n",
    "import java.util.function.BiFunction;\n",
    "import roll.words.*;\n",
    "\n",
    "// now we define a function :: (string, string) -> boolean and this function is used to \n",
    "// determine whether a string is in the target language\n",
    "// this function resolves all membership queries posed by the learners\n",
    "mqOracle = {\n",
    "    // a^w + ab^w\n",
    "    stem,loop -> \n",
    "    \n",
    "    if (loop.length() < 1) return false;     // this is a finite word\n",
    "    \n",
    "    // check whether it is a^w \n",
    "    int numBInStem = 0, numBInLoop = 0;\n",
    "    // counter the number of b's in stem\n",
    "    for (int i = 0; i < stem.length(); i ++) {\n",
    "        if(stem.charAt(i) == 'b') {\n",
    "            numBInStem ++;\n",
    "        }\n",
    "    }\n",
    "    // counter the number of b's in loop\n",
    "    for (int i = 0; i < loop.length(); i ++) {\n",
    "        if(loop.charAt(i) == 'b') {\n",
    "            numBInLoop ++;\n",
    "        }\n",
    "    }\n",
    "    \n",
    "    if(numBInStem == 0 && numBInLoop == 0) return true;\n",
    "    // check whether it is ab^w\n",
    "    // check a's in loop\n",
    "    if(numBInLoop != loop.length()) return false;\n",
    "    if(stem.length() < 1) return false;\n",
    "    if(stem.charAt(0) != 'a') return false;\n",
    "    if(stem.length() - 1 != numBInStem) return false;\n",
    "    return true;\n",
    "};\n",
    "\n",
    "// now we create a tree-based recurrent FDFA learner to learn the target language L\n",
    "fdfaLearner = JupyterROLL.createFDFALearner(\"recurrent\", \"table\", mqOracle);\n",
    "\n",
    "// we can also see the tree data structure of the learner in a DOT graph\n",
    "fdfaLearner"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;1 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// output current hypothesis to see whether it recognizes the target language\n",
    "fdfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"214pt\" height=\"79pt\" viewBox=\"0.00 0.00 214.00 79.28\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 75.2803)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-75.2803 210,-75.2803 210,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-20.2803\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-16.5803\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-37.3176C101.319,-47.1382 103.445,-56.2803 109,-56.2803 112.472,-56.2803 114.604,-52.7092 115.398,-47.6332\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-47.3113 115.379,-37.3176 111.897,-47.3238 118.897,-47.3113\"/><text text-anchor=\"middle\" x=\"109\" y=\"-60.0803\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"188\" cy=\"-20.2803\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-16.5803\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.089,-20.2803C136.659,-20.2803 148.817,-20.2803 159.677,-20.2803\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.959,-23.7804 169.959,-20.2803 159.959,-16.7804 159.959,-23.7804\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-24.0803\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.821,-9.14203C165.757,-3.65931 155.084,1.2803 145,-1.2803 141.042,-2.28533 137.047,-3.83796 133.244,-5.63201\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-2.60875 124.311,-10.4146 134.779,-8.77986 131.475,-2.60875\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-5.0803\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M181.266,-37.3176C179.892,-47.1382 182.137,-56.2803 188,-56.2803 191.665,-56.2803 193.916,-52.7092 194.753,-47.6332\"/><polygon fill=\"black\" stroke=\"black\" points=\"198.252,-47.311 194.734,-37.3176 191.252,-47.3242 198.252,-47.311\"/><text text-anchor=\"middle\" x=\"188\" y=\"-60.0803\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-20.2803C62.6538,-20.2803 72.0513,-20.2803 80.5951,-20.2803\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-23.7804 90.8257,-20.2803 80.8257,-16.7804 80.8257,-23.7804\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 1: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// the hypothesis is not correct and we can use a counterexample (a, b)\n",
    "// which is in the symmetric difference of the language of A and the target language\n",
    "fdfaLearner.refineHypothesis(\"a\", \"b\")\n",
    "fdfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"214pt\" height=\"79pt\" viewBox=\"0.00 0.00 214.00 79.28\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 75.2803)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-75.2803 210,-75.2803 210,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-20.2803\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-16.5803\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-37.3176C101.319,-47.1382 103.445,-56.2803 109,-56.2803 112.472,-56.2803 114.604,-52.7092 115.398,-47.6332\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-47.3113 115.379,-37.3176 111.897,-47.3238 118.897,-47.3113\"/><text text-anchor=\"middle\" x=\"109\" y=\"-60.0803\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"188\" cy=\"-20.2803\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-16.5803\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.089,-20.2803C136.659,-20.2803 148.817,-20.2803 159.677,-20.2803\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.959,-23.7804 169.959,-20.2803 159.959,-16.7804 159.959,-23.7804\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-24.0803\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.821,-9.14203C165.757,-3.65931 155.084,1.2803 145,-1.2803 141.042,-2.28533 137.047,-3.83796 133.244,-5.63201\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-2.60875 124.311,-10.4146 134.779,-8.77986 131.475,-2.60875\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-5.0803\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M181.266,-37.3176C179.892,-47.1382 182.137,-56.2803 188,-56.2803 191.665,-56.2803 193.916,-52.7092 194.753,-47.6332\"/><polygon fill=\"black\" stroke=\"black\" points=\"198.252,-47.311 194.734,-37.3176 191.252,-47.3242 198.252,-47.311\"/><text text-anchor=\"middle\" x=\"188\" y=\"-60.0803\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-20.2803C62.6538,-20.2803 72.0513,-20.2803 80.5951,-20.2803\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-23.7804 90.8257,-20.2803 80.8257,-16.7804 80.8257,-23.7804\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 1: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"388pt\" height=\"121pt\" viewBox=\"0.00 0.00 388.00 120.59\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 116.587)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-116.587 384,-116.587 384,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18.5866\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.8866\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57.5866\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-57.5866\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-53.8866\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M125.618,-26.1062C136.095,-31.1509 150.2,-37.942 162.626,-43.9253\"/><polygon fill=\"black\" stroke=\"black\" points=\"161.186,-47.1162 171.714,-48.3009 164.223,-40.8092 161.186,-47.1162\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-41.3866\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title><ellipse fill=\"none\" stroke=\"black\" cx=\"275\" cy=\"-24.5866\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"275\" y=\"-20.8866\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 0&#45;&gt;2 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M126.969,-15.6384C147.586,-12.4726 183.411,-8.31084 214,-11.5866 225.128,-12.7783 237.221,-15.1794 247.616,-17.5973\"/><polygon fill=\"black\" stroke=\"black\" points=\"246.8,-21.001 257.345,-19.9767 248.463,-14.2014 246.8,-21.001\"/><text text-anchor=\"middle\" x=\"192\" y=\"-15.3866\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-78.5774C183.369,-88.6739 185.93,-97.5866 192,-97.5866 195.889,-97.5866 198.337,-93.9288 199.346,-88.6453\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-88.689 199.683,-78.5774 195.85,-88.4546 202.846,-88.689\"/><text text-anchor=\"middle\" x=\"192\" y=\"-101.387\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M212.608,-49.5983C223.399,-45.2018 236.916,-39.695 248.517,-34.9685\"/><polygon fill=\"black\" stroke=\"black\" points=\"250.162,-38.0777 258.103,-31.0633 247.521,-31.595 250.162,-38.0777\"/><text text-anchor=\"middle\" x=\"235.5\" y=\"-44.3866\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M268.266,-41.6239C266.892,-51.4446 269.137,-60.5866 275,-60.5866 278.665,-60.5866 280.916,-57.0155 281.753,-51.9396\"/><polygon fill=\"black\" stroke=\"black\" points=\"285.252,-51.6173 281.734,-41.6239 278.252,-51.6305 285.252,-51.6173\"/><text text-anchor=\"middle\" x=\"275\" y=\"-64.3866\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3 --><g id=\"node4\" class=\"node\"><title>3</title><ellipse fill=\"none\" stroke=\"black\" cx=\"358\" cy=\"-24.5866\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"358\" cy=\"-24.5866\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"358\" y=\"-20.8866\" font-family=\"Times,serif\" font-size=\"14.00\">3</text></g><!-- 2&#45;&gt;3 --><g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M291.184,-33.2468C297.161,-36.1905 304.211,-39.1084 311,-40.5866 317.034,-41.9004 323.369,-41.1624 329.342,-39.4365\"/><polygon fill=\"black\" stroke=\"black\" points=\"330.833,-42.6138 338.935,-35.7868 328.344,-36.0712 330.833,-42.6138\"/><text text-anchor=\"middle\" x=\"314.5\" y=\"-44.3866\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3&#45;&gt;2 --><g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M335.943,-22.2571C328.115,-21.6431 319.156,-21.2378 311,-21.5866 308.441,-21.6961 305.779,-21.8504 303.118,-22.0319\"/><polygon fill=\"black\" stroke=\"black\" points=\"302.763,-18.549 293.071,-22.8291 303.317,-25.5271 302.763,-18.549\"/><text text-anchor=\"middle\" x=\"314.5\" y=\"-25.3866\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3&#45;&gt;2 --><g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M341.383,-10.0167C332.731,-3.71043 321.607,1.58664 311,-1.58664 306.49,-2.936 302.022,-5.07417 297.863,-7.51579\"/><polygon fill=\"black\" stroke=\"black\" points=\"295.757,-4.7128 289.359,-13.1571 299.627,-10.5462 295.757,-4.7128\"/><text text-anchor=\"middle\" x=\"314.5\" y=\"-5.38664\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 4 --><g id=\"node5\" class=\"node\"><title>4</title></g><!-- 4&#45;&gt;0 --><g id=\"edge9\" class=\"edge\"><title>4&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18.5866C62.6538,-18.5866 72.0513,-18.5866 80.5951,-18.5866\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-22.0867 90.8257,-18.5866 80.8257,-15.0867 80.8257,-22.0867\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// hypothesis is still not correct, use (a,bab) to refine it\n",
    "fdfaLearner.refineHypothesis(\"a\", \"bab\")\n",
    "fdfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"293pt\" height=\"168pt\" viewBox=\"0.00 0.00 293.00 168.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 164)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-164 289,-164 289,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-83\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-79.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 2 --><g id=\"node2\" class=\"node\"><title>2</title><ellipse fill=\"none\" stroke=\"black\" cx=\"267\" cy=\"-76\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-72.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 0&#45;&gt;2 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M126.992,-82.2376C153.81,-81.0342 206.21,-78.6829 238.456,-77.2359\"/><polygon fill=\"black\" stroke=\"black\" points=\"238.72,-80.7277 248.553,-76.7829 238.406,-73.7348 238.72,-80.7277\"/><text text-anchor=\"middle\" x=\"188\" y=\"-84.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node3\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"188\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M123.412,-71.6779C135.116,-61.7981 152.298,-47.2935 165.852,-35.8519\"/><polygon fill=\"black\" stroke=\"black\" points=\"168.358,-38.3174 173.741,-29.1924 163.842,-32.9685 168.358,-38.3174\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-56.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M263.584,-93.7817C263.004,-103.315 264.143,-112 267,-112 268.741,-112 269.844,-108.775 270.309,-104.098\"/><polygon fill=\"black\" stroke=\"black\" points=\"273.812,-103.817 270.416,-93.7817 266.812,-103.745 273.812,-103.817\"/><text text-anchor=\"middle\" x=\"267\" y=\"-115.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M261.441,-93.1418C258.17,-110.585 260.023,-130 267,-130 272.614,-130 274.91,-117.428 273.889,-103.429\"/><polygon fill=\"black\" stroke=\"black\" points=\"277.313,-102.61 272.559,-93.1418 270.37,-103.508 277.313,-102.61\"/><text text-anchor=\"middle\" x=\"267\" y=\"-133.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;2 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M202.766,-28.3692C214.192,-36.9759 230.659,-49.3793 243.924,-59.3712\"/><polygon fill=\"black\" stroke=\"black\" points=\"242,-62.304 252.094,-65.525 246.212,-56.7127 242,-62.304\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-52.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M181.266,-35.0373C179.892,-44.8579 182.137,-54 188,-54 191.665,-54 193.916,-50.4289 194.753,-45.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"198.252,-45.0307 194.734,-35.0373 191.252,-45.0439 198.252,-45.0307\"/><text text-anchor=\"middle\" x=\"188\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3 --><g id=\"node4\" class=\"node\"><title>3</title></g><!-- 3&#45;&gt;0 --><g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-83C62.6538,-83 72.0513,-83 80.5951,-83\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-86.5001 90.8257,-83 80.8257,-79.5001 80.8257,-86.5001\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 1: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br><p> Progress FA for 2: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// hypothesis is still not correct, use (ba,b) to refine it\n",
    "fdfaLearner.refineHypothesis(\"ba\", \"b\")\n",
    "fdfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<p> Leading FA M :  </p> <br> <?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"372pt\" height=\"200pt\" viewBox=\"0.00 0.00 372.00 200.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 196)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-196 368,-196 368,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-164\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-160.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 2 --><g id=\"node2\" class=\"node\"><title>2</title><ellipse fill=\"none\" stroke=\"black\" cx=\"346\" cy=\"-105\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"346\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 0&#45;&gt;2 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M126.736,-168.229C158.87,-175.476 230.825,-187.44 285,-165 303.146,-157.484 318.665,-141.522 329.372,-127.95\"/><polygon fill=\"black\" stroke=\"black\" points=\"332.204,-130.008 335.397,-119.906 326.601,-125.812 332.204,-130.008\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-180.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node3\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"188\" cy=\"-105\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M123.766,-153.452C135.192,-144.697 151.659,-132.08 164.924,-121.915\"/><polygon fill=\"black\" stroke=\"black\" points=\"167.285,-124.516 173.094,-115.656 163.027,-118.96 167.285,-124.516\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-140.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M342.584,-122.782C342.004,-132.315 343.143,-141 346,-141 347.741,-141 348.844,-137.775 349.309,-133.098\"/><polygon fill=\"black\" stroke=\"black\" points=\"352.812,-132.817 349.416,-122.782 345.812,-132.745 352.812,-132.817\"/><text text-anchor=\"middle\" x=\"346\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M340.441,-122.142C337.17,-139.585 339.023,-159 346,-159 351.614,-159 353.91,-146.428 352.889,-132.429\"/><polygon fill=\"black\" stroke=\"black\" points=\"356.313,-131.61 351.559,-122.142 349.37,-132.508 356.313,-131.61\"/><text text-anchor=\"middle\" x=\"346\" y=\"-162.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 4 --><g id=\"node4\" class=\"node\"><title>4</title><ellipse fill=\"none\" stroke=\"black\" cx=\"267\" cy=\"-105\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text></g><!-- 1&#45;&gt;4 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;4</title><path fill=\"none\" stroke=\"black\" d=\"M206.089,-105C215.659,-105 227.817,-105 238.677,-105\"/><polygon fill=\"black\" stroke=\"black\" points=\"238.959,-108.5 248.959,-105 238.959,-101.5 238.959,-108.5\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-108.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3 --><g id=\"node5\" class=\"node\"><title>3</title><ellipse fill=\"none\" stroke=\"black\" cx=\"267\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text></g><!-- 1&#45;&gt;3 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M200.695,-91.7866C213.204,-77.6523 233.21,-55.049 247.785,-38.5805\"/><polygon fill=\"black\" stroke=\"black\" points=\"250.441,-40.8607 254.448,-31.0527 245.199,-36.2214 250.441,-40.8607\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-68.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 4&#45;&gt;2 --><g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M285.089,-105C294.659,-105 306.817,-105 317.677,-105\"/><polygon fill=\"black\" stroke=\"black\" points=\"317.959,-108.5 327.959,-105 317.959,-101.5 317.959,-108.5\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-108.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 4&#45;&gt;4 --><g id=\"edge9\" class=\"edge\"><title>4&#45;&gt;4</title><path fill=\"none\" stroke=\"black\" d=\"M260.266,-122.037C258.892,-131.858 261.137,-141 267,-141 270.665,-141 272.916,-137.429 273.753,-132.353\"/><polygon fill=\"black\" stroke=\"black\" points=\"277.252,-132.031 273.734,-122.037 270.252,-132.044 277.252,-132.031\"/><text text-anchor=\"middle\" x=\"267\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3&#45;&gt;2 --><g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M279.695,-31.2134C292.204,-45.3477 312.21,-67.951 326.785,-84.4195\"/><polygon fill=\"black\" stroke=\"black\" points=\"324.199,-86.7786 333.448,-91.9473 329.441,-82.1393 324.199,-86.7786\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-68.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3&#45;&gt;3 --><g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M260.266,-35.0373C258.892,-44.8579 261.137,-54 267,-54 270.665,-54 272.916,-50.4289 273.753,-45.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"277.252,-45.0307 273.734,-35.0373 270.252,-45.0439 277.252,-45.0307\"/><text text-anchor=\"middle\" x=\"267\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 5 --><g id=\"node6\" class=\"node\"><title>5</title></g><!-- 5&#45;&gt;0 --><g id=\"edge11\" class=\"edge\"><title>5&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-164C62.6538,-164 72.0513,-164 80.5951,-164\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-167.5 90.8257,-164 80.8257,-160.5 80.8257,-167.5\"/></g></g></svg><p> Progress FA for 0: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 1: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 2: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"135pt\" height=\"110pt\" viewBox=\"0.00 0.00 135.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 131,-106 131,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-18\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M105.764,-35.7817C105.214,-45.3149 106.293,-54 109,-54 110.65,-54 111.694,-50.7749 112.135,-46.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-45.8156 112.236,-35.7817 108.638,-45.7469 115.638,-45.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-35.4203C100.654,-52.791 102.426,-72 109,-72 114.29,-72 116.471,-59.5617 115.542,-45.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-44.9328 114.316,-35.4203 112.031,-45.7657 118.981,-44.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-18C62.6538,-18 72.0513,-18 80.5951,-18\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-21.5001 90.8257,-18 80.8257,-14.5001 80.8257,-21.5001\"/></g></g></svg><br><p> Progress FA for 3: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;1 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br><p> Progress FA for 4: </p> <br><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?><!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\"><!-- Generated by graphviz version 2.38.0 (20140413.2041) --><!-- Title: %3 Pages: 1 --><svg width=\"222pt\" height=\"85pt\" viewBox=\"0.00 0.00 222.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 218,-81 218,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text></g><!-- 0&#45;&gt;0 --><g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M102.621,-39.0373C101.319,-48.8579 103.445,-58 109,-58 112.472,-58 114.604,-54.4289 115.398,-49.3529\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.897,-49.031 115.379,-39.0373 111.897,-49.0435 118.897,-49.031\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1 --><g id=\"node2\" class=\"node\"><title>1</title><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"192\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"192\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text></g><!-- 0&#45;&gt;1 --><g id=\"edge1\" class=\"edge\"><title>0&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M127.178,-22C136.61,-22 148.601,-22 159.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.811,-25.5001 169.811,-22 159.811,-18.5001 159.811,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M173.925,-9.20141C165.428,-4.3314 154.882,-0.490639 145,-3 141.042,-4.00504 137.047,-5.55766 133.244,-7.35171\"/><polygon fill=\"black\" stroke=\"black\" points=\"131.475,-4.32845 124.311,-12.1343 134.779,-10.4996 131.475,-4.32845\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M184.317,-42.9908C183.369,-53.0872 185.93,-62 192,-62 195.889,-62 198.337,-58.3422 199.346,-53.0587\"/><polygon fill=\"black\" stroke=\"black\" points=\"202.846,-53.1023 199.683,-42.9908 195.85,-52.868 202.846,-53.1023\"/><text text-anchor=\"middle\" x=\"192\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2 --><g id=\"node3\" class=\"node\"><title>2</title></g><!-- 2&#45;&gt;0 --><g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-22C62.6538,-22 72.0513,-22 80.5951,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-25.5001 90.8257,-22 80.8257,-18.5001 80.8257,-25.5001\"/></g></g></svg><br>"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// hypothesis is still not correct, use (aa,a) to refine it\n",
    "fdfaLearner.refineHypothesis(\"aa\", \"a\")\n",
    "fdfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "Invalid counterexample, neither in hypothesis or target\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "null"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// hypothesis is correct, if we use (aa, aba) to refine it, the learner will report error message\n",
    "fdfaLearner.refineHypothesis(\"aa\", \"aba\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Groovy",
   "language": "groovy",
   "name": "groovy"
  },
  "language_info": {
   "codemirror_mode": "groovy",
   "file_extension": ".groovy",
   "mimetype": "",
   "name": "Groovy",
   "nbconverter_exporter": "",
   "version": "2.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}