debugging deaggregation

examples/deaggregation/deaggregation.py → examples/deaggregation/deag_example.py

@@ -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_INTERACTIVE
+    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

hylaa/aggdag.py

@@ -3,35 +3,16 @@
 Aggregation Directed Acyclic Graph (DAG) implementation
 '''
 
-from collections import namedtuple
-
 from termcolor import cprint
 
 from graphviz import Digraph
 
-from hylaa.settings import HylaaSettings, PlotSettings
+from hylaa.settings import HylaaSettings
 from hylaa.util import Freezable
 from hylaa.stateset import StateSet
 from hylaa.timerutil import Timers
 from hylaa import lputil, aggregate
-from hylaa.deaggregation import DeaggregationManager
-
-# Operation types
-OpInvIntersect = namedtuple('OpInvIntersect', ['step', 'node', 'i_index', 'is_stronger'])
-OpLeftInvariant = namedtuple('OpLeftInvariant', ['step', 'node', 'reached_time_bound'])
-
-class OpTransition(): # pylint: disable=too-few-public-methods
-    'a transition operation'
-
-    def __init__(self, step, parent_node, child_node, transition, poststate):
-        self.step = step
-        self.parent_node = parent_node
-        self.child_node = child_node
-        self.transition = transition
-        self.poststate = poststate
-
-    def __str__(self):
-        return f"[OpTransition({self.step}, {self.transition})]"
+from hylaa.deaggregation import DeaggregationManager, OpInvIntersect, OpLeftInvariant, OpTransition
 
 class AggDag(Freezable):
     'Aggregation directed acyclic graph (DAG) used to manage the deaggregation process'
@@ -45,7 +26,7 @@ def __init__(self, settings, core):
 
         self.waiting_list = [] # a list of OpTransition (with child_node = None). StateSet is in op.poststate
 
-        self.deagg_man = DeaggregationManager(self, self.settings.plot.plot_mode != PlotSettings.PLOT_NONE)
+        self.deagg_man = DeaggregationManager(self)
 
         self.viz_count = 0
 
@@ -175,7 +156,7 @@ def _get_node_leaf_ops(self, node):
 
         return rv
 
-    def remove_node_from_waiting_list(self, node):
+    def remove_node_decendants_from_waiting_list(self, node):
         'remove all waiting list states originating from the passed-in node'
 
         to_remove_ops = self._get_node_leaf_ops(node)
@@ -213,21 +194,36 @@ def pop_waiting_list(self):
             agg_type = self.settings.aggstrat.get_agg_type(op_list)
 
         # create a new AggDagNode for the current computation
-        self.cur_node = AggDagNode(op_list, agg_type, self)
+        self.cur_node = self.make_node(op_list, agg_type, 'full')
 
         return self.cur_node.get_cur_state()
 
-    def make_node(self, ops, agg_type):
-        'make an aggdag node'
+    def make_node(self, ops, agg_type, aggstring):
+        '''make an aggdag node
 
