Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
li213
DryVRtool
Commits
93f9d78a
Commit
93f9d78a
authored
Dec 01, 2021
by
li213
Browse files
fixing existing dryvr examples
parent
5bc495c7
Changes
19
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
93f9d78a
...
...
@@ -207,3 +207,7 @@ fabric.properties
# Sonarlint plugin
.idea/sonarlint
.vscode/
# output/
# config
# output.txt
\ No newline at end of file
examples/AF_rendezvous/rendezvous_sim.py
View file @
93f9d78a
...
...
@@ -163,29 +163,29 @@ def plot_total_force(arr):
# - Each step is timed so that it is obvious what the limiting functions are.
###########################
def
TC_Simulate
(
curLabel
,
initCondition
,
transiteTime
):
print
"
\n
~~~ Starting Simulation ~~~"
print
(
"
\n
~~~ Starting Simulation ~~~"
)
start
=
dt
.
datetime
.
now
()
time
=
dt
.
datetime
.
now
()
arr
=
generate_trace
(
curLabel
,
initCondition
,
transiteTime
)
print
'
\t
Generated Trace:'
,
(
dt
.
datetime
.
now
()
-
time
).
total_seconds
()
*
1000
,
'ms'
print
(
'
\t
Generated Trace:'
,
(
dt
.
datetime
.
now
()
-
time
).
total_seconds
()
*
1000
,
'ms'
)
time
=
dt
.
datetime
.
now
()
arr
=
add_variables
(
arr
)
print
'
\t
Added Variables:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
print
(
'
\t
Added Variables:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
)
time
=
dt
.
datetime
.
now
()
arr
=
calculate_acceleration
(
arr
)
print
'
\t
Calculated Acceleration:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
print
(
'
\t
Calculated Acceleration:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
)
time
=
dt
.
datetime
.
now
()
arr
=
compact_trace
(
arr
,
100
)
print
'
\t
Compacted Trace:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
print
(
'
\t
Compacted Trace:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
)
time
=
dt
.
datetime
.
now
()
arr
=
calculate_forces
(
arr
)
print
'
\t
Calculated Forces:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
print
(
'
\t
Calculated Forces:'
,
(
dt
.
datetime
.
now
()
-
time
).
microseconds
/
1000
,
'ms'
)
print
"Completed:"
,
(
dt
.
datetime
.
now
()
-
start
).
total_seconds
()
*
1000
,
'ms'
print
"Trace Length:"
,
len
(
arr
)
print
(
"Completed:"
,
(
dt
.
datetime
.
now
()
-
start
).
total_seconds
()
*
1000
,
'ms'
)
print
(
"Trace Length:"
,
len
(
arr
)
)
return
arr
examples/BM_15/BM_15.py
View file @
93f9d78a
...
...
@@ -70,7 +70,7 @@ if __name__ == "__main__":
sol
=
TC_Simulate
(
"Default"
,
[
0.0060145
,
-
0.0009624
,
0.0177578
,
-
0.0047553
,
0.0177717
,
-
0.0122932
,
-
0.0026115
,
-
0.0122392
,
0.0014043
,
-
0.0219818
,
-
0.0396104
,
-
0.0042632
,
-
0.0070418
,
-
0.009347
,
0.0022889
],
10.0
)
for
s
in
sol
:
print
(
s
)
print
(
s
)
# time = [row[0] for row in sol]
...
...
examples/BM_48/BM_48.py
View file @
93f9d78a
...
...
@@ -135,7 +135,7 @@ if __name__ == "__main__":
sol
=
TC_Simulate
(
"Default"
,
[
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0002
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
-
0.0001
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
10.0
)
for
s
in
sol
:
print
(
s
)
print
(
s
)
# time = [row[0] for row in sol]
...
...
examples/billiard/billiard_sim.py
View file @
93f9d78a
...
...
@@ -21,7 +21,7 @@ def TC_Simulate(Modes,initialCondition,time_bound):
return
Final_trace
if
__name__
==
"__main__"
:
trace
=
TC_Simulate
(
"normal"
,
[
0
,
0
,
1
,
1
],
5
)
print
trace
print
(
trace
)
trace
=
TC_Simulate
(
"normal;normal"
,
[
0
,
0
,
1
,
0
,
0
,
0
,
0
,
1
],
5
)
print
trace
print
(
trace
)
examples/c2e2wrapper.py
View file @
93f9d78a
...
...
@@ -41,6 +41,7 @@ def invokeSimulator(modeNum, simFile, initial, timeStep, remainTime):
result
=
[]
for
line
in
f
:
line
=
map
(
float
,
line
.
strip
().
split
(
' '
))
line
=
list
(
line
)
if
not
result
:
result
.
append
(
line
)
elif
line
[
0
]
==
result
[
-
1
][
0
]:
...
...
examples/cars_fix/Car_Dynamic_Single.py
View file @
93f9d78a
...
...
@@ -185,11 +185,11 @@ def Car_simulate(Mode,initial,time_bound):
return
trace
if
__name__
==
"__main__"
:
print
"start test"
print
(
"start test"
)
# 16.67*3.6 = 60km/hr
traj
=
Car_simulate
(
"TurnRight"
,
[
0.0
,
0.0
,
0.0
,
21.16
],
"10"
)
for
line
in
traj
:
print
line
print
(
line
)
# # x = [16.67, 4.17, 30.0, 20.0, 25.0, 10.0,8.0,5.0,3.0,27.5,17.5,2,12.5,1]
# # y = [0.014,0.22,0.0043,0.0097,0.0061,0.039,0.069,0.155,0.43,0.0052,0.0125,0.97,0.025,4.03]
# speed = 30
...
...
examples/cars_fix/simulate.py
View file @
93f9d78a
...
...
@@ -25,8 +25,8 @@ def simulate(g,initialCondition,Time_horizon):
simResult
=
[]
while
remainTime
>
0
:
print
'-----------------------------------------------------'
print
'Current State'
,
g
.
vs
[
Current_Vertex
][
'label'
]
print
(
'-----------------------------------------------------'
)
print
(
'Current State'
,
g
.
vs
[
Current_Vertex
][
'label'
]
)
Current_successors
=
g
.
successors
(
Current_Vertex
)
if
len
(
Current_successors
)
==
0
:
...
...
examples/navigation/nav_ode.py
View file @
93f9d78a
...
...
@@ -51,6 +51,6 @@ def TC_Simulate(Mode,initialCondition,time_bound):
return
trace
if
__name__
==
"__main__"
:
ret
=
TC_
s
imulate
(
"Zone3"
,
[
0.5
,
0.5
,
0.0
,
0.0
],
2
)
ret
=
TC_
S
imulate
(
"Zone3"
,
[
0.5
,
0.5
,
0.0
,
0.0
],
2
)
for
r
in
ret
:
print
r
print
(
r
)
examples/newcars/Car_Sim.py
View file @
93f9d78a
...
...
@@ -16,10 +16,10 @@ def TC_Simulate(Modes,initialCondition,time_bound):
Final_trace
=
trace
else
:
if
len
(
trace
)
!=
len
(
Final_trace
):
print
len
(
trace
),
len
(
Final_trace
)
print
(
len
(
trace
),
len
(
Final_trace
)
)
for
i
in
range
(
min
(
len
(
trace
),
len
(
Final_trace
))):
print
trace
[
i
][
0
],
Final_trace
[
i
][
0
]
print
Final_trace
print
(
trace
[
i
][
0
],
Final_trace
[
i
][
0
]
)
print
(
Final_trace
)
Final_trace
=
np
.
concatenate
((
Final_trace
,
trace
[:,
1
:
6
]),
axis
=
1
)
else
:
print
(
'Number of cars does not match the initial condition'
)
...
...
@@ -30,15 +30,15 @@ if __name__ == "__main__":
sol
=
TC_Simulate
(
"Dec"
,
[
0
,
0
,
0
,
1
,
0.0
],
30
)
# for line in sol:
# print
line
# print
(
line
#nextsol = TC_Simulate("TurnRight",sol[-1][1:],50)#2.4
#finalsol = TC_Simulate("Const",nextsol[-1][1:],1.5)
#print
sol
#print
(
sol
#for i in sol:
# print
i
# print
(
i
#for j in nextsol:
# print
j
# print
(
j
#nextsoltime = [(row[0]+sol[-1][0]) for row in nextsol]
#sxnext = [row[1] for row in nextsol]
...
...
examples/rrtcars/Car_Sim.py
View file @
93f9d78a
...
...
@@ -17,7 +17,7 @@ def TC_Simulate(Modes,initialCondition,time_bound):
def
main
():
t
=
TC_Simulate
(
"TurnLeft"
,
[
0
,
15
,
0
,
0
],
10
)
for
line
in
t
:
print
line
print
(
line
)
if
__name__
==
"__main__"
:
main
()
examples/spiking_neuron/spiking_neuron.py
View file @
93f9d78a
...
...
@@ -46,7 +46,7 @@ if __name__ == "__main__":
sol
=
TC_Simulate
(
"Default"
,
[
-
50
,
0.0
],
100.0
)
for
s
in
sol
:
print
(
s
)
print
(
s
)
# time = [row[0] for row in sol]
...
...
examples/vehicle_platoon_3/vehicle_dynamic.py
View file @
93f9d78a
...
...
@@ -69,6 +69,6 @@ if __name__ == "__main__":
sol
=
TC_Simulate
(
"l1"
,
[
1.0
,
1.0
,
1.0
,
1.0
,
1.0
,
1.0
,
1.0
,
1.0
,
1.0
],
2.0
)
for
s
in
sol
:
print
(
s
)
print
(
s
)
\ No newline at end of file
input/daginput/input_autopassingUnsafe.json
View file @
93f9d78a
{
"vertex"
:[
"Acc1;Const"
,
"TurnLeft;Const"
,
"Acc2;Const"
,
"Dec;Const"
,
"TurnRight;Const"
,
"Const;Const"
,
"Acc1;Acc1"
,
"Dec;Acc1"
,
"TurnRight;Acc1"
,
"Acc1;Dec"
,
"Const;Dec"
,
"TurnRight;Const"
],
"edge"
:[[
0
,
1
],[
1
,
2
],[
2
,
3
],[
3
,
4
],[
4
,
5
],[
1
,
6
],[
6
,
7
],[
7
,
8
],[
8
,
5
],[
1
,
9
],[
9
,
10
],[
10
,
11
],[
11
,
5
]],
"guards"
:[
"variables"
:[
"car1_x"
,
"car1_y"
,
"car1_vx"
,
"car1_vy"
,
"car2_x"
,
"car2_y"
,
"car2_vx"
,
"car2_vy"
],
"guards"
:[
"And(t>5.0,t<=6.0)"
,
"And(t>10.0,t<=12.0)"
,
"And(t>5.0,t<=6.0)"
,
...
...
input/daginput/input_breakSplit.json
View file @
93f9d78a
...
...
@@ -4,7 +4,7 @@
"variables"
:[
"car1_x"
,
"car1_y"
,
"car1_vx"
,
"car1_vy"
,
"car2_x"
,
"car2_y"
,
"car2_vx"
,
"car2_vy"
],
"guards"
:[
"And(t>1.0,t<=2.0)"
,
"And(t>2
,
5,t<=3.5)"
"And(t>2
.
5,t<=3.5)"
],
"initialSet"
:[[
0.0
,
-3.0
,
0.0
,
1.0
,
0.0
,
-23.0
,
0.0
,
0.0
],[
0.0
,
3.0
,
0.0
,
1.0
,
0.0
,
-14.0
,
0.0
,
0.0
]],
"unsafeSet"
:
"@Allmode:And(car1_y-car2_y<3)"
,
...
...
main.py
View file @
93f9d78a
...
...
@@ -13,6 +13,9 @@ with open(sys.argv[-1], 'r') as f:
data
=
json
.
load
(
f
)
simFunction
=
importSimFunction
(
data
[
"directory"
])
safety
,
reach
=
verify
(
data
,
simFunction
)
lines
=
reach
.
raw
.
split
(
"
\n
"
)
print
(
type
(
lines
[
0
]),
lines
[
0
])
initNode
,
y_min
,
y_max
=
parse
(
lines
)
if
safety
==
'SAFE'
:
lines
=
reach
.
raw
.
split
(
"
\n
"
)
print
(
type
(
lines
[
0
]),
lines
[
0
])
initNode
,
y_min
,
y_max
=
parse
(
lines
)
# elif safety == 'UNSAFE':
# print('')
\ No newline at end of file
src/common/utils.py
View file @
93f9d78a
...
...
@@ -65,6 +65,8 @@ def randomPoint(lower, upper):
random point (either float or list of float)
"""
# random.seed(4)
if
isinstance
(
lower
,
int
)
or
isinstance
(
lower
,
float
):
return
random
.
uniform
(
lower
,
upper
)
...
...
src/core/dryvrcore.py
View file @
93f9d78a
...
...
@@ -268,6 +268,7 @@ def calc_bloated_tube(
Bloated reach tube
"""
random
.
seed
(
4
)
cur_center
=
calcCenterPoint
(
initial_set
[
0
],
initial_set
[
1
])
cur_delta
=
calcDelta
(
initial_set
[
0
],
initial_set
[
1
])
traces
=
[
sim_func
(
mode_label
,
cur_center
,
time_horizon
)]
...
...
src/discrepancy/Global_Disc.py
View file @
93f9d78a
...
...
@@ -8,7 +8,8 @@ import scipy as sp
import
scipy.spatial
_TRUE_MIN_CONST
=
-
10
_EPSILON
=
1.0e-100
_EPSILON
=
1.0e-6
_SMALL_EPSILON
=
1e-10
def
get_reachtube_segment
(
training_traces
:
np
.
ndarray
,
initial_radii
:
np
.
ndarray
,
method
=
'PWGlobal'
)
->
np
.
array
:
...
...
@@ -105,7 +106,7 @@ def all_sensitivities_calc(training_traces: np.ndarray, initial_radii: np.ndarra
normalizing_initial_set_radii
[
np
.
where
(
normalizing_initial_set_radii
==
0
)]
=
1.0
for
cur_dim_ind
in
range
(
1
,
ndims
):
normalized_initial_points
:
np
.
array
=
training_traces
[:,
0
,
1
:]
/
normalizing_initial_set_radii
initial_distances
=
sp
.
spatial
.
distance
.
pdist
(
normalized_initial_points
,
'chebyshev'
)
initial_distances
=
sp
.
spatial
.
distance
.
pdist
(
normalized_initial_points
,
'chebyshev'
)
+
_SMALL_EPSILON
for
cur_time_ind
in
range
(
1
,
trace_len
):
y_points
[
cur_dim_ind
-
1
,
cur_time_ind
-
1
]
=
np
.
max
((
sp
.
spatial
.
distance
.
pdist
(
np
.
reshape
(
training_traces
[:,
cur_time_ind
,
cur_dim_ind
],
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment