From 52d39d3ebeada179a842a6fb9d71edbc86f1d14c Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sat, 13 Jan 2018 20:29:49 +0000 Subject: [PATCH] Experiments: options, script --- rs_testing.py | 130 +++++++++++++++++++++++++++++++++++-- rssmt.py | 2 + scripts/run_mutex_param.sh | 15 ++++- 3 files changed, 140 insertions(+), 7 deletions(-) diff --git a/rs_testing.py b/rs_testing.py index 2760c8f..8d480f9 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -28,7 +28,25 @@ def run_tests(cmd_args): # gene_expression(cmd_args) - mutex_param_bench(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)") + return + + smode = int(cmd_args.special_mode) + + if smode == 1: + mutex_param_bench(cmd_args) + elif smode == 2: + mutex_nonparam_bench(cmd_args) + else: + print("Unrecognised mode") + return def mutex_param_bench(cmd_args): """ @@ -41,7 +59,8 @@ def mutex_param_bench(cmd_args): shared_entities = ["lock","done","s"] if not cmd_args.scaling_parameter: - raise RuntimeError("Missing scaling parameter") + print("Missing scaling parameter") + return n_proc = int(cmd_args.scaling_parameter) r = ReactionSystemWithConcentrationsParam() @@ -136,10 +155,113 @@ def mutex_param_bench(cmd_args): 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_time.log" - filename_m="bench_mutex_param_mem.log" + 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: diff --git a/rssmt.py b/rssmt.py index 6012cc5..690634e 100755 --- a/rssmt.py +++ b/rssmt.py @@ -54,6 +54,8 @@ def main(): help="minimise the parametric computation result", action="store_true") parser.add_argument("-n", "--scaling-parameter", help="scaling parameter value (used in some benchmarks)") + parser.add_argument("-s", "--special_mode", + help="special mode (used in some benchmarks)") args = parser.parse_args() diff --git a/scripts/run_mutex_param.sh b/scripts/run_mutex_param.sh index 93168a4..c15dbb7 100755 --- a/scripts/run_mutex_param.sh +++ b/scripts/run_mutex_param.sh @@ -4,9 +4,18 @@ #sudo systemsetup -setcomputersleep Never # sudo systemsetup -setcomputersleep 1 -for i in `seq 2 20` +for i in `seq 2 100` do - echo $i - ./rssmt.py -o -n $i + for special_mode in 1 2 + do + echo "$i (sm=${special_mode})" + if [[ $special_mode -eq 1 ]] + then + ./rssmt.py -n $i -s $special_mode + ./rssmt.py -o -n $i -s $special_mode + else + ./rssmt.py -n $i -s $special_mode + fi + done done