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

add new example (Minimalautomat)

parent 7d324e49
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-2/Minimalautomat.ipynb 0 → 100644
+ 1436
− 0
View file @ f9cb0a49
%% Cell type:markdown id: tags:
## Algorithmus Minimalautomat
Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten.
%% Cell type:code id: tags:
``` prob
::load
MACHINE DFA
SETS
Z = {z0,z1,z2,z3,z4}
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)↦z2,
(z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 }
DEFINITIONS
SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
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:
Der Automat sieht grafisch so aus:
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
In der folgenden B Maschine sind (bis auf die Entfernung der nicht erreichbaren Zustände) die Schritte des Algorithmus umgesetzt worden.
%% Cell type:code id: tags:
``` prob
::load
MACHINE MinimalDFA
SETS
Z = {z0,z1,z2,z3,z4}
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)↦z2,
(z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 }
VARIABLES
markiert, fusioniert
INVARIANT markiert : Z <-> Z &
fusioniert : Z <-> Z
INITIALISATION markiert := {za,zb| za∈F ⇔ zb∉F} || fusioniert := {}
OPERATIONS
Markiere(za,zb,a) = SELECT (za,zb) ∉ markiert ∧
a∈Σ ∧
(δ(za,a),δ(zb,a)) ∈ markiert THEN
markiert := markiert \/ {(za,zb),(zb,za)}
END;
Fertig = SELECT !(za,zb,a).((za,zb) ∉ markiert ∧ a∈Σ
=>
(δ(za,a),δ(zb,a)) ∉ markiert) THEN
fusioniert := {za,zb|(za,zb) ∉ markiert ∧ za ≠ zb} ||
markiert := {}
END
DEFINITIONS
SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
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});
CUSTOM_GRAPH_EDGES4 == rec(color:"gray",label:"×",style:"dotted",edges:markiert);
CUSTOM_GRAPH_EDGES5 == rec(color:"purple",label:"↔",style:"bold",edges:fusioniert)
END
```
%% Output
Loaded machine: MinimalDFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% 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:markdown id: tags:
Markiere alle Paare $\{z, z'\}$ mit
* $z \in F \Longleftrightarrow z' \not\in F$.
Dies wird in der B Maschine in der INITIALISATION Klausel gemacht. Im Graphen unten sind die markierten Paare mit $\times$ gekennzeichnet.
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=circo
```
%% Output
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Sei $\{z, z'\}$ ein unmarkiertes Paar. Prüfe für jedes
$a \in \Sigma$, ob $\{\delta(z,a), \delta(z',a)\}$ bereits markiert
ist. Ist mindestens ein Test erfolgreich, so markiere auch
$\{z,z'\}$.
Dies ist hier der Fall:
%% Cell type:code id: tags:
``` prob
:exec Markiere
```
%% Output
Executed operation: Markiere(z1,z0,1)
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
:exec Markiere
```
%% Output
Executed operation: Markiere(z3,z0,1)
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
:exec Markiere
```
%% Output
Executed operation: Markiere(z4,z0,1)
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
:exec Fertig
```
%% Output
Executed operation: Fertig()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment