diff --git a/info4/kapitel-5/DFA_PDA_TM.ipynb b/info4/kapitel-5/DFA_PDA_TM.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..9bf4c1d26dbfaad272cb0feaf117469c74f851ae
--- /dev/null
+++ b/info4/kapitel-5/DFA_PDA_TM.ipynb
@@ -0,0 +1,286 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# DFAs, PDAs und TM\n",
+ "Im folgenden werden wir uns damit befassen wie die verschiedenen Automatenmodelle in Verbinndung stehen und wie man sie ineinander übersetzt.\n",
+ "\n",
+ "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",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: DFA_PDA_TM"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE DFA_PDA_TM\n",
+ "/* B Modell einer 1-band Turing Maschine */\n",
+ "/* by Michael Leuschel, 2012 */\n",
+ "/* Akzeptiert die Sprache a^n b^n c^n (siehe Folien 14ff von folien-kapitel-5 */\n",
+ "SETS\n",
+ " Alphabet={a,b,c,X,Blank, Bottom, lambda};\n",
+ " States = {z0,z1,z2,z3,z4,z5,z6,z_end};\n",
+ " Direction = {L,R,N}\n",
+ "DEFINITIONS\n",
+ " Σ == {a, b};\n",
+ " CurSymbol == (Right<-Blank)(1);\n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,0,cur)};\n",
+ " /* ANIMATION_FUNCTION__xx == {(1,1,Left), (1,3,Right)}; */\n",
+ " ANIMATION_FUNCTION1 == {1} *( (λi.(i∈-size(Left)..-1|i+size(Left)+1) ; Left) ∪ Right)\n",
+ "CONSTANTS Final, δ,\n",
+ " DFA, Z_DFA, δ_DFA, z_start, F_DFA,\n",
+ " PDA, Γ_PDA, Z_PDA, δ_PDA,\n",
+ " TM, Γ_TM, Z_TM, δ_TM, F_TM\n",
+ "PROPERTIES\n",
+ " //Allgemeine Regeln\n",
+ " Σ ⊆ Alphabet ∧\n",
+ " z_end ∉ Z_DFA ∪ Z_PDA ∧\n",
+ " lambda ∉ Σ ∪ Γ_PDA ∪ Γ_TM ∧\n",
+ " \n",
+ " //Definition des DFAs\n",
+ " DFA = (Σ, Z_DFA, δ_DFA, z_start, F_DFA) ∧\n",
+ " Z_DFA ⊆ States ∧\n",
+ " δ_DFA ∈ (Z_DFA×Σ)→Z_DFA ∧\n",
+ " z_start ∈ Z_DFA ∧\n",
+ " F_DFA ⊆ Z_DFA ∧\n",
+ "\n",
+ " //Definition eines PDAs zum DFA\n",
+ " PDA = (Σ, Γ_PDA, Z_PDA, δ_PDA, z_start, Bottom) ∧\n",
+ " Γ_PDA ⊆ Alphabet ∧\n",
+ " Z_PDA ⊆ States ∧\n",
+ " δ_PDA ∈ (Z_PDA×(Σ∪{lambda})×Γ_PDA)⇸(Z_PDA×seq(Γ_PDA)) ∧\n",
+ " z_start ∈ Z_PDA ∧ \n",
+ " Bottom ∈ Γ_PDA ∧\n",
+ " \n",
+ " Γ_PDA = Σ∪{Bottom} ∧\n",
+ " Z_PDA = Z_DFA ∧\n",
+ " δ_PDA = {regel|∃zustand1,zustand2,terminal.((zustand1,terminal)↦zustand2 ∈ δ_DFA ∧\n",
+ " (regel = (zustand1, terminal, Bottom) ↦ (zustand2, [Bottom])))}\n",
+ " ∪\n",
+ " {regel | ∃zustand.(zustand ∈ F_DFA ∧\n",
+ " regel = (zustand, lambda, Bottom) ↦ (zustand, []))} ∧\n",
+ " \n",
+ " TM = (Σ, Γ_TM, Z_TM, δ_TM, z_start, Blank, F_TM) ∧\n",
+ " Γ_TM ⊆ Alphabet ∧\n",
+ " Z_TM ⊆ States ∧\n",
+ " δ_TM ∈ (Z_TM×Γ_TM)→(Z_TM×Γ_TM×Direction) ∧\n",
+ " z_start ∈ Z_TM ∧\n",
+ " Blank ∈ Γ_TM ∧\n",
+ " F_TM ⊆ Z_TM ∧\n",
+ " \n",
+ " Γ_TM = Σ ∪ {Blank} ∧\n",
+ " Z_TM = Z_DFA ∪ {z_end} ∧\n",
+ " δ_TM = {regel|∃zustand1,zustand2,terminal.((zustand1,terminal)↦zustand2 ∈ δ_DFA ∧\n",
+ " (regel = (zustand1, terminal) ↦ (zustand2, Blank, R)))}\n",
+ " ∪\n",
+ " {regel | ∃zustand.(zustand ∈ Z_DFA\\F_DFA ∧\n",
+ " regel = (zustand, Blank) ↦ (zustand, Blank, N))}\n",
+ " ∪\n",
+ " {regel | ∃zustand.(zustand ∈ F_DFA ∧\n",
+ " regel = (zustand, Blank) ↦ (z_end, Blank, N))}\n",
+ " ∪\n",
+ " {regel | ∃terminal.(terminal ∈ Γ_TM ∧ regel = (z_end, terminal) ↦ (z_end, terminal, N))} ∧\n",
+ " F_TM = {z_end} ∧\n",
+ " \n",
+ " Final ⊆ States ∧\n",
+ " δ ∈ (States * Alphabet) ↔ (States * Alphabet * Direction) ∧\n",
+ "\n",
+ " δ = { /* Neuer Zyklus */\n",
+ " (z0,a) ↦ (z1,X,R),\n",
+ " (z0,X) ↦ (z0,X,R),\n",
+ " \n",
+ " /* ein a getilgt (X), nächstes b suchen */\n",
+ " (z1,a) ↦ (z1,a,R),\n",
+ " (z1,b) ↦ (z2,X,R),\n",
+ " (z1,X) ↦ (z1,X,R),\n",
+ " \n",
+ " /* ein a,b getilgt (X), nächstes c suchen */\n",
+ " (z2,b) ↦ (z2,b,R),\n",
+ " (z2,c) ↦ (z3,X,R),\n",
+ " (z2,X) ↦ (z2,X,R),\n",
+ " \n",
+ " /* ein a,b,c getilgt (X), rechten Rand suchen */\n",
+ " (z3,c) ↦ (z3,c,R),\n",
+ " (z3,Blank) ↦ (z4,Blank,L),\n",
+ " \n",
+ " /* Zurücklaufen und testen ob alle a,b,c getilgt */\n",
+ " (z4,X) ↦ (z4,X,L),\n",
+ " (z4,Blank) ↦ (z6,Blank,R), /* Erfolg ∀ */\n",
+ " (z4,c) ↦ (z5,c,L), \n",
+ " \n",
+ " /* Test nicht erfolgreich; zum linken Rand zurücklaufen und neuer Zyklus */\n",
+ " (z5,X) ↦ (z5,X,L),\n",
+ " (z5,Blank) ↦ (z0,Blank,R),\n",
+ " (z5,a) ↦ (z5,a,L),\n",
+ " (z5,b) ↦ (z5,b,L),\n",
+ " (z5,c) ↦ (z5,c,L)\n",
+ " } ∧\n",
+ " Final = {z6}\n",
+ "VARIABLES Left,cur,Right\n",
+ "INVARIANT\n",
+ " cur ∈ States ∧\n",
+ " Left ∈ seq(Alphabet) ∧ Right ∈ seq(Alphabet)\n",
+ "INITIALISATION Left,cur,Right := [],z0,[a,a,b,b,c,c]\n",
+ "OPERATIONS\n",
+ " Accept = PRE cur ∈ Final THEN skip END;\n",
+ " GoTo(z,S,znew,NewSymbol,Dir) =\n",
+ " PRE z=cur ∧ S=CurSymbol ∧\n",
+ " (z, S) ↦ (znew,NewSymbol,Dir) ∈ δ THEN\n",
+ " ANY tail_Right \n",
+ " WHERE (Right=[] ⇒ tail_Right=[]) ∧ (Right≠[] ⇒ tail_Right = tail(Right)) THEN\n",
+ " cur := znew ||\n",
+ " IF Dir = N THEN\n",
+ " Right := NewSymbol -> tail_Right\n",
+ " ELSIF Dir = R THEN\n",
+ " Left,Right := Left <- NewSymbol, tail_Right\n",
+ " ELSIF Left=[] THEN\n",
+ " Left,Right := [], Blank -> (NewSymbol -> tail_Right)\n",
+ " ELSE\n",
+ " Left,Right := front(Left), last(Left) -> (NewSymbol -> tail_Right)\n",
+ " END\n",
+ " END\n",
+ " END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants DFA=({a, b}, //Σ\n",
+ " {z0,z1,z2,z3}, //Z\n",
+ " {(z0,a)↦z1, (z0,b)↦z3,\n",
+ " (z1,a)↦z3, (z1,b)↦z2,\n",
+ " (z2,a)↦z2, (z2,b)↦z2,\n",
+ " (z3,a)↦z3, (z3,b)↦z3 }, //δ\n",
+ " z0, {z0, z2}) //z0, F"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":dot COMMAND [FORMULA]\n",
+ "```\n",
+ "\n",
+ "Execute and show a dot visualisation.\n",
+ "\n",
+ "The following dot visualisation commands are available:\n",
+ "\n",
+ "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
+ "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n",
+ "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n",
+ "* `state_space` - State Space: Show state space\n",
+ "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
+ "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
+ "* `history` - Path to Current State: Show a path leading to current state\n",
+ "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
+ "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
+ "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
+ "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+ "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
+ "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
+ "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
+ "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
+ "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
+ "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
+ "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
+ "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
+ "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
+ "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
+ "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
+ "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
+ "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ ],
+ "text/plain": [
+ ":dot COMMAND [FORMULA]\n",
+ "Execute and show a dot visualisation.\n",
+ "\n",
+ "The following dot visualisation commands are available:\n",
+ "\n",
+ "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
+ "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n",
+ "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n",
+ "* `state_space` - State Space: Show state space\n",
+ "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
+ "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
+ "* `history` - Path to Current State: Show a path leading to current state\n",
+ "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
+ "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
+ "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
+ "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+ "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
+ "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
+ "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
+ "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
+ "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
+ "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
+ "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
+ "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
+ "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
+ "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
+ "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
+ "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
+ "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help dot"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 4
+}