{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Jars\n",
    "\n",
    "This is the B model of a puzzle from the movie \"Die Hard with a Vengeance\":\n",
    " https://www.youtube.com/watch?v=BVtQNK_ZUJg\n",
    " http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm\n",
    " \n",
    "Input:\n",
    "* one 3 gallon and one 5 gallon jug\n",
    "* and we need to measure precisely 4 gallons\n",
    "We can \n",
    "* empty a jug,\n",
    "* completely fill any jug and\n",
    "* transfer water from one jug to another until either the destination jug is full or the source jug is empty.\n",
    "\n",
    "Here is a generic B model with three operations ```FillJar```, ```EmptyJar``` and ```Transfer```.\n",
    "It hase one variable ```level``` for the current level of the jars.\n",
    "The constant ```maxf``` defines for each jar the maximum fill level in gallons."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Jars"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE Jars\n",
    "DEFINITIONS\n",
    "  GOAL == (4:ran(level));\n",
    "  ANIMATION_IMG1 == \"images/Filled.gif\";\n",
    "  ANIMATION_IMG2 == \"images/Empty.gif\";\n",
    "  ANIMATION_IMG3 == \"images/Void.gif\";\n",
    "  gmax == max(ran(maxf));\n",
    "  ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};\n",
    "  ri == (gmax+1-r);\n",
    "  ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &\n",
    "                                 (ri<=level(c) => i=1 ) & (ri>level(c) => i=2)};\n",
    "SETS\n",
    " Jars = {j3,j5}\n",
    "CONSTANTS maxf\n",
    "PROPERTIES maxf : Jars --> NATURAL &\n",
    "           maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */\n",
    "VARIABLES level\n",
    "INVARIANT\n",
    "  level: Jars --> NATURAL\n",
    "INITIALISATION level := Jars * {0}  /* all jars start out empty */\n",
    "OPERATIONS\n",
    "  FillJar(j) = /* we can completely fill a jar j */\n",
    "   PRE j:Jars & level(j)<maxf(j) THEN\n",
    "    level(j) := maxf(j)\n",
    "   END;\n",
    "  EmptyJar(j) = /* we can completely empty a jar j */\n",
    "   PRE j:Jars & level(j)>0 THEN\n",
    "    level(j) := 0\n",
    "   END;\n",
    "  Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */\n",
    "   PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &\n",
    "                               amount = min({level(j1), maxf(j2)-level(j2)}) THEN\n",
    "      level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }\n",
    "   END\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We start off with all jars being empty:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{(\\mathit{j3}\\mapsto 0),(\\mathit{j5}\\mapsto 0)\\}$"
      ],
      "text/plain": [
       "{(j3↦0),(j5↦0)}"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "level"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We now fill the 5 gallon jar using the operation FillJar with parameter j:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: FillJar(j5)"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec FillJar j=j5"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This jar is now full:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{(\\mathit{j3}\\mapsto 0),(\\mathit{j5}\\mapsto 5)\\}$"
      ],
      "text/plain": [
       "{(j3↦0),(j5↦5)}"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "level"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can inspect the state graphically using the defined ANIMATION_FUNCTION:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We now transfer water to the empty jar until it is filled using the operation FillJar with parameters j1, amount and j2:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Transfer(j5,3,j3)"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Transfer (j1=j5 & amount=3 & j2=j3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{(\\mathit{j3}\\mapsto 3),(\\mathit{j5}\\mapsto 2)\\}$"
      ],
      "text/plain": [
       "{(j3↦3),(j5↦2)}"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "level"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We now empty the three gallon jar using the operation EmptyJar with parameter j:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: EmptyJar(j3)"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec EmptyJar j=j3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Transfer(j5,2,j3)"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Transfer (j1=j5 & amount=2 & j2=j3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: FillJar(j5)"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec FillJar j=j5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Transfer(j5,1,j3)"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Transfer j1=j5 & amount=1 & j2=j3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/Empty.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/Void.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/Filled.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The puzzle has now been solve, the goal predicate has become true:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "GOAL"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Title: g Pages: 1 -->\n",
       "<svg width=\"304pt\" height=\"110pt\"\n",
       " viewBox=\"0.00 0.00 304.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
       "<title>g</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 300,-106 300,4 -4,4\"/>\n",
       "<!-- Noderoot -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>Noderoot</title>\n",
       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">∈</text>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
       "</g>\n",
       "<!-- Node1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>Node1</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
       "<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
       "</g>\n",
       "<!-- Node1&#45;&gt;Noderoot -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>Node1&#45;&gt;Noderoot</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-74.499C81.796,-71.7653 72.6401,-68.7134 63.905,-65.8017\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.8886,-62.4403 54.295,-62.5983 62.675,-69.0811 64.8886,-62.4403\"/>\n",
       "</g>\n",
       "<!-- Node2 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>Node2</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-.5 90,-46.5 144,-46.5 144,-.5 90,-.5\"/>\n",
       "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">ran</text>\n",
       "<polyline fill=\"none\" stroke=\"#000000\" points=\"90,-23.5 144,-23.5 \"/>\n",
       "<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{3,4}</text>\n",
       "</g>\n",
       "<!-- Node2&#45;&gt;Noderoot -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>Node2&#45;&gt;Noderoot</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-32.501C81.796,-35.2347 72.6401,-38.2866 63.905,-41.1983\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.675,-37.9189 54.295,-44.4017 64.8886,-44.5597 62.675,-37.9189\"/>\n",
       "</g>\n",
       "<!-- Node3 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>Node3</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-.5 180,-46.5 296,-46.5 296,-.5 180,-.5\"/>\n",
       "<text text-anchor=\"middle\" x=\"238\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">level</text>\n",
       "<polyline fill=\"none\" stroke=\"#000000\" points=\"180,-23.5 296,-23.5 \"/>\n",
       "<text text-anchor=\"middle\" x=\"238\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(j3↦3),(j5↦4)}</text>\n",
       "</g>\n",
       "<!-- Node3&#45;&gt;Node2 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>Node3&#45;&gt;Node2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M179.9808,-23.5C171.2934,-23.5 162.5376,-23.5 154.4316,-23.5\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.2102,-20.0001 144.2101,-23.5 154.2101,-27.0001 154.2102,-20.0001\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: goal []>"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot goal"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "ProB 2",
   "language": "prob",
   "name": "prob2"
  },
  "language_info": {
   "codemirror_mode": "prob2_jupyter_repl",
   "file_extension": ".prob",
   "mimetype": "text/x-prob2-jupyter-repl",
   "name": "prob"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}