diff --git a/logics/__init__.py b/logics/__init__.py index 768c246..3d0d860 100644 --- a/logics/__init__.py +++ b/logics/__init__.py @@ -2,3 +2,4 @@ from logics.rsltl import Formula_rsLTL from logics.bags import BagDescription from logics.param_constr import ParamConstraint from logics.rsltl_encoder import rsLTL_Encoder +from logics.param_constr_encoder import ParamConstr_Encoder \ No newline at end of file diff --git a/logics/param_constr.py b/logics/param_constr.py index 211697d..eb8fc50 100644 --- a/logics/param_constr.py +++ b/logics/param_constr.py @@ -49,7 +49,7 @@ class ParamConstraint(object): @classmethod def f_param_ent(cls, param, entity_name): - return cls(ParamConstraint_oper.entity, param=param, entity=entity_name) + return cls(ParamConstraint_oper.param_entity, param=param, entity=entity_name) @classmethod def f_TRUE(cls): diff --git a/logics/param_constr_encoder.py b/logics/param_constr_encoder.py new file mode 100644 index 0000000..6fb6032 --- /dev/null +++ b/logics/param_constr_encoder.py @@ -0,0 +1,59 @@ +from logics.param_constr import * +from z3 import And, Not, Or + +class ParamConstr_Encoder(object): + """Class for encoding parameter constraints""" + + def __init__(self, smt_checker): + self.smt_checker = smt_checker + self.rs = smt_checker.rs + + # self.v = None + # self.v_ctx = None + # self.loop_position = None + + def load_variables(self, var_rs, var_ctx, var_loop_pos): + + self.v = var_rs + self.v_ctx = var_ctx + self.loop_position = var_loop_pos + + def encode(self, param_constr): + + if not param_constr: + raise RuntimeError("param_constr is None") + + if param_constr.f_type == ParamConstraint_oper.param_entity: + return self.smt_checker.get_enc_param(param_constr.param.name, param_constr.entity) + + if param_constr.f_type == ParamConstraint_oper.true: + return True + + if param_constr.f_type == ParamConstraint_oper.l_and: + return And(self.encode(param_constr.left_operand), + self.encode(param_constr.right_operand)) + + if param_constr.f_type == ParamConstraint_oper.l_or: + return Or(self.encode(param_constr.left_operand), + self.encode(param_constr.right_operand)) + + if param_constr.f_type == ParamConstraint_oper.l_not: + return Not(self.encode(param_constr.left_operand)) + + if param_constr.f_type == ParamConstraint_oper.lt: + return self.encode(param_constr.left_operand) < int(param_constr.right_operand) + + if param_constr.f_type == ParamConstraint_oper.le: + return self.encode(param_constr.left_operand) <= int(param_constr.right_operand) + + if param_constr.f_type == ParamConstraint_oper.eq: + return self.encode(param_constr.left_operand) == int(param_constr.right_operand) + + if param_constr.f_type == ParamConstraint_oper.ge: + return self.encode(param_constr.left_operand) >= int(param_constr.right_operand) + + if param_constr.f_type == ParamConstraint_oper.gt: + return self.encode(param_constr.left_operand) > int(param_constr.right_operand) + + assert False, "Unsupported case {:s}".format(param_constr.f_type) + diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index 222535c..9211e39 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -1,7 +1,7 @@ from logics.rsltl import * def simplify(x): - return x + return x class rsLTL_Encoder(object): """Class for encoding rsLTL formulae for a given smt_checker instance""" diff --git a/rs/reaction_system.py b/rs/reaction_system.py index 42c8bc9..8112462 100644 --- a/rs/reaction_system.py +++ b/rs/reaction_system.py @@ -23,6 +23,10 @@ class ReactionSystem(object): def set_of_bgset_ids(self): return set(range(self.background_set_size)) + @property + def ordered_list_of_bgset_ids(self): + return list(range(self.background_set_size)) + def assume_not_in_bgset(self, name): if self.is_in_background_set(name): raise RuntimeError("The entity " + name + " is already on the list") diff --git a/rs_testing.py b/rs_testing.py index 2d7bc31..6a86e22 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -25,14 +25,24 @@ def gene_expression(cmd_args): Simple gene expression example """ r = ReactionSystemWithConcentrationsParam() - + + r.add_bg_set_entity(("x", 1)) + r.add_bg_set_entity(("xp", 1)) + r.add_bg_set_entity(("X", 1)) r.add_bg_set_entity(("y", 1)) r.add_bg_set_entity(("yp", 1)) r.add_bg_set_entity(("Y", 1)) r.add_bg_set_entity(("h", 1)) + r.add_bg_set_entity(("Q", 1)) all_entities = set(r.background_set) + r.add_reaction([("x",1)],[("h",1)],[("x",1)]) + r.add_reaction([("x",1)],[("h",1)],[("xp",1)]) + r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)]) + + r.add_reaction([("X",1),("Y",1)],[("h",1)],[("Q",1)]) + ## y # r.add_reaction([("y",1)],[("h",1)],[("y",1)]) # r.add_reaction([("y",1)],[("Q",1)],[("yp",1)]) @@ -50,10 +60,11 @@ def gene_expression(cmd_args): c.add_state("1") # the experiments starts with adding x and y: - c.add_transition("0", [("y", 1)], "1") + c.add_transition("0", [("y", 1),("x",1)], "1") # for all the remaining steps we have empty context sequences c.add_transition("1", [], "1") + c.add_transition("1", [("h", 1)], "1") rc = ReactionSystemWithAutomaton(r, c) rc.show() @@ -65,32 +76,42 @@ def gene_expression(cmd_args): # exact_state(["x", "xp"], all_entities), # ltl_X(bag_Not("h"), exact_state("X", all_entities)))) - reach_yp = ltl_F(True, "yp") - reach_Y = ltl_F(True, "Y") - reach_y = ltl_F(True, "y") + # reachability + reach_y = ltl_F(bag_entity("h") == 0, "y") + reach_yp = ltl_F(bag_entity("h") == 0, "yp") + reach_Y = ltl_F(bag_entity("h") == 0, "Y") + # + phi_r = ltl_And(reach_y, reach_yp, reach_Y) - f_y1 = ltl_G(bag_entity("h") == 0, ltl_Implies( + # rules + phi_c1 = ltl_G(bag_entity("h") == 0, ltl_Implies( bag_entity("y") > 0, ltl_X(True, bag_And(bag_entity("y") > 0, bag_entity("yp") > 0)))) - f_y2 = ltl_G(bag_entity("h") == 0, ltl_Implies( + phi_c2 = ltl_G(bag_entity("h") == 0, ltl_Implies( bag_And(bag_entity("y") > 0, bag_entity("yp") > 0), ltl_F(True, bag_entity("Y") > 0))) - - # delayed_Y = ltl_X(True, ltl_And(bag_entity("Y") == 0, ltl_X(True, bag_entity("Y") == 0))) - delayed_Y = ltl_X(True, bag_entity("Y") == 0) - obs_1 = ltl_And(f_y1, reach_y, delayed_Y) - obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y) + # delayed_Y = ltl_X(True, ltl_And(bag_entity("Y") == 0, ltl_X(True, bag_entity("Y") == 0))) + + # delayed_Y = ltl_X(True, bag_entity("Y") == 0) + + delayed_Q = ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_F(True, bag_entity("Q") > 0)))))) + + obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q) + + # obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q) # f_x2 = ltl_G(True, ltl_Implies( # exact_state(["x", "xp"], all_entities), # ltl_X(bag_Not("h"), exact_state("X", all_entities)))) # + + param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0) smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise) # - smt_rsc.check_rsltl(formulae_list=[obs_1, obs_2], max_level=4, cont_if_sat=True) + smt_rsc.check_rsltl(formulae_list=[obs_1], param_constr=param_constr) #, max_level=4, cont_if_sat=True) # smt_rsc.check_rsltl(formula=f_x1, print_witness=True) diff --git a/rsltl_shortcuts.py b/rsltl_shortcuts.py index ab1a8ea..c9349ce 100644 --- a/rsltl_shortcuts.py +++ b/rsltl_shortcuts.py @@ -61,6 +61,11 @@ def ltl_X(ctx_arg, a0): a0 = get_bag_if_str(a0) return Formula_rsLTL.f_X(ctx_arg, a0) +def ltl_U(ctx_arg, a0, a1): + a0 = get_bag_if_str(a0) + a1 = get_bag_if_str(a1) + return Formula_rsLTL.f_U(ctx_arg, a0, a1) + def ltl_And(*args): assert len(args) > 1 last = get_bag_if_str(args[0]) @@ -77,3 +82,13 @@ def ltl_Implies(a0, a1): a1 = get_bag_if_str(a1) return Formula_rsLTL.f_Implies(a0, a1) +def param_entity(param, entity_name): + return ParamConstraint.f_param_ent(param, entity_name) + +def param_And(*args): + assert len(args) > 1 + last = args[0] + for arg in args[1:]: + last = ParamConstraint.f_And(last, arg) + return last + diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index d424dcc..a71747f 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -10,6 +10,7 @@ import resource from colour import * from logics import rsLTL_Encoder +from logics import ParamConstr_Encoder from rs.reaction_system_with_concentrations_param import ParameterObj, is_param @@ -224,12 +225,19 @@ class SmtCheckerRSCParam(object): # we start collecting bg-related vars for the given param vars_for_param = [] - for entity in self.rs.set_of_bgset_ids: + for entity in self.rs.ordered_list_of_bgset_ids: new_var = Int("Pm{:s}_{:s}".format(param_name, self.rs.get_entity_name(entity))) vars_for_param.append(new_var) self.v_param[param_name] = vars_for_param - + + def get_enc_param(self, param_name, entity_name): + """ + Returns encoded param[entity_name] + """ + entity_id = self.rs.get_entity_id(entity_name) + return self.v_param[param_name][entity_id] + def load_varset_for_path(self, path_idx): """ Loads the the variables for the path with path_idx @@ -682,7 +690,8 @@ class SmtCheckerRSCParam(object): self, formulae_list, print_witness=True, print_time=True, print_mem=True, - max_level=None, cont_if_sat=False): + max_level=None, cont_if_sat=False, + param_constr=None): """ Bounded Model Checking for rsLTL properties @@ -694,10 +703,14 @@ class SmtCheckerRSCParam(object): * cont_if_sat -- if True, then the method continues up until max_level is reached (even if sat found) + * param_constr -- constraints on parameters """ if not isinstance(formulae_list, (list, tuple)): print_error("Expected a list of formulae") + + print_info("Parameter constraint: {:s}".format(str(param_constr))) + self.reset() @@ -734,6 +747,11 @@ class SmtCheckerRSCParam(object): self.solver_add(self.enc_param_concentration_levels_assertion()) encoder = rsLTL_Encoder(self) + + if param_constr: + param_contr_encoder = ParamConstr_Encoder(self) + enc_param_constr = param_contr_encoder.encode(param_constr) + self.solver_add(enc_param_constr) if self.optimise: self.assert_param_optimisation()