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

Clean-up

Browse Source
This commit is contained in:
Artur Meski
2019-09-29 16:23:48 +01:00
parent f621808e9b
commit de8ed11498
1 changed files with 0 additions and 451 deletions
Download Patch File Download Diff File Expand all files Collapse all files

451
rs_testing.py
View File

@@ -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: <chainLen> <maxConc> <formulaNumber>")
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()