diff --git a/rs/context_automaton_with_concentrations.py b/rs/context_automaton_with_concentrations.py index 04ac2e3..4310cc5 100644 --- a/rs/context_automaton_with_concentrations.py +++ b/rs/context_automaton_with_concentrations.py @@ -60,4 +60,10 @@ class ContextAutomatonWithConcentrations(ContextAutomaton): ca.add_transition(ca.get_state_name(src),new_ctx,ca.get_state_name(dst)) - return ca + return ca + + def show(self): + self.show_header() + self.show_states() + self.show_transitions() + diff --git a/rs_testing.py b/rs_testing.py index 3eb2bc4..c7a200e 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -2,17 +2,94 @@ from rs import * from smt import * import rs_examples from logics import * +import sys +import resource def run_tests(): # test_extended_automaton() # process() - test_rsLTL() + heat_shock_response() + +def heat_shock_response(print_system=True): + + stress_temp = 42 + max_temp = 50 + + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("hsp",1)) + r.add_bg_set_entity(("hsf",1)) + r.add_bg_set_entity(("hsf2",1)) + r.add_bg_set_entity(("hsf3",1)) + r.add_bg_set_entity(("hse",1)) + r.add_bg_set_entity(("mfp",1)) + r.add_bg_set_entity(("prot",1)) + 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",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)]) + r.add_reaction([("hsf3",1)], [("hse",1),("hsp",1)],[("hsf",1)]) + r.add_reaction([("hsf3",1),("hsp",1),("mfp",1)], [("hse",1)], [("hsf",1)]) + r.add_reaction([("hsf3",1),("hse",1)], [("hsp",1)], [("hsf3:hse",1)]) + r.add_reaction([("hsp",1),("hsf3",1),("mfp",1),("hse",1)],[], [("hsf3:hse",1)]) + r.add_reaction([("hse",1)], [("hsf3",1)], [("hse",1)]) + r.add_reaction([("hsp",1),("hsf3",1),("hse",1)], [("mfp",1)], [("hse",1)]) + r.add_reaction([("hsf3:hse",1)], [("hsp",1)], [("hsp",1),("hsf3:hse",1)]) + r.add_reaction([("hsp",1),("mfp",1),("hsf3:hse",1)],[], [("hsp",1),("hsf3:hse",1)]) + r.add_reaction([("hsf",1),("hsp",1)], [("mfp",1)], [("hsp:hsf",1)]) + r.add_reaction([("hsp:hsf",1),("temp",stress_temp)],[], [("hsf",1),("hsp",1)]) + r.add_reaction([("hsp:hsf",1)], [("temp",stress_temp)],[("hsp:hsf",1)]) + r.add_reaction([("hsp",1),("hsf3:hse",1)], [("mfp",1)], [("hse",1),("hsp:hsf",1)]) + r.add_reaction([("temp",stress_temp),("prot",1)], [], [("mfp",1),("prot",1)]) + r.add_reaction([("prot",1)], [("temp",stress_temp)], [("prot",1)]) + r.add_reaction([("hsp",1),("mfp",1)], [], [("hsp:mfp",1)]) + 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)]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("0") + c.add_state("1") + c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",35)], "1") + c.add_transition("1", [("cool",1)], "1") + c.add_transition("1", [("heat",1)], "1") + c.add_transition("1", [], "1") + + rc = ReactionSystemWithAutomaton(r,c) + + if print_system: + rc.show() + + # prop_req = [("hsp:hsf",1),("hse",1),("prot",1)] + # prop_block = [("temp",stress_temp)] + prop_req = [ ("mfp",1) ] + prop_block = [ ] + prop = (prop_req,prop_block) + rs_prop = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block)) + + f_reach_mfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("mfp") > 0) ) + + smt_rsc = SmtCheckerRSC(rc) + # smt_rsc.check_reachability(prop,max_level=40) + smt_rsc.check_rsltl(formula=f_reach_mfp) + +def state_translate_rsc2rs(p): + return [e[0] + "#" + str(e[1]) for e in p] def test_rsLTL(): r = ReactionSystemWithConcentrations() r.add_bg_set_entity(("inc",2)) + r.add_bg_set_entity(("ent1",1)) r.add_bg_set_entity(("ent2",5)) r.add_reaction([("ent2",1),("inc",1)],[],[("ent2",2)]) r.add_reaction([("ent2",2)],[],[("ent2",2)]) @@ -24,9 +101,9 @@ def test_rsLTL(): c.add_transition("working", [("inc",1)], "working") # x = ( Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) - # x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) + x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) - x = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("ent2") == 2) ) + #x = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("ent2") == 2) ) print(x) diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 42bd98d..2c8926b 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -370,6 +370,8 @@ class SmtCheckerRSC(object): def check_rsltl(self, formula, print_witness=True, print_time=True, print_mem=True, max_level=None): """Bounded Model Checking for rsLTL properties""" + print("[" + colour_str(C_BOLD, "i") + "] Running rsLTL bounded model checking") + if print_time: # start = time() start = resource.getrusage(resource.RUSAGE_SELF).ru_utime @@ -392,11 +394,12 @@ class SmtCheckerRSC(object): stdout.flush() # reachability test: - print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...") self.solver.push() - + print("[" + colour_str(C_BOLD, "i") + "] Adding the formula encoding...") f = encoder.encode(formula, 0, self.current_level) self.solver.add(f) + + print("[" + colour_str(C_BOLD, "i") + "] Adding the loops encoding...") self.solver.add(self.get_loop_encodings()) result = self.solver.check()