Add more puzzles and refactor

Bridges_Puzzle.ipynb

@@ -62,7 +62,7 @@
     }
    ],
    "source": [
-    "::load DOT=/usr/bin/dot\n",
+    "::load\n",
     "MACHINE Bridges\n",
     "DEFINITIONS\n",
     " MAXBRIDGES==2;\n",
@@ -240,7 +240,7 @@
     }
    ],
    "source": [
-    "::load DOT=/usr/bin/dot\n",
+    "::load\n",
     "MACHINE Bridges\n",
     "DEFINITIONS\n",
     " MAXBRIDGES==2;\n",
@@ -576,15 +576,6 @@
     ":dot custom_graph"
    ]
   },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    ":dot "
-   ]
-  },
   {
    "cell_type": "code",
    "execution_count": null,

Fibonacci_Numbers.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Fibonacci Numbers with Automatic Dynamic Programming\n",
+    "\n",
+    "In this jupyter notebook, we show you how to encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding.\n",
+    "\n",
+    "First of all we have to load the machine, if you are struggeling with any operation of our jupyter kernel, try out `:help` or take a look at our `ProB Jupyter Noteboook Overview`.\n",
+    "\n",
+    "After loading the machine, we are setting up the constants with `:constants` and initialising it with `:init`.\n",
+    "\n",
+    "Now you can ask the machine for the solution of the `n`th fibonacci number by typing in `sol`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Fibonacci_Dynamic_Programming"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Fibonacci_Dynamic_Programming\n",
+    "/* an encoding of Fibonacci where we get dynamic programming for free from ProB */\n",
+    "DEFINITIONS\n",
+    "  DOM == INTEGER; /* INTEGER : For ProB no restriction necessary; for Kodkod yes */\n",
+    "CONSTANTS n, fib, sol\n",
+    "PROPERTIES\n",
+    "  fib : 0..n --> DOM &\n",
+    "  fib(0) = 1 & fib(1) = 1 &\n",
+    "  !x.(x:2..n => fib(x) = fib(x-1) + fib(x-2))\n",
+    " /* You can change n here: */\n",
+    "  & n = 5 & sol = fib(n)\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": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$5$"
+      ],
+      "text/plain": [
+       "5"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$8$"
+      ],
+      "text/plain": [
+       "8"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "sol"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Please note, that there is an explanation missing for this machine."
+   ]
+  }
+ ],
+ "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
+}

Game_of_Life.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Game of Life\n",
+    "\n",
+    "This is an improved model of Conway’s Game of Life. It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some pre-determined area of the grid. In this notebook we will examine the following machine and animate it.\n",
+    "\n",
+    "To see all the specifications for Conway's Game of Life, click [here](https://en.wikipedia.org/wiki/Conway's_Game_of_Life)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: GameOfLife"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE GameOfLife\n",
+    " /* A simple B model of the Game of Life */\n",
+    " /* by Jens Bendisposto and Michael Leuschel */\n",
+    " /* v2: improved version with more elegant neighbour relation */\n",
+    "ABSTRACT_CONSTANTS neigh\n",
+    "PROPERTIES\n",
+    "  /* neighbour relation: */\n",
+    "  neigh = {x,y,nb | x∈COORD ∧ y∈COORD ∧ (x,y) ≠ nb ∧ \n",
+    "                    prj1(COORD,COORD)(nb) ∈ (x-1)..(x+1) ∧\n",
+    "                    prj2(COORD,COORD)(nb) ∈ (y-1)..(y+1) } \n",
+    "VARIABLES alive\n",
+    "DEFINITIONS \n",
+    "      COORD == INTEGER;\n",
+    "      /* some simple GOL patterns: */\n",
+    "      blinker == {(2,1),(2,2),(2,3)} ; glider == {(1,2),(2,3),(3,1),(3,2),(3,3)} ;\n",
+    "      SET_PREF_CLPFD == TRUE;\n",
+    "      \n",
+    "      /* describing the animation function for the graphical visualization: */\n",
+    "      wmin == min(dom(alive)∪{1}); wmax == max(dom(alive)∪{1});\n",
+    "      hmin == min(ran(alive)∪{1}); hmax == max(ran(alive)∪{1});\n",
+    "      ANIMATION_FUNCTION_DEFAULT == ( (wmin..wmax)*(hmin..hmax)*{0}  );\n",
+    "      ANIMATION_FUNCTION == ( alive * {1} );\n",
+    "      ANIMATION_RIGHT_CLICK(I,J) == BEGIN step END;\n",
+    "      ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/sm_gray_box.gif\"\n",
+    "INVARIANT\n",
+    "    alive ⊆ COORD * COORD ∧ alive ≠ ∅\n",
+    "INITIALISATION \n",
+    "\talive := glider\n",
+    "OPERATIONS \n",
+    " step  =  alive := { uv1 |  uv1∈alive ∧ card(neigh[{uv1}] ∩ alive) = 2 }\n",
+    "                   ∪\n",
+    "                   { uv2 |  uv2∈neigh[alive] ∧ /* restrict enumeration to neighbours */\n",
+    "                            card(neigh[{uv2}] ∩ alive)=3 }\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: step()"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec step"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: step()"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec step"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: step()"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec step"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_gray_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 15,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "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
+}

