Skip to content

Commit

Permalink
delegate path formula substitution to TreeNode
Browse files Browse the repository at this point in the history
  • Loading branch information
Roman Andriushchenko committed Sep 20, 2024
1 parent c23c119 commit ed86b17
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 113 deletions.
4 changes: 2 additions & 2 deletions paynt/parser/jani.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
2 changes: 1 addition & 1 deletion paynt/synthesizer/synthesizer_ar.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))

Expand Down
62 changes: 19 additions & 43 deletions payntbind/src/synthesis/quotient/ColoringSmt.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,37 +119,13 @@ ColoringSmt<ValueType>::ColoringSmt(
state_substitution_expr.push_back(substitution_expr);
}

// create choice substitutions
// std::vector<z3::expr_vector> choice_action_substitution_expr;
std::vector<z3::expr_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<z3::expr_vector> path_step_expression;
z3::expr_vector path_expression(ctx);
for(std::vector<bool> 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<const TerminalNode *>(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) {
Expand All @@ -160,31 +136,31 @@ ColoringSmt<ValueType>::ColoringSmt(
}
}

/*std::vector<z3::expr_vector> state_path_expresssion;
std::vector<z3::expr_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<z3::expr_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();
Expand Down
66 changes: 22 additions & 44 deletions payntbind/src/synthesis/quotient/TreeNode.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,13 +122,13 @@ std::shared_ptr<TreeNode> TreeNode::getChild(bool condition) const {
return condition ? child_true : child_false;
}

const TreeNode *TreeNode::getNodeOfPath(std::vector<bool> const& path, uint64_t step) const {
/*const TreeNode *TreeNode::getNodeOfPath(std::vector<bool> 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);
}
}*/



Expand Down Expand Up @@ -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<bool> const& path, z3::expr_vector & expression) const {
expression.push_back(action_expr);
uint64_t TerminalNode::getPathActionHole(std::vector<bool> const& path) {
return action_hole.hole;
}

void TerminalNode::loadPathExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector & expression) const {
expression.push_back(action_expr_harm);
}

void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {
void TerminalNode::substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {
//
}

z3::expr TerminalNode::substituteActionExpressionHarmonizing(std::vector<bool> 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<bool> const& path, uint64_t action) const {
return action_hole.solver_variable == (int)action;
}

void TerminalNode::loadAllHoles(std::vector<const Hole *> & holes) const {
holes[action_hole.hole] = &action_hole;
void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {
//
}

void TerminalNode::loadPathStepHoles(std::vector<bool> const& path, std::vector<std::vector<uint64_t>> & step_holes) const {
step_holes.push_back({action_hole.hole});
z3::expr TerminalNode::substituteActionExpressionHarmonizing(std::vector<bool> 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);
}


Expand Down Expand Up @@ -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<bool> 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<bool> const& path) {
return getChild(path[depth])->getPathActionHole(path);
}

void InnerNode::loadPathExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector & expression) const {

void InnerNode::substitutePrefixExpression(std::vector<bool> 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<bool> const& path, uint64_t action) const {
return getChild(path[depth])->substituteActionExpression(path,action);
}

void InnerNode::substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {
Expand All @@ -398,27 +397,6 @@ z3::expr InnerNode::substituteActionExpressionHarmonizing(std::vector<bool> cons
}



void InnerNode::loadAllHoles(std::vector<const Hole *> & 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<bool> const& path, std::vector<std::vector<uint64_t>> & step_holes) const {
std::vector<uint64_t> 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) {
Expand Down
42 changes: 19 additions & 23 deletions payntbind/src/synthesis/quotient/TreeNode.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,26 +105,26 @@ class TreeNode {
/** Retrieve true child of this node if the condition holds, get false child otherwise. */
std::shared_ptr<TreeNode> getChild(bool condition) const;
/** Execute the path and the corresponding node of the tree. */
const TreeNode *getNodeOfPath(std::vector<bool> const& path, uint64_t step) const;
// const TreeNode *getNodeOfPath(std::vector<bool> 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<std::tuple<uint64_t,std::string,std::string>> & 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<bool> const& path, z3::expr_vector & expression) const {}
/** Create expression for a harmonizing path. */
virtual void loadPathExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector & expression) const {}
/** TODO */
virtual void substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {}
virtual z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const { return z3::expr(ctx); }

virtual void loadAllHoles(std::vector<const Hole *> & holes) const {};
virtual void loadPathStepHoles(std::vector<bool> const& path, std::vector<std::vector<uint64_t>> & step_holes) const {};
/** Retrieve action hole associated with the path. */
virtual uint64_t getPathActionHole(std::vector<bool> const& path) {return 0;}

/** Add a step expression evaluated for a given state valuation. */
virtual void substitutePrefixExpression(std::vector<bool> 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<bool> 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<bool> 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<bool> 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 {}
Expand Down Expand Up @@ -173,15 +173,13 @@ class TerminalNode: public TreeNode {
void createHoles(Family& family) override;
void loadHoleInfo(std::vector<std::tuple<uint64_t,std::string,std::string>> & hole_info) const override;
void createPaths(z3::expr const& harmonizing_variable) override;
uint64_t getPathActionHole(std::vector<bool> const& path);

void loadPathExpression(std::vector<bool> const& path, z3::expr_vector & expression) const override;
void loadPathExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector & expression) const override;
void substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpression(std::vector<bool> const& path, uint64_t action) const override;
void substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const override;

void loadAllHoles(std::vector<const Hole *> & holes) const override;
void loadPathStepHoles(std::vector<bool> const& path, std::vector<std::vector<uint64_t>> & step_holes) const override;

void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override;
bool isPathEnabledInState(
std::vector<bool> const& path,
Expand Down Expand Up @@ -229,15 +227,13 @@ class InnerNode: public TreeNode {
void createHoles(Family& family) override;
void loadHoleInfo(std::vector<std::tuple<uint64_t,std::string,std::string>> & hole_info) const override;
void createPaths(z3::expr const& harmonizing_variable) override;
uint64_t getPathActionHole(std::vector<bool> const& path);

void loadPathExpression(std::vector<bool> const& path, z3::expr_vector & expression) const override;
void loadPathExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector & expression) const override;
void substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpression(std::vector<bool> const& path, uint64_t action) const override;
void substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const override;

void loadAllHoles(std::vector<const Hole *> & holes) const override;
void loadPathStepHoles(std::vector<bool> const& path, std::vector<std::vector<uint64_t>> & step_holes) const override;

void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override;
bool isPathEnabledInState(
std::vector<bool> const& path,
Expand Down

0 comments on commit ed86b17

Please sign in to comment.