diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index babbb4a78..4bcf324e6 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/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 diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 517fac3f7..7f125031c 100644 --- a/paynt/synthesizer/statistic.py +++ b/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,7 +54,7 @@ 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 @@ -59,6 +62,17 @@ 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 diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py index 1cb6d35fb..ab6204201 100644 --- a/paynt/synthesizer/synthesizer.py +++ b/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) diff --git a/paynt/synthesizer/synthesizer_onebyone.py b/paynt/synthesizer/synthesizer_onebyone.py index acd43c88c..ef2c6941f 100644 --- a/paynt/synthesizer/synthesizer_onebyone.py +++ b/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) )