diff --git a/rs_testing.py b/rs_testing.py index 8ee47c3..727dcce 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -28,363 +28,6 @@ def run_tests(cmd_args): # param_gene_expression(cmd_args) - mutex_bench_main(cmd_args) - -def mutex_bench_main(cmd_args): - - if not cmd_args.special_mode: - print("Missing special mode parameter") - print("* 1 - parametric") - print("* 2 - non-parametric (with parametric implementation)") - print("* 3 - non-parametric (with non-parametric implementation)") - return - - smode = int(cmd_args.special_mode) - - if smode == 1: - mutex_param_bench(cmd_args) - elif smode == 2: - mutex_nonparam_bench(cmd_args) - elif smode == 3: - mutex_nonparam_bench_oldimpl(cmd_args) - else: - print("Unrecognised mode") - return - -def mutex_param_bench(cmd_args): - """ - Mutex Benchmark - - Parametric - """ - - base_entities = ["out","req","in","act"] - shared_entities = ["lock","done","s"] - - if not cmd_args.scaling_parameter: - print("Missing scaling parameter") - return - n_proc = int(cmd_args.scaling_parameter) - - r = ReactionSystemWithConcentrationsParam() - - def E(a,b,c=1): - return (a + "_" + str(b), c) - - for i in range(n_proc): - for ent in base_entities: - max_conc = 1 - if ent == "in": - max_conc = 3 - elif ent == "req": - max_conc = 2 - r.add_bg_set_entity(E(ent,i,max_conc)) - - for ent in shared_entities: - max_conc = 1 - r.add_bg_set_entity((ent, max_conc)) - - ################################################### - - Inhib = [("s",1)] - - for i in range(n_proc): - - r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)]) - r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)]) - - for j in range(n_proc): - if i != j: - r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)]) - - r.add_reaction([E("req",i)],[E("act",i)],[E("req",i,2)]) - - enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)] - r.add_reaction([E("req",i,2),E("act",i)],enter_inhib,[E("in",i,3), ("lock",1)]) - - r.add_reaction([E("in",i,3),E("act",i)],Inhib,[E("in",i,2)]) - r.add_reaction([E("in",i,2),E("act",i)],Inhib,[E("in",i,1)]) - - r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)]) - r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)]) - - r.add_reaction([("lock",1)],[("done",1)],[("lock",1)]) - - lda1 = r.get_param("lda1") - lda2 = r.get_param("lda2") - lda3 = r.get_param("lda3") - - r.add_reaction(lda1,lda2,lda3) - - ################################################### - - c = ContextAutomatonWithConcentrations(r) - c.add_init_state("0") - c.add_state("1") - - init_ctx = [] - for i in range(n_proc): - init_ctx.append(E("out", i)) - - # the experiments starts with adding x and y: - c.add_transition("0", init_ctx, "1") - - all_act = powerset([E("act",i) for i in range(n_proc)], 2) - - for actions in all_act: - actions = list(actions) - - c.add_transition("1", actions, "1") - - # for all the remaining steps we have empty context sequences - # c.add_transition("1", [], "1") - # c.add_transition("1", [("h", 1)], "1") - - ################################################### - - rc = ReactionSystemWithAutomaton(r, c) - rc.show() - - f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1)) - - ent_of_Nth_proc = [ent + "_" + str(n_proc-1) for ent in base_entities] + shared_entities - disallow = ["in_" + str(n_proc-1)] - for ent in r.background_set: - if ent not in ent_of_Nth_proc: - disallow.append(ent) - - # disallow.append("act_" + str(n_proc-1)) - - # disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"] - lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow] - lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow] - lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow] - lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow - - # for bent in base_entities: - # print(param_entity(lda3, bent + "_0")) - - param_constr = param_And(*lda_disallow) - - smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise) - smt_rsc.check_rsltl(formulae_list=[f_attack], param_constr=param_constr) #, max_level=4, cont_if_sat=True) - - log_suffix = "" - if cmd_args.optimise: - log_suffix = "_OPT" - - time=0 - mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_mutex_param" + log_suffix + "_time.dat" - filename_m="bench_mutex_param" + log_suffix + "_mem.dat" - time=smt_rsc.get_verification_time() - - with open(filename_t, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, time) - f.write(log_str) - - with open(filename_m, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, mem_usage) - f.write(log_str) - -def mutex_nonparam_bench(cmd_args): - """ - Mutex Benchmark - - Parametric - """ - - base_entities = ["out","req","in","act"] - shared_entities = ["lock","done","s"] - - if not cmd_args.scaling_parameter: - raise RuntimeError("Missing scaling parameter") - n_proc = int(cmd_args.scaling_parameter) - - r = ReactionSystemWithConcentrationsParam() - - def E(a,b): - return (a + "_" + str(b), 1) - - for i in range(n_proc): - for ent in base_entities: - r.add_bg_set_entity(E(ent,i)) - - for ent in shared_entities: - r.add_bg_set_entity((ent, 1)) - - ################################################### - - Inhib = [("s",1)] - - for i in range(n_proc): - - r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)]) - r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)]) - - for j in range(n_proc): - if i != j: - r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)]) - - r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)]) - - enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)] - r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)]) - - r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)]) - r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)]) - - r.add_reaction([("lock",1)],[("done",1)],[("lock",1)]) - - r.add_reaction([E("out",n_proc-1)],[("s",1)],[("done",1),E("req",n_proc-1)]) - - ################################################### - - c = ContextAutomatonWithConcentrations(r) - c.add_init_state("0") - c.add_state("1") - - init_ctx = [] - for i in range(n_proc): - init_ctx.append(E("out", i)) - - # the experiments starts with adding x and y: - c.add_transition("0", init_ctx, "1") - - all_act = powerset([E("act",i) for i in range(n_proc)], 2) - - for actions in all_act: - actions = list(actions) - - c.add_transition("1", actions, "1") - - # for all the remaining steps we have empty context sequences - # c.add_transition("1", [], "1") - # c.add_transition("1", [("h", 1)], "1") - - ################################################### - - rc = ReactionSystemWithAutomaton(r, c) - rc.show() - - f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1)) - - smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise) - smt_rsc.check_rsltl(formulae_list=[f_attack]) - - time=0 - mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_mutex_nonparam_time.dat" - filename_m="bench_mutex_nonparam_mem.dat" - time=smt_rsc.get_verification_time() - - with open(filename_t, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, time) - f.write(log_str) - - with open(filename_m, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, mem_usage) - f.write(log_str) - -def mutex_nonparam_bench_oldimpl(cmd_args): - """ - Mutex Benchmark - - Parametric - """ - - base_entities = ["out","req","in","act"] - shared_entities = ["lock","done","s"] - - if not cmd_args.scaling_parameter: - raise RuntimeError("Missing scaling parameter") - n_proc = int(cmd_args.scaling_parameter) - - r = ReactionSystemWithConcentrations() - - def E(a,b): - return (a + "_" + str(b), 1) - - for i in range(n_proc): - for ent in base_entities: - r.add_bg_set_entity(E(ent,i)) - - for ent in shared_entities: - r.add_bg_set_entity((ent, 1)) - - ################################################### - - Inhib = [("s",1)] - - for i in range(n_proc): - - r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)]) - r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)]) - - for j in range(n_proc): - if i != j: - r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)]) - - r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)]) - - enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)] - r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)]) - - r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)]) - r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)]) - - r.add_reaction([("lock",1)],[("done",1)],[("lock",1)]) - - r.add_reaction([E("out",n_proc-1)],[("s",1)],[("done",1),E("req",n_proc-1)]) - - ################################################### - - c = ContextAutomatonWithConcentrations(r) - c.add_init_state("0") - c.add_state("1") - - init_ctx = [] - for i in range(n_proc): - init_ctx.append(E("out", i)) - - # the experiments starts with adding x and y: - c.add_transition("0", init_ctx, "1") - - all_act = powerset([E("act",i) for i in range(n_proc)], 2) - - for actions in all_act: - actions = list(actions) - - c.add_transition("1", actions, "1") - - # for all the remaining steps we have empty context sequences - # c.add_transition("1", [], "1") - # c.add_transition("1", [("h", 1)], "1") - - ################################################### - - rc = ReactionSystemWithAutomaton(r, c) - rc.show() - - f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1)) - - smt_rsc = SmtCheckerRSC(rc) - smt_rsc.check_rsltl(formula=f_attack) - - time=0 - mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_mutex_nonparam_oldimpl_time.dat" - filename_m="bench_mutex_nonparam_oldimpl_mem.dat" - time=smt_rsc.get_verification_time() - - with open(filename_t, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, time) - f.write(log_str) - - with open(filename_m, 'a') as f: - log_str="{:d} {:f}\n".format(n_proc, mem_usage) - f.write(log_str) - def param_gene_expression(cmd_args): """ Simple gene expression example with parameters @@ -1002,97 +645,3 @@ def heat_shock_response(print_system=True): def state_translate_rsc2rs(p): return [e[0] + "#" + str(e[1]) for e in p] - -def scalable_chain(print_system=False): - - if len(sys.argv) < 1+3: - print("arguments: ") - exit(1) - - chainLen=int(sys.argv[1]) # chain length - maxConc=int(sys.argv[2]) # depth (max concentration) - formula_number=int(sys.argv[3]) - - if chainLen < 1 or maxConc < 1: - print("be reasonable") - exit(1) - if not formula_number in range(1,5+1): - print("formulaNumber must be in 1..5") - exit(1) - - r = ReactionSystemWithConcentrations() - r.add_bg_set_entity(("inc",1)) - r.add_bg_set_entity(("dec",1)) - - for i in range(1,chainLen+1): - r.add_bg_set_entity(("e_" + str(i),maxConc)) - - for i in range(1,chainLen+1): - ent = "e_" + str(i) - r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)]) - r.add_reaction_dec(ent, "dec", [(ent, 1)],[]) - if i < chainLen: - r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)]) - - r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)]) - - c = ContextAutomatonWithConcentrations(r) - c.add_init_state("init") - c.add_state("working") - c.add_transition("init", [("e_1",1),("inc",1)], "working") - c.add_transition("working", [("inc",1)], "working") - - rc = ReactionSystemWithAutomaton(r,c) - - if print_system: - rc.show() - - smt_rsc = SmtCheckerRSC(rc) - - if formula_number == 1: - f_1 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) ) - smt_rsc.check_rsltl(formula=f_1) - elif formula_number == 2: - f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) ) - for i in range(chainLen-1,0,-1): - f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) ) - f_2 = f_tmp - smt_rsc.check_rsltl(formula=f_2) - elif formula_number == 3: - f_3 = Formula_rsLTL.f_G( BagDescription.f_TRUE(), - Formula_rsLTL.f_Implies( - (BagDescription.f_entity('e_1') == 1), - Formula_rsLTL.f_F( - BagDescription.f_entity("inc") > 0, - (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) - ) - ) - ) - print(i) - smt_rsc.check_rsltl(formula=f_3) - elif formula_number == 4: - f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc ) - smt_rsc.check_rsltl(formula=f_4) - - elif formula_number == 5: - f_5 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_U( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') > 0, BagDescription.f_entity('e_2') > 0 ) ) - smt_rsc.check_rsltl(formula=f_5) - - ########################################################################### - - time=0 - mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_rsc_F" + str(formula_number) + "_time.log" - filename_m="bench_rsc_F" + str(formula_number) + "_mem.log" - time=smt_rsc.get_verification_time() - - f=open(filename_t, 'a') - log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n" - f.write(log_str) - f.close() - - f=open(filename_m, 'a') - log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" - f.write(log_str) - f.close() -