diff --git a/notebooks/presentations/ABZ 2021.ipynb b/notebooks/presentations/ABZ 2021.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..558d784dbcca68514a249fabfe108c44efd5b1fe --- /dev/null +++ b/notebooks/presentations/ABZ 2021.ipynb @@ -0,0 +1,1563 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, + "source": [ + "# ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods\n", + "\n", + "### David Geleßus, Michael Leuschel\n", + "### ABZ 2021\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", + " * Notebooks are saved as a file\n", + " * Code can be re-executed later\n", + " * Can be shared with other users\n", + "* Implementations: Mathematica, Maple, Jupyter, others" + ] + }, + { + "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", + "* Jupyter notebooks can also use languages other than Python\n", + "* Strict separation between frontend and kernel:\n", + " * The generic **frontend** implements e.g. the user interface and file format\n", + " * A language-specific **kernel** allows the frontend to use the language\n", + "* Language-neutral interface between frontend and kernel\n", + " * Kernels can be implemented in (nearly) any language - no Python code necessary" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "## ProB (https://prob.hhu.de/w/)\n", + "\n", + "* Animation, verification and visualisation tool for formal specifications\n", + "* Based on a solver for predicate logic, set theory with relations, functions, and arithmetic\n", + "* Supports mainly B specifications (classical B, Event-B)\n", + "* Also understands some other formalisms, e.g. TLA<sup>+</sup> and Z\n", + "* Core of ProB implemented in SICStus Prolog\n", + "* High-level Java API available\n", + "* Jupyter kernel written in Java based on this API" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, + "source": [ + "# 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": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$3$" + ], + "text/plain": [ + "3" + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "1 + 2" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{x} = 2$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tx = 2" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "1 + x = 3" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{1,2,3,4,5,10,11,12,13,14,15\\}$" + ], + "text/plain": [ + "{1,2,3,4,5,10,11,12,13,14,15}" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "1..5 \\/ 10..15" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Example: Set of all prime numbers < 500" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "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": 4, + "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": {}, + "source": [ + "Outputs are rendered as $\\LaTeX$ formulas:" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "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": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "Unicode symbols can also be used in inputs:" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "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": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{R} = 8$\n", + "* $\\mathit{S} = 9$\n", + "* $\\mathit{D} = 7$\n", + "* $\\mathit{E} = 5$\n", + "* $\\mathit{Y} = 2$\n", + "* $\\mathit{M} = 1$\n", + "* $\\mathit{N} = 6$\n", + "* $\\mathit{O} = 0$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tR = 8\n", + "\tS = 9\n", + "\tD = 7\n", + "\tE = 5\n", + "\tY = 2\n", + "\tM = 1\n", + "\tN = 6\n", + "\tO = 0" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{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" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "Finding all solutions as a set and displaying them as a table using the `:table` command:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|S|E|N|D|M|O|R|Y|\n", + "|---|---|---|---|---|---|---|---|\n", + "|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|\n" + ], + "text/plain": [ + "S\tE\tN\tD\tM\tO\tR\tY\n", + "9\t5\t6\t7\t1\t0\t8\t2\n" + ] + }, + "execution_count": 8, + "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": { + "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": 9, + "metadata": {}, + "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": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{x,y|x:1..5 & y:1..5 & x>y}" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT_ENGINE = circo\n" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT_ENGINE=circo" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", + "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", + " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", + "<!-- Generated by graphviz version 2.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": 11, + "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": {}, + "source": [ + "## Working with Machines" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: Lift" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "MACHINE Lift\n", + "VARIABLES curfloor\n", + "INVARIANT curfloor : 1..5\n", + "INITIALISATION curfloor := 5\n", + "OPERATIONS\n", + " up = PRE curfloor < 5 THEN curfloor := curfloor + 1 END;\n", + " down = BEGIN curfloor := curfloor - 1 END\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: INITIALISATION()" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Expressions are evaluated in the current state of the machine." + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$5$" + ], + "text/plain": [ + "5" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "curfloor" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: down()" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec down" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$4$" + ], + "text/plain": [ + "4" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "curfloor" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "0.093 sec, 7 of 8 states processed, 12 transitions" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "Model check uncovered an error: Invariant violation found.\n", + "Use :trace to view the trace to the error state." + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":modelcheck" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "* -1: Root state\n", + "* 0: `INITIALISATION()`\n", + "* 1: `down()`\n", + "* 2: `down()`\n", + "* 3: `down()`\n", + "* 4: `down()`\n", + "* 5: `down()` **(current)**" + ], + "text/plain": [ + "-1: Root state\n", + "0: INITIALISATION()\n", + "1: down()\n", + "2: down()\n", + "3: down()\n", + "4: down()\n", + "5: down() (current)" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":trace" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": { + "scrolled": true + }, + "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: visited_states Pages: 1 -->\n", + "<svg width=\"1148pt\" height=\"90pt\"\n", + " viewBox=\"0.00 0.00 1147.93 89.89\" 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 85.8853)\">\n", + "<title>visited_states</title>\n", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-85.8853 1143.9253,-85.8853 1143.9253,4 -4,4\"/>\n", + "<!-- root -->\n", + "<g id=\"node1\" class=\"node\">\n", + "<title>root</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"44.3223,-19.9205 88.4675,-51.4205 .177,-51.4205 44.3223,-19.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"44.3223\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n", + "</g>\n", + "<!-- 0 -->\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>0</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"233.6445,-58.9205 160.6445,-58.9205 160.6445,-22.9205 233.6445,-22.9205 233.6445,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"197.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 5</text>\n", + "</g>\n", + "<!-- root->0 -->\n", + "<g id=\"edge1\" class=\"edge\">\n", + "<title>root->0</title>\n", + "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"1,5\" d=\"M73.7879,-40.9205C95.5141,-40.9205 125.5073,-40.9205 150.4784,-40.9205\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"150.4791,-44.4206 160.479,-40.9205 150.479,-37.4206 150.4791,-44.4206\"/>\n", + "<text text-anchor=\"middle\" x=\"135.1332\" y=\"-31.3205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">INITIALISATION</text>\n", + "</g>\n", + "<!-- 1 -->\n", + "<g id=\"node3\" class=\"node\">\n", + "<title>1</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"378.6445,-58.9205 305.6445,-58.9205 305.6445,-22.9205 378.6445,-22.9205 378.6445,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"342.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 4</text>\n", + "</g>\n", + "<!-- 0->1 -->\n", + "<g id=\"edge2\" class=\"edge\">\n", + "<title>0->1</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M203.7517,-59.1114C225.8314,-86.2861 297.3874,-88.6347 328.0192,-66.1572\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"330.5878,-68.5471 335.4986,-59.1591 325.8052,-63.4356 330.5878,-68.5471\"/>\n", + "<text text-anchor=\"middle\" x=\"252.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "<!-- 1->0 -->\n", + "<g id=\"edge3\" class=\"edge\">\n", + "<title>1->0</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M335.5374,-22.7296C313.4576,4.4451 241.9017,6.7937 211.2699,-15.6838\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"208.7013,-13.2939 203.7905,-22.682 213.4839,-18.4054 208.7013,-13.2939\"/>\n", + "<text text-anchor=\"middle\" x=\"266.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", + "</g>\n", + "<!-- 2 -->\n", + "<g id=\"node4\" class=\"node\">\n", + "<title>2</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"523.6445,-58.9205 450.6445,-58.9205 450.6445,-22.9205 523.6445,-22.9205 523.6445,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"487.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 3</text>\n", + "</g>\n", + "<!-- 1->2 -->\n", + "<g id=\"edge4\" class=\"edge\">\n", + "<title>1->2</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M348.7517,-59.1114C370.8314,-86.2861 442.3874,-88.6347 473.0192,-66.1572\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"475.5878,-68.5471 480.4986,-59.1591 470.8052,-63.4356 475.5878,-68.5471\"/>\n", + "<text text-anchor=\"middle\" x=\"397.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "<!-- 2->1 -->\n", + "<g id=\"edge5\" class=\"edge\">\n", + "<title>2->1</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M480.5374,-22.7296C458.4576,4.4451 386.9017,6.7937 356.2699,-15.6838\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"353.7013,-13.2939 348.7905,-22.682 358.4839,-18.4054 353.7013,-13.2939\"/>\n", + "<text text-anchor=\"middle\" x=\"411.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", + "</g>\n", + "<!-- 3 -->\n", + "<g id=\"node5\" class=\"node\">\n", + "<title>3</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"668.6445,-58.9205 595.6445,-58.9205 595.6445,-22.9205 668.6445,-22.9205 668.6445,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"632.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 2</text>\n", + "</g>\n", + "<!-- 2->3 -->\n", + "<g id=\"edge6\" class=\"edge\">\n", + "<title>2->3</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M493.7517,-59.1114C515.8314,-86.2861 587.3874,-88.6347 618.0192,-66.1572\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"620.5878,-68.5471 625.4986,-59.1591 615.8052,-63.4356 620.5878,-68.5471\"/>\n", + "<text text-anchor=\"middle\" x=\"542.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "<!-- 3->2 -->\n", + "<g id=\"edge7\" class=\"edge\">\n", + "<title>3->2</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M625.5374,-22.7296C603.4576,4.4451 531.9017,6.7937 501.2699,-15.6838\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"498.7013,-13.2939 493.7905,-22.682 503.4839,-18.4054 498.7013,-13.2939\"/>\n", + "<text text-anchor=\"middle\" x=\"556.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", + "</g>\n", + "<!-- 4 -->\n", + "<g id=\"node6\" class=\"node\">\n", + "<title>4</title>\n", + "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"813.6445,-58.9205 740.6445,-58.9205 740.6445,-22.9205 813.6445,-22.9205 813.6445,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"777.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 1</text>\n", + "</g>\n", + "<!-- 3->4 -->\n", + "<g id=\"edge8\" class=\"edge\">\n", + "<title>3->4</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M638.7517,-59.1114C660.8314,-86.2861 732.3874,-88.6347 763.0192,-66.1572\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"765.5878,-68.5471 770.4986,-59.1591 760.8052,-63.4356 765.5878,-68.5471\"/>\n", + "<text text-anchor=\"middle\" x=\"687.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "<!-- 4->3 -->\n", + "<g id=\"edge9\" class=\"edge\">\n", + "<title>4->3</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M770.5374,-22.7296C748.4576,4.4451 676.9017,6.7937 646.2699,-15.6838\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"643.7013,-13.2939 638.7905,-22.682 648.4839,-18.4054 643.7013,-13.2939\"/>\n", + "<text text-anchor=\"middle\" x=\"701.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", + "</g>\n", + "<!-- 5 -->\n", + "<g id=\"node7\" class=\"node\">\n", + "<title>5</title>\n", + "<polygon fill=\"#ff3800\" stroke=\"#ff3800\" stroke-width=\"2\" points=\"987.0554,-33.4647 987.0554,-48.3764 958.4863,-58.9205 918.0835,-58.9205 889.5145,-48.3764 889.5145,-33.4647 918.0835,-22.9205 958.4863,-22.9205 987.0554,-33.4647\"/>\n", + "<polygon fill=\"none\" stroke=\"#ff3800\" stroke-width=\"2\" points=\"991.066,-30.6798 991.066,-51.1612 959.2046,-62.9205 917.3652,-62.9205 885.5038,-51.1612 885.5038,-30.6798 917.3652,-18.9205 959.2046,-18.9205 991.066,-30.6798\"/>\n", + "<text text-anchor=\"middle\" x=\"938.2849\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 0</text>\n", + "</g>\n", + "<!-- 4->5 -->\n", + "<g id=\"edge10\" class=\"edge\">\n", + "<title>4->5</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M784.4871,-59.1114C807.9991,-85.1504 881.9947,-88.395 918.088,-68.8454\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"920.403,-71.5093 926.793,-63.0584 916.5276,-65.6799 920.403,-71.5093\"/>\n", + "<text text-anchor=\"middle\" x=\"837.7876\" y=\"-67.3784\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "<!-- 5->4 -->\n", + "<g id=\"edge11\" class=\"edge\">\n", + "<title>5->4</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M926.9538,-18.9161C898.5346,4.7749 824.2191,5.7065 792.1902,-16.1212\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"789.6384,-13.7 784.351,-22.8812 794.2098,-19.0012 789.6384,-13.7\"/>\n", + "<text text-anchor=\"middle\" x=\"853.072\" y=\"-20.9186\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", + "</g>\n", + "<!-- 6 -->\n", + "<g id=\"node8\" class=\"node\">\n", + "<title>6</title>\n", + "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"1139.9253,-58.9205 1062.9253,-58.9205 1062.9253,-22.9205 1139.9253,-22.9205 1139.9253,-58.9205\"/>\n", + "<text text-anchor=\"middle\" x=\"1101.4253\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = -1</text>\n", + "</g>\n", + "<!-- 5->6 -->\n", + "<g id=\"edge12\" class=\"edge\">\n", + "<title>5->6</title>\n", + "<path fill=\"none\" stroke=\"#006391\" d=\"M991.2519,-40.9205C1010.9682,-40.9205 1033.2372,-40.9205 1052.5683,-40.9205\"/>\n", + "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"1052.6745,-44.4206 1062.6744,-40.9205 1052.6744,-37.4206 1052.6745,-44.4206\"/>\n", + "<text text-anchor=\"middle\" x=\"1008.4101\" y=\"-44.3205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", + "</g>\n", + "</g>\n", + "</svg>\n" + ], + "text/plain": [ + "<Dot visualization: state_space []>" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":dot state_space" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, + "source": [ + "# Applications" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "## Interactive Usage as a REPL\n", + "\n", + "* Jupyter Notebook can be used like a REPL\n", + "* Advantages: easy multi-line input, rich text output, advanced editor features, saveable" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "## Interactive Editing of Models\n", + "\n", + "* Any part of a notebook can be edited and re-executed\n", + "* Simplifies testing changes to the code, e.g.:\n", + " * Changing the values of constants and preferences\n", + " * Adding/removing invariants/guards\n", + " * Changing the order of operations\n", + "* Notebooks created by other users can be easily edited\n", + " * Notebook files are never \"read-only\"\n", + " * The same interface is used for viewing and editing notebooks" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "## Documentation of Models\n", + "\n", + "* Notebooks can be used to document an existing model\n", + "* Animation steps can be used to demonstrate behavior of model in specific cases\n", + "* Similar to trace files, but with ability to add inline explanations\n", + "* Visualisation features make states easier to understand" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "## Example: Documentation of ProB Standard Libraries" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# External Functions\n", + "## LibraryStrings\n", + "\n", + "In pure B there are only two built-in operators on strings: equality $=$ and inequality $\\neq$.\n", + "This library provides several string manipulation functions, and assumes that STRINGS are\n", + " sequences of unicode characters (in UTF-8 encoding).\n", + "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n", + "\n", + "`DEFINITIONS \"LibraryStrings.def\"`\n", + "\n", + "The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.\n", + "You can also include the machine `LibraryStrings.mch` instead of the definition file;\n", + " the machine defines some of the functions below as proper B functions (i.e., functions\n", + " for which you can compute the domain and use constructs such as\n", + " relational image)." + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: Jupyter_LibraryStrings" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "MACHINE Jupyter_LibraryStrings\n", + "DEFINITIONS \"LibraryStrings.def\"\n", + "END" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### STRING_LENGTH\n", + "\n", + "This external function takes a string and returns the length.\n", + "\n", + "Type: $STRING \\rightarrow INTEGER$." + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$3$" + ], + "text/plain": [ + "3" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_LENGTH(\"abc\")" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$0$" + ], + "text/plain": [ + "0" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_LENGTH(\"\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### STRING_SPLIT\n", + "\n", + "This external function takes two strings and separates the first string\n", + " according to the separator specified by the second string.\n", + "\n", + "Type: $STRING \\times STRING \\rightarrow \\mathit{seq}(STRING) $." + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(1\\mapsto\\text{\"filename\"}),(2\\mapsto\\text{\"ext\"})\\}$" + ], + "text/plain": [ + "{(1↦\"filename\"),(2↦\"ext\")}" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_SPLIT(\"filename.ext\",\".\")" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(1\\mapsto\\text{\"filename.ext\"})\\}$" + ], + "text/plain": [ + "{(1↦\"filename.ext\")}" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_SPLIT(\"filename.ext\",\"/\")" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(1\\mapsto\\text{\"usr\"}),(2\\mapsto\\text{\"local\"}),(3\\mapsto\\text{\"lib\"})\\}$" + ], + "text/plain": [ + "{(1↦\"usr\"),(2↦\"local\"),(3↦\"lib\")}" + ] + }, + "execution_count": 25, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_SPLIT(\"usr/local/lib\",\"/\")" + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(1\\mapsto\\text{\"\"})\\}$" + ], + "text/plain": [ + "{(1↦\"\")}" + ] + }, + "execution_count": 26, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "STRING_SPLIT(\"\",\".\")" + ] + }, + { + "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 concepts like relations, finite automata\n", + " * `nbconvert` renders notebooks to standard formats (HTML, PDF)\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" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: BaseTypes" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "MACHINE BaseTypes\n", + "SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}\n", + "END" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "In mathematics a binary relation over the sets $A$ and $B$ is defined to be\n", + " a subset of $A\\times B$.\n", + "The Cartesian product $A \\times B$ in turn is defined to be the set of pairs\n", + " $a \\mapsto b$ such that $a\\in A$ and $b\\in B$.\n", + " For example, we have:" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\mathit{peter}\\mapsto\\mathit{red}),(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue}),(\\mathit{paul}\\mapsto\\mathit{red}),(\\mathit{paul}\\mapsto\\mathit{green}),(\\mathit{paul}\\mapsto\\mathit{blue}),(\\mathit{mary}\\mapsto\\mathit{red}),(\\mathit{mary}\\mapsto\\mathit{green}),(\\mathit{mary}\\mapsto\\mathit{blue})\\}$" + ], + "text/plain": [ + "{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PERSONS × COLOURS" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "A particular relation could be the following one, which is a subset of PERSONS × COLOURS:" + ] + }, + { + "cell_type": "code", + "execution_count": 29, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue}),(\\mathit{mary}\\mapsto\\mathit{blue})\\}$" + ], + "text/plain": [ + "{(peter↦green),(peter↦blue),(mary↦blue)}" + ] + }, + "execution_count": 29, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{peter|->green,peter|->blue,mary|->blue}" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "We can visualize this relation graphically as follows:" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", + "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", + " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", + "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", + " -->\n", + "<!-- Title: state Pages: 1 -->\n", + "<svg width=\"440pt\" height=\"44pt\"\n", + " viewBox=\"0.00 0.00 440.00 44.00\" 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 40)\">\n", + "<title>state</title>\n", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-40 436,-40 436,4 -4,4\"/>\n", + "<!-- mary -->\n", + "<g id=\"node1\" class=\"node\">\n", + "<title>mary</title>\n", + "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"54,-36 0,-36 0,0 54,0 54,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"27\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">mary</text>\n", + "</g>\n", + "<!-- blue -->\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>blue</title>\n", + "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"180,-36 126,-36 126,0 180,0 180,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"153\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">blue</text>\n", + "</g>\n", + "<!-- mary->blue -->\n", + "<g id=\"edge1\" class=\"edge\">\n", + "<title>mary->blue</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M54.0302,-18C71.9281,-18 95.6509,-18 115.3839,-18\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"115.5798,-21.5001 125.5798,-18 115.5797,-14.5001 115.5798,-21.5001\"/>\n", + "<text text-anchor=\"middle\" x=\"78.707\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n", + "</g>\n", + "<!-- peter -->\n", + "<g id=\"node3\" class=\"node\">\n", + "<title>peter</title>\n", + "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"306,-36 252,-36 252,0 306,0 306,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"279\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">peter</text>\n", + "</g>\n", + "<!-- peter->blue -->\n", + "<g id=\"edge2\" class=\"edge\">\n", + "<title>peter->blue</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M251.9698,-18C234.0719,-18 210.3491,-18 190.6161,-18\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"190.4203,-14.5001 180.4202,-18 190.4202,-21.5001 190.4203,-14.5001\"/>\n", + "<text text-anchor=\"middle\" x=\"215.293\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n", + "</g>\n", + "<!-- green -->\n", + "<g id=\"node4\" class=\"node\">\n", + "<title>green</title>\n", + "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"432,-36 378,-36 378,0 432,0 432,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"405\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">green</text>\n", + "</g>\n", + "<!-- peter->green -->\n", + "<g id=\"edge3\" class=\"edge\">\n", + "<title>peter->green</title>\n", + "<path fill=\"none\" stroke=\"#b22222\" d=\"M306.0302,-18C323.9281,-18 347.6509,-18 367.3839,-18\"/>\n", + "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"367.5798,-21.5001 377.5798,-18 367.5797,-14.5001 367.5798,-21.5001\"/>\n", + "<text text-anchor=\"middle\" x=\"330.707\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n", + "</g>\n", + "</g>\n", + "</svg>\n" + ], + "text/plain": [ + "<Dot visualization: expr_as_graph [(\"r1\",{(peter,green),(peter,blue),(mary,blue)})]>" + ] + }, + "execution_count": 30, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":dot expr_as_graph (\"r1\",{peter|->green,peter|->blue,mary|->blue})" + ] + }, + { + "cell_type": "code", + "execution_count": 31, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|prj1|prj2|\n", + "|---|---|\n", + "|$\\mathit{peter}$|$\\mathit{green}$|\n", + "|$\\mathit{peter}$|$\\mathit{blue}$|\n", + "|$\\mathit{mary}$|$\\mathit{blue}$|\n" + ], + "text/plain": [ + "prj1\tprj2\n", + "peter\tgreen\n", + "peter\tblue\n", + "mary\tblue\n" + ] + }, + "execution_count": 31, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table {peter|->green,peter|->blue,mary|->blue}" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "As in B a relation is a set of pairs, all set operators can be applied to relations.\n", + "For example," + ] + }, + { + "cell_type": "code", + "execution_count": 32, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue})\\}$" + ], + "text/plain": [ + "{(peter↦green),(peter↦blue)}" + ] + }, + "execution_count": 32, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{peter|->green,peter|->blue,mary|->blue} - {mary|->blue}" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\mathit{mary}\\mapsto\\mathit{blue})\\}$" + ], + "text/plain": [ + "{(mary↦blue)}" + ] + }, + "execution_count": 33, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{peter|->green,peter|->blue,mary|->blue} /\\ {mary}*COLOURS" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, + "source": [ + "# Conclusion\n", + "\n", + "* the B language relatively close to the mathematical notation used when teaching theoretical computer science\n", + "* the B language supports functional programming, constraint programming, logical inference and proving\n", + "* ProB can be used to evaluate, animate, and visualize B (and other formalisms)\n", + "* the new Jupyter kernel allows creating interactive, executable documents\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`, ...)" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "ProB 2", + "language": "prob", + "name": "prob2" + }, + "language_info": { + "codemirror_mode": "prob2_jupyter_repl", + "file_extension": ".prob", + "mimetype": "text/x-prob2-jupyter-repl", + "name": "prob" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/notebooks/presentations/img/prob_logo.png b/notebooks/presentations/img/prob_logo.png new file mode 100644 index 0000000000000000000000000000000000000000..a836e0edd4cc8701cf957306ed2aad433e0657fd Binary files /dev/null and b/notebooks/presentations/img/prob_logo.png differ