diff --git a/notebooks/presentations/FMTea2022.ipynb b/notebooks/presentations/FMTea2022.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..d48cb6b598e2045921096ca0e17dc7302d347855
--- /dev/null
+++ b/notebooks/presentations/FMTea2022.ipynb
@@ -0,0 +1,867 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# ProB for Teaching Theoretical Computer Science and Formal Methods\n",
+ "\n",
+ "### David Geleßus, Michael Leuschel\n",
+ "### FMTea 2022\n",
+ "\n",
+ "https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel\n",
+ "\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Intro: Notebooks, Jupyter"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## What is a Notebook?\n",
+ "\n",
+ "* Document containing text and executable code blocks\n",
+ "* Code can be executed interactively\n",
+ "* Results are shown in the notebook below the corresponding code\n",
+ "* Similar to a REPL (read-eval-print-loop), with some differences:\n",
+ " * Code blocks can be edited and executed out-of-order\n",
+ " * Results can contain rich text and graphics\n",
+ " * Can be shared with other users"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Jupyter Notebook\n",
+ "\n",
+ "* Browser-based notebook interface\n",
+ "* Open-source and cross-platform\n",
+ "* Originated in the Python community, implemented in Python\n",
+ "* Also supports languages other than \n",
+ "* Language integration provided by a separate *kernel*"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## ProB Jupyter Kernel (https://prob.hhu.de/w/)\n",
+ "\n",
+ "* Understands both classical B syntax and Rodin Event-B syntax\n",
+ "* Many features: Code completion, graph visualisation, ..."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Some Features"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Evaluating Formulas\n",
+ "\n",
+ "Evaluating B expressions and solving predicates:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$3$"
+ ],
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1+2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 2"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1 + x = 3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ },
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{-3,1,2,3,4,5,10,18\\}$"
+ ],
+ "text/plain": [
+ "{−3,1,2,3,4,5,10,18}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1..5 \\/ {-3, 4, 10, 18}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Example: Set of all prime numbers < 500"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}/*@\\mathit{symbolic}*/ \\{\\mathit{x}\\mid\\mathit{x} > 1 \\land \\lnot(\\exists\\mathit{y}\\qdot(\\mathit{y} > 1 \\land \\mathit{y} < \\mathit{x} \\land \\mathit{x} \\mathit{mod} \\mathit{y} = 0))\\}$"
+ ],
+ "text/plain": [
+ "/*@symbolic*/ {x∣x > 1 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))}"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x | x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Outputs are rendered as $\\LaTeX$ formulas:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{x} > 1 \\wedge \\mathit{x} < 500 \\wedge \\neg (\\exists \\mathit{y}\\cdot (\\mathit{y} > 1 \\wedge \\mathit{y} < \\mathit{x} \\wedge \\mathit{x} \\mod \\mathit{y} = 0))$"
+ ],
+ "text/plain": [
+ "x > 1 ∧ x < 500 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Unicode symbols can also be used in inputs:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499\\}$"
+ ],
+ "text/plain": [
+ "{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499}"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x | x>1 ∧ x<500 ∧ ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Convenient multiline input, with syntax highlighting and code completion:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "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": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {S,E,N,D,M,O,R,Y |\n",
+ "\n",
+ "{S, E, N, D, M, O, R, Y} ⊆ 0..9\n",
+ "∧ S > 0 ∧ M > 0\n",
+ "∧ card({S, E, N, D, M, O, R, Y}) = 8\n",
+ "∧\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",
+ "\n",
+ "}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Find distinct digits such that this multiplication becomes true:\n",
+ "\n",
+ "\n",
+ "\n",
+ "(This is a more difficult version of the Send+More=Money puzzle.)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|K|I|S|P|A|O|N|\n",
+ "|---|---|---|---|---|---|---|\n",
+ "|2|0|3|4|1|8|9|\n"
+ ],
+ "text/plain": [
+ "K\tI\tS\tP\tA\tO\tN\n",
+ "2\t0\t3\t4\t1\t8\t9\n"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {K,I,S,P,A,O,N | {K,P} ⊆ 1..9 ∧\n",
+ " {I,S,A,O,N} ⊆ 0..9 ∧\n",
+ " (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n",
+ " = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N ∧\n",
+ " card({K, I, S, P, A, O, N}) = 7}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Visualisation\n",
+ "\n",
+ "In B, sequences are also functions, functions are relations, and relations are sets.\n",
+ "Relations can be displayed visually:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(2\\mapsto 1),(3\\mapsto 1),(3\\mapsto 2),(4\\mapsto 1),(4\\mapsto 2),(4\\mapsto 3),(5\\mapsto 1),(5\\mapsto 2),(5\\mapsto 3),(5\\mapsto 4)\\}$"
+ ],
+ "text/plain": [
+ "{(2↦1),(3↦1),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(5↦4)}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x,y | x:1..5 & y:1..5 & x>y}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ },
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_ENGINE = circo\n"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_ENGINE=circo"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"243pt\" height=\"235pt\"\n viewBox=\"0.00 0.00 243.39 234.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 230.7203)\">\n<title>state</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-230.7203 239.3858,-230.7203 239.3858,4 -4,4\"/>\n<!-- 5 -->\n<g id=\"node1\" class=\"node\">\n<title>5</title>\n<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-36 112.1026,-36 112.1026,0 166.1026,0 166.1026,-36\"/>\n<text text-anchor=\"middle\" x=\"139.1026\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5</text>\n</g>\n<!-- 4 -->\n<g id=\"node2\" class=\"node\">\n<title>4</title>\n<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"235.3858,-131.3602 181.3858,-131.3602 181.3858,-95.3602 235.3858,-95.3602 235.3858,-131.3602\"/>\n<text text-anchor=\"middle\" x=\"208.3858\" y=\"-109.6602\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n</g>\n<!-- 5->4 -->\n<g id=\"edge1\" class=\"edge\">\n<title>5->4</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M152.4611,-36.3864C162.879,-50.7254 177.4897,-70.8353 189.1646,-86.9044\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"186.5938,-89.3207 195.3033,-95.3536 192.257,-85.2062 186.5938,-89.3207\"/>\n<text text-anchor=\"middle\" x=\"161.8128\" y=\"-65.4454\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 3 -->\n<g id=\"node3\" class=\"node\">\n<title>3</title>\n<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-190.296 0,-190.296 0,-154.296 54,-154.296 54,-190.296\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-168.596\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n</g>\n<!-- 5->3 -->\n<g id=\"edge2\" class=\"edge\">\n<title>5->3</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M126.0236,-36.0017C106.3845,-63.0326 69.1556,-114.2737 46.3626,-145.6457\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"43.3895,-143.7832 40.3432,-153.9307 49.0526,-147.8978 43.3895,-143.7832\"/>\n<text text-anchor=\"middle\" x=\"77.1931\" y=\"-94.6237\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 2 -->\n<g id=\"node4\" class=\"node\">\n<title>2</title>\n<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-226.7203 112.1026,-226.7203 112.1026,-190.7203 166.1026,-190.7203 166.1026,-226.7203\"/>\n<text text-anchor=\"middle\" x=\"139.1026\" y=\"-205.0203\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n</g>\n<!-- 5->2 -->\n<g id=\"edge3\" class=\"edge\">\n<title>5->2</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M139.1026,-36.2871C139.1026,-69.6799 139.1026,-140.734 139.1026,-180.4178\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"135.6027,-180.4886 139.1026,-190.4886 142.6027,-180.4887 135.6027,-180.4886\"/>\n<text text-anchor=\"middle\" x=\"130.1026\" y=\"-112.1524\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 1 -->\n<g id=\"node5\" class=\"node\">\n<title>1</title>\n<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-72.4243 0,-72.4243 0,-36.4243 54,-36.4243 54,-72.4243\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-50.7243\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n</g>\n<!-- 5->1 -->\n<g id=\"edge4\" class=\"edge\">\n<title>5->1</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M111.9657,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"62.7045,-39.143 54.2756,-45.562 64.8677,-45.8004 62.7045,-39.143\"/>\n<text text-anchor=\"middle\" x=\"79.063\" y=\"-38.3838\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 4->3 -->\n<g id=\"edge5\" class=\"edge\">\n<title>4->3</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M181.2305,-122.1835C150.0179,-132.3251 98.6277,-149.0227 63.8291,-160.3295\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"62.4733,-157.0898 54.0443,-163.5088 64.6364,-163.7472 62.4733,-157.0898\"/>\n<text text-anchor=\"middle\" x=\"113.5298\" y=\"-145.0565\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 4->2 -->\n<g id=\"edge6\" class=\"edge\">\n<title>4->2</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M195.0273,-131.7466C184.6094,-146.0856 169.9987,-166.1955 158.3238,-182.2646\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"155.2315,-180.5663 152.1851,-190.7138 160.8946,-184.6809 155.2315,-180.5663\"/>\n<text text-anchor=\"middle\" x=\"167.6756\" y=\"-160.8056\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 4->1 -->\n<g id=\"edge7\" class=\"edge\">\n<title>4->1</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M181.2305,-104.5369C150.0179,-94.3953 98.6277,-77.6976 63.8291,-66.3908\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"64.6364,-62.9731 54.0443,-63.2116 62.4733,-69.6305 64.6364,-62.9731\"/>\n<text text-anchor=\"middle\" x=\"113.5298\" y=\"-89.2639\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 3->2 -->\n<g id=\"edge8\" class=\"edge\">\n<title>3->2</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M54.1369,-181.1133C68.4889,-185.7765 86.3236,-191.5714 101.9423,-196.6462\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"101.2349,-200.0964 111.827,-199.858 103.3981,-193.439 101.2349,-200.0964\"/>\n<text text-anchor=\"middle\" x=\"69.0396\" y=\"-192.6798\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 3->1 -->\n<g id=\"edge9\" class=\"edge\">\n<title>3->1</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M27,-154.1369C27,-135.157 27,-105.1104 27,-82.9567\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"30.5001,-82.7983 27,-72.7983 23.5001,-82.7983 30.5001,-82.7983\"/>\n<text text-anchor=\"middle\" x=\"18\" y=\"-122.3468\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n<!-- 2->1 -->\n<g id=\"edge10\" class=\"edge\">\n<title>2->1</title>\n<path fill=\"none\" stroke=\"#b22222\" d=\"M126.0236,-190.7187C106.3845,-163.6878 69.1556,-112.4466 46.3626,-81.0746\"/>\n<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n<text text-anchor=\"middle\" x=\"77.1931\" y=\"-139.6966\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"K5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"K5\", {x,y | x:1..5 & y:1..5 & x>y})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Applications"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "* Interactive Development\n",
+ "* Documentation of Models\n",
+ "* Documentation of ProB's standard libraries"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Use in Teaching\n",
+ "\n",
+ "* Course materials/lecture notes as notebooks\n",
+ " * Students can execute examples themselves and experiment with the code\n",
+ " * Visualisation of relations, graphs, etc.\n",
+ " * `nbconvert` renders notebooks to HTML, PDF, etc.\n",
+ "* Exercise sheets as notebooks\n",
+ " * An incomplete notebook with exercises is provided\n",
+ " * Students solve the exercises and turn in the finished notebook\n",
+ " * `nbgrader` assists with creating and grading exercises\n",
+ " * Automatic grading sometimes possible"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Example: Course Notes for Theoretical CS (German)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "### DFA\n",
+ "\n",
+ "Ein __deterministischer endlicher Automat__ (kurz DFA für\n",
+ " deterministic finite automaton) ist ein Quintupel \n",
+ " $M =(\\Sigma, Z, \\delta , z_0, F)$, wobei\n",
+ "* $\\Sigma$ ein Alphabet ist,\n",
+ "* $Z$ eine endliche Menge von Zuständen mit\n",
+ " $\\Sigma \\cap Z = \\emptyset$,\n",
+ "* $\\delta : Z \\times \\Sigma \\rightarrow Z$ die Überführungsfunktion,\n",
+ "* $z_0 \\in Z$ der Startzustand und\n",
+ "* $F \\subseteq Z$ die Menge der Endzustände (Finalzustände).\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: DFA"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE DFA\n",
+ "SETS\n",
+ " Z = {z0,z1,z2,z3}\n",
+ "CONSTANTS Σ, F, δ\n",
+ "PROPERTIES\n",
+ " F ⊆ Z ∧\n",
+ " δ ∈ (Z×Σ) → Z\n",
+ " ∧\n",
+ " /* Der Automat von Folie 10: */\n",
+ " Σ = {0,1} ∧\n",
+ " F = {z2} ∧\n",
+ " δ = { (z0,0)↦z1, (z0,1)↦z3,\n",
+ " (z1,0)↦z3, (z1,1)↦z2,\n",
+ " (z2,0)↦z2, (z2,1)↦z2,\n",
+ " (z3,0)↦z3, (z3,1)↦z3 }\n",
+ "DEFINITIONS // Für den Zustandsgraphen:\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"red\",label:\"0\",edges:{a,b|(a,0)|->b:δ}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{a,b|(a,1)|->b:δ});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"black\",label:\"\",edges:{\"\" |-> z0}) // Kante für den Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Ein Automat befindet sich jeweils in einem der Zustände aus Z. Am Anfang befindet er sich in $z_0$. \n",
+ "Der Automat kann jeweils in einem Zustand $z$ ein Symbol $x$ aus $\\Sigma$ verarbeiten und wechselt dann in den Zustand $\\delta(z,x)$.\n",
+ "Zum Beispiel, wenn der DFA im Startzustand z0 das Symbol $0$ erhält wechselt er nach:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{z1}$"
+ ],
+ "text/plain": [
+ "z1"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "δ(z0,0)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{z2}$"
+ ],
+ "text/plain": [
+ "z2"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "δ(z1,1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Da $z2\\in F$ ein Endzustand ist, akzeptiert der DFA das Wort $01$ (oder $[0,1]$ in der Notation vom Notebook).\n",
+ "\n",
+ "\n",
+ "### Arbeitsweise eines DFAs\n",
+ "\n",
+ "Ein DFA $M= (\\Sigma, Z, \\delta , z_0, F)$ akzeptiert bzw. verwirft eine\n",
+ "Eingabe $x$ wie folgt:\n",
+ "* $M$ beginnt beim Anfangszustand $z_0$ und führt insgesamt $|x|$ Schritte aus.\n",
+ "* Der Lesekopf wandert dabei v.l.n.r. über das Eingabewort $x$, Symbol\n",
+ " für Symbol, und ändert dabei seinen Zustand jeweils gemäß der\n",
+ " Überführungsfunktion $\\delta$:\n",
+ " Ist $M$ im Zustand $z \\in Z$ und liest das\n",
+ " Symbol $a \\in \\Sigma$ und gilt $\\delta(z,a) = z'$, so ändert $M$ seinen\n",
+ " Zustand in $z'$.\n",
+ "* Ist der letzte erreichte Zustand (nachdem $x$ abgearbeitet ist)\n",
+ " * ein Endzustand, so akzeptiert $M$ die Eingabe $x$;\n",
+ " * andernfalls lehnt $M$ sie ab.\n",
+ "\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Da in diesem Automaten z0 kein Endzustand ist, wird zum Beispiel das leere Wort abgelehnt:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "z0 ∈ F"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Zustandgraph\n",
+ "\n",
+ "Man kann den DFA auch grafisch darstellen: Endzustände sind mit einem doppelten Kreis gekennzeichnet, der Anfangszustand wird durch eine besondere Startkante gekennzeichnet.\n",
+ "\n",
+ "Formal ist dies so definiert:\n",
+ "Ein DFA $M= (\\Sigma, Z, \\delta , z_0, F)$ lässt sich anschaulich durch \n",
+ "seinen __Zustandsgraphen__ darstellen,\n",
+ "\n",
+ "* dessen Knoten die Zustände von $M$ und\n",
+ "* dessen Kanten Zustandsübergänge gemäß der\n",
+ " Überführungsfunktion $\\delta$ repräsentieren.\n",
+ "* Gilt $\\delta(z,a) = z'$ für ein Symbol $a \\in \\Sigma$ und für\n",
+ " zwei Zustände $z, z' \\in Z$, so hat dieser Graph eine gerichtete\n",
+ " Kante von $z$ nach $z'$, die mit $a$ beschriftet ist.\n",
+ "* Der Startzustand wird durch einen Pfeil auf $z_0$ dargestellt.\n",
+ "* Endzustände sind durch einen Doppelkreis markiert.\n",
+ "\n",
+ "Für den Automaten oben ergiebt dies folgenden Zustandsgraphen.\n",
+ "(Anmerkung: diese Darstellung erfordert eine neue Version des ProB-Jupyter-Kernels. Falls diese bei ihnen nicht funktioniert schauen Sie sich die Abbildung auf den Folien an)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "python"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n -->\n<!-- Title: prob_graph Pages: 1 -->\n<svg width=\"540pt\" height=\"717pt\"\n viewBox=\"0.00 0.00 540.00 717.37\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(0.99 0.99) rotate(0) translate(4 724)\">\n<title>prob_graph</title>\n<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724 544,-724 544,4 -4,4\"/>\n<!-- 0 -->\n<g id=\"node1\" class=\"node\">\n<title>0</title>\n<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"59.91\" cy=\"-55\" rx=\"18\" ry=\"18\"/>\n<ellipse fill=\"none\" stroke=\"black\" cx=\"59.91\" cy=\"-55\" rx=\"22\" ry=\"22\"/>\n<text text-anchor=\"middle\" x=\"59.91\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">z2</text>\n</g>\n<!-- 0->0 -->\n<g id=\"edge3\" class=\"edge\">\n<title>0->0</title>\n<path fill=\"none\" stroke=\"green\" d=\"M79.67,-65.43C90.26,-67.2 99.91,-63.72 99.91,-55 99.91,-49.28 95.75,-45.81 89.9,-44.61\"/>\n<polygon fill=\"green\" stroke=\"green\" points=\"89.68,-41.11 79.67,-44.57 89.66,-48.11 89.68,-41.11\"/>\n<text text-anchor=\"middle\" x=\"103.41\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n</g>\n<!-- 0->0 -->\n<g id=\"edge7\" class=\"edge\">\n<title>0->0</title>\n<path fill=\"none\" stroke=\"red\" d=\"M75.65,-70.43C95.01,-82.46 117.91,-77.32 117.91,-55 117.91,-36.17 101.61,-29.57 84.88,-35.19\"/>\n<polygon fill=\"red\" stroke=\"red\" points=\"83.18,-32.12 75.65,-39.57 86.18,-38.45 83.18,-32.12\"/>\n<text text-anchor=\"middle\" x=\"121.41\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n</g>\n<!-- 1 -->\n<g id=\"node2\" class=\"node\">\n<title>1</title>\n<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"280.91\" cy=\"-492\" rx=\"18\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"280.91\" y=\"-488.9\" font-family=\"Times,serif\" font-size=\"12.00\">z0</text>\n</g>\n<!-- 2 -->\n<g id=\"node3\" class=\"node\">\n<title>2</title>\n<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"206.91\" cy=\"-278\" rx=\"18\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"206.91\" y=\"-274.9\" font-family=\"Times,serif\" font-size=\"12.00\">z1</text>\n</g>\n<!-- 1->2 -->\n<g id=\"edge5\" class=\"edge\">\n<title>1->2</title>\n<path fill=\"none\" stroke=\"red\" d=\"M275.23,-474.72C262.45,-438.11 231.36,-349.05 215.92,-304.81\"/>\n<polygon fill=\"red\" stroke=\"red\" points=\"219.21,-303.63 212.61,-295.34 212.6,-305.93 219.21,-303.63\"/>\n<text text-anchor=\"middle\" x=\"250.41\" y=\"-381.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n</g>\n<!-- 3 -->\n<g id=\"node4\" class=\"node\">\n<title>3</title>\n<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"354.91\" cy=\"-55\" rx=\"18\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"354.91\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">z3</text>\n</g>\n<!-- 1->3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>1->3</title>\n<path fill=\"none\" stroke=\"green\" d=\"M283.76,-474.21C295.03,-408.02 336.42,-164.69 350.32,-82.97\"/>\n<polygon fill=\"green\" stroke=\"green\" points=\"353.8,-83.42 352.02,-72.97 346.89,-82.24 353.8,-83.42\"/>\n<text text-anchor=\"middle\" x=\"322.41\" y=\"-274.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n</g>\n<!-- 2->0 -->\n<g id=\"edge2\" class=\"edge\">\n<title>2->0</title>\n<path fill=\"none\" stroke=\"green\" d=\"M197.26,-262.5C172.9,-225.87 108.61,-129.22 77.4,-82.3\"/>\n<polygon fill=\"green\" stroke=\"green\" points=\"80.25,-80.26 71.8,-73.87 74.42,-84.14 80.25,-80.26\"/>\n<text text-anchor=\"middle\" x=\"141.41\" y=\"-168.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n</g>\n<!-- 2->3 -->\n<g id=\"edge6\" class=\"edge\">\n<title>2->3</title>\n<path fill=\"none\" stroke=\"red\" d=\"M216.62,-262.5C241.77,-224.95 309.17,-124.29 339.62,-78.84\"/>\n<polygon fill=\"red\" stroke=\"red\" points=\"342.7,-80.52 345.36,-70.27 336.88,-76.63 342.7,-80.52\"/>\n<text text-anchor=\"middle\" x=\"284.41\" y=\"-168.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n</g>\n<!-- 3->3 -->\n<g id=\"edge4\" class=\"edge\">\n<title>3->3</title>\n<path fill=\"none\" stroke=\"green\" d=\"M370.08,-64.81C380.57,-67.79 390.91,-64.52 390.91,-55 390.91,-48.76 386.46,-45.2 380.43,-44.33\"/>\n<polygon fill=\"green\" stroke=\"green\" points=\"379.75,-40.88 370.08,-45.19 380.33,-47.85 379.75,-40.88\"/>\n<text text-anchor=\"middle\" x=\"394.41\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n</g>\n<!-- 3->3 -->\n<g id=\"edge8\" class=\"edge\">\n<title>3->3</title>\n<path fill=\"none\" stroke=\"red\" d=\"M367.11,-68.67C385.6,-82.89 408.91,-78.34 408.91,-55 408.91,-35.31 392.31,-28.99 376.02,-36.04\"/>\n<polygon fill=\"red\" stroke=\"red\" points=\"373.93,-33.21 367.11,-41.33 377.5,-39.23 373.93,-33.21\"/>\n<text text-anchor=\"middle\" x=\"412.41\" y=\"-51.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n</g>\n<!-- 4 -->\n<g id=\"node5\" class=\"node\">\n<title>4</title>\n</g>\n<!-- 4->1 -->\n<g id=\"edge9\" class=\"edge\">\n<title>4->1</title>\n<path fill=\"none\" stroke=\"black\" d=\"M280.91,-656.97C280.91,-625.57 280.91,-558.31 280.91,-520.42\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"284.41,-520.11 280.91,-510.11 277.41,-520.11 284.41,-520.11\"/>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Conclusion\n",
+ "\n",
+ "* ProB Jupyter notebooks allow conveniently working interactively with B\n",
+ "* Usable standalone or with existing models\n",
+ "* Applications: development, documentation, teaching\n",
+ "* Jupyter Notebook makes it easy to integrate new languages/tools in notebooks\n",
+ "* The Jupyter ecosystem provides a standard file format and useful tools (`nbconvert`, `nbgrader`, ...)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Links\n",
+ "\n",
+ "Load this notebook in your browser: https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob2-jupyter-kernel.git/master?filepath=notebooks%2Fpresentations%2FABZ%202021.ipynb\n",
+ "\n",
+ "Download and install locally: https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel"
+ ]
+ }
+ ],
+ "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"
+ },
+ "vscode": {
+ "interpreter": {
+ "hash": "301501caf4ced90c88b4867a75dc974b7f77d88824feb914d0cf4e75e12213b3"
+ }
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}