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

add execution trace

parent 9bed047e
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-3/PDA_nach_kfG.ipynb
+ 347
− 14
View file @ 111f7a77
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# PDA nach kfG # PDA nach kfG
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE PDA_to_CFG MACHINE PDA_to_CFG
/* Translating a PDA to a CFG */ /* Translating a PDA to a CFG */
SETS SETS
STATES = {z0,z1, symbol}; STATES = {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*/ SYMBOLS={a,b, A, BOT, lambda, S} /* BOT = # = bottom of stack*/
DEFINITIONS DEFINITIONS
CFG_Alphabet == (STATES*(SYMBOLS-{lambda})*STATES); CFG_Alphabet == (STATES*(SYMBOLS-{lambda})*STATES);
Σ == {a,b}; Σ == {a,b};
Γ == {A,BOT}; Γ == {A,BOT};
ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))}; 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_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_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(STATES*SYMBOLS,STATES)(cur(c))};
ANIMATION_STR_JUSTIFY_LEFT == TRUE; ANIMATION_STR_JUSTIFY_LEFT == TRUE;
SET_PREF_PP_SEQUENCES == TRUE; SET_PREF_PP_SEQUENCES == TRUE;
PDA_STATES == (STATES-{symbol}); PDA_STATES == (STATES-{symbol});
SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END; SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;
SYM(s) == (symbol,s,symbol); SYM(s) == (symbol,s,symbol);
TERMINALS == {x|∃t.(t∈Σ ∧ x=SYM(t))} TERMINALS == {x|∃t.(t∈Σ ∧ x=SYM(t))}
CONSTANTS delta, Productions CONSTANTS delta, Productions
PROPERTIES PROPERTIES
/* A PDA accepting {a^mb^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */ /* A PDA accepting {a^mb^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */
delta = { (z0,a,BOT) ↦ (z0,[A,BOT]), delta = { (z0,a,BOT) ↦ (z0,[A,BOT]),
(z0,a,A) ↦ (z0,[A,A]), (z0,a,A) ↦ (z0,[A,A]),
(z0,b,A) ↦ (z1,[]), (z0,b,A) ↦ (z1,[]),
(z1,lambda,BOT) ↦ (z1,[]), (z1,lambda,BOT) ↦ (z1,[]),
(z1,b,A) ↦ (z1,[]) } ∧ (z1,b,A) ↦ (z1,[]) } ∧
Productions = /* Punkt 1 Folie 109 */ Productions = /* Punkt 1 Folie 109 */
{ lhs,rhs | ∃z.(z∈PDA_STATES ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])} { lhs,rhs | ∃z.(z∈PDA_STATES ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}
∪ ∪
/* Punkt 2 Folie 109 */ /* 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,[])∈delta ∧
lhs=(z,A,z2) ∧ rhs = SYMS(a)) } lhs=(z,A,z2) ∧ rhs = SYMS(a)) }
∪ ∪
/* Punkt 3 Folie 110 */ /* 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])∈delta ∧ z2∈PDA_STATES ∧
lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) } lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) }
∪ ∪
/* Punkt 4 Folie 110 */ /* Punkt 4 Folie 110 */
{ lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈delta ∧ { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈delta ∧
z2∈PDA_STATES ∧ z3∈PDA_STATES ∧ z2∈PDA_STATES ∧ z3∈PDA_STATES ∧
lhs=(z,A,z3) ∧ rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) } lhs=(z,A,z3) ∧ rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }
VARIABLES cur VARIABLES cur
INVARIANT INVARIANT
cur ∈ seq(CFG_Alphabet) cur ∈ seq(CFG_Alphabet)
INITIALISATION cur:=SYMS(S) INITIALISATION cur:=SYMS(S)
OPERATIONS OPERATIONS
ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Productions ∧ ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Productions ∧
cur = pre^[LHS]^post ∧ cur = pre^[LHS]^post ∧
ran(pre) ⊆ TERMINALS /* Links Ableitung */ ran(pre) ⊆ TERMINALS /* Links Ableitung */
THEN THEN
cur := pre^RHS^post cur := pre^RHS^post
END END
END END
``` ```
%% Output %% Output
Loaded machine: PDA_to_CFG Loaded machine: PDA_to_CFG
%% 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:code id: tags: %% Cell type:code id: tags:
``` prob ``` 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 :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:10px">symbol</td> <td style="padding:10px">symbol</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">S</td> <td style="padding:10px">S</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">symbol</td> <td style="padding:10px">symbol</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PDA_to_CFG Machine: PDA_to_CFG
Sets: STATES, SYMBOLS Sets: STATES, SYMBOLS
Constants: delta, Productions Constants: delta, Productions
Variables: cur Variables: cur
Operations: Operations:
ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[]) ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])
ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[]) ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` 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 :exec ApplyRule
``` ```
%% Output %% Output
Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[]) 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: %% 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