diff --git a/rs/reaction_system_with_concentrations.py b/rs/reaction_system_with_concentrations.py index 4167aa2..daf9fde 100644 --- a/rs/reaction_system_with_concentrations.py +++ b/rs/reaction_system_with_concentrations.py @@ -56,8 +56,7 @@ class ReactionSystemWithConcentrations(ReactionSystem): if len(e) == 2 and type(e[1]) is int: return True - print("FATAL. Invalid entity+concentration:") - print(e) + print("FATAL. Invalid entity+concentration: {:s}".format(e)) exit(1) return False diff --git a/rs_testing.py b/rs_testing.py index 5733617..05586bc 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -2,6 +2,8 @@ from rs import * from smt import * import rs_examples from logics import * +from rsltl_shortcuts import * + import sys import resource @@ -13,9 +15,58 @@ def run_tests(cmd_args): # scalable_chain(print_system=True) # example44() # example44_param() - heat_shock_response_param(cmd_args) + # heat_shock_response_param(cmd_args) # simple_param(cmd_args) + gene_expression(cmd_args) + +def gene_expression(cmd_args): + """ + Simple gene expression example + """ + r = ReactionSystemWithConcentrationsParam() + + r.add_bg_set_entity(("x", 1)) + r.add_bg_set_entity(("xp", 1)) + r.add_bg_set_entity(("X", 1)) + + r.add_bg_set_entity(("y", 1)) + r.add_bg_set_entity(("yp", 1)) + r.add_bg_set_entity(("Y", 1)) + + r.add_bg_set_entity(("z", 1)) + r.add_bg_set_entity(("zp", 1)) + r.add_bg_set_entity(("Z", 1)) + + r.add_bg_set_entity(("h", 1)) + r.add_bg_set_entity(("Q", 1)) + r.add_bg_set_entity(("U", 1)) + + r.add_reaction([("x",1)],[("h",1)],[("x",1)]) + r.add_reaction([("x",1)],[("h",1)],[("xp",1)]) + r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)]) + r.add_reaction([("y",1)],[("h",1)],[("y",1)]) + r.add_reaction([("y",1)],[("Q",1)],[("yp",1)]) + r.add_reaction([("y",1),("yp",1)],[("h",1)],[("Y",1)]) + r.add_reaction([("z",1)],[("h",1)],[("z",1)]) + r.add_reaction([("z",1)], [("X",1)], [("zp",1)]) + r.add_reaction([("z",1),("zp",1)],[("h",1)],[("Z",1)]) + r.add_reaction([("U",1),("X",1)],[("h",1)],[("Q",1)]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("0") + c.add_state("1") + + # the experiments starts with adding x and y: + c.add_transition("0", [("x", 1),("y", 1)], "1") + + # for all the remaining steps we have empty context sequences + c.add_transition("1", [], "1") + + rc = ReactionSystemWithAutomaton(r, c) + rc.show() + + def trivial_param(): r = ReactionSystemWithConcentrationsParam() @@ -38,9 +89,11 @@ def trivial_param(): rc.show() smt_rsc = SmtCheckerRSCParam(rc) - f1 = Formula_rsLTL.f_F( - BagDescription.f_TRUE(), - BagDescription.f_entity("final") >= 1) + f1 = ltl_F(bag_entity("final") >= 1) + + # f1 = Formula_rsLTL.f_F( + # BagDescription.f_TRUE(), + # BagDescription.f_entity("final") >= 1) # # WARNING: depth limit is set @@ -152,7 +205,9 @@ def heat_shock_response_param(cmd_args, print_system=True): # 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) ) + + # f_reach_mfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("mfp") > 0) ) + f_reach_mfp = ltl_F(bag_entity("mfp") > 0) f_reach_hspmfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("hsp:mfp") > 0) ) diff --git a/rsltl_shortcuts.py b/rsltl_shortcuts.py new file mode 100644 index 0000000..815dce4 --- /dev/null +++ b/rsltl_shortcuts.py @@ -0,0 +1,26 @@ +from logics import * + +##### SHORTCUTS + +def bag_True(): + return BagDescription.f_TRUE() + +def bag_entity(name): + return BagDescription.f_entity(name) + +def ltl_F(a0, ctx_arg=None): + if ctx_arg == None: + ctx_arg = bag_True() + return Formula_rsLTL.f_F(ctx_arg, a0) + +def ltl_G(a0, ctx_arg=None): + if ctx_arg == None: + ctx_arg = bag_True() + return Formula_rsLTL.f_G(ctx_arg, a0) + +def ltl_X(a0, ctx_arg=None): + if ctx_arg == None: + ctx_arg = bag_True() + return Formula_rsLTL.f_X(ctx_arg, a0) + +