Commit f7b1832c authored by Christopher Happe's avatar Christopher Happe
Browse files

Erste Version Notebook Vergleich der Automaten

parent 78a26a5c
%% Cell type:markdown id: tags:
# DFAs, PDAs und TM
Im folgenden werden wir uns damit befassen wie die verschiedenen Automatenmodelle in Verbinndung stehen und wie man sie ineinander übersetzt.
Wie bereits aus der Vorlesung bekannt ist, akzeptieren DFAs reguläre, PDAs kontextfreie und Turingmaschienen $\mathbb{L}_0$ Sprachen. Da die $REG\subseteq CF \subseteq \mathbb{L}_0$ kann jeder DFA durch einen PDA und jeder PDA durch eine TM dargestellt werden. Folgende Maschiene demonstriert eine Möglichkeit dies zu tun:
%% Cell type:code id: tags:
``` prob
MACHINE DFA_PDA_TM
/* B Modell einer 1-band Turing Maschine */
/* by Michael Leuschel, 2012 */
/* Akzeptiert die Sprache a^n b^n c^n (siehe Folien 14ff von folien-kapitel-5 */
SETS
Alphabet={a,b,c,X,Blank, Bottom, lambda};
States = {z0,z1,z2,z3,z4,z5,z6,z_end};
Direction = {L,R,N}
DEFINITIONS
Σ == {a, b};
CurSymbol == (Right<-Blank)(1);
ANIMATION_FUNCTION_DEFAULT == {(1,0,cur)};
/* ANIMATION_FUNCTION__xx == {(1,1,Left), (1,3,Right)}; */
ANIMATION_FUNCTION1 == {1} *( (λi.(i∈-size(Left)..-1|i+size(Left)+1) ; Left) ∪ Right)
CONSTANTS Final, δ,
DFA, Z_DFA, δ_DFA, z_start, F_DFA,
PDA, Γ_PDA, Z_PDA, δ_PDA,
TM, Γ_TM, Z_TM, δ_TM, F_TM
PROPERTIES
//Allgemeine Regeln
Σ ⊆ Alphabet ∧
z_end ∉ Z_DFA ∪ Z_PDA ∧
lambda ∉ Σ ∪ Γ_PDA ∪ Γ_TM ∧
//Definition des DFAs
DFA = (Σ, Z_DFA, δ_DFA, z_start, F_DFA) ∧
Z_DFA ⊆ States ∧
δ_DFA ∈ (Z_DFA×Σ)→Z_DFA ∧
z_start ∈ Z_DFA ∧
F_DFA ⊆ Z_DFA ∧
//Definition eines PDAs zum DFA
PDA = (Σ, Γ_PDA, Z_PDA, δ_PDA, z_start, Bottom) ∧
Γ_PDA ⊆ Alphabet ∧
Z_PDA ⊆ States ∧
δ_PDA ∈ (Z_PDA×(Σ∪{lambda})×Γ_PDA)⇸(Z_PDA×seq(Γ_PDA)) ∧
z_start ∈ Z_PDA ∧
Bottom ∈ Γ_PDA ∧
Γ_PDA = Σ∪{Bottom} ∧
Z_PDA = Z_DFA ∧
δ_PDA = {regel|∃zustand1,zustand2,terminal.((zustand1,terminal)↦zustand2 ∈ δ_DFA ∧
(regel = (zustand1, terminal, Bottom) ↦ (zustand2, [Bottom])))}
{regel | ∃zustand.(zustand ∈ F_DFA ∧
regel = (zustand, lambda, Bottom) ↦ (zustand, []))} ∧
TM = (Σ, Γ_TM, Z_TM, δ_TM, z_start, Blank, F_TM) ∧
Γ_TM ⊆ Alphabet ∧
Z_TM ⊆ States ∧
δ_TM ∈ (Z_TM×Γ_TM)→(Z_TM×Γ_TM×Direction) ∧
z_start ∈ Z_TM ∧
Blank ∈ Γ_TM ∧
F_TM ⊆ Z_TM ∧
Γ_TM = Σ ∪ {Blank} ∧
Z_TM = Z_DFA ∪ {z_end} ∧
δ_TM = {regel|∃zustand1,zustand2,terminal.((zustand1,terminal)↦zustand2 ∈ δ_DFA ∧
(regel = (zustand1, terminal) ↦ (zustand2, Blank, R)))}
{regel | ∃zustand.(zustand ∈ Z_DFA\F_DFA ∧
regel = (zustand, Blank) ↦ (zustand, Blank, N))}
{regel | ∃zustand.(zustand ∈ F_DFA ∧
regel = (zustand, Blank) ↦ (z_end, Blank, N))}
{regel | ∃terminal.(terminal ∈ Γ_TM ∧ regel = (z_end, terminal) ↦ (z_end, terminal, N))} ∧
F_TM = {z_end} ∧
Final ⊆ States ∧
δ ∈ (States * Alphabet) ↔ (States * Alphabet * Direction) ∧
δ = { /* Neuer Zyklus */
(z0,a) ↦ (z1,X,R),
(z0,X) ↦ (z0,X,R),
/* ein a getilgt (X), nächstes b suchen */
(z1,a) ↦ (z1,a,R),
(z1,b) ↦ (z2,X,R),
(z1,X) ↦ (z1,X,R),
/* ein a,b getilgt (X), nächstes c suchen */
(z2,b) ↦ (z2,b,R),
(z2,c) ↦ (z3,X,R),
(z2,X) ↦ (z2,X,R),
/* ein a,b,c getilgt (X), rechten Rand suchen */
(z3,c) ↦ (z3,c,R),
(z3,Blank) ↦ (z4,Blank,L),
/* Zurücklaufen und testen ob alle a,b,c getilgt */
(z4,X) ↦ (z4,X,L),
(z4,Blank) ↦ (z6,Blank,R), /* Erfolg ∀ */
(z4,c) ↦ (z5,c,L),
/* Test nicht erfolgreich; zum linken Rand zurücklaufen und neuer Zyklus */
(z5,X) ↦ (z5,X,L),
(z5,Blank) ↦ (z0,Blank,R),
(z5,a) ↦ (z5,a,L),
(z5,b) ↦ (z5,b,L),
(z5,c) ↦ (z5,c,L)
} ∧
Final = {z6}
VARIABLES Left,cur,Right
INVARIANT
cur ∈ States ∧
Left ∈ seq(Alphabet) ∧ Right ∈ seq(Alphabet)
INITIALISATION Left,cur,Right := [],z0,[a,a,b,b,c,c]
OPERATIONS
Accept = PRE cur ∈ Final THEN skip END;
GoTo(z,S,znew,NewSymbol,Dir) =
PRE z=cur ∧ S=CurSymbol ∧
(z, S) ↦ (znew,NewSymbol,Dir) ∈ δ THEN
ANY tail_Right
WHERE (Right=[] ⇒ tail_Right=[]) ∧ (Right≠[] ⇒ tail_Right = tail(Right)) THEN
cur := znew ||
IF Dir = N THEN
Right := NewSymbol -> tail_Right
ELSIF Dir = R THEN
Left,Right := Left <- NewSymbol, tail_Right
ELSIF Left=[] THEN
Left,Right := [], Blank -> (NewSymbol -> tail_Right)
ELSE
Left,Right := front(Left), last(Left) -> (NewSymbol -> tail_Right)
END
END
END
END
```
%% Output
Loaded machine: DFA_PDA_TM
%% Cell type:code id: tags:
``` prob
:constants DFA=({a, b}, //Σ
{z0,z1,z2,z3}, //Z
{(z0,a)↦z1, (z0,b)↦z3,
(z1,a)↦z3, (z1,b)↦z2,
(z2,a)↦z2, (z2,b)↦z2,
(z3,a)↦z3, (z3,b)↦z3 }, //δ
z0, {z0, z2}) //z0, F
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:help dot
```
%% Output
```
:dot COMMAND [FORMULA]
```
Execute and show a dot visualisation.
The following dot visualisation commands are available:
* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
* `operations` - Operation Call Graph: Shows the call graph of a classical B model
* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `current_state` - Current State in State Space: Show current state and successors in state space
* `history` - Path to Current State: Show a path leading to current state
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
* `enable_graph` - Enable Graph: Show enabling graph of events
* `state_as_graph` - Current State as Graph: Show values in current state as a graph
* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES
* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
* `invariant` - Invariant Formula Tree: Show invariant as a formula tree
* `properties` - Properties Formula Tree: Show properties as a formula tree
* `assertions` - Assertions Formula Tree: Show assertions as a formula tree
* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
* `last_error` - Last Error Formula Tree: Show last error source as a formula tree
:dot COMMAND [FORMULA]
Execute and show a dot visualisation.
The following dot visualisation commands are available:
* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
* `operations` - Operation Call Graph: Shows the call graph of a classical B model
* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `current_state` - Current State in State Space: Show current state and successors in state space
* `history` - Path to Current State: Show a path leading to current state
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
* `enable_graph` - Enable Graph: Show enabling graph of events
* `state_as_graph` - Current State as Graph: Show values in current state as a graph
* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES
* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
* `invariant` - Invariant Formula Tree: Show invariant as a formula tree
* `properties` - Properties Formula Tree: Show properties as a formula tree
* `assertions` - Assertions Formula Tree: Show assertions as a formula tree
* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
* `last_error` - Last Error Formula Tree: Show last error source as a formula tree
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment