Merge pull request #41 from stanleybak/master

Merge model generation + hylaa printer

README.md

@@ -77,7 +77,7 @@ After building Hyst.jar, you can run it as an executable .jar file with the -hel
 
 ```
 $ java -jar Hyst.jar -help
-Hyst v1.3 General Usage:
+Hyst v1.6 General Usage:
  -debug (-d)                            : print debug (and verbose) output
                                           (default: false)
  -generate (-gen) GEN_NAME GEN_PARAMS   : generate a model (rather than loading
@@ -256,9 +256,9 @@ Another basic example is the ShortenModeNamesPass.java ( https://github.com/veri
 
 #### ECLIPSE SETUP:
 
-You need to compile with antlt-4.4-runtime.jar and several others jars (in /lib) on your classpath. In Eclipse, you do this by going to: 
+You need to compile with antlr-4.4-runtime.jar and several others jars (in /lib) on your classpath. In Eclipse, you do this by going to: 
 
-Project -> Properties -> Java Build Path -> Libraries -> Add External Jar -> select the antlt-4.4-complete.jar file (should be in the project directory) -> Ok
+Project -> Properties -> Java Build Path -> Libraries -> Add External Jar -> select the antlr-4.4-complete.jar file (should be in the project directory) -> Ok
 
 #### RUNNING DIRECTLY FROM .CLASS FILES:
 

doc/model_generators/drivetrain/README

@@ -0,0 +1,7 @@
+This folder contains the drivetrain benchmark from: Matthias Althoff, Bruce H. Krogh: "Avoiding geometric intersection operations in reachability analysis of hybrid systems" in HSCC 2012
+
+It originally defines a 7 + 2*theta dimensional system, where theta >= 0 is a user parameter.
+
+There is also a control input u , which is set by a benchmark maneuver to: -5 when time is in [0, 0.2], and +5 when time is in [0.2, 2]. To handle this, we add a dimension 't' and a guard when t = 0.2, giving us a 8 + 2*theta dimensional system with 6 modes (3 before time 0.2, and 3 after time 0.2)
+
+

doc/model_generators/drivetrain/plot.py

@@ -0,0 +1,39 @@
+'''Script for generating drivetrain benchmark and running with pysim'''
+
+# make sure hybridpy is on your PYTHONPATH: hyst/src/hybridpy
+import hybridpy.hypy as hypy
+
+def main():
+    '''main entry point'''
+
+    theta = 1
+
+    gen_drivetrain_pysim(theta)
+
+def gen_drivetrain_pysim(theta):
+    'generate a drivetrain benchmark instance and plot a simulation'
+
+    title = "Drivetrain (Theta={})".format(theta)
+    image_path = "pysim_drivetrain_theta{}.png".format(theta)
+    output_path = "pysim_drivetrain{}.py".format(theta)
+    gen_param = '-theta {} -init_points 10'.format(theta)
+
+    tool_param = "-title \"{}\" -xdim 0 -ydim 2".format(title)
+
+    e = hypy.Engine('pysim', tool_param)
+    e.set_generator('drivetrain', gen_param)
+    #e.set_output(output_path)
+    #e.set_verbose(True)
+
+    #e.add_pass("sub_constants", "")
+    #e.add_pass("simplify", "-p")
+
+    print 'Running ' + title
+    res = e.run(print_stdout=True, image_path=image_path)
+    print 'Finished ' + title
+
+    if res['code'] != hypy.Engine.SUCCESS:
+        raise RuntimeError('Error in ' + title + ': ' + str(res['code']))
+
+if __name__ == '__main__':
+    main()

doc/model_generators/navigation/README

@@ -1,4 +1,4 @@
-This folder contains nevigation benchmark models generated using Hyst, and their pysim simulation images.
+This folder contains navigation benchmark models generated using Hyst, and their pysim simulation images.
 
 The navigation models that are here are from the original paper: http://ai.eecs.umich.edu/people/rounds/HSCC/83.pdf
 

doc/model_generators/navigation/nav_fig1b.py

@@ -1,229 +1,201 @@
 '''
-Created by Hyst v1.3
+Created by Hyst v1.4
 Hybrid Automaton in PySim
 Converted from file: 
-Command Line arguments: -gen nav "-matrix -1.2 0.1 0.1 -1.2 -i_list 2 2 A 4 3 4 B 2 4 -width 3 -startx 0.5 -starty 1.5 -noise 0.1" -o nav_fig1b.py -tool pysim "-corners True -legend False -rand 100 -time 5 -title nav_fig1b"
+Command Line arguments: -gen nav "-matrix -1.2 0.1 0.1 -1.2 -i_list B 2 4 4 3 4 2 2 A -width 3 -startx 0.5 -starty 1.5 -noise 0.1" -o nav_fig1b.py -tool pysim "-corners True -legend False -rand 100 -time 5 -title nav_fig1b"
 '''
 
 import hybridpy.pysim.simulate as sim
-from hybridpy.pysim.hybrid_automaton import HybridAutomaton
-from hybridpy.pysim.hybrid_automaton import HyperRectangle
-from hybridpy.pysim.simulate import init_list_to_q_list
-from sympy.core import symbols
-from sympy import And, Or
+from hybridpy.pysim.simulate import init_list_to_q_list, PySimSettings
+from hybridpy.pysim.hybrid_automaton import HybridAutomaton, HyperRectangle
 
 def define_ha():
     '''make the hybrid automaton and return it'''
-    # Variable ordering: [x, y, xvel, yvel]
-
-    sym_x, sym_y, sym_xvel, sym_yvel = symbols('x y xvel yvel ')
 
     ha = HybridAutomaton()
+    ha.variables = ["x", "y", "xvel", "yvel"]
+
 
     mode_0_0 = ha.new_mode('mode_0_0')
-    mode_0_0.inv = lambda state: state[0] <= 1 and state[1] <= 1
-    mode_0_0.inv_sympy = And(sym_x <= 1, sym_y <= 1)
-    mode_0_0.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1) + 0.1 * (state[3] - 0.00000000000000006123233995736766), 0.1 * (state[2] - 1) + -1.2 * (state[3] - 0.00000000000000006123233995736766)]
+    mode_0_0.inv = lambda state: state[0] <= 1.0 and state[1] <= 1.0
+    mode_0_0.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1.0) + 0.1 * (state[3] - 0.0), 0.1 * (state[2] - 1.0) + -1.2 * (state[3] - 0.0)]
     mode_0_0.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_1_0 = ha.new_mode('mode_1_0')
-    mode_1_0.inv = lambda state: state[0] >= 1 and state[0] <= 2 and state[1] <= 1
-    mode_1_0.inv_sympy = And(And(sym_x >= 1, sym_x <= 2), sym_y <= 1)
-    mode_1_0.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1) + 0.1 * (state[3] - 0.00000000000000006123233995736766), 0.1 * (state[2] - 1) + -1.2 * (state[3] - 0.00000000000000006123233995736766)]
+    mode_1_0.inv = lambda state: state[0] >= 1.0 and state[0] <= 2.0 and state[1] <= 1.0
+    mode_1_0.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1.0) + 0.1 * (state[3] - 0.0), 0.1 * (state[2] - 1.0) + -1.2 * (state[3] - 0.0)]
     mode_1_0.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_2_0 = ha.new_mode('mode_2_0')
-    mode_2_0.inv = lambda state: state[0] >= 2 and state[1] <= 1
-    mode_2_0.inv_sympy = And(sym_x >= 2, sym_y <= 1)
-    mode_2_0.der = lambda _, state: [0, 0, 0, 0]
+    mode_2_0.inv = lambda state: state[0] >= 2.0 and state[1] <= 1.0
+    mode_2_0.der = lambda _, state: [0.0, 0.0, 0.0, 0.0]
     mode_2_0.der_interval_list = [[0, 0], [0, 0], [0, 0], [0, 0]]
 
     mode_0_1 = ha.new_mode('mode_0_1')
-    mode_0_1.inv = lambda state: state[0] <= 1 and state[1] >= 1 and state[1] <= 2
-    mode_0_1.inv_sympy = And(And(sym_x <= 1, sym_y >= 1), sym_y <= 2)
-    mode_0_1.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.00000000000000012246467991473532) + 0.1 * (state[3] - -1), 0.1 * (state[2] - 0.00000000000000012246467991473532) + -1.2 * (state[3] - -1)]
+    mode_0_1.inv = lambda state: state[0] <= 1.0 and state[1] >= 1.0 and state[1] <= 2.0
+    mode_0_1.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.0) + 0.1 * (state[3] - -1.0), 0.1 * (state[2] - 0.0) + -1.2 * (state[3] - -1.0)]
     mode_0_1.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_1_1 = ha.new_mode('mode_1_1')
-    mode_1_1.inv = lambda state: state[0] >= 1 and state[0] <= 2 and state[1] >= 1 and state[1] <= 2
-    mode_1_1.inv_sympy = And(And(And(sym_x >= 1, sym_x <= 2), sym_y >= 1), sym_y <= 2)
+    mode_1_1.inv = lambda state: state[0] >= 1.0 and state[0] <= 2.0 and state[1] >= 1.0 and state[1] <= 2.0
     mode_1_1.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.7071067811865476) + 0.1 * (state[3] - -0.7071067811865475), 0.1 * (state[2] - 0.7071067811865476) + -1.2 * (state[3] - -0.7071067811865475)]
     mode_1_1.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_2_1 = ha.new_mode('mode_2_1')
-    mode_2_1.inv = lambda state: state[0] >= 2 and state[1] >= 1 and state[1] <= 2
-    mode_2_1.inv_sympy = And(And(sym_x >= 2, sym_y >= 1), sym_y <= 2)
-    mode_2_1.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.00000000000000012246467991473532) + 0.1 * (state[3] - -1), 0.1 * (state[2] - 0.00000000000000012246467991473532) + -1.2 * (state[3] - -1)]
+    mode_2_1.inv = lambda state: state[0] >= 2.0 and state[1] >= 1.0 and state[1] <= 2.0
+    mode_2_1.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.0) + 0.1 * (state[3] - -1.0), 0.1 * (state[2] - 0.0) + -1.2 * (state[3] - -1.0)]
     mode_2_1.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_0_2 = ha.new_mode('mode_0_2')
-    mode_0_2.inv = lambda state: state[0] <= 1 and state[1] >= 2
-    mode_0_2.inv_sympy = And(sym_x <= 1, sym_y >= 2)
-    mode_0_2.der = lambda _, state: [0, 0, 0, 0]
+    mode_0_2.inv = lambda state: state[0] <= 1.0 and state[1] >= 2.0
+    mode_0_2.der = lambda _, state: [0.0, 0.0, 0.0, 0.0]
     mode_0_2.der_interval_list = [[0, 0], [0, 0], [0, 0], [0, 0]]
 
     mode_1_2 = ha.new_mode('mode_1_2')
-    mode_1_2.inv = lambda state: state[0] >= 1 and state[0] <= 2 and state[1] >= 2
-    mode_1_2.inv_sympy = And(And(sym_x >= 1, sym_x <= 2), sym_y >= 2)
-    mode_1_2.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1) + 0.1 * (state[3] - 0.00000000000000006123233995736766), 0.1 * (state[2] - 1) + -1.2 * (state[3] - 0.00000000000000006123233995736766)]
+    mode_1_2.inv = lambda state: state[0] >= 1.0 and state[0] <= 2.0 and state[1] >= 2.0
+    mode_1_2.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 1.0) + 0.1 * (state[3] - 0.0), 0.1 * (state[2] - 1.0) + -1.2 * (state[3] - 0.0)]
     mode_1_2.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     mode_2_2 = ha.new_mode('mode_2_2')
-    mode_2_2.inv = lambda state: state[0] >= 2 and state[1] >= 2
-    mode_2_2.inv_sympy = And(sym_x >= 2, sym_y >= 2)
-    mode_2_2.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.00000000000000012246467991473532) + 0.1 * (state[3] - -1), 0.1 * (state[2] - 0.00000000000000012246467991473532) + -1.2 * (state[3] - -1)]
+    mode_2_2.inv = lambda state: state[0] >= 2.0 and state[1] >= 2.0
+    mode_2_2.der = lambda _, state: [state[2], state[3], -1.2 * (state[2] - 0.0) + 0.1 * (state[3] - -1.0), 0.1 * (state[2] - 0.0) + -1.2 * (state[3] - -1.0)]
     mode_2_2.der_interval_list = [[0, 0], [0, 0], [-0.1, 0.1], [-0.1, 0.1]]
 
     t = ha.new_transition(mode_0_0, mode_1_0)
-    t.guard = lambda state: state[0] >= 1
+    t.guard = lambda state: state[0] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 1
 
     t = ha.new_transition(mode_0_0, mode_0_1)
-    t.guard = lambda state: state[1] >= 1
+    t.guard = lambda state: state[1] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 1
 
     t = ha.new_transition(mode_1_0, mode_0_0)
-    t.guard = lambda state: state[0] <= 1
+    t.guard = lambda state: state[0] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 1
 
     t = ha.new_transition(mode_1_0, mode_2_0)
-    t.guard = lambda state: state[0] >= 2
+    t.guard = lambda state: state[0] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 2
 
     t = ha.new_transition(mode_1_0, mode_1_1)
-    t.guard = lambda state: state[1] >= 1
+    t.guard = lambda state: state[1] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 1
 
     t = ha.new_transition(mode_2_0, mode_1_0)
-    t.guard = lambda state: state[0] <= 2
+    t.guard = lambda state: state[0] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 2
 
     t = ha.new_transition(mode_2_0, mode_2_1)
-    t.guard = lambda state: state[1] >= 1
+    t.guard = lambda state: state[1] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 1
 
     t = ha.new_transition(mode_0_1, mode_1_1)
-    t.guard = lambda state: state[0] >= 1
+    t.guard = lambda state: state[0] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 1
 
     t = ha.new_transition(mode_0_1, mode_0_0)
-    t.guard = lambda state: state[1] <= 1
+    t.guard = lambda state: state[1] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 1
 
     t = ha.new_transition(mode_0_1, mode_0_2)
-    t.guard = lambda state: state[1] >= 2
+    t.guard = lambda state: state[1] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 2
 
     t = ha.new_transition(mode_1_1, mode_0_1)
-    t.guard = lambda state: state[0] <= 1
+    t.guard = lambda state: state[0] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 1
 
     t = ha.new_transition(mode_1_1, mode_2_1)
-    t.guard = lambda state: state[0] >= 2
+    t.guard = lambda state: state[0] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 2
 
     t = ha.new_transition(mode_1_1, mode_1_0)
-    t.guard = lambda state: state[1] <= 1
+    t.guard = lambda state: state[1] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 1
 
     t = ha.new_transition(mode_1_1, mode_1_2)
-    t.guard = lambda state: state[1] >= 2
+    t.guard = lambda state: state[1] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 2
 
     t = ha.new_transition(mode_2_1, mode_1_1)
-    t.guard = lambda state: state[0] <= 2
+    t.guard = lambda state: state[0] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 2
 
     t = ha.new_transition(mode_2_1, mode_2_0)
-    t.guard = lambda state: state[1] <= 1
+    t.guard = lambda state: state[1] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 1
 
     t = ha.new_transition(mode_2_1, mode_2_2)
-    t.guard = lambda state: state[1] >= 2
+    t.guard = lambda state: state[1] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y >= 2
 
     t = ha.new_transition(mode_0_2, mode_1_2)
-    t.guard = lambda state: state[0] >= 1
+    t.guard = lambda state: state[0] >= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 1
 
     t = ha.new_transition(mode_0_2, mode_0_1)
-    t.guard = lambda state: state[1] <= 2
+    t.guard = lambda state: state[1] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 2
 
     t = ha.new_transition(mode_1_2, mode_0_2)
-    t.guard = lambda state: state[0] <= 1
+    t.guard = lambda state: state[0] <= 1.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 1
 
     t = ha.new_transition(mode_1_2, mode_2_2)
-    t.guard = lambda state: state[0] >= 2
+    t.guard = lambda state: state[0] >= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x >= 2
 
     t = ha.new_transition(mode_1_2, mode_1_1)
-    t.guard = lambda state: state[1] <= 2
+    t.guard = lambda state: state[1] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 2
 
     t = ha.new_transition(mode_2_2, mode_1_2)
-    t.guard = lambda state: state[0] <= 2
+    t.guard = lambda state: state[0] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_x <= 2
 
     t = ha.new_transition(mode_2_2, mode_2_1)
-    t.guard = lambda state: state[1] <= 2
+    t.guard = lambda state: state[1] <= 2.0
     t.reset = lambda state: [None, None, None, None]
-    t.guard_sympy = sym_y <= 2
 
     return ha
 
 def define_init_states(ha):
     '''returns a list of (mode, HyperRectangle)'''
     # Variable ordering: [x, y, xvel, yvel]
     rv = []
+
+    rv.append((ha.modes['mode_0_1'],HyperRectangle([(0.5, 0.5), (1.5, 1.5), (-1, 1), (-1, 1)])))
+    return rv
 
-    r = HyperRectangle([(0.5, 0.5), (1.5, 1.5), (-1, 1), (-1, 1)])
-    rv.append((ha.modes['mode_0_1'], r))
 
-    return rv
+def define_settings():
+    '''defines the automaton / plot settings'''
+    s = PySimSettings()
+    s.max_time = 5.0
+    s.step = 0.1
+    s.dim_x = 0
+    s.dim_y = 1
 
+    return s
 
-def simulate(init_states, max_time=5):
+def simulate(init_states, settings):
     '''simulate the automaton from each initial rect'''
 
     q_list = init_list_to_q_list(init_states, center=True, star=True, corners=True, rand=100)
-    result = sim.simulate_multi(q_list, max_time)
+    result = sim.simulate_multi(q_list, settings.max_time)
 
     return result
 
-def plot(result, init_states, filename='plot.png', dim_x=0, dim_y=1):
+def plot(result, init_states, image_path, settings):
     '''plot a simulation result to a file'''
 
     draw_events = len(result) == 1
     shouldShow = False
-    sim.plot_sim_result_multi(result, dim_x, dim_y, filename, draw_events, legend=False, title='nav_fig1b', show=shouldShow, init_states=init_states)
+    sim.plot_sim_result_multi(result, settings.dim_x, settings.dim_y, image_path, draw_events, legend=False, title='nav_fig1b', show=shouldShow, init_states=init_states)
 
 if __name__ == '__main__':
     ha = define_ha()
+    settings = define_settings()
     init_states = define_init_states(ha)
-    plot(simulate(init_states), init_states)
+    plot(simulate(init_states, settings), init_states, 'plot.png', settings)