optional reset of the optimum value after synthesis

paynt/synthesizer/synthesizer.py

@@ -112,10 +112,11 @@ def synthesize_one(self, family):
         ''' to be overridden '''
         pass
 
-    def synthesize(self, family=None, optimum_threshold=None, return_all=False, print_stats=True):
+    def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, return_all=False, print_stats=True):
         '''
         :param family family of assignment to search in
-        :param optimum_threshold known value of the optimum value
+        :param optimum_threshold known bound on the optimum value
+        :param keep_optimum if True, the optimality specification will not be reset upon finish
         :param return_all if True and the synthesis returns a family, all assignments will be returned instead of an
             arbitrary one
         :param print_stats if True, synthesis stats will be printed upon completion
@@ -143,9 +144,13 @@ def synthesize(self, family=None, optimum_threshold=None, return_all=False, prin
             model = self.quotient.build_assignment(assignment)
             mc_result = model.check_specification(self.quotient.specification)
             logger.info(f"double-checking specification satisfiability: {mc_result}")
-        
+
         if print_stats:
             self.stat.print()
+
+        if not keep_optimum:
+            self.quotient.specification.reset()
+
         return assignment
 
 

paynt/synthesizer/synthesizer_pomdp.py

@@ -93,7 +93,7 @@ def __init__(self, quotient, method, storm_control):
     def synthesize(self, family, print_stats=True):
         synthesizer = self.synthesizer(self.quotient)
         family.constraint_indices = self.quotient.design_space.constraint_indices
-        assignment = synthesizer.synthesize(family, print_stats=print_stats)
+        assignment = synthesizer.synthesize(family, keep_optimum=True, print_stats=print_stats)
         self.total_iters += synthesizer.stat.iterations_mdp
         return assignment
 

paynt/verification/property.py

@@ -199,11 +199,9 @@ def __init__(self, prop, discount_factor=1, epsilon=0):
         if rf.optimality_type == stormpy.OptimizationDirection.Minimize:
             self.minimizing = True
             self.op = operator.lt
-            self.threshold = math.inf
         else:
             self.minimizing = False
             self.op = operator.gt
-            self.threshold = -math.inf
 
         # construct quantitative formula (without bound) for explicit model checking
         self.formula = rf.clone()
@@ -213,6 +211,9 @@ def __init__(self, prop, discount_factor=1, epsilon=0):
         self.optimum = None
         self.epsilon = epsilon
 
+        self.reset()
+
+
     def __str__(self):
         eps = f"[eps = {self.epsilon}]" if self.epsilon > 0 else ""
         return f"{str(self.property.raw_formula)} {eps}"
@@ -222,6 +223,10 @@ def copy(self):
 
     def reset(self):
         self.optimum = None
+        if self.minimizing:
+            self.threshold = math.inf
+        else:
+            self.threshold = -math.inf
 
     def meets_op(self, a, b):
         ''' For optimality objective, we want to accept improvements above model checking precision. '''
@@ -235,7 +240,6 @@ def improves_optimum(self, value):
 
     def update_optimum(self, optimum):
         # assert self.improves_optimum(optimum)
-        #logger.debug(f"New opt = {optimum}.")
         self.optimum = optimum
         if self.minimizing:
             self.threshold = optimum * (1 - self.epsilon)