From 27c86497e4d7096ee6f75f49b5e65fa64d6fdc1d Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 13 Aug 2017 13:48:42 +0100 Subject: [PATCH] RSC with Param; RSCA for Param, SMTChecker for Param --- rs/reaction_system_with_automaton.py | 12 +++ ...action_system_with_concentrations_param.py | 85 ++++++++++++------- rs_testing.py | 81 +++++++++++++++++- smt/__init__.py | 1 + smt/smt_checker_rsc_param.py | 8 +- 5 files changed, 151 insertions(+), 36 deletions(-) diff --git a/rs/reaction_system_with_automaton.py b/rs/reaction_system_with_automaton.py index 9690ce2..500a883 100644 --- a/rs/reaction_system_with_automaton.py +++ b/rs/reaction_system_with_automaton.py @@ -1,4 +1,5 @@ from rs.reaction_system_with_concentrations import ReactionSystemWithConcentrations +from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam from rs.context_automaton_with_concentrations import ContextAutomatonWithConcentrations class ReactionSystemWithAutomaton(object): @@ -11,6 +12,17 @@ class ReactionSystemWithAutomaton(object): self.rs.show(soft) self.ca.show() + def is_concentr_and_param_compatible(self): + """ + Checks if the underlying RS/CA are compatible + with parameters and concentrations + """ + if not isinstance(self.rs, ReactionSystemWithConcentrationsParam): + return False + if not isinstance(self.ca, ContextAutomatonWithConcentrations): + return False + return True + def is_with_concentrations(self): if not isinstance(self.rs, ReactionSystemWithConcentrations): return False diff --git a/rs/reaction_system_with_concentrations_param.py b/rs/reaction_system_with_concentrations_param.py index 5c18e0f..20e2134 100644 --- a/rs/reaction_system_with_concentrations_param.py +++ b/rs/reaction_system_with_concentrations_param.py @@ -102,7 +102,10 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): return reactants,inhibitors,products def add_reaction(self, R, I, P): - """Adds a reaction""" + """Adds a reaction + + R, I, and P are sets of entities (not their IDs) + """ if P == []: raise RuntimeError("No products defined") @@ -201,6 +204,8 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): def get_reactions_by_product(self): """Sorts reactions by their products and returns a dictionary of products""" + assert False + if self.reactions_by_prod != None: return self.reactions_by_prod @@ -247,6 +252,9 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): return reactions_by_prod def get_reaction_system(self): + """ + Translates RSC into RS + """ rs = ReactionSystem() @@ -372,36 +380,51 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): return rs -class ReactionSystemWithAutomaton(object): - - def __init__(self, reaction_system, context_automaton): - self.rs = reaction_system - self.ca = context_automaton - - def show(self, soft=False): - self.rs.show(soft) - self.ca.show() - - def is_with_concentrations(self): - if not isinstance(self.rs, ReactionSystemWithConcentrations): - return False - if not isinstance(self.ca, ContextAutomatonWithConcentrations): - return False - return True - - def sanity_check(self): - pass - - def get_ordinary_reaction_system_with_automaton(self): - - if not self.is_with_concentrations(): - raise RuntimeError("Not RS/CA with concentrations") - - ors = self.rs.get_reaction_system() - oca = self.ca.get_automaton_with_flat_contexts(ors) - - return ReactionSystemWithAutomaton(ors, oca) - +# class ReactionSystemWithAutomaton(object): +# +# def __init__(self, reaction_system, context_automaton): +# self.rs = reaction_system +# self.ca = context_automaton +# +# def show(self, soft=False): +# self.rs.show(soft) +# self.ca.show() +# +# def is_concentr_and_param_compatible(self): +# """ +# Checks if the underlying RS/CA are compatible +# with parameters and concentrations +# """ +# if not isinstance(self.rs, ReactionSystemWithConcentrationsParam): +# return False +# if not isinstance(self.ca, ContextAutomatonWithConcentrations): +# return False +# return True +# +# def is_with_concentrations(self): +# """ +# Checks if the underlying RS and CA provide +# concentration levels +# """ +# if not isinstance(self.rs, ReactionSystemWithConcentrations): +# return False +# if not isinstance(self.ca, ContextAutomatonWithConcentrations): +# return False +# return True +# +# def sanity_check(self): +# pass +# +# def get_ordinary_reaction_system_with_automaton(self): +# +# if not self.is_with_concentrations(): +# raise RuntimeError("Not RS/CA with concentrations") +# +# ors = self.rs.get_reaction_system() +# oca = self.ca.get_automaton_with_flat_contexts(ors) +# +# return ReactionSystemWithAutomaton(ors, oca) +# # class ReactionSystemWithConcentrationWithAutomaton(ReactionSystemWithAutomaton): # diff --git a/rs_testing.py b/rs_testing.py index 6ecb83c..4e61f7b 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -11,7 +11,86 @@ def run_tests(): # process() # heat_shock_response() # scalable_chain(print_system=True) - example44() + # example44() + example44_param() + +def example44_param(): + + r = ReactionSystemWithConcentrationsParam() + r.add_bg_set_entity(("x",2)) + r.add_bg_set_entity(("y",4)) + r.add_bg_set_entity(("h",2)) + r.add_bg_set_entity(("m",1)) + + r.add_reaction([("y",1),("x",1)], [("y",2),("h",1)], [("y",2)]) + r.add_reaction([("y",2),("x",2)], [("y",3),("h",1)], [("y",3)]) + r.add_reaction([("y",3),("h",1)], [("y",4),("h",2)], [("y",4)]) + r.add_reaction([("y",4),("h",1)], [("h",2)], [("y",3)]) + r.add_reaction([("y",4),("x",2)], [("h",1)], [("y",2)]) + r.add_reaction([("m",1)], [("y",3)], [("m",1)]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("0") + c.add_state("1") + c.add_transition("0", [("y",1),("m",1),("x",1)], "1") + c.add_transition("1", [("x",1)], "1") + c.add_transition("1", [("x",1),("h",1)], "1") + c.add_transition("1", [("x",2)], "1") + c.add_transition("1", [("x",2),("h",1)], "1") + c.add_transition("1", [("h",1)], "1") + + + rc = ReactionSystemWithAutomaton(r,c) + rc.show() + smt_rsc = SmtCheckerRSCParam(rc) + + # Universal property which seems to be true: (holds also existentially) + f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") >= 3 + ) + ) + ) + + # lets see if we can find a counterexample to this property: + neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_And( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") < 3 + ) + ) + ) + + # we fix the property f1 + # this one holds: + f2 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1) & (BagDescription.f_entity("h") < 1), + BagDescription.f_entity("y") >= 3 + ) + ) + ) + + # neg_f1 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, + # Formula_rsLTL.f_And( + # (BagDescription.f_entity('y') > 0), + # Formula_rsLTL.f_X( + # BagDescription.f_entity("x") > 0, + # Formula_rsLTL.f_X( + # BagDescription.f_entity("x") > 1, + # BagDescription.f_entity("y") < 3 + # ) + # ) + # ) + # )) + # smt_rsc.check_rsltl(formula=neg_f1) def example44(): diff --git a/smt/__init__.py b/smt/__init__.py index d4c1b71..8958447 100644 --- a/smt/__init__.py +++ b/smt/__init__.py @@ -1,5 +1,6 @@ #from smt.smt_checker import SmtChecker from smt.smt_checker_rs import SmtCheckerRS from smt.smt_checker_rsc import SmtCheckerRSC +from smt.smt_checker_rsc_param import SmtCheckerRSCParam from smt.smt_checker_rs_na import SmtCheckerRSNA from smt.smt_checker_distrib_rs import SmtCheckerDistribRS diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index 4604f87..399c3a6 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -14,14 +14,14 @@ from logics import rsLTL_Encoder # def simplify(x): # return x -class SmtCheckerRSC(object): +class SmtCheckerRSCParam(object): def __init__(self, rsca): - + rsca.sanity_check() - if not rsca.is_with_concentrations(): - raise RuntimeError("RS and CA with concentrations expected") + if not rsca.is_concentr_and_param_compatible(): + raise RuntimeError("RS and CA with concentrations (and parameters) expected") self.rs = rsca.rs self.ca = rsca.ca