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

Anpassung der Namen

parent 111f7a77
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# PDA nach kfG
%% Cell type:code id: tags:
``` prob
::load
MACHINE PDA_to_CFG
/* Translating a PDA to a CFG */
SETS
STATES = {z0,z1, symbol};
Z = {z0,z1, symbol};
/* symbol: virtueller Zustand um S und andere Symbole in der Grammatik darzustellen */
SYMBOLS={a,b, A, BOT, lambda, S} /* BOT = # = bottom of stack*/
SYMBOLE={a,b, A, BOT, lambda, S} /* BOT = # = Ende vom Keller */
DEFINITIONS
CFG_Alphabet == (STATES*(SYMBOLS-{lambda})*STATES);
kfG_Alphabet == (Z*(SYMBOLE \ {lambda})*Z);
Σ == {a,b};
Γ == {A,BOT};
ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};
ANIMATION_FUNCTION2 == {r,c,i| r=2 ∧ c∈dom(cur) ∧ i=prj2(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};
ANIMATION_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(STATES*SYMBOLS,STATES)(cur(c))};
ANIMATION_STR_JUSTIFY_LEFT == TRUE;
SET_PREF_PP_SEQUENCES == TRUE;
PDA_STATES == (STATES-{symbol});
PDA_Zustände == (Z-{symbol});
SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;
SYM(s) == (symbol,s,symbol);
TERMINALS == {x|∃t.(t∈Σ ∧ x=SYM(t))}
CONSTANTS delta, Productions
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))};
ANIMATION_STR_JUSTIFY_LEFT == TRUE;
SET_PREF_PP_SEQUENCES == TRUE
CONSTANTS δ, Regeln
PROPERTIES
/* A PDA accepting {a^mb^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */
delta = { (z0,a,BOT) ↦ (z0,[A,BOT]),
/* 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,[]) } ∧
Productions = /* Punkt 1 Folie 109 */
{ lhs,rhs | ∃z.(z∈PDA_STATES ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}
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,[])∈delta
{ 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])∈delta ∧ z2∈PDA_STATES
{ 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])∈delta ∧
z2∈PDA_STATES ∧ z3∈PDA_STATES ∧
lhs=(z,A,z3) ∧ rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }
{ 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)]) }
VARIABLES cur
INVARIANT
cur ∈ seq(CFG_Alphabet)
INITIALISATION cur:=SYMS(S)
cur ∈ seq(kfG_Alphabet)
INITIALISATION
cur:=SYMS(S)
OPERATIONS
ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Productions ∧
// Anwendung einer Grammatikregel
ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Regeln ∧
cur = pre^[LHS]^post ∧
ran(pre) ⊆ TERMINALS /* Links Ableitung */
ran(pre) ⊆ kfG_TERMINALE /* Links Ableitung */
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
delta
δ
```
%% 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: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
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>
</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>
</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>
</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
Variables: cur
Operations:
%% 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