From 01b0bc03bd17505cd4de03c7453ca5a9f2de863d Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 24 Nov 2023 18:02:18 +0100 Subject: [PATCH] move synthesis of all family members to SynthesizerAR --- paynt/quotient/quotient.py | 2 +- paynt/synthesizer/synthesizer_all.py | 53 ------------- paynt/synthesizer/synthesizer_ar.py | 92 +++++++++++++++++++++-- paynt/synthesizer/synthesizer_onebyone.py | 3 + paynt/synthesizer/synthesizer_pomdp.py | 4 +- paynt_pomdp_sketch.py | 9 ++- 6 files changed, 99 insertions(+), 64 deletions(-) delete mode 100644 paynt/synthesizer/synthesizer_all.py diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index 6ab52d0ea..946bc3d18 100644 --- a/paynt/quotient/quotient.py +++ b/paynt/quotient/quotient.py @@ -185,7 +185,7 @@ def expected_visits(self, mdp, prop, choices): dtmc = QuotientContainer.mdp_to_dtmc(sub_mdp) # compute visits - dtmc_visits = stormpy.synthesis.compute_expected_number_of_visits(MarkovChain.environment, dtmc).get_values() + dtmc_visits = stormpy.compute_expected_number_of_visits(MarkovChain.environment, dtmc).get_values() dtmc_visits = list(dtmc_visits) # handle infinity- and zero-visits diff --git a/paynt/synthesizer/synthesizer_all.py b/paynt/synthesizer/synthesizer_all.py deleted file mode 100644 index a38bb7782..000000000 --- a/paynt/synthesizer/synthesizer_all.py +++ /dev/null @@ -1,53 +0,0 @@ -import paynt.synthesizer.synthesizer -import paynt.synthesizer.synthesizer_ar - -import logging -logger = logging.getLogger(__name__) - -class SynthesizerAll(paynt.synthesizer.synthesizer_ar.SynthesizerAR): - - @property - def method_name(self): - return "AR (all)" - - def synthesize(self, family=None, find_all=False): - self.stat.start() - if family is None: - family = self.quotient.design_space - logger.info("synthesis initiated, design space: {}".format(family.size)) - satisfying_families,unsatisfying_families = self.synthesize_all(family) - self.stat.finished(satisfying_families) - return satisfying_families - - def synthesize_all(self, family=None): - # assuming no optimality - assert not self.quotient.specification.has_optimality - self.quotient.discarded = 0 - satisfying_families = [] - unsatisfying_families = [] - families = [family] - while families: - family = families.pop() - self.quotient.build(family) - self.stat.iteration_mdp(family.mdp.states) - res = family.mdp.check_specification(self.quotient.specification, constraint_indices = family.constraint_indices, short_evaluation = True) - family.analysis_result = res - if res.improving_assignment == "any": - self.explore(family) - satisfying_families.append(family) - continue - - if res.can_improve == False: - self.explore(family) - unsatisfying_families.append(family) - continue - - # undecided - subfamilies = self.quotient.split(family, paynt.synthesizer.synthesizer.Synthesizer.incomplete_search) - families = families + subfamilies - - return satisfying_families,unsatisfying_families - - - def evaluate_all(self, family): - pass diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index ca8345766..36a30fa06 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -1,8 +1,9 @@ -from .synthesizer import Synthesizer +import paynt.synthesizer.synthesizer -import paynt +import logging +logger = logging.getLogger(__name__) -class SynthesizerAR(Synthesizer): +class SynthesizerAR(paynt.synthesizer.synthesizer.Synthesizer): @property def method_name(self): @@ -47,7 +48,7 @@ def synthesize_assignment(self, family): continue # undecided - subfamilies = self.quotient.split(family, Synthesizer.incomplete_search) + subfamilies = self.quotient.split(family, paynt.synthesizer.synthesizer.Synthesizer.incomplete_search) families = families + subfamilies return satisfying_assignment @@ -95,10 +96,91 @@ def synthesize_assignment_experimental(self, family): # split family with the best value family = undecided_families[0] - subfamilies = self.quotient.split(family, Synthesizer.incomplete_search) + subfamilies = self.quotient.split(family, paynt.synthesizer.synthesizer.Synthesizer.incomplete_search) families = subfamilies + undecided_families[1:] return satisfying_assignment + + def synthesize_all(self, family=None): + self.stat.start() + if family is None: + family = self.quotient.design_space + logger.info("synthesis initiated, design space: {}".format(family.size)) + assert not self.quotient.specification.has_optimality, "expecting specification with constraints only" + self.quotient.discarded = 0 + + satisfying_families = [] + unsatisfying_families = [] + families = [family] + while families: + family = families.pop() + self.quotient.build(family) + self.stat.iteration_mdp(family.mdp.states) + res = family.mdp.check_specification(self.quotient.specification, constraint_indices = family.constraint_indices, short_evaluation = True) + family.analysis_result = res + if res.improving_assignment == "any": + self.explore(family) + satisfying_families.append(family) + continue + + if res.can_improve == False: + self.explore(family) + unsatisfying_families.append(family) + continue + + # undecided + subfamilies = self.quotient.split(family, paynt.synthesizer.synthesizer.Synthesizer.incomplete_search) + families = families + subfamilies + + self.stat.finished(satisfying_families) + return satisfying_families,unsatisfying_families + + + def evaluate_family(self, family, prop, precision): + self.quotient.build(family) + self.stat.iteration_mdp(family.mdp.states) + + # compute minimum first + result_primary = family.mdp.model_check_property(prop, alt=prop.maximizing) + if prop.reward and math.isinf(result_primary.value): + return None,None + result_secondary = family.mdp.model_check_property(prop, alt=True) + print(result_primary.value) + exit() + + def evaluate_all(self, family=None, precision=0): + raise NotImplementedError("AR does not support evaluation of all family members") + + self.stat.start() + if family is None: + family = self.quotient.design_space + logger.info("synthesis initiated, design space: {}".format(family.size)) + assert self.quotient.specification.has_optimality, "expecting specification without contstraints" + self.quotient.discarded = 0 + + prop = self.quotient.get_property() + family_to_value = [] + + families = [family] + while families: + family = families.pop() + res = self.evaluate_family(family,prop,precision) + family.analysis_result = res + if res.improving_assignment == "any": + self.explore(family) + satisfying_families.append(family) + continue + + if res.can_improve == False: + self.explore(family) + unsatisfying_families.append(family) + continue + + # undecided + subfamilies = self.quotient.split(family, paynt.synthesizer.synthesizer.Synthesizer.incomplete_search) + families = families + subfamilies + self.stat.finished(family_to_value) + return family_to_value diff --git a/paynt/synthesizer/synthesizer_onebyone.py b/paynt/synthesizer/synthesizer_onebyone.py index a7c1ea2ed..af7deab75 100644 --- a/paynt/synthesizer/synthesizer_onebyone.py +++ b/paynt/synthesizer/synthesizer_onebyone.py @@ -30,3 +30,6 @@ def synthesize_assignment(self, family): return accepting_assignment return satisfying_assignment + + def evaluate_all(self, family=None): + raise NotImplementedError("One-by-one synthesizer does not support evaluation of all family members") diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py index 540b74835..6a3c62961 100644 --- a/paynt/synthesizer/synthesizer_pomdp.py +++ b/paynt/synthesizer/synthesizer_pomdp.py @@ -594,7 +594,7 @@ def strategy_expected(self): # dtmc = self.quotient.build_chain(synthesized_assignment) # # compute expected visits for this dtmc - # dtmc_visits = stormpy.synthesis.compute_expected_number_of_visits(MarkovChain.environment, dtmc.model).get_values() + # dtmc_visits = stormpy.compute_expected_number_of_visits(MarkovChain.environment, dtmc.model).get_values() # dtmc_visits = list(dtmc_visits) # # handle infinity- and zero-visits @@ -821,7 +821,7 @@ def strategy_expected_uai(self): dtmc = self.quotient.build_chain(synthesized_assignment) # compute expected visits for this dtmc - dtmc_visits = stormpy.synthesis.compute_expected_number_of_visits(MarkovChain.environment, dtmc.model).get_values() + dtmc_visits = stormpy.compute_expected_number_of_visits(MarkovChain.environment, dtmc.model).get_values() dtmc_visits = list(dtmc_visits) # handle infinity- and zero-visits diff --git a/paynt_pomdp_sketch.py b/paynt_pomdp_sketch.py index ebb85a271..4fed0906a 100644 --- a/paynt_pomdp_sketch.py +++ b/paynt_pomdp_sketch.py @@ -3,6 +3,8 @@ import paynt.cli import paynt.parser.sketch import paynt.quotient.pomdp_family +import paynt.synthesizer.synthesizer_onebyone +import paynt.synthesizer.synthesizer_ar import os import random @@ -75,11 +77,12 @@ def investigate_hole_assignment(pomdp_sketch, hole_assignment): dtmc_sketch = pomdp_sketch.build_dtmc_sketch(fsc) # to each (sub-family of) environment(s), assign a value corresponding to the minimum specification satisfiability -# TODO +synthesizer = paynt.synthesizer.synthesizer_onebyone.SynthesizerOneByOne(dtmc_sketch) +family_to_value = synthesizer.evaluate_all() # pick the worst environment # TODO -worst_family = pomdp_sketch.design_space.pick_random() +worst_family,worst_value = family_to_value[0] -print("printing the worst family below:") +print("the worst value has value {}, printing the worst family below:".format(worst_value)) print(worst_family)