fix single-property synthesis

paynt/parser/sketch.py

@@ -122,7 +122,7 @@ def load_sketch(cls, sketch_path, properties_path,
             except SyntaxError:
                 pass
 
-        assert filetype is not None, "unknow format of input file"
+        assert filetype is not None, "unknown format of input file"
         logger.info("sketch parsing OK")
 
         paynt.verification.property.Property.initialize()

paynt/quotient/quotient.py

@@ -267,11 +267,6 @@ def holes_with_max_score(self, hole_score):
         with_max_score = [hole_index for hole_index in hole_score if hole_score[hole_index] == max_score]
         return with_max_score
 
-    def most_inconsistent_holes(self, scheduler_assignment):
-        num_definitions = [len(options) for options in scheduler_assignment]
-        most_inconsistent = self.holes_with_max_score(num_definitions) 
-        return most_inconsistent
-
     def split(self, family):
 
         mdp = family.mdp

paynt/synthesizer/synthesizer.py

@@ -16,7 +16,7 @@ def __init__(self, family, value, sat, policy):
 class Synthesizer:
 
     @staticmethod
-    def choose_synthesizer(quotient, method, fsc_synthesis, storm_control):
+    def choose_synthesizer(quotient, method, fsc_synthesis=False, storm_control=None):
 
         # hiding imports here to avoid mutual top-level imports
         import paynt.quotient.mdp
@@ -168,8 +168,9 @@ def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, re
         if self.best_assignment is not None and self.best_assignment.size > 1 and not return_all:
             self.best_assignment = self.best_assignment.pick_any()
         self.stat.finished_synthesis()
-        # logger.info("synthesis finished, printing synthesized assignment below:")
-        # logger.info(assignment)
+        if self.best_assignment is not None:
+            logger.info("printing synthesized assignment below:")
+            logger.info(self.best_assignment)
 
         if self.best_assignment is not None and self.best_assignment.size == 1:
             dtmc = self.quotient.build_assignment(self.best_assignment)

paynt/synthesizer/synthesizer_ar.py

@@ -16,35 +16,40 @@ def check_specification_for_mdp(self, family):
         self.stat.iteration(mdp)
 
         # check constraints
+        admissible_assignment = None
         spec = self.quotient.specification
         if family.constraint_indices is None:
             family.constraint_indices = spec.all_constraint_indices()
         results = [None for _ in spec.constraints]
         for index in family.constraint_indices:
             constraint = spec.constraints[index]
             result = paynt.verification.property_result.MdpPropertyResult(constraint)
+            results[index] = result
 
             # check primary direction
             result.primary = mdp.model_check_property(constraint)
-
-            # no need to check secondary direction if primary direction yields UNSAT
-            if not result.primary.sat:
+            if result.primary.sat is False:
                 result.sat = False
-            else:
-                # check secondary direction
-                result.secondary = mdp.model_check_property(constraint, alt=True)
-                if mdp.is_deterministic and result.primary.value != result.secondary.value:
-                    logger.warning("WARNING: model is deterministic but min<max")
-                if result.secondary.sat:
+                break
+
+            # check if the primary scheduler is consistent
+            result.primary_selection,consistent = self.quotient.scheduler_is_consistent(mdp, constraint, result.primary.result)
+            if consistent:
+                assignment = family.assume_options_copy(result.primary_selection)
+                dtmc = self.quotient.build_assignment(assignment)
+                res = dtmc.check_specification(self.quotient.specification)
+                if res.accepting_dtmc(self.quotient.specification):
                     result.sat = True
+                    admissible_assignment = assignment
+
+            # primary direction is SAT: check secondary direction to see whether all SAT
+            result.secondary = mdp.model_check_property(constraint, alt=True)
+            if mdp.is_deterministic and result.primary.value != result.secondary.value:
+                logger.warning("WARNING: model is deterministic but min<max")
+            if result.secondary.sat:
+                result.sat = True
+                continue
 
-            # primary direction is SAT
-            if result.sat is None:
-                # check if the primary scheduler is consistent
-                result.primary_selection,_ = self.quotient.scheduler_is_consistent(mdp, constraint, result.primary.result)
-            results[index] = result
-            if result.sat is False:
-                break
         spec_result = paynt.verification.property_result.MdpSpecificationResult()
         spec_result.constraints_result = paynt.verification.property_result.ConstraintsResult(results)
 
@@ -73,7 +78,7 @@ def check_specification_for_mdp(self, family):
                         result.improving_value = res.optimality_result.value
             spec_result.optimality_result = result
 
-        spec_result.evaluate(family)
+        spec_result.evaluate(family, admissible_assignment)
         family.analysis_result = spec_result
 
 
@@ -84,14 +89,20 @@ def verify_family(self, family):
 
     def update_optimum(self, family):
         ia = family.analysis_result.improving_assignment
-        iv = family.analysis_result.improving_value
-        if iv is not None and self.quotient.specification.optimality.improves_optimum(iv):
-            self.quotient.specification.optimality.update_optimum(iv)
+        if ia is None:
+            return
+        if not self.quotient.specification.has_optimality:
             self.best_assignment = ia
-            self.best_assignment_value = iv
-            # logger.info(f"new optimum achieved: {iv}")
-            if isinstance(self.quotient, paynt.quotient.pomdp.PomdpQuotient):
-                self.stat.new_fsc_found(family.analysis_result.improving_value, ia, self.quotient.policy_size(ia))
+            return
+        iv = family.analysis_result.improving_value
+        if not self.quotient.specification.optimality.improves_optimum(iv):
+            return
+        self.quotient.specification.optimality.update_optimum(iv)
+        self.best_assignment = ia
+        self.best_assignment_value = iv
+        # logger.info(f"new optimum achieved: {iv}")
+        if isinstance(self.quotient, paynt.quotient.pomdp.PomdpQuotient):
+            self.stat.new_fsc_found(family.analysis_result.improving_value, ia, self.quotient.policy_size(ia))
 
 
     def synthesize_one(self, family):

paynt/verification/property.py

@@ -118,7 +118,7 @@ def alt_formula(formula):
         return formula_alt
 
     def __str__(self):
-        return str(self.formula)
+        return str(self.property.raw_formula)
 
     @property
     def reward(self):

paynt/verification/property_result.py

@@ -107,9 +107,9 @@ def __init__(self, prop):
 class MdpSpecificationResult(SpecificationResult):
 
     def __init__(self):
-        pass
+        super().__init__()
 
-    def evaluate(self, family):
+    def evaluate(self, family=None, admissible_assignment=None):
         self.improving_assignment = None
         self.improving_value = None
         self.can_improve = None
@@ -124,7 +124,10 @@ def evaluate(self, family):
         if cr.sat is True:
             # all constraints were satisfied
             if opt is None:
-                self.improving_assignment = family
+                if admissible_assignment is not None:
+                    self.improving_assignment = admissible_assignment
+                else:
+                    self.improving_assignment = family
                 self.can_improve = False
             else:
                 self.improving_assignment = opt.improving_assignment