From 88344fb46fb6546f2443fd20d75eb7d2f34ef724 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 19 May 2023 14:19:55 +0200
Subject: [PATCH] minor changes
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
info4/kapitel-2/RegulaereAusdruecke.ipynb | 32 +-
info4/kapitel-3/CYK_Algorithmus.ipynb | 172 +-
.../PDA-Kellerautomaten-Unicode.ipynb | 1653 +++++++++++++++++
info4/kapitel-3/PDA-Kellerautomaten.ipynb | 40 +-
4 files changed, 1792 insertions(+), 105 deletions(-)
create mode 100644 info4/kapitel-3/PDA-Kellerautomaten-Unicode.ipynb
diff --git a/info4/kapitel-2/RegulaereAusdruecke.ipynb b/info4/kapitel-2/RegulaereAusdruecke.ipynb
index 3283846..7e529bf 100644
--- a/info4/kapitel-2/RegulaereAusdruecke.ipynb
+++ b/info4/kapitel-2/RegulaereAusdruecke.ipynb
@@ -94,7 +94,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
@@ -103,7 +103,7 @@
"Loaded machine: Regex"
]
},
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -117,16 +117,16 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Machine initialised using operation 0: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -144,7 +144,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
@@ -156,7 +156,7 @@
"TRUE"
]
},
- "execution_count": 6,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -167,7 +167,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -179,7 +179,7 @@
"TRUE"
]
},
- "execution_count": 9,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -190,7 +190,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -202,7 +202,7 @@
"TRUE"
]
},
- "execution_count": 14,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -213,7 +213,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -225,7 +225,7 @@
"TRUE"
]
},
- "execution_count": 15,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -244,19 +244,19 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 4,\\mathit{string}\\in\\text{\"aab\"},\\mathit{submatches}\\in\\emptyset)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 4,\\mathit{string}\\in\\text{\"aab\"},\\mathit{submatches}\\in\\emptyset)$"
],
"text/plain": [
"rec(length∈3,position∈4,string∈\"aab\",submatches∈∅)"
]
},
- "execution_count": 20,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/info4/kapitel-3/CYK_Algorithmus.ipynb b/info4/kapitel-3/CYK_Algorithmus.ipynb
index d83a945..46226cd 100644
--- a/info4/kapitel-3/CYK_Algorithmus.ipynb
+++ b/info4/kapitel-3/CYK_Algorithmus.ipynb
@@ -85,7 +85,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
@@ -105,7 +105,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
@@ -117,6 +117,26 @@
":init"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: PP_SEQUENCES = TRUE\n"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref PP_SEQUENCES=TRUE"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -126,19 +146,19 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\{(1\\mapsto \\mathit{b}),(2\\mapsto \\mathit{a}),(3\\mapsto \\mathit{a}),(4\\mapsto \\mathit{b}),(5\\mapsto \\mathit{a})\\}$"
+ "$[\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{a}]$"
],
"text/plain": [
- "{(1↦b),(2↦a),(3↦a),(4↦b),(5↦a)}"
+ "[b,a,a,b,a]"
]
},
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -157,7 +177,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -184,7 +204,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -195,7 +215,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -207,7 +227,7 @@
"{S,A,B,C}"
]
},
- "execution_count": 6,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -218,19 +238,19 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\{(\\{(1\\mapsto \\mathit{S})\\}\\mapsto\\{(1\\mapsto \\mathit{A}),(2\\mapsto \\mathit{B})\\}),(\\{(1\\mapsto \\mathit{S})\\}\\mapsto\\{(1\\mapsto \\mathit{B}),(2\\mapsto \\mathit{C})\\}),(\\{(1\\mapsto \\mathit{A})\\}\\mapsto\\{(1\\mapsto \\mathit{a})\\}),(\\{(1\\mapsto \\mathit{A})\\}\\mapsto\\{(1\\mapsto \\mathit{B}),(2\\mapsto \\mathit{A})\\}),(\\{(1\\mapsto \\mathit{B})\\}\\mapsto\\{(1\\mapsto \\mathit{b})\\}),(\\{(1\\mapsto \\mathit{B})\\}\\mapsto\\{(1\\mapsto \\mathit{C}),(2\\mapsto \\mathit{C})\\}),(\\{(1\\mapsto \\mathit{C})\\}\\mapsto\\{(1\\mapsto \\mathit{a})\\}),(\\{(1\\mapsto \\mathit{C})\\}\\mapsto\\{(1\\mapsto \\mathit{A}),(2\\mapsto \\mathit{B})\\})\\}$"
+ "$\\{([\\mathit{S}]\\mapsto[\\mathit{A},\\mathit{B}]),([\\mathit{S}]\\mapsto[\\mathit{B},\\mathit{C}]),([\\mathit{A}]\\mapsto[\\mathit{a}]),([\\mathit{A}]\\mapsto[\\mathit{B},\\mathit{A}]),([\\mathit{B}]\\mapsto[\\mathit{b}]),([\\mathit{B}]\\mapsto[\\mathit{C},\\mathit{C}]),([\\mathit{C}]\\mapsto[\\mathit{a}]),([\\mathit{C}]\\mapsto[\\mathit{A},\\mathit{B}])\\}$"
],
"text/plain": [
- "{({(1↦S)}↦{(1↦A),(2↦B)}),({(1↦S)}↦{(1↦B),(2↦C)}),({(1↦A)}↦{(1↦a)}),({(1↦A)}↦{(1↦B),(2↦A)}),({(1↦B)}↦{(1↦b)}),({(1↦B)}↦{(1↦C),(2↦C)}),({(1↦C)}↦{(1↦a)}),({(1↦C)}↦{(1↦A),(2↦B)})}"
+ "{([S]↦[A,B]),([S]↦[B,C]),([A]↦[a]),([A]↦[B,A]),([B]↦[b]),([B]↦[C,C]),([C]↦[a]),([C]↦[A,B])}"
]
},
- "execution_count": 7,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -241,7 +261,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -253,7 +273,7 @@
"(1↦1)"
]
},
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -264,7 +284,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
@@ -273,7 +293,7 @@
"Executed operation: For_k_loop(1,1,{S,A})"
]
},
- "execution_count": 9,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -284,7 +304,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -296,7 +316,7 @@
"(2↦1)"
]
},
- "execution_count": 10,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -307,7 +327,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
@@ -341,7 +361,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 11,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -352,7 +372,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
@@ -361,7 +381,7 @@
"Executed operation: For_k_loop(2,1,{B})"
]
},
- "execution_count": 12,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -372,7 +392,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
@@ -384,7 +404,7 @@
"(3↦1)"
]
},
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -395,7 +415,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
@@ -429,7 +449,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -440,7 +460,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
@@ -452,7 +472,7 @@
"{(1↦0↦{B}),(1↦1↦{S,A}),(2↦0↦{A,C}),(2↦1↦{B}),(3↦0↦{A,C}),(4↦0↦{B}),(5↦0↦{A,C})}"
]
},
- "execution_count": 15,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -463,7 +483,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -472,7 +492,7 @@
"Executed operation: For_k_loop(3,1,{S,C})"
]
},
- "execution_count": 16,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -483,7 +503,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -492,7 +512,7 @@
"Executed operation: For_k_loop(4,1,{S,A})"
]
},
- "execution_count": 17,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -503,7 +523,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
@@ -537,7 +557,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 18,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -548,16 +568,16 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Executed operation: For_k_loop(1,2,{})"
+ "Executed operation: For_k_loop(1,2,[])"
]
},
- "execution_count": 19,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -568,7 +588,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 21,
"metadata": {},
"outputs": [
{
@@ -580,7 +600,7 @@
"(2↦2)"
]
},
- "execution_count": 20,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@@ -591,7 +611,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 22,
"metadata": {},
"outputs": [
{
@@ -620,7 +640,7 @@
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\n",
+ "<td style=\"padding:10px\">[]</td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
@@ -632,7 +652,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 21,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -643,7 +663,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 23,
"metadata": {},
"outputs": [
{
@@ -652,7 +672,7 @@
"Executed operation: For_k_loop(2,2,{B})"
]
},
- "execution_count": 22,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
@@ -663,7 +683,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 24,
"metadata": {},
"outputs": [
{
@@ -672,7 +692,7 @@
"Executed operation: For_k_loop(3,2,{B})"
]
},
- "execution_count": 23,
+ "execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
@@ -683,7 +703,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 25,
"metadata": {},
"outputs": [
{
@@ -712,7 +732,7 @@
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\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",
@@ -724,7 +744,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 24,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
@@ -735,16 +755,16 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 26,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Executed operation: For_k_loop(1,3,{})"
+ "Executed operation: For_k_loop(1,3,[])"
]
},
- "execution_count": 25,
+ "execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
@@ -755,7 +775,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
@@ -784,14 +804,14 @@
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\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",
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\n",
+ "<td style=\"padding:10px\">[]</td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
@@ -803,7 +823,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 26,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -814,7 +834,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
@@ -823,7 +843,7 @@
"Executed operation: For_k_loop(2,3,{S,A,C})"
]
},
- "execution_count": 27,
+ "execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
@@ -834,7 +854,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 29,
"metadata": {},
"outputs": [
{
@@ -863,14 +883,14 @@
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\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",
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\n",
+ "<td style=\"padding:10px\">[]</td>\n",
"<td style=\"padding:10px\">{S,A,C}</td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
@@ -882,7 +902,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 28,
+ "execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
@@ -893,7 +913,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -902,7 +922,7 @@
"Executed operation: For_k_loop(1,4,{S,A,C})"
]
},
- "execution_count": 29,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -913,7 +933,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
@@ -942,14 +962,14 @@
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\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",
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
- "<td style=\"padding:10px\">{}</td>\n",
+ "<td style=\"padding:10px\">[]</td>\n",
"<td style=\"padding:10px\">{S,A,C}</td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
@@ -968,7 +988,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 30,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -979,7 +999,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -991,7 +1011,7 @@
"TRUE"
]
},
- "execution_count": 31,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -1002,7 +1022,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -1011,7 +1031,7 @@
"Executed operation: TRUE <-- Accept()"
]
},
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -1022,7 +1042,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -1034,7 +1054,7 @@
"(1↦5↦5)"
]
},
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/info4/kapitel-3/PDA-Kellerautomaten-Unicode.ipynb b/info4/kapitel-3/PDA-Kellerautomaten-Unicode.ipynb
new file mode 100644
index 0000000..9456b8f
--- /dev/null
+++ b/info4/kapitel-3/PDA-Kellerautomaten-Unicode.ipynb
@@ -0,0 +1,1653 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# PDA (Push Down Automata - Kellerautomaten)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "Ein __(nichtdeterministischer) Kellerautomat__ \n",
+ "(kurz PDA für __push-down automaton__) ist ein $6$-Tupel \n",
+ " $M = (\\Sigma, \\Gamma, Z, \\delta , z_0, \\#)$, 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",
+ "\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": 94,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PDA"
+ ]
+ },
+ "execution_count": 94,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PDA\n",
+ "/* B Modell eines PDA */\n",
+ "SETS\n",
+ " Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand\n",
+ " SYMBOLE={a,b, A, `#`, `λ`} /* BOT = # = Bottom-Symbol im Keller*/\n",
+ "DEFINITIONS\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_PP_SEQUENCES == TRUE\n",
+ "CONSTANTS δ, Σ, Γ\n",
+ "PROPERTIES\n",
+ " Σ = {a,b} // das Eingabe-Alphabet\n",
+ " ∧\n",
+ " Γ = {A,`#`} // das Kelleralphabet\n",
+ " ∧\n",
+ " /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",
+ " δ = { (z0,a,`#`) ↦ (z0,[A,`#`]),\n",
+ " (z0,a,A) ↦ (z0,[A,A]),\n",
+ " (z0,b,A) ↦ (z1,[]),\n",
+ " (z1,`λ`,`#`) ↦ (z1,[]),\n",
+ " (z1,b,A) ↦ (z1,[]) }\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",
+ "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",
+ " γ := [`#`] || // 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,`λ`,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": 95,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 95,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 96,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 96,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 97,
+ "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\">`#`</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": 97,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 98,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,[A,`#`])"
+ ]
+ },
+ "execution_count": 98,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[A,`#`])"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "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\">`#`</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 100,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 101,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(\\mathit{z0}\\mapsto[\\mathit{a},\\mathit{b},\\mathit{b}]\\mapsto[\\mathit{A},`\\exists`])$"
+ ],
+ "text/plain": [
+ "(z0↦[a,b,b]↦[A,`∃`])"
+ ]
+ },
+ "execution_count": 101,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(z,α,γ)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 102,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,[A,A])"
+ ]
+ },
+ "execution_count": 102,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 103,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[A,A])"
+ ]
+ },
+ "execution_count": 103,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 104,
+ "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\">`#`</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 104,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 105,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 105,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 106,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 106,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 107,
+ "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\">`#`</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 107,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 108,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 108,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 109,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z1,[])"
+ ]
+ },
+ "execution_count": 109,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 110,
+ "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\">`#`</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 110,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 111,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(z1,[])"
+ ]
+ },
+ "execution_count": 111,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 112,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(z1,[])"
+ ]
+ },
+ "execution_count": 112,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 113,
+ "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:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 113,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 114,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: δ, Σ, Γ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Akzeptieren()"
+ ]
+ },
+ "execution_count": 114,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 115,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Akzeptieren()"
+ ]
+ },
+ "execution_count": 115,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Akzeptieren"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Das Eingabewort ``aabb`` wurde akzeptiert."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 116,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 8.0.5 (20230430.1635)\n",
+ " -->\n",
+ "<!-- Title: visited_states Pages: 1 -->\n",
+ "<svg width=\"473pt\" height=\"1185pt\"\n",
+ " viewBox=\"0.00 0.00 472.66 1185.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 1181)\">\n",
+ "<title>visited_states</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-1181 468.66,-1181 468.66,4 -4,4\"/>\n",
+ "<!-- root -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"224,-1132.5 268.2,-1165.88 179.8,-1165.88 224,-1132.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-1150.47\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
+ "</g>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"448,-1010.25 0,-1010.25 0,-959.5 448,-959.5 448,-1010.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-994.85\" font-family=\"Times,serif\" font-size=\"12.00\">δ((z0|->a|->A)) = (z0|->[A,A]),δ((z0|->a|->`#`)) = (z0|->[A,`#`]),δ((z0|->b|->A)) = (z1|->[]),</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-980.6\" font-family=\"Times,serif\" font-size=\"12.00\">δ((z1|->b|->A)) = (z1|->[]),δ((z1|->`λ`|->`#`)) = (z1|->[]),Σ = {a,b},</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-966.35\" font-family=\"Times,serif\" font-size=\"12.00\">Γ = {A,`#`}</text>\n",
+ "</g>\n",
+ "<!-- root->0 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>root->0</title>\n",
+ "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M224,-1131.46C224,-1103.41 224,-1054.9 224,-1021.64\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"227.5,-1022 224,-1012 220.5,-1022 227.5,-1022\"/>\n",
+ "<text text-anchor=\"middle\" x=\"281.38\" y=\"-1067.1\" font-family=\"Times,serif\" font-size=\"12.00\">SETUP_CONSTANTS</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"295.75,-837.25 152.25,-837.25 152.25,-800.75 295.75,-800.75 295.75,-837.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-821.85\" font-family=\"Times,serif\" font-size=\"12.00\">z = z0,α(1) = a,α(2) = a,</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-807.6\" font-family=\"Times,serif\" font-size=\"12.00\">α(3) = b,α(4) = b,γ(1) = `#`</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-958.63C224,-929.01 224,-880.02 224,-848.91\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-848.94 224,-838.94 220.5,-848.94 227.5,-848.94\"/>\n",
+ "<text text-anchor=\"middle\" x=\"269.75\" y=\"-894.1\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"296.88,-678.5 151.12,-678.5 151.12,-642 296.88,-642 296.88,-678.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-663.1\" font-family=\"Times,serif\" font-size=\"12.00\">z = z0,α(1) = a,α(2) = b,</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-648.85\" font-family=\"Times,serif\" font-size=\"12.00\">α(3) = b,γ(1) = A,γ(2) = `#`</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-800.02C224,-773.09 224,-722.02 224,-689.91\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-690.02 224,-680.02 220.5,-690.02 227.5,-690.02\"/>\n",
+ "<text text-anchor=\"middle\" x=\"266.75\" y=\"-735.35\" font-family=\"Times,serif\" font-size=\"12.00\">Schritt(z0,[A,`#`])</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"298,-519.75 150,-519.75 150,-483.25 298,-483.25 298,-519.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-504.35\" font-family=\"Times,serif\" font-size=\"12.00\">z = z0,α(1) = b,α(2) = b,</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-490.1\" font-family=\"Times,serif\" font-size=\"12.00\">γ(1) = A,γ(2) = A,γ(3) = `#`</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-641.27C224,-614.34 224,-563.27 224,-531.16\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-531.27 224,-521.27 220.5,-531.27 227.5,-531.27\"/>\n",
+ "<text text-anchor=\"middle\" x=\"264.5\" y=\"-576.6\" font-family=\"Times,serif\" font-size=\"12.00\">Schritt(z0,[A,A])</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"290.5,-361 157.5,-361 157.5,-324.5 290.5,-324.5 290.5,-361\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-345.6\" font-family=\"Times,serif\" font-size=\"12.00\">z = z1,α(1) = b,γ(1) = A,</text>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-331.35\" font-family=\"Times,serif\" font-size=\"12.00\">γ(2) = `#`</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-482.52C224,-455.59 224,-404.52 224,-372.41\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-372.52 224,-362.52 220.5,-372.52 227.5,-372.52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"254\" y=\"-417.85\" font-family=\"Times,serif\" font-size=\"12.00\">Schritt(z1,[])</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>5</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"285.25,-202.25 162.75,-202.25 162.75,-166.25 285.25,-166.25 285.25,-202.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-179.97\" font-family=\"Times,serif\" font-size=\"12.00\">z = z1,α = [],γ(1) = `#`</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-323.8C224,-296.91 224,-245.93 224,-213.87\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-213.99 224,-203.99 220.5,-213.99 227.5,-213.99\"/>\n",
+ "<text text-anchor=\"middle\" x=\"254\" y=\"-259.1\" font-family=\"Times,serif\" font-size=\"12.00\">Schritt(z1,[])</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node8\" class=\"node\">\n",
+ "<title>6</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"294.91,-14.54 294.91,-29.46 253.37,-40 194.63,-40 153.09,-29.46 153.09,-14.54 194.63,-4 253.37,-4 294.91,-14.54\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"298.91,-11.43 298.91,-32.57 253.87,-44 194.13,-44 149.09,-32.57 149.09,-11.43 194.13,0 253.87,0 298.91,-11.43\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224\" y=\"-17.73\" font-family=\"Times,serif\" font-size=\"12.00\">z = z1,α = [],γ = []</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M224,-165.49C224,-139.1 224,-89.09 224,-55.9\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"227.5,-55.93 224,-45.93 220.5,-55.93 227.5,-55.93\"/>\n",
+ "<text text-anchor=\"middle\" x=\"273.5\" y=\"-100.85\" font-family=\"Times,serif\" font-size=\"12.00\">LambdaSchritt(z1,[])</text>\n",
+ "</g>\n",
+ "<!-- 6->6 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>6->6</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M292.01,-35.26C348.29,-40.83 406.91,-36.41 406.91,-22 406.91,-8.52 355.6,-3.78 302.91,-7.79\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"302.67,-4.39 293.01,-8.74 303.28,-11.36 302.67,-4.39\"/>\n",
+ "<text text-anchor=\"middle\" x=\"435.78\" y=\"-17.73\" font-family=\"Times,serif\" font-size=\"12.00\">Akzeptieren</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_space []>"
+ ]
+ },
+ "execution_count": 116,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_space"
+ ]
+ },
+ {
+ "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": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PDA_für_kfG"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PDA_für_kfG\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_PP_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": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|z|x|X|z2|Xs|\n",
+ "|---|---|---|---|---|\n",
+ "|z0|a|a|z0|[]|\n",
+ "|z0|b|b|z0|[]|\n",
+ "|z0|S|S|z0|[]|\n",
+ "|z0|C|C|z0|[]|\n",
+ "|z0|lambda|S|z0|[C]|\n",
+ "|z0|lambda|S|z0|[a,S,b]|\n",
+ "|z0|lambda|C|z0|[a,b]|\n",
+ "|z0|lambda|lambda|z0|[]|\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[C]\n",
+ "z0\tlambda\tS\tz0\t[a,S,b]\n",
+ "z0\tlambda\tC\tz0\t[a,b]\n",
+ "z0\tlambda\tlambda\tz0\t[]\n"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "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": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_für_kfG\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: P, δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(z0,[C])\n",
+ "LambdaSchritt(z0,[a,S,b])"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(z0,[a,S,b])"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt s = [a,S,b]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "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": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_für_kfG\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: P, δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "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": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_für_kfG\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: P, δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(z0,[C])\n",
+ "LambdaSchritt(z0,[a,S,b])"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(z0,[C])"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt s = [C]"
+ ]
+ },
+ {
+ "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\">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": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_für_kfG\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: P, δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "LambdaSchritt(z0,[a,b])"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: LambdaSchritt(z0,[a,b])"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec LambdaSchritt s=[a,b]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "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": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_für_kfG\n",
+ "Sets: Z, SYMBOLE\n",
+ "Constants: P, δ\n",
+ "Variables: z, α, γ\n",
+ "Operations: \n",
+ "Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "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": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 43,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "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": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(z0,[])"
+ ]
+ },
+ "execution_count": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "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": 46,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Akzeptieren()"
+ ]
+ },
+ "execution_count": 47,
+ "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,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
+ {
+ "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
+}
diff --git a/info4/kapitel-3/PDA-Kellerautomaten.ipynb b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
index 27ccb38..9c00fc5 100644
--- a/info4/kapitel-3/PDA-Kellerautomaten.ipynb
+++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
@@ -112,7 +112,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
@@ -132,7 +132,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
@@ -284,7 +284,7 @@
{
"data": {
"text/markdown": [
- "$(\\mathit{z0}\\mapsto [a,\\mathit{b},b]\\mapsto [A,BOT])$"
+ "$(\\mathit{z0}\\mapsto[\\mathit{a},\\mathit{b},\\mathit{b}]\\mapsto[\\mathit{A},\\mathit{BOT}])$"
],
"text/plain": [
"(z0↦[a,b,b]↦[A,BOT])"
@@ -684,6 +684,13 @@
"Das Eingabewort ``aabb`` wurde akzeptiert."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -781,7 +788,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 24,
@@ -801,7 +808,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 25,
@@ -823,14 +830,14 @@
"text/markdown": [
"|z|x|X|z2|Xs|\n",
"|---|---|---|---|---|\n",
- "|$\\mathit{z0}$|$\\mathit{a}$|$\\mathit{a}$|$\\mathit{z0}$|$[]$|\n",
- "|$\\mathit{z0}$|$\\mathit{b}$|$\\mathit{b}$|$\\mathit{z0}$|$[]$|\n",
- "|$\\mathit{z0}$|$\\mathit{S}$|$\\mathit{S}$|$\\mathit{z0}$|$[]$|\n",
- "|$\\mathit{z0}$|$\\mathit{C}$|$\\mathit{C}$|$\\mathit{z0}$|$[]$|\n",
- "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$[C]$|\n",
- "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$[a,\\mathit{S},b]$|\n",
- "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{C}$|$\\mathit{z0}$|$[a,b]$|\n",
- "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{lambda}$|$\\mathit{z0}$|$[]$|\n"
+ "|z0|a|a|z0|[]|\n",
+ "|z0|b|b|z0|[]|\n",
+ "|z0|S|S|z0|[]|\n",
+ "|z0|C|C|z0|[]|\n",
+ "|z0|lambda|S|z0|[C]|\n",
+ "|z0|lambda|S|z0|[a,S,b]|\n",
+ "|z0|lambda|C|z0|[a,b]|\n",
+ "|z0|lambda|lambda|z0|[]|\n"
],
"text/plain": [
"z\tx\tX\tz2\tXs\n",
@@ -1474,6 +1481,13 @@
"Das Wort ``aabb`` wird sowohl von der Grammatik generiert als auch von diesem generierten PDA akzeptiert."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
{
"cell_type": "code",
"execution_count": null,
--
GitLab