diff --git a/notebooks/presentations/ABZ 2021.ipynb b/notebooks/presentations/ABZ 2021.ipynb
index 558d784dbcca68514a249fabfe108c44efd5b1fe..d7eaec16c5944fe17d1eb4beeb1c0b517f7d5a3a 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`, ...)"
]
}
],