Skip to content
Snippets Groups Projects
Commit 6fbbb250 authored by Chris's avatar Chris
Browse files

Visualisierung PDA nach kfG angepasst

parent 6032f916
No related branches found
No related tags found
1 merge request!1Master
%% Cell type:markdown id: tags:
# PDA nach kfG
Aus einem gegebenen PDA kann man auch eine kontextfreie Grammatik generieren, die die gleiche Sprache akzeptiert.
%% Cell type:code id: tags:
``` prob
::load
MACHINE PDA_to_CFG
/* Translating a PDA to a CFG */
SETS
Z = {z0,z1, symbol};
/* symbol: virtueller Zustand um S und andere Symbole in der Grammatik darzustellen */
SYMBOLE={a,b, A, BOT, lambda, S} /* BOT = # = Ende vom Keller */
DEFINITIONS
kfG_Alphabet == (Z*(SYMBOLE \ {lambda})*Z);
Σ == {a,b};
Γ == {A,BOT};
PDA_Zustände == (Z-{symbol});
SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;
SYM(s) == (symbol,s,symbol); // Darstellung eines Symbols als Tripel für die Grammatik
kfG_TERMINALE == {x|∃t.(t∈Σ ∧ x=SYM(t))};
ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(Z,SYMBOLE)(prj1(Z*SYMBOLE,Z)(cur(c)))};
ANIMATION_FUNCTION2 == {r,c,i| r=2 ∧ c∈dom(cur) ∧ i=prj2(Z,SYMBOLE)(prj1(Z*SYMBOLE,Z)(cur(c)))};
ANIMATION_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(Z*SYMBOLE,Z)(cur(c))};
"LibraryStrings.def";
ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧
i= IF ∃t.(t∈SYMBOLE ∧ cur(c) = (symbol |->t|-> symbol))
THEN LET s BE s=TO_STRING({x | (symbol|->x|->symbol)=cur(c)})
IN SUB_STRING(s,2,STRING_LENGTH(s)-2) END
ELSE TO_STRING(cur(c)) END};
ANIMATION_STR_JUSTIFY_LEFT == TRUE;
SET_PREF_PP_SEQUENCES == TRUE
CONSTANTS δ, Regeln
CONSTANTS δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
PROPERTIES
/* Ein 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,[]) } ∧
Regeln = /* Punkt 1 Folie 109 */
{ lhs,rhs | ∃z.(z∈PDA_Zustände ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}
/* Punkt 2 Folie 109 */
{ lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈δ ∧
lhs=(z,A,z2) ∧ rhs = SYMS(a)) }
/* Punkt 3 Folie 110 */
{ lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈δ ∧ z2∈PDA_Zustände ∧
lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) }
/* Punkt 4 Folie 110 */
{ lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈δ ∧
z2∈PDA_Zustände ∧
z3∈PDA_Zustände ∧
/*Die Regeln der kfG zum PDA*/
/* Punkt 1 Folie 109 */
RegelnP1 = { lhs,rhs | ∃z.(z∈PDA_Zustände ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])} ∧
/* Punkt 2 Folie 109 */
RegelnP2 = { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈δ ∧ lhs=(z,A,z2) ∧ rhs = SYMS(a)) } ∧
/* Punkt 3 Folie 110 */
RegelnP3 = { lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈δ ∧ z2∈PDA_Zustände ∧
lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) } ∧
/* Punkt 4 Folie 110 */
RegelnP4 = { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈δ ∧
z2∈PDA_Zustände ∧ z3∈PDA_Zustände ∧
lhs=(z,A,z3) ∧
rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }
rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) } ∧
Regeln = RegelnP1 ∪ RegelnP2 ∪ RegelnP3 ∪ RegelnP4
VARIABLES cur
INVARIANT
cur ∈ seq(kfG_Alphabet)
INITIALISATION
cur:=SYMS(S)
OPERATIONS
// Anwendung einer Grammatikregel
ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Regeln ∧
cur = pre^[LHS]^post ∧
ran(pre) ⊆ kfG_TERMINALE /* Links Ableitung */
ran(pre) ⊆ kfG_TERMINALE /* Linksableitung */
THEN
cur := pre^RHS^post
END
END
```
%% Output
Loaded machine: PDA_to_CFG
%% 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
δ
```
%% Output
$\{(\mathit{z0}\mapsto \mathit{a}\mapsto \mathit{A}\mapsto(\mathit{z0}\mapsto [A,A])),(\mathit{z0}\mapsto \mathit{a}\mapsto \mathit{BOT}\mapsto(\mathit{z0}\mapsto [A,BOT])),(\mathit{z0}\mapsto \mathit{b}\mapsto \mathit{A}\mapsto(\mathit{z1}\mapsto [])),(\mathit{z1}\mapsto \mathit{b}\mapsto \mathit{A}\mapsto(\mathit{z1}\mapsto [])),(\mathit{z1}\mapsto \mathit{lambda}\mapsto \mathit{BOT}\mapsto(\mathit{z1}\mapsto []))\}$
{(z0↦a↦A↦(z0↦[A,A])),(z0↦a↦BOT↦(z0↦[A,BOT])),(z0↦b↦A↦(z1↦[])),(z1↦b↦A↦(z1↦[])),(z1↦lambda↦BOT↦(z1↦[]))}
%% Cell type:markdown id: tags:
Die Grammatik startet mit dem Startsymbol und simuliert die Ausführung eines entsprechenden PDAs. Dabei gibt es teils mehrere Wege, aber das Wort ab wird von mindestens einem erreicht.
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">symbol</td>
</tr>
<tr>
<td style="padding:10px">S</td>
</tr>
<tr>
<td style="padding:10px">symbol</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA_to_CFG
Sets: STATES, SYMBOLS
Constants: delta, Productions
Sets: Z, SYMBOLE
Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
Variables: cur
Operations:
ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])
ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])
%% Cell type:code id: tags:
``` prob
:exec ApplyRule RHS = [(z0|->BOT|->z1)]
```
%% Output
Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z0</td>
</tr>
<tr>
<td style="padding:10px">BOT</td>
</tr>
<tr>
<td style="padding:10px">z1</td>
<td style="padding:10px">(z0|->BOT|->z1)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA_to_CFG
Sets: STATES, SYMBOLS
Constants: delta, Productions
Variables: cur
Operations:
ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z0),(z0|->BOT|->z1)],[],[])
ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)],[],[])
%% Cell type:code id: tags:
``` prob
:exec ApplyRule RHS = [(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)]
```
%% Output
Executed operation: ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)],[],[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">z1</td>
</tr>
<tr>
<td style="padding:10px">a</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
</tr>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">(z0|->A|->z1)</td>
<td style="padding:10px">(z1|->BOT|->z1)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA_to_CFG
Sets: STATES, SYMBOLS
Constants: delta, Productions
Variables: cur
Operations:
ApplyRule((z0|->A|->z1),[(symbol|->b|->symbol)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])
ApplyRule((z0|->A|->z1),[(symbol|->a|->symbol),(z0|->A|->z0),(z0|->A|->z1)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])
ApplyRule((z0|->A|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->A|->z1)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])
%% Cell type:code id: tags:
``` prob
:exec ApplyRule RHS=[(symbol|->b|->symbol)]
```
%% Output
Executed operation: ApplyRule((z0|->A|->z1),[(symbol|->b|->symbol)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">symbol</td>
<td style="padding:10px">z1</td>
</tr>
<tr>
<td style="padding:10px">a</td>
<td style="padding:10px">b</td>
<td style="padding:10px">BOT</td>
</tr>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">symbol</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">(z1|->BOT|->z1)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA_to_CFG
Sets: STATES, SYMBOLS
Constants: delta, Productions
Variables: cur
Operations:
ApplyRule((z1|->BOT|->z1),[],[(symbol|->a|->symbol),(symbol|->b|->symbol)],[])
%% Cell type:code id: tags:
``` prob
:exec ApplyRule
```
%% Output
Executed operation: ApplyRule((z1|->BOT|->z1),[],[(symbol|->a|->symbol),(symbol|->b|->symbol)],[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">symbol</td>
</tr>
<tr>
<td style="padding:10px">a</td>
<td style="padding:10px">b</td>
</tr>
<tr>
<td style="padding:10px">symbol</td>
<td style="padding:10px">symbol</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: PDA_to_CFG
Sets: STATES, SYMBOLS
Constants: delta, Productions
Sets: Z, SYMBOLE
Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
Variables: cur
Operations:
%% Cell type:markdown id: tags:
Da das Wort fertig abgeleitet wurde ist keine Regel mehr ausführbar.
%% 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