Incrementation & decrementation by a specified value.
This commit is contained in:
Artur Meski
8
mkplotdat.sh
Executable file
8
mkplotdat.sh
Executable file
@@ -0,0 +1,8 @@
|
||||
#!/bin/sh
|
||||
if [ "$1" = "" ];then
|
||||
echo "Usage: $0 <input file>"
|
||||
exit 1
|
||||
fi
|
||||
f="$1"
|
||||
cat $f | tr -d '()' | tr ',' '\t'
|
||||
|
||||
155
rctsys.py
155
rctsys.py
@@ -185,7 +185,7 @@ class ContextAutomatonWithConcentrations(ContextAutomaton):
|
||||
|
||||
for ent,conc in ctx:
|
||||
for i in range(1,conc+1):
|
||||
n = self._reaction_system.get_entity_name(ent) + "_" + str(i)
|
||||
n = self._reaction_system.get_entity_name(ent) + "#" + str(i)
|
||||
ca._reaction_system.ensure_bg_set_entity(n)
|
||||
new_ctx.add(n)
|
||||
|
||||
@@ -207,19 +207,21 @@ class ReactionSystem(object):
|
||||
self.init_contexts = []
|
||||
self.context_entities = []
|
||||
|
||||
def add_bg_set_entity(self, name):
|
||||
if not self.is_in_background_set(name):
|
||||
self.background_set.append(name)
|
||||
else:
|
||||
def assume_not_in_bgset(self, name):
|
||||
if self.is_in_background_set(name):
|
||||
raise RuntimeError("The entity " + name + " is already on the list")
|
||||
|
||||
def add_bg_set_entity(self, name):
|
||||
self.assume_not_in_bgset(name)
|
||||
self.background_set.append(name)
|
||||
|
||||
def ensure_bg_set_entity(self, name):
|
||||
if not self.is_in_background_set(name):
|
||||
self.background_set.append(name)
|
||||
|
||||
def add_bg_set_entities(self, names):
|
||||
for name in names:
|
||||
self.add_bg_set_entity(name)
|
||||
def add_bg_set_entities(self, elements):
|
||||
for e in elements:
|
||||
self.add_bg_set_entity(e)
|
||||
|
||||
def is_in_background_set(self, entity):
|
||||
"""Checks if the given name is valid wrt the background set="""
|
||||
@@ -250,7 +252,7 @@ class ReactionSystem(object):
|
||||
"""Adds a reaction"""
|
||||
|
||||
if R == [] or P == []:
|
||||
raise RuntimeError("No reactants of products defined")
|
||||
raise RuntimeError("No reactants or products defined")
|
||||
|
||||
reactants = []
|
||||
for entity in R:
|
||||
@@ -380,6 +382,28 @@ class ReactionSystemWithConcentrations(ReactionSystem):
|
||||
self.reactions_by_prod = None
|
||||
|
||||
self.max_concentration = 0
|
||||
self.max_conc_per_ent = dict()
|
||||
|
||||
def add_bg_set_entity(self, e):
|
||||
name = ""
|
||||
def_max_conc = -1
|
||||
if type(e) is tuple and len(e) == 2:
|
||||
name,def_max_conc = e
|
||||
elif type(e) is str:
|
||||
name = e
|
||||
else:
|
||||
raise RuntimeError("Bad entity type when adding background set element")
|
||||
|
||||
self.assume_not_in_bgset(name)
|
||||
self.background_set.append(name)
|
||||
|
||||
if def_max_conc != -1:
|
||||
ent_id = self.get_entity_id(name)
|
||||
self.max_conc_per_ent.setdefault(ent_id, 0)
|
||||
if self.max_conc_per_ent[ent_id] < def_max_conc:
|
||||
self.max_conc_per_ent[ent_id] = def_max_conc
|
||||
if self.max_concentration < def_max_conc:
|
||||
self.max_concentration = def_max_conc
|
||||
|
||||
def is_valid_entity_with_concentration(self, e):
|
||||
"""Sanity check for entities with concentration"""
|
||||
@@ -406,7 +430,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
|
||||
if elem[1] < 1:
|
||||
raise RuntimeError("Unexpected concentration level in state: " + str(elem))
|
||||
|
||||
def process_rip(self, R, I, P):
|
||||
def check_rip(self, R, I, P):
|
||||
"""Chcecks concentration levels and converts entities names into their ids"""
|
||||
|
||||
if R == []:
|
||||
@@ -442,24 +466,24 @@ class ReactionSystemWithConcentrations(ReactionSystem):
|
||||
|
||||
if P == []:
|
||||
raise RuntimeError("No products defined")
|
||||
reaction = self.process_rip(R,I,P)
|
||||
reaction = self.check_rip(R,I,P)
|
||||
self.reactions.append(reaction)
|
||||
|
||||
def add_reaction_inc(self, incr_entity, R, I):
|
||||
def add_reaction_inc(self, incr_entity, incrementer, R, I):
|
||||
"""Adds a macro/meta reaction for increasing the value of incr_entity"""
|
||||
|
||||
reactants,inhibitors,products = self.process_rip(R,I,[])
|
||||
reactants,inhibitors,products = self.check_rip(R,I,[])
|
||||
incr_entity_id = self.get_entity_id(incr_entity)
|
||||
self.meta_reactions.setdefault(incr_entity_id,[])
|
||||
self.meta_reactions[incr_entity_id].append(("inc", reactants, inhibitors))
|
||||
self.meta_reactions[incr_entity_id].append(("inc", self.get_entity_id(incrementer), reactants, inhibitors))
|
||||
|
||||
def add_reaction_dec(self, incr_entity, R, I):
|
||||
def add_reaction_dec(self, decr_entity, decrementer, R, I):
|
||||
"""Adds a macro/meta reaction for decreasing the value of incr_entity"""
|
||||
|
||||
reactants,inhibitors,products = self.process_rip(R,I,[])
|
||||
reactants,inhibitors,products = self.check_rip(R,I,[])
|
||||
decr_entity_id = self.get_entity_id(decr_entity)
|
||||
self.meta_reactions.setdefault(decr_entity_id,[])
|
||||
self.meta_reactions[decr_entity_id].append(("dec", reactants, inhibitors))
|
||||
self.meta_reactions[decr_entity_id].append(("dec", self.get_entity_id(decrementer), reactants, inhibitors))
|
||||
|
||||
def set_context_entities(self, entities):
|
||||
raise NotImplementedError
|
||||
@@ -491,10 +515,10 @@ class ReactionSystemWithConcentrations(ReactionSystem):
|
||||
def show_meta_reactions(self):
|
||||
print("[*] Meta reactions:")
|
||||
for param_ent,reactions in self.meta_reactions.items():
|
||||
for r_type,reactants,inhibitors in reactions:
|
||||
for r_type,command,reactants,inhibitors in reactions:
|
||||
if r_type == "inc" or r_type == "dec":
|
||||
print("\t - [ Type=" + repr(r_type) + " Parameter=( " + self.get_entity_name(param_ent) + \
|
||||
" ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )")
|
||||
print("\t - [ Type=" + repr(r_type) + " Operand=( " + self.get_entity_name(param_ent) + \
|
||||
" ) Command=( " + self.get_entity_name(command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )")
|
||||
else:
|
||||
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
|
||||
|
||||
@@ -543,72 +567,87 @@ class ReactionSystemWithConcentrations(ReactionSystem):
|
||||
new_products = []
|
||||
|
||||
for ent,conc in reactants:
|
||||
n = self.get_entity_name(ent) + "_" + str(conc)
|
||||
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)
|
||||
n = self.get_entity_name(ent) + "#" + str(conc)
|
||||
rs.ensure_bg_set_entity(n)
|
||||
new_inhibitors.append(n)
|
||||
|
||||
for ent,conc in products:
|
||||
for i in range(1,conc+1):
|
||||
n = self.get_entity_name(ent) + "_" + str(i)
|
||||
n = self.get_entity_name(ent) + "#" + str(i)
|
||||
rs.ensure_bg_set_entity(n)
|
||||
new_products.append(n)
|
||||
|
||||
rs.add_reaction(new_reactants,new_inhibitors,new_products)
|
||||
|
||||
for param_ent,reactions in self.meta_reactions.items():
|
||||
for r_type,reactants,inhibitors in reactions:
|
||||
for r_type,command,reactants,inhibitors in reactions:
|
||||
|
||||
param_ent_name = self.get_entity_name(param_ent)
|
||||
|
||||
new_reactants = []
|
||||
new_inhibitors = []
|
||||
|
||||
|
||||
for ent,conc in reactants:
|
||||
n = self.get_entity_name(ent) + "_" + str(conc)
|
||||
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)
|
||||
n = self.get_entity_name(ent) + "#" + str(conc)
|
||||
rs.ensure_bg_set_entity(n)
|
||||
new_inhibitors.append(n)
|
||||
|
||||
if r_type == "inc":
|
||||
|
||||
# pre_conc -- predecessor concentration
|
||||
# succ_conc -- successor concentration concentration
|
||||
|
||||
for i in range(1,self.max_concentration):
|
||||
pre_conc = param_ent_name + "_" + str(i)
|
||||
rs.ensure_bg_set_entity(pre_conc)
|
||||
new_products = []
|
||||
succ_value = i+1
|
||||
for j in range(1,succ_value+1):
|
||||
new_p = param_ent_name + "_" + str(j)
|
||||
rs.ensure_bg_set_entity(new_p)
|
||||
new_products.append(new_p)
|
||||
rs.add_reaction(new_reactants + [pre_conc], new_inhibitors, new_products)
|
||||
|
||||
elif r_type == "dec":
|
||||
|
||||
for i in range(1,self.max_concentration):
|
||||
pre_conc = param_ent_name + "_" + str(i+1)
|
||||
rs.ensure_bg_set_entity(pre_conc)
|
||||
new_products = []
|
||||
succ_value = i
|
||||
for j in range(1,succ_value+1):
|
||||
new_p = param_ent_name + "_" + str(j)
|
||||
rs.ensure_bg_set_entity(new_p)
|
||||
new_products.append(new_p)
|
||||
rs.add_reaction(new_reactants + [pre_conc], new_inhibitors, new_products)
|
||||
|
||||
max_cmd_c = self.max_concentration
|
||||
if command in self.max_conc_per_ent:
|
||||
max_cmd_c = self.max_conc_per_ent[command]
|
||||
else:
|
||||
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
|
||||
print("WARNING:\n\tThere is no maximal concentration level defined for " + self.get_entity_name(command))
|
||||
print("\tThis is a very bad idea -- expect degraded performance\n")
|
||||
|
||||
for l in range(1,max_cmd_c+1):
|
||||
|
||||
cmd_ent = self.get_entity_name(command) + "#" + str(l)
|
||||
rs.ensure_bg_set_entity(cmd_ent)
|
||||
|
||||
if r_type == "inc":
|
||||
|
||||
# pre_conc -- predecessor concentration
|
||||
# succ_conc -- successor concentration concentration
|
||||
|
||||
for i in range(1,self.max_concentration):
|
||||
pre_conc = param_ent_name + "#" + str(i)
|
||||
rs.ensure_bg_set_entity(pre_conc)
|
||||
new_products = []
|
||||
succ_value = i+l
|
||||
for j in range(1,succ_value+1):
|
||||
if j > self.max_concentration: break
|
||||
new_p = param_ent_name + "#" + str(j)
|
||||
rs.ensure_bg_set_entity(new_p)
|
||||
new_products.append(new_p)
|
||||
if new_products != []:
|
||||
rs.add_reaction(set(new_reactants + [pre_conc,cmd_ent]), set(new_inhibitors), set(new_products))
|
||||
|
||||
elif r_type == "dec":
|
||||
for i in range(1,self.max_concentration+1):
|
||||
pre_conc = param_ent_name + "#" + str(i)
|
||||
rs.ensure_bg_set_entity(pre_conc)
|
||||
new_products = []
|
||||
succ_value = i-l
|
||||
for j in range(1,succ_value+1):
|
||||
if j > self.max_concentration: break
|
||||
new_p = param_ent_name + "#" + str(j)
|
||||
rs.ensure_bg_set_entity(new_p)
|
||||
new_products.append(new_p)
|
||||
if new_products != []:
|
||||
rs.add_reaction(set(new_reactants + [pre_conc,cmd_ent]), set(new_inhibitors), set(new_products))
|
||||
|
||||
else:
|
||||
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
|
||||
|
||||
return rs
|
||||
|
||||
|
||||
@@ -323,15 +323,16 @@ def chain_reaction(print_system=False):
|
||||
exit(1)
|
||||
|
||||
r = ReactionSystemWithConcentrations()
|
||||
r.add_bg_set_entity("inc")
|
||||
r.add_bg_set_entity("dec")
|
||||
r.add_bg_set_entity(("inc",1))
|
||||
r.add_bg_set_entity(("dec",1))
|
||||
|
||||
for i in range(1,chainLen+1):
|
||||
r.add_bg_set_entity("e_" + str(i))
|
||||
|
||||
for i in range(1,chainLen+1):
|
||||
ent = "e_" + str(i)
|
||||
r.add_reaction_inc(ent, [(ent, 1),("inc",1)],[(ent,maxConc)])
|
||||
r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
|
||||
r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
|
||||
if i < chainLen:
|
||||
r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
|
||||
|
||||
@@ -350,15 +351,17 @@ def chain_reaction(print_system=False):
|
||||
|
||||
if verify_rsc:
|
||||
smt_rsc = SmtCheckerRSC(rc)
|
||||
smt_rsc.check_reachability([('e_'+str(chainLen),maxConc)],max_level=maxConc*chainLen+10)
|
||||
# smt_rsc.show_encoding([('e_'+str(1),1)],print_time=True,max_level=maxConc*chainLen+10)
|
||||
prop = [('e_'+str(chainLen),maxConc)]
|
||||
smt_rsc.check_reachability(prop,max_level=maxConc*chainLen+10)
|
||||
# smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10)
|
||||
|
||||
if not verify_rsc:
|
||||
else:
|
||||
orc = rc.get_ordinary_reaction_system_with_automaton()
|
||||
if print_system:
|
||||
print("\nTranslated:")
|
||||
orc.show()
|
||||
smt_tr_rs = SmtCheckerPGRS(orc)
|
||||
smt_tr_rs.check_reachability(['e_'+str(chainLen)+"_"+str(maxConc)])
|
||||
smt_tr_rs.check_reachability(['e_'+str(chainLen)+"#"+str(maxConc)])
|
||||
|
||||
# print("Reaction System with Concentrations:", smt_rsc.get_verification_time())
|
||||
# print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time())
|
||||
|
||||
2
rssmt.py
2
rssmt.py
@@ -29,7 +29,7 @@ rsmc_banner = """
|
||||
def process():
|
||||
|
||||
# rs_examples.run_counter_exp()
|
||||
rs_examples.chain_reaction()
|
||||
rs_examples.chain_reaction(print_system=True)
|
||||
|
||||
##################################################################
|
||||
|
||||
|
||||
@@ -8,8 +8,8 @@ from sys import stdout
|
||||
from itertools import chain
|
||||
import resource
|
||||
|
||||
# def simplify(x):
|
||||
# return x
|
||||
def simplify(x):
|
||||
return x
|
||||
|
||||
class SmtCheckerRSC(object):
|
||||
|
||||
@@ -114,26 +114,59 @@ class SmtCheckerRSC(object):
|
||||
|
||||
# -------- meta reactions ---------------------------------------------------
|
||||
|
||||
for r_type,reactants,inhibitors in meta_reactions:
|
||||
for r_type,command_entity,reactants,inhibitors in meta_reactions:
|
||||
|
||||
# command entity is e.g. 'inc' for incrementation operation
|
||||
# (inc,W) gives us the value W by which the given entity's value should be incremented
|
||||
|
||||
enc_reactants = True
|
||||
enc_inhibitors = True
|
||||
|
||||
for reactant,concentration in reactants:
|
||||
enc_reactants = simplify(And(enc_reactants,
|
||||
enc_reactants = simplify(And(enc_reactants,
|
||||
Or(self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
|
||||
|
||||
# command entity needs to be present (with concentration level > 0) in order to perform the operation
|
||||
enc_reactants = simplify(And(enc_reactants,
|
||||
Or(self.v[level][command_entity] > 0, self.v_ctx[level][command_entity] > 0)))
|
||||
|
||||
for inhibitor,concentration in inhibitors:
|
||||
enc_inhibitors = simplify(And(enc_inhibitors,
|
||||
And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
|
||||
|
||||
if r_type == "inc":
|
||||
|
||||
enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]+1
|
||||
# if r_type == "inc":
|
||||
# # depending on if the value of the command entity is greater in the context or in the current RS state
|
||||
# # we choose to increment by the greater value from v or v_ctx (this is because we take the max value).
|
||||
# enc_products = Or(
|
||||
# And(self.v_ctx[level][command_entity] >= self.v[level][command_entity],
|
||||
# self.v[level+1][prod_entity] == If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity])+self.v_ctx[level][command_entity]),
|
||||
# And(self.v[level][command_entity] > self.v_ctx[level][command_entity],
|
||||
# self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])+self.v[level][command_entity]))
|
||||
#
|
||||
# elif r_type == "dec":
|
||||
# # same happens here, but we decrement with the maximum value encoded at v or v_ctx.
|
||||
# enc_products = Or(
|
||||
# And(self.v_ctx[level][command_entity] >= self.v[level][command_entity],
|
||||
# self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])-self.v_ctx[level][command_entity]),
|
||||
# And(self.v[level][command_entity] > self.v_ctx[level][command_entity],
|
||||
# self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])-self.v[level][command_entity]))
|
||||
#
|
||||
# if r_type == "inc":
|
||||
# enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]+1
|
||||
#
|
||||
# elif r_type == "dec":
|
||||
# enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]-1
|
||||
|
||||
elif r_type == "dec":
|
||||
if r_type == "inc":
|
||||
enc_products = self.v[level+1][prod_entity] == \
|
||||
If(self.v[level][prod_entity]>self.v_ctx[level][prod_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity]) + \
|
||||
If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity])
|
||||
|
||||
elif r_type == "dec":
|
||||
enc_products = self.v[level+1][prod_entity] == \
|
||||
If(self.v[level][prod_entity]>self.v_ctx[level][prod_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity]) - \
|
||||
If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity])
|
||||
|
||||
enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]-1
|
||||
|
||||
else:
|
||||
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
|
||||
|
||||
@@ -355,7 +388,8 @@ class SmtCheckerRSC(object):
|
||||
self.solver.push()
|
||||
|
||||
s = self.enc_min_state(current_level,state)
|
||||
print(s)
|
||||
print("Test: ", s)
|
||||
|
||||
self.solver.add(s)
|
||||
|
||||
result = self.solver.check()
|
||||
|
||||
Reference in New Issue
Block a user