move synthesis of all family members to SynthesizerAR

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

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

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")

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

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)