diff --git a/info4/kapitel-2/Abschlusseigenschaften.ipynb b/info4/kapitel-2/Abschlusseigenschaften.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..e2e003d7ab59bb9fda7934075ccc50b3ff37907c
--- /dev/null
+++ b/info4/kapitel-2/Abschlusseigenschaften.ipynb
@@ -0,0 +1,1681 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Abschlusseigenschaften regulärer Sprachen\n",
+ "\n",
+ "Abschlusseigenschaften sind ein weiteres nützliches Werkzeug um verschiedene Sprachklassen zu charakterisieren.\n",
+ "Damit kann man untersuchen, ob eine Sprache zu einer Sprachklasse gehört oder nicht.\n",
+ "\n",
+ "Die regulären Sprachen sind abgeschlossen unter:\n",
+ "* Vereinigung A ∪ B\n",
+ "* Komplement A̅\n",
+ "* Schnitt A ∩ B\n",
+ "* Differenz A/B\n",
+ "* Konkatenation AB\n",
+ "* Iteration A*\n",
+ "* Spiegelung sp(A)\n",
+ "\n",
+ "In den Folien wird diese Aussage zwar aufgestellt, aber nicht bewiesen.\n",
+ "Hier schauen wir uns für einige Operationen Beweisideen an konkreten Beispielen an."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "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)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE NFA\n",
+ "SETS\n",
+ " Z = {z10,z11,z12,z13, z20,z21,z22}\n",
+ "CONSTANTS Σ, M, S, F, δ,\n",
+ " M1, Z1, δ1, S1, F1,\n",
+ " M2, Z2, δ2, S2, F2\n",
+ " \n",
+ "PROPERTIES\n",
+ " Σ = {0,1} ∧\n",
+ " Z1 ∩ Z2 = ∅\n",
+ " ∧\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",
+ " ∧\n",
+ " Z1 = {z10,z11,z12,z13} ∧\n",
+ " S1 = {z10} ∧ F1 = {z12} ∧\n",
+ " δ1 = { (z10,0)↦{z10}, (z10,1)↦{z10,z11},\n",
+ " (z11,0)↦{z12}, (z11,1)↦{z12},\n",
+ " (z12,0)↦{z13}, (z12,1)↦{z13},\n",
+ " (z13,0)↦{z13}, (z13,1)↦{z13} }\n",
+ " \n",
+ " ∧\n",
+ " // 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",
+ " ∧\n",
+ " Z2 = {z20,z21,z22} ∧\n",
+ " S2 = {z20} ∧ F2 = {z21} ∧\n",
+ " δ2 = { (z20,0)↦{z20}, (z20,1)↦{z20,z21},\n",
+ " (z21,0)↦{z22}, (z21,1)↦{z22},\n",
+ " (z22,0)↦{z22}, (z22,1)↦{z22}}\n",
+ " \n",
+ " ∧\n",
+ " //Der Vereinigungsautomat M:\n",
+ " M=(Σ, Z, δ, S, F) ∧\n",
+ " Z= Z1 ∪ Z2 ∧\n",
+ " δ = δ1 ∪ δ2 ∧\n",
+ " S = S1 ∪ S2 ∧\n",
+ " F = F1 ∪ F2\n",
+ " \n",
+ " \n",
+ "DEFINITIONS // Für den Zustandsgraphen:\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|y∈δ(x,0) ∧ y∈δ(x,1)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*S) // Kanten für Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "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 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.80\" 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.24)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-724.24 546.15,-724.24 546.15,4 -4,4\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"74.9\" cy=\"-210\" rx=\"23.3\" ry=\"23.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"74.9\" cy=\"-210\" rx=\"27.29\" ry=\"27.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74.9\" y=\"-206.9\" font-family=\"Times,serif\" font-size=\"12.00\">z12</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"74.9\" cy=\"-40\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74.9\" y=\"-36.9\" font-family=\"Times,serif\" font-size=\"12.00\">z13</text>\n",
+ "</g>\n",
+ "<!-- 0->4 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>0->4</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M74.9,-182.38C74.9,-152.87 74.9,-105.26 74.9,-73.56\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"78.4,-73.46 74.9,-63.46 71.4,-73.46 78.4,-73.46\"/>\n",
+ "<text text-anchor=\"middle\" x=\"86.4\" y=\"-117.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"365.9\" cy=\"-386\" rx=\"23.3\" ry=\"23.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"365.9\" cy=\"-386\" rx=\"27.29\" ry=\"27.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"365.9\" y=\"-382.9\" font-family=\"Times,serif\" font-size=\"12.00\">z21</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>6</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"365.9\" cy=\"-210\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"365.9\" y=\"-206.9\" font-family=\"Times,serif\" font-size=\"12.00\">z22</text>\n",
+ "</g>\n",
+ "<!-- 1->6 -->\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
+ "<title>1->6</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M365.9,-358.57C365.9,-327.78 365.9,-276.87 365.9,-243.64\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"369.4,-243.51 365.9,-233.51 362.4,-243.51 369.4,-243.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"377.4\" y=\"-294.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"74.9\" cy=\"-556\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74.9\" y=\"-552.9\" font-family=\"Times,serif\" font-size=\"12.00\">z10</text>\n",
+ "</g>\n",
+ "<!-- 2->2 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>2->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M94.92,-568.5C106.05,-570.83 116.3,-566.66 116.3,-556 116.3,-548.84 111.67,-544.6 105.26,-543.31\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"104.85,-539.81 94.92,-543.5 104.99,-546.81 104.85,-539.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.8\" y=\"-552.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"74.9\" cy=\"-386\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74.9\" y=\"-382.9\" font-family=\"Times,serif\" font-size=\"12.00\">z11</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M74.9,-532.34C74.9,-503.33 74.9,-452.85 74.9,-419.68\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"78.4,-419.57 74.9,-409.57 71.4,-419.57 78.4,-419.57\"/>\n",
+ "<text text-anchor=\"middle\" x=\"78.9\" y=\"-471.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 3->0 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>3->0</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M74.9,-362.25C74.9,-333.12 74.9,-282.26 74.9,-247.64\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"78.4,-247.45 74.9,-237.45 71.4,-247.45 78.4,-247.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"86.4\" y=\"-294.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 4->4 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>4->4</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M94.06,-54.06C105.52,-57.19 116.3,-52.5 116.3,-40 116.3,-31.41 111.2,-26.51 104.29,-25.3\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"103.82,-21.82 94.06,-25.94 104.26,-28.81 103.82,-21.82\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.8\" y=\"-36.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>5</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"365.9\" cy=\"-556\" rx=\"23.29\" ry=\"23.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"365.9\" y=\"-552.9\" font-family=\"Times,serif\" font-size=\"12.00\">z20</text>\n",
+ "</g>\n",
+ "<!-- 5->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>5->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M365.9,-532.34C365.9,-504.46 365.9,-456.75 365.9,-423.64\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"369.4,-423.44 365.9,-413.44 362.4,-423.44 369.4,-423.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"369.9\" y=\"-471.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 5->5 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>5->5</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M385.92,-568.5C397.05,-570.83 407.3,-566.66 407.3,-556 407.3,-548.84 402.67,-544.6 396.26,-543.31\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"395.85,-539.81 385.92,-543.5 395.99,-546.81 395.85,-539.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"418.8\" y=\"-552.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 6->6 -->\n",
+ "<g id=\"edge11\" class=\"edge\">\n",
+ "<title>6->6</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M384.2,-225.19C395.97,-229.16 407.3,-224.09 407.3,-210 407.3,-200.09 401.7,-194.64 394.28,-193.66\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"393.74,-190.2 384.2,-194.81 394.53,-197.16 393.74,-190.2\"/>\n",
+ "<text text-anchor=\"middle\" x=\"418.8\" y=\"-206.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 7 -->\n",
+ "<g id=\"node8\" class=\"node\">\n",
+ "<title>7</title>\n",
+ "</g>\n",
+ "<!-- 7->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>7->2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M199.21,-671.74C173.6,-648.11 127.59,-605.63 99.3,-579.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"101.54,-576.83 91.82,-572.62 96.79,-581.97 101.54,-576.83\"/>\n",
+ "</g>\n",
+ "<!-- 7->5 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>7->5</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M237.25,-671.74C263.89,-647.98 311.89,-605.17 341.13,-579.1\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"343.71,-581.48 348.84,-572.21 339.05,-576.26 343.71,-581.48\"/>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "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:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: DFA"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE DFA\n",
+ "SETS\n",
+ " Z = {z0,z1,z2,z3}\n",
+ "CONSTANTS Σ, M, δ, F, M2, z_start\n",
+ "PROPERTIES\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",
+ "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",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"red\",label:\"0\",edges:{a,b|(a,0)|->b:δ}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{a,b|(a,1)|->b:δ});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"black\",label:\"\",edges:{\"\" |-> z_start}) // Kante für den Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Diese Maschiene hat die feste Zustandsmenge Z={z0,z1,z2,z3} und das Alphabet Σ = {0,1}, aber die restlichen Elemente werden der Anweisung ```:constants``` übergeben. Somit kann das Komplement eines beliebigen DFAs erzeugt werden."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants M=({0,1}, //Σ\n",
+ " {z0,z1,z2,z3}, //Z\n",
+ " {(z0,0)↦z1, (z0,1)↦z3,\n",
+ " (z1,0)↦z3, (z1,1)↦z2,\n",
+ " (z2,0)↦z2, (z2,1)↦z2,\n",
+ " (z3,0)↦z3, (z3,1)↦z3 }, //δ\n",
+ " z0, {z0, z2}) //z0, F"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "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 2.44.1 (0)\n",
+ " -->\n",
+ "<!-- Title: prob_graph Pages: 1 -->\n",
+ "<svg width=\"540pt\" height=\"716pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 716.05\" 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 725.95)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-725.95 546.49,-725.95 546.49,4 -4,4\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"189.65\" cy=\"-282\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"189.65\" cy=\"-282\" rx=\"22.44\" ry=\"22.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"189.65\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">z1</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"344.65\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"344.65\" cy=\"-54\" rx=\"22.44\" ry=\"22.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"344.65\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z3</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"red\" d=\"M202.07,-262.89C229.4,-223.03 294.85,-127.61 326.67,-81.22\"/>\n",
+ "<polygon fill=\"red\" stroke=\"red\" points=\"329.61,-83.11 332.38,-72.89 323.84,-79.15 329.61,-83.11\"/>\n",
+ "<text text-anchor=\"middle\" x=\"270.65\" y=\"-164.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=\"48.65\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"48.65\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z2</text>\n",
+ "</g>\n",
+ "<!-- 0->3 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>0->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M178.11,-262.51C152.63,-221.67 91.62,-123.87 63.41,-78.66\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"66.33,-76.73 58.07,-70.1 60.39,-80.44 66.33,-76.73\"/>\n",
+ "<text text-anchor=\"middle\" x=\"122.65\" y=\"-164.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>1->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M365.05,-64.31C375.6,-65.9 385.12,-62.46 385.12,-54 385.12,-48.45 381.02,-45.06 375.22,-43.83\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"375.1,-40.33 365.05,-43.69 375,-47.33 375.1,-40.33\"/>\n",
+ "<text text-anchor=\"middle\" x=\"389.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1->1 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>1->1</title>\n",
+ "<path fill=\"none\" stroke=\"red\" d=\"M361.11,-69.52C380.5,-80.88 403.12,-75.71 403.12,-54 403.12,-35.68 387.01,-29.14 370.34,-34.37\"/>\n",
+ "<polygon fill=\"red\" stroke=\"red\" points=\"368.82,-31.21 361.11,-38.48 371.67,-37.6 368.82,-31.21\"/>\n",
+ "<text text-anchor=\"middle\" x=\"407.12\" y=\"-50.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=\"267.65\" cy=\"-500\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"267.65\" y=\"-496.9\" font-family=\"Times,serif\" font-size=\"12.00\">z0</text>\n",
+ "</g>\n",
+ "<!-- 2->0 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>2->0</title>\n",
+ "<path fill=\"none\" stroke=\"red\" d=\"M261.66,-482.41C248.53,-446.06 217.07,-358.95 200.42,-312.82\"/>\n",
+ "<polygon fill=\"red\" stroke=\"red\" points=\"203.69,-311.58 197,-303.37 197.11,-313.96 203.69,-311.58\"/>\n",
+ "<text text-anchor=\"middle\" x=\"234.65\" y=\"-392.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M270.67,-481.59C282.28,-414.64 324.16,-173.14 339.21,-86.34\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"342.69,-86.76 340.95,-76.31 335.79,-85.57 342.69,-86.76\"/>\n",
+ "<text text-anchor=\"middle\" x=\"312.65\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>3->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M64.39,-63.75C74.89,-66.49 85.12,-63.24 85.12,-54 85.12,-47.94 80.71,-44.45 74.72,-43.55\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"74.13,-40.08 64.39,-44.25 74.61,-47.07 74.13,-40.08\"/>\n",
+ "<text text-anchor=\"middle\" x=\"89.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>3->3</title>\n",
+ "<path fill=\"none\" stroke=\"red\" d=\"M61.23,-67.64C79.83,-81.37 103.12,-76.82 103.12,-54 103.12,-34.74 86.54,-28.5 70.19,-35.26\"/>\n",
+ "<polygon fill=\"red\" stroke=\"red\" points=\"68.19,-32.37 61.23,-40.36 71.65,-38.46 68.19,-32.37\"/>\n",
+ "<text text-anchor=\"middle\" x=\"107.12\" y=\"-50.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",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M267.65,-659.8C267.65,-629.26 267.65,-565.3 267.65,-528.56\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"271.15,-528.53 267.65,-518.53 264.15,-528.53 271.15,-528.53\"/>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "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."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "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",
+ " \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",
+ " ∧\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",
+ " // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\n",
+ " S2 = {z20} ∧ 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",
+ " //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",
+ " ∃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",
+ " (zustand∈Z2 ∧ menge = δ2(zustand,symbol))))}\n",
+ " \n",
+ "DEFINITIONS // Für den Zustandsgraphen:\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|y∈δ(x,0) ∧ y∈δ(x,1)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*S) // Kanten für Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "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 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",
+ "<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",
+ "<!-- 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",
+ "</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",
+ "</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",
+ "</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",
+ "</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",
+ "</g>\n",
+ "<!-- 1->4 -->\n",
+ "<g id=\"edge3\" 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",
+ "</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",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge4\" 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",
+ "</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",
+ "</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",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge5\" 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",
+ "</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",
+ "</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",
+ "</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",
+ "</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",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>6</title>\n",
+ "</g>\n",
+ "<!-- 6->0 -->\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",
+ "</g>\n",
+ "<!-- 6->2 -->\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",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "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. "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "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",
+ " \n",
+ "PROPERTIES\n",
+ " Σ = {0,1}\n",
+ " \n",
+ " ∧\n",
+ " \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 ∧\n",
+ " F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧\n",
+ " δ2 ∈ (Z2×Σ) → ℙ(Z2)\n",
+ " ∧\n",
+ " \n",
+ " //Die Regeln von Folie 53\n",
+ " Z2 = IF S1∩F1 ≠ ∅ THEN Z1 ELSE Z1∪{z} END ∧\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",
+ " //Die Regeln von Folie 54:\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",
+ " \n",
+ "DEFINITIONS // Für den Zustandsgraphen:\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F2); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z2\\F2); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*S2) // Kanten für Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "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 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",
+ "<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",
+ "<!-- 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",
+ "</g>\n",
+ "<!-- 0->0 -->\n",
+ "<g id=\"edge4\" 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",
+ "</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",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge5\" 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",
+ "</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",
+ "</g>\n",
+ "<!-- 0->2 -->\n",
+ "<g id=\"edge1\" 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",
+ "</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",
+ "</g>\n",
+ "<!-- 1->2 -->\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",
+ "</g>\n",
+ "<!-- 2->0 -->\n",
+ "<g id=\"edge6\" 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",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge7\" 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",
+ "</g>\n",
+ "<!-- 2->2 -->\n",
+ "<g id=\"edge2\" 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",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "</g>\n",
+ "<!-- 3->0 -->\n",
+ "<g id=\"edge10\" 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",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "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."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "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",
+ " \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",
+ " ∧\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",
+ " // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\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",
+ " S = S1*S2 ∧\n",
+ " F = F1*(Z2\\F2) ∧\n",
+ " δ = {x | x∈((Z*Z)*INTEGER)*POW(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",
+ "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",
+ " ANIMATION_FUNCTION3 == {r,c,i| r∈dom(f) ∧ c=1 ∧ i=δ(f(r), 0)};\n",
+ " ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">Zustand</td>\n",
+ "<td style=\"padding:10px\">δ(Zustand,0)</td>\n",
+ "<td style=\"padding:10px\">δ(Zustand,1)</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "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."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "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",
+ " \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",
+ " ∧\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",
+ " // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):\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",
+ " S = S1*S2 ∧\n",
+ " F = F1*F2 ∧\n",
+ " δ = {x | x∈((Z*Z)*INTEGER)*POW(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",
+ "DEFINITIONS // Für den Zustandsgraphen:\n",
+ " \"LibraryStrings.def\";\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",
+ " ANIMATION_FUNCTION3 == {r,c,i| r∈dom(f) ∧ c=1 ∧ i=δ(f(r), 0)};\n",
+ " ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">Zustand</td>\n",
+ "<td style=\"padding:10px\">δ(Zustand,0)</td>\n",
+ "<td style=\"padding:10px\">δ(Zustand,1)</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z10|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z11|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z20)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z21)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z21)}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">(z12|->z22)</td>\n",
+ "<td style=\"padding:10px\">{(z12|->z22)}</td>\n",
+ "<td style=\"padding:10px\">{(z11|->z22)}</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Zuletzt bleibt noch die Spiegelung einer Sprache. Um dies zu erreichen erstellen wir aus einem DFA einen NFA."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: DFA"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE DFA\n",
+ "SETS\n",
+ " Z = {z0,z1,z2,z3}\n",
+ "CONSTANTS Σ, M, δ, δ2, F, M2, z_start\n",
+ "PROPERTIES\n",
+ " M = (Σ, Z, δ, z_start, F) ∧\n",
+ " M2 = (Σ, Z, δ2, F, {z_start}) ∧\n",
+ " z_start ∈ Z ∧\n",
+ " F ⊆ Z ∧\n",
+ " δ ∈ (Z×Σ) → Z ∧\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",
+ "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",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z:y)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,z| ∃y.(y∈δ2[{(x,1)}] ∧ y∉δ2[{(x,0)}] ∧ z:y)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∈δ2[{(x,1)}] ∧ z:y)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*F) // Kanten für Startknoten\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants M=({0,1}, //Σ\n",
+ " {z0,z1,z2,z3}, //Z\n",
+ " {(z0,0)↦z1, (z0,1)↦z3,\n",
+ " (z1,0)↦z3, (z1,1)↦z2,\n",
+ " (z2,0)↦z2, (z2,1)↦z2,\n",
+ " (z3,0)↦z3, (z3,1)↦z3 }, //δ\n",
+ " z0, {z0, z2}) //z0, F"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "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 2.44.1 (0)\n",
+ " -->\n",
+ "<!-- Title: prob_graph Pages: 1 -->\n",
+ "<svg width=\"540pt\" height=\"718pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 717.82\" 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 726.01)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-726.01 545.17,-726.01 545.17,4 -4,4\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"189.5\" cy=\"-56\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"189.5\" cy=\"-56\" rx=\"22.44\" ry=\"22.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"189.5\" y=\"-52.9\" font-family=\"Times,serif\" font-size=\"12.00\">z0</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"189.5\" cy=\"-280\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"189.5\" y=\"-276.9\" font-family=\"Times,serif\" font-size=\"12.00\">z1</text>\n",
+ "</g>\n",
+ "<!-- 1->0 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>1->0</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M189.5,-261.21C189.5,-223.71 189.5,-136.13 189.5,-88.77\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"193,-88.75 189.5,-78.75 186,-88.75 193,-88.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"193.5\" y=\"-169.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=\"152.5\" cy=\"-494\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"152.5\" y=\"-490.9\" font-family=\"Times,serif\" font-size=\"12.00\">z2</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M155.53,-475.65C161.95,-438.83 177,-352.64 184.73,-308.34\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"188.21,-308.74 186.48,-298.29 181.31,-307.54 188.21,-308.74\"/>\n",
+ "<text text-anchor=\"middle\" x=\"176.5\" y=\"-383.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 2->2 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>2->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M164.83,-507.95C176.41,-515.18 188.97,-510.53 188.97,-494 188.97,-482.12 182.48,-476.37 174.53,-476.77\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"173.18,-473.53 164.83,-480.05 175.42,-480.16 173.18,-473.53\"/>\n",
+ "<text text-anchor=\"middle\" x=\"200.47\" y=\"-490.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"392.5\" cy=\"-494\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"392.5\" y=\"-490.9\" font-family=\"Times,serif\" font-size=\"12.00\">z3</text>\n",
+ "</g>\n",
+ "<!-- 3->0 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>3->0</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M385.03,-476.97C354.9,-412.24 241.95,-169.66 202.89,-85.76\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"206,-84.15 198.61,-76.57 199.66,-87.11 206,-84.15\"/>\n",
+ "<text text-anchor=\"middle\" x=\"305.5\" y=\"-276.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M380.11,-480.06C345.99,-444.43 250.48,-344.68 209.06,-301.43\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"211.43,-298.84 201.99,-294.04 206.38,-303.69 211.43,-298.84\"/>\n",
+ "<text text-anchor=\"middle\" x=\"301.5\" y=\"-383.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>3->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M404.83,-507.95C416.41,-515.18 428.97,-510.53 428.97,-494 428.97,-482.12 422.48,-476.37 414.53,-476.77\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"413.18,-473.53 404.83,-480.05 415.42,-480.16 413.18,-473.53\"/>\n",
+ "<text text-anchor=\"middle\" x=\"440.47\" y=\"-490.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "</g>\n",
+ "<!-- 4->0 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>4->0</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M70.89,-658.8C87.63,-573.87 161.53,-198.9 183.39,-88\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"186.84,-88.6 185.34,-78.11 179.97,-87.24 186.84,-88.6\"/>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M75.5,-658.97C90.52,-626.98 123.03,-557.76 140.62,-520.3\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"143.87,-521.61 144.95,-511.07 137.53,-518.63 143.87,-521.61\"/>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "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": {
+ "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": 4
+}