Add N-Bishops

468fc17e · penguinn · ce057a5e · 468fc17e · 468fc17e · 468fc17e
Commit 468fc17e authored 5 years ago by penguinn
--- a/Apples_and_Oranges.ipynb
+++ b/Apples_and_Oranges.ipynb
@@ -266,11 +266,25 @@
   ]
  },
  {
-   "cell_type": "code",
-   "execution_count": null,
+   "cell_type": "markdown",
   "metadata": {},
-   "outputs": [],
-   "source": []
+   "source": [
+    "## Argumentation Theory\n",
+    "\n",
+    "\n",
+    "\n",
+    "Below we try to model some concepts of argumentation theory in B. The examples try to show that classical (monotonic) logic with set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory. Alternative solutions are encoding arguments as normal logic programs (with non-monotonic negation) and using answer set solvers for problem solving.\n",
+    "\n",
+    "The following model was inspired by a talk given by Claudia Schulz.\n",
+    "\n",
+    "The model below represents the labelling of the arguments as a total function from arguments to its status, which can either be in (the argument is accepted), out (the argument is rejected), or undec (the argument is undecided). The relation between the arguments is given in the binary attacks relation.\n",
+    "\n",
+    "In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a summary page about the B syntax in our handbook):\n",
+    "\n",
+    "* `x : S` specifies that x is an element of S\n",
+    "* `a|→b` represents the pair (a,b); note that a relation and function in B is a set of pairs.\n",
+    "* "
+   ]
  }
 ],
 "metadata": {

 %% Cell type:markdown id: tags:

 # Apples and Oranges

 Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.

 This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from
 [1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the
 following information:

 * (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.
 * (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.
 * (3) Opening just one box, and without looking in the box, you take out one piece of fruit.
 * (4) By looking at the fruit, how can you immediately label all of the boxes correctly?

 Here is one encoding of this puzzle in B:

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE ApplesOranges
 SETS
 Fruit={apple,orange}; // possible content for the boxes
 Label={A,O,Both} // labels for the boxes
 CONSTANTS a,o,b,  // a,o,b are the three boxes
          Take,  // which box should we open (the label of that box)
          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
 PROPERTIES
  a = {apple} & o={orange} & b={apple,orange} // (1)
  &
  Take : Label //3
  &
  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
  !label. ( // the decision function has to work for all allowed labelings
  ( label : {a,o,b} >->> Label &
    label(a) /= A & label(o) /= O & label(b) /= Both // (2)
  )
   =>
  !f.(f: label~(Take)
      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
     )
  )
 END
 ```

 %% Output

    Loaded machine: ApplesOranges

 %% Cell type:markdown id: tags:

 We have abstracted the box of apples `a` by the set containing `apple`.
 Ditto for `o` and `b`, which are abstracted by `{orange}` and
 `{apple,orange}` respectively.

 NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.

 `:goto Number` jumps to the state with the given number.

 With the `:trace` command, you will get the information of your current trace.

 There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`.

 This model gives you just one solution, after setting up the constants with `:constants`.

 %% Cell type:code id: tags:

 ``` prob
 :goto -1
 ```

 %% Output

    Changed to state with index -1

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state **(current)**
    -1: Root state (current)

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 Take
 ```

 %% Output

    $\mathit{Both}$
    Both

 %% Cell type:markdown id: tags:

 As we can see, the only solution is to open the box labelled with
 "Both". We can inspect the decision function by using the jupyter notebook code block, like follows:

 %% Cell type:code id: tags:

 ``` prob
 DecisionFunction(apple)
 ```

 %% Output

    $\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$
    {(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}

 %% Cell type:code id: tags:

 ``` prob
 DecisionFunction(orange)
 ```

 %% Output

    $\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$
    {(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}

 %% Cell type:markdown id: tags:

 In other words, when we pick an apple out of the box labelled with
 "Both", then it contains only apples and the box labelled "O"ranges
 contains both apples and oranges. The box labelled "A"pples contains
 just oranges. Similarly, if we pick up an orange out of the box labelled
 with "Both", then it contains only oranges and the box labelled with
 "A"pples contains contains both apples and oranges. The box labelled
 "O"ranges contains just apples.

 NOTE: You can use `:table Expression` to get values or expressions in a tabular form.

 %% Cell type:code id: tags:

 ``` prob
 :table DecisionFunction
 ```

 %% Output

    |prj1|prj2|
    |---|---|
    |$\mathit{apple}$|$\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$|
    |$\mathit{orange}$|$\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$|
    prj1	prj2
    apple	{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
    orange	{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}

-%% Cell type:code id: tags:
+%% Cell type:markdown id: tags:

-``` prob
-```
+## Argumentation Theory
+
+
+
+Below we try to model some concepts of argumentation theory in B. The examples try to show that classical (monotonic) logic with set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory. Alternative solutions are encoding arguments as normal logic programs (with non-monotonic negation) and using answer set solvers for problem solving.
+
+The following model was inspired by a talk given by Claudia Schulz.
+
+The model below represents the labelling of the arguments as a total function from arguments to its status, which can either be in (the argument is accepted), out (the argument is rejected), or undec (the argument is undecided). The relation between the arguments is given in the binary attacks relation.
+
+In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a summary page about the B syntax in our handbook):
+
+* `x : S` specifies that x is an element of S
+* `a|→b` represents the pair (a,b); note that a relation and function in B is a set of pairs.
+*

--- a/N-Bishops.ipynb
+++ b/N-Bishops.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# N-Bishops Puzzle\n",
+    "\n",
+    "\n",
+    "This puzzle is a variation of the N-Queens puzzle. You can find the N-Queens puzzle in our modeling examples as well. In this puzzle we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function `1..n >-> 1..n`. \n",
+    "\n",
+    "There are two encodings shown below. The first and following represents the bishops as a subset of the Cartesian product `(1..n)*(1..n)`, i.e., a set of positions (aka a binary relation on `1..n`).\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`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: NBishopsSets"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE NBishopsSets\n",
+    "CONSTANTS n, nbishops, hasbishop\n",
+    "PROPERTIES\n",
+    " n=8 &\n",
+    " hasbishop <: (1..n)*(1..n) &\n",
+    " !(i,j).(i:1..n & j:1..n\n",
+    "    =>\n",
+    "    ( (i,j): hasbishop\n",
+    "       =>\n",
+    "        (!k.(k:(i+1)..n =>\n",
+    "           (k,j+k-i) /: hasbishop &\n",
+    "           (k,j-k+i) /: hasbishop\n",
+    "        ))\n",
+    "    ))\n",
+    " & nbishops = card(hasbishop)\n",
+    " & nbishops >13\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "One can try and find the maximum number of bishops by gradually\n",
+    "increasing the lower limit for nbishops in the last line of the model\n",
+    "before the final END. The maximum number of bishops that can be placed\n",
+    "is 2*n - 2; see [here](http://mathworld.wolfram.com/BishopsProblem.html).\n",
+    "\n",
+    "To show this graphically, we will now include the ANIMATION_FUNCTION for this example. The ANIMATION_FUNCTION has to be declared in the `DEFINITIONS` section as follows:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: NBishopsSets"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE NBishopsSets\n",
+    "DEFINITIONS\n",
+    "      BWOFFSET(x,y) == (x+y) mod 2;\n",
+    "      ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 }  );\n",
+    "      ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ;\n",
+    "      ANIMATION_IMG0 == \"images/ChessPieces/Chess_emptyl45.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/ChessPieces/Chess_emptyd45.gif\";\n",
+    "      ANIMATION_IMG2 == \"images/ChessPieces/Chess_bll45.gif\";\n",
+    "      ANIMATION_IMG3 == \"images/ChessPieces/Chess_bld45.gif\";\n",
+    "     SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1;\n",
+    "CONSTANTS n, nbishops, hasbishop\n",
+    "PROPERTIES\n",
+    " n=8 &\n",
+    " hasbishop <: (1..n)*(1..n) &\n",
+    " !(i,j).(i:1..n & j:1..n\n",
+    "    =>\n",
+    "    ( (i,j): hasbishop\n",
+    "       =>\n",
+    "        (!k.(k:(i+1)..n =>\n",
+    "           (k,j+k-i) /: hasbishop &\n",
+    "           (k,j-k+i) /: hasbishop\n",
+    "        ))\n",
+    "    ))\n",
+    " & nbishops = card(hasbishop)\n",
+    " & nbishops >13\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We will now initialise the machine and run the default setting to take a look at the animation."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "With the `:show` command from the jupyter kernel you can see the results of the N-Queens problem for yourself.\n",
+    "\n",
+    "Please note, that the image paths given in the DEFINITIONS have to be relative to the jupyter notebook."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
+       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "For the chess pieces we have used the images available at [this site](https://commons.wikimedia.org/wiki/Category:SVG_chess_pieces). These images are available under the [Creative Commons](https://en.wikipedia.org/wiki/Creative_Commons)\n",
+    "[Attribution-Share Alike 3.0 Unported license](https://creativecommons.org/licenses/by-sa/3.0/deed.en). The same applies to the screenshots shown here."
+   ]
+  },
+  {
+   "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
+}
+%% Cell type:markdown id: tags:
+
+# N-Bishops Puzzle
+
+
+This puzzle is a variation of the N-Queens puzzle. You can find the N-Queens puzzle in our modeling examples as well. In this puzzle we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function `1..n >-> 1..n`.
+
+There are two encodings shown below. The first and following represents the bishops as a subset of the Cartesian product `(1..n)*(1..n)`, i.e., a set of positions (aka a binary relation on `1..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`.
+
+%% Cell type:code id: tags:
+
+``` prob
+::load
+MACHINE NBishopsSets
+CONSTANTS n, nbishops, hasbishop
+PROPERTIES
+ n=8 &
+ hasbishop <: (1..n)*(1..n) &
+ !(i,j).(i:1..n & j:1..n
+    =>
+    ( (i,j): hasbishop
+       =>
+        (!k.(k:(i+1)..n =>
+           (k,j+k-i) /: hasbishop &
+           (k,j-k+i) /: hasbishop
+        ))
+    ))
+ & nbishops = card(hasbishop)
+ & nbishops >13
+END
+```
+
+%% Output
+
+    Loaded machine: NBishopsSets
+
+%% Cell type:markdown id: tags:
+
+One can try and find the maximum number of bishops by gradually
+increasing the lower limit for nbishops in the last line of the model
+before the final END. The maximum number of bishops that can be placed
+is 2*n - 2; see [here](http://mathworld.wolfram.com/BishopsProblem.html).
+
+To show this graphically, we will now include the ANIMATION_FUNCTION for this example. The ANIMATION_FUNCTION has to be declared in the `DEFINITIONS` section as follows:
+
+%% Cell type:code id: tags:
+
+``` prob
+::load
+MACHINE NBishopsSets
+DEFINITIONS
+      BWOFFSET(x,y) == (x+y) mod 2;
+      ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 }  );
+      ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ;
+      ANIMATION_IMG0 == "images/ChessPieces/Chess_emptyl45.gif";
+      ANIMATION_IMG1 == "images/ChessPieces/Chess_emptyd45.gif";
+      ANIMATION_IMG2 == "images/ChessPieces/Chess_bll45.gif";
+      ANIMATION_IMG3 == "images/ChessPieces/Chess_bld45.gif";
+     SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1;
+CONSTANTS n, nbishops, hasbishop
+PROPERTIES
+ n=8 &
+ hasbishop <: (1..n)*(1..n) &
+ !(i,j).(i:1..n & j:1..n
+    =>
+    ( (i,j): hasbishop
+       =>
+        (!k.(k:(i+1)..n =>
+           (k,j+k-i) /: hasbishop &
+           (k,j-k+i) /: hasbishop
+        ))
+    ))
+ & nbishops = card(hasbishop)
+ & nbishops >13
+END
+```
+
+%% Output
+
+    Loaded machine: NBishopsSets
+
+%% Cell type:markdown id: tags:
+
+We will now initialise the machine and run the default setting to take a look at the animation.
+
+%% Cell type:code id: tags:
+
+``` prob
+:constants
+```
+
+%% Output
+
+    Machine constants set up using operation 0: $setup_constants()
+
+%% Cell type:code id: tags:
+
+``` prob
+:init
+```
+
+%% Output
+
+    Machine initialised using operation 1: $initialise_machine()
+
+%% Cell type:markdown id: tags:
+
+With the `:show` command from the jupyter kernel you can see the results of the N-Queens problem for yourself.
+
+Please note, that the image paths given in the DEFINITIONS have to be relative to the jupyter notebook.
+
+%% Cell type:code id: tags:
+
+``` prob
+:show
+```
+
+%% Output
+
+    <table style="font-family:monospace"><tbody>
+    <tr>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    </tr>
+    <tr>
+    <td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
+    <td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
+    <td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
+    </tr>
+    </tbody></table>
+    <Animation function visualisation>
+
+%% Cell type:markdown id: tags:
+
+For the chess pieces we have used the images available at [this site](https://commons.wikimedia.org/wiki/Category:SVG_chess_pieces). These images are available under the [Creative Commons](https://en.wikipedia.org/wiki/Creative_Commons)
+[Attribution-Share Alike 3.0 Unported license](https://creativecommons.org/licenses/by-sa/3.0/deed.en). The same applies to the screenshots shown here.
+
+%% Cell type:code id: tags:
+
+``` prob
+```
--- a/ProB_Jupyter_Notebook_Overview.ipynb
+++ b/ProB_Jupyter_Notebook_Overview.ipynb
@@ -6,7 +6,7 @@
   "source": [
    "# ProB2 Jupyter Notebook Overview\n",
    "\n",
-    "In this jupyter notebook we want to give you an overview over the functionalities of the ProB2 Jupyter Notebook.\n",
+    "In this jupyter notebook, we will give you an extended overview of the functionalities that come with the ProB2 jupyter kernel.\n",
    "For this purpose, we will take a look at the simple machine `Lift.mch` taken from the [ProB Public Examples](https://www3.hhu.de/stups/downloads/prob/source/)."
   ]
  },

 %% Cell type:markdown id: tags:

 # ProB2 Jupyter Notebook Overview

-In this jupyter notebook we want to give you an overview over the functionalities of the ProB2 Jupyter Notebook.
+In this jupyter notebook, we will give you an extended overview of the functionalities that come with the ProB2 jupyter kernel.
 For this purpose, we will take a look at the simple machine `Lift.mch` taken from the [ProB Public Examples](https://www3.hhu.de/stups/downloads/prob/source/).

 %% Cell type:markdown id: tags:

 ## The Help Command

 If you want to find out more about the commands and how to use them, type in `:help [COMMAND]`. The ProB2 Jupyter Notebook has an autocompletion function which also helps you to find what you need. Simply press `TAB` after the space after `:help`.

 %% Cell type:code id: tags:

 ``` prob
 :help :help
 ```

 %% Output

    ```
    :help [COMMAND]
    ```
    
    Display help for a specific command, or general help about the REPL.
    :help [COMMAND]
    Display help for a specific command, or general help about the REPL.

 %% Cell type:markdown id: tags:

 ## Loading a Machine

 To start of with the ProB Jupyter Kernel, we have to load a machine. This can be done by typing `::load` in a Code cell before the machine code and pressing `Shift+Enter`.

 %% Cell type:code id: tags:

 ``` prob
 :help ::load
 ```

 %% Output

    ```
    ::load [PREF=VALUE ...]
    MACHINE
    ...
    END
    ```
    
    Load the machine source code given in the cell body.
    
    There must be a newline between the `::load` command name and the machine code.
    
    Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.
    ::load [PREF=VALUE ...]
    MACHINE
    ...
    END
    Load the machine source code given in the cell body.
    
    There must be a newline between the `::load` command name and the machine code.
    
    Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.

 %% Cell type:code id: tags:

 ``` prob
 ::load DOT=/usr/bin/dot
 MODEL Lift
 DEFINITIONS SET_PREF_SHOW_EVENTB_ANY_VALUES==TRUE;
  ASSERT_LTL == "G( [push_call_button(groundf)] => F {cur_floor=groundf & door_open=TRUE})";
  Rconv == (topf-r+groundf);
 CONSTANTS groundf,topf
 PROPERTIES
  topf : INTEGER & groundf : INTEGER & (groundf = -1) & (topf = 2) & (groundf < topf)
 VARIABLES call_buttons,cur_floor,direction_up,door_open
 INVARIANT
       cur_floor : (groundf .. topf) &
       door_open : BOOL &
       call_buttons : POW(groundf .. topf) &
       direction_up : BOOL &
       (door_open = TRUE => cur_floor : call_buttons)
 INITIALISATION cur_floor := (groundf) || door_open := FALSE || call_buttons := ({}) || direction_up := TRUE
 OPERATIONS
 move_up = SELECT door_open = FALSE & cur_floor < topf & direction_up = TRUE &
             # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &
            (cur_floor /: call_buttons) THEN
   cur_floor := ((cur_floor)+(1))
 END ;
 move_down = SELECT door_open = FALSE & cur_floor > groundf & (direction_up = FALSE) &
       # cu.((cu : INTEGER) & ((cu : INTEGER) & (cu < cur_floor) & (cu : call_buttons))) &
      (cur_floor /: call_buttons) THEN
   cur_floor := ((cur_floor)-(1))
 END ;
 reverse_lift_up = SELECT direction_up = FALSE & door_open = FALSE &
   # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &
   ! l.((l : INTEGER) => (((l : INTEGER) & (l <= cur_floor) & (l >= groundf)) => (l /: call_buttons))) THEN
   direction_up := TRUE
 END ;
 reverse_lift_down = SELECT direction_up = TRUE & door_open = FALSE &
  # cd.(cd : INTEGER & ((cd : INTEGER) & (cd < cur_floor) & (cd : call_buttons))) &
  ! u.(u : INTEGER => (((u : INTEGER) & (u >= cur_floor) & (u <= topf)) => (u /: call_buttons))) THEN
  direction_up := FALSE
 END ;
 open_door = SELECT door_open = FALSE & (cur_floor : call_buttons) THEN
    door_open := TRUE
 END ;
 close_door = SELECT door_open = TRUE THEN
    door_open := FALSE || call_buttons := ((call_buttons)\({cur_floor}))
 END ;
 push_call_button(floor) = SELECT (floor : (groundf .. topf)) & (floor /: call_buttons) THEN
     call_buttons := ((call_buttons)\/({floor}))
 END
 END
 ```

 %% Output

    Loaded machine: Lift

 %% Cell type:markdown id: tags:

 ## Initialising a Machine

 Now we will set up constants and initialise the machine, to be able to interact with it. You can set up constants with the commant `:constants` and initialise with the command `:init`.

 %% Cell type:code id: tags:

 ``` prob
 :help :constants
 ```

 %% Output

    ```
    :constants [PREDICATE]
    ```
    
    Set up the current machine's constants.
    
    This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
    :constants [PREDICATE]
    Set up the current machine's constants.
    
    This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :help :init
 ```

 %% Output

    ```
    :init [PREDICATE]
    ```
    
    Initialise the current machine with the specified predicate
    
    This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
    :init [PREDICATE]
    Initialise the current machine with the specified predicate
    
    This is a shorthand for `:exec INITIALISATION [PREDICATE]`.

 %% Cell type:code id: tags:

 ``` prob
 :init
 ```

 %% Output

    Machine initialised using operation 1: $initialise_machine()

 %% Cell type:markdown id: tags:

 ## Trace and State

 After loading and initialising the machine, we can explore the state, visualise the machine and state and more. We will start by finding out in which trace we are currently in, to ensure, that we initialised the machine. This can be done with the command `:trace`.

 %% Cell type:code id: tags:

 ``` prob
 :help :trace
 ```

 %% Output

    ```
    :trace
    ```
    
    Display all states and transitions in the current trace.
    
    Each state has an index, which can be passed to the `:goto` command to go to that state.
    
    The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.
    :trace
    Display all states and transitions in the current trace.
    
    Each state has an index, which can be passed to the `:goto` command to go to that state.
    
    The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state
    * 0: `SETUP_CONSTANTS()`
    * 1: `INITIALISATION()` **(current)**
    -1: Root state
    0: SETUP_CONSTANTS()
    1: INITIALISATION() (current)

 %% Cell type:markdown id: tags:

 Switching to a different trace is possible by typing in `:goto INDEX`.

 %% Cell type:code id: tags:

 ``` prob
 :help :goto
 ```

 %% Output

    ```
    :goto INDEX
    ```
    
    Go to the state with the specified index in the current trace.
    
    Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.
    
    Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).
    :goto INDEX
    Go to the state with the specified index in the current trace.
    
    Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.
    
    Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).

 %% Cell type:code id: tags:

 ``` prob
 :goto -1
 ```

 %% Output

    Changed to state with index -1

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state **(current)**
    * 0: `SETUP_CONSTANTS()`
    * 1: `INITIALISATION()`
    -1: Root state (current)
    0: SETUP_CONSTANTS()
    1: INITIALISATION()

 %% Cell type:markdown id: tags:

 Now that we set the current state to -1, we are at out root state again. We did not set up constants or initialise the machine, yet. From here, we have two possibilities to go back to the initialised state. Either by setting up constants and initialising again, or by simply typing `:goto 1`.

 %% Cell type:code id: tags:

 ``` prob
 :goto 1
 ```

 %% Output

    Changed to state with index 1

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state
    * 0: `SETUP_CONSTANTS()`
    * 1: `INITIALISATION()` **(current)**
    -1: Root state
    0: SETUP_CONSTANTS()
    1: INITIALISATION() (current)

 %% Cell type:markdown id: tags:

 Another feature of ProB is, that you can find a state, for which a predicate is true. In the following we will try to use it:

 %% Cell type:code id: tags:

 ``` prob
 :help :find
 ```

 %% Output

    ```
    :find PREDICATE
    ```
    
    Try to find a state for which the given predicate is true (in addition to the machine's invariant).
    
    If such a state is found, it is made the current state, otherwise an error is displayed.
    
    Note that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single "fake" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.
    :find PREDICATE
    Try to find a state for which the given predicate is true (in addition to the machine's invariant).
    
    If such a state is found, it is made the current state, otherwise an error is displayed.
    
    Note that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single "fake" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.

 %% Cell type:code id: tags:

 ``` prob
 :find cur_floor=0
 ```

 %% Output

    Found a matching state and made it current state

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state
    * 0: `find_valid_state` **(current)**
    -1: Root state
    0: find_valid_state (current)

 %% Cell type:markdown id: tags:

 Note that the command leaves us with the root state and the current state, with a valid trace. That means, we lose our previous trace.

 For the next example we will have to recreate that trace again, with the following three commands:

 %% Cell type:code id: tags:

 ``` prob
 :goto -1
 ```

 %% Output

    Changed to state with index -1

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :init
 ```

 %% Output

    Machine initialised using operation 1: $initialise_machine()

 %% Cell type:markdown id: tags:

 ## Interacting with the Machine

 If you want to interact with the machine, meaning, that you want to know, which values the variables and constants have, you can simply type in the identifiers of those. e.g. type in `cur_floor` to find out on which floor we are currently at.

 %% Cell type:code id: tags:

 ``` prob
 cur_floor
 ```

 %% Output

    $-1$
    −1

 %% Cell type:markdown id: tags:

 If you want to get an overview over the whole machine state and which operations are currently possible, you can use `:browse`.

 %% Cell type:code id: tags:

 ``` prob
 :help :browse
 ```

 %% Output

    ```
    :browse
    ```
    
    Show information about the current state.
    
    The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state.
    :browse
    Show information about the current state.
    
    The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state.

 %% Cell type:code id: tags:

 ``` prob
 :browse
 ```

 %% Output

    Machine: Lift
    Sets: (none)
    Constants: groundf, topf
    Variables: call_buttons, cur_floor, direction_up, door_open
    Operations:
    push_call_button(-1)
    push_call_button(0)
    push_call_button(1)
    push_call_button(2)

 %% Cell type:markdown id: tags:

 To use operations, you have to use another command, that is slightly different. Type in the name of any operation, that is currently possible and put `:exec` before:

 %% Cell type:code id: tags:

 ``` prob
 :help :exec
 ```

 %% Output

    ```
    :exec OPERATION [PREDICATE]
    ```
    
    Execute an operation.
    
    A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.
    :exec OPERATION [PREDICATE]
    Execute an operation.
    
    A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.

 %% Cell type:code id: tags:

 ``` prob
 :exec push_call_button floor=-1
 ```

 %% Output

    Executed operation: push_call_button(-1)

 %% Cell type:markdown id: tags:

 If we check our trace again and browse our actions, we can see, that the call button of the floor -1 is now pushed.

 %% Cell type:code id: tags:

 ``` prob
 :trace
 ```

 %% Output

    * -1: Root state
    * 0: `SETUP_CONSTANTS()`
    * 1: `INITIALISATION()`
    * 2: `push_call_button(-1)` **(current)**
    -1: Root state
    0: SETUP_CONSTANTS()
    1: INITIALISATION()
    2: push_call_button(-1) (current)

 %% Cell type:code id: tags:

 ``` prob
 :browse
 ```

 %% Output

    Machine: Lift
    Sets: (none)
    Constants: groundf, topf
    Variables: call_buttons, cur_floor, direction_up, door_open
    Operations:
    open_door()
    push_call_button(0)
    push_call_button(1)
    push_call_button(2)

 %% Cell type:markdown id: tags:

 Of course, we could also type in `call_buttons` to find out, which call buttons are currently pushed.

 %% Cell type:code id: tags:

 ``` prob
 call_buttons
 ```

 %% Output

    $\{-1\}$
    {−1}

 %% Cell type:markdown id: tags:

 The `:let` command lets you store the value of an expression under a different name. It is evaluated once on the current state. You can use the `:unlet` command if you are not using the local variable anymore.

 %% Cell type:code id: tags:

 ``` prob
 :help :let
 ```

 %% Output

    ```
    :let NAME EXPR
    ```
    
    Evaluate an expression and store it in a local variable.
    
    The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.
    
    **Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.
    :let NAME EXPR
    Evaluate an expression and store it in a local variable.
    
    The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.
    
    **Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.

 %% Cell type:code id: tags:

 ``` prob
 :let first_floor_called 1:call_buttons
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:code id: tags:

 ``` prob
 :exec push_call_button floor=1
 ```

 %% Output

    Executed operation: push_call_button(1)

 %% Cell type:code id: tags:

 ``` prob
 first_floor_called
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:code id: tags:

 ``` prob
 :help :unlet
 ```

 %% Output

    ```
    :unlet NAME
    ```
    
    Remove a local variable.
    :unlet NAME
    Remove a local variable.

 %% Cell type:code id: tags:

 ``` prob
 :unlet first_floor_called
 ```

 %% Cell type:code id: tags:

 ``` prob
 first_floor_called
 ```

 %% Output

    :eval: Computation not completed: Unknown identifier "first_floor_called"

 %% Cell type:markdown id: tags:

 Additionally, you can use the `:table` command to display an expression as a table.

 %% Cell type:code id: tags:

 ``` prob
 :help :table
 ```

 %% Output

    ```
    :table EXPRESSION
    ```
    
    Display an expression as a table.
    
    Although any expression is accepted, this command is most useful for sets of tuples.
    :table EXPRESSION
    Display an expression as a table.
    
    Although any expression is accepted, this command is most useful for sets of tuples.

 %% Cell type:code id: tags:

 ``` prob
 :table cur_floor
 ```

 %% Output

    |cur_floor|
    |---|
    |$-1$|
    cur_floor
    -1

 %% Cell type:markdown id: tags:

 If you are not sure which type an formula has, you can use `:type` to find out.

 %% Cell type:code id: tags:

 ``` prob
 :help :type
 ```

 %% Output

    ```
    :type FORMULA
    ```
    
    Display the type of a formula.
    
    The returned types are *not* standard B types. They are human-readable, but cannot be used in code.
    :type FORMULA
    Display the type of a formula.
    
    The returned types are *not* standard B types. They are human-readable, but cannot be used in code.

 %% Cell type:code id: tags:

 ``` prob
 :type cur_floor
 ```

 %% Output

    INTEGER

 %% Cell type:code id: tags:

 ``` prob
 :type call_buttons
 ```

 %% Output

    POW(INTEGER)

 %% Cell type:markdown id: tags:

 ## Evaluations

 If you just want to make sure, that a predicate is true, use the `:assert` command instead.

 %% Cell type:code id: tags:

 ``` prob
 :help :assert
 ```

 %% Output

    ```
    :assert PREDICATE
    ```
    
    Ensure that the predicate is true, and show an error otherwise.
    
    This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
    
    Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.
    :assert PREDICATE
    Ensure that the predicate is true, and show an error otherwise.
    
    This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
    
    Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.

 %% Cell type:code id: tags:

 ``` prob
 :assert cur_floor=0
 ```

 %% Output

    :assert: Assertion is not true: FALSE

 %% Cell type:code id: tags:

 ``` prob
 :assert cur_floor=-1
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 :browse
 ```

 %% Output

    Machine: Lift
    Sets: (none)
    Constants: groundf, topf
    Variables: call_buttons, cur_floor, direction_up, door_open
    Operations:
    open_door()
    push_call_button(0)
    push_call_button(2)

 %% Cell type:markdown id: tags:

 Another notable feature is the following command, with which you can pretty print predicates. Use `:prettyprint` to access it.

 You also have the option to solve predicates with different solvers. For this you can use the command `:solve`.

 %% Cell type:code id: tags:

 ``` prob
 :help :prettyprint
 ```

 %% Cell type:code id: tags:

 ``` prob
 :prettyprint cur_floor=-1
 ```

 %% Output

    $\mathit{cur\_floor} = - 1$
    cur_floor = - 1

 %% Cell type:code id: tags:

 ``` prob
 :help :solve
 ```

 %% Output

    ```
    :solve SOLVER PREDICATE
    ```
    
    Solve a predicate with the specified solver.
    
    The following solvers are currently available:
    
    * `cvc4`
    * `kodkod`
    * `prob`
    * `smt_supported_interpreter`
    * `z3`
    :solve SOLVER PREDICATE
    Solve a predicate with the specified solver.
    
    The following solvers are currently available:
    
    * `cvc4`
    * `kodkod`
    * `prob`
    * `smt_supported_interpreter`
    * `z3`

 %% Cell type:markdown id: tags:

 ## Modifying the Preferences

 We have seen before, that you can set preferences when loading the machine with the `::load` command. You can modify or change the values of preferences by using the `:pref` command.

 %% Cell type:code id: tags:

 ``` prob
 :help :pref
 ```

 %% Output

    ```
    :pref [NAME ...]
    :pref NAME=VALUE [NAME=VALUE ...]
    ```
    
    View or change the value of one or more preferences.
    
    In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.
    
    Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command.
    :pref [NAME ...]
    :pref NAME=VALUE [NAME=VALUE ...]
    View or change the value of one or more preferences.
    
    In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.
    
    Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command.

 %% Cell type:markdown id: tags:

 ## Additional Features

 In addition to the previous commands, you have the possibility to use the `:stats` command to show statistics about the state space. Moreover, you can use the `:time` command to measure the execution time of commands with their arguments. This can be helpful for measuring the solving time for specific machines.

 %% Cell type:code id: tags:

 ``` prob
 :help :stats
 ```

 %% Output

    ```
    :stats
    ```
    
    Show statistics about the state space.
    :stats
    Show statistics about the state space.

 %% Cell type:code id: tags:

 ``` prob
 :stats
 ```

 %% Output

    **Explored States:** 4/15
    **Transitions:** 14
    Explored States: 4/15
    Transitions: 14

 %% Cell type:code id: tags:

 ``` prob
 :help :time
 ```

 %% Output

    ```
    :time COMMAND [ARGS ...]
    ```
    
    Execute the given command and measure how long it takes to execute.
    
    The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.
    
    As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB.
    :time COMMAND [ARGS ...]
    Execute the given command and measure how long it takes to execute.
    
    The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.
    
    As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB.

 %% Cell type:code id: tags:

 ``` prob
 :time :stats
 ```

 %% Output

    Execution time: 0.044099194 seconds

    **Explored States:** 4/15
    **Transitions:** 14
    Explored States: 4/15
    Transitions: 14

 %% Cell type:markdown id: tags:

 To find out your current ProB CLI and ProB2 version, you can use `:version`.

 %% Cell type:code id: tags:

 ``` prob
 :help :version
 ```

 %% Output

    ```
    :version
    ```
    
    Display version info about the ProB CLI and ProB 2.
    :version
    Display version info about the ProB CLI and ProB 2.

 %% Cell type:code id: tags:

 ``` prob
 :version
 ```

 %% Output

    ProB CLI: 1.9.0-nightly (ab12dcd41e1150b19e8c00897fe53f96f76cbd0d)
    ProB 2: 3.2.12-SNAPSHOT (06e75efe84ffdadf56df45e34acb44ec8e4603dd)

 %% Cell type:markdown id: tags:

 ## Visualisations

 There are two possible ways of visualising the machine in jupyter notebook. One can be accessed via the `:dot` command. This command allows you to visualise a variety of different things, e.g. the state as graph. You can use autocomplete by clicking `TAB` after the command, as well.

 %% Cell type:code id: tags:

 ``` prob
 :help :dot
 ```

 %% Output

    ```
    :dot COMMAND [FORMULA]
    ```
    
    Execute and show a dot visualisation.
    
    The following dot visualisation commands are available:
    
    * `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
    * `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)
    * `state_space` - State Space: Show state space
    * `state_space_sfdp` - State Space (Fast): Show state space (fast)
    * `current_state` - Current State in State Space: Show current state and successors in state space
    * `signature_merge` - Signature Merge: Show signature-merged reduced state space
    * `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
    * `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
    * `enable_graph` - Enable Graph: Show enabling graph of events
    * `state_as_graph` - Current State as Graph: Show values in current state as a graph
    * `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)
    * `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
    * `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
    * `invariant` - Invariant Formula Tree: Show invariant as a formula tree
    * `properties` - Properties Formula Tree: Show properties as a formula tree
    * `assertions` - Assertions Formula Tree: Show assertions as a formula tree
    * `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
    * `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)
    * `dependence_graph` - Dependence Graph: Show dependence graph of events
    * `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
    * `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
    * `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
    * `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)
    :dot COMMAND [FORMULA]
    Execute and show a dot visualisation.
    
    The following dot visualisation commands are available:
    
    * `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
    * `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)
    * `state_space` - State Space: Show state space
    * `state_space_sfdp` - State Space (Fast): Show state space (fast)
    * `current_state` - Current State in State Space: Show current state and successors in state space
    * `signature_merge` - Signature Merge: Show signature-merged reduced state space
    * `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
    * `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
    * `enable_graph` - Enable Graph: Show enabling graph of events
    * `state_as_graph` - Current State as Graph: Show values in current state as a graph
    * `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)
    * `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
    * `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
    * `invariant` - Invariant Formula Tree: Show invariant as a formula tree
    * `properties` - Properties Formula Tree: Show properties as a formula tree
    * `assertions` - Assertions Formula Tree: Show assertions as a formula tree
    * `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
    * `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)
    * `dependence_graph` - Dependence Graph: Show dependence graph of events
    * `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
    * `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
    * `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
    * `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)

 %% Cell type:code id: tags:

 ``` prob
 :dot state_as_graph
 ```

 %% Output


    <Dot visualization: state_as_graph []>

 %% Cell type:markdown id: tags:

 Another option is to use the `ANIMATION_FUNCTION` with the command `:show`. Note, however, that to use this you have to write an `ANIMATION_FUNCTION` for your B model.

 The following B model contains such an `ANIMATION_FUNCTION` for the visualisation of Lift4. You can use what you have learned before to explore the visualisation.

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MODEL Lift0
 DEFINITIONS SET_PREF_SHOW_EVENTB_ANY_VALUES==TRUE;
  ASSERT_LTL == "G( [push_call_button(groundf)] => F {cur_floor=groundf & door_open=TRUE})";
  Rconv == (topf-r+groundf);
  ANIMATION_FUNCTION == ( {r,c,i|r:groundf..topf & ((c=2 & i=0) or (c=1 & i=2))} <+
                            ({r,c,i|r:groundf..topf & Rconv:call_buttons & c=2 & i=1} \/
                             {r,c,i|r:groundf..topf & Rconv=cur_floor & c=1 &
                                    ((door_open=TRUE & i=3) or (door_open=FALSE & i=4))}
                              ) \/ {r,c,i| r=topf+1 & c=1 &
                                       ((direction_up=TRUE & i=5) or (direction_up=FALSE & i=6)) } );
      ANIMATION_IMG0 == "images/CallButtonOff.gif";
      ANIMATION_IMG1 == "images/CallButtonOn.gif";
      ANIMATION_IMG2 == "images/LiftEmpty.gif";
      ANIMATION_IMG3 == "images/LiftOpen.gif";
      ANIMATION_IMG4 == "images/LiftClosed.gif";
      ANIMATION_IMG5 == "images/up_arrow.gif";
      ANIMATION_IMG6 == "images/down_arrow.gif";
      ANIMATION_RIGHT_CLICK(J,r) ==
               IF J=2 THEN
                push_call_button(topf-r+groundf)
               ELSIF J=1 THEN
                 CHOICE open_door OR close_door OR move_up OR move_down OR
                        reverse_lift_up OR reverse_lift_down
                 END
               END;
 CONSTANTS groundf,topf
 PROPERTIES
  topf : INTEGER & groundf : INTEGER & (groundf = -1) & (topf = 2) & (groundf < topf)
 VARIABLES call_buttons,cur_floor,direction_up,door_open
 INVARIANT
       cur_floor : (groundf .. topf) &
       door_open : BOOL &
       call_buttons : POW(groundf .. topf) &
       direction_up : BOOL &
       (door_open = TRUE => cur_floor : call_buttons)
 INITIALISATION cur_floor := (groundf) || door_open := FALSE || call_buttons := ({}) || direction_up := TRUE
 OPERATIONS
 move_up = SELECT door_open = FALSE & cur_floor < topf & direction_up = TRUE &
             # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &
            (cur_floor /: call_buttons) THEN
   cur_floor := ((cur_floor)+(1))
 END ;
 move_down = SELECT door_open = FALSE & cur_floor > groundf & (direction_up = FALSE) &
       # cu.((cu : INTEGER) & ((cu : INTEGER) & (cu < cur_floor) & (cu : call_buttons))) &
      (cur_floor /: call_buttons) THEN
   cur_floor := ((cur_floor)-(1))
 END ;
 reverse_lift_up = SELECT direction_up = FALSE & door_open = FALSE &
   # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &
   ! l.((l : INTEGER) => (((l : INTEGER) & (l <= cur_floor) & (l >= groundf)) => (l /: call_buttons))) THEN
   direction_up := TRUE
 END ;
 reverse_lift_down = SELECT direction_up = TRUE & door_open = FALSE &
  # cd.(cd : INTEGER & ((cd : INTEGER) & (cd < cur_floor) & (cd : call_buttons))) &
  ! u.(u : INTEGER => (((u : INTEGER) & (u >= cur_floor) & (u <= topf)) => (u /: call_buttons))) THEN
  direction_up := FALSE
 END ;
 open_door = SELECT door_open = FALSE & (cur_floor : call_buttons) THEN
    door_open := TRUE
 END ;
 close_door = SELECT door_open = TRUE THEN
    door_open := FALSE || call_buttons := ((call_buttons)\({cur_floor}))
 END ;
 push_call_button(floor) = SELECT (floor : (groundf .. topf)) & (floor /: call_buttons) THEN
     call_buttons := ((call_buttons)\/({floor}))
 END
 END
 ```

 %% Output

    Loaded machine: Lift0

 %% Cell type:code id: tags:

 ``` prob
 :help :show
 ```

 %% Output

    ```
    :show
    ```
    
    Show the machine's animation function visualisation for the current state.
    
    The visualisation is static, any defined right-click options cannot be viewed or used.
    :show
    Show the machine's animation function visualisation for the current state.
    
    The visualisation is static, any defined right-click options cannot be viewed or used.

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :init
 ```

 %% Output

    Machine initialised using operation 1: $initialise_machine()

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/LiftClosed.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:code id: tags:

 ``` prob
 :browse
 ```

 %% Output

    Machine: Lift0
    Sets: (none)
    Constants: groundf, topf
    Variables: call_buttons, cur_floor, direction_up, door_open
    Operations:
    push_call_button(-1)
    push_call_button(0)
    push_call_button(1)
    push_call_button(2)

 %% Cell type:code id: tags:

 ``` prob
 :exec push_call_button floor=-1
 ```

 %% Output

    Executed operation: push_call_button(-1)

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/LiftClosed.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/CallButtonOn.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:code id: tags:

 ``` prob
 :exec open_door
 ```

 %% Output

    Executed operation: open_door()

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="3" src="images/LiftOpen.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/CallButtonOn.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:code id: tags:

 ``` prob
 :exec close_door
 ```

 %% Output

    Executed operation: close_door()

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/LiftClosed.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:code id: tags:

 ``` prob
 :browse
 ```

 %% Output

    Machine: Lift0
    Sets: (none)
    Constants: groundf, topf
    Variables: call_buttons, cur_floor, direction_up, door_open
    Operations:
    push_call_button(-1)
    push_call_button(0)
    push_call_button(1)
    push_call_button(2)

 %% Cell type:code id: tags:

 ``` prob
 :exec push_call_button floor=1
 ```

 %% Output

    Executed operation: push_call_button(1)

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/CallButtonOn.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/LiftClosed.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:code id: tags:

 ``` prob
 :exec move_up
 ```

 %% Output

    Executed operation: move_up()

 %% Cell type:code id: tags:

 ``` prob
 :show
 ```

 %% Output

    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/CallButtonOn.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/LiftClosed.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/LiftEmpty.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/CallButtonOff.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/up_arrow.gif"/></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>

 %% Cell type:markdown id: tags:

 This concludes the overview over the ProB jupyter notebook kernel.

--- a/images/ChessPieces/Chess_bdd45.gif
+++ b/images/ChessPieces/Chess_bdd45.gif
--- a/images/ChessPieces/Chess_bdl45.gif
+++ b/images/ChessPieces/Chess_bdl45.gif
--- a/images/ChessPieces/Chess_bld45.gif
+++ b/images/ChessPieces/Chess_bld45.gif
--- a/images/ChessPieces/Chess_bll45.gif
+++ b/images/ChessPieces/Chess_bll45.gif
--- a/images/ChessPieces/Chess_emptyXg45.gif
+++ b/images/ChessPieces/Chess_emptyXg45.gif
--- a/images/ChessPieces/Chess_emptyd45.gif
+++ b/images/ChessPieces/Chess_emptyd45.gif
--- a/images/ChessPieces/Chess_emptyg45.gif
+++ b/images/ChessPieces/Chess_emptyg45.gif
--- a/images/ChessPieces/Chess_emptyl45.gif
+++ b/images/ChessPieces/Chess_emptyl45.gif
--- a/images/ChessPieces/Chess_kdd45.gif
+++ b/images/ChessPieces/Chess_kdd45.gif
--- a/images/ChessPieces/Chess_kdl45.gif
+++ b/images/ChessPieces/Chess_kdl45.gif
--- a/images/ChessPieces/Chess_kld45.gif
+++ b/images/ChessPieces/Chess_kld45.gif
--- a/images/ChessPieces/Chess_kll45.gif
+++ b/images/ChessPieces/Chess_kll45.gif
--- a/images/ChessPieces/Chess_krd45.gif
+++ b/images/ChessPieces/Chess_krd45.gif
--- a/images/ChessPieces/Chess_krl45.gif
+++ b/images/ChessPieces/Chess_krl45.gif
--- a/images/ChessPieces/Chess_krt45.gif
+++ b/images/ChessPieces/Chess_krt45.gif
--- a/images/ChessPieces/Chess_ndd45.gif
+++ b/images/ChessPieces/Chess_ndd45.gif
--- a/images/ChessPieces/Chess_ndl45.gif
+++ b/images/ChessPieces/Chess_ndl45.gif