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

benchmarks for SC

Browse Source
This commit is contained in:
Artur Meski
2017-03-16 20:57:42 +01:00
parent 59cd3af3e1
commit ab5550d3fd
4 changed files with 82 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
logics/rsltl_encoder.py
View File

@@ -117,8 +117,8 @@ class rsLTL_Encoder(object):
# level == bound # level == bound
enc = False enc = False
for loop_level in range(1, bound+1): for loop_level in range(1, bound+1):
enc = Or(enc, And(self.loop_position == loop_level, enc = simplify(Or(enc, And(self.loop_position == loop_level,
self.encode(formula.left_operand, loop_level, bound))) self.encode(formula.left_operand, loop_level, bound))))
enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level)) enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level))
enc = simplify(enc) enc = simplify(enc)
@@ -135,12 +135,12 @@ class rsLTL_Encoder(object):
# level == bound # level == bound
enc_loops = False enc_loops = False
for loop_level in range(1, bound+1): for loop_level in range(1, bound+1):
enc_loops = Or(enc_loops, enc_loops = simplify(Or(enc_loops,
And( And(
self.loop_position == loop_level, self.loop_position == loop_level,
self.encode_approx(formula, loop_level, bound), self.encode_approx(formula, loop_level, bound),
) )
) ))
enc = And( enc = And(
self.encode(formula.left_operand, bound, bound), self.encode(formula.left_operand, bound, bound),
enc_loops, enc_loops,
@@ -163,12 +163,12 @@ class rsLTL_Encoder(object):
# level == bound # level == bound
enc_loops = False enc_loops = False
for loop_level in range(1, bound+1): for loop_level in range(1, bound+1):
enc_loops = Or(enc_loops, enc_loops = simplify(Or(enc_loops,
And( And(
self.loop_position == loop_level, self.loop_position == loop_level,
self.encode_approx(formula, loop_level, bound), self.encode_approx(formula, loop_level, bound),
) )
) ))
#print(enc) #print(enc)
enc = Or(self.encode(formula.left_operand, bound, bound), enc = Or(self.encode(formula.left_operand, bound, bound),
And( And(
@@ -188,12 +188,12 @@ class rsLTL_Encoder(object):
# level == bound # level == bound
inner_enc = False inner_enc = False
for loop_level in range(1, bound+1): for loop_level in range(1, bound+1):
inner_enc = Or(inner_enc, inner_enc = simplify(Or(inner_enc,
And( And(
self.loop_position == loop_level, self.loop_position == loop_level,
self.encode_approx(formula, loop_level, bound) self.encode_approx(formula, loop_level, bound)
) )
) ))
enc = Or( enc = Or(
self.encode(formula.right_operand, level, bound), self.encode(formula.right_operand, level, bound),
@@ -213,12 +213,12 @@ class rsLTL_Encoder(object):
# level == bound # level == bound
inner_enc = False inner_enc = False
for loop_level in range(1, bound+1): for loop_level in range(1, bound+1):
inner_enc = Or(inner_enc, inner_enc = simplify(Or(inner_enc,
And( And(
self.loop_position == loop_level, self.loop_position == loop_level,
self.encode_approx(formula, loop_level, bound) self.encode_approx(formula, loop_level, bound)
) )
) ))
enc = And( enc = And(
self.encode(formula.right_operand, level, bound), self.encode(formula.right_operand, level, bound),

62
rs_testing.py
View File

@@ -101,16 +101,20 @@ def state_translate_rsc2rs(p):
def scalable_chain(print_system=False): def scalable_chain(print_system=False):
if len(sys.argv) < 1+2: if len(sys.argv) < 1+3:
print("provide <chainLen> <maxConc>") 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])
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,4+1):
print("formulaNumber must be in 1..4")
exit(1)
r = ReactionSystemWithConcentrations() r = ReactionSystemWithConcentrations()
r.add_bg_set_entity(("inc",1)) r.add_bg_set_entity(("inc",1))
@@ -141,40 +145,36 @@ def scalable_chain(print_system=False):
smt_rsc = SmtCheckerRSC(rc) smt_rsc = SmtCheckerRSC(rc)
prop = [('e_'+str(chainLen),maxConc)] if formula_number == 1:
# smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10) 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)
# smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10) elif formula_number == 2:
f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) )
# (1) for i in range(chainLen-1,0,-1):
f_1 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) ) f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) )
smt_rsc.check_rsltl(formula=f_1) f_2 = f_tmp
smt_rsc.check_rsltl(formula=f_2)
# (2) elif formula_number == 3:
# f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) ) f_3 = Formula_rsLTL.f_G( BagDescription.f_TRUE(),
# for i in range(chainLen-1,0,-1): Formula_rsLTL.f_Implies(
# f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) ) (BagDescription.f_entity('e_1') == 1),
# f_2 = f_tmp Formula_rsLTL.f_F(
# smt_rsc.check_rsltl(formula=f_2) BagDescription.f_entity("inc") > 0,
(BagDescription.f_entity('e_'+str(i)) == maxConc)
# (3) )
# f_3 = Formula_rsLTL.f_G( BagDescription.f_TRUE(), )
# Formula_rsLTL.f_Implies( )
# (BagDescription.f_entity('e_1') == 1), smt_rsc.check_rsltl(formula=f_3)
# Formula_rsLTL.f_F( elif formula_number == 4:
# BagDescription.f_entity("inc") > 0, f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
# (BagDescription.f_entity('e_'+str(i)) == maxConc) smt_rsc.check_rsltl(formula=f_4)
# )
# )
# )
# smt_rsc.check_rsltl(formula=f_3)
########################################################################### ###########################################################################
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_time.log" filename_t="bench_rsc_F" + str(formula_number) + "_time.log"
filename_m="bench_rsc_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')

34
scripts/run_scalable_chain_rsLTL_FI.sh Executable file
View File

@@ -0,0 +1,34 @@
#!/bin/sh
# sudo systemsetup -getcomputersleep
sudo systemsetup -setcomputersleep Never
# sudo systemsetup -setcomputersleep 1
formula=1
for i in `seq 2 50`
do
echo $i
./rssmt.py $i 2 $formula
done
formula=2
for i in `seq 2 50`
do
echo $i
./rssmt.py $i 2 $formula
done
formula=3
for i in `seq 2 50`
do
echo $i
./rssmt.py $i 2 $formula
done
formula=4
for i in `seq 2 50`
do
echo $i
./rssmt.py $i 2 $formula
done

8
smt/smt_checker_rsc.py
View File

@@ -411,7 +411,13 @@ class SmtCheckerRSC(object):
print("[" + colour_str(C_BOLD, "i") + "] Generating the formula encoding...") print("[" + colour_str(C_BOLD, "i") + "] Generating the formula encoding...")
encoder.init_ncalls() encoder.init_ncalls()
f = encoder.encode(formula, 0, self.current_level) f = encoder.encode(formula, 0, self.current_level)
print("[" + colour_str(C_BOLD, "i") + "] Encode calls: " + str(encoder.get_ncalls())) ncalls = encoder.get_ncalls()
print("[" + colour_str(C_BOLD, "i") + "] Encode calls: " + str(ncalls[0]) + " " + str(ncalls[1]), end="")
if ncalls[0] > 9999:
print(" I bet it is rather slow now... :(")
printed = True
else:
print()
print("[" + colour_str(C_BOLD, "i") + "] Adding the formula to the solver...") print("[" + colour_str(C_BOLD, "i") + "] Adding the formula to the solver...")
self.solver.add(f) self.solver.add(f)