Skip to content
Snippets Groups Projects
Commit ebb00993 authored by li213's avatar li213
Browse files

Change how neureach are handled; Change tutorial to use dl files;

parent d2b33d64
No related branches found
No related tags found
1 merge request!9Tutorial
Hide whitespace changes
Inline Side-by-side
setup.py
+ 19
− 18
View file @ ebb00993
...@@ -8,33 +8,34 @@ setup( ...@@ -8,33 +8,34 @@ setup(
author='Yangge Li, Katherine Braught, Haoqing Zhu', author='Yangge Li, Katherine Braught, Haoqing Zhu',
maintainer='Yangge Li, Katherine Braught, Haoqing Zhu', maintainer='Yangge Li, Katherine Braught, Haoqing Zhu',
maintainer_email='{li213, braught2, haoqing3}@illinois.edu', maintainer_email='{li213, braught2, haoqing3}@illinois.edu',
license='Apache-2.0',
packages=find_packages(exclude=["tests", "demo"]), packages=find_packages(exclude=["tests", "demo"]),
python_requires='>=3.8', python_requires='>=3.8',
install_requires=[ install_requires=[
"numpy~=1.22.1", "numpy",
"scipy~=1.8.1", "scipy",
"matplotlib~=3.4.2", "matplotlib",
"polytope~=0.2.3", "polytope",
"pyvista~=0.32.1", "pyvista",
"networkx~=2.2", "networkx",
"sympy~=1.6.2", "sympy",
"six~=1.14.0", "six",
"astunparse~=1.6.3", "astunparse",
"treelib~=1.6.1", "treelib",
"z3-solver~=4.8.17.0", "z3-solver",
"igraph~=0.9.10", "igraph",
"plotly~=5.8.0", "plotly",
"beautifulsoup4~=4.11.1", "beautifulsoup4",
"lxml~=4.9.1", "lxml",
"torch", "torch",
"tqdm" "tqdm",
"intervaltree",
"Pympler"
"nbformat",
], ],
classifiers=[ classifiers=[
'Development Status :: 2 - Pre-Alpha', 'Development Status :: 2 - Pre-Alpha',
'Intended Audience :: Science/Research', 'Intended Audience :: Science/Research',
'Topic :: Scientific/Engineering', 'Topic :: Scientific/Engineering',
'License :: OSI Approved :: Apache License 2.0',
'Programming Language :: Python :: 3.8', 'Programming Language :: Python :: 3.8',
] ]
) )
tutorial/Verse_Tutorial.ipynb
+ 9
− 28
View file @ ebb00993
%% Cell type:markdown id:9cb21069 tags: %% Cell type:markdown id:9cb21069 tags:
# 1. Getting Started # 1. Getting Started
%% Cell type:markdown id:6ee9346d tags: %% Cell type:markdown id:6ee9346d tags:
A verse scenario is defined by a map, a set of agents and, if there exist multiple agents, a sensor. A verse scenario is defined by a map, a set of agents and, if there exist multiple agents, a sensor.
%% Cell type:markdown id:d34d63e6 tags: %% Cell type:markdown id:d34d63e6 tags:
In this section, we are going to look at how to create a simple scenario in Verse. In this scenario we will have only one car following a straight lane and will brake after reaching a certain position. In this section, we are going to look at how to create a simple scenario in Verse. In this scenario we will have only one car following a straight lane and will brake after reaching a certain position.
%% Cell type:markdown id:5e80ec75 tags: %% Cell type:markdown id:5e80ec75 tags:
## 1.1 Instantiate map ## 1.1 Instantiate map
The map of a scenario specifies the tracks that the agents can follow. In this example, we will only look at a simple map we one straight lane aligned with the x-axis with type <code>T0</code>, which are also referred as track mode in later sections. We will talk about how to create more interesting maps in later sections The map of a scenario specifies the tracks that the agents can follow. In this example, we will only look at a simple map we one straight lane aligned with the x-axis with type <code>T0</code>, which are also referred as track mode in later sections. We will talk about how to create more interesting maps in later sections
%% Cell type:code id:d789ceb2 tags: %% Cell type:code id:d789ceb2 tags:
``` python ```
from tutorial_map import M1 from tutorial_map import M1
map1 = M1() map1 = M1()
``` ```
%% Cell type:markdown id:3b120f0c tags: %% Cell type:markdown id:3b120f0c tags:
## 1.2 Creating agent ## 1.2 Creating agent
To create such a scenario in Verse, we first need to create an agent for Verse. An agent in Verse is defined by a set of tactical modes, a decision logic to determine the transition between tactical modes, and a flow function that defines continuous evolution. The agent's tactical mode and decision logic are provided as python code strings and the flow function is provided as a python function. To create such a scenario in Verse, we first need to create an agent for Verse. An agent in Verse is defined by a set of tactical modes, a decision logic to determine the transition between tactical modes, and a flow function that defines continuous evolution. The agent's tactical mode and decision logic are provided as python code strings and the flow function is provided as a python function.
%% Cell type:markdown id:96d7ce5e tags: %% Cell type:markdown id:96d7ce5e tags:
The tactical mode of the agents corresponds to an agent's decision. For example, in this car braking example, the tactical mode for the agent can be <code>Normal</code> and <code>Brake</code>. The decision logic also need to know the available track modes from the map. The tactical modes and track modes are provided as <code>Enums</code> to Verse. The tactical mode of the agents corresponds to an agent's decision. For example, in this car braking example, the tactical mode for the agent can be <code>Normal</code> and <code>Brake</code>. The decision logic also need to know the available track modes from the map. The tactical modes and track modes are provided as <code>Enums</code> to Verse.
%% Cell type:code id:0fbb7f1f tags: %% Cell type:code id:0fbb7f1f tags:
``` python ```
from enum import Enum, auto from enum import Enum, auto
class AgentMode(Enum): class AgentMode(Enum):
Normal = auto() Normal = auto()
Brake = auto() Brake = auto()
class TrackMode(Enum): class TrackMode(Enum):
T0 = auto() T0 = auto()
``` ```
%% Cell type:markdown id:25ec7639 tags: %% Cell type:markdown id:25ec7639 tags:
We also require the user to provide the continuous and discrete variables of the agents together with the decision logic. The variables are provided inside class with name <code>State</code>. Variables end with <code>_mode</code> will be identify by verse as discrete variables. In the example below, <code>agent_mode</code> and <code>track_mode</code> are the discrete variables and <code>x</code>, <code>y</code>, <code>theta</code>, <code>v</code> are the continuous variables. The type hints for the discrete variables are necessary to associate discrete variables with the tactical modes and lane modes defined above We also require the user to provide the continuous and discrete variables of the agents together with the decision logic. The variables are provided inside class with name <code>State</code>. Variables end with <code>_mode</code> will be identify by verse as discrete variables. In the example below, <code>agent_mode</code> and <code>track_mode</code> are the discrete variables and <code>x</code>, <code>y</code>, <code>theta</code>, <code>v</code> are the continuous variables. The type hints for the discrete variables are necessary to associate discrete variables with the tactical modes and lane modes defined above
%% Cell type:code id:7edf89dc tags: %% Cell type:code id:7edf89dc tags:
``` python ```
class State: class State:
x:float x:float
y:float y:float
theta:float theta:float
v:float v:float
agent_mode:AgentMode agent_mode:AgentMode
track_mode:TrackMode track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode): def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass pass
``` ```
%% Cell type:markdown id:3b0ea818 tags: %% Cell type:markdown id:3b0ea818 tags:
The decision logic describe for an agent takes as input its current state and the (observable) states of the other agents if there's any, and updates the tactical mode of the ego agent. In this example, the decision logic is traight forward: When the x position of the car is above certain threshold, the car will starts to brake. This's no other agents in this scenario. The decision logic of the agent can be written in an expressive subset of Python inside function <code>decisionLogic</code>. The decision logic describe for an agent takes as input its current state and the (observable) states of the other agents if there's any, and updates the tactical mode of the ego agent. In this example, the decision logic is traight forward: When the x position of the car is above certain threshold, the car will starts to brake. This's no other agents in this scenario. The decision logic of the agent can be written in an expressive subset of Python inside function <code>decisionLogic</code>.
%% Cell type:code id:ba6e3ba2 tags: %% Cell type:code id:ba6e3ba2 tags:
``` python ```
import copy import copy
def decisionLogic(ego:State, track_map): def decisionLogic(ego:State, track_map):
output = copy.deepcopy(ego) output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal: if ego.agent_mode == AgentMode.Normal:
if ego.x > 10: if ego.x > 10:
output.agent_mode = AgentMode.Brake output.agent_mode = AgentMode.Brake
return output return output
``` ```
%% Cell type:markdown id:a6a323e4 tags: %% Cell type:markdown id:a6a323e4 tags:
We incoperate the above definition of tactical modes and decision logic into code strings and combine it with an imported agent flow, we can then obtain the agent for this sceanrio. We incoperate the above definition of tactical modes and decision logic into code strings and combine it with an imported agent flow, we can then obtain the agent for this sceanrio.
%% Cell type:code id:61837729 tags: %% Cell type:code id:61837729 tags:
``` python ```
dl = In[2]+"\n"+In[3]+"\n" + In[4]
from tutorial_agent import Agent1 from tutorial_agent import Agent1
car = Agent1('car', code=dl) car = Agent1('car', file_name="dl_sec1.py")
``` ```
%% Cell type:markdown id:9eb4979a tags: %% Cell type:markdown id:9eb4979a tags:
## 1.3 Creating scenario ## 1.3 Creating scenario
With the agent and map defined, we can now define the scenario. With the agent and map defined, we can now define the scenario.
%% Cell type:code id:b046fe36 tags: %% Cell type:code id:b046fe36 tags:
``` python ```
from verse.scenario import Scenario from verse.scenario import Scenario
scenario = Scenario() scenario = Scenario()
``` ```
%% Cell type:markdown id:549cd907 tags: %% Cell type:markdown id:549cd907 tags:
We can set the initial condition of the agent and add the agent We can set the initial condition of the agent and add the agent
%% Cell type:code id:6f54eada tags: %% Cell type:code id:6f54eada tags:
``` python ```
car.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0)) car.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0))
scenario.add_agent(car) scenario.add_agent(car)
``` ```
%% Cell type:markdown id:2366ed3a tags: %% Cell type:markdown id:2366ed3a tags:
and set the map for the sceanrio and set the map for the sceanrio
%% Cell type:code id:a1e2a90c tags: %% Cell type:code id:a1e2a90c tags:
``` python ```
scenario.set_map(map1) scenario.set_map(map1)
``` ```
%% Cell type:markdown id:52b2b0cb tags: %% Cell type:markdown id:52b2b0cb tags:
Since we only have one agent in the scenario, we don't need to specify a sensor. Since we only have one agent in the scenario, we don't need to specify a sensor.
%% Cell type:markdown id:b9e32951 tags: %% Cell type:markdown id:b9e32951 tags:
We can then compute simulation traces or reachable states for the scenario We can then compute simulation traces or reachable states for the scenario
%% Cell type:code id:cc1cdb50 tags: %% Cell type:code id:cc1cdb50 tags:
``` python ```
traces_simu = scenario.simulate(10, 0.01) traces_simu = scenario.simulate(10, 0.01)
traces_veri = scenario.verify(10, 0.01) traces_veri = scenario.verify(10, 0.01)
``` ```
%% Cell type:markdown id:4e33613e tags: %% Cell type:markdown id:4e33613e tags:
We can visualize the results using functions provided with Verse We can visualize the results using functions provided with Verse
%% Cell type:code id:c1d70fcf tags: %% Cell type:code id:c1d70fcf tags:
``` python ```
import plotly.graph_objects as go import plotly.graph_objects as go
from verse.plotter.plotter2D import * from verse.plotter.plotter2D import *
fig = go.Figure() fig = go.Figure()
fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
fig = go.Figure() fig = go.Figure()
fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
``` ```
%% Cell type:markdown id:1e162f7f tags: %% Cell type:markdown id:1e162f7f tags:
# 2. Adding multiple agents # 2. Adding multiple agents
%% Cell type:markdown id:e947eec4 tags: %% Cell type:markdown id:e947eec4 tags:
In the previous section, we played around with a scenario with a single vehicle. In this example, we will create a scenario with multiple agents and explore the potential of Verse to handle multi-agent scenarios. In the previous section, we played around with a scenario with a single vehicle. In this example, we will create a scenario with multiple agents and explore the potential of Verse to handle multi-agent scenarios.
%% Cell type:markdown id:7c233fa9 tags: %% Cell type:markdown id:7c233fa9 tags:
In this example, we will look at a two car braking example. Two cars will be running in same direction on the same lane with the front car running slower than the later car. The later car will brake and stop when it gets in 5m from the front car. In this example, we will look at a two car braking example. Two cars will be running in same direction on the same lane with the front car running slower than the later car. The later car will brake and stop when it gets in 5m from the front car.
%% Cell type:markdown id:cbe185ab tags: %% Cell type:markdown id:cbe185ab tags:
We will first setup a new scenario and add the map. We will first setup a new scenario and add the map.
%% Cell type:code id:a7ce4fd2 tags: %% Cell type:code id:a7ce4fd2 tags:
``` python ```
from verse.scenario import Scenario from verse.scenario import Scenario
from tutorial_map import M1 from tutorial_map import M1
scenario = Scenario() scenario = Scenario()
scenario.set_map(M1()) scenario.set_map(M1())
``` ```
%% Cell type:markdown id:ddae7760 tags: %% Cell type:markdown id:ddae7760 tags:
We will use the same tactical mode, track mode and state definition as last section. We will use the same tactical mode, track mode and state definition as last section.
%% Cell type:code id:32205aa3 tags: %% Cell type:code id:32205aa3 tags:
``` python ```
from enum import Enum, auto from enum import Enum, auto
class AgentMode(Enum): class AgentMode(Enum):
Normal = auto() Normal = auto()
Brake = auto() Brake = auto()
class TrackMode(Enum): class TrackMode(Enum):
T0 = auto() T0 = auto()
class State: class State:
x:float x:float
y:float y:float
theta:float theta:float
v:float v:float
agent_mode:AgentMode agent_mode:AgentMode
track_mode:TrackMode track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode): def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass pass
``` ```
%% Cell type:markdown id:38300e84 tags: %% Cell type:markdown id:38300e84 tags:
Verse's decision logic support python <code>any</code> and <code>all</code> functions, which allows the decision logic to quantify over other agents in the scenario. This enable user to easily create multi-agent scenario. In this case, the decision logic will take an additional argument <code>others</code>, which provides the states for other agents. Notice the type hint for both <code>ego</code> and <code>others</code>. The updated agent's decision logic looks like following. Verse's decision logic support python <code>any</code> and <code>all</code> functions, which allows the decision logic to quantify over other agents in the scenario. This enable user to easily create multi-agent scenario. In this case, the decision logic will take an additional argument <code>others</code>, which provides the states for other agents. Notice the type hint for both <code>ego</code> and <code>others</code>. The updated agent's decision logic looks like following.
%% Cell type:code id:57d0747c tags: %% Cell type:code id:57d0747c tags:
``` python ```
from typing import List from typing import List
import copy import copy
def decisionLogic(ego:State, others: List[State], track_map): def decisionLogic(ego:State, others: List[State], track_map):
output = copy.deepcopy(ego) output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal: if ego.agent_mode == AgentMode.Normal:
if any(other.x-ego.x< 8 and other.x-ego.x>0 for other in others): if any(other.x-ego.x< 8 and other.x-ego.x>0 for other in others):
output.agent_mode = AgentMode.Brake output.agent_mode = AgentMode.Brake
return output return output
``` ```
%% Cell type:code id:cb17f4b1 tags:
``` python
dl = In[12]+"\n"+In[13]
```
%% Cell type:markdown id:7c927d21 tags: %% Cell type:markdown id:7c927d21 tags:
With the updated decision logic, we can now spawn the two agents with their initial conditions. With the updated decision logic, we can now spawn the two agents with their initial conditions.
%% Cell type:code id:2187c4b7 tags: %% Cell type:code id:2187c4b7 tags:
``` python ```
from tutorial_agent import Agent1 from tutorial_agent import Agent1
car1 = Agent1('car1', code=dl) car1 = Agent1('car1', file_name="dl_sec2.py")
car1.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0)) car1.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0))
car2 = Agent1('car2', code=dl) car2 = Agent1('car2', file_name="dl_sec2.py")
car2.set_initial([[15,-0.5,0,1],[16,0.5,0,1]], (AgentMode.Normal, TrackMode.T0)) car2.set_initial([[15,-0.5,0,1],[16,0.5,0,1]], (AgentMode.Normal, TrackMode.T0))
``` ```
%% Cell type:markdown id:518d6ea4 tags: %% Cell type:markdown id:518d6ea4 tags:
We can then add both agents to the scenario We can then add both agents to the scenario
%% Cell type:code id:a16287c3 tags: %% Cell type:code id:a16287c3 tags:
``` python ```
scenario.add_agent(car1) scenario.add_agent(car1)
scenario.add_agent(car2) scenario.add_agent(car2)
``` ```
%% Cell type:markdown id:468ca941 tags: %% Cell type:markdown id:468ca941 tags:
With multiple agents in the scenario, we now need to add the sensor. The sensor defines how an agent is visible to other agents. In this example, we will use the default sensor function, which allows all agents to see all variables of other agents. With multiple agents in the scenario, we now need to add the sensor. The sensor defines how an agent is visible to other agents. In this example, we will use the default sensor function, which allows all agents to see all variables of other agents.
%% Cell type:code id:d39dbe69 tags: %% Cell type:code id:d39dbe69 tags:
``` python ```
from tutorial_sensor import DefaultSensor from tutorial_sensor import DefaultSensor
scenario.set_sensor(DefaultSensor()) scenario.set_sensor(DefaultSensor())
``` ```
%% Cell type:markdown id:db79f70b tags: %% Cell type:markdown id:db79f70b tags:
With the scenario fully constructed, we can now simulte or verify the scenario using the simulate/verify function provided by Verse. With the scenario fully constructed, we can now simulte or verify the scenario using the simulate/verify function provided by Verse.
%% Cell type:code id:c48ad5ad tags: %% Cell type:code id:c48ad5ad tags:
``` python ```
traces_simu = scenario.simulate(10, 0.01) traces_simu = scenario.simulate(10, 0.01)
traces_veri = scenario.verify(10, 0.01) traces_veri = scenario.verify(10, 0.01)
``` ```
%% Cell type:markdown id:fe9981ec tags: %% Cell type:markdown id:fe9981ec tags:
We can visualize the results using functions provided with Verse We can visualize the results using functions provided with Verse
%% Cell type:code id:5d180128 tags: %% Cell type:code id:5d180128 tags:
``` python ```
import plotly.graph_objects as go import plotly.graph_objects as go
from verse.plotter.plotter2D import * from verse.plotter.plotter2D import *
fig = go.Figure() fig = go.Figure()
fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
fig = go.Figure() fig = go.Figure()
fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
``` ```
%% Cell type:markdown id:42c81f78 tags: %% Cell type:markdown id:42c81f78 tags:
# 3. Adding safety assertions # 3. Adding safety assertions
%% Cell type:code id:d046cc9d tags: %% Cell type:code id:d046cc9d tags:
``` python ```
from verse.scenario import Scenario from verse.scenario import Scenario
from tutorial_map import M1 from tutorial_map import M1
scenario = Scenario() scenario = Scenario()
scenario.config.init_seg_length = 5 scenario.config.init_seg_length = 5
scenario.set_map(M1()) scenario.set_map(M1())
``` ```
%% Cell type:code id:9f137299 tags: %% Cell type:code id:9f137299 tags:
``` python ```
from enum import Enum, auto from enum import Enum, auto
class AgentMode(Enum): class AgentMode(Enum):
Normal = auto() Normal = auto()
Brake = auto() Brake = auto()
class TrackMode(Enum): class TrackMode(Enum):
T0 = auto() T0 = auto()
class State: class State:
x:float x:float
y:float y:float
theta:float theta:float
v:float v:float
agent_mode:AgentMode agent_mode:AgentMode
track_mode:TrackMode track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode): def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass pass
``` ```
%% Cell type:markdown id:ea4a9f2c tags: %% Cell type:markdown id:ea4a9f2c tags:
Verse allow checking safety conditions while performing simulation and verification. The safety conditions in verse can be specified using Python assert statements in the decision logic. With the <code>any</code> and <code>all</code> functions, the user can also define safety conditions between different agents. In this example, we are going to add a safety condition that the distance between two agents in x direction should always be greater than or equan to 1.0m. The updated decision logic is shown below. Verse allow checking safety conditions while performing simulation and verification. The safety conditions in verse can be specified using Python assert statements in the decision logic. With the <code>any</code> and <code>all</code> functions, the user can also define safety conditions between different agents. In this example, we are going to add a safety condition that the distance between two agents in x direction should always be greater than or equan to 1.0m. The updated decision logic is shown below.
%% Cell type:code id:7a5d64cb tags: %% Cell type:code id:7a5d64cb tags:
``` python ```
from typing import List from typing import List
import copy import copy
def decisionLogic(ego:State, others: List[State], track_map): def decisionLogic(ego:State, others: List[State], track_map):
output = copy.deepcopy(ego) output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal: if ego.agent_mode == AgentMode.Normal:
if any( other.x-ego.x< 8 and other.x-ego.x>0 for other in others): if any( other.x-ego.x< 8 and other.x-ego.x>0 for other in others):
output.agent_mode = AgentMode.Brake output.agent_mode = AgentMode.Brake
### Adding safety assertions ### Adding safety assertions
assert not any(other.x-ego.x<1.0 and other.x-ego.x>-1.0 for other in others), 'Seperation' assert not any(other.x-ego.x<1.0 and other.x-ego.x>-1.0 for other in others), 'Seperation'
########## ##########
return output return output
``` ```
%% Cell type:code id:ab2fa45a tags:
``` python
dl = In[21]+"\n"+In[22]
```
%% Cell type:markdown id:361154ca tags: %% Cell type:markdown id:361154ca tags:
We can then construct the two agents and the scenario exactly as previous section. We can then construct the two agents and the scenario exactly as previous section.
%% Cell type:code id:4251f544 tags: %% Cell type:code id:4251f544 tags:
``` python ```
from tutorial_agent import Agent1 from tutorial_agent import Agent1
car1 = Agent1('car1', code=dl) car1 = Agent1('car1', file_name="dl_sec3.py")
car1.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0)) car1.set_initial([[0,-0.5,0,2],[1,0.5,0,2]], (AgentMode.Normal, TrackMode.T0))
car2 = Agent1('car2', code=dl) car2 = Agent1('car2', file_name="dl_sec3.py")
car2.set_initial([[15,-0.5,0,1],[16,0.5,0,1]], (AgentMode.Normal, TrackMode.T0)) car2.set_initial([[15,-0.5,0,1],[16,0.5,0,1]], (AgentMode.Normal, TrackMode.T0))
scenario.add_agent(car1) scenario.add_agent(car1)
scenario.add_agent(car2) scenario.add_agent(car2)
from tutorial_sensor import DefaultSensor from tutorial_sensor import DefaultSensor
scenario.set_sensor(DefaultSensor()) scenario.set_sensor(DefaultSensor())
``` ```
%% Cell type:markdown id:5cb2f06a tags: %% Cell type:markdown id:5cb2f06a tags:
We can then simulate and verify the scenario and visualize the result. We can see from the result that this scenario is safe. We can then simulate and verify the scenario and visualize the result. We can see from the result that this scenario is safe.
%% Cell type:code id:736897de tags: %% Cell type:code id:736897de tags:
``` python ```
traces_simu = scenario.simulate(10, 0.01) traces_simu = scenario.simulate(10, 0.01)
traces_veri = scenario.verify(10, 0.01) traces_veri = scenario.verify(10, 0.01)
``` ```
%% Cell type:code id:e31dc9ff tags: %% Cell type:code id:e31dc9ff tags:
``` python ```
import plotly.graph_objects as go import plotly.graph_objects as go
from verse.plotter.plotter2D import * from verse.plotter.plotter2D import *
fig = go.Figure() fig = go.Figure()
fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = simulation_tree(traces_simu, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
fig = go.Figure() fig = go.Figure()
fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
``` ```
%% Cell type:markdown id:19ec1f20 tags: %% Cell type:markdown id:19ec1f20 tags:
If we tweak the initial condition of car1 by increasing it's speed to 6m/s and redo verification, the safety condition is violated and the result is shown in the plot. If we tweak the initial condition of car1 by increasing it's speed to 6m/s and redo verification, the safety condition is violated and the result is shown in the plot.
%% Cell type:code id:c6682e63 tags: %% Cell type:code id:c6682e63 tags:
``` python ```
scenario.set_init_single('car1',[[0,-0.5,0,5],[1,0.5,0,5]], (AgentMode.Normal, TrackMode.T0)) scenario.set_init_single('car1',[[0,-0.5,0,5],[1,0.5,0,5]], (AgentMode.Normal, TrackMode.T0))
traces_veri = scenario.verify(10, 0.01) traces_veri = scenario.verify(10, 0.01)
``` ```
%% Cell type:code id:5393d213 tags: %% Cell type:code id:5393d213 tags:
``` python ```
import plotly.graph_objects as go import plotly.graph_objects as go
from verse.plotter.plotter2D import * from verse.plotter.plotter2D import *
fig = go.Figure() fig = go.Figure()
fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace') fig = reachtube_tree(traces_veri, None, fig, 0, 1, [0, 1], 'lines', 'trace')
fig.show() fig.show()
``` ```
%% Cell type:markdown id:351d0b71 tags: %% Cell type:markdown id:351d0b71 tags:
# 4. Creating agent flow # 4. Creating agent flow
%% Cell type:markdown id:9ed472ab tags: %% Cell type:markdown id:9ed472ab tags:
In previous sections, we discussed about how to create the decision logic for agents in Verse, in section we will look into detail about how the agent flows are specified and how the pieces are combined together for an agent in Verse. In previous sections, we discussed about how to create the decision logic for agents in Verse, in section we will look into detail about how the agent flows are specified and how the pieces are combined together for an agent in Verse.
%% Cell type:markdown id:dd2ddad5 tags: %% Cell type:markdown id:dd2ddad5 tags:
The flow function define the continuous time evolution of agents' continuous states. It takes as input the initial states of the agent and the a time, and outputs the state of the agent from that initial states at that time. In Verse, the flow function is implemented by the <code>TC_simulate</code> function in the agent class. The <code>TC_simulate</code> takes as input a mode, a initial continuous states, a time bound, a simulation time step and the map. It will output simulation of agent dynamics at given mode starting from the initial continuous states, until the time bound with time step as an np array. Below shows an implementation of the <code>TC_simulate</code> function for the car agent. Note some detail helper functions for the car dynamics placed in <code>tutorial_utils</code> are not shown explicitly in the example below. The flow function define the continuous time evolution of agents' continuous states. It takes as input the initial states of the agent and the a time, and outputs the state of the agent from that initial states at that time. In Verse, the flow function is implemented by the <code>TC_simulate</code> function in the agent class. The <code>TC_simulate</code> takes as input a mode, a initial continuous states, a time bound, a simulation time step and the map. It will output simulation of agent dynamics at given mode starting from the initial continuous states, until the time bound with time step as an np array. Below shows an implementation of the <code>TC_simulate</code> function for the car agent. Note some detail helper functions for the car dynamics placed in <code>tutorial_utils</code> are not shown explicitly in the example below.
%% Cell type:code id:c1dda851 tags: %% Cell type:code id:c1dda851 tags:
``` python ```
from tutorial_utils import car_dynamics, car_action_handler from tutorial_utils import car_dynamics, car_action_handler
import numpy as np import numpy as np
from scipy.integrate import ode from scipy.integrate import ode
def TC_simulate(self, mode: List[str], initialCondition, time_bound, time_step, track_map=None)->np.ndarray: def TC_simulate(self, mode: List[str], initialCondition, time_bound, time_step, track_map=None)->np.ndarray:
time_bound = float(time_bound) time_bound = float(time_bound)
number_points = int(np.ceil(time_bound/time_step)) number_points = int(np.ceil(time_bound/time_step))
t = [round(i*time_step,10) for i in range(0,number_points)] t = [round(i*time_step,10) for i in range(0,number_points)]
init = initialCondition init = initialCondition
trace = [[0]+init] trace = [[0]+init]
for i in range(len(t)): for i in range(len(t)):
steering, a = car_action_handler(mode, init, track_map) steering, a = car_action_handler(mode, init, track_map)
r = ode(car_dynamics) r = ode(car_dynamics)
r.set_initial_value(init).set_f_params([steering, a]) r.set_initial_value(init).set_f_params([steering, a])
res:np.ndarray = r.integrate(r.t + time_step) res:np.ndarray = r.integrate(r.t + time_step)
init = res.flatten().tolist() init = res.flatten().tolist()
if init[3] < 0: if init[3] < 0:
init[3] = 0 init[3] = 0
trace.append([t[i] + time_step] + init) trace.append([t[i] + time_step] + init)
return np.array(trace) return np.array(trace)
``` ```
%% Cell type:markdown id:3c2e6579 tags: %% Cell type:markdown id:3c2e6579 tags:
With the <code>TC_simulate</code> function specified, we can now combine all parts together to construct a new car agent. An agent class for Verse should have three attributes: 1) <code>id</code>: an unique identifier for each agent in a scenario, 2) <code>controller</code>: a <code>ControllerIR</code> object, which is an intermediate representation of decisionLogic in Verse. It can be constructed automatically by passing in the decision logic code strings described in previous sections, and 3) <code>TC_simulate</code> function. In this example we will create the agent class manually. However, the agent class can also be inherited from the <code>BaseAgent</code> class with proper arguments to automatically having all required fields. With the <code>TC_simulate</code> function specified, we can now combine all parts together to construct a new car agent. An agent class for Verse should have three attributes: 1) <code>id</code>: an unique identifier for each agent in a scenario, 2) <code>controller</code>: a <code>ControllerIR</code> object, which is an intermediate representation of decisionLogic in Verse. It can be constructed automatically by passing in the decision logic code strings described in previous sections, and 3) <code>TC_simulate</code> function. In this example we will create the agent class manually. However, the agent class can also be inherited from the <code>BaseAgent</code> class with proper arguments to automatically having all required fields.
%% Cell type:code id:86626628 tags: %% Cell type:code id:86626628 tags:
``` python ```
class Agent2: class Agent2:
pass pass
``` ```
%% Cell type:code id:2a233433 tags: %% Cell type:code id:2a233433 tags:
``` python ```
``` ```
......
tutorial/dl_sec1.py 0 → 100644
+ 27
− 0
View file @ ebb00993
from enum import Enum, auto
class AgentMode(Enum):
Normal = auto()
Brake = auto()
class TrackMode(Enum):
T0 = auto()
class State:
x:float
y:float
theta:float
v:float
agent_mode:AgentMode
track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass
import copy
def decisionLogic(ego:State, track_map):
output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal:
if ego.x > 10:
output.agent_mode = AgentMode.Brake
return output
\ No newline at end of file
tutorial/dl_sec2.py 0 → 100644
+ 28
− 0
View file @ ebb00993
from enum import Enum, auto
class AgentMode(Enum):
Normal = auto()
Brake = auto()
class TrackMode(Enum):
T0 = auto()
class State:
x:float
y:float
theta:float
v:float
agent_mode:AgentMode
track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass
from typing import List
import copy
def decisionLogic(ego:State, others: List[State], track_map):
output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal:
if any( other.x-ego.x< 8 and other.x-ego.x>0 for other in others):
output.agent_mode = AgentMode.Brake
return output
\ No newline at end of file
tutorial/dl_sec3.py 0 → 100644
+ 33
− 0
View file @ ebb00993
from enum import Enum, auto
class AgentMode(Enum):
Normal = auto()
Brake = auto()
class TrackMode(Enum):
T0 = auto()
class State:
x:float
y:float
theta:float
v:float
agent_mode:AgentMode
track_mode:TrackMode
def __init__(self, x, y, theta, v, agent_mode: AgentMode, track_mode: TrackMode):
pass
from typing import List
import copy
def decisionLogic(ego:State, others: List[State], track_map):
output = copy.deepcopy(ego)
if ego.agent_mode == AgentMode.Normal:
if any( other.x-ego.x< 8 and other.x-ego.x>0 for other in others):
output.agent_mode = AgentMode.Brake
### Adding safety assertions
assert not any(other.x-ego.x<1.0 and other.x-ego.x>-1.0 for other in others), 'Seperation'
##########
return output
\ No newline at end of file
verse/analysis/verifier.py
+ 1
− 1
View file @ ebb00993
...@@ -10,7 +10,6 @@ import numpy as np ...@@ -10,7 +10,6 @@ import numpy as np
from verse.analysis.analysis_tree import AnalysisTreeNode, AnalysisTree from verse.analysis.analysis_tree import AnalysisTreeNode, AnalysisTree
from verse.analysis.dryvr import calc_bloated_tube, SIMTRACENUM from verse.analysis.dryvr import calc_bloated_tube, SIMTRACENUM
from verse.analysis.mixmonotone import calculate_bloated_tube_mixmono_cont, calculate_bloated_tube_mixmono_disc from verse.analysis.mixmonotone import calculate_bloated_tube_mixmono_cont, calculate_bloated_tube_mixmono_disc
from verse.analysis.NeuReach.NeuReach_onestep_rect import postCont
from verse.analysis.incremental import ReachTubeCache, TubeCache, convert_reach_trans, to_simulate, combine_all from verse.analysis.incremental import ReachTubeCache, TubeCache, convert_reach_trans, to_simulate, combine_all
from verse.analysis.utils import dedup from verse.analysis.utils import dedup
from verse.parser.parser import find from verse.parser.parser import find
...@@ -193,6 +192,7 @@ class Verifier: ...@@ -193,6 +192,7 @@ class Verifier:
lane_map = lane_map lane_map = lane_map
) )
elif reachability_method == "NeuReach": elif reachability_method == "NeuReach":
from verse.analysis.NeuReach.NeuReach_onestep_rect import postCont
cur_bloated_tube = postCont( cur_bloated_tube = postCont(
mode, mode,
inits[0], inits[0],
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment