From 203182c520b732ae9a984d820ef41af573aae07d Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 3 Sep 2017 14:53:08 +0100 Subject: [PATCH] parametric example --- rs_testing.py | 272 ++++++++++++++++++++++++++++---------------------- 1 file changed, 150 insertions(+), 122 deletions(-) diff --git a/rs_testing.py b/rs_testing.py index 641bf88..6bb523d 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -12,150 +12,101 @@ def run_tests(): # heat_shock_response() # scalable_chain(print_system=True) # example44() - example44_param() + # example44_param() + trivial_param() + + +def trivial_param(): -def example44_param(): - r = ReactionSystemWithConcentrationsParam() - r.add_bg_set_entity(("x",2)) - r.add_bg_set_entity(("y",4)) - r.add_bg_set_entity(("h",2)) - r.add_bg_set_entity(("m",1)) - - r.add_reaction([("y",1),("x",1)], [("y",2),("h",1)], [("y",2)]) - r.add_reaction([("y",2),("x",2)], [("y",3),("h",1)], [("y",3)]) - r.add_reaction([("y",3),("h",1)], [("y",4),("h",2)], [("y",4)]) - r.add_reaction([("y",4),("h",1)], [("h",2)], [("y",3)]) - r.add_reaction([("y",4),("x",2)], [("h",1)], [("y",2)]) - r.add_reaction([("m",1)], [("y",3)], [("m",1)]) - + r.add_bg_set_entity(("x", 3)) + r.add_bg_set_entity(("y", 3)) + r.add_bg_set_entity(("c", 3)) + r.add_bg_set_entity(("z", 3)) + r.add_bg_set_entity(("final", 1)) + + r.add_reaction([("x", 1)], [("c", 1)], [("y", 2)]) + r.add_reaction([("y", 1)], [("c", 1)], [("z", 1)]) + r.add_reaction([("z", 1)], [("c", 1)], [("final", 1)]) + c = ContextAutomatonWithConcentrations(r) c.add_init_state("0") c.add_state("1") - c.add_transition("0", [("y",1),("m",1),("x",1)], "1") - c.add_transition("1", [("x",1)], "1") - c.add_transition("1", [("x",1),("h",1)], "1") - c.add_transition("1", [("x",2)], "1") - c.add_transition("1", [("x",2),("h",1)], "1") - c.add_transition("1", [("h",1)], "1") + c.add_transition("0", [("x", 1)], "1") + c.add_transition("1", [], "1") - - rc = ReactionSystemWithAutomaton(r,c) + rc = ReactionSystemWithAutomaton(r, c) rc.show() smt_rsc = SmtCheckerRSCParam(rc) - - # Universal property which seems to be true: (holds also existentially) - f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_Implies( - (BagDescription.f_entity('y') == 2), - Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1), - BagDescription.f_entity("y") >= 3 - ) - ) - ) - - # lets see if we can find a counterexample to this property: - neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_And( - (BagDescription.f_entity('y') == 2), - Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1), - BagDescription.f_entity("y") < 3 - ) - ) - ) - - # we fix the property f1 - # this one holds: - f2 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_Implies( - (BagDescription.f_entity('y') == 2), - Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1) & (BagDescription.f_entity("h") < 1), - BagDescription.f_entity("y") >= 3 - ) - ) - ) - - # neg_f1 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, - # Formula_rsLTL.f_And( - # (BagDescription.f_entity('y') > 0), - # Formula_rsLTL.f_X( - # BagDescription.f_entity("x") > 0, - # Formula_rsLTL.f_X( - # BagDescription.f_entity("x") > 1, - # BagDescription.f_entity("y") < 3 - # ) - # ) - # ) - # )) - smt_rsc.check_rsltl(formula=neg_f1) - -def example44(): - - r = ReactionSystemWithConcentrations() - r.add_bg_set_entity(("x",2)) - r.add_bg_set_entity(("y",4)) - r.add_bg_set_entity(("h",2)) - r.add_bg_set_entity(("m",1)) - - r.add_reaction([("y",1),("x",1)], [("y",2),("h",1)], [("y",2)]) - r.add_reaction([("y",2),("x",2)], [("y",3),("h",1)], [("y",3)]) - r.add_reaction([("y",3),("h",1)], [("y",4),("h",2)], [("y",4)]) - r.add_reaction([("y",4),("h",1)], [("h",2)], [("y",3)]) - r.add_reaction([("y",4),("x",2)], [("h",1)], [("y",2)]) - r.add_reaction([("m",1)], [("y",3)], [("m",1)]) - + + f2 = Formula_rsLTL.f_F( + BagDescription.f_TRUE(), + BagDescription.f_entity("final") >= 1) + + smt_rsc.check_rsltl(formula=f2) + + +def example44_param(): + + r = ReactionSystemWithConcentrationsParam() + r.add_bg_set_entity(("x", 2)) + r.add_bg_set_entity(("y", 4)) + r.add_bg_set_entity(("h", 2)) + r.add_bg_set_entity(("m", 1)) + + r.add_reaction([("y", 1), ("x", 1)], [("y", 2), ("h", 1)], [("y", 2)]) + r.add_reaction([("y", 2), ("x", 2)], [("y", 3), ("h", 1)], [("y", 3)]) + r.add_reaction([("y", 3), ("h", 1)], [("y", 4), ("h", 2)], [("y", 4)]) + r.add_reaction([("y", 4), ("h", 1)], [("h", 2)], [("y", 3)]) + r.add_reaction([("y", 4), ("x", 2)], [("h", 1)], [("y", 2)]) + r.add_reaction([("m", 1)], [("y", 3)], [("m", 1)]) + c = ContextAutomatonWithConcentrations(r) c.add_init_state("0") c.add_state("1") - c.add_transition("0", [("y",1),("m",1),("x",1)], "1") - c.add_transition("1", [("x",1)], "1") - c.add_transition("1", [("x",1),("h",1)], "1") - c.add_transition("1", [("x",2)], "1") - c.add_transition("1", [("x",2),("h",1)], "1") - c.add_transition("1", [("h",1)], "1") + c.add_transition("0", [("y", 1), ("m", 1), ("x", 1)], "1") + c.add_transition("1", [("x", 1)], "1") + c.add_transition("1", [("x", 1), ("h", 1)], "1") + c.add_transition("1", [("x", 2)], "1") + c.add_transition("1", [("x", 2), ("h", 1)], "1") + c.add_transition("1", [("h", 1)], "1") - - rc = ReactionSystemWithAutomaton(r,c) + rc = ReactionSystemWithAutomaton(r, c) rc.show() - smt_rsc = SmtCheckerRSC(rc) - + smt_rsc = SmtCheckerRSCParam(rc) + # Universal property which seems to be true: (holds also existentially) - f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_Implies( - (BagDescription.f_entity('y') == 2), - Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1), - BagDescription.f_entity("y") >= 3 - ) + f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") >= 3 ) ) - + ) + # lets see if we can find a counterexample to this property: - neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_And( - (BagDescription.f_entity('y') == 2), - Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1), - BagDescription.f_entity("y") < 3 - ) + neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_And( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") < 3 ) ) - + ) + # we fix the property f1 # this one holds: - f2 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, - Formula_rsLTL.f_Implies( - (BagDescription.f_entity('y') == 2), + f2 = Formula_rsLTL.f_G( + BagDescription.f_entity("x") > 0, Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), Formula_rsLTL.f_X( - (BagDescription.f_entity("x") > 1) & (BagDescription.f_entity("h") < 1), - BagDescription.f_entity("y") >= 3 - ) - ) - ) - + (BagDescription.f_entity("x") > 1) & + (BagDescription.f_entity("h") < 1), + BagDescription.f_entity("y") >= 3))) + # neg_f1 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, # Formula_rsLTL.f_And( # (BagDescription.f_entity('y') > 0), @@ -169,6 +120,83 @@ def example44(): # ) # )) smt_rsc.check_rsltl(formula=neg_f1) + + +def example44(): + + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("x", 2)) + r.add_bg_set_entity(("y", 4)) + r.add_bg_set_entity(("h", 2)) + r.add_bg_set_entity(("m", 1)) + + r.add_reaction([("y", 1), ("x", 1)], [("y", 2), ("h", 1)], [("y", 2)]) + r.add_reaction([("y", 2), ("x", 2)], [("y", 3), ("h", 1)], [("y", 3)]) + r.add_reaction([("y", 3), ("h", 1)], [("y", 4), ("h", 2)], [("y", 4)]) + r.add_reaction([("y", 4), ("h", 1)], [("h", 2)], [("y", 3)]) + r.add_reaction([("y", 4), ("x", 2)], [("h", 1)], [("y", 2)]) + r.add_reaction([("m", 1)], [("y", 3)], [("m", 1)]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("0") + c.add_state("1") + c.add_transition("0", [("y", 1), ("m", 1), ("x", 1)], "1") + c.add_transition("1", [("x", 1)], "1") + c.add_transition("1", [("x", 1), ("h", 1)], "1") + c.add_transition("1", [("x", 2)], "1") + c.add_transition("1", [("x", 2), ("h", 1)], "1") + c.add_transition("1", [("h", 1)], "1") + + rc = ReactionSystemWithAutomaton(r, c) + rc.show() + smt_rsc = SmtCheckerRSC(rc) + + # Universal property which seems to be true: (holds also existentially) + f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") >= 3 + ) + ) + ) + + # lets see if we can find a counterexample to this property: + neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, + Formula_rsLTL.f_And( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1), + BagDescription.f_entity("y") < 3 + ) + ) + ) + + # we fix the property f1 + # this one holds: + f2 = Formula_rsLTL.f_G( + BagDescription.f_entity("x") > 0, Formula_rsLTL.f_Implies( + (BagDescription.f_entity('y') == 2), + Formula_rsLTL.f_X( + (BagDescription.f_entity("x") > 1) & + (BagDescription.f_entity("h") < 1), + BagDescription.f_entity("y") >= 3))) + + # neg_f1 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0, + # Formula_rsLTL.f_And( + # (BagDescription.f_entity('y') > 0), + # Formula_rsLTL.f_X( + # BagDescription.f_entity("x") > 0, + # Formula_rsLTL.f_X( + # BagDescription.f_entity("x") > 1, + # BagDescription.f_entity("y") < 3 + # ) + # ) + # ) + # )) + smt_rsc.check_rsltl(formula=neg_f1) + def heat_shock_response(print_system=True):