add first version of PDA to CFG notebook

info4/kapitel-3/PDA_nach_kfG.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# PDA nach kfG\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: PDA_to_CFG"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE PDA_to_CFG\n",
+    "/* Translating a PDA to a CFG */\n",
+    "SETS\n",
+    " STATES = {z0,z1,   symbol};\n",
+    " SYMBOLS={a,b, A, BOT, lambda,     S} /* BOT = # = bottom of stack*/\n",
+    "DEFINITIONS\n",
+    " CFG_Alphabet  == (STATES*(SYMBOLS-{lambda})*STATES);\n",
+    " Σ == {a,b};\n",
+    " Γ == {A,BOT};\n",
+    " ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};\n",
+    " ANIMATION_FUNCTION2 == {r,c,i| r=2 ∧ c∈dom(cur) ∧ i=prj2(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};\n",
+    " ANIMATION_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(STATES*SYMBOLS,STATES)(cur(c))};\n",
+    " ANIMATION_STR_JUSTIFY_LEFT == TRUE;\n",
+    " SET_PREF_PP_SEQUENCES == TRUE;\n",
+    " PDA_STATES == (STATES-{symbol});\n",
+    "\n",
+    " SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;\n",
+    " SYM(s) == (symbol,s,symbol);\n",
+    " TERMINALS == {x|∃t.(t∈Σ ∧ x=SYM(t))}\n",
+    "CONSTANTS delta, Productions\n",
+    "PROPERTIES\n",
+    " /* A PDA accepting {a^mb^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */\n",
+    " delta = { (z0,a,BOT) ↦ (z0,[A,BOT]),\n",
+    "           (z0,a,A) ↦ (z0,[A,A]),\n",
+    "           (z0,b,A) ↦ (z1,[]),\n",
+    "           (z1,lambda,BOT) ↦ (z1,[]),\n",
+    "           (z1,b,A) ↦ (z1,[]) } ∧\n",
+    "\n",
+    "\n",
+    "  Productions = /* Punkt 1 Folie 109 */\n",
+    "      { lhs,rhs | ∃z.(z∈PDA_STATES ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}\n",
+    "       ∪\n",
+    "       /* Punkt 2 Folie 109 */\n",
+    "       { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈delta ∧\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])∈delta ∧ z2∈PDA_STATES ∧\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])∈delta ∧ \n",
+    "                     z2∈PDA_STATES ∧ z3∈PDA_STATES ∧\n",
+    "                     lhs=(z,A,z3) ∧ rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }\n",
+    "VARIABLES cur\n",
+    "INVARIANT\n",
+    " cur ∈ seq(CFG_Alphabet)\n",
+    "INITIALISATION cur:=SYMS(S)\n",
+    "OPERATIONS\n",
+    "  ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Productions ∧\n",
+    "                                    cur = pre^[LHS]^post ∧\n",
+    "                                    ran(pre) ⊆ TERMINALS /* Links Ableitung */\n",
+    "  THEN\n",
+    "     cur := pre^RHS^post\n",
+    "  END\n",
+    "END\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "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": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: PDA_to_CFG\n",
+       "Sets: STATES, SYMBOLS\n",
+       "Constants: delta, Productions\n",
+       "Variables: cur\n",
+       "Operations: \n",
+       "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])\n",
+       "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec ApplyRule"
+   ]
+  },
+  {
+   "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
+}