diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index 39fb73708..d8e45d374 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/paynt/synthesizer/policy_tree.py @@ -8,6 +8,7 @@ import paynt.quotient.quotient import paynt.verification.property_result from paynt.verification.property import Property +import paynt.utils.profiler import paynt.family.smt import paynt.synthesizer.conflict_generator.dtmc @@ -406,9 +407,8 @@ def merge_compatible_policies(self, policy_indices): def postprocess(self, quotient, prop): - import paynt.utils.profiler - postprocessing_time = paynt.utils.profiler.Timer() - postprocessing_time.start() + postprocessing_timer = paynt.utils.profiler.Timer() + postprocessing_timer.start() logger.info("post-processing the policy tree...") logger.info("merging SAT siblings solved by non-exclusively compatible policies...") @@ -445,9 +445,10 @@ def postprocess(self, quotient, prop): nodes_removed = nodes_before - self.root.num_nodes() logger.info("removed {} nodes".format(nodes_removed)) - postprocessing_time.stop() - time = int(postprocessing_time.read()) + postprocessing_timer.stop() + time = int(postprocessing_timer.read()) logger.debug(f"postprocessing took {time} s") + return time def extract_policies(self, quotient): @@ -527,7 +528,7 @@ def solve_game_abstraction(self, family, prop, game_solver): game_solver.solve(family.selected_choices, prop.maximizing, prop.minimizing) self.stat.iteration_game(family.mdp.states) game_value = game_solver.solution_value - game_sat = prop.satisfies_threshold(game_value) + game_sat = prop.satisfies_threshold_within_precision(game_value) # logger.debug("game solved, value is {}".format(game_value)) game_policy = game_solver.solution_state_to_player1_action # fix irrelevant choices @@ -599,7 +600,12 @@ def verify_family(self, family, game_solver, prop): def choose_splitter(self, family, prop, scheduler_choices, state_values, hole_selection): inconsistent_assignments = {hole:options for hole,options in enumerate(hole_selection) if len(options) > 1} if len(inconsistent_assignments)==0: + # # pick any hole with multiple options involved in the hole selection + for hole,options in enumerate(hole_selection): + if family.hole_num_options(hole) > 1 and len(options) > 0: + return hole # pick any hole with multiple options + logger.debug("picking an arbitrary hole...") for hole in range(family.num_holes): if family.hole_num_options(hole) > 1: return hole @@ -656,12 +662,15 @@ def split(self, family, prop, hole_selection, splitter, policy): policy_consistent = all([len(options) <= 1 for options in hole_selection]) if policy_consistent: # associate the branch of the split that contains hole selection with the policy - assert len(used_options) == 1 - option = used_options[0] - for subfamily in subfamilies: - if option in subfamily.hole_options(splitter): - subfamily.candidate_policy = policy - break + if len(used_options) != 1: + logger.warning(f"splitting wrt. hole that has {len(used_options)} options within the scheduler" + + "(expected 1); most likely caused by model checking precision") + else: + option = used_options[0] + for subfamily in subfamilies: + if option in subfamily.hole_options(splitter): + subfamily.candidate_policy = policy + break return suboptions,subfamilies @@ -709,10 +718,13 @@ def evaluate_all(self, family, prop, keep_value_only=False): self.stat.num_mdps_total = self.quotient.design_space.size self.stat.num_mdps_sat = sum([n.family.size for n in policy_tree.collect_sat()]) self.stat.num_nodes = len(policy_tree.collect_all()) + self.stat.num_leaves = len(policy_tree.collect_leaves()) self.stat.num_policies = len(policy_tree.policies) - policy_tree.postprocess(self.quotient, prop) + postprocessing_time = policy_tree.postprocess(self.quotient, prop) policy_tree.print_stats() + self.stat.postprocessing_time = postprocessing_time self.stat.num_nodes_merged = len(policy_tree.collect_all()) + self.stat.num_leaves_merged = len(policy_tree.collect_leaves()) self.stat.num_policies_merged = len(policy_tree.policies) self.policy_tree = policy_tree diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 098519cbb..531326c67 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -114,7 +114,7 @@ def status(self): fraction_explored = (self.synthesizer.explored + discarded) / self.family_size time_estimate = safe_division(self.synthesis_timer.read(), fraction_explored) percentage_explored = int(fraction_explored * 100000) / 1000.0 - ret_str += f"Progress {percentage_explored}%" + ret_str += f"progress {percentage_explored}%" time_elapsed = int(self.synthesis_timer.read()) ret_str += f", elapsed {time_elapsed} s" @@ -253,26 +253,40 @@ def print_mdp_family_table_entries(self): print(self.num_mdps_total,end=" ") print(self.quotient.quotient_mdp.nr_states*self.num_mdps_total,end=" ") print(self.num_mdps_sat,end=" ") - sat_by_total_percentage = round(self.num_mdps_sat/self.num_mdps_total*100,1) + sat_by_total_percentage = round(self.num_mdps_sat/self.num_mdps_total*100,2) print(sat_by_total_percentage) - - synt_stats_header = "synt info:\t" - synt_stats_header += "\t".join(["time","nodes","nodes (merged)","policies","policies (merged)","policies(merged) / SAT %","game iters","MDP iters", "iters/MDPs"]) + + headers = [ + "time","nodes","nodes (merged)","leaves","leaves (merged)","leaves (merged) / MDPs %", + "policies","policies (merged)","policies (merged) / SAT %","pp time","pp time %", + "game iters","MDP iters","iters/MDPs %"] + synt_stats_header = "synthesis info:\t" + "\t".join(headers) print(synt_stats_header) + # print("\t\t",end="") - synthesis_timer = int(self.synthesis_timer.time) - print(synthesis_timer,end=" ") + synthesis_time = int(self.synthesis_timer.time) + print(synthesis_time,end=" ") print(self.num_nodes,end=" ") print(self.num_nodes_merged,end=" ") + + print(self.num_leaves,end=" ") + print(self.num_leaves_merged,end=" ") + leaves_by_mdps = round(self.num_leaves_merged/self.num_mdps_total*100,2) + print(leaves_by_mdps,end=" ") + print(self.num_policies,end=" ") print(self.num_policies_merged,end=" ") - merged_by_sat_percentage = "N/A" + policies_by_sat = "N/A" if self.num_mdps_sat > 0: - merged_by_sat_percentage = round(self.num_policies_merged/self.num_mdps_sat*100,1) - print(merged_by_sat_percentage,end=" ") + policies_by_sat = round(self.num_policies_merged/self.num_mdps_sat*100,2) + print(policies_by_sat,end=" ") + print(self.postprocessing_time,end=" ") + postprocessing_time_percentage = round(self.postprocessing_time/synthesis_time*100,2) + print(postprocessing_time_percentage,end=" ") + print(self.iterations_game,end=" ") print(self.iterations_mdp,end=" ") - iters_by_mdp = round((self.iterations_game+self.iterations_mdp)/self.num_mdps_total,1) + iters_by_mdp = round((self.iterations_game+self.iterations_mdp)/self.num_mdps_total*100,2) print(iters_by_mdp) print() diff --git a/paynt/verification/property.py b/paynt/verification/property.py index feaf2d72f..cc1ba8630 100644 --- a/paynt/verification/property.py +++ b/paynt/verification/property.py @@ -69,6 +69,10 @@ def __init__(self, prop, discount_factor=1): # set threshold self.threshold = rf.threshold_expr.evaluate_as_double() + if self.minimizing: + self.threshold_plus_precision = self.threshold + Property.model_checking_precision + else: + self.threshold_plus_precision = self.threshold - Property.model_checking_precision # construct quantitative formula (without bound) for explicit model checking # set optimality type @@ -131,6 +135,9 @@ def result_valid(self, value): def satisfies_threshold(self, value): return self.result_valid(value) and self.op(value, self.threshold) + def satisfies_threshold_within_precision(self, value): + return self.result_valid(value) and self.op(value, self.threshold_plus_precision) + @property def can_be_improved(self): return False