diff --git a/notebooks/models/Jars_DieHard_Puzzle.ipynb b/notebooks/models/Jars_DieHard_Puzzle.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..14fdacc1d51558814e5c45e432a9347fcc23806d
--- /dev/null
+++ b/notebooks/models/Jars_DieHard_Puzzle.ipynb
@@ -0,0 +1,756 @@
+{
+ "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": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Jars"
+      ]
+     },
+     "execution_count": 11,
+     "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": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 13,
+     "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": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{j3}\\mapsto 0),(\\mathit{j5}\\mapsto 0)\\}$"
+      ],
+      "text/plain": [
+       "{(j3↦0),(j5↦0)}"
+      ]
+     },
+     "execution_count": 14,
+     "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": 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": "markdown",
+   "metadata": {},
+   "source": [
+    "This jar is now full:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{j3}\\mapsto 0),(\\mathit{j5}\\mapsto 5)\\}$"
+      ],
+      "text/plain": [
+       "{(j3↦0),(j5↦5)}"
+      ]
+     },
+     "execution_count": 16,
+     "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": 17,
+   "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": 17,
+     "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": 18,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Transfer(j5,3,j3)"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Transfer (j1=j5 & amount=3 & j2=j3)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{j3}\\mapsto 3),(\\mathit{j5}\\mapsto 2)\\}$"
+      ],
+      "text/plain": [
+       "{(j3↦3),(j5↦2)}"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "level"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "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": 21,
+     "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": 23,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: EmptyJar(j3)"
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec EmptyJar j=j3"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "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": 24,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Transfer(j5,2,j3)"
+      ]
+     },
+     "execution_count": 25,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Transfer (j1=j5 & amount=2 & j2=j3)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "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": 26,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: FillJar(j5)"
+      ]
+     },
+     "execution_count": 27,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec FillJar j=j5"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "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": 28,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 29,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Transfer(j5,1,j3)"
+      ]
+     },
+     "execution_count": 29,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Transfer j1=j5 & amount=1 & j2=j3"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 30,
+   "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": 30,
+     "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": 31,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 31,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "GOAL"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 33,
+   "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.28.0 (20110509.1545)\n",
+       " -->\n",
+       "<!-- Title: g Pages: 1 -->\n",
+       "<svg width=\"304pt\" height=\"113pt\"\n",
+       " viewBox=\"0.00 0.00 304.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 109)\">\n",
+       "<title>g</title>\n",
+       "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-109 301,-109 301,5 -4,5\"/>\n",
+       "<!-- Noderoot -->\n",
+       "<g id=\"node1\" class=\"node\"><title>Noderoot</title>\n",
+       "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"42,-76.6019 12,-76.6019 0,-64.6019 0,-47.3981 12,-35.3981 42,-35.3981 54,-47.3981 54,-64.6019 42,-76.6019\"/>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M12,-76.6019C6,-76.6019 0,-70.6019 0,-64.6019\"/>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M0,-47.3981C0,-41.3981 6,-35.3981 12,-35.3981\"/>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M42,-35.3981C48,-35.3981 54,-41.3981 54,-47.3981\"/>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M54,-64.6019C54,-70.6019 48,-76.6019 42,-76.6019\"/>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"42,-76.6019 12,-76.6019 \"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M12,-76.6019C6,-76.6019 0,-70.6019 0,-64.6019\"/>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"0,-64.6019 0,-47.3981 \"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M0,-47.3981C0,-41.3981 6,-35.3981 12,-35.3981\"/>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"12,-35.3981 42,-35.3981 \"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M42,-35.3981C48,-35.3981 54,-41.3981 54,-47.3981\"/>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"54,-47.3981 54,-64.6019 \"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M54,-64.6019C54,-70.6019 48,-76.6019 42,-76.6019\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-60.2\" font-family=\"Times,serif\" font-size=\"14.00\">∈</text>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-43.4\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
+       "</g>\n",
+       "<!-- Node1 -->\n",
+       "<g id=\"node2\" class=\"node\"><title>Node1</title>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"90,-69 90,-105 144,-105 144,-69 90,-69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-82.9\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- Node1&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge2\" class=\"edge\"><title>Node1&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.5971,-77.699C81.4311,-74.8223 72.297,-71.6046 63.6152,-68.5463\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"64.6758,-65.2091 54.081,-65.1876 62.35,-71.8114 64.6758,-65.2091\"/>\n",
+       "</g>\n",
+       "<!-- Node2 -->\n",
+       "<g id=\"node4\" class=\"node\"><title>Node2</title>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.2 90,-49.8 144,-49.8 144,-0.2 90,-0.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-33.2\" font-family=\"Times,serif\" font-size=\"14.00\">ran</text>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"90,-25 144,-25 \"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-8.4\" font-family=\"Times,serif\" font-size=\"14.00\">{3,4}</text>\n",
+       "</g>\n",
+       "<!-- Node2&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge4\" class=\"edge\"><title>Node2&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.5971,-34.301C81.4311,-37.1777 72.297,-40.3954 63.6152,-43.4537\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.35,-40.1886 54.081,-46.8124 64.6758,-46.7909 62.35,-40.1886\"/>\n",
+       "</g>\n",
+       "<!-- Node3 -->\n",
+       "<g id=\"node6\" class=\"node\"><title>Node3</title>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"180.32,-0.2 180.32,-49.8 295.68,-49.8 295.68,-0.2 180.32,-0.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"238\" y=\"-33.2\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
+       "<polyline fill=\"none\" stroke=\"black\" points=\"180.32,-25 295.68,-25 \"/>\n",
+       "<text text-anchor=\"middle\" x=\"238\" y=\"-8.4\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
+       "</g>\n",
+       "<!-- Node3&#45;&gt;Node2 -->\n",
+       "<g id=\"edge6\" class=\"edge\"><title>Node3&#45;&gt;Node2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M180.288,-25C171.365,-25 162.358,-25 154.072,-25\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"154.023,-21.5001 144.023,-25 154.023,-28.5001 154.023,-21.5001\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<Dot visualization: goal []>"
+      ]
+     },
+     "execution_count": 33,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":dot goal"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "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
+}
diff --git a/notebooks/models/images/Empty.gif b/notebooks/models/images/Empty.gif
new file mode 100644
index 0000000000000000000000000000000000000000..9a4a394a9e9a2ad18c7bd11a6ce8aa83e9cba5c8
Binary files /dev/null and b/notebooks/models/images/Empty.gif differ
diff --git a/notebooks/models/images/Filled.gif b/notebooks/models/images/Filled.gif
new file mode 100644
index 0000000000000000000000000000000000000000..2d3b77c5e697bfd0fff23e8ea54d405ffd94c5c3
Binary files /dev/null and b/notebooks/models/images/Filled.gif differ
diff --git a/notebooks/models/images/Void.gif b/notebooks/models/images/Void.gif
new file mode 100644
index 0000000000000000000000000000000000000000..1fa01cf4b9a958096a702c5c8fa09e21895d1cc0
Binary files /dev/null and b/notebooks/models/images/Void.gif differ