artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Scripts to reproduce experiments for reaction mining

Browse Source
This commit is contained in:
Artur Meski
2023-11-06 21:07:01 +00:00
parent e9589cd0d9
commit 47e03694e4
16 changed files with 774 additions and 142 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
examples/bdd/generators/gen_drs.py
View File

@@ -1,4 +1,4 @@
#!/usr/bin/env python #!/usr/bin/env python3
import sys import sys
import itertools import itertools

4
examples/smt/chain_reaction.py Normal file → Executable file
View File

@@ -28,7 +28,6 @@ import resource
def chain_reaction(print_system=False): def chain_reaction(print_system=False):
if len(sys.argv) < 1 + 3: if len(sys.argv) < 1 + 3:
print("{source} <N> <M> <type>".format(source=sys.argv[0])) print("{source} <N> <M> <type>".format(source=sys.argv[0]))
print() print()
@@ -39,7 +38,7 @@ def chain_reaction(print_system=False):
print() print()
exit(1) exit(1)
chainLen = int(sys.argv[1]) chainLen = int(sys.argv[1])
maxConc = int(sys.argv[2]) # depth (max concentration) maxConc = int(sys.argv[2]) # depth (max concentration)
verify_rsc = bool(int(sys.argv[3])) verify_rsc = bool(int(sys.argv[3]))
@@ -115,7 +114,6 @@ def chain_reaction(print_system=False):
def main(): def main():
chain_reaction() chain_reaction()

117
examples/smt/heat_shock_response.py Normal file → Executable file
View File

@@ -28,8 +28,7 @@ import resource
def heat_shock_response(print_system=True, verify_rsc=True): def heat_shock_response(print_system=True, verify_rsc=True):
if len(sys.argv) < 1 + 1:
if len(sys.argv) < 1+1:
print("{source} <type>".format(source=sys.argv[0])) print("{source} <type>".format(source=sys.argv[0]))
print("type:") print("type:")
print(" - 1 -- RSC") print(" - 1 -- RSC")
@@ -37,72 +36,80 @@ def heat_shock_response(print_system=True, verify_rsc=True):
print() print()
exit(1) exit(1)
verify_rsc=bool(int(sys.argv[1])) verify_rsc = bool(int(sys.argv[1]))
stress_temp = 42 stress_temp = 42
max_temp = 50 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 = ReactionSystemWithConcentrations()
r.add_reaction_dec("temp", "cool", [("temp",1)],[]) 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 = ContextAutomatonWithConcentrations(r)
c.add_init_state("0") c.add_init_state("0")
c.add_state("1") c.add_state("1")
c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",35)], "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", [("cool", 1)], "1")
c.add_transition("1", [("heat",1)], "1") c.add_transition("1", [("heat", 1)], "1")
c.add_transition("1", [], "1") c.add_transition("1", [], "1")
rc = ReactionSystemWithAutomaton(r,c) rc = ReactionSystemWithAutomaton(r, c)
if print_system: if print_system:
rc.show() rc.show()
prop_req = [ ("mfp",1) ] prop_req = [("mfp", 1)]
prop_block = [ ] prop_block = []
prop = (prop_req,prop_block) prop = (prop_req, prop_block)
rs_prop = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block)) rs_prop = (state_translate_rsc2rs(prop_req), state_translate_rsc2rs(prop_block))
if verify_rsc: if verify_rsc:
smt_rsc = SmtCheckerRSC(rc) smt_rsc = SmtCheckerRSC(rc)
smt_rsc.check_reachability(prop,max_level=40) smt_rsc.check_reachability(prop, max_level=40)
else: else:
orc = rc.get_ordinary_reaction_system_with_automaton() orc = rc.get_ordinary_reaction_system_with_automaton()
if print_system: if print_system:
@@ -117,10 +124,10 @@ def state_translate_rsc2rs(p):
def main(): def main():
heat_shock_response() heat_shock_response()
if __name__ == "__main__": if __name__ == "__main__":
main() main()
# EOF # EOF

17
examples/smt/mutex_param.py Normal file → Executable file
View File

