Skip to content

Commit

Permalink
Merge pull request #5 from stanleybak/unstable
Browse files Browse the repository at this point in the history 
Unstable
  • Loading branch information
@stanleybak
stanleybak authored Jun 3, 2019
2 parents d2a499a + 1cc4fb8 commit 06cb254
Show file tree
Hide file tree
Showing 23 changed files with 1,453 additions and 291 deletions.
96 changes: 96 additions & 0 deletions examples/approx_model/approx_model.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
'''
Harmonic Oscillator Example in Hylaa, demonstrating using
various approximation models for continuous-time reachability
dynamics are:
x' = y + u1
y' = -x
starting from [-5, -4], [0, 1]
with u1 in [-0.2, 0.2]
'''

import math

import numpy as np
from scipy.sparse import csr_matrix

from hylaa.hybrid_automaton import HybridAutomaton
from hylaa.settings import HylaaSettings, PlotSettings
from hylaa.core import Core
from hylaa.stateset import StateSet
from hylaa import lputil

def define_ha():
'''make the hybrid automaton'''

ha = HybridAutomaton()

a_matrix = [[0, 1], [-1, 0]]

b_mat = [[1], [0]]
b_constraints = [[1], [-1]]
b_rhs = [0.2, 0.2]

mode = ha.new_mode('mode')
mode.set_dynamics(a_matrix)
mode.set_inputs(b_mat, b_constraints, b_rhs)

return ha

def make_init(ha):
'''returns list of initial states'''

mode = ha.modes['mode']
# init states: x in [-5, -4], y in [0, 1]
#init_lpi = lputil.from_box([[-5, -4], [0, 1]], mode)
init_lpi = lputil.from_box([[-5, -5], [0, 0]], mode)

init_list = [StateSet(init_lpi, mode)]

return init_list

def define_settings():
'get the hylaa settings object'

step = math.pi/16
max_time = 2*math.pi
settings = HylaaSettings(step, max_time)

plot_settings = settings.plot
plot_settings.plot_mode = PlotSettings.PLOT_IMAGE
plot_settings.xdim_dir = 0
plot_settings.ydim_dir = 1

#plot_settings.plot_mode = PlotSettings.PLOT_VIDEO
#plot_settings.filename = 'ha.mp4'
#plot_settings.video_fps = 2
#plot_settings.video_extra_frames = 10 # extra frames at the end of a video so it doesn't end so abruptly
#plot_settings.video_pause_frames = 5 # frames to render in video whenever a 'pause' occurs

plot_settings.label.y_label = '$y$'
plot_settings.label.x_label = '$x$'
plot_settings.label.title = 'Harmonic Oscillator'

return settings

def run_hylaa():
'Runs hylaa with the given settings'

ha = define_ha()
settings = define_settings()

tuples = []
tuples.append((HylaaSettings.APPROX_NONE, "approx_none.png"))
tuples.append((HylaaSettings.APPROX_CHULL, "approx_chull.png"))
tuples.append((HylaaSettings.APPROX_LGG, "approx_lgg.png"))

for model, filename in tuples:
settings.approx_model, settings.plot.filename = model, filename

init_states = make_init(ha)
print(f"\nMaking {filename}...")
Core(ha, settings).run(init_states)

