From 782ae117a3ac1a88b2bb883685046f55be145375 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 3 Sep 2017 17:59:26 +0100 Subject: [PATCH] introducing parameters --- rs/__init__.py | 4 +- ...action_system_with_concentrations_param.py | 90 +++++++++++++------ rs_testing.py | 4 +- smt/smt_checker_rsc_param.py | 20 ++--- 4 files changed, 75 insertions(+), 43 deletions(-) diff --git a/rs/__init__.py b/rs/__init__.py index 01001bf..2e56fbd 100644 --- a/rs/__init__.py +++ b/rs/__init__.py @@ -2,11 +2,11 @@ from rs.reaction_system import ReactionSystem from rs.context_automaton import ContextAutomaton from rs.reaction_system_with_concentrations import ReactionSystemWithConcentrations -from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam +from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam, ParameterObj from rs.context_automaton_with_concentrations import ContextAutomatonWithConcentrations from rs.extended_context_automaton import ExtendedContextAutomaton from rs.network_of_context_automata import NetworkOfContextAutomata from rs.reaction_system_with_automaton import ReactionSystemWithAutomaton -from rs.reaction_system_with_autnet import ReactionSystemWithNetworkOfAutomata \ No newline at end of file +from rs.reaction_system_with_autnet import ReactionSystemWithNetworkOfAutomata diff --git a/rs/reaction_system_with_concentrations_param.py b/rs/reaction_system_with_concentrations_param.py index 328afbb..c86194f 100644 --- a/rs/reaction_system_with_concentrations_param.py +++ b/rs/reaction_system_with_concentrations_param.py @@ -3,10 +3,13 @@ from colour import * from rs.reaction_system import ReactionSystem -class ParameterSet(object): +class ParameterObj(object): def __init__(self, name): self.name = name + + def __repr__(self): + return "@{0}".format(self.name) class ReactionSystemWithConcentrationsParam(ReactionSystem): @@ -14,6 +17,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): def __init__(self): self.reactions = [] + self.parametric_reactions = [] self.meta_reactions = dict() self.permanent_entities = dict() self.background_set = [] @@ -85,31 +89,55 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): if R == [] and not ignore_empty_R: raise RuntimeError("No reactants defined") + # + # REACTANTS + # reactants = [] - for r in R: - self.is_valid_entity_with_concentration(r) - self.has_non_zero_concentration(r) - entity, level = r - reactants.append((self.get_entity_id(entity), level)) - if self.max_concentration < level: - self.max_concentration = level + if isinstance(R, ParameterObj): + reactants = R + else: + for r in R: + self.is_valid_entity_with_concentration(r) + self.has_non_zero_concentration(r) + entity, level = r + reactants.append((self.get_entity_id(entity), level)) + if self.max_concentration < level: + self.max_concentration = level + + # + # INHIBITORS + # inhibitors = [] - for i in I: - self.is_valid_entity_with_concentration(i) - self.has_non_zero_concentration(i) - entity, level = i - inhibitors.append((self.get_entity_id(entity), level)) - if self.max_concentration < level: - self.max_concentration = level + if isinstance(I, ParameterObj): + inhibitors = I + else: + for i in I: + self.is_valid_entity_with_concentration(i) + self.has_non_zero_concentration(i) + entity, level = i + inhibitors.append((self.get_entity_id(entity), level)) + if self.max_concentration < level: + self.max_concentration = level + + # + # PRODUCTS + # products = [] - for p in P: - self.is_valid_entity_with_concentration(p) - self.has_non_zero_concentration(p) - entity, level = p - products.append((self.get_entity_id(entity), level)) + if isinstance(P, ParameterObj): + products = P + else: + for p in P: + self.is_valid_entity_with_concentration(p) + self.has_non_zero_concentration(p) + entity, level = p + products.append((self.get_entity_id(entity), level)) return reactants, inhibitors, products + def is_parametric_reaction(self, reaction): + result = any([isinstance(r_set, ParameterObj) for r_set in reaction]) + return result + def add_reaction(self, R, I, P): """Adds a reaction @@ -119,7 +147,11 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): if P == []: raise RuntimeError("No products defined") reaction = self.process_rip(R,I,P) - self.reactions.append(reaction) + + if self.is_parametric_reaction(reaction): + self.parametric_reactions.append(reaction) + else: + self.reactions.append(reaction) def add_reaction_without_reactants(self, R, I, P): """Adds a reaction""" @@ -174,10 +206,18 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): return s def state_to_str(self, state): - s = "" - for ent,level in state: - s += self.get_entity_name(ent) + "=" + str(level) + ", " - s = s[:-2] + """ + If state is a parameter, we return + the string representation of the whole state + which should be the name of the parameter + """ + if isinstance(state, ParameterObj): + return str(state) + else: + s = "" + for ent,level in state: + s += self.get_entity_name(ent) + "=" + str(level) + ", " + s = s[:-2] return s def show_background_set(self): diff --git a/rs_testing.py b/rs_testing.py index 6bb523d..5b77c7c 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -27,7 +27,7 @@ def trivial_param(): r.add_reaction([("x", 1)], [("c", 1)], [("y", 2)]) r.add_reaction([("y", 1)], [("c", 1)], [("z", 1)]) - r.add_reaction([("z", 1)], [("c", 1)], [("final", 1)]) + r.add_reaction(ParameterObj("P1"), [("c", 1)], [("final", 1)]) c = ContextAutomatonWithConcentrations(r) c.add_init_state("0") @@ -43,7 +43,7 @@ def trivial_param(): BagDescription.f_TRUE(), BagDescription.f_entity("final") >= 1) - smt_rsc.check_rsltl(formula=f2) + smt_rsc.check_rsltl(formula=f2, max_level=5) def example44_param(): diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index a71a0ae..50ae1bb 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -14,7 +14,7 @@ from logics import rsLTL_Encoder # def simplify(x): # return x -def MAX(a, b): +def z3_max(a, b): return If(a > b, a, b) class SmtCheckerRSCParam(object): @@ -31,7 +31,6 @@ class SmtCheckerRSCParam(object): self.initialise() - def initialise(self): """Initialises all the variables used by the checker""" @@ -41,7 +40,6 @@ class SmtCheckerRSCParam(object): # intermediate products: self.v_improd = [] - self.v_improd_for_entities = [] self.next_level_to_encode = 0 @@ -55,12 +53,10 @@ class SmtCheckerRSCParam(object): self.verification_time = None - def reset(self): """Reinitialises the state of the checker""" - self.initialise() - + self.initialise() def prepare_all_variables(self): """Prepares all the variables""" @@ -68,8 +64,7 @@ class SmtCheckerRSCParam(object): self.prepare_state_variables() self.prepare_context_variables() self.prepare_intermediate_product_variables() - self.next_level_to_encode += 1 - + self.next_level_to_encode += 1 def prepare_context_variables(self): """Prepares all the context variables""" @@ -82,7 +77,6 @@ class SmtCheckerRSCParam(object): self.v_ctx.append(variables) - def prepare_state_variables(self): """Prepares all the state variables""" @@ -95,7 +89,6 @@ class SmtCheckerRSCParam(object): self.ca_state.append(Int("CA"+str(level)+"_state")) - def prepare_intermediate_product_variables(self): """ Prepares the intermediate product variables @@ -261,16 +254,15 @@ class SmtCheckerRSCParam(object): enc = None if len(elements) == 1: - enc = MAX(0, elements[0]) + enc = z3_max(0, elements[0]) elif len(elements) > 1: enc = 0 for i in range(len(elements) - 1): - enc = MAX(enc, MAX(elements[i], elements[i + 1])) + enc = z3_max(enc, z3_max(elements[i], elements[i + 1])) return enc - def enc_automaton_trans(self, level): """Encodes the transition relation for the context automaton""" @@ -603,7 +595,7 @@ class SmtCheckerRSCParam(object): print("Test: ", s) self.solver.add(s) - + result = self.solver.check() if result == sat: print("\n[+] " + colour_str(C_RED, "SAT at level=" + str(self.current_level)))