ReactionSystemsWithConcentration. Backup
This commit is contained in:
140
rctsys.py
140
rctsys.py
@@ -230,13 +230,16 @@ class ReactionSystem(object):
|
|||||||
s = s[:-2]
|
s = s[:-2]
|
||||||
return s
|
return s
|
||||||
|
|
||||||
|
def state_to_str(self, state):
|
||||||
|
return self.entities_ids_set_to_str(state)
|
||||||
|
|
||||||
def show_reactions(self, soft=False):
|
def show_reactions(self, soft=False):
|
||||||
print("[*] Reactions:")
|
print("[*] Reactions:")
|
||||||
if soft and len(self.reactions) > 50:
|
if soft and len(self.reactions) > 50:
|
||||||
print("\t -> there are more than 50 reactions (" + str(len(self.reactions)) + ")")
|
print("\t -> there are more than 50 reactions (" + str(len(self.reactions)) + ")")
|
||||||
else:
|
else:
|
||||||
for reaction in self.reactions:
|
for reaction in self.reactions:
|
||||||
print("\t - ( R={" + self.entities_ids_set_to_str(reaction[0]) + "}, \tI={" + self.entities_ids_set_to_str(reaction[1]) + "}, \tP={" + self.entities_ids_set_to_str(reaction[2]) + "} )")
|
print("\t - ( R={" + self.state_to_str(reaction[0]) + "}, \tI={" + self.state_to_str(reaction[1]) + "}, \tP={" + self.state_to_str(reaction[2]) + "} )")
|
||||||
|
|
||||||
def show_background_set(self):
|
def show_background_set(self):
|
||||||
print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
|
print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
|
||||||
@@ -293,12 +296,130 @@ class ReactionSystem(object):
|
|||||||
print("Empty background set")
|
print("Empty background set")
|
||||||
exit(1)
|
exit(1)
|
||||||
|
|
||||||
if self.init_contexts == []:
|
|
||||||
print("No initial context defined")
|
class ReactionSystemWithConcentrations(ReactionSystem):
|
||||||
|
|
||||||
|
def __init__(self):
|
||||||
|
|
||||||
|
self.reactions = []
|
||||||
|
self.background_set = []
|
||||||
|
self.context_entities = []
|
||||||
|
|
||||||
|
self.reactions_by_agents = [] # each element is 'reactions_by_prod'
|
||||||
|
|
||||||
|
self.reactions_by_prod = None
|
||||||
|
|
||||||
|
def get_entity_id(self, name):
|
||||||
|
try:
|
||||||
|
return self.background_set.index(name)
|
||||||
|
except ValueError:
|
||||||
|
print("Undefined background set entity: " + repr(name))
|
||||||
exit(1)
|
exit(1)
|
||||||
|
|
||||||
if self.context_entities == []:
|
def get_state_ids(self, state):
|
||||||
print("WARNING: no context entities!")
|
ids = []
|
||||||
|
for entity in state:
|
||||||
|
ids.append(self.get_entity_id(entity))
|
||||||
|
return ids
|
||||||
|
|
||||||
|
def is_valid_entity_with_concentration(self, e):
|
||||||
|
"""Sanity check for entities with concentration"""
|
||||||
|
|
||||||
|
if type(e) is tuple:
|
||||||
|
if len(e) == 2 and type(e[1]) is int:
|
||||||
|
return True
|
||||||
|
|
||||||
|
if type(e) is list:
|
||||||
|
if len(e) == 2 and type(e[1]) is int:
|
||||||
|
return True
|
||||||
|
|
||||||
|
print("FATAL. Invalid entity+concentration:")
|
||||||
|
print(e)
|
||||||
|
exit(1)
|
||||||
|
|
||||||
|
return False
|
||||||
|
|
||||||
|
def add_reaction(self, R, I, P):
|
||||||
|
"""Adds a reaction"""
|
||||||
|
|
||||||
|
if R == [] or P == []:
|
||||||
|
print("No reactants of products defined")
|
||||||
|
raise
|
||||||
|
|
||||||
|
reactants = []
|
||||||
|
for r in R:
|
||||||
|
self.is_valid_entity_with_concentration(r)
|
||||||
|
entity,level = r
|
||||||
|
reactants.append((self.get_entity_id(entity),level))
|
||||||
|
|
||||||
|
inhibitors = []
|
||||||
|
for i in I:
|
||||||
|
self.is_valid_entity_with_concentration(i)
|
||||||
|
entity,level = i
|
||||||
|
inhibitors.append((self.get_entity_id(entity),level))
|
||||||
|
|
||||||
|
products = []
|
||||||
|
for p in P:
|
||||||
|
self.is_valid_entity_with_concentration(p)
|
||||||
|
entity,level = p
|
||||||
|
products.append((self.get_entity_id(entity),level))
|
||||||
|
|
||||||
|
self.reactions.append((reactants, inhibitors, products))
|
||||||
|
|
||||||
|
def set_context_entities(self, entities):
|
||||||
|
raise NotImplementedError
|
||||||
|
|
||||||
|
def entities_names_set_to_str(self, entities):
|
||||||
|
s = ""
|
||||||
|
for entity in entities:
|
||||||
|
s += entity + ", "
|
||||||
|
s = s[:-2]
|
||||||
|
return s
|
||||||
|
|
||||||
|
def entities_ids_set_to_str(self, entities):
|
||||||
|
s = ""
|
||||||
|
for entity in entities:
|
||||||
|
s += self.get_entity_name(entity) + ", "
|
||||||
|
s = s[:-2]
|
||||||
|
return s
|
||||||
|
|
||||||
|
def states_to_str(self, state):
|
||||||
|
s = ""
|
||||||
|
for entity,level in state:
|
||||||
|
s += str((self.get_entity_name(entity),level)) + ", "
|
||||||
|
s = s[:-2]
|
||||||
|
return s
|
||||||
|
|
||||||
|
def show_background_set(self):
|
||||||
|
print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
|
||||||
|
|
||||||
|
def show(self, soft=False):
|
||||||
|
self.show_background_set()
|
||||||
|
self.show_reactions(soft)
|
||||||
|
|
||||||
|
def get_reactions_by_product(self):
|
||||||
|
"""Sorts reactions by their products and returns a dictionary of products"""
|
||||||
|
|
||||||
|
if self.reactions_by_prod != None:
|
||||||
|
return self.reactions_by_prod
|
||||||
|
|
||||||
|
producible_entities = set()
|
||||||
|
|
||||||
|
for reaction in self.reactions:
|
||||||
|
producible_entities = producible_entities.union(set(reaction[2]))
|
||||||
|
|
||||||
|
reactions_by_prod = {}
|
||||||
|
|
||||||
|
for prod_entity in producible_entities:
|
||||||
|
reactions_by_prod[prod_entity] = []
|
||||||
|
for reaction in self.reactions:
|
||||||
|
if prod_entity in reaction[2]:
|
||||||
|
reactions_by_prod[prod_entity].append([reaction[0],reaction[1]])
|
||||||
|
|
||||||
|
# save in cache
|
||||||
|
self.reactions_by_prod = reactions_by_prod
|
||||||
|
|
||||||
|
return reactions_by_prod
|
||||||
|
|
||||||
|
|
||||||
class ReactionSystemWithAutomaton(object):
|
class ReactionSystemWithAutomaton(object):
|
||||||
@@ -311,12 +432,3 @@ class ReactionSystemWithAutomaton(object):
|
|||||||
self.rs.show(soft)
|
self.rs.show(soft)
|
||||||
self.ca.show()
|
self.ca.show()
|
||||||
|
|
||||||
def sanity_check(self):
|
|
||||||
if self.rs.context_entities != []:
|
|
||||||
raise RuntimeError("Context entities should not be defined within RS!")
|
|
||||||
|
|
||||||
if self.rs.init_contexts != []:
|
|
||||||
raise RuntimeError("Initial context should not be defined!")
|
|
||||||
|
|
||||||
|
|
||||||
# rs should have no initial context, no context entities, etc.
|
|
||||||
|
|||||||
16
rssmt.py
16
rssmt.py
@@ -6,7 +6,7 @@
|
|||||||
|
|
||||||
"""
|
"""
|
||||||
|
|
||||||
from rctsys import ReactionSystem
|
from rctsys import ReactionSystem,ReactionSystemWithConcentrations
|
||||||
from smtchecker import SmtChecker
|
from smtchecker import SmtChecker
|
||||||
from smtcheckerpgrs import SmtCheckerPGRS
|
from smtcheckerpgrs import SmtCheckerPGRS
|
||||||
from smtcheckerdistribrs import SmtCheckerDistribRS
|
from smtcheckerdistribrs import SmtCheckerDistribRS
|
||||||
@@ -42,10 +42,10 @@ def main():
|
|||||||
# smt = SmtCheckerPGRS(rsca)
|
# smt = SmtCheckerPGRS(rsca)
|
||||||
# smt.check_reachability(rs_examples.ca_toy_ex1_property1(), print_time=True)
|
# smt.check_reachability(rs_examples.ca_toy_ex1_property1(), print_time=True)
|
||||||
|
|
||||||
rsca = rs_examples.ca_bitctr(N)
|
# rsca = rs_examples.ca_bitctr(N)
|
||||||
rsca.show(True)
|
# rsca.show(True)
|
||||||
smt = SmtCheckerPGRS(rsca)
|
# smt = SmtCheckerPGRS(rsca)
|
||||||
smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
|
# smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
|
||||||
|
|
||||||
# Distributed RS:
|
# Distributed RS:
|
||||||
#drs = rs_examples.drs_mutex(N)
|
#drs = rs_examples.drs_mutex(N)
|
||||||
@@ -64,6 +64,12 @@ def main():
|
|||||||
# smt = SmtCheckerDistribRS(drs,debug_level=3)
|
# smt = SmtCheckerDistribRS(drs,debug_level=3)
|
||||||
# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True)
|
# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True)
|
||||||
|
|
||||||
|
r = ReactionSystemWithConcentrations()
|
||||||
|
r.add_bg_set_entities(["a","b","c","d"])
|
||||||
|
|
||||||
|
r.add_reaction([("a",1)],[("b",2)],[("c",1)])
|
||||||
|
r.show()
|
||||||
|
|
||||||
if __name__ == "__main__":
|
if __name__ == "__main__":
|
||||||
try:
|
try:
|
||||||
if profiling:
|
if profiling:
|
||||||
|
|||||||
Reference in New Issue
Block a user