diff --git a/rs_examples.py b/rs_examples.py index ec01e4c..e641c2d 100755 --- a/rs_examples.py +++ b/rs_examples.py @@ -279,7 +279,7 @@ def run_counter_exp(): r.add_bg_set_entity("e") r.add_bg_set_entity("inc") - r.add_reaction_inc("e",[("e",1),("inc",1)],[("e",N)]) + r.add_reaction_inc("e","inc",[("e",1),("inc",1)],[("e",N)]) # for i in range(1,N): # r.add_reaction([("e",i),("inc",1)],[("e",N)],[("e",i+1)]) # r.show() @@ -289,19 +289,19 @@ def run_counter_exp(): c.add_state("working") c.add_transition("init", [("e",1),("inc",1)], "working") c.add_transition("working", [("inc",1)], "working") - # c.show() + # c.show() rc = ReactionSystemWithAutomaton(r,c) rc.show() smt_rsc = SmtCheckerRSC(rc) - smt_rsc.check_reachability([('e',N)],print_time=True,max_level=N) + 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) + 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()) @@ -352,7 +352,7 @@ def chain_reaction(print_system=False): if verify_rsc: smt_rsc = SmtCheckerRSC(rc) prop = [('e_'+str(chainLen),maxConc)] - smt_rsc.check_reachability(prop,max_level=maxConc*chainLen+10) + smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10) # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10) else: @@ -422,7 +422,6 @@ def blood_glucose_regulation(print_system=True): r.add_permanency("sugar",[("expire_sugar",1)]) r.add_permanency("glycemia",[]) - # moje: r.add_reaction([("sugar",1)],[],[("sugar",1)]) @@ -447,6 +446,9 @@ def blood_glucose_regulation(print_system=True): # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10) def heat_shock_response(print_system=True): + + stress_temp = 42 + max_temp = 50 r = ReactionSystemWithConcentrations() r.add_bg_set_entity(("hsp",1)) @@ -459,9 +461,9 @@ def heat_shock_response(print_system=True): r.add_bg_set_entity(("hsf3:hse",1)) r.add_bg_set_entity(("hsp:mfp",1)) r.add_bg_set_entity(("hsp:hsf",1)) - r.add_bg_set_entity(("temp",50)) - - stress_temp = 42 + r.add_bg_set_entity(("temp",max_temp)) + r.add_bg_set_entity(("heat",1)) + r.add_bg_set_entity(("cool",1)) r.add_reaction([("hsf",1)],[("hsp",1)],[("hsf3",1)]) r.add_reaction([("hsf",1),("hsp",1),("mfp",1)],[],[("hsf3",1)]) @@ -483,14 +485,22 @@ def heat_shock_response(print_system=True): r.add_reaction([("mfp",1)],[("hsp",1)],[("mfp",1)]) r.add_reaction([("hsp:mfp",1)],[],[("hsp",1),("prot",1)]) + r.add_reaction_inc("temp", "heat", [("temp",1)],[("temp",max_temp)]) + r.add_reaction_dec("temp", "cool", [("temp",1)],[]) + + r.add_permanency("temp",[("heat",1),("cool",1)]) + #r.add_permanency("temp",[]) + c = ContextAutomatonWithConcentrations(r) c.add_init_state("0") c.add_state("1") - c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",36)], "1") - c.add_transition("0", [("hse",1),("prot",1),("hsp:hsf",1),("temp",stress_temp)], "1") - c.add_transition("0", [("hsp",1),("prot",1),("hsf3:hse",1),("mfp",1),("hsp:mfp",1),("temp",36)], "1") - c.add_transition("1", [("temp",36)], "1") - c.add_transition("1", [("temp",43)], "1") + c.add_transition("0", [("temp",20)], "1") + c.add_transition("1", [("hsf",1),("prot",1),("hse",1),("temp",20)], "1") + #c.add_transition("1", [("hse",1),("prot",1),("hsp:hsf",1),("temp",stress_temp)], "1") + c.add_transition("1", [("hsp",1),("prot",1),("hsf3:hse",1),("mfp",1),("hsp:mfp",1),("temp",20)], "1") + c.add_transition("1", [("heat",1)], "1") + c.add_transition("1", [("cool",1)], "1") + c.add_transition("1", [], "1") # c.add_transition("1", [("sugar",1)], "1") rc = ReactionSystemWithAutomaton(r,c) @@ -500,5 +510,6 @@ def heat_shock_response(print_system=True): smt_rsc = SmtCheckerRSC(rc) prop = ([("hsp",1)],[("temp",stress_temp)]) # no stress - smt_rsc.check_reachability(prop,max_level=10) + #prop = ([("temp",36)],[]) # no stress + smt_rsc.check_reachability(prop,max_level=40) diff --git a/rssmt.py b/rssmt.py index 9269111..c74bad6 100755 --- a/rssmt.py +++ b/rssmt.py @@ -79,4 +79,4 @@ if __name__ == "__main__": # drs.show() # # smt = SmtCheckerDistribRS(drs,debug_level=3) -# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True) \ No newline at end of file +# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True) diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py index 9ef8371..1faa99a 100644 --- a/smtcheckerrsc.py +++ b/smtcheckerrsc.py @@ -91,8 +91,6 @@ class SmtCheckerRSC(object): if prod_entity in self.rs.permanent_entities: permanency_inhibition = self.rs.permanent_entities[prod_entity] - print(prod_entity,permanency_inhibition) - if rcts_for_prod_entity == [] and meta_reactions == []: return simplify(self.v[level+1][prod_entity] == 0) # this should never happen @@ -194,7 +192,6 @@ class SmtCheckerRSC(object): enc_enabledness = simplify(Or(enc_enabledness, And(enc_reactants, enc_inhibitors))) enc_permanency = And(enc_reactants, enc_inhibitors, enc_products) - print(enc_permanency) enc_rct_prod = simplify(Or(enc_rct_prod, enc_permanency)) # ----------------------------------------------------------------------------- @@ -324,7 +321,7 @@ class SmtCheckerRSC(object): for level in range(max_level+1): - print("\n[Level=" + repr(level) + "]") + print("\n{:-^70}".format("[ level=" + repr(level) + " ]")) print(" State: {", end=""), for var_id in range(len(self.v[level])): @@ -397,7 +394,7 @@ class SmtCheckerRSC(object): stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime self.verification_time = stop-start print() - print("[i] Time: " + repr(self.verification_time)) + print("[i] Time: " + repr(self.verification_time) + " s") if print_mem: print("[i] Memory: " + repr(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)) + " MB")