diff --git a/notebooks/presentations/BadHonnef_2019.ipynb b/notebooks/presentations/BadHonnef_2019.ipynb index 605dc888af3e2088dbbad72aa1ad70d06bd82fd5..988a91d7b02deea91febb27e7abb196d3376e92d 100644 --- a/notebooks/presentations/BadHonnef_2019.ipynb +++ b/notebooks/presentations/BadHonnef_2019.ipynb @@ -1051,9 +1051,9 @@ } }, "source": [ - "# Anwendung: Skript für theoretische Informatik\n", + "# Anwendung: Skript für theoretische Informatik (NFA)\n", "\n", - "## NFA\n", + "Es folgen Teile aus dem Skript von Informatik 4 (Hauptautor Jörg Rothe).\n", "\n", "Nun erweitern wir die Überführungsfunktion in der Definition eines DFA \n", "und bezeichnen die neuen Automaten als NFA.\n", @@ -1095,22 +1095,21 @@ "Deshalb wird aus\n", "* $\\Sigma$ wird ```Sig```\n", "* $\\Sigma^*$ wird ```seq(Seq)```\n", - "* $\\delta$ wird ```delta```\n", - "* $\\widehat{\\delta}$ wird ```deltas```" + "* $\\widehat{\\delta}$ wird ```δs```" ] }, { "cell_type": "code", - "execution_count": 122, + "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Loaded machine: NFA_to_DFA" + "Loaded machine: NFA_nach_DFA" ] }, - "execution_count": 122, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -1120,20 +1119,21 @@ "MACHINE NFA_nach_DFA\n", "SETS\n", " Z = {z0,z1,z2,z3}\n", - "ABSTRACT_CONSTANTS deltas, L\n", - "CONSTANTS S, F, delta\n", + "DEFINITIONS Sig == {0,1}\n", + "ABSTRACT_CONSTANTS δs, L\n", + "CONSTANTS S, F, δ\n", "PROPERTIES\n", - " S ⊆ Z ∧ F ⊆ Z ∧ delta ∈ (Z×Sig) → ℙ(Z) ∧\n", + " S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Sig) → ℙ(Z) ∧\n", "\n", " /* Definition der erweiterten Übergangsfunktion */\n", - " deltas = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|deltas(delta(z,first(s)),tail(s))) END )\n", + " δs = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|δs(δ(z,first(s)),tail(s))) END )\n", " ∧\n", " /* die vom Automaten generierte Sprache */\n", - " L = {s|s∈seq(Sig) ∧ deltas(S,s) ∩ F ≠ ∅}\n", + " L = {s|s∈seq(Sig) ∧ δs(S,s) ∩ F ≠ ∅}\n", " ∧\n", " /* Nun ein Beispiel-Automat von Folie 24 (Info 4) */\n", " S = {z0} ∧ F={z2} ∧\n", - " delta = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},\n", + " δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},\n", " (z1,0)↦{z2}, (z1,1)↦{z2},\n", " (z2,0)↦{z3}, (z2,1)↦{z3},\n", " (z3,0)↦{z3}, (z3,1)↦{z3} }\n", @@ -1142,7 +1142,7 @@ }, { "cell_type": "code", - "execution_count": 123, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -1151,7 +1151,7 @@ "Machine constants set up using operation 0: $setup_constants()" ] }, - "execution_count": 123, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -1162,7 +1162,7 @@ }, { "cell_type": "code", - "execution_count": 124, + "execution_count": 6, "metadata": {}, "outputs": [ { @@ -1171,7 +1171,7 @@ "Machine initialised using operation 1: $initialise_machine()" ] }, - "execution_count": 124, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } @@ -1193,7 +1193,7 @@ }, { "cell_type": "code", - "execution_count": 125, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -1205,13 +1205,13 @@ "{z0,z1}" ] }, - "execution_count": 125, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "delta(z0,1)" + "δ(z0,1)" ] }, { @@ -1223,7 +1223,7 @@ }, { "cell_type": "code", - "execution_count": 126, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -1235,13 +1235,13 @@ "2" ] }, - "execution_count": 126, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "card(delta(z0,1))" + "card(δ(z0,1))" ] }, { @@ -1260,7 +1260,7 @@ }, { "cell_type": "code", - "execution_count": 134, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -1289,18 +1289,18 @@ "z3\t1\t{z3}\n" ] }, - "execution_count": 134, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":table delta" + ":table δ" ] }, { "cell_type": "code", - "execution_count": 133, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -1381,16 +1381,17 @@ "</svg>" ], "text/plain": [ - "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:delta(x, 0)})]>" + "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:δ(x, 0)})]>" ] }, - "execution_count": 133, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"0\",{x,y| x∈Z & y:delta(x,0)},\"1\",{x,y| x∈S & y:delta(x,1)})" + ":dot expr_as_graph (\"0\",{x,y| x∈Z & y:δ(x,0)},\n", + " \"1\",{x,y| x∈S & y∈δ(x,1)})" ] }, { @@ -1406,7 +1407,7 @@ }, { "cell_type": "code", - "execution_count": 131, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -1418,13 +1419,13 @@ "{z0,z1,z2,z3}" ] }, - "execution_count": 131, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "deltas(S,[1,1,1])" + "δs(S,[1,1,1])" ] }, { @@ -1436,7 +1437,7 @@ }, { "cell_type": "code", - "execution_count": 128, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -1448,18 +1449,18 @@ "{z2}" ] }, - "execution_count": 128, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "deltas(S,[1,1,1]) ∩ F" + "δs(S,[1,1,1]) ∩ F" ] }, { "cell_type": "code", - "execution_count": 129, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -1471,13 +1472,13 @@ "∅" ] }, - "execution_count": 129, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "deltas(S,[1,0,1]) ∩ F" + "δs(S,[1,0,1]) ∩ F" ] }, { @@ -1559,14 +1560,14 @@ } ], "source": [ - ":table {x,y,z| {x,y,z} ⊆ Sig & not([x,y,z]∈L)}" + ":table {x,y,z| {x,y,z} ⊆ Sig & ¬([x,y,z]∈L)}" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { - "slide_type": "subslide" + "slide_type": "slide" } }, "source": [ @@ -1632,7 +1633,7 @@ }, { "cell_type": "code", - "execution_count": 144, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -1709,13 +1710,13 @@ "{z3}\t1\t{z3}\n" ] }, - "execution_count": 144, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":table {x,a,y| a:Sig & x∈ℙ(Z) & y=deltas(x,[a])}" + ":table {x,a,y| a:Sig & x∈ℙ(Z) & y=δs(x,[a])}" ] }, { @@ -1731,7 +1732,7 @@ }, { "cell_type": "code", - "execution_count": 147, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -1740,7 +1741,7 @@ "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n" ] }, - "execution_count": 147, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -1751,7 +1752,7 @@ }, { "cell_type": "code", - "execution_count": 153, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -2098,17 +2099,17 @@ "</svg>" ], "text/plain": [ - "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & deltas(x, [0])=y})]>" + "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & δs(x, [0])=y})]>" ] }, - "execution_count": 153, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"0\",{x,y| x∈ℙ(Z) & deltas(x,[0]) = y},\n", - " \"1\",{x,y| x∈ℙ(Z) & deltas(x,[1]) = y},\n", + ":dot expr_as_graph (\"0\",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},\n", + " \"1\",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},\n", " \"start\", {x,y|x=y & x={z0}},\n", " \"end\", {x,y|x=y & x∩F ≠ ∅})" ] @@ -2122,8 +2123,14 @@ }, "source": [ "# Anwendung: Prüfbericht\n", + "ProB wird zur Datenvalidierung benutzt.\n", + "Man kann mit Jupyter auch Prüfberichte erstellen, inklusive der Darstellung von Gegenbeispielen und Erklärungen.\n", + "Als Beispiel werden hier keine Daten aus der Bahntechnik sondern Daten über chemische Elemente benutzt.\n", "\n", - "Dieser Bericht wurde mit folgender Version von ProB erstellt:" + "\n", + "## Validation Report: Chemical Elements\n", + "\n", + "This report was generated with the following version of ProB:" ] }, { @@ -2542,7 +2549,7 @@ } }, "source": [ - "We can now extract a table with the counter examples to the rule:" + "In case the property is false, we can extract a table with the counter examples to the rule:" ] }, { @@ -2584,6 +2591,26 @@ " DEC_STRING_TO_INT(aw1,3) > DEC_STRING_TO_INT(aw2,3))}" ] }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, + "source": [ + "# Anwendung: Modelldokumentation, Beschreibung von Szenarien, Tests\n", + "\n", + "Die ProB-Jupyter Kernel kann auch zur Erstellung von Dokumentation von B Modellen\n", + "benutzt werden:\n", + "- Beschreibung der Datenstrukturen und wie das Modell benutzt werden kann\n", + "- Beschreibung von gewünschten oder unerwünschten Szenarien\n", + "\n", + "### Beispiel: problematisches Szenario im AMASS Projekt: \n", + "\n", + "" + ] + }, { "cell_type": "markdown", "metadata": { @@ -2605,11 +2632,18 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ - "TO DO:\n", - "- Info4 Beispiel ?\n", - "- Railway Beispiel : Szenario mit Visualisierung" + "# Zusammenfassung\n", + "* die B Sprache ist relativ nahe an der Mathematik die man in der Lehre der Informatik verwendet\n", + "* die B Sprache erlaubt funktionale Programmierung, Constraint-Programmierung, logisches Schließen und Beweisen\n", + "* mit ProB kann man B (und TLA+ und Z) animieren, auswerten, grafisch darstellen\n", + "* mit dem neuen Jupyter Kernel kann man interaktive, ausführbare Dokumente erstellen.\n", + "* die Anwendungen sind hoffentlich vielfältig" ] }, {