diff --git a/.ipynb_checkpoints/DryVR_Notebook-checkpoint.ipynb b/.ipynb_checkpoints/DryVR_Notebook-checkpoint.ipynb index 2fd6442..eb9eac2 100644 --- a/.ipynb_checkpoints/DryVR_Notebook-checkpoint.ipynb +++ b/.ipynb_checkpoints/DryVR_Notebook-checkpoint.ipynb @@ -1,6 +1,973 @@ { - "cells": [], - "metadata": {}, + "cells": [ + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "from src.core.dryvrmain import verify\n", + "%matplotlib notebook\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "ename": "IndentationError", + "evalue": "unindent does not match any outer indentation level (, line 11)", + "output_type": "error", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32m11\u001b[0m\n\u001b[0;31m time.sleep(1)\u001b[0m\n\u001b[0m ^\u001b[0m\n\u001b[0;31mIndentationError\u001b[0m\u001b[0;31m:\u001b[0m unindent does not match any outer indentation level\n" + ] + } + ], + "source": [ + "from scipy.integrate import odeint\n", + "import numpy as np \n", + "import time\n", + "\n", + "def thermo_dynamic(y,t,rate):\n", + " dydt = rate*y\n", + " return dydt\n", + "\n", + "def TC_Simulate(Mode,initialCondition,time_bound):\n", + " time_step = 0.05;\n", + " time.sleep(1)\n", + " time_bound = float(time_bound)\n", + " initial = [float(tmp) for tmp in initialCondition]\n", + " number_points = int(np.ceil(time_bound/time_step))\n", + " t = [i*time_step for i in range(0,number_points)]\n", + " if t[-1] != time_step:\n", + " t.append(time_bound)\n", + "\n", + " y_initial = initial[0]\n", + "\n", + " if Mode == 'On':\n", + " rate = 0.1\n", + " elif Mode == 'Off':\n", + " rate = -0.1\n", + " else:\n", + " print('Wrong Mode name!')\n", + " sol = odeint(thermo_dynamic,y_initial,t,args=(rate,),hmax = time_step)\n", + "\n", + " # Construct the final output\n", + " trace = []\n", + " for j in range(len(t)):\n", + " #print t[j], current_psi\n", + " tmp = []\n", + " tmp.append(t[j])\n", + " tmp.append(sol[j,0])\n", + " trace.append(tmp)\n", + " return trace" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [], + "source": [ + "args = {\n", + " \"vertex\" : [\"On\",\"Off\",\"On\"],\n", + " \"edge\":[[0,1],[1,2]],\n", + " \"variables\":[\"temp\"],\n", + " \"guards\":[\"And(t>1.0,t<=1.1)\",\"And(t>1.0,t<=1.1)\"],\n", + " \"initialSet\":[[75.0],[76.0]],\n", + " \"unsafeSet\":\"@On:temp>91@Off:temp>91\",\n", + " \"timeHorizon\":3.5,\n", + "}" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "application/javascript": [ + "/* Put everything inside the global mpl namespace */\n", + "window.mpl = {};\n", + "\n", + "\n", + "mpl.get_websocket_type = function() {\n", + " if (typeof(WebSocket) !== 'undefined') {\n", + " return WebSocket;\n", + " } else if (typeof(MozWebSocket) !== 'undefined') {\n", + " return MozWebSocket;\n", + " } else {\n", + " alert('Your browser does not have WebSocket support.' +\n", + " 'Please try Chrome, Safari or Firefox ≥ 6. ' +\n", + " 'Firefox 4 and 5 are also supported but you ' +\n", + " 'have to enable WebSockets in about:config.');\n", + " };\n", + "}\n", + "\n", + "mpl.figure = function(figure_id, websocket, ondownload, parent_element) {\n", + " this.id = figure_id;\n", + "\n", + " this.ws = websocket;\n", + "\n", + " this.supports_binary = (this.ws.binaryType != undefined);\n", + "\n", + " if (!this.supports_binary) {\n", + " var warnings = document.getElementById(\"mpl-warnings\");\n", + " if (warnings) {\n", + " warnings.style.display = 'block';\n", + " warnings.textContent = (\n", + " \"This browser does not support binary websocket messages. \" +\n", + " \"Performance may be slow.\");\n", + " }\n", + " }\n", + "\n", + " this.imageObj = new Image();\n", + "\n", + " this.context = undefined;\n", + " this.message = undefined;\n", + " this.canvas = undefined;\n", + " this.rubberband_canvas = undefined;\n", + " this.rubberband_context = undefined;\n", + " this.format_dropdown = undefined;\n", + "\n", + " this.image_mode = 'full';\n", + "\n", + " this.root = $('
');\n", + " this._root_extra_style(this.root)\n", + " this.root.attr('style', 'display: inline-block');\n", + "\n", + " $(parent_element).append(this.root);\n", + "\n", + " this._init_header(this);\n", + " this._init_canvas(this);\n", + " this._init_toolbar(this);\n", + "\n", + " var fig = this;\n", + "\n", + " this.waiting = false;\n", + "\n", + " this.ws.onopen = function () {\n", + " fig.send_message(\"supports_binary\", {value: fig.supports_binary});\n", + " fig.send_message(\"send_image_mode\", {});\n", + " if (mpl.ratio != 1) {\n", + " fig.send_message(\"set_dpi_ratio\", {'dpi_ratio': mpl.ratio});\n", + " }\n", + " fig.send_message(\"refresh\", {});\n", + " }\n", + "\n", + " this.imageObj.onload = function() {\n", + " if (fig.image_mode == 'full') {\n", + " // Full images could contain transparency (where diff images\n", + " // almost always do), so we need to clear the canvas so that\n", + " // there is no ghosting.\n", + " fig.context.clearRect(0, 0, fig.canvas.width, fig.canvas.height);\n", + " }\n", + " fig.context.drawImage(fig.imageObj, 0, 0);\n", + " };\n", + "\n", + " this.imageObj.onunload = function() {\n", + " fig.ws.close();\n", + " }\n", + "\n", + " this.ws.onmessage = this._make_on_message_function(this);\n", + "\n", + " this.ondownload = ondownload;\n", + "}\n", + "\n", + "mpl.figure.prototype._init_header = function() {\n", + " var titlebar = $(\n", + " '
');\n", + " var titletext = $(\n", + " '
');\n", + " titlebar.append(titletext)\n", + " this.root.append(titlebar);\n", + " this.header = titletext[0];\n", + "}\n", + "\n", + "\n", + "\n", + "mpl.figure.prototype._canvas_extra_style = function(canvas_div) {\n", + "\n", + "}\n", + "\n", + "\n", + "mpl.figure.prototype._root_extra_style = function(canvas_div) {\n", + "\n", + "}\n", + "\n", + "mpl.figure.prototype._init_canvas = function() {\n", + " var fig = this;\n", + "\n", + " var canvas_div = $('
');\n", + "\n", + " canvas_div.attr('style', 'position: relative; clear: both; outline: 0');\n", + "\n", + " function canvas_keyboard_event(event) {\n", + " return fig.key_event(event, event['data']);\n", + " }\n", + "\n", + " canvas_div.keydown('key_press', canvas_keyboard_event);\n", + " canvas_div.keyup('key_release', canvas_keyboard_event);\n", + " this.canvas_div = canvas_div\n", + " this._canvas_extra_style(canvas_div)\n", + " this.root.append(canvas_div);\n", + "\n", + " var canvas = $('');\n", + " canvas.addClass('mpl-canvas');\n", + " canvas.attr('style', \"left: 0; top: 0; z-index: 0; outline: 0\")\n", + "\n", + " this.canvas = canvas[0];\n", + " this.context = canvas[0].getContext(\"2d\");\n", + "\n", + " var backingStore = this.context.backingStorePixelRatio ||\n", + "\tthis.context.webkitBackingStorePixelRatio ||\n", + "\tthis.context.mozBackingStorePixelRatio ||\n", + "\tthis.context.msBackingStorePixelRatio ||\n", + "\tthis.context.oBackingStorePixelRatio ||\n", + "\tthis.context.backingStorePixelRatio || 1;\n", + "\n", + " mpl.ratio = (window.devicePixelRatio || 1) / backingStore;\n", + "\n", + " var rubberband = $('');\n", + " rubberband.attr('style', \"position: absolute; left: 0; top: 0; z-index: 1;\")\n", + "\n", + " var pass_mouse_events = true;\n", + "\n", + " canvas_div.resizable({\n", + " start: function(event, ui) {\n", + " pass_mouse_events = false;\n", + " },\n", + " resize: function(event, ui) {\n", + " fig.request_resize(ui.size.width, ui.size.height);\n", + " },\n", + " stop: function(event, ui) {\n", + " pass_mouse_events = true;\n", + " fig.request_resize(ui.size.width, ui.size.height);\n", + " },\n", + " });\n", + "\n", + " function mouse_event_fn(event) {\n", + " if (pass_mouse_events)\n", + " return fig.mouse_event(event, event['data']);\n", + " }\n", + "\n", + " rubberband.mousedown('button_press', mouse_event_fn);\n", + " rubberband.mouseup('button_release', mouse_event_fn);\n", + " // Throttle sequential mouse events to 1 every 20ms.\n", + " rubberband.mousemove('motion_notify', mouse_event_fn);\n", + "\n", + " rubberband.mouseenter('figure_enter', mouse_event_fn);\n", + " rubberband.mouseleave('figure_leave', mouse_event_fn);\n", + "\n", + " canvas_div.on(\"wheel\", function (event) {\n", + " event = event.originalEvent;\n", + " event['data'] = 'scroll'\n", + " if (event.deltaY < 0) {\n", + " event.step = 1;\n", + " } else {\n", + " event.step = -1;\n", + " }\n", + " mouse_event_fn(event);\n", + " });\n", + "\n", + " canvas_div.append(canvas);\n", + " canvas_div.append(rubberband);\n", + "\n", + " this.rubberband = rubberband;\n", + " this.rubberband_canvas = rubberband[0];\n", + " this.rubberband_context = rubberband[0].getContext(\"2d\");\n", + " this.rubberband_context.strokeStyle = \"#000000\";\n", + "\n", + " this._resize_canvas = function(width, height) {\n", + " // Keep the size of the canvas, canvas container, and rubber band\n", + " // canvas in synch.\n", + " canvas_div.css('width', width)\n", + " canvas_div.css('height', height)\n", + "\n", + " canvas.attr('width', width * mpl.ratio);\n", + " canvas.attr('height', height * mpl.ratio);\n", + " canvas.attr('style', 'width: ' + width + 'px; height: ' + height + 'px;');\n", + "\n", + " rubberband.attr('width', width);\n", + " rubberband.attr('height', height);\n", + " }\n", + "\n", + " // Set the figure to an initial 600x600px, this will subsequently be updated\n", + " // upon first draw.\n", + " this._resize_canvas(600, 600);\n", + "\n", + " // Disable right mouse context menu.\n", + " $(this.rubberband_canvas).bind(\"contextmenu\",function(e){\n", + " return false;\n", + " });\n", + "\n", + " function set_focus () {\n", + " canvas.focus();\n", + " canvas_div.focus();\n", + " }\n", + "\n", + " window.setTimeout(set_focus, 100);\n", + "}\n", + "\n", + "mpl.figure.prototype._init_toolbar = function() {\n", + " var fig = this;\n", + "\n", + " var nav_element = $('
')\n", + " nav_element.attr('style', 'width: 100%');\n", + " this.root.append(nav_element);\n", + "\n", + " // Define a callback function for later on.\n", + " function toolbar_event(event) {\n", + " return fig.toolbar_button_onclick(event['data']);\n", + " }\n", + " function toolbar_mouse_event(event) {\n", + " return fig.toolbar_button_onmouseover(event['data']);\n", + " }\n", + "\n", + " for(var toolbar_ind in mpl.toolbar_items) {\n", + " var name = mpl.toolbar_items[toolbar_ind][0];\n", + " var tooltip = mpl.toolbar_items[toolbar_ind][1];\n", + " var image = mpl.toolbar_items[toolbar_ind][2];\n", + " var method_name = mpl.toolbar_items[toolbar_ind][3];\n", + "\n", + " if (!name) {\n", + " // put a spacer in here.\n", + " continue;\n", + " }\n", + " var button = $('');\n", + " button.click(method_name, toolbar_event);\n", + " button.mouseover(tooltip, toolbar_mouse_event);\n", + " nav_element.append(button);\n", + " }\n", + "\n", + " // Add the status bar.\n", + " var status_bar = $('');\n", + " nav_element.append(status_bar);\n", + " this.message = status_bar[0];\n", + "\n", + " // Add the close button to the window.\n", + " var buttongrp = $('
');\n", + " var button = $('');\n", + " button.click(function (evt) { fig.handle_close(fig, {}); } );\n", + " button.mouseover('Stop Interaction', toolbar_mouse_event);\n", + " buttongrp.append(button);\n", + " var titlebar = this.root.find($('.ui-dialog-titlebar'));\n", + " titlebar.prepend(buttongrp);\n", + "}\n", + "\n", + "mpl.figure.prototype._root_extra_style = function(el){\n", + " var fig = this\n", + " el.on(\"remove\", function(){\n", + "\tfig.close_ws(fig, {});\n", + " });\n", + "}\n", + "\n", + "mpl.figure.prototype._canvas_extra_style = function(el){\n", + " // this is important to make the div 'focusable\n", + " el.attr('tabindex', 0)\n", + " // reach out to IPython and tell the keyboard manager to turn it's self\n", + " // off when our div gets focus\n", + "\n", + " // location in version 3\n", + " if (IPython.notebook.keyboard_manager) {\n", + " IPython.notebook.keyboard_manager.register_events(el);\n", + " }\n", + " else {\n", + " // location in version 2\n", + " IPython.keyboard_manager.register_events(el);\n", + " }\n", + "\n", + "}\n", + "\n", + "mpl.figure.prototype._key_event_extra = function(event, name) {\n", + " var manager = IPython.notebook.keyboard_manager;\n", + " if (!manager)\n", + " manager = IPython.keyboard_manager;\n", + "\n", + " // Check for shift+enter\n", + " if (event.shiftKey && event.which == 13) {\n", + " this.canvas_div.blur();\n", + " event.shiftKey = false;\n", + " // Send a \"J\" for go to next cell\n", + " event.which = 74;\n", + " event.keyCode = 74;\n", + " manager.command_mode();\n", + " manager.handle_keydown(event);\n", + " }\n", + "}\n", + "\n", + "mpl.figure.prototype.handle_save = function(fig, msg) {\n", + " fig.ondownload(fig, null);\n", + "}\n", + "\n", + "\n", + "mpl.find_output_cell = function(html_output) {\n", + " // Return the cell and output element which can be found *uniquely* in the notebook.\n", + " // Note - this is a bit hacky, but it is done because the \"notebook_saving.Notebook\"\n", + " // IPython event is triggered only after the cells have been serialised, which for\n", + " // our purposes (turning an active figure into a static one), is too late.\n", + " var cells = IPython.notebook.get_cells();\n", + " var ncells = cells.length;\n", + " for (var i=0; i= 3 moved mimebundle to data attribute of output\n", + " data = data.data;\n", + " }\n", + " if (data['text/html'] == html_output) {\n", + " return [cell, data, j];\n", + " }\n", + " }\n", + " }\n", + " }\n", + "}\n", + "\n", + "// Register the function which deals with the matplotlib target/channel.\n", + "// The kernel may be null if the page has been refreshed.\n", + "if (IPython.notebook.kernel != null) {\n", + " IPython.notebook.kernel.comm_manager.register_target('matplotlib', mpl.mpl_figure_comm);\n", + "}\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "name": "stdout", "output_type": "stream", "text": [ - "transit time 1.05 remain time 2.45\n", - "transit time 1.0 remain time 1.45\n", - "transit time 1.45 remain time 0.0\n", + "transit time 1.1 remain time 2.4\n", + "transit time 1.05 remain time 1.35\n", + "transit time 1.35 remain time 0.0\n", "Verification Begin\n", "===============================================\n", "Mode: 0\n", @@ -92,7 +887,7 @@ "Delta: [0.5]\n", "\n", "current mode label: On\n", - "Off 1.0 [[82.88479750557151], [84.83713438129338]] And(t>1.0,t<=1.1)\n", + "Off 1.0 [[82.88456683811637], [85.26238232238468]] And(t>1.0,t<=1.1)\n", "Mode 0 check bloated tube safe\n", "Child exist in cur mode inital 1 is curModeStack Now\n", "===============================================\n", @@ -100,12 +895,12 @@ "stack size: 1\n", "remainTime: 2.5\n", "\n", - "Lower Bound: [82.88479750557151]\n", - "Upper Bound: [84.83713438129338]\n", - "Delta: [0.9761684378609345]\n", + "Lower Bound: [82.88456683811637]\n", + "Upper Bound: [85.26238232238468]\n", + "Delta: [1.1889077421341554]\n", "\n", "current mode label: Off\n", - "On 1.0 [[73.88070144522607], [76.76017197110366]] And(t>1.0,t<=1.1)\n", + "On 1.0 [[73.88049583544938], [77.14415877097372]] And(t>1.0,t<=1.1)\n", "Mode 1 check bloated tube safe\n", "Child exist in cur mode inital 2 is curModeStack Now\n", "===============================================\n", @@ -113,9 +908,9 @@ "stack size: 1\n", "remainTime: 1.5\n", "\n", - "Lower Bound: [73.88070144522607]\n", - "Upper Bound: [76.76017197110366]\n", - "Delta: [1.4397352629387967]\n", + "Lower Bound: [73.88049583544938]\n", + "Upper Bound: [77.14415877097372]\n", + "Delta: [1.6318314677621686]\n", "\n", "current mode label: On\n", "Mode 2 check bloated tube safe\n", @@ -125,9 +920,19 @@ "back flag safe from 1 to 0\n", "No child in prev mode initial, pop, 0 is curModeStack Now\n", "System is Safe!\n", - "simulation time 0.0378980636597\n", - "verification time 0.317549943924\n" + "simulation time 0.343491077423\n", + "verification time 3.9116358757\n" ] + }, + { + "data": { + "text/plain": [ + "" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ diff --git a/output/Traj.txt b/output/Traj.txt index 466882a..1ba73f2 100644 --- a/output/Traj.txt +++ b/output/Traj.txt @@ -1,73 +1,73 @@ -0.0 75.36513494111749 -0.05 75.74290472019997 -0.1 76.12256805264495 -0.15 76.50413412129275 -0.2 76.8876125779359 -0.25 77.27301334178641 -0.3 77.66034593510459 -0.35 78.04962003929238 -0.4 78.44084538715921 -0.45 78.83403176075774 -0.5 79.2291889893958 -0.55 79.6263269518851 -0.6 80.02545557669117 -0.65 80.42658484205006 -0.7 80.82972477621979 -0.75 81.23488545772014 -0.8 81.64207701558806 -0.85 82.05130962963354 -0.9 82.46259353069325 -0.95 82.87593900088615 -1.0 83.29135637387051 -1.05 83.70885603510236 -1.1 84.12844842209492 -1.1 84.55014402467971 -1.15 84.12844790272061 -1.2 83.70885503178842 -1.25 83.29135526422652 -1.3 82.87593802293648 -1.35 82.46259255970634 -1.4 82.0513086656841 -1.45 81.64207605667998 -1.5 81.23488450289511 -1.55 80.82972382600354 -1.6 80.42658389656496 -1.65 80.02545463591274 -1.7 79.62632601579885 -1.75 79.22918805798723 -1.8 78.83403083400262 -1.85 78.44084446489346 -1.9 78.04961912098125 -1.95 77.66034502161216 -2.0 77.27301243491343 -2.05 76.88761167755021 -2.1 76.50413311448351 -2.1 76.12256715872924 -2.15 76.50413358731487 -2.2 76.88761259977169 -2.25 77.27301347130742 -2.3 77.6603459505988 -2.35 78.04962005661837 -2.4 78.44084540731505 -2.45 78.83403178139055 -2.5 79.22918900947046 -2.55 79.62632697191884 -2.6 80.0254555968297 -2.65 80.4265848622985 -2.7 80.82972479657344 -2.75 81.23488547817355 -2.8 81.64207703614251 -2.85 82.0513096502909 -2.9 82.46259355145418 -2.95 82.87593902175118 -3.0 83.29135639484016 -3.05 83.70885605617713 -3.1 84.12844844327533 -3.15 84.55014404596632 -3.2 84.9739534066621 -3.25 85.39988712061879 -3.3 85.82795583620141 -3.35 86.25817025515012 -3.4 86.69054113284781 -3.45 87.12507927858898 -3.5 87.56179555584988 +0.0 75.24412111137498 +0.05 75.6212843054687 +0.1 76.00033801218457 +0.15 76.38129140066859 +0.2 76.76415410563315 +0.25 77.14893603131273 +0.3 77.53564668452083 +0.35 77.92429573111482 +0.4 78.31489288827342 +0.45 78.70744792234404 +0.5 79.10197064685157 +0.55 79.49847092474518 +0.6 79.89695866854822 +0.65 80.29744384047468 +0.7 80.69993645268023 +0.75 81.10444656750153 +0.8 81.51098429771133 +0.85 81.91955980677393 +0.9 82.33018330909835 +0.95 82.7428650702935 +1.0 83.15761540742494 +1.0 83.57444468927271 +1.05 83.15761489440445 +1.1 82.7428640784181 +1.15 82.33018221420025 +1.2 81.91955884152385 +1.25 81.51098333933682 +1.3 81.1044456160758 +1.35 80.69993550622641 +1.4 80.29744289804951 +1.45 79.89695773067004 +1.5 79.49846999154036 +1.55 79.10196971830106 +1.6 78.70744699842905 +1.65 78.31489196883592 +1.7 77.92429481562 +1.75 77.53564577383167 +1.8 77.14893512722588 +1.85 76.76415320801647 +1.9 76.38129039663538 +1.95 76.00033712149241 +2.0 75.62128385873584 +2.05 75.24412113201433 +2.05 74.8688395122401 +2.1 75.244121596894 +2.15 75.62128476583325 +2.2 76.00033813992002 +2.25 76.38129130965865 +2.3 76.76415412757744 +2.35 77.14893605345601 +2.4 77.53564670494087 +2.45 77.92429575075286 +2.5 78.31489290852511 +2.55 78.70744794283736 +2.6 79.10197066744756 +2.65 79.49847094544012 +2.7 79.8969586893423 +2.75 80.2974438613739 +2.8 80.69993647368553 +2.85 81.10444658861223 +2.9 81.51098431892787 +2.95 81.91955982809682 +3.0 82.33018333052813 +3.05 82.74286509183072 +3.1 83.15761542907016 +3.15 83.57444471102646 +3.2 83.99336335845337 +3.25 84.41438184433886 +3.3 84.83751069416705 +3.35 85.26276048618121 +3.4 85.6901418516483 +3.45 86.11966547512472 +3.5 86.55134209472342 diff --git a/playground/.ipynb_checkpoints/GraphProgressPlotter-checkpoint.ipynb b/playground/.ipynb_checkpoints/GraphProgressPlotter-checkpoint.ipynb index a90a622..6b27e22 100644 --- a/playground/.ipynb_checkpoints/GraphProgressPlotter-checkpoint.ipynb +++ b/playground/.ipynb_checkpoints/GraphProgressPlotter-checkpoint.ipynb @@ -2,16 +2,9 @@ "cells": [ { "cell_type": "code", - "execution_count": 32, + "execution_count": 4, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Warning: Cannot change to a different GUI toolkit: notebook. Using nbagg instead.\n" - ] - }, { "data": { "application/javascript": [ @@ -795,7 +788,7 @@ { "data": { "text/html": [ - "" + "" ], "text/plain": [ "" @@ -803,6 +796,14 @@ }, "metadata": {}, "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[('A', 'C'), ('E', 'C')]\n", + "[]\n" + ] } ], "source": [ @@ -815,16 +816,17 @@ "ax = fig.add_subplot(111)\n", "\n", "def draw(red_edges):\n", + " ax.clear()\n", " print(red_edges)\n", " G = nx.DiGraph()\n", " G.add_edges_from(\n", " [('A', 'B'), ('A', 'C'), ('D', 'B'), ('E', 'C'), ('E', 'F'),\n", - " ('B', 'H'), ('B', 'G'), ('B', 'F'), ('C', 'G')])\n", + " ('B', 'H'), ('B', 'G'), ('B', 'F')])\n", "\n", " val_map = {'A': 1.0,\n", " 'D': 0.5714285714285714,\n", " 'H': 0.0}\n", - " red_edges = [('A', 'C'), ('E', 'C')]\n", + "# red_edges = [('A', 'C'), ('E', 'C')]\n", "\n", " values = [val_map.get(node, 0.25) for node in G.nodes()]\n", "\n", @@ -839,13 +841,13 @@ " nx.draw_networkx_nodes(G, pos, cmap=plt.get_cmap('jet'), node_size = 500)\n", " nx.draw_networkx_labels(G, pos)\n", " nx.draw_networkx_edges(G, pos, edgelist=red_edges, edge_color='r', arrows=True)\n", - " nx.draw_networkx_edges(G, pos, edgelist=black_edges, arrows=False)\n", + " nx.draw_networkx_edges(G, pos, edgelist=black_edges, arrows=True)\n", "\n", - "plt.show() \n", "red_edges_1 = [('A', 'C'), ('E', 'C')]\n", "red_edges_2 = []\n", "draw(red_edges_1)\n", - "ax.clear()\n", + "fig.canvas.draw()\n", + "time.sleep(2)\n", "draw(red_edges_2)\n", "\n" ] diff --git a/playground/GraphProgressPlotter.ipynb b/playground/GraphProgressPlotter.ipynb index df0ea0a..4333d26 100644 --- a/playground/GraphProgressPlotter.ipynb +++ b/playground/GraphProgressPlotter.ipynb @@ -2,16 +2,9 @@ "cells": [ { "cell_type": "code", - "execution_count": 41, + "execution_count": 8, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Warning: Cannot change to a different GUI toolkit: notebook. Using nbagg instead.\n" - ] - }, { "data": { "application/javascript": [ @@ -795,7 +788,7 @@ { "data": { "text/html": [ - "" + "" ], "text/plain": [ "" @@ -803,14 +796,6 @@ }, "metadata": {}, "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[('A', 'C'), ('E', 'C')]\n", - "[]\n" - ] } ], "source": [ @@ -822,12 +807,13 @@ "fig = plt.figure()\n", "ax = fig.add_subplot(111)\n", "\n", - "def draw(red_edges):\n", - " print(red_edges)\n", - " G = nx.DiGraph()\n", - " G.add_edges_from(\n", - " [('A', 'B'), ('A', 'C'), ('D', 'B'), ('E', 'C'), ('E', 'F'),\n", - " ('B', 'H'), ('B', 'G'), ('B', 'F'), ('C', 'G')])\n", + "def draw(red_edges, G, pos):\n", + " ax.clear()\n", + "# print(red_edges)\n", + "# G = nx.DiGraph()\n", + "# G.add_edges_from(\n", + "# [('A', 'B'), ('A', 'C'), ('D', 'B'), ('E', 'C'), ('E', 'F'),\n", + "# ('B', 'H'), ('B', 'G'), ('B', 'F')])\n", "\n", " val_map = {'A': 1.0,\n", " 'D': 0.5714285714285714,\n", @@ -843,20 +829,24 @@ "\n", " # Need to create a layout when doing\n", " # separate calls to draw nodes and edges\n", - " pos = nx.spring_layout(G)\n", + "# pos = nx.spring_layout(G)\n", " nx.draw_networkx_nodes(G, pos, cmap=plt.get_cmap('jet'), node_size = 500)\n", " nx.draw_networkx_labels(G, pos)\n", " nx.draw_networkx_edges(G, pos, edgelist=red_edges, edge_color='r', arrows=True)\n", - " nx.draw_networkx_edges(G, pos, edgelist=black_edges, arrows=False)\n", - " plt.show() \n", + " nx.draw_networkx_edges(G, pos, edgelist=black_edges, arrows=True)\n", + " fig.canvas.draw()\n", + "\n", + "G = nx.DiGraph()\n", + "G.add_edges_from(\n", + " [('A', 'B'), ('A', 'C'), ('D', 'B'), ('E', 'C'), ('E', 'F'),\n", + " ('B', 'H'), ('B', 'G'), ('B', 'F')])\n", + "pos = nx.spring_layout(G)\n", "\n", "red_edges_1 = [('A', 'C'), ('E', 'C')]\n", "red_edges_2 = []\n", - "draw(red_edges_1)\n", - "fig.canvas.draw()\n", + "draw(red_edges_1, G ,pos)\n", "time.sleep(2)\n", - "ax.clear()\n", - "draw(red_edges_2)\n", + "draw(red_edges_2, G, pos)\n", "\n" ] }, diff --git a/src/common/utils.py b/src/common/utils.py index c5e9de1..042624d 100644 --- a/src/common/utils.py +++ b/src/common/utils.py @@ -243,3 +243,16 @@ def checkSynthesisInput(data): if data["bloatingMethod"] == "PW": assert 'kvalue' in data, "kvalue need to be provided when bloating method set to PW" + +def isIpynb(): + """ + Check if the code is running on Ipython notebook + """ + try: + cfg = get_ipython().config + if "IPKernelApp" in cfg: + return True + else: + return False + except NameError: + return False diff --git a/src/core/dryvrmain.py b/src/core/dryvrmain.py index c577e14..3b061eb 100644 --- a/src/core/dryvrmain.py +++ b/src/core/dryvrmain.py @@ -6,10 +6,11 @@ from src.common.constant import * from src.common.io import parseVerificationInputFile, writeReachTubeFile, parseRrtInputFile, writeRrtResultFile -from src.common.utils import importSimFunction, randomPoint, buildModeStr +from src.common.utils import importSimFunction, randomPoint, buildModeStr, isIpynb from src.core.distance import DistChecker from src.core.dryvrcore import * from src.core.goalchecker import GoalChecker +from src.core.graph import Graph from src.core.guard import Guard from src.core.initialset import InitialSet from src.core.initialsetstack import InitialSetStack, GraphSearchNode @@ -39,6 +40,9 @@ def verify(data, simFunction): params.resets ) + # Build the progress graph for jupyter notebook + progressGraph = Graph(params, isIpynb()) + # Make sure the initial mode is specfieid if the graph is dag # FIXME should move this part to input check # Bolun 02/12/2018 @@ -143,6 +147,8 @@ def verify(data, simFunction): print "current mode label:",curLabel curSuccessors = graph.successors(curVertex) curInitial = [curStack[-1].lowerBound, curStack[-1].upperBound] + # Update the progress graph + progressGraph.update(buildModeStr(graph, curVertex), curModeStack.bloatedTube[0], curModeStack.remainTime) if len(curSuccessors) == 0: # If there is not successor diff --git a/src/core/graph.py b/src/core/graph.py new file mode 100644 index 0000000..3a0ec47 --- /dev/null +++ b/src/core/graph.py @@ -0,0 +1,73 @@ +""" +This file contains graph class for DryVR +""" +import matplotlib.pyplot as plt +import networkx as nx + + +class Graph(): + """ + This is class to plot the progress graph for dryvr's + function, it is supposed to display the graph in jupyter + notebook and update the graph as dryvr is running + """ + def __init__(self, params, isIpynb): + """ + Guard checker class initialization function. + + Args: + params (obj): An object contains the parameter + isIpynb (bool): check if the code is running on ipython or not + """ + vertex = [] + # Build unique identifier for a vertex and mode name + for idx,v in enumerate(params.vertex): + vertex.append(v+","+str(idx)) + + edges = params.edge + self.edgeList = [] + for e in edges: + self.edgeList.append((vertex[e[0]], vertex[e[1]])) + # Initialize the plot + self.fig = plt.figure() + self.ax = self.fig.add_subplot(111) + + # Initialize the graph + self.G = nx.DiGraph() + self.G.add_edges_from(self.edgeList) + self.pos = nx.spring_layout(self.G) + self.colors = ['green'] * len(self.G.nodes()) + self.fig.suptitle('', fontsize=10) + # Draw the graph when initialize + self.draw() + if isIpynb: + plt.show() + + + + def draw(self): + """ + Draw the white-box transition graph. + """ + + # Delete old plot + nx.draw_networkx_nodes(self.G, self.pos, node_color=self.colors, cmap=plt.get_cmap('jet'), node_size = 1000) + nx.draw_networkx_labels(self.G, self.pos) + nx.draw_networkx_edges(self.G, self.pos, edge_color='b', arrows=True) + self.fig.canvas.draw() + + def update(self, curNode, title, remainTime): + """ + update the graph + Args: + curNode (str): current vertice dryvr is verifiying + title (str): current transition path as the title + remainTime (float): remaining time + """ + self.ax.clear() + self.colors = ['green'] * len(self.G.nodes()) + self.colors[list(self.G.nodes()).index(curNode)] = 'red' + self.fig.suptitle(title, fontsize=10) + self.ax.set_title("remain:"+str(remainTime)) + self.draw() + diff --git a/src/core/reachtube.py b/src/core/reachtube.py index 16bc0da..b98c957 100644 --- a/src/core/reachtube.py +++ b/src/core/reachtube.py @@ -20,8 +20,6 @@ def __init__(self, tube, variables, modes): self.tube = tube self.variables = variables self.modes = modes - print(variables) - print(modes) # Build the raw string representation so user can print it