@@ -42,7 +42,7 @@ def powerset(iterable, N=None):
def mutex_param_bench(cmd_args): def mutex_param_bench(cmd_args):
""" """
Mutex Benchmark Mutex Benchmark
Parametric Parametric
""" """
@@ -77,7 +77,6 @@ def mutex_param_bench(cmd_args):
Inhib = [("s", 1)] Inhib = [("s", 1)]
for i in range(n_proc): 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)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", 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): def mutex_nonparam_bench(cmd_args):
""" """
Mutex Benchmark Mutex Benchmark
Parametric Parametric
""" """
@@ -217,7 +216,6 @@ def mutex_nonparam_bench(cmd_args):
Inhib = [("s", 1)] Inhib = [("s", 1)]
for i in range(n_proc): 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)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", 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): def mutex_nonparam_bench_oldimpl(cmd_args):
""" """
Mutex Benchmark Mutex Benchmark
Parametric Parametric
""" """
@@ -325,7 +323,6 @@ def mutex_nonparam_bench_oldimpl(cmd_args):
Inhib = [("s", 1)] Inhib = [("s", 1)]
for i in range(n_proc): 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)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", 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): def mutex_bench_main(cmd_args):
mode = cmd_args.mode mode = cmd_args.mode
if mode == "p": if mode == "p":
@@ -422,17 +418,16 @@ def mutex_bench_main(cmd_args):
def main(): def main():
parser = argparse.ArgumentParser() parser = argparse.ArgumentParser()
parser.add_argument( parser.add_argument(
"scaling", "scaling",
help="scaling parameter value", help="scaling parameter value",
) )
parser.add_argument( parser.add_argument(
"mode", "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)", 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() args = parser.parse_args()
mutex_bench_main(args) mutex_bench_main(args)

150
examples/smt/scalable_chain.py Normal file → Executable file
View File

@@ -31,76 +31,102 @@ from itertools import chain, combinations
import sys import sys
import resource import resource
def generate_system(chainLen, maxConc): def generate_system(chainLen, maxConc):
""" """
This function generates the reaction system with concentrations This function generates the reaction system with concentrations
for the scalable chain benchmark for the scalable chain benchmark
chainLen is the length of the chain chainLen is the length of the chain
maxConc is the maximal concentration 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 = ContextAutomatonWithConcentrations(r)
c.add_init_state("init") c.add_init_state("init")
c.add_state("working") c.add_state("working")
c.add_transition("init", [("e_1",1),("inc",1)], "working") c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
c.add_transition("working", [("inc",1)], "working") c.add_transition("working", [("inc", 1)], "working")
rc = ReactionSystemWithAutomaton(r,c) rc = ReactionSystemWithAutomaton(r, c)
return rc return rc
def generate_formula(formula_number, chainLen, maxConc): 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 corresponding to the formula_number parameter
""" """
if formula_number == 1: 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: elif formula_number == 2:
f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) ) f_tmp = Formula_rsLTL.f_F(
for i in range(chainLen-1,0,-1): BagDescription.f_entity("inc") > 0,
f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) ) (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 ret = f_tmp
elif formula_number == 3: elif formula_number == 3:
ret = Formula_rsLTL.f_G( BagDescription.f_TRUE(), ret = Formula_rsLTL.f_G(
BagDescription.f_TRUE(),
Formula_rsLTL.f_Implies( Formula_rsLTL.f_Implies(
(BagDescription.f_entity('e_1') == 1), (BagDescription.f_entity("e_1") == 1),
Formula_rsLTL.f_F( Formula_rsLTL.f_F(
BagDescription.f_entity("inc") > 0, BagDescription.f_entity("inc") > 0,
(BagDescription.f_entity('e_'+str(chainLen)) == maxConc) (BagDescription.f_entity("e_" + str(chainLen)) == maxConc),
) ),
) ),
) )
elif formula_number == 4: 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: 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: else:
ret = None ret = None
assert ret is not None, "Unknown formula" assert ret is not None, "Unknown formula"
return ret return ret
@@ -110,64 +136,64 @@ def save_statistics(smt_rsc, formula_number, chainLen, maxConc):
""" """
Saves the statistics fetched from smt_rsc into files Saves the statistics fetched from smt_rsc into files
""" """
time=0 time = 0
mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
filename_t="bench_rsc_F" + str(formula_number) + "_time.log" filename_t = "bench_rsc_F" + str(formula_number) + "_time.log"
filename_m="bench_rsc_F" + str(formula_number) + "_mem.log" filename_m = "bench_rsc_F" + str(formula_number) + "_mem.log"
time=smt_rsc.get_verification_time() time = smt_rsc.get_verification_time()
f=open(filename_t, 'a') f = open(filename_t, "a")
log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n" log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
f.write(log_str) f.write(log_str)
f.close() f.close()
f=open(filename_m, 'a') f = open(filename_m, "a")
log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
f.write(log_str) f.write(log_str)
f.close() f.close()
def scalable_chain(print_system=False): def scalable_chain(print_system=False):
""" """
This is the entry point for the benchmark This is the entry point for the benchmark
""" """
if len(sys.argv) < 1+3: if len(sys.argv) < 1 + 3:
print("arguments: <chainLen> <maxConc> <formulaNumber>") print("arguments: <chainLen> <maxConc> <formulaNumber>")
exit(1) exit(1)
chainLen=int(sys.argv[1]) # chain length chainLen = int(sys.argv[1]) # chain length
maxConc=int(sys.argv[2]) # depth (max concentration) maxConc = int(sys.argv[2]) # depth (max concentration)
formula_number=int(sys.argv[3]) formula_number = int(sys.argv[3])
if chainLen < 1 or maxConc < 1: if chainLen < 1 or maxConc < 1:
print("be reasonable") print("be reasonable")
exit(1) 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") print("formulaNumber must be in 1..5")
exit(1) exit(1)
# Generate the reaction systems with concentrations # Generate the reaction systems with concentrations
rc = generate_system(chainLen, maxConc) rc = generate_system(chainLen, maxConc)
# Generate the formula # Generate the formula
form = generate_formula(formula_number, chainLen, maxConc) form = generate_formula(formula_number, chainLen, maxConc)
# Optional dump/print of the system # Optional dump/print of the system
if print_system: if print_system:
rc.show() rc.show()
# Create an instance of the SMT checker for RS with concentrations # Create an instance of the SMT checker for RS with concentrations
smt_rsc = SmtCheckerRSC(rc) smt_rsc = SmtCheckerRSC(rc)
# Start the verification process # Start the verification process
smt_rsc.check_rsltl(formula=form) smt_rsc.check_rsltl(formula=form)
save_statistics(smt_rsc, formula_number, chainLen, maxConc) save_statistics(smt_rsc, formula_number, chainLen, maxConc)
def main(): def main():
scalable_chain(print_system=True) scalable_chain(print_system=True)
if __name__ == "__main__": if __name__ == "__main__":
main() main()

24
experiments/drs_cell_signal/run.sh
View File

@@ -1,12 +1,12 @@
#!/usr/bin/env bash #!/usr/bin/env bash
x_values="`seq 2 20`" x_values="2 3 4"
y_values="`seq 2 20`" y_values="`seq 2 20`"
z_values="`seq 2 20`" z_values="`seq 2 20`"
aut_values="a b" aut_values="a b"
reactics="$1" reactics="$1"
reactics_opts="-z -v -B -c" reactics_opts="-z -x -vv -B -c"
input_generator="../../examples/bdd/generators/gen_drs.py" input_generator="../../examples/bdd/generators/gen_drs.py"
@@ -34,16 +34,16 @@ fi
#ulimit -t 3600 #ulimit -t 3600
#ulimit -v 2097152 #ulimit -v 2097152
ulimit -t 360 ulimit -t 3600
ulimit -v 1000000 #ulimit -v 1000000
for a in $aut_values for a in $aut_values
do do
for x in $x_values for z in $z_values
do do
for y in $y_values for y in $y_values
do do
for z in $z_values for x in $x_values
do do
if [[ $y -lt $z ]] if [[ $y -lt $z ]]
@@ -52,13 +52,19 @@ do
continue continue
fi fi
if [[ $y -ne $z ]]
then
# More aggressive skipping
continue
fi
bench_identifier="${benchname}_F${formname}_A${a}" bench_identifier="${benchname}_F${formname}_A${a}"
filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}" filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}"
outfile="${filename_base}.out" outfile="${filename_base}.out"
infile="${filename_base}.drs" infile="${filename_base}.drs"
stopfile="DONE_${bench_identifier}" stopfile="DONE_${bench_identifier}"
if [[ -e "$stopfile" ]] if [[ -e "$stopfile" ]]
then then
@@ -68,7 +74,7 @@ do
$input_generator $x $y $z $a > ${infile} $input_generator $x $y $z $a > ${infile}
$reactics $reactics_opts $formname $infile > ${outfile} 2>&1 $reactics $reactics_opts $formname $infile |& tee ${outfile}
exitcode=$? exitcode=$?
echo "ReactICS exit code: $exitcode" echo "ReactICS exit code: $exitcode"
@@ -76,7 +82,7 @@ do
if [ "$result" = "" ] if [ "$result" = "" ]
then then
echo "TIME LIMIT; marking as finished" echo "TIME LIMIT; marking as finished"
touch $stopfile #touch $stopfile
else else
echo "$x ; $y ; $z ; $a ; $exitcode $result" >> $outdir/summary_${bench_identifier}.txt 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 echo "$x $y $z $a $(echo $result | sed 's/;/ /g')" >> $outdir/${bench_identifier}.dat

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat Normal file
View File

@@ -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

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat Normal file
View File

@@ -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

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat Normal file
View File

@@ -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

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat Normal file
View File

@@ -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

20
experiments/reaction_mining_mutex/bench_mutex_param_mem.dat Normal file
View File

@@ -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

20
experiments/reaction_mining_mutex/bench_mutex_param_time.dat Normal file
View File

@@ -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

454
experiments/reaction_mining_mutex/pmutex.py Executable file
View File

@@ -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

26
experiments/reaction_mining_mutex/run_mutex_param.sh Executable file
View File

@@ -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

2
reactics
View File

@@ -52,7 +52,7 @@ then
then then
python3 $* python3 $*
else else
echo "Nothing to do" echo "Provide path to an example script (typically from ./examples/smt)"
fi fi
elif [[ "$mode" == "setup" ]] elif [[ "$mode" == "setup" ]]

0
rs_testing.py → reactics-smt/rs_testing.py
View File