if __name__ == '__main__':
run_hylaa()
23 changes: 16 additions & 7 deletions examples/building/building.py
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
'''
Building Example in Hylaa. This is the building example from
ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics
ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics
originally from
Expand Down Expand Up @@ -76,7 +76,6 @@ def make_init(ha):

bounds_list.append((lb, ub))


mode = ha.modes['mode']
init_lpi = lputil.from_box(bounds_list, mode)

Expand All @@ -97,7 +96,7 @@ def define_settings(ha, limit):
#settings.time_elapse.scipy_sim.rtol = 1e-9
#settings.time_elapse.scipy_sim.atol = 1e-12

#settings.skip_step_times = False
settings.stdout = stdout = HylaaSettings.STDOUT_VERBOSE

plot_settings = settings.plot

Expand All @@ -117,6 +116,7 @@ def define_settings(ha, limit):
plot_settings.label.big(size=36)

settings.stop_on_concrete_error = False
settings.make_counterexample = False

line = [(0.0, -limit), (max_time, -limit)]
lc = collections.LineCollection([line], animated=True, colors=('red'), linewidths=(1), linestyle='dashed')
Expand All @@ -131,10 +131,19 @@ def run_hylaa():
limit = 0.005 # unreachable

ha = define_ha(limit)
settings = define_settings(ha, limit)
init_states = make_init(ha)

Core(ha, settings).run(init_states)

tuples = []
tuples.append((HylaaSettings.APPROX_NONE, "approx_none.png"))
tuples.append((HylaaSettings.APPROX_CHULL, "approx_chull.png"))
#tuples.append((HylaaSettings.APPROX_LGG, "approx_lgg.png"))

for model, filename in tuples:
settings = define_settings(ha, limit)
settings.approx_model, settings.plot.filename = model, filename

init_states = make_init(ha)
print(f"\nMaking {filename}...")
Core(ha, settings).run(init_states)

if __name__ == '__main__':
run_hylaa()
5 changes: 3 additions & 2 deletions examples/deaggregation/deaggregation.py → examples/deaggregation/deag_example.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,10 +73,11 @@ def make_settings(unsafe_box):

settings.plot.video_pause_frames = 5
settings.plot.video_fps = 5
settings.plot.plot_mode = PlotSettings.PLOT_IMAGE
settings.plot.plot_mode = PlotSettings.PLOT_NONE
settings.plot.interactive_skip_count = 5

#settings.plot.plot_mode = PlotSettings.PLOT_VIDEO
#settings.plot.filename = "deaggregation.mp4"
#settings.plot.filename = "deagg_example.mp4"

settings.stop_on_aggregated_error = False
settings.aggstrat.deaggregate = True # use deaggregation
Expand Down
4 changes: 2 additions & 2 deletions examples/harmonic_oscillator/ha.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ def make_init(ha):
def define_settings():
'get the hylaa settings object'

step = math.pi/8
max_time = 3 * math.pi / 2
step = math.pi/4
max_time = 1 * math.pi / 2
settings = HylaaSettings(step, max_time)

plot_settings = settings.plot
Expand Down
120 changes: 75 additions & 45 deletions examples/rendezvous/rendezvous.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,14 @@
from hylaa.settings import HylaaSettings, PlotSettings, LabelSettings
from hylaa.core import Core
from hylaa.stateset import StateSet
from hylaa import lputil
from hylaa import lputil, aggstrat

def make_automaton(safe):
def make_automaton(safe, passive_time=120):
'make the hybrid automaton'

ha = HybridAutomaton('Spacecraft Rendezvous with Abort')
ha = HybridAutomaton(f'Spacecraft Rendezvous (Abort at t={passive_time})')

passive_time += 1e-4 # ensures switch to passive at a single step intead of at two steps

############## Modes ##############
p2 = ha.new_mode('P2')
Expand All @@ -32,8 +34,8 @@ def make_automaton(safe):
[-0.000174031357370456, -0.0665123984901026, -0.00875351105536225, -2.90300269286856, 0.0, 0.0], \
[0.0, 0.0, 0.0, 0.0, 0.0, 1.0], \
[0, 0, 0, 0, 0, 0]]
inv_mat = [[0.0, 0.0, 0.0, 0.0, 1.0, 0], [1.0, 0.0, 0.0, 0.0, 0.0, 0]]
inv_rhs = [125.0, -100.0]
inv_mat = [[0.0, 0.0, 0.0, 0.0, 1.0, 0], [1.0, 0.0, 0.0, 0.0, 0.0, 0], [0., 0., 0., 0., 1., 0]]
inv_rhs = [125.0, -100.0, passive_time]
p2.set_dynamics(a_mat)
p2.set_invariant(inv_mat, inv_rhs)

Expand All @@ -56,7 +58,7 @@ def make_automaton(safe):
[-1.0, 1.0, 0., 0., 0., 0], \
[1.0, -1.0, 0., 0., 0., 0], \
[0., 0., 0., 0., 1., 0]]
inv_rhs = [100, 100, 100, 100, 141.1, 141.1, 141.1, 141.1, 120.0]
inv_rhs = [100, 100, 100, 100, 141.1, 141.1, 141.1, 141.1, passive_time]
p3.set_dynamics(a_mat)
p3.set_invariant(inv_mat, inv_rhs)

Expand Down Expand Up @@ -88,9 +90,9 @@ def make_automaton(safe):
guard_rhs = [100, 100, 100, 100, 141.1, 141.1, 141.1, 141.1]
t1.set_guard(guard_mat, guard_rhs)

ha.new_transition(p2, passive).set_guard([[0.0, 0.0, 0.0, 0.0, -1.0, 0]], [-120])
ha.new_transition(p2, passive).set_guard([[0.0, 0.0, 0.0, 0.0, -1.0, 0]], [-passive_time])

ha.new_transition(p3, passive).set_guard([[0.0, 0.0, 0.0, 0.0, -1.0, 0]], [-120])
ha.new_transition(p3, passive).set_guard([[0.0, 0.0, 0.0, 0.0, -1.0, 0]], [-passive_time])

############## Error Transitions ##############
# In the aborting mode, the vehicle must avoid the target, which is modeled as a box B with
Expand All @@ -107,9 +109,9 @@ def make_automaton(safe):

#In the rendezvous attempt the spacecraft must remain within the lineof-sight
#cone L = {[x, y]^T | (x >= -100m) AND (y >= x*tan(30)) AND (-y >= x*tan(30))}
ha.new_transition(p3, error).set_guard([[1, 0, 0., 0., 0., 0]], [-100])
ha.new_transition(p3, error).set_guard([[-0.57735, 1, 0, 0., 0., 0]], [0])
ha.new_transition(p3, error).set_guard([[-0.57735, -1, 0., 0., 0., 0]], [0])
ha.new_transition(p3, error, 'los1').set_guard([[1, 0, 0., 0., 0., 0]], [-100])
ha.new_transition(p3, error, 'los2').set_guard([[-0.57735, 1, 0, 0., 0., 0]], [0])
ha.new_transition(p3, error, 'los3').set_guard([[-0.57735, -1, 0., 0., 0., 0]], [0])

# sqrt(vx^2 + vy^2) should stay below 0.055 m/SECOND (time in model is in MINUTES)
# to make the model unsafe, try changing this to 0.05
Expand All @@ -118,61 +120,89 @@ def make_automaton(safe):
h = meters_per_min_limit * math.cos(math.pi / 8.0)
w = meters_per_min_limit * math.sin(math.pi / 8.0)

ha.new_transition(p3, error).set_guard([[0, 0, 1., 0., 0., 0]], [-h])
ha.new_transition(p3, error).set_guard([[0, 0, -1., 0., 0., 0]], [-h])
ha.new_transition(p3, error).set_guard([[0, 0, 0., 1., 0., 0]], [-h])
ha.new_transition(p3, error).set_guard([[0, 0, 0., -1., 0., 0]], [-h])

ha.new_transition(p3, error).set_guard([[0, 0, 1., 1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error).set_guard([[0, 0, -1., 1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error).set_guard([[0, 0, -1., -1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error).set_guard([[0, 0, 1., -1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error, 'g1').set_guard([[0, 0, 1., 0., 0., 0]], [-h])
ha.new_transition(p3, error, 'g2').set_guard([[0, 0, -1., 0., 0., 0]], [-h])
ha.new_transition(p3, error, 'g3').set_guard([[0, 0, 0., 1., 0., 0]], [-h])
ha.new_transition(p3, error, 'g4').set_guard([[0, 0, 0., -1., 0., 0]], [-h])

ha.new_transition(p3, error, 'g5').set_guard([[0, 0, 1., 1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error, 'g6').set_guard([[0, 0, -1., 1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error, 'g7').set_guard([[0, 0, -1., -1., 0., 0]], [-(w + h)])
ha.new_transition(p3, error, 'g8').set_guard([[0, 0, 1., -1., 0., 0]], [-(w + h)])

return ha

def make_init(ha):
'make the initial states'

p2 = ha.modes['P2']
init_lpi = lputil.from_box([(-925.0, -875.0), (-425.0, -375.0), (0.0, 0.0), (0.0, 0.0), (0.0, 0.0), (1.0, 1.0)], p2)

box = [(-925.0, -875.0), (-425.0, -375.0), (0.0, 0.0), (0.0, 0.0), (0.0, 0.0), (1.0, 1.0)]

init_lpi = lputil.from_box(box, p2)
init_list = [StateSet(init_lpi, p2)]

#corners = [[(box[0][0], box[0][0]), (box[1][0], box[1][0]), (0, 0), (0, 0), (0, 0), (1, 1)], \
# [(box[0][1], box[0][1]), (box[1][0], box[1][0]), (0, 0), (0, 0), (0, 0), (1, 1)], \
# [(box[0][1], box[0][1]), (box[1][1], box[1][1]), (0, 0), (0, 0), (0, 0), (1, 1)], \
# [(box[0][0], box[0][0]), (box[1][0], box[1][0]), (0, 0), (0, 0), (0, 0), (1, 1)]]

#init_list = [StateSet(lputil.from_box(c, p2), p2) for c in corners]

return init_list

def make_settings(safe):
def make_settings(safe, passive_time=120):
'make the reachability settings object'

# see hylaa.settings for a list of reachability settings
settings = HylaaSettings(1.0, 200.0) # step: 0.1, bound: 200.0
settings.plot.plot_mode = PlotSettings.PLOT_IMAGE
settings = HylaaSettings(0.1, 300.0) # step: 0.1, bound: 200.0
settings.plot.plot_mode = PlotSettings.PLOT_NONE #IMAGE
settings.stdout = HylaaSettings.STDOUT_VERBOSE

settings.plot.filename = "rendezvous.png"
settings.plot.plot_size = (10, 10)

settings.plot.xdim_dir = [0, 2]
settings.plot.ydim_dir = [1, 3]
settings.plot.label = [LabelSettings(), LabelSettings()]
#settings.aggstrat = aggstrat.Unaggregated()
#settings.stop_on_concrete_error = False

settings.plot.label[0].big(size=32)
settings.plot.label[1].big(size=32)
settings.stop_on_aggregated_error = False
#settings.process_urgent_guards = True

settings.aggstrat.deaggregate = True # use deaggregation
settings.aggstrat.deagg_preference = aggstrat.Aggregated.DEAGG_LEAVES_FIRST

settings.plot.filename = f"rendezvous_t{passive_time:03}.png"
settings.plot.plot_size = (8, 10)

settings.plot.xdim_dir = [0, 0, 2]
settings.plot.ydim_dir = [1, 1, 3]
settings.plot.label = [LabelSettings(), LabelSettings(), LabelSettings()]

settings.plot.label[0].big(size=26)
settings.plot.label[0].title_size = 22
settings.plot.label[1].big(size=26)
settings.plot.label[2].big(size=26)

settings.plot.label[0].x_label = '$x$'
settings.plot.label[0].y_label = '$y$'

settings.plot.label[1].x_label = '$x_{vel}$'
settings.plot.label[1].y_label = '$y_{vel}$'
settings.plot.label[1].x_label = '$x$'
settings.plot.label[1].y_label = '$y$'

settings.plot.label[0].axes_limits = [-130, 130, -80, 80]
settings.plot.label[1].axes_limits = [-5, 5, -5, 5]
settings.plot.label[2].x_label = '$x_{vel}$'
settings.plot.label[2].y_label = '$y_{vel}$'

settings.plot.label[0].axes_limits = [-950, 200, -450, 200]
#settings.plot.label[1].axes_limits = [-10, 10, -10, 10]
settings.plot.label[1].axes_limits = [-110, 10, -110, 110]
settings.plot.label[2].axes_limits = [-5, 5, -5, 5]

y = 57.735
line = [(-100, y), (-100, -y), (0, 0), (-100, y)]
c1 = collections.LineCollection([line], animated=True, colors=('gray'), linewidths=(2), linestyle='dashed')
c1_copy = collections.LineCollection([line], animated=True, colors=('gray'), linewidths=(2), linestyle='dashed')

rad = 0.2
line = [(-rad, -rad), (-rad, rad), (rad, rad), (rad, -rad), (-rad, -rad)]
c2 = collections.LineCollection([line], animated=True, colors=('red'), linewidths=(2))
c2_copy = collections.LineCollection([line], animated=True, colors=('red'), linewidths=(2))

meters_per_sec_limit = 0.055 if safe else 0.05
meters_per_min_limit = meters_per_sec_limit * 60
Expand All @@ -183,9 +213,9 @@ def make_settings(safe):
vel_oct = collections.LineCollection([line], animated=True, colors=('gray'), linewidths=(2), linestyle='dashed')

r = meters_per_min_limit
patch_col = collections.PatchCollection([Circle((0, 0), r)], alpha=0.1)
patch_col = collections.PatchCollection([Circle((0, 0), r)], alpha=0.25)

settings.plot.extra_collections = [[c1, c2], [vel_oct, patch_col]]
settings.plot.extra_collections = [[c1_copy, c2_copy], [c1, c2], [vel_oct, patch_col]]

return settings

Expand All @@ -194,13 +224,13 @@ def run_hylaa():

safe = True

ha = make_automaton(safe)

init_states = make_init(ha)

settings = make_settings(safe)

Core(ha, settings).run(init_states)
for passive_time in [120]: #range(5, 265, 5):
print(passive_time)
ha = make_automaton(safe, passive_time)
init_states = make_init(ha)
settings = make_settings(safe, passive_time)
Core(ha, settings).run(init_states)

if __name__ == "__main__":
run_hylaa()

Loading

0 comments on commit 06cb254

Please sign in to comment.