Output der Zellen an aktuellen Stand der Maschiene angepasst

f8a51ec4 · Chris · 9fe42d20 · f8a51ec4
Commit f8a51ec4 authored Nov 7, 2020 by Chris
--- a/info4/kapitel-3/PDA-Kellerautomaten.ipynb
+++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
@@ -191,7 +191,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 63,
+   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
@@ -199,13 +199,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "Schritt(z0,[A,BOT])"
      ]
     },
-     "execution_count": 63,
+     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -216,7 +216,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 64,
+   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
@@ -225,7 +225,7 @@
       "Executed operation: Schritt(z0,[A,BOT])"
      ]
     },
-     "execution_count": 64,
+     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -236,7 +236,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 65,
+   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
@@ -267,7 +267,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 65,
+     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -278,7 +278,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 66,
+   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
@@ -290,7 +290,7 @@
       "(z0↦[a,b,b]↦[A,BOT])"
      ]
     },
-     "execution_count": 66,
+     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -301,7 +301,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 67,
+   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
@@ -309,13 +309,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "Schritt(z0,[A,A])"
      ]
     },
-     "execution_count": 67,
+     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -326,7 +326,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 68,
+   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
@@ -335,7 +335,7 @@
       "Executed operation: Schritt(z0,[A,A])"
      ]
     },
-     "execution_count": 68,
+     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -346,7 +346,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 69,
+   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
@@ -377,7 +377,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 69,
+     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -388,7 +388,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 70,
+   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
@@ -396,13 +396,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "Schritt(z1,[])"
      ]
     },
-     "execution_count": 70,
+     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -413,7 +413,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 71,
+   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
@@ -422,7 +422,7 @@
       "Executed operation: Schritt(z1,[])"
      ]
     },
-     "execution_count": 71,
+     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -433,7 +433,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 72,
+   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
@@ -461,7 +461,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 72,
+     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -472,7 +472,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 73,
+   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
@@ -480,13 +480,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "Schritt(z1,[])"
      ]
     },
-     "execution_count": 73,
+     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -497,7 +497,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 74,
+   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
@@ -506,7 +506,7 @@
       "Executed operation: Schritt(z1,[])"
      ]
     },
-     "execution_count": 74,
+     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -517,7 +517,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 75,
+   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
@@ -542,7 +542,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 75,
+     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -553,7 +553,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 76,
+   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
@@ -561,13 +561,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "LambdaSchritt(z1,[])"
      ]
     },
-     "execution_count": 76,
+     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -578,7 +578,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 77,
+   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
@@ -587,7 +587,7 @@
       "Executed operation: LambdaSchritt(z1,[])"
      ]
     },
-     "execution_count": 77,
+     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -598,7 +598,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 78,
+   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
@@ -623,7 +623,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 78,
+     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -634,7 +634,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 79,
+   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
@@ -642,13 +642,13 @@
      "text/plain": [
       "Machine: PDA\n",
       "Sets: Z, SYMBOLE\n",
-       "Constants: δ\n",
+       "Constants: δ, Σ, Γ\n",
       "Variables: z, α, γ\n",
       "Operations: \n",
       "Akzeptieren()"
      ]
     },
-     "execution_count": 79,
+     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -659,7 +659,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 80,
+   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
@@ -668,7 +668,7 @@
       "Executed operation: Akzeptieren()"
      ]
     },
-     "execution_count": 80,
+     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -695,7 +695,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 34,
+   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
@@ -704,7 +704,7 @@
       "Loaded machine: PDA_für_kfG"
      ]
     },
-     "execution_count": 34,
+     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -775,7 +775,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
@@ -784,7 +784,7 @@
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
-     "execution_count": 35,
+     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -795,7 +795,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 36,
+   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
@@ -804,7 +804,7 @@
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
-     "execution_count": 36,
+     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -815,7 +815,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 37,
+   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
@@ -844,7 +844,7 @@
       "z0\tlambda\tlambda\tz0\t[]\n"
      ]
     },
-     "execution_count": 37,
+     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -855,7 +855,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 38,
+   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
@@ -889,7 +889,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 38,
+     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -900,7 +900,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 39,
+   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
@@ -915,7 +915,7 @@
       "LambdaSchritt(z0,[a,S,b])"
      ]
     },
-     "execution_count": 39,
+     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -926,7 +926,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 40,
+   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
@@ -935,7 +935,7 @@
       "Executed operation: LambdaSchritt(z0,[a,S,b])"
      ]
     },
-     "execution_count": 40,
+     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -946,7 +946,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 41,
+   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
@@ -980,7 +980,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 41,
+     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -991,7 +991,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 42,
+   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
@@ -1005,7 +1005,7 @@
       "Schritt(z0,[])"
      ]
     },
-     "execution_count": 42,
+     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1016,7 +1016,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 43,
+   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
@@ -1025,7 +1025,7 @@
       "Executed operation: Schritt(z0,[])"
      ]
     },
