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

maxsat

Browse Source
This commit is contained in:
Artur Meski
2017-09-17 20:57:45 +01:00
parent 9501feeb7e
commit 687b1c9cab
2 changed files with 42 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
rs_testing.py
View File

@@ -72,7 +72,7 @@ def simple_param():
rc = ReactionSystemWithAutomaton(r, c) rc = ReactionSystemWithAutomaton(r, c)
rc.show() rc.show()
smt_rsc = SmtCheckerRSCParam(rc) smt_rsc = SmtCheckerRSCParam(rc, optimise=True)
f1 = Formula_rsLTL.f_F( f1 = Formula_rsLTL.f_F(
BagDescription.f_TRUE(), BagDescription.f_TRUE(),

58
smt/smt_checker_rsc_param.py
View File

@@ -21,7 +21,7 @@ def z3_max(a, b):
class SmtCheckerRSCParam(object): class SmtCheckerRSCParam(object):
def __init__(self, rsca): def __init__(self, rsca, optimise=False):
rsca.sanity_check() rsca.sanity_check()
@@ -31,6 +31,8 @@ class SmtCheckerRSCParam(object):
self.rs = rsca.rs self.rs = rsca.rs
self.ca = rsca.ca self.ca = rsca.ca
self.optimise = optimise
self.initialise() self.initialise()
def initialise(self): def initialise(self):
@@ -59,6 +61,10 @@ class SmtCheckerRSCParam(object):
# improducible - entities that are never produces (there is no reaction that produces that entity) # improducible - entities that are never produces (there is no reaction that produces that entity)
self.loop_position = Int("loop_position") self.loop_position = Int("loop_position")
if self.optimise:
self.solver = Optimize()
else:
self.solver = Solver() #For("QF_FD") self.solver = Solver() #For("QF_FD")
self.verification_time = None self.verification_time = None
@@ -206,6 +212,12 @@ class SmtCheckerRSCParam(object):
return simplify(And(enc_param_gz, enc_non_empty)) return simplify(And(enc_param_gz, enc_non_empty))
def assert_param_optimisation(self):
for param_vars in self.v_param.values():
for pvar in param_vars:
self.solver.add_soft(pvar < 1)
def enc_concentration_levels_assertion(self, level): def enc_concentration_levels_assertion(self, level):
""" """
Encodes assertions that (some) variables need to be >=0 Encodes assertions that (some) variables need to be >=0
@@ -452,7 +464,6 @@ class SmtCheckerRSCParam(object):
return enc_trans return enc_trans
def enc_exact_state(self, level, state): def enc_exact_state(self, level, state):
"""Encodes the state at the given level with the exact concentration values""" """Encodes the state at the given level with the exact concentration values"""
@@ -583,19 +594,22 @@ class SmtCheckerRSCParam(object):
start = resource.getrusage(resource.RUSAGE_SELF).ru_utime start = resource.getrusage(resource.RUSAGE_SELF).ru_utime
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add(self.enc_init_state(0)) self.solver_add(self.enc_init_state(0))
self.current_level = 0 self.current_level = 0
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add(self.enc_concentration_levels_assertion(0)) self.solver_add(self.enc_concentration_levels_assertion(0))
self.solver.add(self.enc_param_concentration_levels_assertion()) self.solver_add(self.enc_param_concentration_levels_assertion())
if self.optimise:
self.assert_param_optimisation()
encoder = rsLTL_Encoder(self) encoder = rsLTL_Encoder(self)
while True: while True:
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add( self.solver_add(
self.enc_concentration_levels_assertion( self.enc_concentration_levels_assertion(
self.current_level + 1)) self.current_level + 1))
@@ -619,11 +633,11 @@ class SmtCheckerRSCParam(object):
"] Adding the formula to the solver...") "] Adding the formula to the solver...")
encoder.flush_cache() encoder.flush_cache()
self.solver.add(f) self.solver_add(f)
print("[" + colour_str(C_BOLD, "i") + print("[" + colour_str(C_BOLD, "i") +
"] Adding the loops encoding...") "] Adding the loops encoding...")
self.solver.add(self.get_loop_encodings()) self.solver_add(self.get_loop_encodings())
result = self.solver.check() result = self.solver.check()
if result == sat: if result == sat:
@@ -642,7 +656,7 @@ class SmtCheckerRSCParam(object):
print("[" + colour_str(C_BOLD, "i") + print("[" + colour_str(C_BOLD, "i") +
"] Unrolling the transition relation") "] Unrolling the transition relation")
self.solver.add(self.enc_transition_relation(self.current_level)) self.solver_add(self.enc_transition_relation(self.current_level))
print( print(
"{:->70}".format("[ level=" + str(self.current_level) + " done ]")) "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
@@ -669,7 +683,6 @@ class SmtCheckerRSCParam(object):
resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
(1024 * 1024)) + " MB")) (1024 * 1024)) + " MB"))
def dummy_unroll(self, levels): def dummy_unroll(self, levels):
"""Unrolls the variables for testing purposes""" """Unrolls the variables for testing purposes"""
@@ -680,7 +693,6 @@ class SmtCheckerRSCParam(object):
print(C_MARK_INFO + " Dummy Unrolling done.") print(C_MARK_INFO + " Dummy Unrolling done.")
def state_equality(self, level_A, level_B): def state_equality(self, level_A, level_B):
"""Encodes equality of two states at two different levels""" """Encodes equality of two states at two different levels"""
@@ -695,7 +707,6 @@ class SmtCheckerRSCParam(object):
return eq_enc return eq_enc
def get_loop_encodings(self): def get_loop_encodings(self):
k = self.current_level k = self.current_level
@@ -714,6 +725,13 @@ class SmtCheckerRSCParam(object):
return loop_enc return loop_enc
def solver_add(self, expression):
if expression == False:
raise RuntimeError("Trying to assert False.")
if not (expression == True):
self.solver.add(expression)
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):
@@ -726,16 +744,16 @@ class SmtCheckerRSCParam(object):
start = resource.getrusage(resource.RUSAGE_SELF).ru_utime start = resource.getrusage(resource.RUSAGE_SELF).ru_utime
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add(self.enc_init_state(0)) self.solver_add(self.enc_init_state(0))
self.current_level = 0 self.current_level = 0
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add(self.enc_concentration_levels_assertion(0)) self.solver_add(self.enc_concentration_levels_assertion(0))
while True: while True:
self.prepare_all_variables() self.prepare_all_variables()
self.solver.add(self.enc_concentration_levels_assertion(self.current_level+1)) self.solver_add(self.enc_concentration_levels_assertion(self.current_level+1))
print("\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]")) print("\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
stdout.flush() stdout.flush()
@@ -744,7 +762,7 @@ class SmtCheckerRSCParam(object):
print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...") print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")
self.solver.push() self.solver.push()
self.solver.add(self.enc_state_with_blocking(self.current_level,state)) self.solver_add(self.enc_state_with_blocking(self.current_level,state))
result = self.solver.check() result = self.solver.check()
if result == sat: if result == sat:
@@ -757,7 +775,7 @@ class SmtCheckerRSCParam(object):
self.solver.pop() self.solver.pop()
print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation") print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
self.solver.add(self.enc_transition_relation(self.current_level)) self.solver_add(self.enc_transition_relation(self.current_level))
print("{:->70}".format("[ level=" + str(self.current_level) + " done ]")) print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
self.current_level += 1 self.current_level += 1
@@ -790,7 +808,7 @@ class SmtCheckerRSCParam(object):
self.prepare_all_variables() self.prepare_all_variables()
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)
self.current_level = 0 self.current_level = 0
self.prepare_all_variables() self.prepare_all_variables()
@@ -808,7 +826,7 @@ class SmtCheckerRSCParam(object):
s = self.enc_min_state(self.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:
@@ -822,7 +840,7 @@ class SmtCheckerRSCParam(object):
print("[i] Unrolling the transition relation") print("[i] Unrolling the transition relation")
t = self.enc_transition_relation(self.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(self.current_level) + " done ]") print("-----[ level=" + str(self.current_level) + " done ]")
self.current_level += 1 self.current_level += 1