diff --git a/logics/rsltl.py b/logics/rsltl.py index a0bfb17..2de24ec 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -197,8 +197,13 @@ class Encoder_rsLTL(object): def encode_bag_ctx(self, bag_formula, level): return self.encode_bag(bag_formula, level, context=True) - def encode(self, formula, level, bound): + def encode(self, formula, level, bound, loop_level=None): + if loop_level != None and level == bound: + next_level = loop_level + else: + next_level = level + 1 + if not isinstance(formula, Formula_rsLTL): raise NotImplementedError("Unsupported formula type: " + str(type(formula))) @@ -217,36 +222,39 @@ class Encoder_rsLTL(object): elif formula.f_type == rsLTL_form_type.l_and: return And( - self.encode(formula.left_operand, level, bound), - self.encode(formula.right_operand, level, bound) + self.encode(formula.left_operand, level, bound, loop_level), + self.encode(formula.right_operand, level, bound, loop_level) ) 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) + self.encode(formula.left_operand, level, bound, loop_level), + self.encode(formula.right_operand, level, bound, loop_level) ) elif formula.f_type == rsLTL_form_type.t_next: enc = And( - self.encode(formula.left_operand, level+1, bound), + self.encode(formula.left_operand, next_level, bound, loop_level), self.encode_bag_ctx(formula.sub_operand, level) ) return enc elif formula.f_type == rsLTL_form_type.t_globally: enc = And( - self.encode(formula.left_operand, level, bound), + self.encode(formula.left_operand, level, bound, loop_level), self.encode_bag_ctx(formula.sub_operand, level), - self.encode(formula, level+1, bound) + self.encode(formula, next_level, bound, loop_level) ) + # enc = True + # for i in range(level, bound+1): + return enc elif formula.f_type == rsLTL_form_type.t_finally: enc = Or( - self.encode(formula.left_operand, level, bound), + self.encode(formula.left_operand, level, bound, loop_level), And( - self.encode(formula, level+1, bound), + self.encode(formula, next_level, bound, loop_level), self.encode_bag_ctx(formula.sub_operand, level) ) ) @@ -254,10 +262,10 @@ class Encoder_rsLTL(object): elif formula.f_type == rsLTL_form_type.t_until: enc = Or( - self.encode(formula.right_operand, level, bound), + self.encode(formula.right_operand, level, bound, loop_level), And( - self.encode(formula.left_operand, level, bound), - self.encode(formula, level+1, bound), + self.encode(formula.left_operand, level, bound, loop_level), + self.encode(formula, next_level, bound, loop_level), self.encode_bag_ctx(formula.sub_operand, level) ) ) @@ -265,11 +273,11 @@ class Encoder_rsLTL(object): elif formula.f_type == rsLTL_form_type.t_release: enc = And( - self.encode(formula.right_operand, level, bound), + self.encode(formula.right_operand, level, bound, loop_level), Or( - self.encode(formula.left_operand, level, bound), + self.encode(formula.left_operand, level, bound, loop_level), And( - self.encode(formula, level+1, bound), + self.encode(formula, next_level, bound, loop_level), self.encode_bag_ctx(formula.sub_operand, level) ) ) diff --git a/rs_testing.py b/rs_testing.py index a43b558..e45f556 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -31,10 +31,12 @@ def test_rsLTL(): rc = ReactionSystemWithAutomaton(r,c) checker = SmtCheckerRSC(rc) - checker.dummy_unroll(1000) - e = Encoder_rsLTL(checker) + checker.dummy_unroll(10) + #e = Encoder_rsLTL(checker) - print(e.encode(x, 0, 10)) + print(checker.get_loop_encodings()) + + # print(e.encode(x, 0, 10)) def test_extended_automaton(): diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 3550579..932aba3 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -31,6 +31,8 @@ class SmtCheckerRSC(object): self.ca_state = [] self.next_level_to_encode = 0 + self.loop_position = Int("loop_position") + self.solver = Solver() self.verification_time = None @@ -370,11 +372,41 @@ class SmtCheckerRSC(object): def dummy_unroll(self, levels): """Unrolls the variables for testing purposes""" - - for i in range(levels): - self.prepare_all_variables() - print(C_MARK_INFO + " Dummy Unrolling done.") + self.current_level = 0 + for i in range(levels+1): + self.prepare_all_variables() + self.current_level += 1 + + print(C_MARK_INFO + " Dummy Unrolling done.") + + def state_equality(self, level_A, level_B): + """Encodes equality of two states at two different levels""" + + eq_enc = True + + print(level_A, level_B, self.current_level) + print(len(self.v), self.v) + + for e_i in range(len(self.rs.background_set)): + e_i_equality = self.v[level_A][e_i] == self.v[level_B][e_i] + eq_enc = simplify(And(eq_enc, e_i_equality)) + + return eq_enc + + def get_loop_encodings(self): + + k = self.current_level-1 # TODO: cos jest pokichane z tymi indeksami. sprawdzic. zasypiam. + loop_var = self.loop_position + + loop_k = True + for i in range(1,k+1): + loop_k = simplify(And(loop_k, Implies( loop_var == i, self.state_equality(i-1, k) ))) + + loop_enc = loop_k + + return loop_enc + def check_reachability(self, state, print_witness=True, print_time=True, print_mem=True, max_level=1000): """Main testing function""" @@ -445,43 +477,43 @@ class SmtCheckerRSC(object): init_s = self.enc_init_state(0) print(init_s) self.solver.add(init_s) - current_level = 0 + self.current_level = 0 self.prepare_all_variables() while True: self.prepare_all_variables() - print("-----[ Working at level=" + str(current_level) + " ]-----") + print("-----[ Working at level=" + str(self.current_level) + " ]-----") stdout.flush() # reachability test: print("[i] Adding the reachability test...") self.solver.push() - s = self.enc_min_state(current_level,state) + s = self.enc_min_state(self.current_level,state) print("Test: ", s) self.solver.add(s) result = self.solver.check() if result == sat: - print("\n[+] " + colour_str(C_RED, "SAT at level=" + str(current_level))) + print("\n[+] " + colour_str(C_RED, "SAT at level=" + str(self.current_level))) if print_witness: - self.decode_witness(current_level) + self.decode_witness(self.current_level) break else: self.solver.pop() print("[i] Unrolling the transition relation") - t = self.enc_transition_relation(current_level) + t = self.enc_transition_relation(self.current_level) print(t) self.solver.add(t) - print("-----[ level=" + str(current_level) + " done ]") - current_level += 1 + print("-----[ level=" + str(self.current_level) + " done ]") + self.current_level += 1 - if current_level > max_level: + if self.current_level > max_level: print("Stopping at level=" + str(max_level)) break else: