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

small comments

parent c977cdf9
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# PDA (Push Down Automata - Kellerautomaten)
%% Cell type:markdown id: tags:
Ein __(nichtdeterministischer) Kellerautomat__
(kurz PDA für __push-down automaton__) ist ein $6$-Tupel
$M = (\Sigma, \Gamma, Z, \delta , z_0, \#)$, wobei
* $\Sigma$ das Eingabe-Alphabet ist,
* $\Gamma$ das Kelleralphabet,
* $Z$ eine endliche Menge von Zuständen,
* $\delta : Z \times (\Sigma \cup \{\lambda\}) \times \Gamma
\rightarrow \mathfrak{P}_e(Z \times \Gamma^{\ast})$ die
Überführungsfunktion,
* $z_0 \in Z$ der Startzustand,
* $\# \in \Gamma$ das Bottom-Symbol im Keller.
Anmerkung: $\mathfrak{P}_e(Z \times \Gamma^{\ast})$ ist die Menge aller
__endlichen__ Teilmengen von $Z \times \Gamma^{\ast}$.
%% Cell type:code id: tags:
``` prob
::load
MACHINE PDA
/* B Modell eines PDA */
SETS
Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand
SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/
DEFINITIONS
Σ == {a,b}; // das Eingabe-Alphabet
Γ == {A,BOT}; // das Kelleralphabet
ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
ANIMATION_FUNCTION == {2}*α \/ {3}*(γ);
ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
SET_PREF_PRETTY_PRINT_SEQUENCES == TRUE
CONSTANTS δ
PROPERTIES
/* A PDA für {a^mb^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
/* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
δ = { (z0,a,BOT) ↦ (z0,[A,BOT]),
(z0,a,A) ↦ (z0,[A,A]),
(z0,b,A) ↦ (z1,[]),
(z1,lambda,BOT) ↦ (z1,[]),
(z1,b,A) ↦ (z1,[]) }
// Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert
// Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript
VARIABLES
z, α, γ // Konfiguration in dem sich der PDA befindet
INVARIANT
z ∈ Z ∧ // der aktuelle Zustand
α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
γ ∈ seq(Γ) // aktuelle Kellerinhalt
INITIALISATION
z := z0 ||
γ := [BOT] || // Initialisierung des Stapels
α := [a,a,b,b] // das Eingabewort
OPERATIONS
// die Operationen Schritt und LambdaSchritt modellieren
// Schritte in der Ableitungsrelation
Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
z := z‘ || // in den neuen Zustand wechseln
α := tail(α) || // das erste Symbol auf der Eingabe löschen
γ := s^tail(γ) // s auf den Stapel packen
END;
LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
z := z‘ || // in den neuen Zustand wechseln
γ := s^tail(γ) // s auf den Stapel packen
END;
Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN
/* Wir akzeptieren wenn Eingabe und Stapel leer sind */
skip END
END
```
%% Output
Loaded machine: PDA
%% 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:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z0</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">a</td>
<td style="padding:10px">a</td>
<td style="padding:10px">b</td>
<td style="padding:10px">b</td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">BOT</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
Schritt(z0,{(1|->A),(2|->BOT)})
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z0,{(1|->A),(2|->BOT)})
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z0</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">a</td>
<td style="padding:10px">b</td>
<td style="padding:10px">b</td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
(z,α,γ)
```
%% Output
$(\mathit{z0}\mapsto\{(1\mapsto \mathit{a}),(2\mapsto \mathit{b}),(3\mapsto \mathit{b})\}\mapsto\{(1\mapsto \mathit{A}),(2\mapsto \mathit{BOT})\})$
(z0↦{(1↦a),(2↦b),(3↦b)}↦{(1↦A),(2↦BOT)})
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
Schritt(z0,{(1|->A),(2|->A)})
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z0,{(1|->A),(2|->A)})
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z0</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">b</td>
<td style="padding:10px">b</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
Schritt(z1,{})
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z1,{})
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z1</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">b</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
Schritt(z1,{})
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z1,{})
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z1</td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
LambdaSchritt(z1,{})
%% Cell type:code id: tags:
``` prob
:exec LambdaSchritt
```
%% Output
Executed operation: LambdaSchritt(z1,{})
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z1</td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA
Sets: Z, SYMBOLE
Constants: δ
Variables: z, α, γ
Operations:
Akzeptieren()
%% Cell type:code id: tags:
``` prob
:exec Akzeptieren
```
%% Output
Executed operation: Akzeptieren()
%% Cell type:markdown id: tags:
Das Eingabewort ``aabb`` wurde akzeptiert.
%% 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