Adding dtNest to PAYNT

models/pomdp/sketches/avoid-discounted/sketch.props

@@ -1 +1 @@
-R{"penalty"}min=? [C{0.99}]
+R{"penalty"}min=? [Cdiscount=0.99]

paynt/cli.py

@@ -16,6 +16,7 @@
 import paynt.synthesizer.synthesizer_cegis
 import paynt.synthesizer.policy_tree
 import paynt.synthesizer.decision_tree
+import paynt.synthesizer.dtnest
 
 import click
 import sys
@@ -130,6 +131,10 @@ def setup_logger(log_path = None):
     "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for Cassandra models",
 )
 
+# dtNest related options
+@click.option("--dtnest", is_flag=True, default=False, help="run dtNest algorithm for decision tree synthesis")
+@click.option("--dtnest-initial-tree", type=click.Path(), default=None, help="path to initial decision tree for dtNest")
+
 @click.option(
     "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True,
     help="counterexample generator",
@@ -149,6 +154,7 @@ def paynt_run(
     mdp_discard_unreachable_choices,
     tree_depth, tree_enumeration, tree_map_scheduler, add_dont_care_action,
     constraint_bound,
+    dtnest, dtnest_initial_tree,
     ce_generator,
     profiling
 ):
@@ -180,6 +186,8 @@ def paynt_run(
     paynt.synthesizer.decision_tree.SynthesizerDecisionTree.scheduler_path = tree_map_scheduler
     paynt.quotient.mdp.MdpQuotient.add_dont_care_action = add_dont_care_action
 
+    paynt.synthesizer.dtnest.DtNest.initial_tree_path = dtnest_initial_tree
+
     storm_control = None
     if storm_pomdp:
         storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl()
@@ -191,7 +199,7 @@ def paynt_run(
     sketch_path = os.path.join(project, sketch)
     properties_path = os.path.join(project, props)
     quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound, exact)
-    synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
+    synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control, dtnest)
     synthesizer.run(optimum_threshold)
 
     if profiling:

paynt/parser/sketch.py

@@ -130,6 +130,16 @@ def load_sketch(cls, sketch_path, properties_path,
                 filetype = "cassandra"
             except SyntaxError:
                 pass
+        if filetype is None:
+            try:
+                # TODO not tested yet
+                logger.info(f"assuming sketch in JANI format...")
+                jani_model, properties = stormpy.parse_jani_model(sketch_path)
+                specification = paynt.verification.property.Specification(properties)
+                explicit_quotient = paynt.models.model_builder.ModelBuilder.from_jani(jani_model, specification)
+                filetype = "jani"
+            except SyntaxError:
+                pass
 
         assert filetype is not None, "unknown format of input file"
         logger.info("sketch parsing OK")

paynt/synthesizer/decision_tree.py

@@ -87,6 +87,8 @@ def verify_family(self, family):
             return
         self.harmonize_inconsistent_scheduler(family)
 
+    def compute_normalized_value(self, value, opt, random):
+        return (value-random)/(opt-random) if opt-random != 0 else 1.0
 
     def counters_reset(self):
         self.num_families_considered = 0
@@ -119,8 +121,7 @@ def export_decision_tree(self, decision_tree, export_filename_base):
         tree.render(export_filename_base, format="png", cleanup=True) # using export_filename_base since graphviz appends .png by default
         logger.info(f"exported decision tree visualization to {tree_visualization_filename}")
 
-
-    def synthesize_tree(self, depth:int):
+    def synthesize_tree(self, depth:int, family=None):
         self.counters_reset()
         self.quotient.reset_tree(depth)
         self.best_assignment = self.best_assignment_value = None
@@ -132,23 +133,30 @@ def synthesize_tree(self, depth:int):
         self.best_assignment = self.best_assignment_value = None
         self.counters_print()
 
-    def synthesize_tree_sequence(self, opt_result_value):
+    def synthesize_tree_sequence(self, opt_result_value, overall_timeout=None, max_depth=None, break_if_found=False):
         self.best_tree = self.best_tree_value = None
 
-        global_timeout = paynt.utils.timer.GlobalTimer.global_timer.time_limit_seconds
-        if global_timeout is None: global_timeout = 900
-        depth_timeout = global_timeout / 2 / SynthesizerDecisionTree.tree_depth
-        for depth in range(SynthesizerDecisionTree.tree_depth+1):
+        if max_depth is None:
+            max_depth = SynthesizerDecisionTree.tree_depth+1
+        if overall_timeout is None:
+            global_timeout = paynt.utils.timer.GlobalTimer.global_timer.time_limit_seconds
+            if global_timeout is None: global_timeout = 900
+            overall_timeout = global_timeout
+            tree_sequence_timer = None
+        else:
+            tree_sequence_timer = paynt.utils.timer.Timer(overall_timeout)
+            tree_sequence_timer.start()
+        depth_timeout = overall_timeout / 2 / (max_depth-1) if max_depth > 1 else overall_timeout
+        for depth in range(max_depth):
             print()
             self.quotient.reset_tree(depth)
             best_assignment_old = self.best_assignment
-
             family = self.quotient.family
             self.explored = 0
             self.counters_reset()
             self.stat = paynt.synthesizer.statistic.Statistic(self)
             self.stat.start(family)
-            timeout = depth_timeout if depth < SynthesizerDecisionTree.tree_depth else None
+            timeout = depth_timeout if depth < max_depth-1 else overall_timeout / 2 # second half of the time for the last depth
             self.synthesis_timer = paynt.utils.timer.Timer(timeout)
             self.synthesis_timer.start()
             families = [family]
@@ -179,10 +187,10 @@ def synthesize_tree_sequence(self, opt_result_value):
                 self.best_tree.root.associate_assignment(self.best_assignment)
                 self.best_tree_value = self.best_assignment_value
 
-                if abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-3:
+                if break_if_found or (opt_result_value != 0 and abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-3) or (opt_result_value == 0 and self.best_assignment_value < 1e-3):
                     break
 
-            if self.resource_limit_reached():
+            if self.resource_limit_reached() or tree_sequence_timer is not None and tree_sequence_timer.time_limit_reached():
                 break
 
     def map_scheduler(self, scheduler_choices):
@@ -245,7 +253,7 @@ def run(self, optimum_threshold=None):
             self.map_scheduler(scheduler_choices)
         else:
             if self.quotient.specification.has_optimality:
-                epsilon = 1e-1
+                epsilon = 0.05
                 mc_result_positive = opt_result_value > 0
                 if self.quotient.specification.optimality.maximizing == mc_result_positive:
                     epsilon *= -1
@@ -271,9 +279,11 @@ def run(self, optimum_threshold=None):
             if self.quotient.specification.has_optimality:
                 logger.info(f"the synthesized tree has value {self.best_tree_value}")
             if self.quotient.DONT_CARE_ACTION_LABEL in self.quotient.action_labels:
-                logger.info(f"the synthesized tree has relative value: {(self.best_tree_value-random_result_value)/(opt_result_value-random_result_value)}")
+                logger.info(f"the synthesized tree has relative value: {self.compute_normalized_value(self.best_tree_value, opt_result_value, random_result_value)}")
             logger.info(f"printing the synthesized tree below:")
-            print(self.best_tree.to_string())
+
+            # print(self.best_tree.to_string())
+            # print(self.best_tree.to_graphviz())
             # logger.info(f"printing the PRISM module below:")
             # print(self.best_tree.to_prism())
 
@@ -284,8 +294,5 @@ def run(self, optimum_threshold=None):
         logger.info(f"synthesis finished after {time_total} seconds")
 
         print()
-        for name,time in self.quotient.coloring.getProfilingInfo():
-            time_percent = round(time/time_total*100,1)
-            print(f"{name} = {time} s ({time_percent} %)")
 
         return self.best_tree