NFALearning.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# NFA 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 regular language  $L =\\Sigma^* b \\Sigma \\Sigma$ over the alphabet $\\Sigma = \\{a, b\\}$ by means of nondeterministic finite automata (NFAs).\n",
    "The NFA learning algorithm used here is called NL$^*$ which was introduced by Benedikt Bollig, Peter Habermehl, Carsten Kern, and Martin Leucker in their paper titled \"Angluin-Style Learning of NFA\".\n",
    "This algorithm uses an observation table to store the membership query results and makes use of a notion called \"prime rows\" corresponding to a state in the conjectured NFAs.\n",
    "We refer the reader to that paper for more details on NL$^*$ learning algorithm.\n",
    "\n",
    "The first way is to use embedded [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 regular language $L$ from DK by giving a target NFA $N$**"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "we first need to create the target NFA $N$ which accepts the regular language $L$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[0->a, 1->b]"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import roll.words.Alphabet\n",
    "import roll.automata.DFA\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",
    "// use JupyterROLL to create an NFA object N\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",
    "N = JupyterROLL.createNFA();\n",
    "\n",
    "// now we can get the alphabet in the DFA\n",
    "alphabet = N.getAlphabet();"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<?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=\"380pt\" height=\"114pt\" viewBox=\"0.00 0.00 380.00 114.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 110)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-110 376,-110 376,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=\"M105.764,-39.7817C105.214,-49.3149 106.293,-58 109,-58 110.65,-58 111.694,-54.7749 112.135,-50.0981\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-49.8156 112.236,-39.7817 108.638,-49.7469 115.638,-49.8156\"/><text text-anchor=\"middle\" x=\"109\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-39.4203C100.654,-56.791 102.426,-76 109,-76 114.29,-76 116.471,-63.5617 115.542,-49.652\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-48.9328 114.316,-39.4203 112.031,-49.7657 118.981,-48.9328\"/><text text-anchor=\"middle\" x=\"109\" y=\"-79.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=\"188\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" 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.089,-22C136.659,-22 148.817,-22 159.677,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"159.959,-25.5001 169.959,-22 159.959,-18.5001 159.959,-25.5001\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-25.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=\"267\" cy=\"-22\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 1&#45;&gt;2 --><g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M206.089,-22C215.659,-22 227.817,-22 238.677,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"238.959,-25.5001 248.959,-22 238.959,-18.5001 238.959,-25.5001\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M203.311,-12.1343C209.402,-8.50652 216.763,-4.83778 224,-3 230.618,-1.31961 237.489,-2.86929 243.71,-5.6828\"/><polygon fill=\"black\" stroke=\"black\" points=\"242.397,-8.9626 252.821,-10.8617 245.857,-2.87709 242.397,-8.9626\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-6.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3 --><g id=\"node4\" class=\"node\"><title>3</title><ellipse fill=\"none\" stroke=\"black\" cx=\"350\" cy=\"-22\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"350\" cy=\"-22\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"350\" y=\"-18.3\" 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=\"M285.178,-22C294.61,-22 306.601,-22 317.637,-22\"/><polygon fill=\"black\" stroke=\"black\" points=\"317.811,-25.5001 327.811,-22 317.811,-18.5001 317.811,-25.5001\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;3 --><g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M282.311,-12.1343C288.402,-8.50652 295.763,-4.83778 303,-3 309.485,-1.35323 316.256,-2.44123 322.546,-4.7602\"/><polygon fill=\"black\" stroke=\"black\" points=\"321.389,-8.0849 331.925,-9.20141 324.385,-1.75835 321.389,-8.0849\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-6.8\" 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=\"edge8\" class=\"edge\"><title>4&#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>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// now we are ready to create the NFA which accepts the regular language L\n",
    "// we first create 4 states\n",
    "N.createState();\n",
    "N.createState();\n",
    "N.createState();\n",
    "N.createState();\n",
    "\n",
    "\n",
    "// 4 indices for the states\n",
    "int fst = 0, snd = 1, thd = 2, fur = 3;\n",
    "// the function getState is to get a state object by its state index\n",
    "N.getState(fst).addTransition(alphabet.indexOf((char)'a'), fst); // 0 -> 0 via a\n",
    "N.getState(fst).addTransition(alphabet.indexOf((char)'b'), fst); // 0 -> 0 via b\n",
    "N.getState(fst).addTransition(alphabet.indexOf((char)'b'), snd); // 0 -> 1 via b\n",
    "N.getState(snd).addTransition(alphabet.indexOf((char)'a'), thd); // 1 -> 2 via a\n",
    "N.getState(snd).addTransition(alphabet.indexOf((char)'b'), thd); // 1 -> 2 via b\n",
    "N.getState(thd).addTransition(alphabet.indexOf((char)'a'), fur); // 2 -> 3 via a\n",
    "N.getState(thd).addTransition(alphabet.indexOf((char)'b'), fur); // 2 -> 3 via b\n",
    "\n",
    "// set 0 as the initial state\n",
    "N.setInitial(fst);\n",
    "// set 3 as a final state\n",
    "N.setFinal(fur);\n",
    "\n",
    "// now we can output target in a DOT graph\n",
    "N"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we are ready to create an NFA learner to learn a hypothesis NFA $A$ from DK. The NFA $A$ accepts the regular language $L$ and happens to have the minimal number of states.\n",
    "\n",
    "In the following, we will demostrate how to use the learning algorithm to learn the target language $L$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 7,
     "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 data structure, the second is the current hypothesis NFA, and the third is the counterexample\n",
    "// which refines the previous hypothesis NFA to the current hypothesis\n",
    "sequence = JupyterROLL.learningSeq(\"nlstar\", \"table\", N);\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 with only 2 equivalence queries.\n",
    "\n",
    "we now can check the Triple object at each step of the learning procedure. **The prime rows in the observation table have been labeled by \"\\*\" in the front**."
   ]
  },
  {
   "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>    || ϵ | \n",
       "==========\n",
       "* ϵ || - | \n",
       "==========\n",
       "* a || - | \n",
       "* b || - | \n",
       "</pre></td>\n",
       "    <td><center><?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></center></td>\n",
       "    <td><center></center></td>\n",
       "  </tr>\n",
       "</table>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// initial learner data\n",
    "sequence.get(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "scrolled": true
   },
   "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>       || ϵ | baa | aa | a | \n",
       "============================\n",
       "* ϵ    || - | +   | -  | - | \n",
       "* b    || - | +   | +  | - | \n",
       "* ba   || - | +   | -  | + | \n",
       "* baa  || + | +   | -  | - | \n",
       "============================\n",
       "* a    || - | +   | -  | - | \n",
       "  bb   || - | +   | +  | + | \n",
       "  bab  || + | +   | +  | - | \n",
       "* baaa || - | +   | -  | - | \n",
       "* baab || - | +   | +  | - | \n",
       "</pre></td>\n",
       "    <td><center><?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=\"380pt\" height=\"223pt\" viewBox=\"0.00 0.00 380.00 223.48\" 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 219.484)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-219.484 376,-219.484 376,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-79.4837\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.7837\" 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,-97.2654C105.214,-106.799 106.293,-115.484 109,-115.484 110.65,-115.484 111.694,-112.259 112.135,-107.582\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-107.299 112.236,-97.2654 108.638,-107.231 115.638,-107.299\"/><text text-anchor=\"middle\" x=\"109\" y=\"-119.284\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-96.904C100.654,-114.275 102.426,-133.484 109,-133.484 114.29,-133.484 116.471,-121.045 115.542,-107.136\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-106.417 114.316,-96.904 112.031,-107.249 118.981,-106.417\"/><text text-anchor=\"middle\" x=\"109\" y=\"-137.284\" 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=\"188\" cy=\"-79.4837\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-75.7837\" 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=\"M119.417,-64.721C125.582,-56.5 134.442,-47.0297 145,-42.4837 155.738,-37.86 165.66,-45.7546 173.161,-55.4223\"/><polygon fill=\"black\" stroke=\"black\" points=\"170.313,-57.4586 178.857,-63.7243 176.085,-53.4983 170.313,-57.4586\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-46.2837\" 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=\"M172.557,-89.5004C164.603,-93.8526 154.454,-97.5422 145,-95.4837 141.499,-94.7215 137.929,-93.5765 134.473,-92.2426\"/><polygon fill=\"black\" stroke=\"black\" points=\"135.746,-88.9786 125.184,-88.1439 132.92,-95.3829 135.746,-88.9786\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-99.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M169.929,-77.7262C164.234,-77.2184 157.849,-76.7339 152,-76.4837 147.271,-76.2814 142.247,-76.3734 137.38,-76.6237\"/><polygon fill=\"black\" stroke=\"black\" points=\"136.87,-73.1515 127.152,-77.3718 137.381,-80.1329 136.87,-73.1515\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-80.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M181.266,-96.521C179.892,-106.342 182.137,-115.484 188,-115.484 191.665,-115.484 193.916,-111.913 194.753,-106.837\"/><polygon fill=\"black\" stroke=\"black\" points=\"198.252,-106.514 194.734,-96.521 191.252,-106.528 198.252,-106.514\"/><text text-anchor=\"middle\" x=\"188\" y=\"-119.284\" 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=\"267\" cy=\"-108.484\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-104.784\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 1&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M205.33,-85.6339C215.505,-89.466 228.814,-94.4784 240.373,-98.8319\"/><polygon fill=\"black\" stroke=\"black\" points=\"239.366,-102.193 249.958,-102.442 241.833,-95.6419 239.366,-102.193\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-98.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M205.052,-73.339C213.095,-71.2082 222.834,-70.1012 231,-73.4837 237.828,-76.3118 244.018,-81.1897 249.228,-86.421\"/><polygon fill=\"black\" stroke=\"black\" points=\"246.85,-89.0127 256.122,-94.1407 252.072,-84.3504 246.85,-89.0127\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-77.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;0 --><g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M263.321,-126.44C259.524,-145.324 250.701,-174.475 231,-190.484 209.889,-207.639 197.07,-198.164 170,-195.484 158.724,-194.367 153.433,-198.052 145,-190.484 121.709,-169.583 113.789,-133.345 111.166,-107.977\"/><polygon fill=\"black\" stroke=\"black\" points=\"114.642,-107.528 110.337,-97.847 107.665,-108.099 114.642,-107.528\"/><text text-anchor=\"middle\" x=\"188\" y=\"-204.284\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;0 --><g id=\"edge12\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M252.789,-119.766C246.533,-124.607 238.745,-129.951 231,-133.484 206.214,-144.788 195.168,-149.909 170,-139.484 151.854,-131.967 136.335,-116.006 125.628,-102.434\"/><polygon fill=\"black\" stroke=\"black\" points=\"128.399,-100.295 119.603,-94.3895 122.796,-104.492 128.399,-100.295\"/><text text-anchor=\"middle\" x=\"188\" y=\"-148.284\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;1 --><g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M249.544,-114.116C241.58,-115.934 232.029,-116.742 224,-113.484 217.355,-110.787 211.277,-106.156 206.118,-101.165\"/><polygon fill=\"black\" stroke=\"black\" points=\"208.628,-98.7238 199.258,-93.7774 203.498,-103.487 208.628,-98.7238\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-118.284\" 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=\"350\" cy=\"-37.4837\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"350\" cy=\"-37.4837\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"350\" y=\"-33.7837\" font-family=\"Times,serif\" font-size=\"14.00\">3</text></g><!-- 2&#45;&gt;3 --><g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M279.458,-95.2647C286.051,-87.9491 294.66,-78.8705 303,-71.4837 309.273,-65.9282 316.407,-60.3414 323.155,-55.3474\"/><polygon fill=\"black\" stroke=\"black\" points=\"325.347,-58.0813 331.4,-49.3857 321.245,-52.4088 325.347,-58.0813\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-75.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;3 --><g id=\"edge13\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M284.112,-101.968C292.357,-98.1765 302.258,-92.8802 310,-86.4837 317.756,-80.0757 325,-71.8984 331.089,-64.068\"/><polygon fill=\"black\" stroke=\"black\" points=\"334.069,-65.9251 337.213,-55.8074 328.446,-61.7564 334.069,-65.9251\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-94.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3&#45;&gt;0 --><g id=\"edge14\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M328.671,-32.0757C290.54,-23.0624 206.58,-8.64115 145,-37.4837 136.721,-41.3612 129.718,-48.2658 124.202,-55.3711\"/><polygon fill=\"black\" stroke=\"black\" points=\"121.286,-53.4341 118.423,-63.6348 127.022,-57.4459 121.286,-53.4341\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-25.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3&#45;&gt;0 --><g id=\"edge16\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M330.279,-26.7133C306.125,-14.0758 262.616,4.45115 224,-1.48372 186.878,-7.18892 173.479,-6.99844 145,-31.4837 136.99,-38.3703 129.787,-47.4297 124.028,-55.821\"/><polygon fill=\"black\" stroke=\"black\" points=\"121.093,-53.9135 118.575,-64.2047 126.961,-57.7303 121.093,-53.9135\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-5.28372\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3&#45;&gt;1 --><g id=\"edge15\" class=\"edge\"><title>3&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M328.107,-42.2511C303.202,-48.0292 260.379,-58.2665 224,-68.4837 221.126,-69.291 218.13,-70.1715 215.155,-71.0713\"/><polygon fill=\"black\" stroke=\"black\" points=\"213.831,-67.8175 205.319,-74.1264 215.907,-74.5024 213.831,-67.8175\"/><text text-anchor=\"middle\" x=\"267\" y=\"-65.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 4 --><g id=\"node5\" class=\"node\"><title>4</title></g><!-- 4&#45;&gt;0 --><g id=\"edge17\" class=\"edge\"><title>4&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-79.4837C62.6538,-79.4837 72.0513,-79.4837 80.5951,-79.4837\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-82.9838 90.8257,-79.4837 80.8257,-75.9838 80.8257,-82.9838\"/></g></g></svg></center></td>\n",
       "    <td><center>$baa$</center></td>\n",
       "  </tr>\n",
       "</table>"
      ]
     },
     "execution_count": 9,
     "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 a NFA A from DK out of a given NFA N. Sometimes we may not have the target NFA 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 learning algorithm to show how to learn the NFA A from ourselves.\n",
    "\n",
    "**2. Learning the regular language $L$ in an interactive way**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<pre>    || ϵ | \n",
       "==========\n",
       "* ϵ || - | \n",
       "==========\n",
       "* a || - | \n",
       "* b || - | \n",
       "</pre>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import roll.jupyter.*;\n",
    "import java.util.function.Function;\n",
    "import roll.words.*;\n",
    "\n",
    "// now we define a function :: 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",
    "    s -> \n",
    "    // b is the third last letter\n",
    "    int num = s.length();\n",
    "    if(num < 3) {\n",
    "        return false;\n",
    "    }\n",
    "    // check the third last letter\n",
    "    if (s.charAt(num - 3) == 'b') {\n",
    "        return true;\n",
    "    }\n",
    "    return false;\n",
    "};\n",
    "\n",
    "// now we create an NFA learner to learn the target language \n",
    "nfaLearner = JupyterROLL.createNFALearner(\"nlstar\", \"table\", mqOracle);\n",
    "// we can also see the data structure of the learner in a DOT graph\n",
    "nfaLearner"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<?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>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// output current hypothesis to see whether it recognizes the target language\n",
    "nfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<?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=\"380pt\" height=\"223pt\" viewBox=\"0.00 0.00 380.00 223.48\" 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 219.484)\"><title>%3</title><polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-219.484 376,-219.484 376,4 -4,4\"/><!-- 0 --><g id=\"node1\" class=\"node\"><title>0</title><ellipse fill=\"none\" stroke=\"black\" cx=\"109\" cy=\"-79.4837\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"109\" y=\"-75.7837\" 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,-97.2654C105.214,-106.799 106.293,-115.484 109,-115.484 110.65,-115.484 111.694,-112.259 112.135,-107.582\"/><polygon fill=\"black\" stroke=\"black\" points=\"115.638,-107.299 112.236,-97.2654 108.638,-107.231 115.638,-107.299\"/><text text-anchor=\"middle\" x=\"109\" y=\"-119.284\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 0&#45;&gt;0 --><g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M103.684,-96.904C100.654,-114.275 102.426,-133.484 109,-133.484 114.29,-133.484 116.471,-121.045 115.542,-107.136\"/><polygon fill=\"black\" stroke=\"black\" points=\"118.981,-106.417 114.316,-96.904 112.031,-107.249 118.981,-106.417\"/><text text-anchor=\"middle\" x=\"109\" y=\"-137.284\" 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=\"188\" cy=\"-79.4837\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"188\" y=\"-75.7837\" 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=\"M119.417,-64.721C125.582,-56.5 134.442,-47.0297 145,-42.4837 155.738,-37.86 165.66,-45.7546 173.161,-55.4223\"/><polygon fill=\"black\" stroke=\"black\" points=\"170.313,-57.4586 178.857,-63.7243 176.085,-53.4983 170.313,-57.4586\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-46.2837\" 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=\"M172.557,-89.5004C164.603,-93.8526 154.454,-97.5422 145,-95.4837 141.499,-94.7215 137.929,-93.5765 134.473,-92.2426\"/><polygon fill=\"black\" stroke=\"black\" points=\"135.746,-88.9786 125.184,-88.1439 132.92,-95.3829 135.746,-88.9786\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-99.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;0 --><g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M169.929,-77.7262C164.234,-77.2184 157.849,-76.7339 152,-76.4837 147.271,-76.2814 142.247,-76.3734 137.38,-76.6237\"/><polygon fill=\"black\" stroke=\"black\" points=\"136.87,-73.1515 127.152,-77.3718 137.381,-80.1329 136.87,-73.1515\"/><text text-anchor=\"middle\" x=\"148.5\" y=\"-80.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 1&#45;&gt;1 --><g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M181.266,-96.521C179.892,-106.342 182.137,-115.484 188,-115.484 191.665,-115.484 193.916,-111.913 194.753,-106.837\"/><polygon fill=\"black\" stroke=\"black\" points=\"198.252,-106.514 194.734,-96.521 191.252,-106.528 198.252,-106.514\"/><text text-anchor=\"middle\" x=\"188\" y=\"-119.284\" 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=\"267\" cy=\"-108.484\" rx=\"18\" ry=\"18\"/><text text-anchor=\"middle\" x=\"267\" y=\"-104.784\" font-family=\"Times,serif\" font-size=\"14.00\">2</text></g><!-- 1&#45;&gt;2 --><g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M205.33,-85.6339C215.505,-89.466 228.814,-94.4784 240.373,-98.8319\"/><polygon fill=\"black\" stroke=\"black\" points=\"239.366,-102.193 249.958,-102.442 241.833,-95.6419 239.366,-102.193\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-98.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 1&#45;&gt;2 --><g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;2</title><path fill=\"none\" stroke=\"black\" d=\"M205.052,-73.339C213.095,-71.2082 222.834,-70.1012 231,-73.4837 237.828,-76.3118 244.018,-81.1897 249.228,-86.421\"/><polygon fill=\"black\" stroke=\"black\" points=\"246.85,-89.0127 256.122,-94.1407 252.072,-84.3504 246.85,-89.0127\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-77.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;0 --><g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M263.321,-126.44C259.524,-145.324 250.701,-174.475 231,-190.484 209.889,-207.639 197.07,-198.164 170,-195.484 158.724,-194.367 153.433,-198.052 145,-190.484 121.709,-169.583 113.789,-133.345 111.166,-107.977\"/><polygon fill=\"black\" stroke=\"black\" points=\"114.642,-107.528 110.337,-97.847 107.665,-108.099 114.642,-107.528\"/><text text-anchor=\"middle\" x=\"188\" y=\"-204.284\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;0 --><g id=\"edge12\" class=\"edge\"><title>2&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M252.789,-119.766C246.533,-124.607 238.745,-129.951 231,-133.484 206.214,-144.788 195.168,-149.909 170,-139.484 151.854,-131.967 136.335,-116.006 125.628,-102.434\"/><polygon fill=\"black\" stroke=\"black\" points=\"128.399,-100.295 119.603,-94.3895 122.796,-104.492 128.399,-100.295\"/><text text-anchor=\"middle\" x=\"188\" y=\"-148.284\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 2&#45;&gt;1 --><g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M249.544,-114.116C241.58,-115.934 232.029,-116.742 224,-113.484 217.355,-110.787 211.277,-106.156 206.118,-101.165\"/><polygon fill=\"black\" stroke=\"black\" points=\"208.628,-98.7238 199.258,-93.7774 203.498,-103.487 208.628,-98.7238\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-118.284\" 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=\"350\" cy=\"-37.4837\" rx=\"18\" ry=\"18\"/><ellipse fill=\"none\" stroke=\"black\" cx=\"350\" cy=\"-37.4837\" rx=\"22\" ry=\"22\"/><text text-anchor=\"middle\" x=\"350\" y=\"-33.7837\" font-family=\"Times,serif\" font-size=\"14.00\">3</text></g><!-- 2&#45;&gt;3 --><g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M279.458,-95.2647C286.051,-87.9491 294.66,-78.8705 303,-71.4837 309.273,-65.9282 316.407,-60.3414 323.155,-55.3474\"/><polygon fill=\"black\" stroke=\"black\" points=\"325.347,-58.0813 331.4,-49.3857 321.245,-52.4088 325.347,-58.0813\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-75.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 2&#45;&gt;3 --><g id=\"edge13\" class=\"edge\"><title>2&#45;&gt;3</title><path fill=\"none\" stroke=\"black\" d=\"M284.112,-101.968C292.357,-98.1765 302.258,-92.8802 310,-86.4837 317.756,-80.0757 325,-71.8984 331.089,-64.068\"/><polygon fill=\"black\" stroke=\"black\" points=\"334.069,-65.9251 337.213,-55.8074 328.446,-61.7564 334.069,-65.9251\"/><text text-anchor=\"middle\" x=\"306.5\" y=\"-94.2837\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3&#45;&gt;0 --><g id=\"edge14\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M328.671,-32.0757C290.54,-23.0624 206.58,-8.64115 145,-37.4837 136.721,-41.3612 129.718,-48.2658 124.202,-55.3711\"/><polygon fill=\"black\" stroke=\"black\" points=\"121.286,-53.4341 118.423,-63.6348 127.022,-57.4459 121.286,-53.4341\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-25.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 3&#45;&gt;0 --><g id=\"edge16\" class=\"edge\"><title>3&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M330.279,-26.7133C306.125,-14.0758 262.616,4.45115 224,-1.48372 186.878,-7.18892 173.479,-6.99844 145,-31.4837 136.99,-38.3703 129.787,-47.4297 124.028,-55.821\"/><polygon fill=\"black\" stroke=\"black\" points=\"121.093,-53.9135 118.575,-64.2047 126.961,-57.7303 121.093,-53.9135\"/><text text-anchor=\"middle\" x=\"227.5\" y=\"-5.28372\" font-family=\"Times,serif\" font-size=\"14.00\">a</text></g><!-- 3&#45;&gt;1 --><g id=\"edge15\" class=\"edge\"><title>3&#45;&gt;1</title><path fill=\"none\" stroke=\"black\" d=\"M328.107,-42.2511C303.202,-48.0292 260.379,-58.2665 224,-68.4837 221.126,-69.291 218.13,-70.1715 215.155,-71.0713\"/><polygon fill=\"black\" stroke=\"black\" points=\"213.831,-67.8175 205.319,-74.1264 215.907,-74.5024 213.831,-67.8175\"/><text text-anchor=\"middle\" x=\"267\" y=\"-65.2837\" font-family=\"Times,serif\" font-size=\"14.00\">b</text></g><!-- 4 --><g id=\"node5\" class=\"node\"><title>4</title></g><!-- 4&#45;&gt;0 --><g id=\"edge17\" class=\"edge\"><title>4&#45;&gt;0</title><path fill=\"none\" stroke=\"black\" d=\"M54.195,-79.4837C62.6538,-79.4837 72.0513,-79.4837 80.5951,-79.4837\"/><polygon fill=\"black\" stroke=\"black\" points=\"80.8257,-82.9838 90.8257,-79.4837 80.8257,-75.9838 80.8257,-82.9838\"/></g></g></svg>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// the hypothesis is no correct and we can use a counterexample\n",
    "// which is in the symmetric difference of the language of A and the target language\n",
    "// here we use baa\n",
    "nfaLearner.refineHypothesis(\"baa\")\n",
    "// this hypothesis is the correct NFA\n",
    "nfaLearner.getHypothesis()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<pre>       || ϵ | baa | aa | a | \n",
       "============================\n",
       "* ϵ    || - | +   | -  | - | \n",
       "* b    || - | +   | +  | - | \n",
       "* ba   || - | +   | -  | + | \n",
       "* baa  || + | +   | -  | - | \n",
       "============================\n",
       "* a    || - | +   | -  | - | \n",
       "  bb   || - | +   | +  | + | \n",
       "  bab  || + | +   | +  | - | \n",
       "* baaa || - | +   | -  | - | \n",
       "* baab || - | +   | +  | - | \n",
       "</pre>"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// we can output the current observation table \n",
    "nfaLearner"
   ]
  },
  {
   "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
}