From 387a3cf106f92b0f01deb2d978895cc66f82e167 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 19 Jan 2024 10:05:24 +0100 Subject: [PATCH] optional reset of the optimum value after synthesis --- paynt/synthesizer/synthesizer.py | 11 ++++++++--- paynt/synthesizer/synthesizer_pomdp.py | 2 +- paynt/verification/property.py | 10 +++++++--- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py index 6beeecb0c..41401cae4 100644 --- a/paynt/synthesizer/synthesizer.py +++ b/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 diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py index e18f43220..62ac12b36 100644 --- a/paynt/synthesizer/synthesizer_pomdp.py +++ b/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 diff --git a/paynt/verification/property.py b/paynt/verification/property.py index cc1ba8630..42228b09c 100644 --- a/paynt/verification/property.py +++ b/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)