Skip to content
Snippets Groups Projects
Commit a52b19f7 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add picture

parent 5eb7580f
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-2/DFA.ipynb
+ 90
− 576
View file @ a52b19f7
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Endliche Automaten : DFA ## Endliche Automaten : DFA
Jede Klasse der Chomsky-Hierarchie kann durch einen geeigneten Automatentypen charakterisiert Jede Klasse der Chomsky-Hierarchie kann durch einen geeigneten Automatentypen charakterisiert
werden. Beispielsweise kann jede reguläre Sprache (Typ 3) durch einen endlichen Automaten werden. Beispielsweise kann jede reguläre Sprache (Typ 3) durch einen endlichen Automaten
erkannt werden, und jede von einem endlichen Automaten erkannte Sprache ist erkannt werden, und jede von einem endlichen Automaten erkannte Sprache ist
regulär. 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): 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"/> <img src="http://www.tcpipguide.com/free/diagrams/dhcpfsm.png" width="500"/>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### DFA ### DFA
Ein __deterministischer endlicher Automat__ (kurz DFA für Ein __deterministischer endlicher Automat__ (kurz DFA für
deterministic finite automaton) ist ein Quintupel deterministic finite automaton) ist ein Quintupel
$M =(\Sigma, Z, \delta , z_0, F)$, wobei $M =(\Sigma, Z, \delta , z_0, F)$, wobei
* $\Sigma$ ein Alphabet ist, * $\Sigma$ ein Alphabet ist,
* $Z$ eine endliche Menge von Zuständen mit * $Z$ eine endliche Menge von Zuständen mit
$\Sigma \cap Z = \emptyset$, $\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion, * $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion,
* $z_0 \in Z$ der Startzustand und * $z_0 \in Z$ der Startzustand und
* $F \subseteq Z$ die Menge der Endzustände (Finalzustände). * $F \subseteq Z$ die Menge der Endzustände (Finalzustände).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE DFA MACHINE DFA
SETS SETS
Z = {z0,z1,z2,z3} Z = {z0,z1,z2,z3}
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ F ⊆ Z ∧
δ ∈ (Z×Σ) → Z δ ∈ (Z×Σ) → Z
∧ ∧
/* Der Automat von Folie 10: */ /* Der Automat von Folie 10: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z2} ∧ F = {z2} ∧
δ = { (z0,0)↦z1, (z0,1)↦z3, δ = { (z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2, (z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2, (z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 } (z3,0)↦z3, (z3,1)↦z3 }
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustä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_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_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_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0}) // Kante für den Startknoten CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0}) // Kante für den Startknoten
END END
``` ```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% 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)$. Ein Automat befindet sich jeweils in einem der Zustände aus Z. Am Anfang befindet er sich in $z_0$.
Zum Beispiel, wenn der DFA im Zustand z0 das Symbol $0$ erhält wechselt er nach: Der Automat kann jeweils in einem Zustand $z$ ein Symbol $x$ aus $\Sigma$ verarbeiten und wechselt dann in den Zustand $\delta(z,x)$.
Zum Beispiel, wenn der DFA im Startzustand z0 das Symbol $0$ erhält wechselt er nach:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(z0,0) δ(z0,0)
``` ```
%% Output
$\mathit{z1}$
z1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach: Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(z1,1) δ(z1,1)
``` ```
%% Output %% 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).
### Arbeitsweise eines DFAs
Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ akzeptiert bzw. verwirft eine
Eingabe $x$ wie folgt:
* $M$ beginnt beim Anfangszustand $z_0$ und führt insgesamt $|x|$ Schritte aus.
* Der Lesekopf wandert dabei v.l.n.r. über das Eingabewort $x$, Symbol
für Symbol, und ändert dabei seinen Zustand jeweils gemäß der
Überführungsfunktion $\delta$:
Ist $M$ im Zustand $z \in Z$ und liest das
Symbol $a \in \Sigma$ und gilt $\delta(z,a) = z'$, so ändert $M$ seinen
Zustand in $z'$.
* Ist der letzte erreichte Zustand (nachdem $x$ abgearbeitet ist)
* ein Endzustand, so akzeptiert $M$ die Eingabe $x$;
* andernfalls lehnt $M$ sie ab.
$\mathit{z2}$ ![Arbeitsweise](./img/endl_auto.png)
z2
%% Cell type:markdown id: tags: %% 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). Da in diesem Automaten z0 kein Endzustand ist, wird zum Beispiel das leere Wort abgelehnt:
%% Cell type:code id: tags:
``` prob
z0 ∈ F
```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### Zustandgraph #### Zustandgraph
Man kann den DFA auch grafisch darstellen: Endzustände sind mit einem doppelten Kreis gekennzeichnet, der Anfangszustand wird durch eine besondere Startkante gekennzeichnet. 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: Formal ist dies so definiert:
Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ lässt sich anschaulich durch Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ lässt sich anschaulich durch
seinen __Zustandsgraphen__ darstellen, seinen __Zustandsgraphen__ darstellen,
* dessen Knoten die Zustände von $M$ und * dessen Knoten die Zustände von $M$ und
* dessen Kanten Zustandsübergänge gemäß der * dessen Kanten Zustandsübergänge gemäß der
Überführungsfunktion $\delta$ repräsentieren. Überführungsfunktion $\delta$ repräsentieren.
* Gilt $\delta(z,a) = z'$ für ein Symbol $a \in \Sigma$ und für * 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 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. * Der Startzustand wird durch einen Pfeil auf $z_0$ dargestellt.
* Endzustände sind durch einen Doppelkreis markiert. * Endzustände sind durch einen Doppelkreis markiert.
Für den Automaten oben ergiebt dies folgenden Zustandsgraphen. Für den Automaten oben ergiebt dies folgenden Zustandsgraphen.
(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). (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: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### Erweiterte Überführungsfunktion und akzeptierte Sprache #### Erweiterte Überführungsfunktion und akzeptierte Sprache
Wir hatten gesehen, dass der Automat von $z0$ bei der Eingabe von $0$ nach $z1=\delta(z0,0)$ 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. 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: Den aktuellen Zustand nach der Eingabe von dem Wort $01$ kann man also so berechnen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(δ(z0,0),1) δ(δ(z0,0),1)
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags: %% 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: 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. Sei $M = (\Sigma, Z, \delta , z_0, F)$ ein DFA.
Die __erweiterte Überführungsfunktion Die __erweiterte Überführungsfunktion
$\widehat{\delta} : Z \times \Sigma^* \rightarrow Z$ von $M$ ist induktiv definiert: $\widehat{\delta} : Z \times \Sigma^* \rightarrow Z$ von $M$ ist induktiv definiert:
* ${\delta}(z, \lambda) = z$ * ${\delta}(z, \lambda) = z$
* ${\delta}(z, ax) = \widehat{\delta}(\delta(z,a), x) $ * ${\delta}(z, ax) = \widehat{\delta}(\delta(z,a), x) $
für alle $z \in Z$, $a \in \Sigma$ und $x \in \Sigma^*$. für alle $z \in Z$, $a \in \Sigma$ und $x \in \Sigma^*$.
Die vom DFA $M$ __akzeptierte Sprache__ ist definiert durch Die vom DFA $M$ __akzeptierte Sprache__ ist definiert durch
* $L(M) = \{w \in \Sigma^* \Longleftrightarrow \widehat{\delta}(z_0,w) \in F\}$ * $L(M) = \{w \in \Sigma^* \Longleftrightarrow \widehat{\delta}(z_0,w) \in F\}$
Diese Definitionen sind in der folgenden B Maschine umgesetzt. Diese Definitionen sind in der folgenden B Maschine umgesetzt.
$\widehat{\delta}$ wird durch die rekursive Funktion $\delta s$ dargestellt. $\widehat{\delta}$ wird durch die rekursive Funktion $\delta s$ dargestellt.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE DFA MACHINE DFA
SETS SETS
Z = {z0,z1,z2,z3} Z = {z0,z1,z2,z3}
ABSTRACT_CONSTANTS δs, L ABSTRACT_CONSTANTS δs, L
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Definition der erweiterten Überführungsfunktion */ /* Definition der erweiterten Überführungsfunktion */
δs ∈ (Z×seq(Σ)) → Z ∧ δs ∈ (Z×seq(Σ)) → Z ∧
δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) | δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
IF s=[] THEN z IF s=[] THEN z
ELSE δs(δ(z,first(s)),tail(s)) END) ELSE δs(δ(z,first(s)),tail(s)) END)
∧ ∧
/* Die vom Automaten akzeptierte Sprache L */ /* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F} L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
∧ ∧
/* Der Automat von Folie 10: */ /* Der Automat von Folie 10: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z2} ∧ F = {z2} ∧
δ = { (z0,0)↦z1, (z0,1)↦z3, δ = { (z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2, (z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2, (z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 } (z3,0)↦z3, (z3,1)↦z3 }
DEFINITIONS DEFINITIONS
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""}); 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_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_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})
END END
``` ```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann mit der erweiterten Überführungsfunktion den Zustand nach der Eingabe [0,1] so bestimmen: Man kann mit der erweiterten Überführungsfunktion den Zustand nach der Eingabe [0,1] so bestimmen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(z0,[0,1]) δs(z0,[0,1])
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Da $z0\in F$ gilt: Da $z0\in F$ gilt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[0,1] ∈ L [0,1] ∈ L
``` ```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(z0,[1,0]) δs(z0,[1,0])
``` ```
%% Output
$\mathit{z3}$
z3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Da $z3\not\in F$ Da $z3\not\in F$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[1,0] ∈ L [1,0] ∈ L
``` ```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier sind die Wörter der Länge 3 und 4 die vom DFA akzeptiert werden: Hier sind die Wörter der Länge 3 und 4 die vom DFA akzeptiert werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {w1,w2,w3| [w1,w2,w3] : L} :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: %% Cell type:code id: tags:
``` prob ``` prob
:table {w1,w2,w3,w4| [w1,w2,w3,w4] : L} :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: %% Cell type:markdown id: tags:
Anmerkung: Anmerkung:
Für $a \in \Sigma$ gilt $\widehat{\delta}(z, a) = \delta(z, a)$, und 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: \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).$ * $\widehat{\delta}(z, x) = \delta( \cdots \delta(\delta(z, a_1), a_2)\cdots , a_n).$
Zum Beispiel: Zum Beispiel:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(z0,[0,1,1,1]) δs(z0,[0,1,1,1])
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
ist identisch zu: ist identisch zu:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(δ(δ(δ(z0,0),1),1),1) δ(δ(δ(δ(z0,0),1),1),1)
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Was man schrittweise ausrechnen kann: Was man schrittweise ausrechnen kann:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(δ(δ(z1,1),1),1) δ(δ(δ(z1,1),1),1)
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(δ(z2,1),1) δ(δ(z2,1),1)
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(z2,1) δ(z2,1)
``` ```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Der Automat oben akzeptiert alle Wörter die mit 01 beginnen. Der Automat oben akzeptiert alle Wörter die mit 01 beginnen.
Unten zeigen wir noch ein weiteres Beispiel. Unten zeigen wir noch ein weiteres Beispiel.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE DFA MACHINE DFA
SETS SETS
Z = {z0,z1,z2} Z = {z0,z1,z2}
ABSTRACT_CONSTANTS δs, L ABSTRACT_CONSTANTS δs, L
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Definition der erweiterten Überführungsfunktion */ /* Definition der erweiterten Überführungsfunktion */
δs ∈ (Z×seq(Σ)) → Z ∧ δs ∈ (Z×seq(Σ)) → Z ∧
δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) | δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
IF s=[] THEN z IF s=[] THEN z
ELSE δs(δ(z,first(s)),tail(s)) END) ELSE δs(δ(z,first(s)),tail(s)) END)
∧ ∧
/* Die vom Automaten akzeptierte Sprache L */ /* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F} L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
∧ ∧
/* Der Automat von Folie 10: */ /* Der Automat von Folie 10: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z0} ∧ F = {z0} ∧
δ = { (z0,0)↦z1, (z0,1)↦z2, δ = { (z0,0)↦z1, (z0,1)↦z2,
(z1,0)↦z2, (z1,1)↦z0, (z1,0)↦z2, (z1,1)↦z0,
(z2,0)↦z2, (z2,1)↦z2 } (z2,0)↦z2, (z2,1)↦z2 }
DEFINITIONS DEFINITIONS
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""}); 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_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_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})
END END
``` ```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Dieser Automat akzeptiert zum Beispiel das leere Wort, da $z0 \in F$. Dieser Automat akzeptiert zum Beispiel das leere Wort, da $z0 \in F$.
Er akzeptiert auch: Er akzeptiert auch:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(z0,[0,1]) δs(z0,[0,1])
``` ```
%% Output
$\mathit{z0}$
z0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Er akzeptiert aber nicht das Wort [0]: Er akzeptiert aber nicht das Wort [0]:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(z0,[0]) δs(z0,[0])
``` ```
%% Output
$\mathit{z1}$
z1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{[], [0,1], [0,1,0,1], [0,1,0,1,0,1]} ⊆ L {[], [0,1], [0,1,0,1], [0,1,0,1,0,1]} ⊆ L
``` ```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[0] ∈ L [0] ∈ L
``` ```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Der Zustandsgraph ist wie folgt: Der Zustandsgraph ist wie folgt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output
<Dot visualization: custom_graph []>
......
info4/kapitel-2/img/endl_auto.png 0 → 100644
+ 0
− 0
View file @ a52b19f7
info4/kapitel-2/img/endl_auto.png

19.7 KiB

0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment