artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Translation RSC->RS for meta-reactions.

Browse Source
This commit is contained in:
Artur Meski
2016-02-21 14:55:48 +01:00
parent 060f5dc1f5
commit b21a0cee48
3 changed files with 82 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

42
rctsys.py
View File

@@ -484,7 +484,11 @@ class ReactionSystemWithConcentrations(ReactionSystem):
print("[*] Meta reactions:")
for incr_ent,reactions in self.meta_reactions.items():
for r_type,reactants,inhibitors in reactions:
print("\t - [ Type=" + repr(r_type) + " Parameter=( " + self.get_entity_name(incr_ent) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )")
if r_type == "inc":
print("\t - [ Type=" + repr(r_type) + " Parameter=( " + self.get_entity_name(incr_ent) + \
" ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )")
else:
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
def show(self, soft=False):
self.show_background_set()
@@ -548,6 +552,42 @@ class ReactionSystemWithConcentrations(ReactionSystem):
rs.add_reaction(new_reactants,new_inhibitors,new_products)
for incr_ent,reactions in self.meta_reactions.items():
for r_type,reactants,inhibitors in reactions:
if r_type == "inc":
incr_ent_name = self.get_entity_name(incr_ent)
new_reactants = []
new_inhibitors = []
for ent,conc in reactants:
n = self.get_entity_name(ent) + "_" + str(conc)
rs.ensure_bg_set_entity(n)
new_reactants.append(n)
for ent,conc in inhibitors:
n = self.get_entity_name(ent) + "_" + str(conc)
rs.ensure_bg_set_entity(n)
new_inhibitors.append(n)
pre_conc = incr_ent_name + "_" + str(1)
rs.ensure_bg_set_entity(pre_conc)
for i in range(1,self.max_concentration):
succ_conc = incr_ent_name + "_" + str(i+1)
rs.ensure_bg_set_entity(succ_conc)
new_products = []
for j in range(1,i+1):
new_p = incr_ent_name + "_" + str(j)
rs.ensure_bg_set_entity(new_p)
new_products.append(new_p)
new_products.append(succ_conc)
rs.add_reaction(new_reactants + [pre_conc], new_inhibitors, new_products)
pre_conc = succ_conc
else:
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
return rs

12
rssmt.py
View File

@@ -18,7 +18,7 @@ import resource
profiling = False
version = "0.002"
version = "2016/02/21/00"
rsmc_banner = """
*** Reaction Systems SMT-Based Model Checking
@@ -89,13 +89,13 @@ def main():
smt_rsc = SmtCheckerRSC(rc)
smt_rsc.check_reachability([('e',N)],print_time=True,max_level=N)
# orc = rc.get_ordinary_reaction_system_with_automaton()
# orc.show()
# smt_tr_rs = SmtCheckerPGRS(orc)
# smt_tr_rs.check_reachability(['e_' + str(N)],print_time=True)
orc = rc.get_ordinary_reaction_system_with_automaton()
orc.show()
smt_tr_rs = SmtCheckerPGRS(orc)
smt_tr_rs.check_reachability(['e_' + str(N)],print_time=True)
print("Reaction System with Concentrations:", smt_rsc.get_verification_time())
# print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time())
print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time())
if __name__ == "__main__":
try:

42
smtcheckerrsc.py
View File

@@ -111,6 +111,8 @@ class SmtCheckerRSC(object):
# -------- meta reactions ---------------------------------------------------
for r_type,reactants,inhibitors in meta_reactions:
if r_type == "inc":
enc_reactants = True
enc_inhibitors = True
@@ -122,11 +124,13 @@ class SmtCheckerRSC(object):
And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]+1
enc_enabledness = simplify(Or(enc_enabledness, And(enc_reactants, enc_inhibitors)))
enc_rct_prod = simplify(Or(enc_rct_prod, And(enc_reactants, enc_inhibitors, enc_products)))
else:
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
# -----------------------------------------------------------------------------
enc_when_to_produce_zero_conc = simplify(And(Not(enc_enabledness), self.v[level+1][prod_entity] == 0))
@@ -160,7 +164,6 @@ class SmtCheckerRSC(object):
for prod_entity in chain(reactions, meta_reactions):
unused_entities.remove(prod_entity)
enc_trans = simplify(And(enc_trans, self.enc_produced_concentration(level, prod_entity)))
for prod_entity in unused_entities:
@@ -198,20 +201,22 @@ class SmtCheckerRSC(object):
def enc_exact_state(self, level, state):
"""Encodes the state at the given level with the exact concentration values"""
enc = True
used_entities_ids = self.rs.get_state_ids(state)
raise RuntimeError("Should not be used with RSC")
for ent,conc in state:
e_id = self.rs.get_entity_id(ent)
enc = And(enc, self.v[level][e_id] == conc)
not_in_state = set(range(len(self.rs.background_set)))
not_in_state = not_in_state.difference(set(used_entities_ids))
for entity in not_in_state:
enc = And(enc, self.v[level][entity] == 0)
return simplify(enc)
# enc = True
# used_entities_ids = self.rs.get_state_ids(state)
#
# for ent,conc in state:
# e_id = self.rs.get_entity_id(ent)
# enc = And(enc, self.v[level][e_id] == conc)
#
# not_in_state = set(range(len(self.rs.background_set)))
# not_in_state = not_in_state.difference(set(used_entities_ids))
#
# for entity in not_in_state:
# enc = And(enc, self.v[level][entity] == 0)
#
# return simplify(enc)
def enc_min_state(self, level, state):
"""Encodes the state at the given level with the minimal required concentration levels"""
@@ -260,7 +265,7 @@ class SmtCheckerRSC(object):
print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
print(" }")
def check_reachability(self, state, exact_state=False, print_witness=True,
def check_reachability(self, state, print_witness=True,
print_time=False, print_mem=False, max_level=100):
"""Main testing function"""
@@ -283,9 +288,6 @@ class SmtCheckerRSC(object):
print("[i] Adding the reachability test...")
self.solver.push()
if exact_state:
self.solver.add(self.enc_exact_state(current_level,state))
else:
self.solver.add(self.enc_min_state(current_level,state))
result = self.solver.check()