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

adapt notebook for older probcli

parent 56cd46b7
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# NFA - Nichtdeterministische Automaten
Nun erweitern wir die Überführungsfunktion in der Definition eines DFA
und bezeichnen die neuen Automaten als NFA.
Ein __nichtdeterministischer endlicher Automat__
(kurz NFA) ist ein Quintupel $M = (\Sigma, Z, \delta , S, F)$, wobei
* $\Sigma$ ein Alphabet ist,
* $Z$ eine endliche Menge von Zust"anden mit
$\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow \mathfrak{P}(Z)$ die
Überführungsfunktion (hier: $\mathfrak{P}(Z)$ ist die Potenzmenge
* $\delta : Z \times \Sigma \rightarrow (Z)$ die
Überführungsfunktion (hier: $(Z)$ ist die Potenzmenge
von $Z$, also die Menge aller Teilmengen von $Z$),
* $S \subseteq Z$ die Menge der Startzustände und
* $F \subseteq Z$ die Menge der Endzust"ande (Finalzustände).
* $F \subseteq Z$ die Menge der Endzustände (Finalzustände).
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z0,z1,z2,z3}
CONSTANTS Σ, S, F, δ
PROPERTIES
F ⊆ Z ∧ S ⊆ Z ∧
δ ∈ (Z×Σ) → ℙ(Z)
/* Der Automat von Folie 21: */
Σ = {0,1} ∧
S = {z0} ∧ F = {z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z3}, (z2,1)↦{z3},
(z3,0)↦{z3}, (z3,1)↦{z3} }
DEFINITIONS // Für den Zustandsgraphen:
SET_PREF_DOT_LIMIT_PAGE_SIZE == FALSE; // requires brand-new probcli
SET_PREF_DOT_HORIZONTAL_LAYOUT == TRUE;
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:{x,y|y∈δ(x,0)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1)});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags:
Die Übergangsfunktion $\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustande an.
Dieser Automat ist nichtdeterministisch, für den Zustand 0 und die Eingabe 1 gibt es zwei mögliche Zielknoten:
%% Cell type:code id: tags:
``` prob
δ(z0,0)
```
%% Output
$\{\mathit{z0}\}$
{z0}
%% Cell type:code id: tags:
``` prob
δ(z0,1)
```
%% Output
$\{\mathit{z0},\mathit{z1}\}$
{z0,z1}
%% Cell type:code id: tags:
``` prob
card(δ(z0,1)) > 1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Wir können die Übergangsfunktion $\delta$ des Automaten auch als Tabelle darstellen:
%% Cell type:code id: tags:
``` prob
:table {x,a,y|y∈δ(x,a)}
```
%% Output
|x|a|y|
|---|---|---|
|$\mathit{z0}$|$0$|$\mathit{z0}$|
|$\mathit{z0}$|$1$|$\mathit{z0}$|
|$\mathit{z0}$|$1$|$\mathit{z1}$|
|$\mathit{z1}$|$0$|$\mathit{z2}$|
|$\mathit{z1}$|$1$|$\mathit{z2}$|
|$\mathit{z2}$|$0$|$\mathit{z3}$|
|$\mathit{z2}$|$1$|$\mathit{z3}$|
|$\mathit{z3}$|$0$|$\mathit{z3}$|
|$\mathit{z3}$|$1$|$\mathit{z3}$|
x a y
z0 0 z0
z0 1 z0
z0 1 z1
z1 0 z2
z1 1 z2
z2 0 z3
z2 1 z3
z3 0 z3
z3 1 z3
%% Cell type:markdown id: tags:
Der Zustandsgraph ist ähnlich zu vorher definiert. Die einzigen Unterschiede sind:
* es gibt möglicherweise mehrere Startzustände
* es gibt eine Kante von x nach y mit Label a falls $y \in \delta(x,a)$
Alle Kanten mit dem Label "0" sind:
%% Cell type:code id: tags:
``` prob
{x,y|y∈δ(x,0)}
```
%% Output
$\{(\mathit{z0}\mapsto \mathit{z0}),(\mathit{z1}\mapsto \mathit{z2}),(\mathit{z2}\mapsto \mathit{z3}),(\mathit{z3}\mapsto \mathit{z3})\}$
{(z0↦z0),(z1↦z2),(z2↦z3),(z3↦z3)}
%% Cell type:markdown id: tags:
und grafisch ist der komplette Zustandsgraph:
%% Cell type:code id: tags:
``` prob
:pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
```
%% Output
Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
### Sprache eines NFAs
Die __erweiterte Überführungsfunktion__
$\widehat{\delta} : \mathfrak{P}(Z) \times \Sigma^* \rightarrow
\mathfrak{P}(Z)$ von $M$ ist induktiv definiert:
$\widehat{\delta} : (Z) \times \Sigma^* \rightarrow
(Z)$ von $M$ ist induktiv definiert:
* $\widehat{\delta}(Z', \lambda) = Z'$
* ${\delta}(Z', ax) = \bigcup_{z \in Z'} \widehat{\delta}(\delta(z,a), x) $
für alle $Z' \subseteq Z$, $a \in \Sigma$ und $x \in \Sigma^*$.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z0,z1,z2,z3}
ABSTRACT_CONSTANTS L, δs
CONSTANTS Σ, S, F, δ
PROPERTIES
F ⊆ Z ∧ S ⊆ Z ∧
δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Überführungsfunktion */
δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
IF s=[] THEN Z′
ELSE ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
/* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
/* Der Automat von Folie 21: */
Σ = {0,1} ∧
S = {z0} ∧ F = {z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z3}, (z2,1)↦{z3},
(z3,0)↦{z3}, (z3,1)↦{z3} }
DEFINITIONS // Für den Zustandsgraphen:
SET_PREF_DOT_LIMIT_PAGE_SIZE == FALSE; // requires brand-new probcli
SET_PREF_DOT_HORIZONTAL_LAYOUT == TRUE;
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:{x,y|y∈δ(x,0)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1)});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags:
Wir generieren noch einmal den Zustandgraphen:
%% Cell type:code id: tags:
``` prob
:pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
```
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Die Funktion $\widehat{\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden.
Für das leere Wort bekommen wir die Startzustände zurück:
%% Cell type:code id: tags:
``` prob
δs({z0},[])
```
%% Output
$\{\mathit{z0}\}$
{z0}
%% Cell type:markdown id: tags:
Das leere Wort $\lambda$ wird nicht akzeptiert da $\widehat{\delta}(S,\lambda) \cap F$ leer ist:
%% Cell type:code id: tags:
``` prob
δs({z0},[]) ∩ F
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags:
Schauen wir uns nun die Wörter $0$ und $01$ an.
Wir haben
* $\widehat{\delta}(\{z_0\},0)$ =
* $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), \lambda)$ =
* $\delta(z_0,0)$.
%% Cell type:code id: tags:
``` prob
δs({z0},[0])
```
%% Output
$\{\mathit{z0}\}$
{z0}
%% Cell type:code id: tags:
``` prob
δ(z0,0)
```
%% Output
$\{\mathit{z0}\}$
{z0}
%% Cell type:code id: tags:
``` prob
δs(δ(z0,0),[])
```
%% Output
$\{\mathit{z0}\}$
{z0}
%% Cell type:markdown id: tags:
Wir haben
* $\widehat{\delta}(\{z_0\},01)$ =
* $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), 1)$ =
* $\widehat{\delta}(\delta(z_0,0), 1)$ =
* $\widehat{\delta}(\{z_0\}, 1)$ =
* $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,1), \lambda)$ =
* $\delta(z_0,1)$.
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1])
```
%% Output
$\{\mathit{z0},\mathit{z1}\}$
{z0,z1}
%% Cell type:code id: tags:
``` prob
δ(z0,1)
```
%% Output
$\{\mathit{z0},\mathit{z1}\}$
{z0,z1}
%% Cell type:markdown id: tags:
Das Wort $01$ wird nicht akzeptiert da $\widehat{\delta}(S,01) \cap F$ leer ist:
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1]) ∩ F
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags:
Wir haben
* $\widehat{\delta}(\{z_0\},011)$ =
* $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), 11)$ =
* $\widehat{\delta}(\delta(z_0,0), 11)$ =
* $\widehat{\delta}(\{z_0\}, 11)$ =
* $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,1), 1)$ =
* $\widehat{\delta}(\delta(z_0,1), 1)$ =
* $\widehat{\delta}(\{z_0,z_1\}, 1)$ =
* $\bigcup_{z \in \{z_0,z_1\}} \widehat{\delta}(\delta(z,1), \lambda)$ =
* $\delta(z_0,1) \cup \delta(z_1,1)$.
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1,1])
```
%% Output
$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$
{z0,z1,z2}
%% Cell type:code id: tags:
``` prob
δ(z0,1) ∪ δ(z1,1)
```
%% Output
$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$
{z0,z1,z2}
%% Cell type:markdown id: tags:
Das Wort $0111$ wird akzeptiert da $\widehat{\delta}(S,0111) \cap F$ nicht leer ist:
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1,1]) ∩ F
```
%% Output
$\{\mathit{z2}\}$
{z2}
%% Cell type:markdown id: tags:
Schauen wir uns nun das Wort $0111$ an. Hier erhalten wir mit $\widehat{\delta}$ die komplette Menge Z:
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1,1,1])
```
%% Output
$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$
{z0,z1,z2,z3}
%% Cell type:markdown id: tags:
Das Wort $0111$ wird akzeptiert da $\widehat{\delta}(S,0111) \cap F$ nicht leer ist:
%% Cell type:code id: tags:
``` prob
δs({z0},[0,1,1,1]) ∩ F
```
%% Output
$\{\mathit{z2}\}$
{z2}
%% Cell type:markdown id: tags:
$L(M) = \{w \in \{0,1\}^* \Longleftrightarrow w = u 1 v \text{ mit $u \in
\{0,1\}^*$ und $v \in \{0,1\}$}\}$.
%% Cell type:markdown id: tags:
## DFA versus NFA, Satz von Rabin und Scott}
Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs. Die
Antwort lautet: Nein.
### Theorem (Rabin und Scott)
Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert
werden.
#### Beweis
Sei $M = (\Sigma, Z, \delta , S, E)$ ein NFA.
Konstruiere einen zu
$M$ äquivalenten DFA
$M' = (\Sigma, ℙ(Z), \delta' ,z_0', F)$ wie folgt:
* Zustandsmenge von $M'$: die Potenzmenge $ℙ(Z)$ von $Z$,
* $\delta'(Z' , a) = \widehat{\delta}(Z',a)$ für alle $Z' \subseteq Z$ und $a \in \Sigma$,
* $z_0'=S$,
* $F = \{ Z' \subseteq Z \mid Z' \cap E \neq \emptyset\}$.
Offenbar sind M' und M äquivalent, denn für alle ...
%% Cell type:markdown id: tags:
Für den oben geladen Automaten können wir diese Konstruktion illustrieren.
Die Potenzmenge der Zustände ist:
%% Cell type:code id: tags:
``` prob
ℙ(Z)
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{z0}\},\{\mathit{z0},\mathit{z1}\},\{\mathit{z0},\mathit{z2}\},\{\mathit{z0},\mathit{z3}\},\{\mathit{z1}\},\{\mathit{z0},\mathit{z1},\mathit{z2}\},\{\mathit{z0},\mathit{z1},\mathit{z3}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z1},\mathit{z3}\},\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2}\},\{\mathit{z0},\mathit{z2},\mathit{z3}\},\{\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2},\mathit{z3}\},\{\mathit{z3}\}\}$
{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}
%% Cell type:markdown id: tags:
Jedes Element der Potenzmenge (ist eine Menge) und wird zu einem Zustand des NFAs.
Tabellarisch können wir $\widehat{\delta}$ für $ℙ(Z)$ wie folgt ausrechnen:
%% Cell type:code id: tags:
``` prob
:table {x,a,y| a∈Σ & x∈ℙ(Z) & y=δs(x,[a])}
```
%% Output
|x|a|y|
|---|---|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$0$|$\emptyset$|
|$\emptyset$|$1$|$\emptyset$|
|$\{\mathit{z0}\}$|$0$|$\{\mathit{z0}\}$|
|$\{\mathit{z0}\}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$0$|$\{\mathit{z0},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1}\}$|$0$|$\{\mathit{z2}\}$|
|$\{\mathit{z1}\}$|$1$|$\{\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
|$\{0\}$|$0$|$\{0\}$|
|$\{0\}$|$1$|$\{0,1\}$|
|$\{0,1\}$|$0$|$\{0,2\}$|
|$\{0,1\}$|$1$|$\{0,1,2\}$|
|$\{0,2\}$|$0$|$\{0,3\}$|
|$\{0,2\}$|$1$|$\{0,1,3\}$|
|$\{0,3\}$|$0$|$\{0,4\}$|
|$\{0,3\}$|$1$|$\{0,1,4\}$|
|$\{0,4\}$|$0$|$\{0,5\}$|
|$\{0,4\}$|$1$|$\{0,1,5\}$|
|$\{0,5\}$|$0$|$\{0,5\}$|
|$\{0,5\}$|$1$|$\{0,1,5\}$|
|$\{1\}$|$0$|$\{2\}$|
|$\{1\}$|$1$|$\{2\}$|
|$\{0,1,2\}$|$0$|$\{0,2,3\}$|
|$\{0,1,2\}$|$1$|$\{0,1,2,3\}$|
|$\{0,1,3\}$|$0$|$\{0,2,4\}$|
|$\{0,1,3\}$|$1$|$\{0,1,2,4\}$|
|$\{0,1,4\}$|$0$|$\{0,2,5\}$|
|$\{0,1,4\}$|$1$|$\{0,1,2,5\}$|
|$\{0,1,5\}$|$0$|$\{0,2,5\}$|
|$\{0,1,5\}$|$1$|$\{0,1,2,5\}$|
|$\{1,2\}$|$0$|$\{2,3\}$|
|$\{1,2\}$|$1$|$\{2,3\}$|
|$\{1,3\}$|$0$|$\{2,4\}$|
|$\{1,3\}$|$1$|$\{2,4\}$|
|$\{1,4\}$|$0$|$\{2,5\}$|
|$\{1,4\}$|$1$|$\{2,5\}$|
|$\{1,5\}$|$0$|$\{2,5\}$|
|$\{1,5\}$|$1$|$\{2,5\}$|
|$\{0,1,2,3\}$|$0$|$\{0,2,3,4\}$|
|$\{0,1,2,3\}$|$1$|$\{0,1,2,3,4\}$|
|$\{0,1,2,4\}$|$0$|$\{0,2,3,5\}$|
|$\{0,1,2,4\}$|$1$|$\{0,1,2,3,5\}$|
|$\{0,1,2,5\}$|$0$|$\{0,2,3,5\}$|
|$\{0,1,2,5\}$|$1$|$\{0,1,2,3,5\}$|
|$\{0,1,3,4\}$|$0$|$\{0,2,4,5\}$|
|$\{0,1,3,4\}$|$1$|$\{0,1,2,4,5\}$|
|$\{0,1,3,5\}$|$0$|$\{0,2,4,5\}$|
|$\{0,1,3,5\}$|$1$|$\{0,1,2,4,5\}$|
|$\{0,1,4,5\}$|$0$|$\{0,2,5\}$|
|$\{0,1,4,5\}$|$1$|$\{0,1,2,5\}$|
|$\{2\}$|$0$|$\{3\}$|
|$\{2\}$|$1$|$\{3\}$|
|$\{0,2,3\}$|$0$|$\{0,3,4\}$|
|$\{0,2,3\}$|$1$|$\{0,1,3,4\}$|
|$\{0,2,4\}$|$0$|$\{0,3,5\}$|
|$\{0,2,4\}$|$1$|$\{0,1,3,5\}$|
|$\{0,2,5\}$|$0$|$\{0,3,5\}$|
|$\{0,2,5\}$|$1$|$\{0,1,3,5\}$|
|$\{0,1,2,3,4\}$|$0$|$\{0,2,3,4,5\}$|
|$\{0,1,2,3,4\}$|$1$|$\{0,1,2,3,4,5\}$|
|$\{0,1,2,3,5\}$|$0$|$\{0,2,3,4,5\}$|
|$\{0,1,2,3,5\}$|$1$|$\{0,1,2,3,4,5\}$|
|$\{0,1,2,3,4,5\}$|$0$|$\{0,2,3,4,5\}$|
|$\{0,1,2,3,4,5\}$|$1$|$\{0,1,2,3,4,5\}$|
|$\{0,1,2,4,5\}$|$0$|$\{0,2,3,5\}$|
|$\{0,1,2,4,5\}$|$1$|$\{0,1,2,3,5\}$|
|$\{1,2,3\}$|$0$|$\{2,3,4\}$|
|$\{1,2,3\}$|$1$|$\{2,3,4\}$|
|$\{1,2,4\}$|$0$|$\{2,3,5\}$|
|$\{1,2,4\}$|$1$|$\{2,3,5\}$|
|$\{1,2,5\}$|$0$|$\{2,3,5\}$|
|$\{1,2,5\}$|$1$|$\{2,3,5\}$|
|$\{2,3\}$|$0$|$\{3,4\}$|
|$\{2,3\}$|$1$|$\{3,4\}$|
|$\{2,4\}$|$0$|$\{3,5\}$|
|$\{2,4\}$|$1$|$\{3,5\}$|
|$\{2,5\}$|$0$|$\{3,5\}$|
|$\{2,5\}$|$1$|$\{3,5\}$|
|$\{0,2,3,4\}$|$0$|$\{0,3,4,5\}$|
|$\{0,2,3,4\}$|$1$|$\{0,1,3,4,5\}$|
|$\{0,2,3,5\}$|$0$|$\{0,3,4,5\}$|
|$\{0,2,3,5\}$|$1$|$\{0,1,3,4,5\}$|
|$\{0,2,4,5\}$|$0$|$\{0,3,5\}$|
|$\{0,2,4,5\}$|$1$|$\{0,1,3,5\}$|
|$\{1,2,3,4\}$|$0$|$\{2,3,4,5\}$|
|$\{1,2,3,4\}$|$1$|$\{2,3,4,5\}$|
|$\{1,2,3,5\}$|$0$|$\{2,3,4,5\}$|
|$\{1,2,3,5\}$|$1$|$\{2,3,4,5\}$|
|$\{1,2,4,5\}$|$0$|$\{2,3,5\}$|
|$\{1,2,4,5\}$|$1$|$\{2,3,5\}$|
|$\{3\}$|$0$|$\{4\}$|
|$\{3\}$|$1$|$\{4\}$|
|$\{0,3,4\}$|$0$|$\{0,4,5\}$|
|$\{0,3,4\}$|$1$|$\{0,1,4,5\}$|
|$\{0,3,5\}$|$0$|$\{0,4,5\}$|
|$\{0,3,5\}$|$1$|$\{0,1,4,5\}$|
|$\{0,1,3,4,5\}$|$0$|$\{0,2,4,5\}$|
|$\{0,1,3,4,5\}$|$1$|$\{0,1,2,4,5\}$|
|$\{0,2,3,4,5\}$|$0$|$\{0,3,4,5\}$|
|$\{0,2,3,4,5\}$|$1$|$\{0,1,3,4,5\}$|
|$\{1,3,4\}$|$0$|$\{2,4,5\}$|
|$\{1,3,4\}$|$1$|$\{2,4,5\}$|
|$\{1,3,5\}$|$0$|$\{2,4,5\}$|
|$\{1,3,5\}$|$1$|$\{2,4,5\}$|
|$\{1,2,3,4,5\}$|$0$|$\{2,3,4,5\}$|
|$\{1,2,3,4,5\}$|$1$|$\{2,3,4,5\}$|
|$\{2,3,4\}$|$0$|$\{3,4,5\}$|
|$\{2,3,4\}$|$1$|$\{3,4,5\}$|
|$\{2,3,5\}$|$0$|$\{3,4,5\}$|
|$\{2,3,5\}$|$1$|$\{3,4,5\}$|
|$\{3,4\}$|$0$|$\{4,5\}$|
|$\{3,4\}$|$1$|$\{4,5\}$|
|$\{3,5\}$|$0$|$\{4,5\}$|
|$\{3,5\}$|$1$|$\{4,5\}$|
|$\{0,3,4,5\}$|$0$|$\{0,4,5\}$|
|$\{0,3,4,5\}$|$1$|$\{0,1,4,5\}$|
|$\{1,3,4,5\}$|$0$|$\{2,4,5\}$|
|$\{1,3,4,5\}$|$1$|$\{2,4,5\}$|
|$\{2,3,4,5\}$|$0$|$\{3,4,5\}$|
|$\{2,3,4,5\}$|$1$|$\{3,4,5\}$|
|$\{4\}$|$0$|$\{5\}$|
|$\{4\}$|$1$|$\{5\}$|
|$\{0,4,5\}$|$0$|$\{0,5\}$|
|$\{0,4,5\}$|$1$|$\{0,1,5\}$|
|$\{1,4,5\}$|$0$|$\{2,5\}$|
|$\{1,4,5\}$|$1$|$\{2,5\}$|
|$\{2,4,5\}$|$0$|$\{3,5\}$|
|$\{2,4,5\}$|$1$|$\{3,5\}$|
|$\{3,4,5\}$|$0$|$\{4,5\}$|
|$\{3,4,5\}$|$1$|$\{4,5\}$|
|$\{4,5\}$|$0$|$\{5\}$|
|$\{4,5\}$|$1$|$\{5\}$|
|$\{5\}$|$0$|$\{5\}$|
|$\{5\}$|$1$|$\{5\}$|
x a y
{} 0 {}
{} 1 {}
{z0} 0 {z0}
{z0} 1 {z0,z1}
{z0,z1} 0 {z0,z2}
{z0,z1} 1 {z0,z1,z2}
{z0,z2} 0 {z0,z3}
{z0,z2} 1 {z0,z1,z3}
{z0,z3} 0 {z0,z3}
{z0,z3} 1 {z0,z1,z3}
{z1} 0 {z2}
{z1} 1 {z2}
{z0,z1,z2} 0 {z0,z2,z3}
{z0,z1,z2} 1 {z0,z1,z2,z3}
{z0,z1,z3} 0 {z0,z2,z3}
{z0,z1,z3} 1 {z0,z1,z2,z3}
{z1,z2} 0 {z2,z3}
{z1,z2} 1 {z2,z3}
{z1,z3} 0 {z2,z3}
{z1,z3} 1 {z2,z3}
{z0,z1,z2,z3} 0 {z0,z2,z3}
{z0,z1,z2,z3} 1 {z0,z1,z2,z3}
{z2} 0 {z3}
{z2} 1 {z3}
{z0,z2,z3} 0 {z0,z3}
{z0,z2,z3} 1 {z0,z1,z3}
{z1,z2,z3} 0 {z2,z3}
{z1,z2,z3} 1 {z2,z3}
{z2,z3} 0 {z3}
{z2,z3} 1 {z3}
{z3} 0 {z3}
{z3} 1 {z3}
{0} 0 {0}
{0} 1 {0,1}
{0,1} 0 {0,2}
{0,1} 1 {0,1,2}
{0,2} 0 {0,3}
{0,2} 1 {0,1,3}
{0,3} 0 {0,4}
{0,3} 1 {0,1,4}
{0,4} 0 {0,5}
{0,4} 1 {0,1,5}
{0,5} 0 {0,5}
{0,5} 1 {0,1,5}
{1} 0 {2}
{1} 1 {2}
{0,1,2} 0 {0,2,3}
{0,1,2} 1 {0,1,2,3}
{0,1,3} 0 {0,2,4}
{0,1,3} 1 {0,1,2,4}
{0,1,4} 0 {0,2,5}
{0,1,4} 1 {0,1,2,5}
{0,1,5} 0 {0,2,5}
{0,1,5} 1 {0,1,2,5}
{1,2} 0 {2,3}
{1,2} 1 {2,3}
{1,3} 0 {2,4}
{1,3} 1 {2,4}
{1,4} 0 {2,5}
{1,4} 1 {2,5}
{1,5} 0 {2,5}
{1,5} 1 {2,5}
{0,1,2,3} 0 {0,2,3,4}
{0,1,2,3} 1 {0,1,2,3,4}
{0,1,2,4} 0 {0,2,3,5}
{0,1,2,4} 1 {0,1,2,3,5}
{0,1,2,5} 0 {0,2,3,5}
{0,1,2,5} 1 {0,1,2,3,5}
{0,1,3,4} 0 {0,2,4,5}
{0,1,3,4} 1 {0,1,2,4,5}
{0,1,3,5} 0 {0,2,4,5}
{0,1,3,5} 1 {0,1,2,4,5}
{0,1,4,5} 0 {0,2,5}
{0,1,4,5} 1 {0,1,2,5}
{2} 0 {3}
{2} 1 {3}
{0,2,3} 0 {0,3,4}
{0,2,3} 1 {0,1,3,4}
{0,2,4} 0 {0,3,5}
{0,2,4} 1 {0,1,3,5}
{0,2,5} 0 {0,3,5}
{0,2,5} 1 {0,1,3,5}
{0,1,2,3,4} 0 {0,2,3,4,5}
{0,1,2,3,4} 1 {0,1,2,3,4,5}
{0,1,2,3,5} 0 {0,2,3,4,5}
{0,1,2,3,5} 1 {0,1,2,3,4,5}
{0,1,2,3,4,5} 0 {0,2,3,4,5}
{0,1,2,3,4,5} 1 {0,1,2,3,4,5}
{0,1,2,4,5} 0 {0,2,3,5}
{0,1,2,4,5} 1 {0,1,2,3,5}
{1,2,3} 0 {2,3,4}
{1,2,3} 1 {2,3,4}
{1,2,4} 0 {2,3,5}
{1,2,4} 1 {2,3,5}
{1,2,5} 0 {2,3,5}
{1,2,5} 1 {2,3,5}
{2,3} 0 {3,4}
{2,3} 1 {3,4}
{2,4} 0 {3,5}
{2,4} 1 {3,5}
{2,5} 0 {3,5}
{2,5} 1 {3,5}
{0,2,3,4} 0 {0,3,4,5}
{0,2,3,4} 1 {0,1,3,4,5}
{0,2,3,5} 0 {0,3,4,5}
{0,2,3,5} 1 {0,1,3,4,5}
{0,2,4,5} 0 {0,3,5}
{0,2,4,5} 1 {0,1,3,5}
{1,2,3,4} 0 {2,3,4,5}
{1,2,3,4} 1 {2,3,4,5}
{1,2,3,5} 0 {2,3,4,5}
{1,2,3,5} 1 {2,3,4,5}
{1,2,4,5} 0 {2,3,5}
{1,2,4,5} 1 {2,3,5}
{3} 0 {4}
{3} 1 {4}
{0,3,4} 0 {0,4,5}
{0,3,4} 1 {0,1,4,5}
{0,3,5} 0 {0,4,5}
{0,3,5} 1 {0,1,4,5}
{0,1,3,4,5} 0 {0,2,4,5}
{0,1,3,4,5} 1 {0,1,2,4,5}
{0,2,3,4,5} 0 {0,3,4,5}
{0,2,3,4,5} 1 {0,1,3,4,5}
{1,3,4} 0 {2,4,5}
{1,3,4} 1 {2,4,5}
{1,3,5} 0 {2,4,5}
{1,3,5} 1 {2,4,5}
{1,2,3,4,5} 0 {2,3,4,5}
{1,2,3,4,5} 1 {2,3,4,5}
{2,3,4} 0 {3,4,5}
{2,3,4} 1 {3,4,5}
{2,3,5} 0 {3,4,5}
{2,3,5} 1 {3,4,5}
{3,4} 0 {4,5}
{3,4} 1 {4,5}
{3,5} 0 {4,5}
{3,5} 1 {4,5}
{0,3,4,5} 0 {0,4,5}
{0,3,4,5} 1 {0,1,4,5}
{1,3,4,5} 0 {2,4,5}
{1,3,4,5} 1 {2,4,5}
{2,3,4,5} 0 {3,4,5}
{2,3,4,5} 1 {3,4,5}
{4} 0 {5}
{4} 1 {5}
{0,4,5} 0 {0,5}
{0,4,5} 1 {0,1,5}
{1,4,5} 0 {2,5}
{1,4,5} 1 {2,5}
{2,4,5} 0 {3,5}
{2,4,5} 1 {3,5}
{3,4,5} 0 {4,5}
{3,4,5} 1 {4,5}
{4,5} 0 {5}
{4,5} 1 {5}
{5} 0 {5}
{5} 1 {5}
%% Cell type:markdown id: tags:
Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert.
%% Cell type:code id: tags:
``` prob
:pref DOT_DECOMPOSE_NODES=FALSE
```
%% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},
"1",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},
"start", {x,y|x=y & x={z0}},
"end", {x,y|x=y & x∩F ≠ ∅})
```
%% Output
<Dot visualization: expr_as_graph [("0",{x,y|x:POW(Z) & δs(x, [0])=y})]>
%% Cell type:markdown id: tags:
Mit den CUSTOM_GRAPH Fähigkeiten der B Maschine kann man diese Konstruktion schöner darstellen:
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
MACHINE NFA_nach_DFA
SETS
Z = {z0,z1,z2,z3}
ABSTRACT_CONSTANTS L, δs
CONSTANTS Σ, S, F, δ
PROPERTIES
F ⊆ Z ∧ S ⊆ Z ∧
δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Überführungsfunktion */
δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
IF s=[] THEN Z′
ELSE ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
/* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
/* Der Automat von Folie 21: */
Σ = {0,1} ∧
S = {z0} ∧ F = {z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z3}, (z2,1)↦{z3},
(z3,0)↦{z3}, (z3,1)↦{z3} }
DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
SET_PREF_DOT_LIMIT_PAGE_SIZE == FALSE; // requires brand-new probcli
SET_PREF_DOT_HORIZONTAL_LAYOUT == TRUE;
SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈ℙ(Z) & x/\F /= {}}); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈ℙ(Z) & x/\F = {}}); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈ℙ(Z) & y=δs(x,[0])});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈ℙ(Z) & y=δs(x,[1])});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
Loaded machine: NFA_nach_DFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
```
%% Output
Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
#### Beweis
Offenbar sind $M'$ und $M$ "aquivalent, denn für alle $x = a_1 a_2 \cdots a_n$
in $\Sigma^*$ gilt:
\begin{eqnarray*}
x \in L(M)
& \Longleftrightarrow & \widehat{\delta}(S,x) \cap E \neq \emptyset \\
& \Longleftrightarrow & \mbox{es gibt eine Folge von Teilmengen} \\
& & \mbox{$Z_1 , Z_2, \ldots , Z_n \subseteq Z$ mit $\delta'(S,a_1)=Z_1$,}\\
& & \mbox{$\delta'(Z_1,a_2)=Z_2$, $\ldots$,
$\delta'(Z_{n-1},a_{n})=Z_n$ und} \\
& & \mbox{$Z_n \cap E \neq \emptyset$} \\
& \Longleftrightarrow & Z_n = \widehat{\delta'}(z_0',x) \in F \\
& \Longleftrightarrow & x \in L(M') .
\end{eqnarray*}
Somit ist $L(M') = L(M)$.
%% Cell type:markdown id: tags:
### Weitere Beispiele
Wir modifizieren den NFA aus dem obigen Beispiel etwas und
betrachten den folgenden um einen Zustand kleineren NFA
$M=(\Sigma, Z, \delta , S, E)$:
Dieser NFA akzeptiert die Sprache aller W"orter "uber $\{0,1\}^*$, die
Dieser NFA akzeptiert die Sprache aller Wörter über $\{0,1\}^*$, die
an letzter Stelle eine $1$ haben.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z0,z1,z2}
ABSTRACT_CONSTANTS L, δs
CONSTANTS Σ, S, F, δ
PROPERTIES
F ⊆ Z ∧ S ⊆ Z ∧
δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Überführungsfunktion */
δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
IF s=[] THEN Z′
ELSE ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
/* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
/* Der Automat von Folie 28: */
Σ = {0,1} ∧
S = {z0} ∧ F = {z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z2}, (z2,1)↦{z2} }
DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
SET_PREF_DOT_LIMIT_PAGE_SIZE == FALSE; // requires brand-new probcli
SET_PREF_DOT_HORIZONTAL_LAYOUT == TRUE;
SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈ℙ(Z) & x/\F /= {}}); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈ℙ(Z) & x/\F = {}}); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈ℙ(Z) & y=δs(x,[0])});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈ℙ(Z) & y=δs(x,[1])});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{x,y|y∈δ(x,0)},"1",{x,y|y∈δ(x,1)})
```
%% Output
<Dot visualization: expr_as_graph [("0",{x,y|y:δ(x, 0)})]>
%% Cell type:markdown id: tags:
Wir konstruieren nun einen zu $M$ äquivalenten DFA $M' = (\Sigma,
Z', \delta' , S, F)$ gemäß dem Satz von Rabin und Scott:
%% Cell type:code id: tags:
``` prob
:pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
```
%% Output
Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Die Zustände $\emptyset$, $\{z_1\}$, $\{z_2\}$, $\{z_1,z_2\}$ können
vom Startzustand $\{z_0\}$ nicht erreicht werden und werden zur
Vereinfachung weggelassen.
%% Cell type:markdown id: tags:
Wir betrachten für $n \geq 1$ die Sprache
\begin{eqnarray*}
L_n & = & \{x\in\{0,1\}^* \mid
\text{ der $n$-te Buchstabe von hinten in }
x \text{ ist } 1 \} \\
& = & \{x \in \{0,1\}^* \mid x = u 1 v \text{ mit $u \in
\{0,1\}^*$ und $v \in \{0,1\}^{n-1}$}\}.
\end{eqnarray*}
Es gilt:
* Es gibt einen NFA f"ur $L_n$ mit $n+2$ Zust"anden.
(Beweis: Einfache Modifikation der NFAs für $L_2$ und $L_1$ in
den vorigen Abbildungen.)
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA_DFA_Explosion
ABSTRACT_CONSTANTS δs
CONSTANTS Σ, Z, S, F, δ, n
PROPERTIES
F ⊆ Z ∧ S ⊆ Z ∧
δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Überführungsfunktion */
δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
IF s=[] THEN Z′
ELSE ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
/* Für die Automaten ab Folie 31: */
Σ = {0,1} ∧
Z = 0..(n+1) ∧
S = {0} ∧
n ∈ 1..8 ∧
F = {n+1} ∧
δ = { (0,0)↦{0}, (0,1)↦{0,1},
(n+1,0)↦{(n+1)}, (n+1,1)↦{n+1} } \/
λ(z,i).(z∈1..n & i∈Σ | {z+1})
ASSERTIONS
δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(INTEGER)
VARIABLES Reachable
INVARIANT Reachable <: POW(Z)
INITIALISATION Reachable := POW(Z)
OPERATIONS Compute_Reachable = // Berechne erreichbaren Konfigurationen von S aus
BEGIN Reachable := closure({x,y| x:POW(Z) & (y=δs(x,[0]) or y= δs(x,[1]))}) [ {S} ] END
DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
SET_PREF_DOT_LIMIT_PAGE_SIZE == TRUE; // requires brand-new probcli
SET_PREF_DOT_HORIZONTAL_LAYOUT == TRUE;
SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈Reachable & x/\F /= {}}); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈Reachable & x/\F = {}}); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈Reachable & y=δs(x,[0])});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈Reachable & y=δs(x,[1])});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA_DFA_Explosion
%% Cell type:code id: tags:
``` prob
:goto -1
```
%% Output
Changed to state with index -1
%% Cell type:code id: tags:
``` prob
:constants n=4
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{x,y|y∈δ(x,0)},"1",{x,y|y∈δ(x,1)})
```
%% Output
<Dot visualization: expr_as_graph [("0",{x,y|y:δ(x, 0)})]>
%% Cell type:markdown id: tags:
Wir schauen uns nun den NFA mit allen möglichen Untermengen von Z an (bei grösseren Werten von n vorher ```:pref DOT_ENGINE=sfdp``` ausführen):
%% Cell type:code id: tags:
``` prob
:pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
```
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Wir können diesen Graphen auch auf die erreichbaren Zustände beschränken:
%% Cell type:code id: tags:
``` prob
:exec Compute_Reachable
```
%% Output
Executed operation: Compute_Reachable()
%% Cell type:code id: tags:
``` prob
Reachable
```
%% Output
$\{\{0\},\{0,1\},\{0,2\},\{0,3\},\{0,4\},\{0,5\},\{0,1,2\},\{0,1,3\},\{0,1,4\},\{0,1,5\},\{0,1,2,3\},\{0,1,2,4\},\{0,1,2,5\},\{0,1,3,4\},\{0,1,3,5\},\{0,1,4,5\},\{0,2,3\},\{0,2,4\},\{0,2,5\},\{0,1,2,3,4\},\{0,1,2,3,5\},\{0,1,2,3,4,5\},\{0,1,2,4,5\},\{0,2,3,4\},\{0,2,3,5\},\{0,2,4,5\},\{0,3,4\},\{0,3,5\},\{0,1,3,4,5\},\{0,2,3,4,5\},\{0,3,4,5\},\{0,4,5\}\}$
{{0},{0,1},{0,2},{0,3},{0,4},{0,5},{0,1,2},{0,1,3},{0,1,4},{0,1,5},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,1,3,4},{0,1,3,5},{0,1,4,5},{0,2,3},{0,2,4},{0,2,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,3,4,5},{0,1,2,4,5},{0,2,3,4},{0,2,3,5},{0,2,4,5},{0,3,4},{0,3,5},{0,1,3,4,5},{0,2,3,4,5},{0,3,4,5},{0,4,5}}
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment