diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index a7d9bcc2..c8eae798 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -45,7 +45,7 @@ jobs: run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} deploy-mdp: - name: Deploy on latest (mdp) (${{ matrix.buildType.name }}) + name: Deploy on branch (mdp) (${{ matrix.buildType.name }}) runs-on: ubuntu-latest strategy: matrix: diff --git a/paynt/quotient/mdp.py b/paynt/quotient/mdp.py index 38da49b4..fab80111 100644 --- a/paynt/quotient/mdp.py +++ b/paynt/quotient/mdp.py @@ -180,8 +180,10 @@ def __init__(self, mdp, specification): super().__init__(specification=specification) updated = payntbind.synthesis.restoreActionsInAbsorbingStates(mdp) if updated is not None: mdp = updated + # action_labels, _ payntbind.synthesis.extractActionLabels(mdp) if MdpQuotient.add_dont_care_action: mdp = payntbind.synthesis.addDontCareAction(mdp) + # stormpy.export_to_drn(mdp, sketch_path+".drn") self.quotient_mdp = mdp self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(mdp) diff --git a/paynt/synthesizer/decision_tree.py b/paynt/synthesizer/decision_tree.py index ccd6932d..2d8400a2 100644 --- a/paynt/synthesizer/decision_tree.py +++ b/paynt/synthesizer/decision_tree.py @@ -82,7 +82,7 @@ def verify_family(self, family): self.check_specification_for_mdp(family) if not family.analysis_result.can_improve: return - self.harmonize_inconsistent_scheduler(family) + # self.harmonize_inconsistent_scheduler(family) def counters_reset(self): @@ -115,6 +115,8 @@ def synthesize_tree_sequence(self, opt_result_value): global_timeout = 300 depth_timeout = global_timeout / 2 / SynthesizerDecisionTree.tree_depth for depth in range(SynthesizerDecisionTree.tree_depth+1): + print() + print("DEPTH = ", depth) print() self.quotient.set_depth(depth) best_assignment_old = self.best_assignment diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index f06c6818..2bbc9fd4 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -25,7 +25,6 @@ ColoringSmt::ColoringSmt( solver(ctx), harmonizing_variable(ctx), one_consistency_check(one_consistency_check) { 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) { @@ -109,7 +108,7 @@ ColoringSmt::ColoringSmt( } } - // create choice substitutions + // create state substitutions std::vector state_substitution_expr; for(uint64_t state = 0; state < numStates(); ++state) { z3::expr_vector substitution_expr(ctx); @@ -141,7 +140,8 @@ ColoringSmt::ColoringSmt( state_path_expression.push_back(z3::expr_vector(ctx)); for(uint64_t path = 0; path < numPaths(); ++path) { z3::expr_vector substituted(ctx); - getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_substitution_expr[state], substituted); + // getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_substitution_expr[state], substituted); + getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_valuation[state], substituted); state_path_expression[state].push_back(z3::mk_or(substituted)); } } @@ -415,12 +415,6 @@ std::pair>> ColoringSmt::areCh timers[__FUNCTION__].start(); std::vector> hole_options_vector(family.numHoles()); - if(one_consistency_check) { - solver.pop(); - timers[__FUNCTION__].stop(); - return std::make_pair(false,hole_options_vector); - } - timers["areChoicesConsistent::1 is scheduler consistent?"].start(); solver.push(); getRoot()->addFamilyEncoding(subfamily,solver); @@ -432,7 +426,6 @@ std::pair>> ColoringSmt::areCh solver.add(choice_path_expresssion[choice][path], label); } } - // std::cout << "(1) added choices: " << choices.getNumberOfSetBits() << std::endl; bool consistent = check(); timers["areChoicesConsistent::1 is scheduler consistent?"].stop(); @@ -444,6 +437,14 @@ std::pair>> ColoringSmt::areCh timers[__FUNCTION__].stop(); return std::make_pair(true,hole_options_vector); } + + if(one_consistency_check) { + solver.pop(); + solver.pop(); + timers[__FUNCTION__].stop(); + return std::make_pair(false,hole_options_vector); + } + solver.pop(); timers["areChoicesConsistent::2 better unsat core"].start(); @@ -539,95 +540,6 @@ std::pair>> ColoringSmt::areCh -template -std::pair>> ColoringSmt::areChoicesConsistentUseHint(BitVector const& choices, Family const& subfamily, std::vector> const& unsat_core_hint) { - timers[__FUNCTION__].start(); - std::vector> hole_options_vector(family.numHoles()); - - timers["areChoicesConsistent::2 better unsat core"].start(); - solver.push(); - getRoot()->addFamilyEncoding(subfamily,solver); - solver.push(); - std::queue unexplored_states; - BitVector state_reached(numStates(),false); - for(auto [choice,path]: unsat_core_hint) { - uint64_t state = choice_to_state[choice]; - if(not state_reached[state]) { - unexplored_states.push(state); - state_reached.set(state,true); - } - } - if(not state_reached[initial_state]) { - unexplored_states.push(initial_state); - state_reached.set(initial_state,true); - } - bool consistent = true; - while(not unexplored_states.empty()) { - uint64_t state = unexplored_states.front(); unexplored_states.pop(); - for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - if(not choices[choice]) { - continue; - } - for(uint64_t path: state_path_enabled[state]) { - const char *label = choice_path_label[choice][path].c_str(); - solver.add(choice_path_expresssion[choice][path], label); - } - consistent = check(); - 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); - } - } - break; - } - } - timers["areChoicesConsistent::2 better unsat core"].stop(); - - if(consistent) { - z3::model model = solver.get_model(); - solver.pop(); - solver.pop(); - getRoot()->loadHoleAssignmentFromModel(model,hole_options_vector); - timers[__FUNCTION__].stop(); - return std::make_pair(true,hole_options_vector); - } - z3::expr_vector unsat_core_expr = solver.unsat_core(); - solver.pop(); - loadUnsatCore(unsat_core_expr,subfamily); - - if(PRINT_UNSAT_CORE) - std::cout << "-- unsat core start --" << std::endl; - timers["areChoicesConsistent::3 unsat core analysis"].start(); - solver.push(); - solver.add(0 <= harmonizing_variable and harmonizing_variable < family.numHoles(), "harmonizing_domain"); - for(auto [choice,path]: this->unsat_core) { - solver.add(choice_path_expresssion_harm[choice][path]); - } - consistent = check(); - STORM_LOG_THROW(consistent, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT"); - z3::model model = solver.get_model(); - solver.pop(); - solver.pop(); - - uint64_t harmonizing_hole = model.eval(harmonizing_variable).get_numeral_uint64(); - getRoot()->loadHoleAssignmentFromModel(model,hole_options_vector); - getRoot()->loadHoleAssignmentFromModelHarmonizing(model,hole_options_vector,harmonizing_hole); - if(hole_options_vector[harmonizing_hole][0] > hole_options_vector[harmonizing_hole][1]) { - uint64_t tmp = hole_options_vector[harmonizing_hole][0]; - hole_options_vector[harmonizing_hole][0] = hole_options_vector[harmonizing_hole][1]; - hole_options_vector[harmonizing_hole][1] = tmp; - } - if(PRINT_UNSAT_CORE) - std::cout << "-- unsat core end --" << std::endl; - timers["areChoicesConsistent::3 unsat core analysis"].stop(); - - timers[__FUNCTION__].stop(); - return std::make_pair(false,hole_options_vector); -} template class ColoringSmt<>; diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.h b/payntbind/src/synthesis/quotient/ColoringSmt.h index b0dde6f2..73e7b8d2 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.h +++ b/payntbind/src/synthesis/quotient/ColoringSmt.h @@ -49,9 +49,6 @@ class ColoringSmt { std::pair>> areChoicesConsistent( BitVector const& choices, Family const& subfamily ); - std::pair>> areChoicesConsistentUseHint( - BitVector const& choices, Family const& subfamily, std::vector> const& unsat_core_hint - ); std::map timers; std::vector> getProfilingInfo() { diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index 7d83ed19..ea68af24 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -165,7 +165,7 @@ uint64_t TerminalNode::getPathActionHole(std::vector const& path) { } -void TerminalNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { +void TerminalNode::substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const { // } @@ -374,10 +374,29 @@ uint64_t InnerNode::getPathActionHole(std::vector const& path) { } -void InnerNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { +void InnerNode::substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const { bool step_to_true_child = path[depth]; - z3::expr step = step_to_true_child ? step_true : step_false; - substituted.push_back(step.substitute(state_substitution_variables,state_valuation)); + // z3::expr step = step_to_true_child ? step_true : step_false; + // substituted.push_back(step.substitute(state_substitution_variables,state_valuation)); + + z3::expr_vector step_options(ctx); + z3::expr const& dv = decision_hole.solver_variable; + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + z3::expr const& vv = variable_hole[variable].solver_variable; + // mind the negation below + if(step_to_true_child) { + if(state_valuation[variable] > 0) { + // not (Vi = vj => sj<=xj) + step_options.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) <= vv)); + } + } else { + if(state_valuation[variable] < variable_domain[variable].size()-1) { + step_options.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) > vv)); + } + } + } + substituted.push_back(z3::mk_or(step_options)); + getChild(step_to_true_child)->substitutePrefixExpression(path,state_valuation,substituted); } diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h index 590de8ad..9dc378fc 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.h +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -118,7 +118,7 @@ class TreeNode { virtual uint64_t getPathActionHole(std::vector const& path) {return 0;} /** Add a step expression evaluated for a given state valuation. */ - virtual void substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {}; + virtual void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const {}; /** Add an action expression evaluated for a given state valuation. */ virtual z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const {return z3::expr(ctx);}; /** Add a step expression evaluated for a given state valuation (harmonizing). */ @@ -175,7 +175,7 @@ class TerminalNode: public TreeNode { void createPaths(z3::expr const& harmonizing_variable) override; uint64_t getPathActionHole(std::vector const& path); - void substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const override; z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const override; void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; @@ -229,7 +229,7 @@ class InnerNode: public TreeNode { void createPaths(z3::expr const& harmonizing_variable) override; uint64_t getPathActionHole(std::vector const& path); - void substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const override; z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const override; void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index e8e71d5b..64e3feea 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -330,7 +330,6 @@ void bindings_coloring(py::module& m) { .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("areChoicesConsistentUseHint", &synthesis::ColoringSmt<>::areChoicesConsistentUseHint) .def("getProfilingInfo", &synthesis::ColoringSmt<>::getProfilingInfo) ; } diff --git a/payntbind/src/synthesis/translation/choiceTransformation.cpp b/payntbind/src/synthesis/translation/choiceTransformation.cpp index 6128da2e..96f02b20 100644 --- a/payntbind/src/synthesis/translation/choiceTransformation.cpp +++ b/payntbind/src/synthesis/translation/choiceTransformation.cpp @@ -403,10 +403,9 @@ std::shared_ptr> addDontCareAction( components.transitionMatrix = builder.build(); auto rewardModels = synthesis::translateRewardModels(model,translated_to_original_choice,translated_choice_mask); for(auto & [name,reward_model]: rewardModels) { - std::cout << "processing " << name << std::endl; std::vector & choice_reward = reward_model.getStateActionRewardVector(); - ValueType reward_sum = 0; for(uint64_t state = 0; state < num_states; ++state) { + ValueType reward_sum = 0; uint64_t new_translated_choice = row_groups_new[state+1]-1; uint64_t state_num_choices = new_translated_choice-row_groups_new[state]; for(uint64_t translated_choice = row_groups_new[state]; translated_choice < new_translated_choice; ++translated_choice) {