diff --git a/info4/kapitel-2/Abschlusseigenschaften.ipynb b/info4/kapitel-2/Abschlusseigenschaften.ipynb
index e2e003d7ab59bb9fda7934075ccc50b3ff37907c..d23c81dd9f218ce4bee2339442d3bd0a871df1f4 100644
--- a/info4/kapitel-2/Abschlusseigenschaften.ipynb
+++ b/info4/kapitel-2/Abschlusseigenschaften.ipynb
@@ -29,7 +29,7 @@
"Zuerst betrachten wir die Vereinigung.\n",
"\n",
"Zu jeder regulären Sprache kann man auch einen NFA angeben.\n",
- "Wenn $M_1=(Σ, Z1, δ1, S1, F1)$ und $M_2=(Σ, Z2, δ2, S2, F2)$ zwei NFAs sind, dann lässt sich ein Vereinigungs-NFA $M=(Σ, Z1 ∪ Z2, δ1∪δ2, S1∪S2, F1∪F2)$ erstellen, so dass $L(M) = L(M_1) ∪ L(M_2)$. Man erhält M, indem man alle Mengen der Tupel von $M_1$ und $M_2$ paarweise vereinigt (analog zum Beweis des Satzes von Kleene Folie 52)."
+ "Wenn $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ und $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ zwei NFAs sind, dann lässt sich ein Vereinigungs-NFA $M=(Σ, Z_1 ∪ Z_2, δ_1∪δ_2, S_1∪S_2, F_1∪F_2)$ erstellen, so dass $L(M) = L(M_1) ∪ L(M_2)$. Man erhält M, indem man alle Mengen der Tupel von $M_1$ und $M_2$ paarweise vereinigt (analog zum Beweis des Satzes von Kleene Folie 52)."
]
},
{
@@ -53,7 +53,7 @@
"MACHINE NFA\n",
"SETS\n",
" Z = {z10,z11,z12,z13, z20,z21,z22}\n",
- "CONSTANTS Σ, M, S, F, δ,\n",
+ "CONSTANTS Σ, M, δ, S, F, \n",
" M1, Z1, δ1, S1, F1,\n",
" M2, Z2, δ2, S2, F2\n",
" \n",
@@ -63,9 +63,9 @@
" ∧\n",
" // Der Automat M1 von Folie 21 (L(M1)={u1v|u∈{0,1}* ∧ v∈{0,1}}):\n",
" M1=(Σ, Z1, δ1, S1, F1) ∧\n",
- " Z1 ⊆ Z ∧ \n",
- " F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧\n",
- " δ1 ∈ (Z1×Σ) → ℙ(Z1)\n",
+ " Z1 ⊆ Z ∧\n",
+ " δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧\n",
+ " S1 ⊆ Z1 ∧ F1 ⊆ Z1\n",
" ∧\n",
" Z1 = {z10,z11,z12,z13} ∧\n",
" S1 = {z10} ∧ F1 = {z12} ∧\n",
@@ -78,8 +78,8 @@
" // Der Automat M2 von Folie 28 (L(M2)={u1|u∈{0,1}*}):\n",
" M2=(Σ, Z2, δ2, S2, F2) ∧\n",
" Z2 ⊆ Z ∧\n",
- " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
- " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
+ " δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧\n",
+ " S2 ⊆ Z2 ∧ F2 ⊆ Z2\n",
" ∧\n",
" Z2 = {z20,z21,z22} ∧\n",
" S2 = {z20} ∧ F2 = {z21} ∧\n",
@@ -110,7 +110,9 @@
{
"cell_type": "code",
"execution_count": 2,
- "metadata": {},
+ "metadata": {
+ "scrolled": true
+ },
"outputs": [
{
"data": {
@@ -127,6 +129,13 @@
":constants"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Hier sieht man auf der linken Seite $M_1$, auf der rechten $M_2$ und das gesamte Bild stellt den Vereinigungsautomaten $M$ dar."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 3,
@@ -289,7 +298,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Eine weitere Eigenschaft, die man leicht zeigen kann ist, dass das Komplement einer Sprache $L$ regulär ist. Sei $M=(Σ, Z, δ, z0, F)$ ein DFA mit $L(M)=L$. Dann gilt für $M'=(Σ, Z, δ, z0, Z/F)$, dass $L(M')= \\overline{L}$. Dies kann man auch mit folgender Machiene darstellen:"
+ "Eine weitere Eigenschaft, die man leicht zeigen kann ist, dass das Komplement einer Sprache $L$ regulär ist. Sei $M=(Σ, Z, δ, z_0, F)$ ein DFA mit $L(M)=L$. Dann gilt für $M_2=(Σ, Z, δ, z_0, Z/F)$, dass $L(M_2)= \\overline{L}$. Dies kann man auch mit folgender Machiene darstellen:"
]
},
{
@@ -315,12 +324,13 @@
" Z = {z0,z1,z2,z3}\n",
"CONSTANTS Σ, M, δ, F, M2, z_start\n",
"PROPERTIES\n",
+ " Σ = {0,1}\n",
+ " ∧\n",
" M = (Σ, Z, δ, z_start, F) ∧\n",
" M2 = (Σ, Z, δ, z_start, Z\\F) ∧\n",
- " z_start ∈ Z ∧\n",
- " F ⊆ Z ∧\n",
" δ ∈ (Z×Σ) → Z ∧\n",
- " Σ = {0,1}\n",
+ " z_start ∈ Z ∧\n",
+ " F ⊆ Z\n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:Z\\F); // Endzustände von M2\n",
" CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:F); // andere Zustände von M2\n",
@@ -364,6 +374,13 @@
" z0, {z0, z2}) //z0, F"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Hier sieht man $M_2$, der aus $M$ erzeugt wurde, indem man alle das Komplement der Endzustandsmenge als neue Endzustandsmenge wählt."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 6,
@@ -495,7 +512,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Als nächstes befassen wir uns mit der Konkatenation zweier Sprachen. Um dies zu erreichen schaltet man 2 NFAs hintereinander."
+ "Als nächstes befassen wir uns mit der Konkatenation zweier Sprachen. Um dies zu erreichen schaltet man 2 NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ hintereinander. Dies erreicht man, indem man jedes Mal, wenn ein Zustand in $F_1$ erreicht wird zusätzlich auch alle Zustände in $S_2$ erreicht werden."
]
},
{
@@ -519,42 +536,43 @@
"MACHINE NFA\n",
"SETS\n",
" Z = {z10,z11, z12, z20,z21,z22}\n",
- "CONSTANTS Σ, S, F, δ,\n",
- " Z1, S1, F1, δ1,\n",
- " Z2, S2, F2, δ2\n",
+ "CONSTANTS Σ, M, δ, S, F, \n",
+ " M1, Z1, δ1, S1, F1, \n",
+ " M2, Z2, δ2, S2, F2\n",
" \n",
"PROPERTIES\n",
- " Σ = {0,1}\n",
- " \n",
+ " Σ = {0,1} ∧\n",
+ " Z1 ∩ Z2 = ∅\n",
" ∧\n",
- " \n",
+ " // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
+ " M1=(Σ, Z1, δ1, S1, F1) ∧\n",
" Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧\n",
- " F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧\n",
- " δ1 ∈ (Z1×Σ) → ℙ(Z1)\n",
+ " δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧\n",
+ " S1 ⊆ Z1 ∧ F1 ⊆ Z1\n",
" ∧\n",
- " // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
" S1 = {z10} ∧ F1 = {z10, z12} ∧\n",
" δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},\n",
" (z11,0)↦{z12}, (z11,1)↦{z11},\n",
" (z12,0)↦{z12}, (z12,1)↦{z11}} ∧\n",
" \n",
" \n",
+ " // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\n",
+ " M2 = (Σ, Z2, δ2, S2, F2) ∧\n",
" Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧\n",
- " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
- " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
+ " δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧\n",
+ " S2 ⊆ Z2 ∧ F2 ⊆ Z2\n",
" ∧\n",
- " // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\n",
- " S2 = {z20} ∧ F2 = {z20, z21} ∧\n",
+ " S2 = {z20} ∧ F2 = {z21} ∧\n",
" δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},\n",
" (z21,0)↦{z22}, (z21,1)↦{z21},\n",
" (z22,0)↦{z22}, (z22,1)↦{z22}} ∧\n",
"\n",
" //Die Regeln von Folie 51:\n",
- " Z1 ∩ Z2 = ∅ ∧\n",
- " Z= Z1 ∪ Z2 ∧\n",
- " S = S1 ∪ ran((S1∩F1)*S2)\n",
- " ∧ F = F2 ∪ ran((S2∩F2)*F1)\n",
- " ∧ δ = {x | x∈(Z*INTEGER)*POW(Z) ∧\n",
+ " M = (Σ, Z, δ, S, F) ∧\n",
+ " Z = Z1 ∪ Z2 ∧\n",
+ " S = S1 ∪ ran((S1∩F1)*S2) ∧\n",
+ " F = F2 ∪ ran((S2∩F2)*F1) ∧\n",
+ " δ = {x | x∈(Z*INTEGER)*POW(Z) ∧\n",
" ∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (\n",
" (zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F1= ∅) ∨\n",
" (zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F1 ≠ ∅) ∨\n",
@@ -605,164 +623,161 @@
"<!-- Generated by graphviz version 2.44.1 (0)\n",
" -->\n",
"<!-- Title: prob_graph Pages: 1 -->\n",
- "<svg width=\"540pt\" height=\"712pt\"\n",
- " viewBox=\"0.00 0.00 540.00 711.78\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
- "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.98 0.98) rotate(0) translate(4 724.81)\">\n",
+ "<svg width=\"540pt\" height=\"714pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 714.39\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.98 0.98) rotate(0) translate(4 724.84)\">\n",
"<title>prob_graph</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724.81 548.92,-724.81 548.92,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724.84 546.92,-724.84 546.92,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>0</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"283.92\" cy=\"-606\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"283.92\" cy=\"-606\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"283.92\" y=\"-602.9\" font-family=\"Times,serif\" font-size=\"12.00\">z10</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"139.12\" cy=\"-146\" rx=\"23.3\" ry=\"23.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"139.12\" cy=\"-146\" rx=\"27.29\" ry=\"27.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.12\" y=\"-142.9\" font-family=\"Times,serif\" font-size=\"12.00\">z21</text>\n",
+ "</g>\n",
+ "<!-- 0->0 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>0->0</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M164.32,-157.12C175.2,-158.03 184.51,-154.32 184.51,-146 184.51,-140.54 180.5,-137.07 174.67,-135.58\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"174.54,-132.07 164.32,-134.88 174.06,-139.05 174.54,-132.07\"/>\n",
+ "<text text-anchor=\"middle\" x=\"188.51\" y=\"-142.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>5</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"303.12\" cy=\"-28\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"303.12\" y=\"-24.9\" font-family=\"Times,serif\" font-size=\"12.00\">z22</text>\n",
+ "</g>\n",
+ "<!-- 0->5 -->\n",
+ "<g id=\"edge13\" class=\"edge\">\n",
+ "<title>0->5</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M161.23,-129.36C190.96,-108.33 243.78,-70.97 275.91,-48.24\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"278.25,-50.88 284.39,-42.25 274.2,-45.16 278.25,-50.88\"/>\n",
+ "<text text-anchor=\"middle\" x=\"235.12\" y=\"-81.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"97.92\" cy=\"-487\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"97.92\" cy=\"-487\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"97.92\" y=\"-483.9\" font-family=\"Times,serif\" font-size=\"12.00\">z12</text>\n",
- "</g>\n",
- "<!-- 0->1 -->\n",
- "<g id=\"edge6\" class=\"edge\">\n",
- "<title>0->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M261.11,-590.65C228.06,-569.86 166.74,-531.29 129.4,-507.8\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"131.24,-504.83 120.91,-502.46 127.51,-510.75 131.24,-504.83\"/>\n",
- "<text text-anchor=\"middle\" x=\"200.92\" y=\"-543.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"147.12\" cy=\"-606\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.12\" y=\"-602.9\" font-family=\"Times,serif\" font-size=\"12.00\">z10</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"179.92\" cy=\"-259\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"179.92\" cy=\"-259\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"179.92\" y=\"-255.9\" font-family=\"Times,serif\" font-size=\"12.00\">z20</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"251.12\" cy=\"-493\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"251.12\" y=\"-489.9\" font-family=\"Times,serif\" font-size=\"12.00\">z11</text>\n",
"</g>\n",
- "<!-- 0->2 -->\n",
- "<g id=\"edge7\" class=\"edge\">\n",
- "<title>0->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M256.44,-603.17C207.48,-598.25 106.15,-580.21 61.92,-514.39 9.6,-436.53 102.9,-331.75 152.24,-284.69\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"154.85,-287.04 159.75,-277.65 150.06,-281.93 154.85,-287.04\"/>\n",
- "<text text-anchor=\"middle\" x=\"57.92\" y=\"-424.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M162.91,-588.14C180.42,-569.45 208.81,-539.16 228.63,-518\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"231.23,-520.34 235.51,-510.65 226.12,-515.56 231.23,-520.34\"/>\n",
+ "<text text-anchor=\"middle\" x=\"210.12\" y=\"-545.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"87.12\" cy=\"-379\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"87.12\" y=\"-375.9\" font-family=\"Times,serif\" font-size=\"12.00\">z12</text>\n",
+ "</g>\n",
+ "<!-- 1->3 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>1->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M141.25,-583.02C130.56,-542.92 107.86,-457.8 95.53,-411.54\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"98.87,-410.5 92.91,-401.74 92.11,-412.31 98.87,-410.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.12\" y=\"-489.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"262.92\" cy=\"-373\" rx=\"23.29\" ry=\"23.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"262.92\" y=\"-369.9\" font-family=\"Times,serif\" font-size=\"12.00\">z11</text>\n",
- "</g>\n",
- "<!-- 0->4 -->\n",
- "<g id=\"edge1\" class=\"edge\">\n",
- "<title>0->4</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M281.51,-578.5C277.64,-535.95 270.06,-452.52 265.87,-406.46\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"269.35,-406.06 264.96,-396.42 262.38,-406.69 269.35,-406.06\"/>\n",
- "<text text-anchor=\"middle\" x=\"279.92\" y=\"-483.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
- "</g>\n",
- "<!-- 1->1 -->\n",
- "<g id=\"edge10\" class=\"edge\">\n",
- "<title>1->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M123.13,-497.74C134,-498.62 143.31,-495.04 143.31,-487 143.31,-481.72 139.3,-478.36 133.47,-476.93\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"133.33,-473.41 123.13,-476.26 132.88,-480.4 133.33,-473.41\"/>\n",
- "<text text-anchor=\"middle\" x=\"147.31\" y=\"-483.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
- "</g>\n",
- "<!-- 1->2 -->\n",
- "<g id=\"edge11\" class=\"edge\">\n",
- "<title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M107.01,-460.95C121.69,-420.48 150.67,-340.61 167.33,-294.69\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"170.67,-295.76 170.79,-285.16 164.09,-293.37 170.67,-295.76\"/>\n",
- "<text text-anchor=\"middle\" x=\"151.92\" y=\"-369.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"303.12\" cy=\"-265\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"303.12\" y=\"-261.9\" font-family=\"Times,serif\" font-size=\"12.00\">z20</text>\n",
"</g>\n",
"<!-- 1->4 -->\n",
- "<g id=\"edge3\" class=\"edge\">\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
"<title>1->4</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M120.17,-470.9C149.92,-450.7 202.65,-414.91 235.03,-392.93\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"237.27,-395.64 243.58,-387.13 233.34,-389.85 237.27,-395.64\"/>\n",
- "<text text-anchor=\"middle\" x=\"194.92\" y=\"-424.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M131.15,-588.47C92.45,-546.38 0.76,-433.04 55.12,-355.61 104.29,-285.56 213.9,-270.03 269.45,-266.75\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"269.68,-270.25 279.49,-266.26 269.33,-263.25 269.68,-270.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"47.12\" y=\"-432.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 3 -->\n",
- "<g id=\"node4\" class=\"node\">\n",
- "<title>3</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"312.92\" cy=\"-141\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"312.92\" cy=\"-141\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"312.92\" y=\"-137.9\" font-family=\"Times,serif\" font-size=\"12.00\">z21</text>\n",
+ "<!-- 2->2 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>2->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M272.41,-503.19C283.03,-504.6 292.51,-501.2 292.51,-493 292.51,-487.62 288.43,-484.3 282.62,-483.06\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"282.5,-479.56 272.41,-482.81 282.32,-486.55 282.5,-479.56\"/>\n",
+ "<text text-anchor=\"middle\" x=\"296.51\" y=\"-489.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 2->3 -->\n",
- "<g id=\"edge4\" class=\"edge\">\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
"<title>2->3</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M200.12,-240.38C222.68,-220.71 259.34,-188.73 284.72,-166.6\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"287.29,-168.99 292.53,-159.78 282.69,-163.72 287.29,-168.99\"/>\n",
- "<text text-anchor=\"middle\" x=\"254.92\" y=\"-196.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M231.98,-478.93C202.97,-459.12 147.73,-421.4 114.48,-398.69\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"116.36,-395.73 106.13,-392.98 112.41,-401.51 116.36,-395.73\"/>\n",
+ "<text text-anchor=\"middle\" x=\"178.12\" y=\"-432.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 5 -->\n",
- "<g id=\"node6\" class=\"node\">\n",
- "<title>5</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"179.92\" cy=\"-27\" rx=\"23.29\" ry=\"23.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"179.92\" y=\"-23.9\" font-family=\"Times,serif\" font-size=\"12.00\">z22</text>\n",
+ "<!-- 2->4 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>2->4</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M256.2,-469.92C265.44,-429.75 285.03,-344.59 295.75,-298.03\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"299.18,-298.7 298.01,-288.17 292.36,-297.13 299.18,-298.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"287.12\" y=\"-375.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 2->5 -->\n",
- "<g id=\"edge12\" class=\"edge\">\n",
- "<title>2->5</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M179.92,-231.17C179.92,-188.82 179.92,-106.62 179.92,-60.82\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"183.42,-60.55 179.92,-50.55 176.42,-60.55 183.42,-60.55\"/>\n",
- "<text text-anchor=\"middle\" x=\"183.92\" y=\"-137.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M109.85,-385.92C134.63,-393.2 174.57,-407.36 203.12,-429.5 215.18,-438.85 225.84,-451.92 234.04,-463.7\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"231.35,-465.98 239.8,-472.36 237.18,-462.1 231.35,-465.98\"/>\n",
+ "<text text-anchor=\"middle\" x=\"220.12\" y=\"-432.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 3->3 -->\n",
- "<g id=\"edge5\" class=\"edge\">\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
"<title>3->3</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M338.13,-151.74C349,-152.62 358.31,-149.04 358.31,-141 358.31,-135.72 354.3,-132.36 348.47,-130.93\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"348.33,-127.41 338.13,-130.26 347.88,-134.4 348.33,-127.41\"/>\n",
- "<text text-anchor=\"middle\" x=\"362.31\" y=\"-137.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
- "</g>\n",
- "<!-- 3->5 -->\n",
- "<g id=\"edge13\" class=\"edge\">\n",
- "<title>3->5</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M292.43,-122.75C269.02,-103.03 230.7,-70.76 205.39,-49.45\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"207.57,-46.71 197.66,-42.94 203.06,-52.06 207.57,-46.71\"/>\n",
- "<text text-anchor=\"middle\" x=\"254.92\" y=\"-77.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M108.41,-389.19C119.03,-390.6 128.51,-387.2 128.51,-379 128.51,-373.62 124.43,-370.3 118.62,-369.06\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"118.5,-365.56 108.41,-368.81 118.32,-372.55 118.5,-365.56\"/>\n",
+ "<text text-anchor=\"middle\" x=\"132.51\" y=\"-375.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 4->1 -->\n",
- "<g id=\"edge8\" class=\"edge\">\n",
- "<title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M248.45,-391.47C237.04,-404.49 220.22,-422.07 202.92,-434.5 181.18,-450.11 153.99,-463.3 132.73,-472.42\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"131.29,-469.23 123.42,-476.32 133.99,-475.69 131.29,-469.23\"/>\n",
- "<text text-anchor=\"middle\" x=\"221.92\" y=\"-424.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge11\" class=\"edge\">\n",
+ "<title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M107.83,-367.26C146.29,-347.32 228.88,-304.49 273.33,-281.44\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"275.2,-284.42 282.47,-276.71 271.98,-278.2 275.2,-284.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"206.12\" y=\"-318.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 4->2 -->\n",
- "<g id=\"edge9\" class=\"edge\">\n",
- "<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M249.21,-353.51C236.4,-336.22 217.05,-310.1 202.05,-289.86\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"204.69,-287.54 195.92,-281.59 199.06,-291.71 204.69,-287.54\"/>\n",
- "<text text-anchor=\"middle\" x=\"230.92\" y=\"-315.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<!-- 4->0 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>4->0</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M284.3,-250.58C256.27,-230.58 203.23,-192.74 169.6,-168.75\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"171.26,-165.63 161.09,-162.67 167.2,-171.33 171.26,-165.63\"/>\n",
+ "<text text-anchor=\"middle\" x=\"235.12\" y=\"-204.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
- "<!-- 4->4 -->\n",
- "<g id=\"edge2\" class=\"edge\">\n",
- "<title>4->4</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M284.22,-382.83C294.84,-384.19 304.31,-380.91 304.31,-373 304.31,-367.81 300.23,-364.61 294.42,-363.42\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"294.3,-359.91 284.22,-363.17 294.13,-366.91 294.3,-359.91\"/>\n",
- "<text text-anchor=\"middle\" x=\"308.31\" y=\"-369.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge12\" class=\"edge\">\n",
+ "<title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M303.12,-241.47C303.12,-199.71 303.12,-110.15 303.12,-61.71\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"306.62,-61.46 303.12,-51.46 299.62,-61.46 306.62,-61.46\"/>\n",
+ "<text text-anchor=\"middle\" x=\"307.12\" y=\"-142.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 5->5 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>5->5</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M201.22,-36.83C211.84,-38.19 221.31,-34.91 221.31,-27 221.31,-21.81 217.23,-18.61 211.42,-17.42\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"211.3,-13.91 201.22,-17.17 211.13,-20.91 211.3,-13.91\"/>\n",
- "<text text-anchor=\"middle\" x=\"232.81\" y=\"-23.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M324.41,-38.19C335.03,-39.6 344.51,-36.2 344.51,-28 344.51,-22.62 340.43,-19.3 334.62,-18.06\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"334.5,-14.56 324.41,-17.81 334.32,-21.55 334.5,-14.56\"/>\n",
+ "<text text-anchor=\"middle\" x=\"356.01\" y=\"-24.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>6</title>\n",
"</g>\n",
- "<!-- 6->0 -->\n",
+ "<!-- 6->1 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
- "<title>6->0</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M417.61,-683.39C389.56,-667.36 345.91,-642.43 316.18,-625.43\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"317.85,-622.36 307.43,-620.44 314.38,-628.44 317.85,-622.36\"/>\n",
+ "<title>6->1</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M364.96,-687.91C319.25,-670.94 227.18,-636.74 178.67,-618.72\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"179.61,-615.33 169.01,-615.13 177.17,-621.9 179.61,-615.33\"/>\n",
"</g>\n",
- "<!-- 6->2 -->\n",
+ "<!-- 6->4 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
- "<title>6->2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M471.98,-688.03C501.6,-674.03 544.92,-646.75 544.92,-607 544.92,-607 544.92,-607 544.92,-372 544.92,-304.03 310.64,-273.08 217.48,-263.46\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"217.65,-259.96 207.35,-262.44 216.95,-266.93 217.65,-259.96\"/>\n",
+ "<title>6->4</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M419.24,-693.7C461.46,-685.3 538.12,-662.4 538.12,-607 538.12,-607 538.12,-607 538.12,-378 538.12,-289.81 401.57,-270.99 336.65,-267.03\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"336.68,-263.52 326.51,-266.49 336.31,-270.51 336.68,-263.52\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -784,7 +799,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Um zu zeigen, dass die Iteration einer regulären Sprache wieder regulär ist, bilden wir zu einem NFA den Rückkopplungsautomaten. "
+ "Um zu zeigen, dass die Iteration einer regulären Sprache wieder regulär ist, bilden wir zu einem NFA $M=(Σ, Z_1, δ_1, S_1, F_1)$ einen Rückkopplungsautomaten $M_2$. Wir starten damit den $M$ mit sich selbst zu verketten (analog zur Konkatenation). Dann müssen wir nur noch sichergehen, dass das leere Wort akzeptiert wird. Dafür fügen wir (falls notwendig) einen Zustand ein, der sowohl Start- als auch Endzustand ist."
]
},
{
@@ -808,46 +823,42 @@
"MACHINE NFA\n",
"SETS\n",
" Z = {z10,z11, z12, z}\n",
- "CONSTANTS M1, M2, M,\n",
- " Σ, δ,\n",
- " Z1, S1, F1, δ1,\n",
- " Z2, S2, F2, δ2\n",
+ "CONSTANTS Σ, M, δ, \n",
+ " M1, Z1, δ1, S1, F1,\n",
+ " M2, Z2, δ2, S2, F2\n",
" \n",
"PROPERTIES\n",
" Σ = {0,1}\n",
- " \n",
" ∧\n",
- " \n",
- " M1 = (Σ, Z1, δ1, S1, F1)∧\n",
+ " // Der Automat M1 (L(M1)={w| w=u0 mit u∈{0,1}*}):\n",
+ " M1 = (Σ, Z1, δ1, S1, F1) ∧\n",
" Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧\n",
- " F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧\n",
- " δ1 ∈ (Z1×Σ) → ℙ(Z1)\n",
+ " δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧\n",
+ " S1 ⊆ Z1 ∧ F1 ⊆ Z1\n",
" ∧\n",
- " // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
- " S1 = {z10} ∧ F1 = {z10, z12} ∧\n",
+ " S1 = {z10} ∧ F1 = {z12} ∧\n",
" δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},\n",
" (z11,0)↦{z12}, (z11,1)↦{z11},\n",
" (z12,0)↦{z12}, (z12,1)↦{z11}} ∧\n",
" \n",
- " \n",
+ " //Die Regeln von Folie 53\n",
+ " M2 = (Σ, Z2, δ2, S2, F2) ∧\n",
" Z2 ⊆ Z ∧\n",
- " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
- " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
+ " δ2 ∈ (Z2×Σ) +-> ℙ(Z2) ∧\n",
+ " S2 ⊆ Z2 ∧ F2 ⊆ Z2\n",
" ∧\n",
- " \n",
- " //Die Regeln von Folie 53\n",
" Z2 = IF S1∩F1 ≠ ∅ THEN Z1 ELSE Z1∪{z} END ∧\n",
+ " δ2 = δ1 ∧\n",
" S2 = IF S1∩F1 ≠ ∅ THEN S1 ELSE S1∪{z} END ∧\n",
" F2 = IF S1∩F1 ≠ ∅ THEN F1 ELSE F1∪{z} END ∧\n",
- " M2 = (Σ, Z2, δ1, S2, F2) ∧\n",
+ " \n",
" \n",
" //Die Regeln von Folie 54:\n",
- " δ = {x | x:(Z*INTEGER)*POW(Z) ∧\n",
+ " M = (Σ, Z2, δ, S2, F2) ∧\n",
+ " δ = {x | x∈(Z*INTEGER)*POW(Z) ∧\n",
" ∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (\n",
- " (zustand∈Z2 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F2= ∅) ∨\n",
- " (zustand∈Z2 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F2 ≠ ∅)))} ∧\n",
- "\n",
- " M = (Σ, Z2, δ, S2, F2)\n",
+ " (zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∧ δ2(zustand,symbol)∩F2= ∅) ∨\n",
+ " (zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∪ S2 ∧ δ2(zustand,symbol)∩F2 ≠ ∅)))}\n",
" \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F2); // Endzustände\n",
@@ -894,103 +905,136 @@
"<!-- Generated by graphviz version 2.44.1 (0)\n",
" -->\n",
"<!-- Title: prob_graph Pages: 1 -->\n",
- "<svg width=\"540pt\" height=\"715pt\"\n",
- " viewBox=\"0.00 0.00 540.00 714.53\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
- "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.98 0.98) rotate(0) translate(4 724.78)\">\n",
+ "<svg width=\"540pt\" height=\"716pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 716.39\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.98 0.98) rotate(0) translate(4 724.75)\">\n",
"<title>prob_graph</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724.78 546.77,-724.78 546.77,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724.75 545.32,-724.75 545.32,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>0</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"354.33\" cy=\"-500\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"354.33\" cy=\"-500\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"354.33\" y=\"-496.9\" font-family=\"Times,serif\" font-size=\"12.00\">z10</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"92.12\" cy=\"-663\" rx=\"23.3\" ry=\"23.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"92.12\" cy=\"-663\" rx=\"27.29\" ry=\"27.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"92.12\" y=\"-659.9\" font-family=\"Times,serif\" font-size=\"12.00\">z12</text>\n",
"</g>\n",
"<!-- 0->0 -->\n",
- "<g id=\"edge4\" class=\"edge\">\n",
+ "<g id=\"edge11\" class=\"edge\">\n",
"<title>0->0</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M375.34,-517.58C387.9,-521.48 399.72,-515.62 399.72,-500 399.72,-488.77 393.61,-482.58 385.51,-481.44\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"384.96,-477.98 375.34,-482.42 385.63,-484.95 384.96,-477.98\"/>\n",
- "<text text-anchor=\"middle\" x=\"403.72\" y=\"-496.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M112.19,-681.99C125.09,-686.95 137.51,-680.62 137.51,-663 137.51,-650.06 130.81,-643.21 122.14,-642.45\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"121.52,-639 112.19,-644.01 122.61,-645.92 121.52,-639\"/>\n",
+ "<text text-anchor=\"middle\" x=\"141.51\" y=\"-659.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"96.33\" cy=\"-271\" rx=\"23.3\" ry=\"23.3\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"96.33\" cy=\"-271\" rx=\"27.29\" ry=\"27.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"96.33\" y=\"-267.9\" font-family=\"Times,serif\" font-size=\"12.00\">z12</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"293.12\" cy=\"-47\" rx=\"18\" ry=\"18\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"293.12\" cy=\"-47\" rx=\"22\" ry=\"22\"/>\n",
+ "<text text-anchor=\"middle\" x=\"293.12\" y=\"-43.9\" font-family=\"Times,serif\" font-size=\"12.00\">z</text>\n",
"</g>\n",
"<!-- 0->1 -->\n",
- "<g id=\"edge5\" class=\"edge\">\n",
+ "<g id=\"edge12\" class=\"edge\">\n",
"<title>0->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M334.08,-481.19C288.21,-440.83 176.28,-342.34 124.03,-296.38\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"126.3,-293.71 116.48,-289.73 121.67,-298.96 126.3,-293.71\"/>\n",
- "<text text-anchor=\"middle\" x=\"229.33\" y=\"-381.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M82.3,-637.15C56.37,-567.27 -7.13,-364.91 66.12,-223.61 109.52,-139.87 212.86,-83.95 263.76,-60.5\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"265.24,-63.67 272.92,-56.37 262.36,-57.29 265.24,-63.67\"/>\n",
+ "<text text-anchor=\"middle\" x=\"38.12\" y=\"-345.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"336.33\" cy=\"-52\" rx=\"23.29\" ry=\"23.29\"/>\n",
- "<text text-anchor=\"middle\" x=\"336.33\" y=\"-48.9\" font-family=\"Times,serif\" font-size=\"12.00\">z11</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"283.12\" cy=\"-451\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"283.12\" y=\"-447.9\" font-family=\"Times,serif\" font-size=\"12.00\">z10</text>\n",
"</g>\n",
"<!-- 0->2 -->\n",
- "<g id=\"edge1\" class=\"edge\">\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
"<title>0->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M353.25,-472.44C350.13,-395.11 341.06,-170.27 337.64,-85.68\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"341.14,-85.48 337.24,-75.62 334.15,-85.76 341.14,-85.48\"/>\n",
- "<text text-anchor=\"middle\" x=\"350.33\" y=\"-267.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
- "</g>\n",
- "<!-- 1->0 -->\n",
- "<g id=\"edge8\" class=\"edge\">\n",
- "<title>1->0</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M118.64,-287.25C147.14,-307.08 197.55,-343.37 237.33,-378.5 271.05,-408.29 306.62,-445.94 329.57,-471.16\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"327.25,-473.82 336.56,-478.89 332.44,-469.12 327.25,-473.82\"/>\n",
- "<text text-anchor=\"middle\" x=\"255.33\" y=\"-381.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M113.08,-645.23C136.91,-625.68 176.35,-591.77 206.12,-558.5 228.45,-533.54 250.48,-502.19 265.22,-479.99\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"268.32,-481.65 270.88,-471.37 262.47,-477.81 268.32,-481.65\"/>\n",
+ "<text text-anchor=\"middle\" x=\"220.12\" y=\"-548.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 1->1 -->\n",
- "<g id=\"edge9\" class=\"edge\">\n",
- "<title>1->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M115.92,-290.49C128.99,-295.98 141.72,-289.48 141.72,-271 141.72,-257.28 134.71,-250.17 125.75,-249.66\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"125.1,-246.22 115.92,-251.51 126.4,-253.09 125.1,-246.22\"/>\n",
- "<text text-anchor=\"middle\" x=\"145.72\" y=\"-267.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"98.12\" cy=\"-247\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"98.12\" y=\"-243.9\" font-family=\"Times,serif\" font-size=\"12.00\">z11</text>\n",
"</g>\n",
- "<!-- 1->2 -->\n",
+ "<!-- 0->3 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
- "<title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M116.38,-251.87C160.15,-212.3 264.14,-118.27 311.76,-75.22\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"314.36,-77.58 319.43,-68.28 309.67,-72.39 314.36,-77.58\"/>\n",
- "<text text-anchor=\"middle\" x=\"228.33\" y=\"-153.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<title>0->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M85.11,-636.4C74.18,-593.37 55.02,-503.79 62.12,-427.61 65.69,-389.29 70.58,-380.24 78.12,-342.5 82.28,-321.65 87.23,-298.26 91.16,-279.97\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"94.6,-280.63 93.29,-270.12 87.76,-279.16 94.6,-280.63\"/>\n",
+ "<text text-anchor=\"middle\" x=\"66.12\" y=\"-447.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 2->0 -->\n",
- "<g id=\"edge6\" class=\"edge\">\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
"<title>2->0</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M341.6,-74.92C346.08,-94.58 352.27,-124.29 355.33,-150.5 367.73,-256.97 369.3,-284.43 364.33,-391.5 363.23,-415.21 360.77,-441.76 358.56,-462.54\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"355.08,-462.22 357.48,-472.54 362.04,-462.98 355.08,-462.22\"/>\n",
- "<text text-anchor=\"middle\" x=\"370.33\" y=\"-267.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M267.76,-468.89C234.78,-505.15 156.93,-590.74 116.87,-634.78\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"114.23,-632.49 110.09,-642.24 119.4,-637.2 114.23,-632.49\"/>\n",
+ "<text text-anchor=\"middle\" x=\"198.12\" y=\"-548.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
- "<g id=\"edge7\" class=\"edge\">\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M322,-70.77C303.37,-93.41 269.3,-133.23 236.33,-163.5 201.06,-195.88 156.48,-228.55 127.22,-249\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"124.88,-246.37 118.66,-254.94 128.87,-252.12 124.88,-246.37\"/>\n",
- "<text text-anchor=\"middle\" x=\"252.33\" y=\"-153.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M283.68,-427.53C285.36,-359.78 290.4,-157.41 292.34,-79.27\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"295.84,-79.18 292.59,-69.1 288.84,-79 295.84,-79.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"293.12\" y=\"-243.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 2->2 -->\n",
- "<g id=\"edge2\" class=\"edge\">\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
"<title>2->2</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M352.47,-68.98C364.97,-75.33 377.72,-69.67 377.72,-52 377.72,-39.02 370.84,-32.52 362.24,-32.5\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"361.28,-29.13 352.47,-35.02 363.03,-35.91 361.28,-29.13\"/>\n",
- "<text text-anchor=\"middle\" x=\"381.72\" y=\"-48.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M299.69,-467.53C312.05,-473.31 324.51,-467.8 324.51,-451 324.51,-438.8 317.93,-432.55 309.6,-432.26\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"308.69,-428.88 299.69,-434.47 310.21,-435.71 308.69,-428.88\"/>\n",
+ "<text text-anchor=\"middle\" x=\"328.51\" y=\"-447.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
- "<!-- 3 -->\n",
- "<g id=\"node4\" class=\"node\">\n",
- "<title>3</title>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M267.66,-433.13C234.95,-397.4 158.59,-314.03 120.52,-272.46\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"122.99,-269.98 113.66,-264.97 117.83,-274.71 122.99,-269.98\"/>\n",
+ "<text text-anchor=\"middle\" x=\"201.12\" y=\"-345.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 3->0 -->\n",
- "<g id=\"edge10\" class=\"edge\">\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
"<title>3->0</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M354.33,-662.84C354.33,-634.2 354.33,-576.06 354.33,-537.83\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"357.83,-537.61 354.33,-527.61 350.83,-537.61 357.83,-537.61\"/>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M97.79,-270.69C96.8,-338.78 93.86,-541.83 92.65,-625.42\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"89.15,-625.42 92.5,-635.47 96.15,-625.52 89.15,-625.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"100.12\" y=\"-447.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M114.07,-229.8C148.7,-194.64 230.79,-111.29 270.64,-70.82\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"273.5,-72.91 278.02,-63.33 268.51,-68 273.5,-72.91\"/>\n",
+ "<text text-anchor=\"middle\" x=\"206.12\" y=\"-141.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "</g>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M116.71,-261.41C139.87,-278.63 179.95,-310.18 209.12,-342.5 231.4,-367.19 252.46,-398.9 266.37,-421.47\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"263.51,-423.51 271.7,-430.24 269.49,-419.88 263.51,-423.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"223.12\" y=\"-345.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>3->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M114.69,-263.87C127.05,-269.75 139.51,-264.13 139.51,-247 139.51,-234.55 132.93,-228.18 124.6,-227.89\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"123.67,-224.51 114.69,-230.13 125.22,-231.33 123.67,-224.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"143.51\" y=\"-243.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "</g>\n",
+ "<!-- 4->1 -->\n",
+ "<g id=\"edge14\" class=\"edge\">\n",
+ "<title>4->1</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M446.73,-644.94C425.02,-560.6 329.13,-187.93 300.94,-78.38\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"304.31,-77.43 298.42,-68.62 297.53,-79.18 304.31,-77.43\"/>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge13\" class=\"edge\">\n",
+ "<title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M437.37,-644.81C407.85,-607.91 338.26,-520.93 303.55,-477.54\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"306.27,-475.34 297.29,-469.72 300.81,-479.71 306.27,-475.34\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -1012,8 +1056,8 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Im folgenden schauen wir uns die Differenz zweier Sprachen L1-L2 genauer an.\n",
- "Das Vorgehen ist hierbei, dass man zwei NFAs parallel ausführt und die Endzustandsmenge so wählt, dass man in einem Endzustand des ersten, aber nicht des zweiten NFAs landet."
+ "Im folgenden schauen wir uns die Differenz zweier Sprachen $L1-L2$ genauer an.\n",
+ "Das Vorgehen ist hierbei, dass man zwei NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ parallel ausführt und die Endzustandsmenge so wählt, dass man in einem Zustand aus $F_1$, aber nicht gleichzeitig in einem aus $F_2$ landet."
]
},
{
@@ -1037,51 +1081,53 @@
"MACHINE NFA\n",
"SETS\n",
" Z = {z10,z11, z12, z20,z21,z22}\n",
- "CONSTANTS Σ, Z_gesamt, S, F, δ, f,\n",
- " Z1, S1, F1, δ1,\n",
- " Z2, S2, F2, δ2\n",
+ "CONSTANTS Σ, M, Z_gesamt, δ, S, F, f,\n",
+ " M1, Z1, δ1, S1, F1,\n",
+ " M2, Z2, δ2, S2, F2\n",
" \n",
"PROPERTIES\n",
- " Σ = {0,1}\n",
- " \n",
- " ∧\n",
- " \n",
- " Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧\n",
- " F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧\n",
- " δ1 ∈ (Z1×Σ) → ℙ(Z1)\n",
+ " Σ = {0,1} ∧\n",
+ " Z1 ∩ Z2 = ∅ ∧\n",
+ " Z= Z1 ∪ Z2\n",
+ "\n",
" ∧\n",
" // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
+ " M1 = (Σ, Z1, δ1, S1, F1) ∧\n",
+ " Z1 ⊆ Z ∧\n",
+ " δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧\n",
+ " S1 ⊆ Z1 ∧ F1 ⊆ Z1\n",
+ " ∧\n",
+ " Z1 = {z10,z11,z12} ∧\n",
" S1 = {z10} ∧ F1 = {z10, z12} ∧\n",
" δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},\n",
" (z11,0)↦{z12}, (z11,1)↦{z11},\n",
" (z12,0)↦{z12}, (z12,1)↦{z11}} ∧\n",
" \n",
- " \n",
- " Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧\n",
- " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
- " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
- " ∧\n",
" // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\n",
+ " M2 = (Σ, Z2, δ2, S2, F2) ∧\n",
+ " Z2 ⊆ Z ∧\n",
+ " δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧\n",
+ " S2 ⊆ Z2 ∧ F2 ⊆ Z2\n",
+ " ∧\n",
+ " Z2 = {z20,z21,z22} ∧\n",
" S2 = {z20, z21} ∧ F2 = {z20, z21} ∧\n",
" δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},\n",
" (z21,0)↦{z22}, (z21,1)↦{z21},\n",
" (z22,0)↦{z22}, (z22,1)↦{z22}} ∧\n",
"\n",
" //TODO Referenz auf Buch einbauen!\n",
- " Z1 ∩ Z2 = ∅ ∧\n",
- " Z= Z1 ∪ Z2 ∧\n",
- " Z_gesamt = {x | ∃a,b.(a∈Z1 ∧ b∈Z2 ∧ x=(a, b))}∧\n",
+ " M = (Σ, Z, δ, S, F) ∧\n",
+ " Z_gesamt = Z1*Z2 ∧\n",
" S = S1*S2 ∧\n",
" F = F1*(Z2\\F2) ∧\n",
- " δ = {x | x∈((Z*Z)*INTEGER)*POW(Z_gesamt) ∧\n",
+ " δ = {x | x∈((Z1*Z2)*Σ)*ℙ(Z_gesamt) ∧\n",
" ∃zustand1,zustand2,symbol,menge.(\n",
" x=((zustand1, zustand2), symbol)↦menge ∧\n",
" zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧\n",
- " menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))}\n",
- " \n",
- " ∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt\n",
+ " menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))} ∧\n",
" \n",
- " \n",
+ " //Eine Hilfsfunktion zur Visualisierung\n",
+ " f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)};\n",
" ANIMATION_FUNCTION2 == {(0,0,\"Zustand\"),(0,1,\"δ(Zustand,0)\"),(0,2,\"δ(Zustand,1)\")};\n",
@@ -1208,7 +1254,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Indem man die Endzustände so wählt, dass man in einem Enzustand beider NFAs landet, kann man auch zeigen, dass der Schnitt zweier regulärer Sprachen regulär ist."
+ "Indem man die Endzustände in der obigen Konstruktion so wählt, dass man in einem Zustand in $F_1$ und $F_2$ landet, kann man auch zeigen, dass der Schnitt zweier regulärer Sprachen regulär ist."
]
},
{
@@ -1232,51 +1278,52 @@
"MACHINE NFA\n",
"SETS\n",
" Z = {z10,z11, z12, z20,z21,z22}\n",
- "CONSTANTS Σ, Z_gesamt, S, F, δ, f,\n",
- " Z1, S1, F1, δ1,\n",
- " Z2, S2, F2, δ2\n",
+ "CONSTANTS Σ, M, Z_gesamt, δ, S, F, f,\n",
+ " M1, Z1, δ1, S1, F1,\n",
+ " M2, Z2, δ2, S2, F2\n",
" \n",
"PROPERTIES\n",
- " Σ = {0,1}\n",
+ " Σ = {0,1}∧\n",
+ " Z1 ∩ Z2 = ∅ ∧\n",
+ " Z= Z1 ∪ Z2\n",
" \n",
" ∧\n",
- " \n",
+ " // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
+ " M1 = (Σ, Z1, δ1, S1, F1) ∧\n",
" Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧\n",
" F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧\n",
" δ1 ∈ (Z1×Σ) → ℙ(Z1)\n",
" ∧\n",
- " // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):\n",
" S1 = {z10} ∧ F1 = {z10, z12} ∧\n",
" δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},\n",
" (z11,0)↦{z12}, (z11,1)↦{z11},\n",
" (z12,0)↦{z12}, (z12,1)↦{z11}} ∧\n",
- " \n",
- " \n",
- " Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧\n",
- " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
- " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
- " ∧\n",
+ "\n",
" // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\n",
+ " M2 = (Σ, Z2, δ2, S2, F2) ∧\n",
+ " Z2 ⊆ Z ∧\n",
+ " δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧\n",
+ " S2 ⊆ Z2 ∧ F2 ⊆ Z2 \n",
+ " ∧\n",
+ " Z2 = {z20,z21,z22} ∧\n",
" S2 = {z20, z21} ∧ F2 = {z20, z21} ∧\n",
" δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},\n",
" (z21,0)↦{z22}, (z21,1)↦{z21},\n",
" (z22,0)↦{z22}, (z22,1)↦{z22}} ∧\n",
"\n",
" //Konstruktion analog zu TODO Referenz auf Buch\n",
- " Z1 ∩ Z2 = ∅ ∧\n",
- " Z= Z1 ∪ Z2 ∧\n",
- " Z_gesamt = {x | ∃a,b.(a∈Z1 ∧ b∈Z2 ∧ x=(a, b))}∧\n",
+ " M = (Σ, Z_gesamt, δ, S, F) ∧\n",
+ " Z_gesamt = Z1*Z2 ∧\n",
" S = S1*S2 ∧\n",
" F = F1*F2 ∧\n",
- " δ = {x | x∈((Z*Z)*INTEGER)*POW(Z_gesamt) ∧\n",
+ " δ = {x | x∈((Z*Z)*Σ)*ℙ(Z_gesamt) ∧\n",
" ∃zustand1,zustand2,symbol,menge.(\n",
" x=((zustand1, zustand2), symbol)↦menge ∧\n",
" zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧\n",
" menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))}\n",
" \n",
- " ∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt\n",
- " \n",
- " \n",
+ " //Eine Hilfsfunktion zur Visualisierung\n",
+ " ∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" \"LibraryStrings.def\";\n",
" ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)};\n",
@@ -1430,14 +1477,17 @@
" Z = {z0,z1,z2,z3}\n",
"CONSTANTS Σ, M, δ, δ2, F, M2, z_start\n",
"PROPERTIES\n",
+ " Σ = {0,1}\n",
+ " ∧\n",
" M = (Σ, Z, δ, z_start, F) ∧\n",
- " M2 = (Σ, Z, δ2, F, {z_start}) ∧\n",
+ " δ ∈ (Z×Σ) → Z ∧\n",
" z_start ∈ Z ∧\n",
" F ⊆ Z ∧\n",
- " δ ∈ (Z×Σ) → Z ∧\n",
+ " \n",
+ " M2 = (Σ, Z, δ2, F, {z_start}) ∧\n",
" δ2 ∈ (Z×Σ) <-> ℙ(Z) ∧\n",
- " δ2 = {x |∃a,s,s2.(x=(s2, a, {s}) ∧ a∈Σ ∧ s∈Z ∧ s2∈Z ∧ δ(s,a) = s2)} ∧\n",
- " Σ = {0,1}\n",
+ " δ2 = {x |∃a,s,s2.(x=((s2, a)↦{s}) ∧ a∈Σ ∧ s∈Z ∧ s2∈Z ∧ δ(s,a) = s2)}\n",
+ " \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{z_start}); // Endzustände\n",
" CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\{z_start}); // andere Zustände\n",
@@ -1592,75 +1642,6 @@
"source": [
":dot custom_graph"
]
- },
- {
- "cell_type": "code",
- "execution_count": 24,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{z1}\\mapsto 0\\mapsto\\{\\mathit{z0}\\}),(\\mathit{z2}\\mapsto 0\\mapsto\\{\\mathit{z2}\\}),(\\mathit{z2}\\mapsto 1\\mapsto\\{\\mathit{z1}\\}),(\\mathit{z2}\\mapsto 1\\mapsto\\{\\mathit{z2}\\}),(\\mathit{z3}\\mapsto 0\\mapsto\\{\\mathit{z1}\\}),(\\mathit{z3}\\mapsto 0\\mapsto\\{\\mathit{z3}\\}),(\\mathit{z3}\\mapsto 1\\mapsto\\{\\mathit{z0}\\}),(\\mathit{z3}\\mapsto 1\\mapsto\\{\\mathit{z3}\\})\\}$"
- ],
- "text/plain": [
- "{(z1↦0↦{z0}),(z2↦0↦{z2}),(z2↦1↦{z1}),(z2↦1↦{z2}),(z3↦0↦{z1}),(z3↦0↦{z3}),(z3↦1↦{z0}),(z3↦1↦{z3})}"
- ]
- },
- "execution_count": 24,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "δ2"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 25,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{z1}\\mapsto \\mathit{z0}),(\\mathit{z3}\\mapsto \\mathit{z1})\\}$"
- ],
- "text/plain": [
- "{(z1↦z0),(z3↦z1)}"
- ]
- },
- "execution_count": 25,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z:y)}"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 26,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{\\{\\mathit{z0}\\}\\}$"
- ],
- "text/plain": [
- "{{z0}}"
- ]
- },
- "execution_count": 26,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "δ2[{(z1,0)}]"
- ]
}
],
"metadata": {