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

working on the new encoding; backup commit

Browse Source
This commit is contained in:
Artur Meski
2017-03-09 23:06:44 +01:00
parent f70cc0034b
commit 97ff4baf35
3 changed files with 74 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
logics/rsltl.py
View File

@@ -197,8 +197,13 @@ class Encoder_rsLTL(object):
def encode_bag_ctx(self, bag_formula, level): def encode_bag_ctx(self, bag_formula, level):
return self.encode_bag(bag_formula, level, context=True) 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): if not isinstance(formula, Formula_rsLTL):
raise NotImplementedError("Unsupported formula type: " + str(type(formula))) 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: elif formula.f_type == rsLTL_form_type.l_and:
return And( return And(
self.encode(formula.left_operand, level, bound), self.encode(formula.left_operand, level, bound, loop_level),
self.encode(formula.right_operand, level, bound) self.encode(formula.right_operand, level, bound, loop_level)
) )
elif formula.f_type == rsLTL_form_type.l_or: elif formula.f_type == rsLTL_form_type.l_or:
return Or( return Or(
self.encode(formula.left_operand, level, bound), self.encode(formula.left_operand, level, bound, loop_level),
self.encode(formula.right_operand, level, bound) self.encode(formula.right_operand, level, bound, loop_level)
) )
elif formula.f_type == rsLTL_form_type.t_next: elif formula.f_type == rsLTL_form_type.t_next:
enc = And( 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) self.encode_bag_ctx(formula.sub_operand, level)
) )
return enc return enc
elif formula.f_type == rsLTL_form_type.t_globally: elif formula.f_type == rsLTL_form_type.t_globally:
enc = And( 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_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 return enc
elif formula.f_type == rsLTL_form_type.t_finally: elif formula.f_type == rsLTL_form_type.t_finally:
enc = Or( enc = Or(
self.encode(formula.left_operand, level, bound), self.encode(formula.left_operand, level, bound, loop_level),
And( And(
self.encode(formula, level+1, bound), self.encode(formula, next_level, bound, loop_level),
self.encode_bag_ctx(formula.sub_operand, 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: elif formula.f_type == rsLTL_form_type.t_until:
enc = Or( enc = Or(
self.encode(formula.right_operand, level, bound), self.encode(formula.right_operand, level, bound, loop_level),
And( And(
self.encode(formula.left_operand, level, bound), self.encode(formula.left_operand, level, bound, loop_level),
self.encode(formula, level+1, bound), self.encode(formula, next_level, bound, loop_level),
self.encode_bag_ctx(formula.sub_operand, 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: elif formula.f_type == rsLTL_form_type.t_release:
enc = And( enc = And(
self.encode(formula.right_operand, level, bound), self.encode(formula.right_operand, level, bound, loop_level),
Or( Or(
self.encode(formula.left_operand, level, bound), self.encode(formula.left_operand, level, bound, loop_level),
And( And(
self.encode(formula, level+1, bound), self.encode(formula, next_level, bound, loop_level),
self.encode_bag_ctx(formula.sub_operand, level) self.encode_bag_ctx(formula.sub_operand, level)
) )
) )

8
rs_testing.py
View File

@@ -31,10 +31,12 @@ def test_rsLTL():
rc = ReactionSystemWithAutomaton(r,c) rc = ReactionSystemWithAutomaton(r,c)
checker = SmtCheckerRSC(rc) checker = SmtCheckerRSC(rc)
checker.dummy_unroll(1000) checker.dummy_unroll(10)
e = Encoder_rsLTL(checker) #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(): def test_extended_automaton():

58
smt/smt_checker_rsc.py
View File

@@ -31,6 +31,8 @@ class SmtCheckerRSC(object):
self.ca_state = [] self.ca_state = []
self.next_level_to_encode = 0 self.next_level_to_encode = 0
self.loop_position = Int("loop_position")
self.solver = Solver() self.solver = Solver()
self.verification_time = None self.verification_time = None
@@ -370,11 +372,41 @@ class SmtCheckerRSC(object):
def dummy_unroll(self, levels): def dummy_unroll(self, levels):
"""Unrolls the variables for testing purposes""" """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, def check_reachability(self, state, print_witness=True,
print_time=True, print_mem=True, max_level=1000): print_time=True, print_mem=True, max_level=1000):
"""Main testing function""" """Main testing function"""
@@ -445,43 +477,43 @@ class SmtCheckerRSC(object):
init_s = self.enc_init_state(0) init_s = self.enc_init_state(0)
print(init_s) print(init_s)
self.solver.add(init_s) self.solver.add(init_s)
current_level = 0 self.current_level = 0
self.prepare_all_variables() self.prepare_all_variables()
while True: while True:
self.prepare_all_variables() self.prepare_all_variables()
print("-----[ Working at level=" + str(current_level) + " ]-----") print("-----[ Working at level=" + str(self.current_level) + " ]-----")
stdout.flush() stdout.flush()
# reachability test: # reachability test:
print("[i] Adding the reachability test...") print("[i] Adding the reachability test...")
self.solver.push() self.solver.push()
s = self.enc_min_state(current_level,state) s = self.enc_min_state(self.current_level,state)
print("Test: ", s) print("Test: ", s)
self.solver.add(s) self.solver.add(s)
result = self.solver.check() result = self.solver.check()
if result == sat: 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: if print_witness:
self.decode_witness(current_level) self.decode_witness(self.current_level)
break break
else: else:
self.solver.pop() self.solver.pop()
print("[i] Unrolling the transition relation") print("[i] Unrolling the transition relation")
t = self.enc_transition_relation(current_level) t = self.enc_transition_relation(self.current_level)
print(t) print(t)
self.solver.add(t) self.solver.add(t)
print("-----[ level=" + str(current_level) + " done ]") print("-----[ level=" + str(self.current_level) + " done ]")
current_level += 1 self.current_level += 1
if current_level > max_level: if self.current_level > max_level:
print("Stopping at level=" + str(max_level)) print("Stopping at level=" + str(max_level))
break break
else: else: