fix first version of interactive shell

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

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

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

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()
+

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