From 4c968736cb83fa7fe10999bf5b31f916d835d661 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Wed, 9 Oct 2019 14:15:31 +0200
Subject: [PATCH] Add another model reference example

---
 notebooks/models/Jars_DieHard_Puzzle.ipynb | 756 +++++++++++++++++++++
 notebooks/models/images/Empty.gif          | Bin 0 -> 1345 bytes
 notebooks/models/images/Filled.gif         | Bin 0 -> 1166 bytes
 notebooks/models/images/Void.gif           | Bin 0 -> 947 bytes
 4 files changed, 756 insertions(+)
 create mode 100644 notebooks/models/Jars_DieHard_Puzzle.ipynb
 create mode 100644 notebooks/models/images/Empty.gif
 create mode 100644 notebooks/models/images/Filled.gif
 create mode 100644 notebooks/models/images/Void.gif

diff --git a/notebooks/models/Jars_DieHard_Puzzle.ipynb b/notebooks/models/Jars_DieHard_Puzzle.ipynb
new file mode 100644
index 0000000..14fdacc
--- /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
GIT binary patch
literal 1345
zcmZ?wbhEHboWNkq@SVZ%|HuZ(=l+jmB*4Hhk`V&~gAM}&0|O{8FmU{5VC0ao2$<^F
z6w1NpvqFHuxs_kgti;0b(V;F0=_rvM6BixpVc=Oc%VX1ngOfCZSH+y%wDk0JCf7qE
zH#e$zbjlYy?Wqh@KR4H|T5HPBNg8Jsdra1vTX|_|V86rSe{-~^Xt~b|Z%&&U75XB0
zTKx1bS?_Hbm#3L*blSRW+v~7xW?Q$_zAno<u{q)6w7aLbzrQ;%jq$Q<j=5g=p|*#s
zeBXqwKeeGw**i^3Vy)w`4)N@1-8(-#Ti6%uG|y+3$;pcv^ULD?MjAf9Rw}<p&+_(`
z+)G>4m(`yAz2W)2b+zT^?oRme_HlKua0sup@rN5{>$%M%E%QsC+)&nDe(u-K&oA#S
zW&a;9XI1+1&5NUX{gvCSe|&$uu-$ymzx-dnYhJ%^)1UwU`;Y%$-S3t5&uzcoI89I^
zs`}zi_5~G8Zab#du_<LNtmI01v7kkO?L}g{LePwdtt#`v5(|0GU4PJ}^-V3Q(_o#-
zqc-_V9E*An&*iw)VR-C^QoF^b7x#M={@!>z(K<*hrQ2E0a>+ywH_oM#`GYv0qzAZF
zKIw4^yZLnL!_<{a`>pt1s7_8d(_AtmdD;opSqZB+pSS01t9&>m{@M)niF(sK=gy7(
zb#k6o*egr*`Tks4@(WTvt%&X_a+~#R$=|CdHR|%cq|}$TslC$ZnjhCCGp}8&OJjLJ
zq?T6I%tcwRR$pAHwo9vQN!G2EtE*2f%c$M#b?w!%1NWqII(BQ_T3vQDj4gZR&ZNjV
H2L@{ZUv}Cq

literal 0
HcmV?d00001

diff --git a/notebooks/models/images/Filled.gif b/notebooks/models/images/Filled.gif
new file mode 100644
index 0000000000000000000000000000000000000000..2d3b77c5e697bfd0fff23e8ea54d405ffd94c5c3
GIT binary patch
literal 1166
zcmZ?wbhEHboWNkq@SVZ%|HuZ04F5+m5@28$$%ui0L5G2XfdP~k7&!hjFmlLP1WY}s
z#UZQ}b7I57!|ejfUUNJ)E^-WIG0xJd*s$n$zk+kul8VB`o_(v_R>hp$^z_gqb>FxW
z&&|txI}DPu=2UK8?mykKROrdi%_{=?9b36ns<x~QZu6XKRO_`hGh|`#>a4Goq3PGw
zCS;cN{xn?^IW^gTn(gUt$x$<9Z=d4*S@!tW&I;LUcO}i&$IoG#nzrZn_xJY>)^cn6
zRa9g=I@%?@xW#8@*OR6F+Ryj$G;Dabd5&#8pS0EI7u%Kw&-*sJ%JlVtCiUINZdZM~
zb8B1R;l8^!OY+w4sGrTNC!_Q6(Sh>gV!eN!e|+XY-+BA07=zC*&6XzXud21a{wk=p
zy7>Lg+M2Qt5l3gQkF2u|_!4(@cmB<~f2V$ZbANQ+U)(P8=bz3k@eLk7my0#9>`GOL
zS*5CRt*K1$g@UKRr>hTIba*=y6C^%fyWJ}NDqJy1q3uR|`<~eJMRCejVUN047wwqS
ZV&HUjQI2WTlEglaw<jJ)FfuY&0{}1rECT=l

literal 0
HcmV?d00001

diff --git a/notebooks/models/images/Void.gif b/notebooks/models/images/Void.gif
new file mode 100644
index 0000000000000000000000000000000000000000..1fa01cf4b9a958096a702c5c8fa09e21895d1cc0
GIT binary patch
literal 947
zcmZ?wbhEHboWNkq@SVZ%|0oy@fsq;l3=9l93=9kmpuE7qF@xbRr;Nvj1qYisgtcN$
zY*=`>T|n7uj>pDDN4q7Av+kVOxcGR#f^(OQ=cXkmCu;<+iaEJy>FMbP$*1OcZeDhF
zwng!)J0~|UKR@50nM>Ad%ZiJOJtk|#p4zhV^74SiUUR*+uDZH9VsqBrQ(ISGU!QQe
zOV)eanwy(5F0YC`y>0F7?FEld&Gp{C?(Xi2&#&&D-oF0+{sv}lIiDK|4h+@+@v2ih

literal 0
HcmV?d00001

-- 
GitLab