From 20464ac6ddb997379921ded63add65857650dfa4 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 12 Mar 2017 12:50:09 +0100 Subject: [PATCH] bugfix for F and G encodings -- missing element for i=k --- logics/rsltl.py | 4 +-- logics/rsltl_encoder.py | 73 ++++++++++++++++++++++++++++++++--------- rs_testing.py | 18 +++++----- smt/smt_checker_rsc.py | 22 +++++++------ 4 files changed, 82 insertions(+), 35 deletions(-) diff --git a/logics/rsltl.py b/logics/rsltl.py index 98960f5..d636817 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -61,8 +61,8 @@ class Formula_rsLTL(object): return cls(rsLTL_form_type.t_until, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) @classmethod - def f_F(cls, sub, arg_L, arg_R): - return cls(rsLTL_form_type.t_finally, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) + def f_F(cls, sub, arg_L): + return cls(rsLTL_form_type.t_finally, L_oper = arg_L, sub_oper = sub) @classmethod def f_R(cls, sub, arg_L, arg_R): diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index b9f6d00..9171e46 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -93,7 +93,7 @@ class rsLTL_Encoder(object): else: # level == bound enc = False - for loop_level in range(1, bound): + 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 = And(enc, self.encode_bag_ctx(formula.sub_operand, level)) @@ -110,13 +110,20 @@ class rsLTL_Encoder(object): ) else: # level == bound - enc = False - for loop_level in range(1, bound): - enc = Or(enc, And(self.loop_position == loop_level), - self.encode_approx(formula, loop_level, bound), + enc_loops = False + for loop_level in range(1, bound+1): + enc_loops = Or(enc, + And( + self.loop_position == loop_level, + self.encode_approx(formula, loop_level, bound), + ) ) - enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level)) - enc = simplify(enc) + enc = And( + self.encode(formula.left_operand, bound, bound), + enc_loops, + self.encode_bag_ctx(formula.sub_operand, level) + ) + enc = simplify(enc) return enc @@ -131,14 +138,22 @@ class rsLTL_Encoder(object): ) else: # level == bound - enc = False - for loop_level in range(1, bound): - enc = Or(enc, + enc_loops = False + for loop_level in range(1, bound+1): + enc_loops = Or(enc_loops, And( - self.loop_position == loop_level), + self.loop_position == loop_level, self.encode_approx(formula, loop_level, bound), + ) ) - enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level)) + #print(enc) + enc = Or(self.encode(formula.left_operand, bound, bound), + And( + enc_loops, + self.encode_bag_ctx(formula.sub_operand, level) + ) + ) + enc = simplify(enc) return enc @@ -149,7 +164,7 @@ class rsLTL_Encoder(object): else: # level == bound inner_enc = False - for loop_level in range(1, bound): + for loop_level in range(1, bound+1): inner_enc = Or(inner_enc, And( self.loop_position == loop_level, @@ -174,7 +189,7 @@ class rsLTL_Encoder(object): else: # level == bound inner_enc = False - for loop_level in range(1, bound): + for loop_level in range(1, bound+1): inner_enc = Or(inner_enc, And( self.loop_position == loop_level, @@ -193,7 +208,6 @@ class rsLTL_Encoder(object): ) ) - return enc else: @@ -238,6 +252,35 @@ class rsLTL_Encoder(object): return enc + elif formula.f_type == rsLTL_form_type.t_globally: + if level < bound: + enc = And( + self.encode(formula.left_operand, level, bound), + self.encode_bag_ctx(formula.sub_operand, level), + self.encode_approx(formula, level + 1, bound) + ) + else: + # level == bound + enc = self.encode(formula.left_operand, bound, bound) + + return enc + + elif formula.f_type == rsLTL_form_type.t_finally: + if level < bound: + enc = Or( + self.encode(formula.left_operand, level, bound), + And( + self.encode_bag_ctx(formula.sub_operand, level), + self.encode_approx(formula, level + 1, bound) + ) + ) + else: + # level == bound + enc = self.encode(formula.left_operand, bound, bound) + + return enc + + else: raise NotImplementedError("Unsupported operator in approximation encoding") diff --git a/rs_testing.py b/rs_testing.py index 129a67c..3eb2bc4 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -12,26 +12,28 @@ def run_tests(): def test_rsLTL(): r = ReactionSystemWithConcentrations() - r.add_bg_set_entity(("a",2)) r.add_bg_set_entity(("inc",2)) - r.add_bg_set_entity(("dec",2)) - r.add_bg_set_entity(("ent1",5)) - r.add_bg_set_entity(("ent2",3)) - r.add_bg_set_entity(("ent3",3)) + r.add_bg_set_entity(("ent2",5)) + r.add_reaction([("ent2",1),("inc",1)],[],[("ent2",2)]) + r.add_reaction([("ent2",2)],[],[("ent2",2)]) c = ContextAutomatonWithConcentrations(r) c.add_init_state("init") c.add_state("working") - c.add_transition("init", [("a",1),("inc",1)], "working") + c.add_transition("init", [("ent2",1),("inc",1)], "working") c.add_transition("working", [("inc",1)], "working") # x = ( Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) - x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) + # x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) + + x = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("ent2") == 2) ) + print(x) rc = ReactionSystemWithAutomaton(r,c) - checker = SmtCheckerRSC(rc) + rc.show() + checker = SmtCheckerRSC(rc) checker.check_rsltl(formula=x) # checker.dummy_unroll(10) diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 1ca4d07..42bd98d 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -376,7 +376,7 @@ class SmtCheckerRSC(object): self.prepare_all_variables() self.solver.add(self.enc_init_state(0)) - current_level = 0 + self.current_level = 0 self.prepare_all_variables() @@ -386,34 +386,36 @@ class SmtCheckerRSC(object): while True: self.prepare_all_variables() - self.solver.add(self.enc_concentration_levels_assertion(current_level+1)) + self.solver.add(self.enc_concentration_levels_assertion(self.current_level+1)) - print("\n{:-^70}".format("[ Working at level=" + str(current_level) + " ]")) + print("\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]")) stdout.flush() # reachability test: print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...") self.solver.push() - self.solver.add(encoder.encode(formula, 0, current_level)) + f = encoder.encode(formula, 0, self.current_level) + self.solver.add(f) + self.solver.add(self.get_loop_encodings()) result = self.solver.check() if result == sat: - print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(current_level))) + print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(self.current_level))) if print_witness: print("\n{:=^70}".format("[ WITNESS ]")) - self.decode_witness(current_level) + self.decode_witness(self.current_level) break else: self.solver.pop() print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation") - self.solver.add(self.enc_transition_relation(current_level)) + self.solver.add(self.enc_transition_relation(self.current_level)) - print("{:->70}".format("[ level=" + str(current_level) + " done ]")) - current_level += 1 + print("{:->70}".format("[ level=" + str(self.current_level) + " done ]")) + self.current_level += 1 - if not max_level is None and current_level > max_level: + if not max_level is None and self.current_level > max_level: print("Stopping at level=" + str(max_level)) break