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

comment out preferences not yet available in 1.2.0 kernel

parent 2aaa2e38
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
+ 4
− 4
View file @ 8f3ffe52
%% Cell type:markdown id: tags:
## 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.
%% 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 = {z3,z4} ∧
δ = { (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;
//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}
CONSTANTS Σ, F, δ
PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Der Automat von den Folien: */
Σ = {0,1} ∧
F = {z3,z4} ∧
δ = { (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 fusioniert={} ∧
!(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;
//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,0)
%% 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(z2,z0,0)
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% 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.
%% 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:markdown id: tags:
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:
``` prob
:version
```
%% Output
ProB 2 Jupyter kernel: 1.1.1-SNAPSHOT (e52e0cac2096ac02eac65e556edce9dcd142d920)
ProB 2: 3.10.0 (0ee5d5eea6894b2899690565dfc3d9042098ce89)
ProB CLI:
1.10.0-nightly (05b24c45455b15cf94ea1daf18d2189efafa22fa)
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
%% 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