From 47e03694e4ede12ef723fa7a4b5caf659447a534 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 6 Nov 2023 21:07:01 +0000 Subject: [PATCH] Scripts to reproduce experiments for reaction mining --- examples/bdd/generators/gen_drs.py | 2 +- examples/smt/chain_reaction.py | 4 +- examples/smt/heat_shock_response.py | 117 ++--- examples/smt/mutex_param.py | 17 +- examples/smt/scalable_chain.py | 150 +++--- experiments/drs_cell_signal/run.sh | 24 +- .../bench_mutex_nonparam_mem.dat | 20 + .../bench_mutex_nonparam_oldimpl_mem.dat | 20 + .../bench_mutex_nonparam_oldimpl_time.dat | 20 + .../bench_mutex_nonparam_time.dat | 20 + .../bench_mutex_param_mem.dat | 20 + .../bench_mutex_param_time.dat | 20 + experiments/reaction_mining_mutex/pmutex.py | 454 ++++++++++++++++++ .../reaction_mining_mutex/run_mutex_param.sh | 26 + reactics | 2 +- rs_testing.py => reactics-smt/rs_testing.py | 0 16 files changed, 774 insertions(+), 142 deletions(-) mode change 100644 => 100755 examples/smt/chain_reaction.py mode change 100644 => 100755 examples/smt/heat_shock_response.py mode change 100644 => 100755 examples/smt/mutex_param.py mode change 100644 => 100755 examples/smt/scalable_chain.py create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_param_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_param_time.dat create mode 100755 experiments/reaction_mining_mutex/pmutex.py create mode 100755 experiments/reaction_mining_mutex/run_mutex_param.sh rename rs_testing.py => reactics-smt/rs_testing.py (100%) diff --git a/examples/bdd/generators/gen_drs.py b/examples/bdd/generators/gen_drs.py index 99f8a03..c076f7a 100755 --- a/examples/bdd/generators/gen_drs.py +++ b/examples/bdd/generators/gen_drs.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python3 import sys import itertools diff --git a/examples/smt/chain_reaction.py b/examples/smt/chain_reaction.py old mode 100644 new mode 100755 index 9c5205b..b44a67e --- a/examples/smt/chain_reaction.py +++ b/examples/smt/chain_reaction.py @@ -28,7 +28,6 @@ import resource def chain_reaction(print_system=False): - if len(sys.argv) < 1 + 3: print("{source} ".format(source=sys.argv[0])) print() @@ -39,7 +38,7 @@ def chain_reaction(print_system=False): print() exit(1) - chainLen = int(sys.argv[1]) + chainLen = int(sys.argv[1]) maxConc = int(sys.argv[2]) # depth (max concentration) verify_rsc = bool(int(sys.argv[3])) @@ -115,7 +114,6 @@ def chain_reaction(print_system=False): def main(): - chain_reaction() diff --git a/examples/smt/heat_shock_response.py b/examples/smt/heat_shock_response.py old mode 100644 new mode 100755 index 3707236..eb627cd --- a/examples/smt/heat_shock_response.py +++ b/examples/smt/heat_shock_response.py @@ -28,8 +28,7 @@ import resource def heat_shock_response(print_system=True, verify_rsc=True): - - if len(sys.argv) < 1+1: + if len(sys.argv) < 1 + 1: print("{source} ".format(source=sys.argv[0])) print("type:") print(" - 1 -- RSC") @@ -37,72 +36,80 @@ def heat_shock_response(print_system=True, verify_rsc=True): print() exit(1) - verify_rsc=bool(int(sys.argv[1])) + verify_rsc = bool(int(sys.argv[1])) 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 = 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_permanency("temp",[("heat",1),("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("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) - + rc = ReactionSystemWithAutomaton(r, c) + if print_system: rc.show() - - prop_req = [ ("mfp",1) ] - prop_block = [ ] - prop = (prop_req,prop_block) - rs_prop = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block)) - + + prop_req = [("mfp", 1)] + prop_block = [] + prop = (prop_req, prop_block) + rs_prop = (state_translate_rsc2rs(prop_req), state_translate_rsc2rs(prop_block)) + if verify_rsc: smt_rsc = SmtCheckerRSC(rc) - smt_rsc.check_reachability(prop,max_level=40) + smt_rsc.check_reachability(prop, max_level=40) else: orc = rc.get_ordinary_reaction_system_with_automaton() if print_system: @@ -117,10 +124,10 @@ def state_translate_rsc2rs(p): def main(): - heat_shock_response() + if __name__ == "__main__": main() - + # EOF diff --git a/examples/smt/mutex_param.py b/examples/smt/mutex_param.py old mode 100644 new mode 100755 index 5a5ff15..ae51160 --- a/examples/smt/mutex_param.py +++ b/examples/smt/mutex_param.py @@ -42,7 +42,7 @@ def powerset(iterable, N=None): def mutex_param_bench(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -77,7 +77,6 @@ def mutex_param_bench(cmd_args): 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)]) @@ -189,7 +188,7 @@ def mutex_param_bench(cmd_args): def mutex_nonparam_bench(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -217,7 +216,6 @@ def mutex_nonparam_bench(cmd_args): 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)]) @@ -297,7 +295,7 @@ def mutex_nonparam_bench(cmd_args): def mutex_nonparam_bench_oldimpl(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -325,7 +323,6 @@ def mutex_nonparam_bench_oldimpl(cmd_args): 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)]) @@ -407,7 +404,6 @@ def state_translate_rsc2rs(p): def mutex_bench_main(cmd_args): - mode = cmd_args.mode if mode == "p": @@ -422,17 +418,16 @@ def mutex_bench_main(cmd_args): def main(): - parser = argparse.ArgumentParser() parser.add_argument( "scaling", help="scaling parameter value", ) - + parser.add_argument( "mode", - choices=['p', 'np-p', 'np-np'], + choices=["p", "np-p", "np-np"], help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)", ) @@ -447,7 +442,7 @@ def main(): ) args = parser.parse_args() - + mutex_bench_main(args) diff --git a/examples/smt/scalable_chain.py b/examples/smt/scalable_chain.py old mode 100644 new mode 100755 index d129704..71d11e2 --- a/examples/smt/scalable_chain.py +++ b/examples/smt/scalable_chain.py @@ -31,76 +31,102 @@ from itertools import chain, combinations import sys import resource + def generate_system(chainLen, maxConc): """ This function generates the reaction system with concentrations for the scalable chain benchmark - + chainLen is the length of the chain maxConc is the maximal concentration """ - - 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)]) - + 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) + c.add_transition("init", [("e_1", 1), ("inc", 1)], "working") + c.add_transition("working", [("inc", 1)], "working") + + rc = ReactionSystemWithAutomaton(r, c) return rc + def generate_formula(formula_number, chainLen, maxConc): """ - This function generates the rsLTL formula + This function generates the rsLTL formula corresponding to the formula_number parameter """ if formula_number == 1: - ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) ) + ret = Formula_rsLTL.f_F( + BagDescription.f_entity("inc") > 0, + (BagDescription.f_entity("e_" + str(chainLen)) >= maxConc), + ) 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_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), + ) ret = f_tmp - + elif formula_number == 3: - ret = Formula_rsLTL.f_G( BagDescription.f_TRUE(), + ret = Formula_rsLTL.f_G( + BagDescription.f_TRUE(), Formula_rsLTL.f_Implies( - (BagDescription.f_entity('e_1') == 1), + (BagDescription.f_entity("e_1") == 1), Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, - (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) - ) - ) + (BagDescription.f_entity("e_" + str(chainLen)) == maxConc), + ), + ), ) elif formula_number == 4: - ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc ) - + ret = Formula_rsLTL.f_F( + BagDescription.f_entity("inc") > 0, + BagDescription.f_entity("e_1") == maxConc, + ) + elif formula_number == 5: - ret = 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 ) ) + ret = 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, + ), + ) else: ret = None - + assert ret is not None, "Unknown formula" return ret @@ -110,64 +136,64 @@ def save_statistics(smt_rsc, formula_number, chainLen, maxConc): """ Saves the statistics fetched from smt_rsc into files """ - 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() + 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 = 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 = open(filename_m, "a") + log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" f.write(log_str) f.close() - + def scalable_chain(print_system=False): """ This is the entry point for the benchmark """ - if len(sys.argv) < 1+3: + 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]) - + 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): + if not formula_number in range(1, 5 + 1): print("formulaNumber must be in 1..5") exit(1) - + # Generate the reaction systems with concentrations rc = generate_system(chainLen, maxConc) - + # Generate the formula form = generate_formula(formula_number, chainLen, maxConc) - + # Optional dump/print of the system if print_system: rc.show() - + # Create an instance of the SMT checker for RS with concentrations smt_rsc = SmtCheckerRSC(rc) - + # Start the verification process smt_rsc.check_rsltl(formula=form) - + save_statistics(smt_rsc, formula_number, chainLen, maxConc) - - + + def main(): scalable_chain(print_system=True) + if __name__ == "__main__": main() - diff --git a/experiments/drs_cell_signal/run.sh b/experiments/drs_cell_signal/run.sh index 786dc58..e514361 100755 --- a/experiments/drs_cell_signal/run.sh +++ b/experiments/drs_cell_signal/run.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash -x_values="`seq 2 20`" +x_values="2 3 4" y_values="`seq 2 20`" z_values="`seq 2 20`" aut_values="a b" reactics="$1" -reactics_opts="-z -v -B -c" +reactics_opts="-z -x -vv -B -c" input_generator="../../examples/bdd/generators/gen_drs.py" @@ -34,16 +34,16 @@ fi #ulimit -t 3600 #ulimit -v 2097152 -ulimit -t 360 -ulimit -v 1000000 +ulimit -t 3600 +#ulimit -v 1000000 for a in $aut_values do - for x in $x_values + for z in $z_values do for y in $y_values do - for z in $z_values + for x in $x_values do if [[ $y -lt $z ]] @@ -52,13 +52,19 @@ do continue fi + if [[ $y -ne $z ]] + then + # More aggressive skipping + continue + fi + bench_identifier="${benchname}_F${formname}_A${a}" filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}" outfile="${filename_base}.out" infile="${filename_base}.drs" - stopfile="DONE_${bench_identifier}" + stopfile="DONE_${bench_identifier}" if [[ -e "$stopfile" ]] then @@ -68,7 +74,7 @@ do $input_generator $x $y $z $a > ${infile} - $reactics $reactics_opts $formname $infile > ${outfile} 2>&1 + $reactics $reactics_opts $formname $infile |& tee ${outfile} exitcode=$? echo "ReactICS exit code: $exitcode" @@ -76,7 +82,7 @@ do if [ "$result" = "" ] then echo "TIME LIMIT; marking as finished" - touch $stopfile + #touch $stopfile else echo "$x ; $y ; $z ; $a ; $exitcode $result" >> $outdir/summary_${bench_identifier}.txt echo "$x $y $z $a $(echo $result | sed 's/;/ /g')" >> $outdir/${bench_identifier}.dat diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat new file mode 100644 index 0000000..75c8ef6 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat @@ -0,0 +1,20 @@ +2 69.171875 +3 69.937500 +4 86.109375 +5 76.093750 +6 81.812500 +7 97.078125 +8 88.562500 +9 102.968750 +10 93.546875 +11 98.515625 +12 113.671875 +13 115.656250 +14 132.140625 +15 141.546875 +16 149.890625 +17 155.125000 +18 153.500000 +19 166.953125 +20 169.750000 +21 212.468750 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat new file mode 100644 index 0000000..ed1a7a8 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat @@ -0,0 +1,20 @@ +2 68.765625 +3 73.140625 +4 71.625000 +5 73.359375 +6 79.234375 +7 75.578125 +8 79.812500 +9 85.828125 +10 81.718750 +11 79.828125 +12 83.984375 +13 80.406250 +14 75.859375 +15 85.812500 +16 89.093750 +17 84.296875 +18 89.078125 +19 87.609375 +20 88.281250 +21 85.406250 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat new file mode 100644 index 0000000..a8311e3 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat @@ -0,0 +1,20 @@ +2 0.068995 +3 0.110615 +4 0.164639 +5 0.234950 +6 0.322793 +7 0.438878 +8 0.578109 +9 0.752163 +10 0.955217 +11 1.190432 +12 1.519409 +13 1.808177 +14 2.200211 +15 2.654874 +16 3.265984 +17 3.824895 +18 4.413004 +19 5.303216 +20 6.310782 +21 7.038971 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat new file mode 100644 index 0000000..4ac4eed --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat @@ -0,0 +1,20 @@ +2 0.095321 +3 0.171177 +4 0.272130 +5 0.417800 +6 0.584877 +7 0.766862 +8 1.009195 +9 1.295766 +10 1.741482 +11 2.354580 +12 2.949242 +13 3.127326 +14 4.074318 +15 4.978959 +16 6.690042 +17 8.114637 +18 12.006410 +19 11.929118 +20 14.044730 +21 15.673520 diff --git a/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat new file mode 100644 index 0000000..3f84c8e --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat @@ -0,0 +1,20 @@ +2 80.093750 +3 76.062500 +4 88.312500 +5 97.140625 +6 95.234375 +7 109.843750 +8 111.218750 +9 132.921875 +10 142.546875 +11 151.546875 +12 175.546875 +13 186.109375 +14 206.546875 +15 235.281250 +16 245.515625 +17 249.562500 +18 260.203125 +19 278.796875 +20 292.781250 +21 300.562500 diff --git a/experiments/reaction_mining_mutex/bench_mutex_param_time.dat b/experiments/reaction_mining_mutex/bench_mutex_param_time.dat new file mode 100644 index 0000000..eb244af --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_param_time.dat @@ -0,0 +1,20 @@ +2 0.487115 +3 0.880007 +4 1.301547 +5 2.172839 +6 2.662308 +7 3.880329 +8 4.491871 +9 6.922392 +10 8.729740 +11 10.901971 +12 13.885037 +13 18.246820 +14 21.987255 +15 28.236579 +16 41.065607 +17 44.456013 +18 50.782835 +19 59.535617 +20 83.400427 +21 96.250559 diff --git a/experiments/reaction_mining_mutex/pmutex.py b/experiments/reaction_mining_mutex/pmutex.py new file mode 100755 index 0000000..3564725 --- /dev/null +++ b/experiments/reaction_mining_mutex/pmutex.py @@ -0,0 +1,454 @@ +#!/usr/bin/env python + +# +# Copyright (c) 2015-2019 Artur Meski +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# + +from rs import * +from smt import * +from logics import * +from rsltl_shortcuts import * + +from itertools import chain, combinations + +import sys +import resource +import argparse + + +def powerset(iterable, N=None): + if N is None: + N = len(s) + s = list(iterable) + return chain.from_iterable(combinations(s, r) for r in range(N + 1)) + + +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: + print("Missing scaling parameter") + return + n_proc = int(cmd_args.scaling) + + 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: + raise RuntimeError("Missing scaling parameter") + n_proc = int(cmd_args.scaling) + + 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: + raise RuntimeError("Missing scaling parameter") + n_proc = int(cmd_args.scaling) + + 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 state_translate_rsc2rs(p): + return [e[0] + "#" + str(e[1]) for e in p] + + +def mutex_bench_main(cmd_args): + mode = cmd_args.mode + + if mode == "p": + mutex_param_bench(cmd_args) + elif mode == "np-p": + mutex_nonparam_bench(cmd_args) + elif mode == "np-np": + mutex_nonparam_bench_oldimpl(cmd_args) + else: + print("Unrecognised mode") + return + + +def main(): + parser = argparse.ArgumentParser() + + parser.add_argument( + "scaling", + help="scaling parameter value", + ) + + parser.add_argument( + "mode", + choices=["p", "np-p", "np-np"], + help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)", + ) + + parser.add_argument( + "-v", "--verbose", help="turn verbosity on", action="store_true" + ) + parser.add_argument( + "-o", + "--optimise", + help="minimise the parametric computation result", + action="store_true", + ) + + args = parser.parse_args() + + mutex_bench_main(args) + + +if __name__ == "__main__": + main() + +# EOF diff --git a/experiments/reaction_mining_mutex/run_mutex_param.sh b/experiments/reaction_mining_mutex/run_mutex_param.sh new file mode 100755 index 0000000..ccb2082 --- /dev/null +++ b/experiments/reaction_mining_mutex/run_mutex_param.sh @@ -0,0 +1,26 @@ +#!/bin/sh + +# sudo systemsetup -getcomputersleep +#sudo systemsetup -setcomputersleep Never +# sudo systemsetup -setcomputersleep 1 + +REACTICS_SMT="../../reactics-smt" +export PYTHONPATH="$PYTHONPATH:$REACTICS_SMT" + +REACTICS_SCRIPT="./pmutex.py" + +for i in `seq 2 50` +do + for special_mode in "p" "np-p" "np-np" + do + echo "$i (sm=${special_mode})" + if [[ $special_mode -eq 1 ]] + then + $REACTICS_SCRIPT $i $special_mode + $REACTICS_SCRIPT -o $i $special_mode + else + $REACTICS_SCRIPT $i $special_mode + fi + done +done + diff --git a/reactics b/reactics index 4cc8de4..b4da96b 100755 --- a/reactics +++ b/reactics @@ -52,7 +52,7 @@ then then python3 $* else - echo "Nothing to do" + echo "Provide path to an example script (typically from ./examples/smt)" fi elif [[ "$mode" == "setup" ]] diff --git a/rs_testing.py b/reactics-smt/rs_testing.py similarity index 100% rename from rs_testing.py rename to reactics-smt/rs_testing.py