From 650bd6b46c3bc47c48e5d16acf288a11d5a3c6cf Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Wed, 4 Sep 2024 10:48:28 +0200 Subject: [PATCH] inconsistency for decision tree templates via SMT --- paynt/cli.py | 9 +- paynt/family/family.py | 85 ++--- paynt/models/models.py | 19 + paynt/parser/jani.py | 2 +- paynt/parser/sketch.py | 2 +- paynt/quotient/decpomdp.py | 12 +- paynt/quotient/mdp.py | 176 ++++----- paynt/quotient/mdp_family.py | 2 - paynt/quotient/pomdp.py | 17 +- paynt/quotient/pomdp_family.py | 4 +- paynt/quotient/posg.py | 1 - paynt/quotient/quotient.py | 162 ++------ paynt/synthesizer/conflict_generator/dtmc.py | 5 +- paynt/synthesizer/conflict_generator/mdp.py | 5 +- paynt/synthesizer/decision_tree.py | 143 ++++++- paynt/synthesizer/policy_tree.py | 7 +- paynt/synthesizer/statistic.py | 20 +- paynt/synthesizer/synthesizer.py | 42 +- paynt/synthesizer/synthesizer_ar.py | 150 ++++---- paynt/synthesizer/synthesizer_ar_storm.py | 24 +- paynt/synthesizer/synthesizer_cegis.py | 17 +- paynt/synthesizer/synthesizer_decpomdp.py | 4 +- paynt/synthesizer/synthesizer_hybrid.py | 11 +- paynt/synthesizer/synthesizer_multicore_ar.py | 6 +- paynt/synthesizer/synthesizer_onebyone.py | 7 +- paynt/synthesizer/synthesizer_pomdp.py | 224 +---------- paynt/utils/graphs.py | 16 +- paynt/utils/profiler.py | 16 + paynt/verification/property.py | 4 +- paynt/verification/property_result.py | 46 +-- .../src/synthesis/quotient/ColoringSmt.cpp | 338 +++++++++++++---- .../src/synthesis/quotient/ColoringSmt.h | 20 +- payntbind/src/synthesis/quotient/TreeNode.cpp | 359 ++++++++---------- payntbind/src/synthesis/quotient/TreeNode.h | 104 +++-- payntbind/src/synthesis/quotient/bindings.cpp | 5 +- .../translation/choiceTransformation.cpp | 6 +- 36 files changed, 985 insertions(+), 1085 deletions(-) diff --git a/paynt/cli.py b/paynt/cli.py index f5cd7d3f1..12d330f15 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -1,5 +1,6 @@ from . import version +import paynt.utils.profiler import paynt.parser.sketch import paynt.quotient @@ -59,6 +60,8 @@ def setup_logger(log_path = None): help="known optimum bound") @click.option("--precision", type=click.FLOAT, default=1e-4, help="model checking precision") +@click.option("--timeout", type=int, + help="timeout (s)") @click.option("--export", type=click.Choice(['jani', 'drn', 'pomdp']), @@ -132,7 +135,7 @@ def setup_logger(log_path = None): help="decision tree synthesis: if set, all trees of size at most tree_depth will be enumerated") @click.option( - "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for cassandra models", + "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for Cassandra models", ) @click.option( @@ -143,7 +146,7 @@ def setup_logger(log_path = None): help="run profiling") def paynt_run( - project, sketch, props, relative_error, optimum_threshold, precision, + project, sketch, props, relative_error, optimum_threshold, precision, timeout, export, method, disable_expected_visits, @@ -158,10 +161,12 @@ def paynt_run( ce_generator, profiling ): + profiler = None if profiling: profiler = cProfile.Profile() profiler.enable() + paynt.utils.profiler.GlobalTimeoutTimer.start(timeout) logger.info("This is Paynt version {}.".format(version())) diff --git a/paynt/family/family.py b/paynt/family/family.py index 0d7ee9501..6d2742465 100644 --- a/paynt/family/family.py +++ b/paynt/family/family.py @@ -10,6 +10,21 @@ logger = logging.getLogger(__name__) +class ParentInfo(): + ''' + Container for stuff to be remembered when splitting an undecided family into subfamilies. Generally used to + speed-up work with the subfamilies. + :note it is better to store these things in a separate container instead + of having a reference to the parent family (that will never be considered again) for memory efficiency. + ''' + def __init__(self): + pass + self.selected_choices = None + self.constraint_indices = None + self.refinement_depth = None + self.splitter = None + + class Family: def __init__(self, other=None): @@ -22,6 +37,21 @@ def __init__(self, other=None): self.hole_to_name = other.hole_to_name self.hole_to_option_labels = other.hole_to_option_labels + self.parent_info = None + self.refinement_depth = 0 + self.constraint_indices = None + + self.selected_choices = None + self.mdp = None + self.analysis_result = None + self.splitter = None + self.encoding = None + + def add_parent_info(self, parent_info): + self.parent_info = parent_info + self.refinement_depth = parent_info.refinement_depth + 1 + self.constraint_indices = parent_info.constraint_indices + @property def num_holes(self): return self.family.numHoles() @@ -121,61 +151,6 @@ def subholes(self, hole_index, options): shallow_copy.hole_set_options(hole_index,options) return shallow_copy - - -class ParentInfo(): - ''' - Container for stuff to be remembered when splitting an undecided family - into subfamilies. Generally used to speed-up work with the subfamilies. - :note it is better to store these things in a separate container instead - of having a reference to the parent family (that will never be considered - again) for the purposes of memory efficiency. - ''' - def __init__(self): - # list of constraint indices still undecided in this family - self.constraint_indices = None - - # how many refinements were needed to create this family - self.refinement_depth = None - - # index of a hole used to split the family - self.splitter = None - - -class DesignSpace(Family): - ''' - List of holes supplied with - - a list of constraint indices to investigate in this design space - - (optionally) z3 encoding of this design space - :note z3 (re-)encoding construction must be invoked manually - ''' - - # whether hints will be stored for subsequent MDP model checking - store_hints = True - - def __init__(self, family = None, parent_info = None): - super().__init__(family) - - self.mdp = None - self.selected_choices = None - - # SMT encoding - self.encoding = None - - self.refinement_depth = 0 - self.constraint_indices = None - - self.analysis_result = None - self.splitter = None - self.parent_info = parent_info - if parent_info is not None: - self.refinement_depth = parent_info.refinement_depth + 1 - self.constraint_indices = parent_info.constraint_indices - - def copy(self): - return DesignSpace(super().copy()) - - def collect_parent_info(self, specification): pi = ParentInfo() pi.selected_choices = self.selected_choices diff --git a/paynt/models/models.py b/paynt/models/models.py index 5895687e0..85c37778b 100644 --- a/paynt/models/models.py +++ b/paynt/models/models.py @@ -37,6 +37,25 @@ def model_check_property(self, prop, alt=False): value = result.at(self.initial_state) return paynt.verification.property_result.PropertyResult(prop, result, value) + def check_specification(self, spec, constraint_indices=None, short_evaluation=False): + ''' Assuming this is a DTMC. ''' + if constraint_indices is None: + constraint_indices = spec.all_constraint_indices() + results = [None for _ in spec.constraints] + for index in constraint_indices: + result = self.model_check_property(spec.constraints[index]) + results[index] = result + if short_evaluation and result.sat is False: + break + spec_result = paynt.verification.property_result.SpecificationResult() + spec_result.constraints_result = paynt.verification.property_result.ConstraintsResult(results) + + if spec.has_optimality and not (short_evaluation and spec_result.constraints_result.sat is False): + spec_result.optimality_result = self.model_check_property(spec.optimality) + return spec_result + + + class SubMdp(Mdp): def __init__(self, model, quotient_state_map, quotient_choice_map): diff --git a/paynt/parser/jani.py b/paynt/parser/jani.py index 86cd8600d..4b2aa244d 100644 --- a/paynt/parser/jani.py +++ b/paynt/parser/jani.py @@ -216,7 +216,7 @@ def construct_edge(self, edge, substitution = None): for templ_edge_dest in edge.template_edge.destinations: assignments = templ_edge_dest.assignments.clone() if substitution is not None: - assignments.substitute(substitution,substitute_transcendental_numbers=False) + assignments.substitute(substitution) templ_edge.add_destination(stormpy.storage.JaniTemplateEdgeDestination(assignments)) new_edge = stormpy.storage.JaniEdge( diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index cc9b10ad4..685d519d0 100644 --- a/paynt/parser/sketch.py +++ b/paynt/parser/sketch.py @@ -223,7 +223,7 @@ def export(cls, export, sketch_path, jani_unfolder, explicit_quotient): def build_quotient_container(cls, prism, jani_unfolder, explicit_quotient, family, coloring, specification, obs_evaluator, decpomdp_manager): if jani_unfolder is not None: if prism.model_type == stormpy.storage.PrismModelType.DTMC: - quotient_container = paynt.quotient.quotient.DtmcFamilyQuotient(explicit_quotient, family, coloring, specification) + quotient_container = paynt.quotient.quotient.Quotient(explicit_quotient, family, coloring, specification) elif prism.model_type == stormpy.storage.PrismModelType.MDP: quotient_container = paynt.quotient.mdp_family.MdpFamilyQuotient(explicit_quotient, family, coloring, specification) elif prism.model_type == stormpy.storage.PrismModelType.POMDP: diff --git a/paynt/quotient/decpomdp.py b/paynt/quotient/decpomdp.py index 33db23744..0c5b52e49 100644 --- a/paynt/quotient/decpomdp.py +++ b/paynt/quotient/decpomdp.py @@ -105,20 +105,18 @@ def unfold_memory(self): self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp) logger.debug(f"constructed quotient MDP having {self.quotient_mdp.nr_states} states and {self.quotient_mdp.nr_choices} actions.") - family, choice_to_hole_options = self.create_coloring() + self.family, choice_to_hole_options = self.create_coloring() - self.coloring = payntbind.synthesis.Coloring(family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options) + self.coloring = payntbind.synthesis.Coloring(self.family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options) # to each hole-option pair a list of actions colored by this combination - self.hole_option_to_actions = [[] for hole in range(family.num_holes)] - for hole in range(family.num_holes): - self.hole_option_to_actions[hole] = [[] for option in family.hole_options(hole)] + self.hole_option_to_actions = [[] for hole in range(self.family.num_holes)] + for hole in range(self.family.num_holes): + self.hole_option_to_actions[hole] = [[] for option in self.family.hole_options(hole)] for choice in range(self.quotient_mdp.nr_choices): for hole,option in choice_to_hole_options[choice]: self.hole_option_to_actions[hole][option].append(choice) - self.design_space = paynt.family.family.DesignSpace(family) - def create_coloring(self): # short aliases diff --git a/paynt/quotient/mdp.py b/paynt/quotient/mdp.py index cc6530213..c002b2c57 100644 --- a/paynt/quotient/mdp.py +++ b/paynt/quotient/mdp.py @@ -10,14 +10,11 @@ class Variable: - def __init__(self, name, model): + def __init__(self, variable, name, state_valuations): self.name = name - - assert model.has_state_valuations(), "model has no state valuations" domain = set() - for state in range(model.nr_states): - valuation = json.loads(str(model.state_valuations.get_json(state))) - value = valuation[name] + for state,valuation in enumerate(state_valuations): + value = valuation[variable] domain.add(value) domain = list(domain) # conversion of boolean variables to integers @@ -56,7 +53,13 @@ def __str__(self): def from_model(cls, model): assert model.has_state_valuations(), "model has no state valuations" valuation = json.loads(str(model.state_valuations.get_json(0))) - variables = [Variable(var,model) for var in valuation] + variable_name = [var_name for var_name in valuation] + state_valuations = [] + for state in range(model.nr_states): + valuation = json.loads(str(model.state_valuations.get_json(state))) + valuation = [valuation[var_name] for var_name in variable_name] + state_valuations.append(valuation) + variables = [Variable(var,var_name,state_valuations) for var,var_name in enumerate(variable_name)] variables = [v for v in variables if len(v.domain) > 1] return variables @@ -74,7 +77,7 @@ def __init__(self, parent): @property def is_terminal(self): - return self.variable_index is None + return self.child_false is None and self.child_true is None @property def child_nodes(self): @@ -84,20 +87,15 @@ def child_nodes(self): def is_true_child(self): return self is self.parent.child_true - def set_variable(self, variable_index:int): + def add_decision(self): ''' Associate (an index of) a variable with the node. ''' if self.is_terminal: self.child_false = DecisionTreeNode(self) self.child_true = DecisionTreeNode(self) - self.variable_index = variable_index - def set_variable_by_name(self, variable_name:str, decision_tree): - variable_index = [variable.name for variable in decision_tree.variables].index(variable_name) - self.set_variable(variable_index) - - def assign_identifiers(self, identifier): + def assign_identifiers(self, identifier=0): self.identifier = identifier if self.is_terminal: return self.identifier @@ -120,7 +118,7 @@ def set_depth(self, depth:int): self.reset() for level in range(depth): for node in self.collect_terminals(): - node.set_variable(0) + node.add_decision() def collect_nodes(self, node_condition=None): if node_condition is None: @@ -135,15 +133,13 @@ def collect_nodes(self, node_condition=None): return output_nodes def collect_terminals(self): - node_condition = lambda node : node.is_terminal - return self.collect_nodes(node_condition) + return self.collect_nodes(lambda node : node.is_terminal) def collect_nonterminals(self): - node_condition = lambda node : not node.is_terminal - return self.collect_nodes(node_condition) + return self.collect_nodes(lambda node : not node.is_terminal) def to_list(self): - self.root.assign_identifiers(0) + self.root.assign_identifiers() num_nodes = len(self.collect_nodes()) node_info = [ None for node in range(num_nodes) ] for node in self.collect_nodes(): @@ -162,7 +158,6 @@ def collect_variables(self): node_to_variable[node.identifier] = node.variable_index return node_to_variable - class MdpQuotient(paynt.quotient.quotient.Quotient): def __init__(self, mdp, specification): @@ -175,9 +170,7 @@ def __init__(self, mdp, specification): self.decision_tree = DecisionTree(mdp) self.coloring = None - self.design_space = None - - self.is_action_hole = None + self.family = None def decide(self, node, var_name): node.set_variable_by_name(var_name,self.decision_tree) @@ -185,26 +178,19 @@ def decide(self, node, var_name): ''' Build the design space and coloring corresponding to the current decision tree. ''' - def build_coloring(self, use_generic_template=True): + def build_coloring(self): # logger.debug("building coloring...") variables = self.decision_tree.variables variable_name = [v.name for v in variables] variable_domain = [v.domain for v in variables] tree_list = self.decision_tree.to_list() - - node_to_variable = [] - if not use_generic_template: - node_to_variable = self.decision_tree.collect_variables() - self.coloring = payntbind.synthesis.ColoringSmt( - self.quotient_mdp, variable_name, variable_domain, tree_list, node_to_variable - ) + self.coloring = payntbind.synthesis.ColoringSmt(self.quotient_mdp, variable_name, variable_domain, tree_list) # reconstruct the family hole_info = self.coloring.getFamilyInfo() - family = paynt.family.family.Family() + self.family = paynt.family.family.Family() self.is_action_hole = [False for hole in hole_info] self.is_decision_hole = [False for hole in hole_info] - self.is_bound_hole = [False for hole in hole_info] self.is_variable_hole = [False for hole in hole_info] domain_max = max([len(domain) for domain in variable_domain]) bound_domain = list(range(domain_max)) @@ -223,21 +209,23 @@ def build_coloring(self, use_generic_template=True): self.is_variable_hole[hole] = True variable = variable_name.index(hole_type) option_labels = variables[variable].hole_domain - family.add_hole(hole_name, option_labels) - self.design_space = paynt.family.family.DesignSpace(family) + self.family.add_hole(hole_name, option_labels) + def build_unsat_result(self): - constraints_result = paynt.verification.property_result.ConstraintsResult([]) - optimality_result = paynt.verification.property_result.MdpOptimalityResult(None) - optimality_result.can_improve = False - analysis_result = paynt.verification.property_result.MdpSpecificationResult(constraints_result,optimality_result) - return analysis_result + spec_result = paynt.verification.property_result.MdpSpecificationResult() + spec_result.constraints_result = paynt.verification.property_result.ConstraintsResult([]) + spec_result.optimality_result = paynt.verification.property_result.MdpOptimalityResult(None) + spec_result.evaluate(None) + spec_result.can_improve = False + return spec_result def build(self, family): # logger.debug("building sub-MDP...") # print("\nfamily = ", family, flush=True) # family.parent_info = None + if family.parent_info is None: choices = self.coloring.selectCompatibleChoices(family.family) else: @@ -250,8 +238,17 @@ def build(self, family): # proceed as before family.selected_choices = choices family.mdp = self.build_from_choice_mask(choices) - family.mdp.design_space = family + family.mdp.family = family + + def are_choices_consistent(self, choices, family): + ''' Separate method for profiling purposes. ''' + # print(self.family) + # print(family) + # for hole in range(family.num_holes): + # print(f"{family.hole_name(hole)} = {family.hole_options(hole)}") + return self.coloring.areChoicesConsistent(choices, family.family) + return self.coloring.areChoicesConsistent2(choices, family.family) def scheduler_is_consistent(self, mdp, prop, result): ''' Get hole options involved in the scheduler selection. ''' @@ -260,57 +257,29 @@ def scheduler_is_consistent(self, mdp, prop, result): assert scheduler.memoryless and scheduler.deterministic state_to_choice = self.scheduler_to_state_to_choice(mdp, scheduler) choices = self.state_to_choice_to_choices(state_to_choice) - consistent,hole_selection = self.coloring.areChoicesConsistent(choices, mdp.design_space.family) + if self.specification.is_single_property: + mdp.family.scheduler_choices = choices + consistent,hole_selection = self.are_choices_consistent(choices, mdp.family) + # print(mdp.family) # print(consistent,hole_selection) - # threshold hack - # import math - # choice_values = self.choice_values(mdp.model, self.get_property(), result.get_values()) - # ndi = mdp.model.nondeterministic_choice_indices - # state_relevant = [False] * self.quotient_mdp.nr_states - # state_diff = [] - # for state in range(mdp.model.nr_states): - # state_min = state_max = choice_values[ndi[state]] - # for choice in range(ndi[state]+1,ndi[state+1]): - # if choice_values[choice] < state_min: - # state_min = choice_values[choice] - # if choice_values[choice] > state_max: - # state_max = choice_values[choice] - # divisor = None - # max_diff = state_max-state_min - # if math.fabs(state_min) > 0.001: - # state_diff = math.fabs(max_diff/state_min) - # elif math.fabs(state_max) > 0.001: - # state_diff = math.fabs(max_diff/state_max) - # else: - # state_diff = 0 - # if state_diff > 0: - # state_relevant[mdp.quotient_state_map[state]] = True - # consistent,hole_selection = self.coloring.areChoicesConsistentRelevant(choices, mdp.design_space.family, state_relevant) + # if not consistent: + # inconsistent_assignments = {hole:options for hole,options in enumerate(hole_selection) if len(options) > 1 } + # assert len(inconsistent_assignments) > 0, f"obtained selection with no inconsistencies: {hole_selection}" for hole,options in enumerate(hole_selection): for option in options: - assert option in mdp.design_space.hole_options(hole), \ - f"option {option} for hole {hole} ({mdp.design_space.hole_name(hole)}) is not in the family" + assert option in mdp.family.hole_options(hole), \ + f"option {option} for hole {hole} ({mdp.family.hole_name(hole)}) is not in the family" return hole_selection, consistent - def scheduler_get_quantitative_values(self, mdp, prop, result, selection): - ''' - :return choice values - :return expected visits - :return hole scores - ''' - # return None,None,None - + def scheduler_scores(self, mdp, prop, result, selection): inconsistent_assignments = {hole:options for hole,options in enumerate(selection) if len(options) > 1 } - if len(inconsistent_assignments) == 0: - assert False, f"obtained selection with no inconsistencies: {selection}" - inconsistent_assignments = {hole:options for hole,options in enumerate(selection) if len(options) > 0 } + assert len(inconsistent_assignments) > 0, f"obtained selection with no inconsistencies: {selection}" inconsistent_action_holes = [(hole,options) for hole,options in inconsistent_assignments.items() if self.is_action_hole[hole]] inconsistent_decision_holes = [(hole,options) for hole,options in inconsistent_assignments.items() if self.is_decision_hole[hole]] - inconsistent_bound_holes = [(hole,options) for hole,options in inconsistent_assignments.items() if self.is_bound_hole[hole]] inconsistent_variable_holes = [(hole,options) for hole,options in inconsistent_assignments.items() if self.is_variable_hole[hole]] # choose one splitter and force its score @@ -321,15 +290,11 @@ def scheduler_get_quantitative_values(self, mdp, prop, result, selection): splitter = inconsistent_action_holes[0][0] elif len(inconsistent_decision_holes) > 0: splitter = inconsistent_decision_holes[0][0] - elif len(inconsistent_bound_holes) > 0: - splitter = inconsistent_bound_holes[0][0] else: - splitter,options = inconsistent_variable_holes[0] - # selection[splitter] = [options[0]] + splitter = inconsistent_variable_holes[0][0] assert splitter is not None, "splitter not set" + return {splitter:10} - inconsistent_differences = {splitter:10} - return None, None, inconsistent_differences def split(self, family): @@ -339,7 +304,7 @@ def split(self, family): # split family wrt last undecided result result = family.analysis_result.undecided_result() hole_assignments = result.primary_selection - scores = result.primary_scores + scores = self.scheduler_scores(mdp, result.prop, result.primary.result, result.primary_selection) splitters = self.holes_with_max_score(scores) splitter = splitters[0] @@ -347,27 +312,38 @@ def split(self, family): assert len(hole_assignments[splitter]) > 1 core_suboptions,other_suboptions = self.suboptions_enumerate(mdp, splitter, hole_assignments[splitter]) else: - # split in half subfamily_options = family.hole_options(splitter) - index_half = len(subfamily_options)//2 - core_suboptions = [subfamily_options[:index_half], subfamily_options[index_half:]] + + # split in half + index_split = len(subfamily_options)//2 + + assert len(hole_assignments[splitter]) == 2, "when does this not hold?" + option_1 = hole_assignments[splitter][0] + option_2 = hole_assignments[splitter][1] + index_split = subfamily_options.index(option_2) + # index_split = subfamily_options.index(option_1)+1 + + core_suboptions = [subfamily_options[:index_split], subfamily_options[index_split:]] + for options in core_suboptions: assert len(options) > 0 other_suboptions = [] - new_design_space = mdp.design_space.copy() + new_family = mdp.family.copy() if len(other_suboptions) == 0: suboptions = core_suboptions else: suboptions = [other_suboptions] + core_suboptions # DFS solves core first - # construct corresponding design subspaces - design_subspaces = [] + # construct corresponding subfamilies + subfamilies = [] family.splitter = splitter parent_info = family.collect_parent_info(self.specification) + parent_info.analysis_result = family.analysis_result + parent_info.scheduler_choices = family.scheduler_choices for suboption in suboptions: - subholes = new_design_space.subholes(splitter, suboption) - design_subspace = paynt.family.family.DesignSpace(subholes, parent_info) - design_subspace.hole_set_options(splitter, suboption) - design_subspaces.append(design_subspace) + subfamily = new_family.subholes(splitter, suboption) + subfamily.add_parent_info(parent_info) + subfamily.hole_set_options(splitter, suboption) + subfamilies.append(subfamily) - return design_subspaces + return subfamilies diff --git a/paynt/quotient/mdp_family.py b/paynt/quotient/mdp_family.py index 37789aa71..497921045 100644 --- a/paynt/quotient/mdp_family.py +++ b/paynt/quotient/mdp_family.py @@ -40,8 +40,6 @@ def map_state_to_available_actions(state_action_choices): def __init__(self, quotient_mdp, family, coloring, specification): super().__init__(quotient_mdp = quotient_mdp, family = family, coloring = coloring, specification = specification) - self.design_space = paynt.family.family.DesignSpace(self.family) - # number of distinct actions in the quotient self.num_actions = None # a list of action labels diff --git a/paynt/quotient/pomdp.py b/paynt/quotient/pomdp.py index 614b234e5..17388720a 100644 --- a/paynt/quotient/pomdp.py +++ b/paynt/quotient/pomdp.py @@ -30,7 +30,7 @@ def __init__(self, pomdp, specification, decpomdp_manager=None): # unfolded POMDP self.quotient_mdp = None - self.design_space = None + self.family = None self.coloring = None # to each hole-option pair a list of actions colored by this combination (reverse coloring) self.hole_option_to_actions = None @@ -342,21 +342,18 @@ def unfold_memory(self): self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp) logger.debug(f"constructed quotient MDP having {self.quotient_mdp.nr_states} states and {self.quotient_mdp.nr_choices} actions.") - family, choice_to_hole_options = self.create_coloring() + self.family, choice_to_hole_options = self.create_coloring() - self.coloring = payntbind.synthesis.Coloring(family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options) + self.coloring = payntbind.synthesis.Coloring(self.family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options) # to each hole-option pair a list of actions colored by this combination - self.hole_option_to_actions = [[] for hole in range(family.num_holes)] - for hole in range(family.num_holes): - self.hole_option_to_actions[hole] = [[] for option in family.hole_options(hole)] + self.hole_option_to_actions = [[] for hole in range(self.family.num_holes)] + for hole in range(self.family.num_holes): + self.hole_option_to_actions[hole] = [[] for option in self.family.hole_options(hole)] for choice in range(self.quotient_mdp.nr_choices): for hole,option in choice_to_hole_options[choice]: self.hole_option_to_actions[hole][option].append(choice) - self.design_space = paynt.family.family.DesignSpace(family) - - def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_assignments, choice_values, expected_visits): @@ -598,7 +595,7 @@ def export_policy(self, dtmc, mc_result): def extract_policy(self, assignment): dtmc = self.build_assignment(assignment) - mc_result = self.check_specification_for_dtmc(dtmc) + mc_result = dtmc.check_specification(self.specification) policy = self.collect_policy(dtmc, mc_result) return policy diff --git a/paynt/quotient/pomdp_family.py b/paynt/quotient/pomdp_family.py index 289b21b53..6d5b01793 100644 --- a/paynt/quotient/pomdp_family.py +++ b/paynt/quotient/pomdp_family.py @@ -105,7 +105,7 @@ def build_dtmc_sketch(self, fsc): product_choice_to_choice = self.product_pomdp_fsc.product_choice_to_choice # the product inherits the design space - product_family = self.design_space.copy() + product_family = self.family.copy() # the choices of the product inherit colors of the quotient product_choice_to_hole_options = [] @@ -122,7 +122,7 @@ def build_dtmc_sketch(self, fsc): # handle specification product_specification = self.specification.copy() - dtmc_sketch = paynt.quotient.quotient.DtmcFamilyQuotient(product, product_family, product_coloring, product_specification) + dtmc_sketch = paynt.quotient.quotient.Quotient(product, product_family, product_coloring, product_specification) return dtmc_sketch diff --git a/paynt/quotient/posg.py b/paynt/quotient/posg.py index 920e0ab12..e101bc3a7 100644 --- a/paynt/quotient/posg.py +++ b/paynt/quotient/posg.py @@ -22,7 +22,6 @@ def __init__(self, quotient_mdp, specification): # TODO Antonin self.coloring = None self.family = None - self.design_space = None pomdp = self.quotient_mdp print(type(pomdp), dir(pomdp)) diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index f2d2ec83c..5a784f781 100644 --- a/paynt/quotient/quotient.py +++ b/paynt/quotient/quotient.py @@ -78,7 +78,7 @@ def build(self, family): choices = self.coloring.selectCompatibleChoices(family.family) family.mdp = self.build_from_choice_mask(choices) family.selected_choices = choices - family.mdp.design_space = family + family.mdp.family = family @staticmethod @@ -201,7 +201,7 @@ def compute_expected_visits(self, mdp, prop, choices): def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_assignments, choice_values, expected_visits): hole_variance = payntbind.synthesis.computeInconsistentHoleVariance( - self.design_space.family, mdp.nondeterministic_choice_indices, quotient_choice_map, choice_values, + self.family.family, mdp.nondeterministic_choice_indices, quotient_choice_map, choice_values, self.coloring, inconsistent_assignments, expected_visits) return hole_variance @@ -214,7 +214,7 @@ def scheduler_is_consistent(self, mdp, prop, result): :return whether the scheduler is consistent ''' if mdp.is_deterministic: - selection = [[mdp.design_space.hole_options(hole)[0]] for hole in range(mdp.design_space.num_holes)] + selection = [[mdp.family.hole_options(hole)[0]] for hole in range(mdp.family.num_holes)] return selection, True # get qualitative scheduler selection, filter inconsistent assignments @@ -224,27 +224,22 @@ def scheduler_is_consistent(self, mdp, prop, result): for hole,options in enumerate(selection): if len(options) == 0: # if some hole options are not involved in the selection, we can fix an arbitrary value - selection[hole] = [mdp.design_space.hole_options(hole)[0]] + selection[hole] = [mdp.family.hole_options(hole)[0]] return selection, scheduler_is_consistent - def scheduler_get_quantitative_values(self, mdp, prop, result, selection): - ''' - :return choice values - :return expected visits - :return hole scores - ''' + def scheduler_scores(self, mdp, prop, result, selection): inconsistent_assignments = {hole:options for hole,options in enumerate(selection) if len(options) > 1 } choice_values = self.choice_values(mdp.model, prop, result.get_values()) choices = result.scheduler.compute_action_support(mdp.model.nondeterministic_choice_indices) expected_visits = self.compute_expected_visits(mdp.model, prop, choices) - inconsistent_differences = self.estimate_scheduler_difference(mdp.model, mdp.quotient_choice_map, inconsistent_assignments, choice_values, expected_visits) - return choice_values, expected_visits, inconsistent_differences + scores = self.estimate_scheduler_difference(mdp.model, mdp.quotient_choice_map, inconsistent_assignments, choice_values, expected_visits) + return scores def suboptions_half(self, mdp, splitter): ''' Split options of a splitter into two halves. ''' - options = mdp.design_space.hole_options(splitter) + options = mdp.family.hole_options(splitter) half = len(options) // 2 suboptions = [options[:half], options[half:]] return suboptions @@ -254,7 +249,7 @@ def suboptions_unique(self, mdp, splitter, used_options): assert len(used_options) > 1 suboptions = [[option] for option in used_options] index = 0 - for option in mdp.design_space.hole_options(splitter): + for option in mdp.family.hole_options(splitter): if option in used_options: continue suboptions[index].append(option) @@ -264,7 +259,7 @@ def suboptions_unique(self, mdp, splitter, used_options): def suboptions_enumerate(self, mdp, splitter, used_options): assert len(used_options) > 1 core_suboptions = [[option] for option in used_options] - other_suboptions = [option for option in mdp.design_space.hole_options(splitter) if option not in used_options] + other_suboptions = [option for option in mdp.family.hole_options(splitter) if option not in used_options] return core_suboptions, other_suboptions def holes_with_max_score(self, hole_score): @@ -284,23 +279,22 @@ def split(self, family): # split family wrt last undecided result result = family.analysis_result.undecided_result() - hole_assignments = result.primary_selection - scores = result.primary_scores + scores = self.scheduler_scores(mdp, result.prop, result.primary.result, result.primary_selection) if scores is None: - scores = {hole:0 for hole in range(mdp.design_space.num_holes) if mdp.design_space.hole_num_options(hole) > 1} + scores = {hole:0 for hole in range(mdp.family.num_holes) if mdp.family.hole_num_options(hole) > 1} splitters = self.holes_with_max_score(scores) splitter = splitters[0] if len(hole_assignments[splitter]) > 1: core_suboptions,other_suboptions = self.suboptions_enumerate(mdp, splitter, hole_assignments[splitter]) else: - assert mdp.design_space.hole_num_options(splitter) > 1 + assert mdp.family.hole_num_options(splitter) > 1 core_suboptions = self.suboptions_half(mdp, splitter) other_suboptions = [] - # print(mdp.design_space[splitter], core_suboptions, other_suboptions) + # print(mdp.family[splitter], core_suboptions, other_suboptions) - new_design_space = mdp.design_space.copy() + new_family = mdp.family.copy() if len(other_suboptions) == 0: suboptions = core_suboptions else: @@ -309,28 +303,17 @@ def split(self, family): # construct corresponding design subspaces design_subspaces = [] + # construct corresponding subfamilies + subfamilies = [] family.splitter = splitter parent_info = family.collect_parent_info(self.specification) for suboption in suboptions: - subholes = new_design_space.subholes(splitter, suboption) - design_subspace = paynt.family.family.DesignSpace(subholes, parent_info) - design_subspace.hole_set_options(splitter, suboption) - design_subspaces.append(design_subspace) - - return design_subspaces + subfamily = new_family.subholes(splitter, suboption) + subfamily.add_parent_info(parent_info) + subfamily.hole_set_options(splitter, suboption) + subfamilies.append(subfamily) - - def double_check_assignment(self, assignment): - ''' - Double-check whether this assignment truly improves optimum. - ''' - dtmc = self.build_assignment(assignment) - res = self.check_specification_for_dtmc(dtmc) - # opt_result = dtmc.model_check_property(opt_prop) - if res.constraints_result.sat and self.specification.optimality.improves_optimum(res.optimality_result.value): - return assignment, res.optimality_result.value - else: - return None, None + return subfamilies def get_property(self): @@ -353,104 +336,3 @@ def identify_absorbing_states(self, model): def identify_target_states(self, model, prop): target_label = prop.get_target_label() return model.labeling.get_states(target_label) - - - def check_specification_for_dtmc(self, dtmc, constraint_indices=None, short_evaluation=False): - - # check constraints - if constraint_indices is None: - constraint_indices = range(len(self.specification.constraints)) - results = [None for _ in self.specification.constraints] - for index in constraint_indices: - result = dtmc.model_check_property(self.specification.constraints[index]) - results[index] = result - if short_evaluation and result.sat is False: - break - constraints_result = paynt.verification.property_result.ConstraintsResult(results) - - #check optimality - optimality_result = None - if self.specification.has_optimality and not (short_evaluation and constraints_result.sat is False): - optimality_result = dtmc.model_check_property(self.specification.optimality) - - return paynt.verification.property_result.SpecificationResult(constraints_result, optimality_result) - - - def check_specification_for_mdp(self, mdp, constraint_indices=None, double_check=True): - ''' - Check specification. - :param specification containing constraints and optimality - :param constraint_indices a selection of property indices to investigate (default: all) - :param double_check if True, the new optimum is double-checked - ''' - # check constraints - if constraint_indices is None: - constraint_indices = range(len(self.specification.constraints)) - results = [None for _ in self.specification.constraints] - for index in constraint_indices: - constraint = self.specification.constraints[index] - result = paynt.verification.property_result.MdpPropertyResult(constraint) - - # check primary direction - result.primary = mdp.model_check_property(constraint) - - # no need to check secondary direction if primary direction yields UNSAT - if not result.primary.sat: - result.sat = False - else: - # check secondary direction - result.secondary = mdp.model_check_property(constraint, alt=True) - if mdp.is_deterministic and result.primary.value != result.secondary.value: - logger.warning("WARNING: model is deterministic but min state_max: + state_max = mdp_choice_values[choice] + divisor = None + max_diff = state_max-state_min + if abs(state_min) > 0.001: + state_diff = abs(max_diff/state_min) + elif abs(state_max) > 0.001: + state_diff = abs(max_diff/state_max) + else: + state_diff = 0 + state_score[mdp_state] = state_diff + state_score[mdp_state] *= expected_visits[mdp_state] + threshold = 0 + # threshold = numpy.quantile(state_score,0.2) # keep some percentage + for mdp_state,score in enumerate(state_score): + quotient_state = mdp.quotient_state_map[mdp_state] + if state_to_choice[quotient_state] is not None and score <= threshold: + choices_reduced.set(state_to_choice[quotient_state],False) + + consistent,hole_selection = self.quotient.are_choices_consistent(choices_reduced, family.family) + if not consistent: + return + # logger.info(f"harmonization is SAT") + spec = self.quotient.specification + assignment = family.assume_options_copy(hole_selection) + dtmc = self.quotient.build_assignment(assignment) + res = dtmc.check_specification(spec) + if res.constraints_result.sat: + if not spec.has_optimality: + family.analysis_result.improving_assignment = assignment + family.analysis_result.can_improve = False + else: + assignment_value = res.optimality_result.value + if spec.optimality.improves_optimum(assignment_value): + logger.info(f"harmonization achieved value {res.optimality_result.value}") + self.num_harmonization_succeeded += 1 + family.analysis_result.improving_assignment = assignment + family.analysis_result.improving_value = assignment_value + family.analysis_result.can_improve = True + + family_value = family.analysis_result.optimality_result.primary.value + if(abs(family_value-assignment_value) < 0.001): + logger.info(f"harmonization leads to family skip") + self.num_harmonization_skip += 1 + family.analysis_result.can_improve = False + def verify_family(self, family): - self.stat.iteration_smt() + self.num_families_considered += 1 + self.quotient.build(family) if family.mdp is None: + self.num_families_skipped += 1 return - self.stat.iteration_mdp(family.mdp.states) - res = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices) - if res.improving_assignment == "any": - res.improving_assignment = family - family.analysis_result = res + + if family.parent_info is not None: + for choice in family.parent_info.scheduler_choices: + if not family.selected_choices[choice]: + break + else: + # scheduler preserved in the sub-family + self.num_schedulers_preserved += 1 + family.analysis_result = family.parent_info.analysis_result + family.scheduler_choices = family.parent_info.scheduler_choices + # print("DTMC size = ", family.scheduler_choices.number_of_set_bits()) + consistent,hole_selection = self.quotient.are_choices_consistent(family.scheduler_choices, family) + # print("consistent (same parent) ", consistent) + assert not consistent + family.analysis_result.optimality_result.primary_selection = hole_selection + return + + self.num_families_model_checked += 1 + self.check_specification_for_mdp(family) + if not family.analysis_result.can_improve: + return + # self.harmonize_inconsistent_scheduler(family) + def synthesize_tree(self, depth:int): logger.debug(f"synthesizing tree of depth {depth}") self.quotient.decision_tree.set_depth(depth) self.quotient.build_coloring() - assignment = self.synthesize(keep_optimum=True) - if assignment is not None: - self.best_assignment = assignment - if self.quotient.specification.has_optimality: - logger.info(f"new optimum {self.quotient.specification.optimality.optimum} found, printing assignment below:") - print(self.best_assignment) + self.synthesize(keep_optimum=True) def run(self, optimum_threshold=None, export_evaluation=None): paynt_mdp = paynt.models.models.Mdp(self.quotient.quotient_mdp) mc_result = paynt_mdp.model_check_property(self.quotient.get_property()) - mc_result_positive = mc_result.value > 0 logger.info(f"the optimal scheduler has value: {mc_result}") + self.num_families_considered = 0 + self.num_families_skipped = 0 + self.num_families_model_checked = 0 + self.num_schedulers_preserved = 0 + self.num_harmonizations = 0 + self.num_harmonization_succeeded = 0 + self.num_harmonization_skip = 0 + if self.quotient.specification.has_optimality: epsilon = 1e-1 + mc_result_positive = mc_result.value > 0 if self.quotient.specification.optimality.maximizing == mc_result_positive: epsilon *= -1 # optimum_threshold = mc_result.value * (1 + epsilon) - if self.quotient.specification.has_optimality and optimum_threshold is not None: - self.quotient.specification.optimality.update_optimum(optimum_threshold) - logger.debug(f"optimality threshold set to {optimum_threshold}") - + self.set_optimality_threshold(optimum_threshold) self.best_assignment = None + self.best_assignment_value = None + if not SynthesizerDecisionTree.tree_enumeration: self.synthesize_tree(SynthesizerDecisionTree.tree_depth) else: @@ -72,8 +166,19 @@ def run(self, optimum_threshold=None, export_evaluation=None): else: logger.info("no admissible assignment found") + print() + logger.info(f"families considered: {self.num_families_considered}") + logger.info(f"families skipped by construction: {self.num_families_skipped}") + logger.info(f"families model checked: {self.num_families_model_checked}") + logger.info(f"families with schedulers preserved: {self.num_schedulers_preserved}") + logger.info(f"harmonizations attempted: {self.num_harmonizations}") + logger.info(f"harmonizations succeeded: {self.num_harmonization_succeeded}") + logger.info(f"harmonizations lead to family skip: {self.num_harmonization_skip}") + + print() + time_total = self.stat.synthesis_timer_total.read() for name,time in self.quotient.coloring.getProfilingInfo(): - time_percent = round(time / self.stat.synthesis_timer_total.read()*100,1) + time_percent = round(time/time_total*100,1) print(f"{name} = {time} s ({time_percent} %)") print() diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index efcde10a9..a536f172a 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/paynt/synthesizer/policy_tree.py @@ -716,10 +716,9 @@ def split(self, family, prop, hole_selection, splitter, policy): # construct corresponding design subspaces subfamilies = [] family.splitter = splitter - new_design_space = family.copy() + new_family = family.copy() for suboption in suboptions: - subholes = new_design_space.subholes(splitter, suboption) - subfamily = paynt.family.family.DesignSpace(subholes) + subfamily = new_family.subholes(splitter, suboption) subfamily.hole_set_options(splitter, suboption) subfamily.candidate_policy = None subfamilies.append(subfamily) @@ -770,7 +769,7 @@ def evaluate_all(self, family, prop, keep_value_only=False): policy_tree.double_check(self.quotient, prop) policy_tree.print_stats() - self.stat.num_mdps_total = self.quotient.design_space.size + self.stat.num_mdps_total = self.quotient.family.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()) diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 404336417..e34eb6c35 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -43,8 +43,6 @@ def __init__(self, synthesizer): self.acc_size_mdp = 0 self.avg_size_mdp = 0 - self.iterations_smt = None - self.iterations_game = None self.acc_size_game = 0 self.avg_size_game = 0 @@ -89,11 +87,6 @@ def iteration_dtmc(self, size_dtmc): self.acc_size_dtmc += size_dtmc self.print_status() - def iteration_smt(self): - if self.iterations_smt is None: - self.iterations_smt = 0 - self.iterations_smt += 1 - def iteration_mdp(self, size_mdp): if self.iterations_mdp is None: self.iterations_mdp = 0 @@ -148,6 +141,7 @@ def status(self): if self.iterations_dtmc is not None: iters += [f"DTMC: {self.iterations_dtmc}"] ret_str += ", iters = {" + ", ".join(iters) + "}" + # ret_str += f", pres = {self.synthesizer.num_preserved}" spec = self.quotient.specification if spec.has_optimality and spec.optimality.optimum is not None: @@ -163,10 +157,10 @@ def print_status(self): self.status_horizon = self.synthesis_timer.read() + Statistic.status_period_seconds - def finished_synthesis(self, assignment): + def finished_synthesis(self): self.job_type = "synthesis" self.synthesis_timer.stop() - self.synthesized_assignment = assignment + self.synthesized_assignment = self.synthesizer.best_assignment def finished_evaluation(self, evaluations): self.job_type = "evaluation" @@ -195,10 +189,6 @@ def get_summary_iterations(self): type_stats = f"MDP stats: avg MDP size: {avg_size}, iterations: {self.iterations_mdp}" iterations += f"{type_stats}\n" - if self.iterations_smt is not None: - type_stats = f"SMT stats: iterations: {self.iterations_smt}" - iterations += f"{type_stats}\n" - if self.iterations_dtmc is not None: avg_size = round(safe_division(self.acc_size_dtmc, self.iterations_dtmc)) type_stats = f"DTMC stats: avg DTMC size: {avg_size}, iterations: {self.iterations_dtmc}" @@ -218,7 +208,7 @@ def get_summary_evaluation(self): if not self.evaluations or not isinstance(self.evaluations[0], paynt.synthesizer.synthesizer.FamilyEvaluation): return "" members_sat = sum( [evaluation.family.size for evaluation in self.evaluations if evaluation.sat ]) - members_total = self.quotient.design_space.size + members_total = self.quotient.family.size members_sat_percentage = int(round(members_sat/members_total*100,0)) return f"satisfied {members_sat}/{members_total} members ({members_sat_percentage}%)" @@ -231,7 +221,7 @@ 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_or_order}, quotient: {quotient_states} states / {quotient_actions} actions" + design_space = f"number of holes: {self.quotient.family.num_holes}, family size: {self.quotient.family.size_or_order}, quotient: {quotient_states} states / {quotient_actions} actions" timing = f"method: {self.synthesizer.method_name}, synthesis time: {round(self.synthesis_timer.time, 2)} s" iterations = self.get_summary_iterations() diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py index 9c411b641..7bfe295a5 100644 --- a/paynt/synthesizer/synthesizer.py +++ b/paynt/synthesizer/synthesizer.py @@ -63,22 +63,28 @@ def choose_synthesizer(quotient, method, fsc_synthesis, storm_control): if method == "ar_multicore": return paynt.synthesizer.synthesizer_multicore_ar.SynthesizerMultiCoreAR(quotient) raise ValueError("invalid method name") - - + + def __init__(self, quotient): self.quotient = quotient self.stat = None self.explored = None - + self.best_assignment = None + self.best_assignment_value = None + @property def method_name(self): ''' to be overridden ''' pass - + + def set_optimality_threshold(self, optimum_threshold): + if self.quotient.specification.has_optimality and optimum_threshold is not None: + self.quotient.specification.optimality.update_optimum(optimum_threshold) + logger.debug(f"optimality threshold set to {optimum_threshold}") + def explore(self, family): self.explored += family.size - def evaluate_all(self, family, prop, keep_value_only=False): ''' to be overridden ''' pass @@ -99,7 +105,7 @@ def evaluate(self, family=None, prop=None, keep_value_only=False, print_stats=Tr :returns a list of (family,evaluation) pairs ''' if family is None: - family = self.quotient.design_space + family = self.quotient.family if prop is None: prop = self.quotient.get_property() @@ -134,34 +140,34 @@ def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, re :param print_stats if True, synthesis stats will be printed upon completion ''' if family is None: - family = self.quotient.design_space + family = self.quotient.family if family.constraint_indices is None: family.constraint_indices = list(range(len(self.quotient.specification.constraints))) - if self.quotient.specification.has_optimality and optimum_threshold is not None: - self.quotient.specification.optimality.update_optimum(optimum_threshold) - logger.debug(f"optimality threshold set to {optimum_threshold}") - + self.set_optimality_threshold(optimum_threshold) self.stat = paynt.synthesizer.statistic.Statistic(self) self.explored = 0 logger.info("synthesis initiated, design space: {}".format(family.size_or_order)) self.stat.start(family) - assignment = self.synthesize_one(family) - if assignment is not None and assignment.size > 1 and not return_all: - assignment = assignment.pick_any() - self.stat.finished_synthesis(assignment) + self.synthesize_one(family) + if self.best_assignment is not None and self.best_assignment.size > 1 and not return_all: + self.best_assignment = self.best_assignment.pick_any() + self.stat.finished_synthesis() # logger.info("synthesis finished, printing synthesized assignment below:") # logger.info(assignment) - if assignment is not None and assignment.size == 1: - dtmc = self.quotient.build_assignment(assignment) - result = self.quotient.check_specification_for_dtmc(dtmc) + if self.best_assignment is not None and self.best_assignment.size == 1: + dtmc = self.quotient.build_assignment(self.best_assignment) + result = dtmc.check_specification(self.quotient.specification) logger.info(f"double-checking specification satisfiability: {result}") if print_stats: self.stat.print() + assignment = self.best_assignment if not keep_optimum: + self.best_assignment = None + self.best_assignment_value = None self.quotient.specification.reset() return assignment diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index 58d7348a6..690d4f3f1 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -1,6 +1,7 @@ import paynt.synthesizer.synthesizer import paynt.quotient.pomdp import paynt.verification.property_result +import paynt.utils.profiler import logging logger = logging.getLogger(__name__) @@ -10,92 +11,103 @@ class SynthesizerAR(paynt.synthesizer.synthesizer.Synthesizer): @property def method_name(self): return "AR" - + + def check_specification_for_mdp(self, family): + mdp = family.mdp + self.stat.iteration(mdp) + + # check constraints + spec = self.quotient.specification + if family.constraint_indices is None: + family.constraint_indices = spec.all_constraint_indices() + results = [None for _ in spec.constraints] + for index in family.constraint_indices: + constraint = spec.constraints[index] + result = paynt.verification.property_result.MdpPropertyResult(constraint) + + # check primary direction + result.primary = mdp.model_check_property(constraint) + + # no need to check secondary direction if primary direction yields UNSAT + if not result.primary.sat: + result.sat = False + else: + # check secondary direction + result.secondary = mdp.model_check_property(constraint, alt=True) + if mdp.is_deterministic and result.primary.value != result.secondary.value: + logger.warning("WARNING: model is deterministic but min0} - if len(nonzero_scores) > 0: - hole_scores = nonzero_scores - else: - hole_scores = all_scores - - max_score = max(hole_scores.values()) - if max_score > 0: - hole_scores = {h:v for h,v in hole_scores.items() if v / max_score > 0.01 } - with_max_score = [hole for hole in hole_scores if hole_scores[hole] == max_score] - selected_hole = with_max_score[0] - # selected_hole = holes_to_inject[0] - selected_options = selection[selected_hole] - - print() - print("hole scores: ", hole_scores) - print("selected hole: ", selected_hole) - print("hole has options: ", selected_options) - - # identify observation having this hole - for obs in range(self.quotient.observations): - if selected_hole in self.quotient.obs_to_holes[obs]: - selected_observation = obs - break - - if len(selected_options) > 1: - # identify whether this hole is inconsistent in actions or updates - actions,updates = self.quotient.sift_actions_and_updates(selected_observation, selected_hole, selected_options) - if len(actions) > 1: - # action inconsistency - action_inconsistencies[obs] |= actions - else: - memory_inconsistencies[obs] |= updates - - # print status - opt = "-" - if self.quotient.specification.optimality.optimum is not None: - opt = round(self.quotient.specification.optimality.optimum,3) - elapsed = round(fsc_synthesis_timer.read(),1) - logger.info("FSC synthesis: elapsed {} s, opt = {}, injections: {}.".format(elapsed, opt, memory_injections)) - # logger.info("FSC synthesis: assignment: {}".format(best_assignment)) - - # inject memory and continue - logger.info("Injecting memory into observation {} ...".format(selected_observation)) - self.quotient.increase_memory_size(selected_observation) - memory_injections += 1 - def run(self, optimum_threshold=None, export_evaluation=None): @@ -616,7 +403,6 @@ def run(self, optimum_threshold=None, export_evaluation=None): print("\n------------------------------------\n") # Pure PAYNT POMDP synthesis else: - # self.strategy_expected_uai() # self.strategy_iterative(unfold_imperfect_only=False) self.strategy_iterative(unfold_imperfect_only=True) diff --git a/paynt/utils/graphs.py b/paynt/utils/graphs.py index 1ca4b724d..59a10c093 100644 --- a/paynt/utils/graphs.py +++ b/paynt/utils/graphs.py @@ -22,16 +22,16 @@ def __init__(self) -> None: """ self.graph = pgv.AGraph(strict=False, directed=True) - def parse(self, design_space) -> None: + def parse(self, family) -> None: """Parses the design space holes into the nodes dictionary: {start_node: {end_node1: [observation1],...}, end_node2: ...} - design_space: list of holes + family: list of holes """ self.nodes = {} - for hole in range(design_space.num_holes): - tmp = parse_hole(design_space.hole_name(hole)) - tmp["next"] = list(design_space.hole_options(hole)) + for hole in range(family.num_holes): + tmp = parse_hole(family.hole_name(hole)) + tmp["next"] = list(family.hole_options(hole)) for next in tmp["next"]: if tmp["type"] == "Assignment": @@ -62,14 +62,14 @@ def create_graph(self, show_labels=False) -> None: self.graph.add_edge(start, end) self.graph.layout("circo") - def print(self, design_space, file_name="out", show_labels=False, args="-Gsize=5! -Gratio=\"expand\" -Gnodesep=.5") -> None: + def print(self, family, file_name="out", show_labels=False, args="-Gsize=5! -Gratio=\"expand\" -Gnodesep=.5") -> None: """Prints a graph in .png format. - design_space: list of Holes + family: list of Holes file_name: name of file where the graph will be saved without the extention (e.g. file_name=file => file.png) args: string with Graphvix arguments to specify the output format """ - self.parse(design_space) + self.parse(family) self.create_graph(show_labels=show_labels) self.graph.draw(file_name + ".png", format="png", args=args) diff --git a/paynt/utils/profiler.py b/paynt/utils/profiler.py index 511060f4a..8b3ef5a4d 100644 --- a/paynt/utils/profiler.py +++ b/paynt/utils/profiler.py @@ -33,6 +33,22 @@ def read(self): else: return self.time + (self.timestamp() - self.timer) +class GlobalTimeoutTimer(Timer): + + @classmethod + def start(cls, timeout=None): + cls.timeout = timeout + cls.global_timer = Timer() + cls.global_timer.start() + + @classmethod + def stop(cls): + cls.global_timer.stop() + + @classmethod + def timeout_reached(cls): + return cls.timeout is not None and cls.global_timer.read() > cls.timeout + class Profiler: diff --git a/paynt/verification/property.py b/paynt/verification/property.py index d4bf303bf..f28ddf5fb 100644 --- a/paynt/verification/property.py +++ b/paynt/verification/property.py @@ -258,7 +258,6 @@ def improves_optimum(self, value): return self.result_valid(value) and self.meets_op(value, self.optimum) def update_optimum(self, optimum): - # assert self.improves_optimum(optimum) self.optimum = optimum if self.minimizing: self.threshold = optimum * (1 - self.epsilon) @@ -347,6 +346,9 @@ def all_properties(self): properties += [self.optimality] return properties + def all_constraint_indices(self): + return range(len(self.constraints)) + def stormpy_properties(self): return [p.property for p in self.all_properties()] diff --git a/paynt/verification/property_result.py b/paynt/verification/property_result.py index 440747725..07cb2dc2b 100644 --- a/paynt/verification/property_result.py +++ b/paynt/verification/property_result.py @@ -37,9 +37,9 @@ def __str__(self): class SpecificationResult: - def __init__(self, constraints_result, optimality_result): - self.constraints_result = constraints_result - self.optimality_result = optimality_result + def __init__(self): + self.constraints_result = None + self.optimality_result = None def __str__(self): return str(self.constraints_result) + " : " + str(self.optimality_result) @@ -77,15 +77,10 @@ def undecided_result(self): class MdpPropertyResult: def __init__(self,prop): self.prop = prop - self.primary = None self.secondary = None self.sat = None - self.primary_selection = None - self.primary_choice_values = None - self.primary_expected_visits = None - self.primary_scores = None @property def minimizing(self): @@ -98,8 +93,6 @@ def __str__(self): return "{} - {}".format(prim,seco) else: return "{} - {}".format(seco,prim) - - @@ -113,12 +106,10 @@ def __init__(self, prop): class MdpSpecificationResult(SpecificationResult): - def __init__(self, constraints_result, optimality_result): - super().__init__(constraints_result,optimality_result) - self.evaluate() + def __init__(self): + pass - - def evaluate(self): + def evaluate(self, family): self.improving_assignment = None self.improving_value = None self.can_improve = None @@ -126,28 +117,25 @@ def evaluate(self): cr = self.constraints_result opt = self.optimality_result - if cr.sat == True: + if cr.sat is False: + self.can_improve = False + return + + if cr.sat is True: # all constraints were satisfied if opt is None: - self.improving_assignment = "any" + self.improving_assignment = family self.can_improve = False else: self.improving_assignment = opt.improving_assignment self.improving_value = opt.improving_value - self.can_improve = opt.can_improve - - return - - if cr.sat == False: - self.can_improve = False + self.can_improve = opt.can_improve return - # constraints undecided: try to push optimality assignment - if opt is not None: + # constraints undecided + if opt is None: + self.can_improve = True + else: self.improving_assignment = opt.improving_assignment self.improving_value = opt.improving_value self.can_improve = opt.improving_value is None and opt.can_improve - else: - self.can_improve = True - - diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index e85244943..b43f855f9 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -15,16 +15,16 @@ ColoringSmt::ColoringSmt( storm::models::sparse::NondeterministicModel const& model, std::vector const& variable_name, std::vector> const& variable_domain, - std::vector> const& tree_list, - std::vector const& node_to_variable + std::vector> const& tree_list ) : initial_state(*model.getInitialStates().begin()), row_groups(model.getNondeterministicChoiceIndices()), choice_destinations(synthesis::computeChoiceDestinations(model)), choice_to_action(synthesis::extractActionLabels(model).second), variable_name(variable_name), variable_domain(variable_domain), - solver(ctx) { + solver(ctx), harmonizing_variable(ctx) { timers[__FUNCTION__].start(); + // std::cout << __FUNCTION__ << " start" << std::endl; for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { @@ -59,11 +59,7 @@ ColoringSmt::ColoringSmt( "Inner node has only one child." ); if(child_true != num_nodes) { - if(node_to_variable.empty()) { - tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain)); - } else { - tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,node_to_variable[node])); - } + tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain)); } else { tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,num_actions)); } @@ -78,6 +74,8 @@ ColoringSmt::ColoringSmt( substitution_variables.push_back(ctx.int_const("act")); getRoot()->createHoles(family); getRoot()->createPaths(substitution_variables); + harmonizing_variable = ctx.int_const("__harm__"); + getRoot()->createPathsHarmonizing(substitution_variables, harmonizing_variable); for(uint64_t state = 0; state < numStates(); ++state) { state_path_enabled.push_back(BitVector(numPaths())); } @@ -109,13 +107,11 @@ ColoringSmt::ColoringSmt( std::vector choice_substitution_expr; for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - std::vector substitution = state_valuation[state]; - uint64_t action = choice_to_action[choice]; - substitution.push_back(action); z3::expr_vector substitution_expr(ctx); - for(uint64_t value: substitution) { + for(uint64_t value: state_valuation[state]) { substitution_expr.push_back(ctx.int_val(value)); } + substitution_expr.push_back(ctx.int_val(choice_to_action[choice])); choice_substitution_expr.push_back(substitution_expr); } } @@ -132,48 +128,72 @@ ColoringSmt::ColoringSmt( path_action_hole.push_back(terminal->action_hole.hole); } - /*std::vector path_expressions; - for(std::vector> const& path: getRoot()->paths) { - z3::expr_vector expression(ctx); - getRoot()->loadPathExpression(path,expression); - path_expressions.push_back(expression); - - const TreeNode *node = getRoot()->getNodeOfPath(path,path.size()-1); - const TerminalNode * terminal = dynamic_cast(node); - path_action_hole.push_back(terminal->action_hole.hole); - }*/ - // create choice colors timers["ColoringSmt:: create choice colors"].start(); for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - std::vector path_prefix; - z3::expr_vector all_paths(ctx); + std::vector path_exprs; + std::vector path_exprs_harm; + z3::expr_vector path_and_action(ctx); + z3::expr_vector path_and_action_harm(ctx); std::vector path_label; for(uint64_t path = 0; path < numPaths(); ++path) { - z3::expr_vector prefix_steps_evaluated(ctx); + std::string label = "p" + std::to_string(choice) + "_" + std::to_string(path); + path_label.push_back(label); + + z3::expr_vector path_steps_evaluated(ctx); for(uint64_t step = 0; step < path_expressions[path].size()-1; ++step) { z3::expr step_expr = path_expressions[path][step]; - prefix_steps_evaluated.push_back(step_expr.substitute(substitution_variables,choice_substitution_expr[choice])); + path_steps_evaluated.push_back(step_expr.substitute(substitution_variables,choice_substitution_expr[choice])); } - z3::expr action_expr = path_expressions[path].back(); - z3::expr action_evaluated = action_expr.substitute(substitution_variables,choice_substitution_expr[choice]); - - z3::expr prefix_evaluated = z3::mk_and(prefix_steps_evaluated); - path_prefix.push_back(prefix_evaluated); - all_paths.push_back(not prefix_evaluated or action_evaluated); - std::string label = "m" + std::to_string(choice) + "_" + std::to_string(path); - path_label.push_back(label); + z3::expr action_evaluated = path_expressions[path].back().substitute(substitution_variables,choice_substitution_expr[choice]); + z3::expr path_evaluated = not z3::mk_and(path_steps_evaluated); // mind the negation + path_exprs.push_back(path_evaluated); + path_and_action.push_back(path_evaluated or action_evaluated); } - choice_path_prefix.push_back(path_prefix); - choice_path_and_action.push_back(all_paths); - choice_path_and_action_expr.push_back(z3::mk_and(all_paths)); choice_path_label.push_back(path_label); + + choice_path.push_back(path_exprs); + choice_path_and_action.push_back(path_and_action); } } + + // create harmonizing variants + std::vector all_holes(family.numHoles()); + getRoot()->loadAllHoles(all_holes); + std::vector> path_holes(numPaths()); + for(uint64_t path = 0; path < numPaths(); ++path) { + getRoot()->loadPathHoles(getRoot()->paths[path],path_holes[path]); + } + std::vector hole_what; + std::vector hole_with; + for(const TreeNode::Hole *hole: all_holes) { + z3::expr_vector what(ctx); what.push_back(hole->solver_variable); hole_what.push_back(what); + z3::expr_vector with(ctx); with.push_back(hole->solver_variable_harm); hole_with.push_back(with); + } + + for(uint64_t choice = 0; choice < numChoices(); ++choice) { + z3::expr_vector path_variants(ctx); + for(uint64_t path = 0; path < numPaths(); ++path) { + std::vector choice_path_variants; + z3::expr e = choice_path_and_action[choice][path]; + z3::expr_vector variants(ctx); + variants.push_back(e); + for(uint64_t hole: path_holes[path]) { + variants.push_back( + (harmonizing_variable == (int)hole) and e.substitute(hole_what[hole],hole_with[hole]) + ); + } + path_variants.push_back(z3::mk_or(variants)); + // std::cout << choice_path_and_action[choice][path] << std::endl; + // std::cout << path_variants.back() << std::endl; + } + choice_path_and_action_harm.push_back(path_variants); + } timers["ColoringSmt:: create choice colors"].stop(); + // std::cout << __FUNCTION__ << " end" << std::endl; timers[__FUNCTION__].stop(); } @@ -207,6 +227,14 @@ uint64_t ColoringSmt::numPaths() { return getRoot()->paths.size(); } +template +bool ColoringSmt::check() { + timers["solver.check()"].start(); + bool sat = solver.check() == z3::sat; + timers["solver.check()"].stop(); + return sat; +} + templatestd::vector> ColoringSmt::getFamilyInfo() { std::vector> hole_info(family.numHoles()); getRoot()->loadHoleInfo(hole_info); @@ -227,9 +255,7 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil timers["selectCompatibleChoices::1 is family sat"].start(); solver.push(); getRoot()->addFamilyEncoding(subfamily,solver); - timers["solver.check()"].start(); - bool subfamily_sat = solver.check() == z3::sat; - timers["solver.check()"].stop(); + bool subfamily_sat = check(); solver.pop(); timers["selectCompatibleChoices::1 is family sat"].stop(); STORM_LOG_THROW( @@ -251,13 +277,13 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil timers["selectCompatibleChoices::2 state exploration"].start(); BitVector selection(numChoices(),false); // std::vector> state_enabled_choices(numStates()); - std::queue reachable_states; - BitVector state_explored(numStates(),false); - reachable_states.push(initial_state); - state_explored.set(initial_state,true); + std::queue unexplored_states; + unexplored_states.push(initial_state); + BitVector state_reached(numStates(),false); + state_reached.set(initial_state,true); - while(not reachable_states.empty()) { - uint64_t state = reachable_states.front(); reachable_states.pop(); + while(not unexplored_states.empty()) { + uint64_t state = unexplored_states.front(); unexplored_states.pop(); /*std::cout << "state: "; for(uint64_t variable = 0; variable < numVariables(); ++variable) { std::cout << variable_name[variable] << " = " << variable_domain[variable][state_valuation[state][variable]] << ", "; @@ -281,9 +307,9 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil any_choice_enabled = true; // state_enabled_choices[state].push_back(choice); for(uint64_t dst: choice_destinations[choice]) { - if(not state_explored[dst]) { - reachable_states.push(dst); - state_explored.set(dst,true); + if(not state_reached[dst]) { + unexplored_states.push(dst); + state_reached.set(dst,true); } } break; @@ -292,11 +318,22 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil } // if(state_enabled_choices[state].empty()) { if(not any_choice_enabled) { - STORM_LOG_WARN_COND(not subfamily.isAssignment(), "Hole assignment does not induce a DTMC."); - selection.clear(); - timers["selectCompatibleChoices::2 state exploration"].stop(); - timers[__FUNCTION__].stop(); - return selection; + if(subfamily.isAssignment()) { + // STORM_LOG_WARN("Hole assignment does not induce a DTMC, enabling first action..."); + uint64_t choice = row_groups[state]; + selection.set(choice,true); + for(uint64_t dst: choice_destinations[choice]) { + if(not state_reached[dst]) { + unexplored_states.push(dst); + state_reached.set(dst,true); + } + } + } else { + selection.clear(); + timers["selectCompatibleChoices::2 state exploration"].stop(); + timers[__FUNCTION__].stop(); + return selection; + } } } timers["selectCompatibleChoices::2 state exploration"].stop(); @@ -306,7 +343,7 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil solver.push(); getRoot()->addFamilyEncoding(subfamily,solver); timers["selectCompatibleChoices::3 prepare to check consistent scheduler existence"].start(); - for(uint64_t state: state_explored) { + for(uint64_t state: state_reached) { z3::expr_vector enabled_choices(ctx); /*for(uint64_t choice: state_enabled_choices[state]) { // enabled_choices.push_back(z3::mk_and(choice_path_and_action[choice])); @@ -316,9 +353,7 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil } timers["selectCompatibleChoices::3 prepare to check consistent scheduler existence"].stop(); timers["selectCompatibleChoices::4 consistent scheduler existence"].start(); - timers["solver.check()"].start(); - bool consistent_scheduler_exists = solver.check() == z3::sat; - timers["solver.check()"].stop(); + bool consistent_scheduler_exists = check(); timers["selectCompatibleChoices::4 consistent scheduler existence"].stop(); if(not consistent_scheduler_exists) { STORM_LOG_WARN_COND(not subfamily.isAssignment(), "Hole assignment does not induce a DTMC."); @@ -326,6 +361,7 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil } solver.pop(); } + timers["selectCompatibleChoices::2 state exploration"].stop(); timers[__FUNCTION__].stop(); return selection; @@ -335,34 +371,29 @@ template std::pair>> ColoringSmt::areChoicesConsistent(BitVector const& choices, Family const& subfamily) { timers[__FUNCTION__].start(); + timers["areChoicesConsistent::1 is scheduler consistent?"].start(); solver.push(); getRoot()->addFamilyEncoding(subfamily,solver); solver.push(); for(uint64_t choice: choices) { uint64_t state = choice_to_state[choice]; - for(uint64_t path = 0; path < numPaths(); ++path) { - if(not state_path_enabled[state][path]) { - continue; - } + for(uint64_t path: state_path_enabled[state]) { const char *label = choice_path_label[choice][path].c_str(); - bool action_enabled = subfamily.holeContains(path_action_hole[path],choice_to_action[choice]); + + solver.add(choice_path_and_action[choice][path], label); + + /*bool action_enabled = subfamily.holeContains(path_action_hole[path],choice_to_action[choice]); if(action_enabled) { solver.add(choice_path_and_action[choice][path], label); } else { - solver.add(not choice_path_prefix[choice][path], label); - } + solver.add(choice_path[choice][path], label); + }*/ } } - timers["solver.check()"].start(); - bool consistent = solver.check() == z3::sat; - timers["solver.check()"].stop(); + bool consistent = check(); timers["areChoicesConsistent::1 is scheduler consistent?"].stop(); - // timers["areChoicesConsistent::1 is scheduler consistent? (reworked)"].start(); - - // timers["areChoicesConsistent::1 is scheduler consistent? (reworked)"].stop(); - std::vector> hole_options(family.numHoles()); std::vector> hole_options_vector(family.numHoles()); if(consistent) { @@ -383,19 +414,20 @@ std::pair>> ColoringSmt::areCh std::istringstream iss(expr.decl().name().str()); // std::cout << expr << std::endl; char prefix; iss >> prefix; - if(prefix == 'h' or prefix == 'r') { + if(prefix == 'h' or prefix == 'z') { continue; } uint64_t choice,path; iss >> choice; iss >> prefix; iss >> path; uint64_t action = choice_to_action[choice]; bool action_enabled = subfamily.holeContains(path_action_hole[path],choice_to_action[choice]); + // std::cout << "state = " << choice_to_state[choice] << ", choice = " << choice << ", path = " << path << std::endl; /*if(action_enabled) { std::cout << "UC: " << choice_path_and_action[choice][path] << std::endl; } else { - std::cout << "UC: " << (not choice_path_prefix[choice][path]) << std::endl; + std::cout << "UC: " << (choice_path[choice][path]) << std::endl; }*/ - getRoot()->unsatCoreAnalysisMeta( + getRoot()->unsatCoreAnalysis( subfamily, getRoot()->paths[path], state_valuation[choice_to_state[choice]], choice_to_action[choice], action_enabled, hole_options ); @@ -412,6 +444,160 @@ std::pair>> ColoringSmt::areCh } +template +std::pair>> ColoringSmt::areChoicesConsistent2(BitVector const& choices, Family const& subfamily) { + timers[__FUNCTION__].start(); + + timers["areChoicesConsistent::1 is scheduler consistent?"].start(); + solver.push(); + getRoot()->addFamilyEncoding(subfamily,solver); + solver.push(); + for(uint64_t choice: choices) { + uint64_t state = choice_to_state[choice]; + for(uint64_t path: state_path_enabled[state]) { + const char *label = choice_path_label[choice][path].c_str(); + + solver.add(choice_path_and_action[choice][path], label); + + /*bool action_enabled = subfamily.holeContains(path_action_hole[path],choice_to_action[choice]); + if(action_enabled) { + solver.add(choice_path_and_action[choice][path], label); + } else { + solver.add(choice_path[choice][path], label); + }*/ + } + } + bool consistent = check(); + timers["areChoicesConsistent::1 is scheduler consistent?"].stop(); + + if(consistent) { + z3::model model = solver.get_model(); + solver.pop(); + solver.pop(); + std::vector> hole_options_vector(family.numHoles()); + getRoot()->loadHoleAssignmentFromModel(model,hole_options_vector); + timers[__FUNCTION__].stop(); + return std::make_pair(true,hole_options_vector); + } + solver.pop(); + + timers["areChoicesConsistent::2 better unsat core"].start(); + solver.push(); + std::queue unexplored_states; + unexplored_states.push(initial_state); + BitVector state_reached(numStates(),false); + state_reached.set(initial_state,true); + uint64_t states_explored = 0; + consistent = true; + while(consistent) { + STORM_LOG_THROW(not unexplored_states.empty(), storm::exceptions::UnexpectedException, "all states explored but UNSAT core not found"); + uint64_t state = unexplored_states.front(); unexplored_states.pop(); + // std::cout << "exploring state " << state; + states_explored += 1; + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + if(not choices[choice]) { + continue; + } + // std::cout << "adding choice = " << choice << std::endl; + for(uint64_t path = 0; path < numPaths(); ++path) { + if(not state_path_enabled[state][path]) { + continue; + } + const char *label = choice_path_label[choice][path].c_str(); + solver.add(choice_path_and_action[choice][path], label); + } + consistent = check(); + if(not consistent) { + // std::cout << "inconsistent" << std::endl; + break; + } + for(uint64_t dst: choice_destinations[choice]) { + if(not state_reached[dst]) { + unexplored_states.push(dst); + state_reached.set(dst,true); + } + } + } + } + // std::cout << "states_explored = " << states_explored << std::endl; + z3::expr_vector unsat_core = solver.unsat_core(); + solver.pop(); + timers["areChoicesConsistent::2 better unsat core"].stop(); + + bool PRINT_UNSAT_CORE = false; + if(PRINT_UNSAT_CORE) + std::cout << "-- unsat core start --" << std::endl; + timers["areChoicesConsistent::3 unsat core analysis"].start(); + solver.push(); + for(z3::expr expr: unsat_core) { + std::istringstream iss(expr.decl().name().str()); + char prefix; iss >> prefix; + if(prefix == 'h' or prefix == 'z') { + continue; + } + + uint64_t choice,path; iss >> choice; iss >> prefix; iss >> path; + const char *label = choice_path_label[choice][path].c_str(); + solver.add(choice_path_and_action_harm[choice][path], label); + if(PRINT_UNSAT_CORE) { + bool action_enabled = subfamily.holeContains(path_action_hole[path],choice_to_action[choice]); + std::cout << "choice = " << choice << ", path = " << path << ", enabled = " << action_enabled << std::endl; + std::cout << choice_path_and_action[choice][path] << std::endl; + // std::cout << choice_path_and_action_harm[choice][path] << std::endl; + } + + } + // std::cout << "harmonizing holes: "; + /*uint64_t num_harmonizing_holes = 0; + std::vector all_holes(family.numHoles()); + getRoot()->loadAllHoles(all_holes); + uint64_t min_depth = 10; + uint64_t max_depth = 0; + uint64_t harmonizing_hole; + for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + solver.push(); + solver.add(harmonizing_variable == (int)hole, "harmonizing domain"); + bool consistent = check(); + if(consistent) { + // std::cout << hole << ","; + num_harmonizing_holes += 1; + // if(all_holes[hole]->depth < min_depth) { + // min_depth = all_holes[hole]->depth; + // harmonizing_hole = hole; + // } + if(all_holes[hole]->depth >= max_depth) { + max_depth = all_holes[hole]->depth; + harmonizing_hole = hole; + } + } + solver.pop(); + }*/ + // std::cout << " (" << num_harmonizing_holes << "/" << family.numHoles() << ")" << std::endl; + // solver.add(harmonizing_variable == int(harmonizing_hole), "harmonizing_domain"); + + solver.add(0 <= harmonizing_variable and harmonizing_variable < family.numHoles(), "harmonizing_domain"); + consistent = check(); + STORM_LOG_THROW(consistent, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT"); + z3::model model = solver.get_model(); + + uint64_t harmonizing_hole = model.eval(harmonizing_variable).get_numeral_uint64(); + std::vector> hole_options(family.numHoles()); + getRoot()->loadHarmonizingHoleAssignmentFromModel(model,hole_options,harmonizing_hole); + if(PRINT_UNSAT_CORE) + std::cout << "-- unsat core end --" << std::endl; + + solver.pop(); + solver.pop(); + timers["areChoicesConsistent::3 unsat core analysis"].stop(); + + std::vector> hole_options_vector(family.numHoles()); + for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + hole_options_vector[hole].assign(hole_options[hole].begin(),hole_options[hole].end()); + } + timers[__FUNCTION__].stop(); + return std::make_pair(false,hole_options_vector); +} + template class ColoringSmt<>; } \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.h b/payntbind/src/synthesis/quotient/ColoringSmt.h index 7737f63e3..77d809b40 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.h +++ b/payntbind/src/synthesis/quotient/ColoringSmt.h @@ -25,8 +25,7 @@ class ColoringSmt { storm::models::sparse::NondeterministicModel const& model, std::vector const& variable_name, std::vector> const& variable_domain, - std::vector> const& tree_list, - std::vector const& node_to_variable + std::vector> const& tree_list ); /** For each hole, get a list of name-type pairs. */ @@ -49,6 +48,9 @@ class ColoringSmt { std::pair>> areChoicesConsistent( BitVector const& choices, Family const& subfamily ); + std::pair>> areChoicesConsistent2( + BitVector const& choices, Family const& subfamily + ); std::map timers; std::vector> getProfilingInfo() { @@ -105,16 +107,24 @@ class ColoringSmt { /** Unrefined family. */ Family family; + bool check(); + /** For each path, an index of the hole that occurs at its end. */ std::vector path_action_hole; /** For each choice and path, a label passed to SMT solver. */ std::vector> choice_path_label; - /** For each choice and path, the corresponding expression describing the prefix. */ - std::vector> choice_path_prefix; + + /** For each choice and path, the corresponding (negated!) expression describing the prefix. */ + std::vector> choice_path; /** For each choice, its color expressed as a conjunction of all path implications. */ std::vector choice_path_and_action; + + z3::expr harmonizing_variable; + /** For each choice and path, the corresponding (negated!) expression describing the prefix. */ + std::vector> choice_path_harm; /** For each choice, its color expressed as a conjunction of all path implications. */ - std::vector choice_path_and_action_expr; + std::vector choice_path_and_action_harm; + /** For each state, whether (in the last subfamily) the path was enabled. */ std::vector state_path_enabled; diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index 03adfc71a..562303f88 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -8,57 +8,65 @@ namespace synthesis { TreeNode::Hole::Hole(bool is_interval_type, z3::context& ctx) -: is_interval_type(is_interval_type), solver_variable(ctx), restriction(ctx) { +: is_interval_type(is_interval_type), solver_variable(ctx), solver_variable_harm(ctx), restriction(ctx) { + // left intentionally blank +} + +TreeNode::Hole::Hole(bool is_interval_type, z3::context& ctx, uint64_t depth) +: is_interval_type(is_interval_type), solver_variable(ctx), solver_variable_harm(ctx), restriction(ctx), depth(depth) { // left intentionally blank } void TreeNode::Hole::createSolverVariable() { solver_variable = solver_variable.ctx().int_const(name.c_str()); solver_string_domain = "h_" + std::to_string(hole); + solver_string_domain_harm = "z_" + std::to_string(hole); solver_string_restriction = "r_" + std::to_string(hole); + + name_harm = name + "_h"; + solver_variable_harm = solver_variable.ctx().int_const(name_harm.c_str()); } uint64_t TreeNode::Hole::getModelValue(z3::model const& model) const { return model.eval(solver_variable).get_numeral_int64(); } - -z3::expr TreeNode::Hole::domainEncoding(Family const& subfamily) const { - if(is_interval_type) { - return domainInterval(subfamily); - } else { - return domainEnumeration(subfamily); - } +uint64_t TreeNode::Hole::getModelValueHarmonizing(z3::model const& model) const { + return model.eval(solver_variable_harm).get_numeral_int64(); } - -void TreeNode::Hole::addDomainEncoding(Family const& subfamily, z3::solver& solver) const { - z3::expr encoding = domainEncoding(subfamily); - // std::cout << solver_string_domain.c_str() << " : " << encoding << std::endl; - solver.add(encoding, solver_string_domain.c_str()); - if(is_interval_type) { - // std::cout << solver_string_restriction.c_str() << " : " << restriction << std::endl; - // solver.add(restriction, solver_string_restriction.c_str()); - } +void TreeNode::Hole::loadModelValueHarmonizing(z3::model const& model, std::vector> & hole_options) const { + hole_options[hole].insert(getModelValue(model)); + hole_options[hole].insert(getModelValueHarmonizing(model)); } -z3::expr TreeNode::Hole::domainInterval(Family const& subfamily) const { +z3::expr TreeNode::Hole::domainEncoding(Family const& subfamily, bool harmonizing) const { + z3::expr const& variable = not harmonizing ? solver_variable : solver_variable_harm; std::vector const& domain = subfamily.holeOptions(hole); - int domain_min = domain.front(); - int domain_max = domain.back(); - if(domain_min < domain_max) { - return (domain_min <= solver_variable) and (solver_variable <= domain_max); + if(is_interval_type) { + int domain_min = domain.front(); + int domain_max = domain.back(); + if(domain_min < domain_max) { + return (domain_min <= variable) and (variable <= domain_max); + } else { + return (variable == domain_min); + } } else { - return (solver_variable == domain_min); + z3::expr_vector options(variable.ctx()); + for(uint64_t option: domain) { + options.push_back(variable == (int)option); + } + return z3::mk_or(options); } } -z3::expr TreeNode::Hole::domainEnumeration(Family const& subfamily) const { - z3::expr_vector options(solver_variable.ctx()); - for(uint64_t option: subfamily.holeOptions(hole)) { - options.push_back(solver_variable == (int)option); - } - return z3::mk_or(options); -} +void TreeNode::Hole::addDomainEncoding(Family const& subfamily, z3::solver& solver) const { + solver.add(domainEncoding(subfamily, false), solver_string_domain.c_str()); + solver.add(domainEncoding(subfamily, true), solver_string_domain_harm.c_str()); + /*if(is_interval_type) { + std::cout << solver_string_restriction.c_str() << " : " << restriction << std::endl; + solver.add(restriction, solver_string_restriction.c_str()); + }*/ +} bool TreeNode::verifyExpression(z3::solver & solver, z3::expr const& expr) { solver.push(); @@ -133,11 +141,13 @@ TerminalNode::TerminalNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, std::vector> const& variable_domain, uint64_t num_actions -) : TreeNode(identifier,ctx,variable_name,variable_domain), num_actions(num_actions), action_hole(false,ctx), action_expr(ctx) {} +) : TreeNode(identifier,ctx,variable_name,variable_domain), num_actions(num_actions), action_hole(false,ctx), + action_expr(ctx), action_expr_harm(ctx) {} void TerminalNode::createHoles(Family& family) { action_hole.hole = family.addHole(num_actions); action_hole.name = "A_" + std::to_string(identifier); + action_hole.depth = depth; action_hole.createSolverVariable(); } @@ -150,199 +160,90 @@ void TerminalNode::createPaths(z3::expr_vector const& substitution_variables) { paths.push_back({true}); } -void TerminalNode::loadPathExpression( - std::vector const& path, z3::expr_vector & expression -) const { - expression.push_back(action_expr); -} - -void TerminalNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { - action_hole.addDomainEncoding(subfamily,solver); -} - -void TerminalNode::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { - hole_options[action_hole.hole].push_back(action_hole.getModelValue(model)); +void TerminalNode::createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) { + z3::expr const& hv = harmonizing_variable; + int hole = (int)action_hole.hole; + z3::expr eh = action_hole.solver_variable_harm == substitution_variables.back(); + action_expr_harm = (hv != hole and action_expr) or (hv == hole and ((not action_expr and eh) or (action_expr and not eh))); } -bool TerminalNode::isPathEnabledInState( - std::vector const& path, Family const& subfamily, std::vector const& state_valuation -) const { - return true; +void TerminalNode::loadPathExpression(std::vector const& path, z3::expr_vector & expression) const { + expression.push_back(action_expr); } -void TerminalNode::unsatCoreAnalysisMeta( - Family const& subfamily, - std::vector const& path, - std::vector const& state_valuation, - uint64_t path_action, bool action_enabled, - std::vector> & hole_options -) const { - if(not action_enabled) { - return; - } - hole_options[action_hole.hole].insert(path_action); +void TerminalNode::loadAllHoles(std::vector & holes) const { + holes[action_hole.hole] = &action_hole; } - - - - - -InnerNodeSpecific::InnerNodeSpecific( - uint64_t identifier, z3::context & ctx, - std::vector const& variable_name, - std::vector> const& variable_domain, - uint64_t variable -) : TreeNode(identifier,ctx,variable_name,variable_domain), variable(variable), variable_hole(true,ctx), -step_true(ctx), step_false(ctx) {} - -void InnerNodeSpecific::createHoles(Family& family) { - variable_hole.hole = family.addHole(variable_domain[variable].size()-1); - variable_hole.name = variable_name[variable] + "_" + std::to_string(identifier); - variable_hole.createSolverVariable(); - - // add restrictions - InnerNodeSpecific *node = this; - InnerNodeSpecific *node_parent = std::dynamic_pointer_cast(node->parent).get(); - InnerNodeSpecific *lower_bound = NULL; - InnerNodeSpecific *upper_bound = NULL; - while(node_parent != NULL) { - if(node_parent->variable == variable) { - if(node->isTrueChild()) { - if(upper_bound == NULL) { - upper_bound = node_parent; - } - } else { - if(lower_bound == NULL) { - lower_bound = node_parent; - } - } - if(upper_bound != NULL and lower_bound != NULL) { - break; - } - } - node = node_parent; - node_parent = std::dynamic_pointer_cast(node->parent).get(); - } - z3::expr_vector restriction(ctx); - if(lower_bound != NULL) { - restriction.push_back(variable_hole.solver_variable >= lower_bound->variable_hole.solver_variable); - } - if(upper_bound != NULL) { - restriction.push_back(variable_hole.solver_variable <= upper_bound->variable_hole.solver_variable); - } - variable_hole.restriction = z3::mk_and(restriction); - child_true->createHoles(family); - child_false->createHoles(family); +void TerminalNode::loadPathHoles(std::vector const& path, std::vector & holes) const { + holes.push_back(action_hole.hole); } -void InnerNodeSpecific::loadHoleInfo(std::vector> & hole_info) const { - hole_info[variable_hole.hole] = std::make_pair(variable_hole.name,variable_name[variable]); - child_true->loadHoleInfo(hole_info); - child_false->loadHoleInfo(hole_info); +void TerminalNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { + action_hole.addDomainEncoding(subfamily,solver); } -void InnerNodeSpecific::createPaths(z3::expr_vector const& substitution_variables) { - child_true->createPaths(substitution_variables); - child_false->createPaths(substitution_variables); - - step_true = substitution_variables[variable] <= variable_hole.solver_variable; - step_false = substitution_variables[variable] > variable_hole.solver_variable; - for(bool condition: {true,false}) { - std::shared_ptr child = getChild(condition); - for(std::vector const& suffix: child->paths) { - std::vector path; - path.push_back(condition); - path.insert(path.end(),suffix.begin(),suffix.end()); - paths.push_back(path); - } - } +void TerminalNode::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { + hole_options[action_hole.hole].push_back(action_hole.getModelValue(model)); } - -void InnerNodeSpecific::loadPathExpression( - std::vector const& path, z3::expr_vector & expression +void TerminalNode::loadHarmonizingHoleAssignmentFromModel( + z3::model const& model, std::vector> & hole_options, uint64_t harmonizing_hole ) const { - bool step_to_true_child = path[depth]; - z3::expr const& step = step_to_true_child ? step_true : step_false; - expression.push_back(step); - getChild(step_to_true_child)->loadPathExpression(path,expression); + if(action_hole.hole == harmonizing_hole) { + action_hole.loadModelValueHarmonizing(model,hole_options); + } } -void InnerNodeSpecific::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { - variable_hole.addDomainEncoding(subfamily,solver); - child_true->addFamilyEncoding(subfamily,solver); - child_false->addFamilyEncoding(subfamily,solver); +void TerminalNode::printHarmonizing(z3::model const& model) const { + std::cout << action_hole.name_harm << " = " << action_hole.getModelValueHarmonizing(model) << std::endl; } -bool InnerNodeSpecific::isPathEnabledInState( +bool TerminalNode::isPathEnabledInState( std::vector const& path, Family const& subfamily, std::vector const& state_valuation ) const { - bool step_to_true_child = path[depth]; - uint64_t value = state_valuation[variable]; - std::vector const& domain = subfamily.holeOptions(variable_hole.hole); - if( step_to_true_child and not (value <= domain.back())) { - return false; - } - if(not step_to_true_child and not (value > domain.front())) { - return false; - } - return getChild(step_to_true_child)->isPathEnabledInState(path,subfamily,state_valuation); -} - -void InnerNodeSpecific::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { - uint64_t hole_option = variable_hole.getModelValue(model); - hole_options[variable_hole.hole].push_back(hole_option); - child_true->loadHoleAssignmentFromModel(model,hole_options); - child_false->loadHoleAssignmentFromModel(model,hole_options); + return true; } -void InnerNodeSpecific::unsatCoreAnalysisMeta( +void TerminalNode::unsatCoreAnalysis( Family const& subfamily, std::vector const& path, std::vector const& state_valuation, uint64_t path_action, bool action_enabled, std::vector> & hole_options ) const { - bool step_to_true_child = path[depth]; - std::vector const& domain = subfamily.holeOptions(variable_hole.hole); - if(action_enabled == step_to_true_child) { - if(state_valuation[variable] <= domain.back()) { - hole_options[variable_hole.hole].insert(domain.back()); - } - } else { - if(state_valuation[variable] > domain.front()) { - hole_options[variable_hole.hole].insert(domain.front()); - } + if(not action_enabled) { + return; } - getChild(step_to_true_child)->unsatCoreAnalysisMeta(subfamily,path,state_valuation,path_action,action_enabled,hole_options); + hole_options[action_hole.hole].insert(path_action); } - -InnerNodeGeneric::InnerNodeGeneric( +InnerNode::InnerNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, std::vector> const& variable_domain -) : TreeNode(identifier,ctx,variable_name,variable_domain), decision_hole(false,ctx), step_true(ctx), step_false(ctx) {} +) : TreeNode(identifier,ctx,variable_name,variable_domain), decision_hole(false,ctx), + step_true(ctx), step_false(ctx), step_true_harm(ctx), step_false_harm(ctx) {} -void InnerNodeGeneric::createHoles(Family& family) { +void InnerNode::createHoles(Family& family) { + decision_hole.hole = family.addHole(numVariables()); + decision_hole.name = "V_" + std::to_string(identifier); + decision_hole.depth = depth; + decision_hole.createSolverVariable(); for(uint64_t variable = 0; variable < numVariables(); ++variable) { - Hole hole(true,ctx); + Hole hole(true,ctx,depth); hole.hole = family.addHole(variable_domain[variable].size()-1); hole.name = variable_name[variable] + "_" + std::to_string(identifier); hole.createSolverVariable(); variable_hole.push_back(hole); } - decision_hole.hole = family.addHole(numVariables()); - decision_hole.name = "V_" + std::to_string(identifier); - decision_hole.createSolverVariable(); - InnerNodeGeneric *node = this; - InnerNodeGeneric *node_parent = std::dynamic_pointer_cast(node->parent).get(); - std::vector lower_bounds; - std::vector upper_bounds; + InnerNode *node = this; + InnerNode *node_parent = std::dynamic_pointer_cast(node->parent).get(); + std::vector lower_bounds; + std::vector upper_bounds; while(node_parent != NULL) { if(node->isTrueChild()) { upper_bounds.push_back(node_parent); @@ -350,18 +251,18 @@ void InnerNodeGeneric::createHoles(Family& family) { lower_bounds.push_back(node_parent); } node = node_parent; - node_parent = std::dynamic_pointer_cast(node->parent).get(); + node_parent = std::dynamic_pointer_cast(node->parent).get(); } for(uint64_t variable = 0; variable < numVariables(); ++variable) { // Vi=v => (V_lb=v => Xlb <= Xi) and (V_ub=v => Xi <= Xub) z3::expr lhs = decision_hole.solver_variable != (int)variable; z3::expr_vector rhs(ctx); z3::expr const& var_node = variable_hole[variable].solver_variable; - for(InnerNodeGeneric *bound: lower_bounds) { + for(InnerNode *bound: lower_bounds) { z3::expr const& var_bound = bound->variable_hole[variable].solver_variable; rhs.push_back(bound->decision_hole.solver_variable != (int)variable or var_bound <= var_node); } - for(InnerNodeGeneric *bound: upper_bounds) { + for(InnerNode *bound: upper_bounds) { z3::expr const& var_bound = bound->variable_hole[variable].solver_variable; rhs.push_back(bound->decision_hole.solver_variable != (int)variable or var_node <= var_bound); } @@ -371,7 +272,7 @@ void InnerNodeGeneric::createHoles(Family& family) { child_false->createHoles(family); } -void InnerNodeGeneric::loadHoleInfo(std::vector> & hole_info) const { +void InnerNode::loadHoleInfo(std::vector> & hole_info) const { hole_info[decision_hole.hole] = std::make_pair(decision_hole.name,"__decision__"); for(uint64_t variable = 0; variable < numVariables(); ++variable) { Hole const& hole = variable_hole[variable]; @@ -381,7 +282,7 @@ void InnerNodeGeneric::loadHoleInfo(std::vectorloadHoleInfo(hole_info); } -void InnerNodeGeneric::createPaths(z3::expr_vector const& substitution_variables) { +void InnerNode::createPaths(z3::expr_vector const& substitution_variables) { child_true->createPaths(substitution_variables); child_false->createPaths(substitution_variables); @@ -410,16 +311,58 @@ void InnerNodeGeneric::createPaths(z3::expr_vector const& substitution_variables } } -void InnerNodeGeneric::loadPathExpression( - std::vector const& path, z3::expr_vector & expression -) const { +void InnerNode::createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) { + child_true->createPathsHarmonizing(substitution_variables, harmonizing_variable); + child_false->createPathsHarmonizing(substitution_variables, harmonizing_variable); + + // create steps + z3::expr_vector step_true_options(ctx); + z3::expr_vector step_false_options(ctx); + z3::expr const& hv = harmonizing_variable; + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + Hole d = decision_hole; + z3::expr de = d.solver_variable == (int)variable; + z3::expr deh = d.solver_variable_harm == (int)variable; + z3::expr expr_decision = (hv != (int)d.hole and de) or (hv == (int)d.hole and ((not de and deh) or (de and not deh)) ); + + Hole v = variable_hole[variable]; + z3::expr ve = substitution_variables[variable] <= v.solver_variable; + z3::expr veh = substitution_variables[variable] <= v.solver_variable_harm; + z3::expr expr_true = (hv != (int)v.hole and ve) or (hv == (int)v.hole and ((not ve and veh) or (ve and not veh)) ); + z3::expr expr_false = (hv != (int)v.hole and not ve) or (hv == (int)v.hole and ((ve and not veh) or (not ve and veh)) ); + + step_true_options.push_back(expr_decision and expr_true); + step_false_options.push_back(expr_decision and expr_false); + } + step_true_harm = z3::mk_or(step_true_options); + step_false_harm = z3::mk_or(step_false_options); +} + +void InnerNode::loadPathExpression(std::vector const& path, z3::expr_vector & expression) const { bool step_to_true_child = path[depth]; z3::expr const& step = step_to_true_child ? step_true : step_false; expression.push_back(step); getChild(step_to_true_child)->loadPathExpression(path,expression); } -void InnerNodeGeneric::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { +void InnerNode::loadAllHoles(std::vector & holes) const { + holes[decision_hole.hole] = &decision_hole; + for(Hole const& hole: variable_hole) { + holes[hole.hole] = &hole; + } + child_true->loadAllHoles(holes); + child_false->loadAllHoles(holes); +} + +void InnerNode::loadPathHoles(std::vector const& path, std::vector & holes) const { + holes.push_back(decision_hole.hole); + for(Hole const& hole: variable_hole) { + holes.push_back(hole.hole); + } + getChild(path[depth])->loadPathHoles(path,holes); +} + +void InnerNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { decision_hole.addDomainEncoding(subfamily,solver); for(Hole const& hole: variable_hole) { hole.addDomainEncoding(subfamily,solver); @@ -428,7 +371,7 @@ void InnerNodeGeneric::addFamilyEncoding(Family const& subfamily, z3::solver& so child_false->addFamilyEncoding(subfamily,solver); } -bool InnerNodeGeneric::isPathEnabledInState( +bool InnerNode::isPathEnabledInState( std::vector const& path, Family const& subfamily, std::vector const& state_valuation ) const { bool step_to_true_child = path[depth]; @@ -447,7 +390,7 @@ bool InnerNodeGeneric::isPathEnabledInState( return false; } -void InnerNodeGeneric::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { +void InnerNode::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { hole_options[decision_hole.hole].push_back(decision_hole.getModelValue(model)); for(Hole const& hole: variable_hole) { hole_options[hole.hole].push_back(hole.getModelValue(model)); @@ -455,8 +398,33 @@ void InnerNodeGeneric::loadHoleAssignmentFromModel(z3::model const& model, std:: child_true->loadHoleAssignmentFromModel(model,hole_options); child_false->loadHoleAssignmentFromModel(model,hole_options); } +void InnerNode::loadHarmonizingHoleAssignmentFromModel( + z3::model const& model, std::vector> & hole_options, uint64_t harmonizing_hole +) const { + if(decision_hole.hole == harmonizing_hole) { + decision_hole.loadModelValueHarmonizing(model,hole_options); + return; + } + for(Hole const& hole: variable_hole) { + if(hole.hole == harmonizing_hole) { + hole.loadModelValueHarmonizing(model,hole_options); + return; + } + } + child_true->loadHarmonizingHoleAssignmentFromModel(model,hole_options,harmonizing_hole); + child_false->loadHarmonizingHoleAssignmentFromModel(model,hole_options,harmonizing_hole); +} + +void InnerNode::printHarmonizing(z3::model const& model) const { + std::cout << decision_hole.name_harm << " = " << decision_hole.getModelValueHarmonizing(model) << std::endl; + for(Hole const& hole: variable_hole) { + std::cout << hole.name_harm << " = " << hole.getModelValueHarmonizing(model) << std::endl; + } + child_true->printHarmonizing(model); + child_false->printHarmonizing(model); +} -void InnerNodeGeneric::unsatCoreAnalysisMeta( +void InnerNode::unsatCoreAnalysis( Family const& subfamily, std::vector const& path, std::vector const& state_valuation, @@ -513,10 +481,9 @@ void InnerNodeGeneric::unsatCoreAnalysisMeta( hole_options[decision_hole.hole].insert(sat_variable); hole_options[variable_hole[sat_variable].hole].insert(sat_variable_option); return; - } + } } - getChild(step_to_true_child)->unsatCoreAnalysisMeta(subfamily,path,state_valuation,path_action,action_enabled,hole_options); + getChild(step_to_true_child)->unsatCoreAnalysis(subfamily,path,state_valuation,path_action,action_enabled,hole_options); } - } diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h index a67b216eb..af0fe68e1 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.h +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -31,14 +31,24 @@ class TreeNode { z3::expr solver_variable; std::string solver_string_domain; + // harmonizing variable + std::string name_harm; + z3::expr solver_variable_harm; + std::string solver_string_domain_harm; + z3::expr restriction; std::string solver_string_restriction; + uint64_t depth; + Hole(bool is_interval_type, z3::context& ctx); + Hole(bool is_interval_type, z3::context& ctx, uint64_t depth); void createSolverVariable(); uint64_t getModelValue(z3::model const& model) const; + uint64_t getModelValueHarmonizing(z3::model const& model) const; + void loadModelValueHarmonizing(z3::model const& model, std::vector> & hole_options) const; - z3::expr domainEncoding(Family const& subfamily) const; + z3::expr domainEncoding(Family const& subfamily, bool harmonizing) const; void addDomainEncoding(Family const& subfamily, z3::solver& solver) const; protected: @@ -105,10 +115,13 @@ class TreeNode { /** Create a list of paths from this node. */ virtual void createPaths(z3::expr_vector const& substitution_variables) {} + /** Create a list of paths from this node. */ + virtual void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) {} /** Create expression for a path. */ - virtual void loadPathExpression( - std::vector const& path, z3::expr_vector & expression - ) const {} + virtual void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const {} + /** TODO */ + virtual void loadAllHoles(std::vector & holes) const {}; + virtual void loadPathHoles(std::vector const& path, std::vector & holes) const {}; /** Add encoding of hole option in the given family. */ virtual void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const {} @@ -123,7 +136,13 @@ class TreeNode { virtual void loadHoleAssignmentFromModel( z3::model const& model, std::vector> & hole_options ) const {} - virtual void unsatCoreAnalysisMeta( + virtual void loadHarmonizingHoleAssignmentFromModel( + z3::model const& model, std::vector> & hole_options, uint64_t harmonizing_hole + ) const {} + + virtual void printHarmonizing(z3::model const& model) const {} + + virtual void unsatCoreAnalysis( Family const& subfamily, std::vector const& path, std::vector const& state_valuation, @@ -139,6 +158,7 @@ class TerminalNode: public TreeNode { const uint64_t num_actions; Hole action_hole; z3::expr action_expr; + z3::expr action_expr_harm; TerminalNode( uint64_t identifier, z3::context & ctx, @@ -150,9 +170,10 @@ class TerminalNode: public TreeNode { void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; void createPaths(z3::expr_vector const& substitution_variables) override; - void loadPathExpression( - std::vector const& path, z3::expr_vector & expression - ) const override; + void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) override; + void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; + void loadAllHoles(std::vector & holes) const override; + void loadPathHoles(std::vector const& path, std::vector & holes) const override; void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; bool isPathEnabledInState( @@ -164,50 +185,12 @@ class TerminalNode: public TreeNode { void loadHoleAssignmentFromModel( z3::model const& model, std::vector> & hole_options ) const override; - void unsatCoreAnalysisMeta( - Family const& subfamily, - std::vector const& path, - std::vector const& state_valuation, - uint64_t path_action, bool action_enabled, - std::vector> & hole_options + void loadHarmonizingHoleAssignmentFromModel( + z3::model const& model, std::vector> & hole_options, uint64_t harmonizing_hole ) const override; -}; - - -class InnerNodeSpecific: public TreeNode { -public: - - uint64_t variable; - Hole variable_hole; + void printHarmonizing(z3::model const& model) const override; - z3::expr step_true; - z3::expr step_false; - - InnerNodeSpecific( - uint64_t identifier, z3::context & ctx, - std::vector const& variable_name, - std::vector> const& variable_domain, - uint64_t variable - ); - - void createHoles(Family& family) override; - void loadHoleInfo(std::vector> & hole_info) const override; - void createPaths(z3::expr_vector const& substitution_variables) override; - void loadPathExpression( - std::vector const& path, z3::expr_vector & expression - ) const override; - - void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; - bool isPathEnabledInState( - std::vector const& path, - Family const& subfamily, - std::vector const& state_valuation - ) const override; - - void loadHoleAssignmentFromModel( - z3::model const& model, std::vector> & hole_options - ) const override; - void unsatCoreAnalysisMeta( + void unsatCoreAnalysis( Family const& subfamily, std::vector const& path, std::vector const& state_valuation, @@ -217,7 +200,7 @@ class InnerNodeSpecific: public TreeNode { }; -class InnerNodeGeneric: public TreeNode { +class InnerNode: public TreeNode { public: Hole decision_hole; @@ -226,7 +209,10 @@ class InnerNodeGeneric: public TreeNode { z3::expr step_true; z3::expr step_false; - InnerNodeGeneric( + z3::expr step_true_harm; + z3::expr step_false_harm; + + InnerNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, std::vector> const& variable_domain @@ -235,9 +221,10 @@ class InnerNodeGeneric: public TreeNode { void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; void createPaths(z3::expr_vector const& substitution_variables) override; - void loadPathExpression( - std::vector const& path, z3::expr_vector & expression - ) const override; + void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) override; + void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; + void loadAllHoles(std::vector & holes) const override; + void loadPathHoles(std::vector const& path, std::vector & holes) const override; void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; bool isPathEnabledInState( @@ -249,7 +236,12 @@ class InnerNodeGeneric: public TreeNode { void loadHoleAssignmentFromModel( z3::model const& model, std::vector> & hole_options ) const override; - void unsatCoreAnalysisMeta( + void loadHarmonizingHoleAssignmentFromModel( + z3::model const& model, std::vector> & hole_options, uint64_t harmonizing_hole + ) const override; + void printHarmonizing(z3::model const& model) const override; + + void unsatCoreAnalysis( Family const& subfamily, std::vector const& path, std::vector const& state_valuation, diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index c692af803..8ba89e755 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -294,7 +294,6 @@ void bindings_coloring(py::module& m) { m.def("policyToChoicesForFamily", &synthesis::policyToChoicesForFamily); - py::class_(m, "Family") .def(py::init<>()) .def(py::init()) @@ -323,13 +322,13 @@ void bindings_coloring(py::module& m) { storm::models::sparse::NondeterministicModel const&, std::vector const&, std::vector> const&, - std::vector> const&, - std::vector const& + std::vector> const& >()) .def("getFamilyInfo", &synthesis::ColoringSmt<>::getFamilyInfo) .def("selectCompatibleChoices", py::overload_cast(&synthesis::ColoringSmt<>::selectCompatibleChoices)) .def("selectCompatibleChoices", py::overload_cast(&synthesis::ColoringSmt<>::selectCompatibleChoices)) .def("areChoicesConsistent", &synthesis::ColoringSmt<>::areChoicesConsistent) + .def("areChoicesConsistent2", &synthesis::ColoringSmt<>::areChoicesConsistent2) .def("getProfilingInfo", &synthesis::ColoringSmt<>::getProfilingInfo) ; } diff --git a/payntbind/src/synthesis/translation/choiceTransformation.cpp b/payntbind/src/synthesis/translation/choiceTransformation.cpp index b1f6ded6a..9f751593f 100644 --- a/payntbind/src/synthesis/translation/choiceTransformation.cpp +++ b/payntbind/src/synthesis/translation/choiceTransformation.cpp @@ -63,7 +63,7 @@ bool assertChoiceLabelingIsCanonic( auto const& labels = choice_labeling.getLabelsOfChoice(choice); if(labels.size() != 1) { if(throw_on_fail) { - STORM_LOG_THROW(labels.size() == 1, storm::exceptions::InvalidModelException, "expected exactly 1 label for choice " << choice); + STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "expected exactly 1 label for choice " << choice); } else { return false; } @@ -71,7 +71,7 @@ bool assertChoiceLabelingIsCanonic( std::string const& label = *(labels.begin()); if(state_labels.find(label) != state_labels.end()) { if(throw_on_fail) { - STORM_LOG_THROW(state_labels.find(label) == state_labels.end(), storm::exceptions::InvalidModelException, "label " << label << " is used twice for choices in state " << state); + STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "label " << label << " is used twice for choices in state " << state); } else { return false; } @@ -133,7 +133,7 @@ std::pair,std::vector> extractActionLabels( action_labels.push_back(label); } - assertChoiceLabelingIsCanonic(model.getTransitionMatrix().getRowGroupIndices(), choice_labeling); + assertChoiceLabelingIsCanonic(model.getTransitionMatrix().getRowGroupIndices(), choice_labeling, false); std::vector choice_to_action(model.getNumberOfChoices()); for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { auto const& labels = choice_labeling.getLabelsOfChoice(choice);