SEND-MORE-MONEY.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# SEND-MORE-MONEY\n",
+    "\n",
+    "In this jupyter notebook, we will study how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.\n",
+    "The quickest way is to use the ProB Logic Calculator, which is implemented in Jupyter notebook. To solve the puzzle, simply type in: \n",
+    "`{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y` and press enter:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{R} = 8$\n",
+       "* $\\mathit{S} = 9$\n",
+       "* $\\mathit{D} = 7$\n",
+       "* $\\mathit{E} = 5$\n",
+       "* $\\mathit{Y} = 2$\n",
+       "* $\\mathit{M} = 1$\n",
+       "* $\\mathit{N} = 6$\n",
+       "* $\\mathit{O} = 0$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tR = 8\n",
+       "\tS = 9\n",
+       "\tD = 7\n",
+       "\tE = 5\n",
+       "\tY = 2\n",
+       "\tM = 1\n",
+       "\tN = 6\n",
+       "\tO = 0"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Explanation\n",
+    "\n",
+    "Now let us review the individual conjuncts of the B encoding of the puzzle: The following specifies that S,E,N,D,M,O,R,Y are all digits. \n",
+    "\n",
+    "Note that `<:` is the subset operator in B:\n",
+    "`{S,E,N,D, M,O,R, Y} <: 0..9`\n",
+    "\n",
+    "An alternative, slightly longer, encoding would have been to write:\n",
+    "`S:0..9 & E:0..9 & N:0..9 & D:0..9 & M:0..9 & O:0..9 & R:0..9 & Y:0..9`\n",
+    "\n",
+    "The following conjunct specifies that the S and M cannot be 0:\n",
+    "`S>0 & M>0`\n",
+    "\n",
+    "The next conjunct specifies that all digits are distinct:\n",
+    "`card({S,E,N,D, M,O,R, Y})=8`\n",
+    "\n",
+    "Note that an alternative, but much longer encoding would have been to specify inequalities:\n",
+    "`S /= E & S /= N & S /= D & … & R/=Y`\n",
+    "\n",
+    "Finally, the last conjunct expresses the sum constraint:\n",
+    "`S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y`"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Alternative Solutions\n",
+    "\n",
+    "We are still not sure if this is the only solution. One way to ensure this is to compute a set comprehension with all solutions:\n",
+    "\n",
+    "`{S,E,N,D,M,O,R,Y|{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y}`\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(9\\mapsto 5\\mapsto 6\\mapsto 7\\mapsto 1\\mapsto 0\\mapsto 8\\mapsto 2)\\}$"
+      ],
+      "text/plain": [
+       "{(9↦5↦6↦7↦1↦0↦8↦2)}"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "{S,E,N,D,M,O,R,Y|{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Wrapping predicate into B machine\n",
+    "\n",
+    "Another alternative is to wrap the predicate into a full B machine with the following content:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: SendMoreMoney"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE SendMoreMoney\n",
+    "CONSTANTS S,E,N,D, M,O,R, Y\n",
+    "PROPERTIES\n",
+    "   {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &\n",
+    "   card({S,E,N,D, M,O,R, Y}) = 8 &\n",
+    "   S*1000 + E*100 + N*10 + D +\n",
+    "   M*1000 + O*100 + R*10 + E =\n",
+    "   M*10000 + O*1000 + N*100 + E*10 + Y\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "To run this example, you will need to setup the constants and initialise the machine with the following commands:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "To see the result, we will create the following table:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|S|E|N|D|M|O|R|Y|\n",
+       "|---|---|---|---|---|---|---|---|\n",
+       "|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|\n"
+      ],
+      "text/plain": [
+       "S\tE\tN\tD\tM\tO\tR\tY\n",
+       "9\t5\t6\t7\t1\t0\t8\t2\n"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table (S,E,N,D, M,O,R, Y)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## KISS * KISS = PASSION\n",
+    "\n",
+    "A similar puzzle, this times involving multiplication is the KISS * KISS = PASSION puzzle. \n",
+    "Here we again have distinct digits K, I, S, P, A, O, N such that the square of KISS equals the decimal number passion. \n",
+    "The puzzle can be described and solved in a fashion very similar to the problem above:\n",
+    "\n",
+    "`{K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7`"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "To make sure, that we don't use the variables from our machine loaded above, we reset our machine to be empty:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: empty"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE empty\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{P} = 4$\n",
+       "* $\\mathit{A} = 1$\n",
+       "* $\\mathit{S} = 3$\n",
+       "* $\\mathit{I} = 0$\n",
+       "* $\\mathit{K} = 2$\n",
+       "* $\\mathit{N} = 9$\n",
+       "* $\\mathit{O} = 8$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tP = 4\n",
+       "\tA = 1\n",
+       "\tS = 3\n",
+       "\tI = 0\n",
+       "\tK = 2\n",
+       "\tN = 9\n",
+       "\tO = 8"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "{K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
+   ]
+  }
+ ],
+ "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
+}