From 1d0e5c11a4c52d5e75c4e2c384419a964100350e Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 7 Jul 2025 00:23:01 +0200 Subject: [PATCH 01/11] added constraints; tree contraint not working for now --- paynt/cli.py | 21 +++- paynt/family/constraints/constraints.py | 17 +++ paynt/family/constraints/prob_goal.py | 109 +++++++++++++++++ paynt/family/constraints/tree.py | 152 ++++++++++++++++++++++++ paynt/family/smt.py | 25 +++- paynt/synthesizer/synthesizer_cegis.py | 5 +- paynt/synthesizer/synthesizer_hybrid.py | 2 +- 7 files changed, 324 insertions(+), 7 deletions(-) create mode 100644 paynt/family/constraints/constraints.py create mode 100644 paynt/family/constraints/prob_goal.py create mode 100644 paynt/family/constraints/tree.py diff --git a/paynt/cli.py b/paynt/cli.py index 4b9acc850..53185faef 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -1,4 +1,3 @@ -import paynt.quotient.mdp_family from . import version import paynt.utils.timer @@ -10,12 +9,15 @@ import paynt.quotient.posmg import paynt.quotient.storm_pomdp_control import paynt.quotient.mdp +import paynt.quotient.mdp_family import paynt.synthesizer.synthesizer import paynt.synthesizer.synthesizer_cegis import paynt.synthesizer.policy_tree import paynt.synthesizer.decision_tree +import paynt.family.constraints.tree + import click import sys import os @@ -133,6 +135,16 @@ def setup_logger(log_path = None): "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True, help="counterexample generator", ) + +@click.option("--constraint", + type=click.Choice(['prob1', 'prob0', 'tree']), + default=None , show_default=True, + help="constraint type for CEGIS" +) +@click.option("--tree-nodes", default=None, type=int, + help="constraint tree: number of nodes in the decision tree (only for --constraint tree)") + + @click.option("--profiling", is_flag=True, default=False, help="run profiling") @@ -148,7 +160,7 @@ def paynt_run( mdp_discard_unreachable_choices, tree_depth, tree_enumeration, tree_map_scheduler, add_dont_care_action, constraint_bound, - ce_generator, + ce_generator, constraint, tree_nodes, profiling ): @@ -164,6 +176,7 @@ def paynt_run( paynt.quotient.quotient.Quotient.disable_expected_visits = disable_expected_visits paynt.synthesizer.synthesizer.Synthesizer.export_synthesis_filename_base = export_synthesis paynt.synthesizer.synthesizer_cegis.SynthesizerCEGIS.conflict_generator_type = ce_generator + paynt.synthesizer.synthesizer_cegis.SynthesizerCEGIS.constraint = constraint paynt.quotient.pomdp.PomdpQuotient.initial_memory_size = fsc_memory_size paynt.quotient.pomdp.PomdpQuotient.posterior_aware = posterior_aware paynt.quotient.decpomdp.DecPomdpQuotient.initial_memory_size = fsc_memory_size @@ -178,6 +191,10 @@ def paynt_run( paynt.synthesizer.decision_tree.SynthesizerDecisionTree.scheduler_path = tree_map_scheduler paynt.quotient.mdp.MdpQuotient.add_dont_care_action = add_dont_care_action + if constraint == "tree": + paynt.family.constraints.tree.DecisionTreeConstraint.tree_depth = tree_depth + paynt.family.constraints.tree.DecisionTreeConstraint.tree_nodes = tree_nodes + storm_control = None if storm_pomdp: storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl() diff --git a/paynt/family/constraints/constraints.py b/paynt/family/constraints/constraints.py new file mode 100644 index 000000000..f11b85808 --- /dev/null +++ b/paynt/family/constraints/constraints.py @@ -0,0 +1,17 @@ + +from paynt.family.constraints.tree import DecisionTreeConstraint +from paynt.family.constraints.prob_goal import ProbGoalConstraint + +class Constraints: + + @staticmethod + def create_constraint(constraint_type): + if constraint_type == "prob1": + return ProbGoalConstraint(prob=1) + elif constraint_type == "prob0": + return ProbGoalConstraint(prob=0) + elif constraint_type == "tree": + # TODO add tree size + return DecisionTreeConstraint() + else: + raise ValueError(f"Unknown constraint type: {constraint_type}") diff --git a/paynt/family/constraints/prob_goal.py b/paynt/family/constraints/prob_goal.py new file mode 100644 index 000000000..8bb78b655 --- /dev/null +++ b/paynt/family/constraints/prob_goal.py @@ -0,0 +1,109 @@ +"""Reach goal with prob>0 or prob=1.""" + +import z3 +import math +from stormpy import model_checking + +import logging +logger = logging.getLogger(__name__) + +class ProbGoalConstraint(): + def __init__(self, prob: int = 0): + assert prob in [0, 1], "ProbGoal requires prob to be either 0 or 1." + self.prob0 = (prob == 0) + + def build_constraint( + self, + variables, + quotient + ) -> z3.ExprRef: + + # We build the quotient here + quotient.build(quotient.family) + + transition_matrix = quotient.family.mdp.model.transition_matrix + + choice_to_assignment = quotient.coloring.getChoiceToAssignment() + + target_states = model_checking(quotient.family.mdp.model, quotient.specification.all_properties()[0].formula.subformula.subformula).get_truth_values() + + assertions = [] + + reachability_vars = [] + for state in range(transition_matrix.nr_columns): + reach_var = z3.Bool(f"reach_{state}") + reachability_vars.append(reach_var) + + if not self.prob0: + max_step_vars = [] + for state in range(transition_matrix.nr_columns): + max_step_var = z3.Int(f"max_step_{state}") + max_step_vars.append(max_step_var) + assertions.append(max_step_var >= 0) + + for state in range(transition_matrix.nr_columns): + if target_states.get(state): + assertions.append(reachability_vars[state]) + continue + + statement_for_state = [] + + rows = transition_matrix.get_rows_for_group(state) + for row in rows: + assignment = choice_to_assignment[row] + assignment_as_z3 = z3.And([ + variables[var] == x + for var, x in assignment + ]) + + reachability_vars_of_row = [] + max_step_vars_of_row = [] + + for entry in transition_matrix.get_row(row): + value = entry.value() + if value == 0: + continue + assert value > 0, "Transition probabilities must be positive." + to_state = entry.column + if to_state == state: + continue + reachability_vars_of_row.append(reachability_vars[to_state]) + max_step_vars_of_row.append(max_step_vars[to_state]) + statement_for_state.append(z3.Implies(assignment_as_z3, z3.And(reachability_vars_of_row))) + assertions.append( + z3.Implies( + assignment_as_z3, + z3.Or([max_step_vars[state] == x + 1 for x in max_step_vars_of_row]) + ) + ) + assertions.append(z3.Implies(reachability_vars[state], z3.And(statement_for_state))) + + assertions.append(z3.Implies(reachability_vars[state], max_step_vars[state] < transition_matrix.nr_columns)) + + + # else: + # assertions.append( + # z3.Implies( + # z3.And(reachability_vars[to_state], assignment_as_z3), + # z3.And(reachability_vars[state]) + # ) + # ) + # max_step_vars_of_row.append(max_step_vars[to_state]) + + # if not self.prob0: + # assertions.append( + # z3.Implies( + # reachability_vars[state], + # z3.Or([max_step_vars[state] > x for x in max_step_vars_of_row]) + # ) + # ) + + initial_state = quotient.family.mdp.model.initial_states[0] + assert len(quotient.family.mdp.model.initial_states) == 1, "ProbGoal only supports single initial states." + + assertions.append(reachability_vars[initial_state]) + logger.info("Done building assertions for ProbGoal.") + return assertions + + # def show_result(self, model, solver, **args): + # print([(x, model[x]) for x in model if x.name().startswith("reach_")]) diff --git a/paynt/family/constraints/tree.py b/paynt/family/constraints/tree.py new file mode 100644 index 000000000..94bebe2d6 --- /dev/null +++ b/paynt/family/constraints/tree.py @@ -0,0 +1,152 @@ +"""A classic decision tree.""" + +import z3 + + +def piecewise_select(array, z3_int): + """Select an element of an array based on a z3 integer.""" + return z3.Sum([z3.If(z3_int == i, array[i], 0) for i in range(len(array))]) + + +def get_property_names(variable_name): + return [ + x.strip().split("=")[0].replace("!", "") + for x in variable_name[ + variable_name.find("[") + 1 : variable_name.find("]") + ].split("&") + ] + + +def get_property_values(variable_name): + return [ + int(x.strip().split("=")[1]) if "=" in x else (0 if x.strip()[0] == "!" else 1) + for x in variable_name[ + variable_name.find("[") + 1 : variable_name.find("]") + ].split("&") + ] + + +class DecisionTreeConstraint(): + + tree_depth: int + + tree_nodes: int | None + + def __init__(self): + pass + + def build_constraint(self, variables, quotient): + tree_depth = self.tree_depth + self.variables = variables + num_enabled_nodes = self.tree_nodes + + # variables have names of the form + # A([picked0=1 & picked1=0 & picked2=1 & picked3=1 & picked4=0 & picked5=1 & picked6=1 & x=3 & y=2],0 + first_variable_name = str(variables[0]) + if "A([" not in first_variable_name: + raise ValueError( + "Variables must have properties (e.g., generated from POMDPs.)." + ) + property_names = get_property_names(first_variable_name) + num_properties = len(property_names) + + property_ranges = [(1e6, -1e6) for _ in range(num_properties)] + for variable in variables: + property_values = get_property_values(str(variable)) + for i in range(num_properties): + property_ranges[i] = ( + min(property_ranges[i][0], property_values[i]), + max(property_ranges[i][1], property_values[i]), + ) + + # create a function + max_action_size = max([len(quotient.family.hole_options(hole)) for hole in range(len(variables))]) + decision_func = z3.Function( + "decision", *[z3.IntSort()] * num_properties, z3.BitVecSort(max_action_size) + ) + + decision_func_int = z3.Function( + "decision", *[z3.IntSort()] * num_properties, z3.IntSort() + ) + + constraints = [] + + # tree is structured as follows + # 0 + # 1 2 + # 3 4 5 6 + # 7 8 9 10 11 12 13 14 + + num_nodes = 2**tree_depth - 1 + leaf_values = [ + z3.BitVec(f"leaf_{i}", max_action_size) for i in range(num_nodes + 1) + ] + + # make weight nodes for constraints + node_property = [] + node_constants = [] + for i in range(num_nodes): + # weight per variable + prop_index = z3.Int(f"node_{i}") + + # prop index must be in range + constraints.append(prop_index >= 0) + constraints.append(prop_index < num_properties) + + node_property.append(prop_index) + constant_var = z3.Int(f"const_{i}") + node_constants.append(constant_var) + constraints.append(constant_var >= 0) + + # if the constant of this node is > 0, this is also true for the parent + # this breaks symmetry for disabled nodes + if i > 0: + constraints.append( + z3.Implies(node_constants[i] > 0, node_constants[(i - 1) // 2] > 0) + ) + # if the constant is 0, the property must be 0 + constraints.append( + z3.Implies(node_constants[i] == 0, node_property[i] == 0) + ) + + # only num_enabled_nodes nodes can have constant > 0 + if num_enabled_nodes is not None: + constraints.append( + z3.Sum([z3.If(node_constants[i] > 0, 1, 0) for i in range(num_nodes)]) + == num_enabled_nodes + ) + + def decision_at_node(node: int, properties): + return z3.Or( + node_constants[node] == 0, + z3.Sum( + [ + z3.If(node_property[node] == i, properties[i], 0) + for i in range(num_properties) + ] + ) + >= node_constants[node], + ) + + def traverse_tree(node: int, properties: list[z3.Int]): + if node >= num_nodes: + return leaf_values[node - num_nodes] + else: + left = traverse_tree(2 * node + 1, properties) + right = traverse_tree(2 * node + 2, properties) + return z3.If(decision_at_node(node, properties), left, right) + + decision_variables = [z3.Int(f"decision_{i}") for i in range(num_properties)] + constraints.append( + z3.ForAll( + decision_variables, + traverse_tree(0, decision_variables) + == decision_func(*decision_variables), + ) + ) + + for variable in variables: + property_values = get_property_values(str(variable)) + constraints.append(variable == decision_func_int(*property_values)) + return constraints + diff --git a/paynt/family/smt.py b/paynt/family/smt.py index e1feacae5..37a203037 100644 --- a/paynt/family/smt.py +++ b/paynt/family/smt.py @@ -1,6 +1,8 @@ import sys import z3 +from paynt.family.constraints.constraints import Constraints + # import pycvc5 if installed import importlib if importlib.util.find_spec('pycvc5') is not None: @@ -49,6 +51,17 @@ def __init__(self, smt_solver, family): else: pass + if smt_solver.constraint is not None: + + constraint = Constraints.create_constraint(smt_solver.constraint) + + constraint_smt_clauses = constraint.build_constraint( + self.smt_solver.solver_vars, + self.smt_solver.quotient + ) + + encoding = z3.And(encoding, *constraint_smt_clauses) + self.hole_clauses = hole_clauses self.encoding = encoding @@ -86,7 +99,7 @@ def pick_assignment(self): class SmtSolver(): - def __init__(self, family): + def __init__(self, quotient, constraint=None): # SMT solver containing description of the unexplored design space self.solver = None @@ -103,8 +116,14 @@ def __init__(self, family): # current depth of push/pop solving self.solver_depth = 0 + # initial constraint for the design space + self.constraint = constraint + + self.quotient = quotient + family = quotient.family + # choose solver - if "pycvc5" in sys.modules: + if "pycvc5" in sys.modules and self.constraint is None: logger.debug("using CVC5 for SMT solving.") self.use_cvc = True else: @@ -115,7 +134,7 @@ def __init__(self, family): self.solver_clauses = [] if self.use_python_z3: self.solver = z3.Solver() - self.solver_vars = [z3.Int(hole) for hole in range(family.num_holes)] + self.solver_vars = [z3.Int(family.hole_name(hole)) for hole in range(family.num_holes)] elif self.use_cvc: self.solver = pycvc5.Solver() self.solver.setOption("produce-models", "true") diff --git a/paynt/synthesizer/synthesizer_cegis.py b/paynt/synthesizer/synthesizer_cegis.py index 95ab4cbc4..816bd0d7b 100644 --- a/paynt/synthesizer/synthesizer_cegis.py +++ b/paynt/synthesizer/synthesizer_cegis.py @@ -12,6 +12,9 @@ class SynthesizerCEGIS(paynt.synthesizer.synthesizer.Synthesizer): # CLI argument selecting conflict generator conflict_generator_type = None + # CLI argument for setting initial constraint on the design space + constraint = None + def __init__(self, quotient): super().__init__(quotient) @@ -92,7 +95,7 @@ def synthesize_one(self, family): self.conflict_generator.initialize() # use sketch design space as a SAT baseline (TODO why?) - smt_solver = paynt.family.smt.SmtSolver(self.quotient.family) + smt_solver = paynt.family.smt.SmtSolver(self.quotient, self.constraint) # CEGIS loop assignment = smt_solver.pick_assignment(family) diff --git a/paynt/synthesizer/synthesizer_hybrid.py b/paynt/synthesizer/synthesizer_hybrid.py index da0485865..ee9c0cd83 100644 --- a/paynt/synthesizer/synthesizer_hybrid.py +++ b/paynt/synthesizer/synthesizer_hybrid.py @@ -94,7 +94,7 @@ def method_name(self): def synthesize_one(self, family): self.conflict_generator.initialize() - smt_solver = paynt.family.smt.SmtSolver(self.quotient.family) + smt_solver = paynt.family.smt.SmtSolver(self.quotient) # AR-CEGIS loop families = [family] From d1bbff0b8262f78b4945b3a88607855867c76105 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 7 Jul 2025 11:00:16 +0200 Subject: [PATCH 02/11] trying to fix the tree constraint --- paynt/family/constraints/tree.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/paynt/family/constraints/tree.py b/paynt/family/constraints/tree.py index 94bebe2d6..7d202d795 100644 --- a/paynt/family/constraints/tree.py +++ b/paynt/family/constraints/tree.py @@ -62,13 +62,13 @@ def build_constraint(self, variables, quotient): # create a function max_action_size = max([len(quotient.family.hole_options(hole)) for hole in range(len(variables))]) decision_func = z3.Function( - "decision", *[z3.IntSort()] * num_properties, z3.BitVecSort(max_action_size) - ) - - decision_func_int = z3.Function( "decision", *[z3.IntSort()] * num_properties, z3.IntSort() ) + # decision_func_int = z3.Function( + # "decision", *[z3.IntSort()] * num_properties, z3.IntSort() + # ) + constraints = [] # tree is structured as follows @@ -79,7 +79,7 @@ def build_constraint(self, variables, quotient): num_nodes = 2**tree_depth - 1 leaf_values = [ - z3.BitVec(f"leaf_{i}", max_action_size) for i in range(num_nodes + 1) + z3.Int(f"leaf_{i}") for i in range(num_nodes + 1) ] # make weight nodes for constraints @@ -147,6 +147,6 @@ def traverse_tree(node: int, properties: list[z3.Int]): for variable in variables: property_values = get_property_values(str(variable)) - constraints.append(variable == decision_func_int(*property_values)) + constraints.append(variable == decision_func(*property_values)) return constraints From e9f56cb1ca4bcf5b9d06f5bc26cbb67216f1f6f2 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 7 Jul 2025 12:35:52 +0200 Subject: [PATCH 03/11] added flexibletree constraint --- paynt/cli.py | 5 +- paynt/family/constraints/constraints.py | 3 +- paynt/family/constraints/flexibletree.py | 264 +++++++++++++++++++++++ paynt/family/constraints/tree.py | 2 +- 4 files changed, 268 insertions(+), 6 deletions(-) create mode 100644 paynt/family/constraints/flexibletree.py diff --git a/paynt/cli.py b/paynt/cli.py index 53185faef..f1e6d1536 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -16,7 +16,7 @@ import paynt.synthesizer.policy_tree import paynt.synthesizer.decision_tree -import paynt.family.constraints.tree +import paynt.family.constraints.flexibletree import click import sys @@ -192,8 +192,7 @@ def paynt_run( paynt.quotient.mdp.MdpQuotient.add_dont_care_action = add_dont_care_action if constraint == "tree": - paynt.family.constraints.tree.DecisionTreeConstraint.tree_depth = tree_depth - paynt.family.constraints.tree.DecisionTreeConstraint.tree_nodes = tree_nodes + paynt.family.constraints.flexibletree.DecisionTreeConstraint.tree_nodes = tree_nodes storm_control = None if storm_pomdp: diff --git a/paynt/family/constraints/constraints.py b/paynt/family/constraints/constraints.py index f11b85808..134a14353 100644 --- a/paynt/family/constraints/constraints.py +++ b/paynt/family/constraints/constraints.py @@ -1,5 +1,5 @@ -from paynt.family.constraints.tree import DecisionTreeConstraint +from paynt.family.constraints.flexibletree import DecisionTreeConstraint from paynt.family.constraints.prob_goal import ProbGoalConstraint class Constraints: @@ -11,7 +11,6 @@ def create_constraint(constraint_type): elif constraint_type == "prob0": return ProbGoalConstraint(prob=0) elif constraint_type == "tree": - # TODO add tree size return DecisionTreeConstraint() else: raise ValueError(f"Unknown constraint type: {constraint_type}") diff --git a/paynt/family/constraints/flexibletree.py b/paynt/family/constraints/flexibletree.py new file mode 100644 index 000000000..bd7b0effc --- /dev/null +++ b/paynt/family/constraints/flexibletree.py @@ -0,0 +1,264 @@ +"""A classic decision tree.""" + +import z3 +from itertools import product, chain +import os + + +def piecewise_select(array, z3_int): + """Select an element of an array based on a z3 integer.""" + return z3.Sum([z3.If(z3_int == i, array[i], 0) for i in range(len(array))]) + + +def get_property_names(variable_name): + return [ + x.strip().split("=")[0].replace("!", "") + for x in variable_name[ + variable_name.find("[") + 1 : variable_name.find("]") + ].split("&") + ] + + +def get_property_values(variable_name): + return [ + int(x.strip().split("=")[1]) if "=" in x else (0 if x.strip()[0] == "!" else 1) + for x in variable_name[ + variable_name.find("[") + 1 : variable_name.find("]") + ].split("&") + ] + + +class DecisionTreeConstraint(): + + tree_nodes: int | None + + def __init__(self): + self.policy_vars = None + self.labels = None + self.label_to_index = None + self.left_child_ranges = None + self.right_child_ranges = None + + + def build_constraint(self, variables, quotient): + self.variables = variables + num_nodes = self.tree_nodes + + policy_indices = list(range(len(variables))) + policy_vars = [variables[i] for i in policy_indices] + self.policy_vars = policy_vars + + # Collect all action labels and put them into an order + labels = list( + dict.fromkeys( + chain( + *[quotient.family.hole_to_option_labels[i] for i in policy_indices] + ) + ) + ) + print(labels) + label_to_index = {label: i for i, label in enumerate(labels)} + self.labels = labels + self.label_to_index = label_to_index + hole_to_label_indices = [] + # assert 2**num_bits > len(labels) + + # Check that the available action labels of policy vars are consistent + for i in policy_indices: + hole_to_label_indices.append( + [ + label_to_index[label] + for label in quotient.family.hole_to_option_labels[i] + ] + ) + + # variables have names of the form + # A([picked0=1 & picked1=0 & picked2=1 & picked3=1 & picked4=0 & picked5=1 & picked6=1 & x=3 & y=2],0 + first_variable_name = str(policy_vars[0]) + if "A([" not in first_variable_name: + raise ValueError( + "Variables must have properties (e.g., generated from POMDPs.)." + ) + property_names = get_property_names(first_variable_name) + num_properties = len(property_names) + + property_ranges = [(1e6, -1e6) for _ in range(num_properties)] + for variable in policy_vars: + property_values = get_property_values(str(variable)) + for i in range(num_properties): + property_ranges[i] = ( + min(property_ranges[i][0], property_values[i]), + max(property_ranges[i][1], property_values[i]), + ) + + constraints = [] + + # create a function for each node + decision_functions = [] + for i in range(num_nodes): + decision_functions.append( + z3.Function( + f"decision_{i}", + *[z3.IntSort()] * num_properties, + z3.IntSort(), + ) + ) + + # Left child is in range even([i+1, min(2i, num_nodes-1)]) + # Right child is in range odd([i+2, min(2i+1, num_nodes)]) + self.left_child_ranges = [ + [j for j in range(i + 1, min(2 * (i + 1), num_nodes)) if j % 2 == 1] + for i in range(num_nodes) + ] + self.right_child_ranges = [ + [j for j in range(i + 2, min(2 * (i + 1) + 1, num_nodes)) if j % 2 == 0] + for i in range(num_nodes) + ] + + # make weight nodes for constraints + node_constants = [] + property_indices = [] + node_is_leaf = [] + left_children = [] + right_children = [] + + for i in range(num_nodes): + # Is this node a leaf? + is_leaf = z3.Bool(f"leaf_{i}") + node_is_leaf.append(is_leaf) + + # The constant of a node + constant_var = z3.Int(f"const_{i}") + node_constants.append(constant_var) + + # The property index of a node + prop_index = z3.Int(f"prop_index_{i}") + # Must be in range + constraints.append(prop_index >= 0) + # print(num_properties) + constraints.append(prop_index < num_properties) + property_indices.append(prop_index) + + constraints.append(constant_var >= 0) + constraints.append( + z3.If( + is_leaf, + constant_var < len(labels), + constant_var <= piecewise_select( + [z3.IntVal(x[1]) for x in property_ranges], + prop_index, + ), + ) + ) + + left_child = z3.Int(f"left_{i}") + left_children.append(left_child) + right_child = z3.Int(f"right_{i}") + right_children.append(right_child) + # If this node is a leaf, the left and right children must be 0 + + constraints.append( + z3.If( + is_leaf, + left_child == 0, + left_child <= len(self.left_child_ranges[i]), + ) + ) + constraints.append( + z3.If( + is_leaf, + right_child == 0, + right_child <= len(self.right_child_ranges[i]), + ) + ) + constraints.append(z3.Implies(is_leaf, prop_index == 0)) + + all_property_values = [ + get_property_values(str(variable)) + for variable in enumerate(policy_vars) + ] + + for values in all_property_values: + prop_vals = [z3.IntVal(v) for v in values] + constraints.append( + z3.If( + is_leaf, + decision_functions[i](*prop_vals) == constant_var, + z3.If( + piecewise_select(prop_vals, prop_index) >= constant_var, + z3.Or( + *[ + z3.And( + left_child == j, + decision_functions[i](*prop_vals) + == decision_functions[ + self.left_child_ranges[i][j] + ](*prop_vals), + ) + for j in range(len(self.left_child_ranges[i])) + ] + ), + z3.Or( + *[ + z3.And( + right_child == j, + decision_functions[i](*prop_vals) + == decision_functions[ + self.right_child_ranges[i][j] + ](*prop_vals), + ) + for j in range(len(self.right_child_ranges[i])) + ] + ), + ), + ) + ) + + # each tree has (num_nodes+1) / 2 leaves + constraints.append(z3.Sum(node_is_leaf) == (num_nodes + 1) // 2) + # each node, except 0, must have a parent, that is before it + + for i in range(1, num_nodes): + # identify the nodes that have i in left_child_ranges or right_child_ranges + left_children_ranges = [ + j for j in range(num_nodes) if i in self.left_child_ranges[j] + ] + right_children_ranges = [ + j for j in range(num_nodes) if i in self.right_child_ranges[j] + ] + # i is left_child of one of the left_children or right_child of one of the right_children + parent_constraint = z3.Or( + *[ + z3.And( + left_children[x] == self.left_child_ranges[x].index(i), + z3.Not(node_is_leaf[x]), + ) + for x in left_children_ranges + if i in self.left_child_ranges[x] + ] + + [ + z3.And( + right_children[x] == self.right_child_ranges[x].index(i), + z3.Not(node_is_leaf[x]), + ) + for x in right_children_ranges + if i in self.right_child_ranges[x] + ] + ) + constraints.append(parent_constraint) + + for i, variable in enumerate(policy_vars): + label_range = quotient.family.hole_to_option_labels[policy_indices[i]] + if label_range == labels: + # The semantics of the variable is the same as the decision tree's + property_values = get_property_values(str(variable)) + constraints.append(variable == decision_functions[0](*property_values)) + else: + # We need to map the decision tree's value to the label index + label_indices = [label_to_index[label] for label in label_range] + property_values = get_property_values(str(variable)) + x = decision_functions[0](*property_values) + for index, label_index in enumerate(label_indices): + constraints.append((variable == index) == (x == label_index)) + + return constraints diff --git a/paynt/family/constraints/tree.py b/paynt/family/constraints/tree.py index 7d202d795..e579facfd 100644 --- a/paynt/family/constraints/tree.py +++ b/paynt/family/constraints/tree.py @@ -26,7 +26,7 @@ def get_property_values(variable_name): ] -class DecisionTreeConstraint(): +class DecisionTreeConstraintOld(): tree_depth: int From 3512da3f0496451491bc8a5b25edca018d83d717 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 7 Jul 2025 23:05:27 +0200 Subject: [PATCH 04/11] updated reachability contraint --- paynt/family/constraints/prob_goal.py | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/paynt/family/constraints/prob_goal.py b/paynt/family/constraints/prob_goal.py index 8bb78b655..9b9625a3f 100644 --- a/paynt/family/constraints/prob_goal.py +++ b/paynt/family/constraints/prob_goal.py @@ -35,15 +35,16 @@ def build_constraint( reachability_vars.append(reach_var) if not self.prob0: - max_step_vars = [] + min_step_vars = [] for state in range(transition_matrix.nr_columns): - max_step_var = z3.Int(f"max_step_{state}") - max_step_vars.append(max_step_var) - assertions.append(max_step_var >= 0) + min_step_var = z3.Int(f"min_step_{state}") + min_step_vars.append(min_step_var) + assertions.append(min_step_var >= 0) for state in range(transition_matrix.nr_columns): if target_states.get(state): assertions.append(reachability_vars[state]) + assertions.append(min_step_vars[state] == 0) continue statement_for_state = [] @@ -52,12 +53,12 @@ def build_constraint( for row in rows: assignment = choice_to_assignment[row] assignment_as_z3 = z3.And([ - variables[var] == x + variables[var] == z3.IntVal(x) for var, x in assignment ]) reachability_vars_of_row = [] - max_step_vars_of_row = [] + min_step_vars_of_row = [] for entry in transition_matrix.get_row(row): value = entry.value() @@ -68,17 +69,20 @@ def build_constraint( if to_state == state: continue reachability_vars_of_row.append(reachability_vars[to_state]) - max_step_vars_of_row.append(max_step_vars[to_state]) + min_step_vars_of_row.append(min_step_vars[to_state]) statement_for_state.append(z3.Implies(assignment_as_z3, z3.And(reachability_vars_of_row))) assertions.append( z3.Implies( - assignment_as_z3, - z3.Or([max_step_vars[state] == x + 1 for x in max_step_vars_of_row]) + z3.And(reachability_vars[state], assignment_as_z3), + z3.And( + z3.Or([min_step_vars[state] == x + 1 for x in min_step_vars_of_row]), + z3.And([min_step_vars[state] <= x + 1 for x in min_step_vars_of_row]) + ) ) ) assertions.append(z3.Implies(reachability_vars[state], z3.And(statement_for_state))) - - assertions.append(z3.Implies(reachability_vars[state], max_step_vars[state] < transition_matrix.nr_columns)) + else: + assert False, "prob0 not implemented." # else: From d98f870a792d2425e8194f93c2a0cc7ab22c345a Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 9 Jul 2025 16:01:32 +0200 Subject: [PATCH 05/11] added costs contraint --- paynt/cli.py | 10 ++++- paynt/family/constraints/constraints.py | 3 ++ paynt/family/constraints/costs.py | 56 ++++++++++++++++++++++++ paynt/family/constraints/flexibletree.py | 6 ++- 4 files changed, 72 insertions(+), 3 deletions(-) create mode 100644 paynt/family/constraints/costs.py diff --git a/paynt/cli.py b/paynt/cli.py index f1e6d1536..1484d08f9 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -17,6 +17,7 @@ import paynt.synthesizer.decision_tree import paynt.family.constraints.flexibletree +import paynt.family.constraints.costs import click import sys @@ -137,12 +138,14 @@ def setup_logger(log_path = None): ) @click.option("--constraint", - type=click.Choice(['prob1', 'prob0', 'tree']), + type=click.Choice(['prob1', 'prob0', 'tree', 'costs']), default=None , show_default=True, help="constraint type for CEGIS" ) @click.option("--tree-nodes", default=None, type=int, help="constraint tree: number of nodes in the decision tree (only for --constraint tree)") +@click.option("--costs-threshold", default=None, type=int, + help="costs constraint: threshold for costs (only for --constraint costs)") @click.option("--profiling", is_flag=True, default=False, @@ -160,7 +163,7 @@ def paynt_run( mdp_discard_unreachable_choices, tree_depth, tree_enumeration, tree_map_scheduler, add_dont_care_action, constraint_bound, - ce_generator, constraint, tree_nodes, + ce_generator, constraint, tree_nodes, costs_threshold, profiling ): @@ -193,6 +196,9 @@ def paynt_run( if constraint == "tree": paynt.family.constraints.flexibletree.DecisionTreeConstraint.tree_nodes = tree_nodes + elif constraint == "costs": + paynt.family.constraints.costs.CostsConstraint.costs_threshold = costs_threshold + paynt.family.constraints.costs.CostsConstraint.model_folder = project storm_control = None if storm_pomdp: diff --git a/paynt/family/constraints/constraints.py b/paynt/family/constraints/constraints.py index 134a14353..4fca69f5b 100644 --- a/paynt/family/constraints/constraints.py +++ b/paynt/family/constraints/constraints.py @@ -1,6 +1,7 @@ from paynt.family.constraints.flexibletree import DecisionTreeConstraint from paynt.family.constraints.prob_goal import ProbGoalConstraint +from paynt.family.constraints.costs import CostsConstraint class Constraints: @@ -12,5 +13,7 @@ def create_constraint(constraint_type): return ProbGoalConstraint(prob=0) elif constraint_type == "tree": return DecisionTreeConstraint() + elif constraint_type == "costs": + return CostsConstraint() else: raise ValueError(f"Unknown constraint type: {constraint_type}") diff --git a/paynt/family/constraints/costs.py b/paynt/family/constraints/costs.py new file mode 100644 index 000000000..d2f1645f7 --- /dev/null +++ b/paynt/family/constraints/costs.py @@ -0,0 +1,56 @@ +import z3 + +import logging +import os +logger = logging.getLogger(__name__) + + +class CostsConstraint(): + + costs_threshold = 0 + model_folder : str + + COSTS_FILE = "sketch.costs" + + def __init__(self): + pass + + def build_constraint( + self, + variables, + quotient + ) -> z3.ExprRef: + # We build the quotient here + + assertions = [] + + lines = None + costs_path = os.path.join(self.model_folder, self.COSTS_FILE) + with open(costs_path, "r") as f: + lines = f.readlines() + + cost_vars = [] + line_index = 0 + for hole in range(quotient.family.num_holes): + for option in range(quotient.family.hole_num_options(hole)): + hole_name = quotient.family.hole_name(hole) + cost_var = z3.Int(f"cost_{hole_name}_{option}") + cost_vars.append(cost_var) + line = lines[line_index].strip() + line_index += 1 + line_hole, line_option, cost_value = line.split() + assert line_hole == hole_name, f"Expected hole {hole_name}, got {line_hole}" + assert int(line_option) == option, f"Expected option {option}, got {line_option}" + + assertions.append( + z3.If( + variables[hole] == option, + cost_var == cost_value, + cost_var == 0 + ) + ) + + # Add constraint: sum of cost_vars <= costs_threshold + assertions.append(z3.Sum(cost_vars) <= self.costs_threshold) + return assertions + \ No newline at end of file diff --git a/paynt/family/constraints/flexibletree.py b/paynt/family/constraints/flexibletree.py index bd7b0effc..afc1491e0 100644 --- a/paynt/family/constraints/flexibletree.py +++ b/paynt/family/constraints/flexibletree.py @@ -40,7 +40,11 @@ def __init__(self): self.right_child_ranges = None - def build_constraint(self, variables, quotient): + def build_constraint( + self, + variables, + quotient + ) -> z3.ExprRef: self.variables = variables num_nodes = self.tree_nodes From cdac883eaf0b88e48384d834bf2e135b1418650d Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 9 Jul 2025 16:23:53 +0200 Subject: [PATCH 06/11] type update --- paynt/family/constraints/costs.py | 2 +- paynt/family/constraints/flexibletree.py | 2 +- paynt/family/constraints/prob_goal.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/paynt/family/constraints/costs.py b/paynt/family/constraints/costs.py index d2f1645f7..526d52b6c 100644 --- a/paynt/family/constraints/costs.py +++ b/paynt/family/constraints/costs.py @@ -19,7 +19,7 @@ def build_constraint( self, variables, quotient - ) -> z3.ExprRef: + ): # We build the quotient here assertions = [] diff --git a/paynt/family/constraints/flexibletree.py b/paynt/family/constraints/flexibletree.py index afc1491e0..d1008821d 100644 --- a/paynt/family/constraints/flexibletree.py +++ b/paynt/family/constraints/flexibletree.py @@ -44,7 +44,7 @@ def build_constraint( self, variables, quotient - ) -> z3.ExprRef: + ): self.variables = variables num_nodes = self.tree_nodes diff --git a/paynt/family/constraints/prob_goal.py b/paynt/family/constraints/prob_goal.py index 9b9625a3f..eab36d8ac 100644 --- a/paynt/family/constraints/prob_goal.py +++ b/paynt/family/constraints/prob_goal.py @@ -16,7 +16,7 @@ def build_constraint( self, variables, quotient - ) -> z3.ExprRef: + ): # We build the quotient here quotient.build(quotient.family) From 20f001760b9667559df243a4f3485f0f1d52cc62 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 9 Jul 2025 20:22:56 +0200 Subject: [PATCH 07/11] added explicit type conversion --- paynt/family/constraints/costs.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/paynt/family/constraints/costs.py b/paynt/family/constraints/costs.py index 526d52b6c..35577330e 100644 --- a/paynt/family/constraints/costs.py +++ b/paynt/family/constraints/costs.py @@ -45,7 +45,7 @@ def build_constraint( assertions.append( z3.If( variables[hole] == option, - cost_var == cost_value, + cost_var == int(cost_value), cost_var == 0 ) ) From 81965cc0679fb8a96bd08657128589f2b007d8a0 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 15 Jul 2025 17:21:59 +0200 Subject: [PATCH 08/11] added missing __init__.py --- paynt/family/constraints/__init__.py | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 paynt/family/constraints/__init__.py diff --git a/paynt/family/constraints/__init__.py b/paynt/family/constraints/__init__.py new file mode 100644 index 000000000..343a1ca8c --- /dev/null +++ b/paynt/family/constraints/__init__.py @@ -0,0 +1,10 @@ +__version__ = "unknown" + +try: + from .._version import __version__ +except ImportError: + # We're running in a tree that doesn't have a _version.py, so we don't know what our version is. + pass + +def version(): + return __version__ \ No newline at end of file From 1b887a07d15eb732a98bb723204ec0672b8c8bea Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 16 Jul 2025 12:48:01 +0200 Subject: [PATCH 09/11] added support for prob0 constraints --- paynt/family/constraints/prob_goal.py | 67 +++++++++++++++++---------- paynt/family/smt.py | 1 + 2 files changed, 44 insertions(+), 24 deletions(-) diff --git a/paynt/family/constraints/prob_goal.py b/paynt/family/constraints/prob_goal.py index eab36d8ac..44708e8d2 100644 --- a/paynt/family/constraints/prob_goal.py +++ b/paynt/family/constraints/prob_goal.py @@ -29,6 +29,9 @@ def build_constraint( assertions = [] + initial_state = quotient.family.mdp.model.initial_states[0] + assert len(quotient.family.mdp.model.initial_states) == 1, "ProbGoal only supports single initial states." + reachability_vars = [] for state in range(transition_matrix.nr_columns): reach_var = z3.Bool(f"reach_{state}") @@ -82,32 +85,48 @@ def build_constraint( ) assertions.append(z3.Implies(reachability_vars[state], z3.And(statement_for_state))) else: - assert False, "prob0 not implemented." - - - # else: - # assertions.append( - # z3.Implies( - # z3.And(reachability_vars[to_state], assignment_as_z3), - # z3.And(reachability_vars[state]) - # ) - # ) - # max_step_vars_of_row.append(max_step_vars[to_state]) - - # if not self.prob0: - # assertions.append( - # z3.Implies( - # reachability_vars[state], - # z3.Or([max_step_vars[state] > x for x in max_step_vars_of_row]) - # ) - # ) + backwards_assertions = [[] for _ in range(transition_matrix.nr_columns)] + target_state_assertions = [] + for state in range(transition_matrix.nr_columns): + if target_states.get(state): + target_state_assertions.append(reachability_vars[state]) + continue + + statement_for_state = [] + + rows = transition_matrix.get_rows_for_group(state) + for row in rows: + assignment = choice_to_assignment[row] + assignment_as_z3 = z3.And([ + variables[var] == z3.IntVal(x) + for var, x in assignment + ]) - initial_state = quotient.family.mdp.model.initial_states[0] - assert len(quotient.family.mdp.model.initial_states) == 1, "ProbGoal only supports single initial states." + reachability_vars_of_row = [] + + for entry in transition_matrix.get_row(row): + value = entry.value() + if value == 0: + continue + assert value > 0, "Transition probabilities must be positive." + to_state = entry.column + if to_state == state: + continue + reachability_vars_of_row.append(reachability_vars[to_state]) + backwards_assertions[to_state].append( + z3.And(assignment_as_z3, reachability_vars[state]) + ) + for to_state, x in enumerate(backwards_assertions): + if to_state == initial_state: + continue + assertions.append( + z3.Implies( + reachability_vars[to_state], + z3.Or(x) + ) + ) + assertions.append(z3.Or(target_state_assertions)) assertions.append(reachability_vars[initial_state]) logger.info("Done building assertions for ProbGoal.") return assertions - - # def show_result(self, model, solver, **args): - # print([(x, model[x]) for x in model if x.name().startswith("reach_")]) diff --git a/paynt/family/smt.py b/paynt/family/smt.py index 37a203037..e2df29678 100644 --- a/paynt/family/smt.py +++ b/paynt/family/smt.py @@ -53,6 +53,7 @@ def __init__(self, smt_solver, family): if smt_solver.constraint is not None: + logger.info(f"Adding constraint {smt_solver.constraint} to the encoding.") constraint = Constraints.create_constraint(smt_solver.constraint) constraint_smt_clauses = constraint.build_constraint( From 15c7de52ca9c7017f6b76643e9ef98375ba8438a Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 21 Jul 2025 14:58:10 +0200 Subject: [PATCH 10/11] updated prob0 constraint --- paynt/family/constraints/prob_goal.py | 33 +++++++++++++++------------ 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/paynt/family/constraints/prob_goal.py b/paynt/family/constraints/prob_goal.py index 44708e8d2..0853b2a41 100644 --- a/paynt/family/constraints/prob_goal.py +++ b/paynt/family/constraints/prob_goal.py @@ -85,11 +85,16 @@ def build_constraint( ) assertions.append(z3.Implies(reachability_vars[state], z3.And(statement_for_state))) else: - backwards_assertions = [[] for _ in range(transition_matrix.nr_columns)] - target_state_assertions = [] + min_step_vars = [] + for state in range(transition_matrix.nr_columns): + min_step_var = z3.Int(f"min_step_{state}") + min_step_vars.append(min_step_var) + assertions.append(min_step_var >= 0) + for state in range(transition_matrix.nr_columns): if target_states.get(state): - target_state_assertions.append(reachability_vars[state]) + assertions.append(reachability_vars[state]) + assertions.append(min_step_vars[state] == 0) continue statement_for_state = [] @@ -103,6 +108,7 @@ def build_constraint( ]) reachability_vars_of_row = [] + min_step_vars_of_row = [] for entry in transition_matrix.get_row(row): value = entry.value() @@ -113,19 +119,18 @@ def build_constraint( if to_state == state: continue reachability_vars_of_row.append(reachability_vars[to_state]) - backwards_assertions[to_state].append( - z3.And(assignment_as_z3, reachability_vars[state]) + min_step_vars_of_row.append(min_step_vars[to_state]) + statement_for_state.append(z3.Implies(assignment_as_z3, z3.Or(reachability_vars_of_row))) + assertions.append( + z3.Implies( + z3.And(reachability_vars[state], assignment_as_z3), + z3.And( + z3.Or([min_step_vars[state] == x + 1 for x in min_step_vars_of_row]), + z3.And([min_step_vars[state] <= x + 1 for x in min_step_vars_of_row]) + ) ) - for to_state, x in enumerate(backwards_assertions): - if to_state == initial_state: - continue - assertions.append( - z3.Implies( - reachability_vars[to_state], - z3.Or(x) ) - ) - assertions.append(z3.Or(target_state_assertions)) + assertions.append(z3.Implies(reachability_vars[state], z3.Or(statement_for_state))) assertions.append(reachability_vars[initial_state]) logger.info("Done building assertions for ProbGoal.") From 0770999e486ef84f6b0638593a527f6c961d5462 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 30 Jul 2025 14:37:28 +0200 Subject: [PATCH 11/11] added option to turn off CEs in CEGIS loop --- paynt/cli.py | 2 +- paynt/synthesizer/synthesizer_cegis.py | 18 +++++++++++++----- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/paynt/cli.py b/paynt/cli.py index 1484d08f9..5201233ac 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -133,7 +133,7 @@ def setup_logger(log_path = None): ) @click.option( - "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True, + "--ce-generator", type=click.Choice(["dtmc", "mdp", "none"]), default="dtmc", show_default=True, help="counterexample generator", ) diff --git a/paynt/synthesizer/synthesizer_cegis.py b/paynt/synthesizer/synthesizer_cegis.py index 816bd0d7b..0c51f92c0 100644 --- a/paynt/synthesizer/synthesizer_cegis.py +++ b/paynt/synthesizer/synthesizer_cegis.py @@ -28,15 +28,19 @@ def __init__(self, quotient): def choose_conflict_generator(self, quotient): if SynthesizerCEGIS.conflict_generator_type == "mdp": conflict_generator = paynt.synthesizer.conflict_generator.mdp.ConflictGeneratorMdp(quotient) - else: + elif SynthesizerCEGIS.conflict_generator_type == "dtmc": # default conflict generator conflict_generator = paynt.synthesizer.conflict_generator.dtmc.ConflictGeneratorDtmc(quotient) + elif SynthesizerCEGIS.conflict_generator_type == "none": + conflict_generator = None + else: + raise ValueError(f"Unknown conflict generator type: {SynthesizerCEGIS.conflict_generator_type}") return conflict_generator @property def method_name(self): - return "CEGIS " + self.conflict_generator.name + return "CEGIS " + (self.conflict_generator.name if self.conflict_generator else "no CEs") def collect_conflict_requests(self, family, mc_result): @@ -82,8 +86,11 @@ def analyze_family_assignment_cegis(self, family, assignment): if accepting and not self.quotient.specification.can_be_improved(): return [], accepting_assignment - conflict_requests = self.collect_conflict_requests(family, result) - conflicts = self.conflict_generator.construct_conflicts(family, assignment, dtmc, conflict_requests) + if self.conflict_generator is not None: + conflict_requests = self.collect_conflict_requests(family, result) + conflicts = self.conflict_generator.construct_conflicts(family, assignment, dtmc, conflict_requests) + else: + conflicts = [[hole for hole in range(family.num_holes)]] return conflicts, accepting_assignment @@ -92,7 +99,8 @@ def synthesize_one(self, family): # build the quotient, map mdp states to hole indices self.quotient.build(family) - self.conflict_generator.initialize() + if self.conflict_generator is not None: + self.conflict_generator.initialize() # use sketch design space as a SAT baseline (TODO why?) smt_solver = paynt.family.smt.SmtSolver(self.quotient, self.constraint)