Skip to content

Commit

Permalink
finish demo
Browse files Browse the repository at this point in the history
  • Loading branch information
qibolun committed Apr 7, 2018
1 parent d4d2fc4 commit 8e01964
Show file tree
Hide file tree
Showing 8 changed files with 6,542 additions and 337 deletions.
Binary file modified .DS_Store
Binary file not shown.
2,188 changes: 2,184 additions & 4 deletions .ipynb_checkpoints/GraphSearchNotebook-checkpoint.ipynb

Large diffs are not rendered by default.

1,240 changes: 1,078 additions & 162 deletions .ipynb_checkpoints/VerificationNotebook-checkpoint.ipynb

Large diffs are not rendered by default.

2,188 changes: 2,184 additions & 4 deletions GraphSearchNotebook.ipynb

Large diffs are not rendered by default.

1,240 changes: 1,078 additions & 162 deletions VerificationNotebook.ipynb

Large diffs are not rendered by default.

13 changes: 9 additions & 4 deletions input/daginput/input_autopassingSimpleSafe.json
@@ -1,14 +1,19 @@
{
"vertex":["Acc1;Const","TurnLeft;Const","Acc1;Const","Dec;Const","TurnRight;Const","Const;Const"],
"edge":[[0,1],[1,2],[2,3],[3,4],[4,5]],
"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(t>=5.0, t<=6.0)",
"And(t>=5.0, t<=6.0)",
"And(car2_y-car1_y>=10,car2_y-car1_y<=10.1)",
"And(t>10.0,t<=12.0)"
],
"resets":[
"",
"",
"car1_vy=1.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":50.0,
Expand Down
8 changes: 7 additions & 1 deletion main.py
Expand Up @@ -4,8 +4,14 @@
from src.core.dryvrmain import verify
from src.common.utils import importSimFunction

from src.plotter.parser import parse


assert ".json" in sys.argv[-1], "Please provide json input file"
with open(sys.argv[-1], 'r') as f:
data = json.load(f)
simFunction = importSimFunction(data["directory"])
verify(data, simFunction)
safey, reach = verify(data, simFunction)
lines = reach.raw.split("\n")
print type(lines[0]), lines[0]
initNode, y_min, y_max= parse(lines)
2 changes: 2 additions & 0 deletions src/plotter/parser.py
Expand Up @@ -38,6 +38,8 @@ def parse(data):

else:
line = map(float,line.strip().split())
if len(line)<=1:
continue
if LOWER:
LOWER = False
# This data appered in lowerBound before, concat the data
Expand Down

0 comments on commit 8e01964

Please sign in to comment.