diff --git a/.gitignore b/.gitignore
index 252430f3843d2c7bd04f3304fb10248ca0a8bd2c..28affb7420b24d8cb24638534a99a43d89b56720 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
__pycache__/
**/__pycache__/
-.vscode/
\ No newline at end of file
+.vscode/
+.idea/
\ No newline at end of file
diff --git a/README.md b/README.md
index e4a50bd2e087fa6b2fd3f9c2fcc5c0b08cb8b9a0..90949c79037858bb87d12cf6f7d92856cce1d810 100644
--- a/README.md
+++ b/README.md
@@ -1,35 +1,43 @@
# GraphGeneration
-NOTE: I made a mistake and uploaded the wrong file before I left town today. generateGraph-new.py is outdated! I am so sorry, but it doesn't have the updates the build the graph, it only computes the paths.
+## Installation
+The package requires python 3.8+. All the required packages can be installed through
+```
+python3 -m pip install -r requirements.txt
+```
-working repo for graph generation
+## Examples
+The package comes with two controller examples
+- The first example consists a scenario with a single vehicle, which can perform lane switch based on its location. The
+first example can be run by using command
-generateGraph-new.py has the code that finds paths. It creates a mode for each path through the code and any "mode" in the code is just a variable, not a named mode.
+```
+python3 example_car_lane_switch.py
+```
+- The second example consists a scenario with two vehicles, which can perform lane switch based on their relative position.
+The second example can be run using command
-generateGraph.py has the old code which only allows 2 levels of if statements and isn't as stable. Reads mode variable and sets vertices based on modes. Requires that an if statement checks the mode and the new mode is set within the if statement.
+```
+python3 example_two_car_lane_switch.py
+```
+## Package Structure
+The source code of the package is contained in the src folder, which contains the following sub-directories.
-Run within DryVR directory
+- **scene_verifier**, which contains building blocks for creating and analyzing scenarios.
+
+ - **scene_verifier/scenario** contains code for the scenario base class. A scenario is constructed by several **agents** with continuous dynamics and controller, a **map** and a **sensor** defining how different agents interact with each other.
+ - **scene_verifier/agents** contains code for the agent base class in the scenario.
+ - **scene_verifier/map** contains code for the lane map base class and corresponding utilities in the scenario.
+ - **scene_verifier/code_parser** contains code for converting the controller code to ASTs.
+ - **scene_verifier/automaton** contains code implementing components in hybrid-automaton
+ - **scene_verifier/analysis** contains the **Simulator** and **Verifier** and related utilities for doing analysis of the scenario
+ - **scene_verifier/dryvr** dryvr for computing reachable sets
-Usage:
-model generation only:
+- **example** contains example map, sensor and agents that we provided
-python generateGraph-new.py cfile.c jsonfilewithinitialinfo.json out.json
-
-
-DryVR pipeline (this may not be ready yet, still needs work with mode names):
-
-./fullrun cfile.c jsonfilewithinitialinfo.json out.json
-
-
-
-
-Example:
-
-python generateGraph-new.py cartoy.c singlevehiclesat.json out.json #this toy example was just for looking at nesting, doesn't have an initial json
-
-./full_run singlevehiclesat.c singlevehiclesat.json output.json
+- **plotter** contains code for visualizing the computed results
\ No newline at end of file
diff --git a/billiard_input.json b/billiard_input.json
deleted file mode 100644
index ce0b5c076e89d76ee15184c75a36937f6c748d3b..0000000000000000000000000000000000000000
--- a/billiard_input.json
+++ /dev/null
@@ -1,8 +0,0 @@
-{
- "initialVertex":0,
- "initialSet":[[1.5, 0.0, 1.0, 1.0],[1.51, 0.0, 1.0, 1.0]],
- "unsafeSet":"@Allmode:posy>=12.0",
- "timeHorizon":16,
- "directory":"examples/billiard",
- "deterministic":true
-}
diff --git a/billiard_out.json b/billiard_out.json
deleted file mode 100644
index 7ec65a276cc452a9a8fa220e80465a8d47c795af..0000000000000000000000000000000000000000
--- a/billiard_out.json
+++ /dev/null
@@ -1,135 +0,0 @@
-{
- "initialVertex": 0,
- "initialSet": [
- [
- 1.5,
- 0.0,
- 1.0,
- 1.0
- ],
- [
- 1.51,
- 0.0,
- 1.0,
- 1.0
- ]
- ],
- "unsafeSet": "@Allmode:posy>=12.0",
- "timeHorizon": 16,
- "directory": "examples/billiard",
- "deterministic": true,
- "variables": [
- "posx",
- "posy",
- "vx",
- "vy"
- ],
- "vertex": [
- "NormalA",
- "NormalB",
- "NormalC",
- "NormalD"
- ],
- "edge": [
- [
- 0,
- 0
- ],
- [
- 0,
- 1
- ],
- [
- 0,
- 2
- ],
- [
- 0,
- 3
- ],
- [
- 1,
- 1
- ],
- [
- 1,
- 0
- ],
- [
- 1,
- 2
- ],
- [
- 1,
- 3
- ],
- [
- 2,
- 2
- ],
- [
- 2,
- 0
- ],
- [
- 2,
- 1
- ],
- [
- 2,
- 3
- ],
- [
- 3,
- 3
- ],
- [
- 3,
- 0
- ],
- [
- 3,
- 1
- ],
- [
- 3,
- 2
- ]
- ],
- "guards": [
- "And(posy<0,posy>=-0.01)",
- "And(posx<0,posx>=-0.01)",
- "And(posx<=5.01,posx>5)",
- "And(posy>5,posy<=5.01)",
- "And(posy<0,posy>=-0.01)",
- "And(posx<0,posx>=-0.01)",
- "And(posx<=5.01,posx>5)",
- "And(posy>5,posy<=5.01)",
- "And(posy<0,posy>=-0.01)",
- "And(posx<0,posx>=-0.01)",
- "And(posx<=5.01,posx>5)",
- "And(posy>5,posy<=5.01)",
- "And(posy<0,posy>=-0.01)",
- "And(posx<0,posx>=-0.01)",
- "And(posx<=5.01,posx>5)",
- "And(posy>5,posy<=5.01)"
- ],
- "resets": [
- "vy=-vy;posy=0",
- "vx=-vx;posx=0",
- "vx=-vx;posx=5",
- "vy=-vy;posy=5",
- "vy=-vy;posy=0",
- "vx=-vx;posx=0",
- "vx=-vx;posx=5",
- "vy=-vy;posy=5",
- "vy=-vy;posy=0",
- "vx=-vx;posx=0",
- "vx=-vx;posx=5",
- "vy=-vy;posy=5",
- "vy=-vy;posy=0",
- "vx=-vx;posx=0",
- "vx=-vx;posx=5",
- "vy=-vy;posy=5"
- ]
-}
\ No newline at end of file
diff --git a/billiardsrc.c b/billiardsrc.c
deleted file mode 100644
index 5e56e4814156785b5c85ec88f248c3251a89bd8d..0000000000000000000000000000000000000000
--- a/billiardsrc.c
+++ /dev/null
@@ -1,119 +0,0 @@
-enum modes {NormalA, NormalB, NormalC, NormalD};
-
-struct State {
-int posx;
-int posy;
-int vx;
-int vy;
-enum modes mode;
-};
-
-
-
-struct State P(struct State s) {
- int posx = s.posx;
- int posy = s.posy;
- int vx = s.vx;
- int vy = s.vy;
- enum modes state = s.mode;
- if (state ==NormalA) {
- if (posy<0 && posy>=-0.01) {
- vy=-vy;
- posy=0;
- state=NormalA;
- }
- if (posx<0 && posx>=-0.01) {
- vx=-vx;
- posx=0;
- state=NormalB;
- }
- if (posx<=5.01 && posx>5) {
- vx=-vx;
- posx=5;
- state=NormalC;
- }
- if (posy>5 && posy<=5.01) {
- vy=-vy;
- posy=5;
- state = NormalD;
- }
-
- }
- if (state ==NormalB) {
- if (posy<0 && posy>=-0.01) {
- vy=-vy;
- posy=0;
- state=NormalB;
- }
- if (posx<0 && posx>=-0.01) {
- vx=-vx;
- posx=0;
- state=NormalA;
- }
- if (posx<=5.01 && posx>5) {
- vx=-vx;
- posx=5;
- state=NormalC;
- }
- if (posy>5 && posy<=5.01) {
- vy=-vy;
- posy=5;
- state = NormalD;
- }
-
- }
- if (state ==NormalC) {
- if (posy<0 && posy>=-0.01) {
- vy=-vy;
- posy=0;
- state=NormalC;
- }
- if (posx<0 && posx>=-0.01) {
- vx=-vx;
- posx=0;
- state=NormalA;
- }
- if (posx<=5.01 && posx>5) {
- vx=-vx;
- posx=5;
- state=NormalB;
- }
- if (posy>5 && posy<=5.01) {
- vy=-vy;
- posy=5;
- state = NormalD;
- }
-
- }
-
- if (state ==NormalD) {
- if (posy<0 && posy>=-0.01) {
- vy=-vy;
- posy=0;
- state=NormalD;
- }
- if (posx<0 && posx>=-0.01) {
- vx=-vx;
- posx=0;
- state=NormalA;
- }
- if (posx<=5.01 && posx>5) {
- vx=-vx;
- posx=5;
- state=NormalB;
- }
- if (posy>5 && posy<=5.01) {
- vy=-vy;
- posy=5;
- state = NormalC;
- }
-
- }
- s.posx = posx;
- s.posy= posy;
- s.vx = vx;
- s.vy = vy;
- s.mode = state;
- return s;
-
-}
diff --git a/cartoy-out.json b/cartoy-out.json
deleted file mode 100644
index d12a408bf00d1e227a818344a87bee93bd3e6e09..0000000000000000000000000000000000000000
--- a/cartoy-out.json
+++ /dev/null
@@ -1,89 +0,0 @@
-{
- "unsafeSet": "",
- "initialSet": [
- [
- 0,
- -0.2,
- 0
- ],
- [
- 0,
- 0.2,
- 0
- ]
- ],
- "timeHorizon": 10,
- "directory": "examples/curve_controller_hybrid",
- "initialVertex": 0,
- "deterministic": true,
- "variables": [
- "vx",
- "vy",
- "dist"
- ],
- "vertex": [
- "0",
- "1",
- "2"
- ],
- "edge": [
- [
- "0",
- "0"
- ],
- [
- "1",
- "0"
- ],
- [
- "2",
- "0"
- ],
- [
- "0",
- "1"
- ],
- [
- "1",
- "1"
- ],
- [
- "2",
- "1"
- ],
- [
- "0",
- "2"
- ],
- [
- "1",
- "2"
- ],
- [
- "2",
- "2"
- ]
- ],
- "guards": [
- "And(dist < 10,(And(dist < 2,(state != move_over))))",
- "And(dist < 10,(And(dist < 2,(state != move_over))))",
- "And(dist < 10,(And(dist < 2,(state != move_over))))",
- "And(dist < 10,(And(dist < 2,(dist > 2))))",
- "And(dist < 10,(And(dist < 2,(dist > 2))))",
- "And(dist < 10,(And(dist < 2,(dist > 2))))",
- "And(dist < 10,(state == move_over))",
- "And(dist < 10,(state == move_over))",
- "And(dist < 10,(state == move_over))"
- ],
- "resets": [
- "vy=vy -5;vx= vx + 5",
- "vy=vy -5;vx= vx + 5",
- "vy=vy -5;vx= vx + 5",
- "vx=vx - 5",
- "vx=vx - 5",
- "vx=vx - 5",
- "vx = vx + 5",
- "vx = vx + 5",
- "vx = vx + 5"
- ]
-}
\ No newline at end of file
diff --git a/cartoy.c b/cartoy.c
deleted file mode 100644
index 9c9bcee6b61fd0c73392df5b7f196348d91674d4..0000000000000000000000000000000000000000
--- a/cartoy.c
+++ /dev/null
@@ -1,41 +0,0 @@
-enum modes {go_forward, move_over};
-
-struct State {
-int vx;
-int vy;
-int dist;
-//enum modes mode;
-};
-
-
-
-struct State P(struct State s) {
- int posx = s.posx;
- int posy = s.posy;
- int vx = s.vx;
- int vy = s.vy;
- int dist = s.dist
- enum modes state = s.mode;
- if (dist < 10) {
- if (dist < 2) {
- if (state != move_over) {
- //if super close, slow down and begin move over if we aren't already
- vy=vy -5;
- vx= vx + 5;
- }
- }
- else if (dist > 2) {
- vx=vx - 5;
- }
-
- }
- else if (state == move_over) {
- vx = vx + 5;
-
- }
- s.vx = vx;
- s.vy = vy;
- s.mode = state;
- return s;
-
-}
diff --git a/common_road_vis.py b/common_road_vis.py
deleted file mode 100644
index c0e3c067524512097e40e962fa3cf7e387bdb14b..0000000000000000000000000000000000000000
--- a/common_road_vis.py
+++ /dev/null
@@ -1,39 +0,0 @@
-import matplotlib.pyplot as plt
-import xml.etree.ElementTree as ET
-
-if __name__ == "__main__":
- fn = 'ARG_Carcarana-11_1_T-1.xml'
- tree = ET.parse(fn)
- root = tree.getroot()
-
- lanelet_list = root.findall('lanelet')
- for j in range(len(lanelet_list)):
- example_lanelet = lanelet_list[j]
- left_bound = example_lanelet.find('leftBound')
- right_bound = example_lanelet.find('rightBound')
- leftpoint_list = left_bound.findall('point')
- rightpoint_list = right_bound.findall('point')
- assert(len(leftpoint_list)==len(rightpoint_list))
- left_x = []
- left_y = []
- right_x = []
- right_y = []
- middle_x = []
- middle_y = []
- for i in range(len(leftpoint_list)):
- leftpoint = leftpoint_list[i]
- left_x.append(float(leftpoint.find('x').text))
- left_y.append(float(leftpoint.find('y').text))
-
- rightpoint = rightpoint_list[i]
- right_x.append(float(rightpoint.find('x').text))
- right_y.append(float(rightpoint.find('y').text))
-
- middle_x.append((float(leftpoint.find('x').text)+float(rightpoint.find('x').text))/2)
- middle_y.append((float(leftpoint.find('y').text)+float(rightpoint.find('y').text))/2)
-
- # plt.plot(left_x, left_y,'-*')
- # plt.plot(right_x, right_y,'-*')
- plt.plot(middle_x, middle_y, '-*')
-
- plt.show()
\ No newline at end of file
diff --git a/example_car_lane_switch.py b/example_car_lane_switch.py
index 4d82cba6834770d9474ae28b1063d49d57e2960c..5861a91a770dbdd88bd17a8476fe275c2e507734 100644
--- a/example_car_lane_switch.py
+++ b/example_car_lane_switch.py
@@ -9,44 +9,60 @@ class VehicleMode(Enum):
class LaneMode(Enum):
Lane0 = auto()
-def controller(x,y,theta,v,vehicle_mode, lane_mode):
- output_vehicle_mode = vehicle_mode
- output_lane_mode = lane_mode
- if vehicle_mode == VehicleMode.Normal:
- if lane_mode == LaneMode.Lane0:
- if x > 3 and x < 5:
+class State:
+ x = 0.0
+ y = 0.0
+ theta = 0.0
+ v = 0.0
+ vehicle_mode: VehicleMode = VehicleMode.Normal
+ lane_mode: LaneMode = LaneMode.Lane0
+
+ def __init__(self, x, y, theta, v, vehicle_mode: VehicleMode, lane_mode: LaneMode):
+ self.data = []
+
+def controller(ego:State):
+ output_vehicle_mode = ego.vehicle_mode
+ output_lane_mode = ego.lane_mode
+ if ego.vehicle_mode == VehicleMode.Normal:
+ if ego.lane_mode == LaneMode.Lane0:
+ if ego.x > 3 and ego.x < 5:
output_vehicle_mode = VehicleMode.SwitchLeft
- if x > 3 and x < 5:
+ if ego.x > 3 and ego.x < 5:
output_vehicle_mode = VehicleMode.SwitchRight
- if vehicle_mode == VehicleMode.SwitchLeft:
- if lane_mode == LaneMode.Lane0:
- if x > 10:
+ if ego.vehicle_mode == VehicleMode.SwitchLeft:
+ if ego.lane_mode == LaneMode.Lane0:
+ if ego.x > 10:
output_vehicle_mode = VehicleMode.Normal
- if vehicle_mode == VehicleMode.SwitchRight:
- if lane_mode == LaneMode.Lane0:
- if x > 10:
+ if ego.vehicle_mode == VehicleMode.SwitchRight:
+ if ego.lane_mode == LaneMode.Lane0:
+ if ego.x > 10:
output_vehicle_mode = VehicleMode.Normal
return output_vehicle_mode, output_lane_mode
-from ourtool.agents.car_agent import CarAgent
-from ourtool.scenario.scenario import Scenario
-import matplotlib.pyplot as plt
+from src.example.example_agent.car_agent import CarAgent
+from src.scene_verifier.scenario.scenario import Scenario
+from src.example.example_map.simple_map import SimpleMap2
+from src.example.example_sensor.fake_sensor import FakeSensor1
+import matplotlib.pyplot as plt
import numpy as np
if __name__ == "__main__":
- input_code_name = 'car_lane_switch.py'
+ input_code_name = 'example_car_lane_switch.py'
scenario = Scenario()
car = CarAgent('ego', file_name=input_code_name)
scenario.add_agent(car)
+ scenario.add_map(SimpleMap2())
+ scenario.set_sensor(FakeSensor1())
# simulator = Simulator()
+ scenario.set_init(
+ [[0,3,0,0.5]],
+ [(VehicleMode.Normal, LaneMode.Lane0)]
+ )
+
traces = scenario.simulate(
- [[0,0,0,0.5]],
- [(VehicleMode.Normal, LaneMode.Lane0)],
- [car],
- scenario,
40
)
diff --git a/example_two_car_lane_switch.py b/example_two_car_lane_switch.py
index fe7cce85a89947a5f7e409cf71f62e77287b4efa..c270eb0ca16cbc11f68a301d4c0fa4dd2280fc44 100644
--- a/example_two_car_lane_switch.py
+++ b/example_two_car_lane_switch.py
@@ -1,7 +1,5 @@
from enum import Enum, auto
-from ourtool.map.lane_map import LaneMap
-
class VehicleMode(Enum):
Normal = auto()
@@ -53,13 +51,13 @@ def controller(ego: State, other: State, lane_map):
return output
-from ourtool.agents.car_agent import CarAgent
-from ourtool.scenario.scenario import Scenario
-from user.simple_map import SimpleMap, SimpleMap2
-from plotter.plotter2D import plot_tree
+from src.example.example_agent.car_agent import CarAgent
+from src.scene_verifier.scenario.scenario import Scenario
+from src.example.example_map.simple_map import SimpleMap2
+from src.plotter.plotter2D import plot_tree
+from src.example.example_sensor.fake_sensor import FakeSensor2
import matplotlib.pyplot as plt
-import numpy as np
if __name__ == "__main__":
input_code_name = 'example_two_car_lane_switch.py'
@@ -70,6 +68,7 @@ if __name__ == "__main__":
car = CarAgent('car2', file_name=input_code_name)
scenario.add_agent(car)
scenario.add_map(SimpleMap2())
+ scenario.set_sensor(FakeSensor2())
scenario.set_init(
[
[[10, 0, 0, 0.5],[10, 0, 0, 0.5]],
diff --git a/full_run b/full_run
deleted file mode 100644
index d95c8c760cdf68d3769218a5d627b426853ed023..0000000000000000000000000000000000000000
--- a/full_run
+++ /dev/null
@@ -1,27 +0,0 @@
-#!/bin/bash
-
-START="$(date +%s.%N)"
-
-
-input_code=$1
-input_info=$2
-#output should have path to correct place in dryvr directory
-output=$3
-
-GSTART="$(date +%s.%N)"
-
-python generateGraph-new.py $input_code $input_info $output
-
-GEND="$(date +%s.%N)"
-
-python main.py $output
-
-END="$(date +%s.%N)"
-#DURATION=$[ $'expr (date +%s.%N) - ${START}' ]
-DURATION=$( echo "$END - $START" | bc -l )
-GDURATION=$( echo "$GEND - $GSTART" | bc -l )
-
-echo "Running time of pipeline is"
-echo ${DURATION}
-echo "Running time of model generation is"
-echo ${GDURATION}
diff --git a/generateGraph-new.py b/generateGraph-new.py
deleted file mode 100644
index 849f1464f73a056d863fa1631e7942622866936c..0000000000000000000000000000000000000000
--- a/generateGraph-new.py
+++ /dev/null
@@ -1,483 +0,0 @@
-#NEW VERSION OF CODE WHICH ANALYZES PATHS AND COLLECTS VARAIBLES ALONG THE WAY
-
-import clang.cindex
-import typing
-import json
-import sys
-#from cfg import CFG
-#import clang.cfg
-
-
-#index = clang.cindex.Index.create()
-#translation_unit = index.parse('my_source.c', args=['-std=c99'])
-
-#print all the cursor types
-#for i in translation_unit.get_tokens(extent=translation_unit.cursor.extent):
-# print (i.kind)
-
-#get the structs
-def filter_node_list_by_node_kind(
- nodes: typing.Iterable[clang.cindex.Cursor],
- kinds: list
-) -> typing.Iterable[clang.cindex.Cursor]:
- result = []
- for i in nodes:
- if i.kind in kinds:
- result.append(i)
- return result
-
-#exclude includes
-def filter_node_list_by_file(
- nodes: typing.Iterable[clang.cindex.Cursor],
- file_name: str
-) -> typing.Iterable[clang.cindex.Cursor]:
- result = []
- for i in nodes:
- if i.location.file.name == file_name:
- result.append(i)
- return result
-
-
-#all_classes = filter_node_list_by_node_kind(translation_unit.cursor.get_children(), [clang.cindex.CursorKind.ENUM_DECL, clang.cindex.CursorKind.STRUCT_DECL])
-#for i in all_classes:
-# print (i.spelling)
-
-#captured fields in classes
-def is_exposed_field(node):return node.access_specifier == clang.cindex.AccessSpecifier.PUBLIC
-def find_all_exposed_fields(
- cursor: clang.cindex.Cursor
-):
- result = []
- field_declarations = filter_node_list_by_node_kind(cursor.get_children(), [clang.cindex.CursorKind.FIELD_DECL])
- for i in field_declarations:
- if not is_exposed_field(i):
- continue
- result.append(i.displayname)
- return result
-
-
-def populate_field_list_recursively(class_name: str,class_field_map,class_inheritance_map):
- field_list = class_field_map.get(class_name)
- if field_list is None:
- return []
- baseClasses = class_inheritance_map[class_name]
- for i in baseClasses:
- field_list = populate_field_list_recursively(i.spelling) + field_list
- return field_list
-#rtti_map = {}
-
-
-
-def get_state_variables(translation_unit):
- rtti_map = {}
- source_nodes = filter_node_list_by_file(translation_unit.cursor.get_children(), translation_unit.spelling)
- all_classes = filter_node_list_by_node_kind(source_nodes, [clang.cindex.CursorKind.ENUM_DECL, clang.cindex.CursorKind.STRUCT_DECL])
- class_inheritance_map = {}
- class_field_map = {}
- for i in all_classes:
- bases = []
- for node in i.get_children():
- if node.kind == clang.cindex.CursorKind.CXX_BASE_SPECIFIER:
- referenceNode = node.referenced
- bases.append(node.referenced)
- class_inheritance_map[i.spelling] = bases
- for i in all_classes:
- fields = find_all_exposed_fields(i)
- class_field_map[i.spelling] = fields
- #print("foo")
- for class_name, class_list in class_inheritance_map.items():
- rtti_map[class_name] = populate_field_list_recursively(class_name,class_field_map,class_inheritance_map)
- for class_name, field_list in rtti_map.items():
- rendered_fields = []
- for f in field_list:
- rendered_fields.append(f)
- return rendered_fields
-
-
-
-#def populate_field_list_recursively(class_name: str):
-# field_list = class_field_map.get(class_name)
-# if field_list is None:
-# return []
-# baseClasses = class_inheritance_map[class_name]
-# for i in baseClasses:
-# field_list = populate_field_list_recursively(i.spelling) + field_list
-# return field_list
-#rtti_map = {}
-
-#def get_state_variables():
-# print("foo")
-# for class_name, class_list in class_inheritance_map.items():
-# rtti_map[class_name] = populate_field_list_recursively(class_name)
-# for class_name, field_list in rtti_map.items():
-# rendered_fields = []
-# for f in field_list:
-# rendered_fields.append(f)
-# return rendered_fields
-
-
-
-#how can we get the structure with the if statements
-#need to get ahold of if statement, then using if statement methods, we can get the inner statement
-
-
-#all_ifs = filter_node_list_by_node_kind(translation_unit.cursor.get_children(), [clang.cindex.CursorKind.IF_STMT])
-#for i in all_ifs:
-# print (i.spelling)
-
-#print(translation_unit.spelling)
-
-def find_ifstmt(node):
- if node.kind.is_statement():
- #ref_node = clang.cindex.Cursor_ref(node)
- #print ("found %s"" % node.location.line)
- print(node.displayname)
- print(node.location.line)
- for c in node.get_children():
- find_ifstmt(c)
-
-#finds the if statement, but cant get anything out of it
-#find_ifstmt(translation_unit.cursor)
-
-
-def rectree(node, indent):
- print("%s item %s of kind %s" % (indent, node.spelling, node.kind))
- for c in node.get_children():
- rectree(c, indent + " ")
-#goes through every part of code but doesn't give info about non variable names
-#rectree(translation_unit.cursor, "")
-
-#CursorKind.IF_STMT
-
-#given the if statement as node, visit each of the else if statements
-def visit_elif(node):
- print("visiting inner elseif statement")
- for i in node.get_children():
- #print(i.kind)
- #print(i.spelling)
- if i.kind == clang.cindex.CursorKind.IF_STMT or i.kind == clang.cindex.CursorKind.COMPOUND_STMT:
- print("found el-if of compound")
- print(i.spelling)
- visit_elif(i)
- print("finished elseif statement")
-#if (node.hasElseStorage()):
- #print("foo")
-
-
-#TODO, but a method to get us the info from an if statemen
-def visitif(node):
- print(node.spelling)
-
-def visit_inner_if(node):
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- print("inner if %s" % i.kind)
- visit_elif(node)
- else:
- visit_inner_if(i)
-
-def get_cursor_id(cursor, cursor_list = []):
- if cursor is None:
- return None
-
- # FIXME: This is really slow. It would be nice if the index API exposed
- # something that let us hash cursors.
- for i,c in enumerate(cursor_list):
- if cursor == c:
- return i
- cursor_list.append(cursor)
- return len(cursor_list) - 1
-
-def get_info(node, depth=0):
- children = [get_info(c, depth+1)
- for c in node.get_children()]
- return { 'id' : get_cursor_id(node),
- 'kind' : node.kind,
- 'usr' : node.get_usr(),
- 'spelling' : node.spelling,
- 'location' : node.location,
- 'extent.start' : node.extent.start,
- 'extent.end' : node.extent.end,
- 'is_definition' : node.is_definition(),
- 'definition id' : get_cursor_id(node.get_definition())}
- #'children' : children }
-
-def code_from_cursor(cursor):
- code = []
- line = ""
- prev_token = None
- for tok in cursor.get_tokens():
- if prev_token is None:
- prev_token = tok
- prev_location = prev_token.location
- prev_token_end_col = prev_location.column + len(prev_token.spelling)
- cur_location = tok.location
- if cur_location.line > prev_location.line:
- code.append(line)
- line = " " * (cur_location.column - 1)
- else:
- if cur_location.column > (prev_token_end_col):
- line += " "
- line += tok.spelling
- prev_token = tok
- if len(line.strip()) > 0:
- code.append(line)
- return code
-
-
-def visit_outter_if(node):
- if_statements = []
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- #print("Outter if statement %s" % i.kind)
- #visit_inner_if(i)
- if_statements.append(code_from_cursor(i)[0])
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = visit_outter_if(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-#visit_outter_if(translation_unit.cursor)
-
-
-def get_outter_if_cursors(node):
- if_statements = []
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- #print("Outter if statement %s" % i.kind)
- #visit_inner_if(i)
- if_statements.append(i)
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = get_outter_if_cursors(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-
-def get_inner_if_cursors(node):
- if_statements = []
- for i in node.get_children():
- #print(i.kind)
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- if_statements.append(i)
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = get_inner_if_cursors(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-
-
-#input: current node, the set of guards/conditionals up to this point, the set of resets
-#return: the sets of guards/resets for all the children
-def traverse_tree(node, guards, resets, indent,hasIfParent):
- #print(guards)
- childrens_guards=[]
- childrens_resets=[]
- results = []
- found = []
- #print(resets)
- #if (indent== '------'):
- # print(guards)
- # return [guards,resets]
- #if (node.kind == clang.cindex.CursorKind.RETURN_STMT):
- # return [guards, resets]
- #elseifstatement = False
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT: #TODO: add else statements
- temp_results = traverse_tree(i, guards, resets, indent+ "-", True)
- for item in temp_results:
- found.append(item)
- #childrens_guards.append(result_guards)
- #childrens_resets.append(result_resets)
-
- else:
- reset_copy = resets
- guard_copy = guards
- if hasIfParent:
- if node.kind == clang.cindex.CursorKind.IF_STMT and i.kind != clang.cindex.CursorKind.COMPOUND_STMT:
- childrens_guards.append(code_from_cursor(i))
- #print(indent + "Guard statement")
- #print(code_from_cursor(i))
- #print(get_info(i))
- #found.append(code_from_cursor(i))
- #temp_results = traverse_tree(i, guard_copy, reset_copy, indent+ "-", hasIfParent)
- #for result in temp_results:
- # result.append(code_from_cursor(i))
- # results.append(result)
- #if len(temp_results)== 0:
- # result.append([code_from_cursor(i)])
- # print("foo")
- if node.kind == clang.cindex.CursorKind.COMPOUND_STMT and i.kind != clang.cindex.CursorKind.DECL_STMT:
- #print(indent + "Reset statement")
- #print(code_from_cursor(i))
- childrens_resets.append(code_from_cursor(i))
- #found.append(code_from_cursor(i))
- #temp_results = traverse_tree(i, guard_copy, reset_copy, indent+ "-", hasIfParent)
- #for result in temp_results:
- # result.append(code_from_cursor(i))
- # results.append(result)
- #if len(temp_results) == 0:
- # results.append([code_from_cursor(i)])
- # print("foo")
- #else:
- temp_results = traverse_tree(i, guard_copy, reset_copy, indent+ "-", hasIfParent)
- for item in temp_results:
- found.append(item)
- #childrens_guards.append(results[0])
- #childrens_resets.append(results[1])
- #if my parent is an if statement and i'm and else if statement, I want to add the negation of my parent, not myself
- if len(found) == 0 and len(childrens_resets) > 0:
- found.append([])
- for item in found:
- for reset in childrens_resets:
- #for item in found:
- item.append([reset, 'r'])
- results.append(item)
- for guard in childrens_guards:
- item.append([guard, 'g'])
-
- return results
-
-#assumption, word mode is not in states
-def pretty_vertices(vertices):
- output = []
- for vertex_code in vertices:
- parts = vertex_code.split("==")
- nonwhitespace = parts[-1].split()
- if "mode" not in nonwhitespace:
- output.append(nonwhitespace[0].strip(')'))
- return output
-
-def get_next_state(code):
- line = code[-2]
- parts = line.split("=")
- state = parts[-1].strip(';')
- return state.strip()
-
-
-#TODO: And( , )
-def pretty_guards(guards):
- output = ""
- first = True
- for condition in guards:
- #print(type(condition))
- if first:
- output+= condition[0]
- else:
- output = "And(" + condition[0] + ",(" + output + "))"
- first = False
- return output
-
-#assumption: reset;reset;reset
-def pretty_resets(resets):
- outstring = ""
- for reset in resets:
- outstring+=reset[0] + ';'
- return outstring.strip(';')
-
-
-##main code###
-#print(sys.argv)
-if len(sys.argv) < 4:
- print("incorrect usage. call createGraph.py program inputfile outputfilename")
- quit()
-
-input_code_name = sys.argv[1]
-input_file_name = sys.argv[2]
-output_file_name = sys.argv[3]
-
-
-
-with open(input_file_name) as in_json_file:
- input_json = json.load(in_json_file)
-
-output_dict = {
-}
-
-output_dict.update(input_json)
-
-#file parsing set up
-index = clang.cindex.Index.create()
-translation_unit = index.parse(input_code_name, args=['-std=c99'])
-print("testing cfg")
-
-#FunctionDecl* func = /* ... */ ;
-#ASTContext* context = /* ... */ ;
-#Stmt* funcBody = func->getBody();
-#CFG* sourceCFG = CFG::buildCFG(func, funcBody, context, clang::CFG::BuildOptions());
-
-#add each variable in state struct as variable
-variables = get_state_variables(translation_unit)
-output_dict['variables'] = variables
-
-#traverse the tree for all the paths
-paths = traverse_tree(translation_unit.cursor, [],[], "", False)
-
-vertices = []
-counter = 0
-for path in paths:
- vertices.append(str(counter))
- counter += 1
- print(path)
-output_dict['vertex'] = vertices
-
-
-
-
-#traverse outter if statements and find inner statements
-edges = []
-guards = []
-resets = []
-
-counter = 0
-for path in paths:
- guard = []
- reset = []
- for item in path:
- if item[1] == 'g':
- guard.append(item[0])
- elif item[1] == 'r':
- reset.append(item[0])
- #create an edge from all other nodes to me
- for vertex in vertices:
- edges.append([vertex, str(counter)])
- guards.append(pretty_guards(guard))
- resets.append(pretty_resets(reset))
- counter+= 1
-
-#add edge, transition(guards) and resets
-output_dict['edge'] = edges
-output_dict['guards'] = guards
-output_dict['resets'] = resets
-
-output_json = json.dumps(output_dict, indent=4)
-#print(output_json)
-outfile = open(output_file_name, "w")
-outfile.write(output_json)
-outfile.close()
-
-print("wrote json to " + output_file_name)
-
-
-
-
-
-
-
-
-
-
diff --git a/generateGraph.py b/generateGraph.py
deleted file mode 100644
index 5fb5919f1d2f62dab80d86fb82dd0b6704f5b0aa..0000000000000000000000000000000000000000
--- a/generateGraph.py
+++ /dev/null
@@ -1,401 +0,0 @@
-#OLD CODE WHICH ONLY ALLOWS TWO LEVELS OF IF STATEMENTS AND EXPLICT MODES
-#NOT THE UPDATED CODE
-
-import clang.cindex
-import typing
-import json
-import sys
-
-#index = clang.cindex.Index.create()
-#translation_unit = index.parse('my_source.c', args=['-std=c99'])
-
-#print all the cursor types
-#for i in translation_unit.get_tokens(extent=translation_unit.cursor.extent):
-# print (i.kind)
-
-#get the structs
-def filter_node_list_by_node_kind(
- nodes: typing.Iterable[clang.cindex.Cursor],
- kinds: list
-) -> typing.Iterable[clang.cindex.Cursor]:
- result = []
- for i in nodes:
- if i.kind in kinds:
- result.append(i)
- return result
-
-#exclude includes
-def filter_node_list_by_file(
- nodes: typing.Iterable[clang.cindex.Cursor],
- file_name: str
-) -> typing.Iterable[clang.cindex.Cursor]:
- result = []
- for i in nodes:
- if i.location.file.name == file_name:
- result.append(i)
- return result
-
-
-#all_classes = filter_node_list_by_node_kind(translation_unit.cursor.get_children(), [clang.cindex.CursorKind.ENUM_DECL, clang.cindex.CursorKind.STRUCT_DECL])
-#for i in all_classes:
-# print (i.spelling)
-
-#captured fields in classes
-def is_exposed_field(node):return node.access_specifier == clang.cindex.AccessSpecifier.PUBLIC
-def find_all_exposed_fields(
- cursor: clang.cindex.Cursor
-):
- result = []
- field_declarations = filter_node_list_by_node_kind(cursor.get_children(), [clang.cindex.CursorKind.FIELD_DECL])
- for i in field_declarations:
- if not is_exposed_field(i):
- continue
- result.append(i.displayname)
- return result
-
-
-def populate_field_list_recursively(class_name: str,class_field_map,class_inheritance_map):
- field_list = class_field_map.get(class_name)
- if field_list is None:
- return []
- baseClasses = class_inheritance_map[class_name]
- for i in baseClasses:
- field_list = populate_field_list_recursively(i.spelling) + field_list
- return field_list
-#rtti_map = {}
-
-
-
-def get_state_variables(translation_unit):
- rtti_map = {}
- source_nodes = filter_node_list_by_file(translation_unit.cursor.get_children(), translation_unit.spelling)
- all_classes = filter_node_list_by_node_kind(source_nodes, [clang.cindex.CursorKind.ENUM_DECL, clang.cindex.CursorKind.STRUCT_DECL])
- class_inheritance_map = {}
- class_field_map = {}
- for i in all_classes:
- bases = []
- for node in i.get_children():
- if node.kind == clang.cindex.CursorKind.CXX_BASE_SPECIFIER:
- referenceNode = node.referenced
- bases.append(node.referenced)
- class_inheritance_map[i.spelling] = bases
- for i in all_classes:
- fields = find_all_exposed_fields(i)
- class_field_map[i.spelling] = fields
- #print("foo")
- for class_name, class_list in class_inheritance_map.items():
- rtti_map[class_name] = populate_field_list_recursively(class_name,class_field_map,class_inheritance_map)
- for class_name, field_list in rtti_map.items():
- rendered_fields = []
- for f in field_list:
- rendered_fields.append(f)
- return rendered_fields
-
-
-
-#def populate_field_list_recursively(class_name: str):
-# field_list = class_field_map.get(class_name)
-# if field_list is None:
-# return []
-# baseClasses = class_inheritance_map[class_name]
-# for i in baseClasses:
-# field_list = populate_field_list_recursively(i.spelling) + field_list
-# return field_list
-#rtti_map = {}
-
-#def get_state_variables():
-# print("foo")
-# for class_name, class_list in class_inheritance_map.items():
-# rtti_map[class_name] = populate_field_list_recursively(class_name)
-# for class_name, field_list in rtti_map.items():
-# rendered_fields = []
-# for f in field_list:
-# rendered_fields.append(f)
-# return rendered_fields
-
-
-
-#how can we get the structure with the if statements
-#need to get ahold of if statement, then using if statement methods, we can get the inner statement
-
-
-#all_ifs = filter_node_list_by_node_kind(translation_unit.cursor.get_children(), [clang.cindex.CursorKind.IF_STMT])
-#for i in all_ifs:
-# print (i.spelling)
-
-#print(translation_unit.spelling)
-
-def find_ifstmt(node):
- if node.kind.is_statement():
- #ref_node = clang.cindex.Cursor_ref(node)
- #print ("found %s"" % node.location.line)
- print(node.displayname)
- print(node.location.line)
- for c in node.get_children():
- find_ifstmt(c)
-
-#finds the if statement, but cant get anything out of it
-#find_ifstmt(translation_unit.cursor)
-
-
-def rectree(node, indent):
- print("%s item %s of kind %s" % (indent, node.spelling, node.kind))
- for c in node.get_children():
- rectree(c, indent + " ")
-#goes through every part of code but doesn't give info about non variable names
-#rectree(translation_unit.cursor, "")
-
-#CursorKind.IF_STMT
-
-#given the if statement as node, visit each of the else if statements
-def visit_elif(node):
- print("visiting inner elseif statement")
- for i in node.get_children():
- #print(i.kind)
- #print(i.spelling)
- if i.kind == clang.cindex.CursorKind.IF_STMT or i.kind == clang.cindex.CursorKind.COMPOUND_STMT:
- print("found el-if of compound")
- print(i.spelling)
- visit_elif(i)
- print("finished elseif statement")
-#if (node.hasElseStorage()):
- #print("foo")
-
-
-#TODO, but a method to get us the info from an if statemen
-def visitif(node):
- print(node.spelling)
-
-def visit_inner_if(node):
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- print("inner if %s" % i.kind)
- visit_elif(node)
- else:
- visit_inner_if(i)
-
-def get_cursor_id(cursor, cursor_list = []):
- if cursor is None:
- return None
-
- # FIXME: This is really slow. It would be nice if the index API exposed
- # something that let us hash cursors.
- for i,c in enumerate(cursor_list):
- if cursor == c:
- return i
- cursor_list.append(cursor)
- return len(cursor_list) - 1
-
-def get_info(node, depth=0):
- children = [get_info(c, depth+1)
- for c in node.get_children()]
- return { 'id' : get_cursor_id(node),
- 'kind' : node.kind,
- 'usr' : node.get_usr(),
- 'spelling' : node.spelling,
- 'location' : node.location,
- 'extent.start' : node.extent.start,
- 'extent.end' : node.extent.end,
- 'is_definition' : node.is_definition(),
- 'definition id' : get_cursor_id(node.get_definition())}
- #'children' : children }
-
-def code_from_cursor(cursor):
- code = []
- line = ""
- prev_token = None
- for tok in cursor.get_tokens():
- if prev_token is None:
- prev_token = tok
- prev_location = prev_token.location
- prev_token_end_col = prev_location.column + len(prev_token.spelling)
- cur_location = tok.location
- if cur_location.line > prev_location.line:
- code.append(line)
- line = " " * (cur_location.column - 1)
- else:
- if cur_location.column > (prev_token_end_col):
- line += " "
- line += tok.spelling
- prev_token = tok
- if len(line.strip()) > 0:
- code.append(line)
- return code
-
-
-def visit_outter_if(node):
- if_statements = []
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- #print("Outter if statement %s" % i.kind)
- #visit_inner_if(i)
- if_statements.append(code_from_cursor(i)[0])
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = visit_outter_if(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-#visit_outter_if(translation_unit.cursor)
-
-
-def get_outter_if_cursors(node):
- if_statements = []
- for i in node.get_children():
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- #print("Outter if statement %s" % i.kind)
- #visit_inner_if(i)
- if_statements.append(i)
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = get_outter_if_cursors(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-
-def get_inner_if_cursors(node):
- if_statements = []
- for i in node.get_children():
- #print(i.kind)
- if i.kind == clang.cindex.CursorKind.IF_STMT:
- if_statements.append(i)
- #print(if_statements)
- #print(i.spelling)
- #for child in i.get_children():
- # print(str(i.kind) + str(i.spelling))
- else:
- out_ifs = get_inner_if_cursors(i)
- for statement in out_ifs:
- if_statements.append(statement)
- return if_statements
-
-#assumption, word mode is not in states
-def pretty_vertices(vertices):
- output = []
- for vertex_code in vertices:
- parts = vertex_code.split("==")
- nonwhitespace = parts[-1].split()
- if "mode" not in nonwhitespace:
- output.append(nonwhitespace[0].strip(')'))
- return output
-
-def get_next_state(code):
- line = code[-2]
- parts = line.split("=")
- state = parts[-1].strip(';')
- return state.strip()
-
-
-#TODO: consider or??
-def pretty_guards(code):
- line = code[0]
- conditional = line.strip('if').strip('{')
- conditions = conditional.split('&&')
- output = "And"
- for condition in conditions:
- output += condition.strip() + ","
- output = output.strip(",")
- return output
-
-#assumption: last two lines of code are reset and bracket... not idea
-def pretty_resets(code):
- outstring = ""
- for index in range(0,len(code)):
- if index != 0 and index != len(code)-1 and index != len(code)-2:
- outstring += code[index].strip().strip('\n')
- return outstring.strip(';')
-
-##main code###
-#print(sys.argv)
-if len(sys.argv) < 4:
- print("incorrect usage. call createGraph.py program inputfile outputfilename")
- quit()
-
-input_code_name = sys.argv[1]
-input_file_name = sys.argv[2]
-output_file_name = sys.argv[3]
-
-with open(input_file_name) as in_json_file:
- input_json = json.load(in_json_file)
-
-output_dict = {
-}
-
-output_dict.update(input_json)
-
-#file parsing set up
-index = clang.cindex.Index.create()
-translation_unit = index.parse(input_code_name, args=['-std=c99'])
-
-#add each variable in state struct as variable
-variables = get_state_variables(translation_unit)
-#assumption mode variable
-variables.remove('mode')
-output_dict['variables'] = variables
-
-#capture each outter if statement and create state
-vertices = pretty_vertices(visit_outter_if(translation_unit.cursor))
-#print(vertice
-output_dict['vertex'] = vertices
-
-
-#traverse outter if statements and find inner statements
-edges = []
-guards = []
-resets = []
-
-#print(type(translation_unit.cursor))
-
-index = 0
-outter_ifs = get_outter_if_cursors(translation_unit.cursor)
-#print(outter_ifs)
-for if_statement in outter_ifs:
- inner_statements = get_inner_if_cursors(if_statement)
- for in_statement in inner_statements:
- code = code_from_cursor(in_statement)
- guards.append(pretty_guards(code))
- #reset = ""
- #for line in range(1, len(code)):
- # reset += str(code[line])
- resets.append(pretty_resets(code))
- to_edge = 0
- #key assumption, second to last line gives next state, fix!
- for i in range(0,len(vertices)):
- #print(vertices[i])
- #print(get_next_state(code))
- if vertices[i] == get_next_state(code):
- to_edge = i
- edges.append([index,to_edge])
- index+=1
-
-#each inner if
-#add edge, transition(guards) and resets
-output_dict['edge'] = edges
-output_dict['guards'] = guards
-output_dict['resets'] = resets
-
-output_json = json.dumps(output_dict, indent=4)
-#print(output_json)
-outfile = open(output_file_name, "w")
-outfile.write(output_json)
-outfile.close()
-
-print("wrote json to " + output_file_name)
-
-
-
-
-
-
-
-
-
-
diff --git a/ourtool/automaton/__init__.py b/ourtool/automaton/__init__.py
deleted file mode 100644
index 171bea6f2daef09e5dd888ad0e79d32db6695628..0000000000000000000000000000000000000000
--- a/ourtool/automaton/__init__.py
+++ /dev/null
@@ -1,4 +0,0 @@
-# try:
-# from hybrid_automaton import *
-# except:
-# from ourtool.automaton.hybrid_automaton import *
\ No newline at end of file
diff --git a/ourtool/map/__init__.py b/ourtool/map/__init__.py
deleted file mode 100644
index e7b9ea180897f28e93a2da6b3d4aec642a08938b..0000000000000000000000000000000000000000
--- a/ourtool/map/__init__.py
+++ /dev/null
@@ -1,8 +0,0 @@
-# try:
-# from lane_map import LaneMap
-# from single_straight_lane import SingleStraightLaneMap
-# from lane_segment import LaneSegment
-# except:
-# from ourtool.map.lane_segment import LaneSegment
-# # from ourtool.map.lane_map import LaneMap
-# # from ourtool.map.single_straight_lane import SingleStraightLaneMap
\ No newline at end of file
diff --git a/ourtool/map/single_straight_lane.py b/ourtool/map/single_straight_lane.py
deleted file mode 100644
index e968f17fd0ca9fd5e929858cfc4d2b38bcbda8de..0000000000000000000000000000000000000000
--- a/ourtool/map/single_straight_lane.py
+++ /dev/null
@@ -1,8 +0,0 @@
-from ourtool.map.lane_map import LaneMap
-from ourtool.map.lane_segment import LaneSegment
-
-class SingleStraightLaneMap(LaneMap):
- def __init__(self):
- super().__init__()
- segment = LaneSegment(0, None, None, None, None)
- self.lane_segment_dict[segment.id] = segment
\ No newline at end of file
diff --git a/ourtool/scenario/__init__.py b/ourtool/scenario/__init__.py
deleted file mode 100644
index 76c3abd5dff7acdee36f5d23104f86e6ee455f19..0000000000000000000000000000000000000000
--- a/ourtool/scenario/__init__.py
+++ /dev/null
@@ -1,4 +0,0 @@
-# try:
-# from Scenario import *
-# except:
-# from ourtool.scenario.Scenario import *
\ No newline at end of file
diff --git a/out.json b/out.json
deleted file mode 100644
index 0984a68184e7819e8d0ce7dea15d944487635cac..0000000000000000000000000000000000000000
--- a/out.json
+++ /dev/null
@@ -1,21 +0,0 @@
-{
- "initialVertex": 0,
- "initialSet": [
- [
- 1.5,
- 0.0,
- 1.0,
- 1.0
- ],
- [
- 1.51,
- 0.0,
- 1.0,
- 1.0
- ]
- ],
- "unsafeSet": "@Allmode:posy>=12.0",
- "timeHorizon": 16,
- "directory": "examples/billiard",
- "deterministic": true
-}
\ No newline at end of file
diff --git a/requirements.txt b/requirements.txt
new file mode 100644
index 0000000000000000000000000000000000000000..2af2f8061800760758da46e37292b86ee2a26373
--- /dev/null
+++ b/requirements.txt
@@ -0,0 +1,10 @@
+networkx~=2.2
+sympy~=1.6.2
+numpy~=1.22.1
+six~=1.14.0
+matplotlib~=3.4.2
+scipy~=1.8.0
+astunparse~=1.6.3
+treelib~=1.6.1
+polytope~=0.2.3
+pyvista~=0.32.1
\ No newline at end of file
diff --git a/singlevehiclesat-out.json b/singlevehiclesat-out.json
deleted file mode 100644
index 28aa3e5796fad7e36ee8b1bc1252975d2cccfa35..0000000000000000000000000000000000000000
--- a/singlevehiclesat-out.json
+++ /dev/null
@@ -1,89 +0,0 @@
-{
- "unsafeSet": "",
- "initialSet": [
- [
- 0,
- -0.2,
- 0
- ],
- [
- 0,
- 0.2,
- 0
- ]
- ],
- "timeHorizon": 10,
- "directory": "examples/curve_controller_hybrid",
- "initialVertex": 0,
- "deterministic": true,
- "variables": [
- "vx",
- "vy",
- "dist"
- ],
- "vertex": [
- "0",
- "1",
- "2"
- ],
- "edge": [
- [
- "0",
- "0"
- ],
- [
- "1",
- "0"
- ],
- [
- "2",
- "0"
- ],
- [
- "0",
- "1"
- ],
- [
- "1",
- "1"
- ],
- [
- "2",
- "1"
- ],
- [
- "0",
- "2"
- ],
- [
- "1",
- "2"
- ],
- [
- "2",
- "2"
- ]
- ],
- "guards": [
- "And(dist < 10,And((dist > 2),And(dist < 2,state != move_over)))",
- "And(dist < 10,And((dist > 2),And(dist < 2,state != move_over)))",
- "And(dist < 10,And((dist > 2),And(dist < 2,state != move_over)))",
- "dist < 10",
- "dist < 10",
- "dist < 10",
- "And(dist < 10,state == move_over)",
- "And(dist < 10,state == move_over)",
- "And(dist < 10,state == move_over)"
- ],
- "resets": [
- "vy=vy - 5;vx= vx + 5;{",
- "vy=vy - 5;vx= vx + 5;{",
- "vy=vy - 5;vx= vx + 5;{",
- "vx=vx - 5;{",
- "vx=vx - 5;{",
- "vx=vx - 5;{",
- "vx = vx + 5",
- "vx = vx + 5",
- "vx = vx + 5"
- ]
-}
\ No newline at end of file
diff --git a/singlevehiclesat.c b/singlevehiclesat.c
deleted file mode 100644
index a5d84ff81926110b2f81f7d918539349d46b2b30..0000000000000000000000000000000000000000
--- a/singlevehiclesat.c
+++ /dev/null
@@ -1,42 +0,0 @@
-enum modes {Normal,Sat_low,Sat_high};
-
-struct State {
-double tau;
-double yf;
-double thetaf;
-enum modes mode;
-};
-
-
-
-struct State P(struct State s) {
- double tau = s.tau;
- double yf = s.yf;
- double thetaf = s.theta;
- enum modes state = s.mode;
- if (s.mode==Normal) {
- if (-0.155914*yf-thetaf <= -0.60871) {
- state=Sat_low;
- }
- if (-0.155914*yf-thetaf >= 0.60871) {
- state=Sat_high;
- }
-
- }
- if (s.mode ==Sat_low) {
- if (-0.155914*yf-thetaf >= -0.60871) {
- state=Normal;
- }
-
- }
- if (s.mode == Sat_high) {
- if (-0.155914*yf-thetaf <= 0.60871) {
- state=Normal;
- }
- }
-
- }
- s.mode = state;
- return s;
-
-}
diff --git a/singlevehiclesat.json b/singlevehiclesat.json
deleted file mode 100644
index de98f9d2eecf699a060e692af9506d920116aa4b..0000000000000000000000000000000000000000
--- a/singlevehiclesat.json
+++ /dev/null
@@ -1,8 +0,0 @@
-{
-"unsafeSet": "",
-"initialSet": [[0,-0.2,0, "Normal"],[0,0.2,0, "Normal"]],
-"timeHorizon": 10,
-"directory": "examples/curve_controller_hybrid",
-"initialVertex":0,
-"deterministic":true
-}
diff --git a/ourtool/__init__.py b/src/__init__.py
similarity index 100%
rename from ourtool/__init__.py
rename to src/__init__.py
diff --git a/ourtool/agents/__init__.py b/src/example/__init__.py
similarity index 100%
rename from ourtool/agents/__init__.py
rename to src/example/__init__.py
diff --git a/ourtool/analysis/__init__.py b/src/example/example_agent/__init__.py
similarity index 100%
rename from ourtool/analysis/__init__.py
rename to src/example/example_agent/__init__.py
diff --git a/ourtool/agents/car_agent.py b/src/example/example_agent/car_agent.py
similarity index 96%
rename from ourtool/agents/car_agent.py
rename to src/example/example_agent/car_agent.py
index c967ca3ee1b9b16255b5ef98ea75c53c3f3b2de3..f8adc8878dd8e36b533e1c5bb420cc867bce7510 100644
--- a/ourtool/agents/car_agent.py
+++ b/src/example/example_agent/car_agent.py
@@ -1,7 +1,7 @@
-from ourtool.agents.base_agent import BaseAgent
+from src.scene_verifier.agents.base_agent import BaseAgent
import numpy as np
from scipy.integrate import ode
-from ourtool.map.lane_map import LaneMap
+from src.scene_verifier.map.lane_map import LaneMap
class CarAgent(BaseAgent):
def __init__(self, id, code = None, file_name = None):
diff --git a/ourtool/dryvr/__init__.py b/src/example/example_map/__init__.py
similarity index 100%
rename from ourtool/dryvr/__init__.py
rename to src/example/example_map/__init__.py
diff --git a/user/simple_map.py b/src/example/example_map/simple_map.py
similarity index 94%
rename from user/simple_map.py
rename to src/example/example_map/simple_map.py
index 848171f5e7748577bfefcd39e5cd9a0d294719c7..2665aa9e49a049f3aba09dccdb3ad1c9014a3b35 100644
--- a/user/simple_map.py
+++ b/src/example/example_map/simple_map.py
@@ -1,5 +1,5 @@
-from ourtool.map.lane_map import LaneMap
-from ourtool.map.lane_segment import LaneSegment
+from src.scene_verifier.map.lane_map import LaneMap
+from src.scene_verifier.map.lane_segment import LaneSegment
class SimpleMap(LaneMap):
def __init__(self):
diff --git a/ourtool/dryvr/core/__init__.py b/src/example/example_sensor/__init__.py
similarity index 100%
rename from ourtool/dryvr/core/__init__.py
rename to src/example/example_sensor/__init__.py
diff --git a/src/example/example_sensor/fake_sensor.py b/src/example/example_sensor/fake_sensor.py
new file mode 100644
index 0000000000000000000000000000000000000000..d415d1d555d8fab301810937ae89a227c8788f3d
--- /dev/null
+++ b/src/example/example_sensor/fake_sensor.py
@@ -0,0 +1,98 @@
+import numpy as np
+
+class FakeSensor1:
+ def sense(self, scenario, agent, state_dict, lane_map):
+ cnts = {}
+ disc = {}
+ state = state_dict['ego'][0]
+ mode = state_dict['ego'][1].split(',')
+ cnts['ego.x'] = state[1]
+ cnts['ego.y'] = state[2]
+ cnts['ego.theta'] = state[3]
+ cnts['ego.v'] = state[4]
+ disc['ego.vehicle_mode'] = mode[0]
+ disc['ego.lane_mode'] = mode[1]
+ return cnts, disc
+
+
+class FakeSensor2:
+ def sense(self, scenario, agent, state_dict, lane_map):
+ cnts = {}
+ disc = {}
+ tmp = np.array(state_dict['car1'][0])
+ if tmp.ndim < 2:
+ if agent.id == 'car1':
+ state = state_dict['car1'][0]
+ mode = state_dict['car1'][1].split(',')
+ cnts['ego.x'] = state[1]
+ cnts['ego.y'] = state[2]
+ cnts['ego.theta'] = state[3]
+ cnts['ego.v'] = state[4]
+ disc['ego.vehicle_mode'] = mode[0]
+ disc['ego.lane_mode'] = mode[1]
+
+ state = state_dict['car2'][0]
+ mode = state_dict['car2'][1].split(',')
+ cnts['other.x'] = state[1]
+ cnts['other.y'] = state[2]
+ cnts['other.theta'] = state[3]
+ cnts['other.v'] = state[4]
+ disc['other.vehicle_mode'] = mode[0]
+ disc['other.lane_mode'] = mode[1]
+ elif agent.id == 'car2':
+ state = state_dict['car2'][0]
+ mode = state_dict['car2'][1].split(',')
+ cnts['ego.x'] = state[1]
+ cnts['ego.y'] = state[2]
+ cnts['ego.theta'] = state[3]
+ cnts['ego.v'] = state[4]
+ disc['ego.vehicle_mode'] = mode[0]
+ disc['ego.lane_mode'] = mode[1]
+
+ state = state_dict['car1'][0]
+ mode = state_dict['car1'][1].split(',')
+ cnts['other.x'] = state[1]
+ cnts['other.y'] = state[2]
+ cnts['other.theta'] = state[3]
+ cnts['other.v'] = state[4]
+ disc['other.vehicle_mode'] = mode[0]
+ disc['other.lane_mode'] = mode[1]
+ return cnts, disc
+ else:
+ if agent.id == 'car1':
+ state = state_dict['car1'][0]
+ mode = state_dict['car1'][1].split(',')
+ cnts['ego.x'] = [state[0][1], state[1][1]]
+ cnts['ego.y'] = [state[0][2], state[1][2]]
+ cnts['ego.theta'] = [state[0][3], state[1][3]]
+ cnts['ego.v'] = [state[0][4], state[1][4]]
+ disc['ego.vehicle_mode'] = mode[0]
+ disc['ego.lane_mode'] = mode[1]
+
+ state = state_dict['car2'][0]
+ mode = state_dict['car2'][1].split(',')
+ cnts['other.x'] = [state[0][1], state[1][1]]
+ cnts['other.y'] = [state[0][2], state[1][2]]
+ cnts['other.theta'] = [state[0][3], state[1][3]]
+ cnts['other.v'] = [state[0][4], state[1][4]]
+ disc['other.vehicle_mode'] = mode[0]
+ disc['other.lane_mode'] = mode[1]
+ elif agent.id == 'car2':
+ state = state_dict['car2'][0]
+ mode = state_dict['car2'][1].split(',')
+ cnts['ego.x'] = [state[0][1], state[1][1]]
+ cnts['ego.y'] = [state[0][2], state[1][2]]
+ cnts['ego.theta'] = [state[0][3], state[1][3]]
+ cnts['ego.v'] = [state[0][4], state[1][4]]
+ disc['ego.vehicle_mode'] = mode[0]
+ disc['ego.lane_mode'] = mode[1]
+
+ state = state_dict['car1'][0]
+ mode = state_dict['car1'][1].split(',')
+ cnts['other.x'] = [state[0][1], state[1][1]]
+ cnts['other.y'] = [state[0][2], state[1][2]]
+ cnts['other.theta'] = [state[0][3], state[1][3]]
+ cnts['other.v'] = [state[0][4], state[1][4]]
+ disc['other.vehicle_mode'] = mode[0]
+ disc['other.lane_mode'] = mode[1]
+ return cnts, disc
diff --git a/ourtool/dryvr/plotter/__init__.py b/src/plotter/__init__.py
similarity index 100%
rename from ourtool/dryvr/plotter/__init__.py
rename to src/plotter/__init__.py
diff --git a/plotter/parser.py b/src/plotter/parser.py
similarity index 100%
rename from plotter/parser.py
rename to src/plotter/parser.py
diff --git a/plotter/plotter2D.py b/src/plotter/plotter2D.py
similarity index 100%
rename from plotter/plotter2D.py
rename to src/plotter/plotter2D.py
diff --git a/plotter/plotter3D.py b/src/plotter/plotter3D.py
similarity index 100%
rename from plotter/plotter3D.py
rename to src/plotter/plotter3D.py
diff --git a/ourtool/dryvr/discrepancy/__init__.py b/src/scene_verifier/__init__.py
similarity index 100%
rename from ourtool/dryvr/discrepancy/__init__.py
rename to src/scene_verifier/__init__.py
diff --git a/src/scene_verifier/agents/__init__.py b/src/scene_verifier/agents/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/ourtool/agents/base_agent.py b/src/scene_verifier/agents/base_agent.py
similarity index 78%
rename from ourtool/agents/base_agent.py
rename to src/scene_verifier/agents/base_agent.py
index a533b3579b3e110806a09538e43b24b16f1ca2cc..e0044528e0c7ce5c0d0119b932d049c8d65b4802 100644
--- a/ourtool/agents/base_agent.py
+++ b/src/scene_verifier/agents/base_agent.py
@@ -1,4 +1,4 @@
-from pythonparser import ControllerAst
+from src.scene_verifier.code_parser.pythonparser import ControllerAst
class BaseAgent:
def __init__(self, id, code = None, file_name = None):
diff --git a/src/scene_verifier/analysis/__init__.py b/src/scene_verifier/analysis/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/ourtool/analysis/analysis_tree_node.py b/src/scene_verifier/analysis/analysis_tree_node.py
similarity index 100%
rename from ourtool/analysis/analysis_tree_node.py
rename to src/scene_verifier/analysis/analysis_tree_node.py
diff --git a/ourtool/analysis/simulator.py b/src/scene_verifier/analysis/simulator.py
similarity index 97%
rename from ourtool/analysis/simulator.py
rename to src/scene_verifier/analysis/simulator.py
index 10a1b23f77a4d51b4b84c0581310773df007bdda..30f47ce5dd44ab46dc9f9bdfca34fc528fdcbcab 100644
--- a/ourtool/analysis/simulator.py
+++ b/src/scene_verifier/analysis/simulator.py
@@ -3,8 +3,8 @@ import copy
import numpy as np
-from ourtool.agents.base_agent import BaseAgent
-from ourtool.analysis.analysis_tree_node import AnalysisTreeNode
+from src.scene_verifier.agents.base_agent import BaseAgent
+from src.scene_verifier.analysis.analysis_tree_node import AnalysisTreeNode
class Simulator:
def __init__(self):
diff --git a/ourtool/analysis/verifier.py b/src/scene_verifier/analysis/verifier.py
similarity index 94%
rename from ourtool/analysis/verifier.py
rename to src/scene_verifier/analysis/verifier.py
index 918cc5e2aaa2f5f0967d2c17e6db707f38e8061b..53a3b501ba64c8b63d3feb33c1e5d4be0cbbf31b 100644
--- a/ourtool/analysis/verifier.py
+++ b/src/scene_verifier/analysis/verifier.py
@@ -3,10 +3,10 @@ import copy
import numpy as np
-from ourtool.agents.base_agent import BaseAgent
-from ourtool.analysis.analysis_tree_node import AnalysisTreeNode
-from ourtool.dryvr.core.dryvrcore import calc_bloated_tube
-import ourtool.dryvr.common.config as userConfig
+from src.scene_verifier.agents.base_agent import BaseAgent
+from src.scene_verifier.analysis.analysis_tree_node import AnalysisTreeNode
+from src.scene_verifier.dryvr.core.dryvrcore import calc_bloated_tube
+import src.scene_verifier.dryvr.common.config as userConfig
class Verifier:
def __init__(self):
diff --git a/src/scene_verifier/automaton/__init__.py b/src/scene_verifier/automaton/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..a1ae96f571beeb44895a0b155022d6c852604e6e
--- /dev/null
+++ b/src/scene_verifier/automaton/__init__.py
@@ -0,0 +1,4 @@
+# try:
+# from hybrid_automaton import *
+# except:
+# from scene_verifier.automaton.hybrid_automaton import *
\ No newline at end of file
diff --git a/ourtool/automaton/guard.py b/src/scene_verifier/automaton/guard.py
similarity index 99%
rename from ourtool/automaton/guard.py
rename to src/scene_verifier/automaton/guard.py
index 0a80a3a20109d44ed15060665d3e44142604f49e..3c65044756030181162ff058f0198b68070bc1fe 100644
--- a/ourtool/automaton/guard.py
+++ b/src/scene_verifier/automaton/guard.py
@@ -2,7 +2,7 @@ import enum
import re
from typing import List, Dict
import pickle
-# from ourtool.automaton.hybrid_io_automaton import HybridIoAutomaton
+# from scene_verifier.automaton.hybrid_io_automaton import HybridIoAutomaton
# from pythonparser import Guard
import ast
import copy
diff --git a/ourtool/automaton/hybrid_automaton.py b/src/scene_verifier/automaton/hybrid_automaton.py
similarity index 100%
rename from ourtool/automaton/hybrid_automaton.py
rename to src/scene_verifier/automaton/hybrid_automaton.py
diff --git a/ourtool/automaton/hybrid_io_automaton.py b/src/scene_verifier/automaton/hybrid_io_automaton.py
similarity index 90%
rename from ourtool/automaton/hybrid_io_automaton.py
rename to src/scene_verifier/automaton/hybrid_io_automaton.py
index e0b936c5f24dd19a26b728172d6be13793702b4c..74f2c963c7ec16095d2ecbc846da58a21e336702 100644
--- a/ourtool/automaton/hybrid_io_automaton.py
+++ b/src/scene_verifier/automaton/hybrid_io_automaton.py
@@ -1,4 +1,4 @@
-from ourtool.automaton.hybrid_automaton import HybridAutomaton
+from src.scene_verifier.automaton.hybrid_automaton import HybridAutomaton
class HybridIoAutomaton(HybridAutomaton):
def __init__(
diff --git a/ourtool/automaton/reset.py b/src/scene_verifier/automaton/reset.py
similarity index 100%
rename from ourtool/automaton/reset.py
rename to src/scene_verifier/automaton/reset.py
diff --git a/src/scene_verifier/code_parser/__init__.py b/src/scene_verifier/code_parser/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/pythonparser.py b/src/scene_verifier/code_parser/pythonparser.py
similarity index 99%
rename from pythonparser.py
rename to src/scene_verifier/code_parser/pythonparser.py
index 0adc8327c0e46b657347214d91090a95b0395587..885ab535ec24cd03ca8ae971655b861be327a7c5 100644
--- a/pythonparser.py
+++ b/src/scene_verifier/code_parser/pythonparser.py
@@ -472,9 +472,9 @@ if __name__ == "__main__":
# print("incorrect usage. call createGraph.py program inputfile outputfilename")
# quit()
- input_code_name = 'toythermomini.py' #sys.argv[1]
- input_file_name = 'billiard_input.json' #sys.argv[2]
- output_file_name = 'out.json' #sys.argv[3]
+ input_code_name = sys.argv[1]
+ input_file_name = sys.argv[2]
+ output_file_name = sys.argv[3]
with open(input_file_name) as in_json_file:
input_json = json.load(in_json_file)
diff --git a/src/scene_verifier/dryvr/__init__.py b/src/scene_verifier/dryvr/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/ourtool/dryvr/common/__init__.py b/src/scene_verifier/dryvr/common/__init__.py
similarity index 100%
rename from ourtool/dryvr/common/__init__.py
rename to src/scene_verifier/dryvr/common/__init__.py
diff --git a/ourtool/dryvr/common/config.py b/src/scene_verifier/dryvr/common/config.py
similarity index 100%
rename from ourtool/dryvr/common/config.py
rename to src/scene_verifier/dryvr/common/config.py
diff --git a/ourtool/dryvr/common/constant.py b/src/scene_verifier/dryvr/common/constant.py
similarity index 100%
rename from ourtool/dryvr/common/constant.py
rename to src/scene_verifier/dryvr/common/constant.py
diff --git a/ourtool/dryvr/common/io.py b/src/scene_verifier/dryvr/common/io.py
similarity index 95%
rename from ourtool/dryvr/common/io.py
rename to src/scene_verifier/dryvr/common/io.py
index c5b55e206966a7b8a5adb4fc016f5da359ec2b3d..bf864448b0ab522a1f5e17df03d67e2be0512390 100644
--- a/ourtool/dryvr/common/io.py
+++ b/src/scene_verifier/dryvr/common/io.py
@@ -4,7 +4,7 @@ This file contains IO functions for DryVR
import six
-from ourtool.dryvr.common.utils import DryVRInput, RrtInput, checkVerificationInput, checkSynthesisInput
+from src.scene_verifier.dryvr.common.utils import DryVRInput, RrtInput, checkVerificationInput, checkSynthesisInput
def writeReachTubeFile(result, path):
@@ -90,7 +90,7 @@ def parseVerificationInputFile(data):
if data['bloatingMethod'] == "GLOBAL":
data['kvalue'] = [1.0 for i in range(len(data['variables']))]
- # Set a fake directory if the directory is not provided, this means the user provides
+ # Set a fake directory if the directory is not provided, this means the example provides
# simulation function to DryVR directly
if not 'directory' in data:
data['directory'] = ""
@@ -134,7 +134,7 @@ def parseRrtInputFile(data):
if data['bloatingMethod'] == "GLOBAL":
data['kvalue'] = [1.0 for i in range(len(data['variables']))]
- # Set a fake directory if the directory is not provided, this means the user provides
+ # Set a fake directory if the directory is not provided, this means the example provides
# simulation function to DryVR directly
if not 'directory' in data:
data['directory'] = ""
diff --git a/ourtool/dryvr/common/utils.py b/src/scene_verifier/dryvr/common/utils.py
similarity index 98%
rename from ourtool/dryvr/common/utils.py
rename to src/scene_verifier/dryvr/common/utils.py
index 21d64ff954b9f63fff37f7595b33a37808234b39..1923a84ea51badf888fc64852a0d89edd45d3575 100644
--- a/ourtool/dryvr/common/utils.py
+++ b/src/scene_verifier/dryvr/common/utils.py
@@ -278,11 +278,11 @@ def isIpynb():
def overloadConfig(configObj, userConfig):
"""
- Overload user config to config module
+ Overload example config to config module
Args:
configObj (module): config module
- userConfig (dict): user specified config
+ userConfig (dict): example specified config
"""
if "SIMUTESTNUM" in userConfig:
diff --git a/src/scene_verifier/dryvr/core/__init__.py b/src/scene_verifier/dryvr/core/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/ourtool/dryvr/core/distance.py b/src/scene_verifier/dryvr/core/distance.py
similarity index 100%
rename from ourtool/dryvr/core/distance.py
rename to src/scene_verifier/dryvr/core/distance.py
diff --git a/ourtool/dryvr/core/dryvrcore.py b/src/scene_verifier/dryvr/core/dryvrcore.py
similarity index 95%
rename from ourtool/dryvr/core/dryvrcore.py
rename to src/scene_verifier/dryvr/core/dryvrcore.py
index 29ff8cd3152d260cd3d85eadc64aaf6dcd57e595..14df5292f4f25786be7c265288aaa585663d15c4 100644
--- a/ourtool/dryvr/core/dryvrcore.py
+++ b/src/scene_verifier/dryvr/core/dryvrcore.py
@@ -9,12 +9,12 @@ import numpy as np
import igraph
-from ourtool.dryvr.common.constant import *
-from ourtool.dryvr.common.io import writeReachTubeFile
-from ourtool.dryvr.common.utils import randomPoint, calcDelta, calcCenterPoint, trimTraces
-from ourtool.dryvr.discrepancy.Global_Disc import get_reachtube_segment
-# from ourtool.dryvr.tube_computer.backend.reachabilityengine import ReachabilityEngine
-# from ourtool.dryvr.tube_computer.backend.initialset import InitialSet
+from src.scene_verifier.dryvr.common.constant import *
+from src.scene_verifier.dryvr.common.io import writeReachTubeFile
+from src.scene_verifier.dryvr.common.utils import randomPoint, calcDelta, calcCenterPoint, trimTraces
+from src.scene_verifier.dryvr.discrepancy.Global_Disc import get_reachtube_segment
+# from scene_verifier.dryvr.tube_computer.backend.reachabilityengine import ReachabilityEngine
+# from scene_verifier.dryvr.tube_computer.backend.initialset import InitialSet
def build_graph(vertex, edge, guards, resets):
"""
diff --git a/ourtool/dryvr/core/dryvrmain.py b/src/scene_verifier/dryvr/core/dryvrmain.py
similarity index 98%
rename from ourtool/dryvr/core/dryvrmain.py
rename to src/scene_verifier/dryvr/core/dryvrmain.py
index af6ddd87302b6811d056b6ccffb4930da690bfea..7b085aab083f01e9af8b9fe52bd82857493d544c 100644
--- a/ourtool/dryvr/core/dryvrmain.py
+++ b/src/scene_verifier/dryvr/core/dryvrmain.py
@@ -28,7 +28,7 @@ def verify(data, sim_function, param_config=None):
Args:
data (dict): dictionary that contains params for the input file
sim_function (function): black-box simulation function
- param_config (dict or None): user-specified configuration
+ param_config (dict or None): example-specified configuration
Returns:
Safety (str): safety of the system
@@ -37,8 +37,8 @@ def verify(data, sim_function, param_config=None):
"""
if param_config is None:
param_config = {}
- # There are some fields can be config by user,
- # If user specified these fields in paramConfig,
+ # There are some fields can be config by example,
+ # If example specified these fields in paramConfig,
# overload these parameters to userConfig
overloadConfig(userConfig, param_config)
@@ -348,7 +348,7 @@ def graph_search(data, sim_function, param_config=None):
Args:
data (dict): dictionary that contains params for the input file
sim_function (function): black-box simulation function
- param_config (dict or None): user-specified configuration
+ param_config (dict or None): example-specified configuration
Returns:
None
@@ -356,8 +356,8 @@ def graph_search(data, sim_function, param_config=None):
"""
if param_config is None:
param_config = {}
- # There are some fields can be config by user,
- # If user specified these fields in paramConfig,
+ # There are some fields can be config by example,
+ # If example specified these fields in paramConfig,
# overload these parameters to userConfig
overloadConfig(userConfig, param_config)
# Parse the input json file and read out the parameters
diff --git a/ourtool/dryvr/core/goalchecker.py b/src/scene_verifier/dryvr/core/goalchecker.py
similarity index 100%
rename from ourtool/dryvr/core/goalchecker.py
rename to src/scene_verifier/dryvr/core/goalchecker.py
diff --git a/ourtool/dryvr/core/graph.py b/src/scene_verifier/dryvr/core/graph.py
similarity index 100%
rename from ourtool/dryvr/core/graph.py
rename to src/scene_verifier/dryvr/core/graph.py
diff --git a/ourtool/dryvr/core/guard.py b/src/scene_verifier/dryvr/core/guard.py
similarity index 100%
rename from ourtool/dryvr/core/guard.py
rename to src/scene_verifier/dryvr/core/guard.py
diff --git a/ourtool/dryvr/core/initialset.py b/src/scene_verifier/dryvr/core/initialset.py
similarity index 100%
rename from ourtool/dryvr/core/initialset.py
rename to src/scene_verifier/dryvr/core/initialset.py
diff --git a/ourtool/dryvr/core/initialsetstack.py b/src/scene_verifier/dryvr/core/initialsetstack.py
similarity index 100%
rename from ourtool/dryvr/core/initialsetstack.py
rename to src/scene_verifier/dryvr/core/initialsetstack.py
diff --git a/ourtool/dryvr/core/reachtube.py b/src/scene_verifier/dryvr/core/reachtube.py
similarity index 97%
rename from ourtool/dryvr/core/reachtube.py
rename to src/scene_verifier/dryvr/core/reachtube.py
index f985f43778cc4fe2b8ef7f165025a6394e32a17b..850b8a5a1fd796541d4cade354e0ad3537b3ad6c 100644
--- a/ourtool/dryvr/core/reachtube.py
+++ b/src/scene_verifier/dryvr/core/reachtube.py
@@ -25,7 +25,7 @@ class ReachTube:
self._variables = variables
self._modes = modes
- # Build the raw string representation so user can print it
+ # Build the raw string representation so example can print it
self.raw = ""
for line in tube:
diff --git a/ourtool/dryvr/core/reset.py b/src/scene_verifier/dryvr/core/reset.py
similarity index 100%
rename from ourtool/dryvr/core/reset.py
rename to src/scene_verifier/dryvr/core/reset.py
diff --git a/ourtool/dryvr/core/uniformchecker.py b/src/scene_verifier/dryvr/core/uniformchecker.py
similarity index 100%
rename from ourtool/dryvr/core/uniformchecker.py
rename to src/scene_verifier/dryvr/core/uniformchecker.py
diff --git a/ourtool/dryvr/discrepancy/Global_Disc.py b/src/scene_verifier/dryvr/discrepancy/Global_Disc.py
similarity index 100%
rename from ourtool/dryvr/discrepancy/Global_Disc.py
rename to src/scene_verifier/dryvr/discrepancy/Global_Disc.py
diff --git a/ourtool/dryvr/discrepancy/PW_Discrepancy.py b/src/scene_verifier/dryvr/discrepancy/PW_Discrepancy.py
similarity index 100%
rename from ourtool/dryvr/discrepancy/PW_Discrepancy.py
rename to src/scene_verifier/dryvr/discrepancy/PW_Discrepancy.py
diff --git a/src/scene_verifier/dryvr/discrepancy/__init__.py b/src/scene_verifier/dryvr/discrepancy/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/ourtool/dryvr/plotter/.ipynb_checkpoints/plotterInterface-checkpoint.ipynb b/src/scene_verifier/dryvr/plotter/.ipynb_checkpoints/plotterInterface-checkpoint.ipynb
similarity index 100%
rename from ourtool/dryvr/plotter/.ipynb_checkpoints/plotterInterface-checkpoint.ipynb
rename to src/scene_verifier/dryvr/plotter/.ipynb_checkpoints/plotterInterface-checkpoint.ipynb
diff --git a/ourtool/dryvr/plotter/README.md b/src/scene_verifier/dryvr/plotter/README.md
similarity index 100%
rename from ourtool/dryvr/plotter/README.md
rename to src/scene_verifier/dryvr/plotter/README.md
diff --git a/plotter/__init__.py b/src/scene_verifier/dryvr/plotter/__init__.py
similarity index 100%
rename from plotter/__init__.py
rename to src/scene_verifier/dryvr/plotter/__init__.py
diff --git a/ourtool/dryvr/plotter/linkednode.py b/src/scene_verifier/dryvr/plotter/linkednode.py
similarity index 100%
rename from ourtool/dryvr/plotter/linkednode.py
rename to src/scene_verifier/dryvr/plotter/linkednode.py
diff --git a/ourtool/dryvr/plotter/parser.py b/src/scene_verifier/dryvr/plotter/parser.py
similarity index 100%
rename from ourtool/dryvr/plotter/parser.py
rename to src/scene_verifier/dryvr/plotter/parser.py
diff --git a/ourtool/dryvr/plotter/plot.py b/src/scene_verifier/dryvr/plotter/plot.py
similarity index 100%
rename from ourtool/dryvr/plotter/plot.py
rename to src/scene_verifier/dryvr/plotter/plot.py
diff --git a/ourtool/dryvr/plotter/plot_util.py b/src/scene_verifier/dryvr/plotter/plot_util.py
similarity index 100%
rename from ourtool/dryvr/plotter/plot_util.py
rename to src/scene_verifier/dryvr/plotter/plot_util.py
diff --git a/ourtool/dryvr/plotter/plotter_interface.ipynb b/src/scene_verifier/dryvr/plotter/plotter_interface.ipynb
similarity index 100%
rename from ourtool/dryvr/plotter/plotter_interface.ipynb
rename to src/scene_verifier/dryvr/plotter/plotter_interface.ipynb
diff --git a/src/scene_verifier/map/__init__.py b/src/scene_verifier/map/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..c4fd24f6b4b1fa640294337d048c0fc8d7051183
--- /dev/null
+++ b/src/scene_verifier/map/__init__.py
@@ -0,0 +1,8 @@
+# try:
+# from lane_map import LaneMap
+# from single_straight_lane import SingleStraightLaneMap
+# from lane_segment import LaneSegment
+# except:
+# from scene_verifier.map.lane_segment import LaneSegment
+# # from scene_verifier.map.lane_map import LaneMap
+# # from scene_verifier.map.single_straight_lane import SingleStraightLaneMap
\ No newline at end of file
diff --git a/ourtool/map/lane_map.py b/src/scene_verifier/map/lane_map.py
similarity index 97%
rename from ourtool/map/lane_map.py
rename to src/scene_verifier/map/lane_map.py
index 31cd4b7ab4b0d3e924d7115412eb71b0e681c53d..9e54323250cfc4cd834cae5ec083defbce9bb075 100644
--- a/ourtool/map/lane_map.py
+++ b/src/scene_verifier/map/lane_map.py
@@ -2,7 +2,7 @@ from typing import Dict, List
import copy
from enum import Enum,auto
-from ourtool.map.lane_segment import LaneSegment
+from src.scene_verifier.map.lane_segment import LaneSegment
class LaneMap:
def __init__(self, lane_seg_list:List[LaneSegment] = []):
diff --git a/ourtool/map/lane_segment.py b/src/scene_verifier/map/lane_segment.py
similarity index 100%
rename from ourtool/map/lane_segment.py
rename to src/scene_verifier/map/lane_segment.py
diff --git a/src/scene_verifier/scenario/__init__.py b/src/scene_verifier/scenario/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..559069149e378ddbcab6cecd08c7ec429a29962f
--- /dev/null
+++ b/src/scene_verifier/scenario/__init__.py
@@ -0,0 +1,4 @@
+# try:
+# from Scenario import *
+# except:
+# from scene_verifier.scenario.Scenario import *
\ No newline at end of file
diff --git a/ourtool/scenario/scenario.py b/src/scene_verifier/scenario/scenario.py
similarity index 72%
rename from ourtool/scenario/scenario.py
rename to src/scene_verifier/scenario/scenario.py
index 5f41f5dee153d365a7dc194ccd1751284e2aaa72..7ad1a5db8760aba1567b540ec309c3fb3b658b5f 100644
--- a/ourtool/scenario/scenario.py
+++ b/src/scene_verifier/scenario/scenario.py
@@ -1,101 +1,18 @@
-from typing import Dict, List, Tuple
+from typing import Tuple
import copy
import itertools
-import ast
import numpy as np
-from ourtool.agents.base_agent import BaseAgent
-from ourtool.automaton.guard import GuardExpressionAst
-from ourtool.automaton.reset import ResetExpression
-from pythonparser import Guard
-from pythonparser import Reset
-from ourtool.analysis.simulator import Simulator
-from ourtool.analysis.verifier import Verifier
-from ourtool.map.lane_map import LaneMap
+from src.scene_verifier.agents.base_agent import BaseAgent
+from src.scene_verifier.automaton.guard import GuardExpressionAst
+from src.scene_verifier.automaton.reset import ResetExpression
+from src.scene_verifier.code_parser.pythonparser import Guard
+from src.scene_verifier.code_parser.pythonparser import Reset
+from src.scene_verifier.analysis.simulator import Simulator
+from src.scene_verifier.analysis.verifier import Verifier
+from src.scene_verifier.map.lane_map import LaneMap
-class FakeSensor:
- def sense(self, scenario, agent, state_dict, lane_map):
- cnts = {}
- disc = {}
- tmp = np.array(state_dict['car1'][0])
- if tmp.ndim < 2:
- if agent.id == 'car1':
- state = state_dict['car1'][0]
- mode = state_dict['car1'][1].split(',')
- cnts['ego.x'] = state[1]
- cnts['ego.y'] = state[2]
- cnts['ego.theta'] = state[3]
- cnts['ego.v'] = state[4]
- disc['ego.vehicle_mode'] = mode[0]
- disc['ego.lane_mode'] = mode[1]
-
- state = state_dict['car2'][0]
- mode = state_dict['car2'][1].split(',')
- cnts['other.x'] = state[1]
- cnts['other.y'] = state[2]
- cnts['other.theta'] = state[3]
- cnts['other.v'] = state[4]
- disc['other.vehicle_mode'] = mode[0]
- disc['other.lane_mode'] = mode[1]
- elif agent.id == 'car2':
- state = state_dict['car2'][0]
- mode = state_dict['car2'][1].split(',')
- cnts['ego.x'] = state[1]
- cnts['ego.y'] = state[2]
- cnts['ego.theta'] = state[3]
- cnts['ego.v'] = state[4]
- disc['ego.vehicle_mode'] = mode[0]
- disc['ego.lane_mode'] = mode[1]
-
- state = state_dict['car1'][0]
- mode = state_dict['car1'][1].split(',')
- cnts['other.x'] = state[1]
- cnts['other.y'] = state[2]
- cnts['other.theta'] = state[3]
- cnts['other.v'] = state[4]
- disc['other.vehicle_mode'] = mode[0]
- disc['other.lane_mode'] = mode[1]
- return cnts, disc
- else:
- if agent.id == 'car1':
- state = state_dict['car1'][0]
- mode = state_dict['car1'][1].split(',')
- cnts['ego.x'] = [state[0][1],state[1][1]]
- cnts['ego.y'] = [state[0][2],state[1][2]]
- cnts['ego.theta'] = [state[0][3],state[1][3]]
- cnts['ego.v'] = [state[0][4],state[1][4]]
- disc['ego.vehicle_mode'] = mode[0]
- disc['ego.lane_mode'] = mode[1]
-
- state = state_dict['car2'][0]
- mode = state_dict['car2'][1].split(',')
- cnts['other.x'] = [state[0][1],state[1][1]]
- cnts['other.y'] = [state[0][2],state[1][2]]
- cnts['other.theta'] = [state[0][3],state[1][3]]
- cnts['other.v'] = [state[0][4],state[1][4]]
- disc['other.vehicle_mode'] = mode[0]
- disc['other.lane_mode'] = mode[1]
- elif agent.id == 'car2':
- state = state_dict['car2'][0]
- mode = state_dict['car2'][1].split(',')
- cnts['ego.x'] = [state[0][1],state[1][1]]
- cnts['ego.y'] = [state[0][2],state[1][2]]
- cnts['ego.theta'] = [state[0][3],state[1][3]]
- cnts['ego.v'] = [state[0][4],state[1][4]]
- disc['ego.vehicle_mode'] = mode[0]
- disc['ego.lane_mode'] = mode[1]
-
- state = state_dict['car1'][0]
- mode = state_dict['car1'][1].split(',')
- cnts['other.x'] = [state[0][1],state[1][1]]
- cnts['other.y'] = [state[0][2],state[1][2]]
- cnts['other.theta'] = [state[0][3],state[1][3]]
- cnts['other.v'] = [state[0][4],state[1][4]]
- disc['other.vehicle_mode'] = mode[0]
- disc['other.lane_mode'] = mode[1]
- return cnts, disc
-
class Scenario:
def __init__(self):
self.agent_dict = {}
@@ -104,7 +21,10 @@ class Scenario:
self.init_dict = {}
self.init_mode_dict = {}
self.map = None
- self.sensor = FakeSensor()
+ self.sensor = None
+
+ def set_sensor(self, sensor):
+ self.sensor = sensor
def add_map(self, lane_map:LaneMap):
self.map = lane_map
diff --git a/toythermo.py b/toythermo.py
deleted file mode 100644
index 34a85817fe20c3ee18897c550a3c9e6fbed71508..0000000000000000000000000000000000000000
--- a/toythermo.py
+++ /dev/null
@@ -1,135 +0,0 @@
-#python logic toy code:
-
-from enum import Enum, auto
-from ssl import VERIFY_X509_PARTIAL_CHAIN
-from statistics import mode
-from termios import VSTART
-
-
-class Modes(Enum):
- NormalA = auto()
- NormalB = auto()
- NormalC = auto()
- NormalD = auto()
-
-class State:
- posx = 0.0
- posy = 0.0
- vx = 1.0
- vy = 1.0
- mode = Modes.NormalA
-
- def __init__(self):
- self.data = []
-
-
-if __name__ == "__main__":
-#todo: how would this actually be given
- s = State()
-
- posx = s.posx
- posy = s.posy
- vx = s.vx
- vy = s.vy
- state = s.mode
- if (state ==Modes.NormalA):
- if posy<0 and posy>=-0.01:
- vy=-vy
- posy=0
- state=Modes.NormalA
-
- if (posx<0 and posx>=-0.01) :
- vx=-vx
- posx=0
- state=Modes.NormalB
-
- if (posx<=5.01 and posx>5) :
- vx=-vx
- posx=5
- state=Modes.NormalC
-
- if (posy>5 and posy<=5.01) :
- vy=-vy
- posy=5
- state = Modes.NormalD
-
-
-
- if (state ==Modes.NormalB) :
- if (posy<0 and posy>=-0.01) :
- vy=-vy
- posy=0
- state=Modes.NormalB
-
- if (posx<0 and posx>=-0.01) :
- vx=-vx
- posx=0
- state=Modes.NormalA
-
- if (posx<=5.01 and posx>5) :
- vx=-vx
- posx=5
- state=Modes.NormalC
-
- if (posy>5 and posy<=5.01) :
- vy=-vy
- posy=5
- state = Modes.NormalD
-
-
-
- if (state ==Modes.NormalC) :
- if (posy<0 and posy>=-0.01) :
- vy=-vy
- posy=0
- state=Modes.NormalC
-
- if (posx<0 and posx>=-0.01) :
- vx=-vx
- posx=0
- state=Modes.NormalA
-
- if (posx<=5.01 and posx>5) :
- vx=-vx
- posx=5
- state=Modes.NormalB
-
- if (posy>5 and posy<=5.01) :
- vy=-vy
- posy=5
- state = Modes.NormalD
-
-
-
-
- if (state ==State.Modes.NormalD) :
- if (posy<0 and posy>=-0.01) :
- vy=-vy
- posy=0
- state=Modes.NormalD
-
- if (posx<0 and posx>=-0.01) :
- vx=-vx
- posx=0
- state=Modes.NormalA
-
- if (posx<=5.01 and posx>5) :
- vx=-vx
- posx=5
- state=Modes.NormalB
-
- if (posy>5 and posy<=5.01) :
- vy=-vy
- posy=5
- state = Modes.NormalC
-
-
-
- s.posx = posx
- s.posy= posy
- s.vx = vx
- s.vy = vy
- s.mode = state
-
- #TODO: what is output?
-
diff --git a/toythermomini.py b/toythermomini.py
deleted file mode 100644
index 0423c8c84ddb00372658d640e9c30d39ea5e0904..0000000000000000000000000000000000000000
--- a/toythermomini.py
+++ /dev/null
@@ -1,45 +0,0 @@
-#python logic toy code:
-
-from enum import Enum, auto
-
-class Modes(Enum):
- NormalA = auto()
- NormalB = auto()
- NormalC = auto()
- NormalD = auto()
-
-class State:
- posx = 0.0
- posy = 0.0
- mode = Modes.NormalA
-
- def __init__(self):
- self.data = []
-
-
-def controller(posx, posy, mode):
- outmode = mode
-#todo: how would this actually be given
- if (mode ==Modes.NormalA):
- if posy<0 and posy>=-0.0:
- posy=0
- outmode=Modes.NormalA
- if posy>10 and posy==-10:
- posy=10
- outmode=Modes.NormalB
-
- if (mode ==Modes.NormalB):
- if posy<0 and posy>=-0.0:
- posy=0
- outmode=Modes.NormalA
- if posy>10 and posy==-10:
- posy=10
- outmode=Modes.NormalB
-
-
-
-
- return outmode
-
- #TODO: what is output?
-