diff --git a/info4/kapitel-4/DPDA.ipynb b/info4/kapitel-4/DPDA.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..28c43b8853f836ea9da6c880ab4cf8dfb595e9a3
--- /dev/null
+++ b/info4/kapitel-4/DPDA.ipynb
@@ -0,0 +1,651 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# DPDA\n",
+ "\n",
+ "Ein __deterministischer Kellerautomat__ \n",
+ "(kurz DPDA für __deterministic push-down automaton__) ist ein $7$-Tupel \n",
+ " $M = (\\Sigma, \\Gamma, Z, \\delta , z_0, \\#,F)$, wobei\n",
+ "* $\\Sigma$ das Eingabe-Alphabet ist, \n",
+ "* $\\Gamma$ das Kelleralphabet, \n",
+ "* $Z$ eine endliche Menge von Zuständen,\n",
+ "* $\\delta : Z \\times (\\Sigma \\cup \\{\\lambda\\}) \\times \\Gamma\n",
+ " \\rightarrow \\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ die\n",
+ " Überführungsfunktion,\n",
+ "* $z_0 \\in Z$ der Startzustand,\n",
+ "* $\\# \\in \\Gamma$ das Bottom-Symbol im Keller,\n",
+ "* $F \\subseteq Z$ sind die Endzustände\n",
+ "\n",
+ "wo gilt:\n",
+ "* $(\\forall a \\in \\Sigma)\\, (\\forall A \\in \\Gamma)\\, (\\forall z \\in\n",
+ " Z)\\, [ \\|\\delta(z, a, A)\\| + \\|\\delta(z, \\lambda , A)\\| \\leq 1]$\n",
+ "\n",
+ "Anmerkung: $\\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ ist die Menge aller\n",
+ " __endlichen__ Teilmengen von $Z \\times \\Gamma^{\\ast}$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: DPDA"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE DPDA\n",
+ "/* B Modell eines PDA */\n",
+ "SETS\n",
+ " Z = {z0,z1,ze}; // die Zustände des Automaten, z0 ist der Startzustand\n",
+ " SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n",
+ "DEFINITIONS\n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",
+ " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n",
+ " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n",
+ " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",
+ " SET_PREF_PP_SEQUENCES == TRUE\n",
+ "CONSTANTS δ, F, Σ, Γ\n",
+ "PROPERTIES\n",
+ " Σ = {a,b} // das Eingabe-Alphabet\n",
+ " ∧\n",
+ " Γ = {A,BOT} // das Kelleralphabet\n",
+ " ∧\n",
+ " /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",
+ " δ = { (z0,a,BOT) ↦ (z0,[A,BOT]),\n",
+ " (z0,a,A) ↦ (z0,[A,A]),\n",
+ " (z0,b,A) ↦ (z1,[]),\n",
+ " (z1,lambda,BOT) ↦ (ze,[]),\n",
+ " (z1,b,A) ↦ (z1,[]) } ∧\n",
+ " F = {ze} // die Endzustände\n",
+ " // Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert\n",
+ " // Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript\n",
+ "ASSERTIONS\n",
+ " !(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,a,A)}]) ≤ 1)\n",
+ " /*@desc Die Überführungsfunktion ist deterministisch */\n",
+ "VARIABLES \n",
+ " z, α, γ // Konfiguration in dem sich der PDA befindet\n",
+ "INVARIANT\n",
+ " z ∈ Z ∧ // der aktuelle Zustand\n",
+ " α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts\n",
+ " γ ∈ seq(Γ) // aktuelle Kellerinhalt\n",
+ "INITIALISATION\n",
+ " z := z0 ||\n",
+ " γ := [BOT] || // Initialisierung des Stapels\n",
+ " α := [a,a,b,b] // das Eingabewort\n",
+ "OPERATIONS\n",
+ " // die Operationen Schritt und LambdaSchritt modellieren\n",
+ " // Schritte in der Ableitungsrelation\n",
+ " Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧\n",
+ " z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN\n",
+ " z := z‘ || // in den neuen Zustand wechseln\n",
+ " α := tail(α) || // das erste Symbol auf der Eingabe löschen\n",
+ " γ := s^tail(γ) // s auf den Stapel packen\n",
+ " END;\n",
+ " LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧\n",
+ " z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN\n",
+ " z := z‘ || // in den neuen Zustand wechseln\n",
+ " γ := s^tail(γ) // s auf den Stapel packen\n",
+ " END;\n",
+ " Akzeptieren = PRE γ = ∅ ∧ z∈F THEN \n",
+ " /* Wir akzeptieren wenn Eingabe leer und wir in einem Endzustand sind */\n",
+ " skip END;\n",
+ " AkzeptierenMitLeeremKeller = PRE γ = ∅ ∧ α = ∅ THEN \n",
+ " /* Wir akzeptieren wenn Eingabe und Stapel leer sind */\n",
+ " skip END\n",
+ "END\n",
+ "\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir prüfen nun ob der PDA auch wirklich deterministisch ist:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "!(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,lambda,A)}]) ≤ 1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir können uns auch tabellarisch für jede Kombination an Symbolen und Zuständen die Kardinalität der möglichen Übergange ausgeben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|a|A|z|ca|cl|\n",
+ "|---|---|---|---|---|\n",
+ "|$\\mathit{a}$|$\\mathit{A}$|$\\mathit{z0}$|$1$|$0$|\n",
+ "|$\\mathit{a}$|$\\mathit{A}$|$\\mathit{z1}$|$0$|$0$|\n",
+ "|$\\mathit{a}$|$\\mathit{A}$|$\\mathit{ze}$|$0$|$0$|\n",
+ "|$\\mathit{a}$|$\\mathit{BOT}$|$\\mathit{z0}$|$1$|$0$|\n",
+ "|$\\mathit{a}$|$\\mathit{BOT}$|$\\mathit{z1}$|$0$|$1$|\n",
+ "|$\\mathit{a}$|$\\mathit{BOT}$|$\\mathit{ze}$|$0$|$0$|\n",
+ "|$\\mathit{b}$|$\\mathit{A}$|$\\mathit{z0}$|$1$|$0$|\n",
+ "|$\\mathit{b}$|$\\mathit{A}$|$\\mathit{z1}$|$1$|$0$|\n",
+ "|$\\mathit{b}$|$\\mathit{A}$|$\\mathit{ze}$|$0$|$0$|\n",
+ "|$\\mathit{b}$|$\\mathit{BOT}$|$\\mathit{z0}$|$0$|$0$|\n",
+ "|$\\mathit{b}$|$\\mathit{BOT}$|$\\mathit{z1}$|$0$|$1$|\n",
+ "|$\\mathit{b}$|$\\mathit{BOT}$|$\\mathit{ze}$|$0$|$0$|\n"
+ ],
+ "text/plain": [
+ "a\tA\tz\tca\tcl\n",
+ "a\tA\tz0\t1\t0\n",
+ "a\tA\tz1\t0\t0\n",
+ "a\tA\tze\t0\t0\n",
+ "a\tBOT\tz0\t1\t0\n",
+ "a\tBOT\tz1\t0\t1\n",
+ "a\tBOT\tze\t0\t0\n",
+ "b\tA\tz0\t1\t0\n",
+ "b\tA\tz1\t1\t0\n",
+ "b\tA\tze\t0\t0\n",
+ "b\tBOT\tz0\t0\t0\n",
+ "b\tBOT\tz1\t0\t1\n",
+ "b\tBOT\tze\t0\t0\n"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {a,A,z,ca,cl| a∈Σ ∧ A∈Γ ∧ z∈Z ∧ ca=card(δ[{(z,a,A)}]) & cl = card(δ[{(z,lambda,A)}])}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: DPDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, F, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,[A,BOT])"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[A,BOT])"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[A,A])"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">A</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:10px\">BOT</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: DPDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, F, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(ze,[])"
+ ]
+ },
+ "execution_count": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(ze,[])"
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">z: </td>\n",
+ "<td style=\"padding:10px\">ze</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">α:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">γ:</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 43,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: DPDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, F, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Akzeptieren()\n",
+ "AkzeptierenMitLeeremKeller()"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Akzeptieren()"
+ ]
+ },
+ "execution_count": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Akzeptieren"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "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": 2
+}