diff --git a/colour.py b/colour.py index 07cc048..29ba737 100644 --- a/colour.py +++ b/colour.py @@ -14,4 +14,6 @@ def colour_str(col, s): return col + s + C_ENDC def print_error(s): - print(C_MARK_ERROR + " " + C_RED + s + C_ENDC) \ No newline at end of file + print(C_MARK_ERROR + " " + C_RED + s + C_ENDC) + +# EOF diff --git a/rs_examples.py b/rs_examples.py old mode 100644 new mode 100755 index bbe9478..f0e26b9 --- a/rs_examples.py +++ b/rs_examples.py @@ -187,3 +187,4 @@ def heat_shock_response(print_system=True,verify_rsc=True): def state_translate_rsc2rs(p): return [e[0] + "#" + str(e[1]) for e in p] +# EOF \ No newline at end of file diff --git a/rs_testing.py b/rs_testing.py index 9f9110c..4d746c6 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -48,7 +48,7 @@ def trivial_param(): # # WARNING: depth limit is set # - smt_rsc.check_rsltl(formula=f1, max_level=5) + smt_rsc.check_rsltl(formula=f1, max_level=10, print_witness=True) def example44_param(): diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index 50ae1bb..fa9941f 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -41,17 +41,25 @@ class SmtCheckerRSCParam(object): # intermediate products: self.v_improd = [] self.v_improd_for_entities = [] + + self.v_param = [] self.next_level_to_encode = 0 + # this is probably not needed anymore self.producible_entities = self.rs.get_producible_entities() - self.improducible_entities = set(self.rs.get_state_ids(self.rs.background_set)) - self.producible_entities + # self.improducible_entities = set(self.rs.get_state_ids(self.rs.background_set)) - self.producible_entities + + # WARNING: improd vs. improducible + # there is some confusion related to the variables naming: + # improd - intermediate products + # improducible - entities that are never produces (there is no reaction that produces that entity) self.loop_position = Int("loop_position") self.solver = Solver() #For("QF_FD") - self.verification_time = None + self.verification_time = None def reset(self): """Reinitialises the state of the checker""" @@ -64,6 +72,7 @@ class SmtCheckerRSCParam(object): self.prepare_state_variables() self.prepare_context_variables() self.prepare_intermediate_product_variables() + self.prepare_param_variables() self.next_level_to_encode += 1 def prepare_context_variables(self): @@ -93,7 +102,7 @@ class SmtCheckerRSCParam(object): """ Prepares the intermediate product variables carrying the individual concentration levels produced - the reactions. + by the reactions. These variables are used later on to encode the final concentration levels for all the entities @@ -123,12 +132,12 @@ class SmtCheckerRSCParam(object): entities_dict = dict() for entity, conc in products: - varname = Int("IP" + str(level) + "_R" + + new_var = Int("IP" + str(level) + "_R" + str(reaction_id) + "_e" + str(entity)) - entities_dict[entity] = varname + entities_dict[entity] = new_var all_entities_dict.setdefault(entity, []) - all_entities_dict[entity].append(varname) + all_entities_dict[entity].append(new_var) reactions_dict[reaction_id] = entities_dict @@ -139,6 +148,25 @@ class SmtCheckerRSCParam(object): # print(self.v_improd_for_entities) + def prepare_param_variables(self): + """ + Prepares variables for parameters + + A parameter (it's valuation) is a subset of the background set, + therefore we need separate variables for each element of the + background set. + """ + + level = self.next_level_to_encode + + params = [] + for entity in self.rs.background_set: + new_var = Int("L{:d}_Pm_{:s}".format(level, entity)) + params.append(new_var) + self.v_param.append(params) + + print(self.v_param) + def enc_concentration_levels_assertion(self, level): """ Encodes assertions that (some) variables need to be >0 @@ -177,6 +205,46 @@ class SmtCheckerRSCParam(object): And(self.enc_rs_trans(level), self.enc_automaton_trans(level))) + def enc_single_reaction(self, level, reaction): + """ + Encodes a single reaction + + For encoding the products we use intermediate variables: + + * each reaction has its own product variables, + + * those are meant to be used to compute the MAX concentration + + """ + + reactants, inhibitors, products = reaction + + # we need reaction_id to find the intermediate product variable + reaction_id = self.rs.reactions.index(reaction) + + enc_reactants = True + for entity, conc in reactants: + enc_reactants = And(enc_reactants, Or( + self.v[level][entity] >= conc, self.v_ctx[level][entity] >= conc)) + + enc_inhibitors = True + for entity, conc in inhibitors: + enc_inhibitors = And(enc_inhibitors, And( + self.v[level][entity] < conc, self.v_ctx[level][entity] < conc)) + + enc_products = True + for entity, conc in products: + enc_products = And(enc_products, self.v_improd[ + level + 1][reaction_id][entity] == conc) + + # + # (R and I) iff P + # + enc_reaction = simplify( + And(enc_reactants, enc_inhibitors) == enc_products) + + return enc_reaction + def enc_rs_trans(self, level): """Encodes the transition relation""" @@ -188,62 +256,43 @@ class SmtCheckerRSCParam(object): # # They should have concentration levels set to 0. # + # That needs to happen automatically (in the MAX encoding) -- for the parametric + # case it makes no sense to identify the entities that are never produced, unless + # we have no parameters as products (special case, so that could be an + # optimisation) + # enc_trans = True for reaction in self.rs.reactions: - - reactants, inhibitors, products = reaction - reaction_id = self.rs.reactions.index(reaction) - - enc_reactants = True - for entity, conc in reactants: - enc_reactants = And(enc_reactants, Or( - self.v[level][entity] >= conc, self.v_ctx[level][entity] >= conc)) - - enc_inhibitors = True - for entity, conc in inhibitors: - enc_inhibitors = And(enc_inhibitors, And( - self.v[level][entity] < conc, self.v_ctx[level][entity] < conc)) - - enc_products = True - for entity, conc in products: - enc_products = And(enc_products, self.v_improd[ - level + 1][reaction_id][entity] == conc) - - # - # (R and I) iff P - # - enc_reaction = simplify( - And(enc_reactants, enc_inhibitors) == enc_products) - + enc_reaction = self.enc_single_reaction(level, reaction) enc_trans = simplify(And(enc_trans, enc_reaction)) - # print(enc_trans) - - # - # TODO: - # - # Max of all the produced concentrations for each entity/product... + # Next we encode the MAX concentration values: + # we collect those from the intermediate product variables enc_max_prod = True + # Save all the intermediate product variables for a given level: + # + # - Intermediate products of (level+1) correspond to the next level + # + # {reactants & inhibitors}[level] + # => + # {improd}[level+1] + # => + # {products}[level+1] + # current_v_improd_for_entities = self.v_improd_for_entities[level + 1] + for entity, per_reaction_vars in current_v_improd_for_entities.items(): - # enc_max_single_ent = True - - # sorted_vars_by_conc = sorted(per_reaction_vars, key=lambda conc_var: conc_var[0]) - # list_of_vars = [v for c,v in sorted_vars_by_conc] - - # print(per_reaction_vars, "--->", self.enc_max(per_reaction_vars)) - enc_max_prod = simplify( And(enc_max_prod, self.v[level + 1][entity] == self.enc_max(per_reaction_vars))) - for entity in self.improducible_entities: - enc_max_prod = simplify( - And(enc_max_prod, self.v[level + 1][entity] == 0)) + # for entity in self.improducible_entities: + # enc_max_prod = simplify( + # And(enc_max_prod, self.v[level + 1][entity] == 0)) enc_trans_with_max = simplify(And(enc_max_prod, enc_trans)) @@ -428,6 +477,7 @@ class SmtCheckerRSCParam(object): result = self.solver.check() if result == sat: print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(self.current_level))) + print(self.solver.model()) if print_witness: print("\n{:=^70}".format("[ WITNESS ]")) self.decode_witness(self.current_level)