-     "execution_count": 43,
+     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1036,7 +1036,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 44,
+   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
@@ -1067,7 +1067,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 44,
+     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1078,7 +1078,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 45,
+   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
@@ -1093,7 +1093,7 @@
       "LambdaSchritt(z0,[a,S,b])"
      ]
     },
-     "execution_count": 45,
+     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1104,7 +1104,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 46,
+   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
@@ -1113,7 +1113,7 @@
       "Executed operation: LambdaSchritt(z0,[C])"
      ]
     },
-     "execution_count": 46,
+     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1124,7 +1124,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 47,
+   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
@@ -1155,7 +1155,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 47,
+     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1166,7 +1166,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 48,
+   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
@@ -1180,7 +1180,7 @@
       "LambdaSchritt(z0,[a,b])"
      ]
     },
-     "execution_count": 48,
+     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1191,7 +1191,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 49,
+   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
@@ -1200,7 +1200,7 @@
       "Executed operation: LambdaSchritt(z0,[a,b])"
      ]
     },
-     "execution_count": 49,
+     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1211,7 +1211,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 50,
+   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
@@ -1242,7 +1242,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 50,
+     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1253,7 +1253,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 51,
+   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
@@ -1267,7 +1267,7 @@
       "Schritt(z0,[])"
      ]
     },
-     "execution_count": 51,
+     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1278,7 +1278,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 52,
+   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
@@ -1287,7 +1287,7 @@
       "Executed operation: Schritt(z0,[])"
      ]
     },
-     "execution_count": 52,
+     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1298,7 +1298,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 53,
+   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
@@ -1326,7 +1326,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 53,
+     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1337,7 +1337,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 54,
+   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
@@ -1346,7 +1346,7 @@
       "Executed operation: Schritt(z0,[])"
      ]
     },
-     "execution_count": 54,
+     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1357,7 +1357,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 55,
+   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
@@ -1382,7 +1382,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 55,
+     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1393,7 +1393,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 56,
+   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
@@ -1402,7 +1402,7 @@
       "Executed operation: Schritt(z0,[])"
      ]
     },
-     "execution_count": 56,
+     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1413,7 +1413,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 57,
+   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
@@ -1438,7 +1438,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 57,
+     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1449,7 +1449,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 58,
+   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
@@ -1458,7 +1458,7 @@
       "Executed operation: Akzeptieren()"
      ]
     },
-     "execution_count": 58,
+     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }

 %% Cell type:markdown id: tags:
 # PDA (Push Down Automata - Kellerautomaten)
 %% Cell type:markdown id: tags:
 Ein __(nichtdeterministischer) Kellerautomat__
 (kurz PDA für __push-down automaton__) ist ein $6$-Tupel
  $M = (\Sigma, \Gamma, Z, \delta , z_0, \#)$, wobei
 * $\Sigma$ das Eingabe-Alphabet ist,
 * $\Gamma$ das Kelleralphabet,
 * $Z$ eine endliche Menge von Zuständen,
 * $\delta : Z \times (\Sigma \cup \{\lambda\}) \times \Gamma
  \rightarrow \mathfrak{P}_e(Z \times \Gamma^{\ast})$ die
  Überführungsfunktion,
 * $z_0 \in Z$ der Startzustand,
 * $\# \in \Gamma$ das Bottom-Symbol im Keller.
 Anmerkung: $\mathfrak{P}_e(Z \times \Gamma^{\ast})$ ist die Menge aller
  __endlichen__ Teilmengen von $Z \times \Gamma^{\ast}$.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE PDA
 /* B Modell eines PDA */
 SETS
 Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand
 SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/
 DEFINITIONS
 ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
 ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);
 ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
 ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
 SET_PREF_PP_SEQUENCES == TRUE
 CONSTANTS δ, Σ, Γ
 PROPERTIES
 Σ = {a,b}    // das Eingabe-Alphabet
 ∧
 Γ = {A,BOT} // das Kelleralphabet
 ∧
 /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
 δ = {     (z0,a,BOT)      ↦  (z0,[A,BOT]),
           (z0,a,A)        ↦  (z0,[A,A]),
           (z0,b,A)        ↦  (z1,[]),
           (z1,lambda,BOT) ↦  (z1,[]),
           (z1,b,A)        ↦  (z1,[]) }
 // Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert
 //  Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript
 VARIABLES
  z, α, γ  // Konfiguration in dem sich der PDA befindet
 INVARIANT
 z ∈ Z ∧ // der aktuelle Zustand
 α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
 γ ∈ seq(Γ) // aktuelle Kellerinhalt
 INITIALISATION
  z := z0 ||
  γ := [BOT] || // Initialisierung des Stapels
  α := [a,a,b,b] // das Eingabewort
 OPERATIONS
 // die Operationen Schritt und LambdaSchritt modellieren
 // Schritte in der Ableitungsrelation
  Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
                z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
     z := z‘ || // in den neuen Zustand wechseln
     α := tail(α) || // das erste Symbol auf der Eingabe löschen
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
                      z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
     z := z‘ ||  // in den neuen Zustand wechseln
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN
              /* Wir akzeptieren wenn Eingabe und Stapel leer sind */
   skip END
 END
 ```
 %% Output
    Loaded machine: PDA
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">BOT</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 (z,α,γ)
 ```
 %% Output
    $(\mathit{z0}\mapsto [a,\mathit{b},b]\mapsto [A,BOT])$
    (z0↦[a,b,b]↦[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[A,A])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[A,A])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt
 ```
 %% Output
    Executed operation: LambdaSchritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
-    Constants: δ
+    Constants: δ, Σ, Γ
    Variables: z, α, γ
    Operations:
    Akzeptieren()
 %% Cell type:code id: tags:
 ``` prob
 :exec Akzeptieren
 ```
 %% Output
    Executed operation: Akzeptieren()
 %% Cell type:markdown id: tags:
 Das Eingabewort ``aabb`` wurde akzeptiert.
 %% Cell type:markdown id: tags:
 ## PDA für eine kfG
 Aus einer kontextfreien Grammatik kann man einen PDA konstruieren der die gleiche Sprache akzeptiert.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE PDA_für_kfG
 /* B Modell eines PDA */
 SETS
 Z = {z0}; // die Zustände des Automaten, z0 ist der Startzustand
 SYMBOLE={a,b, S, C, lambda} /* BOT = # = Bottom-Symbol im Keller*/
 DEFINITIONS
 Σ == {a,b};   // das Eingabe-Alphabet
 BOT == S;
 Γ == {S,C}; // das Kelleralphabet
 ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
 ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);
 ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
 ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
 SET_PREF_PP_SEQUENCES == TRUE
 CONSTANTS P, δ
 PROPERTIES
 /* Die Grammatik Regeln */
 P = { S ↦ [a,S,b], S ↦ [C],
       C ↦ [a,b] } ∧
 /* Berechnung von δ aus P */
  δ =  /* lässt sich eine Regel auf das Top-Symbol im Keller anwenden tue
          dies ohne etwas zu lesen :*/
         { lhs,rhs | ∃(A,q).( A↦q ∈ P ∧ lhs=(z0,lambda,A) ∧ rhs=(z0,q))}
         ∪
          /* ist das Top-Symbol im Keller ein Terminalzeichen a welches
             auf der Eingabe steht, so wird dies aus dem Keller gePOPt */
         { lhs,rhs | ∃a.(a∈Σ ∧ lhs = (z0,a,a) & rhs = (z0,[]))}
 VARIABLES
  z, α, γ  // Konfiguration in dem sich der PDA befindet
 INVARIANT
 z ∈ Z ∧ // der aktuelle Zustand
 α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
 γ ∈ seq(Γ) // aktuelle Kellerinhalt
 INITIALISATION
  z := z0 ||
  γ := [BOT] || // Initialisierung des Stapels
  α := [a,a,b,b] // das Eingabewort
 OPERATIONS
 // die Operationen Schritt und LambdaSchritt modellieren
 // Schritte in der Ableitungsrelation
  Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
                z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
     z := z‘ || // in den neuen Zustand wechseln
     α := tail(α) || // das erste Symbol auf der Eingabe löschen
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
                      z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
     z := z‘ ||  // in den neuen Zustand wechseln
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN
              /* Wir akzeptieren wenn Eingabe und Stapel leer sind */
   skip END
 END
 ```
 %% Output
    Loaded machine: PDA_für_kfG
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}
 ```
 %% Output
    |z|x|X|z2|Xs|
    |---|---|---|---|---|
    |$\mathit{z0}$|$\mathit{a}$|$\mathit{a}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{b}$|$\mathit{b}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{S}$|$\mathit{S}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{C}$|$\mathit{C}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{S}$|$\mathit{z0}$|$[C]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{S}$|$\mathit{z0}$|$[a,\mathit{S},b]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{C}$|$\mathit{z0}$|$[a,b]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{lambda}$|$\mathit{z0}$|$[]$|
    z	x	X	z2	Xs
    z0	a	a	z0	[]
    z0	b	b	z0	[]
    z0	S	S	z0	[]
    z0	C	C	z0	[]
    z0	lambda	S	z0	[C]
    z0	lambda	S	z0	[a,S,b]
    z0	lambda	C	z0	[a,b]
    z0	lambda	lambda	z0	[]
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">S</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[C])
    LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s = [a,S,b]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">S</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">S</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[C])
    LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s = [C]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[C])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">C</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[a,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s=[a,b]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[a,b])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Akzeptieren
 ```
 %% Output
    Executed operation: Akzeptieren()
 %% Cell type:markdown id: tags:
 Das Wort ``aabb`` wird sowohl von der Grammatik generiert als auch von diesem generierten PDA akzeptiert.
 %% Cell type:code id: tags:
 ``` prob
 ```