{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Deterministic finite automata" ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "from tock import *" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Loading DFAs from files\n", "\n", "Sipser and other textbooks represent DFAs, and all kinds of automata, using either tables or graphs. You can create automata either way and load them into Tock.\n", "\n", "To create tables, you can use any spreadsheet software (Excel, OpenOffice, iWork, Google Drive) and export in CSV or Excel (`.xlsx`) format. Then read it into Tock using the `read_csv` or `read_excel` function." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "m = read_csv(\"examples/sipser-1-4.csv\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Graphs should be in Trivial Graph Format (TGF), which most graph-editing software ([yED], [Gephi]) can export in. Then a graph can be read into Tock using the `read_tgf` function.\n", "\n", "[yED]: http://www.yworks.com/en/products/yfiles/yed/\n", "[Gephi]: http://gephi.github.io" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [], "source": [ "m = read_tgf(\"examples/sipser-1-4.tgf\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Creating DFAs in code\n", "\n", "You can also use Tock functions to create an automaton in code." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [], "source": [ "m = FiniteAutomaton()\n", "m.set_start_state('q1')\n", "m.add_accept_state('q2')\n", "m.add_transition('q1, 0 -> q1')\n", "m.add_transition('q1, 1 -> q2')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "You can also specify a transition as two strings or two lists of strings." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [], "source": [ "m.add_transition('q2, 0', 'q3')\n", "m.add_transition(['q2', '1'], ['q3'])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "And you can use `m.add_transitions` to add several transitions at once." ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [], "source": [ "m.add_transitions(['q3, 0 -> q2',\n", " 'q3, 1 -> q2'])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Editing DFAs graphically\n", "\n", "In a Jupyter notebook, you can edit a DFA graphically." ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "application/javascript": [ "/*\n", " Finite State Machine Designer (http://madebyevan.com/fsm/)\n", " License: MIT License (see below)\n", "\n", " Copyright (c) 2010 Evan Wallace\n", "\n", " Permission is hereby granted, free of charge, to any person\n", " obtaining a copy of this software and associated documentation\n", " files (the \"Software\"), to deal in the Software without\n", " restriction, including without limitation the rights to use,\n", " copy, modify, merge, publish, distribute, sublicense, and/or sell\n", " copies of the Software, and to permit persons to whom the\n", " Software is furnished to do so, subject to the following\n", " conditions:\n", "\n", " The above copyright notice and this permission notice shall be\n", " included in all copies or substantial portions of the Software.\n", "\n", " THE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND,\n", " EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES\n", " OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND\n", " NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT\n", " HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,\n", " WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING\n", " FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR\n", " OTHER DEALINGS IN THE SOFTWARE.\n", "*/\n", "\n", "/* \n", " Bugs:\n", " - In Jupyter, if the canvas is too wide, a horizontal scrollbar appears,\n", " which makes the output too high, so a vertical scrollbar appears too.\n", "\n", " To do:\n", " - Change keybinding for delete node/edge\n", " - Change edge's endpoint\n", " - Map > and @ to start/accept state?\n", " - Help\n", "*/\n", "\n", "function StartLink(node, start) {\n", " this.node = node;\n", " this.deltaX = 0;\n", " this.deltaY = 0;\n", "\n", " if(start) {\n", " this.setAnchorPoint(start.x, start.y);\n", " }\n", "}\n", "\n", "StartLink.prototype.setAnchorPoint = function(x, y) {\n", " this.deltaX = x - this.node.x;\n", " this.deltaY = y - this.node.y;\n", "\n", " if(Math.abs(this.deltaX) < snapToPadding) {\n", " this.deltaX = 0;\n", " }\n", "\n", " if(Math.abs(this.deltaY) < snapToPadding) {\n", " this.deltaY = 0;\n", " }\n", "};\n", "\n", "StartLink.prototype.getEndPoints = function() {\n", " var startX = this.node.x + this.deltaX;\n", " var startY = this.node.y + this.deltaY;\n", " var end = this.node.closestPointOnCircle(startX, startY);\n", " return {\n", " 'startX': startX,\n", " 'startY': startY,\n", " 'endX': end.x,\n", " 'endY': end.y,\n", " };\n", "};\n", "\n", "StartLink.prototype.draw = function(c) {\n", " var stuff = this.getEndPoints();\n", "\n", " // draw the line\n", " c.beginPath();\n", " c.moveTo(stuff.startX, stuff.startY);\n", " c.lineTo(stuff.endX, stuff.endY);\n", " c.stroke();\n", "\n", " // draw the head of the arrow\n", " drawArrow(c, stuff.endX, stuff.endY, Math.atan2(-this.deltaY, -this.deltaX));\n", "};\n", "\n", "StartLink.prototype.containsPoint = function(x, y) {\n", " var stuff = this.getEndPoints();\n", " var dx = stuff.endX - stuff.startX;\n", " var dy = stuff.endY - stuff.startY;\n", " var length = Math.sqrt(dx*dx + dy*dy);\n", " var percent = (dx * (x - stuff.startX) + dy * (y - stuff.startY)) / (length * length);\n", " var distance = (dx * (y - stuff.startY) - dy * (x - stuff.startX)) / length;\n", " return (percent > 0 && percent < 1 && Math.abs(distance) < hitTargetPadding);\n", "};\n", "\n", "function Link(a, b) {\n", " this.nodeA = a;\n", " this.nodeB = b;\n", " this.text = '';\n", " this.lineAngleAdjust = 0; // value to add to textAngle when link is straight line\n", "\n", " // make anchor point relative to the locations of nodeA and nodeB\n", " this.parallelPart = 0.5; // percentage from nodeA to nodeB\n", " this.perpendicularPart = 0; // pixels from line between nodeA and nodeB\n", "}\n", "\n", "Link.prototype.getAnchorPoint = function() {\n", " var dx = this.nodeB.x - this.nodeA.x;\n", " var dy = this.nodeB.y - this.nodeA.y;\n", " var scale = Math.sqrt(dx * dx + dy * dy);\n", " return {\n", " 'x': this.nodeA.x + dx * this.parallelPart - dy * this.perpendicularPart / scale,\n", " 'y': this.nodeA.y + dy * this.parallelPart + dx * this.perpendicularPart / scale\n", " };\n", "};\n", "\n", "Link.prototype.setAnchorPoint = function(x, y) {\n", " var dx = this.nodeB.x - this.nodeA.x;\n", " var dy = this.nodeB.y - this.nodeA.y;\n", " var scale = Math.sqrt(dx * dx + dy * dy);\n", " this.parallelPart = (dx * (x - this.nodeA.x) + dy * (y - this.nodeA.y)) / (scale * scale);\n", " this.perpendicularPart = (dx * (y - this.nodeA.y) - dy * (x - this.nodeA.x)) / scale;\n", " // snap to a straight line\n", " if(this.parallelPart > 0 && this.parallelPart < 1 && Math.abs(this.perpendicularPart) < snapToPadding) {\n", " this.lineAngleAdjust = (this.perpendicularPart < 0) * Math.PI;\n", " this.perpendicularPart = 0;\n", " }\n", "};\n", "\n", "Link.prototype.getEndPointsAndCircle = function() {\n", " if(this.perpendicularPart == 0) {\n", " var midX = (this.nodeA.x + this.nodeB.x) / 2;\n", " var midY = (this.nodeA.y + this.nodeB.y) / 2;\n", " var start = this.nodeA.closestPointOnCircle(midX, midY);\n", " var end = this.nodeB.closestPointOnCircle(midX, midY);\n", " return {\n", " 'hasCircle': false,\n", " 'startX': start.x,\n", " 'startY': start.y,\n", " 'endX': end.x,\n", " 'endY': end.y,\n", " };\n", " }\n", " var anchor = this.getAnchorPoint();\n", " var circle = circleFromThreePoints(this.nodeA.x, this.nodeA.y, this.nodeB.x, this.nodeB.y, anchor.x, anchor.y);\n", " var isReversed = (this.perpendicularPart > 0);\n", " var reverseScale = isReversed ? 1 : -1;\n", " var startAngle = Math.atan2(this.nodeA.y - circle.y, this.nodeA.x - circle.x) - reverseScale * nodeRadius / circle.radius;\n", " var endAngle = Math.atan2(this.nodeB.y - circle.y, this.nodeB.x - circle.x) + reverseScale * nodeRadius / circle.radius;\n", " var startX = circle.x + circle.radius * Math.cos(startAngle);\n", " var startY = circle.y + circle.radius * Math.sin(startAngle);\n", " var endX = circle.x + circle.radius * Math.cos(endAngle);\n", " var endY = circle.y + circle.radius * Math.sin(endAngle);\n", " return {\n", " 'hasCircle': true,\n", " 'startX': startX,\n", " 'startY': startY,\n", " 'endX': endX,\n", " 'endY': endY,\n", " 'startAngle': startAngle,\n", " 'endAngle': endAngle,\n", " 'circleX': circle.x,\n", " 'circleY': circle.y,\n", " 'circleRadius': circle.radius,\n", " 'reverseScale': reverseScale,\n", " 'isReversed': isReversed,\n", " };\n", "};\n", "\n", "Link.prototype.draw = function(c) {\n", " var stuff = this.getEndPointsAndCircle();\n", " // draw arc\n", " c.beginPath();\n", " if(stuff.hasCircle) {\n", " c.arc(stuff.circleX, stuff.circleY, stuff.circleRadius, stuff.startAngle, stuff.endAngle, stuff.isReversed);\n", " } else {\n", " c.moveTo(stuff.startX, stuff.startY);\n", " c.lineTo(stuff.endX, stuff.endY);\n", " }\n", " c.stroke();\n", " // draw the head of the arrow\n", " if(stuff.hasCircle) {\n", " drawArrow(c, stuff.endX, stuff.endY, stuff.endAngle - stuff.reverseScale * (Math.PI / 2));\n", " } else {\n", " drawArrow(c, stuff.endX, stuff.endY, Math.atan2(stuff.endY - stuff.startY, stuff.endX - stuff.startX));\n", " }\n", " // draw the text\n", " if(stuff.hasCircle) {\n", " var startAngle = stuff.startAngle;\n", " var endAngle = stuff.endAngle;\n", " if(endAngle < startAngle) {\n", " endAngle += Math.PI * 2;\n", " }\n", " var textAngle = (startAngle + endAngle) / 2 + stuff.isReversed * Math.PI;\n", " var textX = stuff.circleX + stuff.circleRadius * Math.cos(textAngle);\n", " var textY = stuff.circleY + stuff.circleRadius * Math.sin(textAngle);\n", " drawText(c, this.text, textX, textY, textAngle, selectedObject == this);\n", " } else {\n", " var textX = (stuff.startX + stuff.endX) / 2;\n", " var textY = (stuff.startY + stuff.endY) / 2;\n", " var textAngle = Math.atan2(stuff.endX - stuff.startX, stuff.startY - stuff.endY);\n", " drawText(c, this.text, textX, textY, textAngle + this.lineAngleAdjust, selectedObject == this);\n", " }\n", "};\n", "\n", "Link.prototype.containsPoint = function(x, y) {\n", " var stuff = this.getEndPointsAndCircle();\n", " if(stuff.hasCircle) {\n", " var dx = x - stuff.circleX;\n", " var dy = y - stuff.circleY;\n", " var distance = Math.sqrt(dx*dx + dy*dy) - stuff.circleRadius;\n", " if(Math.abs(distance) < hitTargetPadding) {\n", " var angle = Math.atan2(dy, dx);\n", " var startAngle = stuff.startAngle;\n", " var endAngle = stuff.endAngle;\n", " if(stuff.isReversed) {\n", " var temp = startAngle;\n", " startAngle = endAngle;\n", " endAngle = temp;\n", " }\n", " if(endAngle < startAngle) {\n", " endAngle += Math.PI * 2;\n", " }\n", " if(angle < startAngle) {\n", " angle += Math.PI * 2;\n", " } else if(angle > endAngle) {\n", " angle -= Math.PI * 2;\n", " }\n", " return (angle > startAngle && angle < endAngle);\n", " }\n", " } else {\n", " var dx = stuff.endX - stuff.startX;\n", " var dy = stuff.endY - stuff.startY;\n", " var length = Math.sqrt(dx*dx + dy*dy);\n", " var percent = (dx * (x - stuff.startX) + dy * (y - stuff.startY)) / (length * length);\n", " var distance = (dx * (y - stuff.startY) - dy * (x - stuff.startX)) / length;\n", " return (percent > 0 && percent < 1 && Math.abs(distance) < hitTargetPadding);\n", " }\n", " return false;\n", "};\n", "\n", "function Node(x, y) {\n", " this.x = x;\n", " this.y = y;\n", " this.mouseOffsetX = 0;\n", " this.mouseOffsetY = 0;\n", " this.isAcceptState = false;\n", " this.text = '';\n", "}\n", "\n", "Node.prototype.setMouseStart = function(x, y) {\n", " this.mouseOffsetX = this.x - x;\n", " this.mouseOffsetY = this.y - y;\n", "};\n", "\n", "Node.prototype.setAnchorPoint = function(x, y) {\n", " this.x = x + this.mouseOffsetX;\n", " this.y = y + this.mouseOffsetY;\n", "};\n", "\n", "Node.prototype.draw = function(c) {\n", " // draw the circle\n", " c.beginPath();\n", " c.arc(this.x, this.y, nodeRadius, 0, 2 * Math.PI, false);\n", " c.stroke();\n", "\n", " // draw the text\n", " drawText(c, this.text, this.x, this.y, null, selectedObject == this, nodeRadius*1.6);\n", "\n", " // draw a double circle for an accept state\n", " if(this.isAcceptState) {\n", " c.beginPath();\n", " c.arc(this.x, this.y, nodeRadius * 0.8, 0, 2 * Math.PI, false);\n", " c.stroke();\n", " }\n", "};\n", "\n", "Node.prototype.closestPointOnCircle = function(x, y) {\n", " var dx = x - this.x;\n", " var dy = y - this.y;\n", " var scale = Math.sqrt(dx * dx + dy * dy);\n", " return {\n", " 'x': this.x + dx * nodeRadius / scale,\n", " 'y': this.y + dy * nodeRadius / scale,\n", " };\n", "};\n", "\n", "Node.prototype.containsPoint = function(x, y) {\n", " return (x - this.x)*(x - this.x) + (y - this.y)*(y - this.y) < nodeRadius*nodeRadius;\n", "};\n", "\n", "function SelfLink(node, mouse) {\n", " this.node = node;\n", " this.anchorAngle = 0;\n", " this.mouseOffsetAngle = 0;\n", " this.text = '';\n", "\n", " if(mouse) {\n", " this.setAnchorPoint(mouse.x, mouse.y);\n", " }\n", "}\n", "\n", "SelfLink.prototype.setMouseStart = function(x, y) {\n", " this.mouseOffsetAngle = this.anchorAngle - Math.atan2(y - this.node.y, x - this.node.x);\n", "};\n", "\n", "SelfLink.prototype.setAnchorPoint = function(x, y) {\n", " this.anchorAngle = Math.atan2(y - this.node.y, x - this.node.x) + this.mouseOffsetAngle;\n", " // snap to 90 degrees\n", " var snap = Math.round(this.anchorAngle / (Math.PI / 2)) * (Math.PI / 2);\n", " if(Math.abs(this.anchorAngle - snap) < 0.1) this.anchorAngle = snap;\n", " // keep in the range -pi to pi so our containsPoint() function always works\n", " if(this.anchorAngle < -Math.PI) this.anchorAngle += 2 * Math.PI;\n", " if(this.anchorAngle > Math.PI) this.anchorAngle -= 2 * Math.PI;\n", "};\n", "\n", "SelfLink.prototype.getEndPointsAndCircle = function() {\n", " var circleX = this.node.x + 1.5 * nodeRadius * Math.cos(this.anchorAngle);\n", " var circleY = this.node.y + 1.5 * nodeRadius * Math.sin(this.anchorAngle);\n", " var circleRadius = 0.75 * nodeRadius;\n", " var startAngle = this.anchorAngle - Math.PI * 0.8;\n", " var endAngle = this.anchorAngle + Math.PI * 0.8;\n", " var startX = circleX + circleRadius * Math.cos(startAngle);\n", " var startY = circleY + circleRadius * Math.sin(startAngle);\n", " var endX = circleX + circleRadius * Math.cos(endAngle);\n", " var endY = circleY + circleRadius * Math.sin(endAngle);\n", " return {\n", " 'hasCircle': true,\n", " 'startX': startX,\n", " 'startY': startY,\n", " 'endX': endX,\n", " 'endY': endY,\n", " 'startAngle': startAngle,\n", " 'endAngle': endAngle,\n", " 'circleX': circleX,\n", " 'circleY': circleY,\n", " 'circleRadius': circleRadius\n", " };\n", "};\n", "\n", "SelfLink.prototype.draw = function(c) {\n", " var stuff = this.getEndPointsAndCircle();\n", " // draw arc\n", " c.beginPath();\n", " c.arc(stuff.circleX, stuff.circleY, stuff.circleRadius, stuff.startAngle, stuff.endAngle, false);\n", " c.stroke();\n", " // draw the text on the loop farthest from the node\n", " var textX = stuff.circleX + stuff.circleRadius * Math.cos(this.anchorAngle);\n", " var textY = stuff.circleY + stuff.circleRadius * Math.sin(this.anchorAngle);\n", " drawText(c, this.text, textX, textY, this.anchorAngle, selectedObject == this);\n", " // draw the head of the arrow\n", " drawArrow(c, stuff.endX, stuff.endY, stuff.endAngle + Math.PI * 0.4);\n", "};\n", "\n", "SelfLink.prototype.containsPoint = function(x, y) {\n", " var stuff = this.getEndPointsAndCircle();\n", " var dx = x - stuff.circleX;\n", " var dy = y - stuff.circleY;\n", " var distance = Math.sqrt(dx*dx + dy*dy) - stuff.circleRadius;\n", " return (Math.abs(distance) < hitTargetPadding);\n", "};\n", "\n", "function TemporaryLink(from, to) {\n", " this.from = from;\n", " this.to = to;\n", "}\n", "\n", "TemporaryLink.prototype.draw = function(c) {\n", " // draw the line\n", " c.beginPath();\n", " c.moveTo(this.to.x, this.to.y);\n", " c.lineTo(this.from.x, this.from.y);\n", " c.stroke();\n", "\n", " // draw the head of the arrow\n", " drawArrow(c, this.to.x, this.to.y, Math.atan2(this.to.y - this.from.y, this.to.x - this.from.x));\n", "};\n", "\n", "function det(a, b, c, d, e, f, g, h, i) {\n", " return a*e*i + b*f*g + c*d*h - a*f*h - b*d*i - c*e*g;\n", "}\n", "\n", "function circleFromThreePoints(x1, y1, x2, y2, x3, y3) {\n", " var a = det(x1, y1, 1, x2, y2, 1, x3, y3, 1);\n", " var bx = -det(x1*x1 + y1*y1, y1, 1, x2*x2 + y2*y2, y2, 1, x3*x3 + y3*y3, y3, 1);\n", " var by = det(x1*x1 + y1*y1, x1, 1, x2*x2 + y2*y2, x2, 1, x3*x3 + y3*y3, x3, 1);\n", " var c = -det(x1*x1 + y1*y1, x1, y1, x2*x2 + y2*y2, x2, y2, x3*x3 + y3*y3, x3, y3);\n", " return {\n", " 'x': -bx / (2*a),\n", " 'y': -by / (2*a),\n", " 'radius': Math.sqrt(bx*bx + by*by - 4*a*c) / (2*Math.abs(a))\n", " };\n", "}\n", "\n", "var mappings = {'&': 'ε', '|-': '⊢', '-|': '⊣', '_': '␣', '->': '→'}\n", "function convertShortcuts(text) {\n", " for (var s in mappings)\n", " text = text.replace(s, mappings[s]);\n", " return text;\n", "}\n", "\n", "function drawArrow(c, x, y, angle) {\n", " var dx = Math.cos(angle) * arrowSize;\n", " var dy = Math.sin(angle) * arrowSize;\n", " c.beginPath();\n", " c.moveTo(x, y);\n", " c.lineTo(x - 2 * dx + dy, y - 2 * dy - dx);\n", " c.lineTo(x - 2 * dx - dy, y - 2 * dy + dx);\n", " c.fill();\n", "}\n", "\n", "function canvasHasFocus() {\n", " return document.activeElement == canvas;\n", "}\n", "\n", "function drawText(c, originalText, x, y, angleOrNull, isSelected, maxWidth) {\n", " var text = convertShortcuts(originalText);\n", " c.save();\n", "\n", " var tmpFontSize = fontSize;\n", " c.font = ''+tmpFontSize+'px monospace';\n", " var width = c.measureText(text).width;\n", "\n", " // resize to fit in maxWidth\n", " if (maxWidth !== undefined && width > maxWidth) {\n", " tmpFontSize *= maxWidth/width;\n", " c.font = ''+tmpFontSize+'px monospace';\n", " width = c.measureText(text).width;\n", " }\n", "\n", " // center the text\n", " x -= width / 2;\n", "\n", " // position the text intelligently if given an angle\n", " if(angleOrNull != null) {\n", " var cos = Math.cos(angleOrNull);\n", " var sin = Math.sin(angleOrNull);\n", " var cornerPointX = (width / 2 + fontSize/4) * (cos > 0 ? 1 : -1);\n", " var cornerPointY = (fontSize/2 + 5) * (sin > 0 ? 1 : -1);\n", " var slide = sin * Math.pow(Math.abs(sin), 40) * cornerPointX - cos * Math.pow(Math.abs(cos), 10) * cornerPointY;\n", " x += cornerPointX - sin * slide;\n", " y += cornerPointY + cos * slide;\n", " }\n", "\n", " // draw text and caret (round the coordinates so the caret falls on a pixel)\n", " x = Math.round(x);\n", " y = Math.round(y);\n", " c.textBaseline = \"middle\";\n", " c.fillText(text, x, y);\n", " if(isSelected && caretVisible && canvasHasFocus() && document.hasFocus()) {\n", " x += width;\n", " c.lineWidth = lineWidth;\n", " c.beginPath();\n", " c.moveTo(x, y - fontSize/2);\n", " c.lineTo(x, y + fontSize/2);\n", " c.stroke();\n", " }\n", " c.restore();\n", "}\n", "\n", "var caretTimer;\n", "var caretVisible = true;\n", "\n", "function resetCaret() {\n", " clearInterval(caretTimer);\n", " caretTimer = setInterval(function () { caretVisible = !caretVisible; draw(); }, 500);\n", " caretVisible = true;\n", "}\n", "\n", "var canvas;\n", "var canvas_dpr;\n", "var nodeRadius = 30;\n", "var arrowSize = 4;\n", "var lineWidth = 1;\n", "var fontSize = 16;\n", "var selectColor = '#00823e';\n", "var nodes = [];\n", "var links = [];\n", "\n", "var cursorVisible = true;\n", "var snapToPadding = 6; // pixels\n", "var hitTargetPadding = 6; // pixels\n", "var selectedObject = null; // either a Link or a Node\n", "var currentLink = null; // a Link\n", "var movingObject = false;\n", "var originalClick;\n", "\n", "function drawUsing(c) {\n", " c.clearRect(0, 0, canvas.width, canvas.height);\n", " c.save();\n", " c.translate(0.5, 0.5);\n", "\n", " for(var i = 0; i < nodes.length; i++) {\n", " if (nodes[i] == selectedObject) {\n", " c.lineWidth = 3*lineWidth;\n", " c.fillStyle = c.strokeStyle = selectColor;\n", " } else {\n", " c.lineWidth = lineWidth;\n", " c.fillStyle = c.strokeStyle = 'black';\n", " }\n", " nodes[i].draw(c);\n", " }\n", " for(var i = 0; i < links.length; i++) {\n", " if (links[i] == selectedObject) {\n", " c.lineWidth = 3*lineWidth;\n", " c.fillStyle = c.strokeStyle = selectColor;\n", " } else {\n", " c.lineWidth = lineWidth;\n", " c.fillStyle = c.strokeStyle = 'black';\n", " }\n", " links[i].draw(c);\n", " }\n", " if(currentLink != null) {\n", " c.lineWidth = lineWidth;\n", " c.fillStyle = c.strokeStyle = 'black';\n", " currentLink.draw(c);\n", " }\n", "\n", " c.restore();\n", "}\n", "\n", "function draw() {\n", " drawUsing(canvas.getContext('2d'));\n", "}\n", "\n", "function selectObject(x, y) {\n", " for(var i = 0; i < nodes.length; i++) {\n", " if(nodes[i].containsPoint(x, y)) {\n", " return nodes[i];\n", " }\n", " }\n", " for(var i = 0; i < links.length; i++) {\n", " if(links[i].containsPoint(x, y)) {\n", " return links[i];\n", " }\n", " }\n", " return null;\n", "}\n", "\n", "function snapNode(node) {\n", " for(var i = 0; i < nodes.length; i++) {\n", " if(nodes[i] == node) continue;\n", "\n", " if(Math.abs(node.x - nodes[i].x) < snapToPadding) {\n", " node.x = nodes[i].x;\n", " }\n", "\n", " if(Math.abs(node.y - nodes[i].y) < snapToPadding) {\n", " node.y = nodes[i].y;\n", " }\n", " }\n", "}\n", "\n", "var message_bar;\n", "function message(s) {\n", " message_bar.innerHTML = s;\n", "}\n", "\n", "function main(ei) {\n", " canvas = document.createElement(\"canvas\");\n", " canvas.setAttribute(\"style\", \"outline: 1px solid black; width: 600px; height: 600px;\");\n", " canvas.setAttribute(\"tabindex\", -1); // make canvas focusable\n", " canvas_dpr = window.devicePixelRatio || 1;\n", " canvas.width = 600 * canvas_dpr;\n", " canvas.height = 600 * canvas_dpr;\n", " element.append(canvas);\n", " \n", " nodeRadius *= canvas_dpr; arrowSize *= canvas_dpr;\n", " lineWidth *= canvas_dpr; fontSize *= canvas_dpr;\n", " snapToPadding *= canvas_dpr; hitTargetPadding *= canvas_dpr;\n", "\n", " load(ei); // bug: if there is an error later in the notebook, this doesn't work\n", " //draw();\n", "\n", " element.append(document.createElement(\"br\"));\n", "\n", " function make_button(label, callback) {\n", " var button = document.createElement(\"button\");\n", " button.setAttribute(\"style\", \"margin: 0 10px 0 0;\");\n", " button.innerHTML = label;\n", " button.onclick = callback;\n", " element.append(button);\n", " }\n", " make_button('Load', function() { load(ei); });\n", " make_button('Save', function() { save(ei); });\n", "\n", " message_bar = document.createElement(\"span\");\n", " element.append(message_bar);\n", "\n", " canvas.onmousedown = function(e) {\n", " var mouse = crossBrowserRelativeMousePos(e);\n", " selectedObject = selectObject(mouse.x, mouse.y);\n", " movingObject = false;\n", " originalClick = mouse;\n", "\n", " if(selectedObject != null) {\n", " if(shift && selectedObject instanceof Node) {\n", " currentLink = new SelfLink(selectedObject, mouse);\n", " } else {\n", " movingObject = true;\n", " if(selectedObject.setMouseStart) {\n", " selectedObject.setMouseStart(mouse.x, mouse.y);\n", " }\n", " }\n", " resetCaret();\n", " } else if(shift) {\n", " currentLink = new TemporaryLink(mouse, mouse);\n", " }\n", "\n", " draw();\n", "\n", " // In Colab the canvas is inside an iframe, which seems to cause trouble\n", " // with this first case.\n", " if(0 && canvasHasFocus()) {\n", " // disable drag-and-drop only if the canvas is already focused\n", " return false;\n", " } else {\n", " // otherwise, let the browser switch the focus away from wherever it was\n", " resetCaret();\n", " return true;\n", " }\n", " };\n", "\n", " canvas.ondblclick = function(e) {\n", " var mouse = crossBrowserRelativeMousePos(e);\n", " selectedObject = selectObject(mouse.x, mouse.y);\n", "\n", " if(selectedObject == null) {\n", " selectedObject = new Node(mouse.x, mouse.y);\n", " if(typeof Jupyter !== 'undefined') Jupyter.keyboard_manager.disable();\n", " nodes.push(selectedObject);\n", " resetCaret();\n", " draw();\n", " } else if(selectedObject instanceof Node) {\n", " selectedObject.isAcceptState = !selectedObject.isAcceptState;\n", " draw();\n", " }\n", " };\n", "\n", " canvas.onmousemove = function(e) {\n", " var mouse = crossBrowserRelativeMousePos(e);\n", "\n", " if(currentLink != null) {\n", " var targetNode = selectObject(mouse.x, mouse.y);\n", " if(!(targetNode instanceof Node)) {\n", " targetNode = null;\n", " }\n", "\n", " if(selectedObject == null) {\n", " if(targetNode != null) {\n", " currentLink = new StartLink(targetNode, originalClick);\n", " } else {\n", " currentLink = new TemporaryLink(originalClick, mouse);\n", " }\n", " } else {\n", " if(targetNode == selectedObject) {\n", " currentLink = new SelfLink(selectedObject, mouse);\n", " } else if(targetNode != null) {\n", " currentLink = new Link(selectedObject, targetNode);\n", " } else {\n", " currentLink = new TemporaryLink(selectedObject.closestPointOnCircle(mouse.x, mouse.y), mouse);\n", " }\n", " }\n", " draw();\n", " }\n", "\n", " if(movingObject) {\n", " selectedObject.setAnchorPoint(mouse.x, mouse.y);\n", " if(selectedObject instanceof Node) {\n", " snapNode(selectedObject);\n", " }\n", " draw();\n", " }\n", " };\n", "\n", " canvas.onmouseup = function(e) {\n", " movingObject = false;\n", "\n", " if(currentLink != null) {\n", " if(!(currentLink instanceof TemporaryLink)) {\n", " selectedObject = currentLink;\n", " if (currentLink instanceof StartLink) {\n", " for(var i=0; i= 0x20 && key <= 0x7E && !e.metaKey && !e.altKey && !e.ctrlKey && selectedObject != null && 'text' in selectedObject) {\n", " selectedObject.text += String.fromCharCode(key);\n", " resetCaret();\n", " draw();\n", "\n", " // don't let keys do their actions (like space scrolls down the page)\n", " return false;\n", " } else if(key == 8) {\n", " // backspace is a shortcut for the back button, but do NOT want to change pages\n", " return false;\n", " }\n", "};\n", "\n", "function crossBrowserKey(e) {\n", " e = e || window.event;\n", " return e.which || e.keyCode;\n", "}\n", "\n", "function crossBrowserElementPos(e) {\n", " e = e || window.event;\n", " // Add up offsets\n", " var obj = e.target || e.srcElement;\n", " var x = 0, y = 0;\n", " while(obj.offsetParent) {\n", " x += obj.offsetLeft;\n", " y += obj.offsetTop;\n", " obj = obj.offsetParent;\n", " }\n", " // Add up scroll positions\n", " obj = e.target || e.srcElement;\n", " while (obj) {\n", " x -= obj.scrollLeft;\n", " y -= obj.scrollTop;\n", " obj = obj.parentElement;\n", " }\n", " return { 'x': x * canvas_dpr, 'y': y * canvas_dpr };\n", "}\n", "\n", "function crossBrowserMousePos(e) {\n", " e = e || window.event;\n", " var x = e.pageX || e.clientX + document.body.scrollLeft + document.documentElement.scrollLeft;\n", " var y = e.pageY || e.clientY + document.body.scrollTop + document.documentElement.scrollTop;\n", " return { 'x': x * canvas_dpr, 'y': y * canvas_dpr };\n", "}\n", "\n", "function crossBrowserRelativeMousePos(e) {\n", " var element = crossBrowserElementPos(e);\n", " var mouse = crossBrowserMousePos(e);\n", " return {\n", " 'x': mouse.x - element.x,\n", " 'y': mouse.y - element.y\n", " };\n", "}\n", "\n", "function getNodeId(node) {\n", " for(var i = 0; i < nodes.length; i++)\n", " if(nodes[i] == node)\n", " return i;\n", "}\n", "\n", "function to_json() {\n", " var g = {'nodes': {}, 'edges': {}};\n", " var start;\n", " for(var i = 0; i < links.length; i++) {\n", " if(links[i] instanceof StartLink)\n", " start = getNodeId(links[i].node);\n", " }\n", " for (var i = 0; i < nodes.length; i++) {\n", " g.nodes[nodes[i].text] = {\n", " 'start': i == start,\n", " 'accept': nodes[i].isAcceptState\n", " };\n", " }\n", " if (Object.keys(g.nodes).length != nodes.length) {\n", " message(\"Every state must have a unique name.\");\n", " return null;\n", " }\n", " for(var i = 0; i < links.length; i++) {\n", " if(links[i] instanceof Link) {\n", " var u = links[i].nodeA.text;\n", " var v = links[i].nodeB.text;\n", " if (!(u in g.edges)) g.edges[u] = {};\n", " if (!(v in g.edges[u])) g.edges[u][v] = [];\n", " g.edges[u][v].push({ 'label': links[i].text });\n", " } else if(links[i] instanceof SelfLink) {\n", " var v = links[i].node.text;\n", " if (!(v in g.edges)) g.edges[v] = {};\n", " if (!(v in g.edges[v])) g.edges[v][v] = [];\n", " g.edges[v][v].push({ 'label': links[i].text });\n", " }\n", " }\n", " return g;\n", "}\n", "\n", "function save(ei) {\n", " for (var vi=0; vi message('Save successful'), message);\n", " }\n", "}\n", "\n", "function from_json(g) {\n", " // Clear the current graph\n", " nodes = [];\n", " links = [];\n", " selectedObject = null;\n", "\n", " // Transform from graphviz coordinates to ours\n", " var eps = Math.min(canvas.width, canvas.height)*0.03; \n", " function tx(x) { return (x-g.xmin+eps) / (g.xmax-g.xmin+2*eps) * canvas.width; }\n", " function ty(y) { return (g.ymax-y+eps) / (g.ymax-g.ymin+2*eps) * canvas.height; }\n", "\n", " var node_index = {}\n", " for (var v in g.nodes) {\n", " var newnode;\n", " if ('x' in g.nodes[v] && 'y' in g.nodes[v])\n", " newnode = new Node(tx(g.nodes[v].x), ty(g.nodes[v].y));\n", " else\n", " newnode = new Node(0, 0); // will move later\n", " var label = v;\n", " if (g.nodes[v].start)\n", " links.push(new StartLink(newnode, {'x': tx(g.nodes[v].startx),\n", " 'y': ty(g.nodes[v].starty)}));\n", " if (g.nodes[v].accept)\n", " newnode.isAcceptState = true;\n", " newnode.text = label;\n", " nodes.push(newnode);\n", " node_index[v] = newnode;\n", " }\n", "\n", " for (var u in g.edges) {\n", " var unode = node_index[u];\n", " for (var v in g.edges[u]) {\n", " var vnode = node_index[v];\n", " for (var i=0; i" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "m.edit()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Inspecting DFAs" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Once a machine is loaded, we can test whether it is indeed a DFA:" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "m.is_finite() # is it a finite automaton?" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "m.is_deterministic() # is it deterministic?" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Regardless of how it was created and loaded, it can be viewed as a table:" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
01
>q1q1q2
@q2q3q3
q3q2q2
" ], "text/plain": [ "" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "to_table(m)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "This machine has three states, listed in the first column: `q1`, `q2`, and `q3`. The `>` means that `q1` is the start state (the state the machine starts in), and the `@` means that `q2` is a final state (meaning that when the machine has read all of the input, it accepts the input iff it is in a final state). These symbols are not part of the state name.\n", "\n", "The first row lists all possible input symbols (here, `0` and `1`), and the interior cells indicate what the new state should be after reading a symbol. For example, if the machine is in state `q1` and reads a `1`, then it changes to state `q2`.\n", "\n", "It's more convenient to visualize the automaton's operation using a state transition diagram:" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q3\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "to_graph(m)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "You can also iterate over all transitions:" ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "q1,0 → q1\n", "q1,1 → q2\n", "q2,0 → q3\n", "q2,1 → q3\n", "q3,0 → q2\n", "q3,1 → q2\n" ] } ], "source": [ "for t in m.get_transitions(): print(t)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Running DFAs" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now let's run the automaton on a string (remember to separate symbols by spaces):" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
q1[0] 0 0 1 1 1
q1[0] 0 1 1 1
q1[0] 1 1 1
q1[1] 1 1
q2[1] 1
q31
q2ε
\n", "

accept

" ], "text/plain": [ "" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "run(m, '0 0 0 1 1 1').only_path()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "At each time step, this shows the state and the remainder of the input, with square brackets on the next-to-be-read symbol.\n", "\n", "The return value of `run` is actually a graph:" ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "scrolled": false }, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q3\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "run(m, '0 0 0 1 1 1')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Each node says what state the machine is at a time step, and on the right is the input string, with the next symbol marked with square brackets. The run ends with a double node, indicating that at the end of the input string, the machine was in a final state, so it accepted the string.\n", "\n", "Let's try a different string:" ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "q3\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q3\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "run(m, '1 0 0 0')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "This time, the fact that the run doesn't end with a double node means that the string was rejected." ] } ], "metadata": { "kernelspec": { "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.8.13" } }, "nbformat": 4, "nbformat_minor": 1 }