-        return AggDagNode(ops, agg_type, self)
+        aggstring is a string that describes the current aggregation from the previous transition
+        'full' -> full aggergation
+        'init' -> from initial state
+        '0100' -> transition was split four times, this is the state from the first, second, first, first partitions
+        '''
 
-    def save_viz(self):
-        'save the viz to a sequentially-named file'
+        node = AggDagNode(ops, agg_type, self, aggstring)
 
-        self.viz(filename=f"viz{self.viz_count}")
+        #if plot:
+        #    print(".aggdag make_node() plotting aggdagnode")
+        #    self.core.plotman.add_plotted_states([node.stateset])
+
+        return node
 
+    def save_viz(self):
+        '''save the viz to a sequentially-named file, returns the filename'''
+
+        filename = f"aggdag_{self.viz_count:02d}"
         self.viz_count += 1
+
+        self.viz(filename=filename)
+
+        return filename
 
     def viz(self, lr=True, filename=None):
         'visualize the aggdag using graphviz'
@@ -267,7 +263,7 @@ def viz(self, lr=True, filename=None):
 class AggDagNode(Freezable):
     'A node of the Aggregation DAG'
 
-    def __init__(self, parent_op_list, agg_type, aggdag):
+    def __init__(self, parent_op_list, agg_type, aggdag, aggstring):
         self.aggdag = aggdag
         self.op_list = [] # list of Op* objects
         self.stateset = None # StateSet
@@ -287,6 +283,8 @@ def __init__(self, parent_op_list, agg_type, aggdag):
             self.aggdag.core.print_verbose(f"Aggregating {len(state_list)} states")
             state = self._aggregate_from_state_op_list(state_list, parent_op_list, agg_type)
 
+        state.aggstring = aggstring
+
         add_root = False
 
         for op in parent_op_list:
@@ -318,13 +316,19 @@ def split(self):
 
         assert len(self.parent_ops) > 1, "attempted to split() unaggregated aggdag node"
 
+        parent_aggstring = self.stateset.aggstring
+
+        if parent_aggstring == 'full':
+            parent_aggstring = ''
+
         rv = []
 
         mid_index = len(self.parent_ops) // 2
         parent_op_lists = [self.parent_ops[:mid_index], self.parent_ops[mid_index:]]
 
-        for parent_op_list in parent_op_lists:
-            node = AggDagNode(parent_op_list, self.agg_type_from_parents, self.aggdag)
+        for agg_suffix, parent_op_list in zip(['0', '1'], parent_op_lists):
+            aggstring = parent_aggstring + agg_suffix
+            node = self.aggdag.make_node(parent_op_list, self.agg_type_from_parents, aggstring)
 
             rv.append(node)
 
@@ -406,12 +410,21 @@ def replay_op(self, op_list, i):
 
                     break
 
-            if not skip:           
+            print(".aggdag %%%% debug never skipping invariant intersection")
+            # hmm, skipping invariant intersections is only valid if deaggregation is a subset of aggregated set...
+            # for our krylov aggregation, this isn't really the case though... so in general you need to invaraint
+            # intersect at every step... plus this is really an optimization rather than the main algorithm
+
+            if True or not skip:
+                self.aggdag.core.print_verbose(
+                    f"doing invariant intersection in replay at step {cur_state.cur_step_in_mode}")
                 is_feasible = self.replay_op_intersect_invariant(cur_state, op)
 
                 if not is_feasible:
                     op = OpLeftInvariant(op.step, self, False)
                     self.op_list.append(op)
+            else:
+                self.aggdag.core.print_verbose("skipping invariant intersection because stronger one is coming up")
 
         Timers.toc('replay_op')
 
@@ -421,7 +434,8 @@ def replay_op_transition(self, state, op):
 
         print_verbose = self.aggdag.core.print_verbose
 
-        state.step(op.step)
+        state.step(op.step) # advance the state first
+
         # check if the transition is still enabled
 
         t = op.transition
@@ -437,15 +451,15 @@ def replay_op_transition(self, state, op):
 
             if op.child_node is None:
                 self.aggdag.waiting_list.append(new_op)
-                print_verbose("Replay Transition added new Discrete Successor to '{}' at step {}".format( \
-                              t.to_mode.name, state.cur_steps_since_start))
+                print_verbose("Replay Transition {} when deaggreaged to steps {}".format( \
+                              t, state.cur_steps_since_start))
             else:
                 self.aggdag.deagg_man.update_transition_successors(op, new_op)
 
-                print_verbose("Replay Transition refined Discrete Successor to '{}' at step {}".format( \
-                              t.to_mode.name, state.cur_steps_since_start))
+                print_verbose("Replay Transition refined transition {} when deaggregated at steps {}".format( \
+                              t, state.cur_steps_since_start))
         else:
-            print_verbose(f"Replay skipped transition at step {state.cur_steps_since_start}")
+            print_verbose(f"Replay skipped transition {t} when deaggregated to steps {state.cur_steps_since_start}")
 
     def replay_op_intersect_invariant(self, state, op):
         '''replay a single operation of type OpInvIntersect
@@ -514,7 +528,8 @@ def viz(self, g, already_drawn_nodes):
             else:
                 label += f" ({steps})"
         else:
-            label += " (incomplete)"
+            steps = self.stateset.cur_step_in_mode
+            label += f" (incomplete, {steps} so far)"
 
         print(f"vizing node {name} ({label}) with {len(self.parent_ops)} parent ops")
         g.node(name, label=label)

hylaa/check_trace.py

@@ -114,10 +114,10 @@ def check(a_matrix, b_matrix, step, max_time, start_point, inputs, normal_vec, e
         remaining = elapsed / ((1.0+index) / len(inputs)) - elapsed
 
         if stdout and num_steps > 1 and remaining > 2.0:
-            print "Combining {} steps (identical inputs)".format(num_steps)
+            print("Combining {} steps (identical inputs)".format(num_steps))
 
         if stdout and remaining > 2.0:
-            print "{} / {} (ETA: {:.2f} sec)".format(index, len(inputs), remaining)
+            print("{} / {} (ETA: {:.2f} sec)".format(index, len(inputs), remaining))
 
         der_func = make_der_func(a_matrix, b_matrix, inputs[index])
         new_states, new_times = sim(sim_states[-1], der_func, step * num_steps, samples_per_input * num_steps, quick)
@@ -147,10 +147,10 @@ def check(a_matrix, b_matrix, step, max_time, start_point, inputs, normal_vec, e
         data.rel_error = numerator / denominator
 
     if stdout:
-        print "Final Time: {}".format(index * step)
-        print "Absolute Error (l-2 norm): {}".format(numerator)
-        print "Relative Error (l-2 norm): {}".format(data.rel_error)
-        print "Runtime: {:.2f} seconds".format(time.time() - start)
+        print("Final Time: {}".format(index * step))
+        print("Absolute Error (l-2 norm): {}".format(numerator))
+        print("Relative Error (l-2 norm): {}".format(data.rel_error))
+        print("Runtime: {:.2f} seconds".format(time.time() - start))
 
     return (sim_states, sim_times, data)
 
@@ -187,12 +187,12 @@ def plot(sim_states, sim_times, inputs, normal_vec, normal_val, max_time, step,
     tol = 1e-6
 
     if len(end_point) < 10:
-        print "End Point: {}".format(end_point)
+        print("End Point: {}".format(end_point))
 
     if end_val - tol <= normal_val:
-        print "End Point is a violation (within tolerance): {} - {} <= {}".format(end_val, tol, normal_val)
+        print("End Point is a violation (within tolerance): {} - {} <= {}".format(end_val, tol, normal_val))
     else:
-        print "End point is NOT a violation: {} - {} (tolerance) > {}".format(end_val, tol, normal_val)
+        print("End point is NOT a violation: {} - {} (tolerance) > {}".format(end_val, tol, normal_val))
 
     epsilon = step / 8.0 # to prevent round-off error on the end range
     input_times = np.arange(0.0, max_time + epsilon, step)

hylaa/core.py

@@ -3,16 +3,14 @@
 Stanley Bak, 2018
 '''
 
-from collections import defaultdict
-
 import numpy as np
 from termcolor import cprint
 
 from hylaa.settings import HylaaSettings, PlotSettings
 
 from hylaa.plotutil import PlotManager
 from hylaa.aggdag import AggDag
-from hylaa.counterexample import make_counterexample
+from hylaa.result import HylaaResult, make_counterexample
 from hylaa.stateset import StateSet
 from hylaa.hybrid_automaton import HybridAutomaton, was_tt_taken
 from hylaa.timerutil import Timers
@@ -149,8 +147,7 @@ def check_guards(self):
 
                 self.aggdag.add_transition_successor(t, t_lpi)
 
-                self.print_verbose("Added Discrete Successor to '{}' at step {}".format( \
-                                   t.to_mode.name, cur_state.cur_steps_since_start))
+                self.print_verbose(f"Took transition {t} at steps {cur_state.cur_steps_since_start}")
 
                 # if it's a time-triggered transition, we may remove cur_state immediately
                 if self.settings.optimize_tt_transitions and t.time_triggered:
@@ -281,7 +278,7 @@ def do_step_pop(self):
 
         # pause plot
         self.print_verbose("Pausing due to step_pop()")
-        self.plotman.interactive.paused = True
+        self.plotman.pause()
 
         Timers.toc('do_step_pop')
 
@@ -307,12 +304,11 @@ def do_step_reach(self):
                 self.aggdag.deagg_man.do_step_replay()
             else:
                 # begin a deaggregation replay or pop a state off the waiting list
-                #deagg_node = self.settings.aggstrat.get_deagg_node(self.aggdag)
-                #print(f".core deagg_node = {deagg_node}")
+                deagg_node = self.settings.aggstrat.get_deagg_node(self.aggdag)
 
                 if deagg_node:
                     self.aggdag.deagg_man.begin_replay(deagg_node)
-                    self.aggdag.deagg_man.do_step_replay() # do the first step
+                    self.aggdag.deagg_man.do_step_replay()
                 else:
                     #print(".core popping, calling aggdag.save_viz()")
                     #self.aggdag.save_viz()
@@ -409,7 +405,7 @@ def run(self, init_state_list):
         if self.result.has_concrete_error:
             self.print_normal("Result: Error modes are reachable (found counter-example).\n")
         elif self.result.has_aggregated_error:
-            self.print_normal("Result: Error modes are reachable when aggergation (overapproximation) was used.\n")
+            self.print_normal("Result: System is safe, although error modes were reachable when aggregation (overapproximation) was used.\n")
         else:
             self.print_normal("Result: System is safe. Error modes are NOT reachable.\n")
 
@@ -486,7 +482,7 @@ def do_step_sim(self):
 
             self.sim_should_try_guards = self.settings.process_urgent_guards
             self.sim_took_transition = [False] * len(self.sim_states)
-            self.plotman.interactive.paused = True
+            self.plotman.pause()
             self.print_verbose("Pausing due to sim pop()")
         else:
             # simulate one step for all states in sim_states
@@ -541,23 +537,3 @@ def do_step_sim(self):
             if finished:
                 self.plotman.commit_cur_sims()
                 self.sim_states = None
-
-class HylaaResult(Freezable): # pylint: disable=too-few-public-methods
-    'result object returned by core.run()'
-
-    def __init__(self):
-        self.top_level_timer = None # TimerData for total time
-
-        # verification result:
-        self.has_aggregated_error = False
-        self.has_concrete_error = False
-
-        self.counterexample = [] # if unsafe, a list of CounterExampleSegment objects
-
-        # assigned if setting.plot.store_plot_result is True, a map name -> list of lists (the verts at each step)
-        self.mode_to_polys = defaultdict(list)
-
-        # the last core.cur_state object... used for unit testing
-        self.last_cur_state = None
-
-        self.freeze_attrs()