add kfG to PDA example

info4/kapitel-3/PDA-Kellerautomaten.ipynb

@@ -57,7 +57,7 @@
     " Γ == {A,BOT}; // das Kelleralphabet\n",
     " \n",
     " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",
-    " ANIMATION_FUNCTION == {2}*α \\/ {3}*(γ);\n",
+    " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n",
     " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n",
     " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",
     " SET_PREF_PRETTY_PRINT_SEQUENCES == TRUE\n",
@@ -682,6 +682,796 @@
     "Das Eingabewort ``aabb`` wurde akzeptiert."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## PDA für eine kfG\n",
+    "\n",
+    "Aus einer kontextfreien Grammatik kann man einen PDA konstruieren der die gleiche Sprache akzeptiert."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: PDA"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE PDA\n",
+    "/* B Modell eines PDA */\n",
+    "SETS\n",
+    " Z = {z0}; // die Zustände des Automaten, z0 ist der Startzustand\n",
+    " SYMBOLE={a,b, S, C, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n",
+    "DEFINITIONS\n",
+    " Σ == {a,b};   // das Eingabe-Alphabet\n",
+    " BOT == S;\n",
+    " Γ == {S,C}; // das Kelleralphabet\n",
+    " \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_PRETTY_PRINT_SEQUENCES == TRUE\n",
+    "CONSTANTS P, δ\n",
+    "PROPERTIES\n",
+    "/* Die Grammatik Regeln */\n",
+    " P = { S ↦ [a,S,b], S ↦ [C],\n",
+    "       C ↦ [a,b] } ∧\n",
+    "    \n",
+    " /* Berechnung von δ aus P */\n",
+    "  δ =  /* lässt sich eine Regel auf das Top-Symbol im Keller anwenden tue \n",
+    "          dies ohne etwas zu lesen :*/\n",
+    "         { lhs,rhs | ∃(A,q).( A↦q ∈ P ∧ lhs=(z0,lambda,A) ∧ rhs=(z0,q))}\n",
+    "         ∪\n",
+    "          /* ist das Top-Symbol im Keller ein Terminalzeichen a welches\n",
+    "             auf der Eingabe steht, so wird dies aus dem Keller gePOPt */\n",
+    "         { lhs,rhs | ∃a.(a∈Σ ∧ lhs = (z0,a,a) & rhs = (z0,[]))}\n",
+    " \n",
+    " \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 γ = ∅ ∧ α = ∅ THEN  \n",
+    "              /* Wir akzeptieren wenn Eingabe und Stapel leer sind */\n",
+    "   skip END\n",
+    "END\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 33,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|z|x|X|z2|Xs|\n",
+       "|---|---|---|---|---|\n",
+       "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{z0}$|$\\mathit{a}$|$\\mathit{a}$|$\\mathit{z0}$|$\\emptyset$|\n",
+       "|$\\mathit{z0}$|$\\mathit{b}$|$\\mathit{b}$|$\\mathit{z0}$|$\\emptyset$|\n",
+       "|$\\mathit{z0}$|$\\mathit{S}$|$\\mathit{S}$|$\\mathit{z0}$|$\\emptyset$|\n",
+       "|$\\mathit{z0}$|$\\mathit{C}$|$\\mathit{C}$|$\\mathit{z0}$|$\\emptyset$|\n",
+       "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{C})\\}$|\n",
+       "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{S}),(3\\mapsto \\mathit{b})\\}$|\n",
+       "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{C}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{b})\\}$|\n",
+       "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{lambda}$|$\\mathit{z0}$|$\\emptyset$|\n"
+      ],
+      "text/plain": [
+       "z\tx\tX\tz2\tXs\n",
+       "z0\ta\ta\tz0\t{}\n",
+       "z0\tb\tb\tz0\t{}\n",
+       "z0\tS\tS\tz0\t{}\n",
+       "z0\tC\tC\tz0\t{}\n",
+       "z0\tlambda\tS\tz0\t{(1|->C)}\n",
+       "z0\tlambda\tS\tz0\t{(1|->a),(2|->S),(3|->b)}\n",
+       "z0\tlambda\tC\tz0\t{(1|->a),(2|->b)}\n",
+       "z0\tlambda\tlambda\tz0\t{}\n"
+      ]
+     },
+     "execution_count": 33,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "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",
+       "<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\">b</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:10px\">γ:</td>\n",
+       "<td style=\"padding:10px\">S</td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: P, δ\n",
+       "Variables: z, α, γ\n",
+       "Operations: \n",
+       "LambdaSchritt(z0,{(1|->C)})\n",
+       "LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec LambdaSchritt s = [a,S,b]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "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",
+       "<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\">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\">S</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: P, δ\n",
+       "Variables: z, α, γ\n",
+       "Operations: \n",
+       "Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Schritt"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "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\">S</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: P, δ\n",
+       "Variables: z, α, γ\n",
+       "Operations: \n",
+       "LambdaSchritt(z0,{(1|->C)})\n",
+       "LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})"
+      ]
+     },
+     "execution_count": 15,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: LambdaSchritt(z0,{(1|->C)})"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec LambdaSchritt s = [C]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "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\">C</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "<td style=\"padding:0px\"></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 17,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: P, δ\n",
+       "Variables: z, α, γ\n",
+       "Operations: \n",
+       "LambdaSchritt(z0,{(1|->a),(2|->b)})"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 19,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: LambdaSchritt(z0,{(1|->a),(2|->b)})"
+      ]
+     },
+     "execution_count": 19,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec LambdaSchritt s=[a,b]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "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\">b</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 22,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: P, δ\n",
+       "Variables: z, α, γ\n",
+       "Operations: \n",
+       "Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 22,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Schritt"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "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",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:10px\">α:</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\">b</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 24,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 25,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Schritt"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "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",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:10px\">α:</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:10px\">γ:</td>\n",
+       "<td style=\"padding:10px\">b</td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 26,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Schritt(z0,{})"
+      ]
+     },
+     "execution_count": 27,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Schritt"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "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",
+       "</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": 28,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 30,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Akzeptieren()"
+      ]
+     },
+     "execution_count": 30,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Akzeptieren"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Das Wort ``aabb`` wird sowohl von der Grammatik generiert als auch von diesem generierten PDA akzeptiert."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,