From 781777ac5657f3d4b8ef10fd829afe8bde80205a Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Thu, 10 Mar 2016 12:33:32 +0100 Subject: [PATCH] Production of the maximal concentration 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. --- smtcheckerrsc.py | 71 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 52 insertions(+), 19 deletions(-) diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py index 92c18dc..fda4936 100644 --- a/smtcheckerrsc.py +++ b/smtcheckerrsc.py @@ -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()