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

bugfix for F and G encodings -- missing element for i=k

Browse Source
This commit is contained in:
Artur Meski
2017-03-12 12:50:09 +01:00
parent fab7880ccf
commit 20464ac6dd
4 changed files with 82 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
logics/rsltl.py
View File

@@ -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):

71
logics/rsltl_encoder.py
View File

@@ -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,12 +110,19 @@ 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 = 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")

18
rs_testing.py
View File

@@ -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)

22
smt/smt_checker_rsc.py
View File

@@ -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