From 66968d57704c803c8d42cb02c6ec6bbf6d5f641f Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Thu, 5 Dec 2024 18:19:44 +0100 Subject: [PATCH] model-free SMT coloring --- paynt/quotient/mdp.py | 16 +- paynt/synthesizer/decision_tree.py | 33 +-- paynt/verification/property.py | 4 +- .../src/synthesis/quotient/ColoringSmt.cpp | 208 ++++++++++-------- .../src/synthesis/quotient/ColoringSmt.h | 49 +++-- payntbind/src/synthesis/quotient/TreeNode.cpp | 18 +- payntbind/src/synthesis/quotient/bindings.cpp | 15 +- 7 files changed, 197 insertions(+), 146 deletions(-) diff --git a/paynt/quotient/mdp.py b/paynt/quotient/mdp.py index ca919208..20e5b30f 100644 --- a/paynt/quotient/mdp.py +++ b/paynt/quotient/mdp.py @@ -325,7 +325,7 @@ def scheduler_json_to_choices(self, scheduler_json): choices = self.state_to_choice_to_choices(state_to_choice) return choices - def reset_tree(self, depth, disable_counterexamples=False): + def reset_tree(self, depth, enable_harmonization=True): ''' Rebuild the decision tree template, the design space and the coloring. ''' @@ -333,12 +333,15 @@ def reset_tree(self, depth, disable_counterexamples=False): self.decision_tree = DecisionTree(self,self.variables,self.state_valuations) self.decision_tree.set_depth(depth) - # 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() - self.coloring = payntbind.synthesis.ColoringSmt(self.quotient_mdp, variable_name, variable_domain, tree_list, disable_counterexamples) + self.coloring = payntbind.synthesis.ColoringSmt( + self.quotient_mdp.nondeterministic_choice_indices, self.choice_to_action, self.quotient_mdp.state_valuations, + variable_name, variable_domain, tree_list, enable_harmonization + ) + self.coloring.enableStateExploration(self.quotient_mdp) # reconstruct the family hole_info = self.coloring.getFamilyInfo() @@ -398,10 +401,7 @@ def build(self, family): def are_choices_consistent(self, choices, family): ''' Separate method for profiling purposes. ''' return self.coloring.areChoicesConsistent(choices, family.family) - # if family.parent_info is None: - # return self.coloring.areChoicesConsistent(choices, family.family) - # else: - # return self.coloring.areChoicesConsistentUseHint(choices, family.family, family.parent_info.unsat_core_hint) + def scheduler_is_consistent(self, mdp, prop, result): ''' Get hole options involved in the scheduler selection. ''' @@ -484,7 +484,7 @@ def split(self, family): parent_info = family.collect_parent_info(self.specification) parent_info.analysis_result = family.analysis_result parent_info.scheduler_choices = family.scheduler_choices - parent_info.unsat_core_hint = self.coloring.unsat_core.copy() + # parent_info.unsat_core_hint = self.coloring.unsat_core.copy() subfamilies = family.split(splitter,suboptions) for subfamily in subfamilies: subfamily.add_parent_info(parent_info) diff --git a/paynt/synthesizer/decision_tree.py b/paynt/synthesizer/decision_tree.py index 958223b4..e664ee3f 100644 --- a/paynt/synthesizer/decision_tree.py +++ b/paynt/synthesizer/decision_tree.py @@ -185,35 +185,20 @@ def synthesize_tree_sequence(self, opt_result_value): if self.resource_limit_reached(): break - def map_scheduler(self, scheduler_choices, opt_result_value): - # use counterexamples iff a dont' care action exists - disable_counterexamples = "__random__" not in self.quotient.action_labels + def map_scheduler(self, scheduler_choices): self.counters_reset() for depth in range(SynthesizerDecisionTree.tree_depth+1): - self.quotient.reset_tree(depth,disable_counterexamples=disable_counterexamples) - family = self.quotient.family - self.quotient.build(family) + self.quotient.reset_tree(depth,enable_harmonization=False) + family = self.quotient.family.copy() family.analysis_result = self.quotient.build_unsat_result() - best_assignment_old = self.best_assignment - + self.quotient.build(family) consistent,hole_selection = self.quotient.are_choices_consistent(scheduler_choices, family) if consistent: self.verify_hole_selection(family,hole_selection) - elif not disable_counterexamples: - harmonizing_hole = [hole for hole,options in enumerate(hole_selection) if len(options)>1][0] - selection_1 = hole_selection.copy(); selection_1[harmonizing_hole] = [selection_1[harmonizing_hole][0]] - selection_2 = hole_selection.copy(); selection_2[harmonizing_hole] = [selection_2[harmonizing_hole][1]] - for selection in [selection_1,selection_2]: - self.verify_hole_selection(family,selection) - - new_assignment_synthesized = self.best_assignment != best_assignment_old - if new_assignment_synthesized: - self.best_tree = self.quotient.decision_tree - self.best_tree.root.associate_assignment(self.best_assignment) - self.best_tree_value = self.best_assignment_value - if consistent: - break - if not disable_counterexamples and abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-4: + if self.best_assignment is not None: + self.best_tree = self.quotient.decision_tree + self.best_tree.root.associate_assignment(self.best_assignment) + self.best_tree_value = self.best_assignment_value break if self.resource_limit_reached(): @@ -240,7 +225,7 @@ def run(self, optimum_threshold=None): self.best_assignment = self.best_assignment_value = None self.best_tree = self.best_tree_value = None if scheduler_choices is not None: - self.map_scheduler(scheduler_choices, opt_result_value) + self.map_scheduler(scheduler_choices) else: if self.quotient.specification.has_optimality: epsilon = 1e-1 diff --git a/paynt/verification/property.py b/paynt/verification/property.py index c7de16d1..c3901898 100644 --- a/paynt/verification/property.py +++ b/paynt/verification/property.py @@ -149,7 +149,9 @@ def reward(self): @property def is_discounted_reward(self): - return self.formula.is_reward_operator and self.formula.subformula.is_discounted_total_reward_formula + # TODO add discounted reward as a type to Stormpy formula + # return self.formula.is_reward_operator and self.formula.subformula.is_discounted_total_reward_formula + return self.formula.is_reward_operator and "discount" in str(self.formula.subformula) @property def maximizing(self): diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index 454715e1..2842c9c5 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -6,23 +6,22 @@ #include #include -#include namespace synthesis { + template ColoringSmt::ColoringSmt( - storm::models::sparse::NondeterministicModel const& model, + std::vector const& row_groups, + std::vector const& choice_to_action, + storm::storage::sparse::StateValuations const& state_valuations, std::vector const& variable_name, std::vector> const& variable_domain, std::vector> const& tree_list, - bool disable_counterexamples -) : initial_state(*model.getInitialStates().begin()), - row_groups(model.getNondeterministicChoiceIndices()), - choice_destinations(synthesis::computeChoiceDestinations(model)), - choice_to_action(synthesis::extractActionLabels(model).second), + bool enable_harmonization +) : row_groups(row_groups), choice_to_action(choice_to_action), variable_name(variable_name), variable_domain(variable_domain), - solver(ctx), harmonizing_variable(ctx), disable_counterexamples(disable_counterexamples) { + solver(ctx), harmonizing_variable(ctx), enable_harmonization(enable_harmonization) { timers[__FUNCTION__].start(); @@ -34,7 +33,6 @@ ColoringSmt::ColoringSmt( // extract variables in the order of variable_name std::vector program_variables; - storm::storage::sparse::StateValuations const& state_valuations = model.getStateValuations(); auto const& valuation = state_valuations.at(0); for(std::string const& name: variable_name) { bool variable_found = false; @@ -62,7 +60,7 @@ ColoringSmt::ColoringSmt( // create the tree uint64_t num_nodes = tree_list.size(); - uint64_t num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())+1; + this->num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())+1; for(uint64_t node = 0; node < num_nodes; ++node) { auto [parent,child_true,child_false] = tree_list[node]; STORM_LOG_THROW( @@ -72,7 +70,7 @@ ColoringSmt::ColoringSmt( if(child_true != num_nodes) { tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,state_substitution_variables)); } else { - tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,num_actions,action_substitution_variable)); + tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,this->num_actions,action_substitution_variable)); } } getRoot()->createTree(tree_list,tree); @@ -108,16 +106,6 @@ ColoringSmt::ColoringSmt( } } - // create state substitutions - std::vector state_substitution_expr; - for(uint64_t state = 0; state < numStates(); ++state) { - z3::expr_vector substitution_expr(ctx); - for(uint64_t value: state_valuation[state]) { - substitution_expr.push_back(ctx.int_val(value)); - } - state_substitution_expr.push_back(substitution_expr); - } - // create choice colors timers["ColoringSmt:: create choice colors"].start(); @@ -146,7 +134,7 @@ ColoringSmt::ColoringSmt( } } std::vector action_path_expression; - for(uint64_t action = 0; action < num_actions; ++action) { + for(uint64_t action = 0; action < this->num_actions; ++action) { action_path_expression.push_back(z3::expr_vector(ctx)); for(uint64_t path = 0; path < numPaths(); ++path) { z3::expr evaluated = getRoot()->substituteActionExpression(getRoot()->paths[path], action); @@ -165,12 +153,24 @@ ColoringSmt::ColoringSmt( } timers["ColoringSmt:: create choice colors"].stop(); - if(disable_counterexamples) { + if(not this->enable_harmonization) { timers[__FUNCTION__].stop(); return; } timers["ColoringSmt:: create harmonizing variants"].start(); + + // create state substitutions + std::vector state_substitution_expr; + for(uint64_t state = 0; state < numStates(); ++state) { + z3::expr_vector substitution_expr(ctx); + for(uint64_t value: state_valuation[state]) { + substitution_expr.push_back(ctx.int_val(value)); + } + state_substitution_expr.push_back(substitution_expr); + } + + // create harmonizing expressions std::vector state_path_expression_harmonizing; for(uint64_t state = 0; state < numStates(); ++state) { getRoot()->createPrefixSubstitutionsHarmonizing(state_substitution_expr[state]); @@ -203,6 +203,13 @@ ColoringSmt::ColoringSmt( timers[__FUNCTION__].stop(); } +template +void ColoringSmt::enableStateExploration(storm::models::sparse::NondeterministicModel const& model) { + this->enable_state_exploration = true; + this->initial_state = *model.getInitialStates().begin(); + this->choice_destinations = synthesis::computeChoiceDestinations(model); +} + template const uint64_t ColoringSmt::numStates() const { return row_groups.size()-1; @@ -235,9 +242,9 @@ uint64_t ColoringSmt::numPaths() { template bool ColoringSmt::check() { - timers["solver.check()"].start(); + timers[__FUNCTION__].start(); bool sat = solver.check() == z3::sat; - timers["solver.check()"].stop(); + timers[__FUNCTION__].stop(); return sat; } @@ -252,6 +259,16 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil return selectCompatibleChoices(subfamily,BitVector(numChoices(),true)); } +template +void ColoringSmt::visitChoice(uint64_t choice, BitVector & state_reached, std::queue & unexplored_states) { + for(uint64_t dst: choice_destinations[choice]) { + if(not state_reached[dst]) { + unexplored_states.push(dst); + state_reached.set(dst,true); + } + } +} + template BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamily, BitVector const& base_choices) { timers[__FUNCTION__].start(); @@ -281,81 +298,105 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil // check individual choices timers["selectCompatibleChoices::2 state exploration"].start(); - BitVector selection(numChoices(),false); - // std::vector> state_enabled_choices(numStates()); - std::queue unexplored_states; - unexplored_states.push(initial_state); - BitVector state_reached(numStates(),false); - state_reached.set(initial_state,true); - 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]] << ", "; - } - std::cout << std::endl;*/ - state_path_enabled[state].clear(); - for(uint64_t path = 0; path < numPaths(); ++path) { - bool path_enabled = getRoot()->isPathEnabledInState(getRoot()->paths[path],subfamily,state_valuation[state]); - state_path_enabled[state].set(path,path_enabled); - } + BitVector selection(numChoices(),false); + if(this->enable_state_exploration) { + std::queue unexplored_states; + unexplored_states.push(initial_state); + BitVector state_reached(numStates(),false); + state_reached.set(initial_state,true); + while(not unexplored_states.empty()) { + uint64_t state = unexplored_states.front(); unexplored_states.pop(); + state_path_enabled[state].clear(); + for(uint64_t path = 0; path < numPaths(); ++path) { + bool path_enabled = getRoot()->isPathEnabledInState(getRoot()->paths[path],subfamily,state_valuation[state]); + state_path_enabled[state].set(path,path_enabled); + } - bool any_choice_enabled = false; - for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - if(not base_choices[choice]) { - continue; + bool any_choice_enabled = false; + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + if(not base_choices[choice]) { + continue; + } + bool choice_enabled = false; + for(uint64_t path: state_path_enabled[state]) { + if(subfamily.holeContains(path_action_hole[path],choice_to_action[choice])) { + selection.set(choice,true); + any_choice_enabled = true; + visitChoice(choice,state_reached,unexplored_states); + break; + } + } } - bool choice_enabled = false; - for(uint64_t path: state_path_enabled[state]) { - if(subfamily.holeContains(path_action_hole[path],choice_to_action[choice])) { + // if(state_enabled_choices[state].empty()) { + if(not any_choice_enabled) { + if(subfamily.isAssignment()) { + // STORM_LOG_WARN("Hole assignment does not induce a DTMC, enabling first action..."); + // uint64_t choice = row_groups[state]; // pick the first choice + uint64_t choice = row_groups[state+1]-1; // pick the last choice executing the random choice selection.set(choice,true); - any_choice_enabled = true; - // state_enabled_choices[state].push_back(choice); - for(uint64_t dst: choice_destinations[choice]) { - if(not state_reached[dst]) { - unexplored_states.push(dst); - state_reached.set(dst,true); - } - } - break; + visitChoice(choice,state_reached,unexplored_states); + } else { + selection.clear(); + timers["selectCompatibleChoices::2 state exploration"].stop(); + timers[__FUNCTION__].stop(); + return selection; } } } - // if(state_enabled_choices[state].empty()) { - if(not any_choice_enabled) { - if(subfamily.isAssignment()) { - // STORM_LOG_WARN("Hole assignment does not induce a DTMC, enabling first action..."); - // uint64_t choice = row_groups[state]; // pick the first choice - uint64_t choice = row_groups[state+1]-1; // pick the last choice executing the random choice - 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 { + for(uint64_t state = 0; state < numStates(); ++state) { + state_path_enabled[state].clear(); + for(uint64_t path = 0; path < numPaths(); ++path) { + bool path_enabled = getRoot()->isPathEnabledInState(getRoot()->paths[path],subfamily,state_valuation[state]); + state_path_enabled[state].set(path,path_enabled); + } + + bool any_choice_enabled = false; + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + if(not base_choices[choice]) { + continue; + } + bool choice_enabled = false; + for(uint64_t path: state_path_enabled[state]) { + if(subfamily.holeContains(path_action_hole[path],choice_to_action[choice])) { + selection.set(choice,true); + any_choice_enabled = true; + break; } } - } else { - selection.clear(); - timers["selectCompatibleChoices::2 state exploration"].stop(); - timers[__FUNCTION__].stop(); - return selection; } + // if(state_enabled_choices[state].empty()) { + if(not any_choice_enabled) { + if(subfamily.isAssignment()) { + // STORM_LOG_WARN("Hole assignment does not induce a DTMC, enabling first action..."); + // uint64_t choice = row_groups[state]; // pick the first choice + uint64_t choice = row_groups[state+1]-1; // pick the last choice executing the random choice + selection.set(choice,true); + } else { + selection.clear(); + timers["selectCompatibleChoices::2 state exploration"].stop(); + timers[__FUNCTION__].stop(); + return selection; + } + } + } } + timers["selectCompatibleChoices::2 state exploration"].stop(); - if(CHECK_CONSISTENT_SCHEDULER_EXISTENCE) { + /*if(CHECK_CONSISTENT_SCHEDULER_EXISTENCE) { // check selected choices simultaneously solver.push(); getRoot()->addFamilyEncoding(subfamily,solver); for(uint64_t state: state_reached) { z3::expr_vector enabled_choices(ctx); - /*for(uint64_t choice: state_enabled_choices[state]) { + for(uint64_t choice: state_enabled_choices[state]) { // enabled_choices.push_back(z3::mk_and(choice_path_expresssion[choice])); enabled_choices.push_back(choice_path_expresssion_expr[choice]); } - solver.add(z3::mk_or(enabled_choices));*/ + solver.add(z3::mk_or(enabled_choices)); } bool consistent_scheduler_exists = check(); if(not consistent_scheduler_exists) { @@ -363,7 +404,7 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamil selection.clear(); } solver.pop(); - } + }*/ timers[__FUNCTION__].stop(); return selection; @@ -439,7 +480,7 @@ std::pair>> ColoringSmt::areCh return std::make_pair(true,hole_options_vector); } - if(disable_counterexamples) { + if(not this->enable_harmonization) { solver.pop(); solver.pop(); timers[__FUNCTION__].stop(); @@ -470,12 +511,7 @@ std::pair>> ColoringSmt::areCh if(not consistent) { break; } - for(uint64_t dst: choice_destinations[choice]) { - if(not state_reached[dst]) { - unexplored_states.push(dst); - state_reached.set(dst,true); - } - } + visitChoice(choice,state_reached,unexplored_states); break; } } diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.h b/payntbind/src/synthesis/quotient/ColoringSmt.h index d1a38237..e413aa06 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.h +++ b/payntbind/src/synthesis/quotient/ColoringSmt.h @@ -8,6 +8,7 @@ #include #include +#include #include #include @@ -21,21 +22,35 @@ template class ColoringSmt { public: + /** + * Construct an SMT coloring. + * @param row groups (nondeterministic choice indices) of an underlying MDP + * @param choice_to_action for every choice, the corresponding action + * @param state_valuations state valuation of the underlying MDP + * @param variable_name list of variable names + * @param variable_domain list of possible variable values + * @param tree_list a decision tree template encoded via a list of (parent id, left child id, right child id) triples + * @param enable_harmonization if true, the object will be set up to enable CE generation via harmonization + */ ColoringSmt( - storm::models::sparse::NondeterministicModel const& model, + std::vector const& row_groups, + std::vector const& choice_to_action, + storm::storage::sparse::StateValuations const& state_valuations, std::vector const& variable_name, std::vector> const& variable_domain, std::vector> const& tree_list, - bool disable_counterexamples = false + bool enable_harmonization ); + /** + * Enable efficient state exploration of reachable states. + * @note this is required for harmonization + */ + void enableStateExploration(storm::models::sparse::NondeterministicModel const& model); + /** For each hole, get a list of name-type pairs. */ std::vector> getFamilyInfo(); - /** Whether a check for an admissible family member is done before choice selection. */ - const bool CHECK_FAMILY_CONSISTENCE = true; - /** Whether a check for constent scheduler existence is done after choice selection. */ - const bool CHECK_CONSISTENT_SCHEDULER_EXISTENCE = false; /** Get a mask of choices compatible with the family. */ BitVector selectCompatibleChoices(Family const& subfamily); /** Get a mask of sub-choices of \p base_choices compatible with the family. */ @@ -59,17 +74,14 @@ class ColoringSmt { return profiling; } - - /** TODO */ + /** A list of choice-path indices appeared in the last UNSAT core. */ std::vector> unsat_core; protected: - /** If true, the object will be setup for one consistency check. */ - bool disable_counterexamples; + /** Whether a check for an admissible family member is done before choice selection. */ + const bool CHECK_FAMILY_CONSISTENCE = true; - /** The initial state. */ - const uint64_t initial_state; /** Valuation of each state. */ std::vector> state_valuation; @@ -81,8 +93,6 @@ class ColoringSmt { const uint64_t numStates() const; /** Number of choices in the quotient. */ const uint64_t numChoices() const; - /** For each state, a list of target states. */ - std::vector> choice_destinations; /** Number of MDP actions. */ uint64_t num_actions; @@ -112,6 +122,15 @@ class ColoringSmt { /** Unrefined family. */ Family family; + /** Whether efficient state exploration has been enabled. */ + bool enable_state_exploration = false; + /** The initial state. */ + uint64_t initial_state; + /** For each state, a list of target states. */ + std::vector> choice_destinations; + /** Add unexplored destinations of the given choice to the queue and mark them as reached. */ + void visitChoice(uint64_t choice, BitVector & state_reached, std::queue & unexplored_states); + /** Check the current SMT formula. */ bool check(); @@ -122,6 +141,8 @@ class ColoringSmt { /** For each choice, its color expressed as a conjunction of all path implications. */ std::vector choice_path_expresssion; + /** TODO. */ + const bool enable_harmonization; /** SMT variable refering to harmonizing hole. */ z3::expr harmonizing_variable; /** For each choice, its color expressed as a conjunction of all path implications. */ diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index c351c8dd..c9908f1c 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -134,11 +134,11 @@ std::shared_ptr TreeNode::getChild(bool condition) const { TerminalNode::TerminalNode( - uint64_t identifier, z3::context & ctx, - std::vector const& variable_name, - std::vector> const& variable_domain, - uint64_t num_actions, - z3::expr const& action_substitution_variable + uint64_t identifier, z3::context & ctx, + std::vector const& variable_name, + std::vector> const& variable_domain, + uint64_t num_actions, + z3::expr const& action_substitution_variable ) : TreeNode(identifier,ctx,variable_name,variable_domain), num_actions(num_actions), action_substitution_variable(action_substitution_variable), action_hole(false,ctx), action_expr(ctx), action_expr_harm(ctx) {} @@ -228,10 +228,10 @@ void TerminalNode::unsatCoreAnalysis( InnerNode::InnerNode( - uint64_t identifier, z3::context & ctx, - std::vector const& variable_name, - std::vector> const& variable_domain, - z3::expr_vector const& state_substitution_variables + uint64_t identifier, z3::context & ctx, + std::vector const& variable_name, + std::vector> const& variable_domain, + z3::expr_vector const& state_substitution_variables ) : TreeNode(identifier,ctx,variable_name,variable_domain), decision_hole(false,ctx), state_substitution_variables(state_substitution_variables), step_true(ctx), step_false(ctx), substituted_true(ctx), substituted_false(ctx), step_true_harm(ctx), step_false_harm(ctx) {} diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index 64e3feea..d0c0dd0a 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -41,7 +41,7 @@ std::shared_ptr> addStateValuations( std::vector boolean_values; std::vector integer_values(em->getNumberOfVariables()); for(auto [variable_name,value]: state_valuations[state]) { - integer_values[em->getVariable(variable_name).getIndex()] = value; + integer_values[em->getVariable(variable_name).getOffset()] = value; } sv_builder.addState(state, std::move(boolean_values), std::move(integer_values)); } @@ -310,7 +310,11 @@ void bindings_coloring(py::module& m) { ; py::class_(m, "Coloring") - .def(py::init const&, std::vector>> >()) + .def(py::init< + synthesis::Family const&, + std::vector const&, + std::vector>> + >()) .def("getChoiceToAssignment", &synthesis::Coloring::getChoiceToAssignment) .def("getStateToHoles", &synthesis::Coloring::getStateToHoles) .def("selectCompatibleChoices", &synthesis::Coloring::selectCompatibleChoices) @@ -319,17 +323,20 @@ void bindings_coloring(py::module& m) { py::class_>(m, "ColoringSmt") .def(py::init< - storm::models::sparse::NondeterministicModel const&, + std::vector const&, + std::vector const&, + storm::storage::sparse::StateValuations const&, std::vector const&, std::vector> const&, std::vector> const&, bool >()) + .def("enableStateExploration", &synthesis::ColoringSmt<>::enableStateExploration) .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_property_readonly("unsat_core", [](synthesis::ColoringSmt<>& coloring) {return coloring.unsat_core;}) + // .def_property_readonly("unsat_core", [](synthesis::ColoringSmt<>& coloring) {return coloring.unsat_core;}) .def("getProfilingInfo", &synthesis::ColoringSmt<>::getProfilingInfo) ; }