minor fixes

5eb7580f · Michael Leuschel · 4f033988 · 5eb7580f
Commit 5eb7580f authored May 5, 2020 by Michael Leuschel
--- a/info4/kapitel-2/DFA.ipynb
+++ b/info4/kapitel-2/DFA.ipynb
@@ -68,13 +68,13 @@
    "           (z1,0)↦z3, (z1,1)↦z2,\n",
    "           (z2,0)↦z2, (z2,1)↦z2,\n",
    "           (z3,0)↦z3, (z3,1)↦z3 }\n",
-    "DEFINITIONS\n",
-    "  CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F);\n",
-    "  CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F);\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})\n",
+    "  CUSTOM_GRAPH_EDGES3 == rec(color:\"black\",label:\"\",edges:{\"\" |-> z0}) // Kante für den Startknoten\n",
    "END"
   ]
  },
@@ -177,18 +177,18 @@
    "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",
-    "\\begin{itemize}\n",
+    "\n",
    "* dessen Knoten die Zustände von $M$ und\n",
-    "* dessen Kanten Zustands\"uberg\"ange gemäß der\n",
-    "  Überführungs\\-funktion $\\delta$ repräsentieren.\n",
-    "* Gilt $\\delta(z,a) = z'$ f\"ur ein Symbol $a \\in \\Sigma$ und für\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",
+    "  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 Jupyter-Kernels. Falls diese bei ihnen nicht funktioniert schauen Sie sich die Abbildung auf den Folien an)."
+    "(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:markdown id: tags:

 ## Endliche Automaten : DFA


 Jede Klasse der Chomsky-Hierarchie kann durch einen geeigneten Automatentypen charakterisiert
 werden. Beispielsweise kann jede reguläre Sprache (Typ 3) durch einen endlichen Automaten
 erkannt werden, und jede von einem endlichen Automaten erkannte Sprache ist
 regulär.

 Endliche Automaten sind weit verbreitet. Ein Beispiel ist die Spezifikation des [DHCP Protokolls](http://www.tcpipguide.com/free/t_DHCPGeneralOperationandClientFiniteStateMachine.htm#Figure_262):

 <img src="http://www.tcpipguide.com/free/diagrams/dhcpfsm.png" width="500"/>

 %% Cell type:markdown id: tags:


 ### DFA

 Ein __deterministischer endlicher Automat__ (kurz DFA für
  deterministic finite automaton) ist ein Quintupel
  $M =(\Sigma, Z, \delta , z_0, F)$, wobei
 * $\Sigma$ ein Alphabet ist,
 * $Z$ eine endliche Menge von Zuständen mit
  $\Sigma \cap Z = \emptyset$,
 * $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion,
 * $z_0 \in Z$ der Startzustand und
 * $F \subseteq Z$ die Menge der Endzustände (Finalzustände).

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE DFA
 SETS
   Z = {z0,z1,z2,z3}
 CONSTANTS Σ, F, δ
 PROPERTIES
 F ⊆ Z ∧
 δ ∈ (Z×Σ) → Z
 ∧
 /* Der Automat von Folie 10: */
 Σ = {0,1} ∧
- F={z2} ∧
+ F = {z2} ∧
 δ = {     (z0,0)↦z1, (z0,1)↦z3,
           (z1,0)↦z3, (z1,1)↦z2,
           (z2,0)↦z2, (z2,1)↦z2,
           (z3,0)↦z3, (z3,1)↦z3 }
-DEFINITIONS
-  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
-  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
+DEFINITIONS // Für den Zustandsgraphen:
+  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
+  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
-  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
+  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0}) // Kante für den Startknoten
 END
 ```

 %% Output

    Loaded machine: DFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:markdown id: tags:

 Ein Automat befindet sich jeweils in einem der Zustände $z$ aus Z. Er kann dann in diesem Zustand ein Symbol $x$ aus $\Sigma$ verarbeiten und wechselt dann in den Zustand $\delta(z,x)$.
 Zum Beispiel, wenn der DFA im Zustand z0 das Symbol $0$ erhält wechselt er nach:

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,0)
 ```

 %% Output

    $\mathit{z1}$
    z1

 %% Cell type:markdown id: tags:

 Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:

 %% Cell type:code id: tags:

 ``` prob
 δ(z1,1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 Da $z2\in F$ ein Endzustand ist, akzeptiert der DFA das Wort $01$ (oder $[0,1]$ in der Notation vom Notebook).

 %% Cell type:markdown id: tags:

 #### Zustandgraph

 Man kann den DFA auch grafisch darstellen: Endzustände sind mit einem doppelten Kreis gekennzeichnet, der Anfangszustand wird durch eine besondere Startkante gekennzeichnet.

 Formal ist dies so definiert:
 Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ lässt sich anschaulich durch
 seinen __Zustandsgraphen__ darstellen,
-\begin{itemize}
+
 * dessen Knoten die Zustände von $M$ und
-* dessen Kanten Zustands"uberg"ange gemäß der
-  Überführungs\-funktion $\delta$ repräsentieren.
-* Gilt $\delta(z,a) = z'$ f"ur ein Symbol $a \in \Sigma$ und für
+* dessen Kanten Zustandsübergänge gemäß der
+  Überführungsfunktion $\delta$ repräsentieren.
+* Gilt $\delta(z,a) = z'$ für ein Symbol $a \in \Sigma$ und für
  zwei Zustände $z, z' \in Z$, so hat dieser Graph eine gerichtete
-  Kante von $z$ nach~$z'$, die mit $a$ beschriftet ist.
+  Kante von $z$ nach $z'$, die mit $a$ beschriftet ist.
 * Der Startzustand wird durch einen Pfeil auf $z_0$ dargestellt.
 * Endzustände sind durch einen Doppelkreis markiert.

 Für den Automaten oben ergiebt dies folgenden Zustandsgraphen.
-(Anmerkung: diese Darstellung erfordert eine neue Version des Jupyter-Kernels. Falls diese bei ihnen nicht funktioniert schauen Sie sich die Abbildung auf den Folien an).
+(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 id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 #### Erweiterte Überführungsfunktion und akzeptierte Sprache

 Wir hatten gesehen, dass der Automat von $z0$ bei der Eingabe von $0$ nach $z1=\delta(z0,0)$
 wechselt und nach einer weiteren Eingabe von $1$ in den Zustand $z2 = \delta(z1,1)$ wechselt.
 Den aktuellen Zustand nach der Eingabe von dem Wort $01$ kann man also so berechnen:

 %% Cell type:code id: tags:

 ``` prob
 δ(δ(z0,0),1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 Dies führt zu der folgenden Definition, mit der man den Zustand nach einer beliebigen Folge von Eingabesymbolen berechnen kann:

 Sei $M = (\Sigma, Z, \delta , z_0, F)$  ein DFA.
 Die __erweiterte Überführungsfunktion
 $\widehat{\delta} : Z \times \Sigma^* \rightarrow Z$ von $M$ ist induktiv definiert:
 * ${\delta}(z, \lambda)  =  z$
 * ${\delta}(z, ax)       =  \widehat{\delta}(\delta(z,a), x) $
 für alle $z \in Z$, $a \in \Sigma$ und $x \in \Sigma^*$.

 Die vom DFA $M$ __akzeptierte Sprache__ ist definiert durch
 * $L(M) = \{w \in \Sigma^* \Longleftrightarrow \widehat{\delta}(z_0,w) \in F\}$

 Diese Definitionen sind in der folgenden B Maschine umgesetzt.
 $\widehat{\delta}$ wird durch die rekursive Funktion $\delta s$ dargestellt.

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE DFA
 SETS
   Z = {z0,z1,z2,z3}
 ABSTRACT_CONSTANTS δs, L
 CONSTANTS Σ, F, δ
 PROPERTIES
 F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs ∈ (Z×seq(Σ)) → Z ∧
 δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
           IF s=[] THEN z
           ELSE         δs(δ(z,first(s)),tail(s)) END)
 ∧
 /* Die vom Automaten akzeptierte Sprache L */
 L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
 ∧
 /* Der Automat von Folie 10: */
 Σ = {0,1} ∧
 F = {z2} ∧
 δ = {     (z0,0)↦z1, (z0,1)↦z3,
           (z1,0)↦z3, (z1,1)↦z2,
           (z2,0)↦z2, (z2,1)↦z2,
           (z3,0)↦z3, (z3,1)↦z3 }
 DEFINITIONS
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
 END
 ```

 %% Output

    Loaded machine: DFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:markdown id: tags:

 Man kann mit der erweiterten Überführungsfunktion den Zustand nach der Eingabe [0,1] so bestimmen:

 %% Cell type:code id: tags:

 ``` prob
 δs(z0,[0,1])
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 Da $z0\in F$ gilt:

 %% Cell type:code id: tags:

 ``` prob
 [0,1] ∈ L
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 δs(z0,[1,0])
 ```

 %% Output

    $\mathit{z3}$
    z3

 %% Cell type:markdown id: tags:

 Da $z3\not\in F$

 %% Cell type:code id: tags:

 ``` prob
 [1,0] ∈ L
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:markdown id: tags:

 Hier sind die Wörter der Länge 3 und 4 die vom DFA akzeptiert werden:

 %% Cell type:code id: tags:

 ``` prob
 :table {w1,w2,w3| [w1,w2,w3] : L}
 ```

 %% Output

    |w1|w2|w3|
    |---|---|---|
    |$0$|$1$|$0$|
    |$0$|$1$|$1$|
    w1	w2	w3
    0	1	0
    0	1	1

 %% Cell type:code id: tags:

 ``` prob
 :table {w1,w2,w3,w4| [w1,w2,w3,w4] : L}
 ```

 %% Output

    |w1|w2|w3|w4|
    |---|---|---|---|
    |$0$|$1$|$0$|$0$|
    |$0$|$1$|$0$|$1$|
    |$0$|$1$|$1$|$0$|
    |$0$|$1$|$1$|$1$|
    w1	w2	w3	w4
    0	1	0	0
    0	1	0	1
    0	1	1	0
    0	1	1	1

 %% Cell type:markdown id: tags:

 Anmerkung:
 Für $a \in \Sigma$ gilt $\widehat{\delta}(z, a) = \delta(z, a)$, und
 \item für $x = a_1 a_2 \cdots a_n$ in $\Sigma^*$ gilt:
 * $\widehat{\delta}(z, x) = \delta( \cdots \delta(\delta(z, a_1), a_2)\cdots , a_n).$

 Zum Beispiel:

 %% Cell type:code id: tags:

 ``` prob
 δs(z0,[0,1,1,1])
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 ist identisch zu:

 %% Cell type:code id: tags:

 ``` prob
 δ(δ(δ(δ(z0,0),1),1),1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 Was man schrittweise ausrechnen kann:

 %% Cell type:code id: tags:

 ``` prob
 δ(δ(δ(z1,1),1),1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:code id: tags:

 ``` prob
 δ(δ(z2,1),1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:code id: tags:

 ``` prob
 δ(z2,1)
 ```

 %% Output

    $\mathit{z2}$
    z2

 %% Cell type:markdown id: tags:

 Der Automat oben akzeptiert alle Wörter die mit 01 beginnen.

 Unten zeigen wir noch ein weiteres Beispiel.

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE DFA
 SETS
   Z = {z0,z1,z2}
 ABSTRACT_CONSTANTS δs, L
 CONSTANTS Σ, F, δ
 PROPERTIES
 F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs ∈ (Z×seq(Σ)) → Z ∧
 δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
           IF s=[] THEN z
           ELSE         δs(δ(z,first(s)),tail(s)) END)
 ∧
 /* Die vom Automaten akzeptierte Sprache L */
 L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
 ∧
 /* Der Automat von Folie 10: */
 Σ = {0,1} ∧
 F = {z0} ∧
 δ = {     (z0,0)↦z1, (z0,1)↦z2,
           (z1,0)↦z2, (z1,1)↦z0,
           (z2,0)↦z2, (z2,1)↦z2 }
 DEFINITIONS
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
 END
 ```

 %% Output

    Loaded machine: DFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:markdown id: tags:

 Dieser Automat akzeptiert zum Beispiel das leere Wort, da $z0 \in F$.
 Er akzeptiert auch:

 %% Cell type:code id: tags:

 ``` prob
 δs(z0,[0,1])
 ```

 %% Output

    $\mathit{z0}$
    z0

 %% Cell type:markdown id: tags:

 Er akzeptiert aber nicht das Wort [0]:

 %% Cell type:code id: tags:

 ``` prob
 δs(z0,[0])
 ```

 %% Output

    $\mathit{z1}$
    z1

 %% Cell type:code id: tags:

 ``` prob
 {[], [0,1], [0,1,0,1], [0,1,0,1,0,1]}  ⊆ L
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 [0] ∈ L
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:markdown id: tags:

 Der Zustandsgraph ist wie folgt:

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>