diff --git a/Bridges_Puzzle.ipynb b/Bridges_Puzzle.ipynb
index 162ac4db1d8561cb987e95e4f6f083868794a9f8..e5c9e46384f6c94510ad3be0bb20c44848078501 100644
--- a/Bridges_Puzzle.ipynb
+++ b/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,
diff --git a/Die_Hard_Jugs.ipynb b/Die_Hard_Jugs.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..a6a4c704a746895e8961488bf55880fa0acc986d
--- /dev/null
+++ b/Die_Hard_Jugs.ipynb
@@ -0,0 +1,875 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Die Hard Jugs Puzzle\n",
+ "\n",
+ "This is the B model of a puzzle from the movie \"Die Hard with a Vengeance\". [This clip](https://www.youtube.com/watch?v=BVtQNK_ZUJg) shows Bruce Willis and Samuel Jackson having a go at the puzzle. A more detailed explanation can be found [here](https://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm). \n",
+ "At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs."
+ ]
+ },
+ {
+ "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",
+ "SETS 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": [
+ "## Trace for solution\n",
+ "\n",
+ "In the following, we will see the trace for the solution of the puzzle. "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: FillJar(j5)"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec FillJar j=j5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Transfer(j5,3,j3)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Transfer j1=j5 & amount=3 & j2=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: EmptyJar(j3)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec EmptyJar j=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Transfer(j5,2,j3)"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Transfer j1=j5 & amount=2 & j2=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: FillJar(j5)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec FillJar j=j5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Transfer(j5,1,j3)"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Transfer j1=j5 & amount=1 & j2=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "* -1: Root state\n",
+ "* 0: `SETUP_CONSTANTS()`\n",
+ "* 1: `INITIALISATION()`\n",
+ "* 2: `FillJar(j5)`\n",
+ "* 3: `Transfer(j5,3,j3)`\n",
+ "* 4: `EmptyJar(j3)`\n",
+ "* 5: `Transfer(j5,2,j3)`\n",
+ "* 6: `FillJar(j5)`\n",
+ "* 7: `Transfer(j5,1,j3)` **(current)**"
+ ],
+ "text/plain": [
+ "-1: Root state\n",
+ "0: SETUP_CONSTANTS()\n",
+ "1: INITIALISATION()\n",
+ "2: FillJar(j5)\n",
+ "3: Transfer(j5,3,j3)\n",
+ "4: EmptyJar(j3)\n",
+ "5: Transfer(j5,2,j3)\n",
+ "6: FillJar(j5)\n",
+ "7: Transfer(j5,1,j3) (current)"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":trace"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|prj1|prj2|\n",
+ "|---|---|\n",
+ "|$\\{(\\mathit{j3}\\mapsto 3),(\\mathit{j5}\\mapsto 5)\\}$|$\\{(\\mathit{j3}\\mapsto 3),(\\mathit{j5}\\mapsto 4)\\}$|\n"
+ ],
+ "text/plain": [
+ "prj1\tprj2\n",
+ "{(j3|->3),(j5|->5)}\t{(j3|->3),(j5|->4)}\n"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table (maxf, level)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Graphical Animation\n",
+ "\n",
+ "Like some of the other jupyter notebook examples, this machine can be animated with the `ANIMATION_FUNCTION`. To do that, we have to add the following lines into the `DEFINTION` section of the machine:\n",
+ "```\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) & (ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}\n",
+ "```\n",
+ "After that, we can just load the machine as usual."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jars"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jars\n",
+ "DEFINITIONS\n",
+ " GOAL == (4 : ran(level));\n",
+ " \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",
+ " \n",
+ "SETS 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": "markdown",
+ "metadata": {},
+ "source": [
+ "Now that we loaded the machine, we have to initiate the machine. To run the animation, you can use the commant `:show`. This will make it easier to understand the trace we have seen before:\n",
+ "\n",
+ "! If you run into any difficulties with the setup for the graphical animation, please consider reading our \"ProB Jupyter Notebook Overview\" notebook for more information."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "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=\"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=\"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",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: FillJar(j5)"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec FillJar j=j5"
+ ]
+ },
+ {
+ "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": "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": 19,
+ "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": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: EmptyJar(j3)"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec EmptyJar j=j3"
+ ]
+ },
+ {
+ "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=\"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": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Transfer(j5,2,j3)"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Transfer j1=j5 & amount=2 & j2=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "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": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: FillJar(j5)"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec FillJar j=j5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "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": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Transfer(j5,1,j3)"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Transfer j1=j5 & amount=1 & j2=j3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "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": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "As you can see, the right jar (that holds 5 gallons) contains exactly 4 gallons of water. With this we precisely measured 4 gallons of water and found a solution for the puzzle."
+ ]
+ },
+ {
+ "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/Fibonacci_Numbers.ipynb b/Fibonacci_Numbers.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..a20c1c7bf573c436990d703164a5e4eac3e8f1c8
--- /dev/null
+++ b/Fibonacci_Numbers.ipynb
@@ -0,0 +1,159 @@
+{
+ "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
+}
diff --git a/Game_of_Life.ipynb b/Game_of_Life.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..0fa9ee89dec082d642c0d5e2d23e41103d2e201f
--- /dev/null
+++ b/Game_of_Life.ipynb
@@ -0,0 +1,367 @@
+{
+ "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
+}
diff --git a/N_Queens.ipynb b/N-Queens.ipynb
similarity index 100%
rename from N_Queens.ipynb
rename to N-Queens.ipynb
diff --git a/SEND-MORE-MONEY.ipynb b/SEND-MORE-MONEY.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..d1492127b8db3df81cbf1ca826a1ced84d33108a
--- /dev/null
+++ b/SEND-MORE-MONEY.ipynb
@@ -0,0 +1,335 @@
+{
+ "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
+}
diff --git a/images/Empty.gif b/images/Empty.gif
new file mode 100644
index 0000000000000000000000000000000000000000..9a4a394a9e9a2ad18c7bd11a6ce8aa83e9cba5c8
Binary files /dev/null and b/images/Empty.gif differ
diff --git a/images/Filled.gif b/images/Filled.gif
new file mode 100644
index 0000000000000000000000000000000000000000..2d3b77c5e697bfd0fff23e8ea54d405ffd94c5c3
Binary files /dev/null and b/images/Filled.gif differ
diff --git a/images/Void.gif b/images/Void.gif
new file mode 100644
index 0000000000000000000000000000000000000000..1fa01cf4b9a958096a702c5c8fa09e21895d1cc0
Binary files /dev/null and b/images/Void.gif differ