added setting to skip invariant strengthening

hylaa/containers.py

@@ -37,6 +37,8 @@ def __init__(self, step, max_time, plot_settings=None):
         self.opt_decompose_lp = True # use the Minkowski sum decomposition optimization (for systems with inputs)
         self.opt_warm_start_lp = True # reuse the LP instances between guard checks (warm-start LP)
 
+        self.do_guard_strengthening = True
+
         self.counter_example_filename = None # the counter-example filename to create on errors: "counterexample.py"
         self.simulation = SimulationSettings(step)
 

hylaa/engine.py

@@ -73,7 +73,10 @@ def load_waiting_list(self, init_list):
             else:
                 raise RuntimeError("Unsupported initial state type '{}': {}".format(type(shape), shape))
 
-            self.waiting_list.add_deaggregated(star)
+            still_feasible, _ = star.trim_to_invariant()
+
+            if still_feasible:
+                self.waiting_list.add_deaggregated(star)
 
     def is_finished(self):
         'is the computation finished'
@@ -389,7 +392,9 @@ def run(self, init_list):
 
         # strengthen guards to inclunde invariants of targets
         ha = init_list[0][0].parent
-        ha.do_guard_strengthening()
+
+        if self.settings.do_guard_strengthening:
+            ha.do_guard_strengthening()
 
         self.result = HylaaResult()
         self.plotman.create_plot()