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

add computation of merged minimal automat

parent 635c1421
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
+ 222
− 2
View file @ 56164efc
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Algorithmus Minimalautomat ## Algorithmus Minimalautomat
Dieses Notebook begleitet die Vorlesung zur Myhill-Nerode Äquivalenzrelation und dem Minimalautomaten.
Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten. Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten.
%% 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,z4} Z = {z0,z1,z2,z3,z4}
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 = {z3,z4} ∧ F = {z3,z4} ∧
δ = { (z0,0)↦z1, (z0,1)↦z2, δ = { (z0,0)↦z1, (z0,1)↦z2,
(z1,0)↦z3, (z1,1)↦z3, (z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4, (z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3, (z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 } (z4,0)↦z4, (z4,1)↦z4 }
DEFINITIONS DEFINITIONS
SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE; SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE; SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
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 %% Output
Loaded machine: DFA Loaded machine: DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Der Automat sieht grafisch so aus: Der Automat sieht grafisch so aus:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% 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. 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: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE MinimalDFA MACHINE MinimalDFA
SETS SETS
Z = {z0,z1,z2,z3,z4} Z = {z0,z1,z2,z3,z4}
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Der Automat von den Folien: */ /* Der Automat von den Folien: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z3,z4} ∧ F = {z3,z4} ∧
δ = { (z0,0)↦z1, (z0,1)↦z2, δ = { (z0,0)↦z1, (z0,1)↦z2,
(z1,0)↦z3, (z1,1)↦z3, (z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4, (z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3, (z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 } (z4,0)↦z4, (z4,1)↦z4 }
VARIABLES VARIABLES
markiert, fusioniert markiert, fusioniert
INVARIANT markiert : Z <-> Z & INVARIANT markiert : Z <-> Z &
fusioniert : Z <-> Z fusioniert : Z <-> Z
INITIALISATION markiert := {za,zb| za∈F ⇔ zb∉F} || fusioniert := {} INITIALISATION markiert := {za,zb| za∈F ⇔ zb∉F} || fusioniert := {}
OPERATIONS OPERATIONS
Markiere(za,zb,a) = SELECT (za,zb) ∉ markiert ∧ Markiere(za,zb,a) = SELECT (za,zb) ∉ markiert ∧
a∈Σ ∧ a∈Σ ∧
(δ(za,a),δ(zb,a)) ∈ markiert THEN (δ(za,a),δ(zb,a)) ∈ markiert THEN
markiert := markiert \/ {(za,zb),(zb,za)} markiert := markiert \/ {(za,zb),(zb,za)}
END; END;
Fertig = SELECT fusioniert={} ∧ Fertig = SELECT fusioniert={} ∧
!(za,zb,a).((za,zb) ∉ markiert ∧ a∈Σ !(za,zb,a).((za,zb) ∉ markiert ∧ a∈Σ
=> =>
(δ(za,a),δ(zb,a)) ∉ markiert) THEN (δ(za,a),δ(zb,a)) ∉ markiert) THEN
fusioniert := {za,zb|(za,zb) ∉ markiert ∧ za ≠ zb} || fusioniert := {za,zb|(za,zb) ∉ markiert ∧ za ≠ zb} ||
markiert := {} markiert := {}
END END
DEFINITIONS DEFINITIONS
SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE; SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE; SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
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});
CUSTOM_GRAPH_EDGES4 == rec(color:"gray",label:"×",style:"dotted",edges:markiert); CUSTOM_GRAPH_EDGES4 == rec(color:"gray",label:"×",style:"dotted",edges:markiert);
CUSTOM_GRAPH_EDGES5 == rec(color:"purple",label:"↔",style:"bold",edges:fusioniert) CUSTOM_GRAPH_EDGES5 == rec(color:"purple",label:"↔",style:"bold",edges:fusioniert)
END END
``` ```
%% Output %% Output
Loaded machine: MinimalDFA Loaded machine: MinimalDFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Machine initialised using operation 1: $initialise_machine() Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Markiere alle Paare $\{z, z'\}$ mit Markiere alle Paare $\{z, z'\}$ mit
* $z \in F \Longleftrightarrow z' \not\in F$. * $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. 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: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=circo :pref DOT_ENGINE=circo
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = circo Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Sei $\{z, z'\}$ ein unmarkiertes Paar. Prüfe für jedes Sei $\{z, z'\}$ ein unmarkiertes Paar. Prüfe für jedes
$a \in \Sigma$, ob $\{\delta(z,a), \delta(z',a)\}$ bereits markiert $a \in \Sigma$, ob $\{\delta(z,a), \delta(z',a)\}$ bereits markiert
ist. Ist mindestens ein Test erfolgreich, so markiere auch ist. Ist mindestens ein Test erfolgreich, so markiere auch
$\{z,z'\}$. $\{z,z'\}$.
Dies ist hier der Fall: Dies ist hier der Fall:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Markiere :exec Markiere
``` ```
%% Output %% Output
Executed operation: Markiere(z1,z0,0) Executed operation: Markiere(z1,z0,0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Markiere :exec Markiere
``` ```
%% Output %% Output
Executed operation: Markiere(z2,z0,0) Executed operation: Markiere(z2,z0,0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es kann jetzt kein Markieren mehr ausgeführt werden, man kann nun Zustände fusionieren. Die Fusion selber ist hier nur grafisch angedeutet, nicht ausgeführt. Es kann jetzt kein Markieren mehr ausgeführt werden, man kann nun Zustände fusionieren. Die Fusion selber ist hier nur grafisch angedeutet, nicht ausgeführt.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Fertig :exec Fertig
``` ```
%% Output %% Output
Executed operation: Fertig() Executed operation: Fertig()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Anmerkung: wenn man oben zum Beispiel $F = \{z2\}$ setzt kommt ein anderes Ergebnis heraus. Anmerkung: wenn man oben zum Beispiel $F = \{z2\}$ setzt kommt ein anderes Ergebnis heraus.
%% Cell type:markdown id: tags:
Das sind die Zustände die fusioniert werden können:
%% Cell type:code id: tags:
``` prob
fusioniert
```
%% Output
$\{(\mathit{z1}\mapsto \mathit{z2}),(\mathit{z2}\mapsto \mathit{z1}),(\mathit{z3}\mapsto \mathit{z4}),(\mathit{z4}\mapsto \mathit{z3})\}$
{(z1↦z2),(z2↦z1),(z3↦z4),(z4↦z3)}
%% Cell type:markdown id: tags:
Wir berechnen jetzt die neue Menge ```ZF``` an fusionierten Zuständen (mit der reflexiven und transitiven Hülle ```closure``` von ```fusioniert```):
%% Cell type:code id: tags:
``` prob
:let ZF {zs| #x.(x:Z & closure(fusioniert)[{x}] = zs)}
```
%% Cell type:markdown id: tags:
Man kann jetzt die Übergangsfunktion für ZF so ausrechnen:
%% Cell type:code id: tags:
``` prob
:let δF %(zfa,a).(zfa:ZF & a:Σ | closure(fusioniert)[UNION(za).(za:zfa|{δ(za,a)})])
```
%% Output
$\{(\{\mathit{z0}\}\mapsto 0\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z0}\}\mapsto 1\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\})\}$
{({z0}↦0↦{z1,z2}),({z0}↦1↦{z1,z2}),({z1,z2}↦0↦{z3,z4}),({z1,z2}↦1↦{z3,z4}),({z3,z4}↦0↦{z3,z4}),({z3,z4}↦1↦{z3,z4})}
%% Cell type:code id: tags:
``` prob
:pref DOT_DECOMPOSE_NODES=FALSE DOT_ENGINE=dot
```
%% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE
Preference changed: DOT_ENGINE = dot
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{a,b|a:ZF & b=δF(a,0)}, "1",{a,b|a:ZF & b=δF(a,1)})
```
%% Output
<Dot visualization: expr_as_graph [δFZFδF={(({z0},0),{z1,z2}),(({z0},1),{z1,z2}),(({z1,z2},0),{z3,z4}),(({z1,z2},1),{z3,z4}),(({z3,z4},0),{z3,z4}),(({z3,z4},1),{z3,z4})} & ZF={{z0},{z1,z2},{z3,z4}}("0",{a,b|a:ZF & b=δF(a, 0)})]>
%% Cell type:code id: tags:
``` prob
:table δF
```
%% Output
|prj11|prj12|prj2|
|---|---|---|
|$\{\mathit{z0}\}$|$0$|$\{\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z0}\}$|$1$|$\{\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z3},\mathit{z4}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z3},\mathit{z4}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$|
prj11 prj12 prj2
{z0} 0 {z1,z2}
{z0} 1 {z1,z2}
{z1,z2} 0 {z3,z4}
{z1,z2} 1 {z3,z4}
{z3,z4} 0 {z3,z4}
{z3,z4} 1 {z3,z4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:version :version
``` ```
%% Output %% Output
ProB 2 Jupyter kernel: 1.1.1-SNAPSHOT (e52e0cac2096ac02eac65e556edce9dcd142d920) ProB 2 Jupyter kernel: 1.1.1-SNAPSHOT (e52e0cac2096ac02eac65e556edce9dcd142d920)
ProB 2: 3.10.0 (0ee5d5eea6894b2899690565dfc3d9042098ce89) ProB 2: 3.10.0 (0ee5d5eea6894b2899690565dfc3d9042098ce89)
ProB CLI: ProB CLI:
1.10.0-nightly (05b24c45455b15cf94ea1daf18d2189efafa22fa) 1.10.0-nightly (05b24c45455b15cf94ea1daf18d2189efafa22fa)
Last changed: Tue May 19 11:43:24 2020 +0200 Last changed: Tue May 19 11:43:24 2020 +0200
Prolog: SICStus 4.5.1 (x86_64-darwin-17.7.0): Tue Apr 2 15:34:32 CEST 2019 Prolog: SICStus 4.5.1 (x86_64-darwin-17.7.0): Tue Apr 2 15:34:32 CEST 2019
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment