From 6fbbb2503f1fe049dce61b932f83f03581bb0b0c Mon Sep 17 00:00:00 2001
From: Chris <Christopher.Happe@uni-duesseldorf.de>
Date: Sun, 11 Oct 2020 18:43:43 +0200
Subject: [PATCH] Visualisierung PDA nach kfG angepasst

---
 info4/kapitel-3/PDA_nach_kfG.ipynb | 259 +++++++++--------------------
 1 file changed, 79 insertions(+), 180 deletions(-)

diff --git a/info4/kapitel-3/PDA_nach_kfG.ipynb b/info4/kapitel-3/PDA_nach_kfG.ipynb
index bd2e7f7..398744a 100644
--- a/info4/kapitel-3/PDA_nach_kfG.ipynb
+++ b/info4/kapitel-3/PDA_nach_kfG.ipynb
@@ -4,12 +4,14 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "# PDA nach kfG\n"
+    "# PDA nach kfG\n",
+    "\n",
+    "Aus einem gegebenen PDA kann man auch eine kontextfreie Grammatik generieren, die die gleiche Sprache akzeptiert."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 41,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [
     {
@@ -18,7 +20,7 @@
        "Loaded machine: PDA_to_CFG"
       ]
      },
-     "execution_count": 41,
+     "execution_count": 1,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -41,12 +43,15 @@
     " SYM(s) == (symbol,s,symbol); // Darstellung eines Symbols als Tripel für die Grammatik\n",
     " kfG_TERMINALE == {x|∃t.(t∈Σ ∧ x=SYM(t))};\n",
     " \n",
-    " ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(Z,SYMBOLE)(prj1(Z*SYMBOLE,Z)(cur(c)))};\n",
-    " ANIMATION_FUNCTION2 == {r,c,i| r=2 ∧ c∈dom(cur) ∧ i=prj2(Z,SYMBOLE)(prj1(Z*SYMBOLE,Z)(cur(c)))};\n",
-    " ANIMATION_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(Z*SYMBOLE,Z)(cur(c))};\n",
+    " \"LibraryStrings.def\";\n",
+    " ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧\n",
+    "         i= IF ∃t.(t∈SYMBOLE ∧ cur(c) = (symbol |->t|-> symbol))\n",
+    "            THEN LET s BE s=TO_STRING({x | (symbol|->x|->symbol)=cur(c)})\n",
+    "                IN SUB_STRING(s,2,STRING_LENGTH(s)-2) END\n",
+    "            ELSE TO_STRING(cur(c)) END};\n",
     " ANIMATION_STR_JUSTIFY_LEFT == TRUE;\n",
     " SET_PREF_PP_SEQUENCES == TRUE\n",
-    "CONSTANTS δ, Regeln\n",
+    "CONSTANTS δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4\n",
     "PROPERTIES\n",
     " /* Ein PDA für {a^m b^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */\n",
     " δ = {     (z0,a,BOT) ↦ (z0,[A,BOT]),\n",
@@ -54,25 +59,23 @@
     "           (z0,b,A) ↦ (z1,[]),\n",
     "           (z1,lambda,BOT) ↦ (z1,[]),\n",
     "           (z1,b,A) ↦ (z1,[]) } ∧\n",
-    "\n",
-    "\n",
-    "  Regeln = /* Punkt 1 Folie 109 */\n",
-    "      { lhs,rhs | ∃z.(z∈PDA_Zustände ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}\n",
-    "       ∪\n",
-    "       /* Punkt 2 Folie 109 */\n",
-    "       { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈δ ∧\n",
-    "                   lhs=(z,A,z2) ∧ rhs = SYMS(a)) }\n",
-    "       ∪\n",
-    "       /* Punkt 3 Folie 110 */\n",
-    "       { lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈δ ∧ z2∈PDA_Zustände ∧\n",
-    "                   lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) }\n",
-    "       ∪\n",
-    "       /* Punkt 4 Folie 110 */\n",
-    "       { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈δ ∧ \n",
-    "                     z2∈PDA_Zustände ∧ \n",
-    "                     z3∈PDA_Zustände ∧\n",
+    "  \n",
+    "  /*Die Regeln der kfG zum PDA*/\n",
+    "  /* Punkt 1 Folie 109 */\n",
+    "  RegelnP1 = { lhs,rhs | ∃z.(z∈PDA_Zustände ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])} ∧\n",
+    "  /* Punkt 2 Folie 109 */\n",
+    "  RegelnP2 = { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈δ ∧ lhs=(z,A,z2) ∧ rhs = SYMS(a)) } ∧\n",
+    "  /* Punkt 3 Folie 110 */\n",
+    "  RegelnP3 = { lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈δ ∧ z2∈PDA_Zustände ∧\n",
+    "                   lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) } ∧\n",
+    "  /* Punkt 4 Folie 110 */\n",
+    "  RegelnP4 = { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈δ ∧ \n",
+    "                     z2∈PDA_Zustände ∧ z3∈PDA_Zustände ∧\n",
     "                     lhs=(z,A,z3) ∧ \n",
-    "                     rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }\n",
+    "                     rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) } ∧\n",
+    "  \n",
+    "  Regeln = RegelnP1 ∪ RegelnP2 ∪ RegelnP3 ∪ RegelnP4\n",
+    "       \n",
     "VARIABLES cur\n",
     "INVARIANT\n",
     " cur ∈ seq(kfG_Alphabet)\n",
@@ -82,7 +85,7 @@
     "  // Anwendung einer Grammatikregel\n",
     "  ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Regeln ∧\n",
     "                                    cur = pre^[LHS]^post ∧\n",
-    "                                    ran(pre) ⊆ kfG_TERMINALE /* Links Ableitung */\n",
+    "                                    ran(pre) ⊆ kfG_TERMINALE /* Linksableitung */\n",
     "  THEN\n",
     "     cur := pre^RHS^post\n",
     "  END\n",
@@ -91,7 +94,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 42,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
@@ -100,7 +103,7 @@
        "Machine constants set up using operation 0: $setup_constants()"
       ]
      },
-     "execution_count": 42,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -111,7 +114,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 43,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -120,7 +123,7 @@
        "Machine initialised using operation 1: $initialise_machine()"
       ]
      },
-     "execution_count": 43,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -131,7 +134,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 45,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -143,7 +146,7 @@
        "{(z0↦a↦A↦(z0↦[A,A])),(z0↦a↦BOT↦(z0↦[A,BOT])),(z0↦b↦A↦(z1↦[])),(z1↦b↦A↦(z1↦[])),(z1↦lambda↦BOT↦(z1↦[]))}"
       ]
      },
-     "execution_count": 45,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -152,9 +155,16 @@
     "δ"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Die Grammatik startet mit dem Startsymbol und simuliert die Ausführung eines entsprechenden PDAs. Dabei gibt es teils mehrere Wege, aber das Wort ab wird von mindestens einem erreicht."
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 46,
+   "execution_count": 5,
    "metadata": {},
    "outputs": [
     {
@@ -162,21 +172,15 @@
       "text/markdown": [
        "<table style=\"font-family:monospace\"><tbody>\n",
        "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "</tr>\n",
-       "<tr>\n",
        "<td style=\"padding:10px\">S</td>\n",
        "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "</tr>\n",
        "</tbody></table>"
       ],
       "text/plain": [
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 46,
+     "execution_count": 5,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -187,22 +191,22 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 6,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/plain": [
        "Machine: PDA_to_CFG\n",
-       "Sets: STATES, SYMBOLS\n",
-       "Constants: delta, Productions\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4\n",
        "Variables: cur\n",
        "Operations: \n",
        "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])\n",
        "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 6,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -213,7 +217,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
@@ -222,7 +226,7 @@
        "Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])"
       ]
      },
-     "execution_count": 21,
+     "execution_count": 7,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -233,7 +237,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -241,13 +245,7 @@
       "text/markdown": [
        "<table style=\"font-family:monospace\"><tbody>\n",
        "<tr>\n",
-       "<td style=\"padding:10px\">z0</td>\n",
-       "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">BOT</td>\n",
-       "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
+       "<td style=\"padding:10px\">(z0|->BOT|->z1)</td>\n",
        "</tr>\n",
        "</tbody></table>"
       ],
@@ -255,7 +253,7 @@
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 22,
+     "execution_count": 8,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -266,33 +264,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "Machine: PDA_to_CFG\n",
-       "Sets: STATES, SYMBOLS\n",
-       "Constants: delta, Productions\n",
-       "Variables: cur\n",
-       "Operations: \n",
-       "ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z0),(z0|->BOT|->z1)],[],[])\n",
-       "ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)],[],[])"
-      ]
-     },
-     "execution_count": 23,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    ":browse"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 9,
    "metadata": {},
    "outputs": [
     {
@@ -301,7 +273,7 @@
        "Executed operation: ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)],[],[])"
       ]
      },
-     "execution_count": 24,
+     "execution_count": 9,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -312,7 +284,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
@@ -320,19 +292,9 @@
       "text/markdown": [
        "<table style=\"font-family:monospace\"><tbody>\n",
        "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">z0</td>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
-       "</tr>\n",
-       "<tr>\n",
        "<td style=\"padding:10px\">a</td>\n",
-       "<td style=\"padding:10px\">A</td>\n",
-       "<td style=\"padding:10px\">BOT</td>\n",
-       "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
+       "<td style=\"padding:10px\">(z0|->A|->z1)</td>\n",
+       "<td style=\"padding:10px\">(z1|->BOT|->z1)</td>\n",
        "</tr>\n",
        "</tbody></table>"
       ],
@@ -340,7 +302,7 @@
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 25,
+     "execution_count": 10,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -351,34 +313,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 26,
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "Machine: PDA_to_CFG\n",
-       "Sets: STATES, SYMBOLS\n",
-       "Constants: delta, Productions\n",
-       "Variables: cur\n",
-       "Operations: \n",
-       "ApplyRule((z0|->A|->z1),[(symbol|->b|->symbol)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])\n",
-       "ApplyRule((z0|->A|->z1),[(symbol|->a|->symbol),(z0|->A|->z0),(z0|->A|->z1)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])\n",
-       "ApplyRule((z0|->A|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->A|->z1)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])"
-      ]
-     },
-     "execution_count": 26,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    ":browse"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [
     {
@@ -387,7 +322,7 @@
        "Executed operation: ApplyRule((z0|->A|->z1),[(symbol|->b|->symbol)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])"
       ]
      },
-     "execution_count": 27,
+     "execution_count": 11,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -398,7 +333,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": 12,
    "metadata": {},
    "outputs": [
     {
@@ -406,19 +341,9 @@
       "text/markdown": [
        "<table style=\"font-family:monospace\"><tbody>\n",
        "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
-       "</tr>\n",
-       "<tr>\n",
        "<td style=\"padding:10px\">a</td>\n",
        "<td style=\"padding:10px\">b</td>\n",
-       "<td style=\"padding:10px\">BOT</td>\n",
-       "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">z1</td>\n",
+       "<td style=\"padding:10px\">(z1|->BOT|->z1)</td>\n",
        "</tr>\n",
        "</tbody></table>"
       ],
@@ -426,7 +351,7 @@
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 28,
+     "execution_count": 12,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -437,32 +362,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "Machine: PDA_to_CFG\n",
-       "Sets: STATES, SYMBOLS\n",
-       "Constants: delta, Productions\n",
-       "Variables: cur\n",
-       "Operations: \n",
-       "ApplyRule((z1|->BOT|->z1),[],[(symbol|->a|->symbol),(symbol|->b|->symbol)],[])"
-      ]
-     },
-     "execution_count": 29,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    ":browse"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 31,
+   "execution_count": 13,
    "metadata": {},
    "outputs": [
     {
@@ -471,7 +371,7 @@
        "Executed operation: ApplyRule((z1|->BOT|->z1),[],[(symbol|->a|->symbol),(symbol|->b|->symbol)],[])"
       ]
      },
-     "execution_count": 31,
+     "execution_count": 13,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -482,7 +382,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 32,
+   "execution_count": 14,
    "metadata": {},
    "outputs": [
     {
@@ -490,24 +390,16 @@
       "text/markdown": [
        "<table style=\"font-family:monospace\"><tbody>\n",
        "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "</tr>\n",
-       "<tr>\n",
        "<td style=\"padding:10px\">a</td>\n",
        "<td style=\"padding:10px\">b</td>\n",
        "</tr>\n",
-       "<tr>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "<td style=\"padding:10px\">symbol</td>\n",
-       "</tr>\n",
        "</tbody></table>"
       ],
       "text/plain": [
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 32,
+     "execution_count": 14,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -518,20 +410,20 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 33,
+   "execution_count": 15,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/plain": [
        "Machine: PDA_to_CFG\n",
-       "Sets: STATES, SYMBOLS\n",
-       "Constants: delta, Productions\n",
+       "Sets: Z, SYMBOLE\n",
+       "Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4\n",
        "Variables: cur\n",
        "Operations: "
       ]
      },
-     "execution_count": 33,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -540,6 +432,13 @@
     ":browse"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Da das Wort fertig abgeleitet wurde ist keine Regel mehr ausführbar."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
-- 
GitLab