From 9fe42d202b3b6fa130c873d58273c770acfd0cb5 Mon Sep 17 00:00:00 2001
From: Chris <Christopher.Happe@uni-duesseldorf.de>
Date: Thu, 5 Nov 2020 09:38:57 +0100
Subject: [PATCH] =?UTF-8?q?Visualisierung=20=C3=BCberarbeitet?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
info4/kapitel-5/DFA_PDA_TM.ipynb | 415 ++++++++++++++++++++-----------
1 file changed, 268 insertions(+), 147 deletions(-)
diff --git a/info4/kapitel-5/DFA_PDA_TM.ipynb b/info4/kapitel-5/DFA_PDA_TM.ipynb
index 9bf4c1d..969e84d 100644
--- a/info4/kapitel-5/DFA_PDA_TM.ipynb
+++ b/info4/kapitel-5/DFA_PDA_TM.ipynb
@@ -12,7 +12,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
@@ -21,28 +21,20 @@
"Loaded machine: DFA_PDA_TM"
]
},
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"MACHINE DFA_PDA_TM\n",
- "/* B Modell einer 1-band Turing Maschine */\n",
- "/* by Michael Leuschel, 2012 */\n",
- "/* Akzeptiert die Sprache a^n b^n c^n (siehe Folien 14ff von folien-kapitel-5 */\n",
+ "\n",
"SETS\n",
- " Alphabet={a,b,c,X,Blank, Bottom, lambda};\n",
- " States = {z0,z1,z2,z3,z4,z5,z6,z_end};\n",
+ " Alphabet={a,b,Blank, Bottom, lambda};\n",
+ " States = {z_0,z_1,z_2,z_3,z_4,z_5,z_6,z_end};\n",
" Direction = {L,R,N}\n",
- "DEFINITIONS\n",
- " Σ == {a, b};\n",
- " CurSymbol == (Right<-Blank)(1);\n",
- " ANIMATION_FUNCTION_DEFAULT == {(1,0,cur)};\n",
- " /* ANIMATION_FUNCTION__xx == {(1,1,Left), (1,3,Right)}; */\n",
- " ANIMATION_FUNCTION1 == {1} *( (λi.(i∈-size(Left)..-1|i+size(Left)+1) ; Left) ∪ Right)\n",
- "CONSTANTS Final, δ,\n",
- " DFA, Z_DFA, δ_DFA, z_start, F_DFA,\n",
+ "\n",
+ "CONSTANTS DFA, Z_DFA, δ_DFA, z_start, F_DFA,\n",
" PDA, Γ_PDA, Z_PDA, δ_PDA,\n",
" TM, Γ_TM, Z_TM, δ_TM, F_TM\n",
"PROPERTIES\n",
@@ -74,6 +66,7 @@
" {regel | ∃zustand.(zustand ∈ F_DFA ∧\n",
" regel = (zustand, lambda, Bottom) ↦ (zustand, []))} ∧\n",
" \n",
+ " //Definition einer TM zum DFA\n",
" TM = (Σ, Γ_TM, Z_TM, δ_TM, z_start, Blank, F_TM) ∧\n",
" Γ_TM ⊆ Alphabet ∧\n",
" Z_TM ⊆ States ∧\n",
@@ -94,72 +87,25 @@
" regel = (zustand, Blank) ↦ (z_end, Blank, N))}\n",
" ∪\n",
" {regel | ∃terminal.(terminal ∈ Γ_TM ∧ regel = (z_end, terminal) ↦ (z_end, terminal, N))} ∧\n",
- " F_TM = {z_end} ∧\n",
- " \n",
- " Final ⊆ States ∧\n",
- " δ ∈ (States * Alphabet) ↔ (States * Alphabet * Direction) ∧\n",
+ " F_TM = {z_end}\n",
"\n",
- " δ = { /* Neuer Zyklus */\n",
- " (z0,a) ↦ (z1,X,R),\n",
- " (z0,X) ↦ (z0,X,R),\n",
- " \n",
- " /* ein a getilgt (X), nächstes b suchen */\n",
- " (z1,a) ↦ (z1,a,R),\n",
- " (z1,b) ↦ (z2,X,R),\n",
- " (z1,X) ↦ (z1,X,R),\n",
- " \n",
- " /* ein a,b getilgt (X), nächstes c suchen */\n",
- " (z2,b) ↦ (z2,b,R),\n",
- " (z2,c) ↦ (z3,X,R),\n",
- " (z2,X) ↦ (z2,X,R),\n",
- " \n",
- " /* ein a,b,c getilgt (X), rechten Rand suchen */\n",
- " (z3,c) ↦ (z3,c,R),\n",
- " (z3,Blank) ↦ (z4,Blank,L),\n",
- " \n",
- " /* Zurücklaufen und testen ob alle a,b,c getilgt */\n",
- " (z4,X) ↦ (z4,X,L),\n",
- " (z4,Blank) ↦ (z6,Blank,R), /* Erfolg ∀ */\n",
- " (z4,c) ↦ (z5,c,L), \n",
- " \n",
- " /* Test nicht erfolgreich; zum linken Rand zurücklaufen und neuer Zyklus */\n",
- " (z5,X) ↦ (z5,X,L),\n",
- " (z5,Blank) ↦ (z0,Blank,R),\n",
- " (z5,a) ↦ (z5,a,L),\n",
- " (z5,b) ↦ (z5,b,L),\n",
- " (z5,c) ↦ (z5,c,L)\n",
- " } ∧\n",
- " Final = {z6}\n",
- "VARIABLES Left,cur,Right\n",
- "INVARIANT\n",
- " cur ∈ States ∧\n",
- " Left ∈ seq(Alphabet) ∧ Right ∈ seq(Alphabet)\n",
- "INITIALISATION Left,cur,Right := [],z0,[a,a,b,b,c,c]\n",
- "OPERATIONS\n",
- " Accept = PRE cur ∈ Final THEN skip END;\n",
- " GoTo(z,S,znew,NewSymbol,Dir) =\n",
- " PRE z=cur ∧ S=CurSymbol ∧\n",
- " (z, S) ↦ (znew,NewSymbol,Dir) ∈ δ THEN\n",
- " ANY tail_Right \n",
- " WHERE (Right=[] ⇒ tail_Right=[]) ∧ (Right≠[] ⇒ tail_Right = tail(Right)) THEN\n",
- " cur := znew ||\n",
- " IF Dir = N THEN\n",
- " Right := NewSymbol -> tail_Right\n",
- " ELSIF Dir = R THEN\n",
- " Left,Right := Left <- NewSymbol, tail_Right\n",
- " ELSIF Left=[] THEN\n",
- " Left,Right := [], Blank -> (NewSymbol -> tail_Right)\n",
- " ELSE\n",
- " Left,Right := front(Left), last(Left) -> (NewSymbol -> tail_Right)\n",
- " END\n",
- " END\n",
- " END\n",
+ "DEFINITIONS\n",
+ " Σ == {a, b};\n",
+ " \n",
+ " //Animation des Zustandsgraphen für den DFA\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes∈F_DFA); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes∈Z_DFA\\F_DFA); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"a\",edges:{x,y|x∈Z_DFA ∧ y=δ_DFA(x,a) ∧ y≠δ_DFA(x,b)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"b\",edges:{x,y|x∈Z_DFA ∧ y=δ_DFA(x,b) ∧ y≠δ_DFA(x,a)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"a, b\",edges:{x,y|x∈Z_DFA ∧ y=δ_DFA(x,a) ∧ y=δ_DFA(x,b)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*{z_start}); // Kanten für Startknoten\n",
"END"
]
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -168,103 +114,278 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants DFA=({a, b}, //Σ\n",
- " {z0,z1,z2,z3}, //Z\n",
- " {(z0,a)↦z1, (z0,b)↦z3,\n",
- " (z1,a)↦z3, (z1,b)↦z2,\n",
- " (z2,a)↦z2, (z2,b)↦z2,\n",
- " (z3,a)↦z3, (z3,b)↦z3 }, //δ\n",
- " z0, {z0, z2}) //z0, F"
+ " {z_0,z_1,z_2,z_3}, //Z\n",
+ " {(z_0,a)↦z_1, (z_0,b)↦z_3,\n",
+ " (z_1,a)↦z_3, (z_1,b)↦z_2,\n",
+ " (z_2,a)↦z_2, (z_2,b)↦z_2,\n",
+ " (z_3,a)↦z_3, (z_3,b)↦z_3 }, //δ\n",
+ " z_0, {z_0, z_2}) //z0, F"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Der Zustandsgraph des DFA sieht wie folgt aus:"
+ ]
+ },
+ {
+ "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=\"718pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 718.36\" 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.18)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-726.18 544.89,-726.18 544.89,4 -4,4\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"286.97\" cy=\"-498\" rx=\"22.3\" ry=\"22.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"286.97\" cy=\"-498\" rx=\"26.32\" ry=\"26.32\"/>\n",
+ "<text text-anchor=\"middle\" x=\"286.97\" y=\"-494.9\" font-family=\"Times,serif\" font-size=\"12.00\">z_0</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"206.97\" cy=\"-279\" rx=\"22.32\" ry=\"22.32\"/>\n",
+ "<text text-anchor=\"middle\" x=\"206.97\" y=\"-275.9\" font-family=\"Times,serif\" font-size=\"12.00\">z_1</text>\n",
+ "</g>\n",
+ "<!-- 0->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>0->2</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M278.11,-472.95C263.35,-432.92 233.8,-352.76 217.82,-309.43\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"221.09,-308.18 214.35,-300.01 214.53,-310.6 221.09,-308.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"250.97\" y=\"-380.9\" font-family=\"Times,serif\" font-size=\"12.00\">a</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"366.97\" cy=\"-59\" rx=\"22.32\" ry=\"22.32\"/>\n",
+ "<text text-anchor=\"middle\" x=\"366.97\" y=\"-55.9\" font-family=\"Times,serif\" font-size=\"12.00\">z_3</text>\n",
+ "</g>\n",
+ "<!-- 0->3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>0->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M291.56,-471.94C305.3,-396.88 346.1,-174.01 361.24,-91.33\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"364.72,-91.76 363.08,-81.29 357.83,-90.5 364.72,-91.76\"/>\n",
+ "<text text-anchor=\"middle\" x=\"332.97\" y=\"-275.9\" font-family=\"Times,serif\" font-size=\"12.00\">b</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"71.97\" cy=\"-59\" rx=\"22.3\" ry=\"22.3\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"71.97\" cy=\"-59\" rx=\"26.32\" ry=\"26.32\"/>\n",
+ "<text text-anchor=\"middle\" x=\"71.97\" y=\"-55.9\" font-family=\"Times,serif\" font-size=\"12.00\">z_2</text>\n",
+ "</g>\n",
+ "<!-- 1->1 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>1->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M90.12,-78.07C103.15,-84.28 116.14,-77.93 116.14,-59 116.14,-44.95 108.98,-37.83 99.97,-37.63\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"99.06,-34.25 90.12,-39.93 100.65,-41.06 99.06,-34.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.64\" y=\"-55.9\" font-family=\"Times,serif\" font-size=\"12.00\">a, b</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M195.7,-259.79C172.53,-222.37 119.36,-136.51 90.85,-90.48\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"93.73,-88.49 85.49,-81.83 87.78,-92.17 93.73,-88.49\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.97\" y=\"-169.9\" font-family=\"Times,serif\" font-size=\"12.00\">b</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M219.8,-260.53C247.95,-222.17 315.29,-130.42 348.21,-85.57\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"351.22,-87.38 354.31,-77.25 345.57,-83.24 351.22,-87.38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"290.97\" y=\"-169.9\" font-family=\"Times,serif\" font-size=\"12.00\">a</text>\n",
+ "</g>\n",
+ "<!-- 3->3 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>3->3</title>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M380.97,-76.57C393.6,-85.12 407.14,-79.26 407.14,-59 407.14,-43.8 399.52,-36.71 390.39,-37.72\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"388.99,-34.51 380.97,-41.43 391.56,-41.02 388.99,-34.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"418.64\" y=\"-55.9\" font-family=\"Times,serif\" font-size=\"12.00\">a, b</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=\"M286.97,-663.88C286.97,-634.44 286.97,-573.63 286.97,-534.66\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"290.47,-534.29 286.97,-524.29 283.47,-534.29 290.47,-534.29\"/>\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": "code",
"execution_count": 4,
"metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Der entstandene PDA hat die gleiche Zustandsmenge, wie der gegebene DFA.\n",
+ "Die Überführungen erfolgen ebenfalls analog.\n",
+ "Damit der PDA allerdings ein Wort akzeptiert muss der Keller leer sein. Dafür werden lambda-Übergänge eingefügt, mit denen man in einem Endzustand des DFA den Keller leeren kann.\n",
+ "Die vollständige Überführungsfunktion des PDA ist durch folgende Tabelle gegeben: "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "```\n",
- ":dot COMMAND [FORMULA]\n",
- "```\n",
- "\n",
- "Execute and show a dot visualisation.\n",
- "\n",
- "The following dot visualisation commands are available:\n",
- "\n",
- "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
- "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n",
- "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n",
- "* `state_space` - State Space: Show state space\n",
- "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
- "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
- "* `history` - Path to Current State: Show a path leading to current state\n",
- "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
- "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
- "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
- "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
- "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
- "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
- "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
- "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
- "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
- "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
- "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
- "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
- "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
- "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
- "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
- "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
- "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ "|z|symbol|keller_symbol|z2|keller_symbole|\n",
+ "|---|---|---|---|---|\n",
+ "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{z\\_0}$|$\\mathit{a}$|$\\mathit{Bottom}$|$\\mathit{z\\_1}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_0}$|$\\mathit{b}$|$\\mathit{Bottom}$|$\\mathit{z\\_3}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_0}$|$\\mathit{lambda}$|$\\mathit{Bottom}$|$\\mathit{z\\_0}$|$\\emptyset$|\n",
+ "|$\\mathit{z\\_1}$|$\\mathit{a}$|$\\mathit{Bottom}$|$\\mathit{z\\_3}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_1}$|$\\mathit{b}$|$\\mathit{Bottom}$|$\\mathit{z\\_2}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{a}$|$\\mathit{Bottom}$|$\\mathit{z\\_2}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{b}$|$\\mathit{Bottom}$|$\\mathit{z\\_2}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{lambda}$|$\\mathit{Bottom}$|$\\mathit{z\\_2}$|$\\emptyset$|\n",
+ "|$\\mathit{z\\_3}$|$\\mathit{a}$|$\\mathit{Bottom}$|$\\mathit{z\\_3}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n",
+ "|$\\mathit{z\\_3}$|$\\mathit{b}$|$\\mathit{Bottom}$|$\\mathit{z\\_3}$|$\\{(1\\mapsto \\mathit{Bottom})\\}$|\n"
],
"text/plain": [
- ":dot COMMAND [FORMULA]\n",
- "Execute and show a dot visualisation.\n",
- "\n",
- "The following dot visualisation commands are available:\n",
- "\n",
- "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
- "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n",
- "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n",
- "* `state_space` - State Space: Show state space\n",
- "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
- "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
- "* `history` - Path to Current State: Show a path leading to current state\n",
- "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
- "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
- "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
- "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
- "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
- "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
- "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
- "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
- "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
- "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
- "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
- "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
- "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
- "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
- "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
- "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
- "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ "z\tsymbol\tkeller_symbol\tz2\tkeller_symbole\n",
+ "z_0\ta\tBottom\tz_1\t{(1|->Bottom)}\n",
+ "z_0\tb\tBottom\tz_3\t{(1|->Bottom)}\n",
+ "z_0\tlambda\tBottom\tz_0\t{}\n",
+ "z_1\ta\tBottom\tz_3\t{(1|->Bottom)}\n",
+ "z_1\tb\tBottom\tz_2\t{(1|->Bottom)}\n",
+ "z_2\ta\tBottom\tz_2\t{(1|->Bottom)}\n",
+ "z_2\tb\tBottom\tz_2\t{(1|->Bottom)}\n",
+ "z_2\tlambda\tBottom\tz_2\t{}\n",
+ "z_3\ta\tBottom\tz_3\t{(1|->Bottom)}\n",
+ "z_3\tb\tBottom\tz_3\t{(1|->Bottom)}\n"
]
},
- "execution_count": 4,
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {z,symbol,keller_symbol,z2,keller_symbole| ((z,symbol,keller_symbol)↦(z2,keller_symbole) : δ_PDA)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Im Gegensatz zum PDA hat die TM einen zusätzlichen Zustand.\n",
+ "Dieser wird benötigt, da eine TM sofort hält, wenn sie einen Endzustand erreicht.\n",
+ "Wenn das Wort also komplett gelesen wurde und die TM in einem Endzustand des DFA ist, darf in den Endzustand der TM übergegangen werden.\n",
+ "Ansonsten sind die Übergänge analog zum DFA.\n",
+ "Die Überführungsfunktion der TM ist durch folgende Tabelle gegeben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|z|x|z2|x2|R|\n",
+ "|---|---|---|---|---|\n",
+ "|$\\mathit{z\\_0}$|$\\mathit{a}$|$\\mathit{z\\_1}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_0}$|$\\mathit{b}$|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_0}$|$\\mathit{Blank}$|$\\mathit{z\\_end}$|$\\mathit{Blank}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_1}$|$\\mathit{a}$|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_1}$|$\\mathit{b}$|$\\mathit{z\\_2}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_1}$|$\\mathit{Blank}$|$\\mathit{z\\_1}$|$\\mathit{Blank}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{a}$|$\\mathit{z\\_2}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{b}$|$\\mathit{z\\_2}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_2}$|$\\mathit{Blank}$|$\\mathit{z\\_end}$|$\\mathit{Blank}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_3}$|$\\mathit{a}$|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_3}$|$\\mathit{b}$|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{R}$|\n",
+ "|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{z\\_3}$|$\\mathit{Blank}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_end}$|$\\mathit{a}$|$\\mathit{z\\_end}$|$\\mathit{a}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_end}$|$\\mathit{b}$|$\\mathit{z\\_end}$|$\\mathit{b}$|$\\mathit{N}$|\n",
+ "|$\\mathit{z\\_end}$|$\\mathit{Blank}$|$\\mathit{z\\_end}$|$\\mathit{Blank}$|$\\mathit{N}$|\n"
+ ],
+ "text/plain": [
+ "z\tx\tz2\tx2\tR\n",
+ "z_0\ta\tz_1\tBlank\tR\n",
+ "z_0\tb\tz_3\tBlank\tR\n",
+ "z_0\tBlank\tz_end\tBlank\tN\n",
+ "z_1\ta\tz_3\tBlank\tR\n",
+ "z_1\tb\tz_2\tBlank\tR\n",
+ "z_1\tBlank\tz_1\tBlank\tN\n",
+ "z_2\ta\tz_2\tBlank\tR\n",
+ "z_2\tb\tz_2\tBlank\tR\n",
+ "z_2\tBlank\tz_end\tBlank\tN\n",
+ "z_3\ta\tz_3\tBlank\tR\n",
+ "z_3\tb\tz_3\tBlank\tR\n",
+ "z_3\tBlank\tz_3\tBlank\tN\n",
+ "z_end\ta\tz_end\ta\tN\n",
+ "z_end\tb\tz_end\tb\tN\n",
+ "z_end\tBlank\tz_end\tBlank\tN\n"
+ ]
+ },
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":help dot"
+ ":table {z,x,z2,x2,R| ((z,x)↦(z2,x2,R)) : δ_TM}"
]
}
],
--
GitLab