fix bug in hybrid simulation

qibolun · Mar 29, 2018 · 1247e15 · 1247e15
1 parent 3c47b6f
commit 1247e15
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 5 deletions.
diff --git a/input/PathPrediction/v8_acc.json b/input/PathPrediction/v8_acc.json
@@ -0,0 +1,17 @@
+{
+    "vertex": ["Acc1;Const","Const;Const"],
+    "edge": [[0,1]],
+    "variables":["car1_x","car1_y","car1_vx","car1_vy","car2_x","car2_y","car2_vx","car2_vy"],
+    "guards": [
+        "car1_y == car2_y"
+    ],
+    "resets": [
+        "car1_vy = 1.0"
+    ],
+    "initialSet":[[-3.0,-1.0,0.0,1.0,0.0,-22.0,0.0,1.0],[-3.0,-0.9,0.0,1.0,0.0,-21.9,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":30.0,
+    "directory":"examples/cars",
+    "bloatingMethod":"PW",
+    "kvalue":[2,2,2,2,2,2,2,2]
+}
diff --git a/src/core/dryvrcore.py b/src/core/dryvrcore.py
@@ -143,7 +143,7 @@ def simulate(g, initCondition, timeHorizon, guard, simFuc, reseter, initialVerte
 
 		if len(curSuccessors) == 0:
 			# Some model return numpy array, convert to list
-			initCondition, trunckedResult = guard.guardSimuTube(
+			initCondition, trunckedResult = guard.guardSimuTrace(
 				curSimResult,
 				None
 			)
@@ -158,7 +158,7 @@ def simulate(g, initCondition, timeHorizon, guard, simFuc, reseter, initialVerte
 				curGuardStr = g.es[edgeID]['guards']
 				curResetStr = g.es[edgeID]['resets']
 
-				nextInit, trunckedResult = guard.guardSimuTube(
+				nextInit, trunckedResult = guard.guardSimuTrace(
 					curSimResult,
 					curGuardStr
 				)

diff --git a/src/core/guard.py b/src/core/guard.py
@@ -55,7 +55,7 @@ def _buildGuard(self, guardStr):
         curSolver.add(eval(guardStr))
         return curSolver, symbolsIdx
 
-    def guardSimuTube(self, trace, guardStr):
+    def guardSimuTrace(self, trace, guardStr):
         """
         Check the guard for simulation trace.
         Note we treat the simulation trace as the set as well.
@@ -96,7 +96,7 @@ def guardSimuTube(self, trace, guardStr):
             curSolver.push()
             for symbol in symbols:
                 curSolver.add(self.varDic[symbol] >= min(lower[symbols[symbol]], upper[symbols[symbol]]))
-                curSolver.add(self.varDic[symbol] <= max(upper[symbols[symbol]], upper[symbols[symbol]]))
+                curSolver.add(self.varDic[symbol] <= max(lower[symbols[symbol]], upper[symbols[symbol]]))
             if curSolver.check() == sat:
                 curSolver.pop()
                 guardSet[idx] = upper
@@ -123,7 +123,7 @@ def guardSimuTraceTime(self, trace, guardStr):
         Returns:
             the length of the truncated traces.
         """
-        nextInit, trace = self.guardSimuTube(trace, guardStr)
+        nextInit, trace = self.guardSimuTrace(trace, guardStr)
         return len(trace)