From ab5550d3fd96a6957f416ad5a6329a0e13bd8bb9 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Thu, 16 Mar 2017 20:57:42 +0100 Subject: [PATCH] benchmarks for SC --- logics/rsltl_encoder.py | 20 ++++----- rs_testing.py | 62 +++++++++++++------------- scripts/run_scalable_chain_rsLTL_FI.sh | 34 ++++++++++++++ smt/smt_checker_rsc.py | 8 +++- 4 files changed, 82 insertions(+), 42 deletions(-) create mode 100755 scripts/run_scalable_chain_rsLTL_FI.sh diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index 34ff47e..312b2d9 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -117,8 +117,8 @@ class rsLTL_Encoder(object): # level == bound enc = False for loop_level in range(1, bound+1): - enc = Or(enc, And(self.loop_position == loop_level, - self.encode(formula.left_operand, loop_level, bound))) + enc = simplify(Or(enc, And(self.loop_position == loop_level, + self.encode(formula.left_operand, loop_level, bound)))) enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level)) enc = simplify(enc) @@ -135,12 +135,12 @@ class rsLTL_Encoder(object): # level == bound enc_loops = False for loop_level in range(1, bound+1): - enc_loops = Or(enc_loops, + enc_loops = simplify(Or(enc_loops, And( self.loop_position == loop_level, self.encode_approx(formula, loop_level, bound), ) - ) + )) enc = And( self.encode(formula.left_operand, bound, bound), enc_loops, @@ -163,12 +163,12 @@ class rsLTL_Encoder(object): # level == bound enc_loops = False for loop_level in range(1, bound+1): - enc_loops = Or(enc_loops, + enc_loops = simplify(Or(enc_loops, And( self.loop_position == loop_level, self.encode_approx(formula, loop_level, bound), ) - ) + )) #print(enc) enc = Or(self.encode(formula.left_operand, bound, bound), And( @@ -188,12 +188,12 @@ class rsLTL_Encoder(object): # level == bound inner_enc = False for loop_level in range(1, bound+1): - inner_enc = Or(inner_enc, + inner_enc = simplify(Or(inner_enc, And( self.loop_position == loop_level, self.encode_approx(formula, loop_level, bound) ) - ) + )) enc = Or( self.encode(formula.right_operand, level, bound), @@ -213,12 +213,12 @@ class rsLTL_Encoder(object): # level == bound inner_enc = False for loop_level in range(1, bound+1): - inner_enc = Or(inner_enc, + inner_enc = simplify(Or(inner_enc, And( self.loop_position == loop_level, self.encode_approx(formula, loop_level, bound) ) - ) + )) enc = And( self.encode(formula.right_operand, level, bound), diff --git a/rs_testing.py b/rs_testing.py index a4f23cd..c6dca3d 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -101,16 +101,20 @@ def state_translate_rsc2rs(p): def scalable_chain(print_system=False): - if len(sys.argv) < 1+2: - print("provide ") + 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]) if chainLen < 1 or maxConc < 1: print("be reasonable") exit(1) + if not formula_number in range(1,4+1): + print("formulaNumber must be in 1..4") + exit(1) r = ReactionSystemWithConcentrations() r.add_bg_set_entity(("inc",1)) @@ -141,40 +145,36 @@ def scalable_chain(print_system=False): smt_rsc = SmtCheckerRSC(rc) - prop = [('e_'+str(chainLen),maxConc)] - # smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10) - - # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10) - - # (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) - - # (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) - - # (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(i)) == maxConc) - # ) - # ) - # ) - # smt_rsc.check_rsltl(formula=f_3) + 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(i)) == maxConc) + ) + ) + ) + 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) ########################################################################### time=0 mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_rsc_time.log" - filename_m="bench_rsc_mem.log" + 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') diff --git a/scripts/run_scalable_chain_rsLTL_FI.sh b/scripts/run_scalable_chain_rsLTL_FI.sh new file mode 100755 index 0000000..e7edb00 --- /dev/null +++ b/scripts/run_scalable_chain_rsLTL_FI.sh @@ -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 + diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 48c6947..9d69adb 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -411,7 +411,13 @@ class SmtCheckerRSC(object): print("[" + colour_str(C_BOLD, "i") + "] Generating the formula encoding...") encoder.init_ncalls() 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...") self.solver.add(f)