From 10d217d3cc966e314e04c5f6eabdc777be4a12d0 Mon Sep 17 00:00:00 2001 From: Aleksandr Shevchenko Date: Wed, 6 Mar 2024 16:15:08 +0100 Subject: [PATCH 1/3] 1 --- models/pomdp/grid/evade/sketch.props | 4 +- models/pomdp/other/cheese/sketch.props | 4 +- paynt/cli.py | 5 + paynt/family/family.py | 11 ++ paynt/quotient/pomdp.py | 8 +- paynt/quotient/quotient.py | 259 ++++++++++++++++++++++++- paynt/synthesizer/statistic.py | 11 +- paynt/synthesizer/synthesizer.py | 2 +- paynt/synthesizer/synthesizer_ar.py | 7 + 9 files changed, 299 insertions(+), 12 deletions(-) diff --git a/models/pomdp/grid/evade/sketch.props b/models/pomdp/grid/evade/sketch.props index 7c7dc5af2..c36288bae 100755 --- a/models/pomdp/grid/evade/sketch.props +++ b/models/pomdp/grid/evade/sketch.props @@ -1,2 +1,2 @@ -//Pmax=?["notbad" U "goal"]; -R{"steps"}min=? ["notbad" U "goal"] \ No newline at end of file +Pmax=?["notbad" U "goal"]; +//R{"steps"}min=? ["notbad" U "goal"] \ No newline at end of file diff --git a/models/pomdp/other/cheese/sketch.props b/models/pomdp/other/cheese/sketch.props index 4ea216c91..5c97650cf 100644 --- a/models/pomdp/other/cheese/sketch.props +++ b/models/pomdp/other/cheese/sketch.props @@ -1,2 +1,2 @@ -//P<0.5 [F "bad"] -R{"rew0"}max=? [F "goal"] \ No newline at end of file +P<0.5 [F "bad"] +//R{"rew0"}max=? [F "goal"] \ No newline at end of file diff --git a/paynt/cli.py b/paynt/cli.py index cb9627800..da75c29e3 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -126,6 +126,8 @@ def setup_logger(log_path = None): help="# if set, randomized abstraction guess-and-verify will be used instead of game abstraction;" + " MDP abstraction scheduler will be used for splitting" ) +@click.option("--use-inheritance", is_flag=True, default=False, + help="# if set, inheritance dependencies will be used for the synthesis of FSCs") @click.option( "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True, @@ -145,6 +147,7 @@ def paynt_run( export_fsc_storm, export_fsc_paynt, export_evaluation, all_in_one, mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction, + use_inheritance, ce_generator, profiling ): @@ -166,6 +169,8 @@ def paynt_run( paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction + paynt.quotient.quotient.Quotient.use_inheritance_build = use_inheritance + storm_control = None if storm_pomdp: storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl() diff --git a/paynt/family/family.py b/paynt/family/family.py index c38b57c04..fa2901319 100644 --- a/paynt/family/family.py +++ b/paynt/family/family.py @@ -136,6 +136,11 @@ def __init__(self): # index of a hole used to split the family self.splitter = None + # explicit list of all non-default actions in the MDP + self.selected_choices = None + # for each hole and for each option explicit list of all non-default actions in the MDP + self.hole_selected_choices = None + class DesignSpace(Family): ''' @@ -152,6 +157,9 @@ def __init__(self, family = None, parent_info = None): super().__init__(family) self.mdp = None + + self.hole_selected_choices = None + self.selected_choices = None # SMT encoding self.encoding = None @@ -223,12 +231,15 @@ def translate_analysis_hints(self): def collect_parent_info(self, specification): pi = ParentInfo() + pi.hole_selected_choices = self.hole_selected_choices + pi.selected_choices = self.selected_choices pi.refinement_depth = self.refinement_depth pi.analysis_hints = self.collect_analysis_hints(specification) cr = self.analysis_result.constraints_result pi.constraint_indices = cr.undecided_constraints if cr is not None else [] pi.splitter = self.splitter pi.mdp = self.mdp + pi.analysis_result = self.analysis_result return pi def encode(self, smt_solver): diff --git a/paynt/quotient/pomdp.py b/paynt/quotient/pomdp.py index 75f4871cd..69cb8d27b 100644 --- a/paynt/quotient/pomdp.py +++ b/paynt/quotient/pomdp.py @@ -383,6 +383,7 @@ def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_a # create inverse quotient-choice-to-mdp-choice map # TODO optimize this for multiple properties quotient_to_restricted_action_map = [None] * self.quotient_mdp.nr_choices + # print(self.quotient_mdp.nr_choices) for choice in range(mdp.nr_choices): quotient_to_restricted_action_map[quotient_choice_map[choice]] = choice @@ -420,8 +421,13 @@ def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_a assert len(self.hole_option_to_actions[hole_index][option]) > choice_index choice_global = self.hole_option_to_actions[hole_index][option][choice_index] - choice = quotient_to_restricted_action_map[choice_global] + choice = quotient_to_restricted_action_map[choice_global] + if choice is None: + continue + choice_value = choice_values[choice] + # print(choice_value) + # print() state_values.append(choice_value) min_value = min(state_values) diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index 0ff16851a..cc468e34c 100644 --- a/paynt/quotient/quotient.py +++ b/paynt/quotient/quotient.py @@ -10,6 +10,12 @@ import logging logger = logging.getLogger(__name__) +# import inspect + +# def print_caller_info(): +# caller_frame = inspect.stack()[2] +# print(f"Called from file: {caller_frame.filename} at line: {caller_frame.lineno}") + class Quotient: @@ -86,12 +92,176 @@ def build_from_choice_mask(self, choice_mask): return mdp + use_inheritance_build = False + + + def mine_scheduler_to_state_to_choice(self, family, parent_mdp, scheduler, compatible_choices, discard_unreachable_choices=True): + state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map) + parent_state_choice = self.empty_scheduler() + states_affected = [False for state in range(self.quotient_mdp.nr_states)] + parent_mdp = family.parent_info.mdp + for state in range(parent_mdp.model.nr_states): + qchoice = state_to_quotient_choice[state] + qstate = parent_mdp.quotient_state_map[state] + parent_state_choice[qstate] = qchoice + if not compatible_choices[qchoice]: + states_affected[qstate] = True + + if discard_unreachable_choices: + parent_state_choice = self.discard_unreachable_choices(parent_state_choice) + return parent_state_choice, states_affected + + def find_all_predecessors(self, family): + predecessors = [set() for s in range(self.quotient_mdp.nr_states)] + tm = family.mdp.model.transition_matrix + for s in range(self.quotient_mdp.nr_states): + for choice in range(tm.get_row_group_start(s),tm.get_row_group_end(s)): + for entry in tm.get_row(choice): + predecessors[entry.column].add(s) + self.predecessors_list = predecessors + + def get_parents_scheduler(self, family, compatible_choices): + parent_mdp = family.parent_info.mdp + parent_result = family.parent_info.analysis_result.optimality_result.primary.result + scheduler = parent_result.scheduler + return self.mine_scheduler_to_state_to_choice(family, parent_mdp, scheduler, compatible_choices, discard_unreachable_choices=False) + + def find_affected_reachable(self, states_affected): + state_queue = [s for s in range(self.quotient_mdp.nr_states) if states_affected[s]] + while state_queue: + state = state_queue.pop() + for pred in self.predecessors_list[state]: + if not states_affected[pred]: + state_queue.append(pred) + states_affected[pred] = True + + num_affected = sum(states_affected) + perc_affected = round(num_affected / self.quotient_mdp.nr_states * 100) + self.perc_affected_sum += perc_affected + self.perc_affected_entries += 1 + + def affected_to_choices(self, family, states_affected, parent_state_choice, compatible_choices): + + parent_mdp = family.parent_info.mdp + tm = parent_mdp.model.transition_matrix + qndi = self.quotient_mdp.nondeterministic_choice_indices.copy() + ndi = parent_mdp.model.nondeterministic_choice_indices.copy() + + + ###################################### WORKS + # for state in range(parent_mdp.model.nr_states): + # qstate = parent_mdp.quotient_state_map[state] + # if states_affected[qstate]: + # continue + # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + # # print("hm") + # qchoice = parent_mdp.quotient_choice_map[choice] + # if not qchoice in parent_state_choice: + # compatible_choices.set(qchoice, False) + # # print("HAHA!") + + # return compatible_choices + ###################################### + + + ###################################### WORKS TOO + # qstate_compatible_choices = [] + # for qstate in range(self.quotient_mdp.nr_states): + # qstate_choices = [] + # for qchoice in range(qndi[qstate],qndi[qstate+1]): + # if compatible_choices[qchoice]: + # qstate_choices.append(qchoice) + # qstate_compatible_choices.append(qstate_choices) + + # affected_states = [] + # for state,qstate in enumerate(parent_mdp.quotient_state_map): + # if states_affected[qstate]: + # affected_states.append( (state,qstate) ) + + + all_true = stormpy.BitVector(self.quotient_mdp.nr_choices, True) + for state,qstate in enumerate(parent_mdp.quotient_state_map): + if states_affected[qstate]: + continue + for choice in range(ndi[state],ndi[state+1]): + qchoice = parent_mdp.quotient_choice_map[choice] + all_true.set(qchoice, False) + + parent_choice = parent_state_choice[qstate] + all_true.set(parent_choice, True) + + return all_true & compatible_choices + ###################################### + + + ###################################### + + + ###################################### COULD WORK + # num_choices = self.quotient_mdp.nr_choices + # choices = stormpy.BitVector(num_choices,False) + # for state in range(parent_mdp.model.nr_states): + # qstate = parent_mdp.quotient_state_map[state] + # # if qstate == 159: + # # print("HEY", states_affected[qstate]) + # if states_affected[qstate]: + # # if qstate == 159: + # # print("EHM") + # # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + # # qchoice = parent_mdp.quotient_choice_map[choice] + # # choices.set(qchoice, compatible_choices.get(qchoice)) + + + # at_least_one = False + # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): + # qchoice = parent_mdp.quotient_choice_map[choice] + # choices.set(qchoice, compatible_choices.get(qchoice)) + # if choices.get(qchoice): + # at_least_one = True + # if not at_least_one: + # # print("WE WERE HERE") + # for choice in range(self.tm.get_row_group_start(qstate),self.tm.get_row_group_end(qstate)): + # # qchoice = parent_mdp.quotient_choice_map[choice] + # choices.set(choice, family.parent_info.selected_choices.get(choice)) + # else: + # qchoice = parent_state_choice[qstate] + # choices.set(qchoice, True) + + # return choices + ###################################### + + + def build_inheritance(self, family, compatible_choices): + if family.parent_info is None: + self.perc_affected_sum = 0 + self.perc_affected_entries = 0 + return compatible_choices + + num_choices = self.quotient_mdp.nr_choices + choices = stormpy.BitVector(num_choices,False) + parent_state_choice, states_affected = self.get_parents_scheduler(family, compatible_choices) + self.find_affected_reachable(states_affected) + choices = self.affected_to_choices(family, states_affected, parent_state_choice, compatible_choices) + return choices + def build(self, family): ''' Construct the quotient MDP for the family. ''' - # select actions compatible with the family and restrict the quotient - choices = self.coloring.selectCompatibleChoices(family.family) - family.selected_choices = choices - family.mdp = self.build_from_choice_mask(choices) + + compatible_choices = self.coloring.selectCompatibleChoices(family.family) + + if self.use_inheritance_build: + result_choices = self.build_inheritance(family, compatible_choices) + else: + result_choices = compatible_choices + # print(len(self.coloring.selectCompatibleChoices(family.family)), self.coloring.selectCompatibleChoices(family.family).number_of_set_bits(), len(result_choices), result_choices.number_of_set_bits()) + # print("COLORING - CHOICES: ", set(self.coloring.selectCompatibleChoices(family.family)).difference(set(compatible_choices))) + # print("CHOICES - COLORING: ", set(compatible_choices).difference(set(self.coloring.selectCompatibleChoices(family.family)))) + + family.selected_choices = result_choices + family.mdp = self.build_from_choice_mask(result_choices) + if self.use_inheritance_build and family.parent_info is None: + self.find_all_predecessors(family) + self.tm = family.mdp.model.transition_matrix family.mdp.design_space = family @@ -340,6 +510,8 @@ def discard(self, mdp, hole_assignments, core_suboptions, other_suboptions, inco def split(self, family, incomplete_search): + # if not self.use_inheritance_build: + # self.check_scheduler_inheritance(family) mdp = family.mdp assert not mdp.is_deterministic @@ -431,6 +603,85 @@ def sample(self): logger.info("done") + def check_scheduler_inheritance(self, family): + # print("VYZVALSYA CHECK SCHEDULER INHERITANCE") + # family --- DesignSpace! + + # if the family does not have a parent, then it is a super-family + # no need to check scheduler inheritance + if family.parent_info is None: + # print("SELECTED:", set(family.selected_choices)) + # print() + self.perc_affected_sum = 0 + self.perc_affected_entries = 0 + return + + # which choices were removed in the child family + choice_diff = set(family.parent_info.selected_choices).difference(set(family.selected_choices)) + # choice_diff = set(family.selected_choices).difference(set(family.selected_choices)) + # print("PARENT CHOICES: ", set(family.parent_info.selected_choices)) + # print() + # print("FAMILY CHOICES:", set(family.selected_choices)) + # print() + # print("CHOICE DIFF:", choice_diff) + # print() + + # get parent's scheduler for optimality + parent_mdp = family.parent_info.mdp + # parent_result = family.parent_info.analysis_result.optimality_result.primary.result + parent_result = family.parent_info.analysis_result.optimality_result.primary.result + assert not parent_result.scheduler.partial + + # get info from parent's scheduler + # print("NR STATES: ",self.quotient_mdp.nr_states) + # print() + parent_state_choice = [None for state in range(self.quotient_mdp.nr_states)] + for state in range(parent_mdp.states): + qstate = parent_mdp.quotient_state_map[state] + sched_choice = parent_result.scheduler.get_choice(state).get_deterministic_choice() + choice = parent_mdp.model.get_choice_index(state,sched_choice) + qchoice = parent_mdp.quotient_choice_map[choice] + parent_state_choice[qstate] = qchoice + # print("PARENT STATE CHOICE:", parent_state_choice) + # print(family) + # print(family.parent_info.splitter) # hole used for splitting + + # mark states in the sub-sub-MDP affected by the removal + state_affected = [False for state in range(family.mdp.states)] + for state in range(family.mdp.states): + qstate = family.mdp.quotient_state_map[state] + if parent_state_choice[qstate] in choice_diff: + state_affected[state] = True + + # for each state, a list of its predecessors + predecessors = [set() for s in range(family.mdp.states)] + tm = family.mdp.model.transition_matrix + for s in range(family.mdp.states): + for choice in range(tm.get_row_group_start(s),tm.get_row_group_end(s)): + for entry in tm.get_row(choice): + predecessors[entry.column].add(s) + + # find all states from which affected states are reachable + # queue of affected states + state_queue = [s for s in range(family.mdp.states) if state_affected[s]] + # print(tm) + while state_queue: + state = state_queue.pop() + # for each affected state, add its predecessors to the queue + for pred in predecessors[state]: + if not state_affected[pred]: + state_queue.append(pred) + state_affected[pred] = True + + # print("affected", state_affected[self.monitored_state]) + # print("parent has ", parent_result.at(self.monitored_state)) + + num_affected = len([x for x in state_affected if x]) + perc_affected = round(num_affected / family.mdp.states * 100) + self.perc_affected_sum += perc_affected + self.perc_affected_entries += 1 + # print("% affected states average: ", self.perc_affected_sum/self.perc_affected_entries) + def identify_absorbing_states(self, model): state_is_absorbing = [True] * model.nr_states tm = model.transition_matrix diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 8cec68a8b..a5bbe10a5 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -210,6 +210,11 @@ def get_summary_evaluation(self): members_total = self.quotient.design_space.size members_sat_percentage = int(round(members_sat/members_total*100,0)) return f"satisfied {members_sat}/{members_total} members ({members_sat_percentage}%)" + + def get_summary_affected(self): + if not self.quotient.use_inheritance_build or self.quotient.perc_affected_entries == 0: + return "" + return f"\naffected states average: {self.quotient.perc_affected_sum/self.quotient.perc_affected_entries} %" def get_summary(self): @@ -220,8 +225,10 @@ def get_summary(self): quotient_states = self.quotient.quotient_mdp.nr_states quotient_actions = self.quotient.quotient_mdp.nr_choices - design_space = f"number of holes: {self.quotient.design_space.num_holes}, family size: {self.quotient.design_space.size}, quotient: {quotient_states} states / {quotient_actions} actions" + # design_space = f"number of holes: {self.quotient.design_space.num_holes}, family size: {self.quotient.design_space.size}, quotient: {quotient_states} states / {quotient_actions} actions" + design_space = f"number of holes: {self.quotient.design_space.num_holes}, quotient: {quotient_states} states / {quotient_actions} actions" timing = f"method: {self.synthesizer.method_name}, synthesis time: {round(self.synthesis_timer.time, 2)} s" + affected = self.get_summary_affected() iterations = self.get_summary_iterations() @@ -234,7 +241,7 @@ def get_summary(self): summary = f"{sep}"\ f"Synthesis summary:\n" \ f"{specification}\n{timing}\n{design_space}\n{explored}\n" \ - f"{iterations}\n{result}\n"\ + f"{iterations}\n{result}{affected}\n"\ f"{sep}" return summary diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py index 41401cae4..a6a74b3ea 100644 --- a/paynt/synthesizer/synthesizer.py +++ b/paynt/synthesizer/synthesizer.py @@ -130,7 +130,7 @@ def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, re self.quotient.specification.optimality.update_optimum(optimum_threshold) logger.debug(f"optimality threshold set to {optimum_threshold}") - logger.info("synthesis initiated, design space: {}".format(family.size)) + # logger.info("synthesis initiated, design space: {}".format(family.size)) self.quotient.discarded = 0 self.stat.start(family) assignment = self.synthesize_one(family) diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index 0e1395376..da9643b8f 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -35,8 +35,15 @@ def synthesize_one(self, family): satisfying_assignment = None families = [family] + iteration_limit = 500 + iteration_count = 0 + while families: + iteration_count += 1 + if iteration_count > iteration_limit: + break + family = families.pop(-1) self.verify_family(family) From 49ca4e1504bb921f035fce0d86002ab695bb4878 Mon Sep 17 00:00:00 2001 From: Aleksandr Shevchenko Date: Sat, 16 Mar 2024 09:15:21 +0100 Subject: [PATCH 2/3] added c++ affected_to_choices --- paynt/cli.py | 5 ++- paynt/quotient/quotient.py | 33 +++++++++++------- payntbind/src/synthesis/quotient/bindings.cpp | 34 +++++++++++++++++++ 3 files changed, 59 insertions(+), 13 deletions(-) diff --git a/paynt/cli.py b/paynt/cli.py index 645b0e0e5..c98f4ef36 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -159,7 +159,7 @@ def paynt_run( profiler = None if profiling: profiler = cProfile.Profile() - profiler.enable() + # profiler.enable() logger.info("This is Paynt version {}.".format(version())) @@ -189,7 +189,10 @@ def paynt_run( if all_in_one is None: quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, discount_factor, precision, constraint_bound) synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control) + if profiling: + profiler.enable() synthesizer.run(optimum_threshold, export_evaluation) + else: all_in_one_program, specification, family = paynt.parser.sketch.Sketch.load_sketch_as_all_in_one(sketch_path, properties_path) all_in_one_analysis = paynt.synthesizer.all_in_one.AllInOne(all_in_one_program, specification, all_in_one, family) diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index cc468e34c..cb663dcec 100644 --- a/paynt/quotient/quotient.py +++ b/paynt/quotient/quotient.py @@ -97,7 +97,7 @@ def build_from_choice_mask(self, choice_mask): def mine_scheduler_to_state_to_choice(self, family, parent_mdp, scheduler, compatible_choices, discard_unreachable_choices=True): state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map) - parent_state_choice = self.empty_scheduler() + parent_state_choice = [-1] * self.quotient_mdp.nr_states states_affected = [False for state in range(self.quotient_mdp.nr_states)] parent_mdp = family.parent_info.mdp for state in range(parent_mdp.model.nr_states): @@ -144,7 +144,7 @@ def affected_to_choices(self, family, states_affected, parent_state_choice, comp parent_mdp = family.parent_info.mdp tm = parent_mdp.model.transition_matrix - qndi = self.quotient_mdp.nondeterministic_choice_indices.copy() + # qndi = self.quotient_mdp.nondeterministic_choice_indices.copy() ndi = parent_mdp.model.nondeterministic_choice_indices.copy() @@ -179,20 +179,29 @@ def affected_to_choices(self, family, states_affected, parent_state_choice, comp # affected_states.append( (state,qstate) ) - all_true = stormpy.BitVector(self.quotient_mdp.nr_choices, True) - for state,qstate in enumerate(parent_mdp.quotient_state_map): - if states_affected[qstate]: - continue - for choice in range(ndi[state],ndi[state+1]): - qchoice = parent_mdp.quotient_choice_map[choice] - all_true.set(qchoice, False) + # all_true = stormpy.BitVector(self.quotient_mdp.nr_choices, True) + # for state,qstate in enumerate(parent_mdp.quotient_state_map): + # if states_affected[qstate]: + # continue + # for choice in range(ndi[state],ndi[state+1]): + # qchoice = parent_mdp.quotient_choice_map[choice] + # all_true.set(qchoice, False) - parent_choice = parent_state_choice[qstate] - all_true.set(parent_choice, True) + # parent_choice = parent_state_choice[qstate] + # all_true.set(parent_choice, True) - return all_true & compatible_choices + # return all_true & compatible_choices ###################################### + + states_affected_to_vector = stormpy.BitVector(self.quotient_mdp.nr_states,False) + for state in range(self.quotient_mdp.nr_states): + if states_affected[state]: + states_affected_to_vector.set(state, True) + + # print(states_affected_to_vector) + # exit() + return payntbind.synthesis.affectedToChoices(parent_mdp.quotient_choice_map, parent_mdp.quotient_state_map, parent_mdp.model, states_affected_to_vector, ndi, parent_state_choice, compatible_choices) ###################################### diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index 79f73100f..7dd7b9898 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -209,6 +209,38 @@ storm::storage::BitVector policyToChoicesForFamily( return choices & family_choices; } +template +storm::storage::BitVector affectedToChoices( + std::vector quotient_choice_map, + std::vector quotient_state_map, + storm::models::sparse::Mdp const& quotient_mdp, + storm::storage::BitVector& states_affected, + std::vector const& row_groups, + std::vector& parent_state_choice, + storm::storage::BitVector& compatible_choices +) { + + uint64_t num_states = quotient_mdp.getNumberOfStates(); + auto const& nci = quotient_mdp.getNondeterministicChoiceIndices(); + storm::storage::BitVector all_true(compatible_choices.size(), true); + + for(uint64_t state=0; state,storm::storage::BitVector> fixPolicyForFamily( std::vector const& policy, uint64_t invalid_action, @@ -270,6 +302,8 @@ void bindings_coloring(py::module& m) { m.def("policyToChoicesForFamily", &synthesis::policyToChoicesForFamily); + m.def("affectedToChoices", &synthesis::affectedToChoices); + py::class_(m, "Family") .def(py::init<>(), "Constructor.") From e78c0e92d129340061dae7573d525152a567d33c Mon Sep 17 00:00:00 2001 From: Aleksandr Shevchenko Date: Tue, 7 May 2024 12:13:52 +0200 Subject: [PATCH 3/3] final version --- models/archive/cav23-saynt/lrv/sketch.props | 1 + models/archive/cav23-saynt/lrv/sketch.templ | 97 +++++ paynt/cli.py | 25 +- paynt/quotient/quotient.py | 352 +++++++----------- paynt/synthesizer/statistic.py | 20 +- paynt/synthesizer/synthesizer_ar.py | 24 +- payntbind/src/synthesis/quotient/bindings.cpp | 177 ++++++++- 7 files changed, 446 insertions(+), 250 deletions(-) create mode 100755 models/archive/cav23-saynt/lrv/sketch.props create mode 100755 models/archive/cav23-saynt/lrv/sketch.templ diff --git a/models/archive/cav23-saynt/lrv/sketch.props b/models/archive/cav23-saynt/lrv/sketch.props new file mode 100755 index 000000000..94d15c4de --- /dev/null +++ b/models/archive/cav23-saynt/lrv/sketch.props @@ -0,0 +1 @@ +R{"cost"}min=? [F "goal"]; \ No newline at end of file diff --git a/models/archive/cav23-saynt/lrv/sketch.templ b/models/archive/cav23-saynt/lrv/sketch.templ new file mode 100755 index 000000000..2d0f1ee2a --- /dev/null +++ b/models/archive/cav23-saynt/lrv/sketch.templ @@ -0,0 +1,97 @@ +pomdp + +observables +started, x, y, m1taken, m1lastobs, m2taken, m2lastobs, m3taken, m3lastobs, finish +endobservables + +const int N = 8; +const int xMx = N; +const int yMx = N; +const int xMIN = 0; +const int yMIN = 0; +const double slippery = 0.0; + +const m1x = N/2; +const m1y = N/2; + +const m2x = 1; +const m2y = 1; + +const m3x = 1; +const m3y = N; + + +const double goodmineral = 0.6; + +formula done = x = xMx & y = yMx; + +formula maxdist = xMx-xMIN+yMx-yMIN; + +formula m1dist = max(m1x-x,x-m1x) + max(m1y-y,y-m1y); +formula m2dist = max(m2x-x,x-m2x) + max(m2y-y,y-m2y); +formula m3dist = max(m3x-x,x-m3x) + max(m3y-y,y-m3y); + +formula normdistrm1 = 1+(m1dist/maxdist); +formula normdistrm2 = 1+(m2dist/maxdist); +formula normdistrm3 = 1+(m3dist/maxdist); + + +module master + started : bool init false; + finish : bool init false; + + [placement] !started -> (started'=true); + [north] started & !done -> true; + [south] started & !done -> true; + [east] started & !done-> true; + [west] started & !done -> true; + [finish] done & !finish -> 1:(finish'=true); +endmodule + +module mineral1 + m1qual : bool init false; + m1taken : bool init false; + m1lastobs : bool init false; + [placement] true -> goodmineral : (m1qual'=true) + (1-goodmineral) : (m1qual'=false); + + [m1collect] started & (x = m1x & y = m1y & !m1taken) -> 1:(m1taken'=true); + [m1sense] started & !m1taken -> (1/normdistrm1): (m1lastobs'=m1qual) + (1-(1/normdistrm1)): (m1lastobs'=!m1qual); + [north] true -> (m1lastobs'=false); + [south] true -> (m1lastobs'=false); + [east] true -> (m1lastobs'=false); + [west] true -> (m1lastobs'=false); +endmodule + +module mineral2 = mineral1[m1collect=m2collect, m1sense=m2sense, m1x = m2x, m1y = m2y, m1qual=m2qual,m1taken=m2taken,m1lastobs=m2lastobs,normdistrm1=normdistrm2] endmodule +module mineral3 = mineral1[m1collect=m3collect, m1sense=m3sense, m1x = m3x, m1y = m3y, m1qual=m3qual,m1taken=m3taken,m1lastobs=m3lastobs,normdistrm1=normdistrm3] endmodule + +module lrv + x : [xMIN..xMx] init 0; + y : [yMIN..yMx] init 0; + + [west] true -> (1-slippery): (x'=max(x-1,xMIN)) + slippery: (x'=max(x,xMIN)); + [east] true -> (1-slippery): (x'=min(x+1,xMx)) + slippery: (x'=min(x,xMx)); + [south] true -> (1-slippery): (y'=min(y+1,yMx)) + slippery: (y'=min(y,yMx)); + [north] true -> (1-slippery): (y'=max(y-1,yMIN)) + slippery: (y'=max(y,yMIN)); +endmodule + +rewards "cost" + [m1sense] true : 1; + [m2sense] true : 1; + [m3sense] true : 1; + + [m1collect] true : 2; + [m2collect] true : 2; + [m3collect] true : 2; + + [north] true : 1; + [south] true : 1; + [west] true : 1; + [east] true : 1; + [finish] true : (m1taken & !m1qual ? 4 : 0) + (m2taken & !m2qual ? 4 : 0) + + (m3taken & !m3qual ? 4 : 0) + + ((m1taken & m2taken & m1qual & m2qual) | (m1taken & m3taken & m1qual & m3qual) | + (m2taken & m3taken & m2qual & m3qual) ? 0 : 18); +endrewards + +label "goal" = finish; \ No newline at end of file diff --git a/paynt/cli.py b/paynt/cli.py index 1a420ce84..73ec87bee 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -1,3 +1,4 @@ +import paynt.synthesizer.synthesizer_ar from . import version import paynt.parser.sketch @@ -130,8 +131,17 @@ def setup_logger(log_path = None): @click.option( "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for cassandra models", ) + +#------------xshevc01---------------- @click.option("--use-inheritance", is_flag=True, default=False, - help="# if set, inheritance dependencies will be used for the synthesis of FSCs") + help="# if set, inheritance dependencies (IDAR) will be used for the synthesis of FSCs") +@click.option("--use-inheritance-extended", is_flag=True, default=False, + help="# if set, extended inheritance dependencies (EIDAR) will be used for the synthesis of FSCs") +@click.option("--use-smart-inheritance", is_flag=True, default=False, + help="# if set, combines classic AR with EIDAR (SEIDAR) for more efficient synthesis of FSCs") +@click.option("--iterations", default=0, show_default=True, + help=" experimental purposes: implicit number of iterations for the synthesis of FSCs") +#------------------------------------ @click.option( "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True, @@ -152,7 +162,12 @@ def paynt_run( all_in_one, mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction, constraint_bound, + #------------xshevc01---------------- use_inheritance, + use_inheritance_extended, + use_smart_inheritance, + iterations, + #------------------------------------ ce_generator, profiling ): @@ -174,7 +189,13 @@ def paynt_run( paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction - paynt.quotient.quotient.Quotient.use_inheritance_build = use_inheritance + #------------xshevc01---------------- + paynt.quotient.quotient.Quotient.use_inheritance = use_inheritance + paynt.quotient.quotient.Quotient.use_inheritance_extended = use_inheritance_extended + paynt.quotient.quotient.Quotient.use_smart_inheritance = use_smart_inheritance + paynt.synthesizer.synthesizer_ar.SynthesizerAR.iterations = iterations + #------------------------------------ + storm_control = None if storm_pomdp: diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index e3daaeca5..a7a00b07c 100644 --- a/paynt/quotient/quotient.py +++ b/paynt/quotient/quotient.py @@ -10,17 +10,17 @@ import logging logger = logging.getLogger(__name__) -# import inspect - -# def print_caller_info(): -# caller_frame = inspect.stack()[2] -# print(f"Called from file: {caller_frame.filename} at line: {caller_frame.lineno}") - class Quotient: # if True, hole scores in the state will be multiplied with the number of expected visits of this state compute_expected_visits = True + #------------xshevc01---------------- + use_inheritance = False + use_inheritance_extended = False + use_smart_inheritance = False + #------------------------------------ + @staticmethod def make_vector_defined(vector): @@ -88,187 +88,175 @@ def build_from_choice_mask(self, choice_mask): mdp = paynt.quotient.models.MDP(mdp, self, state_map, choice_map, None) return mdp + #------------xshevc01---------------- + def find_all_predecessors(self): + """ Find all predecessors for each state in the quotient MDP """ + self.predecessors_list = payntbind.synthesis.findAllPredecessors(self.quotient_mdp) + + + def idar_get_parents_scheduler(self, family, compatible_choices): + """ Use parent's scheduler to find the affected states """ + + parent_mdp = family.parent_info.mdp + parent_result = family.parent_info.analysis_result.optimality_result.primary.result + scheduler = parent_result.scheduler + return self.idar_get_parent_scheduler_choices(parent_mdp, scheduler, compatible_choices) - use_inheritance_build = False + def idar_get_parent_scheduler_choices(self, parent_mdp, scheduler, compatible_choices): + """ Get parent's optimal choices and if they are not + compatible with the family, mark the corresponding states as affected """ - def mine_scheduler_to_state_to_choice(self, family, parent_mdp, scheduler, compatible_choices, discard_unreachable_choices=True): state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map) parent_state_choice = [-1] * self.quotient_mdp.nr_states states_affected = [False for state in range(self.quotient_mdp.nr_states)] - parent_mdp = family.parent_info.mdp for state in range(parent_mdp.model.nr_states): qchoice = state_to_quotient_choice[state] qstate = parent_mdp.quotient_state_map[state] parent_state_choice[qstate] = qchoice - if not compatible_choices[qchoice]: + if not compatible_choices.get(qchoice): states_affected[qstate] = True - - if discard_unreachable_choices: - parent_state_choice = self.discard_unreachable_choices(parent_state_choice) return parent_state_choice, states_affected + - def find_all_predecessors(self, family): - predecessors = [set() for s in range(self.quotient_mdp.nr_states)] - tm = family.mdp.model.transition_matrix - for s in range(self.quotient_mdp.nr_states): - for choice in range(tm.get_row_group_start(s),tm.get_row_group_end(s)): - for entry in tm.get_row(choice): - predecessors[entry.column].add(s) - self.predecessors_list = predecessors + def find_reachable_affected_states(self, states_affected, parent_state_choice): + """ Mark all predecessors of affected states as affected """ - def get_parents_scheduler(self, family, compatible_choices): - parent_mdp = family.parent_info.mdp - parent_result = family.parent_info.analysis_result.optimality_result.primary.result - scheduler = parent_result.scheduler - return self.mine_scheduler_to_state_to_choice(family, parent_mdp, scheduler, compatible_choices, discard_unreachable_choices=False) - - def find_affected_reachable(self, states_affected): state_queue = [s for s in range(self.quotient_mdp.nr_states) if states_affected[s]] while state_queue: state = state_queue.pop() for pred in self.predecessors_list[state]: - if not states_affected[pred]: + qchoice = parent_state_choice[pred] + if not states_affected[pred] and qchoice != -1: state_queue.append(pred) states_affected[pred] = True - num_affected = sum(states_affected) - perc_affected = round(num_affected / self.quotient_mdp.nr_states * 100) - self.perc_affected_sum += perc_affected - self.perc_affected_entries += 1 - def affected_to_choices(self, family, states_affected, parent_state_choice, compatible_choices): - - parent_mdp = family.parent_info.mdp - tm = parent_mdp.model.transition_matrix - # qndi = self.quotient_mdp.nondeterministic_choice_indices.copy() - ndi = parent_mdp.model.nondeterministic_choice_indices.copy() - - - ###################################### WORKS - # for state in range(parent_mdp.model.nr_states): - # qstate = parent_mdp.quotient_state_map[state] - # if states_affected[qstate]: - # continue - # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): - # # print("hm") - # qchoice = parent_mdp.quotient_choice_map[choice] - # if not qchoice in parent_state_choice: - # compatible_choices.set(qchoice, False) - # # print("HAHA!") - - # return compatible_choices - ###################################### - - - ###################################### WORKS TOO - # qstate_compatible_choices = [] - # for qstate in range(self.quotient_mdp.nr_states): - # qstate_choices = [] - # for qchoice in range(qndi[qstate],qndi[qstate+1]): - # if compatible_choices[qchoice]: - # qstate_choices.append(qchoice) - # qstate_compatible_choices.append(qstate_choices) - - # affected_states = [] - # for state,qstate in enumerate(parent_mdp.quotient_state_map): - # if states_affected[qstate]: - # affected_states.append( (state,qstate) ) - - - # all_true = stormpy.BitVector(self.quotient_mdp.nr_choices, True) - # for state,qstate in enumerate(parent_mdp.quotient_state_map): - # if states_affected[qstate]: - # continue - # for choice in range(ndi[state],ndi[state+1]): - # qchoice = parent_mdp.quotient_choice_map[choice] - # all_true.set(qchoice, False) - - # parent_choice = parent_state_choice[qstate] - # all_true.set(parent_choice, True) - - # return all_true & compatible_choices - ###################################### + def convert_to_bitvector(self, states_affected): + """ Converts a list of affected states to a bit vector""" - states_affected_to_vector = stormpy.BitVector(self.quotient_mdp.nr_states,False) + states_affected_bit_vector = stormpy.BitVector(self.quotient_mdp.nr_states,False) for state in range(self.quotient_mdp.nr_states): if states_affected[state]: - states_affected_to_vector.set(state, True) + states_affected_bit_vector.set(state, True) + return states_affected_bit_vector + + + def affected_states_to_mask(self, family, states_affected_bit_vector, parent_state_choice, compatible_choices): + """ Compute the result choices for the family """ - # print(states_affected_to_vector) - # exit() + parent_mdp = family.parent_info.mdp + return payntbind.synthesis.affectedStatesToMask(parent_mdp.quotient_choice_map, parent_mdp.quotient_state_map, parent_mdp.model, states_affected_bit_vector, parent_state_choice, compatible_choices) - return payntbind.synthesis.affectedToChoices(parent_mdp.quotient_choice_map, parent_mdp.quotient_state_map, parent_mdp.model, states_affected_to_vector, ndi, parent_state_choice, compatible_choices) - ###################################### + def idar_build_inheritance(self, family, compatible_choices): + """ Construct the quotient MDP for the family using inheritance dependencies (IDAR) """ + + if family.parent_info is None: + self.perc_affected_sum = 0 + self.perc_affected_entries = 0 + self.choices_per_affected_sum = 0 + return compatible_choices + parent_state_choice, states_affected = self.idar_get_parents_scheduler(family, compatible_choices) + self.find_reachable_affected_states(states_affected, parent_state_choice) + states_affected_bit_vector = self.convert_to_bitvector(states_affected) + result_choices = self.affected_states_to_mask(family, states_affected_bit_vector, parent_state_choice, compatible_choices) + self.count_affected_states(states_affected_bit_vector, family, result_choices) + return result_choices + + + def map_choices_to_states(self): + """ Map choices to states in the quotient MDP (EIDAR) """ + + self.choices_to_states = payntbind.synthesis.mapChoicesToStates(self.quotient_mdp) + + + def eidar_get_parents_scheduler(self, family): + """ Use parent's scheduler to find the affected choices (EIDAR) """ + + parent_mdp = family.parent_info.mdp + parent_result = family.parent_info.analysis_result.optimality_result.primary.result + scheduler = parent_result.scheduler + return self.eidar_get_parent_scheduler_choices(parent_mdp, scheduler) + + def eidar_get_parent_scheduler_choices(self, parent_mdp, scheduler): + """ Get parent's optimal choices and if they are not + compatible with the family, mark the corresponding choices as affected (EIDAR) """ + + state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map) + parent_state_choice = [-1] * self.quotient_mdp.nr_states + optimal_choices = stormpy.BitVector(self.quotient_mdp.nr_choices, False) + for state in range(parent_mdp.model.nr_states): + qchoice = state_to_quotient_choice[state] + optimal_choices.set(qchoice, True) + qstate = parent_mdp.quotient_state_map[state] + parent_state_choice[qstate] = qchoice + return parent_state_choice, optimal_choices + + + def find_optimal_leading_choices(self, parent_state_choice): + """ Find the optimal leading choices (EIDAR) """ + + return payntbind.synthesis.findOptimalLeadingChoices(self.quotient_mdp, parent_state_choice) - ###################################### COULD WORK - # num_choices = self.quotient_mdp.nr_choices - # choices = stormpy.BitVector(num_choices,False) - # for state in range(parent_mdp.model.nr_states): - # qstate = parent_mdp.quotient_state_map[state] - # # if qstate == 159: - # # print("HEY", states_affected[qstate]) - # if states_affected[qstate]: - # # if qstate == 159: - # # print("EHM") - # # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): - # # qchoice = parent_mdp.quotient_choice_map[choice] - # # choices.set(qchoice, compatible_choices.get(qchoice)) - - - # at_least_one = False - # for choice in range(tm.get_row_group_start(state),tm.get_row_group_end(state)): - # qchoice = parent_mdp.quotient_choice_map[choice] - # choices.set(qchoice, compatible_choices.get(qchoice)) - # if choices.get(qchoice): - # at_least_one = True - # if not at_least_one: - # # print("WE WERE HERE") - # for choice in range(self.tm.get_row_group_start(qstate),self.tm.get_row_group_end(qstate)): - # # qchoice = parent_mdp.quotient_choice_map[choice] - # choices.set(choice, family.parent_info.selected_choices.get(choice)) - # else: - # qchoice = parent_state_choice[qstate] - # choices.set(qchoice, True) - - # return choices - ###################################### - - def build_inheritance(self, family, compatible_choices): + def optimal_choices_to_affected_states(self, optimal_choices, compatible_choices, leading_optimals_to_state): + """ Compute the affected states from the optimal choices (EIDAR) """ + + return payntbind.synthesis.optimalChoicesToAffectedStates(self.quotient_mdp, self.choices_to_states, optimal_choices, compatible_choices, leading_optimals_to_state) + + + def eidar_build_inheritance(self, family, compatible_choices): + """ Construct the quotient MDP for the family using extended inheritance dependencies (EIDAR)""" + if family.parent_info is None: self.perc_affected_sum = 0 self.perc_affected_entries = 0 + self.choices_per_affected_sum = 0 return compatible_choices - - num_choices = self.quotient_mdp.nr_choices - choices = stormpy.BitVector(num_choices,False) - parent_state_choice, states_affected = self.get_parents_scheduler(family, compatible_choices) - self.find_affected_reachable(states_affected) - choices = self.affected_to_choices(family, states_affected, parent_state_choice, compatible_choices) - return choices + parent_state_choice, optimal_choices = self.eidar_get_parents_scheduler(family) + leading_optimals_to_state = self.find_optimal_leading_choices(parent_state_choice) + affected_states = self.optimal_choices_to_affected_states(optimal_choices, compatible_choices, leading_optimals_to_state) + result_choices = self.affected_states_to_mask(family, affected_states, parent_state_choice, compatible_choices) + self.count_affected_states(affected_states, family, result_choices) + return result_choices + + + def count_affected_states(self, states_affected_bit_vector, family, choices): + """ Count statistics """ + + num_affected = states_affected_bit_vector.number_of_set_bits() + perc_affected = round(num_affected / family.parent_info.mdp.model.nr_states * 100) + choices_per_affected = (choices.number_of_set_bits() - family.parent_info.mdp.model.nr_states + num_affected) / num_affected + self.perc_affected_sum += perc_affected + self.perc_affected_entries += 1 + self.choices_per_affected_sum += choices_per_affected + def build(self, family): ''' Construct the quotient MDP for the family. ''' compatible_choices = self.coloring.selectCompatibleChoices(family.family) - if self.use_inheritance_build: - result_choices = self.build_inheritance(family, compatible_choices) + if self.use_inheritance: + result_choices = self.idar_build_inheritance(family, compatible_choices) + elif self.use_inheritance_extended or self.use_smart_inheritance: + result_choices = self.eidar_build_inheritance(family, compatible_choices) else: result_choices = compatible_choices - # print(len(self.coloring.selectCompatibleChoices(family.family)), self.coloring.selectCompatibleChoices(family.family).number_of_set_bits(), len(result_choices), result_choices.number_of_set_bits()) - # print("COLORING - CHOICES: ", set(self.coloring.selectCompatibleChoices(family.family)).difference(set(compatible_choices))) - # print("CHOICES - COLORING: ", set(compatible_choices).difference(set(self.coloring.selectCompatibleChoices(family.family)))) - + family.selected_choices = result_choices family.mdp = self.build_from_choice_mask(result_choices) - if self.use_inheritance_build and family.parent_info is None: - self.find_all_predecessors(family) - self.tm = family.mdp.model.transition_matrix + if self.use_inheritance and family.parent_info is None: + self.find_all_predecessors() + if (self.use_inheritance_extended or self.use_smart_inheritance) and family.parent_info is None: + self.map_choices_to_states() + if self.use_smart_inheritance and family.parent_info is None and math.log10(family.size) <= 15: + self.use_smart_inheritance = False + print("SWITCHING TO AR DUE TO THE SIZE OF THE FAMILY") family.mdp.design_space = family + #------------------------------------ def build_with_second_coloring(self, family, main_coloring, main_family): @@ -523,8 +511,6 @@ def discard(self, mdp, hole_assignments, core_suboptions, other_suboptions, inco def split(self, family, incomplete_search): - # if not self.use_inheritance_build: - # self.check_scheduler_inheritance(family) mdp = family.mdp assert not mdp.is_deterministic @@ -560,6 +546,7 @@ def split(self, family, incomplete_search): design_subspace.hole_set_options(splitter, suboption) design_subspaces.append(design_subspace) + # print(splitter, suboptions) return design_subspaces @@ -616,85 +603,6 @@ def sample(self): logger.info("done") - def check_scheduler_inheritance(self, family): - # print("VYZVALSYA CHECK SCHEDULER INHERITANCE") - # family --- DesignSpace! - - # if the family does not have a parent, then it is a super-family - # no need to check scheduler inheritance - if family.parent_info is None: - # print("SELECTED:", set(family.selected_choices)) - # print() - self.perc_affected_sum = 0 - self.perc_affected_entries = 0 - return - - # which choices were removed in the child family - choice_diff = set(family.parent_info.selected_choices).difference(set(family.selected_choices)) - # choice_diff = set(family.selected_choices).difference(set(family.selected_choices)) - # print("PARENT CHOICES: ", set(family.parent_info.selected_choices)) - # print() - # print("FAMILY CHOICES:", set(family.selected_choices)) - # print() - # print("CHOICE DIFF:", choice_diff) - # print() - - # get parent's scheduler for optimality - parent_mdp = family.parent_info.mdp - # parent_result = family.parent_info.analysis_result.optimality_result.primary.result - parent_result = family.parent_info.analysis_result.optimality_result.primary.result - assert not parent_result.scheduler.partial - - # get info from parent's scheduler - # print("NR STATES: ",self.quotient_mdp.nr_states) - # print() - parent_state_choice = [None for state in range(self.quotient_mdp.nr_states)] - for state in range(parent_mdp.states): - qstate = parent_mdp.quotient_state_map[state] - sched_choice = parent_result.scheduler.get_choice(state).get_deterministic_choice() - choice = parent_mdp.model.get_choice_index(state,sched_choice) - qchoice = parent_mdp.quotient_choice_map[choice] - parent_state_choice[qstate] = qchoice - # print("PARENT STATE CHOICE:", parent_state_choice) - # print(family) - # print(family.parent_info.splitter) # hole used for splitting - - # mark states in the sub-sub-MDP affected by the removal - state_affected = [False for state in range(family.mdp.states)] - for state in range(family.mdp.states): - qstate = family.mdp.quotient_state_map[state] - if parent_state_choice[qstate] in choice_diff: - state_affected[state] = True - - # for each state, a list of its predecessors - predecessors = [set() for s in range(family.mdp.states)] - tm = family.mdp.model.transition_matrix - for s in range(family.mdp.states): - for choice in range(tm.get_row_group_start(s),tm.get_row_group_end(s)): - for entry in tm.get_row(choice): - predecessors[entry.column].add(s) - - # find all states from which affected states are reachable - # queue of affected states - state_queue = [s for s in range(family.mdp.states) if state_affected[s]] - # print(tm) - while state_queue: - state = state_queue.pop() - # for each affected state, add its predecessors to the queue - for pred in predecessors[state]: - if not state_affected[pred]: - state_queue.append(pred) - state_affected[pred] = True - - # print("affected", state_affected[self.monitored_state]) - # print("parent has ", parent_result.at(self.monitored_state)) - - num_affected = len([x for x in state_affected if x]) - perc_affected = round(num_affected / family.mdp.states * 100) - self.perc_affected_sum += perc_affected - self.perc_affected_entries += 1 - # print("% affected states average: ", self.perc_affected_sum/self.perc_affected_entries) - def identify_absorbing_states(self, model): state_is_absorbing = [True] * model.nr_states tm = model.transition_matrix diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index a5bbe10a5..a7061860b 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -30,6 +30,9 @@ class Statistic: synthesis_timer_total = paynt.utils.profiler.Timer() def __init__(self, synthesizer): + #------------xshevc01---------------- + self.stop = False + #------------------------------------ self.synthesizer = synthesizer self.quotient = self.synthesizer.quotient @@ -86,7 +89,15 @@ def iteration_dtmc(self, size_dtmc): self.acc_size_dtmc += size_dtmc self.print_status() - def iteration_mdp(self, size_mdp): + def iteration_mdp(self, size_mdp, use_smart_inheritance): + #------------xshevc01---------------- + if use_smart_inheritance and not self.stop: + discarded = self.quotient.discarded + fraction_explored = (self.synthesizer.explored + discarded) / self.family_size + percentage_explored = int(fraction_explored * 100000) / 1000.0 + if percentage_explored > 20: + self.stop = True + #------------------------------------ if self.iterations_mdp is None: self.iterations_mdp = 0 self.iterations_mdp += 1 @@ -211,11 +222,12 @@ def get_summary_evaluation(self): members_sat_percentage = int(round(members_sat/members_total*100,0)) return f"satisfied {members_sat}/{members_total} members ({members_sat_percentage}%)" + #------------xshevc01---------------- def get_summary_affected(self): - if not self.quotient.use_inheritance_build or self.quotient.perc_affected_entries == 0: + if not self.quotient.use_inheritance and not self.quotient.use_inheritance_extended and not self.quotient.use_smart_inheritance or self.quotient.perc_affected_entries == 0: return "" - return f"\naffected states average: {self.quotient.perc_affected_sum/self.quotient.perc_affected_entries} %" - + return f"\n\naffected states average: {self.quotient.perc_affected_sum/self.quotient.perc_affected_entries:.2f} %\nchoices per affected state average: {self.quotient.choices_per_affected_sum/self.quotient.perc_affected_entries:.2f}" + #------------------------------------ def get_summary(self): specification = self.get_summary_specification() diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index 3315f294d..3e14165c1 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -6,6 +6,10 @@ class SynthesizerAR(paynt.synthesizer.synthesizer.Synthesizer): + #------------xshevc01---------------- + iterations = 0 + #------------------------------------ + @property def method_name(self): return "AR" @@ -13,7 +17,7 @@ def method_name(self): def verify_family(self, family): self.quotient.build(family) - self.stat.iteration_mdp(family.mdp.states) + self.stat.iteration_mdp(family.mdp.states, self.quotient.use_smart_inheritance) res = family.mdp.check_specification( self.quotient.specification, constraint_indices = family.constraint_indices, short_evaluation = True) if res.improving_assignment == "any": @@ -41,14 +45,24 @@ def synthesize_one(self, family): satisfying_assignment = None families = [family] - iteration_limit = 500 iteration_count = 0 while families: - + #------------xshevc01---------------- iteration_count += 1 - if iteration_count > iteration_limit: - break + if self.iterations != 0 and iteration_count > self.iterations: + break + + if self.quotient.use_smart_inheritance and (self.iterations != 0 and iteration_count > self.iterations / 5.0 or iteration_count > 100 or self.stat.stop): + self.quotient.use_smart_inheritance = False + affected_states_average = self.quotient.perc_affected_sum/self.quotient.perc_affected_entries + choices_per_affected_state = self.quotient.choices_per_affected_sum/self.quotient.perc_affected_entries + if affected_states_average > 85 or choices_per_affected_state < 5.5: + print("SWITCHING TO AR DUE TO AFFECTED STATES") + else: + self.quotient.use_inheritance_extended = True + print("SWITCHING TO EIDAR") + #------------------------------------ family = families.pop(-1) diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index 7dd7b9898..5b857823b 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -11,6 +11,8 @@ #include +#include + namespace synthesis { template @@ -209,38 +211,174 @@ storm::storage::BitVector policyToChoicesForFamily( return choices & family_choices; } + +//----------------xshevc01---------------- +/** + * Finds all predecessors of each state + * + * @param quotient_mdp The quotient MDP + * + * @return The predecessors of each state +*/ +template +std::vector> findAllPredecessors( + storm::models::sparse::Mdp const& quotient_mdp +){ + auto num_states = quotient_mdp.getNumberOfStates(); + auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices(); + std::vector> predecessors(num_states); + for(uint64_t state=0; state +std::vector mapChoicesToStates( + storm::models::sparse::Mdp const& quotient_mdp +){ + auto num_states = quotient_mdp.getNumberOfStates(); + auto num_choices = quotient_mdp.getNumberOfChoices(); + auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices(); + std::vector choices_to_states(num_choices); + std::vector> leading_choices(num_states); + for(uint64_t state=0; state -storm::storage::BitVector affectedToChoices( - std::vector quotient_choice_map, - std::vector quotient_state_map, +storm::storage::BitVector affectedStatesToMask( + std::vectorconst& quotient_choice_map, + std::vectorconst& quotient_state_map, storm::models::sparse::Mdp const& quotient_mdp, - storm::storage::BitVector& states_affected, - std::vector const& row_groups, + storm::storage::BitVector const& states_affected, std::vector& parent_state_choice, storm::storage::BitVector& compatible_choices ) { - + auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices(); uint64_t num_states = quotient_mdp.getNumberOfStates(); - auto const& nci = quotient_mdp.getNondeterministicChoiceIndices(); - storm::storage::BitVector all_true(compatible_choices.size(), true); - + storm::storage::BitVector mask(compatible_choices.size(), true); for(uint64_t state=0; state +std::vector> findOptimalLeadingChoices( + storm::models::sparse::Mdp const& quotient_mdp, + std::vector& parent_state_choice +){ + auto num_states = quotient_mdp.getNumberOfStates(); + auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices(); + std::vector> optimal_leading_choices(num_states); + for(uint64_t state=0; state +storm::storage::BitVector optimalChoicesToAffectedStates( + storm::models::sparse::Mdp const& quotient_mdp, + std::vector choices_to_states, + storm::storage::BitVector const& optimal_choices, + storm::storage::BitVector const& compatible_choices, + std::vector> leading_optimals_to_state +) { + uint64_t num_states = quotient_mdp.getNumberOfStates(); + uint64_t num_choices = quotient_mdp.getNumberOfChoices(); + storm::storage::BitVector affected_states(num_states, false); + storm::storage::BitVector was_in_queue(num_choices, false); + std::queue queue_affected_choices; + + for(uint64_t choice=0; choice,storm::storage::BitVector> fixPolicyForFamily( std::vector const& policy, uint64_t invalid_action, @@ -296,14 +434,19 @@ void bindings_coloring(py::module& m) { m.def("addChoiceLabelsFromJani", &synthesis::addChoiceLabelsFromJani); m.def("computeChoiceDestinations", &synthesis::computeChoiceDestinations); - + //----------------xshevc01---------------- + m.def("findAllPredecessors", &synthesis::findAllPredecessors); + m.def("mapChoicesToStates", &synthesis::mapChoicesToStates); + m.def("affectedStatesToMask", &synthesis::affectedStatesToMask); + m.def("findOptimalLeadingChoices", &synthesis::findOptimalLeadingChoices); + m.def("optimalChoicesToAffectedStates", &synthesis::optimalChoicesToAffectedStates); + //--------------------------------------- m.def("schedulerToStateToGlobalChoice", &synthesis::schedulerToStateToGlobalChoice); m.def("computeInconsistentHoleVariance", &synthesis::computeInconsistentHoleVariance); m.def("policyToChoicesForFamily", &synthesis::policyToChoicesForFamily); - m.def("affectedToChoices", &synthesis::affectedToChoices); - + py::class_(m, "Family") .def(py::init<>(), "Constructor.")