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

Production of the maximal concentration

Browse Source 
When multiple reactions are enabled, we produce the maximal concentration by exploiting the fact that reactions are sorted (increasing order).  We build the encoding starting from the inner-most reaction (with the lowest concentration level), and then build around that reaction encoding for the reactions with higher concentration levels. This allows us to avoid the disjunctions of possible resulting concentractions. E.g. (x==1 v x==3 v x==7), while we should have only x==7.
This commit is contained in:
Artur Meski
2016-03-10 12:33:32 +01:00
parent a6aa5e4590
commit 781777ac56
1 changed files with 52 additions and 19 deletions
Download Patch File Download Diff File Expand all files Collapse all files

71
smtcheckerrsc.py
View File

@@ -63,6 +63,18 @@ class SmtCheckerRSC(object):
self.ca_state.append(Int("CA"+str(level)+"_state"))
def enc_nonzero_assertion(self, level):
"""Encodes assertions that (some) variables need to be >0
We do not need to actually control all the variables,
only those that can possibly go below 0.
"""
enc_nz = True
for v in self.v[level]:
enc_nz = simplify(And(enc_nz, v >= 0))
return enc_nz
def enc_init_state(self, level):
"""Encodes the initial state at the given level"""
@@ -100,22 +112,40 @@ class SmtCheckerRSC(object):
# ----------- ordinary reactions --------------------------------------------
enc_rct_prod = False
for reactants,inhibitors,products in rcts_for_prod_entity:
enc_reactants = True
enc_inhibitors = True
# enc_products -- below
for reactant,concentration in reactants:
enc_reactants = simplify(And(enc_reactants,
Or(self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
for inhibitor,concentration in inhibitors:
enc_inhibitors = simplify(And(enc_inhibitors,
And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
enc_reactants = True
for reactant,concentration in reactants:
enc_reactants = simplify(And(enc_reactants,
Or(self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
enc_inhibitors = True
for inhibitor,concentration in inhibitors:
enc_inhibitors = simplify(And(enc_inhibitors,
And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
enc_rct_enabled = And(enc_reactants, enc_inhibitors)
enc_products = self.v[level+1][products[0][0]] == products[0][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)))
enc_rct_prod = simplify(If(enc_rct_enabled, enc_products, enc_rct_prod))
enc_enabledness = simplify(Or(enc_enabledness, enc_rct_enabled))
# for reactants,inhibitors,products in rcts_for_prod_entity:
# enc_reactants = True
# enc_inhibitors = True
# # enc_products -- below
#
# for reactant,concentration in reactants:
# enc_reactants = simplify(And(enc_reactants,
# Or(self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
# for inhibitor,concentration in inhibitors:
# enc_inhibitors = simplify(And(enc_inhibitors,
# And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
#
# enc_products = self.v[level+1][products[0][0]] == products[0][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)))
# -------- meta reactions ---------------------------------------------------
@@ -140,14 +170,14 @@ class SmtCheckerRSC(object):
And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
if r_type == "inc":
enc_products = simplify(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]))
value_after_inc = 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] == value_after_inc
elif r_type == "dec":
enc_products = simplify(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]) - \
value_after_dec = simplify(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] == If(value_after_dec < 0, 0, value_after_dec)
else:
raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
@@ -336,9 +366,12 @@ class SmtCheckerRSC(object):
self.prepare_all_variables()
# self.solver.add(self.enc_nonzero_assertion(0))
while True:
self.prepare_all_variables()
# self.solver.add(self.enc_nonzero_assertion(current_level+1))
print("\n{:-^70}".format("[ Working at level=" + str(current_level) + " ]"))
stdout.flush()