From 55a72f85f0fa49e10d7629fdec03873cafae97ce Mon Sep 17 00:00:00 2001 From: Stanley Bak Date: Mon, 25 Jun 2018 17:57:29 -0400 Subject: [PATCH] added setting to skip invariant strengthening --- hylaa/containers.py | 2 ++ hylaa/engine.py | 9 +++++++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/hylaa/containers.py b/hylaa/containers.py index 1fedfb8..7fc6790 100644 --- a/hylaa/containers.py +++ b/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) diff --git a/hylaa/engine.py b/hylaa/engine.py index 7fe8ad3..bed24c7 100644 --- a/hylaa/engine.py +++ b/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()