diff --git a/rctsys.py b/rctsys.py index 32568c5..28c8d28 100755 --- a/rctsys.py +++ b/rctsys.py @@ -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 diff --git a/rssmt.py b/rssmt.py index ad3189c..cc11c86 100755 --- a/rssmt.py +++ b/rssmt.py @@ -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: diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py index 881f7a5..3cdd7d0 100644 --- a/smtcheckerrsc.py +++ b/smtcheckerrsc.py @@ -111,22 +111,26 @@ class SmtCheckerRSC(object): # -------- meta reactions --------------------------------------------------- for r_type,reactants,inhibitors in meta_reactions: - enc_reactants = True - enc_inhibitors = True - 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][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))) + if r_type == "inc": + enc_reactants = True + enc_inhibitors = True + 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][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) - - for ent,conc in state: - e_id = self.rs.get_entity_id(ent) - enc = And(enc, self.v[level][e_id] == conc) + raise RuntimeError("Should not be used with RSC") - 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,10 +288,7 @@ 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)) + self.solver.add(self.enc_min_state(current_level,state)) result = self.solver.check() if result == sat: