adapt 1-by-1 synthesizer to general models

paynt/synthesizer/policy_tree.py

@@ -397,13 +397,13 @@ def double_check_policy(quotient, family, prop, policy):
     def verify_policy(self, family, prop, policy):
         _,mdp = self.quotient.fix_and_apply_policy_to_family(family, policy)
         policy_result = mdp.model_check_property(prop, alt=True)
-        self.stat.iteration_mdp(mdp.states)
+        self.stat.iteration(mdp)
         return policy_result.sat
 
 
     def solve_singleton(self, family, prop):
         result = family.mdp.model_check_property(prop)
-        self.stat.iteration_mdp(family.mdp.states)
+        self.stat.iteration(family.mdp)
         if not result.sat:
             return False
         policy = self.quotient.scheduler_to_policy(result.result.scheduler, family.mdp)
@@ -485,7 +485,7 @@ def verify_family(self, family, game_solver, prop):
             # solve primary direction for the MDP abstraction
             mdp_result = family.mdp.model_check_property(prop)
             mdp_value = mdp_result.value
-            self.stat.iteration_mdp(family.mdp.states)
+            self.stat.iteration(family.mdp)
             # logger.debug("primary-primary direction solved, value is {}".format(mdp_value))
             if not mdp_result.sat:
                 mdp_family_result.policy = False
@@ -528,7 +528,6 @@ def compute_scores(self, prop, scheduler_choices, state_values, inconsistent_ass
         return scores
 
     def split(self, family, prop, hole_selection, splitter):
-
         # split the hole
         used_options = hole_selection[splitter]
         if len(used_options) > 1:
@@ -619,7 +618,7 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
                 self.quotient.build(subfamily)
                 primary_result = subfamily.mdp.model_check_property(prop)
                 assert primary_result.result.has_scheduler
-                self.stat.iteration_mdp(subfamily.mdp.states)
+                self.stat.iteration(subfamily.mdp)
 
                 if primary_result.sat == False:
                     unsat_mdp_families.append(subfamily)
@@ -662,7 +661,7 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
                     current_action_family.mdp.model, prop.formula, extract_scheduler=True, environment=Property.environment)
                 value = mc_result.at(current_action_family.mdp.initial_state)
                 primary_result = paynt.verification.property_result.PropertyResult(prop, mc_result, value)
-                self.stat.iteration_mdp(current_action_family.mdp.states)
+                self.stat.iteration(current_action_family.mdp)
 
                 # discard the family as soon as one MDP is unsat
                 if primary_result.sat == False:
@@ -726,7 +725,7 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
             self.quotient.build(sat_mdp_families[mdp_index])
             primary_result = sat_mdp_families[mdp_index].mdp.model_check_property(prop)
             assert primary_result.result.has_scheduler
-            self.stat.iteration_mdp(sat_mdp_families[mdp_index].mdp.states)
+            self.stat.iteration(sat_mdp_families[mdp_index].mdp)
             policy = self.quotient.scheduler_to_policy(primary_result.result.scheduler, sat_mdp_families[mdp_index].mdp)
             sat_mdp_policies[mdp_index] = policy
 

paynt/synthesizer/statistic.py

@@ -1,4 +1,7 @@
-from ..utils.profiler import Timer
+import stormpy
+import stormpy.storage
+
+import paynt.utils.profiler
 
 import logging
 logger = logging.getLogger(__name__)
@@ -22,7 +25,7 @@ class Statistic:
 
     # parameters
     status_period = 3
-    whole_synthesis_timer = Timer()
+    whole_synthesis_timer = paynt.utils.profiler.Timer()
 
     def __init__(self, synthesizer):
 
@@ -51,14 +54,25 @@ def __init__(self, synthesizer):
         self.num_policies_merged = None
         self.num_policies_yes = None
 
-        self.synthesis_time = Timer()
+        self.synthesis_time = paynt.utils.profiler.Timer()
         self.status_horizon = Statistic.status_period
 
 
     def start(self):
         self.synthesis_time.start()
 
 
+    def iteration(self, model):
+        ''' Identify the type of the model and count corresponding iteration. '''
+        if isinstance(model, paynt.quotient.models.MarkovChain):
+            model = model.model
+        if type(model) == stormpy.storage.SparseDtmc:
+            self.iteration_dtmc(model.nr_states)
+        elif type(model) == stormpy.storage.SparseMdp:
+            self.iteration_mdp(model.nr_states)
+        else:
+            logger.debug(f"unknown model type {type(model)}")
+
     def iteration_dtmc(self, size_dtmc):
         if self.iterations_dtmc is None:
             self.iterations_dtmc = 0

paynt/synthesizer/synthesizer.py

@@ -89,8 +89,8 @@ def run(self):
         if assignment is not None:
             logger.info("Printing synthesized assignment below:")
             logger.info(assignment)
-            chain = self.quotient.build_chain(assignment)
-            result = chain.check_specification(self.quotient.specification)
+            model = self.quotient.build_chain(assignment)
+            result = model.check_specification(self.quotient.specification)
             logger.info("Double-checking specification satisfiability: {}".format(result))
             if self.quotient.export_optimal_result:
                 self.quotient.export_result(dtmc, result)

paynt/synthesizer/synthesizer_onebyone.py

@@ -16,9 +16,9 @@ def synthesize_assignment(self, family):
         for hole_combination in family.all_combinations():
 
             assignment = family.construct_assignment(hole_combination)
-            chain = self.quotient.build_chain(assignment)
-            self.stat.iteration_dtmc(chain.states)
-            result = chain.check_specification(self.quotient.specification, short_evaluation = True)
+            model = self.quotient.build_chain(assignment)
+            self.stat.iteration(model)
+            result = model.check_specification(self.quotient.specification, short_evaluation = True)
             self.explore(assignment)
 
             accepting,improving_value = result.accepting_dtmc(self.quotient.specification)
@@ -38,7 +38,7 @@ def evaluate_all_wrt_property(self, family=None, prop=None, keep_value_only=Fals
         :param prop if None, then the default property of the quotient will be used
         :param keep_value_only if True, then, instead of property result, only the corresponding value will be
             associated with the member
-        :returns a list of (family,property result) pairs where family is neceesarily a singleton
+        :returns a list of (family,property result) pairs where family is necessarily a singleton
         '''
         if family is None:
             family = self.quotient.design_space
@@ -47,9 +47,9 @@ def evaluate_all_wrt_property(self, family=None, prop=None, keep_value_only=Fals
         assignment_evaluation = []
         for hole_combination in family.all_combinations():
             assignment = family.construct_assignment(hole_combination)
-            chain = self.quotient.build_chain(assignment)
-            self.stat.iteration_dtmc(chain.states)
-            evaluation = chain.model_check_property(prop)
+            model = self.quotient.build_chain(assignment)
+            self.stat.iteration(model)
+            evaluation = model.model_check_property(prop)
             if keep_value_only:
                 evaluation = evaluation.value
             assignment_evaluation.append( (assignment,evaluation) )