add two case study

input/casestudy/input_2car_overtake.json

@@ -0,0 +1,17 @@
+{
+	"vertex":["Acc1;Const","TurnLeft;Const","Acc1;Const","TurnRight;Const","Const;Const"],
+	"edge":[[0,1],[1,2],[2,3],[3,4]],
+	"variables":["car1_x","car1_y","car1_vx","car1_vy","car2_x","car2_y","car2_vx","car2_vy"],
+	"guards":[
+		"And(car1_y-car2_y>=10,car1_y-car2_y<=10.1)",
+		"And(t>10.0,t<=12.0)",
+		"And(car2_y-car1_y>=10,car2_y-car1_y<=10.1)",
+		"And(t>10.0,t<=12.0)"
+	],
+	"initialSet":[[0.0,0.5,0.0,1.0,0.0,-17.0,0.0,1.0],[0.0,1.0,0.0,1.0,0.0,-16.5,0.0,1.0]],
+	"unsafeSet":"@Allmode:And(car1_x-car2_x<2, car2_x-car1_x<2, car1_y-car2_y<2, car2_y-car1_y<2)",
+	"timeHorizon":40.0,
+	"directory":"examples/cars",
+	"bloatingMethod":"PW",
+    "kvalue":[2,2,2,2,2,2,2,2]
+}

input/casestudy/input_3car_mergeinbetween.json

@@ -0,0 +1,40 @@
+{
+	"vertex":[
+		"Acc1;Const;Const",
+		"TurnRight;Const;Const",
+		"Const;Const;Const",
+		"Dec;Acc1;Const",
+		"TurnRight;Const;Const"
+	],
+	"edge":[[0,1],[1,2],[0,3],[3,4],[4,2]],
+	"variables":[
+		"car1_x",
+		"car1_y",
+		"car1_vx",
+		"car1_vy",
+		"car2_x",
+		"car2_y",
+		"car2_vx",
+		"car2_vy",
+		"car3_x", 
+		"car3_y", 
+		"car3_vx",
+		"car3_vy"
+	],
+	"guards":[
+		"And(car2_y-car1_y>=10,car2_y-car1_y<=10.1)",
+		"And(t>10.0,t<=12.0)",
+		"And(t>8.0,t<=8.5)",
+		"And(car1_y-car2_y>=10,car1_y-car2_y<=10.1)",
+		"And(t>10.0,t<=12.0)"
+	],
+	"initialSet":[
+		[-3.0,0.5,0.0,1.0,0.0,-17.0,0.0,1.0,0.0,-45.0,0.0,1.0],
+		[-3.0,1.0,0.0,1.0,0.0,-16.5,0.0,1.0,0.0,-44.0,0.0,1.0]
+	],
+	"unsafeSet":"@Allmode:Or(And(car1_x-car2_x<2, car2_x-car1_x<2, car1_y-car2_y<2, car2_y-car1_y<2), And(car1_x-car3_x<2, car3_x-car1_x<2, car1_y-car3_y<2, car3_y-car1_y<2))",
+	"timeHorizon":20.0,
+	"directory":"examples/cars",
+	"bloatingMethod":"PW",
+    "kvalue":[2,2,2,2,2,2,2,2,2,2,2,2]
+}

input/daginput/input_autopassingSimpleSafe.json

@@ -11,5 +11,7 @@
 	"initialSet":[[0.0,0.5,0.0,1.0,0.0,-17.0,0.0,1.0],[0.0,1.0,0.0,1.0,0.0,-16.5,0.0,1.0]],
 	"unsafeSet":"@Allmode:And(car1_x-car2_x<2, car2_x-car1_x<2, car1_y-car2_y<2, car2_y-car1_y<2)",
 	"timeHorizon":40.0,
-	"directory":"examples/cars"
+	"directory":"examples/cars",
+	"bloatingMethod":"PW",
+    "kvalue":[2,2,2,2,2,2,2,2]
 }

src/common/constant.py

@@ -11,8 +11,8 @@
 UNSAFE = -1
 UNKNOWN = 0
 NOSTATUS = 99
-BLOATDEBUG = True
-PLOTDIM = 1
+BLOATDEBUG = False
+PLOTDIM = 2
 
 # File Pathes
 GRAPHOUTPUT = 'output/curGraph.png'

src/core/graph.py

@@ -19,6 +19,9 @@ def __init__(self, params, isIpynb):
             params (obj): An object contains the parameter
             isIpynb (bool): check if the code is running on ipython or not
         """
+        self.isIpynb = isIpynb
+        if not isIpynb:
+            return
         vertex = []
         # Build unique identifier for a vertex and mode name
         for idx,v in enumerate(params.vertex):
@@ -40,8 +43,7 @@ def __init__(self, params, isIpynb):
         self.fig.suptitle('', fontsize=10)
         # Draw the graph when initialize
         self.draw()
-        if isIpynb:
-            plt.show()
+        plt.show()
 
 
 
@@ -69,6 +71,8 @@ def update(self, curNode, title, remainTime):
             title (str): current transition path as the title
             remainTime (float): remaining time
         """
+        if not self.isIpynb:
+            return
         self.ax.clear()
         self.colors = ['green'] * len(self.G.nodes())
         self.colors[list(self.G.nodes()).index(curNode)] = 'red'