diff --git a/paynt/quotient/mdp_family.py b/paynt/quotient/mdp_family.py index 84a555fce..9b7404a25 100644 --- a/paynt/quotient/mdp_family.py +++ b/paynt/quotient/mdp_family.py @@ -1,10 +1,9 @@ import stormpy import stormpy.synthesis -import paynt.quotient.holes -import paynt.quotient.models import paynt.quotient.quotient -import paynt.verification.property_result + +import collections import logging logger = logging.getLogger(__name__) @@ -12,8 +11,8 @@ class MdpFamilyQuotientContainer(paynt.quotient.quotient.QuotientContainer): - @classmethod - def extract_choice_labels(cls, mdp): + @staticmethod + def extract_choice_labels(mdp): ''' :param mdp having a canonic choice labeling (exactly 1 label for each choice) :return a list of action labels @@ -27,57 +26,123 @@ def extract_choice_labels(cls, mdp): label_to_action = {label:index for index,label in enumerate(action_labels)} choice_to_action = [None] * mdp.nr_choices - state_to_actions = [] - tm = mdp.transition_matrix for state in range(mdp.nr_states): - state_choice_label_indices = set() - for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + for choice in mdp.transition_matrix.get_rows_for_group(state): label = list(mdp.choice_labeling.get_labels_of_choice(choice))[0] action = label_to_action[label] choice_to_action[choice] = action - state_choice_label_indices.add(action) - state_to_actions.append(list(state_choice_label_indices)) - return action_labels,choice_to_action,state_to_actions + return action_labels,choice_to_action - - def __init__(self, quotient_mdp, coloring, specification): - super().__init__(quotient_mdp = quotient_mdp, coloring = coloring, specification = specification) - self.design_space = paynt.quotient.holes.DesignSpace(coloring.holes) - - self.action_labels,self.choice_to_action,self.state_to_actions = \ - MdpFamilyQuotientContainer.extract_choice_labels(self.quotient_mdp) - - self.choice_destinations = self.compute_choice_destinations(self.quotient_mdp) - self.state_action_choices = self.compute_state_action_choices(self.quotient_mdp, self.num_actions, self.choice_to_action) - - - @property - def num_actions(self): - return len(self.action_labels) - - - def compute_state_action_choices(self, mdp, num_actions, choice_to_action): + @staticmethod + def map_state_action_to_choices(mdp, num_actions, choice_to_action): state_action_choices = [] - tm = mdp.transition_matrix for state in range(mdp.nr_states): action_choices = [[] for action in range(num_actions)] - for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + for choice in mdp.transition_matrix.get_rows_for_group(state): action = choice_to_action[choice] action_choices[action].append(choice) state_action_choices.append(action_choices) return state_action_choices - def compute_choice_destinations(self, mdp): + @staticmethod + def map_state_to_available_actions(state_action_choices): + state_to_actions = [] + for state,action_choices in enumerate(state_action_choices): + available_actions = [] + for action,choices in enumerate(action_choices): + if choices: + available_actions.append(action) + state_to_actions.append(available_actions) + return state_to_actions + + @staticmethod + def compute_choice_destinations(mdp): choice_destinations = [] - tm = mdp.transition_matrix for choice in range(mdp.nr_choices): destinations = [] - for entry in tm.get_row(choice): + for entry in mdp.transition_matrix.get_row(choice): destinations.append(entry.column) choice_destinations.append(destinations) return choice_destinations + @staticmethod + def randomize_action_variant(mdp, state_action_choices): + ''' + Given an MDP having multiple variants of actions, create an MDP in which this variant selection is randomized. + ''' + + components = stormpy.storage.SparseModelComponents() + # copy state labeling + state_labeling = stormpy.storage.StateLabeling(mdp.nr_states) + for label in mdp.labeling.get_labels(): + state_labeling.add_label(label) + state_labeling.set_states(label, mdp.labeling.get_states(label)) + components.state_labeling = state_labeling + + # build transition matrix and reward models + reward_vectors = {name:[] for name in mdp.reward_models} + builder = stormpy.storage.SparseMatrixBuilder(has_custom_row_grouping=True) + tm = mdp.transition_matrix + num_rows = 0 + choice_to_action = [] + for state in range(mdp.nr_states): + builder.new_row_group(num_rows) + for action,choices in enumerate(state_action_choices[state]): + if not choices: + continue + + # new choice + choice_to_action.append(action) + + # handle transition matrix + num_choices = len(choices) + dst_prob = collections.defaultdict(int) + for choice in choices: + for entry in tm.get_row(choice): + dst_prob[entry.column] += entry.value()/num_choices + + for dst,prob in dst_prob.items(): + builder.add_next_value(num_rows,dst,prob) + num_rows += 1 + + # handle reward models + for name,reward_model in mdp.reward_models.items(): + reward_value = 0 + for choice in choices: + reward_value += reward_model.get_state_action_reward(choice) + reward_value /= num_choices + reward_vectors[name].append(reward_value) + + components.transition_matrix = builder.build() + components.reward_models = {} + for name,state_action_reward in reward_vectors.items(): + components.reward_models[name] = stormpy.SparseRewardModel(optional_state_action_reward_vector=state_action_reward) + model = stormpy.storage.SparseMdp(components) + + return model,choice_to_action + + + + def __init__(self, quotient_mdp, coloring, specification): + super().__init__(quotient_mdp = quotient_mdp, coloring = coloring, specification = specification) + + self.design_space = paynt.quotient.holes.DesignSpace(coloring.holes) + + self.action_labels,self.choice_to_action = MdpFamilyQuotientContainer.extract_choice_labels(self.quotient_mdp) + self.state_action_choices = MdpFamilyQuotientContainer.map_state_action_to_choices( + self.quotient_mdp, self.num_actions, self.choice_to_action) + self.state_to_actions = MdpFamilyQuotientContainer.map_state_to_available_actions(self.state_action_choices) + self.choice_destinations = MdpFamilyQuotientContainer.compute_choice_destinations(self.quotient_mdp) + + self.randomized_abstraction = MdpFamilyQuotientContainer.randomize_action_variant( + self.quotient_mdp, self.state_action_choices) + + + @property + def num_actions(self): + return len(self.action_labels) + def keep_reachable_choices(self, choice_mask, mdp=None, choice_destinations=None): if mdp is None: @@ -92,7 +157,7 @@ def keep_reachable_choices(self, choice_mask, mdp=None, choice_destinations=None choice_mask_reachable = stormpy.BitVector(mdp.nr_choices,False) while state_queue: state = state_queue.pop() - for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + for choice in mdp.transition_matrix.get_rows_for_group(state): if not choice_mask[choice]: continue choice_mask_reachable.set(choice,True) @@ -103,16 +168,6 @@ def keep_reachable_choices(self, choice_mask, mdp=None, choice_destinations=None return choice_mask_reachable - def choices_to_policy(self, choice_mask): - policy = [self.num_actions] * self.quotient_mdp.nr_states - tm = self.quotient_mdp.transition_matrix - for state in range(self.quotient_mdp.nr_states): - for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): - if choice_mask[choice]: - assert policy[state] == self.num_actions - policy[state] = self.choice_to_action[choice] - return policy - def choices_to_hole_selection(self, choice_mask): hole_selection = [set() for hole_index in self.design_space.hole_indices] @@ -123,6 +178,9 @@ def choices_to_hole_selection(self, choice_mask): hole_selection = [list(options) for options in hole_selection] return hole_selection + def empty_policy(self): + return [self.num_actions] * self.quotient_mdp.nr_states + def fix_policy_for_family(self, family, policy): ''' @@ -164,10 +222,31 @@ def apply_policy_to_family(self, family, policy): return self.build_from_choice_mask(choice_mask) - + def assert_mdp_is_deterministic(self, mdp, family): + if mdp.is_deterministic: + return + + logger.error(f"applied policy to a singleton family {family} and obtained MDP with nondeterminism") + for state in range(mdp.model.nr_states): + + choices = mdp.model.transition_matrix.get_rows_for_group(state) + if len(choices)>1: + quotient_state = mdp.quotient_state_map[state] + quotient_choices = [mdp.quotient_choice_map[choice] for choice in choices] + state_str = self.quotient_mdp.state_valuations.get_string(quotient_state) + state_str = state_str.replace(" ","") + state_str = state_str.replace("\t","") + actions_str = [self.action_labels[self.choice_to_action[choice]] for choice in quotient_choices] + logger.error(f"the following state {state_str} has multiple actions {actions_str}") + logger.error("aborting...") + exit(1) + + def build_game_abstraction_solver(self, prop): target_label = str(prop.formula.subformula.subformula) solver = stormpy.synthesis.GameAbstractionSolver( self.quotient_mdp, len(self.action_labels), self.choice_to_action, target_label ) return solver + + \ No newline at end of file diff --git a/paynt/quotient/pomdp_family.py b/paynt/quotient/pomdp_family.py index 82de25afc..ece5dbe93 100644 --- a/paynt/quotient/pomdp_family.py +++ b/paynt/quotient/pomdp_family.py @@ -137,41 +137,28 @@ def __init__(self, model, quotient, quotient_state_map, quotient_choice_map): self.state_action_to_local_choice.append(action_to_local_choice) -class PomdpFamilyQuotientContainer(paynt.quotient.quotient.QuotientContainer): +class PomdpFamilyQuotientContainer(paynt.quotient.mdp_family.MdpFamilyQuotientContainer): def __init__(self, quotient_mdp, coloring, specification, obs_evaluator): super().__init__(quotient_mdp = quotient_mdp, coloring = coloring, specification = specification) self.obs_evaluator = obs_evaluator - self.design_space = paynt.quotient.holes.DesignSpace(coloring.holes) - # a list of action labels - self.action_labels = None - # for each choice, an index of its label in self.action_labels - self.choice_to_action = None # for each observation, a list of actions (indices) available self.observation_to_actions = None - # POMDP manager used for unfolding the memory model into the quotient POMDP self.product_pomdp_fsc = None - self.action_labels,self.choice_to_action,state_to_actions = \ - paynt.quotient.mdp_family.MdpFamilyQuotientContainer.extract_choice_labels(self.quotient_mdp) - # identify actions available at each observation self.observation_to_actions = [None] * self.num_observations - for state,state_actions in enumerate(state_to_actions): + for state,available_actions in enumerate(self.state_to_actions): obs = self.state_to_observation[state] if self.observation_to_actions[obs] is not None: - assert self.observation_to_actions[obs] == state_actions,\ + assert self.observation_to_actions[obs] == available_actions,\ f"two states in observation class {obs} differ in available actions" continue - self.observation_to_actions[obs] = state_actions + self.observation_to_actions[obs] = available_actions - @property - def num_actions(self): - return len(self.action_labels) - @property def num_observations(self): return self.obs_evaluator.num_obs_classes diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index 273d1c493..e952eb3fa 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/paynt/synthesizer/policy_tree.py @@ -14,6 +14,7 @@ def __init__(self): # if False, then all family is UNSAT # otherwise, then contains a satisfying policy for all MDPs in the family self.policy = None + self.policy_source = "" self.scheduler_choices = None self.hole_selection = None @@ -107,7 +108,7 @@ def double_check(self, quotient, prop): else: mdp = quotient.apply_policy_to_family(self.family, self.policy) result = mdp.model_check_property(prop, alt=True) - assert result.sat + assert result.sat, self.family.size def merge_if_single_child(self): @@ -175,14 +176,6 @@ def merge_children_compatible(self, quotient, prop): return # only 1 child node that can be moved to this node PolicyTreeNode.merged += 1 - - - - - - - - class PolicyTree: @@ -237,7 +230,7 @@ def count_diversity(self): from collections import defaultdict children_stats = defaultdict(int) for node in self.collect_all(): - if node.policy is not None: + if node.is_leaf: continue with_policy = len([node for node in node.child_nodes if node.solved]) with_none = len([node for node in node.child_nodes if node.policy is None]) @@ -245,6 +238,14 @@ def count_diversity(self): children_stats[(with_policy,with_none,with_false)] += 1 return children_stats + def count_policy_sources(self): + from collections import defaultdict + sources = defaultdict(int) + for node in self.collect_leaves(): + sources[node.policy_source] += 1 + return sources + + def print_stats(self): members_total = self.root.family.size @@ -322,60 +323,58 @@ def postprocess(self, quotient, prop): self.print_stats() - +class SynthesizerPolicyTree(paynt.synthesizer.synthesizer.Synthesizer): + @property + def method_name(self): + return "AR (policy tree)" + def verify_policy(self, family, prop, policy): + mdp = self.quotient.apply_policy_to_family(family, policy) + if family.size == 1: + self.quotient.assert_mdp_is_deterministic(mdp, family) + policy_result = mdp.model_check_property(prop, alt=True) + self.stat.iteration_mdp(mdp.states) + return policy_result.sat + + def solve_singleton(self, family, prop): + result = family.mdp.model_check_property(prop) -class SynthesizerPolicyTree(paynt.synthesizer.synthesizer.Synthesizer): + self.stat.iteration_mdp(family.mdp.states) + if not result.sat: + return False - @property - def method_name(self): - return "AR (policy tree)" + policy = self.quotient.empty_policy() + for state in range(family.mdp.states): + quotient_state = family.mdp.quotient_state_map[state] + + state_choice = result.result.scheduler.get_choice(state).get_deterministic_choice() + choice = family.mdp.model.nondeterministic_choice_indices[state] + state_choice + quotient_choice = family.mdp.quotient_choice_map[choice] + action = self.quotient.choice_to_action[quotient_choice] - def verify_family(self, family, game_solver, prop, reference_policy=None): - self.quotient.build(family) - mdp_family_result = MdpFamilyResult() + policy[quotient_state] = action - # reference_policy = None - # if reference_policy is not None: - # # check if reference policy works - # mdp = self.quotient.apply_policy_to_family(family, reference_policy) - # policy_result = mdp.model_check_property(prop, alt=True) - # self.stat.iteration_mdp(mdp.states) - # if policy_result.sat: - # print("reference policy worked!") - # # this scheduler is good for all MDPs in the family - # mdp_family_result.policy = reference_policy - # return mdp_family_result + # TODO uncomment this to check policy before double_check() + # assert self.verify_policy(family,prop,policy) + + return policy - if family.size == 1: - primary_primary_result = family.mdp.model_check_property(prop) - self.stat.iteration_mdp(family.mdp.states) - # logger.debug("primary-primary direction solved, value is {}".format(primary_primary_result.value)) - if not primary_primary_result.sat: - mdp_family_result.policy = False - return mdp_family_result - # extract satisfying policy - scheduler = primary_primary_result.result.scheduler - choices = scheduler.compute_action_support(family.mdp.model.nondeterministic_choice_indices) - quotient_choice_mask = stormpy.BitVector(self.quotient.quotient_mdp.nr_choices, False) - for choice in choices: - quotient_choice_mask.set(family.mdp.quotient_choice_map[choice],True) - quotient_choice_mask = self.quotient.keep_reachable_choices(quotient_choice_mask) - mdp_family_result.policy = self.quotient.choices_to_policy(quotient_choice_mask) - return mdp_family_result + def solve_game_abstraction(self, family, prop, game_solver): # construct and solve the game abstraction - # logger.debug("solving the game...") + # logger.debug("solving game abstraction...") game_solver.solve(family.selected_actions_bv, prop.maximizing, prop.minimizing) self.stat.iteration_game(family.mdp.states) # logger.debug("game solved, value is {}".format(game_solver.solution_value)) - game_result_sat = prop.satisfies_threshold(game_solver.solution_value) + policy = game_solver.solution_state_to_player1_action + policy_sat = prop.satisfies_threshold(game_solver.solution_value) if False: + # double-check game value model,state_map,choice_map = self.quotient.restrict_mdp(self.quotient.quotient_mdp, game_solver.solution_reachable_choices) assert(model.nr_states == model.nr_choices) dtmc = paynt.quotient.models.DTMC(model, self.quotient, state_map, choice_map) @@ -384,57 +383,115 @@ def verify_family(self, family, game_solver, prop, reference_policy=None): if abs(dtmc_result.value-game_solver.solution_value) > 0.01: logger.error("game solution is {}, but DTMC model checker yielded {}".format(game_solver.solution_value,dtmc_result.value)) - # if not game_result_sat: - # # apply player 1 actions to the quotient - # policy = game_solver.solution_state_to_player1_action - # mdp = self.quotient.apply_policy_to_family(family, policy) - # policy_result = mdp.model_check_property(prop, alt=True) - # self.stat.iteration_mdp(mdp.states) - # if policy_result.sat: - # # this scheduler is good for all MDPs in the family - # print("game says NO but actually YES") - # mdp_family_result.policy = policy - # return mdp_family_result - - if game_result_sat: - # apply player 1 actions to the quotient - policy = game_solver.solution_state_to_player1_action - mdp = self.quotient.apply_policy_to_family(family, policy) - policy_result = mdp.model_check_property(prop, alt=True) - self.stat.iteration_mdp(mdp.states) - if policy_result.sat: - # this scheduler is good for all MDPs in the family - mdp_family_result.policy = policy + return policy, policy_sat + + + + def solve_randomized_abstraction(self, family, prop): + + choice_to_action = [] + for choice in range(family.mdp.choices): + action = self.quotient.choice_to_action[family.mdp.quotient_choice_map[choice]] + choice_to_action.append(action) + state_action_choices = self.quotient.map_state_action_to_choices(family.mdp.model,self.quotient.num_actions,choice_to_action) + model,choice_to_action = self.quotient.randomize_action_variant(family.mdp.model, state_action_choices) + assert family.mdp.model.nr_states == model.nr_states + + result = stormpy.synthesis.verify_mdp(paynt.quotient.models.MarkovChain.environment,model,prop.formula,True) + self.stat.iteration_mdp(model.nr_states) + value = result.at(model.initial_states[0]) + policy_sat = prop.satisfies_threshold(value) + + # extract policy for the quotient + scheduler = result.scheduler + policy = self.quotient.empty_policy() + for state in range(model.nr_states): + state_choice = scheduler.get_choice(state).get_deterministic_choice() + choice = model.transition_matrix.get_row_group_start(state) + state_choice + action = choice_to_action[choice] + quotient_state = family.mdp.quotient_state_map[state] + policy[quotient_state] = action + + return policy,policy_sat + + + + def verify_family(self, family, game_solver, prop, reference_policy=None): + self.quotient.build(family) + mdp_family_result = MdpFamilyResult() + + if False and reference_policy is not None: + # try reference policy + reference_policy_sat = self.verify_policy(family,prop,reference_policy) + if reference_policy_sat: + # print("reference policy worked!") + mdp_family_result.policy = reference_policy + mdp_family_result.policy_source = "singleton" return mdp_family_result - else: - print("game YES but nor forall family of size ", family.size) - # assert False, "game YES but nor forall" + + if family.size == 1: + mdp_family_result.policy = self.solve_singleton(family,prop) + return mdp_family_result + + if False: + randomized_policy,randomized_sat = self.solve_randomized_abstraction(family,prop) + if randomized_sat: + randomized_policy_sat = self.verify_policy(family,prop,randomized_policy) + if randomized_policy_sat: + mdp_family_result.policy = randomized_policy + mdp_family_result.policy_source = "randomized abstraction" + return mdp_family_result + + if True: + # game abstraction + game_policy,game_sat = self.solve_game_abstraction(family,prop,game_solver) + if game_sat: + game_policy_sat = self.verify_policy(family,prop,game_policy) + if game_policy_sat: + mdp_family_result.policy = game_policy + mdp_family_result.policy_source = "game abstraction" + return mdp_family_result + else: + print("game YES but nor forall family of size ", family.size) + + - # logger.debug("solving primary-primary direction...") # solve primary-primary direction for the family + # logger.debug("solving primary-primary direction...") primary_primary_result = family.mdp.model_check_property(prop) self.stat.iteration_mdp(family.mdp.states) # logger.debug("primary-primary direction solved, value is {}".format(primary_primary_result.value)) if not primary_primary_result.sat: mdp_family_result.policy = False return mdp_family_result + # undecided: prepare to split # map scheduler choices to hole options and check consistency - if True: + if False: + # optimistic splitting scheduler_choices = game_solver.solution_reachable_choices scheduler_choices = self.quotient.keep_reachable_choices(scheduler_choices) else: - mdp_choices = primary_primary_result.result.scheduler.compute_action_support(family.mdp.model.nondeterministic_choice_indices) - scheduler_choices = [family.mdp.quotient_choice_map[choice] for choice in mdp_choices] + # pessimistic splitting + scheduler_choices = stormpy.BitVector(self.quotient.quotient_mdp.nr_choices,False) + for state in range(family.mdp.states): + state_choice = primary_primary_result.result.scheduler.get_choice(state).get_deterministic_choice() + choice = family.mdp.model.nondeterministic_choice_indices[state] + state_choice + quotient_choice = family.mdp.quotient_choice_map[choice] + scheduler_choices.set(quotient_choice,True) + + scheduler_choices = self.quotient.keep_reachable_choices(scheduler_choices) hole_selection = self.quotient.choices_to_hole_selection(scheduler_choices) mdp_family_result.scheduler_choices = scheduler_choices mdp_family_result.hole_selection = hole_selection - if True: + + if False: for choice in scheduler_choices: assert choice in family.selected_actions_bv for hole_index,options in enumerate(hole_selection): assert all([option in family[hole_index].options for option in options]) + return mdp_family_result @@ -509,28 +566,32 @@ def synthesize_policy_tree(self, family): self.last_splitter = -1 prop = self.quotient.specification.constraints[0] game_solver = self.quotient.build_game_abstraction_solver(prop) + game_solver.enable_profiling(True) policy_tree = PolicyTree(family) - reference_policy = None + reference_policy = None policy_tree_leaves = [policy_tree.root] while policy_tree_leaves: + policy_tree_node = policy_tree_leaves.pop(-1) family = policy_tree_node.family # logger.info("investigating family of size {}".format(family.size)) result = self.verify_family(family,game_solver,prop,reference_policy) policy_tree_node.policy = result.policy + policy_tree_node.policy_source = result.policy_source if result.policy == False: - # logger.info("satisfying scheduler cannot be obtained for the following family {}".format(family)) + reference_policy = None self.explore(family) continue if result.policy is not None: - # logger.info("found policy for all MDPs in the family") reference_policy = result.policy self.explore(family) continue + reference_policy = None + # refine splitter,suboptions,subfamilies = self.split( family, prop, game_solver.solution_reachable_choices, game_solver.solution_state_values, result.hole_selection @@ -538,6 +599,7 @@ def synthesize_policy_tree(self, family): policy_tree_node.split(splitter,suboptions,subfamilies) policy_tree_leaves = policy_tree_leaves + policy_tree_node.child_nodes + game_solver.print_profiling() policy_tree.double_check_all_families(self.quotient, prop) policy_tree.print_stats() policy_tree.postprocess(self.quotient, prop) diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 4f3968b10..c1cd89252 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -29,15 +29,15 @@ def __init__(self, synthesizer): self.synthesizer = synthesizer self.quotient = self.synthesizer.quotient - self.iterations_dtmc = 0 + self.iterations_dtmc = None self.acc_size_dtmc = 0 self.avg_size_dtmc = 0 - self.iterations_mdp = 0 + self.iterations_mdp = None self.acc_size_mdp = 0 self.avg_size_mdp = 0 - self.iterations_game = 0 + self.iterations_game = None self.acc_size_game = 0 self.avg_size_game = 0 @@ -53,16 +53,22 @@ def start(self): def iteration_dtmc(self, size_dtmc): + if self.iterations_dtmc is None: + self.iterations_dtmc = 0 self.iterations_dtmc += 1 self.acc_size_dtmc += size_dtmc self.print_status() def iteration_mdp(self, size_mdp): + if self.iterations_mdp is None: + self.iterations_mdp = 0 self.iterations_mdp += 1 self.acc_size_mdp += size_mdp self.print_status() def iteration_game(self, size_game): + if self.iterations_game is None: + self.iterations_game = 0 self.iterations_game += 1 self.acc_size_game += size_game self.print_status() @@ -76,21 +82,31 @@ def new_fsc_found(self, value, assignment, size): def status(self): + ret_str = "> " discarded = self.quotient.discarded if self.quotient.discarded is not None else 0 - fraction_rejected = (self.synthesizer.explored + discarded) / self.quotient.design_space.size - time_estimate = safe_division(self.synthesis_time.read(), fraction_rejected) - percentage_rejected = int(fraction_rejected * 1000000) / 10000.0 - # percentage_rejected = fraction_rejected * 100 - time_elapsed = round(self.synthesis_time.read(),1) - time_estimate = round(time_estimate,1) - iters = (self.iterations_game,self.iterations_mdp,self.iterations_dtmc) - avg_size_mdp = safe_division(self.acc_size_mdp, self.iterations_mdp) - optimum = "-" + fraction_explored = (self.synthesizer.explored + discarded) / self.quotient.design_space.size + time_estimate = safe_division(self.synthesis_time.read(), fraction_explored) + percentage_explored = int(fraction_explored * 1000000) / 10000.0 + ret_str += f"Progress {percentage_explored}%" + + time_elapsed = int(self.synthesis_time.read()) + ret_str += f", elapsed {time_elapsed} s" + time_estimate = int(time_estimate) + ret_str += f", estimated {time_estimate} s" + time_estimate_hrs = round(time_estimate/3600, 1) + if time_estimate_hrs > 1: + ret_str += f" ({time_estimate_hrs} hrs)" + + iters = [self.iterations_game,self.iterations_mdp,self.iterations_dtmc] + iters = [str(i) for i in iters if i is not None] + ret_str += ", iters = (" + ", ".join(iters) + ")" + spec = self.quotient.specification if spec.has_optimality and spec.optimality.optimum is not None: optimum = round(spec.optimality.optimum,3) - - return f"> Progress {percentage_rejected}%, elapsed {time_elapsed} s, iters = {iters}, opt = {optimum}" + ret_str += f", opt = {optimum}" + return ret_str + def print_status(self): if not self.synthesis_time.read() > self.status_horizon: @@ -112,10 +128,6 @@ def finished(self, assignment): if self.quotient.specification.has_optimality: self.optimum = self.quotient.specification.optimality.optimum - self.avg_size_dtmc = safe_division(self.acc_size_dtmc, self.iterations_dtmc) - self.avg_size_mdp = safe_division(self.acc_size_mdp, self.iterations_mdp) - self.avg_size_game = safe_division(self.acc_size_game, self.iterations_game) - def get_summary(self): spec = self.quotient.specification specification = "\n".join([f"constraint {i + 1}: {str(f)}" for i,f in enumerate(spec.constraints)]) + "\n" @@ -131,16 +143,20 @@ def get_summary(self): timing = f"method: {self.synthesizer.method_name}, synthesis time: {round(self.synthesis_time.time, 2)} s" family_stats = "" - game_stats = f"Game stats: avg MDP size: {round(self.avg_size_game)}, iterations: {self.iterations_game}" - ar_stats = f"AR stats: avg MDP size: {round(self.avg_size_mdp)}, iterations: {self.iterations_mdp}" - cegis_stats = f"CEGIS stats: avg DTMC size: {round(self.avg_size_dtmc)}, iterations: {self.iterations_dtmc}" - if self.iterations_game > 0: - family_stats += f"{game_stats}\n" - if self.iterations_mdp > 0: - family_stats += f"{ar_stats}\n" - if self.iterations_dtmc > 0: - family_stats += f"{cegis_stats}\n" - + if self.iterations_game is not None: + avg_size = round(safe_division(self.acc_size_game, self.iterations_game)) + type_stats = f"Game stats: avg MDP size: {avg_size}, iterations: {self.iterations_game}" + family_stats += f"{type_stats}\n" + + if self.iterations_mdp is not None: + avg_size = round(safe_division(self.acc_size_mdp, self.iterations_mdp)) + type_stats = f"AR stats: avg MDP size: {avg_size}, iterations: {self.iterations_mdp}" + family_stats += f"{type_stats}\n" + + if self.iterations_dtmc is not None: + avg_size = round(safe_division(self.acc_size_mdp, self.iterations_dtmc)) + type_stats = f"CEGIS stats: avg DTMC size: {avg_size}, iterations: {self.iterations_dtmc}" + family_stats += f"{type_stats}\n" feasible = "yes" if self.feasible else "no" result = f"feasible: {feasible}" if self.optimum is None else f"optimal: {round(self.optimum, 6)}"