From ed86b178305ef4656104ca718f75f73234df6ef5 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 20 Sep 2024 11:01:05 +0200 Subject: [PATCH] delegate path formula substitution to TreeNode --- paynt/parser/jani.py | 4 +- paynt/synthesizer/synthesizer_ar.py | 2 +- .../src/synthesis/quotient/ColoringSmt.cpp | 62 ++++++----------- payntbind/src/synthesis/quotient/TreeNode.cpp | 66 +++++++------------ payntbind/src/synthesis/quotient/TreeNode.h | 42 ++++++------ 5 files changed, 63 insertions(+), 113 deletions(-) diff --git a/paynt/parser/jani.py b/paynt/parser/jani.py index baafadd4..eb52b69a 100644 --- a/paynt/parser/jani.py +++ b/paynt/parser/jani.py @@ -219,8 +219,8 @@ 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=True) - # assignments.substitute(substitution) # legacy version + # assignments.substitute(substitution, substitute_transcendental_numbers=True) + assignments.substitute(substitution) # legacy version templ_edge.add_destination(stormpy.storage.JaniTemplateEdgeDestination(assignments)) new_edge = stormpy.storage.JaniEdge( diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index 1af7788c..f09a412d 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -100,7 +100,7 @@ def update_optimum(self, family): self.quotient.specification.optimality.update_optimum(iv) self.best_assignment = ia self.best_assignment_value = iv - # logger.info(f"value {round(iv,4)} achieved after {round(paynt.utils.timer.GlobalTimer.read(),2)} seconds") + logger.info(f"value {round(iv,4)} achieved after {round(paynt.utils.timer.GlobalTimer.read(),2)} seconds") if isinstance(self.quotient, paynt.quotient.pomdp.PomdpQuotient): self.stat.new_fsc_found(family.analysis_result.improving_value, ia, self.quotient.policy_size(ia)) diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index 8916adde..f06c6818 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -119,37 +119,13 @@ ColoringSmt::ColoringSmt( state_substitution_expr.push_back(substitution_expr); } - // create choice substitutions - // std::vector choice_action_substitution_expr; - 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) { - z3::expr_vector substitution_expr(ctx); - for(uint64_t value: state_valuation[state]) { - substitution_expr.push_back(ctx.int_val(value)); - } - z3::expr action_substitution_expr = ctx.int_val(choice_to_action[choice]); - substitution_expr.push_back(action_substitution_expr); - choice_substitution_expr.push_back(substitution_expr); - } - } + // create choice colors + timers["ColoringSmt:: create choice colors"].start(); - // collect all path expressions - std::vector path_step_expression; - z3::expr_vector path_expression(ctx); for(std::vector const& path: getRoot()->paths) { - z3::expr_vector step_expression(ctx); - getRoot()->loadPathExpression(path,step_expression); - path_step_expression.push_back(step_expression); - path_expression.push_back(z3::mk_or(step_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); + path_action_hole.push_back(getRoot()->getPathActionHole(path)); } - // create choice colors - timers["ColoringSmt:: create choice colors"].start(); - choice_path_label.resize(numChoices()); for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { @@ -160,31 +136,31 @@ ColoringSmt::ColoringSmt( } } - /*std::vector state_path_expresssion; + std::vector state_path_expression; for(uint64_t state = 0; state < numStates(); ++state) { - z3::expr_vector path_evaluated(ctx); + state_path_expression.push_back(z3::expr_vector(ctx)); for(uint64_t path = 0; path < numPaths(); ++path) { - path_evaluated.push_back(path_expression[path].substitute(state_substitution_variables,state_substitution_expr[state])); + z3::expr_vector substituted(ctx); + getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_substitution_expr[state], substituted); + state_path_expression[state].push_back(z3::mk_or(substituted)); } - state_path_expresssion.push_back(path_evaluated); } - - for(uint64_t state = 0; state < numStates(); ++state) { - for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - z3::expr_vector path_evaluated(ctx); - for(uint64_t path = 0; path < numPaths(); ++path) { - path_evaluated.push_back(state_path_expresssion[state][path].substitute(action_substitution_variables,choice_action_substitution_expr[choice])); - } - choice_path_expresssion.push_back(path_evaluated); + std::vector action_path_expression; + for(uint64_t action = 0; action < num_actions; ++action) { + action_path_expression.push_back(z3::expr_vector(ctx)); + for(uint64_t path = 0; path < numPaths(); ++path) { + z3::expr substituted = getRoot()->substituteActionExpression(getRoot()->paths[path], action); + action_path_expression[action].push_back(substituted); } - }*/ + } + for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - z3::expr_vector path_evaluated(ctx); + choice_path_expresssion.push_back(z3::expr_vector(ctx)); + uint64_t action = choice_to_action[choice]; for(uint64_t path = 0; path < numPaths(); ++path) { - path_evaluated.push_back(path_expression[path].substitute(choice_substitution_variables,choice_substitution_expr[choice])); + choice_path_expresssion[choice].push_back(state_path_expression[state][path] or action_path_expression[action][path]); } - choice_path_expresssion.push_back(path_evaluated); } } timers["ColoringSmt:: create choice colors"].stop(); diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index f3956afb..7d83ed19 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -122,13 +122,13 @@ std::shared_ptr TreeNode::getChild(bool condition) const { return condition ? child_true : child_false; } -const TreeNode *TreeNode::getNodeOfPath(std::vector const& path, uint64_t step) const { +/*const TreeNode *TreeNode::getNodeOfPath(std::vector const& path, uint64_t step) const { if(step == depth) { return this; } bool step_to_true_child = path[depth]; return getChild(step_to_true_child)->getNodeOfPath(path,step); -} +}*/ @@ -160,28 +160,25 @@ void TerminalNode::createPaths(z3::expr const& harmonizing_variable) { action_expr_harm = action_expr or (harmonizing_variable == (int)action_hole.hole and action_hole.solver_variable_harm == action_substitution_variable); } -void TerminalNode::loadPathExpression(std::vector const& path, z3::expr_vector & expression) const { - expression.push_back(action_expr); +uint64_t TerminalNode::getPathActionHole(std::vector const& path) { + return action_hole.hole; } -void TerminalNode::loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const { - expression.push_back(action_expr_harm); -} -void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { +void TerminalNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { // } -z3::expr TerminalNode::substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { - return action_hole.solver_variable == (int)action or (harmonizing_variable == (int)action_hole.hole and action_hole.solver_variable_harm == (int)action); +z3::expr TerminalNode::substituteActionExpression(std::vector const& path, uint64_t action) const { + return action_hole.solver_variable == (int)action; } -void TerminalNode::loadAllHoles(std::vector & holes) const { - holes[action_hole.hole] = &action_hole; +void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { + // } -void TerminalNode::loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const { - step_holes.push_back({action_hole.hole}); +z3::expr TerminalNode::substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { + return action_hole.solver_variable == (int)action or (harmonizing_variable == (int)action_hole.hole and action_hole.solver_variable_harm == (int)action); } @@ -372,18 +369,20 @@ void InnerNode::createPaths(z3::expr const& harmonizing_variable) { step_false_harm = z3::mk_or(step_false_harm_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); +uint64_t InnerNode::getPathActionHole(std::vector const& path) { + return getChild(path[depth])->getPathActionHole(path); } -void InnerNode::loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const { + +void InnerNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { bool step_to_true_child = path[depth]; - z3::expr const& step = step_to_true_child ? step_true_harm : step_false_harm; - expression.push_back(step); - getChild(step_to_true_child)->loadPathExpressionHarmonizing(path,expression); + z3::expr step = step_to_true_child ? step_true : step_false; + substituted.push_back(step.substitute(state_substitution_variables,state_valuation)); + getChild(step_to_true_child)->substitutePrefixExpression(path,state_valuation,substituted); +} + +z3::expr InnerNode::substituteActionExpression(std::vector const& path, uint64_t action) const { + return getChild(path[depth])->substituteActionExpression(path,action); } void InnerNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { @@ -398,27 +397,6 @@ z3::expr InnerNode::substituteActionExpressionHarmonizing(std::vector cons } - -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::loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const { - std::vector holes; - holes.push_back(decision_hole.hole); - for(Hole const& hole: variable_hole) { - holes.push_back(hole.hole); - } - step_holes.push_back(holes); - getChild(path[depth])->loadPathStepHoles(path,step_holes); -} - - void InnerNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { decision_hole.addDomainEncoding(subfamily,solver); for(Hole const& hole: variable_hole) { diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h index 6097a473..590de8ad 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.h +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -105,26 +105,26 @@ class TreeNode { /** Retrieve true child of this node if the condition holds, get false child otherwise. */ std::shared_ptr getChild(bool condition) const; /** Execute the path and the corresponding node of the tree. */ - const TreeNode *getNodeOfPath(std::vector const& path, uint64_t step) const; + // const TreeNode *getNodeOfPath(std::vector const& path, uint64_t step) const; /** Create all holes and solver variables associated with this node. */ virtual void createHoles(Family& family) {} - /** Collect name and type (action,decision, or variable) of each hole. */ + /** Collect name and type (action, decision, or variable) of each hole. */ virtual void loadHoleInfo(std::vector> & hole_info) const {} /** Create a list of paths from this node. */ virtual void createPaths(z3::expr const& harmonizing_variable) {} - - /** Create expression for a path. */ - virtual void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const {} - /** Create expression for a harmonizing path. */ - virtual void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const {} - /** TODO */ - virtual void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {} - virtual z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { return z3::expr(ctx); } - - virtual void loadAllHoles(std::vector & holes) const {}; - virtual void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const {}; + /** Retrieve action hole associated with the path. */ + 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 {}; + /** 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). */ + virtual void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {}; + /** Add an action expression evaluated for a given state valuation (harmonizing). */ + virtual z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const {return z3::expr(ctx);}; /** Add encoding of hole option in the given family. */ virtual void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const {} @@ -173,15 +173,13 @@ class TerminalNode: public TreeNode { void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; void createPaths(z3::expr const& harmonizing_variable) override; + uint64_t getPathActionHole(std::vector const& path); - void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; - void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const override; + void substitutePrefixExpression(std::vector const& path, z3::expr_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; - void loadAllHoles(std::vector & holes) const override; - void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const override; - void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; bool isPathEnabledInState( std::vector const& path, @@ -229,15 +227,13 @@ class InnerNode: public TreeNode { void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; void createPaths(z3::expr const& harmonizing_variable) override; + uint64_t getPathActionHole(std::vector const& path); - void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; - void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const override; + void substitutePrefixExpression(std::vector const& path, z3::expr_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; - void loadAllHoles(std::vector & holes) const override; - void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const override; - void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; bool isPathEnabledInState( std::vector const& path,