From 9b059dd9f118cfa7825d453ee448e8a00ca96580 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 7 Jun 2021 23:13:01 +0200 Subject: [PATCH] Update ABZ 2021 slides --- notebooks/presentations/ABZ 2021.ipynb | 680 ++++++++++++------------- 1 file changed, 326 insertions(+), 354 deletions(-) diff --git a/notebooks/presentations/ABZ 2021.ipynb b/notebooks/presentations/ABZ 2021.ipynb index 558d784..d7eaec1 100644 --- a/notebooks/presentations/ABZ 2021.ipynb +++ b/notebooks/presentations/ABZ 2021.ipynb @@ -64,12 +64,9 @@ "* 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" + "* Also supports languages other than Python\n", + "* Language integration provided by a separate *kernel*\n", + "* Kernels: Python, Julia, Java, B, others" ] }, { @@ -83,12 +80,9 @@ "## 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", + "* Based on a solver for predicate logic, arithmetic, set theory\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" + "* Also understands some other formalisms, e.g. TLA<sup>+</sup> and Z" ] }, { @@ -175,10 +169,10 @@ { "data": { "text/markdown": [ - "$\\{1,2,3,4,5,10,11,12,13,14,15\\}$" + "$\\{-3,1,2,3,4,5,10,18\\}$" ], "text/plain": [ - "{1,2,3,4,5,10,11,12,13,14,15}" + "{−3,1,2,3,4,5,10,18}" ] }, "execution_count": 3, @@ -187,7 +181,7 @@ } ], "source": [ - "1..5 \\/ 10..15" + "1..5 \\/ {-3, 4, 10, 18}" ] }, { @@ -292,73 +286,13 @@ } }, "source": [ - "Convenient multiline input, with syntax highlighting and code completion" + "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": { @@ -372,7 +306,7 @@ "9\t5\t6\t7\t1\t0\t8\t2\n" ] }, - "execution_count": 8, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -381,7 +315,7 @@ ":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", + "& 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", @@ -407,7 +341,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -419,18 +353,18 @@ "{(2↦1),(3↦1),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(5↦4)}" ] }, - "execution_count": 9, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{x,y|x:1..5 & y:1..5 & x>y}" + "{x,y | x:1..5 & y:1..5 & x>y}" ] }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -439,7 +373,7 @@ "Preference changed: DOT_ENGINE = circo\n" ] }, - "execution_count": 10, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -450,7 +384,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -574,13 +508,13 @@ "<Dot visualization: expr_as_graph [(\"K5\",{x,y|x:1..5 & y:1..5 & x>y})]>" ] }, - "execution_count": 11, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"K5\", {x,y|x:1..5 & y:1..5 & x>y})" + ":dot expr_as_graph (\"K5\", {x,y | x:1..5 & y:1..5 & x>y})" ] }, { @@ -592,7 +526,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -601,7 +535,7 @@ "Loaded machine: Lift" ] }, - "execution_count": 12, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -610,16 +544,16 @@ "MACHINE Lift\n", "VARIABLES curfloor\n", "INVARIANT curfloor : 1..5\n", - "INITIALISATION curfloor := 5\n", + "INITIALISATION curfloor := 1\n", "OPERATIONS\n", - " up = PRE curfloor < 5 THEN curfloor := curfloor + 1 END;\n", - " down = BEGIN curfloor := curfloor - 1 END\n", + " up = PRE curfloor <= 5 THEN curfloor := curfloor + 1 END;\n", + " down = PRE curfloor > 1 THEN curfloor := curfloor - 1 END\n", "END" ] }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -628,7 +562,7 @@ "Executed operation: INITIALISATION()" ] }, - "execution_count": 13, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -646,19 +580,19 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$5$" + "$1$" ], "text/plain": [ - "5" + "1" ] }, - "execution_count": 14, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -669,39 +603,39 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Executed operation: down()" + "Executed operation: up()" ] }, - "execution_count": 15, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":exec down" + ":exec up" ] }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$4$" + "$2$" ], "text/plain": [ - "4" + "2" ] }, - "execution_count": 16, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -712,13 +646,13 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 16, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "0.093 sec, 7 of 8 states processed, 12 transitions" + "0.033 sec, 7 of 7 states processed, 11 transitions" ] }, "metadata": {}, @@ -731,7 +665,7 @@ "Use :trace to view the trace to the error state." ] }, - "execution_count": 17, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -742,7 +676,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -750,23 +684,23 @@ "text/markdown": [ "* -1: Root state\n", "* 0: `INITIALISATION()`\n", - "* 1: `down()`\n", - "* 2: `down()`\n", - "* 3: `down()`\n", - "* 4: `down()`\n", - "* 5: `down()` **(current)**" + "* 1: `up()`\n", + "* 2: `up()`\n", + "* 3: `up()`\n", + "* 4: `up()`\n", + "* 5: `up()` **(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)" + "1: up()\n", + "2: up()\n", + "3: up()\n", + "4: up()\n", + "5: up() (current)" ] }, - "execution_count": 18, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -777,7 +711,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 18, "metadata": { "scrolled": true }, @@ -791,11 +725,11 @@ "<!-- 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", + "<svg width=\"999pt\" height=\"90pt\"\n", + " viewBox=\"0.00 0.00 998.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", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-85.8853 994.9253,-85.8853 994.9253,4 -4,4\"/>\n", "<!-- root -->\n", "<g id=\"node1\" class=\"node\">\n", "<title>root</title>\n", @@ -806,7 +740,7 @@ "<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", + "<text text-anchor=\"middle\" x=\"197.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 1</text>\n", "</g>\n", "<!-- root->0 -->\n", "<g id=\"edge1\" class=\"edge\">\n", @@ -819,21 +753,21 @@ "<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", + "<text text-anchor=\"middle\" x=\"342.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 2</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", + "<text text-anchor=\"middle\" x=\"259.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", "</g>\n", "<!-- 1->0 -->\n", - "<g id=\"edge3\" class=\"edge\">\n", + "<g id=\"edge4\" 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", + "<text text-anchor=\"middle\" x=\"259.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", "</g>\n", "<!-- 2 -->\n", "<g id=\"node4\" class=\"node\">\n", @@ -842,92 +776,79 @@ "<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", + "<g id=\"edge3\" 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", + "<text text-anchor=\"middle\" x=\"404.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", "</g>\n", "<!-- 2->1 -->\n", - "<g id=\"edge5\" class=\"edge\">\n", + "<g id=\"edge6\" 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", + "<text text-anchor=\"middle\" x=\"404.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</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", + "<text text-anchor=\"middle\" x=\"632.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 4</text>\n", "</g>\n", "<!-- 2->3 -->\n", - "<g id=\"edge6\" class=\"edge\">\n", + "<g id=\"edge5\" 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", + "<text text-anchor=\"middle\" x=\"549.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", "</g>\n", "<!-- 3->2 -->\n", - "<g id=\"edge7\" class=\"edge\">\n", + "<g id=\"edge8\" 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", + "<text text-anchor=\"middle\" x=\"549.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</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", + "<text text-anchor=\"middle\" x=\"777.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 5</text>\n", "</g>\n", "<!-- 3->4 -->\n", - "<g id=\"edge8\" class=\"edge\">\n", + "<g id=\"edge7\" 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", + "<text text-anchor=\"middle\" x=\"694.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n", "</g>\n", "<!-- 4->3 -->\n", - "<g id=\"edge9\" class=\"edge\">\n", + "<g id=\"edge10\" 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", + "<text text-anchor=\"middle\" x=\"694.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</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", + "<text text-anchor=\"middle\" x=\"938.2849\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 6</text>\n", "</g>\n", "<!-- 4->5 -->\n", - "<g id=\"edge10\" class=\"edge\">\n", + "<g id=\"edge9\" 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", + "<text text-anchor=\"middle\" x=\"844.7876\" y=\"-67.3784\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</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", + "<text text-anchor=\"middle\" x=\"846.072\" y=\"-20.9186\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n", "</g>\n", "</g>\n", "</svg>\n" @@ -936,7 +857,7 @@ "<Dot visualization: state_space []>" ] }, - "execution_count": 19, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -983,8 +904,7 @@ "* 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", + " * Adding/modifying/removing invariants/guards\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" @@ -1000,7 +920,7 @@ "source": [ "## Documentation of Models\n", "\n", - "* Notebooks can be used to document an existing model\n", + "* Notebooks can load existing models from files\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" @@ -1040,7 +960,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -1049,7 +969,7 @@ "Loaded machine: Jupyter_LibraryStrings" ] }, - "execution_count": 20, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -1073,7 +993,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -1085,7 +1005,7 @@ "3" ] }, - "execution_count": 21, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -1096,7 +1016,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -1108,7 +1028,7 @@ "0" ] }, - "execution_count": 22, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -1131,7 +1051,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -1143,7 +1063,7 @@ "{(1↦\"filename\"),(2↦\"ext\")}" ] }, - "execution_count": 23, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -1154,7 +1074,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -1166,7 +1086,7 @@ "{(1↦\"filename.ext\")}" ] }, - "execution_count": 24, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -1177,7 +1097,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 24, "metadata": {}, "outputs": [ { @@ -1189,7 +1109,7 @@ "{(1↦\"usr\"),(2↦\"local\"),(3↦\"lib\")}" ] }, - "execution_count": 25, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -1198,29 +1118,6 @@ "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": { @@ -1250,280 +1147,355 @@ } }, "source": [ - "## Example: Course Notes for Theoretical CS" + "## 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": 27, + "execution_count": 25, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Loaded machine: BaseTypes" + "Loaded machine: DFA" ] }, - "execution_count": 27, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "MACHINE BaseTypes\n", - "SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}\n", + "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": "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, + "execution_count": 26, "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)}" + "Executed operation: SETUP_CONSTANTS()" ] }, - "execution_count": 28, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "PERSONS × COLOURS" + ":constants" ] }, { "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, + "metadata": {}, "source": [ - "A particular relation could be the following one, which is a subset of PERSONS × COLOURS:" + "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": 29, + "execution_count": 27, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue}),(\\mathit{mary}\\mapsto\\mathit{blue})\\}$" + "$\\mathit{z1}$" ], "text/plain": [ - "{(peter↦green),(peter↦blue),(mary↦blue)}" + "z1" ] }, - "execution_count": 29, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{peter|->green,peter|->blue,mary|->blue}" + "δ(z0,0)" ] }, { "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, + "metadata": {}, "source": [ - "We can visualize this relation graphically as follows:" + "Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:" ] }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 28, "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/markdown": [ + "$\\mathit{z2}$" ], "text/plain": [ - "<Dot visualization: expr_as_graph [(\"r1\",{(peter,green),(peter,blue),(mary,blue)})]>" + "z2" ] }, - "execution_count": 30, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"r1\",{peter|->green,peter|->blue,mary|->blue})" + "δ(z1,1)" ] }, { - "cell_type": "code", - "execution_count": 31, + "cell_type": "markdown", "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}" + "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": { - "slideshow": { - "slide_type": "subslide" - } - }, + "metadata": {}, "source": [ - "As in B a relation is a set of pairs, all set operators can be applied to relations.\n", - "For example," + "Da in diesem Automaten z0 kein Endzustand ist, wird zum Beispiel das leere Wort abgelehnt:" ] }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 29, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue})\\}$" + "$\\mathit{FALSE}$" ], "text/plain": [ - "{(peter↦green),(peter↦blue)}" + "FALSE" ] }, - "execution_count": 32, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{peter|->green,peter|->blue,mary|->blue} - {mary|->blue}" + "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": 33, + "execution_count": 30, "metadata": {}, "outputs": [ { "data": { - "text/markdown": [ - "$\\{(\\mathit{mary}\\mapsto\\mathit{blue})\\}$" + "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: 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(.9854 .9854) rotate(0) translate(4 724)\">\n", + "<title>prob_graph</title>\n", + "<polygon fill=\"#ffffff\" 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=\"#d3d3d3\" stroke=\"#000000\" cx=\"34.4216\" cy=\"-360\" rx=\"18\" ry=\"18\"/>\n", + "<ellipse fill=\"none\" stroke=\"#000000\" cx=\"34.4216\" cy=\"-360\" rx=\"22\" ry=\"22\"/>\n", + "<text text-anchor=\"middle\" x=\"34.4216\" y=\"-356.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">z2</text>\n", + "</g>\n", + "<!-- 0->0 -->\n", + "<g id=\"edge3\" class=\"edge\">\n", + "<title>0->0</title>\n", + "<path fill=\"none\" stroke=\"#00ff00\" d=\"M56.2282,-363.3223C65.9841,-363.6387 74.4216,-362.5312 74.4216,-360 74.4216,-358.418 71.1257,-357.3921 66.2719,-356.9225\"/>\n", + "<polygon fill=\"#00ff00\" stroke=\"#00ff00\" points=\"66.3105,-353.4225 56.2282,-356.6777 66.14,-360.4204 66.3105,-353.4225\"/>\n", + "<text text-anchor=\"middle\" x=\"77.9216\" y=\"-356.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">1</text>\n", + "</g>\n", + "<!-- 0->0 -->\n", + "<g id=\"edge7\" class=\"edge\">\n", + "<title>0->0</title>\n", + "<path fill=\"none\" stroke=\"#ff0000\" d=\"M55.8373,-365.72C73.7278,-368.1645 92.4216,-366.2578 92.4216,-360 92.4216,-354.9155 80.0808,-352.7035 65.8569,-353.3639\"/>\n", + "<polygon fill=\"#ff0000\" stroke=\"#ff0000\" points=\"65.477,-349.8839 55.8373,-354.28 66.1145,-356.8548 65.477,-349.8839\"/>\n", + "<text text-anchor=\"middle\" x=\"95.9216\" y=\"-356.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">0</text>\n", + "</g>\n", + "<!-- 1 -->\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>1</title>\n", + "<ellipse fill=\"#d3d3d3\" stroke=\"#000000\" cx=\"342.8583\" cy=\"-360\" rx=\"18\" ry=\"18\"/>\n", + "<text text-anchor=\"middle\" x=\"342.8583\" y=\"-356.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">z0</text>\n", + "</g>\n", + "<!-- 2 -->\n", + "<g id=\"node3\" class=\"node\">\n", + "<title>2</title>\n", + "<ellipse fill=\"#d3d3d3\" stroke=\"#000000\" cx=\"221.8362\" cy=\"-103.4192\" rx=\"18\" ry=\"18\"/>\n", + "<text text-anchor=\"middle\" x=\"221.8362\" y=\"-100.3192\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">z1</text>\n", + "</g>\n", + "<!-- 1->2 -->\n", + "<g id=\"edge5\" class=\"edge\">\n", + "<title>1->2</title>\n", + "<path fill=\"none\" stroke=\"#ff0000\" d=\"M335.1037,-343.5594C314.5681,-300.0216 258.6596,-181.4889 233.9062,-129.0089\"/>\n", + "<polygon fill=\"#ff0000\" stroke=\"#ff0000\" points=\"236.9578,-127.2741 229.5262,-119.7228 230.6267,-130.2604 236.9578,-127.2741\"/>\n", + "<text text-anchor=\"middle\" x=\"281.0049\" y=\"-239.6841\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">0</text>\n", + "</g>\n", + "<!-- 3 -->\n", + "<g id=\"node4\" class=\"node\">\n", + "<title>3</title>\n", + "<ellipse fill=\"#d3d3d3\" stroke=\"#000000\" cx=\"221.8362\" cy=\"-616.5808\" rx=\"18\" ry=\"18\"/>\n", + "<text text-anchor=\"middle\" x=\"221.8362\" y=\"-613.4808\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">z3</text>\n", + "</g>\n", + "<!-- 1->3 -->\n", + "<g id=\"edge1\" class=\"edge\">\n", + "<title>1->3</title>\n", + "<path fill=\"none\" stroke=\"#00ff00\" d=\"M335.1037,-376.4406C314.5681,-419.9784 258.6596,-538.5111 233.9062,-590.9911\"/>\n", + "<polygon fill=\"#00ff00\" stroke=\"#00ff00\" points=\"230.6267,-589.7396 229.5262,-600.2772 236.9578,-592.7259 230.6267,-589.7396\"/>\n", + "<text text-anchor=\"middle\" x=\"281.0049\" y=\"-487.1159\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">1</text>\n", + "</g>\n", + "<!-- 2->0 -->\n", + "<g id=\"edge2\" class=\"edge\">\n", + "<title>2->0</title>\n", + "<path fill=\"none\" stroke=\"#00ff00\" d=\"M210.95,-118.3231C180.2387,-160.3684 92.6205,-280.3225 53.587,-333.7615\"/>\n", + "<polygon fill=\"#00ff00\" stroke=\"#00ff00\" points=\"50.61,-331.9033 47.5379,-342.043 56.2627,-336.0322 50.61,-331.9033\"/>\n", + "<text text-anchor=\"middle\" x=\"128.7685\" y=\"-229.4423\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">1</text>\n", + "</g>\n", + "<!-- 2->3 -->\n", + "<g id=\"edge6\" class=\"edge\">\n", + "<title>2->3</title>\n", + "<path fill=\"none\" stroke=\"#ff0000\" d=\"M221.8362,-121.6828C221.8362,-198.4522 221.8362,-495.3108 221.8362,-588.4564\"/>\n", + "<polygon fill=\"#ff0000\" stroke=\"#ff0000\" points=\"218.3363,-588.536 221.8362,-598.536 225.3363,-588.536 218.3363,-588.536\"/>\n", + "<text text-anchor=\"middle\" x=\"218.3362\" y=\"-358.4696\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">0</text>\n", + "</g>\n", + "<!-- 3->3 -->\n", + "<g id=\"edge4\" class=\"edge\">\n", + "<title>3->3</title>\n", + "<path fill=\"none\" stroke=\"#00ff00\" d=\"M239.618,-619.8166C249.1512,-620.3665 257.8362,-619.2879 257.8362,-616.5808 257.8362,-614.9313 254.6111,-613.8864 249.9343,-613.4462\"/>\n", + "<polygon fill=\"#00ff00\" stroke=\"#00ff00\" points=\"249.6518,-609.9433 239.618,-613.3451 249.5832,-616.943 249.6518,-609.9433\"/>\n", + "<text text-anchor=\"middle\" x=\"261.3362\" y=\"-613.4808\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">1</text>\n", + "</g>\n", + "<!-- 3->3 -->\n", + "<g id=\"edge8\" class=\"edge\">\n", + "<title>3->3</title>\n", + "<path fill=\"none\" stroke=\"#ff0000\" d=\"M239.2565,-621.8967C256.6272,-624.927 275.8362,-623.1551 275.8362,-616.5808 275.8362,-611.2907 263.398,-609.11 249.4882,-610.039\"/>\n", + "<polygon fill=\"#ff0000\" stroke=\"#ff0000\" points=\"248.7691,-606.6 239.2565,-611.265 249.6019,-613.5503 248.7691,-606.6\"/>\n", + "<text text-anchor=\"middle\" x=\"279.3362\" y=\"-613.4808\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">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=\"#000000\" d=\"M470.4194,-360C442.5408,-360 399.4805,-360 371.2321,-360\"/>\n", + "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"371.1935,-356.5001 361.1934,-360 371.1934,-363.5001 371.1935,-356.5001\"/>\n", + "</g>\n", + "</g>\n", + "</svg>\n" ], "text/plain": [ - "{(mary↦blue)}" + "<Dot visualization: custom_graph []>" ] }, - "execution_count": 33, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{peter|->green,peter|->blue,mary|->blue} /\\ {mary}*COLOURS" + ":dot custom_graph" ] }, { @@ -1536,12 +1508,12 @@ "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", + "* ProB Jupyter notebooks allow conveniently working interactively with B\n", + "* Usable standalone or with existing models\n", + "* Applications: development, documentation, teaching\n", + "* Also has uses outside of formal methods, e.g. teaching theoretical CS\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`, ...)" + "* The Jupyter ecosystem provides a standard file format and useful tools (`nbconvert`, `nbgrader`, ...)" ] } ], -- GitLab