diff --git a/logics/rsltl.py b/logics/rsltl.py index 78a3e78..daefcab 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -3,8 +3,7 @@ from enum import Enum from logics.bags import * -rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not t_globally t_finally t_next t_until t_release') - +rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release') class Formula_rsLTL(object): @@ -35,6 +34,8 @@ class Formula_rsLTL(object): return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.l_or: return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )" + if self.f_type == rsLTL_form_type.l_implies: + return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.t_until: return "( " + repr(self.left_operand) + " U[" + repr(self.sub_operand) + "]" + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.t_release: @@ -68,6 +69,10 @@ class Formula_rsLTL(object): def f_R(cls, sub, arg_L, arg_R): return cls(rsLTL_form_type.t_release, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) + @classmethod + def f_Implies(cls, arg_L, arg_R): + return cls(rsLTL_form_type.l_implies, L_oper = arg_L, R_oper = arg_R) + def __and__(self, other): return Formula_rsLTL(rsLTL_form_type.l_and, L_oper = self, R_oper = other) diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index 3ce55dd..34ff47e 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -1,5 +1,8 @@ from logics.rsltl import * +def simplify(x): + return x + class rsLTL_Encoder(object): """Class for encoding rsLTL formulae for a given smt_checker instance""" @@ -10,8 +13,20 @@ class rsLTL_Encoder(object): self.rs = smt_checker.rs self.loop_position = smt_checker.loop_position + self.init_ncalls() + + def init_ncalls(self): + self.ncalls_encode = 0 + self.ncalls_encode_approx = 0 + + def get_ncalls(self): + return (self.ncalls_encode, self.ncalls_encode_approx) + def encode_bag(self, bag_formula, level, context=False): - + + if not bag_formula: + raise RuntimeError("bag_formula is None") + if bag_formula.f_type == BagDesc_oper.entity: entity_id = self.rs.get_entity_id(bag_formula.entity) if context: @@ -56,6 +71,8 @@ class rsLTL_Encoder(object): def encode(self, formula, level, bound): + self.ncalls_encode += 1 + if not isinstance(formula, Formula_rsLTL): raise NotImplementedError("Unsupported formula type: " + str(type(formula))) @@ -76,20 +93,26 @@ class rsLTL_Encoder(object): return And( self.encode(formula.left_operand, level, bound), self.encode(formula.right_operand, level, bound) - ) + ) elif formula.f_type == rsLTL_form_type.l_or: return Or( self.encode(formula.left_operand, level, bound), self.encode(formula.right_operand, level, bound) - ) + ) + elif formula.f_type == rsLTL_form_type.l_implies: + return Implies( + self.encode(formula.left_operand, level, bound), + self.encode(formula.right_operand, level, bound) + ) + elif formula.f_type == rsLTL_form_type.t_next: if level < bound: enc = And( self.encode(formula.left_operand, level + 1, bound), self.encode_bag_ctx(formula.sub_operand, level) - ) + ) else: # level == bound enc = False @@ -107,22 +130,22 @@ class rsLTL_Encoder(object): self.encode(formula.left_operand, level, bound), self.encode_bag_ctx(formula.sub_operand, level), self.encode(formula, level + 1, bound) - ) + ) else: # level == bound enc_loops = False for loop_level in range(1, bound+1): enc_loops = Or(enc_loops, - And( - self.loop_position == loop_level, - self.encode_approx(formula, loop_level, bound), - ) + And( + self.loop_position == loop_level, + self.encode_approx(formula, loop_level, bound), ) - enc = And( - self.encode(formula.left_operand, bound, bound), - enc_loops, - self.encode_bag_ctx(formula.sub_operand, level) ) + enc = And( + self.encode(formula.left_operand, bound, bound), + enc_loops, + self.encode_bag_ctx(formula.sub_operand, level) + ) enc = simplify(enc) return enc @@ -218,6 +241,9 @@ class rsLTL_Encoder(object): Used by encode() """ + + self.ncalls_encode_approx += 1 + if formula.f_type == rsLTL_form_type.t_until: if level < bound: enc = Or( diff --git a/rs_testing.py b/rs_testing.py index 6f645f0..a4f23cd 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -9,7 +9,8 @@ def run_tests(): # test_extended_automaton() # process() - heat_shock_response() + # heat_shock_response() + scalable_chain(print_system=True) def heat_shock_response(print_system=True): @@ -96,7 +97,97 @@ 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+2: + print("provide ") + exit(1) + + chainLen=int(sys.argv[1]) # chain length + maxConc=int(sys.argv[2]) # depth (max concentration) + + if chainLen < 1 or maxConc < 1: + print("be reasonable") + 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) + + 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) + + ########################################################################### + + 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" + 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() + + def test_rsLTL(): r = ReactionSystemWithConcentrations() diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 849aa4f..48c6947 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -383,6 +383,7 @@ class SmtCheckerRSC(object): self.reset() print("[" + colour_str(C_BOLD, "i") + "] Running rsLTL bounded model checking") + print("[" + colour_str(C_BOLD, "i") + "] Formula: " + str(formula)) if print_time: # start = time() @@ -407,8 +408,11 @@ class SmtCheckerRSC(object): # reachability test: self.solver.push() - print("[" + colour_str(C_BOLD, "i") + "] Adding the formula encoding...") + 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())) + print("[" + colour_str(C_BOLD, "i") + "] Adding the formula to the solver...") self.solver.add(f) print("[" + colour_str(C_BOLD, "i") + "] Adding the loops encoding...")